Grip.Parser: ungraded face for graded parsers

Parser α is GParser fallible α: the idempotent fallible grade satisfies Grade.mul fallible fallible = fallible and Grade.choice fallible fallible = fallible (both verified by #guard in Grip.Grade), so standard Monad and Alternative instances work here with grade tracking disabled.

GParser.weakenFallible bridges the precise graded layer: the CoeOut instance makes the coercion transparent, so any GParser g α can be used where a Parser α is expected.

gdo: graded do-notation

gdo desugars let x ← p and bare p lines into GParser.bind/GParser.pure calls, preserving the exact product grade in the elaborated term instead of collapsing everything to fallible. An optional trailing grade_by proof coerces the elaborated grade to the expected one via GParser.gcast.

gdo does not yet support match expressions inside the block; use explicit GParser.bind p fun | .foo => ... calls in that case.

@[reducible, inline]

abbrev Grip.Parser (α : Type) : Type

The ungraded parser type: GParser at the idempotent fallible grade (errors = possibly, consumes = possibly). Standard Monad and Alternative instances work here because Grade.mul fallible fallible = fallible definitionally.

Equations

• Grip.Parser α = Grip.GParser fallible α

Monad instance

@[instance_reducible]

instance Grip.instMonadParser : Monad Parser

Monad instance for Parser. pure wraps a value with GParser.weakenFallible ∘ GParser.pure; bind sequences two Parser actions, weakening the fallible * fallible result grade back to fallible.

Equations

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

Alternative instance

@[instance_reducible]

instance Grip.instAlternativeParser : Alternative Parser

Alternative instance for Parser. failure is GParser.fail weakened to fallible; orElse uses GParser.alt and weakens the choice result to fallible.

Equations

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

Coercion from precisely-graded parsers

@[instance_reducible]

instance Grip.instCoeOutGParserParser {g : Grade} {α : Type} : CoeOut (GParser g α) (Parser α)

Any GParser g α coerces silently to Parser α via GParser.weakenFallible, so precise graded parsers can be used wherever Parser is expected without explicit casts.

We use CoeOut rather than Coe because in Lean 4.28 Coe's first parameter is semiOutParam, which would require the grade g to be determined from the destination type alone; impossible when g is free. CoeOut applies "left-to-right" (source known → determine destination), which is exactly our direction.

Equations

• Grip.instCoeOutGParserParser = { coe := Grip.GParser.weakenFallible }

Grade cast helper

@[inline]

def Grip.GParser.gcast {g g' : Grade} {α : Type} (h : g = g') (p : GParser g α) : GParser g' α

Cast a parser's grade via an equality proof. Used by the grade_by tail of gdo blocks to coerce the elaborated product grade to the expected type.

Equations

• Grip.GParser.gcast h p = h ▸ p

Top-level entry point

def Grip.GParser.parse {g : Grade} {α : Type} (p : GParser g α) (arr : ByteArray) : Except ParseError α

Run a parser from offset 0, returning a positioned ParseError on failure. Line and column are 1-based byte positions derived by scanning arr for newlines.

Equations

• p.parse arr = match p.run arr 0 with | Grip.ParseResult.ok a newOffset => Except.ok a | Grip.ParseResult.error e => Except.error (Grip.mkParseError arr e)

MonadExcept instance

def Grip.GParser.throwErr {α : Type} (e : Err) : Parser α

throw at fallible grade: immediately fail with the supplied labels, its offset set to the current position.

Equations

• Grip.GParser.throwErr e = { run := fun (x : ByteArray) (p : Nat) => Grip.ParseResult.error { pos := p, expected := e.expected }, cwit := ⋯, ewit := ⋯, swit := ⋯, bwit := ⋯, fwit := ⋯ }

def Grip.GParser.tryCatch {α : Type} (p : Parser α) (h : Err → Parser α) : Parser α

tryCatch at fallible grade: run p; on success pass through; on failure call the handler h and run its result from the same offset.

Equations

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

@[instance_reducible]

instance Grip.instMonadExceptErrParser : MonadExcept Err Parser

Equations

• Grip.instMonadExceptErrParser = { throw := fun {α : Type} (e : Grip.Err) => Grip.GParser.throwErr e, tryCatch := fun {α : Type} => Grip.GParser.tryCatch }

def doElemGrade_by_ : Lean.ParserDescr

Trailing element in a gdo block: supply an equality proof to coerce the elaborated grade to the expected type. Example:

gdo
  let a ← p
  q a
  grade_by by rfl

Equations

• doElemGrade_by_ = Lean.ParserDescr.node `doElemGrade_by_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "grade_by ") (Lean.ParserDescr.cat `term 0))

def gdoNotation : Lean.ParserDescr

Graded do-notation over GParser: desugars a do-like block into GParser.bind/GParser.pure calls, preserving the exact product grade.

Supported forms:

• let x ← p: binds p's result via GParser.bind
• let x : T ← p: same with type annotation
• let x := e: local let-binding, no parser action
• bare p (non-final): sequences via GParser.bind _ fun _ => ...
• return e (final): wraps e in GParser.pure
• bare p (final): the parser expression itself
• grade_by proof (optional final): coerces the elaborated grade via GParser.gcast

Example:

-- grade is `conditional`, not collapsed to `fallible`
def twoBytes : GParser conditional (UInt8 × UInt8) :=
  gdo
    let a ← GParser.satisfy (fun _ => true)
    let b ← GParser.satisfy (fun _ => true)
    return (a, b)

Note: match inside gdo is not yet supported; use explicit GParser.bind with a lambda instead.

Equations

• gdoNotation = Lean.ParserDescr.node `gdoNotation 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "gdo ") (Lean.ParserDescr.const `doSeq))

def expandGDo : Lean.Macro

Equations

• expandGDo stx = do let a ← expandGDoBlock✝ stx[1] Pure.pure a.raw

Sanity guards.