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:
Sebastian Ullrich 2020-12-18 17:27:54 +01:00
parent 0ddc932052
commit 7f2caac0b7
32 changed files with 12974 additions and 15939 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
stage0/src/Init/Data/Option/Basic.lean generated
View file

@ -64,10 +64,9 @@ instance : Monad Option := {
/- Remark: when using the polymorphic notation `a <|> b` is not a `[macroInline]`.
Thus, `a <|> b` will make `Option.orelse` to behave like it was marked as `[inline]`. -/
instance : Alternative Option := {
failure := none,
instance : Alternative Option where
failure := none
orElse := Option.orElse
}
@[inline] protected def lt (r : α → α → Prop) : Option α → Option α → Prop
| none, some x => True
@ -82,22 +81,8 @@ instance (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt
end Option
instance [DecidableEq α] : DecidableEq (Option α) := fun a b =>
match a, b with
| none, none => isTrue rfl
| none, (some v₂) => isFalse (fun h => Option.noConfusion h)
| (some v₁), none => isFalse (fun h => Option.noConfusion h)
| (some v₁), (some v₂) =>
match decEq v₁ v₂ with
| (isTrue e) => isTrue (congrArg (@some α) e)
| (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))
instance [BEq α] : BEq (Option α) where
beq
| none, none => true
| none, (some v₂) => false
| (some v₁), none => false
| (some v₁), (some v₂) => v₁ == v₂
deriving instance DecidableEq for Option
deriving instance BEq for Option
instance [HasLess α] : HasLess (Option α) := {
Less := Option.lt (· < ·)

12
stage0/src/Lean/Data/Position.lean generated
View file

@ -10,19 +10,9 @@ namespace Lean
structure Position where
line : Nat
column : Nat
deriving Inhabited
deriving Inhabited, DecidableEq
namespace Position
instance : DecidableEq Position :=
fun ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ =>
if h₁ : l₁ = l₂ then
if h₂ : c₁ = c₂ then
isTrue $ by subst h₁; subst h₂; rfl
else
isFalse fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₂ h₂)
else
isFalse fun contra => Position.noConfusion contra (fun e₁ e₂ => absurd e₁ h₁)
protected def lt : Position → Position → Bool
| ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => (l₁, c₁) < (l₂, c₂)

20
stage0/src/Lean/Elab/Deriving/DecEq.lean generated
View file

@ -23,15 +23,17 @@ def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunNam
where
mkSameCtorRhs : List (Syntax × Syntax × Bool) → TermElabM Syntax
| [] => `(isTrue rfl)
| (a, b, false) :: todo => withFreshMacroScope do
`(if h : $a = $b then
by subst h; exact $(← mkSameCtorRhs todo):term
else
isFalse (by intro n; injection n; apply h _; assumption))
| (a, b, true) :: todo => withFreshMacroScope do
`(@dite _ _ ($(mkIdent auxFunName) $a $b)
(fun h => by subst h; exact $(← mkSameCtorRhs todo):term)
(fun h => isFalse (by intro n; injection n; apply h _; assumption)))
| (a, b, recField) :: todo => withFreshMacroScope do
let rhs ←
`(if h : $a = $b then
by subst h; exact $(← mkSameCtorRhs todo):term
else
isFalse (by intro n; injection n; apply h _; assumption))
if recField then
-- add local instance for `a = b` using the function being defined `auxFunName`
`(let inst := $(mkIdent auxFunName) $a $b; $rhs)
else
return rhs
mkAlts : TermElabM (Array Syntax) := do
let mut alts := #[]

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

@ -258,9 +258,7 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
| _, [] => throwError "non-exhaustive 'match_syntax'"
| discr::discrs, alts => do
let alts := (alts.map getHeadInfo).zip alts;
-- Choose a most specific pattern, ie. a minimal element according to `generalizes`.
-- If there are multiple minimal elements, the choice does not matter.
let (info, alt) := alts.tail!.foldl (fun (min : HeadInfo × Alt) (alt : HeadInfo × Alt) => if min.1.generalizes alt.1 then alt else min) alts.head!;
let (info, alt) := alts.head!
-- introduce pattern matches on the discriminant's children if there are any nested patterns
let newDiscrs ← match info with
| basic { argPats := some pats, .. } => (List.range pats.size).mapM fun i => `(Syntax.getArg discr $(quote i))

48
stage0/src/library/compiler/ir_interpreter.cpp generated
View file

@ -298,7 +298,7 @@ void * lookup_symbol_in_cur_exe(char const * sym) {
}
class interpreter;
static interpreter & get_interpreter();
LEAN_THREAD_PTR(interpreter, g_interpreter);
class interpreter {
// stack of IR variable slots
@ -314,8 +314,8 @@ class interpreter {
frame(name const & mFn, size_t mArgBp, size_t mJpBp) : m_fn(mFn), m_arg_bp(mArgBp), m_jp_bp(mJpBp) {}
};
std::vector<frame> m_call_stack;
environment const * m_env;
options const * m_opts;
environment const & m_env;
options const & m_opts;
// if `false`, use IR code where possible
bool m_prefer_native;
struct constant_cache_entry {
@ -353,30 +353,18 @@ class interpreter {
public:
template<class T>
static inline T with_interpreter(environment const & env, options const & opts, std::function<T(interpreter &)> const & f) {
interpreter & interp = get_interpreter();
if (interp.m_env && is_eqp(*interp.m_env, env) && interp.m_opts && is_eqp(*interp.m_opts, opts)) {
return f(interp);
if (g_interpreter && is_eqp(g_interpreter->m_env, env) && is_eqp(g_interpreter->m_opts, opts)) {
return f(*g_interpreter);
} else {
// We changed threads or the closure was stored and called in a different context.
time_task t("interpretation",
message_builder(env, get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
abstract_type_context trace_ctx(opts);
scope_trace_env scope_trace(env, opts, trace_ctx);
flet<environment const *> fl1(interp.m_env, &env);
flet<options const *> fl2(interp.m_opts, &opts);
flet<bool> fl3(interp.m_prefer_native, opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE));
if (interp.m_env) {
// both these caches contain data from the Environment, so we cannot reuse them when changing it
flet<name_map<constant_cache_entry>> fl4(interp.m_constant_cache, {});
flet<name_map<symbol_cache_entry>> fl5(interp.m_symbol_cache, {});
return f(interp);
} else {
// if there is no outer interpreter, might as well leave the caches around; maybe the next call is for
// the same Environment
interp.m_constant_cache = {};
interp.m_symbol_cache = {};
return f(interp);
}
// the caches contain data from the Environment, so we cannot reuse them when changing it
interpreter interp(env, opts);
flet<interpreter *> fl(g_interpreter, &interp);
return f(interp);
}
}
@ -412,8 +400,8 @@ private:
object * mk_stub_closure(decl const & d, unsigned n, object ** args) {
unsigned cls_size = 3 + decl_params(d).size();
object * cls = alloc_closure(get_stub(cls_size), cls_size, 3 + n);
closure_set(cls, 0, m_env->to_obj_arg());
closure_set(cls, 1, m_opts->to_obj_arg());
closure_set(cls, 0, m_env.to_obj_arg());
closure_set(cls, 1, m_opts.to_obj_arg());
closure_set(cls, 2, d.to_obj_arg());
for (unsigned i = 0; i < n ; i++)
closure_set(cls, 3 + i, args[i]);
@ -741,7 +729,7 @@ private:
return *e;
} else {
symbol_cache_entry e_new { get_decl(fn), nullptr, false };
if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(*m_env, fn)) {
if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
string_ref mangled = name_mangle(fn, *g_mangle_prefix);
string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
// check for boxed version first
@ -760,7 +748,7 @@ private:
/** \brief Retrieve Lean declaration from environment. */
decl get_decl(name const & fn) {
option_ref<decl> d = find_ir_decl(*m_env, fn);
option_ref<decl> d = find_ir_decl(m_env, fn);
if (!d) {
throw exception(sstream() << "unknown declaration '" << fn << "'");
}
@ -780,7 +768,7 @@ private:
return *o;
}
if (get_regular_init_fn_name_for(*m_env, fn)) {
if (get_regular_init_fn_name_for(m_env, fn)) {
// We don't know whether `[init]` decls can be re-executed, so let's not.
throw exception(sstream() << "cannot evaluate `[init]` declaration '" << fn << "' in the same module");
}
@ -917,6 +905,10 @@ private:
}
}
public:
explicit interpreter(environment const & env, options const & opts) : m_env(env), m_opts(opts) {
m_prefer_native = opts.get_bool(*g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE);
}
~interpreter() {
for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) {
if (!e.m_is_scalar) {
@ -944,7 +936,7 @@ public:
} else {
// `lookup_symbol` does not prefer the boxed version for interpreted functions, so check manually.
decl d = e.m_decl;
if (option_ref<decl> d_boxed = find_ir_decl(*m_env, fn + *g_boxed_suffix)) {
if (option_ref<decl> d_boxed = find_ir_decl(m_env, fn + *g_boxed_suffix)) {
d = *d_boxed.get();
}
r = mk_stub_closure(d, 0, nullptr);
@ -1014,8 +1006,6 @@ public:
}
};
MK_THREAD_LOCAL_GET_DEF(interpreter, get_interpreter);
object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
return interpreter::with_interpreter<object *>(env, opts, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
}

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

228
stage0/stdlib/Init/Data/Option/Basic.c generated
View file

@ -18,7 +18,6 @@ lean_object* l_Option_instMonadOption___closed__8;
lean_object* l_Option_instAlternativeOption;
lean_object* l_Option_instMonadOption___closed__7;
lean_object* l_Option_getD___rarg___boxed(lean_object*, lean_object*);
lean_object* l_instDecidableEqOption_match__1___rarg(uint8_t, lean_object*, lean_object*);
lean_object* l_Option_all___rarg(lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___closed__3;
lean_object* l_Option_bind(lean_object*, lean_object*);
@ -28,10 +27,10 @@ lean_object* l_Option_getD(lean_object*);
lean_object* l_Option_toBool_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_orElse(lean_object*);
lean_object* l_Option_instAlternativeOption___closed__1;
lean_object* l_instDecidableEqOption_match__2(lean_object*, lean_object*);
lean_object* l_Option_isSome___rarg___boxed(lean_object*);
lean_object* l_Option_orElse___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Option_instMonadOption;
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1(lean_object*);
lean_object* l_Option_isNone_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___closed__9;
lean_object* l_Option_filter___rarg(lean_object*, lean_object*);
@ -46,8 +45,11 @@ lean_object* l_Option_toBool(lean_object*);
lean_object* l_Option_all_match__1(lean_object*, lean_object*);
lean_object* l_Option_filter_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_lt_match__1(lean_object*, lean_object*);
lean_object* l_instBEqOption___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instBEqOption___rarg(lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649__match__1(lean_object*, lean_object*);
lean_object* l_Option_all(lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649_(lean_object*);
lean_object* l_Option_instMonadOption___lambda__3(lean_object*, lean_object*);
uint8_t l_Option_isSome___rarg(lean_object*);
lean_object* l_Option_isSome(lean_object*);
@ -57,14 +59,14 @@ lean_object* l_Option_orElse___rarg(lean_object*, lean_object*);
lean_object* l_Option_isNone___rarg___boxed(lean_object*);
lean_object* l_instDecidableEqOption(lean_object*);
lean_object* l_Option_toMonad___rarg(lean_object*, lean_object*);
lean_object* l_instBEqOption_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_toMonad_match__1(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530__match__1(lean_object*, lean_object*);
lean_object* l_Option_instDecidableRelLt_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_toMonad(lean_object*, lean_object*, lean_object*);
lean_object* l_instDecidableEqOption_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instBEqOption_match__1(lean_object*, lean_object*);
lean_object* l_Option_filter_match__1(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_toMonad___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___lambda__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_lt_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_any_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -76,21 +78,21 @@ lean_object* l_instBEqOption(lean_object*);
lean_object* l_Option_any(lean_object*);
lean_object* l_Option_any_match__1(lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instDecidableEqOption_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___closed__10;
lean_object* l_Option_toMonad_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___closed__5;
lean_object* l_Option_isNone(lean_object*);
lean_object* l_Option_any___rarg(lean_object*, lean_object*);
lean_object* l_instDecidableEqOption___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649__match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_instMonadOption___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530_(lean_object*);
lean_object* l_Option_getD_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_map___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530__match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_map(lean_object*, lean_object*);
lean_object* l_instDecidableEqOption_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_orElse_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Option_isNone___rarg(lean_object*);
lean_object* l_instDecidableEqOption_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Option_getD_match__1(lean_object*, lean_object*);
lean_object* l_Option_instAlternativeOption___closed__3;
uint8_t l_Option_toBool___rarg(lean_object*);
@ -1450,54 +1452,7 @@ x_3 = lean_alloc_closure((void*)(l_Option_instDecidableRelLt___rarg), 3, 0);
return x_3;
}
}
lean_object* l_instDecidableEqOption_match__1___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (x_1 == 0)
{
lean_object* x_4;
lean_dec(x_2);
x_4 = lean_apply_1(x_3, lean_box(0));
return x_4;
}
else
{
lean_object* x_5;
lean_dec(x_3);
x_5 = lean_apply_1(x_2, lean_box(0));
return x_5;
}
}
}
lean_object* l_instDecidableEqOption_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_instDecidableEqOption_match__1___rarg___boxed), 3, 0);
return x_5;
}
}
lean_object* l_instDecidableEqOption_match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_1);
lean_dec(x_1);
x_5 = l_instDecidableEqOption_match__1___rarg(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_instDecidableEqOption_match__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_instDecidableEqOption_match__1(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
}
}
lean_object* l_instDecidableEqOption_match__2___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* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530__match__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:
{
if (lean_obj_tag(x_1) == 0)
@ -1553,15 +1508,15 @@ return x_15;
}
}
}
lean_object* l_instDecidableEqOption_match__2(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530__match__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instDecidableEqOption_match__2___rarg), 6, 0);
x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530__match__1___rarg), 6, 0);
return x_3;
}
}
lean_object* l_instDecidableEqOption___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -1609,6 +1564,78 @@ return x_12;
}
}
}
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530_(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____rarg), 3, 0);
return x_2;
}
}
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_dec(x_1);
if (lean_obj_tag(x_3) == 0)
{
uint8_t x_4; lean_object* x_5;
x_4 = 1;
x_5 = lean_box(x_4);
return x_5;
}
else
{
uint8_t x_6; lean_object* x_7;
lean_dec(x_3);
x_6 = 0;
x_7 = lean_box(x_6);
return x_7;
}
}
else
{
if (lean_obj_tag(x_3) == 0)
{
uint8_t x_8; lean_object* x_9;
lean_dec(x_2);
lean_dec(x_1);
x_8 = 0;
x_9 = lean_box(x_8);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_2, 0);
lean_inc(x_10);
lean_dec(x_2);
x_11 = lean_ctor_get(x_3, 0);
lean_inc(x_11);
lean_dec(x_3);
x_12 = lean_apply_2(x_1, x_10, x_11);
return x_12;
}
}
}
}
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_instDecidableEqOption___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_instDecidableEqOption(lean_object* x_1) {
_start:
{
@ -1617,71 +1644,63 @@ x_2 = lean_alloc_closure((void*)(l_instDecidableEqOption___rarg), 3, 0);
return x_2;
}
}
lean_object* l_instBEqOption_match__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* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649__match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_7; lean_object* x_8;
lean_dec(x_4);
x_7 = lean_box(0);
x_8 = lean_apply_1(x_3, x_7);
lean_object* x_6; lean_object* x_7;
lean_dec(x_5);
x_6 = lean_box(0);
x_7 = lean_apply_1(x_3, x_6);
return x_7;
}
else
{
lean_object* x_8;
lean_dec(x_3);
x_8 = lean_apply_2(x_5, x_1, x_2);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10;
lean_dec(x_3);
x_9 = lean_ctor_get(x_2, 0);
lean_inc(x_9);
lean_dec(x_2);
x_10 = lean_apply_1(x_4, x_9);
return x_10;
}
}
else
{
lean_dec(x_4);
lean_dec(x_3);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_11; lean_object* x_12;
lean_dec(x_6);
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_apply_1(x_5, x_11);
return x_12;
lean_object* x_9;
lean_dec(x_4);
x_9 = lean_apply_2(x_5, x_1, x_2);
return x_9;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_dec(x_5);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
x_10 = lean_ctor_get(x_1, 0);
lean_inc(x_10);
lean_dec(x_1);
x_14 = lean_ctor_get(x_2, 0);
lean_inc(x_14);
x_11 = lean_ctor_get(x_2, 0);
lean_inc(x_11);
lean_dec(x_2);
x_15 = lean_apply_2(x_6, x_13, x_14);
return x_15;
x_12 = lean_apply_2(x_4, x_10, x_11);
return x_12;
}
}
}
}
lean_object* l_instBEqOption_match__1(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649__match__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_instBEqOption_match__1___rarg), 6, 0);
x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649__match__1___rarg), 5, 0);
return x_3;
}
}
lean_object* l_instBEqOption___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -1729,11 +1748,28 @@ return x_12;
}
}
}
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649_(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg), 3, 0);
return x_2;
}
}
lean_object* l_instBEqOption___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_instBEqOption(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_instBEqOption___rarg), 3, 0);
x_2 = lean_alloc_closure((void*)(l_instBEqOption___rarg), 1, 0);
return x_2;
}
}

