3.5. One scan per generated parser🔗

The former generated implementation first decided Decimal.IsValid, then called Decimal.computeValue. Both operations could scan the same input. The current parser scans once, checks every constraint against that capture map, and computes the result from those same captures:

def Decimal.parse : String → Option Int64 :=
fun s => scannerParse Decimal.grammar Decimal.constraints Decimal.valueExpr Int64.ofInt s#print Decimal.parse

The generated Decimal.parse_eq_gated theorem proves that this implementation is extensionally equal to the old, readable gated presentation:

Decimal.parse_eq_gated : ∀ (s : String),
  Decimal.parse s = gatedParseOfSpec Decimal.IsValid Decimal.computeValue Int64.ofInt s#check @Decimal.parse_eq_gated
@scannerParseMap_eq_gatedParseOfSpec : ∀ {β δ : Type} (g : Grammar) («constraints» : List ConstraintEntry)
  (valueFn : CaptureMap → β) («ofSpec» : β → δ) (s : String),
  scannerParseMap g «constraints» valueFn «ofSpec» s =
    gatedParseOfSpec (fun input => isWf g «constraints» input ∧ satisfiesConstraints g «constraints» input)
      (scannerComputeValueMap g valueFn) «ofSpec» s#check @Triptych.scannerParseMap_eq_gatedParseOfSpec

Soundness, completeness, exact rejection, typed-view equations, printer roundtrips, and external parser equivalence are therefore unchanged. They now depend on the implementation only through Decimal.parse_eq_gated.