mathlib docs: core.data.buffer

source

def buffer (α : Type u) :

Type u

Equations

buffer α = Σ (n : ℕ), array n α

source

def mk_buffer {α : Type u} :

buffer α

Equations

mk_buffer = ⟨0, {data := λ (i : fin 0), i.elim0}⟩

source

def array.to_buffer {α : Type u} {n : ℕ} (a : array n α) :

buffer α

Equations

a.to_buffer = ⟨n, a⟩

source

def buffer.nil {α : Type u} :

buffer α

Equations

buffer.nil = mk_buffer

source

def buffer.size {α : Type u} (b : buffer α) :

ℕ

Equations

b.size = b.fst

source

def buffer.to_array {α : Type u} (b : buffer α) :

array b.size α

Equations

b.to_array = b.snd

source

def buffer.push_back {α : Type u} (a : buffer α) (a_1 : α) :

buffer α

Equations

buffer.push_back ⟨n, a⟩ v = ⟨n + 1, a.push_back v⟩

source

def buffer.pop_back {α : Type u} (a : buffer α) :

buffer α

Equations

buffer.pop_back ⟨n + 1, a⟩ = ⟨n, a.pop_back⟩
buffer.pop_back ⟨0, a⟩ = ⟨0, a⟩

source

def buffer.read {α : Type u} (b : buffer α) (a : fin b.size) :

α

Equations

buffer.read ⟨n, a⟩ i = a.read i

source

def buffer.write {α : Type u} (b : buffer α) (a : fin b.size) (a_1 : α) :

buffer α

Equations

buffer.write ⟨n, a⟩ i v = ⟨n, a.write i v⟩

source

def buffer.read' {α : Type u} [inhabited α] (a : buffer α) (a_1 : ℕ) :

α

Equations

buffer.read' ⟨n, a⟩ i = a.read' i

source

def buffer.write' {α : Type u} (a : buffer α) (a_1 : ℕ) (a_2 : α) :

buffer α

Equations

buffer.write' ⟨n, a⟩ i v = ⟨n, a.write' i v⟩

source

theorem buffer.read_eq_read' {α : Type u} [inhabited α] (b : buffer α) (i : ℕ) (h : i < b.size) :

b.read ⟨i, h⟩ = b.read' i

source

theorem buffer.write_eq_write' {α : Type u} (b : buffer α) (i : ℕ) (h : i < b.size) (v : α) :

b.write ⟨i, h⟩ v = b.write' i v

source

def buffer.to_list {α : Type u} (b : buffer α) :

list α

Equations

b.to_list = b.to_array.to_list

source

def buffer.to_string (b : buffer char) :

string

Equations

b.to_string = b.to_array.to_list.as_string

source

def buffer.append_list {α : Type u} (a : buffer α) (a_1 : list α) :

buffer α

Equations

b.append_list (v :: vs) = (b.push_back v).append_list vs
b.append_list list.nil = b

source

def buffer.append_string (b : buffer char) (s : string) :

buffer char

Equations

b.append_string s = b.append_list s.to_list

source

theorem buffer.lt_aux_1 {a b c : ℕ} (h : a + c < b) :

a < b

source

theorem buffer.lt_aux_2 {n : ℕ} (h : n > 0) :

n - 1 < n

source

theorem buffer.lt_aux_3 {n i : ℕ} (h : i + 1 < n) :

n - 2 - i < n

source

def buffer.append_array {α : Type u} {n : ℕ} (nz : n > 0) (a : buffer α) (a_1 : array n α) (i : ℕ) (a_2 : i < n) :

buffer α

Equations

buffer.append_array nz ⟨m, b⟩ a (j + 1) h = let i : fin n := ⟨n - 2 - j, _⟩ in buffer.append_array nz ⟨m + 1, b.push_back (a.read i)⟩ a j _
buffer.append_array nz ⟨m, b⟩ a 0 _x = let i : fin n := ⟨n - 1, _⟩ in ⟨m + 1, b.push_back (a.read i)⟩

source

def buffer.append {α : Type u} (a a_1 : buffer α) :

buffer α

Equations