101
stage0/stdlib/Lean/Compiler/ExternAttr.c generated
View file

@ -221,6 +221,7 @@ lean_object* l_Lean_initFn____x40_Lean_Compiler_ExternAttr___hyg_243____lambda__
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getExternAttrData___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qpartition_loop___at_Lean_initFn____x40_Lean_Compiler_ExternAttr___hyg_243____spec__7___closed__1;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___spec__3___closed__1;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_getExternConstArity(lean_object*, lean_object*, lean_object*, lean_object*);
@ -657,50 +658,50 @@ x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_nat_dec_eq(x_11, x_12);
if (x_7 == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = l_Lean_Syntax_getArg(x_6, x_12);
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = l_Lean_Syntax_getArg(x_6, x_12);
lean_dec(x_6);
x_23 = l_Lean_numLitKind;
x_24 = l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(x_23, x_22);
lean_dec(x_22);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25;
x_25 = l_Lean_Syntax_decodeNatLitVal_x3f___closed__1;
x_14 = x_25;
goto block_21;
}
else
{
uint8_t x_26;
x_26 = !lean_is_exclusive(x_24);
if (x_26 == 0)
{
x_14 = x_24;
goto block_21;
}
else
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_24, 0);
lean_inc(x_27);
x_25 = l_Lean_numLitKind;
x_26 = l___private_Init_Meta_0__Lean_Syntax_isNatLitAux(x_25, x_24);
lean_dec(x_24);
x_28 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_28, 0, x_27);
x_14 = x_28;
goto block_21;
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27;
x_27 = l_Lean_Syntax_decodeNatLitVal_x3f___closed__1;
x_14 = x_27;
goto block_23;
}
else
{
uint8_t x_28;
x_28 = !lean_is_exclusive(x_26);
if (x_28 == 0)
{
x_14 = x_26;
goto block_23;
}
else
{
lean_object* x_29; lean_object* x_30;
x_29 = lean_ctor_get(x_26, 0);
lean_inc(x_29);
lean_dec(x_26);
x_30 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_30, 0, x_29);
x_14 = x_30;
goto block_23;
}
}
}
else
{
lean_object* x_29;
lean_object* x_31;
lean_dec(x_6);
x_29 = lean_box(0);
x_14 = x_29;
goto block_21;
x_31 = lean_box(0);
x_14 = x_31;
goto block_23;
}
block_21:
block_23:
{
if (x_13 == 0)
{
@ -713,19 +714,10 @@ return x_16;
}
else
{
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_2);
x_17 = l___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___closed__3;
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_4);
return x_18;
}
else
lean_object* x_17; uint8_t x_18;
x_17 = lean_box(0);
x_18 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(x_14, x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = lean_box(0);
@ -734,6 +726,19 @@ lean_dec(x_10);
lean_dec(x_11);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22;
lean_dec(x_14);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_2);
x_21 = l___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___closed__3;
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_4);
return x_22;
}
}
}
}

190
stage0/stdlib/Lean/Compiler/IR/Basic.c generated
View file

