Length-indexed parser input.

structure Input (σ : Type) [Buffer σ] (n : ℕ) : Type

Input to a parser. n is the number of units that haven't been consumed yet.

NOTE: The main reason n is a type parameter instead of a field is performance. Because n is not a field, buf is the only non-Prop field, so Input is erased during compilation.

• buf : σ
• valid : n ≤ Buffer.size self.buf

@[reducible, inline]

abbrev Input.nextTok {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] (inp : Input σ n) : Option τ

Equations

• inp.nextTok = Reader.nextTok inp.buf n

theorem Input.width_le {σ τ : Type} [Buffer σ] {n : ℕ} {t : τ} [Reader σ τ] (inp : Input σ n) (h : inp.nextTok = some t) : Reader.width σ t ≤ n

theorem Input.sub_width_lt {σ τ : Type} [Buffer σ] {n : ℕ} {t : τ} [Reader σ τ] {inp : Input σ n} (h : inp.nextTok = some t) : n - Reader.width σ t < n

@[simp]

theorem Input.nextTok_eq_none {σ τ : Type} [Buffer σ] [Reader σ τ] {inp : Input σ 0} : inp.nextTok = none

@[inline]

def Input.dropTo {σ : Type} [Buffer σ] {n : ℕ} (inp : Input σ n) (m : ℕ) (h : m ≤ n := by omega) : Input σ m

Equations

• inp.dropTo m h = { buf := inp.buf, valid := ⋯ }

@[simp]

theorem Input.dropTo_self {σ : Type} [Buffer σ] {n : ℕ} (inp : Input σ n) (h : n ≤ n) : inp.dropTo n h = inp

@[simp]

