Documentation

PrimParser.Reader

class Reader (σ τ : Type) [Buffer σ] :

Reads tokens of type τ from a buffer σ. A token t : τ has a width of width t units.

width : τ → ℕ
width_pos (t : τ) : 0 < width σ t
nextTok : σ → (remaining : ℕ) → Option τ
remaining is the number of unconsumed units from σ.
nextTok_le {s : σ} {n : ℕ} {t : τ} : nextTok s n = some t → width σ t ≤ n

Instances

@[simp]

theorem Reader.nextTok_zero {σ τ : Type} [Buffer σ] [Reader σ τ] (s : σ) :

nextTok s 0 = none

theorem Reader.sub_width_lt {σ τ : Type} [Buffer σ] [Reader σ τ] {s : σ} {n : ℕ} {t : τ} (h : nextTok s n = some t) :

n - width σ t < n

@[instance_reducible]

instance Reader.instByteArrayChar :

Reader ByteArray Char

Equations

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

@[simp]

theorem Reader.width_byteArray (c : Char) :

width ByteArray c = c.utf8Size

@[simp]

theorem Reader.nextTok_byteArray (b : ByteArray) (n : ℕ) :

nextTok b n = b.utf8DecodeChar? (b.size - n)

@[instance_reducible]

instance Reader.instByteArrayUInt8 :

Reader ByteArray UInt8

Equations

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

@[simp]

theorem Reader.width_uint8 (t : UInt8) :

width ByteArray t = 1

@[simp]

theorem Reader.nextTok_uint8 (b : ByteArray) (n : ℕ) :

nextTok b n = b[b.size - n]?

@[instance_reducible]

instance Reader.instArray {τ : Type} :

Reader (Array τ) τ

Equations

Reader.instArray = { width := fun (x : τ) => 1, width_pos := ⋯, nextTok := fun (a : Array τ) (n : ℕ) => a[a.size - n]?, nextTok_le := ⋯ }

@[simp]

theorem Reader.width_array {τ : Type} (t : τ) :

width (Array τ) t = 1

@[simp]

theorem Reader.nextTok_array {τ : Type} (a : Array τ) (n : ℕ) :

nextTok a n = a[a.size - n]?

class LawfulReader (σ τ : Type) [Buffer σ] [Reader σ τ] :

This class is for documentation only.

nextTok_saturate (s : σ) (n : ℕ) : Reader.nextTok s n = Reader.nextTok s (min n (Buffer.size s))

Instances

instance instLawfulReaderByteArrayChar :

LawfulReader ByteArray Char

instance instLawfulReaderByteArrayUInt8 :

LawfulReader ByteArray UInt8

instance instLawfulReaderArray {τ : Type} :

LawfulReader (Array τ) τ