From 8feacb27a67dd7cbd65c698f9fd6fde1c104cdfb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Mar 2017 18:47:50 -0700
Subject: [PATCH] feat(library/data): add buffer

---
 library/data/buffer.lean         | 99 ++++++++++++++++++++++++++++++++
 library/init/data/fin/basic.lean |  3 +
 2 files changed, 102 insertions(+)
 create mode 100644 library/data/buffer.lean

diff --git a/library/data/buffer.lean b/library/data/buffer.lean
new file mode 100644
index 0000000000..1078ada3b1
--- /dev/null
+++ b/library/data/buffer.lean
@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+universes u w
+
+def buffer (α : Type u) := Σ n, array α n
+
+def mk_buffer {α : Type u} : buffer α :=
+⟨0, {data := λ i, fin.elim0 i}⟩
+
+def array.to_buffer {α : Type u} {n : nat} (a : array α n) : buffer α :=
+⟨n, a⟩
+
+namespace buffer
+variables {α : Type u} {β : Type w}
+
+def nil : buffer α :=
+mk_buffer
+
+def size (b : buffer α) : nat :=
+b.1
+
+def to_array (b : buffer α) : array α (b^.size) :=
+b.2
+
+def push_back : buffer α → α → buffer α
+| ⟨n, a⟩ v := ⟨n+1, a^.push_back v⟩
+
+def pop_back : buffer α → buffer α
+| ⟨0, a⟩   := ⟨0, a⟩
+| ⟨n+1, a⟩ := ⟨n, a^.pop_back⟩
+
+def read : Π (b : buffer α), fin b^.size → α
+| ⟨n, a⟩ i := a^.read i
+
+def write : Π (b : buffer α), fin b^.size → α → buffer α
+| ⟨n, a⟩ i v := ⟨n, a^.write i v⟩
+
+def read' [inhabited α] : buffer α → nat → α
+| ⟨n, a⟩ i := a^.read' i
+
+def write' : buffer α → nat → α → buffer α
+| ⟨n, a⟩ i v := ⟨n, a^.write' i v⟩
+
+def to_list (b : buffer α) : list α :=
+b^.to_array^.to_list
+
+def append_list {α : Type u} : buffer α → list α → buffer α
+| b []      := b
+| b (v::vs) := append_list (b^.push_back v) vs
+
+def append_string (b : buffer char) (s : string) : buffer char :=
+b^.append_list s^.reverse
+
+def append_array {α : Type u} {n : nat} (nz : n > 0) : buffer α → array α n → ∀ i : nat, i < n → buffer α
+| ⟨m, b⟩ a 0     _ :=
+  let i : fin n := ⟨n - 1, array.lt_aux_2 nz⟩ in
+  ⟨m+1, b^.push_back (a^.read i)⟩
+| ⟨m, b⟩ a (j+1) h :=
+  let i : fin n := ⟨n - 2 - j, array.lt_aux_3 h⟩ in
+  append_array ⟨m+1, b^.push_back (a^.read i)⟩ a j (array.lt_aux_1 h)
+
+protected def append {α : Type u} : buffer α → buffer α → buffer α
+| b ⟨0, a⟩   := b
+| b ⟨n+1, a⟩ := append_array (nat.zero_lt_succ _) b a n (nat.lt_succ_self _)
+
+def iterate : Π b : buffer α, β → (fin b^.size → α → β → β) → β
+| ⟨_, a⟩ b f := a^.iterate b f
+
+def foreach : Π b : buffer α, (fin b^.size → α → α) → buffer α
+| ⟨n, a⟩ f := ⟨n, a^.foreach f⟩
+
+def map (f : α → α) : buffer α → buffer α
+| ⟨n, a⟩ := ⟨n, a^.map f⟩
+
+def foldl : buffer α → β → (α → β → β) → β
+| ⟨_, a⟩ b f := a^.foldl b f
+
+def rev_iterate : Π (b : buffer α), β → (fin b^.size → α → β → β) → β
+| ⟨_, a⟩ b f := a^.rev_iterate b f
+
+instance : has_append (buffer α) :=
+⟨buffer.append⟩
+
+instance [has_to_string α] : has_to_string (buffer α) :=
+⟨to_string ∘ to_list⟩
+
+meta instance [has_to_format α] : has_to_format (buffer α) :=
+⟨to_fmt ∘ to_list⟩
+
+meta instance [has_to_tactic_format α] : has_to_tactic_format (buffer α) :=
+⟨tactic.pp ∘ to_list⟩
+
+end buffer
+
+def list.to_buffer {α : Type u} (l : list α) : buffer α :=
+mk_buffer^.append_list l
diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean
index 4a78ca99fd..333c0c6224 100644
--- a/library/init/data/fin/basic.lean
+++ b/library/init/data/fin/basic.lean
@@ -10,6 +10,9 @@ structure fin (n : nat) := (val : nat) (is_lt : val < n)
 
 namespace fin
 
+def {u} elim0 {α : Type u} : fin 0 → α
+| ⟨_, h⟩ := absurd h (not_lt_zero _)
+
 variable {n : nat}
 
 lemma eq_of_veq : ∀ {i j : fin n}, (val i) = (val j) → i = j