diff --git a/stage0/src/Lean/Elab/Frontend.lean b/stage0/src/Lean/Elab/Frontend.lean index 2c5edcb5ae..0b9f3f42b9 100644 --- a/stage0/src/Lean/Elab/Frontend.lean +++ b/stage0/src/Lean/Elab/Frontend.lean @@ -52,7 +52,7 @@ def processCommand : FrontendM Bool := do let scope := cmdState.scopes.head! let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } let pos := ictx.fileMap.toPosition pstate.pos - match profileit "parsing" scope.opts pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with + match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with | (cmd, ps, messages) => modify fun s => { s with commands := s.commands.push cmd } setParserState ps @@ -60,7 +60,7 @@ def processCommand : FrontendM Bool := do if Parser.isEOI cmd || Parser.isExitCommand cmd then pure true -- Done else - profileitM IO.Error "elaboration" scope.opts pos $ elabCommandAtFrontend cmd + profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd pure false partial def processCommands : FrontendM Unit := do diff --git a/stage0/src/Lean/Environment.lean b/stage0/src/Lean/Environment.lean index 9fa22fc296..88ecd08063 100644 --- a/stage0/src/Lean/Environment.lean +++ b/stage0/src/Lean/Environment.lean @@ -543,7 +543,7 @@ structure ImportState where regions : Array CompactedRegion := #[] @[export lean_import_modules] -partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts ⟨0, 0⟩ do +partial def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" opts do let (_, s) ← importMods imports |>.run {} -- (moduleNames, mods, regions) let mut modIdx : Nat := 0 diff --git a/stage0/src/Lean/Meta/SynthInstance.lean b/stage0/src/Lean/Meta/SynthInstance.lean index 5aeb58f020..68916e411a 100644 --- a/stage0/src/Lean/Meta/SynthInstance.lean +++ b/stage0/src/Lean/Meta/SynthInstance.lean @@ -555,7 +555,7 @@ private def preprocessOutParam (type : Expr) : MetaM Expr := Remark: we use a different option for controlling the maximum result size for coercions. -/ -def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) ⟨0, 0⟩ do +def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do let opts ← getOptions let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts) let inputConfig ← getConfig diff --git a/stage0/src/Lean/Meta/Tactic/Injection.lean b/stage0/src/Lean/Meta/Tactic/Injection.lean index 32ae02f435..89f4fbdcb5 100644 --- a/stage0/src/Lean/Meta/Tactic/Injection.lean +++ b/stage0/src/Lean/Meta/Tactic/Injection.lean @@ -10,6 +10,14 @@ import Lean.Meta.Tactic.Intro namespace Lean.Meta +def getCtorNumPropFields (ctorInfo : ConstructorVal) : MetaM Nat := do + forallTelescopeReducing ctorInfo.type fun xs _ => do + let mut numProps := 0 + for i in [:ctorInfo.numFields] do + if (← isProp (← inferType xs[ctorInfo.numParams + i])) then + numProps := numProps + 1 + return numProps + inductive InjectionResultCore where | solved | subgoal (mvarId : MVarId) (numNewEqs : Nat) @@ -42,7 +50,9 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag assignExprMVar mvarId (mkApp val newMVar) let mvarId ← tryClear newMVar.mvarId! fvarId - pure $ InjectionResultCore.subgoal mvarId aCtor.numFields + /- Recall that `noConfusion` does not include equalities for propositions since they are trivial due to proof irrelevance. -/ + let numPropFields ← getCtorNumPropFields aCtor + return InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields) | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction" | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected" diff --git a/stage0/src/Lean/Util/Profile.lean b/stage0/src/Lean/Util/Profile.lean index a0cd020ff1..52640e45e5 100644 --- a/stage0/src/Lean/Util/Profile.lean +++ b/stage0/src/Lean/Util/Profile.lean @@ -9,18 +9,18 @@ namespace Lean /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/ @[extern "lean_profileit"] -def profileit {α : Type} (category : @& String) (opts : @& Options) (pos : @& Position) (fn : Unit → α) : α := fn () +def profileit {α : Type} (category : @& String) (opts : @& Options) (fn : Unit → α) : α := fn () -unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α := - match profileit category opts pos fun _ => unsafeEIO act with +unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α := + match profileit category opts fun _ => unsafeEIO act with | Except.ok a => pure a | Except.error e => throw e @[implementedBy profileitIOUnsafe] -def profileitIO {ε α : Type} (category : String) (opts : Options) (pos : Position) (act : EIO ε α) : EIO ε α := act +def profileitIO {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α := act -- impossible to infer `ε` -def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (pos : Position) (act : m α) : m α := - monadMap (fun {β} => @profileitIO ε β category opts pos) act +def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (act : m α) : m α := + monadMap (fun {β} => profileitIO (ε := ε) (α := β) category opts) act end Lean diff --git a/stage0/src/bin/leanc.in b/stage0/src/bin/leanc.in index 3b238a7a1f..5272bc28fc 100755 --- a/stage0/src/bin/leanc.in +++ b/stage0/src/bin/leanc.in @@ -22,6 +22,7 @@ ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@) for arg in "$@"; do # passed -shared ~> switch to shared linker flags [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) + [[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() [[ $arg == "-print-cflags" ]] && echo "${cflags[@]} ${cflags_ext[@]}" && exit [[ $arg == "-print-ldflags" ]] && echo "${ldflags_ext[@]} ${ldflags[@]}" && exit done diff --git a/stage0/src/include/lean/lean.h b/stage0/src/include/lean/lean.h index 1bbbe7b774..9c61f1df9f 100644 --- a/stage0/src/include/lean/lean.h +++ b/stage0/src/include/lean/lean.h @@ -1358,7 +1358,7 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) { size_t n1 = lean_unbox(a1); size_t n2 = lean_unbox(a2); if (n2 == 0) - return lean_box(0); + return lean_box(n1); else return lean_box(n1 % n2); } else { diff --git a/stage0/src/library/time_task.cpp b/stage0/src/library/time_task.cpp index a7662be471..5e3d7ab8f5 100644 --- a/stage0/src/library/time_task.cpp +++ b/stage0/src/library/time_task.cpp @@ -38,7 +38,7 @@ void finalize_time_task() { delete g_cum_times_mutex; } -time_task::time_task(std::string const & category, options const & opts, pos_info pos, name decl) : +time_task::time_task(std::string const & category, options const & opts, name decl) : m_category(category) { if (get_profiler(opts)) { m_timeit = optional(get_profiling_threshold(opts), [=](second_duration duration) mutable { @@ -63,12 +63,10 @@ time_task::~time_task() { } } -/* profileit {α : Type} (category : String) (opts : Options) (pos : Position) (fn : Unit → α) : α */ -extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, b_obj_arg pos, obj_arg fn) { +/* profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) : α */ +extern "C" obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, obj_arg fn) { time_task t(string_to_std(category), - TO_REF(options, opts), - pos_info(nat(cnstr_get(pos, 0), true).get_small_value(), - nat(cnstr_get(pos, 1), true).get_small_value())); + TO_REF(options, opts)); return apply_1(fn, box(0)); } } diff --git a/stage0/src/library/time_task.h b/stage0/src/library/time_task.h index 78fb3658db..3c2ffb55b1 100644 --- a/stage0/src/library/time_task.h +++ b/stage0/src/library/time_task.h @@ -20,7 +20,7 @@ class time_task { optional m_timeit; time_task * m_parent_task; public: - time_task(std::string const & category, options const & opts, pos_info pos = pos_info(), name decl = name()); + time_task(std::string const & category, options const & opts, name decl = name()); ~time_task(); }; diff --git a/stage0/src/runtime/alloc.cpp b/stage0/src/runtime/alloc.cpp index b53cc94f93..8431068c3d 100644 --- a/stage0/src/runtime/alloc.cpp +++ b/stage0/src/runtime/alloc.cpp @@ -15,6 +15,9 @@ Author: Leonardo de Moura #define LEAN_NUM_SLOTS (LEAN_MAX_SMALL_OBJECT_SIZE / LEAN_OBJECT_SIZE_DELTA) #define LEAN_MAX_TO_EXPORT_OBJS 1024 +LEAN_CASSERT(LEAN_PAGE_SIZE > LEAN_MAX_SMALL_OBJECT_SIZE); +LEAN_CASSERT(LEAN_SEGMENT_SIZE > LEAN_PAGE_SIZE); + namespace lean { namespace allocator { #ifdef LEAN_RUNTIME_STATS @@ -89,6 +92,10 @@ struct segment { m_next_page_mem = get_first_page_mem(); } + bool is_full() const { + return m_next_page_mem + LEAN_PAGE_SIZE > m_data + LEAN_SEGMENT_SIZE; + } + void move_to_heap(heap *); }; @@ -182,6 +189,7 @@ static inline page * page_list_pop(page * & head) { } void page::push_free_obj(void * o) { + lean_assert(get_page_of(o) == this); set_next_obj(o, m_header.m_free_list); m_header.m_free_list = o; m_header.m_num_free++; @@ -240,19 +248,32 @@ void heap::export_objs() { while (o != nullptr) { void * n = get_next_obj(o); heap * h = get_page_of(o)->get_heap(); - lean_assert(h != this); - bool found = false; - for (export_entry & e : to_export) { - if (e.m_heap == h) { - set_next_obj(o, e.m_head); - e.m_head = o; - found = true; - break; + /* + We may have `h == this`. + + Recall that each heap `h` has a list of dead objects `m_to_export_list` from other heaps. + It contains objects deleted by the thread that "owns" `h`. + Now, suppose we have two heaps `h1` and `h2`, and thread `t1` that owns `h1` deletes an object `o` from `h2`. + The object `o` is now in the list `h1.m_to_export_list`. + Then, thread `t2` that owns h2 finishes, and `h2` goes to the orphan list. + Then, `h1` allocates a new segment, and a segment from `h2` containing `o` is reused. + Then, `h1` tries to export dead objects to other threads using this function and finds `o` s.t. which is now + `get_page_of(o)->get_heap() == h1`. + */ + if (h != this) { + bool found = false; + for (export_entry & e : to_export) { + if (e.m_heap == h) { + set_next_obj(o, e.m_head); + e.m_head = o; + found = true; + break; + } + } + if (!found) { + set_next_obj(o, nullptr); + to_export.push_back(export_entry{h, o, o}); } - } - if (!found) { - set_next_obj(o, nullptr); - to_export.push_back(export_entry{h, o, o}); } o = n; } @@ -266,25 +287,34 @@ void heap::export_objs() { } void heap::alloc_segment() { - if (heap * h = g_heap_manager->pop_orphan()) { - lean_assert(h->m_curr_segment); - /* import pending objects, before moving `h`'s segment to *this* heap. */ - h->import_objs(); - segment * s = h->m_curr_segment; - h->m_curr_segment = s->m_next; - s->move_to_heap(this); - if (h->m_curr_segment != nullptr) { - g_heap_manager->push_orphan(h); + while (true) { + if (heap * h = g_heap_manager->pop_orphan()) { + lean_assert(h->m_curr_segment); + /* import pending objects, before moving `h`'s segment to *this* heap. */ + h->import_objs(); + segment * s = h->m_curr_segment; + h->m_curr_segment = s->m_next; + s->move_to_heap(this); + if (h->m_curr_segment != nullptr) { + g_heap_manager->push_orphan(h); + } else { + delete h; + } + s->m_next = m_curr_segment; + m_curr_segment = s; + if (!s->is_full()) { + /* Found segment that is not full */ + break; + } + /* If `s` is full, we must "keep looking" because `alloc_page` assumes that `m_curr_segment` + contains at least one free page. */ } else { - delete h; + LEAN_RUNTIME_STAT_CODE(g_num_segments++); + segment * s = new segment(); + s->m_next = m_curr_segment; + m_curr_segment = s; + break; } - s->m_next = m_curr_segment; - m_curr_segment = s; - } else { - LEAN_RUNTIME_STAT_CODE(g_num_segments++); - segment * s = new segment(); - s->m_next = m_curr_segment; - m_curr_segment = s; } } @@ -294,7 +324,7 @@ static page * alloc_page(heap * h, unsigned obj_size) { LEAN_RUNTIME_STAT_CODE(g_num_pages++); page * p = new (s->m_next_page_mem) page(); s->m_next_page_mem += LEAN_PAGE_SIZE; - if (s->m_next_page_mem + LEAN_PAGE_SIZE > s->m_data + LEAN_SEGMENT_SIZE) { + if (s->is_full()) { /* s is full, we need to allocate a new one. */ h->alloc_segment(); } @@ -311,6 +341,7 @@ static page * alloc_page(heap * h, unsigned obj_size) { while (true) { if (next_free + obj_size > end) break; /* next object doesn't fit */ + lean_assert(get_page_of(curr_free) == p); set_next_obj(next_free, curr_free); curr_free = next_free; next_free = next_free + obj_size; @@ -386,6 +417,7 @@ extern "C" void * lean_alloc_small(unsigned sz, unsigned slot_idx) { } p->m_header.m_free_list = get_next_obj(r); p->m_header.m_num_free--; + lean_assert(get_page_of(r) == p); return r; } diff --git a/stage0/src/runtime/object.cpp b/stage0/src/runtime/object.cpp index b36e3b0660..8226c1823b 100644 --- a/stage0/src/runtime/object.cpp +++ b/stage0/src/runtime/object.cpp @@ -1174,7 +1174,7 @@ extern "C" object * lean_nat_big_mod(object * a1, object * a2) { return a1; } else if (lean_is_scalar(a2)) { usize n2 = lean_unbox(a2); - return n2 == 0 ? a2 : lean_box((mpz_value(a1) % mpz::of_size_t(n2)).get_unsigned_int()); + return n2 == 0 ? a1 : lean_box((mpz_value(a1) % mpz::of_size_t(n2)).get_unsigned_int()); } else { lean_assert(mpz_value(a2) != 0); return mpz_to_nat(mpz_value(a1) % mpz_value(a2)); diff --git a/stage0/stdlib/Lean/Class.c b/stage0/stdlib/Lean/Class.c index 6e5023c04e..da542d97e7 100644 --- a/stage0/stdlib/Lean/Class.c +++ b/stage0/stdlib/Lean/Class.c @@ -143,9 +143,9 @@ size_t l_USize_mul(size_t, size_t); lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_initFn____x40_Lean_Class___hyg_47____spec__4(lean_object*, lean_object*); lean_object* l___private_Lean_Class_0__Lean_checkOutParam_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkFVar(lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; size_t lean_usize_of_nat(lean_object*); lean_object* l_Lean_Expr_hasAnyFVar_visit___at___private_Lean_Class_0__Lean_checkOutParam___spec__3___boxed(lean_object*, lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Lean_ConstantInfo_type(lean_object*); lean_object* l_Lean_getClassName(lean_object*, lean_object*); lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*); @@ -1761,7 +1761,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_initFn____x40_Lean_Class___hyg_47____closed__2; x_2 = l_Lean_initFn____x40_Lean_Class___hyg_47____closed__3; x_3 = l_Lean_initFn____x40_Lean_Class___hyg_47____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Compiler/ClosedTermCache.c b/stage0/stdlib/Lean/Compiler/ClosedTermCache.c index d89539c336..ab24be68bb 100644 --- a/stage0/stdlib/Lean/Compiler/ClosedTermCache.c +++ b/stage0/stdlib/Lean/Compiler/ClosedTermCache.c @@ -85,8 +85,8 @@ size_t lean_usize_modn(size_t, lean_object*); lean_object* l_Lean_closedTermCacheExt; size_t l_USize_mul(size_t, size_t); lean_object* l_Lean_initFn____x40_Lean_Compiler_ClosedTermCache___hyg_8____lambda__2(lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); size_t l_USize_land(size_t, size_t); lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*); @@ -1548,7 +1548,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_initFn____x40_Lean_Compiler_ClosedTermCache___hyg_8____closed__2; x_2 = l_Lean_initFn____x40_Lean_Compiler_ClosedTermCache___hyg_8____closed__3; x_3 = l_Lean_initFn____x40_Lean_Compiler_ClosedTermCache___hyg_8____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c b/stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c index eaab33db41..060324d47a 100644 --- a/stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c +++ b/stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c @@ -216,11 +216,11 @@ lean_object* l_List_format___at_Lean_IR_UnreachableBranches_Value_format___spec_ lean_object* l_Std_AssocList_contains___at_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_540____spec__7___boxed(lean_object*, lean_object*); extern lean_object* l_instReprList___rarg___closed__2; lean_object* l_Lean_IR_UnreachableBranches_projValue___boxed(lean_object*, lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; size_t lean_usize_of_nat(lean_object*); uint8_t l_Lean_IR_UnreachableBranches_containsCtor(lean_object*, lean_object*); lean_object* l_Lean_IR_UnreachableBranches_Value_addChoice(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Compiler_IR_ElimDeadBranches_0__Lean_IR_UnreachableBranches_resetNestedJPParams_match__2(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; extern lean_object* l_Lean_NameSet_empty; extern lean_object* l_Std_Format_sbracket___closed__3; lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___boxed(lean_object*, lean_object*); @@ -4433,7 +4433,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_540____closed__2; x_2 = l_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_540____closed__3; x_3 = l_Lean_IR_UnreachableBranches_initFn____x40_Lean_Compiler_IR_ElimDeadBranches___hyg_540____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Compiler/Specialize.c b/stage0/stdlib/Lean/Compiler/Specialize.c index 2b7e381412..ea50f19bd8 100644 --- a/stage0/stdlib/Lean/Compiler/Specialize.c +++ b/stage0/stdlib/Lean/Compiler/Specialize.c @@ -154,9 +154,9 @@ lean_object* l_Std_PersistentHashMap_insert___at_Lean_Compiler_SpecState_addEntr lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_246____spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_Compiler_SpecState_cache___default___closed__2; lean_object* l_Lean_Compiler_instInhabitedSpecEntry___closed__1; +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; lean_object* l_Lean_Compiler_instInhabitedSpecState___closed__1; size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; extern lean_object* l_Lean_registerTagAttribute___lambda__6___closed__2; lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Compiler_SpecState_addEntry___spec__5(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Compiler_getCachedSpecialization___spec__2___boxed(lean_object*, lean_object*); @@ -4634,7 +4634,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_47____closed__4; x_2 = l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_246____closed__1; x_3 = l_Lean_Compiler_initFn____x40_Lean_Compiler_Specialize___hyg_246____closed__2; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index 015fab54c6..70ed125ba8 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -660,7 +660,6 @@ uint8_t l___private_Lean_Elab_Do_0__Lean_Elab_Term_hasLiftMethod(lean_object*); lean_object* l_Lean_Syntax_mkStrLit(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_hasExitPointPred_loop(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_getDoReassignVars___closed__3; -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(lean_object*, size_t, size_t, lean_object*); extern lean_object* l_instMonadEST___closed__1; lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f_match__3___rarg(lean_object*, lean_object*); lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___spec__1___closed__2; @@ -732,6 +731,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandTermUnless(lean_object*); lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_instInhabitedAlt(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Do_ToCodeBlock_getTryCatchUpdatedVars___spec__1(lean_object*, size_t, size_t, lean_object*); +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTerm___closed__15; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__6___rarg(lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___closed__41; @@ -7473,7 +7473,7 @@ size_t x_7; size_t x_8; lean_object* x_9; x_7 = 0; x_8 = lean_usize_of_nat(x_3); lean_dec(x_3); -x_9 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(x_2, x_7, x_8, x_1); +x_9 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(x_2, x_7, x_8, x_1); return x_9; } } diff --git a/stage0/stdlib/Lean/Elab/Frontend.c b/stage0/stdlib/Lean/Elab/Frontend.c index 7a1d57f465..a27bcc9e8d 100644 --- a/stage0/stdlib/Lean/Elab/Frontend.c +++ b/stage0/stdlib/Lean/Elab/Frontend.c @@ -35,13 +35,14 @@ lean_object* l_Lean_Elab_Frontend_getCommandState___rarg___boxed(lean_object*, l lean_object* lean_st_ref_get(lean_object*, lean_object*); extern lean_object* l_Lean_instInhabitedParserDescr___closed__1; lean_object* l_Lean_Elab_Frontend_runCommandElabM___closed__2; +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3; extern lean_object* l_Std_PersistentArray_empty___closed__1; lean_object* l_Lean_Elab_Frontend_runCommandElabM___closed__1; lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*); lean_object* lean_array_push(lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_runCommandElabM(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_processCommand_match__1(lean_object*); -lean_object* lean_profileit(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_profileit(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint32_t, lean_object*); extern lean_object* l_Lean_Elab_parseImports___closed__1; lean_object* l_Lean_Elab_runFrontend_match__1___rarg(lean_object*); @@ -50,22 +51,23 @@ lean_object* l_List_forIn_loop___at_Lean_Elab_runFrontend___spec__1(lean_object* lean_object* l_Lean_MessageLog_toList(lean_object*); lean_object* l_Lean_Elab_runFrontend_match__1(lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_processCommand___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2; lean_object* lean_st_ref_take(lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_getInputContext___boxed(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_Elab_Frontend_setParserState___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4; lean_object* l_IO_print___at_IO_println___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_mkState(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_runFrontend_match__2(lean_object*, lean_object*); lean_object* l_List_forIn_loop___at_Lean_Elab_runFrontend___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1; lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_getPrintMessageEndPos___boxed(lean_object*); lean_object* l_Lean_Elab_Frontend_processCommand___closed__1; extern lean_object* l_Lean_Parser_instInhabitedModuleParserState___closed__1; -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584_(lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4; -lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582_(lean_object*); lean_object* l_Lean_Elab_Frontend_updateCmdPos(lean_object*); extern lean_object* l_Lean_firstFrontendMacroScope; lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*, lean_object*); @@ -75,24 +77,21 @@ lean_object* l_Lean_Elab_Frontend_processCommand(lean_object*, lean_object*, lea lean_object* l_Lean_Elab_runFrontend_match__2___boxed(lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_updateCmdPos___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1(lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1; lean_object* l_Lean_Parser_parseCommand_parse(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Parser_isExitCommand(lean_object*); lean_object* l_Lean_Elab_Frontend_getInputContext(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_getCommandState(lean_object*); lean_object* l_Lean_Elab_Frontend_getParserState(lean_object*); lean_object* l_Lean_Elab_Frontend_getParserState___rarg(lean_object*, lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2; lean_object* l_Lean_Elab_Frontend_processCommand___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_register_option(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_runCommandElabM_match__2(lean_object*); lean_object* l_Lean_Elab_IO_processCommands_match__1(lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_setParserState(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3; -lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_updateCmdPos___boxed(lean_object*); lean_object* l_Lean_Elab_Frontend_getCommandState___rarg(lean_object*, lean_object*); uint8_t l_Lean_Parser_isEOI(lean_object*); @@ -101,7 +100,7 @@ lean_object* l_Lean_Elab_Frontend_setMessages___boxed(lean_object*, lean_object* lean_object* l_Lean_Elab_Frontend_runCommandElabM_match__1(lean_object*); uint8_t l_Std_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*); uint8_t l_Lean_Elab_getPrintMessageEndPos(lean_object*); -lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Frontend_getParserState___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_Message_toString(lean_object*, uint8_t, lean_object*); lean_object* l_Lean_Elab_Frontend_getParserState___boxed(lean_object*); @@ -1019,20 +1018,20 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_processCommand_match__1___ return x_2; } } -lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { -lean_object* x_8; lean_object* x_9; -x_8 = lean_apply_2(x_4, x_5, x_6); -x_9 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_3, x_8, x_7); -return x_9; +lean_object* x_7; lean_object* x_8; +x_7 = lean_apply_2(x_3, x_4, x_5); +x_8 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_7, x_6); +return x_8; } } lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed), 7, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed), 6, 0); return x_2; } } @@ -1063,7 +1062,7 @@ return x_1; lean_object* l_Lean_Elab_Frontend_processCommand(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; x_4 = l_Lean_Elab_Frontend_updateCmdPos___rarg(x_2, x_3); x_5 = lean_ctor_get(x_4, 1); lean_inc(x_5); @@ -1102,232 +1101,236 @@ lean_ctor_set(x_19, 0, x_12); lean_ctor_set(x_19, 1, x_16); lean_ctor_set(x_19, 2, x_17); lean_ctor_set(x_19, 3, x_18); -x_20 = lean_ctor_get(x_1, 2); -lean_inc(x_20); -x_21 = lean_ctor_get(x_10, 0); -lean_inc(x_21); -x_22 = l_Lean_FileMap_toPosition(x_20, x_21); -lean_dec(x_20); lean_inc(x_1); -x_23 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_processCommand___lambda__1___boxed), 5, 4); -lean_closure_set(x_23, 0, x_1); -lean_closure_set(x_23, 1, x_19); -lean_closure_set(x_23, 2, x_10); -lean_closure_set(x_23, 3, x_13); -x_24 = l_Lean_Elab_Frontend_processCommand___closed__1; -x_25 = lean_profileit(x_24, x_16, x_22, x_23); -x_26 = lean_ctor_get(x_25, 1); +x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_processCommand___lambda__1___boxed), 5, 4); +lean_closure_set(x_20, 0, x_1); +lean_closure_set(x_20, 1, x_19); +lean_closure_set(x_20, 2, x_10); +lean_closure_set(x_20, 3, x_13); +x_21 = l_Lean_Elab_Frontend_processCommand___closed__1; +x_22 = lean_profileit(x_21, x_16, x_20); +x_23 = lean_ctor_get(x_22, 1); +lean_inc(x_23); +x_24 = lean_ctor_get(x_22, 0); +lean_inc(x_24); +lean_dec(x_22); +x_25 = lean_ctor_get(x_23, 0); +lean_inc(x_25); +x_26 = lean_ctor_get(x_23, 1); lean_inc(x_26); -x_27 = lean_ctor_get(x_25, 0); -lean_inc(x_27); -lean_dec(x_25); -x_28 = lean_ctor_get(x_26, 0); +lean_dec(x_23); +x_27 = lean_st_ref_take(x_2, x_11); +x_28 = lean_ctor_get(x_27, 0); lean_inc(x_28); -x_29 = lean_ctor_get(x_26, 1); +x_29 = lean_ctor_get(x_27, 1); lean_inc(x_29); -lean_dec(x_26); -x_30 = lean_st_ref_take(x_2, x_11); -x_31 = lean_ctor_get(x_30, 0); -lean_inc(x_31); -x_32 = lean_ctor_get(x_30, 1); -lean_inc(x_32); -lean_dec(x_30); -x_33 = !lean_is_exclusive(x_31); -if (x_33 == 0) +lean_dec(x_27); +x_30 = !lean_is_exclusive(x_28); +if (x_30 == 0) { -lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41; -x_34 = lean_ctor_get(x_31, 3); -lean_inc(x_27); -x_35 = lean_array_push(x_34, x_27); -lean_ctor_set(x_31, 3, x_35); -x_36 = lean_st_ref_set(x_2, x_31, x_32); -x_37 = lean_ctor_get(x_36, 1); -lean_inc(x_37); -lean_dec(x_36); -x_38 = l_Lean_Elab_Frontend_setParserState(x_28, x_1, x_2, x_37); -x_39 = lean_ctor_get(x_38, 1); -lean_inc(x_39); -lean_dec(x_38); -x_40 = l_Lean_Elab_Frontend_setMessages(x_29, x_1, x_2, x_39); -x_41 = !lean_is_exclusive(x_40); +lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38; +x_31 = lean_ctor_get(x_28, 3); +lean_inc(x_24); +x_32 = lean_array_push(x_31, x_24); +lean_ctor_set(x_28, 3, x_32); +x_33 = lean_st_ref_set(x_2, x_28, x_29); +x_34 = lean_ctor_get(x_33, 1); +lean_inc(x_34); +lean_dec(x_33); +x_35 = l_Lean_Elab_Frontend_setParserState(x_25, x_1, x_2, x_34); +x_36 = lean_ctor_get(x_35, 1); +lean_inc(x_36); +lean_dec(x_35); +x_37 = l_Lean_Elab_Frontend_setMessages(x_26, x_1, x_2, x_36); +x_38 = !lean_is_exclusive(x_37); +if (x_38 == 0) +{ +lean_object* x_39; lean_object* x_40; uint8_t x_41; +x_39 = lean_ctor_get(x_37, 1); +x_40 = lean_ctor_get(x_37, 0); +lean_dec(x_40); +lean_inc(x_24); +x_41 = l_Lean_Parser_isEOI(x_24); if (x_41 == 0) { -lean_object* x_42; lean_object* x_43; uint8_t x_44; -x_42 = lean_ctor_get(x_40, 1); -x_43 = lean_ctor_get(x_40, 0); -lean_dec(x_43); -lean_inc(x_27); -x_44 = l_Lean_Parser_isEOI(x_27); -if (x_44 == 0) +uint8_t x_42; +lean_inc(x_24); +x_42 = l_Lean_Parser_isExitCommand(x_24); +if (x_42 == 0) { -uint8_t x_45; -lean_inc(x_27); -x_45 = l_Lean_Parser_isExitCommand(x_27); -if (x_45 == 0) -{ -lean_object* x_46; lean_object* x_47; lean_object* x_48; -lean_free_object(x_40); -x_46 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); -lean_closure_set(x_46, 0, x_27); -x_47 = l_Lean_Elab_Frontend_processCommand___closed__2; -x_48 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_47, x_16, x_22, x_46, x_1, x_2, x_42); -lean_dec(x_22); +lean_object* x_43; lean_object* x_44; lean_object* x_45; +lean_free_object(x_37); +x_43 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); +lean_closure_set(x_43, 0, x_24); +x_44 = l_Lean_Elab_Frontend_processCommand___closed__2; +x_45 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_44, x_16, x_43, x_1, x_2, x_39); lean_dec(x_16); -if (lean_obj_tag(x_48) == 0) +if (lean_obj_tag(x_45) == 0) { -uint8_t x_49; -x_49 = !lean_is_exclusive(x_48); -if (x_49 == 0) +uint8_t x_46; +x_46 = !lean_is_exclusive(x_45); +if (x_46 == 0) { -lean_object* x_50; uint8_t x_51; lean_object* x_52; -x_50 = lean_ctor_get(x_48, 0); -lean_dec(x_50); +lean_object* x_47; uint8_t x_48; lean_object* x_49; +x_47 = lean_ctor_get(x_45, 0); +lean_dec(x_47); +x_48 = 0; +x_49 = lean_box(x_48); +lean_ctor_set(x_45, 0, x_49); +return x_45; +} +else +{ +lean_object* x_50; uint8_t x_51; lean_object* x_52; lean_object* x_53; +x_50 = lean_ctor_get(x_45, 1); +lean_inc(x_50); +lean_dec(x_45); x_51 = 0; x_52 = lean_box(x_51); -lean_ctor_set(x_48, 0, x_52); -return x_48; -} -else -{ -lean_object* x_53; uint8_t x_54; lean_object* x_55; lean_object* x_56; -x_53 = lean_ctor_get(x_48, 1); -lean_inc(x_53); -lean_dec(x_48); -x_54 = 0; -x_55 = lean_box(x_54); -x_56 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_56, 0, x_55); -lean_ctor_set(x_56, 1, x_53); -return x_56; +x_53 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_53, 0, x_52); +lean_ctor_set(x_53, 1, x_50); +return x_53; } } else { -uint8_t x_57; -x_57 = !lean_is_exclusive(x_48); -if (x_57 == 0) +uint8_t x_54; +x_54 = !lean_is_exclusive(x_45); +if (x_54 == 0) { -return x_48; +return x_45; } else { -lean_object* x_58; lean_object* x_59; lean_object* x_60; -x_58 = lean_ctor_get(x_48, 0); -x_59 = lean_ctor_get(x_48, 1); -lean_inc(x_59); -lean_inc(x_58); -lean_dec(x_48); -x_60 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_60, 0, x_58); -lean_ctor_set(x_60, 1, x_59); -return x_60; +lean_object* x_55; lean_object* x_56; lean_object* x_57; +x_55 = lean_ctor_get(x_45, 0); +x_56 = lean_ctor_get(x_45, 1); +lean_inc(x_56); +lean_inc(x_55); +lean_dec(x_45); +x_57 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_57, 0, x_55); +lean_ctor_set(x_57, 1, x_56); +return x_57; } } } else { -uint8_t x_61; lean_object* x_62; -lean_dec(x_27); -lean_dec(x_22); +uint8_t x_58; lean_object* x_59; +lean_dec(x_24); lean_dec(x_16); lean_dec(x_2); lean_dec(x_1); -x_61 = 1; -x_62 = lean_box(x_61); -lean_ctor_set(x_40, 0, x_62); -return x_40; +x_58 = 1; +x_59 = lean_box(x_58); +lean_ctor_set(x_37, 0, x_59); +return x_37; } } else { -uint8_t x_63; lean_object* x_64; -lean_dec(x_27); -lean_dec(x_22); +uint8_t x_60; lean_object* x_61; +lean_dec(x_24); lean_dec(x_16); lean_dec(x_2); lean_dec(x_1); -x_63 = 1; -x_64 = lean_box(x_63); -lean_ctor_set(x_40, 0, x_64); -return x_40; +x_60 = 1; +x_61 = lean_box(x_60); +lean_ctor_set(x_37, 0, x_61); +return x_37; } } else { -lean_object* x_65; uint8_t x_66; -x_65 = lean_ctor_get(x_40, 1); -lean_inc(x_65); -lean_dec(x_40); -lean_inc(x_27); -x_66 = l_Lean_Parser_isEOI(x_27); -if (x_66 == 0) +lean_object* x_62; uint8_t x_63; +x_62 = lean_ctor_get(x_37, 1); +lean_inc(x_62); +lean_dec(x_37); +lean_inc(x_24); +x_63 = l_Lean_Parser_isEOI(x_24); +if (x_63 == 0) { -uint8_t x_67; -lean_inc(x_27); -x_67 = l_Lean_Parser_isExitCommand(x_27); -if (x_67 == 0) +uint8_t x_64; +lean_inc(x_24); +x_64 = l_Lean_Parser_isExitCommand(x_24); +if (x_64 == 0) { -lean_object* x_68; lean_object* x_69; lean_object* x_70; -x_68 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); -lean_closure_set(x_68, 0, x_27); -x_69 = l_Lean_Elab_Frontend_processCommand___closed__2; -x_70 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_69, x_16, x_22, x_68, x_1, x_2, x_65); -lean_dec(x_22); +lean_object* x_65; lean_object* x_66; lean_object* x_67; +x_65 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); +lean_closure_set(x_65, 0, x_24); +x_66 = l_Lean_Elab_Frontend_processCommand___closed__2; +x_67 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_66, x_16, x_65, x_1, x_2, x_62); lean_dec(x_16); -if (lean_obj_tag(x_70) == 0) +if (lean_obj_tag(x_67) == 0) { -lean_object* x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; -x_71 = lean_ctor_get(x_70, 1); -lean_inc(x_71); -if (lean_is_exclusive(x_70)) { - lean_ctor_release(x_70, 0); - lean_ctor_release(x_70, 1); - x_72 = x_70; +lean_object* x_68; lean_object* x_69; uint8_t x_70; lean_object* x_71; lean_object* x_72; +x_68 = lean_ctor_get(x_67, 1); +lean_inc(x_68); +if (lean_is_exclusive(x_67)) { + lean_ctor_release(x_67, 0); + lean_ctor_release(x_67, 1); + x_69 = x_67; } else { - lean_dec_ref(x_70); - x_72 = lean_box(0); + lean_dec_ref(x_67); + x_69 = lean_box(0); } -x_73 = 0; -x_74 = lean_box(x_73); -if (lean_is_scalar(x_72)) { - x_75 = lean_alloc_ctor(0, 2, 0); +x_70 = 0; +x_71 = lean_box(x_70); +if (lean_is_scalar(x_69)) { + x_72 = lean_alloc_ctor(0, 2, 0); } else { - x_75 = x_72; + x_72 = x_69; } -lean_ctor_set(x_75, 0, x_74); -lean_ctor_set(x_75, 1, x_71); -return x_75; +lean_ctor_set(x_72, 0, x_71); +lean_ctor_set(x_72, 1, x_68); +return x_72; } else { -lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; -x_76 = lean_ctor_get(x_70, 0); -lean_inc(x_76); -x_77 = lean_ctor_get(x_70, 1); -lean_inc(x_77); -if (lean_is_exclusive(x_70)) { - lean_ctor_release(x_70, 0); - lean_ctor_release(x_70, 1); - x_78 = x_70; +lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; +x_73 = lean_ctor_get(x_67, 0); +lean_inc(x_73); +x_74 = lean_ctor_get(x_67, 1); +lean_inc(x_74); +if (lean_is_exclusive(x_67)) { + lean_ctor_release(x_67, 0); + lean_ctor_release(x_67, 1); + x_75 = x_67; } else { - lean_dec_ref(x_70); - x_78 = lean_box(0); + lean_dec_ref(x_67); + x_75 = lean_box(0); } -if (lean_is_scalar(x_78)) { - x_79 = lean_alloc_ctor(1, 2, 0); +if (lean_is_scalar(x_75)) { + x_76 = lean_alloc_ctor(1, 2, 0); } else { - x_79 = x_78; + x_76 = x_75; } -lean_ctor_set(x_79, 0, x_76); -lean_ctor_set(x_79, 1, x_77); +lean_ctor_set(x_76, 0, x_73); +lean_ctor_set(x_76, 1, x_74); +return x_76; +} +} +else +{ +uint8_t x_77; lean_object* x_78; lean_object* x_79; +lean_dec(x_24); +lean_dec(x_16); +lean_dec(x_2); +lean_dec(x_1); +x_77 = 1; +x_78 = lean_box(x_77); +x_79 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_79, 0, x_78); +lean_ctor_set(x_79, 1, x_62); return x_79; } } else { uint8_t x_80; lean_object* x_81; lean_object* x_82; -lean_dec(x_27); -lean_dec(x_22); +lean_dec(x_24); lean_dec(x_16); lean_dec(x_2); lean_dec(x_1); @@ -1335,182 +1338,162 @@ x_80 = 1; x_81 = lean_box(x_80); x_82 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_82, 0, x_81); -lean_ctor_set(x_82, 1, x_65); +lean_ctor_set(x_82, 1, x_62); return x_82; } } +} else { -uint8_t x_83; lean_object* x_84; lean_object* x_85; -lean_dec(x_27); -lean_dec(x_22); +lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; uint8_t x_96; +x_83 = lean_ctor_get(x_28, 0); +x_84 = lean_ctor_get(x_28, 1); +x_85 = lean_ctor_get(x_28, 2); +x_86 = lean_ctor_get(x_28, 3); +lean_inc(x_86); +lean_inc(x_85); +lean_inc(x_84); +lean_inc(x_83); +lean_dec(x_28); +lean_inc(x_24); +x_87 = lean_array_push(x_86, x_24); +x_88 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_88, 0, x_83); +lean_ctor_set(x_88, 1, x_84); +lean_ctor_set(x_88, 2, x_85); +lean_ctor_set(x_88, 3, x_87); +x_89 = lean_st_ref_set(x_2, x_88, x_29); +x_90 = lean_ctor_get(x_89, 1); +lean_inc(x_90); +lean_dec(x_89); +x_91 = l_Lean_Elab_Frontend_setParserState(x_25, x_1, x_2, x_90); +x_92 = lean_ctor_get(x_91, 1); +lean_inc(x_92); +lean_dec(x_91); +x_93 = l_Lean_Elab_Frontend_setMessages(x_26, x_1, x_2, x_92); +x_94 = lean_ctor_get(x_93, 1); +lean_inc(x_94); +if (lean_is_exclusive(x_93)) { + lean_ctor_release(x_93, 0); + lean_ctor_release(x_93, 1); + x_95 = x_93; +} else { + lean_dec_ref(x_93); + x_95 = lean_box(0); +} +lean_inc(x_24); +x_96 = l_Lean_Parser_isEOI(x_24); +if (x_96 == 0) +{ +uint8_t x_97; +lean_inc(x_24); +x_97 = l_Lean_Parser_isExitCommand(x_24); +if (x_97 == 0) +{ +lean_object* x_98; lean_object* x_99; lean_object* x_100; +lean_dec(x_95); +x_98 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); +lean_closure_set(x_98, 0, x_24); +x_99 = l_Lean_Elab_Frontend_processCommand___closed__2; +x_100 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_99, x_16, x_98, x_1, x_2, x_94); +lean_dec(x_16); +if (lean_obj_tag(x_100) == 0) +{ +lean_object* x_101; lean_object* x_102; uint8_t x_103; lean_object* x_104; lean_object* x_105; +x_101 = lean_ctor_get(x_100, 1); +lean_inc(x_101); +if (lean_is_exclusive(x_100)) { + lean_ctor_release(x_100, 0); + lean_ctor_release(x_100, 1); + x_102 = x_100; +} else { + lean_dec_ref(x_100); + x_102 = lean_box(0); +} +x_103 = 0; +x_104 = lean_box(x_103); +if (lean_is_scalar(x_102)) { + x_105 = lean_alloc_ctor(0, 2, 0); +} else { + x_105 = x_102; +} +lean_ctor_set(x_105, 0, x_104); +lean_ctor_set(x_105, 1, x_101); +return x_105; +} +else +{ +lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; +x_106 = lean_ctor_get(x_100, 0); +lean_inc(x_106); +x_107 = lean_ctor_get(x_100, 1); +lean_inc(x_107); +if (lean_is_exclusive(x_100)) { + lean_ctor_release(x_100, 0); + lean_ctor_release(x_100, 1); + x_108 = x_100; +} else { + lean_dec_ref(x_100); + x_108 = lean_box(0); +} +if (lean_is_scalar(x_108)) { + x_109 = lean_alloc_ctor(1, 2, 0); +} else { + x_109 = x_108; +} +lean_ctor_set(x_109, 0, x_106); +lean_ctor_set(x_109, 1, x_107); +return x_109; +} +} +else +{ +uint8_t x_110; lean_object* x_111; lean_object* x_112; +lean_dec(x_24); lean_dec(x_16); lean_dec(x_2); lean_dec(x_1); -x_83 = 1; -x_84 = lean_box(x_83); -x_85 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_85, 0, x_84); -lean_ctor_set(x_85, 1, x_65); -return x_85; -} -} -} -else -{ -lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; uint8_t x_99; -x_86 = lean_ctor_get(x_31, 0); -x_87 = lean_ctor_get(x_31, 1); -x_88 = lean_ctor_get(x_31, 2); -x_89 = lean_ctor_get(x_31, 3); -lean_inc(x_89); -lean_inc(x_88); -lean_inc(x_87); -lean_inc(x_86); -lean_dec(x_31); -lean_inc(x_27); -x_90 = lean_array_push(x_89, x_27); -x_91 = lean_alloc_ctor(0, 4, 0); -lean_ctor_set(x_91, 0, x_86); -lean_ctor_set(x_91, 1, x_87); -lean_ctor_set(x_91, 2, x_88); -lean_ctor_set(x_91, 3, x_90); -x_92 = lean_st_ref_set(x_2, x_91, x_32); -x_93 = lean_ctor_get(x_92, 1); -lean_inc(x_93); -lean_dec(x_92); -x_94 = l_Lean_Elab_Frontend_setParserState(x_28, x_1, x_2, x_93); -x_95 = lean_ctor_get(x_94, 1); -lean_inc(x_95); -lean_dec(x_94); -x_96 = l_Lean_Elab_Frontend_setMessages(x_29, x_1, x_2, x_95); -x_97 = lean_ctor_get(x_96, 1); -lean_inc(x_97); -if (lean_is_exclusive(x_96)) { - lean_ctor_release(x_96, 0); - lean_ctor_release(x_96, 1); - x_98 = x_96; +x_110 = 1; +x_111 = lean_box(x_110); +if (lean_is_scalar(x_95)) { + x_112 = lean_alloc_ctor(0, 2, 0); } else { - lean_dec_ref(x_96); - x_98 = lean_box(0); + x_112 = x_95; } -lean_inc(x_27); -x_99 = l_Lean_Parser_isEOI(x_27); -if (x_99 == 0) -{ -uint8_t x_100; -lean_inc(x_27); -x_100 = l_Lean_Parser_isExitCommand(x_27); -if (x_100 == 0) -{ -lean_object* x_101; lean_object* x_102; lean_object* x_103; -lean_dec(x_98); -x_101 = lean_alloc_closure((void*)(l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed), 4, 1); -lean_closure_set(x_101, 0, x_27); -x_102 = l_Lean_Elab_Frontend_processCommand___closed__2; -x_103 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_102, x_16, x_22, x_101, x_1, x_2, x_97); -lean_dec(x_22); -lean_dec(x_16); -if (lean_obj_tag(x_103) == 0) -{ -lean_object* x_104; lean_object* x_105; uint8_t x_106; lean_object* x_107; lean_object* x_108; -x_104 = lean_ctor_get(x_103, 1); -lean_inc(x_104); -if (lean_is_exclusive(x_103)) { - lean_ctor_release(x_103, 0); - lean_ctor_release(x_103, 1); - x_105 = x_103; -} else { - lean_dec_ref(x_103); - x_105 = lean_box(0); -} -x_106 = 0; -x_107 = lean_box(x_106); -if (lean_is_scalar(x_105)) { - x_108 = lean_alloc_ctor(0, 2, 0); -} else { - x_108 = x_105; -} -lean_ctor_set(x_108, 0, x_107); -lean_ctor_set(x_108, 1, x_104); -return x_108; -} -else -{ -lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; -x_109 = lean_ctor_get(x_103, 0); -lean_inc(x_109); -x_110 = lean_ctor_get(x_103, 1); -lean_inc(x_110); -if (lean_is_exclusive(x_103)) { - lean_ctor_release(x_103, 0); - lean_ctor_release(x_103, 1); - x_111 = x_103; -} else { - lean_dec_ref(x_103); - x_111 = lean_box(0); -} -if (lean_is_scalar(x_111)) { - x_112 = lean_alloc_ctor(1, 2, 0); -} else { - x_112 = x_111; -} -lean_ctor_set(x_112, 0, x_109); -lean_ctor_set(x_112, 1, x_110); +lean_ctor_set(x_112, 0, x_111); +lean_ctor_set(x_112, 1, x_94); return x_112; } } else { uint8_t x_113; lean_object* x_114; lean_object* x_115; -lean_dec(x_27); -lean_dec(x_22); +lean_dec(x_24); lean_dec(x_16); lean_dec(x_2); lean_dec(x_1); x_113 = 1; x_114 = lean_box(x_113); -if (lean_is_scalar(x_98)) { +if (lean_is_scalar(x_95)) { x_115 = lean_alloc_ctor(0, 2, 0); } else { - x_115 = x_98; + x_115 = x_95; } lean_ctor_set(x_115, 0, x_114); -lean_ctor_set(x_115, 1, x_97); +lean_ctor_set(x_115, 1, x_94); return x_115; } } -else -{ -uint8_t x_116; lean_object* x_117; lean_object* x_118; -lean_dec(x_27); -lean_dec(x_22); -lean_dec(x_16); -lean_dec(x_2); -lean_dec(x_1); -x_116 = 1; -x_117 = lean_box(x_116); -if (lean_is_scalar(x_98)) { - x_118 = lean_alloc_ctor(0, 2, 0); -} else { - x_118 = x_98; -} -lean_ctor_set(x_118, 0, x_117); -lean_ctor_set(x_118, 1, x_97); -return x_118; } } -} -} -lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +lean_object* l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { -lean_object* x_8; -x_8 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7); -lean_dec(x_3); +lean_object* x_7; +x_7 = l_Lean_profileitM___at_Lean_Elab_Frontend_processCommand___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6); lean_dec(x_2); lean_dec(x_1); -return x_8; +return x_7; } } lean_object* l_Lean_Elab_Frontend_processCommand___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { @@ -1853,7 +1836,7 @@ return x_47; } } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1() { _start: { lean_object* x_1; @@ -1861,17 +1844,17 @@ x_1 = lean_mk_string("printMessageEndPos"); return x_1; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3() { _start: { lean_object* x_1; @@ -1879,13 +1862,13 @@ x_1 = lean_mk_string("print end position of each message in addition to start po return x_1; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_initFn____x40_Lean_Util_PPExt___hyg_3____closed__3; x_2 = l_Lean_instInhabitedParserDescr___closed__1; -x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3; +x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -1893,12 +1876,12 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584_(lean_object* x_1) { +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2; -x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2; +x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4; x_4 = lean_register_option(x_2, x_3, x_1); return x_4; } @@ -1907,7 +1890,7 @@ uint8_t l_Lean_Elab_getPrintMessageEndPos(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; uint8_t x_4; -x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2; +x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2; x_3 = 0; x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3); return x_4; @@ -2529,15 +2512,15 @@ l_Lean_Elab_Frontend_processCommand___closed__1 = _init_l_Lean_Elab_Frontend_pro lean_mark_persistent(l_Lean_Elab_Frontend_processCommand___closed__1); l_Lean_Elab_Frontend_processCommand___closed__2 = _init_l_Lean_Elab_Frontend_processCommand___closed__2(); lean_mark_persistent(l_Lean_Elab_Frontend_processCommand___closed__2); -l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__1); -l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__2); -l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__3); -l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584____closed__4); -res = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_584_(lean_io_mk_world()); +l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__1); +l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__2); +l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__3); +l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582____closed__4); +res = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_582_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Environment.c b/stage0/stdlib/Lean/Environment.c index c89efa66d3..6aebbf61cc 100644 --- a/stage0/stdlib/Lean/Environment.c +++ b/stage0/stdlib/Lean/Environment.c @@ -95,10 +95,10 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l_Lean_mkTagDeclarationExtension___closed__1; lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_mkTagDeclarationExtension___spec__3(lean_object*, lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3; lean_object* l___private_Lean_Environment_0__Lean_Environment_throwUnexpectedType(lean_object*); lean_object* l_Array_binSearchAux___at_Lean_MapDeclarationExtension_contains___spec__1(lean_object*); lean_object* l_Lean_MapDeclarationExtension_find_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3; lean_object* lean_environment_set_main_module(lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Environment_0__Lean_Environment_isQuotInit___boxed(lean_object*); @@ -212,6 +212,7 @@ lean_object* l_Lean_SimplePersistentEnvExtensionDescr_toArrayFn___default___rarg lean_object* l_Lean_MapDeclarationExtension_find_x3f_match__1(lean_object*, lean_object*); lean_object* l_Lean_instInhabitedEnvExtensionInterface___closed__1; lean_object* l_Lean_instInhabitedEnvironment___closed__3; +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1; lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_mkMapDeclarationExtension___spec__7___rarg(lean_object*, lean_object*); lean_object* l_Lean_EnvironmentHeader_moduleNames___default; lean_object* l_Lean_ImportState_moduleNameSet___default; @@ -224,11 +225,9 @@ lean_object* l_Std_PersistentHashMap_foldlM___at_Lean_mkModuleData___spec__2___b lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_registerSimplePersistentEnvExtension___spec__1___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Environment_0__Lean_Environment_registerNamePrefixes_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1; lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Environment_find_x3f___spec__2(lean_object*, lean_object*); lean_object* lean_write_module(lean_object*, lean_object*, lean_object*); uint8_t l_Array_binSearchAux___at_Lean_TagDeclarationExtension_isTagged___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_getEntries(lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec__8___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_modifyState___rarg(lean_object*, lean_object*, lean_object*); @@ -242,7 +241,6 @@ lean_object* l_Lean_Environment_hasUnsafe___lambda__1___boxed(lean_object*, lean lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Environment_displayStats___spec__8(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_modifyState_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_setState_match__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2; lean_object* l_Nat_foldAux___at_Lean_mkModuleData___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyMUnsafe_any___at_Lean_mkMapDeclarationExtension___spec__8___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_take(lean_object*, lean_object*); @@ -264,6 +262,7 @@ lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___elambda__1___rarg___boxed( lean_object* l_Array_qpartition_loop___at_Lean_mkMapDeclarationExtension___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Environment_0__Lean_getEntriesFor___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_instReprList___rarg___closed__1; +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_instInhabitedEnvironment___closed__5; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Environment_0__Lean_setImportedEntries___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkEmptyEnvironment___closed__1; @@ -295,6 +294,7 @@ lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_registerSimpl lean_object* l___private_Lean_Environment_0__Lean_setImportedEntries___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_namespacesExt___elambda__1(lean_object*); lean_object* l_Lean_ConstantInfo_name(lean_object*); +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2; lean_object* l_IO_fileExists___at_Lean_importModules_importMods___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkMapDeclarationExtension___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_TagDeclarationExtension_isTagged_match__1(lean_object*); @@ -358,7 +358,6 @@ lean_object* l_Lean_Environment_evalConstCheck___rarg___closed__1; lean_object* l_Lean_persistentEnvExtensionsRef; lean_object* l_Lean_mkMapDeclarationExtension(lean_object*); lean_object* l_Lean_ImportState_regions___default; -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(lean_object*, size_t, size_t, lean_object*); lean_object* lean_environment_add(lean_object*, lean_object*); lean_object* lean_save_module_data(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_withImportModules___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -366,6 +365,7 @@ lean_object* l_Lean_ImportState_moduleNames___default; lean_object* l_Lean_EnvExtension_getState___rarg___boxed(lean_object*, lean_object*); lean_object* l_Array_qsort_sort___at_Lean_mkMapDeclarationExtension___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*); size_t lean_usize_modn(size_t, lean_object*); +lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_saveModuleData___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkModuleData(lean_object*, lean_object*); lean_object* l_Lean_MapDeclarationExtension_instInhabitedMapDeclarationExtension(lean_object*); @@ -394,13 +394,15 @@ uint8_t lean_kernel_is_def_eq(lean_object*, lean_object*, lean_object*, lean_obj lean_object* l_Array_anyMUnsafe_any___at_Lean_mkMapDeclarationExtension___spec__8(lean_object*); lean_object* l_Lean_CompactedRegion_free___boxed(lean_object*, lean_object*); lean_object* l_Lean_instInhabitedEnvExtensionInterface; +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(lean_object*, size_t, size_t, lean_object*); extern uint32_t l_instInhabitedUInt32___closed__1; lean_object* l_Lean_EnvExtensionInterfaceImp___closed__6; lean_object* l_Lean_TagDeclarationExtension_instInhabitedTagDeclarationExtension___closed__1; lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__1(lean_object*, lean_object*); lean_object* l_Lean_importModules_importMods_match__2___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; +lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1(lean_object*, lean_object*); size_t lean_usize_of_nat(lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Lean_instInhabitedModuleData; extern lean_object* l_Lean_NameSet_empty; lean_object* l_Lean_ConstantInfo_type(lean_object*); @@ -419,7 +421,6 @@ size_t l_USize_land(size_t, size_t); lean_object* l_Lean_Environment_evalConstCheck___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvironmentHeader_regions___default; -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*); lean_object* l_Lean_mkStateFromImportedEntries___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkEmptyEnvironment___boxed(lean_object*, lean_object*); @@ -510,13 +511,13 @@ lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg___lambda__1(l lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4___closed__1; lean_object* l_Array_binSearchAux___at_Lean_MapDeclarationExtension_find_x3f___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3(lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___closed__2; lean_object* l_Lean_EnvExtensionInterfaceImp___elambda__4(lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Environment_find_x3f___spec__3(lean_object*, size_t, lean_object*); lean_object* l_Lean_EnvExtension_instInhabitedEnvExtension___boxed(lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_mkInitialExtStates___boxed__const__1; lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Environment_find_x3f___spec__2___boxed(lean_object*, lean_object*); +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3(lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_instInhabitedEnvExtensionInterface___closed__3; lean_object* l_Lean_EnvExtensionInterfaceImp___elambda__2___rarg___boxed(lean_object*, lean_object*); lean_object* l_Std_HashMapImp_moveEntries___at_Lean_Environment_addAux___spec__9(lean_object*, lean_object*, lean_object*); @@ -527,6 +528,7 @@ lean_object* l_Lean_SimplePersistentEnvExtension_setState_match__1___rarg(lean_o lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__4___boxed(lean_object*); lean_object* l_Lean_instMonadEnv___rarg___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_foldlM___at_Lean_mkModuleData___spec__2(lean_object*, lean_object*); +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Environment_hasUnsafe_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___closed__3; lean_object* lean_nat_mul(lean_object*, lean_object*); @@ -537,7 +539,7 @@ lean_object* l_Lean_Environment_header___default___closed__1; lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtensionDescr_statsFn___default(lean_object*, lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913_(lean_object*); +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909_(lean_object*); lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_1088_(lean_object*); lean_object* l_Lean_instInhabitedPersistentEnvExtensionState___rarg(lean_object*); lean_object* l___private_Lean_Environment_0__Lean_getEntriesFor___closed__1; @@ -562,7 +564,6 @@ lean_object* l_Std_AssocList_foldlM___at_Lean_importModules___spec__6(lean_objec lean_object* l_Array_forInUnsafe_loop___at_Lean_importModules___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_RBNode_find___at_Lean_MapDeclarationExtension_find_x3f___spec__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___closed__7; -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Environment_allImportedModuleNames(lean_object*); lean_object* l_Lean_Environment_hasUnsafe_match__1(lean_object*); lean_object* l_Lean_Environment_addAux(lean_object*, lean_object*); @@ -570,7 +571,7 @@ uint8_t l_Lean_MapDeclarationExtension_contains___rarg(lean_object*, lean_object lean_object* l_Std_PersistentHashMap_foldlMAux_traverse___at_Lean_mkModuleData___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceImp___elambda__5___rarg(lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceImp___elambda__2(lean_object*); -lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_qpartition_loop___at_Lean_mkMapDeclarationExtension___spec__2(lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_instInhabitedSimplePersistentEnvExtension___rarg(lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___closed__5; @@ -599,7 +600,6 @@ lean_object* l_Lean_EnvExtensionInterfaceUnsafe_mkInitialExtStates(lean_object*) lean_object* l_Lean_mkStateFromImportedEntries___rarg___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_instToStringImport(lean_object*); lean_object* l_Lean_instInhabitedPersistentEnvExtension(lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_Lean_instInhabitedPosition___closed__1; lean_object* l_Array_anyMUnsafe_any___at_Lean_mkTagDeclarationExtension___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Environment_find_x3f___spec__5(lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceImp___elambda__1(lean_object*); @@ -661,10 +661,10 @@ lean_object* l_Array_anyMUnsafe_any___at_Lean_registerPersistentEnvExtensionUnsa extern lean_object* l_Id_instMonadId___closed__4; lean_object* lean_uint32_to_nat(uint32_t); lean_object* l_Array_qsort_sort___at_Lean_mkMapDeclarationExtension___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1(lean_object*, lean_object*); uint32_t l_Lean_EnvironmentHeader_trustLevel___default; lean_object* l_Lean_mkTagDeclarationExtension___closed__3; lean_object* l_Std_HashMapImp_insert___at_Lean_Environment_addAux___spec__6(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5; lean_object* l_Lean_importModules___closed__2; lean_object* l_Lean_Kernel_isDefEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_compacted_region_free(size_t, lean_object*); @@ -683,7 +683,6 @@ lean_object* l___private_Lean_Environment_0__Lean_Environment_registerNamePrefix lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_qsort_sort___at_Lean_mkMapDeclarationExtension___spec__1___rarg___closed__1; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5; lean_object* lean_add_decl(lean_object*, lean_object*); lean_object* l_Std_HashMapImp_contains___at_Lean_Environment_contains___spec__2___boxed(lean_object*, lean_object*); static lean_object* _init_l_Lean_EnvExtensionStateSpec() { @@ -11118,7 +11117,7 @@ return x_1; lean_object* lean_import_modules(lean_object* x_1, lean_object* x_2, uint32_t x_3, lean_object* x_4) { _start: { -lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_inc(x_1); x_5 = lean_alloc_closure((void*)(l_Lean_importModules___lambda__2___boxed), 3, 1); lean_closure_set(x_5, 0, x_1); @@ -11136,10 +11135,9 @@ x_10 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2); lean_closure_set(x_10, 0, x_7); lean_closure_set(x_10, 1, x_9); x_11 = l_Lean_importModules___closed__3; -x_12 = l_Lean_instInhabitedPosition___closed__1; -x_13 = l_Lean_profileitIOUnsafe___rarg(x_11, x_2, x_12, x_10, x_4); +x_12 = l_Lean_profileitIOUnsafe___rarg(x_11, x_2, x_10, x_4); lean_dec(x_2); -return x_13; +return x_12; } } lean_object* l_Std_AssocList_contains___at_Lean_importModules___spec__3___boxed(lean_object* x_1, lean_object* x_2) { @@ -11392,7 +11390,7 @@ x_7 = l_Lean_withImportModules___rarg(x_1, x_2, x_6, x_4, x_5); return x_7; } } -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { _start: { uint8_t x_5; @@ -11415,7 +11413,7 @@ return x_4; } } } -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) { _start: { uint8_t x_5; @@ -11453,7 +11451,7 @@ size_t x_15; size_t x_16; lean_object* x_17; x_15 = 0; x_16 = lean_usize_of_nat(x_7); lean_dec(x_7); -x_17 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(x_6, x_15, x_16, x_4); +x_17 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(x_6, x_15, x_16, x_4); lean_dec(x_6); x_2 = x_11; x_4 = x_17; @@ -11467,7 +11465,7 @@ return x_4; } } } -lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; @@ -11494,13 +11492,13 @@ size_t x_7; size_t x_8; lean_object* x_9; x_7 = 0; x_8 = lean_usize_of_nat(x_3); lean_dec(x_3); -x_9 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3(x_2, x_7, x_8, x_1); +x_9 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3(x_2, x_7, x_8, x_1); return x_9; } } } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1() { _start: { lean_object* x_1; @@ -11508,27 +11506,27 @@ x_1 = lean_mk_string("namespaces"); return x_1; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1; +x_2 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3() { _start: { lean_object* x_1; lean_object* x_2; x_1 = l_Lean_NameSet_empty; -x_2 = lean_alloc_closure((void*)(l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1___boxed), 2, 1); +x_2 = lean_alloc_closure((void*)(l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1___boxed), 2, 1); lean_closure_set(x_2, 0, x_1); return x_2; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4() { _start: { lean_object* x_1; @@ -11537,14 +11535,14 @@ lean_closure_set(x_1, 0, lean_box(0)); return x_1; } } -static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5() { +static lean_object* _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2; +x_1 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2; x_2 = l_Lean_mkTagDeclarationExtension___closed__1; -x_3 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_3 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); @@ -11553,16 +11551,16 @@ lean_ctor_set(x_5, 3, x_4); return x_5; } } -lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913_(lean_object* x_1) { +lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5; +x_2 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5; x_3 = l_Lean_registerSimplePersistentEnvExtension___at_Lean_mkTagDeclarationExtension___spec__3(x_2, x_1); return x_3; } } -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { size_t x_5; size_t x_6; lean_object* x_7; @@ -11570,12 +11568,12 @@ x_5 = lean_unbox_usize(x_2); lean_dec(x_2); x_6 = lean_unbox_usize(x_3); lean_dec(x_3); -x_7 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__2(x_1, x_5, x_6, x_4); +x_7 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__2(x_1, x_5, x_6, x_4); lean_dec(x_1); return x_7; } } -lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { size_t x_5; size_t x_6; lean_object* x_7; @@ -11583,16 +11581,16 @@ x_5 = lean_unbox_usize(x_2); lean_dec(x_2); x_6 = lean_unbox_usize(x_3); lean_dec(x_3); -x_7 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__3(x_1, x_5, x_6, x_4); +x_7 = l_Array_foldlMUnsafe_fold___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__3(x_1, x_5, x_6, x_4); lean_dec(x_1); return x_7; } } -lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2913____spec__1(x_1, x_2); +x_3 = l_Lean_mkStateFromImportedEntries___at_Lean_initFn____x40_Lean_Environment___hyg_2909____spec__1(x_1, x_2); lean_dec(x_2); return x_3; } @@ -13706,16 +13704,16 @@ l_Lean_importModules___closed__2 = _init_l_Lean_importModules___closed__2(); lean_mark_persistent(l_Lean_importModules___closed__2); l_Lean_importModules___closed__3 = _init_l_Lean_importModules___closed__3(); lean_mark_persistent(l_Lean_importModules___closed__3); -l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__1); -l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__2); -l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__3); -l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4); -l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5(); -lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__5); +l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__1); +l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__2); +l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__3); +l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4); +l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5 = _init_l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5(); +lean_mark_persistent(l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__5); l_Lean_namespacesExt___closed__1 = _init_l_Lean_namespacesExt___closed__1(); lean_mark_persistent(l_Lean_namespacesExt___closed__1); l_Lean_namespacesExt___closed__2 = _init_l_Lean_namespacesExt___closed__2(); @@ -13726,7 +13724,7 @@ l_Lean_namespacesExt___closed__4 = _init_l_Lean_namespacesExt___closed__4(); lean_mark_persistent(l_Lean_namespacesExt___closed__4); l_Lean_namespacesExt___closed__5 = _init_l_Lean_namespacesExt___closed__5(); lean_mark_persistent(l_Lean_namespacesExt___closed__5); -res = l_Lean_initFn____x40_Lean_Environment___hyg_2913_(lean_io_mk_world()); +res = l_Lean_initFn____x40_Lean_Environment___hyg_2909_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_namespacesExt = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_namespacesExt); diff --git a/stage0/stdlib/Lean/Meta/Instances.c b/stage0/stdlib/Lean/Meta/Instances.c index d83f0ce6a2..934a0eeeb3 100644 --- a/stage0/stdlib/Lean/Meta/Instances.c +++ b/stage0/stdlib/Lean/Meta/Instances.c @@ -176,9 +176,9 @@ lean_object* l_Lean_Meta_forallMetaTelescopeReducing___boxed(lean_object*, lean_ lean_object* l_Lean_Meta_instanceExtension___closed__1; lean_object* l_Lean_Meta_instanceExtension___closed__2; lean_object* l_Lean_Meta_defaultInstanceExtension___elambda__4(lean_object*, lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; extern lean_object* l_Lean_KernelException_toMessageData___closed__3; size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; extern lean_object* l_Lean_NameSet_empty; lean_object* l_Lean_ConstantInfo_type(lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_690____lambda__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); @@ -5988,7 +5988,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_415____closed__2; x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_415____closed__3; x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_415____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Meta/Match/MatcherInfo.c b/stage0/stdlib/Lean/Meta/Match/MatcherInfo.c index bfbda83a39..90b3f11e6e 100644 --- a/stage0/stdlib/Lean/Meta/Match/MatcherInfo.c +++ b/stage0/stdlib/Lean/Meta/Match/MatcherInfo.c @@ -95,9 +95,9 @@ lean_object* l_Lean_Meta_Match_Extension_extension___closed__4; extern lean_object* l_Lean_mkEmptyEnvironment___lambda__1___closed__1; lean_object* l_Lean_Meta_Match_Extension_addMatcherInfo(lean_object*, lean_object*, lean_object*); size_t l_USize_mul(size_t, size_t); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; lean_object* l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_64____lambda__1(lean_object*); size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Std_AssocList_contains___at_Lean_Meta_Match_Extension_State_addEntry___spec__7___boxed(lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_Match_Extension_getMatcherInfo_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); @@ -1619,7 +1619,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_64____closed__2; x_2 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_64____closed__3; x_3 = l_Lean_Meta_Match_Extension_initFn____x40_Lean_Meta_Match_MatcherInfo___hyg_64____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Meta/SynthInstance.c b/stage0/stdlib/Lean/Meta/SynthInstance.c index 6ead8f23aa..7a0df8386d 100644 --- a/stage0/stdlib/Lean/Meta/SynthInstance.c +++ b/stage0/stdlib/Lean/Meta/SynthInstance.c @@ -21,6 +21,7 @@ extern lean_object* l_Lean_instInhabitedTagAttribute___closed__1; lean_object* l_Lean_Meta_SynthInstance_getMaxHeartbeats___boxed(lean_object*); lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_MkTableKey_normExpr_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1; lean_object* l_Lean_Meta_SynthInstance_instInhabitedAnswer___closed__1; lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessArgs___closed__2; size_t l_USize_add(size_t, size_t); @@ -32,7 +33,6 @@ lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp_ma lean_object* l_Lean_Meta_SynthInstance_addAnswer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_newSubgoal___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessArgs_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1; lean_object* l_Lean_Meta_SynthInstance_newSubgoal___lambda__3(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_SynthInstance_findEntry_x3f___spec__1(lean_object*, lean_object*); lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*); @@ -186,7 +186,7 @@ lean_object* l_Lean_Meta_SynthInstance_getResult___rarg___boxed(lean_object*, le lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_wakeUp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_initFn____x40_Lean_Meta_SynthInstance___hyg_69_(lean_object*); -lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_synthInstance_x3f___lambda__2___closed__7; lean_object* l_Lean_Meta_SynthInstance_tryResolveCore_match__1(lean_object*); uint8_t l_Lean_Meta_SynthInstance_Waiter_isRoot(lean_object*); @@ -209,7 +209,7 @@ lean_object* l_Lean_Meta_SynthInstance_synth___closed__1; lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_getSubgoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___closed__1; lean_object* l_Lean_Meta_SynthInstance_wakeUp_match__1(lean_object*); lean_object* l_Lean_Meta_SynthInstance_initFn____x40_Lean_Meta_SynthInstance___hyg_69____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -273,7 +273,6 @@ lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_preprocessOutParam lean_object* l_Lean_Meta_SynthInstance_instInhabitedConsumerNode; lean_object* l_Lean_Meta_synthInstance_x3f___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_Waiter_isRoot_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_newSubgoal_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_initFn____x40_Lean_Meta_SynthInstance___hyg_69____closed__2; lean_object* l_Lean_Meta_SynthInstance_MkTableKey_normExpr_match__1(lean_object*); @@ -281,6 +280,7 @@ lean_object* l_Array_back___at_Lean_Meta_SynthInstance_getNextToResume___spec__1 lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Meta_synthInstance_x3f___spec__8(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_SynthInstance_getSubgoalsAux_match__1(lean_object*); lean_object* lean_array_to_list(lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at_Lean_Meta_SynthInstance_tryResolve___spec__1___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_getNextToResume___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_initFn____x40_Lean_Meta_SynthInstance___hyg_69____closed__4; @@ -331,8 +331,8 @@ size_t lean_usize_of_nat(lean_object*); lean_object* l_Std_AssocList_find_x3f___at_Lean_Meta_SynthInstance_findEntry_x3f___spec__2___boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4_(lean_object*); lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_32_(lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4717_(lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702_(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4713_(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698_(lean_object*); lean_object* l_Lean_Meta_SynthInstance_MkTableKey_State_lmap___default___closed__1; lean_object* l_Lean_Meta_SynthInstance_getNextToResume___boxed(lean_object*); lean_object* l_Lean_Meta_SynthInstance_MkTableKey_normExpr_match__2(lean_object*); @@ -471,7 +471,7 @@ lean_object* l_Lean_Meta_SynthInstance_resume_match__3(lean_object*); lean_object* l_Array_back___at_Lean_Meta_SynthInstance_getNextToResume___spec__1(lean_object*); lean_object* l_Lean_Meta_SynthInstance_generate___closed__2; lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_generate___closed__1; lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_mkTableKeyFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -488,7 +488,6 @@ extern lean_object* l_term___u2265_____closed__3; lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_SynthInstance_mkAnswer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__5; -extern lean_object* l_Lean_instInhabitedPosition___closed__1; lean_object* l_Lean_Meta_SynthInstance_MkTableKey_State_nextIdx___default; lean_object* l_Lean_Meta_withMCtx___at_Lean_Meta_SynthInstance_newSubgoal___spec__10(lean_object*); lean_object* l_Lean_Meta_SynthInstance_MkTableKey_normExpr_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -17985,20 +17984,20 @@ return x_19; } } } -lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { +lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { -lean_object* x_10; lean_object* x_11; -x_10 = lean_apply_4(x_4, x_5, x_6, x_7, x_8); -x_11 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_3, x_10, x_9); -return x_11; +lean_object* x_9; lean_object* x_10; +x_9 = lean_apply_4(x_3, x_4, x_5, x_6, x_7); +x_10 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_9, x_8); +return x_10; } } lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed), 9, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed), 8, 0); return x_2; } } @@ -21330,7 +21329,7 @@ return x_1; lean_object* l_Lean_Meta_synthInstance_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { -lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; x_8 = lean_ctor_get(x_5, 0); lean_inc(x_8); x_9 = lean_alloc_closure((void*)(l_Lean_Meta_synthInstance_x3f___lambda__4___boxed), 8, 2); @@ -21341,10 +21340,9 @@ x_11 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMet lean_closure_set(x_11, 0, x_10); lean_closure_set(x_11, 1, x_9); x_12 = l_Lean_Meta_synthInstance_x3f___closed__2; -x_13 = l_Lean_instInhabitedPosition___closed__1; -x_14 = l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(x_12, x_8, x_13, x_11, x_3, x_4, x_5, x_6, x_7); +x_13 = l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(x_12, x_8, x_11, x_3, x_4, x_5, x_6, x_7); lean_dec(x_8); -return x_14; +return x_13; } } lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Meta_synthInstance_x3f___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { @@ -21402,15 +21400,14 @@ x_8 = l_Std_PersistentHashMap_insertAux___at_Lean_Meta_synthInstance_x3f___spec_ return x_8; } } -lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) { +lean_object* l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { -lean_object* x_10; -x_10 = l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9); -lean_dec(x_3); +lean_object* x_9; +x_9 = l_Lean_profileitM___at_Lean_Meta_synthInstance_x3f___spec__9___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); lean_dec(x_2); lean_dec(x_1); -return x_10; +return x_9; } } lean_object* l_Lean_Meta_synthInstance_x3f___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { @@ -22551,7 +22548,7 @@ return x_135; } } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { lean_object* x_7; lean_object* x_8; @@ -22560,20 +22557,20 @@ x_8 = l___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp(x_1, x_7, return x_8; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____lambda__1), 6, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____lambda__1), 6, 0); return x_1; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702_(lean_object* x_1) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; x_2 = l_Lean_Meta_synthPendingRef; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1; x_4 = lean_st_ref_set(x_2, x_3, x_1); x_5 = !lean_is_exclusive(x_4); if (x_5 == 0) @@ -22595,7 +22592,7 @@ return x_8; } } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4717_(lean_object* x_1) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4713_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -23039,12 +23036,12 @@ l_Lean_Meta_synthInstance___closed__1 = _init_l_Lean_Meta_synthInstance___closed lean_mark_persistent(l_Lean_Meta_synthInstance___closed__1); l_Lean_Meta_synthInstance___closed__2 = _init_l_Lean_Meta_synthInstance___closed__2(); lean_mark_persistent(l_Lean_Meta_synthInstance___closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702____closed__1); -res = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4702_(lean_io_mk_world()); +l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698____closed__1); +res = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4698_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4717_(lean_io_mk_world()); +res = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4713_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Injection.c b/stage0/stdlib/Lean/Meta/Tactic/Injection.c index 62b6c16150..6a7331e3ce 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Injection.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Injection.c @@ -19,6 +19,7 @@ lean_object* l_Lean_Meta_injectionCore_match__2___rarg(lean_object*, lean_object lean_object* l_Lean_Expr_mvarId_x21(lean_object*); lean_object* l_Lean_Meta_withMVarContext___at_Lean_Meta_admit___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_stringToMessageData(lean_object*); +lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_LocalDecl_userName(lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionIntro_match__2(lean_object*); @@ -27,6 +28,7 @@ lean_object* l_Lean_Meta_injectionCore_match__2(lean_object*); lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Meta_isLevelDefEqAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; lean_object* l_Lean_Meta_injectionIntro_match__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_getCtorNumPropFields(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Tactic_Injection_0__Lean_Meta_heqToEq_match__2(lean_object*); lean_object* l_Lean_Meta_getMVarTag(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_get(lean_object*, lean_object*); @@ -36,9 +38,11 @@ lean_object* l_Lean_Expr_appFn_x21(lean_object*); lean_object* lean_array_push(lean_object*, lean_object*); lean_object* l_ReaderT_bind___at_Lean_Meta_instMonadLCtxMetaM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_appArg_x21(lean_object*); +lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Tactic_injection___closed__1; lean_object* l_Lean_Meta_injectionIntro_match__2___rarg(lean_object*, lean_object*); lean_object* l_Lean_Meta_checkNotAssigned___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionIntro_match__4___rarg(lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionIntro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_myMacro____x40_Init_Notation___hyg_6561____closed__4; @@ -52,6 +56,7 @@ lean_object* l_Lean_addTrace___at_Lean_Meta_isLevelDefEqAux___spec__1(lean_objec lean_object* l_Lean_Meta_tryClear(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_headBeta(lean_object*); lean_object* l_Lean_Meta_injection_match__1(lean_object*); +lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_clear(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionIntro_match__1(lean_object*); @@ -59,6 +64,7 @@ lean_object* l_Lean_Meta_injectionIntro_match__1___rarg(lean_object*, lean_objec lean_object* l___private_Lean_Meta_Tactic_Injection_0__Lean_Meta_heqToEq_match__1___rarg(lean_object*, lean_object*); uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionIntro_match__3___rarg(lean_object*, lean_object*); +extern lean_object* l_Lean_instInhabitedExpr; extern lean_object* l_Lean_KernelException_toMessageData___closed__15; lean_object* l_Lean_Meta_injectionIntro_match__5(lean_object*); lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -73,14 +79,18 @@ extern lean_object* l_Lean_Meta_mkNoConfusion___closed__5; lean_object* l_Lean_Meta_injectionIntro_match__4(lean_object*); lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injection___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l_Lean_mkApp(lean_object*, lean_object*); extern lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_562____closed__4; +lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_Tactic_Injection_0__Lean_Meta_heqToEq_match__1(lean_object*); lean_object* l_Lean_Meta_injection_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkNoConfusion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_getCtorNumPropFields___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_getCtorNumPropFields___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore___lambda__1___closed__3; lean_object* l_Lean_Meta_injectionCore_match__1(lean_object*); lean_object* l___private_Lean_Meta_Tactic_Injection_0__Lean_Meta_heqToEq_match__2___rarg(lean_object*, lean_object*, lean_object*); @@ -92,6 +102,7 @@ lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_objec lean_object* l_Lean_Meta_injection(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore___lambda__1___closed__2; lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_isProp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore___lambda__1___closed__1; lean_object* l_Lean_Meta_injectionCore___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_isConstructorApp_x3f(lean_object*, lean_object*); @@ -101,6 +112,274 @@ lean_object* l_Lean_Meta_injectionIntro_match__3(lean_object*); lean_object* l___private_Lean_Meta_Tactic_Injection_0__Lean_Meta_heqToEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_injectionCore___lambda__1___closed__4; lean_object* l_Lean_Meta_injectionCore_match__3___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) { +_start: +{ +lean_object* x_12; uint8_t x_13; +x_12 = lean_ctor_get(x_3, 1); +x_13 = lean_nat_dec_le(x_12, x_5); +if (x_13 == 0) +{ +lean_object* x_14; uint8_t x_15; +x_14 = lean_unsigned_to_nat(0u); +x_15 = lean_nat_dec_eq(x_4, x_14); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; +x_16 = lean_unsigned_to_nat(1u); +x_17 = lean_nat_sub(x_4, x_16); +lean_dec(x_4); +x_18 = lean_ctor_get(x_1, 3); +x_19 = lean_nat_add(x_18, x_5); +x_20 = l_Lean_instInhabitedExpr; +x_21 = lean_array_get(x_20, x_2, x_19); +lean_dec(x_19); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_22 = l_Lean_Meta_inferType(x_21, x_7, x_8, x_9, x_10, x_11); +if (lean_obj_tag(x_22) == 0) +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; +x_23 = lean_ctor_get(x_22, 0); +lean_inc(x_23); +x_24 = lean_ctor_get(x_22, 1); +lean_inc(x_24); +lean_dec(x_22); +lean_inc(x_10); +lean_inc(x_9); +lean_inc(x_8); +lean_inc(x_7); +x_25 = l_Lean_Meta_isProp(x_23, x_7, x_8, x_9, x_10, x_24); +if (lean_obj_tag(x_25) == 0) +{ +lean_object* x_26; uint8_t x_27; +x_26 = lean_ctor_get(x_25, 0); +lean_inc(x_26); +x_27 = lean_unbox(x_26); +lean_dec(x_26); +if (x_27 == 0) +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_28 = lean_ctor_get(x_25, 1); +lean_inc(x_28); +lean_dec(x_25); +x_29 = lean_ctor_get(x_3, 2); +x_30 = lean_nat_add(x_5, x_29); +lean_dec(x_5); +x_4 = x_17; +x_5 = x_30; +x_11 = x_28; +goto _start; +} +else +{ +lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; +x_32 = lean_ctor_get(x_25, 1); +lean_inc(x_32); +lean_dec(x_25); +x_33 = lean_nat_add(x_6, x_16); +lean_dec(x_6); +x_34 = lean_ctor_get(x_3, 2); +x_35 = lean_nat_add(x_5, x_34); +lean_dec(x_5); +x_4 = x_17; +x_5 = x_35; +x_6 = x_33; +x_11 = x_32; +goto _start; +} +} +else +{ +uint8_t x_37; +lean_dec(x_17); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +x_37 = !lean_is_exclusive(x_25); +if (x_37 == 0) +{ +return x_25; +} +else +{ +lean_object* x_38; lean_object* x_39; lean_object* x_40; +x_38 = lean_ctor_get(x_25, 0); +x_39 = lean_ctor_get(x_25, 1); +lean_inc(x_39); +lean_inc(x_38); +lean_dec(x_25); +x_40 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_40, 0, x_38); +lean_ctor_set(x_40, 1, x_39); +return x_40; +} +} +} +else +{ +uint8_t x_41; +lean_dec(x_17); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +x_41 = !lean_is_exclusive(x_22); +if (x_41 == 0) +{ +return x_22; +} +else +{ +lean_object* x_42; lean_object* x_43; lean_object* x_44; +x_42 = lean_ctor_get(x_22, 0); +x_43 = lean_ctor_get(x_22, 1); +lean_inc(x_43); +lean_inc(x_42); +lean_dec(x_22); +x_44 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_44, 0, x_42); +lean_ctor_set(x_44, 1, x_43); +return x_44; +} +} +} +else +{ +lean_object* x_45; +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_5); +lean_dec(x_4); +x_45 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_45, 0, x_6); +lean_ctor_set(x_45, 1, x_11); +return x_45; +} +} +else +{ +lean_object* x_46; +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_5); +lean_dec(x_4); +x_46 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_46, 0, x_6); +lean_ctor_set(x_46, 1, x_11); +return x_46; +} +} +} +lean_object* l_Lean_Meta_getCtorNumPropFields___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_9 = lean_ctor_get(x_1, 4); +lean_inc(x_9); +x_10 = lean_unsigned_to_nat(0u); +x_11 = lean_unsigned_to_nat(1u); +lean_inc(x_9); +x_12 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_12, 0, x_10); +lean_ctor_set(x_12, 1, x_9); +lean_ctor_set(x_12, 2, x_11); +x_13 = l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1(x_1, x_2, x_12, x_9, x_10, x_10, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_12); +lean_dec(x_1); +if (lean_obj_tag(x_13) == 0) +{ +uint8_t x_14; +x_14 = !lean_is_exclusive(x_13); +if (x_14 == 0) +{ +return x_13; +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_15 = lean_ctor_get(x_13, 0); +x_16 = lean_ctor_get(x_13, 1); +lean_inc(x_16); +lean_inc(x_15); +lean_dec(x_13); +x_17 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_17, 0, x_15); +lean_ctor_set(x_17, 1, x_16); +return x_17; +} +} +else +{ +uint8_t x_18; +x_18 = !lean_is_exclusive(x_13); +if (x_18 == 0) +{ +return x_13; +} +else +{ +lean_object* x_19; lean_object* x_20; lean_object* x_21; +x_19 = lean_ctor_get(x_13, 0); +x_20 = lean_ctor_get(x_13, 1); +lean_inc(x_20); +lean_inc(x_19); +lean_dec(x_13); +x_21 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_21, 0, x_19); +lean_ctor_set(x_21, 1, x_20); +return x_21; +} +} +} +} +lean_object* l_Lean_Meta_getCtorNumPropFields(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_7 = lean_ctor_get(x_1, 0); +lean_inc(x_7); +x_8 = lean_ctor_get(x_7, 2); +lean_inc(x_8); +lean_dec(x_7); +x_9 = lean_alloc_closure((void*)(l_Lean_Meta_getCtorNumPropFields___lambda__1___boxed), 8, 1); +lean_closure_set(x_9, 0, x_1); +x_10 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__4___rarg(x_8, x_9, x_2, x_3, x_4, x_5, x_6); +return x_10; +} +} +lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) { +_start: +{ +lean_object* x_12; +x_12 = l_Std_Range_forIn_loop___at_Lean_Meta_getCtorNumPropFields___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +return x_12; +} +} +lean_object* l_Lean_Meta_getCtorNumPropFields___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l_Lean_Meta_getCtorNumPropFields___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_3); +lean_dec(x_2); +return x_9; +} +} lean_object* l_Lean_Meta_injectionCore_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -551,71 +830,120 @@ lean_inc(x_81); lean_dec(x_80); x_82 = l_Lean_Expr_mvarId_x21(x_77); lean_dec(x_77); +lean_inc(x_8); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); x_83 = l_Lean_Meta_tryClear(x_82, x_1, x_5, x_6, x_7, x_8, x_81); if (lean_obj_tag(x_83) == 0) { -uint8_t x_84; -x_84 = !lean_is_exclusive(x_83); -if (x_84 == 0) +lean_object* x_84; lean_object* x_85; lean_object* x_86; +x_84 = lean_ctor_get(x_83, 0); +lean_inc(x_84); +x_85 = lean_ctor_get(x_83, 1); +lean_inc(x_85); +lean_dec(x_83); +lean_inc(x_43); +x_86 = l_Lean_Meta_getCtorNumPropFields(x_43, x_5, x_6, x_7, x_8, x_85); +if (lean_obj_tag(x_86) == 0) { -lean_object* x_85; lean_object* x_86; lean_object* x_87; -x_85 = lean_ctor_get(x_83, 0); -x_86 = lean_ctor_get(x_43, 4); -lean_inc(x_86); -lean_dec(x_43); -x_87 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_87, 0, x_85); -lean_ctor_set(x_87, 1, x_86); -lean_ctor_set(x_83, 0, x_87); -return x_83; -} -else +uint8_t x_87; +x_87 = !lean_is_exclusive(x_86); +if (x_87 == 0) { -lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; -x_88 = lean_ctor_get(x_83, 0); -x_89 = lean_ctor_get(x_83, 1); +lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; +x_88 = lean_ctor_get(x_86, 0); +x_89 = lean_ctor_get(x_43, 4); lean_inc(x_89); -lean_inc(x_88); -lean_dec(x_83); -x_90 = lean_ctor_get(x_43, 4); -lean_inc(x_90); lean_dec(x_43); +x_90 = lean_nat_sub(x_89, x_88); +lean_dec(x_88); +lean_dec(x_89); x_91 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_91, 0, x_88); +lean_ctor_set(x_91, 0, x_84); lean_ctor_set(x_91, 1, x_90); -x_92 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_92, 0, x_91); -lean_ctor_set(x_92, 1, x_89); -return x_92; +lean_ctor_set(x_86, 0, x_91); +return x_86; +} +else +{ +lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; +x_92 = lean_ctor_get(x_86, 0); +x_93 = lean_ctor_get(x_86, 1); +lean_inc(x_93); +lean_inc(x_92); +lean_dec(x_86); +x_94 = lean_ctor_get(x_43, 4); +lean_inc(x_94); +lean_dec(x_43); +x_95 = lean_nat_sub(x_94, x_92); +lean_dec(x_92); +lean_dec(x_94); +x_96 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_96, 0, x_84); +lean_ctor_set(x_96, 1, x_95); +x_97 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_97, 0, x_96); +lean_ctor_set(x_97, 1, x_93); +return x_97; } } else { -uint8_t x_93; +uint8_t x_98; +lean_dec(x_84); lean_dec(x_43); -x_93 = !lean_is_exclusive(x_83); -if (x_93 == 0) +x_98 = !lean_is_exclusive(x_86); +if (x_98 == 0) +{ +return x_86; +} +else +{ +lean_object* x_99; lean_object* x_100; lean_object* x_101; +x_99 = lean_ctor_get(x_86, 0); +x_100 = lean_ctor_get(x_86, 1); +lean_inc(x_100); +lean_inc(x_99); +lean_dec(x_86); +x_101 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_101, 0, x_99); +lean_ctor_set(x_101, 1, x_100); +return x_101; +} +} +} +else +{ +uint8_t x_102; +lean_dec(x_43); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +x_102 = !lean_is_exclusive(x_83); +if (x_102 == 0) { return x_83; } else { -lean_object* x_94; lean_object* x_95; lean_object* x_96; -x_94 = lean_ctor_get(x_83, 0); -x_95 = lean_ctor_get(x_83, 1); -lean_inc(x_95); -lean_inc(x_94); +lean_object* x_103; lean_object* x_104; lean_object* x_105; +x_103 = lean_ctor_get(x_83, 0); +x_104 = lean_ctor_get(x_83, 1); +lean_inc(x_104); +lean_inc(x_103); lean_dec(x_83); -x_96 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_96, 0, x_94); -lean_ctor_set(x_96, 1, x_95); -return x_96; +x_105 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_105, 0, x_103); +lean_ctor_set(x_105, 1, x_104); +return x_105; } } } else { -uint8_t x_97; +uint8_t x_106; lean_dec(x_72); lean_dec(x_51); lean_dec(x_43); @@ -625,49 +953,49 @@ lean_dec(x_6); lean_dec(x_5); lean_dec(x_3); lean_dec(x_1); -x_97 = !lean_is_exclusive(x_73); -if (x_97 == 0) +x_106 = !lean_is_exclusive(x_73); +if (x_106 == 0) { return x_73; } else { -lean_object* x_98; lean_object* x_99; lean_object* x_100; -x_98 = lean_ctor_get(x_73, 0); -x_99 = lean_ctor_get(x_73, 1); -lean_inc(x_99); -lean_inc(x_98); +lean_object* x_107; lean_object* x_108; lean_object* x_109; +x_107 = lean_ctor_get(x_73, 0); +x_108 = lean_ctor_get(x_73, 1); +lean_inc(x_108); +lean_inc(x_107); lean_dec(x_73); -x_100 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_100, 0, x_98); -lean_ctor_set(x_100, 1, x_99); -return x_100; +x_109 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_109, 0, x_107); +lean_ctor_set(x_109, 1, x_108); +return x_109; } } } else { -lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; +lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_dec(x_69); lean_dec(x_51); lean_dec(x_43); lean_dec(x_1); -x_101 = lean_ctor_get(x_68, 1); -lean_inc(x_101); +x_110 = lean_ctor_get(x_68, 1); +lean_inc(x_110); lean_dec(x_68); -x_102 = l_Lean_Meta_injectionCore___lambda__1___closed__6; -x_103 = lean_box(0); -x_104 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_102, x_103, x_5, x_6, x_7, x_8, x_101); +x_111 = l_Lean_Meta_injectionCore___lambda__1___closed__6; +x_112 = lean_box(0); +x_113 = l_Lean_Meta_throwTacticEx___rarg(x_2, x_3, x_111, x_112, x_5, x_6, x_7, x_8, x_110); lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); lean_dec(x_5); -return x_104; +return x_113; } } else { -uint8_t x_105; +uint8_t x_114; lean_dec(x_51); lean_dec(x_43); lean_dec(x_8); @@ -677,29 +1005,29 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_105 = !lean_is_exclusive(x_68); -if (x_105 == 0) +x_114 = !lean_is_exclusive(x_68); +if (x_114 == 0) { return x_68; } else { -lean_object* x_106; lean_object* x_107; lean_object* x_108; -x_106 = lean_ctor_get(x_68, 0); -x_107 = lean_ctor_get(x_68, 1); -lean_inc(x_107); -lean_inc(x_106); +lean_object* x_115; lean_object* x_116; lean_object* x_117; +x_115 = lean_ctor_get(x_68, 0); +x_116 = lean_ctor_get(x_68, 1); +lean_inc(x_116); +lean_inc(x_115); lean_dec(x_68); -x_108 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_108, 0, x_106); -lean_ctor_set(x_108, 1, x_107); -return x_108; +x_117 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_117, 0, x_115); +lean_ctor_set(x_117, 1, x_116); +return x_117; } } } else { -uint8_t x_109; +uint8_t x_118; lean_dec(x_51); lean_dec(x_43); lean_dec(x_8); @@ -709,30 +1037,30 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_109 = !lean_is_exclusive(x_65); -if (x_109 == 0) +x_118 = !lean_is_exclusive(x_65); +if (x_118 == 0) { return x_65; } else { -lean_object* x_110; lean_object* x_111; lean_object* x_112; -x_110 = lean_ctor_get(x_65, 0); -x_111 = lean_ctor_get(x_65, 1); -lean_inc(x_111); -lean_inc(x_110); +lean_object* x_119; lean_object* x_120; lean_object* x_121; +x_119 = lean_ctor_get(x_65, 0); +x_120 = lean_ctor_get(x_65, 1); +lean_inc(x_120); +lean_inc(x_119); lean_dec(x_65); -x_112 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_112, 0, x_110); -lean_ctor_set(x_112, 1, x_111); -return x_112; +x_121 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_121, 0, x_119); +lean_ctor_set(x_121, 1, x_120); +return x_121; } } } } else { -uint8_t x_113; +uint8_t x_122; lean_dec(x_48); lean_dec(x_43); lean_dec(x_8); @@ -742,23 +1070,23 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_113 = !lean_is_exclusive(x_50); -if (x_113 == 0) +x_122 = !lean_is_exclusive(x_50); +if (x_122 == 0) { return x_50; } else { -lean_object* x_114; lean_object* x_115; lean_object* x_116; -x_114 = lean_ctor_get(x_50, 0); -x_115 = lean_ctor_get(x_50, 1); -lean_inc(x_115); -lean_inc(x_114); +lean_object* x_123; lean_object* x_124; lean_object* x_125; +x_123 = lean_ctor_get(x_50, 0); +x_124 = lean_ctor_get(x_50, 1); +lean_inc(x_124); +lean_inc(x_123); lean_dec(x_50); -x_116 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_116, 0, x_114); -lean_ctor_set(x_116, 1, x_115); -return x_116; +x_125 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_125, 0, x_123); +lean_ctor_set(x_125, 1, x_124); +return x_125; } } } @@ -766,7 +1094,7 @@ return x_116; } else { -uint8_t x_117; +uint8_t x_126; lean_dec(x_30); lean_dec(x_27); lean_dec(x_8); @@ -776,29 +1104,29 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_117 = !lean_is_exclusive(x_32); -if (x_117 == 0) +x_126 = !lean_is_exclusive(x_32); +if (x_126 == 0) { return x_32; } else { -lean_object* x_118; lean_object* x_119; lean_object* x_120; -x_118 = lean_ctor_get(x_32, 0); -x_119 = lean_ctor_get(x_32, 1); -lean_inc(x_119); -lean_inc(x_118); +lean_object* x_127; lean_object* x_128; lean_object* x_129; +x_127 = lean_ctor_get(x_32, 0); +x_128 = lean_ctor_get(x_32, 1); +lean_inc(x_128); +lean_inc(x_127); lean_dec(x_32); -x_120 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_120, 0, x_118); -lean_ctor_set(x_120, 1, x_119); -return x_120; +x_129 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_129, 0, x_127); +lean_ctor_set(x_129, 1, x_128); +return x_129; } } } else { -uint8_t x_121; +uint8_t x_130; lean_dec(x_27); lean_dec(x_8); lean_dec(x_7); @@ -807,29 +1135,29 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_121 = !lean_is_exclusive(x_29); -if (x_121 == 0) +x_130 = !lean_is_exclusive(x_29); +if (x_130 == 0) { return x_29; } else { -lean_object* x_122; lean_object* x_123; lean_object* x_124; -x_122 = lean_ctor_get(x_29, 0); -x_123 = lean_ctor_get(x_29, 1); -lean_inc(x_123); -lean_inc(x_122); +lean_object* x_131; lean_object* x_132; lean_object* x_133; +x_131 = lean_ctor_get(x_29, 0); +x_132 = lean_ctor_get(x_29, 1); +lean_inc(x_132); +lean_inc(x_131); lean_dec(x_29); -x_124 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_124, 0, x_122); -lean_ctor_set(x_124, 1, x_123); -return x_124; +x_133 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_133, 0, x_131); +lean_ctor_set(x_133, 1, x_132); +return x_133; } } } else { -uint8_t x_125; +uint8_t x_134; lean_dec(x_25); lean_dec(x_8); lean_dec(x_7); @@ -838,30 +1166,30 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_125 = !lean_is_exclusive(x_26); -if (x_125 == 0) +x_134 = !lean_is_exclusive(x_26); +if (x_134 == 0) { return x_26; } else { -lean_object* x_126; lean_object* x_127; lean_object* x_128; -x_126 = lean_ctor_get(x_26, 0); -x_127 = lean_ctor_get(x_26, 1); -lean_inc(x_127); -lean_inc(x_126); +lean_object* x_135; lean_object* x_136; lean_object* x_137; +x_135 = lean_ctor_get(x_26, 0); +x_136 = lean_ctor_get(x_26, 1); +lean_inc(x_136); +lean_inc(x_135); lean_dec(x_26); -x_128 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_128, 0, x_126); -lean_ctor_set(x_128, 1, x_127); -return x_128; +x_137 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_137, 0, x_135); +lean_ctor_set(x_137, 1, x_136); +return x_137; } } } } else { -uint8_t x_129; +uint8_t x_138; lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); @@ -869,29 +1197,29 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_129 = !lean_is_exclusive(x_14); -if (x_129 == 0) +x_138 = !lean_is_exclusive(x_14); +if (x_138 == 0) { return x_14; } else { -lean_object* x_130; lean_object* x_131; lean_object* x_132; -x_130 = lean_ctor_get(x_14, 0); -x_131 = lean_ctor_get(x_14, 1); -lean_inc(x_131); -lean_inc(x_130); +lean_object* x_139; lean_object* x_140; lean_object* x_141; +x_139 = lean_ctor_get(x_14, 0); +x_140 = lean_ctor_get(x_14, 1); +lean_inc(x_140); +lean_inc(x_139); lean_dec(x_14); -x_132 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_132, 0, x_130); -lean_ctor_set(x_132, 1, x_131); -return x_132; +x_141 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_141, 0, x_139); +lean_ctor_set(x_141, 1, x_140); +return x_141; } } } else { -uint8_t x_133; +uint8_t x_142; lean_dec(x_8); lean_dec(x_7); lean_dec(x_6); @@ -899,23 +1227,23 @@ lean_dec(x_5); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_133 = !lean_is_exclusive(x_10); -if (x_133 == 0) +x_142 = !lean_is_exclusive(x_10); +if (x_142 == 0) { return x_10; } else { -lean_object* x_134; lean_object* x_135; lean_object* x_136; -x_134 = lean_ctor_get(x_10, 0); -x_135 = lean_ctor_get(x_10, 1); -lean_inc(x_135); -lean_inc(x_134); +lean_object* x_143; lean_object* x_144; lean_object* x_145; +x_143 = lean_ctor_get(x_10, 0); +x_144 = lean_ctor_get(x_10, 1); +lean_inc(x_144); +lean_inc(x_143); lean_dec(x_10); -x_136 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_136, 0, x_134); -lean_ctor_set(x_136, 1, x_135); -return x_136; +x_145 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_145, 0, x_143); +lean_ctor_set(x_145, 1, x_144); +return x_145; } } } diff --git a/stage0/stdlib/Lean/ParserCompiler/Attribute.c b/stage0/stdlib/Lean/ParserCompiler/Attribute.c index 2cf6e488d0..f047192964 100644 --- a/stage0/stdlib/Lean/ParserCompiler/Attribute.c +++ b/stage0/stdlib/Lean/ParserCompiler/Attribute.c @@ -64,9 +64,9 @@ lean_object* lean_eval_const(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_persistentEnvExtensionsRef; lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(lean_object*, lean_object*); lean_object* l_Lean_registerBuiltinAttribute(lean_object*, lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; extern lean_object* l_Lean_KernelException_toMessageData___closed__3; size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_SimplePersistentEnvExtension_getState___rarg(lean_object*, lean_object*); lean_object* l_Lean_ofExcept___at_Lean_ParserCompiler_CombinatorAttribute_runDeclFor___spec__3(lean_object*); @@ -642,7 +642,7 @@ _start: lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_4 = l_Lean_mkMapDeclarationExtension___rarg___closed__1; x_5 = l_Lean_ParserCompiler_registerCombinatorAttribute___closed__1; -x_6 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_6 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; lean_inc(x_1); x_7 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_7, 0, x_1); diff --git a/stage0/stdlib/Lean/ResolveName.c b/stage0/stdlib/Lean/ResolveName.c index f2b8d5dd10..f81feed584 100644 --- a/stage0/stdlib/Lean/ResolveName.c +++ b/stage0/stdlib/Lean/ResolveName.c @@ -186,8 +186,8 @@ lean_object* l_Lean_ResolveName_resolveGlobalName_loop_match__2___rarg(lean_obje lean_object* l_Lean_getAliases(lean_object*, lean_object*); lean_object* l_Lean_ResolveName_resolveNamespace_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_getRevAliases___spec__12___rarg(lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; size_t lean_usize_of_nat(lean_object*); -extern lean_object* l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; lean_object* l_Lean_initFn____x40_Lean_ResolveName___hyg_53____closed__3; lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_getRevAliases___spec__8___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); @@ -2062,7 +2062,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj x_1 = l_Lean_initFn____x40_Lean_ResolveName___hyg_53____closed__2; x_2 = l_Lean_initFn____x40_Lean_ResolveName___hyg_53____closed__3; x_3 = l_Lean_initFn____x40_Lean_ResolveName___hyg_53____closed__4; -x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2913____closed__4; +x_4 = l_Lean_initFn____x40_Lean_Environment___hyg_2909____closed__4; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); diff --git a/stage0/stdlib/Lean/Util/Profile.c b/stage0/stdlib/Lean/Util/Profile.c index 0e32532311..99731bf617 100644 --- a/stage0/stdlib/Lean/Util/Profile.c +++ b/stage0/stdlib/Lean/Util/Profile.c @@ -14,30 +14,29 @@ extern "C" { #endif lean_object* l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed(lean_object*, lean_object*); -lean_object* l_Lean_profileitM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* lean_profileit(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitIOUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitIO(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_profileit(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIOUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIO(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_profileitIOUnsafe___rarg___lambda__1(lean_object*, lean_object*); lean_object* l_Lean_profileitM(lean_object*, lean_object*); lean_object* l_Lean_profileitIOUnsafe_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitIO___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitIO___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_profileitIOUnsafe(lean_object*, lean_object*); -lean_object* l_Lean_profileit___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileit___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_profileitIO___rarg(lean_object*, lean_object*); lean_object* l_Lean_profileitIOUnsafe_match__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileitM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_profileit___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileitM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_profileit___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_6; -x_6 = lean_profileit(x_2, x_3, x_4, x_5); -lean_dec(x_4); +lean_object* x_5; +x_5 = lean_profileit(x_2, x_3, x_4); lean_dec(x_3); lean_dec(x_2); -return x_6; +return x_5; } } lean_object* l_Lean_profileitIOUnsafe_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { @@ -101,34 +100,34 @@ return x_8; } } } -lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_profileitIOUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_6; lean_object* x_7; -x_6 = lean_alloc_closure((void*)(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed), 2, 1); -lean_closure_set(x_6, 0, x_4); -x_7 = lean_profileit(x_1, x_2, x_3, x_6); -if (lean_obj_tag(x_7) == 0) +lean_object* x_5; lean_object* x_6; +x_5 = lean_alloc_closure((void*)(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed), 2, 1); +lean_closure_set(x_5, 0, x_3); +x_6 = lean_profileit(x_1, x_2, x_5); +if (lean_obj_tag(x_6) == 0) { -lean_object* x_8; lean_object* x_9; -x_8 = lean_ctor_get(x_7, 0); -lean_inc(x_8); -lean_dec(x_7); -x_9 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_9, 0, x_8); -lean_ctor_set(x_9, 1, x_5); -return x_9; +lean_object* x_7; lean_object* x_8; +x_7 = lean_ctor_get(x_6, 0); +lean_inc(x_7); +lean_dec(x_6); +x_8 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_8, 0, x_7); +lean_ctor_set(x_8, 1, x_4); +return x_8; } else { -lean_object* x_10; lean_object* x_11; -x_10 = lean_ctor_get(x_7, 0); -lean_inc(x_10); -lean_dec(x_7); -x_11 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_11, 0, x_10); -lean_ctor_set(x_11, 1, x_5); -return x_11; +lean_object* x_9; lean_object* x_10; +x_9 = lean_ctor_get(x_6, 0); +lean_inc(x_9); +lean_dec(x_6); +x_10 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_10, 0, x_9); +lean_ctor_set(x_10, 1, x_4); +return x_10; } } } @@ -136,7 +135,7 @@ lean_object* l_Lean_profileitIOUnsafe(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_Lean_profileitIOUnsafe___rarg___boxed), 5, 0); +x_3 = lean_alloc_closure((void*)(l_Lean_profileitIOUnsafe___rarg___boxed), 4, 0); return x_3; } } @@ -149,15 +148,14 @@ lean_dec(x_2); return x_3; } } -lean_object* l_Lean_profileitIOUnsafe___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_profileitIOUnsafe___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_6; -x_6 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_3, x_4, x_5); -lean_dec(x_3); +lean_object* x_5; +x_5 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_3, x_4); lean_dec(x_2); lean_dec(x_1); -return x_6; +return x_5; } } lean_object* l_Lean_profileitIO___rarg(lean_object* x_1, lean_object* x_2) { @@ -168,62 +166,59 @@ x_3 = lean_apply_1(x_1, x_2); return x_3; } } -lean_object* l_Lean_profileitIO(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_profileitIO(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_6; -x_6 = lean_alloc_closure((void*)(l_Lean_profileitIO___rarg), 2, 0); -return x_6; +lean_object* x_5; +x_5 = lean_alloc_closure((void*)(l_Lean_profileitIO___rarg), 2, 0); +return x_5; } } -lean_object* l_Lean_profileitIO___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_profileitIO___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_6; -x_6 = l_Lean_profileitIO(x_1, x_2, x_3, x_4, x_5); -lean_dec(x_5); +lean_object* x_5; +x_5 = l_Lean_profileitIO(x_1, x_2, x_3, x_4); lean_dec(x_4); lean_dec(x_3); +return x_5; +} +} +lean_object* l_Lean_profileitM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_4, x_5); return x_6; } } -lean_object* l_Lean_profileitM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +lean_object* l_Lean_profileitM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { -lean_object* x_7; -x_7 = l_Lean_profileitIOUnsafe___rarg(x_1, x_2, x_3, x_5, x_6); +lean_object* x_6; lean_object* x_7; +x_6 = lean_alloc_closure((void*)(l_Lean_profileitM___rarg___lambda__1___boxed), 5, 2); +lean_closure_set(x_6, 0, x_3); +lean_closure_set(x_6, 1, x_4); +x_7 = lean_apply_3(x_1, lean_box(0), x_6, x_5); return x_7; } } -lean_object* l_Lean_profileitM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { -_start: -{ -lean_object* x_7; lean_object* x_8; -x_7 = lean_alloc_closure((void*)(l_Lean_profileitM___rarg___lambda__1___boxed), 6, 3); -lean_closure_set(x_7, 0, x_3); -lean_closure_set(x_7, 1, x_4); -lean_closure_set(x_7, 2, x_5); -x_8 = lean_apply_3(x_1, lean_box(0), x_7, x_6); -return x_8; -} -} lean_object* l_Lean_profileitM(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_Lean_profileitM___rarg), 6, 0); +x_3 = lean_alloc_closure((void*)(l_Lean_profileitM___rarg), 5, 0); return x_3; } } -lean_object* l_Lean_profileitM___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +lean_object* l_Lean_profileitM___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { -lean_object* x_7; -x_7 = l_Lean_profileitM___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6); -lean_dec(x_3); +lean_object* x_6; +x_6 = l_Lean_profileitM___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5); lean_dec(x_2); lean_dec(x_1); -return x_7; +return x_6; } } lean_object* initialize_Init(lean_object*);