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:
Lean stage0 autoupdater 2024-08-05 17:53:40 +00:00
parent 8e476e9d22
commit d671d0d61a
13 changed files with 11941 additions and 12069 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
stage0/src/kernel/instantiate.cpp generated
View file

@ -165,22 +165,38 @@ bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(get_app_fn(t));
}
expr apply_beta(expr f, unsigned num_args, expr const * args) {
if (num_args == 0) {
return f;
} else if (!is_lambda(f)) {
return mk_rev_app(f, num_args, args);
} else {
unsigned m = 1;
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
static expr apply_beta_rec(expr e, unsigned i, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
if (is_lambda(e)) {
if (i + 1 < num_rev_args) {
return apply_beta_rec(binding_body(e), i+1, num_rev_args, rev_args, preserve_data, zeta);
} else {
return instantiate(binding_body(e), num_rev_args, rev_args);
}
lean_assert(m <= num_args);
return mk_rev_app(instantiate(binding_body(f), m, args + (num_args - m)), num_args - m, args);
} else if (is_let(e)) {
if (zeta && i < num_rev_args) {
return apply_beta_rec(instantiate(let_body(e), let_value(e)), i, num_rev_args, rev_args, preserve_data, zeta);
} else {
unsigned n = num_rev_args - i;
return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
}
} else if (is_mdata(e)) {
if (preserve_data) {
unsigned n = num_rev_args - i;
return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
} else {
return apply_beta_rec(mdata_expr(e), i, num_rev_args, rev_args, preserve_data, zeta);
}
} else {
unsigned n = num_rev_args - i;
return mk_rev_app(instantiate(e, i, rev_args + n), n, rev_args);
}
}
expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data, bool zeta) {
if (num_rev_args == 0) return f;
return apply_beta_rec(f, 0, num_rev_args, rev_args, preserve_data, zeta);
}
expr head_beta_reduce(expr const & t) {
if (!is_head_beta(t)) {
return t;

2
stage0/src/kernel/instantiate.h generated
View file

@ -24,7 +24,7 @@ inline expr instantiate_rev(expr const & e, buffer<expr> const & s) {
return instantiate_rev(e, s.size(), s.data());
}
expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args);
expr apply_beta(expr f, unsigned num_rev_args, expr const * rev_args, bool preserve_data = true, bool zeta = false);
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t);
/* If `e` is of the form `(fun x, t) a` return `head_beta_const_fn(t)` if `t` does not depend on `x`,

291
stage0/src/kernel/instantiate_mvars.cpp generated
View file

@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
*/
#include <vector>
#include <unordered_map>
#include "util/name_set.h"
#include "runtime/option_ref.h"
#include "runtime/array_ref.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/replace_fn.h"
/*
This module is not used by the kernel. It just provides an efficient implementation of
@ -15,7 +18,6 @@ This module is not used by the kernel. It just provides an efficient implementat
*/
namespace lean {
extern "C" object * lean_get_lmvar_assignment(obj_arg mctx, obj_arg mid);
extern "C" object * lean_assign_lmvar(obj_arg mctx, obj_arg mid, obj_arg val);
@ -29,18 +31,19 @@ option_ref<level> get_lmvar_assignment(metavar_ctx & mctx, name const & mid) {
return option_ref<level>(lean_get_lmvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
}
class instantiate_lmvar_fn {
class instantiate_lmvars_fn {
metavar_ctx & m_mctx;
std::unordered_map<lean_object *, lean_object *> m_cache;
std::unordered_map<lean_object *, level> m_cache;
std::vector<level> m_saved; // Helper vector to prevent values from being garbagge collected
inline level cache(level const & l, level && r, bool shared) {
inline level cache(level const & l, level r, bool shared) {
if (shared) {
m_cache.insert(mk_pair(l.raw(), r.raw()));
m_cache.insert(mk_pair(l.raw(), r));
}
return r;
}
public:
instantiate_lmvar_fn(metavar_ctx & mctx):m_mctx(mctx) {}
instantiate_lmvars_fn(metavar_ctx & mctx):m_mctx(mctx) {}
level visit(level const & l) {
if (!has_mvar(l))
return l;
@ -48,7 +51,7 @@ public:
if (is_shared(l)) {
auto it = m_cache.find(l.raw());
if (it != m_cache.end()) {
return level(it->second, true);
return it->second;
}
shared = true;
}
@ -70,6 +73,12 @@ public:
} else {
level a_new = visit(a);
if (!is_eqp(a, a_new)) {
/*
We save `a` to ensure it will not be garbage collected
after we update `mctx`. This is necessary because `m_cache`
may contain references to its subterms.
*/
m_saved.push_back(a);
assign_lmvar(m_mctx, mvar_id(l), a_new);
}
return a_new;
@ -82,14 +91,274 @@ public:
extern "C" LEAN_EXPORT object * lean_instantiate_level_mvars(object * m, object * l) {
metavar_ctx mctx(m);
level l_new = instantiate_lmvar_fn(mctx)(level(l));
level l_new = instantiate_lmvars_fn(mctx)(level(l));
object * r = alloc_cnstr(0, 2, 0);
cnstr_set(r, 0, mctx.steal());
cnstr_set(r, 1, l_new.steal());
return r;
}
extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object *, object *) {
lean_internal_panic("not implemented yet");
extern "C" object * lean_get_mvar_assignment(obj_arg mctx, obj_arg mid);
extern "C" object * lean_get_delayed_mvar_assignment(obj_arg mctx, obj_arg mid);
extern "C" object * lean_assign_mvar(obj_arg mctx, obj_arg mid, obj_arg val);
typedef object_ref delayed_assignment;
void assign_mvar(metavar_ctx & mctx, name const & mid, expr const & e) {
object * r = lean_assign_mvar(mctx.steal(), mid.to_obj_arg(), e.to_obj_arg());
mctx.set_box(r);
}
option_ref<expr> get_mvar_assignment(metavar_ctx & mctx, name const & mid) {
return option_ref<expr>(lean_get_mvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
}
option_ref<delayed_assignment> get_delayed_mvar_assignment(metavar_ctx & mctx, name const & mid) {
return option_ref<delayed_assignment>(lean_get_delayed_mvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
}
expr replace_fvars(expr const & e, array_ref<expr> const & fvars, expr const * rev_args) {
size_t sz = fvars.size();
if (sz == 0)
return e;
return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
if (!has_fvar(m))
return some_expr(m); // expression m does not contain free variables
if (is_fvar(m)) {
size_t i = sz;
name const & fid = fvar_name(m);
while (i > 0) {
--i;
if (fvar_name(fvars[i]) == fid) {
return some_expr(lift_loose_bvars(rev_args[sz - i - 1], offset));
}
}
}
return none_expr();
});
}
class instantiate_mvars_fn {
metavar_ctx & m_mctx;
instantiate_lmvars_fn m_level_fn;
name_set m_already_normalized; // Store metavariables whose assignment has already been normalized.
std::unordered_map<lean_object *, expr> m_cache;
std::vector<expr> m_saved; // Helper vector to prevent values from being garbagge collected
level visit_level(level const & l) {
return m_level_fn(l);
}
levels visit_levels(levels const & ls) {
buffer<level> lsNew;
for (auto const & l : ls)
lsNew.push_back(visit_level(l));
return levels(lsNew);
}
inline expr cache(expr const & e, expr r, bool shared) {
if (shared) {
m_cache.insert(mk_pair(e.raw(), r));
}
return r;
}
optional<expr> get_assignment(name const & mid) {
option_ref<expr> r = get_mvar_assignment(m_mctx, mid);
if (!r) {
return optional<expr>();
} else {
expr a(r.get_val());
if (!has_mvar(a) || m_already_normalized.contains(mid)) {
return optional<expr>(a);
} else {
m_already_normalized.insert(mid);
expr a_new = visit(a);
if (!is_eqp(a, a_new)) {
/*
We save `a` to ensure it will not be garbage collected
after we update `mctx`. This is necessary because `m_cache`
may contain references to its subterms.
*/
m_saved.push_back(a);
assign_mvar(m_mctx, mid, a_new);
}
return optional<expr>(a_new);
}
}
}
/*
Given `e` of the form `f a_1 ... a_n` where `f` is not a metavariable,
instantiate metavariables.
*/
expr visit_app_default(expr const & e) {
if (is_app(e)) {
return update_app(e, visit_app_default(app_fn(e)), visit(app_arg(e)));
} else {
lean_assert(!is_mvar(e));
return visit(e);
}
}
/*
Given `e` of the form `?m a_1 ... a_n`, return new application where
the metavariables in the arguments `a_i` have been instantiated.
*/
expr visit_mvar_app_args(expr const & e) {
if (is_app(e)) {
return update_app(e, visit_app_default(app_fn(e)), visit(app_arg(e)));
} else {
lean_assert(is_mvar(e));
return e;
}
}
/*
Given `e` of the form `f a_1 ... a_n`, return new application `f_new a_1' ... a_n'`
where `a_i'` is `visit(a_i)`. `args` is an accumulator for the new arguments.
*/
expr visit_args_and_beta(expr const & f_new, expr const & e, buffer<expr> & args) {
if (is_app(e)) {
args.push_back(visit(app_arg(e)));
return visit_args_and_beta(f_new, app_fn(e), args);
} else {
/*
Some of the arguments in `args` are irrelevant after we beta
reduce. Also, it may be a bug to not instantiate them, since they
may depend on free variables that are not in the context (see
issue #4375). So we pass `useZeta := true` to ensure that they are
instantiated.
*/
bool preserve_data = false;
bool zeta = true;
return apply_beta(f_new, args.size(), args.data(), preserve_data, zeta);
}
}
/*
Helper function for delayed assignment case at `visit_app`.
`e` is a term of the form `?m t1 t2 t3`
Moreover, `?m` is delayed assigned
`?m #[x, y] := g x y`
where, `fvars := #[x, y]` and `val := g x y`.
`args` is an accumulator for `e`'s arguments.
We want to return `g t1' t2' t3'` where
`ti'`s are `visit(ti)`.
*/
expr visit_delayed(array_ref<expr> const & fvars, expr const & val, expr const & e, buffer<expr> & args) {
if (is_app(e)) {
args.push_back(visit(app_arg(e)));
return visit_delayed(fvars, val, app_fn(e), args);
} else {
expr val_new = replace_fvars(val, fvars, args.data() + (args.size() - fvars.size()));
return mk_rev_app(val_new, args.size() - fvars.size(), args.data());
}
}
expr visit_app(expr const & e) {
expr const & f = get_app_fn(e);
if (!is_mvar(f)) {
return visit_app_default(e);
} else {
name const & mid = mvar_name(f);
option_ref<delayed_assignment> d = get_delayed_mvar_assignment(m_mctx, mid);
if (!d) {
// mvar is not delayed assigned
expr f_new = visit(f);
if (is_eqp(f, f_new)) {
return visit_mvar_app_args(e);
} else {
buffer<expr> args;
return visit_args_and_beta(f_new, e, args);
}
} else {
/*
Apply "delayed substitution" (i.e., delayed assignment + application).
That is, `f` is some metavariable `?m`, that is delayed assigned to `val`.
If after instantiating `val`, we obtain `newVal`, and `newVal` does not contain
metavariables, we replace the free variables `fvars` in `newVal` with the first
`fvars.size` elements of `args`.
*/
array_ref<expr> fvars(cnstr_get(d.get_val().raw(), 0), true);
name mid_pending(cnstr_get(d.get_val().raw(), 1), true);
if (fvars.size() > get_app_num_args(e)) {
/*
We don't have sufficient arguments for instantiating the free variables `fvars`.
This can only happen if a tactic or elaboration function is not implemented correctly.
We decided to not use `panic!` here and report it as an error in the frontend
when we are checking for unassigned metavariables in an elaborated term. */
return visit_mvar_app_args(e);
}
optional<expr> val = get_assignment(mid_pending);
if (!val)
// mid_pending has not been assigned yet.
return visit_mvar_app_args(e);
if (has_expr_mvar(*val))
// mid_pending has been assigned, but assignment contains mvars.
return visit_mvar_app_args(e);
buffer<expr> args;
return visit_delayed(fvars, *val, e, args);
}
}
}
expr visit_mvar(expr const & e) {
name const & mid = mvar_name(e);
if (auto r = get_assignment(mid)) {
return *r;
} else {
return e;
}
}
public:
instantiate_mvars_fn(metavar_ctx & mctx):m_mctx(mctx), m_level_fn(mctx) {}
expr visit(expr const & e) {
if (!has_mvar(e))
return e;
bool shared = false;
if (is_shared(e)) {
auto it = m_cache.find(e.raw());
if (it != m_cache.end()) {
return it->second;
}
shared = true;
}
switch (e.kind()) {
case expr_kind::BVar:
case expr_kind::Lit: case expr_kind::FVar:
lean_unreachable();
case expr_kind::Sort:
return cache(e, update_sort(e, visit_level(sort_level(e))), shared);
case expr_kind::Const:
return cache(e, update_const(e, visit_levels(const_levels(e))), shared);
case expr_kind::MVar:
return visit_mvar(e);
case expr_kind::MData:
return cache(e, update_mdata(e, visit(mdata_expr(e))), shared);
case expr_kind::Proj:
return cache(e, update_proj(e, visit(proj_expr(e))), shared);
case expr_kind::App:
return cache(e, visit_app(e), shared);
case expr_kind::Pi: case expr_kind::Lambda:
return cache(e, update_binding(e, visit(binding_domain(e)), visit(binding_body(e))), shared);
case expr_kind::Let:
return cache(e, update_let(e, visit(let_type(e)), visit(let_value(e)), visit(let_body(e))), shared);
}
}
expr operator()(expr const & e) { return visit(e); }
};
extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object * m, object * e) {
metavar_ctx mctx(m);
expr e_new = instantiate_mvars_fn(mctx)(expr(e));
object * r = alloc_cnstr(0, 2, 0);
cnstr_set(r, 0, mctx.steal());
cnstr_set(r, 1, e_new.steal());
return r;
}
}

3
stage0/src/runtime/thread.cpp generated
View file

@ -9,6 +9,9 @@ Author: Leonardo de Moura
#include <iostream>
#ifdef LEAN_WINDOWS
#include <windows.h>
# ifdef LEAN_AUTO_THREAD_FINALIZATION
#include <pthread.h>
# endif
#else
#include <pthread.h>
#endif

67
stage0/src/util/shell.cpp generated
View file

@ -191,43 +191,44 @@ static void display_features(std::ostream & out) {
static void display_help(std::ostream & out) {
display_header(out);
std::cout << "Miscellaneous:\n";
std::cout << " --help -h display this message\n";
std::cout << " --features -f display features compiler provides (eg. LLVM support)\n";
std::cout << " --version -v display version number\n";
std::cout << " --githash display the git commit hash number used to build this binary\n";
std::cout << " --run call the 'main' definition in a file with the remaining arguments\n";
std::cout << " --o=oname -o create olean file\n";
std::cout << " --i=iname -i create ilean file\n";
std::cout << " --c=fname -c name of the C output file\n";
std::cout << " --bc=fname -b name of the LLVM bitcode file\n";
std::cout << " --stdin take input from stdin\n";
std::cout << " --root=dir set package root directory from which the module name of the input file is calculated\n"
<< " (default: current working directory)\n";
std::cout << " --trust=num -t trust level (default: max) 0 means do not trust any macro,\n"
<< " and type check all imported modules\n";
std::cout << " --quiet -q do not print verbose messages\n";
std::cout << " --memory=num -M maximum amount of memory that should be used by Lean\n";
std::cout << " (in megabytes)\n";
std::cout << " --timeout=num -T maximum number of memory allocations per task\n";
std::cout << " this is a deterministic way of interrupting long running tasks\n";
std::cout << " -h, --help display this message\n";
std::cout << " -f, --features display features compiler provides (eg. LLVM support)\n";
std::cout << " -v, --version display version number\n";
std::cout << " --githash display the git commit hash number used to build this binary\n";
std::cout << " --run call the 'main' definition in a file with the remaining arguments\n";
std::cout << " -o, --o=oname create olean file\n";
std::cout << " -i, --i=iname create ilean file\n";
std::cout << " -c, --c=fname name of the C output file\n";
std::cout << " -b, --bc=fname name of the LLVM bitcode file\n";
std::cout << " --stdin take input from stdin\n";
std::cout << " --root=dir set package root directory from which the module name\n"
<< " of the input file is calculated\n"
<< " (default: current working directory)\n";
std::cout << " -t, --trust=num trust level (default: max) 0 means do not trust any macro,\n"
<< " and type check all imported modules\n";
std::cout << " -q, --quiet do not print verbose messages\n";
std::cout << " -M, --memory=num maximum amount of memory that should be used by Lean\n";
std::cout << " (in megabytes)\n";
std::cout << " -T, --timeout=num maximum number of memory allocations per task\n";
std::cout << " this is a deterministic way of interrupting long running tasks\n";
#if defined(LEAN_MULTI_THREAD)
std::cout << " --threads=num -j number of threads used to process lean files\n";
std::cout << " --tstack=num -s thread stack size in Kb\n";
std::cout << " --server start lean in server mode\n";
std::cout << " --worker start lean in server-worker mode\n";
std::cout << " -j, --threads=num number of threads used to process lean files\n";
std::cout << " -s, --tstack=num thread stack size in Kb\n";
std::cout << " --server start lean in server mode\n";
std::cout << " --worker start lean in server-worker mode\n";
#endif
std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n";
std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n";
std::cout << " --deps just print dependencies of a Lean input\n";
std::cout << " --print-prefix print the installation prefix for Lean and exit\n";
std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n";
std::cout << " --profile display elaboration/type checking time for each definition/theorem\n";
std::cout << " --stats display environment statistics\n";
std::cout << " --plugin=file load and initialize Lean shared library for registering linters etc.\n";
std::cout << " --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
std::cout << " --json report Lean output (e.g., messages) as JSON (one per line)\n";
std::cout << " --deps just print dependencies of a Lean input\n";
std::cout << " --print-prefix print the installation prefix for Lean and exit\n";
std::cout << " --print-libdir print the installation directory for Lean's built-in libraries and exit\n";
std::cout << " --profile display elaboration/type checking time for each definition/theorem\n";
std::cout << " --stats display environment statistics\n";
DEBUG_CODE(
std::cout << " --debug=tag enable assertions with the given tag\n";
std::cout << " --debug=tag enable assertions with the given tag\n";
)
std::cout << " -D name=value set a configuration option (see set_option command)\n";
std::cout << " -D name=value set a configuration option (see set_option command)\n";
}
static int print_prefix = 0;

1574
stage0/stdlib/Lake/Load/Lean/Elab.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

1676
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -428,6 +428,7 @@ lean_object* l_Lean_Elab_expandDeclId___at_Lean_Elab_Term_expandDeclId___spec__1
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_elabStructureView___spec__4(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addDeclarationRanges___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__20___closed__1;
lean_object* l_Lean_assignLevelMVar___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent_copyFields___spec__2___lambda__2___closed__2;
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_reprStructFieldInfo____x40_Lean_Elab_Structure___hyg_551____closed__24;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_mkCoercionToCopiedParent___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -847,7 +848,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Command_StructFieldKind_noConfusion(lean_ob
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields___spec__5___lambda__6___closed__4;
static lean_object* l_Lean_Elab_elabAttr___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__4___lambda__1___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___lambda__2(lean_object*, 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_assignLevelMVar___at_Lean_Elab_Command_shouldInferResultUniverse___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_expandOptDeclSig(lean_object*);
lean_object* l_Lean_Name_getString_x21(lean_object*);
@ -22692,7 +22692,7 @@ lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_Elab_Command_mkResultUniverse(x_18, x_14);
lean_dec(x_14);
x_21 = l_Lean_assignLevelMVar___at_Lean_Elab_Command_shouldInferResultUniverse___spec__2(x_16, x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_19);
x_21 = l_Lean_assignLevelMVar___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_updateResultingUniverse___spec__1(x_16, x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_19);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);

10990
stage0/stdlib/Lean/Language/Lean.c generated
View file

File diff suppressed because it is too large Load diff

711
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -179,7 +179,6 @@ static lean_object* l_Lean_Meta_getLocalDeclFromUserName___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_approxDefEq(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Diagnostics_unfoldCounter___default;
lean_object* l_Lean_Level_succ___override(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentArray_anyMAux___at_Lean_FVarId_hasForwardDeps___spec__46___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isProp___default;
@ -193,7 +192,6 @@ lean_object* l_Lean_PersistentArray_push___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MVarId_findDecl_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_mkLambdaFVars___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* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentArray_anyMAux___at_Lean_FVarId_hasForwardDeps___spec__30___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Meta_Config_transparency___default;
LEAN_EXPORT lean_object* l_Lean_Meta_withAssignableSyntheticOpaque___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -410,7 +408,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_withLocalDeclsD__
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_FVarId_hasForwardDeps___spec__36___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getParamNames___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_foldl___at___private_Lean_Meta_Basic_0__Lean_Meta_withExistingLocalDeclsImp___spec__1(lean_object*, lean_object*);
size_t lean_ptr_addr(lean_object*);
static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateForallAux___closed__2;
lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImpAux(lean_object*);
@ -570,6 +567,7 @@ LEAN_EXPORT uint64_t l_Array_foldlMUnsafe_fold___at___private_Lean_Meta_Basic_0_
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_FVarId_hasForwardDeps___spec__33___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaLetTelescope___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_instantiate_level_mvars(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_FVarId_getDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withReducibleAndInstances(lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Meta_withIncRecDepth___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -652,11 +650,9 @@ LEAN_EXPORT lean_object* l_Lean_Meta_modifyDiag___boxed(lean_object*, lean_objec
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process(lean_object*);
static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2;
LEAN_EXPORT lean_object* l_Lean_MVarId_setType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_FVarId_hasForwardDeps___spec__12___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_2351_(lean_object*);
lean_object* l_Lean_LocalInstances_erase(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___lambda__3___closed__7;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withExistingLocalDeclsImp(lean_object*);
@ -725,7 +721,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_State_diag___default;
LEAN_EXPORT lean_object* l_Lean_Meta_getResetPostponed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_FVarId_hasForwardDeps___spec__16___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_simpLevelIMax_x27(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_State_mctx___default;
LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaDeltaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_16829____closed__7;
@ -851,7 +846,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_withLocalDecls
LEAN_EXPORT lean_object* l_Lean_Meta_withReducibleAndInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedCache;
lean_object* l_Lean_PersistentHashMap_find_x3f___at_Lean_getLevelMVarAssignment_x3f___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_FVarId_hasForwardDeps___spec__20(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_throwIsDefEqStuck___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2___boxed(lean_object*, lean_object*, lean_object*);
@ -989,7 +983,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_orelseMergeErr
lean_object* l_Lean_LocalDecl_type(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_instInhabitedDefEqCache___closed__1;
lean_object* l_Lean_Core_withRestoreOrSaveFull___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___lambda__3___closed__5;
@ -1016,7 +1009,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1386_(l
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_FVarId_hasForwardDeps___spec__20___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_FVarId_hasForwardDeps___spec__57___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MVarId_checkedAssign___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_processPostponed_loop___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1049,7 +1041,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_checkpointDefEq___at_Lean_Meta_isLevelDefEq
static lean_object* l_Lean_Meta_instOrElseMetaM___closed__1;
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2___rarg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImpAux___at_Lean_Meta_withNewLocalInstances___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_modifyDefEqTransientCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Meta_withErasedFVars___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1176,7 +1167,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getLocalDeclFromUserName___boxed(lean_objec
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_FVarId_hasForwardDeps___spec__4___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_modifyPostponed___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_liftMkBindingM___rarg___closed__2;
lean_object* l_Lean_simpLevelMax_x27(lean_object*, lean_object*, lean_object*);
lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_level_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withReducible___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -38044,652 +38034,97 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_fullApproxDefEq___rarg), 4, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(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_EXPORT lean_object* l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___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) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_8 = lean_st_ref_take(x_4, x_7);
x_9 = lean_ctor_get(x_8, 0);
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; uint8_t x_17;
x_7 = lean_st_ref_get(x_3, x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
x_10 = lean_ctor_get(x_9, 0);
lean_dec(x_7);
x_10 = lean_ctor_get(x_8, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_8, 1);
lean_inc(x_11);
lean_dec(x_8);
x_12 = !lean_is_exclusive(x_9);
if (x_12 == 0)
x_11 = lean_instantiate_level_mvars(x_10, x_1);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_st_ref_take(x_3, x_9);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = !lean_is_exclusive(x_15);
if (x_17 == 0)
{
lean_object* x_13; uint8_t x_14;
x_13 = lean_ctor_get(x_9, 0);
lean_dec(x_13);
x_14 = !lean_is_exclusive(x_10);
if (x_14 == 0)
lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_18 = lean_ctor_get(x_15, 0);
lean_dec(x_18);
lean_ctor_set(x_15, 0, x_12);
x_19 = lean_st_ref_set(x_3, x_15, x_16);
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_15 = lean_ctor_get(x_10, 6);
x_16 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_15, x_1, x_2);
lean_ctor_set(x_10, 6, x_16);
x_17 = lean_st_ref_set(x_4, x_9, x_11);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_17, 0);
lean_dec(x_19);
x_20 = lean_box(0);
lean_ctor_set(x_17, 0, x_20);
return x_17;
lean_object* x_21;
x_21 = lean_ctor_get(x_19, 0);
lean_dec(x_21);
lean_ctor_set(x_19, 0, x_13);
return x_19;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_22 = lean_box(0);
lean_object* x_22; lean_object* x_23;
x_22 = lean_ctor_get(x_19, 1);
lean_inc(x_22);
lean_dec(x_19);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
lean_ctor_set(x_23, 0, x_13);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
else
{
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; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_24 = lean_ctor_get(x_10, 0);
x_25 = lean_ctor_get(x_10, 1);
x_26 = lean_ctor_get(x_10, 2);
x_27 = lean_ctor_get(x_10, 3);
x_28 = lean_ctor_get(x_10, 4);
x_29 = lean_ctor_get(x_10, 5);
x_30 = lean_ctor_get(x_10, 6);
x_31 = lean_ctor_get(x_10, 7);
x_32 = lean_ctor_get(x_10, 8);
lean_inc(x_32);
lean_inc(x_31);
lean_inc(x_30);
lean_inc(x_29);
lean_inc(x_28);
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;
x_24 = lean_ctor_get(x_15, 1);
x_25 = lean_ctor_get(x_15, 2);
x_26 = lean_ctor_get(x_15, 3);
x_27 = lean_ctor_get(x_15, 4);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_10);
x_33 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_30, x_1, x_2);
x_34 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_34, 0, x_24);
lean_ctor_set(x_34, 1, x_25);
lean_ctor_set(x_34, 2, x_26);
lean_ctor_set(x_34, 3, x_27);
lean_ctor_set(x_34, 4, x_28);
lean_ctor_set(x_34, 5, x_29);
lean_ctor_set(x_34, 6, x_33);
lean_ctor_set(x_34, 7, x_31);
lean_ctor_set(x_34, 8, x_32);
lean_ctor_set(x_9, 0, x_34);
x_35 = lean_st_ref_set(x_4, x_9, x_11);
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
if (lean_is_exclusive(x_35)) {
lean_ctor_release(x_35, 0);
lean_ctor_release(x_35, 1);
x_37 = x_35;
} else {
lean_dec_ref(x_35);
x_37 = lean_box(0);
}
x_38 = lean_box(0);
if (lean_is_scalar(x_37)) {
x_39 = lean_alloc_ctor(0, 2, 0);
} else {
x_39 = x_37;
}
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_36);
return x_39;
}
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_40 = lean_ctor_get(x_9, 1);
x_41 = lean_ctor_get(x_9, 2);
x_42 = lean_ctor_get(x_9, 3);
x_43 = lean_ctor_get(x_9, 4);
lean_inc(x_43);
lean_inc(x_42);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_9);
x_44 = lean_ctor_get(x_10, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_10, 1);
lean_inc(x_45);
x_46 = lean_ctor_get(x_10, 2);
lean_inc(x_46);
x_47 = lean_ctor_get(x_10, 3);
lean_inc(x_47);
x_48 = lean_ctor_get(x_10, 4);
lean_inc(x_48);
x_49 = lean_ctor_get(x_10, 5);
lean_inc(x_49);
x_50 = lean_ctor_get(x_10, 6);
lean_inc(x_50);
x_51 = lean_ctor_get(x_10, 7);
lean_inc(x_51);
x_52 = lean_ctor_get(x_10, 8);
lean_inc(x_52);
if (lean_is_exclusive(x_10)) {
lean_ctor_release(x_10, 0);
lean_ctor_release(x_10, 1);
lean_ctor_release(x_10, 2);
lean_ctor_release(x_10, 3);
lean_ctor_release(x_10, 4);
lean_ctor_release(x_10, 5);
lean_ctor_release(x_10, 6);
lean_ctor_release(x_10, 7);
lean_ctor_release(x_10, 8);
x_53 = x_10;
} else {
lean_dec_ref(x_10);
x_53 = lean_box(0);
}
x_54 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_50, x_1, x_2);
if (lean_is_scalar(x_53)) {
x_55 = lean_alloc_ctor(0, 9, 0);
} else {
x_55 = x_53;
}
lean_ctor_set(x_55, 0, x_44);
lean_ctor_set(x_55, 1, x_45);
lean_ctor_set(x_55, 2, x_46);
lean_ctor_set(x_55, 3, x_47);
lean_ctor_set(x_55, 4, x_48);
lean_ctor_set(x_55, 5, x_49);
lean_ctor_set(x_55, 6, x_54);
lean_ctor_set(x_55, 7, x_51);
lean_ctor_set(x_55, 8, x_52);
x_56 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_40);
lean_ctor_set(x_56, 2, x_41);
lean_ctor_set(x_56, 3, x_42);
lean_ctor_set(x_56, 4, x_43);
x_57 = lean_st_ref_set(x_4, x_56, x_11);
x_58 = lean_ctor_get(x_57, 1);
lean_inc(x_58);
if (lean_is_exclusive(x_57)) {
lean_ctor_release(x_57, 0);
lean_ctor_release(x_57, 1);
x_59 = x_57;
} else {
lean_dec_ref(x_57);
x_59 = lean_box(0);
}
x_60 = lean_box(0);
if (lean_is_scalar(x_59)) {
x_61 = lean_alloc_ctor(0, 2, 0);
} else {
x_61 = x_59;
}
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_58);
return x_61;
}
}
}
LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___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) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 1:
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
lean_inc(x_7);
x_8 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_7, x_2, x_3, x_4, x_5, x_6);
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
lean_object* x_10; size_t x_11; size_t x_12; uint8_t x_13;
x_10 = lean_ctor_get(x_8, 0);
x_11 = lean_ptr_addr(x_7);
lean_dec(x_7);
x_12 = lean_ptr_addr(x_10);
x_13 = lean_usize_dec_eq(x_11, x_12);
if (x_13 == 0)
{
lean_object* x_14;
lean_dec(x_1);
x_14 = l_Lean_Level_succ___override(x_10);
lean_ctor_set(x_8, 0, x_14);
return x_8;
}
else
{
lean_dec(x_10);
lean_ctor_set(x_8, 0, x_1);
return x_8;
}
}
else
{
lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; uint8_t x_19;
x_15 = lean_ctor_get(x_8, 0);
x_16 = lean_ctor_get(x_8, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_8);
x_17 = lean_ptr_addr(x_7);
lean_dec(x_7);
x_18 = lean_ptr_addr(x_15);
x_19 = lean_usize_dec_eq(x_17, x_18);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_1);
x_20 = l_Lean_Level_succ___override(x_15);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_16);
return x_21;
}
else
{
lean_object* x_22;
lean_dec(x_15);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_1);
lean_ctor_set(x_22, 1, x_16);
return x_22;
}
}
}
case 2:
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_23 = lean_ctor_get(x_1, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_1, 1);
lean_inc(x_24);
lean_inc(x_23);
x_25 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_23, x_2, x_3, x_4, x_5, x_6);
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
lean_dec(x_25);
lean_inc(x_24);
x_28 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_24, x_2, x_3, x_4, x_5, x_27);
x_29 = !lean_is_exclusive(x_28);
if (x_29 == 0)
{
lean_object* x_30; size_t x_31; size_t x_32; uint8_t x_33;
x_30 = lean_ctor_get(x_28, 0);
x_31 = lean_ptr_addr(x_23);
lean_dec(x_23);
x_32 = lean_ptr_addr(x_26);
x_33 = lean_usize_dec_eq(x_31, x_32);
if (x_33 == 0)
{
lean_object* x_34;
lean_dec(x_24);
lean_dec(x_1);
x_34 = l_Lean_mkLevelMax_x27(x_26, x_30);
lean_ctor_set(x_28, 0, x_34);
return x_28;
}
else
{
size_t x_35; size_t x_36; uint8_t x_37;
x_35 = lean_ptr_addr(x_24);
lean_dec(x_24);
x_36 = lean_ptr_addr(x_30);
x_37 = lean_usize_dec_eq(x_35, x_36);
if (x_37 == 0)
{
lean_object* x_38;
lean_dec(x_1);
x_38 = l_Lean_mkLevelMax_x27(x_26, x_30);
lean_ctor_set(x_28, 0, x_38);
return x_28;
}
else
{
lean_object* x_39;
x_39 = l_Lean_simpLevelMax_x27(x_26, x_30, x_1);
lean_dec(x_1);
lean_dec(x_30);
lean_dec(x_26);
lean_ctor_set(x_28, 0, x_39);
return x_28;
}
}
}
else
{
lean_object* x_40; lean_object* x_41; size_t x_42; size_t x_43; uint8_t x_44;
x_40 = lean_ctor_get(x_28, 0);
x_41 = lean_ctor_get(x_28, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_28);
x_42 = lean_ptr_addr(x_23);
lean_dec(x_23);
x_43 = lean_ptr_addr(x_26);
x_44 = lean_usize_dec_eq(x_42, x_43);
if (x_44 == 0)
{
lean_object* x_45; lean_object* x_46;
lean_dec(x_24);
lean_dec(x_1);
x_45 = l_Lean_mkLevelMax_x27(x_26, x_40);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_41);
return x_46;
}
else
{
size_t x_47; size_t x_48; uint8_t x_49;
x_47 = lean_ptr_addr(x_24);
lean_dec(x_24);
x_48 = lean_ptr_addr(x_40);
x_49 = lean_usize_dec_eq(x_47, x_48);
if (x_49 == 0)
{
lean_object* x_50; lean_object* x_51;
lean_dec(x_1);
x_50 = l_Lean_mkLevelMax_x27(x_26, x_40);
x_51 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_51, 0, x_50);
lean_ctor_set(x_51, 1, x_41);
return x_51;
}
else
{
lean_object* x_52; lean_object* x_53;
x_52 = l_Lean_simpLevelMax_x27(x_26, x_40, x_1);
lean_dec(x_1);
lean_dec(x_40);
lean_dec(x_26);
x_53 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_41);
return x_53;
}
}
}
}
case 3:
{
lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; uint8_t x_60;
x_54 = lean_ctor_get(x_1, 0);
lean_inc(x_54);
x_55 = lean_ctor_get(x_1, 1);
lean_inc(x_55);
lean_inc(x_54);
x_56 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_54, x_2, x_3, x_4, x_5, x_6);
x_57 = lean_ctor_get(x_56, 0);
lean_inc(x_57);
x_58 = lean_ctor_get(x_56, 1);
lean_inc(x_58);
lean_dec(x_56);
lean_inc(x_55);
x_59 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_55, x_2, x_3, x_4, x_5, x_58);
x_60 = !lean_is_exclusive(x_59);
if (x_60 == 0)
{
lean_object* x_61; size_t x_62; size_t x_63; uint8_t x_64;
x_61 = lean_ctor_get(x_59, 0);
x_62 = lean_ptr_addr(x_54);
lean_dec(x_54);
x_63 = lean_ptr_addr(x_57);
x_64 = lean_usize_dec_eq(x_62, x_63);
if (x_64 == 0)
{
lean_object* x_65;
lean_dec(x_55);
lean_dec(x_1);
x_65 = l_Lean_mkLevelIMax_x27(x_57, x_61);
lean_ctor_set(x_59, 0, x_65);
return x_59;
}
else
{
size_t x_66; size_t x_67; uint8_t x_68;
x_66 = lean_ptr_addr(x_55);
lean_dec(x_55);
x_67 = lean_ptr_addr(x_61);
x_68 = lean_usize_dec_eq(x_66, x_67);
if (x_68 == 0)
{
lean_object* x_69;
lean_dec(x_1);
x_69 = l_Lean_mkLevelIMax_x27(x_57, x_61);
lean_ctor_set(x_59, 0, x_69);
return x_59;
}
else
{
lean_object* x_70;
x_70 = l_Lean_simpLevelIMax_x27(x_57, x_61, x_1);
lean_dec(x_1);
lean_ctor_set(x_59, 0, x_70);
return x_59;
}
}
}
else
{
lean_object* x_71; lean_object* x_72; size_t x_73; size_t x_74; uint8_t x_75;
x_71 = lean_ctor_get(x_59, 0);
x_72 = lean_ctor_get(x_59, 1);
lean_inc(x_72);
lean_inc(x_71);
lean_dec(x_59);
x_73 = lean_ptr_addr(x_54);
lean_dec(x_54);
x_74 = lean_ptr_addr(x_57);
x_75 = lean_usize_dec_eq(x_73, x_74);
if (x_75 == 0)
{
lean_object* x_76; lean_object* x_77;
lean_dec(x_55);
lean_dec(x_1);
x_76 = l_Lean_mkLevelIMax_x27(x_57, x_71);
x_77 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_72);
return x_77;
}
else
{
size_t x_78; size_t x_79; uint8_t x_80;
x_78 = lean_ptr_addr(x_55);
lean_dec(x_55);
x_79 = lean_ptr_addr(x_71);
x_80 = lean_usize_dec_eq(x_78, x_79);
if (x_80 == 0)
{
lean_object* x_81; lean_object* x_82;
lean_dec(x_1);
x_81 = l_Lean_mkLevelIMax_x27(x_57, x_71);
x_82 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_82, 0, x_81);
lean_ctor_set(x_82, 1, x_72);
return x_82;
}
else
{
lean_object* x_83; lean_object* x_84;
x_83 = l_Lean_simpLevelIMax_x27(x_57, x_71, x_1);
lean_dec(x_1);
x_84 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_84, 0, x_83);
lean_ctor_set(x_84, 1, x_72);
return x_84;
}
}
}
}
case 5:
{
lean_object* x_85; lean_object* x_86; uint8_t x_87;
x_85 = lean_ctor_get(x_1, 0);
lean_inc(x_85);
x_86 = lean_st_ref_get(x_3, x_6);
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_86, 0);
x_89 = lean_ctor_get(x_86, 1);
x_90 = lean_ctor_get(x_88, 0);
lean_inc(x_90);
lean_dec(x_88);
x_91 = lean_ctor_get(x_90, 6);
lean_inc(x_91);
lean_dec(x_90);
x_92 = l_Lean_PersistentHashMap_find_x3f___at_Lean_getLevelMVarAssignment_x3f___spec__1(x_91, x_85);
if (lean_obj_tag(x_92) == 0)
{
lean_dec(x_85);
lean_ctor_set(x_86, 0, x_1);
return x_86;
}
else
{
lean_object* x_93; uint8_t x_94;
lean_dec(x_1);
x_93 = lean_ctor_get(x_92, 0);
lean_inc(x_93);
lean_dec(x_92);
x_94 = l_Lean_Level_hasMVar(x_93);
if (x_94 == 0)
{
lean_dec(x_85);
lean_ctor_set(x_86, 0, x_93);
return x_86;
}
else
{
lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; uint8_t x_99;
lean_free_object(x_86);
x_95 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_93, x_2, x_3, x_4, x_5, x_89);
x_96 = lean_ctor_get(x_95, 0);
lean_inc(x_96);
x_97 = lean_ctor_get(x_95, 1);
lean_inc(x_97);
lean_dec(x_95);
lean_inc(x_96);
x_98 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_85, x_96, x_2, x_3, x_4, x_5, x_97);
x_99 = !lean_is_exclusive(x_98);
if (x_99 == 0)
{
lean_object* x_100;
x_100 = lean_ctor_get(x_98, 0);
lean_dec(x_100);
lean_ctor_set(x_98, 0, x_96);
return x_98;
}
else
{
lean_object* x_101; lean_object* x_102;
x_101 = lean_ctor_get(x_98, 1);
lean_inc(x_101);
lean_dec(x_98);
x_102 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_102, 0, x_96);
lean_ctor_set(x_102, 1, x_101);
return x_102;
}
}
}
}
else
{
lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107;
x_103 = lean_ctor_get(x_86, 0);
x_104 = lean_ctor_get(x_86, 1);
lean_inc(x_104);
lean_inc(x_103);
lean_dec(x_86);
x_105 = lean_ctor_get(x_103, 0);
lean_inc(x_105);
lean_dec(x_103);
x_106 = lean_ctor_get(x_105, 6);
lean_inc(x_106);
lean_dec(x_105);
x_107 = l_Lean_PersistentHashMap_find_x3f___at_Lean_getLevelMVarAssignment_x3f___spec__1(x_106, x_85);
if (lean_obj_tag(x_107) == 0)
{
lean_object* x_108;
lean_dec(x_85);
x_108 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_108, 0, x_1);
lean_ctor_set(x_108, 1, x_104);
return x_108;
}
else
{
lean_object* x_109; uint8_t x_110;
lean_dec(x_1);
x_109 = lean_ctor_get(x_107, 0);
lean_inc(x_109);
lean_dec(x_107);
x_110 = l_Lean_Level_hasMVar(x_109);
if (x_110 == 0)
{
lean_object* x_111;
lean_dec(x_85);
x_111 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_111, 0, x_109);
lean_ctor_set(x_111, 1, x_104);
return x_111;
}
else
{
lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118;
x_112 = l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___spec__1(x_109, x_2, x_3, x_4, x_5, x_104);
x_113 = lean_ctor_get(x_112, 0);
lean_inc(x_113);
x_114 = lean_ctor_get(x_112, 1);
lean_inc(x_114);
lean_dec(x_112);
lean_inc(x_113);
x_115 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_85, x_113, x_2, x_3, x_4, x_5, x_114);
x_116 = lean_ctor_get(x_115, 1);
lean_inc(x_116);
if (lean_is_exclusive(x_115)) {
lean_ctor_release(x_115, 0);
lean_ctor_release(x_115, 1);
x_117 = x_115;
x_28 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_28, 0, x_12);
lean_ctor_set(x_28, 1, x_24);
lean_ctor_set(x_28, 2, x_25);
lean_ctor_set(x_28, 3, x_26);
lean_ctor_set(x_28, 4, x_27);
x_29 = lean_st_ref_set(x_3, x_28, x_16);
x_30 = lean_ctor_get(x_29, 1);
lean_inc(x_30);
if (lean_is_exclusive(x_29)) {
lean_ctor_release(x_29, 0);
lean_ctor_release(x_29, 1);
x_31 = x_29;
} else {
lean_dec_ref(x_115);
x_117 = lean_box(0);
lean_dec_ref(x_29);
x_31 = lean_box(0);
}
if (lean_is_scalar(x_117)) {
x_118 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_31)) {
x_32 = lean_alloc_ctor(0, 2, 0);
} else {
x_118 = x_117;
}
lean_ctor_set(x_118, 0, x_113);
lean_ctor_set(x_118, 1, x_116);
return x_118;
}
}
}
}
default:
{
lean_object* x_119;
x_119 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_119, 0, x_1);
lean_ctor_set(x_119, 1, x_6);
return x_119;
x_32 = x_31;
}
lean_ctor_set(x_32, 0, x_13);
lean_ctor_set(x_32, 1, x_30);
return x_32;
}
}
}
@ -38725,18 +38160,6 @@ return x_14;
}
}
}
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2___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) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVars___at_Lean_Meta_normalizeLevel___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) {
_start:
{

224
stage0/stdlib/Lean/Meta/LevelDefEq.c generated
View file

@ -42,6 +42,7 @@ static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_LevelDefEq___hyg_1929___
LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Meta_isLevelDefEqAuxImpl___spec__4(lean_object*);
lean_object* l_Lean_Meta_throwIsDefEqStuck___rarg(lean_object*);
static lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq___closed__7;
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_stringToMessageData(lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_Meta_isLevelDefEqAuxImpl___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxMaxMax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -110,12 +111,12 @@ uint8_t l_Lean_Level_isParam(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxSelfMax_solve___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_LevelDefEq___hyg_1929____closed__14;
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxSelfMax_solve(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_LevelDefEq___hyg_1929____closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxSelfMax(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkMaxArgsDiff___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxMaxMax_solve___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Level_isMax(lean_object*);
static lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq___closed__2;
LEAN_EXPORT lean_object* l_ReaderT_pure___at_Lean_Meta_isLevelDefEqAuxImpl___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -125,6 +126,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkMaxArgs
LEAN_EXPORT lean_object* l_Lean_Meta_isLevelDefEqAuxImpl___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq___closed__1;
uint8_t l_Lean_Level_isMVar(lean_object*);
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instInhabitedOfMonad___rarg(lean_object*, lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_isMVarWithGreaterDepth___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -308,6 +310,200 @@ x_9 = lean_apply_5(x_8, x_2, x_3, x_4, x_5, x_6);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(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; uint8_t x_12;
x_8 = lean_st_ref_take(x_4, x_7);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_8, 1);
lean_inc(x_11);
lean_dec(x_8);
x_12 = !lean_is_exclusive(x_9);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14;
x_13 = lean_ctor_get(x_9, 0);
lean_dec(x_13);
x_14 = !lean_is_exclusive(x_10);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_15 = lean_ctor_get(x_10, 6);
x_16 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_15, x_1, x_2);
lean_ctor_set(x_10, 6, x_16);
x_17 = lean_st_ref_set(x_4, x_9, x_11);
x_18 = !lean_is_exclusive(x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_17, 0);
lean_dec(x_19);
x_20 = lean_box(0);
lean_ctor_set(x_17, 0, x_20);
return x_17;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 1);
lean_inc(x_21);
lean_dec(x_17);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
}
}
else
{
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; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_24 = lean_ctor_get(x_10, 0);
x_25 = lean_ctor_get(x_10, 1);
x_26 = lean_ctor_get(x_10, 2);
x_27 = lean_ctor_get(x_10, 3);
x_28 = lean_ctor_get(x_10, 4);
x_29 = lean_ctor_get(x_10, 5);
x_30 = lean_ctor_get(x_10, 6);
x_31 = lean_ctor_get(x_10, 7);
x_32 = lean_ctor_get(x_10, 8);
lean_inc(x_32);
lean_inc(x_31);
lean_inc(x_30);
lean_inc(x_29);
lean_inc(x_28);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_10);
x_33 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_30, x_1, x_2);
x_34 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_34, 0, x_24);
lean_ctor_set(x_34, 1, x_25);
lean_ctor_set(x_34, 2, x_26);
lean_ctor_set(x_34, 3, x_27);
lean_ctor_set(x_34, 4, x_28);
lean_ctor_set(x_34, 5, x_29);
lean_ctor_set(x_34, 6, x_33);
lean_ctor_set(x_34, 7, x_31);
lean_ctor_set(x_34, 8, x_32);
lean_ctor_set(x_9, 0, x_34);
x_35 = lean_st_ref_set(x_4, x_9, x_11);
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
if (lean_is_exclusive(x_35)) {
lean_ctor_release(x_35, 0);
lean_ctor_release(x_35, 1);
x_37 = x_35;
} else {
lean_dec_ref(x_35);
x_37 = lean_box(0);
}
x_38 = lean_box(0);
if (lean_is_scalar(x_37)) {
x_39 = lean_alloc_ctor(0, 2, 0);
} else {
x_39 = x_37;
}
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_36);
return x_39;
}
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_40 = lean_ctor_get(x_9, 1);
x_41 = lean_ctor_get(x_9, 2);
x_42 = lean_ctor_get(x_9, 3);
x_43 = lean_ctor_get(x_9, 4);
lean_inc(x_43);
lean_inc(x_42);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_9);
x_44 = lean_ctor_get(x_10, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_10, 1);
lean_inc(x_45);
x_46 = lean_ctor_get(x_10, 2);
lean_inc(x_46);
x_47 = lean_ctor_get(x_10, 3);
lean_inc(x_47);
x_48 = lean_ctor_get(x_10, 4);
lean_inc(x_48);
x_49 = lean_ctor_get(x_10, 5);
lean_inc(x_49);
x_50 = lean_ctor_get(x_10, 6);
lean_inc(x_50);
x_51 = lean_ctor_get(x_10, 7);
lean_inc(x_51);
x_52 = lean_ctor_get(x_10, 8);
lean_inc(x_52);
if (lean_is_exclusive(x_10)) {
lean_ctor_release(x_10, 0);
lean_ctor_release(x_10, 1);
lean_ctor_release(x_10, 2);
lean_ctor_release(x_10, 3);
lean_ctor_release(x_10, 4);
lean_ctor_release(x_10, 5);
lean_ctor_release(x_10, 6);
lean_ctor_release(x_10, 7);
lean_ctor_release(x_10, 8);
x_53 = x_10;
} else {
lean_dec_ref(x_10);
x_53 = lean_box(0);
}
x_54 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_50, x_1, x_2);
if (lean_is_scalar(x_53)) {
x_55 = lean_alloc_ctor(0, 9, 0);
} else {
x_55 = x_53;
}
lean_ctor_set(x_55, 0, x_44);
lean_ctor_set(x_55, 1, x_45);
lean_ctor_set(x_55, 2, x_46);
lean_ctor_set(x_55, 3, x_47);
lean_ctor_set(x_55, 4, x_48);
lean_ctor_set(x_55, 5, x_49);
lean_ctor_set(x_55, 6, x_54);
lean_ctor_set(x_55, 7, x_51);
lean_ctor_set(x_55, 8, x_52);
x_56 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_56, 0, x_55);
lean_ctor_set(x_56, 1, x_40);
lean_ctor_set(x_56, 2, x_41);
lean_ctor_set(x_56, 3, x_42);
lean_ctor_set(x_56, 4, x_43);
x_57 = lean_st_ref_set(x_4, x_56, x_11);
x_58 = lean_ctor_get(x_57, 1);
lean_inc(x_58);
if (lean_is_exclusive(x_57)) {
lean_ctor_release(x_57, 0);
lean_ctor_release(x_57, 1);
x_59 = x_57;
} else {
lean_dec_ref(x_57);
x_59 = lean_box(0);
}
x_60 = lean_box(0);
if (lean_is_scalar(x_59)) {
x_61 = lean_alloc_ctor(0, 2, 0);
} else {
x_61 = x_59;
}
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_58);
return x_61;
}
}
}
static lean_object* _init_l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___closed__1() {
_start:
{
@ -387,7 +583,7 @@ x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_mkMaxArgsDiff(x_1, x_2, x_12);
x_15 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_1, x_14, x_3, x_4, x_5, x_6, x_13);
x_15 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_1, x_14, x_3, x_4, x_5, x_6, x_13);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
@ -396,6 +592,18 @@ return x_15;
}
}
}
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2___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) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_8;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_LevelDefEq_0__Lean_Meta_tryApproxSelfMax_solve(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:
{
@ -416,7 +624,7 @@ return x_12;
else
{
lean_object* x_13; uint8_t x_14;
x_13 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_3, x_1, x_4, x_5, x_6, x_7, x_8);
x_13 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_3, x_1, x_4, x_5, x_6, x_7, x_8);
x_14 = !lean_is_exclusive(x_13);
if (x_14 == 0)
{
@ -603,7 +811,7 @@ return x_14;
else
{
lean_object* x_15; uint8_t x_16;
x_15 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_4, x_1, x_5, x_6, x_7, x_8, x_9);
x_15 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_4, x_1, x_5, x_6, x_7, x_8, x_9);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
@ -634,7 +842,7 @@ else
{
lean_object* x_24; uint8_t x_25;
lean_dec(x_1);
x_24 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_4, x_2, x_5, x_6, x_7, x_8, x_9);
x_24 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_4, x_2, x_5, x_6, x_7, x_8, x_9);
x_25 = !lean_is_exclusive(x_24);
if (x_25 == 0)
{
@ -2020,7 +2228,7 @@ lean_object* x_176; lean_object* x_177; uint8_t x_178;
lean_free_object(x_169);
x_176 = l_Lean_Level_mvarId_x21(x_1);
lean_dec(x_1);
x_177 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_176, x_2, x_3, x_4, x_5, x_6, x_173);
x_177 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_176, x_2, x_3, x_4, x_5, x_6, x_173);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
@ -2159,7 +2367,7 @@ if (x_207 == 0)
lean_object* x_208; lean_object* x_209; lean_object* x_210; lean_object* x_211; uint8_t x_212; lean_object* x_213; lean_object* x_214;
x_208 = l_Lean_Level_mvarId_x21(x_1);
lean_dec(x_1);
x_209 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_208, x_2, x_3, x_4, x_5, x_6, x_206);
x_209 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_208, x_2, x_3, x_4, x_5, x_6, x_206);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
@ -2292,7 +2500,7 @@ lean_inc(x_234);
lean_dec(x_169);
x_235 = l_Lean_Level_mvarId_x21(x_2);
lean_dec(x_2);
x_236 = l_Lean_assignLevelMVar___at_Lean_Meta_normalizeLevel___spec__2(x_235, x_1, x_3, x_4, x_5, x_6, x_234);
x_236 = l_Lean_assignLevelMVar___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__2(x_235, x_1, x_3, x_4, x_5, x_6, x_234);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);

5144
stage0/stdlib/Lean/MetavarContext.c generated
View file

File diff suppressed because it is too large Load diff