b.append ⟨n + 1, a⟩ = buffer.append_array _ b a n _
b.append ⟨0, a⟩ = b

source

def buffer.iterate {α : Type u} {β : Type w} (b : buffer α) (a : β) (a_1 : fin b.size → α → β → β) :

β

Equations

buffer.iterate ⟨_x, a⟩ b f = a.iterate b f

source

def buffer.foreach {α : Type u} (b : buffer α) (a : fin b.size → α → α) :

buffer α

Equations

buffer.foreach ⟨n, a⟩ f = ⟨n, a.foreach f⟩

source

def buffer.mmap {α : Type u} {β : Type w} {m : Type w → Type u_1} [monad m] (b : buffer α) (f : α → m β) :

m (buffer β)

Monadically map a function over the buffer.

Equations

b.mmap f = array.mmap b.snd f >>= λ (b' : array b.fst β), return b'.to_buffer

source

def buffer.map {α : Type u} {β : Type w} (a : buffer α) (a_1 : α → β) :

buffer β

Map a function over the buffer.

Equations

buffer.map ⟨n, a⟩ f = ⟨n, a.map f⟩

source

def buffer.foldl {α : Type u} {β : Type w} (a : buffer α) (a_1 : β) (a_2 : α → β → β) :

β

Equations

buffer.foldl ⟨_x, a⟩ b f = a.foldl b f

source

def buffer.rev_iterate {α : Type u} {β : Type w} (b : buffer α) (a : β) (a_1 : fin b.size → α → β → β) :

β

Equations

buffer.rev_iterate ⟨_x, a⟩ b f = a.rev_iterate b f

source

def buffer.take {α : Type u} (b : buffer α) (n : ℕ) :

buffer α

Equations

b.take n = dite (n ≤ b.size) (λ (h : n ≤ b.size), ⟨n, b.to_array.take n h⟩) (λ (h : ¬n ≤ b.size), b)

source

def buffer.take_right {α : Type u} (b : buffer α) (n : ℕ) :

buffer α

Equations

b.take_right n = dite (n ≤ b.size) (λ (h : n ≤ b.size), ⟨n, b.to_array.take_right n h⟩) (λ (h : ¬n ≤ b.size), b)

source

def buffer.drop {α : Type u} (b : buffer α) (n : ℕ) :

buffer α

Equations

b.drop n = dite (n ≤ b.size) (λ (h : n ≤ b.size), ⟨b.size - n, b.to_array.drop n h⟩) (λ (h : ¬n ≤ b.size), b)

source

def buffer.reverse {α : Type u} (b : buffer α) :

buffer α

Equations

b.reverse = ⟨b.size, b.to_array.reverse⟩

source

def buffer.mem {α : Type u} (v : α) (a : buffer α) :

Prop

Equations

buffer.mem v a = ∃ (i : fin a.size), a.read i = v

source

@[instance]

def buffer.has_mem {α : Type u} :

has_mem α (buffer α)

Equations

buffer.has_mem = {mem := buffer.mem α}

source

@[instance]

def buffer.has_append {α : Type u} :

has_append (buffer α)

Equations

buffer.has_append = {append := buffer.append α}

source

@[instance]

def buffer.has_repr {α : Type u} [has_repr α] :

has_repr (buffer α)

Equations

buffer.has_repr = {repr := repr ∘ buffer.to_list}

source

@[instance]

meta def buffer.has_to_format {α : Type u} [has_to_format α] :

has_to_format (buffer α)

source

@[instance]

meta def buffer.has_to_tactic_format {α : Type u} [has_to_tactic_format α] :

has_to_tactic_format (buffer α)

source

def list.to_buffer {α : Type u} (l : list α) :

buffer α

Equations

l.to_buffer = mk_buffer.append_list l

source

def char_buffer :

Type

Equations

char_buffer = buffer char

source

meta constant format.to_buffer (a : format) (a_1 : options) :

buffer char

Convert a format object into a character buffer with the provided formatting options.

source

def string.to_char_buffer (s : string) :

char_buffer

Equations

s.to_char_buffer = buffer.nil.append_string s