Parser Stream

Parsers read input tokens from a stream. In contrast to the Std.Stream class, the stream itself does not change, but instead we keep track of the position inside the stream. This helps with error reporting and and allows for backtracking.

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

Parser stream class

This class implements streams based on a static stream with a moving position.

• The type Position is used to record position data for the stream type.
• start (s : σ) : Position returns starting position for the stream s
• next? (s : σ) (pos : Position) : Option (τ × Position) returns the token at position pos in s together with the next position. It returns none if the end of the stream has been reached.

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

• Position : Type u

  Parser stream class

  This class implements streams based on a static stream with a moving position.

  • The type Position is used to record position data for the stream type.
  • start (s : σ) : Position returns starting position for the stream s
  • next? (s : σ) (pos : Position) : Option (τ × Position) returns the token at position pos in s together with the next position. It returns none if the end of the stream has been reached.

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

• start : σ → Position σ

  Parser stream class

  This class implements streams based on a static stream with a moving position.

  • The type Position is used to record position data for the stream type.
  • start (s : σ) : Position returns starting position for the stream s
  • next? (s : σ) (pos : Position) : Option (τ × Position) returns the token at position pos in s together with the next position. It returns none if the end of the stream has been reached.

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

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

  Parser stream class

  This class implements streams based on a static stream with a moving position.

  • The type Position is used to record position data for the stream type.
  • start (s : σ) : Position returns starting position for the stream s
  • next? (s : σ) (pos : Position) : Option (τ × Position) returns the token at position pos in s together with the next position. It returns none if the end of the stream has been reached.

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

@[implicit_reducible]

instance instInhabitedPosition {σ : Type u_1} {τ : Type u_2} [self : Parser.Stream σ τ] [Inhabited σ] : Inhabited (Parser.Stream.Position σ)

Equations

• instInhabitedPosition = { default := Parser.Stream.start default }

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

Stream segment type.

Equations

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

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

• Parser.Stream.instMkDefault σ τ = { Position := σ, start := fun (s : Parser.Stream.mkDefault σ τ) => s, next? := fun (x : Parser.Stream.mkDefault σ τ) => Std.Stream.next? }

@[reducible]

instance Parser.Stream.instStringChar : Parser.Stream String Char

Equations

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

@[reducible]

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

Equations

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

@[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) : Parser.Stream (Subarray τ) τ

Equations

• Parser.Stream.instSubarray τ = { Position := Nat, start := fun (s : Subarray τ) => s.start, next? := fun (s : Subarray τ) (p : Nat) => do let x ← s[p]? some (x, p + 1) }

@[reducible]

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

Equations

• Parser.Stream.instByteSliceUInt8 = { Position := Nat, start := fun (s : ByteSlice) => s.start, next? := fun (s : ByteSlice) (p : Nat) => do let x ← s[p]? some (x, p + 1) }

@[reducible]

instance Parser.Stream.instList (τ : Type u_1) : Parser.Stream (List τ) τ

Equations

• Parser.Stream.instList τ = { Position := List τ, start := fun (s : List τ) => s, next? := fun (x p : List τ) => p.next? }