diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index cd2f626249..a92d1ce7da 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -696,7 +696,7 @@ emitLns [ "static bool _G_initialized = false;", "lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {", "lean_object * res;", - "if (_G_initialized) return lean_mk_io_result(lean_box(0));", + "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));", "_G_initialized = true;" ]; env.imports.forM $ fun imp => emitLns [ @@ -705,7 +705,7 @@ env.imports.forM $ fun imp => emitLns [ "lean_dec_ref(res);"]; let decls := getDecls env; decls.reverse.forM emitDeclInit; -emitLns ["return lean_mk_io_result(lean_box(0));", "}"] +emitLns ["return lean_io_result_mk_ok(lean_box(0));", "}"] def main : M Unit := do emitFileHeader; diff --git a/src/include/lean/io.h b/src/include/lean/io.h index 2b1ffb747e..9cd9b7f962 100644 --- a/src/include/lean/io.h +++ b/src/include/lean/io.h @@ -10,10 +10,10 @@ Author: Leonardo de Moura #include namespace lean { -obj_res set_io_result(obj_arg a); -obj_res set_io_error(obj_arg e); -obj_res set_io_error(char const * msg); -obj_res set_io_error(std::string const & msg); +inline obj_res io_result_mk_ok(obj_arg a) { return lean_io_result_mk_ok(a); } +inline obj_res io_result_mk_error(obj_arg e) { return lean_io_result_mk_error(e); } +obj_res io_result_mk_error(char const * msg); +obj_res io_result_mk_error(std::string const & msg); obj_res decode_io_error(int errnum, b_obj_arg fname); obj_res io_wrap_handle(FILE * hfile); void initialize_io(); diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index c5eaa2cabf..be6f246582 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -1765,13 +1765,14 @@ static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); } void lean_io_result_show_error(b_lean_obj_arg r); void lean_io_mark_end_initialization(); -static inline lean_obj_res lean_mk_io_result(lean_obj_arg a) { +static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) { lean_object * r = lean_alloc_ctor(0, 2, 0); lean_ctor_set(r, 0, a); lean_ctor_set(r, 1, lean_box(0)); return r; } -static inline lean_obj_res lean_mk_io_error(lean_obj_arg e) { +static inline lean_obj_res lean_mk_io_result(lean_obj_arg a) { return lean_io_result_mk_ok(a); } +static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) { lean_object * r = lean_alloc_ctor(1, 2, 0); lean_ctor_set(r, 0, e); lean_ctor_set(r, 1, lean_box(0)); diff --git a/src/library/module.cpp b/src/library/module.cpp index 093c51d07f..a4425f0bd7 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -44,16 +44,16 @@ extern "C" object * lean_save_module_data(object * fname, object * mdata, object exclusive_file_lock output_lock(olean_fn); std::ofstream out(olean_fn, std::ios_base::binary); if (out.fail()) { - return set_io_error((sstream() << "failed to create file '" << olean_fn << "'").str()); + return io_result_mk_error((sstream() << "failed to create file '" << olean_fn << "'").str()); } object_compactor compactor; compactor(mdata_ref.raw()); out.write(g_olean_header, strlen(g_olean_header)); out.write(static_cast(compactor.data()), compactor.size()); out.close(); - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } catch (exception & ex) { - return set_io_error((sstream() << "failed to write '" << olean_fn << "': " << ex.what()).str()); + return io_result_mk_error((sstream() << "failed to write '" << olean_fn << "': " << ex.what()).str()); } } @@ -63,7 +63,7 @@ extern "C" object * lean_read_module_data(object * fname, object *) { shared_file_lock olean_lock(olean_fn); std::ifstream in(olean_fn, std::ios_base::binary); if (in.fail()) { - return set_io_error((sstream() << "failed to open file '" << olean_fn << "'").str()); + return io_result_mk_error((sstream() << "failed to open file '" << olean_fn << "'").str()); } /* Get file size */ in.seekg(0, in.end); @@ -71,19 +71,19 @@ extern "C" object * lean_read_module_data(object * fname, object *) { in.seekg(0); size_t header_size = strlen(g_olean_header); if (size < header_size) { - return set_io_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); + return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); } char * header = new char[header_size]; in.read(header, header_size); if (strncmp(header, g_olean_header, header_size) != 0) { - return set_io_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); + return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); } delete[] header; // use `malloc` here as expected by `compacted_region` char * buffer = static_cast(malloc(size - header_size)); in.read(buffer, size - header_size); if (!in) { - return set_io_error((sstream() << "failed to read file '" << olean_fn << "'").str()); + return io_result_mk_error((sstream() << "failed to read file '" << olean_fn << "'").str()); } in.close(); compacted_region * region = new compacted_region(size - header_size, buffer); @@ -91,9 +91,9 @@ extern "C" object * lean_read_module_data(object * fname, object *) { object * mod_region = alloc_cnstr(0, 2, 0); cnstr_set(mod_region, 0, mod); cnstr_set(mod_region, 1, box_size_t(reinterpret_cast(region))); - return set_io_result(mod_region); + return io_result_mk_ok(mod_region); } catch (exception & ex) { - return set_io_error((sstream() << "failed to read '" << olean_fn << "': " << ex.what()).str()); + return io_result_mk_error((sstream() << "failed to read '" << olean_fn << "': " << ex.what()).str()); } } @@ -153,9 +153,9 @@ extern "C" object * lean_serialize_modifications(object * mod_list, object *) { object * r = alloc_sarray(1, bytes.size(), bytes.size()); memcpy(sarray_cptr(r), bytes.data(), bytes.size()); - return set_io_result(r); + return io_result_mk_ok(r); } catch (exception & ex) { - return set_io_error(ex.what()); + return io_result_mk_error(ex.what()); } } @@ -185,9 +185,9 @@ extern "C" object * lean_perform_serialized_modifications(object * env0, object if (!in.good()) { throw exception(sstream() << "olean file has been corrupted"); } - return set_io_result(env.steal()); + return io_result_mk_ok(env.steal()); } catch (exception & ex) { - return set_io_error(ex.what()); + return io_result_mk_error(ex.what()); } } diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index 4b2f210235..6932c07bb4 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -490,6 +490,6 @@ object * compacted_region::read() { extern "C" obj_res lean_compacted_region_free(usize region, object *) { delete reinterpret_cast(region); - return lean_mk_io_result(lean_box(0)); + return lean_io_result_mk_ok(lean_box(0)); } } diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 94fb128915..d947e8387b 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include #include #include "util/io.h" +#include #include #include #include @@ -75,28 +76,14 @@ extern "C" void lean_io_result_show_error(b_obj_arg r) { dec_ref(str); } -obj_res set_io_result(obj_arg a) { - object * new_r = alloc_cnstr(0, 2, 0); - cnstr_set(new_r, 0, a); - cnstr_set(new_r, 1, box(0)); - return new_r; -} - -obj_res set_io_error(obj_arg e) { - object * new_r = alloc_cnstr(1, 2, 0); - cnstr_set(new_r, 0, e); - cnstr_set(new_r, 1, box(0)); - return new_r; -} - extern "C" object * mk_io_user_error(object * str); -obj_res set_io_error(char const * msg) { - return set_io_error(mk_io_user_error(mk_string(msg))); +obj_res io_result_mk_error(char const * msg) { + return io_result_mk_error(mk_io_user_error(mk_string(msg))); } -obj_res set_io_error(std::string const & msg) { - return set_io_error(mk_io_user_error(mk_string(msg))); +obj_res io_result_mk_error(std::string const & msg) { + return io_result_mk_error(mk_io_user_error(mk_string(msg))); } static bool g_initializing = true; @@ -108,11 +95,11 @@ static obj_res mk_file_not_found_error(b_obj_arg fname) { inc(fname); int errnum = ENOENT; object * details = mk_string(""); - return set_io_error(lean_mk_io_error_no_file_or_directory(fname, errnum, details)); + return io_result_mk_error(lean_mk_io_error_no_file_or_directory(fname, errnum, details)); } extern "C" obj_res lean_io_initializing(obj_arg) { - return set_io_result(box(g_initializing)); + return io_result_mk_ok(box(g_initializing)); } static lean_external_class * g_io_handle_external_class = nullptr; @@ -141,21 +128,21 @@ MK_THREAD_LOCAL_GET(object *, get_stream_current_stderr, g_stream_stderr); extern "C" obj_res lean_get_stdin(obj_arg /* w */) { object * r = get_stream_current_stdin(); inc_ref(r); - return set_io_result(r); + return io_result_mk_ok(r); } /* getStdout : IO FS.Stream */ extern "C" obj_res lean_get_stdout(obj_arg /* w */) { object * r = get_stream_current_stdout(); inc_ref(r); - return set_io_result(r); + return io_result_mk_ok(r); } /* getStderr : IO FS.Stream */ extern "C" obj_res lean_get_stderr(obj_arg /* w */) { object * r = get_stream_current_stderr(); inc_ref(r); - return set_io_result(r); + return io_result_mk_ok(r); } /* setStdin : FS.Stream -> IO FS.Stream */ @@ -163,7 +150,7 @@ extern "C" obj_res lean_get_set_stdin(obj_arg h, obj_arg /* w */) { object * & x = get_stream_current_stdin(); object * r = x; x = h; - return set_io_result(r); + return io_result_mk_ok(r); } /* setStdout : FS.Stream -> IO FS.Stream */ @@ -171,7 +158,7 @@ extern "C" obj_res lean_get_set_stdout(obj_arg h, obj_arg /* w */) { object * & x = get_stream_current_stdout(); object * r = x; x = h; - return set_io_result(r); + return io_result_mk_ok(r); } /* setStderr : FS.Stream -> IO FS.Stream */ @@ -179,7 +166,7 @@ extern "C" obj_res lean_get_set_stderr(obj_arg h, obj_arg /* w */) { object * & x = get_stream_current_stderr(); object * r = x; x = h; - return set_io_result(r); + return io_result_mk_ok(r); } static FILE * io_get_handle(lean_object * hfile) { @@ -281,9 +268,9 @@ obj_res decode_io_error(int errnum, b_obj_arg fname) { /* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Handle */ extern "C" obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) { if (!chmod(lean_string_cstr(filename), mode)) { - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } else { - return set_io_error(decode_io_error(errno, filename)); + return io_result_mk_error(decode_io_error(errno, filename)); } } @@ -291,25 +278,25 @@ extern "C" obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w * extern "C" obj_res lean_io_prim_handle_mk(b_obj_arg filename, b_obj_arg modeStr, obj_arg /* w */) { FILE *fp = fopen(lean_string_cstr(filename), lean_string_cstr(modeStr)); if (!fp) { - return set_io_error(decode_io_error(errno, filename)); + return io_result_mk_error(decode_io_error(errno, filename)); } else { - return set_io_result(io_wrap_handle(fp)); + return io_result_mk_ok(io_wrap_handle(fp)); } } /* Handle.isEof : (@& Handle) → IO Bool */ extern "C" obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) { FILE * fp = io_get_handle(h); - return set_io_result(box(std::feof(fp) != 0)); + return io_result_mk_ok(box(std::feof(fp) != 0)); } /* Handle.flush : (@& Handle) → IO Bool */ extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) { FILE * fp = io_get_handle(h); if (!std::fflush(fp)) { - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } else { - return set_io_error(decode_io_error(errno, nullptr)); + return io_result_mk_error(decode_io_error(errno, nullptr)); } } @@ -319,19 +306,19 @@ static object * g_io_error_eof = nullptr; extern "C" obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) { FILE * fp = io_get_handle(h); if (feof(fp)) { - return set_io_error(g_io_error_eof); + return io_result_mk_error(g_io_error_eof); } obj_res res = lean_alloc_sarray(1, 0, nbytes); usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp); if (n > 0) { lean_sarray_set_size(res, n); - return set_io_result(res); + return io_result_mk_ok(res); } else if (feof(fp)) { dec_ref(res); - return set_io_result(alloc_sarray(1, 0, 0)); + return io_result_mk_ok(alloc_sarray(1, 0, 0)); } else { dec_ref(res); - return set_io_error(decode_io_error(errno, nullptr)); + return io_result_mk_error(decode_io_error(errno, nullptr)); } } @@ -341,9 +328,9 @@ extern "C" obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf, obj_arg usize n = lean_sarray_size(buf); usize m = std::fwrite(lean_sarray_cptr(buf), 1, n, fp); if (m == n) { - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } else { - return set_io_error(decode_io_error(errno, nullptr)); + return io_result_mk_error(decode_io_error(errno, nullptr)); } } @@ -357,7 +344,7 @@ static object * g_io_error_getline = nullptr; extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) { FILE * fp = io_get_handle(h); if (feof(fp)) { - return set_io_result(mk_string("")); + return io_result_mk_ok(mk_string("")); } const int buf_sz = 64; char buf_str[buf_sz]; // NOLINT @@ -368,17 +355,17 @@ extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) { if (out != nullptr) { if (strlen(buf_str) < buf_sz-1 || buf_str[buf_sz-2] == '\n') { if (first) { - return set_io_result(mk_string(out)); + return io_result_mk_ok(mk_string(out)); } else { result.append(out); - return set_io_result(mk_string(result)); + return io_result_mk_ok(mk_string(result)); } } result.append(out); } else if (std::feof(fp)) { - return set_io_result(mk_string(result)); + return io_result_mk_ok(mk_string(result)); } else { - return set_io_error(g_io_error_getline); + return io_result_mk_error(g_io_error_getline); } first = false; } @@ -388,9 +375,9 @@ extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) { extern "C" obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) { FILE * fp = io_get_handle(h); if (std::fputs(lean_string_cstr(s), fp) != EOF) { - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } else { - return set_io_error(decode_io_error(errno, nullptr)); + return io_result_mk_error(decode_io_error(errno, nullptr)); } } @@ -420,21 +407,21 @@ extern "C" obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) { extern "C" obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) { char * val = std::getenv(string_cstr(env_var)); if (val) { - return set_io_result(mk_option_some(mk_string(val))); + return io_result_mk_ok(mk_option_some(mk_string(val))); } else { - return set_io_result(mk_option_none()); + return io_result_mk_ok(mk_option_none()); } } extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) { #if defined(LEAN_EMSCRIPTEN) - return set_io_result(fname); + return io_result_mk_ok(fname); #elif defined(LEAN_WINDOWS) constexpr unsigned BufferSize = 8192; char buffer[BufferSize]; DWORD retval = GetFullPathName(string_cstr(fname), BufferSize, buffer, nullptr); if (retval == 0 || retval > BufferSize) { - return set_io_result(fname); + return io_result_mk_ok(fname); } else { dec_ref(fname); // Hack for making sure disk is lower case @@ -442,7 +429,7 @@ extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) { if (strlen(buffer) >= 2 && buffer[1] == ':') { buffer[0] = tolower(buffer[0]); } - return set_io_result(mk_string(buffer)); + return io_result_mk_ok(mk_string(buffer)); } #else constexpr unsigned BufferSize = 8192; @@ -451,7 +438,7 @@ extern "C" obj_res lean_io_realpath(obj_arg fname, obj_arg) { if (tmp) { obj_res s = mk_string(tmp); dec_ref(fname); - return set_io_result(s); + return io_result_mk_ok(s); } else { obj_res res = mk_file_not_found_error(fname); dec_ref(fname); @@ -464,15 +451,15 @@ extern "C" obj_res lean_io_is_dir(b_obj_arg fname, obj_arg) { struct stat st; if (stat(string_cstr(fname), &st) == 0) { bool b = S_ISDIR(st.st_mode); - return set_io_result(box(b)); + return io_result_mk_ok(box(b)); } else { - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } } extern "C" obj_res lean_io_file_exists(b_obj_arg fname, obj_arg) { bool b = !!std::ifstream(string_cstr(fname)); - return set_io_result(box(b)); + return io_result_mk_ok(box(b)); } extern "C" obj_res lean_io_app_dir(obj_arg) { @@ -487,16 +474,16 @@ extern "C" obj_res lean_io_app_dir(obj_arg) { if (pathstr.size() >= 2 && pathstr[1] == ':') { pathstr[0] = tolower(pathstr[0]); } - return set_io_result(mk_string(pathstr)); + return io_result_mk_ok(mk_string(pathstr)); #elif defined(__APPLE__) char buf1[PATH_MAX]; char buf2[PATH_MAX]; uint32_t bufsize = PATH_MAX; if (_NSGetExecutablePath(buf1, &bufsize) != 0) - return set_io_error("failed to locate application"); + return io_result_mk_error("failed to locate application"); if (!realpath(buf1, buf2)) - return set_io_error("failed to resolve symbolic links when locating application"); - return set_io_result(mk_string(buf2)); + return io_result_mk_error("failed to resolve symbolic links when locating application"); + return io_result_mk_ok(mk_string(buf2)); #else // Linux version char path[PATH_MAX]; @@ -505,9 +492,9 @@ extern "C" obj_res lean_io_app_dir(obj_arg) { pid_t pid = getpid(); snprintf(path, PATH_MAX, "/proc/%d/exe", pid); if (readlink(path, dest, PATH_MAX) == -1) { - return set_io_error("failed to locate application"); + return io_result_mk_error("failed to locate application"); } else { - return set_io_result(mk_string(dest)); + return io_result_mk_ok(mk_string(dest)); } #endif } @@ -516,9 +503,9 @@ extern "C" obj_res lean_io_current_dir(obj_arg) { char buffer[PATH_MAX]; char * cwd = getcwd(buffer, sizeof(buffer)); if (cwd) { - return set_io_result(mk_string(cwd)); + return io_result_mk_ok(mk_string(cwd)); } else { - return set_io_error("failed to retrieve current working directory"); + return io_result_mk_error("failed to retrieve current working directory"); } } @@ -528,7 +515,7 @@ extern "C" obj_res lean_st_mk_ref(obj_arg a, obj_arg) { lean_ref_object * o = (lean_ref_object*)lean_alloc_small_object(sizeof(lean_ref_object)); lean_set_st_header((lean_object*)o, LeanRef, 0); o->m_value = a; - return set_io_result((lean_object*)o); + return io_result_mk_ok((lean_object*)o); } static object * g_io_error_nullptr_read = nullptr; @@ -562,14 +549,14 @@ extern "C" obj_res lean_st_ref_get(b_obj_arg ref, obj_arg) { /* this may happen if another thread wrote `ref` */ dec(tmp); } - return set_io_result(val); + return io_result_mk_ok(val); } } } else { object * val = lean_to_ref(ref)->m_value; lean_assert(val != nullptr); inc(val); - return set_io_result(val); + return io_result_mk_ok(val); } } @@ -579,13 +566,13 @@ extern "C" obj_res lean_st_ref_take(b_obj_arg ref, obj_arg) { while (true) { object * val = val_addr->exchange(nullptr); if (val != nullptr) - return set_io_result(val); + return io_result_mk_ok(val); } } else { object * val = lean_to_ref(ref)->m_value; lean_assert(val != nullptr); lean_to_ref(ref)->m_value = nullptr; - return set_io_result(val); + return io_result_mk_ok(val); } } @@ -601,12 +588,12 @@ extern "C" obj_res lean_st_ref_set(b_obj_arg ref, obj_arg a, obj_arg) { object * old_a = val_addr->exchange(a); if (old_a != nullptr) dec(old_a); - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } else { if (lean_to_ref(ref)->m_value != nullptr) dec(lean_to_ref(ref)->m_value); lean_to_ref(ref)->m_value = a; - return set_io_result(box(0)); + return io_result_mk_ok(box(0)); } } @@ -618,21 +605,21 @@ extern "C" obj_res lean_st_ref_swap(b_obj_arg ref, obj_arg a, obj_arg) { while (true) { object * old_a = val_addr->exchange(a); if (old_a != nullptr) - return set_io_result(old_a); + return io_result_mk_ok(old_a); } } else { object * old_a = lean_to_ref(ref)->m_value; if (old_a == nullptr) - return set_io_error(g_io_error_nullptr_read); + return io_result_mk_error(g_io_error_nullptr_read); lean_to_ref(ref)->m_value = a; - return set_io_result(old_a); + return io_result_mk_ok(old_a); } } extern "C" obj_res lean_st_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) { // TODO(Leo): ref_maybe_mt bool r = lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value; - return set_io_result(box(r)); + return io_result_mk_ok(box(r)); } void initialize_io() { diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index 4c9e90fc7b..6a32054fbe 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -58,7 +58,7 @@ extern "C" obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_ar DWORD exit_code; WaitForSingleObject(h, INFINITE); GetExitCodeProcess(h, &exit_code); - return lean_mk_io_result(box(exit_code)); + return lean_io_result_mk_ok(box(exit_code)); } static FILE * from_win_handle(HANDLE handle, char const * mode) { @@ -183,7 +183,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & if (stderr_mode == stdio::PIPED) CloseHandle(child_stderr); object_ref r = mk_cnstr(0, parent_stdin, parent_stdout, parent_stderr, wrap_win_handle(piProcInfo.hProcess)); - return lean_mk_io_result(r.steal()); + return lean_io_result_mk_ok(r.steal()); } void initialize_process() { @@ -199,11 +199,11 @@ extern "C" obj_res lean_io_process_child_wait(b_obj_arg, obj_arg child, obj_arg) int status; waitpid(pid, &status, 0); if (WIFEXITED(status)) { - return lean_mk_io_result(box(static_cast(WEXITSTATUS(status)))); + return lean_io_result_mk_ok(box(static_cast(WEXITSTATUS(status)))); } else { lean_assert(WIFSIGNALED(status)); // use bash's convention - return lean_mk_io_result(box(128 + static_cast(WTERMSIG(status)))); + return lean_io_result_mk_ok(box(128 + static_cast(WTERMSIG(status)))); } } @@ -304,7 +304,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & object_ref r = mk_cnstr(0, parent_stdin, parent_stdout, parent_stderr, sizeof(pid_t)); static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT cnstr_set_uint32(r.raw(), 3 * sizeof(object *), pid); - return lean_mk_io_result(r.steal()); + return lean_io_result_mk_ok(r.steal()); } void initialize_process() {} @@ -331,7 +331,7 @@ extern "C" obj_res lean_io_process_spawn(obj_arg args_, obj_arg) { cnstr_get_ref_t>(args, 3), cnstr_get_ref_t>>>(args, 4)); } catch (int err) { - return lean_mk_io_error(decode_io_error(err, nullptr)); + return lean_io_result_mk_error(decode_io_error(err, nullptr)); } } diff --git a/tests/compiler/foreign/myfuns.cpp b/tests/compiler/foreign/myfuns.cpp index a3d5cebb78..ee9cff6224 100644 --- a/tests/compiler/foreign/myfuns.cpp +++ b/tests/compiler/foreign/myfuns.cpp @@ -45,16 +45,16 @@ static S g_s(0, 0, ""); extern "C" lean_object * lean_S_global_append(b_lean_obj_arg str, lean_object /* w */) { g_s.m_s += lean_string_cstr(str); - return lean::set_io_result(lean_box(0)); + return lean::io_result_mk_ok(lean_box(0)); } extern "C" lean_object * lean_S_global_string(lean_object /* w */) { - return lean::set_io_result(lean::mk_string(g_s.m_s)); + return lean::io_result_mk_ok(lean::mk_string(g_s.m_s)); } extern "C" lean_object * lean_S_update_global(b_lean_obj_arg s, lean_object /* w */) { g_s.m_x = to_S(s)->m_x; g_s.m_y = to_S(s)->m_y; g_s.m_s = to_S(s)->m_s; - return lean::set_io_result(lean_box(0)); + return lean::io_result_mk_ok(lean_box(0)); }