@ -126,7 +126,6 @@ lean_object* l_Lean_IR_LocalContext_isLocalVar___boxed(lean_object*, lean_object
lean_object* l_Lean_IR_IRType_isStruct_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_IR_instAlphaEqvArrayArg___closed__1;
uint8_t l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_instToStringVarId(lean_object*);
lean_object* l_Lean_IR_Arg_alphaEqv_match__1(lean_object*);
uint8_t l_Lean_IR_CtorInfo_isRef(lean_object*);
@ -135,7 +134,6 @@ lean_object* l_Lean_IR_VarId_alphaEqv___boxed(lean_object*, lean_object*, lean_o
lean_object* l_Lean_IR_addParamRename(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_IRType_isUnion_match__1(lean_object*);
size_t l_Lean_IR_instHashableVarId(lean_object*);
lean_object* l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_IRType_instBEqIRType___closed__1;
lean_object* l_Lean_IR_FnBody_isTerminal___boxed(lean_object*);
lean_object* l_Lean_IR_IRType_isIrrelevant_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -148,6 +146,7 @@ lean_object* l_Lean_IR_FnBody_alphaEqv___boxed(lean_object*, lean_object*, lean_
lean_object* l_Lean_IR_AltCore_modifyBody(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_IRType_isObj_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_IR_LocalContext_isParam_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_appendTrees___rarg(lean_object*, lean_object*);
@ -177,6 +176,7 @@ uint8_t l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__2(lean_object*, lean_ob
lean_object* l_Lean_IR_instInhabitedFnBody;
lean_object* l_Lean_IR_AltCore_mmodifyBody_match__1(lean_object*);
extern lean_object* l_Array_swapAt_x21___rarg___closed__2;
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_IR_mmodifyJPs___spec__1(lean_object*);
lean_object* l_Lean_IR_push(lean_object*, lean_object*);
lean_object* l_Lean_IR_Expr_alphaEqv___boxed(lean_object*, lean_object*, lean_object*);
@ -867,44 +867,39 @@ x_2 = lean_alloc_closure((void*)(l_Lean_IR_IRType_beq_match__1___rarg), 14, 0);
return x_2;
}
}
uint8_t l_Array_isEqvAux___at_Lean_IR_IRType_beq___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) {
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_array_get_size(x_4);
x_8 = lean_nat_dec_lt(x_6, x_7);
lean_dec(x_7);
if (x_8 == 0)
if (lean_obj_tag(x_1) == 0)
{
uint8_t x_9;
lean_dec(x_6);
x_9 = 1;
return x_9;
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_array_fget(x_4, x_6);
x_11 = lean_array_fget(x_5, x_6);
x_12 = l_Lean_IR_IRType_beq(x_10, x_11);
lean_dec(x_11);
lean_dec(x_10);
if (x_12 == 0)
{
uint8_t x_13;
lean_dec(x_6);
x_13 = 0;
return x_13;
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_unsigned_to_nat(1u);
x_15 = lean_nat_add(x_6, x_14);
lean_dec(x_6);
x_3 = lean_box(0);
x_6 = x_15;
goto _start;
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_name_eq(x_6, x_7);
return x_8;
}
}
}
@ -1136,61 +1131,58 @@ case 9:
{
if (lean_obj_tag(x_2) == 9)
{
lean_object* x_21;
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_21 = lean_ctor_get(x_1, 0);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22;
x_22 = lean_ctor_get(x_2, 0);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_23 = lean_ctor_get(x_1, 1);
x_22 = lean_ctor_get(x_1, 1);
x_23 = lean_ctor_get(x_2, 0);
x_24 = lean_ctor_get(x_2, 1);
x_25 = lean_array_get_size(x_23);
x_26 = lean_array_get_size(x_24);
x_27 = lean_nat_dec_eq(x_25, x_26);
lean_dec(x_26);
lean_dec(x_25);
if (x_27 == 0)
x_25 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1(x_21, x_23);
if (x_25 == 0)
{
uint8_t x_28;
x_28 = 0;
return x_28;
uint8_t x_26;
x_26 = 0;
return x_26;
}
else
{
lean_object* x_29; uint8_t x_30;
x_29 = lean_unsigned_to_nat(0u);
x_30 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__1(x_23, x_24, lean_box(0), x_23, x_24, x_29);
lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_27 = lean_array_get_size(x_22);
x_28 = lean_array_get_size(x_24);
x_29 = lean_nat_dec_eq(x_27, x_28);
lean_dec(x_28);
lean_dec(x_27);
if (x_29 == 0)
{
uint8_t x_30;
x_30 = 0;
return x_30;
}
}
else
{
uint8_t x_31;
x_31 = 0;
return x_31;
lean_object* x_31; uint8_t x_32;
x_31 = lean_unsigned_to_nat(0u);
x_32 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__2(x_22, x_24, lean_box(0), x_22, x_24, x_31);
return x_32;
}
}
}
else
{
lean_object* x_32;
x_32 = lean_ctor_get(x_2, 0);
if (lean_obj_tag(x_32) == 0)
{
uint8_t x_33;
x_33 = 0;
return x_33;
}
else
}
default:
{
if (lean_obj_tag(x_2) == 10)
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38;
x_34 = lean_ctor_get(x_1, 1);
x_35 = lean_ctor_get(x_2, 1);
x_36 = lean_ctor_get(x_21, 0);
x_37 = lean_ctor_get(x_32, 0);
x_38 = lean_name_eq(x_36, x_37);
x_34 = lean_ctor_get(x_1, 0);
x_35 = lean_ctor_get(x_1, 1);
x_36 = lean_ctor_get(x_2, 0);
x_37 = lean_ctor_get(x_2, 1);
x_38 = lean_name_eq(x_34, x_36);
if (x_38 == 0)
{
uint8_t x_39;
@ -1200,8 +1192,8 @@ return x_39;
else
{
lean_object* x_40; lean_object* x_41; uint8_t x_42;
x_40 = lean_array_get_size(x_34);
x_41 = lean_array_get_size(x_35);
x_40 = lean_array_get_size(x_35);
x_41 = lean_array_get_size(x_37);
x_42 = lean_nat_dec_eq(x_40, x_41);
lean_dec(x_41);
lean_dec(x_40);
@ -1215,13 +1207,11 @@ else
{
lean_object* x_44; uint8_t x_45;
x_44 = lean_unsigned_to_nat(0u);
x_45 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__2(x_34, x_35, lean_box(0), x_34, x_35, x_44);
x_45 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__3(x_35, x_37, lean_box(0), x_35, x_37, x_44);
return x_45;
}
}
}
}
}
else
{
uint8_t x_46;
@ -1229,66 +1219,18 @@ x_46 = 0;
return x_46;
}
}
default:
{
if (lean_obj_tag(x_2) == 10)
{
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51;
x_47 = lean_ctor_get(x_1, 0);
x_48 = lean_ctor_get(x_1, 1);
x_49 = lean_ctor_get(x_2, 0);
x_50 = lean_ctor_get(x_2, 1);
x_51 = lean_name_eq(x_47, x_49);
if (x_51 == 0)
{
uint8_t x_52;
x_52 = 0;
return x_52;
}
else
{
lean_object* x_53; lean_object* x_54; uint8_t x_55;
x_53 = lean_array_get_size(x_48);
x_54 = lean_array_get_size(x_50);
x_55 = lean_nat_dec_eq(x_53, x_54);
lean_dec(x_54);
lean_dec(x_53);
if (x_55 == 0)
{
uint8_t x_56;
x_56 = 0;
return x_56;
}
else
{
lean_object* x_57; uint8_t x_58;
x_57 = lean_unsigned_to_nat(0u);
x_58 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__3(x_48, x_50, lean_box(0), x_48, x_50, x_57);
return x_58;
}
}
}
else
{
uint8_t x_59;
x_59 = 0;
return x_59;
}
}
}
}
}
lean_object* l_Array_isEqvAux___at_Lean_IR_IRType_beq___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* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_7; lean_object* x_8;
x_7 = l_Array_isEqvAux___at_Lean_IR_IRType_beq___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_IR_IRType_beq___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_8 = lean_box(x_7);
return x_8;
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Array_isEqvAux___at_Lean_IR_IRType_beq___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) {

8
stage0/stdlib/Lean/Data/Json/Parser.c generated
View file

@ -71,6 +71,7 @@ lean_object* l_Lean_Json_Parser_natNumDigits(lean_object*);
lean_object* lean_int_mul(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Json_Parser_num(lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_Parser_natNonZero_match__1(lean_object*);
lean_object* l_Lean_Quickparse_instMonadQuickparse___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_Parser_num___lambda__3___closed__3___boxed__const__1;
@ -125,7 +126,6 @@ lean_object* l_Lean_Json_Parser_num___lambda__3___closed__1;
lean_object* l_Lean_Json_Parser_num___closed__1;
lean_object* l_Lean_Json_Parser_objectCore___closed__1;
lean_object* l_Lean_Json_Parser_escapedChar_match__1(lean_object*);
lean_object* l_instDecidableEqOption___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Int_instInhabitedInt___closed__1;
lean_object* l_Lean_Quickparse_instMonadQuickparse___closed__9;
lean_object* l_Lean_Quickparse_peek_x3f(lean_object*);
@ -3223,14 +3223,14 @@ lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44;
x_41 = l_Lean_Json_Parser_num___lambda__3___closed__2;
x_42 = l_Lean_Json_Parser_num___lambda__3___closed__1;
lean_inc(x_40);
x_43 = l_instDecidableEqOption___rarg(x_41, x_40, x_42);
x_43 = l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(x_41, x_40, x_42);
x_44 = lean_unbox(x_43);
lean_dec(x_43);
if (x_44 == 0)
{
lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_45 = l_Lean_Json_Parser_num___lambda__3___closed__3;
x_46 = l_instDecidableEqOption___rarg(x_41, x_40, x_45);
x_46 = l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(x_41, x_40, x_45);
x_47 = lean_unbox(x_46);
lean_dec(x_46);
if (x_47 == 0)
@ -3389,7 +3389,7 @@ lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint
x_10 = l_Lean_Json_Parser_num___lambda__5___closed__1;
x_11 = l_Lean_Json_Parser_num___lambda__3___closed__2;
x_12 = l_Lean_Json_Parser_num___lambda__5___closed__2;
x_13 = l_instDecidableEqOption___rarg(x_11, x_9, x_12);
x_13 = l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_530____at_instDecidableEqOption___spec__1___rarg(x_11, x_9, x_12);
x_14 = lean_unbox(x_13);
lean_dec(x_13);
if (x_14 == 0)

81
stage0/stdlib/Lean/Data/Position.c generated
View file

@ -15,8 +15,8 @@ extern "C" {
#endif
lean_object* l_Lean_FileMap_toPosition_match__1(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(lean_object*, lean_object*);
extern lean_object* l_instReprSigma___rarg___closed__2;
lean_object* l_Lean_Position_instDecidableEqPosition_match__1(lean_object*);
lean_object* l_Lean_FileMap_ofString_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString___closed__2;
lean_object* l_Lean_instInhabitedPosition;
@ -25,20 +25,22 @@ extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
extern lean_object* l_instReprSigma___rarg___closed__1;
lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
extern lean_object* l_instInhabitedNat;
lean_object* l_Lean_Position_instDecidableEqPosition_match__1___rarg(lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Position_instToFormatPosition___closed__2;
lean_object* l_prodHasDecidableLt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_formatKVMap___closed__1;
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1(lean_object*);
lean_object* l_Lean_FileMap_ofString___closed__1;
lean_object* l_Lean_Position_instToFormatPosition___closed__1;
lean_object* l_Lean_Position_lt(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16____boxed(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition_toColumn(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Position_instToStringPosition_match__1(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1___boxed(lean_object*);
@ -52,24 +54,22 @@ lean_object* l_Lean_FileMap_toPosition_loop___boxed(lean_object*, lean_object*,
lean_object* l_Lean_FileMap_ofString(lean_object*);
lean_object* l_Lean_fmt___at_Lean_Position_instToFormatPosition___spec__1(lean_object*);
lean_object* l_Lean_FileMap_toPosition_toColumn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_instDecidableEqPosition(lean_object*, lean_object*);
lean_object* l_Lean_Position_instToStringPosition(lean_object*);
lean_object* l_Lean_FileMap_toPosition_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
extern lean_object* l_term_x5b___x5d___closed__5;
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_FileMap_toPosition___spec__1(lean_object*);
lean_object* l_Lean_instDecidableEqPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedFileMap___closed__1;
lean_object* l_Lean_Position_instToFormatPosition(lean_object*);
uint8_t l_Lean_Position_instDecidableEqPosition(lean_object*, lean_object*);
lean_object* l_Lean_Position_lt___closed__1;
lean_object* l_Lean_Position_instToFormatPosition_match__1(lean_object*);
lean_object* l_Lean_Position_instDecidableEqPosition_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_instInhabitedPosition___closed__1;
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Position_instDecidableEqPosition___boxed(lean_object*, lean_object*);
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* l_Lean_Position_instToStringPosition_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Position_instDecidableEqPosition_match__2(lean_object*);
lean_object* l_Lean_Position_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Position_lt___closed__2;
@ -98,49 +98,33 @@ x_1 = l_Lean_instInhabitedPosition___closed__1;
return x_1;
}
}
lean_object* l_Lean_Position_instDecidableEqPosition_match__1___rarg(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
x_6 = lean_ctor_get(x_2, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_2, 1);
lean_inc(x_7);
lean_dec(x_2);
x_8 = lean_apply_4(x_3, x_4, x_5, x_6, x_7);
return x_8;
}
}
lean_object* l_Lean_Position_instDecidableEqPosition_match__1(lean_object* x_1) {
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Position_instDecidableEqPosition_match__1___rarg), 2, 0);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16__match__1___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Position_instDecidableEqPosition_match__2___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Lean_Position_instDecidableEqPosition_match__2(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Position_instDecidableEqPosition_match__2___rarg), 2, 0);
return x_2;
}
}
uint8_t l_Lean_Position_instDecidableEqPosition(lean_object* x_1, lean_object* x_2) {
uint8_t l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
@ -163,11 +147,30 @@ return x_9;
}
}
}
lean_object* l_Lean_Position_instDecidableEqPosition___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Position_instDecidableEqPosition(x_1, x_2);
x_3 = l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Lean_instDecidableEqPosition(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l___private_Lean_Data_Position_0__Lean_decEqPosition____x40_Lean_Data_Position___hyg_16_(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_instDecidableEqPosition___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_instDecidableEqPosition(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);

3327
stage0/stdlib/Lean/Elab/Deriving/DecEq.c generated
View file

File diff suppressed because it is too large Load diff

272
stage0/stdlib/Lean/Elab/PreDefinition/Main.c generated
View file

@ -182,6 +182,7 @@ extern lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_98
extern lean_object* l_Array_findSomeM_x3f___rarg___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__1;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_addPreDefinitions___spec__6___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__1___closed__1() {
@ -1966,225 +1967,136 @@ return x_2;
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9(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_44; size_t x_45; size_t 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; size_t x_54;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_27; size_t x_28; size_t 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; size_t x_37;
lean_inc(x_2);
x_4 = l___private_Lean_Util_SCC_0__Lean_SCC_push___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__10(x_2, x_3);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_44 = lean_array_get_size(x_1);
x_45 = lean_usize_of_nat(x_44);
x_46 = 0;
x_47 = l_Array_findSomeM_x3f___rarg___closed__1;
x_48 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__3(x_2, x_47, x_1, x_45, x_46, x_47);
x_49 = lean_ctor_get(x_48, 0);
lean_inc(x_49);
lean_dec(x_48);
x_50 = lean_box(0);
x_51 = l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9___boxed__const__1;
x_52 = lean_box_usize(x_45);
x_27 = lean_array_get_size(x_1);
x_28 = lean_usize_of_nat(x_27);
x_29 = 0;
x_30 = l_Array_findSomeM_x3f___rarg___closed__1;
x_31 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__3(x_2, x_30, x_1, x_28, x_29, x_30);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
lean_dec(x_31);
x_33 = lean_box(0);
x_34 = l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9___boxed__const__1;
x_35 = lean_box_usize(x_28);
lean_inc(x_1);
x_53 = lean_alloc_closure((void*)(l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9___lambda__1___boxed), 6, 4);
lean_closure_set(x_53, 0, x_44);
lean_closure_set(x_53, 1, x_1);
lean_closure_set(x_53, 2, x_51);
lean_closure_set(x_53, 3, x_52);
x_54 = 8192;
if (lean_obj_tag(x_49) == 0)
x_36 = lean_alloc_closure((void*)(l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__9___lambda__1___boxed), 6, 4);
lean_closure_set(x_36, 0, x_27);
lean_closure_set(x_36, 1, x_1);
lean_closure_set(x_36, 2, x_34);
lean_closure_set(x_36, 3, x_35);
x_37 = 8192;
if (lean_obj_tag(x_32) == 0)
{
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_55 = l_Lean_Elab_instInhabitedPreDefinition__1;
x_56 = l_Option_get_x21___rarg___closed__4;
x_57 = lean_panic_fn(x_55, x_56);
x_58 = lean_ctor_get(x_57, 4);
lean_inc(x_58);
lean_dec(x_57);
x_59 = l_Lean_Expr_FoldConstsImpl_initCache;
x_60 = l_Lean_Expr_FoldConstsImpl_fold_visit___rarg(x_53, x_54, x_58, x_50, x_59);
x_61 = lean_ctor_get(x_60, 0);
lean_inc(x_61);
lean_dec(x_60);
x_6 = x_61;
goto block_43;
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_38 = l_Lean_Elab_instInhabitedPreDefinition__1;
x_39 = l_Option_get_x21___rarg___closed__4;
x_40 = lean_panic_fn(x_38, x_39);
x_41 = lean_ctor_get(x_40, 4);
lean_inc(x_41);
lean_dec(x_40);
x_42 = l_Lean_Expr_FoldConstsImpl_initCache;
x_43 = l_Lean_Expr_FoldConstsImpl_fold_visit___rarg(x_36, x_37, x_41, x_33, x_42);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
lean_dec(x_43);
x_6 = x_44;
goto block_26;
}
else
{
lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_62 = lean_ctor_get(x_49, 0);
lean_inc(x_62);
lean_dec(x_49);
x_63 = lean_ctor_get(x_62, 4);
lean_inc(x_63);
lean_dec(x_62);
x_64 = l_Lean_Expr_FoldConstsImpl_initCache;
x_65 = l_Lean_Expr_FoldConstsImpl_fold_visit___rarg(x_53, x_54, x_63, x_50, x_64);
x_66 = lean_ctor_get(x_65, 0);
lean_inc(x_66);
lean_dec(x_65);
x_6 = x_66;
goto block_43;
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_45 = lean_ctor_get(x_32, 0);
lean_inc(x_45);
lean_dec(x_32);
x_46 = lean_ctor_get(x_45, 4);
lean_inc(x_46);
lean_dec(x_45);
x_47 = l_Lean_Expr_FoldConstsImpl_initCache;
x_48 = l_Lean_Expr_FoldConstsImpl_fold_visit___rarg(x_36, x_37, x_46, x_33, x_47);
x_49 = lean_ctor_get(x_48, 0);
lean_inc(x_49);
lean_dec(x_48);
x_6 = x_49;
goto block_26;
}
block_43:
block_26:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc(x_2);
x_7 = l_List_forM___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__19(x_1, x_2, x_6, x_5);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__6(x_2, x_8);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
x_10 = !lean_is_exclusive(x_9);
if (x_10 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
lean_dec(x_10);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_9, 1);
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_11 = lean_ctor_get(x_9, 0);
x_12 = lean_ctor_get(x_9, 1);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_9);
x_14 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(x_2, x_13);
lean_dec(x_2);
return x_14;
}
else
{
uint8_t x_15;
lean_dec(x_12);
lean_dec(x_2);
x_15 = !lean_is_exclusive(x_9);
x_14 = lean_ctor_get(x_11, 0);
lean_inc(x_14);
lean_dec(x_11);
x_15 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(x_13, x_14);
lean_dec(x_14);
lean_dec(x_13);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_ctor_get(x_9, 0);
lean_dec(x_16);
x_17 = lean_box(0);
lean_ctor_set(x_9, 0, x_17);
lean_object* x_16;
lean_dec(x_2);
x_16 = lean_box(0);
lean_ctor_set(x_9, 0, x_16);
return x_9;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_9, 1);
lean_inc(x_18);
lean_dec(x_9);
x_19 = lean_box(0);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
return x_20;
}
lean_object* x_17;
lean_free_object(x_9);
x_17 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(x_2, x_12);
lean_dec(x_2);
return x_17;
}
}
else
{
lean_object* x_21;
x_21 = lean_ctor_get(x_10, 0);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_18 = lean_ctor_get(x_9, 0);
x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_9);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
x_21 = lean_ctor_get(x_18, 0);
lean_inc(x_21);
lean_dec(x_10);
if (lean_obj_tag(x_21) == 0)
{
uint8_t x_22;
lean_dec(x_11);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_9);
lean_dec(x_18);
x_22 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(x_20, x_21);
lean_dec(x_21);
lean_dec(x_20);
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_9, 0);
lean_dec(x_23);
x_24 = lean_box(0);
lean_ctor_set(x_9, 0, x_24);
return x_9;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_9, 1);
lean_inc(x_25);
lean_dec(x_9);
x_26 = lean_box(0);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_25);
return x_27;
}
}
else
{
uint8_t x_28;
x_28 = !lean_is_exclusive(x_9);
if (x_28 == 0)
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_29 = lean_ctor_get(x_9, 1);
x_30 = lean_ctor_get(x_9, 0);
lean_dec(x_30);
x_31 = lean_ctor_get(x_11, 0);
lean_inc(x_31);
lean_dec(x_11);
x_32 = lean_ctor_get(x_21, 0);
lean_inc(x_32);
lean_dec(x_21);
x_33 = lean_nat_dec_eq(x_31, x_32);
lean_dec(x_32);
lean_dec(x_31);
if (x_33 == 0)
{
lean_object* x_34;
lean_dec(x_2);
x_34 = lean_box(0);
lean_ctor_set(x_9, 0, x_34);
return x_9;
x_23 = lean_box(0);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_19);
return x_24;
}
else
{
lean_object* x_35;
lean_free_object(x_9);
x_35 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(x_2, x_29);
lean_object* x_25;
x_25 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(x_2, x_19);
lean_dec(x_2);
return x_35;
}
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_36 = lean_ctor_get(x_9, 1);
lean_inc(x_36);
lean_dec(x_9);
x_37 = lean_ctor_get(x_11, 0);
lean_inc(x_37);
lean_dec(x_11);
x_38 = lean_ctor_get(x_21, 0);
lean_inc(x_38);
lean_dec(x_21);
x_39 = lean_nat_dec_eq(x_37, x_38);
lean_dec(x_38);
lean_dec(x_37);
if (x_39 == 0)
{
lean_object* x_40; lean_object* x_41;
lean_dec(x_2);
x_40 = lean_box(0);
x_41 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_36);
return x_41;
}
else
{
lean_object* x_42;
x_42 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(x_2, x_36);
lean_dec(x_2);
return x_42;
}
}
return x_25;
}
}
}

