Parser errors

The class ParseIt.Error is used throughout the library to report parsing errors. Users are encouraged to provide instances tailored to their applications.

Three general purpose instances are provided:

• Error.Trivial discards all error information.
• Error.Basic records the position and offending token of the furthest error.
• Error.Simple records all error information, without processing.

class ParseIt.HasPos (ι : Type u) (τ : outParam (Type u)) [Std.Iterator ι Id τ] : Type (u + 1)

Position information for error reporting.

• Pos : Type u

  Position type.

• pos : Std.Iter τ → Pos ι

  Current position of an iterator.

class ParseIt.Error (ε ι : Type u) (τ : outParam (Type u)) [Std.Iterator ι Id τ] : Type u

Parser error class

• unexpected it t reports unexpected input at iterator it, optionally with the offending token.
• addMessage e it msg adds information to error e at iterator it.
• merge e₁ e₂ combines the errors of two failed alternatives; by default it keeps e₂.

• unexpected : Std.Iter τ → Option τ → ε
• addMessage : ε → Std.Iter τ → String → ε
• merge : ε → ε → ε

@[reducible, inline]

abbrev ParseIt.Error.Trivial : Type u

Trivial error type: discards all error information.

Equations

• ParseIt.Error.Trivial = ParseIt.Unitᵤ

@[instance_reducible]

instance ParseIt.Error.instTrivial {ι τ : Type u} [Std.Iterator ι Id τ] : Error Trivial ι τ

Equations

• ParseIt.Error.instTrivial = { unexpected := fun (x : Std.Iter τ) (x_1 : Option τ) => PUnit.unit, addMessage := fun (x : ParseIt.Error.Trivial) (x_1 : Std.Iter τ) (x_2 : String) => PUnit.unit }

structure ParseIt.Error.Basic (ι : Type u) {τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : Type u

Basic error type: the position and, optionally, the offending token. Merging keeps the error at the furthest position, preferring the later alternative on ties. Messages are discarded.

• pos : HasPos.Pos ι

  Position of the error.

• token : Option τ

  Offending token, if any.

@[instance_reducible]

instance ParseIt.Error.instBasicOfDecidableLEPos {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] [LE (HasPos.Pos ι)] [DecidableLE (HasPos.Pos ι)] : Error (Basic ι) ι τ

Equations

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

@[instance_reducible]

instance ParseIt.Error.instToStringBasicOfReprPos {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] [Repr τ] [Repr (HasPos.Pos ι)] : ToString (Basic ι)

Equations

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

inductive ParseIt.Error.Simple (ι : Type u) {τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : Type u

Simple error type: records all error information, without processing.

• unexpected {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : HasPos.Pos ι → Option τ → Simple ι

  Unexpected input at a position.

• addMessage {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : Simple ι → HasPos.Pos ι → String → Simple ι

  Error with an additional message at a position.

• merge {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : Simple ι → Simple ι → Simple ι

  Errors from two failed alternatives.

@[instance_reducible]

instance ParseIt.Error.instSimple {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] : Error (Simple ι) ι τ

Equations

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

def ParseIt.Error.Simple.toString {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] [Repr τ] [Repr (HasPos.Pos ι)] : Simple ι → String

Render a simple error, listing alternatives separated by " or ".

Equations

• (ParseIt.Error.Simple.unexpected pos (some t)).toString = toString "unexpected input " ++ toString (repr t) ++ toString " at " ++ toString (repr pos)
• (ParseIt.Error.Simple.unexpected pos none).toString = toString "unexpected input at " ++ toString (repr pos)
• (e.addMessage pos msg).toString = e.toString ++ (toString "; " ++ toString msg ++ toString " at " ++ toString (repr pos))
• (e₁.merge e₂).toString = e₁.toString ++ " or " ++ e₂.toString

@[instance_reducible]

instance ParseIt.Error.instToStringSimpleOfReprPos {ι τ : Type u} [Std.Iterator ι Id τ] [HasPos ι τ] [Repr τ] [Repr (HasPos.Pos ι)] : ToString (Simple ι)

Equations

• ParseIt.Error.instToStringSimpleOfReprPos = { toString := ParseIt.Error.Simple.toString }