feat(library/system/io): implement io using string instead of char_buffer

library/data/buffer.lean

@@ -1,147 +0,0 @@
-/-
-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⟩
-
-lemma read_eq_read' [inhabited α] (b : buffer α) (i : nat) (h : i < b.size) : read b ⟨i, h⟩ = read' b i :=
-by cases b; unfold read read'; simp [array.read_eq_read']
-
-lemma write_eq_write' (b : buffer α) (i : nat) (h : i < b.size) (v : α) : write b ⟨i, h⟩ v = write' b i v :=
-by cases b; unfold write write'; simp [array.write_eq_write']
-
-def to_list (b : buffer α) : list α :=
-b.to_array.to_list
-
-protected def to_string (b : buffer char) : string :=
-b.to_array.to_list.as_string
-
-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.to_list
-
-lemma lt_aux_1 {a b c : nat} (h : a + c < b) : a < b :=
-nat.lt_of_le_of_lt (nat.le_add_right a c) h
-
-lemma lt_aux_2 {n} (h : n > 0) : n - 1 < n :=
-have h₁ : 1 > 0, from dec_trivial,
-nat.sub_lt h h₁
-
-lemma lt_aux_3 {n i} (h : i + 1 < n) : n - 2 - i < n  :=
-have n > 0,     from nat.lt_trans (nat.zero_lt_succ i) h,
-have n - 2 < n, from nat.sub_lt this (dec_trivial),
-nat.lt_of_le_of_lt (nat.sub_le _ _) this
-
-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, 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, lt_aux_3 h⟩ in
-  append_array ⟨m+1, b.push_back (a.read i)⟩ a j (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
-
-/-
-def take (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨n, b.to_array.take n h⟩ else b
-
-def take_right (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨n, b.to_array.take_right n h⟩ else b
-
-def drop (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨_, b.to_array.drop n h⟩ else b
-
-def reverse (b : buffer α) : buffer α :=
-⟨b.size, b.to_array.reverse⟩
--/
-
-protected def mem (v : α) (a : buffer α) : Prop := ∃i, read a i = v
-
-instance : has_mem α (buffer α) := ⟨buffer.mem⟩
-
-instance : has_append (buffer α) :=
-⟨buffer.append⟩
-
-instance [has_repr α] : has_repr (buffer α) :=
-⟨repr ∘ 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
-
-@[reducible] def char_buffer := buffer char
-
-/-- Convert a format object into a character buffer with the provided
-    formatting options. -/
-meta constant format.to_buffer : format → options → buffer char
-
-def string.to_char_buffer (s : string) : char_buffer :=
-buffer.nil.append_string s

library/system/io.lean

@@ -115,31 +115,31 @@ monad_io_file_system.flush
 def close : handle → io unit :=
 monad_io_file_system.close
 
-def read : handle → nat → io char_buffer :=
+def read : handle → nat → io string :=
 monad_io_file_system.read
 
-def write : handle → char_buffer → io unit :=
+def write : handle → string → io unit :=
 monad_io_file_system.write
 
 def get_char (h : handle) : io char :=
 do b ← read h 1,
-   if h : b.size = 1 then return $ b.read ⟨0, h.symm ▸ nat.zero_lt_one⟩
-   else io.fail "get_char failed"
+   if b.is_empty then io.fail "get_char failed"
+   else return b.mk_iterator.curr
 
-def get_line : handle → io char_buffer :=
+def get_line : handle → io string :=
 monad_io_file_system.get_line
 
 def put_char (h : handle) (c : char) : io unit :=
-write h (mk_buffer.push_back c)
+write h (to_string c)
 
 def put_str (h : handle) (s : string) : io unit :=
-write h (mk_buffer.append_string s)
+write h s
 
 def put_str_ln (h : handle) (s : string) : io unit :=
 put_str h s >> put_str h "\n"
 
-def read_to_end (h : handle) : io char_buffer :=
-iterate mk_buffer $ λ r,
+def read_to_end (h : handle) : io string :=
+iterate "" $ λ r,
   do done ← is_eof h,
     if done
     then return none
@@ -147,7 +147,7 @@ iterate mk_buffer $ λ r,
       c ← read h 1024,
       return $ some (r ++ c)
 
-def read_file (s : string) (bin := ff) : io char_buffer :=
+def read_file (s : string) (bin := ff) : io string :=
 do h ← mk_file_handle s io.mode.read bin,
    read_to_end h
 
@@ -199,11 +199,11 @@ format.print (to_fmt a)
     read into `string` which is then returned. -/
 def io.cmd (args : io.process.spawn_args) : io string :=
 do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args },
-  buf ← io.fs.read_to_end child.stdout,
+  s ← io.fs.read_to_end child.stdout,
   io.fs.close child.stdout,
   exitv ← io.proc.wait child,
   when (exitv ≠ 0) $ io.fail $ "process exited with status " ++ repr exitv,
-  return buf.to_string
+  return s
 
 /--
 This is the "back door" into the `io` monad, allowing IO computation to be performed during tactic execution.

library/system/io_interface.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import data.buffer system.random
+import system.random
 
 inductive io.error
 | other     : string → io.error
@@ -55,9 +55,9 @@ class monad_io_file_system (m : Type → Type → Type) [monad_io m] :=
 (is_eof         : (handle m) → m io.error bool)
 (flush          : (handle m) → m io.error unit)
 (close          : (handle m) → m io.error unit)
-(read           : (handle m) → nat → m io.error char_buffer)
-(write          : (handle m) → char_buffer → m io.error unit)
-(get_line       : (handle m) → m io.error char_buffer)
+(read           : (handle m) → nat → m io.error string)
+(write          : (handle m) → string → m io.error unit)
+(get_line       : (handle m) → m io.error string)
 (stdin          : m io.error (handle m))
 (stdout         : m io.error (handle m))
 (stderr         : m io.error (handle m))

src/library/handle.cpp

@@ -28,7 +28,7 @@ Author:  Leonardo de Moura & Jared Roesch
 
 namespace lean {
 
-void handle::write(buffer<char> & buf) {
+void handle::write(std::string const & buf) {
     auto sz = buf.size();
     if (fwrite(buf.data(), 1, sz, m_file) != sz) {
         std::cout << "write_error: " << errno << std::endl;

src/library/handle.h

@@ -27,7 +27,7 @@ public:
 
     ~handle();
 
-    void write(buffer<char> & data);
+    void write(std::string const & data);
     void flush();
 
     bool is_stdin();

src/library/vm/vm_io.cpp

@@ -185,26 +185,18 @@ static vm_obj fs_close(vm_obj const & h, vm_obj const &) {
     }
 }
 
-static vm_obj mk_buffer(parray<vm_obj> const & a) {
-    return mk_vm_pair(mk_vm_nat(a.size()), to_obj(a));
-}
-
 static vm_obj fs_read(vm_obj const & h, vm_obj const & n, vm_obj const &) {
     handle_ref const & href = to_handle(h);
     if (href->is_closed()) return mk_handle_has_been_closed_error();
     buffer<char> tmp;
     unsigned num = force_to_unsigned(n); /* TODO(Leo): handle size_t */
     tmp.resize(num, 0);
-    size_t sz = fread(tmp.data(), 1, num, href->m_file);
+    fread(tmp.data(), 1, num, href->m_file);
     if (ferror(href->m_file)) {
         clearerr(href->m_file);
         return mk_io_failure("read failed");
     }
-    parray<vm_obj> r;
-    for (size_t i = 0; i < sz; i++) {
-        r.push_back(mk_vm_simple(static_cast<unsigned char>(tmp[i])));
-    }
-    return mk_io_result(mk_buffer(r));
+    return mk_io_result(to_obj(std::string(tmp.data())));
 }
 
 static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) {
@@ -214,15 +206,8 @@ static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) {
         return mk_handle_has_been_closed_error();
     }
 
-    buffer<char> tmp;
-    parray<vm_obj> const & a = to_array(cfield(b, 1));
-    unsigned sz = a.size();
-    for (unsigned i = 0; i < sz; i++) {
-        tmp.push_back(static_cast<unsigned char>(cidx(a[i])));
-    }
-
     try {
-        href->write(tmp);
+        href->write(to_string(b));
         return mk_io_result(mk_vm_unit());
     } catch (handle_exception e) {
         return mk_io_failure("write failed");
@@ -236,7 +221,7 @@ static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) {
         return mk_handle_has_been_closed_error();
     }
 
-    parray<vm_obj> r;
+    std::string r;
     while (true) {
         int c = fgetc(href->m_file);
         if (ferror(href->m_file)) {
@@ -245,11 +230,11 @@ static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) {
         }
         if (c == EOF)
             break;
-        r.push_back(mk_vm_simple(static_cast<unsigned char>(static_cast<char>(c))));
+        r.push_back(static_cast<char>(c));
         if (c == '\n')
             break;
     }
-    return mk_io_result(mk_buffer(r));
+    return mk_io_result(to_obj(r));
 }
 
 static vm_obj fs_stdin(vm_obj const &) {