From 13aec480698df8cf2f9aeef535bb34a165a83acc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Feb 2020 16:02:00 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/System/FilePath.lean | 4 +++ stage0/src/library/compiler/util.cpp | 11 ++++++ stage0/src/runtime/io.cpp | 54 ++++++++++++++++++++++++++++ stage0/src/runtime/lean.h | 7 +++- stage0/stdlib/Init/Lean/Util/Path.c | 17 ++------- stage0/stdlib/Init/System/FilePath.c | 25 +++++++++++++ 6 files changed, 102 insertions(+), 16 deletions(-) diff --git a/stage0/src/Init/System/FilePath.lean b/stage0/src/Init/System/FilePath.lean index fab5c64d5c..3e8fba0ed9 100644 --- a/stage0/src/Init/System/FilePath.lean +++ b/stage0/src/Init/System/FilePath.lean @@ -52,4 +52,8 @@ match fname.revPosOf pathSeparator with | some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString end FilePath + +def mkFilePath (parts : List String) : String := +String.intercalate FilePath.pathSeparator.toString parts + end System diff --git a/stage0/src/library/compiler/util.cpp b/stage0/src/library/compiler/util.cpp index 76fdbfe51e..02d8fd2e2b 100644 --- a/stage0/src/library/compiler/util.cpp +++ b/stage0/src/library/compiler/util.cpp @@ -486,6 +486,17 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) { return mk_enf_neutral_type(); } + if (is_pi(e)) { + expr it = e; + while (is_pi(it)) + it = binding_body(it); + if (is_sort(it)) { + // functions that produce types are irrelevant + return mk_enf_neutral_type(); + } + } + + /* If `e` is a trivial structure such as `Subtype`, then convert the only relevant field to a runtime type. */ if (is_app(e)) { diff --git a/stage0/src/runtime/io.cpp b/stage0/src/runtime/io.cpp index d75c4dd061..54dd46a1ba 100644 --- a/stage0/src/runtime/io.cpp +++ b/stage0/src/runtime/io.cpp @@ -612,6 +612,60 @@ extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) { return set_io_result(box(r)); } +/* Mutable quotients are simpler version of IO.Ref */ + +extern "C" obj_res lean_mutquot_mk(obj_arg a) { + 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 (lean_object*)(o); +} + +extern "C" obj_res lean_mutquot_get(obj_arg q) { + if (ref_maybe_mt(q)) { + atomic * val_addr = mt_ref_val_addr(q); + object * val; + while (true) { + val = val_addr->exchange(nullptr); + if (val != nullptr) + break; + } + inc(val); + object * tmp = val_addr->exchange(val); + if (tmp != nullptr) { + /* this may happen if another thread wrote `ref` */ + dec(tmp); + } + dec(q); + return val; + } else { + object * val = lean_to_ref(q)->m_value; + lean_assert(val != nullptr); + inc(val); + dec(q); + return val; + } +} + +extern "C" uint8_t lean_mutquot_set(b_obj_arg q, obj_arg a) { + if (ref_maybe_mt(q)) { + /* We must mark `a` as multi-threaded if `ref` is marked as multi-threaded. + Reason: our runtime relies on the fact that a single-threaded object + cannot be reached from a multi-thread object. */ + mark_mt(a); + atomic * val_addr = mt_ref_val_addr(q); + object * old_a = val_addr->exchange(a); + if (old_a != nullptr) + dec(old_a); + return 0; + } else { + lean_assert(lean_to_ref(q)->m_value); + dec(lean_to_ref(q)->m_value); + lean_to_ref(q)->m_value = a; + return 0; + } +} + void initialize_io() { g_io_error_nullptr_read = mk_string("null reference read"); mark_persistent(g_io_error_nullptr_read); diff --git a/stage0/src/runtime/lean.h b/stage0/src/runtime/lean.h index 67c43efa0d..d4196be469 100644 --- a/stage0/src/runtime/lean.h +++ b/stage0/src/runtime/lean.h @@ -1658,14 +1658,19 @@ static inline lean_obj_res lean_mk_io_error(lean_obj_arg e) { lean_ctor_set(r, 1, lean_box(0)); return r; } -/* IO Ref primitives */ +/* IO Ref primitives */ lean_obj_res lean_io_mk_ref(lean_obj_arg, lean_obj_arg); lean_obj_res lean_io_ref_get(b_lean_obj_arg, lean_obj_arg); lean_obj_res lean_io_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg); lean_obj_res lean_io_ref_reset(b_lean_obj_arg, lean_obj_arg); lean_obj_res lean_io_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg); +/* MutQuot Ref primitives */ +lean_obj_res lean_mutquot_mk(lean_obj_arg); +lean_obj_res lean_mutquot_get(lean_obj_arg); +uint8_t lean_mutquot_set(b_lean_obj_arg, lean_obj_arg); + #ifdef __cplusplus } #endif diff --git a/stage0/stdlib/Init/Lean/Util/Path.c b/stage0/stdlib/Init/Lean/Util/Path.c index efb627b99e..cfbba428bc 100644 --- a/stage0/stdlib/Init/Lean/Util/Path.c +++ b/stage0/stdlib/Init/Lean/Util/Path.c @@ -13,7 +13,6 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* lean_string_push(lean_object*, uint32_t); lean_object* lean_array_uget(lean_object*, size_t); lean_object* l_HashMapImp_moveEntries___main___at_Lean_parseSearchPath___spec__4(lean_object*, lean_object*, lean_object*); lean_object* lean_io_is_dir(lean_object*, lean_object*); @@ -33,7 +32,6 @@ lean_object* lean_array_get_size(lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Name_inhabited; -lean_object* l___private_Init_Lean_Util_Path_1__pathSep___closed__1; extern lean_object* l_String_splitAux___main___closed__1; lean_object* l_IO_getEnv___at_Lean_addSearchPathFromEnv___spec__1___boxed(lean_object*, lean_object*); lean_object* l_String_splitOn(lean_object*, lean_object*); @@ -99,6 +97,7 @@ lean_object* l_Lean_addSearchPathFromEnv(lean_object*, lean_object*); lean_object* l_HashMapImp_find_x3f___at_Lean_findOLean___spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_getBuiltinSearchPath___closed__2; lean_object* l_Lean_getBuiltinSearchPath___closed__4; +extern lean_object* l_System_mkFilePath___closed__1; lean_object* lean_nat_mul(lean_object*, lean_object*); lean_object* l_Lean_mkSearchPathRef___closed__1; lean_object* l_mkHashMap___at_Lean_mkSearchPathRef___spec__1(lean_object*); @@ -128,21 +127,11 @@ lean_object* l_Array_iterateMAux___main___at_Lean_findAtSearchPath___spec__2___b uint8_t lean_string_dec_eq(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); uint8_t l_AssocList_contains___main___at_Lean_parseSearchPath___spec__2(lean_object*, lean_object*); -lean_object* _init_l___private_Init_Lean_Util_Path_1__pathSep___closed__1() { -_start: -{ -lean_object* x_1; uint32_t x_2; lean_object* x_3; -x_1 = l_String_splitAux___main___closed__1; -x_2 = l_System_FilePath_pathSeparator; -x_3 = lean_string_push(x_1, x_2); -return x_3; -} -} lean_object* _init_l___private_Init_Lean_Util_Path_1__pathSep() { _start: { lean_object* x_1; -x_1 = l___private_Init_Lean_Util_Path_1__pathSep___closed__1; +x_1 = l_System_mkFilePath___closed__1; return x_1; } } @@ -2645,8 +2634,6 @@ lean_dec_ref(res); res = initialize_Init_Lean_Data_Name(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l___private_Init_Lean_Util_Path_1__pathSep___closed__1 = _init_l___private_Init_Lean_Util_Path_1__pathSep___closed__1(); -lean_mark_persistent(l___private_Init_Lean_Util_Path_1__pathSep___closed__1); l___private_Init_Lean_Util_Path_1__pathSep = _init_l___private_Init_Lean_Util_Path_1__pathSep(); lean_mark_persistent(l___private_Init_Lean_Util_Path_1__pathSep); l_Lean_mkSearchPathRef___closed__1 = _init_l_Lean_mkSearchPathRef___closed__1(); diff --git a/stage0/stdlib/Init/System/FilePath.c b/stage0/stdlib/Init/System/FilePath.c index a9dec2080b..83228ba9dc 100644 --- a/stage0/stdlib/Init/System/FilePath.c +++ b/stage0/stdlib/Init/System/FilePath.c @@ -14,11 +14,13 @@ extern "C" { #endif lean_object* l_List_reverse___rarg(lean_object*); +lean_object* lean_string_push(lean_object*, uint32_t); extern uint8_t l_System_Platform_isWindows; extern uint8_t l_System_Platform_isOSX; lean_object* l_System_FilePath_searchPathSeparators___closed__1___boxed__const__1; lean_object* l_String_revPosOf(lean_object*, uint32_t); uint8_t l_System_FilePath_isCaseInsensitive; +lean_object* l_System_mkFilePath(lean_object*); lean_object* l_System_FilePath_pathSeparators___closed__2___boxed__const__1; lean_object* lean_string_utf8_set(lean_object*, lean_object*, uint32_t); lean_object* l_System_FilePath_splitSearchPath(lean_object*); @@ -51,8 +53,10 @@ lean_object* l_String_split___at_System_FilePath_splitSearchPath___spec__2___box uint32_t l_System_FilePath_extSeparator; lean_object* l_String_splitAux___main___at_System_FilePath_splitSearchPath___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_UInt32_decEq(uint32_t, uint32_t); +lean_object* l_String_intercalate(lean_object*, lean_object*); uint32_t l_System_FilePath_searchPathSeparator; lean_object* l_System_FilePath_pathSeparators___closed__3; +lean_object* l_System_mkFilePath___closed__1; lean_object* l_System_FilePath_searchPathSeparators___closed__3; lean_object* l_System_FilePath_pathSeparators___closed__2; uint8_t l_List_elem___main___at_System_FilePath_splitSearchPath___spec__1(uint32_t, lean_object*); @@ -631,6 +635,25 @@ return x_8; } } } +lean_object* _init_l_System_mkFilePath___closed__1() { +_start: +{ +lean_object* x_1; uint32_t x_2; lean_object* x_3; +x_1 = l_String_splitAux___main___closed__1; +x_2 = l_System_FilePath_pathSeparator; +x_3 = lean_string_push(x_1, x_2); +return x_3; +} +} +lean_object* l_System_mkFilePath(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = l_System_mkFilePath___closed__1; +x_3 = l_String_intercalate(x_2, x_1); +return x_3; +} +} lean_object* initialize_Init_System_Platform(lean_object*); lean_object* initialize_Init_Data_String_Basic(lean_object*); static bool _G_initialized = false; @@ -680,6 +703,8 @@ lean_mark_persistent(l_System_FilePath_normalizePath___closed__1); l_System_FilePath_normalizePath___closed__2 = _init_l_System_FilePath_normalizePath___closed__2(); l_System_FilePath_dirName___closed__1 = _init_l_System_FilePath_dirName___closed__1(); lean_mark_persistent(l_System_FilePath_dirName___closed__1); +l_System_mkFilePath___closed__1 = _init_l_System_mkFilePath___closed__1(); +lean_mark_persistent(l_System_mkFilePath___closed__1); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus