max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-31 08:25:16 -08:00
parent 3fa1f355eb
commit e47485a9d1
25 changed files with 1063 additions and 721 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Lean/Elab/Frontend.lean generated
View file

@ -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

2
stage0/src/Lean/Environment.lean generated
View file

@ -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

2
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -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

12
stage0/src/Lean/Meta/Tactic/Injection.lean generated
View file

@ -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"

12
stage0/src/Lean/Util/Profile.lean generated
View file

@ -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

1
stage0/src/bin/leanc.in generated
View file

@ -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

2
stage0/src/include/lean/lean.h generated
View file

@ -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 {

10
stage0/src/library/time_task.cpp generated
View file

@ -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<xtimeit>(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));
}
}

2
stage0/src/library/time_task.h generated
View file

@ -20,7 +20,7 @@ class time_task {
optional<xtimeit> 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();
};

92
stage0/src/runtime/alloc.cpp generated
View file

@ -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;
}

2
stage0/src/runtime/object.cpp generated
View file

@ -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));

4
stage0/stdlib/Lean/Class.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Compiler/ClosedTermCache.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Compiler/Specialize.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -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;
}
}

669
stage0/stdlib/Lean/Elab/Frontend.c generated
View file

@ -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));

102
stage0/stdlib/Lean/Environment.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Meta/Instances.c generated
View file

@ -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);

4
stage0/stdlib/Lean/Meta/Match/MatcherInfo.c generated
View file

@ -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);

63
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

@ -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));

636
stage0/stdlib/Lean/Meta/Tactic/Injection.c generated
View file

@ -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;
}
}
}

4
stage0/stdlib/Lean/ParserCompiler/Attribute.c generated
View file

@ -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);

4
stage0/stdlib/Lean/ResolveName.c generated
View file

@ -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);

137
stage0/stdlib/Lean/Util/Profile.c generated
View file

@ -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*);