Parser Stream

Parsers read input tokens from a stream. To help with error reporting and backtracking, the Parser.Stream class extends the basic Stream class with functionality to save and restore stream positions.

The simple way to implement backtracking after a parsing error is to first save the stream state before parsing and, upon encountering an error, restore the saved stream state. The issue with this strategy is that each backtrack point adds a reference to the entire stream state. This prevents linear use of the stream state. The Parser.Stream class allows users to work around this issue. The Parser.Stream.Position type is intended to store just enough information to reconstruct the stream state at a save point without having to save the entire stream state.

class Parser.Stream (σ : Type u_1) (τ : outParam (Type u_2)) extends Std.Stream σ τ : Type (max (max u_1 u_2) (u_3 + 1))

Parser stream class

This class extends the basic Stream class with position features needed by parsers for backtracking and error reporting.

• The type Position is used to record position data for the stream type.
• getPosition (s : σ) : Position returns the current position of stream s.
• setPosition (s : σ) (p : Position) : σ restores stream s to position p.

Implementations should try to make the Position type as lightweight as possible for getPosition and setPosition to work properly. Often Position is just a scalar type or another simple type. This may allow for parsers to use the stream state more efficiently.

• next? : σ → Option (τ × σ)
• Position : Type u_3

  Parser stream class

  This class extends the basic Stream class with position features needed by parsers for backtracking and error reporting.

  • The type Position is used to record position data for the stream type.
  • getPosition (s : σ) : Position returns the current position of stream s.
  • setPosition (s : σ) (p : Position) : σ restores stream s to position p.

  Implementations should try to make the Position type as lightweight as possible for getPosition and setPosition to work properly. Often Position is just a scalar type or another simple type. This may allow for parsers to use the stream state more efficiently.

• getPosition : σ → Position σ

  Parser stream class

  This class extends the basic Stream class with position features needed by parsers for backtracking and error reporting.

  • The type Position is used to record position data for the stream type.
  • getPosition (s : σ) : Position returns the current position of stream s.
  • setPosition (s : σ) (p : Position) : σ restores stream s to position p.

  Implementations should try to make the Position type as lightweight as possible for getPosition and setPosition to work properly. Often Position is just a scalar type or another simple type. This may allow for parsers to use the stream state more efficiently.

• setPosition : σ → Position σ → σ

  Parser stream class

  This class extends the basic Stream class with position features needed by parsers for backtracking and error reporting.

  • The type Position is used to record position data for the stream type.
  • getPosition (s : σ) : Position returns the current position of stream s.
  • setPosition (s : σ) (p : Position) : σ restores stream s to position p.

  Implementations should try to make the Position type as lightweight as possible for getPosition and setPosition to work properly. Often Position is just a scalar type or another simple type. This may allow for parsers to use the stream state more efficiently.

def Parser.Stream.Segment {τ : Type u_1} (σ : Type u_2) [Parser.Stream σ τ] : Type u_3

Stream segment type.

Equations

• Parser.Stream.Segment σ = (Parser.Stream.Position σ × Parser.Stream.Position σ)

@[reducible, inline]

abbrev Parser.Stream.Segment.start {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] (s : Segment σ) : Position σ

Start position of stream segment.

Equations

• s.start = s.fst

@[reducible, inline]

abbrev Parser.Stream.Segment.stop {σ : Type u_1} {τ : Type u_2} [Parser.Stream σ τ] (s : Segment σ) : Position σ

Stop position of stream segment.

Equations

• s.stop = s.snd

def Parser.Stream.mkDefault (σ : Type u_1) (τ : Type u_2) [Std.Stream σ τ] : Type u_1

Default wrapper to make a Parser.Stream from a plain Stream.

This wrapper uses the entire stream state as position information; this is not efficient. Always prefer tailored Parser.Stream instances to this default.

Equations

• Parser.Stream.mkDefault σ τ = σ

@[reducible]

instance Parser.Stream.instMkDefault (σ : Type u_1) (τ : Type u_2) [self : Std.Stream σ τ] : Parser.Stream (mkDefault σ τ) τ

Equations

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

@[reducible]

instance Parser.Stream.instSliceChar : Parser.Stream String.Slice Char

Equations

• Parser.Stream.instSliceChar = { toStream := instStreamSliceChar_parser, Position := String.Slice, getPosition := fun (s : String.Slice) => s, setPosition := fun (x s : String.Slice) => s }

@[reducible]

instance Parser.Stream.instRawChar : Parser.Stream Substring.Raw Char

Equations

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

@[reducible]

instance Parser.Stream.instSubarray (τ : Type u_1) : Parser.Stream (Subarray τ) τ

Equations

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

@[reducible]

instance Parser.Stream.instByteSliceUInt8 : Parser.Stream ByteSlice UInt8

Equations

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

structure Parser.Stream.OfList (τ : Type u_1) : Type u_1

OfList is a view of a list stream that keeps track of consumed tokens.

• next : List τ

  Remaining tokens.

• past : List τ

  Consumed tokens.

def Parser.Stream.OfList.setPosition {τ : Type u_1} (s : OfList τ) (p : Nat) : OfList τ

Restore a list stream to a given position.

Equations

• s.setPosition p = if s.past.length < p then Parser.Stream.OfList.setPosition.fwd (p - s.past.length) s else Parser.Stream.OfList.setPosition.rev (s.past.length - p) s

def Parser.Stream.OfList.setPosition.fwd {τ : Type u_1} : Nat → OfList τ → OfList τ

Internal for OfList.setPosition.

Equations

• Parser.Stream.OfList.setPosition.fwd k.succ { next := x_2 :: rest, past := past } = Parser.Stream.OfList.setPosition.fwd k { next := rest, past := x_2 :: past }
• Parser.Stream.OfList.setPosition.fwd x✝¹ x✝ = x✝

def Parser.Stream.OfList.setPosition.rev {τ : Type u_1} : Nat → OfList τ → OfList τ

Internal for OfList.setPosition.

Equations

• Parser.Stream.OfList.setPosition.rev k.succ { next := rest, past := x_2 :: past } = Parser.Stream.OfList.setPosition.rev k { next := x_2 :: rest, past := past }
• Parser.Stream.OfList.setPosition.rev x✝¹ x✝ = x✝

def Parser.Stream.mkOfList {τ : Type u_1} (data : List τ) (pos : Nat := 0) : OfList τ

Make a Parser.Stream from a List.

Equations

• Parser.Stream.mkOfList data pos = { next := data }.setPosition pos

@[reducible]

instance Parser.Stream.instOfList (τ : Type u_1) : Parser.Stream (OfList τ) τ

Equations

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