8804
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

67
stage0/stdlib/Lean/Elab/Util.c generated
View file

@ -24,6 +24,7 @@ lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__5(lean_object*, lean_object
lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMacroAttribute(lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Elab_getMacros___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__7;
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -67,6 +68,7 @@ lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__6;
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__2;
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_853____closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_evalSyntaxConstant___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_getBetterRef___lambda__1(lean_object*);
@ -104,6 +106,7 @@ lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__4(lean_object*, lean_object
lean_object* l_Lean_Elab_mkMacroAttributeUnsafe___closed__1;
lean_object* l_Lean_Elab_instMonadMacroAdapter___rarg(lean_object*, lean_object*);
size_t lean_usize_modn(size_t, lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedKeyedDeclsAttribute___closed__1;
lean_object* l_Lean_Elab_mkUnusedBaseName___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack(lean_object*);
@ -390,25 +393,64 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_getBetterRef_match__2___rarg), 3, 0
return x_2;
}
}
uint8_t l_Lean_Elab_getBetterRef___lambda__1(lean_object* x_1) {
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_Syntax_getPos(x_2);
if (lean_obj_tag(x_3) == 0)
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_5;
lean_dec(x_3);
x_5 = 1;
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_nat_dec_eq(x_6, x_7);
return x_8;
}
}
}
}
uint8_t l_Lean_Elab_getBetterRef___lambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_Syntax_getPos(x_2);
x_4 = lean_box(0);
x_5 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1(x_3, x_4);
lean_dec(x_3);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = 1;
return x_6;
}
else
{
uint8_t x_7;
x_7 = 0;
return x_7;
}
}
}
static lean_object* _init_l_Lean_Elab_getBetterRef___closed__1() {
@ -455,6 +497,17 @@ return x_1;
}
}
}
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Elab_getBetterRef___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_getBetterRef___lambda__1___boxed(lean_object* x_1) {
_start:
{

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

@ -163,6 +163,7 @@ lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_State_zetaFVarIds___default;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstance___at___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImp___spec__1(lean_object*);
lean_object* l_Lean_Meta_hasAssignableMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
@ -795,6 +796,7 @@ lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__1___rarg_
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getFVarLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateLambdaAux_match__1(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Meta_throwUnknownFVar___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_findLocalDecl_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1137,6 +1139,43 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey_ma
return x_2;
}
}
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_nat_dec_eq(x_6, x_7);
return x_8;
}
}
}
}
uint8_t l_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1156,50 +1195,32 @@ return x_10;
}
else
{
if (lean_obj_tag(x_5) == 0)
{
if (lean_obj_tag(x_8) == 0)
{
uint8_t x_11;
x_11 = lean_expr_eqv(x_4, x_7);
return x_11;
}
else
x_11 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(x_5, x_8);
if (x_11 == 0)
{
uint8_t x_12;
x_12 = 0;
return x_12;
}
}
else
{
if (lean_obj_tag(x_8) == 0)
{
uint8_t x_13;
x_13 = 0;
x_13 = lean_expr_eqv(x_4, x_7);
return x_13;
}
else
}
}
}
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_5, 0);
x_15 = lean_ctor_get(x_8, 0);
x_16 = lean_nat_dec_eq(x_14, x_15);
if (x_16 == 0)
{
uint8_t x_17;
x_17 = 0;
return x_17;
}
else
{
uint8_t x_18;
x_18 = lean_expr_eqv(x_4, x_7);
return x_18;
}
}
}
}
uint8_t x_3; lean_object* x_4;
x_3 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_Meta_InfoCacheKey_instBEqInfoCacheKey___boxed(lean_object* x_1, lean_object* x_2) {

1412
stage0/stdlib/Lean/Meta/FunInfo.c generated
View file

File diff suppressed because it is too large Load diff

1444
stage0/stdlib/Lean/Meta/PPGoal.c generated
View file

File diff suppressed because it is too large Load diff

19
stage0/stdlib/Lean/Parser/Attr.c generated
View file

@ -320,6 +320,7 @@ lean_object* l_Lean_Parser_Attr_class___elambda__1___closed__3;
lean_object* l_Lean_Parser_Attr_macro_formatter___closed__3;
lean_object* l_Lean_Parser_symbolInfo(lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Attr_class_formatter___closed__1;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Attr_externEntry_parenthesizer___closed__6;
@ -700,22 +701,24 @@ return x_8;
lean_object* l_Lean_Parser_Priority_numPrio___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_maxPrec;
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_object* x_6;
x_6 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_6;
lean_dec(x_1);
return x_4;
}
else
{
lean_dec(x_5);
lean_dec(x_1);
return x_4;
lean_object* x_8;
x_8 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_8;
}
}
}

3275
stage0/stdlib/Lean/Parser/Basic.c generated
View file

File diff suppressed because it is too large Load diff

