diff --git a/library/init/io.lean b/library/init/io.lean index 8d6ccd7ca4..0ec3af3228 100644 --- a/library/init/io.lean +++ b/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 diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index ec01e1cf00..24c3c78758 100644 --- a/src/library/vm/vm_io.cpp +++ b/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 m_child; - vm_child(std::shared_ptr && h):m_child(std::move(h)) {} - vm_child(std::shared_ptr 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 const & to_child(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(to_external(o))->m_child; -} - -static vm_obj to_obj(std::shared_ptr && 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 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(stdin))); -} - -static vm_obj fs_stdout(vm_obj const &) { - return mk_io_result(to_obj(std::make_shared(stdout))); -} - -static vm_obj fs_stderr(vm_obj const &) { - return mk_io_result(to_obj(std::make_shared(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 * g_cmdline_args = nullptr; - -static vm_obj to_list(buffer 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 objs; - for (auto & s : *g_cmdline_args) objs.push_back(to_obj(s)); - return to_list(objs); -} - -void set_io_cmdline_args(std::vector const & args) { - *g_cmdline_args = args; -} - optional is_ioe_result(vm_obj const & o) { auto r = cfield(o, 0); if (cidx(o) == 0) @@ -341,39 +213,6 @@ optional is_ioe_error(vm_obj const & o) { return optional(); } -/* -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 lo1 = try_to_unsigned(lo)) { - if (optional 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(); } void finalize_vm_io() { - delete g_cmdline_args; } } diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h index 03d625c571..5538c528db 100644 --- a/src/library/vm/vm_io.h +++ b/src/library/vm/vm_io.h @@ -32,8 +32,6 @@ optional 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 const & args); - void initialize_vm_io(); void finalize_vm_io(); }