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

Parser.Stream class extends Stream with position features

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

  Position type

• getPosition : σ → Position σ

  Get current stream position

• setPosition : σ → Position σ → σ

  Set current stream position

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

Stream segment

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) [Stream σ τ] : Type u_1

Wrapper to make a Parser.Stream from a core Stream

Equations

• Parser.Stream.mkDefault σ τ = σ

@[reducible]

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

Equations

• Parser.Stream.instMkDefault σ τ = Parser.Stream.mk σ (fun (s : Parser.Stream.mkDefault σ τ) => s) fun (x : Parser.Stream.mkDefault σ τ) (p : σ) => p

@[reducible]

instance Parser.Stream.instSubstringChar : Parser.Stream Substring 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.instByteSubarrayUInt8 : Parser.Stream Batteries.ByteSubarray 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 along with a position along that list

• next : List τ

  Remaining tokens

• past : List τ

  Consumed tokens

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

Set 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 τ

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 τ

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, past := [] }.setPosition pos

@[reducible]

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

Equations

• Parser.Stream.instOfList τ = Parser.Stream.mk Nat (fun (s : Parser.Stream.OfList τ) => s.past.length) Parser.Stream.OfList.setPosition