88
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -2041,6 +2041,7 @@ lean_object* l_Lean_Parser_Command_structExplicitBinder_formatter___closed__10;
lean_object* l_Lean_Parser_Command_set__option_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Command_openRenaming___closed__8;
lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__2;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_docComment_formatter___closed__7;
lean_object* l_Lean_Parser_Command_classInductive_formatter___closed__2;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__10;
@ -3341,25 +3342,27 @@ return x_5;
lean_object* l_Lean_Parser_Command_commentBody___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
x_4 = lean_unsigned_to_nat(1u);
x_5 = l_Lean_Parser_finishCommentBlock(x_4, x_1, x_2);
x_6 = lean_ctor_get(x_5, 3);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
x_7 = lean_box(0);
x_8 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_6, x_7);
lean_dec(x_6);
if (x_8 == 0)
{
uint8_t x_7; lean_object* x_8;
x_7 = 1;
x_8 = l___private_Lean_Parser_Basic_0__Lean_Parser_rawAux(x_3, x_7, x_1, x_5);
return x_8;
lean_dec(x_3);
return x_5;
}
else
{
lean_dec(x_6);
lean_dec(x_3);
return x_5;
uint8_t x_9; lean_object* x_10;
x_9 = 1;
x_10 = l___private_Lean_Parser_Basic_0__Lean_Parser_rawAux(x_3, x_9, x_1, x_5);
return x_10;
}
}
}
@ -30334,52 +30337,55 @@ return x_3;
lean_object* l_Lean_Parser_Command_in___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = lean_unsigned_to_nat(1024u);
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = l_Lean_Parser_Term_doFor___elambda__1___closed__6;
x_9 = l_Lean_Parser_Command_in___elambda__1___closed__4;
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_8 = lean_ctor_get(x_4, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = l_Lean_Parser_Term_doFor___elambda__1___closed__6;
x_11 = l_Lean_Parser_Command_in___elambda__1___closed__4;
lean_inc(x_1);
x_10 = l_Lean_Parser_symbolFnAux(x_8, x_9, x_1, x_4);
x_11 = lean_ctor_get(x_10, 3);
lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
x_12 = l_Lean_Parser_symbolFnAux(x_10, x_11, x_1, x_4);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
x_14 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_13, x_6);
lean_dec(x_13);
if (x_14 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_12 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3697____closed__4;
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_Parser_categoryParser___elambda__1(x_12, x_13, x_1, x_10);
lean_object* x_15; lean_object* x_16;
lean_dec(x_1);
x_15 = l_Lean_Parser_Command_in___elambda__1___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_7);
lean_dec(x_7);
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_12, x_15, x_9);
lean_dec(x_9);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_11);
lean_dec(x_1);
x_17 = l_Lean_Parser_Command_in___elambda__1___closed__2;
x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_17, x_7);
lean_dec(x_7);
return x_18;
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_17 = l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3697____closed__4;
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_Parser_categoryParser___elambda__1(x_17, x_18, x_1, x_12);
x_20 = l_Lean_Parser_Command_in___elambda__1___closed__2;
x_21 = l_Lean_Parser_ParserState_mkTrailingNode(x_19, x_20, x_9);
lean_dec(x_9);
return x_21;
}
}
else
{
lean_dec(x_5);
lean_dec(x_1);
return x_4;
}
}
}
static lean_object* _init_l_Lean_Parser_Command_in___closed__1() {

2263
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

148
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -434,6 +434,7 @@ lean_object* l_Lean_Parser_addLeadingParser_match__1(lean_object*);
lean_object* l_Lean_Parser_symbolInfo(lean_object*);
lean_object* l_Lean_Parser_parserAttributeHooks;
lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_updateBuiltinTokens(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserExtension_State_kinds___default;
extern lean_object* l_Lean_Parser_epsilonInfo;
@ -9559,17 +9560,17 @@ lean_dec(x_9);
if (x_5 == 0)
{
x_11 = x_1;
goto block_34;
goto block_37;
}
else
{
lean_object* x_35;
lean_object* x_38;
lean_dec(x_1);
x_35 = l_stx___x3c_x7c_x3e_____closed__6;
x_11 = x_35;
goto block_34;
x_38 = l_stx___x3c_x7c_x3e_____closed__6;
x_11 = x_38;
goto block_37;
}
block_34:
block_37:
{
lean_object* x_12;
x_12 = l_Std_PersistentHashMap_find_x3f___at_Lean_Parser_getCategory___spec__1(x_10, x_11);
@ -9589,7 +9590,7 @@ return x_19;
}
else
{
lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27;
x_20 = lean_ctor_get(x_12, 0);
lean_inc(x_20);
lean_dec(x_12);
@ -9610,51 +9611,54 @@ lean_closure_set(x_25, 2, x_24);
lean_inc(x_3);
lean_inc(x_2);
x_26 = l_Lean_Parser_tryAnti(x_2, x_3);
x_27 = lean_box(0);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
lean_object* x_28; lean_object* x_29; uint8_t x_30;
lean_dec(x_25);
lean_dec(x_23);
lean_inc(x_2);
lean_inc(x_21);
x_27 = l_Lean_Parser_leadingParserAux(x_11, x_21, x_22, x_2, x_3);
x_28 = lean_ctor_get(x_27, 3);
lean_inc(x_28);
if (lean_obj_tag(x_28) == 0)
x_28 = l_Lean_Parser_leadingParserAux(x_11, x_21, x_22, x_2, x_3);
x_29 = lean_ctor_get(x_28, 3);
lean_inc(x_29);
x_30 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_29, x_27);
lean_dec(x_29);
if (x_30 == 0)
{
lean_object* x_29;
x_29 = l_Lean_Parser_trailingLoop(x_21, x_2, x_27);
return x_29;
}
else
{
lean_dec(x_28);
lean_dec(x_21);
lean_dec(x_2);
return x_27;
return x_28;
}
else
{
lean_object* x_31;
x_31 = l_Lean_Parser_trailingLoop(x_21, x_2, x_28);
return x_31;
}
}
else
{
uint8_t x_30; lean_object* x_31; lean_object* x_32;
uint8_t x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
lean_dec(x_11);
x_30 = 1;
x_32 = 1;
lean_inc(x_2);
x_31 = l_Lean_Parser_orelseFnCore(x_23, x_25, x_30, x_2, x_3);
x_32 = lean_ctor_get(x_31, 3);
lean_inc(x_32);
if (lean_obj_tag(x_32) == 0)
x_33 = l_Lean_Parser_orelseFnCore(x_23, x_25, x_32, x_2, x_3);
x_34 = lean_ctor_get(x_33, 3);
lean_inc(x_34);
x_35 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_34, x_27);
lean_dec(x_34);
if (x_35 == 0)
{
lean_object* x_33;
x_33 = l_Lean_Parser_trailingLoop(x_21, x_2, x_31);
lean_dec(x_21);
lean_dec(x_2);
return x_33;
}
else
{
lean_dec(x_32);
lean_dec(x_21);
lean_dec(x_2);
return x_31;
lean_object* x_36;
x_36 = l_Lean_Parser_trailingLoop(x_21, x_2, x_33);
return x_36;
}
}
}
@ -10235,7 +10239,7 @@ return x_2;
lean_object* l_Lean_Parser_runParserCategory(lean_object* x_1, lean_object* x_2, lean_object* 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_object* x_13; lean_object* x_14; uint8_t x_15;
lean_inc(x_3);
x_5 = l_Lean_Parser_mkInputContext(x_3, x_4);
x_6 = lean_box(0);
@ -10252,47 +10256,49 @@ lean_inc(x_9);
x_12 = l_Lean_Parser_categoryParserFnImpl(x_2, x_9, x_11);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
x_15 = lean_string_utf8_at_end(x_3, x_14);
lean_dec(x_14);
lean_dec(x_3);
x_14 = lean_box(0);
x_15 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_13, x_14);
lean_dec(x_13);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
x_17 = l_Lean_Parser_ParserState_mkError(x_12, x_16);
x_18 = l_Lean_Parser_ParserState_toErrorMsg(x_9, x_17);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_18);
return x_19;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_9);
x_20 = lean_ctor_get(x_12, 0);
lean_inc(x_20);
lean_dec(x_12);
x_21 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_20);
lean_dec(x_20);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_21);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24;
lean_dec(x_13);
lean_object* x_16; lean_object* x_17;
lean_dec(x_3);
x_23 = l_Lean_Parser_ParserState_toErrorMsg(x_9, x_12);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_23);
return x_24;
x_16 = l_Lean_Parser_ParserState_toErrorMsg(x_9, x_12);
x_17 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_17, 0, x_16);
return x_17;
}
else
{
lean_object* x_18; uint8_t x_19;
x_18 = lean_ctor_get(x_12, 1);
lean_inc(x_18);
x_19 = lean_string_utf8_at_end(x_3, x_18);
lean_dec(x_18);
lean_dec(x_3);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
x_21 = l_Lean_Parser_ParserState_mkError(x_12, x_20);
x_22 = l_Lean_Parser_ParserState_toErrorMsg(x_9, x_21);
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_22);
return x_23;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_9);
x_24 = lean_ctor_get(x_12, 0);
lean_inc(x_24);
lean_dec(x_12);
x_25 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_24);
lean_dec(x_24);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
return x_26;
}
}
}
}

32
stage0/stdlib/Lean/Parser/Extra.c generated
View file

@ -415,6 +415,7 @@ lean_object* l_Lean_Parser_symbolInfo(lean_object*);
lean_object* l_Lean_Parser_charLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_charLit_parenthesizer___closed__2;
lean_object* l_Lean_Parser_charLit_formatter___closed__3;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Int_instInhabitedInt___closed__1;
lean_object* l_Lean_Parser_notSymbol_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1988,7 +1989,7 @@ return x_10;
lean_object* l_Lean_Parser_many1___elambda__1(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_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_array_get_size(x_4);
@ -1998,23 +1999,25 @@ lean_inc(x_2);
x_6 = lean_apply_2(x_1, x_2, x_3);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
x_8 = lean_box(0);
x_9 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_7, x_8);
lean_dec(x_7);
if (x_9 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_Lean_Parser_manyAux(x_1, x_2, x_6);
x_9 = l_Lean_nullKind;
x_10 = l_Lean_Parser_ParserState_mkNode(x_8, x_9, x_5);
return x_10;
lean_object* x_10; lean_object* x_11;
lean_dec(x_2);
lean_dec(x_1);
x_10 = l_Lean_nullKind;
x_11 = l_Lean_Parser_ParserState_mkNode(x_6, x_10, x_5);
return x_11;
}
else
{
lean_object* x_11; lean_object* x_12;
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
x_11 = l_Lean_nullKind;
x_12 = l_Lean_Parser_ParserState_mkNode(x_6, x_11, x_5);
return x_12;
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = l_Lean_Parser_manyAux(x_1, x_2, x_6);
x_13 = l_Lean_nullKind;
x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_5);
return x_14;
}
}
}
@ -2239,6 +2242,7 @@ if (x_5 == 0)
lean_object* x_6;
lean_dec(x_4);
x_6 = l_Lean_Parser_rawIdentFn(x_1, x_2);
lean_dec(x_1);
return x_6;
}
else

112
stage0/stdlib/Lean/Parser/Level.c generated
View file

