Grip.Grade: the parser grade algebra

structure Grade (tracking error and consumption Modality), the named grades, Grade.mul/Grade.choice, and consumptionWitness with its composition lemmas.

No mathlib. Monoid/Lattice instances for Grade belong in grip-props.

structure Grade : Type

A parser's static grade: whether it may/must produce errors and whether it may/must consume input.

• errors : Modality

  Whether the parser may/must error: never, possibly, or always.

• consumes : Modality

  Whether the parser may/must consume input: never, possibly, or always.

def instDecidableEqGrade.decEq (x✝ x✝¹ : Grade) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqGrade.decEq { errors := a, consumes := a_1 } { errors := b, consumes := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqGrade : DecidableEq Grade

Equations

• instDecidableEqGrade = instDecidableEqGrade.decEq

@[instance_reducible]

instance instReprGrade : Repr Grade

Equations

• instReprGrade = { reprPrec := instReprGrade.repr }

def instReprGrade.repr : Grade → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Grade.conditional : Grade

A parser that always consumes and possibly errors.

Equations

• conditional = { errors := possibly, consumes := always }

@[reducible, inline]

abbrev Grade.flexible : Grade

A parser that possibly consumes and never errors.

Equations

• flexible = { errors := never, consumes := possibly }

@[reducible, inline]

abbrev Grade.fallible : Grade

A parser that possibly consumes and possibly errors.

Equations

• fallible = { errors := possibly, consumes := possibly }

@[reducible, inline]

abbrev Grade.pure : Grade

A parser that never consumes and never errors.

Equations

• Grade.pure = { errors := never, consumes := never }

@[reducible, inline]

abbrev Grade.lookahead : Grade

A parser that never consumes and possibly errors.

Equations

• lookahead = { errors := possibly, consumes := never }

@[reducible, inline]

abbrev Grade.empty : Grade

A parser that never consumes and always errors.

Equations

• empty = { errors := always, consumes := never }

@[reducible, inline]

abbrev Grade.impossible : Grade

The impossible grade: always consumes, never errors. No parser can inhabit this grade on arbitrary input (it must accept empty input).

Equations

• impossible = { errors := never, consumes := always }

@[reducible]

def Grade.mul (a b : Grade) : Grade

Sequential composition: the grade of p >>= q is mul g1 g2, with errors and consumption each being the join of the two grades.

Reducible for the same reason as Modality.sup: goals mentioning a grade product have to stay type-correct at instances transparency.

Equations

• a.mul b = { errors := max a.errors b.errors, consumes := max a.consumes b.consumes }

def Grade.one : Grade

The identity grade for sequential composition: ⟨never, never⟩ = pure.

Equations

• Grade.one = { errors := never, consumes := never }

@[instance_reducible]

instance Grade.instMul : Mul Grade

Equations

• Grade.instMul = { mul := Grade.mul }

@[instance_reducible]

instance Grade.instOne : One Grade

Equations

• Grade.instOne = { one := Grade.one }

def Grade.choice (a b : Grade) : Grade

Ordered-choice grade: errors is the meet (both must agree to fail), consumption is a.errors.ite b.consumes a.consumes (if a always errors, use b's consumption; if a never errors, use a's).

Equations

• a.choice b = { errors := min a.errors b.errors, consumes := a.errors.ite b.consumes a.consumes }

theorem Grade.grade_mul_errors (a b : Grade) : (a * b).errors = max a.errors b.errors

The error grade of a product is the join of the error grades.

theorem Grade.grade_mul_consumes (a b : Grade) : (a * b).consumes = max a.consumes b.consumes

The consumption grade of a product is the join of the consumption grades.

@[reducible, inline]

abbrev consumptionWitness (n m : Nat) : Modality → Prop

Relates the start offset n and end offset m of a successful parse, according to a Modality grade:

• always requires n < m (at least one byte consumed)
• possibly allows n ≤ m (consumed some or none)
• never requires n = m (no input consumed)

Equations

• consumptionWitness n m always = (n < m)
• consumptionWitness n m possibly = (n ≤ m)
• consumptionWitness n m never = (n = m)

theorem consumptionWitness.le {n m : Nat} {a : Modality} (w : consumptionWitness n m a) : n ≤ m

Every consumption witness is monotone in the absolute input offset.

@[simp]

theorem consumptionWitness.rfl {n : Nat} {a : Modality} (h : a ≤ possibly) : consumptionWitness n n a

A reflexive witness holds for any grade a ≤ possibly (i.e. a ≠ always), since no input has been consumed.

theorem consumptionWitness.trans {gc gc' : Modality} {n1 n2 n3 : Nat} (w1 : consumptionWitness n2 n1 gc) (w2 : consumptionWitness n3 n2 gc') : consumptionWitness n3 n1 (max gc gc')

Transitivity: chain two witnesses through a common midpoint. If gc witnesses (n2, n1) and gc' witnesses (n3, n2), then max gc gc' witnesses (n3, n1).

theorem consumptionWitness.ite_left {ge' gc gc' : Modality} {n m : Nat} (c : ge' ≤ possibly) (w : consumptionWitness n m gc') : consumptionWitness n m (ge'.ite gc gc')

If the error grade ge' is at most possibly (i.e. ge' ≠ always), a consumption witness for the second branch gc' lifts to a witness for the ite-computed consumption ge'.ite gc gc'.

theorem consumptionWitness.ite_right {ge' gc gc' : Modality} {n m : Nat} (c : possibly ≤ ge') (w : consumptionWitness n m gc) : consumptionWitness n m (ge'.ite gc gc')

If the error grade ge' is at least possibly (i.e. ge' ≠ never), a consumption witness for the first branch gc lifts to a witness for the ite-computed consumption ge'.ite gc gc'.