Parser Error

The class Parser.Error is used throughout the library for the purpose of reporting parser errors. Users are encouraged to provide their own instances tailored to their applications.

Three general purpose instances are provided:

• Parser.Error.Simple records all parsing error information, without processing.
• Parser.Error.Basic just records the location of the primary parsing error.
• Parser.Error.Trivial discards all parsing error information.

These are intended for use in parser development and as building blocks (or inspiration) for tailored instances.

class Parser.Error (ε : Type u_1) (σ : Type u_2) (τ : outParam (Type u_3)) [Parser.Stream σ τ] : Type (max (max u_1 u_3) u_4)

Parser error class

This class declares an error type for a given parser stream.

Given Parser.Stream σ τ, Parser.Error ε σ τ provides two basic mechanisms for reporting parsing errors:

• unexpected (p : Stream.Position σ) (t : Option τ) : ε is used to report an unexpected input at a given position, optionally with the offending token.
• addMessage (e : ε) (p : Stream.Position σ) (info : String) is used to add additional error information at a given position.

This class can be extended to provide additional error reporting and processing functonality, but only these two mechanisms are used within the library.

• unexpected : Stream.Position σ → Option τ → ε

  Parser error class

  This class declares an error type for a given parser stream.

  Given Parser.Stream σ τ, Parser.Error ε σ τ provides two basic mechanisms for reporting parsing errors:

  • unexpected (p : Stream.Position σ) (t : Option τ) : ε is used to report an unexpected input at a given position, optionally with the offending token.
  • addMessage (e : ε) (p : Stream.Position σ) (info : String) is used to add additional error information at a given position.

  This class can be extended to provide additional error reporting and processing functonality, but only these two mechanisms are used within the library.

• addMessage : ε → Stream.Position σ → String → ε

  Parser error class

  This class declares an error type for a given parser stream.

  Given Parser.Stream σ τ, Parser.Error ε σ τ provides two basic mechanisms for reporting parsing errors:

  • unexpected (p : Stream.Position σ) (t : Option τ) : ε is used to report an unexpected input at a given position, optionally with the offending token.
  • addMessage (e : ε) (p : Stream.Position σ) (info : String) is used to add additional error information at a given position.

  This class can be extended to provide additional error reporting and processing functonality, but only these two mechanisms are used within the library.

@[reducible, inline]

abbrev Parser.Error.Trivial : Type

Trivial error type

This error type simply discards all error information. This is useful for parsers that cannot fail, or where parsing errors are intended to be handled by other means.

Equations

• Parser.Error.Trivial = Unit

instance Parser.Error.instTrivial (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error Trivial σ τ

Equations

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

@[reducible, inline]

abbrev Parser.Error.Basic (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Type (max u_3 u_2)

Basic error type

This error type records the position and, optionally, the offending token where a parsing error occurred; any additional information is discarded. This is useful for parsers where the cause of parsing errors is predictable and only the position of the error is needed for processing.

Equations

• Parser.Error.Basic σ τ = (Parser.Stream.Position σ × Option τ)

instance Parser.Error.instBasic (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error (Basic σ τ) σ τ

Equations

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

instance Parser.Error.instToStringBasicOfReprPosition (σ : Type u_1) (τ : Type u_2) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] : ToString (Basic σ τ)

Equations

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

inductive Parser.Error.Simple (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Type (max u_2 u_3)

Simple error type

This error type simply records all the error information provided, without additional processing. Users are expected to provide any necessary post-processing. This is useful for parser development.

• unexpected {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : Stream.Position σ → Option τ → Simple σ τ

  Unexpected input at position

• addMessage {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] : Simple σ τ → Stream.Position σ → String → Simple σ τ

  Add error message at position

instance Parser.Error.instReprSimpleOfPosition (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Repr (Simple σ τ)

Equations

• Parser.Error.instReprSimpleOfPosition σ τ = { reprPrec := Parser.Error.Simple.reprPrec✝ }

instance Parser.Error.instToStringSimpleOfReprPosition (σ : Type u_1) (τ : Type u_2) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] : ToString (Simple σ τ)

Equations

• Parser.Error.instToStringSimpleOfReprPosition σ τ = { toString := Parser.Error.Simple.toString✝ }

instance Parser.Error.instSimple (σ : Type u_1) (τ : Type u_2) [Parser.Stream σ τ] : Parser.Error (Simple σ τ) σ τ

Equations

• Parser.Error.instSimple σ τ = { unexpected := Parser.Error.Simple.unexpected, addMessage := Parser.Error.Simple.addMessage }