@ -192,6 +192,7 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
lean_object* l___regBuiltin_Lean_Parser_Level_ident_formatter___closed__1;
lean_object* l_Lean_Parser_Level_paren_parenthesizer___closed__5;
lean_object* l_Lean_Parser_symbolInfo(lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__10;
@ -1787,22 +1788,24 @@ return x_5;
lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_maxPrec;
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_object* x_6;
x_6 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_6;
lean_dec(x_1);
return x_4;
}
else
{
lean_dec(x_5);
lean_dec(x_1);
return x_4;
lean_object* x_8;
x_8 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_8;
}
}
}
@ -1940,22 +1943,24 @@ return x_5;
lean_object* l_Lean_Parser_Level_ident___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_maxPrec;
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_object* x_6;
x_6 = l_Lean_Parser_ident___elambda__1(x_1, x_4);
return x_6;
lean_dec(x_1);
return x_4;
}
else
{
lean_dec(x_5);
lean_dec(x_1);
return x_4;
lean_object* x_8;
x_8 = l_Lean_Parser_ident___elambda__1(x_1, x_4);
return x_8;
}
}
}
@ -2130,50 +2135,53 @@ return x_3;
lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = lean_unsigned_to_nat(65u);
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_9 = l_Lean_Parser_Level_addLit___elambda__1___closed__5;
lean_inc(x_1);
x_10 = l_Lean_Parser_symbolFnAux(x_8, x_9, x_1, x_4);
x_11 = lean_ctor_get(x_10, 3);
lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = l_Lean_Parser_numLit___elambda__1(x_1, x_10);
x_13 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_14 = l_Lean_Parser_ParserState_mkTrailingNode(x_12, x_13, x_7);
lean_dec(x_7);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
lean_dec(x_11);
lean_dec(x_1);
x_15 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_15, x_7);
lean_dec(x_7);
return x_16;
}
}
else
{
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_8 = lean_ctor_get(x_4, 0);
lean_inc(x_8);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_11 = l_Lean_Parser_Level_addLit___elambda__1___closed__5;
lean_inc(x_1);
x_12 = l_Lean_Parser_symbolFnAux(x_10, x_11, x_1, x_4);
x_13 = lean_ctor_get(x_12, 3);
lean_inc(x_13);
x_14 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_13, x_6);
lean_dec(x_13);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16;
lean_dec(x_1);
x_15 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_12, x_15, x_9);
lean_dec(x_9);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = l_Lean_Parser_numLit___elambda__1(x_1, x_12);
x_18 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_17, x_18, x_9);
lean_dec(x_9);
return x_19;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Level_addLit___closed__1() {

106
stage0/stdlib/Lean/Parser/StrInterpolation.c generated
View file

@ -46,6 +46,7 @@ lean_object* l_Lean_Parser_interpolatedStr___closed__1;
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
uint8_t l_Lean_Parser_interpolatedStrFn_parse___lambda__1(uint32_t);
lean_object* l_Lean_Parser_interpolatedStr___elambda__1(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Parser_interpolatedStrFn_parse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
@ -151,7 +152,7 @@ goto _start;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_19 = l_Lean_interpolatedStrLitKind;
x_20 = l_Lean_Parser_mkNodeToken(x_19, x_4, x_5, x_11);
lean_inc(x_1);
@ -159,88 +160,93 @@ lean_inc(x_5);
x_21 = lean_apply_2(x_1, x_5, x_20);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
x_24 = l_Lean_Parser_interpolatedStrFn_parse___closed__1;
x_25 = l_Lean_Parser_interpolatedStrFn_parse___closed__2;
x_26 = l_Lean_Parser_satisfyFn(x_24, x_25, x_5, x_21);
x_27 = lean_ctor_get(x_26, 3);
lean_inc(x_27);
if (lean_obj_tag(x_27) == 0)
{
x_4 = x_23;
x_6 = x_26;
goto _start;
}
else
{
lean_dec(x_27);
lean_dec(x_23);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
return x_26;
}
}
else
{
x_23 = lean_box(0);
x_24 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_22, x_23);
lean_dec(x_22);
if (x_24 == 0)
{
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
return x_21;
}
}
else
{
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_25 = lean_ctor_get(x_21, 1);
lean_inc(x_25);
x_26 = l_Lean_Parser_interpolatedStrFn_parse___closed__1;
x_27 = l_Lean_Parser_interpolatedStrFn_parse___closed__2;
x_28 = l_Lean_Parser_satisfyFn(x_26, x_27, x_5, x_21);
x_29 = lean_ctor_get(x_28, 3);
lean_inc(x_29);
x_30 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_29, x_23);
lean_dec(x_29);
if (x_30 == 0)
{
lean_dec(x_25);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_1);
return x_28;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = l_Lean_Parser_interpolatedStrFn_parse___closed__3;
x_30 = l_Lean_Parser_quotedCharCoreFn(x_29, x_5, x_11);
x_31 = lean_ctor_get(x_30, 3);
lean_inc(x_31);
if (lean_obj_tag(x_31) == 0)
{
x_6 = x_30;
x_4 = x_25;
x_6 = x_28;
goto _start;
}
}
}
}
else
{
lean_dec(x_31);
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_32 = l_Lean_Parser_interpolatedStrFn_parse___closed__3;
x_33 = l_Lean_Parser_quotedCharCoreFn(x_32, x_5, x_11);
x_34 = lean_ctor_get(x_33, 3);
lean_inc(x_34);
x_35 = lean_box(0);
x_36 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_34, x_35);
lean_dec(x_34);
if (x_36 == 0)
{
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
return x_30;
return x_33;
}
else
{
x_6 = x_33;
goto _start;
}
}
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
lean_dec(x_1);
x_33 = l_Lean_interpolatedStrLitKind;
x_34 = l_Lean_Parser_mkNodeToken(x_33, x_4, x_5, x_11);
x_38 = l_Lean_interpolatedStrLitKind;
x_39 = l_Lean_Parser_mkNodeToken(x_38, x_4, x_5, x_11);
lean_dec(x_5);
x_35 = l_Lean_interpolatedStrKind;
x_36 = l_Lean_Parser_ParserState_mkNode(x_34, x_35, x_3);
return x_36;
x_40 = l_Lean_interpolatedStrKind;
x_41 = l_Lean_Parser_ParserState_mkNode(x_39, x_40, x_3);
return x_41;
}
}
else
{
lean_object* x_37; lean_object* x_38;
lean_object* x_42; lean_object* x_43;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_37 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
x_38 = l_Lean_Parser_ParserState_mkUnexpectedError(x_6, x_37);
return x_38;
x_42 = l_Lean_Parser_ParserState_mkEOIError___closed__1;
x_43 = l_Lean_Parser_ParserState_mkUnexpectedError(x_6, x_42);
return x_43;
}
}
}

