diff --git a/library/init/io.lean b/library/init/io.lean index 815c271f31..b4f809d7ae 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -30,12 +30,16 @@ In the future, we may want to give more concrete data like in https://doc.rust-lang.org/std/IO/enum.ErrorKind.html -/ @[derive HasToString Inhabited] -def IO.error := String +def IO.Error := String -def IO.userError (s : String) : IO.error := +def IO.userError (s : String) : IO.Error := s -abbrev IO : Type → Type := EIO IO.error +@[export lean.io_error_to_string_core] +def IO.Error.toString : IO.Error → String := +id + +abbrev IO : Type → Type := EIO IO.Error @[inline] unsafe def unsafeIO {α : Type} (fn : IO α) : Option α := diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index a630dfc44e..97269a3616 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "runtime/sstream.h" #include "runtime/thread.h" #include "util/map_foreach.h" +#include "util/io.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" #include "kernel/type_checker.h" @@ -28,13 +29,8 @@ object* set_extension_core(object*, object*, object*); object* environment_set_main_module_core(object*, object*); object* environment_main_module_core(object*); -object* mk_empty_environment(uint32 trust_lvl) { - object* r = mk_empty_environment_core(trust_lvl, io_mk_world()); - if (io_result_is_error(r)) { dec(r); throw exception("error creating empty environment"); } - object* env = io_result_get_value(r); - inc(env); - dec(r); - return env; +environment mk_empty_environment(uint32 trust_lvl) { + return get_io_result(mk_empty_environment_core(trust_lvl, io_mk_world())); } environment::environment(unsigned trust_lvl): diff --git a/src/library/module.cpp b/src/library/module.cpp index 66a65feb07..75c9a6cddf 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -18,6 +18,7 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich #include "runtime/hash.h" #include "runtime/io.h" #include "runtime/compact.h" +#include "util/io.h" #include "util/lean_path.h" #include "util/buffer.h" #include "util/name_map.h" @@ -204,13 +205,7 @@ def writeModule (env : Environment) (fname : String) : IO Unit := */ object * write_module_core(object * env, object * fname, object * w); void write_module(environment const & env, std::string const & olean_fn) { - object * r = write_module_core(env.to_obj_arg(), mk_string(olean_fn), io_mk_world()); - if (io_result_is_error(r)) { - dec_ref(r); - throw exception(sstream() << "failed to write module '" << olean_fn << "'"); - } else { - dec_ref(r); - } + consume_io_result(write_module_core(env.to_obj_arg(), mk_string(olean_fn), io_mk_world())); } /* @@ -221,16 +216,7 @@ object * import_modules_core(object * mod_names, uint32 trust_level, object * w) environment import_modules(unsigned trust_lvl, std::vector const & imports) { names mods(imports.begin(), imports.end()); - object * r = import_modules_core(mods.steal(), trust_lvl, io_mk_world()); - if (io_result_is_error(r)) { - dec_ref(r); - io_result_show_error(r); // TODO(Leo): move to exception - throw exception("failed to import modules"); - } else { - environment env(io_result_get_value(r), true); - dec_ref(r); - return env; - } + return get_io_result(import_modules_core(mods.steal(), trust_lvl, io_mk_world())); } object * environment_add_modification_core(object * env, object * mod); diff --git a/src/runtime/object.h b/src/runtime/object.h index 9652bc3f00..b325fd767c 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -1484,7 +1484,7 @@ inline obj_res io_mk_world() { inline bool io_result_is_ok(b_obj_arg r) { return cnstr_tag(r) == 0; } inline bool io_result_is_error(b_obj_arg r) { return cnstr_tag(r) == 1; } inline b_obj_res io_result_get_value(b_obj_arg r) { lean_assert(io_result_is_ok(r)); return cnstr_get(r, 0); } -inline b_obj_arg io_result_get_error(b_obj_arg r) { lean_assert(io_result_is_error(r)); return cnstr_get(r, 0); } +inline b_obj_res io_result_get_error(b_obj_arg r) { lean_assert(io_result_is_error(r)); return cnstr_get(r, 0); } void io_result_show_error(b_obj_arg r); void io_mark_end_initialization(); diff --git a/src/stage0/init/io.cpp b/src/stage0/init/io.cpp index 33656c4f90..4cb7bb857e 100644 --- a/src/stage0/init/io.cpp +++ b/src/stage0/init/io.cpp @@ -20,6 +20,9 @@ obj* l_IO_println(obj*); obj* l_IO_Ref_set___boxed(obj*, obj*); obj* l_IO_Fs_handle_isEof___at_IO_Fs_handle_readToEnd___spec__1___boxed(obj*, obj*); obj* l_ioOfExcept___rarg(obj*, obj*, obj*); +namespace lean { +obj* io_error_to_string_core(obj*); +} obj* l_IO_Ref_get___rarg(obj*, obj*, obj*); obj* l_EState_Monad(obj*, obj*); obj* l_IO_Ref_swap___boxed(obj*, obj*); @@ -32,7 +35,6 @@ obj* l_IO_Ref_swap(obj*, obj*); obj* l_EIO_Inhabited___rarg(obj*); obj* l_HasRepr_HasEval___rarg(obj*, obj*, obj*); obj* l_IO_Prim_Ref_swap___boxed(obj*, obj*, obj*, obj*); -obj* l_IO_error_Inhabited; obj* l_IO_Fs_handle_mk(obj*, obj*); extern "C" obj* lean_io_prim_handle_is_eof(obj*, obj*); obj* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(obj*, obj*); @@ -42,6 +44,7 @@ obj* l_IO_print___boxed(obj*, obj*); obj* l_IO_print___at_HasRepr_HasEval___spec__2___boxed(obj*, obj*); obj* l_IO_Prim_iterate___at_IO_Fs_handle_readToEnd___spec__3___boxed(obj*, obj*, obj*); obj* l_IO_Ref_reset___rarg(obj*, obj*, obj*); +obj* l_IO_Error_Inhabited; obj* l_EIO_Inhabited(obj*, obj*); obj* l_unsafeIO(obj*); obj* l_IO_Prim_iterate___at_IO_Fs_handle_readToEnd___spec__3(obj*, obj*, obj*); @@ -64,6 +67,7 @@ obj* l_IO_Prim_Ref_get___boxed(obj*, obj*, obj*); extern "C" obj* lean_io_prim_get_line(obj*); extern "C" obj* lean_io_allocprof(obj*, obj*, obj*, obj*); obj* l_IO_Ref_set___rarg(obj*, obj*, obj*, obj*); +obj* l_IO_Error_HasToString; obj* l_IO_print___rarg(obj*, obj*, obj*, obj*); obj* l_IO_userError___boxed(obj*); obj* l_IO_Prim_getLine___boxed(obj*); @@ -86,7 +90,6 @@ obj* l_IO_Prim_liftIO(obj*, obj*); obj* l_IO_Inhabited(obj*); obj* l_IO_Ref_modify___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*); obj* l_IO_Prim_handle_close___boxed(obj*, obj*); -obj* l_IO_error_HasToString; obj* l_IO_Prim_handle_flush___boxed(obj*, obj*); obj* l_IO_println___boxed(obj*); obj* l_ioOfExcept(obj*, obj*); @@ -204,7 +207,7 @@ x_3 = lean::alloc_closure(reinterpret_cast(l_EIO_Inhabited___rarg), 1, 0) return x_3; } } -obj* _init_l_IO_error_HasToString() { +obj* _init_l_IO_Error_HasToString() { _start: { obj* x_1; @@ -212,7 +215,7 @@ x_1 = lean::alloc_closure(reinterpret_cast(l_String_HasToString___boxed), return x_1; } } -obj* _init_l_IO_error_Inhabited() { +obj* _init_l_IO_Error_Inhabited() { _start: { obj* x_1; @@ -236,6 +239,14 @@ lean::dec(x_1); return x_2; } } +namespace lean { +obj* io_error_to_string_core(obj* x_1) { +_start: +{ +return x_1; +} +} +} obj* _init_l_unsafeIO___rarg___closed__1() { _start: { @@ -1733,10 +1744,10 @@ l_EIO_Monad___closed__1 = _init_l_EIO_Monad___closed__1(); lean::mark_persistent(l_EIO_Monad___closed__1); l_EIO_MonadExcept___closed__1 = _init_l_EIO_MonadExcept___closed__1(); lean::mark_persistent(l_EIO_MonadExcept___closed__1); -l_IO_error_HasToString = _init_l_IO_error_HasToString(); -lean::mark_persistent(l_IO_error_HasToString); -l_IO_error_Inhabited = _init_l_IO_error_Inhabited(); -lean::mark_persistent(l_IO_error_Inhabited); +l_IO_Error_HasToString = _init_l_IO_Error_HasToString(); +lean::mark_persistent(l_IO_Error_HasToString); +l_IO_Error_Inhabited = _init_l_IO_Error_Inhabited(); +lean::mark_persistent(l_IO_Error_Inhabited); l_unsafeIO___rarg___closed__1 = _init_l_unsafeIO___rarg___closed__1(); lean::mark_persistent(l_unsafeIO___rarg___closed__1); l_IO_println___rarg___closed__1 = _init_l_IO_println___rarg___closed__1(); diff --git a/src/util/io.h b/src/util/io.h new file mode 100644 index 0000000000..90dd4f6b05 --- /dev/null +++ b/src/util/io.h @@ -0,0 +1,39 @@ +/* +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "runtime/exception.h" +#include "runtime/object.h" +#include "util/string_ref.h" + +namespace lean { +object* io_error_to_string_core(object * err); + +template T get_io_result(object * o) { + if (io_result_is_error(o)) { + object * err_obj = io_result_get_error(o); + inc(err_obj); + dec(o); + string_ref error(io_error_to_string_core(err_obj)); + throw exception(error.to_std_string()); + } else { + T r(io_result_get_value(o), true); + dec(o); + return r; + } +} + +inline void consume_io_result(object * o) { + if (io_result_is_error(o)) { + object * err_obj = io_result_get_error(o); + inc(err_obj); + dec(o); + string_ref error(io_error_to_string_core(err_obj)); + throw exception(error.to_std_string()); + } + dec(o); +} +}