chore(library/init/io): minimize io interface

We are moving to new compiler stack.

library/init/io.lean

@@ -33,8 +33,6 @@ abbreviation eio := except_t io.error io
 
 namespace io
 
-constant cmdline_args : io (list string)
-
 inductive fs.mode
 | read | write | read_write | append
 constant fs.handle : Type
@@ -72,8 +70,8 @@ constant handle.is_eof : handle → eio bool
 constant handle.flush : handle → eio unit
 constant handle.close : handle → eio unit
 -- TODO: replace `string` with byte buffer
---constant handle.read : handle → nat → eio string
-constant handle.write : handle → string → eio unit
+-- constant handle.read : handle → nat → eio string
+-- constant handle.write : handle → string → eio unit
 constant handle.get_line : handle → eio string
 
 def lift_eio {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m]
@@ -102,8 +100,8 @@ def handle.mk (s : string) (mode : mode) (bin : bool := ff) : m handle := prim.l
 def handle.is_eof : handle → m bool := prim.lift_eio ∘ prim.handle.is_eof
 def handle.flush : handle → m unit := prim.lift_eio ∘ prim.handle.flush
 def handle.close : handle → m unit := prim.lift_eio ∘ prim.handle.flush
---def handle.read (h : handle) (bytes : nat) : m string := prim.lift_eio (prim.handle.read h bytes)
-def handle.write (h : handle) (s : string) : m unit := prim.lift_eio (prim.handle.write h s)
+-- def handle.read (h : handle) (bytes : nat) : m string := prim.lift_eio (prim.handle.read h bytes)
+-- def handle.write (h : handle) (s : string) : m unit := prim.lift_eio (prim.handle.write h s)
 def handle.get_line : handle → m string := prim.lift_eio ∘ prim.handle.get_line
 
 /-
@@ -113,14 +111,14 @@ do b ← h.read 1,
    else pure b.mk_iterator.curr
 -/
 
-def handle.put_char (h : handle) (c : char) : m unit :=
-h.write (to_string c)
+-- def handle.put_char (h : handle) (c : char) : m unit :=
+-- h.write (to_string c)
 
-def handle.put_str (h : handle) (s : string) : m unit :=
-h.write s
+-- def handle.put_str (h : handle) (s : string) : m unit :=
+-- h.write s
 
-def handle.put_str_ln (h : handle) (s : string) : m unit :=
-h.put_str s *> h.put_str "\n"
+-- def handle.put_str_ln (h : handle) (s : string) : m unit :=
+-- h.put_str s *> h.put_str "\n"
 
 def handle.read_to_end (h : handle) : m string :=
 prim.lift_eio $ prim.iterate_eio "" $ λ r, do
@@ -138,16 +136,16 @@ do h ← handle.mk fname mode.read bin,
    h.close,
    pure r
 
-def write_file (fname : string) (data : string) (bin := ff) : m unit :=
-do h ← handle.mk fname mode.write bin,
-   h.write data,
-   h.close
+-- def write_file (fname : string) (data : string) (bin := ff) : m unit :=
+-- do h ← handle.mk fname mode.write bin,
+--   h.write data,
+--   h.close
 
 end fs
 
-constant stdin : io fs.handle
-constant stderr : io fs.handle
-constant stdout : io fs.handle
+-- constant stdin : io fs.handle
+-- constant stderr : io fs.handle
+-- constant stdout : io fs.handle
 
 /-
 namespace proc

src/library/vm/vm_io.cpp

@@ -101,27 +101,6 @@ static vm_obj to_obj(handle_ref && h) {
     return mk_vm_external(new vm_handle(std::move(h)));
 }
 