302
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -1161,6 +1161,7 @@ lean_object* l_Lean_Parser_Syntax_sepBy_formatter___closed__9;
lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__5;
lean_object* l_Lean_Parser_Command_syntaxAbbrev___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_optKind___closed__2;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_notationItem_formatter___closed__4;
lean_object* l_Lean_Parser_Command_elabArg_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
@ -1992,22 +1993,24 @@ return x_1;
lean_object* l_Lean_Parser_Syntax_numPrec___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_maxPrec;
x_4 = l_Lean_Parser_checkPrecFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_object* x_6;
x_6 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_6;
lean_dec(x_1);
return x_4;
}
else
{
lean_dec(x_5);
lean_dec(x_1);
return x_4;
lean_object* x_8;
x_8 = l_Lean_Parser_numLit___elambda__1(x_1, x_4);
return x_8;
}
}
}
@ -9503,43 +9506,46 @@ return x_3;
lean_object* l_Lean_Parser_Command_notationItem___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_ctor_get(x_2, 3);
lean_inc(x_3);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = l_Lean_Parser_Command_notationItem___elambda__1___closed__4;
x_5 = lean_ctor_get(x_4, 1);
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_Command_notationItem___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
x_5 = lean_ctor_get(x_2, 3);
lean_inc(x_5);
lean_inc(x_2);
lean_inc(x_1);
x_6 = l_Lean_Parser_tryAnti(x_1, x_2);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10;
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
x_7 = l_Lean_Parser_strLit___closed__2;
x_8 = l_Lean_Parser_Command_identPrec___closed__4;
x_9 = 1;
x_10 = l_Lean_Parser_orelseFnCore(x_7, x_8, x_9, x_1, x_2);
return x_10;
}
else
if (x_7 == 0)
{
lean_object* x_11; uint8_t x_12; lean_object* x_13;
x_11 = l_Lean_Parser_Command_notationItem___elambda__1___closed__5;
x_12 = 1;
x_13 = l_Lean_Parser_orelseFnCore(x_5, x_11, x_12, x_1, x_2);
return x_13;
}
}
else
{
lean_dec(x_3);
lean_dec(x_4);
lean_dec(x_1);
return x_2;
}
else
{
uint8_t x_8;
lean_inc(x_2);
lean_inc(x_1);
x_8 = l_Lean_Parser_tryAnti(x_1, x_2);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
lean_dec(x_4);
x_9 = l_Lean_Parser_strLit___closed__2;
x_10 = l_Lean_Parser_Command_identPrec___closed__4;
x_11 = 1;
x_12 = l_Lean_Parser_orelseFnCore(x_9, x_10, x_11, x_1, x_2);
return x_12;
}
else
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
x_13 = l_Lean_Parser_Command_notationItem___elambda__1___closed__5;
x_14 = 1;
x_15 = l_Lean_Parser_orelseFnCore(x_4, x_13, x_14, x_1, x_2);
return x_15;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Command_notationItem___closed__1() {
@ -13567,41 +13573,44 @@ return x_3;
lean_object* l_Lean_Parser_Command_macroTailTactic___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_Command_macroTailTactic___elambda__1___closed__2;
lean_inc(x_1);
x_4 = l_Lean_Parser_atomicFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7;
lean_inc(x_1);
x_6 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_8 = l_Lean_Parser_Command_macroTailTactic___elambda__1___closed__3;
x_9 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_10 = 1;
x_11 = l_Lean_Parser_orelseFnCore(x_8, x_9, x_10, x_1, x_6);
return x_11;
}
else
{
lean_dec(x_7);
lean_dec(x_1);
return x_6;
}
}
else
{
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc(x_1);
x_8 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
x_10 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_9, x_6);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_1);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_11 = l_Lean_Parser_Command_macroTailTactic___elambda__1___closed__3;
x_12 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_13 = 1;
x_14 = l_Lean_Parser_orelseFnCore(x_11, x_12, x_13, x_1, x_8);
return x_14;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Command_macroTailTactic___closed__1() {
@ -13745,41 +13754,44 @@ return x_3;
lean_object* l_Lean_Parser_Command_macroTailCommand___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_Command_macroTailCommand___elambda__1___closed__2;
lean_inc(x_1);
x_4 = l_Lean_Parser_atomicFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7;
lean_inc(x_1);
x_6 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_8 = l_Lean_Parser_Command_macroTailCommand___elambda__1___closed__5;
x_9 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_10 = 1;
x_11 = l_Lean_Parser_orelseFnCore(x_8, x_9, x_10, x_1, x_6);
return x_11;
}
else
{
lean_dec(x_7);
lean_dec(x_1);
return x_6;
}
}
else
{
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc(x_1);
x_8 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
x_10 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_9, x_6);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_1);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_11 = l_Lean_Parser_Command_macroTailCommand___elambda__1___closed__5;
x_12 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_13 = 1;
x_14 = l_Lean_Parser_orelseFnCore(x_11, x_12, x_13, x_1, x_8);
return x_14;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Command_macroTailCommand___closed__1() {
@ -13913,41 +13925,44 @@ return x_3;
lean_object* l_Lean_Parser_Command_macroTailDefault___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_Command_syntax___elambda__1___closed__4;
lean_inc(x_1);
x_4 = l_Lean_Parser_atomicFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7;
lean_inc(x_1);
x_6 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_8 = l_Lean_Parser_Command_macroTailDefault___elambda__1___closed__4;
x_9 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_10 = 1;
x_11 = l_Lean_Parser_orelseFnCore(x_8, x_9, x_10, x_1, x_6);
return x_11;
}
else
{
lean_dec(x_7);
lean_dec(x_1);
return x_6;
}
}
else
{
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc(x_1);
x_8 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
x_10 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_9, x_6);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_1);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_11 = l_Lean_Parser_Command_macroTailDefault___elambda__1___closed__4;
x_12 = l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__2;
x_13 = 1;
x_14 = l_Lean_Parser_orelseFnCore(x_11, x_12, x_13, x_1, x_8);
return x_14;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Command_macroTailDefault___closed__1() {
@ -16147,40 +16162,43 @@ return x_3;
lean_object* l_Lean_Parser_Command_elabTail___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = l_Lean_Parser_Command_elabTail___elambda__1___closed__9;
lean_inc(x_1);
x_4 = l_Lean_Parser_atomicFn(x_3, x_1, x_2);
x_5 = lean_ctor_get(x_4, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7;
lean_inc(x_1);
x_6 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_term___u2218_____closed__6;
x_9 = lean_unsigned_to_nat(0u);
x_10 = l_Lean_Parser_categoryParser___elambda__1(x_8, x_9, x_1, x_6);
return x_10;
}
else
{
lean_dec(x_7);
lean_dec(x_1);
return x_6;
}
}
else
{
x_6 = lean_box(0);
x_7 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_5, x_6);
lean_dec(x_5);
if (x_7 == 0)
{
lean_dec(x_1);
return x_4;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
lean_inc(x_1);
x_8 = l_Lean_Parser_darrow___elambda__1(x_1, x_4);
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
x_10 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_9, x_6);
lean_dec(x_9);
if (x_10 == 0)
{
lean_dec(x_1);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = l_term___u2218_____closed__6;
x_12 = lean_unsigned_to_nat(0u);
x_13 = l_Lean_Parser_categoryParser___elambda__1(x_11, x_12, x_1, x_8);
return x_13;
}
}
}
}
static lean_object* _init_l_Lean_Parser_Command_elabTail___closed__1() {

341
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -80,6 +80,7 @@ extern lean_object* l_Lean_PrettyPrinter_Formatter_formatterAliasesRef;
lean_object* l___regBuiltin_Lean_Parser_Tactic_nestedTactic_parenthesizer___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Tactic_unknown_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Tactic_tacticSeq;
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Tactic_unknown_parenthesizer___closed__2;
@ -238,7 +239,7 @@ uint8_t x_8;
x_8 = !lean_is_exclusive(x_5);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_9 = lean_ctor_get(x_2, 1);
lean_inc(x_9);
x_10 = lean_alloc_ctor(1, 1, 0);
@ -248,228 +249,236 @@ lean_inc(x_1);
x_11 = l_Lean_Parser_ident___elambda__1(x_1, x_2);
x_12 = lean_ctor_get(x_11, 3);
lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
x_13 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_14 = 1;
x_15 = l_Lean_Parser_errorAtSavedPosFn(x_13, x_14, x_1, x_11);
return x_15;
}
else
{
x_13 = lean_box(0);
x_14 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_12, x_13);
lean_dec(x_12);
if (x_14 == 0)
{
lean_dec(x_1);
return x_11;
}
else
{
lean_object* x_15; uint8_t x_16; lean_object* x_17;
x_15 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_16 = 1;
x_17 = l_Lean_Parser_errorAtSavedPosFn(x_15, x_16, x_1, x_11);
return x_17;
}
}
else
{
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;
x_16 = lean_ctor_get(x_5, 0);
x_17 = lean_ctor_get(x_5, 1);
x_18 = lean_ctor_get(x_5, 2);
x_19 = lean_ctor_get(x_5, 3);
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; uint8_t x_28;
x_18 = lean_ctor_get(x_5, 0);
x_19 = lean_ctor_get(x_5, 1);
x_20 = lean_ctor_get(x_5, 2);
x_21 = lean_ctor_get(x_5, 3);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_5);
x_20 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_20, 0, x_16);
lean_ctor_set(x_20, 1, x_17);
lean_ctor_set(x_20, 2, x_18);
lean_ctor_set(x_20, 3, x_19);
x_21 = lean_ctor_get(x_2, 1);
lean_inc(x_21);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_1, 4, x_22);
lean_ctor_set(x_1, 1, x_20);
x_22 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_22, 0, x_18);
lean_ctor_set(x_22, 1, x_19);
lean_ctor_set(x_22, 2, x_20);
lean_ctor_set(x_22, 3, x_21);
x_23 = lean_ctor_get(x_2, 1);
lean_inc(x_23);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_1, 4, x_24);
lean_ctor_set(x_1, 1, x_22);
lean_inc(x_1);
x_23 = l_Lean_Parser_ident___elambda__1(x_1, x_2);
x_24 = lean_ctor_get(x_23, 3);
lean_inc(x_24);
if (lean_obj_tag(x_24) == 0)
x_25 = l_Lean_Parser_ident___elambda__1(x_1, x_2);
x_26 = lean_ctor_get(x_25, 3);
lean_inc(x_26);
x_27 = lean_box(0);
x_28 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_26, x_27);
lean_dec(x_26);
if (x_28 == 0)
{
lean_object* x_25; uint8_t x_26; lean_object* x_27;
x_25 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_26 = 1;
x_27 = l_Lean_Parser_errorAtSavedPosFn(x_25, x_26, x_1, x_23);
return x_27;
}
else
{
lean_dec(x_24);
lean_dec(x_1);
return x_23;
return x_25;
}
else
{
lean_object* x_29; uint8_t x_30; lean_object* x_31;
x_29 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_30 = 1;
x_31 = l_Lean_Parser_errorAtSavedPosFn(x_29, x_30, x_1, x_25);
return x_31;
}
}
}
else
{
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; lean_object* x_40; lean_object* x_41;
x_28 = lean_ctor_get(x_4, 0);
x_29 = lean_ctor_get(x_4, 1);
x_30 = lean_ctor_get(x_4, 2);
lean_inc(x_30);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_4);
x_31 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_31, 0, x_28);
lean_ctor_set(x_31, 1, x_29);
lean_ctor_set(x_31, 2, x_30);
x_32 = lean_ctor_get(x_5, 0);
lean_inc(x_32);
x_33 = lean_ctor_get(x_5, 1);
lean_inc(x_33);
x_34 = lean_ctor_get(x_5, 2);
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; 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; uint8_t x_47;
x_32 = lean_ctor_get(x_4, 0);
x_33 = lean_ctor_get(x_4, 1);
x_34 = lean_ctor_get(x_4, 2);
lean_inc(x_34);
x_35 = lean_ctor_get(x_5, 3);
lean_inc(x_35);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_4);
x_35 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_35, 0, x_32);
lean_ctor_set(x_35, 1, x_33);
lean_ctor_set(x_35, 2, x_34);
x_36 = lean_ctor_get(x_5, 0);
lean_inc(x_36);
x_37 = lean_ctor_get(x_5, 1);
lean_inc(x_37);
x_38 = lean_ctor_get(x_5, 2);
lean_inc(x_38);
x_39 = lean_ctor_get(x_5, 3);
lean_inc(x_39);
if (lean_is_exclusive(x_5)) {
lean_ctor_release(x_5, 0);
lean_ctor_release(x_5, 1);
lean_ctor_release(x_5, 2);
lean_ctor_release(x_5, 3);
x_36 = x_5;
x_40 = x_5;
} else {
lean_dec_ref(x_5);
x_36 = lean_box(0);
x_40 = lean_box(0);
}
if (lean_is_scalar(x_36)) {
x_37 = lean_alloc_ctor(0, 4, 0);
if (lean_is_scalar(x_40)) {
x_41 = lean_alloc_ctor(0, 4, 0);
} else {
x_37 = x_36;
x_41 = x_40;
}
lean_ctor_set(x_37, 0, x_32);
lean_ctor_set(x_37, 1, x_33);
lean_ctor_set(x_37, 2, x_34);
lean_ctor_set(x_37, 3, x_35);
x_38 = lean_ctor_get(x_2, 1);
lean_inc(x_38);
x_39 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_1, 4, x_39);
lean_ctor_set(x_1, 1, x_37);
lean_ctor_set(x_1, 0, x_31);
lean_ctor_set(x_41, 0, x_36);
lean_ctor_set(x_41, 1, x_37);
lean_ctor_set(x_41, 2, x_38);
lean_ctor_set(x_41, 3, x_39);
x_42 = lean_ctor_get(x_2, 1);
lean_inc(x_42);
x_43 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_1, 4, x_43);
lean_ctor_set(x_1, 1, x_41);
lean_ctor_set(x_1, 0, x_35);
lean_inc(x_1);
x_40 = l_Lean_Parser_ident___elambda__1(x_1, x_2);
x_41 = lean_ctor_get(x_40, 3);
lean_inc(x_41);
if (lean_obj_tag(x_41) == 0)
x_44 = l_Lean_Parser_ident___elambda__1(x_1, x_2);
x_45 = lean_ctor_get(x_44, 3);
lean_inc(x_45);
x_46 = lean_box(0);
x_47 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_45, x_46);
lean_dec(x_45);
if (x_47 == 0)
{
lean_object* x_42; uint8_t x_43; lean_object* x_44;
x_42 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_43 = 1;
x_44 = l_Lean_Parser_errorAtSavedPosFn(x_42, x_43, x_1, x_40);
lean_dec(x_1);
return x_44;
}
else
{
lean_dec(x_41);
lean_dec(x_1);
return x_40;
lean_object* x_48; uint8_t x_49; lean_object* x_50;
x_48 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_49 = 1;
x_50 = l_Lean_Parser_errorAtSavedPosFn(x_48, x_49, x_1, x_44);
return x_50;
}
}
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49; uint8_t 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; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_45 = lean_ctor_get(x_1, 0);
x_46 = lean_ctor_get(x_1, 1);
x_47 = lean_ctor_get(x_1, 2);
x_48 = lean_ctor_get(x_1, 3);
x_49 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_50 = lean_ctor_get_uint8(x_1, sizeof(void*)*6 + 1);
x_51 = lean_ctor_get(x_1, 5);
lean_inc(x_51);
lean_inc(x_48);
lean_inc(x_47);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_1);
x_52 = lean_ctor_get(x_45, 0);
lean_inc(x_52);
x_53 = lean_ctor_get(x_45, 1);
lean_inc(x_53);
x_54 = lean_ctor_get(x_45, 2);
lean_inc(x_54);
if (lean_is_exclusive(x_45)) {
lean_ctor_release(x_45, 0);
lean_ctor_release(x_45, 1);
lean_ctor_release(x_45, 2);
x_55 = x_45;
} else {
lean_dec_ref(x_45);
x_55 = lean_box(0);
}
if (lean_is_scalar(x_55)) {
x_56 = lean_alloc_ctor(0, 3, 0);
} else {
x_56 = x_55;
}
lean_ctor_set(x_56, 0, x_52);
lean_ctor_set(x_56, 1, x_53);
lean_ctor_set(x_56, 2, x_54);
x_57 = lean_ctor_get(x_46, 0);
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; uint8_t x_55; uint8_t x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; uint8_t x_75;
x_51 = lean_ctor_get(x_1, 0);
x_52 = lean_ctor_get(x_1, 1);
x_53 = lean_ctor_get(x_1, 2);
x_54 = lean_ctor_get(x_1, 3);
x_55 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_56 = lean_ctor_get_uint8(x_1, sizeof(void*)*6 + 1);
x_57 = lean_ctor_get(x_1, 5);
lean_inc(x_57);
x_58 = lean_ctor_get(x_46, 1);
lean_inc(x_54);
lean_inc(x_53);
lean_inc(x_52);
lean_inc(x_51);
lean_dec(x_1);
x_58 = lean_ctor_get(x_51, 0);
lean_inc(x_58);
x_59 = lean_ctor_get(x_46, 2);
x_59 = lean_ctor_get(x_51, 1);
lean_inc(x_59);
x_60 = lean_ctor_get(x_46, 3);
x_60 = lean_ctor_get(x_51, 2);
lean_inc(x_60);
if (lean_is_exclusive(x_46)) {
lean_ctor_release(x_46, 0);
lean_ctor_release(x_46, 1);
lean_ctor_release(x_46, 2);
lean_ctor_release(x_46, 3);
x_61 = x_46;
if (lean_is_exclusive(x_51)) {
lean_ctor_release(x_51, 0);
lean_ctor_release(x_51, 1);
lean_ctor_release(x_51, 2);
x_61 = x_51;
} else {
lean_dec_ref(x_46);
lean_dec_ref(x_51);
x_61 = lean_box(0);
}
if (lean_is_scalar(x_61)) {
x_62 = lean_alloc_ctor(0, 4, 0);
x_62 = lean_alloc_ctor(0, 3, 0);
} else {
x_62 = x_61;
}
lean_ctor_set(x_62, 0, x_57);
lean_ctor_set(x_62, 1, x_58);
lean_ctor_set(x_62, 2, x_59);
lean_ctor_set(x_62, 3, x_60);
x_63 = lean_ctor_get(x_2, 1);
lean_ctor_set(x_62, 0, x_58);
lean_ctor_set(x_62, 1, x_59);
lean_ctor_set(x_62, 2, x_60);
x_63 = lean_ctor_get(x_52, 0);
lean_inc(x_63);
x_64 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_64, 0, x_63);
x_65 = lean_alloc_ctor(0, 6, 2);
lean_ctor_set(x_65, 0, x_56);
lean_ctor_set(x_65, 1, x_62);
lean_ctor_set(x_65, 2, x_47);
lean_ctor_set(x_65, 3, x_48);
lean_ctor_set(x_65, 4, x_64);
lean_ctor_set(x_65, 5, x_51);
lean_ctor_set_uint8(x_65, sizeof(void*)*6, x_49);
lean_ctor_set_uint8(x_65, sizeof(void*)*6 + 1, x_50);
x_64 = lean_ctor_get(x_52, 1);
lean_inc(x_64);
x_65 = lean_ctor_get(x_52, 2);
lean_inc(x_65);
x_66 = l_Lean_Parser_ident___elambda__1(x_65, x_2);
x_67 = lean_ctor_get(x_66, 3);
lean_inc(x_67);
if (lean_obj_tag(x_67) == 0)
x_66 = lean_ctor_get(x_52, 3);
lean_inc(x_66);
if (lean_is_exclusive(x_52)) {
lean_ctor_release(x_52, 0);
lean_ctor_release(x_52, 1);
lean_ctor_release(x_52, 2);
lean_ctor_release(x_52, 3);
x_67 = x_52;
} else {
lean_dec_ref(x_52);
x_67 = lean_box(0);
}
if (lean_is_scalar(x_67)) {
x_68 = lean_alloc_ctor(0, 4, 0);
} else {
x_68 = x_67;
}
lean_ctor_set(x_68, 0, x_63);
lean_ctor_set(x_68, 1, x_64);
lean_ctor_set(x_68, 2, x_65);
lean_ctor_set(x_68, 3, x_66);
x_69 = lean_ctor_get(x_2, 1);
lean_inc(x_69);
x_70 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_70, 0, x_69);
x_71 = lean_alloc_ctor(0, 6, 2);
lean_ctor_set(x_71, 0, x_62);
lean_ctor_set(x_71, 1, x_68);
lean_ctor_set(x_71, 2, x_53);
lean_ctor_set(x_71, 3, x_54);
lean_ctor_set(x_71, 4, x_70);
lean_ctor_set(x_71, 5, x_57);
lean_ctor_set_uint8(x_71, sizeof(void*)*6, x_55);
lean_ctor_set_uint8(x_71, sizeof(void*)*6 + 1, x_56);
lean_inc(x_71);
x_72 = l_Lean_Parser_ident___elambda__1(x_71, x_2);
x_73 = lean_ctor_get(x_72, 3);
lean_inc(x_73);
x_74 = lean_box(0);
x_75 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____at_Lean_Parser_ParserState_hasError___spec__1(x_73, x_74);
lean_dec(x_73);
if (x_75 == 0)
{
lean_object* x_68; uint8_t x_69; lean_object* x_70;
x_68 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_69 = 1;
x_70 = l_Lean_Parser_errorAtSavedPosFn(x_68, x_69, x_65, x_66);
return x_70;
lean_dec(x_71);
return x_72;
}
else
{
lean_dec(x_67);
lean_dec(x_65);
return x_66;
lean_object* x_76; uint8_t x_77; lean_object* x_78;
x_76 = l_Lean_Parser_Tactic_unknown___elambda__1___lambda__1___closed__1;
x_77 = 1;
x_78 = l_Lean_Parser_errorAtSavedPosFn(x_76, x_77, x_71, x_72);
return x_78;
}
}
}

