From 3088c66f06384a580bb237b7512fb603c5c18f40 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:09:37 -0700 Subject: [PATCH 01/11] feat(library/noncomputable): mark all VM builtins as computable --- src/library/noncomputable.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 85d62f6ff207..26f19940aecb 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/quote.h" #include "library/constants.h" +#include "library/vm/vm.h" // TODO(Leo): move inline attribute declaration to library #include "library/compiler/inliner.h" namespace lean { @@ -62,17 +63,10 @@ struct noncomputable_modification : public modification { } }; -// TODO(Leo): implement better support for extending this set of builtin constants static bool is_builtin_extra(name const & n) { return - n == get_io_core_name() || n == get_sorry_ax_name() || - n == get_monad_io_impl_name() || - n == get_monad_io_terminal_impl_name() || - n == get_monad_io_file_system_impl_name() || - n == get_monad_io_environment_impl_name() || - n == get_monad_io_process_impl_name() || - n == get_monad_io_random_impl_name(); + is_vm_builtin_function(n); } static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) { From f6ba637378d9a0474b248055bc81e56cb823f5db Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:10:11 -0700 Subject: [PATCH 02/11] feat(library/noncomputable): sorts are computable i.e. constant io.real_world : Type --- src/library/noncomputable.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 26f19940aecb..8bddf1f86928 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -77,7 +77,8 @@ static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ex if (d.is_meta()) { return false; /* ignore nontrusted definitions */ } else if (d.is_axiom()) { - return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_builtin_extra(d.get_name()); + return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_sort(d.get_type()) && + !is_builtin_extra(d.get_name()); } else { return false; } From e7e98f1134ebbeea089dff79171cc6787a461c2a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:36:12 -0700 Subject: [PATCH 03/11] refactor(library/vm/vm_io,library/system/io): remove io classes, make errors explicit --- library/init/control/except.lean | 6 +- library/system/io.lean | 277 +++++++++++++--------- library/system/io_interface.lean | 85 ------- src/library/eval_helper.cpp | 7 +- src/library/tactic/tactic_state.cpp | 21 +- src/library/vm/vm_io.cpp | 348 +++++++--------------------- src/library/vm/vm_io.h | 20 +- 7 files changed, 292 insertions(+), 472 deletions(-) delete mode 100644 library/system/io_interface.lean diff --git a/library/init/control/except.lean b/library/init/control/except.lean index c0f71b5c6cde..35380f544f93 100644 --- a/library/init/control/except.lean +++ b/library/init/control/except.lean @@ -131,8 +131,12 @@ catch t₁ $ λ _, t₂ /-- Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orelse` uses the second. -/ -meta def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α := +def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α := catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if use_first_ex then e₁ else e₂) + +def lift_except [monad_except ε m] [monad m] {α : Type v} : except ε α → m α +| (except.error e) := throw e +| (except.ok a) := pure a end monad_except export monad_except (throw catch) diff --git a/library/system/io.lean b/library/system/io.lean index c45095b5bdb7..a9c9f74e5ac0 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -1,51 +1,91 @@ /- Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Luke Nelson, Jared Roesch and Leonardo de Moura +Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich -/ -import system.io_interface -/- The following constants have a builtin implementation -/ -constant io_core : Type → Type → Type 1 +prelude +import init.control.state init.control.except init.data.string.basic +import init.meta.tactic -/- Auxiliary definition used in the builtin implementation of monad_io_random_impl -/ --- def io_rand_nat : std_gen → nat → nat → nat × std_gen := --- rand_nat +/-- Like https://hackage.haskell.org/package/ghc-prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld. + Makes sure we never reorder `io` operations. -/ +constant io.real_world : Type +-- TODO: make opaque +@[irreducible, derive monad] +def io : Type → Type := state io.real_world -@[instance] constant monad_io_impl : monad_io io_core -@[instance] constant monad_io_terminal_impl : monad_io_terminal io_core -@[instance] constant monad_io_file_system_impl : monad_io_file_system io_core -@[instance] constant monad_io_environment_impl : monad_io_environment io_core -@[instance] constant monad_io_process_impl : monad_io_process io_core +abbreviation monad_io (m : Type → Type) := has_monad_lift_t io m -instance io_core_is_monad (e : Type) : monad (io_core e) := -monad_io_is_monad io_core e +-- TODO: make opaque +-- In the future, we may want to give more concrete data +-- like in https://doc.rust-lang.org/std/io/enum.ErrorKind.html +@[irreducible, derive has_to_string] +def io.error := string -instance io_core_is_monad_fail : monad_fail (io_core io.error) := -monad_io_is_monad_fail io_core +/-- 'io with errors'. A useful default monad stack to use for operations + in the `io` namespace if there is no need for additional layers or + a more specific error type than `io.error`. -/ +abbreviation eio := except_t io.error io -instance io_core_is_alternative : alternative (io_core io.error) := -monad_io_is_alternative io_core - -@[reducible] def io (α : Type) := -io_core io.error α +/- +inductive io.process.stdio +| piped +| inherit +| null + +structure io.process.spawn_args := +/- Command name. -/ +(cmd : string) +/- Arguments for the process -/ +(args : list string := []) +/- Configuration for the process' stdin handle. -/ +(stdin := stdio.inherit) +/- Configuration for the process' stdout handle. -/ +(stdout := stdio.inherit) +/- Configuration for the process' stderr handle. -/ +(stderr := stdio.inherit) +/- Working directory for the process. -/ +(cwd : option string := none) +/- Environment variables for the process. -/ +(env : list (string × option string) := []) + +class monad_io_file_system (m : Type → Type → Type 1) [monad_io m] := +/- Remark: in Haskell, they also provide (Maybe TextEncoding) and NewlineMode -/ +(mk_file_handle : string → io.mode → bool → m io.error (handle 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 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)) + +class monad_io_environment (m : Type → Type → Type 1) := +(get_env : string → m io.error (option string)) +-- we don't provide set_env as it is (thread-)unsafe (at least with glibc) +(get_cwd : m io.error string) +(set_cwd : string → m io.error unit) + +class monad_io_process (m : Type → Type → Type 1) [monad_io m] := +(child : Type) +(stdin : child → (handle m)) +(stdout : child → (handle m)) +(stderr : child → (handle m)) +(spawn : io.process.spawn_args → m io.error child) +(wait : child → m io.error nat) +-/ namespace io -/- Remark: the following definitions can be generalized and defined for any (m : Type -> Type -> Type 1) - that implements the required type classes. However, the generalized versions are very inconvenient to use, - (example: `#eval io.put_str "hello world"` does not work because we don't have enough information to infer `m`.). --/ -def iterate {e} {α β : Type} (a : α) (f : α → io_core e (sum α β)) : io_core e β := -monad_io.iterate e α β a f +/- +constant iterate {α β : Type} (a : α) (f : α → io (sum α β)) : io β -def forever {e} (a : io_core e unit) : io_core e unit := +def forever (a : io unit) : io unit := iterate () $ λ _, a >> return (sum.inl ()) --- TODO(Leo): delete after we merge #1881 -def catch {e₁ e₂ α} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) : io_core e₂ α := -monad_io.catch e₁ e₂ α a b - -def finally {α e} (a : io_core e α) (cleanup : io_core e unit) : io_core e α := do +def finally {α e} (a : io α) (cleanup : io unit) : io α := do res ← catch (sum.inr <$> a) (return ∘ sum.inl), cleanup, match res with @@ -55,110 +95,133 @@ match res with protected def fail {α : Type} (s : string) : io α := monad_io.fail io_core _ _ (io.error.other s) -def put_str : string → io unit := -monad_io_terminal.put_str io_core +namespace env -def put_str_ln (s : string) : io unit := -put_str s >> put_str "\n" +def get (env_var : string) : io (option string) := +monad_io_environment.get_env ionv_var -def get_line : io string := -monad_io_terminal.get_line io_core +/-- get the current working directory -/ +def get_cwd : io string := +monad_io_environment.get_cwd io_core -def cmdline_args : io (list string) := -return (monad_io_terminal.cmdline_args io_core) +/-- set the current working directory -/ +def set_cwd (cwd : string) : io unit := +monad_io_environment.set_cwd io_core cwd -def print {α} [has_to_string α] (s : α) : io unit := -put_str ∘ to_string $ s +end env +-/ -def print_ln {α} [has_to_string α] (s : α) : io unit := -print s >> put_str "\n" +constant cmdline_args : list string -def handle : Type := -monad_io.handle io_core +inductive fs.mode +| read | write | read_write | append +constant fs.handle : Type -def mk_file_handle (s : string) (m : mode) (bin : bool := ff) : io handle := -monad_io_file_system.mk_file_handle io_core s m bin +namespace prim +open fs -def stdin : io handle := -monad_io_file_system.stdin io_core +local notation `ioe` α := io (except io.error α) -def stderr : io handle := -monad_io_file_system.stderr io_core +constant iterate {α β : Type} : α → (α → io (sum α β)) → io β -def stdout : io handle := -monad_io_file_system.stdout io_core +def iterate_ioe {α β : Type} (a : α) (f : α → ioe (sum α β)) : ioe β := +iterate a $ λ r, do + r ← f r, + match r with + | except.ok (sum.inl r) := pure (sum.inl r) + | except.ok (sum.inr r) := pure (sum.inr (except.ok r)) + | except.error e := pure (sum.inr (except.error e)) -namespace env +constant put_str : string → ioe unit +constant get_line : ioe string +constant handle.mk (s : string) (m : mode) (bin : bool := ff) : ioe handle +constant handle.is_eof : handle → ioe bool +constant handle.flush : handle → ioe unit +constant handle.close : handle → ioe unit +-- TODO: replace `string` with byte buffer +--constant handle.read : handle → nat → ioe string +constant handle.write : handle → string → ioe unit +constant handle.get_line : handle → ioe string -def get (env_var : string) : io (option string) := -monad_io_environment.get_env io_core env_var +def lift_ioe {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] {α : Type} + (x : ioe α) : m α := +monad_lift x >>= monad_except.lift_except -/-- get the current working directory -/ -def get_cwd : io string := -monad_io_environment.get_cwd io_core +end prim -/-- set the current working directory -/ -def set_cwd (cwd : string) : io unit := -monad_io_environment.set_cwd io_core cwd +section +variables {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] -end env +def put_str : string → m unit := +prim.lift_ioe ∘ prim.put_str -namespace fs -def is_eof : handle → io bool := -monad_io_file_system.is_eof +def put_str_ln (s : string) : m unit := +put_str s >> put_str "\n" -def flush : handle → io unit := -monad_io_file_system.flush +def print {α} [has_to_string α] (s : α) : m unit := +put_str ∘ to_string $ s -def close : handle → io unit := -monad_io_file_system.close +def print_ln {α} [has_to_string α] (s : α) : m unit := +print s >> put_str "\n" +end -def read : handle → nat → io string := -monad_io_file_system.read +namespace fs +variables {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] -def write : handle → string → io unit := -monad_io_file_system.write +def handle.mk (s : string) (mode : mode) (bin : bool := ff) : m handle := prim.lift_ioe (prim.handle.mk s mode bin) +def handle.is_eof : handle → m bool := prim.lift_ioe ∘ prim.handle.is_eof +def handle.flush : handle → m unit := prim.lift_ioe ∘ prim.handle.flush +def handle.close : handle → m unit := prim.lift_ioe ∘ prim.handle.flush +--def handle.read (h : handle) (bytes : nat) : m string := prim.lift_ioe (prim.handle.read h bytes) +def handle.write (h : handle) (s : string) : m unit := prim.lift_ioe (prim.handle.write h s) +def handle.get_line : handle → m string := prim.lift_ioe ∘ prim.handle.get_line -def get_char (h : handle) : io char := -do b ← read h 1, - if b.is_empty then io.fail "get_char failed" +/- +def get_char (h : handle) : m char := +do b ← h.read 1, + if b.is_empty then fail "get_char failed" else return b.mk_iterator.curr +-/ -def get_line : handle → io string := -monad_io_file_system.get_line - -def put_char (h : handle) (c : char) : io unit := -write h (to_string c) +def handle.put_char (h : handle) (c : char) : m unit := +h.write (to_string c) -def put_str (h : handle) (s : string) : io unit := -write h s +def handle.put_str (h : handle) (s : string) : m unit := +h.write s -def put_str_ln (h : handle) (s : string) : io unit := -put_str h s >> put_str h "\n" +def handle.put_str_ln (h : handle) (s : string) : m unit := +h.put_str s >> h.put_str "\n" -def read_to_end (h : handle) : io string := -iterate "" $ λ r, - do done ← is_eof h, - if done - then return (sum.inr r) -- stop - else do - -- HACK: use less efficient `get_line` while `read` is broken - c ← get_line h, - return $ sum.inl (r ++ c) -- continue +def handle.read_to_end (h : handle) : m string := +prim.lift_ioe $ prim.iterate_ioe "" $ λ r, except_t.run $ do + done ← h.is_eof, + if done + then return (sum.inr r) -- stop + else do + -- HACK: use less efficient `get_line` while `read` is broken + c ← h.get_line, + return $ sum.inl (r ++ c) -- continue -def read_file (fname : string) (bin := ff) : io string := -do h ← mk_file_handle fname io.mode.read bin, - r ← read_to_end h, +/- +def read_file (fname : string) (bin := ff) : m string := +do h ← handle.mk fname mode.read bin, + r ← h.read_to_end, close h, return r +-/ -def write_file (fname : string) (data : string) (bin := ff) : io unit := -do h ← mk_file_handle fname io.mode.write bin, - write h data, - close h +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 : fs.handle +constant stderr : fs.handle +constant stdout : fs.handle + +/- namespace proc def child : Type := monad_io_process.child io_core @@ -179,7 +242,7 @@ def wait (c : child) : io nat := monad_io_process.wait c end proc - +-/ end io meta constant format.print_using : format → options → io unit @@ -193,6 +256,7 @@ format.print_using (to_fmt a) o meta definition pp {α : Type} [has_to_format α] (a : α) : io unit := format.print (to_fmt a) +/- /-- Run the external process specified by `args`. The process will run to completion with its output captured by a pipe, and @@ -204,6 +268,7 @@ do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args }, exitv ← io.proc.wait child, if exitv ≠ 0 then io.fail $ "process exited with status " ++ repr exitv else pure (), return s +-/ /-- This is the "back door" into the `io` monad, allowing IO computation to be performed during tactic execution. @@ -235,4 +300,4 @@ meta constant tactic.unsafe_run_io {α : Type} : io α → tactic α - One single goal of the form `⊢ true`. This action is mainly useful for writing tactics that inspect the environment. -/ -meta constant io.run_tactic {α : Type} (a : tactic α) : io α +meta constant io.run_tactic {α : Type} (a : tactic α) : except_t format io α diff --git a/library/system/io_interface.lean b/library/system/io_interface.lean deleted file mode 100644 index e59b37890ccb..000000000000 --- a/library/system/io_interface.lean +++ /dev/null @@ -1,85 +0,0 @@ -/- -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -inductive io.error -| other : string → io.error -| sys : nat → io.error - -inductive io.mode -| read | write | read_write | append - -inductive io.process.stdio -| piped -| inherit -| null - -structure io.process.spawn_args := -/- Command name. -/ -(cmd : string) -/- Arguments for the process -/ -(args : list string := []) -/- Configuration for the process' stdin handle. -/ -(stdin := stdio.inherit) -/- Configuration for the process' stdout handle. -/ -(stdout := stdio.inherit) -/- Configuration for the process' stderr handle. -/ -(stderr := stdio.inherit) -/- Working directory for the process. -/ -(cwd : option string := none) -/- Environment variables for the process. -/ -(env : list (string × option string) := []) - -class monad_io (m : Type → Type → Type 1) := -[monad : Π e, monad (m e)] --- TODO(Leo): use monad_except after it is merged -(catch : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α) -(fail : Π e α, e → m e α) -(iterate : Π e (α β : Type), α → (α → m e (sum α β)) → m e β) --- Primitive Types -(handle : Type) - -class monad_io_terminal (m : Type → Type → Type 1) := -(put_str : string → m io.error unit) -(get_line : m io.error string) -(cmdline_args : list string) - -open monad_io (handle) - -class monad_io_file_system (m : Type → Type → Type 1) [monad_io m] := -/- Remark: in Haskell, they also provide (Maybe TextEncoding) and NewlineMode -/ -(mk_file_handle : string → io.mode → bool → m io.error (handle 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 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)) - -class monad_io_environment (m : Type → Type → Type 1) := -(get_env : string → m io.error (option string)) --- we don't provide set_env as it is (thread-)unsafe (at least with glibc) -(get_cwd : m io.error string) -(set_cwd : string → m io.error unit) - -class monad_io_process (m : Type → Type → Type 1) [monad_io m] := -(child : Type) -(stdin : child → (handle m)) -(stdout : child → (handle m)) -(stderr : child → (handle m)) -(spawn : io.process.spawn_args → m io.error child) -(wait : child → m io.error nat) - -instance monad_io_is_monad (m : Type → Type → Type 1) (e : Type) [monad_io m] : monad (m e) := -monad_io.monad m e - -instance monad_io_is_monad_fail (m : Type → Type → Type 1) [monad_io m] : monad_fail (m io.error) := -{ fail := λ α s, monad_io.fail _ _ _ (io.error.other s) } - -instance monad_io_is_alternative (m : Type → Type → Type 1) [monad_io m] : alternative (m io.error) := -{ orelse := λ α a b, monad_io.catch _ _ _ a (λ _, b), - failure := λ α, monad_io.fail _ _ _ (io.error.other "failure") } diff --git a/src/library/eval_helper.cpp b/src/library/eval_helper.cpp index 3671af374556..cb1c3845e5c6 100644 --- a/src/library/eval_helper.cpp +++ b/src/library/eval_helper.cpp @@ -42,13 +42,14 @@ optional eval_helper::try_exec_io() { if (is_app_of(m_ty, get_io_name(), 1)) { m_args.push_back(mk_vm_simple(0)); // "world state" auto r = invoke_fn(); - if (auto error = is_io_error(r)) { + /* TODO? if (auto error = is_ioe_error(r)) { throw exception(io_error_to_string(*error)); - } else if (auto result = is_io_result(r)) { + } else if (auto result = is_ioe_result(r)) { return result; } else { throw exception("unexpected vm result of io expression"); - } + }*/ + return some(get_io_result(r)); } return optional(); } diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 20ae10851896..5f5e064b6786 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -37,6 +37,7 @@ Author: Leonardo de Moura #include "library/compiler/vm_compiler.h" #include "library/tactic/tactic_state.h" #include "library/tactic/simp_lemmas.h" +#include "library/tactic/tactic_evaluator.h" namespace lean { /* is_ts_safe is required by the interaction_state implementation. */ @@ -823,15 +824,8 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & } } -vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) { - vm_obj r = invoke(a, mk_vm_unit()); - if (optional a = is_io_result(r)) { - return tactic::mk_success(*a, tactic::to_state(s)); - } else { - optional e = is_io_error(r); - lean_assert(e); - return tactic::mk_exception(format(io_error_to_string(*e)), tactic::to_state(s)); - } +vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const &) { + return run_io(a); } vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) { @@ -839,11 +833,10 @@ vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) { tactic_state s = mk_tactic_state_for(vm.env(), vm.get_options(), "_io_run_tactic", metavar_context(), local_context(), mk_true()); vm_obj r = invoke(tac, to_obj(s)); - if (tactic::is_result_success(r)) { - return mk_io_result(tactic::get_success_value(r)); - } else { - return mk_io_failure("tactic failed"); // TODO(Leo): improve exception message - } + if (auto ex = tactic::is_exception(vm, r)) + return mk_ioe_failure(to_obj(mk_tactic_error_msg(std::get<2>(*ex), std::get<0>(*ex)))); + else + return mk_ioe_result(tactic::get_success_value(r)); } unsigned tactic_user_state::alloc(vm_obj const & v) { diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index a16ab73e4d71..75ae10a6e2ee 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -35,43 +35,53 @@ Author: Leonardo de Moura #include "library/vm/vm_list.h" namespace lean { -vm_obj io_core(vm_obj const &, vm_obj const &) { - return mk_vm_unit(); -} +static vm_obj const REAL_WORLD = mk_vm_simple(0); vm_obj mk_io_result(vm_obj const & r) { - return mk_vm_constructor(0, 1, &r); + return mk_vm_constructor(0, r, REAL_WORLD); +} + +vm_obj get_io_result(vm_obj const & r) { + return cfield(r, 0); +} + +vm_obj run_io(vm_obj const & act) { + auto r = invoke(act, REAL_WORLD); + return cfield(r, 0); } -vm_obj mk_io_failure(vm_obj const & e) { - return mk_vm_constructor(1, 1, &e); +vm_obj mk_ioe_result(vm_obj const & r) { + return mk_io_result(mk_vm_constructor(1, r)); } -vm_obj mk_io_failure(std::string const & s) { - return mk_io_failure(mk_vm_constructor(0, to_obj(s))); +vm_obj mk_ioe_failure(vm_obj const & e) { + return mk_io_result(mk_vm_constructor(0, e)); } -vm_obj mk_io_failure(sstream const & s) { - return mk_io_failure(mk_vm_constructor(0, to_obj(s.str()))); +vm_obj mk_ioe_failure(std::string const & s) { + return mk_ioe_failure(to_obj(s)); +} + +vm_obj mk_ioe_failure(sstream const & s) { + return mk_ioe_failure(s.str()); } static vm_obj io_put_str(vm_obj const & str, vm_obj const &) { - get_global_ios().get_regular_stream() << to_string(str); - return mk_io_result(mk_vm_unit()); + if ((get_global_ios().get_regular_stream() << to_string(str)).bad()) + return mk_ioe_failure("io.put_str failed"); + else + return mk_io_result(mk_vm_unit()); } static vm_obj io_get_line(vm_obj const &) { if (get_global_ios().get_options().get_bool("server")) - throw exception("get_line: cannot read from stdin in server mode"); + return mk_ioe_failure("io.get_line: cannot read from stdin in server mode"); std::string str; std::getline(std::cin, str); - return mk_io_result(to_obj(str)); -} - -static vm_obj cmdline_args_to_obj(std::vector const & ss) { - buffer objs; - for (auto & s : ss) objs.push_back(to_obj(s)); - return to_obj(objs); + if (std::cin.bad()) + return mk_ioe_failure("io.get_line failed"); + else + return mk_ioe_result(to_obj(str)); } struct vm_handle : public vm_external { @@ -93,6 +103,7 @@ 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)) {} @@ -111,6 +122,7 @@ std::shared_ptr const & to_child(vm_obj const & o) { static vm_obj to_obj(std::shared_ptr && h) { return mk_vm_external(new vm_child(std::move(h))); } +*/ /* inductive io.mode @@ -128,24 +140,24 @@ char const * to_c_io_mode(vm_obj const & mode, vm_obj const & bin) { lean_unreachable(); } -/* (mk_file_handle : string → io.mode → bool → m io.error handle) */ +/* (mk_file_handle : string → io.mode → bool → ioe handle) */ static vm_obj fs_mk_file_handle(vm_obj const & fname, vm_obj const & m, vm_obj const & bin, vm_obj const &) { FILE * h = fopen(to_string(fname).c_str(), to_c_io_mode(m, bin)); if (h != nullptr) - return mk_io_result(to_obj(std::make_shared(h))); + return mk_ioe_result(to_obj(std::make_shared(h))); else - return mk_io_failure(sstream() << "failed to open file '" << to_string(fname) << "'"); + return mk_ioe_failure(sstream() << "failed to open file '" << to_string(fname) << "'"); } static vm_obj mk_handle_has_been_closed_error() { - return mk_io_failure("invalid io action, handle has been closed"); + return mk_ioe_failure("invalid io action, handle has been closed"); } static vm_obj fs_is_eof(vm_obj const & h, vm_obj const &) { handle_ref const & href = to_handle(h); if (href->is_closed()) return mk_handle_has_been_closed_error(); bool r = feof(href->m_file) != 0; - return mk_io_result(mk_vm_bool(r)); + return mk_ioe_result(mk_vm_bool(r)); } static vm_obj fs_flush(vm_obj const & h, vm_obj const &) { @@ -157,9 +169,9 @@ static vm_obj fs_flush(vm_obj const & h, vm_obj const &) { try { href->flush(); - return mk_io_result(mk_vm_unit()); + return mk_ioe_result(mk_vm_unit()); } catch (handle_exception e) { - return mk_io_failure("flush failed"); + return mk_ioe_failure("flush failed"); } } @@ -171,17 +183,17 @@ static vm_obj fs_close(vm_obj const & h, vm_obj const &) { } if (href->is_stdin()) - return mk_io_failure("close failed, stdin cannot be closed"); + return mk_ioe_failure("close failed, stdin cannot be closed"); if (href->is_stdout()) - return mk_io_failure("close failed, stdout cannot be closed"); + return mk_ioe_failure("close failed, stdout cannot be closed"); if (href->is_stderr()) - return mk_io_failure("close failed, stderr cannot be closed"); + return mk_ioe_failure("close failed, stderr cannot be closed"); try { href->close(); - return mk_io_result(mk_vm_unit()); + return mk_ioe_result(mk_vm_unit()); } catch (handle_exception e) { - return mk_io_failure("close failed"); + return mk_ioe_failure("close failed"); } } @@ -194,9 +206,9 @@ static vm_obj fs_read(vm_obj const & h, vm_obj const & n, vm_obj const &) { size_t sz = fread(tmp.data(), 1, num, href->m_file); if (ferror(href->m_file)) { clearerr(href->m_file); - return mk_io_failure("read failed"); + return mk_ioe_failure("read failed"); } - return mk_io_result(to_obj(std::string(tmp.data(), sz))); + 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 &) { @@ -208,9 +220,9 @@ static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) { try { href->write(to_string(b)); - return mk_io_result(mk_vm_unit()); + return mk_ioe_result(mk_vm_unit()); } catch (handle_exception e) { - return mk_io_failure("write failed"); + return mk_ioe_failure("write failed"); } } @@ -226,7 +238,7 @@ static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) { int c = fgetc(href->m_file); if (ferror(href->m_file)) { clearerr(href->m_file); - return mk_io_failure("get_line failed"); + return mk_ioe_failure("get_line failed"); } if (c == EOF) break; @@ -234,49 +246,22 @@ static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) { if (c == '\n') break; } - return mk_io_result(to_obj(r)); + 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_stdin() { + return 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_stdout() { + return to_obj(std::make_shared(stdout)); } -static vm_obj fs_stderr(vm_obj const &) { - return mk_io_result(to_obj(std::make_shared(stderr))); +static vm_obj fs_stderr() { + return to_obj(std::make_shared(stderr)); } /* -class monad_io_file_system (m : Type → Type → Type) [monad_io m] := -/- Remark: in Haskell, they also provide (Maybe TextEncoding) and NewlineMode -/ -(mk_file_handle : string → io.mode → bool → m io.error (handle 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 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)) -*/ -static vm_obj monad_io_file_system_impl () { - return mk_vm_constructor(0, { - mk_native_closure(fs_mk_file_handle), - mk_native_closure(fs_is_eof), - mk_native_closure(fs_flush), - mk_native_closure(fs_close), - mk_native_closure(fs_read), - mk_native_closure(fs_write), - mk_native_closure(fs_get_line), - mk_native_closure(fs_stdin), - mk_native_closure(fs_stdout), - mk_native_closure(fs_stderr)}); -} - stdio to_stdio(vm_obj const & o) { switch (cidx(o)) { case 0: @@ -290,128 +275,25 @@ stdio to_stdio(vm_obj const & o) { } } -/* -structure spawn_args := - (cmd : string) - /- Add an argument to pass to the process. -/ - (args : list string) - /- Configuration for the process's stdin handle. -/ - (stdin := stdio.inherit) - /- Configuration for the process's stdout handle. -/ - (stdout := stdio.inherit) - /- Configuration for the process's stderr handle. -/ - (stderr := stdio.inherit) - (cwd : option string) - (env : list (string × option string)) -*/ -static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) { - std::string cmd = to_string(cfield(process_obj, 0)); - - list args = to_list(cfield(process_obj, 1), [&] (vm_obj const & o) -> std::string { - return to_string(o); - }); - auto stdin_stdio = to_stdio(cfield(process_obj, 2)); - auto stdout_stdio = to_stdio(cfield(process_obj, 3)); - auto stderr_stdio = to_stdio(cfield(process_obj, 4)); - - optional cwd; - if (!is_none(cfield(process_obj, 5))) - cwd = to_string(get_some_value(cfield(process_obj, 5))); - - lean::process proc(cmd, stdin_stdio, stdout_stdio, stderr_stdio); - - for (auto arg : args) { - proc.arg(arg); - } - - to_list(cfield(process_obj, 6), [&] (vm_obj const & o) { - auto k = to_string(cfield(o, 0)); - optional v; - if (!is_none(cfield(o, 1))) v = to_string(get_some_value(cfield(o, 1))); - proc.set_env(k, v); - return unit(); - }); - - if (cwd) proc.set_cwd(*cwd); - - return mk_io_result(to_obj(proc.spawn())); -} - static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) { return mk_io_result(mk_vm_nat(to_child(ch)->wait())); } - -/* -class monad_io_process (m : Type → Type → Type) [monad_io m] := -(child : Type) -(stdin : child → (handle m)) -(stdout : child → (handle m)) -(stderr : child → (handle m)) -(spawn : io.process.spawn_args → m io.error child) -(wait : child → m io.error nat) */ -static vm_obj monad_io_process_impl() { - return mk_vm_constructor(0, { - mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c)->get_stdin()); }), - mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c)->get_stdout()); }), - mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c)->get_stderr()); }), - mk_native_closure(io_process_spawn), - mk_native_closure(io_process_wait), - }); -} - -static vm_obj io_return(vm_obj const &, vm_obj const & a, vm_obj const &) { - return mk_io_result(a); -} - -static vm_obj io_bind(vm_obj const & /* α */, vm_obj const & /* β */, vm_obj const & a, vm_obj const & b, vm_obj const &) { - vm_obj r = invoke(a, mk_vm_unit()); - if (cidx(r) == 0) { - vm_obj v = cfield(r, 0); - return invoke(b, v, mk_vm_unit()); - } else { - return r; - } -} - -static vm_obj io_monad(vm_obj const &) { - vm_state & S = get_vm_state(); - vm_obj const & mk_monad = S.get_constant(get_monad_from_pure_bind_name()); - return invoke(mk_monad, mk_vm_simple(0), mk_native_closure(io_return), mk_native_closure(io_bind)); -} - -static vm_obj io_catch(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & b, vm_obj const &) { - vm_obj r = invoke(a, mk_vm_unit()); - if (cidx(r) == 1) { - vm_obj e = cfield(r, 0); - return invoke(b, e, mk_vm_unit()); - } else { - return r; - } -} - -static vm_obj io_fail(vm_obj const &, vm_obj const &, vm_obj const & e, vm_obj const &) { - return mk_io_failure(e); -} -/* (iterate : Π e (α β : Type), α → (α → m e (sum α β)) → m e β) */ +/* (iterate : Π e (α β : Type), α → (α → io e (sum α β)) → io e β) */ static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & fn, vm_obj const &) { vm_obj r = a; while (true) { - vm_obj p = invoke(fn, r, mk_vm_unit()); - if (cidx(p) == 1) { - return p; + vm_obj sum = invoke(fn, r, REAL_WORLD); + if (cidx(sum) == 1) { + return mk_io_result(cfield(sum, 0)); } else { - vm_obj v = cfield(p, 0); - if (cidx(v) == 1) { - return mk_io_result(cfield(v, 0)); - } else { - r = cfield(v, 0); - } + r = cfield(sum, 0); } } } +/* 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)))); @@ -426,7 +308,7 @@ static vm_obj io_get_cwd(vm_obj const &) { if (cwd) { return mk_io_result(to_obj(std::string(cwd))); } else { - return mk_io_failure("get_cwd failed"); + return mk_ioe_failure("get_cwd failed"); } } @@ -434,71 +316,33 @@ 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_io_failure("set_cwd failed"); + return mk_ioe_failure("set_cwd failed"); } } - -/* -class monad_io_environment (m : Type → Type → Type) := -(get_env : string → m io.error (option string)) --- we don't provide set_env as it is (thread-)unsafe (at least with glibc) -(get_cwd : m io.error string) -(set_cwd : string → m io.error unit) */ -vm_obj monad_io_environment_impl() { - return mk_vm_constructor(0, { - mk_native_closure(io_get_env), - mk_native_closure(io_get_cwd), - mk_native_closure(io_set_cwd), - }); -} - -/* -class monad_io (m : Type → Type → Type) := -[monad : Π e, monad (m e)] --- TODO(Leo): use monad_except after it is merged -(catch : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α) -(fail : Π e α, e → m e α) -(iterate : Π e α, α → (α → m e (option α)) → m e α) --- Primitive Types -(handle : Type) -*/ -vm_obj monad_io_impl() { - return mk_vm_constructor(0, { - mk_native_closure(io_monad), - mk_native_closure(io_catch), - mk_native_closure(io_fail), - mk_native_closure(io_iterate)}); - /* field handle is erased */ -} static std::vector * g_cmdline_args = nullptr; -void set_io_cmdline_args(std::vector const & args) { - *g_cmdline_args = args; +static vm_obj io_cmdline_args() { + buffer objs; + for (auto & s : *g_cmdline_args) objs.push_back(to_obj(s)); + return to_obj(objs); } -/* -class monad_io_terminal (m : Type → Type → Type) := -(put_str : string → m io.error unit) -(get_line : m io.error string) -(cmdline_args : list string) -*/ -vm_obj monad_io_terminal_impl() { - return mk_vm_constructor(0, { - mk_native_closure(io_put_str), - mk_native_closure(io_get_line), - cmdline_args_to_obj(*g_cmdline_args)}); +void set_io_cmdline_args(std::vector const & args) { + *g_cmdline_args = args; } -optional is_io_result(vm_obj const & o) { +optional is_ioe_result(vm_obj const & o) { + auto r = cfield(o, 0); if (cidx(o) == 0) return some(cfield(o, 0)); else return optional(); } -optional is_io_error(vm_obj const & o) { +optional is_ioe_error(vm_obj const & o) { + auto r = cfield(o, 0); if (cidx(o) == 1) return some(cfield(o, 0)); else @@ -506,20 +350,6 @@ optional is_io_error(vm_obj const & o) { } /* -inductive io.error -| other : string → io.error -| sys : nat → io.error -*/ -std::string io_error_to_string(vm_obj const & o) { - if (cidx(o) == 0) { - return to_string(cfield(o, 0)); - } else if (cidx(o) == 1) { - return (sstream() << "system error #" << to_unsigned(cfield(o, 0))).str(); - } - lean_vm_check(false); - lean_unreachable(); -} - MK_THREAD_LOCAL_GET_DEF(vm_obj, get_rand_gen); vm_obj io_set_rand_gen(vm_obj const & g, vm_obj const &) { @@ -547,24 +377,26 @@ vm_obj io_rand(vm_obj const & lo, vm_obj const & hi, vm_obj const &) { } return mk_io_result(mk_vm_nat(r)); } else { - return mk_io_failure("not implemented yet, io_rand_nat primitive has been deleted"); + return mk_ioe_failure("not implemented yet, io_rand_nat primitive has been deleted"); } } - -vm_obj monad_io_random_impl() { - return mk_vm_constructor(0, { - mk_native_closure(io_set_rand_gen), - mk_native_closure(io_rand) }); -} +*/ void initialize_vm_io() { - DECLARE_VM_BUILTIN(name("io_core"), io_core); - DECLARE_VM_BUILTIN(name("monad_io_impl"), monad_io_impl); - DECLARE_VM_BUILTIN(name("monad_io_terminal_impl"), monad_io_terminal_impl); - DECLARE_VM_BUILTIN(name("monad_io_file_system_impl"), monad_io_file_system_impl); - DECLARE_VM_BUILTIN(name("monad_io_environment_impl"), monad_io_environment_impl); - DECLARE_VM_BUILTIN(name("monad_io_process_impl"), monad_io_process_impl); - DECLARE_VM_BUILTIN(name("monad_io_random_impl"), monad_io_random_impl); + DECLARE_VM_BUILTIN(name({"io", "prim", "put_str"}), io_put_str); + DECLARE_VM_BUILTIN(name({"io", "prim", "get_line"}), io_get_line); + DECLARE_VM_BUILTIN(name({"io", "prim", "iterate"}), io_iterate); + DECLARE_VM_BUILTIN(name({"io", "prim", "handle", "mk"}), fs_mk_file_handle); + 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(); } diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h index a605e5394546..03d625c5713b 100644 --- a/src/library/vm/vm_io.h +++ b/src/library/vm/vm_io.h @@ -11,14 +11,24 @@ Author: Leonardo de Moura #include "library/handle.h" namespace lean { +/* `(r : α) → (α × real_world)` */ vm_obj mk_io_result(vm_obj const & r); -vm_obj mk_io_failure(std::string const & s); -/* The io monad produces a result object, or an error. +/* `(st : α × real_world) → α` */ +vm_obj get_io_result(vm_obj const & st); +/* `(act : io α) → α` */ +vm_obj run_io(vm_obj const & act); +/* `(r : α) → (except ε α × real_world)` */ +vm_obj mk_ioe_result(vm_obj const & r); +/* `(e : ε) → (except ε α × real_world)` */ +vm_obj mk_ioe_failure(vm_obj const & e); +/* `(s : string) → (except io.error α × real_world)` */ +vm_obj mk_ioe_failure(std::string const & s); +/* `ioe` produces a result object, or an error. If `o` is a result, then we return the result value. */ -optional is_io_result(vm_obj const & o); -/* The io monad produces a result object, or an error. +optional is_ioe_result(vm_obj const & o); +/* `ioe` produces a result object, or an error. If `o` is an error, then we return the io.error value. */ -optional is_io_error(vm_obj const & o); +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); From 4030a2d35645c0a576a01046177839d9a85e3b6f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:43:48 -0700 Subject: [PATCH 04/11] refactor(library/system/io): move into `init` --- gen/apply.lean | 2 +- library/init/default.lean | 2 +- library/{system => init}/io.lean | 0 script/gen_constants_cpp.py | 2 +- tests/ir/lirc.lean | 2 +- tests/lean/parsec1.lean | 2 +- tests/lean/reader1.lean | 2 +- tests/lean/run/deriv.lean | 2 +- tests/lean/run/ext_eff.lean | 2 +- tests/lean/run/handlers.lean | 2 +- tests/lean/run/lirc1.lean | 2 +- tests/lean/run/parser_ir1.lean | 2 +- tests/lean/trust0/t1.lean | 2 +- 13 files changed, 12 insertions(+), 12 deletions(-) rename library/{system => init}/io.lean (100%) diff --git a/gen/apply.lean b/gen/apply.lean index 0b3d4f3b3ac7..0e8d43f73e80 100644 --- a/gen/apply.lean +++ b/gen/apply.lean @@ -1,4 +1,4 @@ -import init.lean.config system.io +import init.lean.config init.io open io @[reducible] def m := reader_t handle io diff --git a/library/init/default.lean b/library/init/default.lean index 11b5a2a41c8f..69dcbfd8d119 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -6,4 +6,4 @@ Authors: Leonardo de Moura prelude import init.core init.control init.data.basic init.version import init.function init.util init.coe init.wf init.meta -import init.meta.well_founded_tactics init.data +import init.meta.well_founded_tactics init.data init.io diff --git a/library/system/io.lean b/library/init/io.lean similarity index 100% rename from library/system/io.lean rename to library/init/io.lean diff --git a/script/gen_constants_cpp.py b/script/gen_constants_cpp.py index 15529192ef86..f5b190a403b3 100755 --- a/script/gen_constants_cpp.py +++ b/script/gen_constants_cpp.py @@ -90,7 +90,7 @@ def main(argv=None): return 0 with open(tst_file, 'w') as f: f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n') - f.write("import system.io\n") + f.write("import init.io\n") f.write("open tactic\n"); f.write("meta def script_check_id (n : name) : tactic unit :=\n"); f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n"); diff --git a/tests/ir/lirc.lean b/tests/ir/lirc.lean index 199791b3676c..ac0c440dfc54 100644 --- a/tests/ir/lirc.lean +++ b/tests/ir/lirc.lean @@ -1,4 +1,4 @@ -import system.io +import init.io import init.lean.ir.lirc open lean.ir io diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean index 18ed23b91a92..4f9d29b5bf35 100644 --- a/tests/lean/parsec1.lean +++ b/tests/lean/parsec1.lean @@ -1,4 +1,4 @@ -import system.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format +import init.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format open lean.parser open lean.parser.monad_parsec diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean index 22c3d128b997..f4b784a01008 100644 --- a/tests/lean/reader1.lean +++ b/tests/lean/reader1.lean @@ -1,4 +1,4 @@ -import init.lean.parser.reader.module system.io +import init.lean.parser.reader.module init.io open lean.parser open lean.parser.reader diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean index 243e808ad064..aa2c673e7835 100644 --- a/tests/lean/run/deriv.lean +++ b/tests/lean/run/deriv.lean @@ -1,5 +1,5 @@ /- Benchmark for new code generator -/ -import system.io +import init.io inductive Expr | Val : int → Expr diff --git a/tests/lean/run/ext_eff.lean b/tests/lean/run/ext_eff.lean index 1e75acccc146..7340dad092ba 100644 --- a/tests/lean/run/ext_eff.lean +++ b/tests/lean/run/ext_eff.lean @@ -1,6 +1,6 @@ -- TODO: renable test after we restore tactic framework #exit -import system.io +import init.io /- An extensible effects library, inspired by "Freer Monads, More Extensible Effects" (O. Kiselyov, H. Ishii) and https://github.com/lexi-lambda/freer-simple -/ diff --git a/tests/lean/run/handlers.lean b/tests/lean/run/handlers.lean index b2ee9fc7ec99..16d62a076b81 100644 --- a/tests/lean/run/handlers.lean +++ b/tests/lean/run/handlers.lean @@ -1,4 +1,4 @@ -import system.io +import init.io /- Based on https://github.com/slindley/effect-handlers -/ diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean index 629851840adf..2696ebd5880e 100644 --- a/tests/lean/run/lirc1.lean +++ b/tests/lean/run/lirc1.lean @@ -1,4 +1,4 @@ -import system.io +import init.io import init.lean.ir.lirc open lean.ir diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index c0435291eb65..8a8f33919037 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -1,4 +1,4 @@ -import system.io +import init.io import init.lean.ir.parser init.lean.ir.format import init.lean.ir.elim_phi init.lean.ir.type_check import init.lean.ir.extract_cpp diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean index fd5d599a56c6..d083d257d5bf 100644 --- a/tests/lean/trust0/t1.lean +++ b/tests/lean/trust0/t1.lean @@ -1,2 +1,2 @@ -import system.io +import init.io #print trust From 5555d3f4a1b7dfc76729869916dec99b5007d803 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 14:47:19 -0700 Subject: [PATCH 05/11] feat(library/init/io): introduce `has_eval` class to customize `#eval` output --- library/init/io.lean | 39 +++++++++++++++++++++++++++++ src/frontends/lean/builtin_cmds.cpp | 12 +++++++++ src/library/constants.cpp | 8 ++++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ 5 files changed, 63 insertions(+) diff --git a/library/init/io.lean b/library/init/io.lean index a9c9f74e5ac0..290b86847885 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -301,3 +301,42 @@ meta constant tactic.unsafe_run_io {α : Type} : io α → tactic α This action is mainly useful for writing tactics that inspect the environment. -/ meta constant io.run_tactic {α : Type} (a : tactic α) : except_t format io α + + +universe u + +/-- Typeclass used for presenting the output of an `#eval` command. -/ +meta class has_eval (α : Type u) := +(eval : α → tactic unit) + +meta instance has_repr.has_eval {α : Type u} [has_repr α] : has_eval α := +⟨tactic.trace ∘ repr⟩ + +meta instance tactic.has_eval {α : Type} [has_eval α] : has_eval (tactic α) := +⟨(>>= has_eval.eval)⟩ + +-- special case: do not print `()` +meta instance tactic_unit.has_eval : has_eval (tactic unit) := +⟨id⟩ + +meta instance io.has_eval {α : Type} [has_eval α] : has_eval (io α) := +⟨λ x, tactic.unsafe_run_io x >>= has_eval.eval⟩ + +-- special case: do not print `()` +meta instance io_unit.has_eval : has_eval (io unit) := +⟨tactic.unsafe_run_io⟩ + +meta instance eio.has_eval {ε α : Type} [has_to_format ε] [has_eval α] : has_eval (except_t ε io α) := +⟨λ x, do + r ← tactic.unsafe_run_io x.run, + match r with + | except.error e := tactic.fail e + | except.ok a := has_eval.eval a⟩ + +-- special case: do not print `()` +meta instance eio_unit.has_eval {ε : Type} [has_to_format ε] : has_eval (except_t ε io unit) := +⟨λ x, do + r ← tactic.unsafe_run_io x.run, + match r with + | except.error e := tactic.fail e + | except.ok a := pure ()⟩ diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8edd0cd1a825..715266cda250 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -455,6 +455,18 @@ static environment eval_cmd(parser & p) { type_context_old tc(p.env(), transparency_mode::All); auto type = tc.infer(e); + + /* Check if resultant type has an instance of has_eval */ + try { + expr has_eval_type = mk_app(tc, get_has_eval_name(), type); + optional eval_instance = tc.mk_class_instance(has_eval_type); + if (eval_instance) { + /* Modify the 'program' to (has_eval.eval e) */ + e = mk_app(tc, get_has_eval_eval_name(), 3, type, *eval_instance, e); + type = tc.infer(e); + } + } catch (exception &) {} + bool has_repr_inst = false; /* Check if resultant type has an instance of has_repr */ diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 770a0f417b5d..0cf181ace0c7 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -74,6 +74,8 @@ name const * g_has_bind_and_then = nullptr; name const * g_has_bind_seq = nullptr; name const * g_has_div_div = nullptr; name const * g_has_emptyc_emptyc = nullptr; +name const * g_has_eval = nullptr; +name const * g_has_eval_eval = nullptr; name const * g_has_insert_insert = nullptr; name const * g_has_neg_neg = nullptr; name const * g_has_one = nullptr; @@ -328,6 +330,8 @@ void initialize_constants() { g_has_bind_seq = new name{"has_bind", "seq"}; g_has_div_div = new name{"has_div", "div"}; g_has_emptyc_emptyc = new name{"has_emptyc", "emptyc"}; + g_has_eval = new name{"has_eval"}; + g_has_eval_eval = new name{"has_eval", "eval"}; g_has_insert_insert = new name{"has_insert", "insert"}; g_has_neg_neg = new name{"has_neg", "neg"}; g_has_one = new name{"has_one"}; @@ -583,6 +587,8 @@ void finalize_constants() { delete g_has_bind_seq; delete g_has_div_div; delete g_has_emptyc_emptyc; + delete g_has_eval; + delete g_has_eval_eval; delete g_has_insert_insert; delete g_has_neg_neg; delete g_has_one; @@ -837,6 +843,8 @@ name const & get_has_bind_and_then_name() { return *g_has_bind_and_then; } name const & get_has_bind_seq_name() { return *g_has_bind_seq; } name const & get_has_div_div_name() { return *g_has_div_div; } name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; } +name const & get_has_eval_name() { return *g_has_eval; } +name const & get_has_eval_eval_name() { return *g_has_eval_eval; } name const & get_has_insert_insert_name() { return *g_has_insert_insert; } name const & get_has_neg_neg_name() { return *g_has_neg_neg; } name const & get_has_one_name() { return *g_has_one; } diff --git a/src/library/constants.h b/src/library/constants.h index 54a711229a3f..76aa89b55538 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -76,6 +76,8 @@ name const & get_has_bind_and_then_name(); name const & get_has_bind_seq_name(); name const & get_has_div_div_name(); name const & get_has_emptyc_emptyc_name(); +name const & get_has_eval_name(); +name const & get_has_eval_eval_name(); name const & get_has_insert_insert_name(); name const & get_has_neg_neg_name(); name const & get_has_one_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 51fa7af78a48..faa9b018c862 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -69,6 +69,8 @@ has_bind.and_then has_bind.seq has_div.div has_emptyc.emptyc +has_eval +has_eval.eval has_insert.insert has_neg.neg has_one From afc4c5e8fc7a9bed483924a0b3f5fd7b9c8bfa82 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 17:05:31 -0700 Subject: [PATCH 06/11] fix(library/{vm/vm_io,init/io}): fix bugs and tests --- library/init/io.lean | 4 +--- src/library/tactic/tactic_state.cpp | 4 ++-- src/library/vm/vm_io.cpp | 8 ++++---- tests/lean/parsec1.lean | 8 ++++---- tests/lean/reader1.lean | 6 +++--- tests/lean/run/deriv.lean | 6 +++--- tests/lean/run/lirc1.lean | 3 +-- tests/lean/run/parser_ir1.lean | 7 +++---- 8 files changed, 21 insertions(+), 25 deletions(-) diff --git a/library/init/io.lean b/library/init/io.lean index 290b86847885..bb208e2b401c 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -202,13 +202,11 @@ prim.lift_ioe $ prim.iterate_ioe "" $ λ r, except_t.run $ do c ← h.get_line, return $ sum.inl (r ++ c) -- continue -/- def read_file (fname : string) (bin := ff) : m string := do h ← handle.mk fname mode.read bin, r ← h.read_to_end, - close h, + h.close, return r --/ def write_file (fname : string) (data : string) (bin := ff) : m unit := do h ← handle.mk fname mode.write bin, diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 5f5e064b6786..f35a7a2e72c3 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -824,8 +824,8 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & } } -vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const &) { - return run_io(a); +vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) { + return tactic::mk_success(run_io(a), s); } vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) { diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 75ae10a6e2ee..383f50804255 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -70,7 +70,7 @@ static vm_obj io_put_str(vm_obj const & str, vm_obj const &) { if ((get_global_ios().get_regular_stream() << to_string(str)).bad()) return mk_ioe_failure("io.put_str failed"); else - return mk_io_result(mk_vm_unit()); + return mk_ioe_result(mk_vm_unit()); } static vm_obj io_get_line(vm_obj const &) { @@ -280,11 +280,11 @@ static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) { } */ -/* (iterate : Π e (α β : Type), α → (α → io e (sum α β)) → io e β) */ -static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & fn, vm_obj const &) { +/* (iterate : Π (α β : Type), α → (α → io (sum α β)) → io β) */ +static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & fn, vm_obj const &) { vm_obj r = a; while (true) { - vm_obj sum = invoke(fn, r, REAL_WORLD); + vm_obj sum = cfield(invoke(fn, r, REAL_WORLD), 0); if (cidx(sum) == 1) { return mk_io_result(cfield(sum, 0)); } else { diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean index 4f9d29b5bf35..c0aa0aaccc16 100644 --- a/tests/lean/parsec1.lean +++ b/tests/lean/parsec1.lean @@ -1,18 +1,18 @@ -import init.io init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format +import init.lean.parser.identifier init.lean.ir.parser init.lean.ir.format open lean.parser open lean.parser.monad_parsec -def test {α} [decidable_eq α] (p : parsec' α) (s : string) (e : α) : io unit := +def test {α} [decidable_eq α] (p : parsec' α) (s : string) (e : α) : eio unit := match parsec.parse p s with | except.ok a := if a = e then return () else io.print_ln "unexpected result" | except.error e := io.print_ln e -def test_failure {α} (p : parsec' α) (s : string) : io unit := +def test_failure {α} (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with | except.ok a := io.print_ln "unexpected success" | except.error e := return () -def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : io unit := +def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with | except.ok a := io.print_ln "result: " >> io.print_ln (repr $ to_string a) | except.error e := io.print_ln e diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean index f4b784a01008..cfb5ddc6234e 100644 --- a/tests/lean/reader1.lean +++ b/tests/lean/reader1.lean @@ -2,7 +2,7 @@ import init.lean.parser.reader.module init.io open lean.parser open lean.parser.reader -def show_result (p : lean.parser.reader) (s : string) : io unit := +def show_result (p : lean.parser.reader) (s : string) : eio unit := let (stx, errors) := p.parse ⟨⟩ s in when (stx.reprint ≠ s) ( io.print_ln "reprint fail:" *> @@ -49,10 +49,10 @@ end b" #eval (do { let (stx, _) := mixfix.reader.parse ⟨⟩ "prefix `+`:10 := _", some {root := stx, ..} ← pure $ reader.parse.view stx, - some stx ← pure $ mixfix.expand stx | io.fail "expand fail", + some stx ← pure $ mixfix.expand stx | throw "expand fail", io.print_ln stx, io.print_ln stx.reprint -} : io unit) +} : eio unit) -- slowly progressing... #eval do diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean index aa2c673e7835..f5e7c7494056 100644 --- a/tests/lean/run/deriv.lean +++ b/tests/lean/run/deriv.lean @@ -78,18 +78,18 @@ def Expr.to_string : Expr → string instance : has_to_string Expr := ⟨Expr.to_string⟩ -meta def nest (f : Expr → io Expr) : nat → Expr → io Expr +meta def nest (f : Expr → eio Expr) : nat → Expr → eio Expr | 0 x := return x | (n+1) x := f x >>= nest n -meta def deriv (f : Expr) : io Expr := +meta def deriv (f : Expr) : eio Expr := do let d := d "x" f, io.put_str "count: ", io.put_str_ln (to_string (count f)), return d -meta def main : io unit := +meta def main : eio unit := do let x := Var "x", let f := pow x x, nest deriv 9 f, diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean index 2696ebd5880e..58a37084d851 100644 --- a/tests/lean/run/lirc1.lean +++ b/tests/lean/run/lirc1.lean @@ -1,8 +1,7 @@ -import init.io import init.lean.ir.lirc open lean.ir -def comp (s : string) : io unit := +def comp (s : string) : eio unit := match lirc s with | except.ok r := io.print r | except.error e := io.print "Error: " >> io.print e diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index 8a8f33919037..8a456f114f85 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -1,4 +1,3 @@ -import init.io import init.lean.ir.parser init.lean.ir.format import init.lean.ir.elim_phi init.lean.ir.type_check import init.lean.ir.extract_cpp @@ -7,12 +6,12 @@ open lean.parser open lean.parser.monad_parsec open lean.ir -def check_decl (d : decl) : io unit := +def check_decl (d : decl) : eio unit := match type_check d with | except.ok _ := return () | except.error e := io.print_ln (to_string e) -def show_result (p : parsec' decl) (s : string) : io unit := +def show_result (p : parsec' decl) (s : string) : eio unit := match parsec.parse p s with | except.ok d := io.print_ln (lean.to_fmt d) >> check_decl d | except.error e := io.print_ln e @@ -44,7 +43,7 @@ end: #eval show_result (whitespace >> parse_def) IR2 -def tst_elim_phi (s : string) : io unit := +def tst_elim_phi (s : string) : eio unit := do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s, check_decl d, io.print_ln (lean.to_fmt (elim_phi d)) From 7cf2452e7c2ff4c068a12eb88b0ea767bf9aed17 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 18:41:22 -0700 Subject: [PATCH 07/11] feat(library/init/{io,control/except}): use `lift_t` to automatically upcast io and other errors --- library/init/coe.lean | 4 ++-- library/init/control/except.lean | 9 +++++++-- library/init/io.lean | 11 ++++++++--- library/init/lean/parser/parsec.lean | 4 ++++ tests/lean/reader1.lean | 2 +- tests/lean/run/parser_ir1.lean | 14 ++++++++------ 6 files changed, 30 insertions(+), 14 deletions(-) diff --git a/library/init/coe.lean b/library/init/coe.lean index 2f75dd122e7b..b957794556e1 100644 --- a/library/init/coe.lean +++ b/library/init/coe.lean @@ -88,8 +88,8 @@ universes u₁ u₂ u₃ instance lift_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_lift a b] [has_lift_t b c] : has_lift_t a c := ⟨λ x, lift_t (lift x : b)⟩ -instance lift_base {a : Sort u} {b : Sort v} [has_lift a b] : has_lift_t a b := -⟨lift⟩ +instance lift_refl {a : Sort u} : has_lift_t a a := +⟨id⟩ instance coe_trans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c := ⟨λ x, coe_t (coe_b x : b)⟩ diff --git a/library/init/control/except.lean b/library/init/control/except.lean index 35380f544f93..c4f9a4c202ea 100644 --- a/library/init/control/except.lean +++ b/library/init/control/except.lean @@ -7,6 +7,7 @@ The except monad transformer. -/ prelude import init.control.alternative init.control.lift init.data.to_string +import init.control.monad_fail universes u v w inductive except (ε : Type u) (α : Type v) @@ -134,8 +135,8 @@ catch t₁ $ λ _, t₂ def orelse' [monad_except ε m] {α : Type v} (t₁ t₂ : m α) (use_first_ex := tt) : m α := catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if use_first_ex then e₁ else e₂) -def lift_except [monad_except ε m] [monad m] {α : Type v} : except ε α → m α -| (except.error e) := throw e +def lift_except {ε' : Type u} [monad_except ε m] [has_lift_t ε' ε] [monad m] {α : Type v} : except ε' α → m α +| (except.error e) := throw ↑e | (except.ok a) := pure a end monad_except @@ -171,3 +172,7 @@ end instance (ε m out) [monad_run out m] : monad_run (λ α, out (except ε α)) (except_t ε m) := ⟨λ α, run ∘ except_t.run⟩ + +-- useful for implicit failures in do-notation +instance (m) [monad m] : monad_fail (except_t string m) := +⟨λ _, throw⟩ diff --git a/library/init/io.lean b/library/init/io.lean index bb208e2b401c..e0b0eaaa8528 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -23,6 +23,11 @@ abbreviation monad_io (m : Type → Type) := has_monad_lift_t io m @[irreducible, derive has_to_string] def io.error := string +-- The `io` primitives can also be used with [monad_except string m] +-- via this error conversion +instance : has_lift io.error string := +⟨to_string⟩ + /-- 'io with errors'. A useful default monad stack to use for operations in the `io` namespace if there is no need for additional layers or a more specific error type than `io.error`. -/ @@ -143,14 +148,14 @@ constant handle.close : handle → ioe unit constant handle.write : handle → string → ioe unit constant handle.get_line : handle → ioe string -def lift_ioe {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] {α : Type} +def lift_ioe {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] (x : ioe α) : m α := monad_lift x >>= monad_except.lift_except end prim section -variables {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] +variables {m : Type → Type} {ε : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] def put_str : string → m unit := prim.lift_ioe ∘ prim.put_str @@ -166,7 +171,7 @@ print s >> put_str "\n" end namespace fs -variables {m : Type → Type} [monad_io m] [monad_except io.error m] [monad m] +variables {m : Type → Type} {ε : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] def handle.mk (s : string) (mode : mode) (bin : bool := ff) : m handle := prim.lift_ioe (prim.handle.mk s mode bin) def handle.is_eof : handle → m bool := prim.lift_ioe ∘ prim.handle.is_eof diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 3273da296163..52eeddec1c23 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -41,6 +41,10 @@ if ex_list = [] then "" else "expected " ++ expected.to_string ex_list instance {μ : Type} : has_to_string (message μ) := ⟨message.to_string⟩ +-- use for e.g. upcasting parsec errors with `monad_except.lift_except` +instance {μ : Type} : has_lift (message μ) string := +⟨to_string⟩ + /- Remark: we store expected "error" messages in `ok_eps` results. They contain the error that would have occurred if a diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean index cfb5ddc6234e..10f7749c8e0b 100644 --- a/tests/lean/reader1.lean +++ b/tests/lean/reader1.lean @@ -52,7 +52,7 @@ end b" some stx ← pure $ mixfix.expand stx | throw "expand fail", io.print_ln stx, io.print_ln stx.reprint -} : eio unit) +} : except_t string io unit) -- slowly progressing... #eval do diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index 8a456f114f85..f659549d42c6 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -6,12 +6,14 @@ open lean.parser open lean.parser.monad_parsec open lean.ir -def check_decl (d : decl) : eio unit := +abbreviation m := except_t string io + +def check_decl (d : decl) : m unit := match type_check d with | except.ok _ := return () | except.error e := io.print_ln (to_string e) -def show_result (p : parsec' decl) (s : string) : eio unit := +def show_result (p : parsec' decl) (s : string) : m unit := match parsec.parse p s with | except.ok d := io.print_ln (lean.to_fmt d) >> check_decl d | except.error e := io.print_ln e @@ -43,8 +45,8 @@ end: #eval show_result (whitespace >> parse_def) IR2 -def tst_elim_phi (s : string) : eio unit := -do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s, +def tst_elim_phi (s : string) : m unit := +do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, check_decl d, io.print_ln (lean.to_fmt (elim_phi d)) @@ -64,8 +66,8 @@ main: " #eval show_result (whitespace >> parse_def) IR3 -def tst_extract_cpp (s : string) : io unit := -do (except.ok d) ← return $ parsec.parse (whitespace >> parse_def) s, +def tst_extract_cpp (s : string) : m unit := +do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, check_decl d, match extract_cpp [elim_phi d] with | except.ok code := io.print_ln code From 7acc674b3c3a071cf181556c9776c1afe0edee21 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 18:45:44 -0700 Subject: [PATCH 08/11] refactor(library/init/io): replace `ioe` with `eio` Old MacDonald had a monad stack eio = except_t io.error io And in his stack he had I/O, io = state io.real_world With a monad here and a monad there Here a monad there a monad Everywhere a monad! --- library/init/io.lean | 50 +++++++++++++++++++++----------------------- 1 file changed, 24 insertions(+), 26 deletions(-) diff --git a/library/init/io.lean b/library/init/io.lean index e0b0eaaa8528..dfce863b0cec 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -125,32 +125,30 @@ constant fs.handle : Type namespace prim open fs -local notation `ioe` α := io (except io.error α) - constant iterate {α β : Type} : α → (α → io (sum α β)) → io β -def iterate_ioe {α β : Type} (a : α) (f : α → ioe (sum α β)) : ioe β := -iterate a $ λ r, do - r ← f r, +def iterate_eio {α β : Type} (a : α) (f : α → eio (sum α β)) : eio β := +except_t.mk $ iterate a $ λ r, do + r ← (f r).run, match r with | except.ok (sum.inl r) := pure (sum.inl r) | except.ok (sum.inr r) := pure (sum.inr (except.ok r)) | except.error e := pure (sum.inr (except.error e)) -constant put_str : string → ioe unit -constant get_line : ioe string -constant handle.mk (s : string) (m : mode) (bin : bool := ff) : ioe handle -constant handle.is_eof : handle → ioe bool -constant handle.flush : handle → ioe unit -constant handle.close : handle → ioe unit +constant put_str : string → eio unit +constant get_line : eio string +constant handle.mk (s : string) (m : mode) (bin : bool := ff) : eio handle +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 → ioe string -constant handle.write : handle → string → ioe unit -constant handle.get_line : handle → ioe string +--constant handle.read : handle → nat → eio string +constant handle.write : handle → string → eio unit +constant handle.get_line : handle → eio string -def lift_ioe {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] - (x : ioe α) : m α := -monad_lift x >>= monad_except.lift_except +def lift_eio {m : Type → Type} {ε α : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] + (x : eio α) : m α := +monad_lift x.run >>= monad_except.lift_except end prim @@ -158,7 +156,7 @@ section variables {m : Type → Type} {ε : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] def put_str : string → m unit := -prim.lift_ioe ∘ prim.put_str +prim.lift_eio ∘ prim.put_str def put_str_ln (s : string) : m unit := put_str s >> put_str "\n" @@ -173,13 +171,13 @@ end namespace fs variables {m : Type → Type} {ε : Type} [monad_io m] [monad_except ε m] [has_lift_t io.error ε] [monad m] -def handle.mk (s : string) (mode : mode) (bin : bool := ff) : m handle := prim.lift_ioe (prim.handle.mk s mode bin) -def handle.is_eof : handle → m bool := prim.lift_ioe ∘ prim.handle.is_eof -def handle.flush : handle → m unit := prim.lift_ioe ∘ prim.handle.flush -def handle.close : handle → m unit := prim.lift_ioe ∘ prim.handle.flush ---def handle.read (h : handle) (bytes : nat) : m string := prim.lift_ioe (prim.handle.read h bytes) -def handle.write (h : handle) (s : string) : m unit := prim.lift_ioe (prim.handle.write h s) -def handle.get_line : handle → m string := prim.lift_ioe ∘ prim.handle.get_line +def handle.mk (s : string) (mode : mode) (bin : bool := ff) : m handle := prim.lift_eio (prim.handle.mk s mode bin) +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.get_line : handle → m string := prim.lift_eio ∘ prim.handle.get_line /- def get_char (h : handle) : m char := @@ -198,7 +196,7 @@ 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_ioe $ prim.iterate_ioe "" $ λ r, except_t.run $ do +prim.lift_eio $ prim.iterate_eio "" $ λ r, do done ← h.is_eof, if done then return (sum.inr r) -- stop From 1ba3c3cb630b4a55c001d66c57d65a241aafcecf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 19:01:16 -0700 Subject: [PATCH 09/11] fix(library/vm/vm_io): move all primitives into `io` While `cmdline_args` has no side-effects, it is certainly not a pure function. The `stdin` etc. should have been safe since all accessors are in `io`, but better be safe than sorry. --- library/init/io.lean | 8 ++++---- src/library/vm/vm_io.cpp | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/library/init/io.lean b/library/init/io.lean index dfce863b0cec..11c12deab051 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -116,7 +116,7 @@ monad_io_environment.set_cwd io_core cwd end env -/ -constant cmdline_args : list string +constant cmdline_args : io (list string) inductive fs.mode | read | write | read_write | append @@ -218,9 +218,9 @@ do h ← handle.mk fname mode.write bin, end fs -constant stdin : fs.handle -constant stderr : fs.handle -constant stdout : 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 383f50804255..00277ee2f47c 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -249,16 +249,16 @@ 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() { - return to_obj(std::make_shared(stdin)); +static vm_obj fs_stdin(vm_obj const &) { + return mk_io_result(to_obj(std::make_shared(stdin))); } -static vm_obj fs_stdout() { - return to_obj(std::make_shared(stdout)); +static vm_obj fs_stdout(vm_obj const &) { + return mk_io_result(to_obj(std::make_shared(stdout))); } -static vm_obj fs_stderr() { - return to_obj(std::make_shared(stderr)); +static vm_obj fs_stderr(vm_obj const &) { + return mk_io_result(to_obj(std::make_shared(stderr))); } /* From 7bd57c9749f8f34fce25b234a12cac3be69178e7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Aug 2018 19:41:18 -0700 Subject: [PATCH 10/11] feat(library/init/control/coroutine_io): coroutine_io --- library/init/control/coroutine_io.lean | 113 +++++++++++++++++++++++++ library/init/io.lean | 10 +++ tests/lean/run/coroutine.lean | 34 +++++++- 3 files changed, 153 insertions(+), 4 deletions(-) create mode 100644 library/init/control/coroutine_io.lean diff --git a/library/init/control/coroutine_io.lean b/library/init/control/coroutine_io.lean new file mode 100644 index 000000000000..d6bd220e045b --- /dev/null +++ b/library/init/control/coroutine_io.lean @@ -0,0 +1,113 @@ +/- +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Sebastian Ullrich +-/ +prelude +import init.io init.control.coroutine + +/-! A variant of `coroutine` on top of `io`. Implementation. -/ + +universes u v w r s + +namespace coroutine_io +variables {α δ β γ : Type} + +export coroutine_result_io (done yielded) + +/-- `resume c a` resumes/invokes the coroutine_io `c` with input `a`. -/ +@[inline] def resume : coroutine_io α δ β → α → io (coroutine_result_io α δ β) +| (mk k) a := k a + +@[inline] protected def pure (b : β) : coroutine_io α δ β := +mk $ λ _, pure (done b) + +/-- Read the input argument passed to the coroutine. + Remark: should we use a different name? I added an instance [monad_reader] later. -/ +@[inline] protected def read : coroutine_io α δ α := +mk $ λ a, pure (done a) + +/-- Return the control to the invoker with result `d` -/ +@[inline] protected def yield (d : δ) : coroutine_io α δ punit := +mk $ λ a : α, pure $ yielded d (coroutine_io.pure ⟨⟩) + +/- +TODO(Leo): following relations have been commented because Lean4 is currently +accepting non-terminating programs. + +/-- Auxiliary relation for showing that bind/pipe terminate -/ +inductive direct_subcoroutine_io : coroutine_io α δ β → coroutine_io α δ β → Prop +| mk : ∀ (k : α → coroutine_result α δ β) (a : α) (d : δ) (c : coroutine_io α δ β), k a = yielded d c → direct_subcoroutine_io c (mk k) + +theorem direct_subcoroutine_wf : well_founded (@direct_subcoroutine_io α δ β) := +begin + constructor, intro c, + apply @coroutine.ind _ _ _ + (λ c, acc direct_subcoroutine_io c) + (λ r, ∀ (d : δ) (c : coroutine_io α δ β), r = yielded d c → acc direct_subcoroutine_io c), + { intros k ih, dsimp at ih, constructor, intros c' h, cases h, apply ih h_a h_d, assumption }, + { intros, contradiction }, + { intros d c ih d₁ c₁ heq, injection heq, subst c, assumption } +end + +/-- Transitive closure of direct_subcoroutine. It is not used here, but may be useful when defining + more complex procedures. -/ +def subcoroutine_io : coroutine_io α δ β → coroutine_io α δ β → Prop := +tc direct_subcoroutine_io + +theorem subcoroutine_wf : well_founded (@subcoroutine_io α δ β) := +tc.wf direct_subcoroutine_wf + +-- Local instances for proving termination by well founded relation + +def bind_wf_inst : has_well_founded (Σ' a : coroutine_io α δ β, (β → coroutine_io α δ γ)) := +{ r := psigma.lex direct_subcoroutine_io (λ _, empty_relation), + wf := psigma.lex_wf direct_subcoroutine_wf (λ _, empty_wf) } + +def pipe_wf_inst : has_well_founded (Σ' a : coroutine_io α δ β, coroutine_io δ γ β) := +{ r := psigma.lex direct_subcoroutine_io (λ _, empty_relation), + wf := psigma.lex_wf direct_subcoroutine_wf (λ _, empty_wf) } + +local attribute [instance] wf_inst₁ wf_inst₂ + +open well_founded_tactics + +-/ + +protected def bind : coroutine_io α δ β → (β → coroutine_io α δ γ) → coroutine_io α δ γ +| (mk k) f := mk $ λ a, k a >>= λ r, + match r, rfl : ∀ (n : _), n = r → _ with + | done b, _ := coroutine_io.resume (f b) a + | yielded d c, h := + -- have direct_subcoroutine_io c (mk k), { apply direct_subcoroutine.mk k a d, rw h }, + pure $ yielded d (bind c f) +-- using_well_founded { dec_tac := unfold_wf_rel >> process_lex (tactic.assumption) } + +def pipe : coroutine_io α δ β → coroutine_io δ γ β → coroutine_io α γ β +| (mk k₁) (mk k₂) := mk $ λ a, do + r ← k₁ a, + match r, rfl : ∀ (n : _), n = r → _ with + | done b, h := pure (done b) + | yielded d k₁', h := do + r ← k₂ d, + pure $ match r with + | done b := done b + | yielded r k₂' := + -- have direct_subcoroutine_io k₁' (mk k₁), { apply direct_subcoroutine.mk k₁ a d, rw h }, + yielded r (pipe k₁' k₂') +-- using_well_founded { dec_tac := unfold_wf_rel >> process_lex (tactic.assumption) } + +instance : monad (coroutine_io α δ) := +{ pure := @coroutine_io.pure _ _, + bind := @coroutine_io.bind _ _ } + +instance : monad_reader α (coroutine_io α δ) := +{ read := @coroutine_io.read _ _ } + +instance (α δ : Type) : coroutine.monad_coroutine α δ (coroutine_io α δ) := +{ yield := coroutine_io.yield } + +instance : monad_io (coroutine_io α δ) := +{ monad_lift := λ _ x, mk (λ _, done <$> x) } + +end coroutine_io diff --git a/library/init/io.lean b/library/init/io.lean index 11c12deab051..a6108f1e3d55 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -341,3 +341,13 @@ meta instance eio_unit.has_eval {ε : Type} [has_to_format ε] : has_eval (excep match r with | except.error e := tactic.fail e | except.ok a := pure ()⟩ + + +local attribute [reducible] io +/-- A variant of `coroutine` on top of `io` -/ +mutual inductive coroutine_io, coroutine_result_io (α δ β: Type) +with coroutine_io : Type +| mk {} : (α → io coroutine_result_io) → coroutine_io +with coroutine_result_io : Type +| done {} : β → coroutine_result_io +| yielded {} : δ → coroutine_io → coroutine_result_io diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index ca5503567041..11647bd51715 100644 --- a/tests/lean/run/coroutine.lean +++ b/tests/lean/run/coroutine.lean @@ -1,5 +1,4 @@ -import init.control.coroutine -import system.io +import init.control.coroutine init.control.coroutine_io universes u v open coroutine @@ -18,7 +17,7 @@ def visit {α : Type v} : tree α → coroutine unit α unit yield a, visit r -def tst {α : Type} [has_to_string α] (t : tree α) : io unit := +def tst {α : Type} [has_to_string α] (t : tree α) : except_t string io unit := do c ← pure $ visit t, (yielded v₁ c) ← pure $ resume c (), (yielded v₂ c) ← pure $ resume c (), @@ -43,7 +42,7 @@ do yield ("2) val: " ++ to_string (x+y)), return () -def tst2 : io unit := +def tst2 : except_t string io unit := do let c := state_t.run ex 5, (yielded r c₁) ← pure $ resume c 10, io.print_ln r, @@ -56,4 +55,31 @@ do let c := state_t.run ex 5, return () #eval tst2 + +def ex3 : except_t string (coroutine_io nat string) unit := +do + x ← read, + io.print_ln $ "got " ++ to_string x, + yield ("1) val: " ++ to_string x), + x ← read, + io.print_ln $ "got " ++ to_string x, + yield ("2) val: " ++ to_string x), + throw "my_error" + +open coroutine_io +def tst3 : except_t string io unit := +do let c := ex3.run, + (yielded r c₁) ← monad_lift $ c.resume 10, + io.print_ln r, + (yielded r c₂) ← monad_lift $ c₁.resume 20, + io.print_ln r, + (done (except.error e)) ← monad_lift $ c₂.resume 30, + io.print_ln $ "error: " ++ e, + (yielded r c₃) ← monad_lift $ c₁.resume 100, + io.print_ln r, + io.print_ln "done", + return () + +#eval tst3 + end ex2 From 8e4aed5eb8c0a37f806bc387969db18ac660cccf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 17 Aug 2018 15:25:16 -0700 Subject: [PATCH 11/11] chore(library/init/io): rename `io.print_ln` to `io.println` --- library/init/io.lean | 2 +- old_tests/tests/lean/io_bug2.lean | 4 ++-- old_tests/tests/lean/run/io_state.lean | 4 ++-- tests/lean/parsec1.lean | 10 +++++----- tests/lean/reader1.lean | 18 +++++++++--------- tests/lean/run/coroutine.lean | 26 +++++++++++++------------- tests/lean/run/ext_eff.lean | 8 ++++---- tests/lean/run/parser_ir1.lean | 12 ++++++------ 8 files changed, 42 insertions(+), 42 deletions(-) diff --git a/library/init/io.lean b/library/init/io.lean index a6108f1e3d55..01b2532b93e5 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -164,7 +164,7 @@ put_str s >> put_str "\n" def print {α} [has_to_string α] (s : α) : m unit := put_str ∘ to_string $ s -def print_ln {α} [has_to_string α] (s : α) : m unit := +def println {α} [has_to_string α] (s : α) : m unit := print s >> put_str "\n" end diff --git a/old_tests/tests/lean/io_bug2.lean b/old_tests/tests/lean/io_bug2.lean index dba3ef4e69a4..ac7a499fcae0 100644 --- a/old_tests/tests/lean/io_bug2.lean +++ b/old_tests/tests/lean/io_bug2.lean @@ -2,8 +2,8 @@ import system.io open io def main : io unit := do - print_ln "t1", + println "t1", (x, y) ← return ((1 : nat), (2 : ℕ)), - print_ln "t2" + println "t2" #eval main diff --git a/old_tests/tests/lean/run/io_state.lean b/old_tests/tests/lean/run/io_state.lean index 2566b8ca21f4..8d8f924c0694 100644 --- a/old_tests/tests/lean/run/io_state.lean +++ b/old_tests/tests/lean/run/io_state.lean @@ -8,10 +8,10 @@ instance lift_io {α} : has_coe (io α) (my_io α) := def tst : my_io unit := do x ← get, - print_ln x, + println x, put (x+10), y ← get, - print_ln y, + println y, put_str "end of program" #eval tst.run 5 diff --git a/tests/lean/parsec1.lean b/tests/lean/parsec1.lean index c0aa0aaccc16..be95f9aef373 100644 --- a/tests/lean/parsec1.lean +++ b/tests/lean/parsec1.lean @@ -4,18 +4,18 @@ open lean.parser.monad_parsec def test {α} [decidable_eq α] (p : parsec' α) (s : string) (e : α) : eio unit := match parsec.parse p s with -| except.ok a := if a = e then return () else io.print_ln "unexpected result" -| except.error e := io.print_ln e +| except.ok a := if a = e then return () else io.println "unexpected result" +| except.error e := io.println e def test_failure {α} (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with -| except.ok a := io.print_ln "unexpected success" +| except.ok a := io.println "unexpected success" | except.error e := return () def show_result {α} [has_to_string α] (p : parsec' α) (s : string) : eio unit := match parsec.parse p s with -| except.ok a := io.print_ln "result: " >> io.print_ln (repr $ to_string a) -| except.error e := io.print_ln e +| except.ok a := io.println "result: " >> io.println (repr $ to_string a) +| except.error e := io.println e #eval test (ch 'a') "a" 'a' #eval test any "a" 'a' diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean index 10f7749c8e0b..7c1e9a05e220 100644 --- a/tests/lean/reader1.lean +++ b/tests/lean/reader1.lean @@ -5,17 +5,17 @@ open lean.parser.reader def show_result (p : lean.parser.reader) (s : string) : eio unit := let (stx, errors) := p.parse ⟨⟩ s in when (stx.reprint ≠ s) ( - io.print_ln "reprint fail:" *> - io.print_ln stx.reprint + io.println "reprint fail:" *> + io.println stx.reprint ) *> match errors with | [] := do - io.print_ln "result: ", - io.print_ln (to_string stx) + io.println "result: ", + io.println (to_string stx) | _ := do - errors.mfor $ λ e, io.print_ln e, - io.print_ln "partial syntax tree:", - io.print_ln (to_string stx) + errors.mfor $ λ e, io.println e, + io.println "partial syntax tree:", + io.println (to_string stx) #eval show_result module.reader "prelude" #eval show_result module.reader "import me" @@ -50,8 +50,8 @@ end b" let (stx, _) := mixfix.reader.parse ⟨⟩ "prefix `+`:10 := _", some {root := stx, ..} ← pure $ reader.parse.view stx, some stx ← pure $ mixfix.expand stx | throw "expand fail", - io.print_ln stx, - io.print_ln stx.reprint + io.println stx, + io.println stx.reprint } : except_t string io unit) -- slowly progressing... diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index 11647bd51715..385f221c771d 100644 --- a/tests/lean/run/coroutine.lean +++ b/tests/lean/run/coroutine.lean @@ -21,8 +21,8 @@ def tst {α : Type} [has_to_string α] (t : tree α) : except_t string io unit : do c ← pure $ visit t, (yielded v₁ c) ← pure $ resume c (), (yielded v₂ c) ← pure $ resume c (), - io.print_ln $ to_string v₁, - io.print_ln $ to_string v₂, + io.println $ to_string v₁, + io.println $ to_string v₂, return () #eval tst (tree.node (tree.node (tree.node tree.leaf 5 tree.leaf) 10 (tree.node tree.leaf 20 tree.leaf)) 30 tree.leaf) @@ -45,13 +45,13 @@ do def tst2 : except_t string io unit := do let c := state_t.run ex 5, (yielded r c₁) ← pure $ resume c 10, - io.print_ln r, + io.println r, (yielded r c₂) ← pure $ resume c₁ 20, - io.print_ln r, + io.println r, (done _) ← pure $ resume c₂ 30, (yielded r c₃) ← pure $ resume c₁ 100, - io.print_ln r, - io.print_ln "done", + io.println r, + io.println "done", return () #eval tst2 @@ -59,10 +59,10 @@ do let c := state_t.run ex 5, def ex3 : except_t string (coroutine_io nat string) unit := do x ← read, - io.print_ln $ "got " ++ to_string x, + io.println $ "got " ++ to_string x, yield ("1) val: " ++ to_string x), x ← read, - io.print_ln $ "got " ++ to_string x, + io.println $ "got " ++ to_string x, yield ("2) val: " ++ to_string x), throw "my_error" @@ -70,14 +70,14 @@ open coroutine_io def tst3 : except_t string io unit := do let c := ex3.run, (yielded r c₁) ← monad_lift $ c.resume 10, - io.print_ln r, + io.println r, (yielded r c₂) ← monad_lift $ c₁.resume 20, - io.print_ln r, + io.println r, (done (except.error e)) ← monad_lift $ c₂.resume 30, - io.print_ln $ "error: " ++ e, + io.println $ "error: " ++ e, (yielded r c₃) ← monad_lift $ c₁.resume 100, - io.print_ln r, - io.print_ln "done", + io.println r, + io.println "done", return () #eval tst3 diff --git a/tests/lean/run/ext_eff.lean b/tests/lean/run/ext_eff.lean index 7340dad092ba..8d499163f3cd 100644 --- a/tests/lean/run/ext_eff.lean +++ b/tests/lean/run/ext_eff.lean @@ -190,8 +190,8 @@ def test1 := r ← monad_lift $ exfn x, modify (λ xs, "end"::xs), pure r in - do repr <$> eff.run_m (tf tt) >>= io.print_ln, - repr <$> eff.run_m (tf ff) >>= io.print_ln + do repr <$> eff.run_m (tf tt) >>= io.println, + repr <$> eff.run_m (tf ff) >>= io.println #eval test1 @@ -203,8 +203,8 @@ def test2 := r ← monad_lift $ exfn x, modify (λ xs, "end"::xs), pure r in - do repr <$> eff.run_m (tf tt) >>= io.print_ln, - repr <$> eff.run_m (tf ff) >>= io.print_ln + do repr <$> eff.run_m (tf tt) >>= io.println, + repr <$> eff.run_m (tf ff) >>= io.println #eval test2 diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index f659549d42c6..e6370c405553 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -11,12 +11,12 @@ abbreviation m := except_t string io def check_decl (d : decl) : m unit := match type_check d with | except.ok _ := return () -| except.error e := io.print_ln (to_string e) +| except.error e := io.println (to_string e) def show_result (p : parsec' decl) (s : string) : m unit := match parsec.parse p s with -| except.ok d := io.print_ln (lean.to_fmt d) >> check_decl d -| except.error e := io.print_ln e +| except.ok d := io.println (lean.to_fmt d) >> check_decl d +| except.error e := io.println e def IR1 := " def succ (x : uint32) : uint32 := @@ -48,7 +48,7 @@ end: def tst_elim_phi (s : string) : m unit := do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, check_decl d, - io.print_ln (lean.to_fmt (elim_phi d)) + io.println (lean.to_fmt (elim_phi d)) #eval tst_elim_phi IR2 @@ -70,8 +70,8 @@ def tst_extract_cpp (s : string) : m unit := do d ← monad_except.lift_except $ parsec.parse (whitespace >> parse_def) s, check_decl d, match extract_cpp [elim_phi d] with - | except.ok code := io.print_ln code - | except.error s := io.print_ln s + | except.ok code := io.println code + | except.error s := io.println s #eval tst_extract_cpp IR3 #eval tst_extract_cpp IR2