5.2. Values and constraints🔗

The analyzable value DSL computes an Int from sign, magnitude, length, and count readers. The analyzable constraints DSL narrows the grammar with arithmetic comparisons, lengths, numeric values, canonical decimal spelling, and count X.

For semantics outside those DSLs, value' accepts an ordinary Lean function returning any type, while constraints' accepts any Boolean Lean predicate. Both can receive scalar captures or repeated-capture List String arguments. Either value form may use ofSpec and toSpec to expose a different application-facing parser result type.

The Cedar-independent Graph example uses value' to produce a structured result:

structure Graph where
  order : Nat
  edges : List (Nat × Nat)

triptych Graph where
  grammar
    Graph ::= Order ":" Cells
    Order ::= digit+
    Cells ::= bit{upperTriangleSize Order}
  value'
    toGraph Order Cells

toGraph : String -> String -> Graph converts the captured order and exact-width cell payload into a vertex count and edge list. A constraints' function can similarly add any decidable format-specific condition that is not expressible in the analyzable constraint DSL.

With value' or constraints', Triptych still proves grammar reconciliation, decidability, typed-view equations, and generated-parser contracts against the supplied functions. Those functions become part of the trusted specification: Lean checks their definitions, but users must ensure that they correctly represent the intended value and constraint.