3977
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff

1586
stage0/stdlib/Lean/Parser/Transform.c generated
View file

File diff suppressed because it is too large Load diff

330
stage0/stdlib/Lean/Server/ServerBin.c generated
View file

@ -1,330 +0,0 @@
// Lean compiler output
// Module: Lean.Server.ServerBin
// Imports: Init Init.System.IO Lean.Server
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_get_stdin(lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* _lean_main(lean_object*, lean_object*);
lean_object* lean_get_stderr(lean_object*);
lean_object* l_main___boxed__const__1;
lean_object* l_IO_getStdin___at_main___spec__1(lean_object*);
lean_object* lean_init_search_path(lean_object*, lean_object*);
lean_object* lean_get_stdout(lean_object*);
lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_initAndRunServer(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_getStdin___at_main___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_get_stdin(x_1);
return x_2;
}
}
static lean_object* _init_l_main___boxed__const__1() {
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = lean_box_uint32(x_1);
return x_2;
}
}
lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_get_stdin(x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_get_stdout(x_5);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_get_stderr(x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_box(0);
x_13 = lean_init_search_path(x_12, x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Server_initAndRunServer(x_4, x_7, x_14);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_16;
lean_dec(x_10);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_15, 0);
lean_dec(x_17);
x_18 = l_main___boxed__const__1;
lean_ctor_set(x_15, 0, x_18);
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_dec(x_15);
x_20 = l_main___boxed__const__1;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_15, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_15, 1);
lean_inc(x_23);
lean_dec(x_15);
x_24 = lean_io_error_to_string(x_22);
x_25 = l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(x_10, x_24, x_23);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26;
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_25, 0);
lean_dec(x_27);
x_28 = l_main___boxed__const__1;
lean_ctor_set(x_25, 0, x_28);
return x_25;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
lean_dec(x_25);
x_30 = l_main___boxed__const__1;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
return x_31;
}
}
else
{
uint8_t x_32;
x_32 = !lean_is_exclusive(x_25);
if (x_32 == 0)
{
return x_25;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_25, 0);
x_34 = lean_ctor_get(x_25, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_25);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
}
else
{
uint8_t x_36;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
x_36 = !lean_is_exclusive(x_13);
if (x_36 == 0)
{
return x_13;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_13, 0);
x_38 = lean_ctor_get(x_13, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_13);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}
else
{
uint8_t x_40;
lean_dec(x_7);
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_9);
if (x_40 == 0)
{
return x_9;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_9, 0);
x_42 = lean_ctor_get(x_9, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_9);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
else
{
uint8_t x_44;
lean_dec(x_4);
x_44 = !lean_is_exclusive(x_6);
if (x_44 == 0)
{
return x_6;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_6, 0);
x_46 = lean_ctor_get(x_6, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_6);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}
else
{
uint8_t x_48;
x_48 = !lean_is_exclusive(x_3);
if (x_48 == 0)
{
return x_3;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_3, 0);
x_50 = lean_ctor_get(x_3, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_3);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Lean_Server(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Server_ServerBin(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
lean_mark_persistent(l_main___boxed__const__1);
return lean_io_result_mk_ok(lean_box(0));
}
void lean_initialize();
#if defined(WIN32) || defined(_WIN32)
#include <windows.h>
#endif
int main(int argc, char ** argv) {
#if defined(WIN32) || defined(_WIN32)
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
lean_object* in; lean_object* res;
lean_initialize();
res = initialize_Lean_Server_ServerBin(lean_io_mk_world());
lean_io_mark_end_initialization();
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
lean_init_task_manager();
in = lean_box(0);
int i = argc;
while (i > 1) {
lean_object* n;
i--;
n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
in = n;
}
res = _lean_main(in, lean_io_mk_world());
}
if (lean_io_result_is_ok(res)) {
int ret = lean_unbox(lean_io_result_get_value(res));
lean_dec_ref(res);
return ret;
} else {
lean_io_result_show_error(res);
lean_dec_ref(res);
return 1;
}
}
#ifdef __cplusplus
}
#endif

206
stage0/stdlib/Lean/Util/SCC.c generated
View file

@ -28,12 +28,13 @@ lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_modifyDataOf(lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack(lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC_add_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2;
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__1;
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf_match__1(lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_SCC_scc_match__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SCC_scc_match__1___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3;
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC(lean_object*);
lean_object* l_Std_HashMapImp_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC_add(lean_object*);
@ -45,6 +46,7 @@ lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf___rarg(lean_o
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf_match__1(lean_object*);
uint8_t l_Lean_SCC_Data_onStack___default;
lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SCC_State_stack___default(lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_modifyDataOf___at___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux(lean_object*);
@ -57,6 +59,7 @@ lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC_add_match__1(lean_obje
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_modifyDataOf_match__1(lean_object*);
lean_object* l_instBEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_instMonadStateT___rarg(lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -69,6 +72,7 @@ lean_object* l_Lean_SCC_scc___rarg___lambda__1(lean_object*, lean_object*, lean_
lean_object* l_Std_HashMapImp_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SCC_scc_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_modifyDataOf___at___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_decEq___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_SCC_State_nextIndex___default;
static lean_object* _init_l_Lean_SCC_Data_index_x3f___default() {
@ -1406,10 +1410,28 @@ x_2 = l_StateT_instMonadStateT___rarg(x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Nat_decEq___boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2;
x_2 = lean_alloc_closure((void*)(l_instBEq___rarg), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___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_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_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; uint8_t x_15;
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
@ -1438,163 +1460,73 @@ lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_14 = l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___rarg(x_1, x_2, x_4, x_13);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
if (lean_obj_tag(x_16) == 0)
x_15 = !lean_is_exclusive(x_14);
if (x_15 == 0)
{
lean_object* x_17;
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
lean_dec(x_15);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_14, 1);
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_16 = lean_ctor_get(x_14, 0);
x_17 = lean_ctor_get(x_14, 1);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_14);
x_19 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(x_1, x_2, x_4, x_18);
return x_19;
}
else
{
uint8_t x_20;
lean_dec(x_17);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_20 = !lean_is_exclusive(x_14);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_14, 0);
x_19 = lean_ctor_get(x_16, 0);
lean_inc(x_19);
lean_dec(x_16);
x_20 = l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3;
x_21 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg(x_20, x_18, x_19);
x_22 = lean_unbox(x_21);
lean_dec(x_21);
x_22 = lean_box(0);
lean_ctor_set(x_14, 0, x_22);
return x_14;
}
else
if (x_22 == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_14, 1);
lean_inc(x_23);
lean_dec(x_14);
x_24 = lean_box(0);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_23);
return x_25;
}
}
}
else
{
lean_object* x_26;
x_26 = lean_ctor_get(x_15, 0);
lean_inc(x_26);
lean_dec(x_15);
if (lean_obj_tag(x_26) == 0)
{
uint8_t x_27;
lean_dec(x_16);
lean_object* x_23;
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_27 = !lean_is_exclusive(x_14);
if (x_27 == 0)
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_ctor_get(x_14, 0);
lean_dec(x_28);
x_29 = lean_box(0);
lean_ctor_set(x_14, 0, x_29);
x_23 = lean_box(0);
lean_ctor_set(x_14, 0, x_23);
return x_14;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_14, 1);
lean_inc(x_30);
lean_dec(x_14);
x_31 = lean_box(0);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_30);
return x_32;
}
}
else
{
uint8_t x_33;
x_33 = !lean_is_exclusive(x_14);
if (x_33 == 0)
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38;
x_34 = lean_ctor_get(x_14, 1);
x_35 = lean_ctor_get(x_14, 0);
lean_dec(x_35);
x_36 = lean_ctor_get(x_16, 0);
lean_inc(x_36);
lean_dec(x_16);
x_37 = lean_ctor_get(x_26, 0);
lean_inc(x_37);
lean_dec(x_26);
x_38 = lean_nat_dec_eq(x_36, x_37);
lean_dec(x_37);
lean_dec(x_36);
if (x_38 == 0)
{
lean_object* x_39;
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_39 = lean_box(0);
lean_ctor_set(x_14, 0, x_39);
return x_14;
}
else
{
lean_object* x_40;
lean_object* x_24;
lean_free_object(x_14);
x_40 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(x_1, x_2, x_4, x_34);
return x_40;
x_24 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(x_1, x_2, x_4, x_17);
return x_24;
}
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44;
x_41 = lean_ctor_get(x_14, 1);
lean_inc(x_41);
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_25 = lean_ctor_get(x_14, 0);
x_26 = lean_ctor_get(x_14, 1);
lean_inc(x_26);
lean_inc(x_25);
lean_dec(x_14);
x_42 = lean_ctor_get(x_16, 0);
lean_inc(x_42);
lean_dec(x_16);
x_43 = lean_ctor_get(x_26, 0);
lean_inc(x_43);
lean_dec(x_26);
x_44 = lean_nat_dec_eq(x_42, x_43);
lean_dec(x_43);
lean_dec(x_42);
if (x_44 == 0)
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
x_28 = lean_ctor_get(x_25, 0);
lean_inc(x_28);
lean_dec(x_25);
x_29 = l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3;
x_30 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_649____rarg(x_29, x_27, x_28);
x_31 = lean_unbox(x_30);
lean_dec(x_30);
if (x_31 == 0)
{
lean_object* x_45; lean_object* x_46;
lean_object* x_32; lean_object* x_33;
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_45 = lean_box(0);
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;
x_32 = lean_box(0);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_26);
return x_33;
}
else
{
lean_object* x_47;
x_47 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(x_1, x_2, x_4, x_41);
return x_47;
}
}
lean_object* x_34;
x_34 = l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___rarg(x_1, x_2, x_4, x_26);
return x_34;
}
}
}
@ -1756,6 +1688,10 @@ l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___rarg___closed__1 = _init_l_
lean_mark_persistent(l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___rarg___closed__1);
l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__1 = _init_l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__1();
lean_mark_persistent(l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__1);
l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2 = _init_l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2();
lean_mark_persistent(l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__2);
l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3 = _init_l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3();
lean_mark_persistent(l___private_Lean_Util_SCC_0__Lean_SCC_sccAux___rarg___closed__3);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus