structure TokenStream (τ : Type u_1) : Type u_1

A token stream backed by an Array with a consumed-count cursor.

Replaces Parser.Stream.OfList as the concrete stream under both parsers. OfList stores its position as the length of a past : List it re-conses on every step, so getPosition — called on every withBacktracking, every choice alternative, twice per located — is O(n) in the number of consumed tokens. TokenStream holds the whole token array once and moves an index, so getPosition/setPosition are O(1) and located is array indexing.

• toks : Array τ

  Every token, consumed and remaining. Never changes after construction.

• idx : Nat

  Number of tokens consumed; the current position. Always ≤ toks.size.

def instReprTokenStream.repr {τ✝ : Type u_1} [Repr τ✝] : TokenStream τ✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance instReprTokenStream {τ✝ : Type u_1} [Repr τ✝] : Repr (TokenStream τ✝)

Equations

• instReprTokenStream = { reprPrec := instReprTokenStream.repr }

@[implicit_reducible]

instance instInhabitedTokenStream {a✝ : Type u_1} : Inhabited (TokenStream a✝)

Equations

• instInhabitedTokenStream = { default := instInhabitedTokenStream.default }

@[inline]

def TokenStream.ofArray {τ : Type u_1} (toks : Array τ) : TokenStream τ

A fresh stream over toks, positioned at the start.

Equations

• TokenStream.ofArray toks = { toks := toks }

@[inline]

def TokenStream.atEnd {τ : Type u_1} (s : TokenStream τ) : Bool

Whether every token has been consumed.

Equations

• s.atEnd = decide (s.toks.size ≤ s.idx)

@[inline]

def TokenStream.get! {τ : Type u_1} [Inhabited τ] (s : TokenStream τ) (n : Nat) : τ

The token at absolute index n, or panic — for located, which only ever asks for indices inside a span the parser has already crossed.

Equations

• s.get! n = s.toks[n]!

@[implicit_reducible]

instance TokenStream.instStream {τ : Type u_1} : Parser.Stream (TokenStream τ) τ

Equations

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