Parser inputs

Iterators for common parser inputs, with HasPos instances for error reporting:

• CharIterator iterates over the characters of a String.Slice. Unlike String.Slice.chars, its type does not depend on the slice, so parsers can name it.
• ByteIterator iterates over the bytes of a ByteArray.
• BitIterator iterates over the bits of a BitVec, least significant bit first.
• Core's ArrayIterator (from Array.iter) reports its index as the position.

structure ParseIt.CharIterator : Type

Iterator over the characters of a String.Slice.

• slice : String.Slice

  The slice being iterated over.

• pos : self.slice.Pos

  The current position in slice.

@[instance_reducible]

instance ParseIt.CharIterator.instIteratorIdChar : Std.Iterator CharIterator Id Char

Equations

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

instance ParseIt.CharIterator.instFiniteIdChar : Std.Iterators.Finite CharIterator Id

@[instance_reducible]

instance ParseIt.CharIterator.instHasPosChar : HasPos CharIterator Char

Positions are byte offsets into the slice.

Equations

• ParseIt.CharIterator.instHasPosChar = { Pos := String.Pos.Raw, pos := fun (it : Std.Iter Char) => it.internalState.pos.offset }

@[inline]

def ParseIt.CharIterator.ofSlice (s : String.Slice) : Std.Iter Char

Iterator over the characters of s.

Equations

• ParseIt.CharIterator.ofSlice s = { internalState := { slice := s, pos := s.startPos } }

@[inline]

def ParseIt.CharIterator.remaining (it : Std.Iter Char) : String.Slice

The remaining characters as a slice.

Equations

• ParseIt.CharIterator.remaining it = it.internalState.slice.sliceFrom it.internalState.pos

structure ParseIt.ByteIterator : Type

Iterator over the bytes of a ByteArray.

• data : ByteArray

  The bytes being iterated over.

• pos : Nat

  The current index in data.

@[instance_reducible]

instance ParseIt.ByteIterator.instIteratorIdUInt8 : Std.Iterator ByteIterator Id UInt8

Equations

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

instance ParseIt.ByteIterator.instFiniteIdUInt8 : Std.Iterators.Finite ByteIterator Id

@[instance_reducible]

instance ParseIt.ByteIterator.instHasPosUInt8 : HasPos ByteIterator UInt8

Positions are byte indices.

Equations

• ParseIt.ByteIterator.instHasPosUInt8 = { Pos := Nat, pos := fun (it : Std.Iter UInt8) => it.internalState.pos }

@[inline]

def ParseIt.ByteIterator.ofByteArray (data : ByteArray) : Std.Iter UInt8

Iterator over the bytes of data.

Equations

• ParseIt.ByteIterator.ofByteArray data = { internalState := { data := data, pos := 0 } }

structure ParseIt.BitIterator : Type

Iterator over the bits of a BitVec, least significant bit first.

• width : Nat

  The width of bits.

• bits : BitVec self.width

  The bits being iterated over.

• pos : Nat

  The index of the current bit.

@[instance_reducible]

instance ParseIt.BitIterator.instIteratorIdBool : Std.Iterator BitIterator Id Bool

Equations

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

instance ParseIt.BitIterator.instFiniteIdBool : Std.Iterators.Finite BitIterator Id

@[instance_reducible]

instance ParseIt.BitIterator.instHasPosBool : HasPos BitIterator Bool

Positions are bit indices.

Equations

• ParseIt.BitIterator.instHasPosBool = { Pos := Nat, pos := fun (it : Std.Iter Bool) => it.internalState.pos }

@[inline]

def ParseIt.BitIterator.ofBitVec {w : Nat} (bits : BitVec w) : Std.Iter Bool

Iterator over the bits of bits, least significant bit first.

Equations

• ParseIt.BitIterator.ofBitVec bits = { internalState := { width := w, bits := bits, pos := 0 } }

@[instance_reducible]

instance ParseIt.instHasPosArrayIterator {α : Type} : HasPos (Std.Iterators.Types.ArrayIterator α) α

Positions are array indices.

Equations

• ParseIt.instHasPosArrayIterator = { Pos := Nat, pos := fun (it : Std.Iter α) => it.internalState.pos }

Running parsers

def ParseIt.captureSlice {ε α : Type} {m : Type → Type} [Monad m] (p : ParserT ε CharIterator Char m α) : ParserT ε CharIterator Char m (α × String.Slice)

captureSlice p parses p and returns its result together with the slice of input that p consumed. The slice is a view into the input; no characters are copied.

Equations

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

@[inline]

def ParseIt.Parser.parseSlice {ε α : Type} (p : Parser ε CharIterator Char α) (s : String.Slice) : Except ε α

Run p on the characters of s.

Equations

• p.parseSlice s = p.parse (ParseIt.CharIterator.ofSlice s)

@[inline]

def ParseIt.Parser.parseString {ε α : Type} (p : Parser ε CharIterator Char α) (s : String) : Except ε α

Run p on the characters of s.

Equations

• p.parseString s = p.parseSlice s.toSlice

@[inline]

def ParseIt.Parser.parseByteArray {ε α : Type} (p : Parser ε ByteIterator UInt8 α) (data : ByteArray) : Except ε α

Run p on the bytes of data.

Equations

• p.parseByteArray data = p.parse (ParseIt.ByteIterator.ofByteArray data)

@[inline]

def ParseIt.Parser.parseBitVec {ε α : Type} {w : Nat} (p : Parser ε BitIterator Bool α) (bits : BitVec w) : Except ε α

Run p on the bits of bits, least significant bit first.

Equations

• p.parseBitVec bits = p.parse (ParseIt.BitIterator.ofBitVec bits)

@[inline]

def ParseIt.Parser.parseArray {ε τ α : Type} (p : Parser ε (Std.Iterators.Types.ArrayIterator τ) τ α) (xs : Array τ) : Except ε α

Run p on the elements of xs.

Equations

• p.parseArray xs = p.parse xs.iter

@[inline]

def ParseIt.Parser.parseVector {ε τ α : Type} {n : Nat} (p : Parser ε (Std.Iterators.Types.ArrayIterator τ) τ α) (xs : Vector τ n) : Except ε α

Run p on the elements of xs. Vectors use the array iterator.

Equations

• p.parseVector xs = p.parse xs.iter

@[inline]

def ParseIt.Parser.parseList {ε τ α : Type} (p : Parser ε (Std.Iterators.Types.ListIterator τ) τ α) (xs : List τ) : Except ε α

Run p on the elements of xs. Lists have no HasPos instance.

Equations

• p.parseList xs = p.parse xs.iter