-/*
-struct vm_child : public vm_external {
-    std::shared_ptr<child> m_child;
-    vm_child(std::shared_ptr<child> && h):m_child(std::move(h)) {}
-    vm_child(std::shared_ptr<child> const & h):m_child(h) {}
-    virtual ~vm_child() {}
-    virtual void dealloc() override { delete this; }
-    virtual vm_external * clone(vm_clone_fn const &) override { return new vm_child(m_child); }
-    virtual vm_external * ts_clone(vm_clone_fn const &) override { lean_unreachable(); }
-};
-
-std::shared_ptr<child> const & to_child(vm_obj const & o) {
-    lean_vm_check(dynamic_cast<vm_child*>(to_external(o)));
-    return static_cast<vm_child*>(to_external(o))->m_child;
-}
-
-static vm_obj to_obj(std::shared_ptr<child> && h) {
-    return mk_vm_external(new vm_child(std::move(h)));
-}
-*/
-
 /*
 inductive io.mode
 | read | write | read_write | append
@@ -195,35 +174,6 @@ static vm_obj fs_close(vm_obj const & h, vm_obj const &) {
     }
 }
 
-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);
-    if (ferror(href->m_file)) {
-        clearerr(href->m_file);
-        return mk_ioe_failure("read failed");
-    }
-    return mk_ioe_result(to_obj(std::string(tmp.data(), sz)));
-}
-
-static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) {
-    handle_ref const & href = to_handle(h);
-
-    if (href->is_closed()) {
-        return mk_handle_has_been_closed_error();
-    }
-
-    try {
-        href->write(to_string(b));
-        return mk_ioe_result(mk_vm_unit());
-    } catch (handle_exception e) {
-        return mk_ioe_failure("write failed");
-    }
-}
-
 static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) {
     handle_ref const & href = to_handle(h);
 
@@ -247,84 +197,6 @@ static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) {
     return mk_ioe_result(to_obj(r));
 }
 
-static vm_obj fs_stdin(vm_obj const &) {
-    return mk_io_result(to_obj(std::make_shared<handle>(stdin)));
-}
-
-static vm_obj fs_stdout(vm_obj const &) {
-    return mk_io_result(to_obj(std::make_shared<handle>(stdout)));
-}
-
-static vm_obj fs_stderr(vm_obj const &) {
-    return mk_io_result(to_obj(std::make_shared<handle>(stderr)));
-}
-
-/*
-stdio to_stdio(vm_obj const & o) {
-    switch (cidx(o)) {
-    case 0:
-        return stdio::PIPED;
-    case 1:
-        return stdio::INHERIT;
-    case 2:
-        return stdio::NUL;
-    default:
-        lean_unreachable()
-    }
-}
-
-static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) {
-    return mk_io_result(mk_vm_nat(to_child(ch)->wait()));
-}
-*/
-
-/*
-static vm_obj io_get_env(vm_obj const & k, vm_obj const &) {
-    if (auto v = getenv(to_string(k).c_str())) {
-        return mk_io_result(mk_vm_some(to_obj(std::string(v))));
-    } else {
-        return mk_io_result(mk_vm_none());
-    }
-}
-
-static vm_obj io_get_cwd(vm_obj const &) {
-    char buffer[PATH_MAX];
-    auto cwd = getcwd(buffer, sizeof(buffer));
-    if (cwd) {
-        return mk_io_result(to_obj(std::string(cwd)));
-    } else {
-        return mk_ioe_failure("get_cwd failed");
-    }
-}
-
-static vm_obj io_set_cwd(vm_obj const & cwd, vm_obj const &) {
-    if (chdir(to_string(cwd).c_str()) == 0) {
-        return mk_io_result(mk_vm_unit());
-    } else {
-        return mk_ioe_failure("set_cwd failed");
-    }
-}
-*/
-
-static std::vector<std::string> * g_cmdline_args = nullptr;
-
-static vm_obj to_list(buffer<vm_obj> const & ls) {
-    vm_obj obj = mk_vm_simple(0);
-    for (unsigned i = ls.size(); i > 0; i--)
-        obj = mk_vm_constructor(1, ls[i - 1], obj);
-    return obj;
-}
-
-static vm_obj io_cmdline_args() {
-    buffer<vm_obj> objs;
-    for (auto & s : *g_cmdline_args) objs.push_back(to_obj(s));
-    return to_list(objs);
-}
-
-void set_io_cmdline_args(std::vector<std::string> const & args) {
-    *g_cmdline_args = args;
-}
-
 optional<vm_obj> is_ioe_result(vm_obj const & o) {
     auto r = cfield(o, 0);
     if (cidx(o) == 0)
@@ -341,39 +213,6 @@ optional<vm_obj> is_ioe_error(vm_obj const & o) {
         return optional<vm_obj>();
 }
 
-/*
-MK_THREAD_LOCAL_GET_DEF(vm_obj, get_rand_gen);
-
-vm_obj io_set_rand_gen(vm_obj const & g, vm_obj const &) {
-    get_rand_gen() = g;
-    return mk_io_result(mk_vm_unit());
-}
-
-vm_obj io_rand(vm_obj const & lo, vm_obj const & hi, vm_obj const &) {
-    vm_obj & gen = get_rand_gen();
-    if (is_simple(gen)) {
-        if (optional<unsigned> lo1 = try_to_unsigned(lo)) {
-            if (optional<unsigned> hi1 = try_to_unsigned(hi)) {
-                unsigned r = 0;
-                if (*lo1 < *hi1) {
-                    r = *lo1 + (std::rand() % (*hi1 - *lo1)); // NOLINT
-                }
-                return mk_io_result(mk_vm_nat(r));
-            }
-        }
-        mpz const & lo1 = vm_nat_to_mpz1(lo);
-        mpz const & hi1 = vm_nat_to_mpz2(hi);
-        mpz r(0);
-        if (lo1 < hi1) {
-            r = lo1 + (mpz(std::rand()) % (hi1 - lo1)); // NOLINT
-        }
-        return mk_io_result(mk_vm_nat(r));
-    } else {
-        return mk_ioe_failure("not implemented yet, io_rand_nat primitive has been deleted");
-    }
-}
-*/
-
 void initialize_vm_io() {
     DECLARE_VM_BUILTIN(name({"io", "prim", "put_str"}), io_put_str);
     DECLARE_VM_BUILTIN(name({"io", "prim", "get_line"}), io_get_line);
@@ -381,17 +220,9 @@ void initialize_vm_io() {
     DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "is_eof"}), fs_is_eof);
     DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "flush"}), fs_flush);
     DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "close"}), fs_close);
-    DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "read"}), fs_read);
-    DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "write"}), fs_write);
     DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "get_line"}), fs_get_line);
-    DECLARE_VM_BUILTIN(name({"io", "stdin"}), fs_stdin);
-    DECLARE_VM_BUILTIN(name({"io", "stdout"}), fs_stdout);
-    DECLARE_VM_BUILTIN(name({"io", "stderr"}), fs_stderr);
-    DECLARE_VM_BUILTIN(name({"io", "cmdline_args"}), io_cmdline_args);
-    g_cmdline_args = new std::vector<std::string>();
 }
 
 void finalize_vm_io() {
-    delete g_cmdline_args;
 }
 }

src/library/vm/vm_io.h

@@ -32,8 +32,6 @@ optional<vm_obj> is_ioe_error(vm_obj const & o);
 /* Convert an io.error object into a string */
 std::string io_error_to_string(vm_obj const & o);
 
-void set_io_cmdline_args(std::vector<std::string> const & args);
-
 void initialize_vm_io();
 void finalize_vm_io();
 }