Grip.Error: the parser result type and parse errors

ParseResult α is the result of running a parser at an offset: ok value newOffset or error e. One constructor holds the value and offset inline, so a successful step allocates a single object.

Err is the error value carried by ParseResult.error. GParser proves that its byte offset lies between the parser's starting offset and the end of the input. Built-in choice additionally uses it to report the furthest failure and the labels expected there; that stronger diagnostic convention is not part of the parser contract.

ParseError is the user-facing error produced by GParser.parse; it adds 1-based line and col computed from the source bytes.

Nothing in this file imports from Grip; only core Lean / Batteries.

structure Grip.Err : Type

The error value carried by ParseResult.error.

For every GParser run started in bounds, pos lies between that starting offset and the end of the input. Built-in combinators use pos for the furthest byte offset reached during parsing and expected for labels attached by label/<?>; the type does not prove that either diagnostic is maximal or complete.

• pos : Nat

  Diagnostic offset used by built-in failure merging.

• expected : List String

  Labels expected at pos in built-in diagnostics.

def Grip.instReprErr.repr : Err → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Grip.instReprErr : Repr Err

Equations

• Grip.instReprErr = { reprPrec := Grip.instReprErr.repr }

def Grip.instDecidableEqErr.decEq (x✝ x✝¹ : Err) : Decidable (x✝ = x✝¹)

Equations

• Grip.instDecidableEqErr.decEq { pos := a, expected := a_1 } { pos := b, expected := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Grip.instDecidableEqErr : DecidableEq Err

Equations

• Grip.instDecidableEqErr = Grip.instDecidableEqErr.decEq

@[instance_reducible]

instance Grip.instBEqErr : BEq Err

Equations

• Grip.instBEqErr = { beq := Grip.instBEqErr.beq }

def Grip.instBEqErr.beq : Err → Err → Bool

Equations

• Grip.instBEqErr.beq { pos := a, expected := a_1 } { pos := b, expected := b_1 } = (a == b && a_1 == b_1)
• Grip.instBEqErr.beq x✝¹ x✝ = false

@[instance_reducible]

instance Grip.instInhabitedErr : Inhabited Err

Equations

• Grip.instInhabitedErr = { default := Grip.instInhabitedErr.default }

inductive Grip.ParseResult (α : Type) : Type

The result of running a parser at an offset: ok value newOffset or error with a diagnostic. One constructor holds the value and the new offset inline, so a successful step allocates a single object rather than an Except.ok wrapping a Prod (the representation Except Err (α × Nat) used before).

• ok {α : Type} (value : α) (newOffset : Nat) : ParseResult α

  Success: the parsed value and the newOffset reached.

• error {α : Type} : Err → ParseResult α

  Failure carrying an Err; built-in combinators retain the furthest one they observe.

@[instance_reducible]

instance Grip.instInhabitedParseResult {α : Type} : Inhabited (ParseResult α)

Equations

• Grip.instInhabitedParseResult = { default := Grip.ParseResult.error default }

structure Grip.ParseError : Type

User-facing positioned parse error, produced by GParser.parse.

• pos : Nat

  Byte offset of the failure.

• line : Nat

  1-based line number (newline = 0x0a).

• col : Nat

  1-based byte column (not grapheme column).

• expected : List String

  Labels collected at the failure position.

@[instance_reducible]

instance Grip.instReprParseError : Repr ParseError

Equations

• Grip.instReprParseError = { reprPrec := Grip.instReprParseError.repr }

def Grip.instReprParseError.repr : ParseError → Nat → Std.Format

Equations

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

def Grip.instDecidableEqParseError.decEq (x✝ x✝¹ : ParseError) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Grip.instDecidableEqParseError : DecidableEq ParseError

Equations

• Grip.instDecidableEqParseError = Grip.instDecidableEqParseError.decEq

def Grip.instBEqParseError.beq : ParseError → ParseError → Bool

Equations

• Grip.instBEqParseError.beq { pos := a, line := a_1, col := a_2, expected := a_3 } { pos := b, line := b_1, col := b_2, expected := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• Grip.instBEqParseError.beq x✝¹ x✝ = false

@[instance_reducible]

instance Grip.instBEqParseError : BEq ParseError

Equations

• Grip.instBEqParseError = { beq := Grip.instBEqParseError.beq }

def Grip.ParseError.message (e : ParseError) : String

Equations

• e.message = match Grip.uniqueStrings✝ e.expected with | [] => "unexpected input" | xs => "expected " ++ " or ".intercalate xs

def Grip.mkParseError (arr : ByteArray) (e : Err) : ParseError

Build a ParseError from a raw Err and the source ByteArray.

Equations

• Grip.mkParseError arr e = match Grip.lineColOf✝ arr e.pos with | (line, col) => { pos := e.pos, line := line, col := col, expected := e.expected }

def Grip.ParseError.pretty (e : ParseError) (src : ByteArray) : String

Render a dependency-free plain fallback as line:col: message, followed by the offending source line and a caret (^). Rich terminal presentation belongs to grip-diagnostics.

Equations

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