theorem Input.dropTo_trans {σ : Type} [Buffer σ] {n m k : ℕ} (inp : Input σ n) (h : m ≤ n) (h' : k ≤ m) : (inp.dropTo m h).dropTo k h' = inp.dropTo k ⋯

@[simp]

theorem Input.dropTo_buf {σ : Type} [Buffer σ] {n m : ℕ} (inp : Input σ n) (h : m ≤ n) : (inp.dropTo m h).buf = inp.buf

@[inline]

def Input.pos {σ : Type} [Buffer σ] {n : ℕ} (inp : Input σ n) : ℕ

how many units have been consumedfrom inp.

Equations

• inp.pos = Buffer.size inp.buf - n

@[simp]

theorem Input.pos_dropTo {σ : Type} [Buffer σ] {n m : ℕ} (inp : Input σ n) (h : m ≤ n) : (inp.dropTo m h).pos = inp.pos + (n - m)

theorem Input.pos_lt {σ : Type} [Buffer σ] {n : ℕ} (inp : Input σ (n + 1)) : inp.pos < Buffer.size inp.buf

@[reducible, inline]

abbrev Input.advance {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] (inp : Input σ n) (t : τ) : Input σ (n - Reader.width σ t)

Move past one token.

Equations

• inp.advance t = inp.dropTo (n - Reader.width σ t) ⋯

@[irreducible, specialize #[]]

def Input.skipWhile {σ τ : Type} [Buffer σ] [Reader σ τ] (f : τ → Bool) {n : ℕ} (inp : Input σ n) : { m : ℕ // m ≤ n }

Skip forward while f holds, returning the number of units left unconsumed.

Equations

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

theorem Input.skipWhile_accept {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] {f : τ → Bool} {t : τ} {inp : Input σ n} (h : inp.nextTok = some t := by assumption) (hf : f t = true := by assumption) : ↑(skipWhile f inp) = ↑(skipWhile f (inp.advance t))

theorem Input.skipWhile_reject {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] {f : τ → Bool} {t : τ} {inp : Input σ n} (h : inp.nextTok = some t := by assumption) (hf : ¬f t = true := by assumption) : ↑(skipWhile f inp) = n

theorem Input.skipWhile_eof {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] {f : τ → Bool} {inp : Input σ n} (h : inp.nextTok = none := by assumption) : ↑(skipWhile f inp) = n

theorem Input.skipWhile_lt_iff {σ τ : Type} [Buffer σ] {n : ℕ} [Reader σ τ] {f : τ → Bool} {inp : Input σ n} : ↑(skipWhile f inp) < n ↔ ∃ (t : τ), inp.nextTok = some t ∧ f t = true

The scanners make progress exactly when the next token is accepted.

def Input.ofArray {τ : Type} (a : Array τ) : Input (Array τ) a.size

Equations

• Input.ofArray a = { buf := a, valid := ⋯ }

structure Input.DigitFold : Type

The result of foldDigits.

• value : ℕ

  The decimal value of the parsed digits.

• restSize : ℕ

  The remaining input size.

def Input.foldDigits {σ : Type} [Buffer σ] [Reader σ Char] {n : ℕ} (inp : Input σ n) : DigitFold

Parse a sequence of ASCII digits as a decimal value.

Equations

• inp.foldDigits = Input.foldDigits.go inp 0

@[irreducible]

def Input.foldDigits.go {σ : Type} [Buffer σ] [Reader σ Char] {m : ℕ} (inp : Input σ m) (acc : ℕ) : DigitFold

Equations

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

theorem Input.foldDigits_go_accept {σ : Type} [Buffer σ] {n : ℕ} [Reader σ Char] {acc : ℕ} {inp : Input σ n} {c : Char} (h : inp.nextTok = some c := by assumption) (hd : c.isDigit = true := by assumption) : foldDigits.go inp acc = foldDigits.go (inp.advance c) (acc * 10 + (c.toNat - '0'.toNat))

theorem Input.foldDigits_go_le {σ : Type} [Buffer σ] {n : ℕ} [Reader σ Char] (inp : Input σ n) (acc : ℕ) : (foldDigits.go inp acc).restSize ≤ n

theorem Input.foldDigits_lt_iff {σ : Type} [Buffer σ] {n : ℕ} [Reader σ Char] {inp : Input σ n} : inp.foldDigits.restSize < n ↔ ∃ (c : Char), inp.nextTok = some c ∧ c.isDigit = true

def Input.ofByteArray (b : ByteArray) : Input ByteArray b.size

Equations

• Input.ofByteArray b = { buf := b, valid := ⋯ }

@[inline]

def Input.head {n : ℕ} (inp : Input ByteArray (n + 1)) : UInt8

Equations

• inp.head = inp.buf[inp.pos]

def Input.ofString (s : String) : Input ByteArray s.toUTF8.size

Equations

• Input.ofString s = { buf := s.toUTF8, valid := ⋯ }

@[specialize #[]]

def Input.takeWhile (f : Char → Bool) {n : ℕ} (inp : Input ByteArray n) : String

Collect characters while f holds, returning them as a String.

Equations

• Input.takeWhile f inp = Input.takeWhile.go f inp ""

@[irreducible, specialize #[]]

def Input.takeWhile.go (f : Char → Bool) {m : ℕ} (inp : Input ByteArray m) (acc : String) : String

Equations

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

theorem Input.takeWhile_go_accept {n : ℕ} {f : Char → Bool} {c : Char} {inp : Input ByteArray n} {acc : String} (h : inp.nextTok = some c := by assumption) (hf : f c = true := by assumption) : takeWhile.go f inp acc = takeWhile.go f (inp.advance c) (acc.push c)

theorem Input.takeWhile_go_reject {n : ℕ} {f : Char → Bool} {c : Char} {inp : Input ByteArray n} {acc : String} (h : inp.nextTok = some c := by assumption) (hf : ¬f c = true := by assumption) : takeWhile.go f inp acc = acc

theorem Input.takeWhile_go_eof {n : ℕ} {f : Char → Bool} {inp : Input ByteArray n} {acc : String} (h : inp.nextTok = none := by assumption) : takeWhile.go f inp acc = acc

theorem Input.takeWhile_reject {n : ℕ} {f : Char → Bool} {c : Char} {inp : Input ByteArray n} (h : inp.nextTok = some c := by assumption) (hf : ¬f c = true := by assumption) : takeWhile f inp = ""

theorem Input.takeWhile_eof {n : ℕ} {f : Char → Bool} {inp : Input ByteArray n} (h : inp.nextTok = none) : takeWhile f inp = ""

theorem Input.utf8ByteSize_takeWhile {n : ℕ} (f : Char → Bool) (inp : Input ByteArray n) : (takeWhile f inp).utf8ByteSize + ↑(skipWhile f inp) = n

theorem Input.val_skipWhile {n : ℕ} (f : Char → Bool) (inp : Input ByteArray n) : ↑(skipWhile f inp) = n - (takeWhile f inp).utf8ByteSize

theorem Input.utf8Size_le_utf8ByteSize_takeWhile {n : ℕ} {f : Char → Bool} {c : Char} {inp : Input ByteArray n} (h : inp.nextTok = some c := by assumption) (hf : f c = true := by assumption) : c.utf8Size ≤ (takeWhile f inp).utf8ByteSize

A character the predicate accepts is part of what takeWhile collects.

theorem Input.utf8ByteSize_takeWhile_pos_iff {n : ℕ} (f : Char → Bool) (inp : Input ByteArray n) : 0 < (takeWhile f inp).utf8ByteSize ↔ ∃ (c : Char), inp.nextTok = some c ∧ f c = true