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

chore(stage0): update

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 22:04:51 -07:00
parent c00788a982
commit ff0d184176
5 changed files with 9273 additions and 3931 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

143
src/stage0/init/lean/compiler/ir/boxing.cpp generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: init.lean.compiler.ir.boxing
// Imports: init.control.estate init.control.reader init.lean.compiler.externattr init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars
// Imports: init.control.estate init.control.reader init.lean.runtime init.lean.compiler.externattr init.lean.compiler.ir.basic init.lean.compiler.ir.compilerm init.lean.compiler.ir.freevars
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
@ -39,6 +39,8 @@ obj* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded(obj*, uint8, obj*, obj*, obj*,
obj* l_Nat_mfoldAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_getScrutineeType___boxed(obj*);
obj* l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1;
uint8 l_Lean_IR_ExplicitBoxing_isBoxedName___main(obj*);
uint8 l_Lean_IR_ExplicitBoxing_isBoxedName(obj*);
obj* l_Lean_IR_ExplicitBoxing_run(obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_mkBoxedVersion___boxed(obj*);
obj* l_Lean_IR_ExplicitBoxing_withParams___rarg(obj*, obj*, obj*, obj*);
@ -91,6 +93,7 @@ uint8 nat_dec_eq(obj*, obj*);
}
obj* l_Lean_IR_ExplicitBoxing_withVDecl___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
extern obj* l_Lean_IR_paramInh;
obj* l_Lean_IR_ExplicitBoxing_isBoxedName___main___boxed(obj*);
obj* l_Array_push(obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitBoxing_visitFnBody___main___spec__2(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_LocalContext_getType(obj*, obj*);
@ -98,6 +101,9 @@ obj* l_Array_ummapAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spe
obj* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_boxArgsIfNeeded___spec__2(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_withJDecl___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___spec__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
namespace lean {
uint8 string_dec_eq(obj*, obj*);
}
obj* l_Lean_IR_LocalContext_getJPParams(obj*, obj*);
obj* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_boxArgsIfNeeded___spec__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitBoxing_visitFnBody___main___spec__2___boxed(obj*, obj*, obj*, obj*);
@ -106,6 +112,8 @@ obj* l_Lean_IR_ExplicitBoxing_castResultIfNeeded___boxed(obj*, obj*, obj*, obj*,
obj* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_getJPParams___boxed(obj*, obj*, obj*);
obj* l_Lean_IR_ExplicitBoxing_getLocalContext(obj*, obj*);
extern obj* l_Lean_closureMaxArgs;
obj* l_Lean_IR_ExplicitBoxing_isBoxedName___boxed(obj*);
obj* l_Lean_IR_ExplicitBoxing_mkFresh(obj*);
obj* l_Lean_PersistentEnvExtension_addEntry___rarg(obj*, obj*, obj*);
uint8 l_Lean_IR_ExplicitBoxing_requiresBoxedVersion(obj*, obj*);
@ -169,6 +177,64 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
uint8 l_Lean_IR_ExplicitBoxing_isBoxedName___main(obj* x_1) {
_start:
{
if (lean::obj_tag(x_1) == 1)
{
obj* x_2; obj* x_3; uint8 x_4;
x_2 = lean::cnstr_get(x_1, 1);
x_3 = l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1;
x_4 = lean::string_dec_eq(x_2, x_3);
if (x_4 == 0)
{
uint8 x_5;
x_5 = 0;
return x_5;
}
else
{
uint8 x_6;
x_6 = 1;
return x_6;
}
}
else
{
uint8 x_7;
x_7 = 0;
return x_7;
}
}
}
obj* l_Lean_IR_ExplicitBoxing_isBoxedName___main___boxed(obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = l_Lean_IR_ExplicitBoxing_isBoxedName___main(x_1);
lean::dec(x_1);
x_3 = lean::box(x_2);
return x_3;
}
}
uint8 l_Lean_IR_ExplicitBoxing_isBoxedName(obj* x_1) {
_start:
{
uint8 x_2;
x_2 = l_Lean_IR_ExplicitBoxing_isBoxedName___main(x_1);
return x_2;
}
}
obj* l_Lean_IR_ExplicitBoxing_isBoxedName___boxed(obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = l_Lean_IR_ExplicitBoxing_isBoxedName(x_1);
lean::dec(x_1);
x_3 = lean::box(x_2);
return x_3;
}
}
obj* l___private_init_lean_compiler_ir_boxing_1__mkFresh(obj* x_1) {
_start:
{
@ -250,40 +316,61 @@ x_3 = l_Lean_IR_Decl_params___main(x_2);
x_4 = lean::array_get_size(x_3);
x_5 = lean::mk_nat_obj(0u);
x_6 = lean::nat_dec_lt(x_5, x_4);
lean::dec(x_4);
if (x_6 == 0)
{
uint8 x_7;
obj* x_7; uint8 x_8;
lean::dec(x_3);
x_7 = 0;
return x_7;
x_7 = l_Lean_closureMaxArgs;
x_8 = lean::nat_dec_lt(x_7, x_4);
lean::dec(x_4);
return x_8;
}
else
{
uint8 x_8; uint8 x_9;
x_8 = l_Lean_IR_Decl_resultType___main(x_2);
x_9 = l_Lean_IR_IRType_isScalar___main(x_8);
if (x_9 == 0)
{
uint8 x_10;
x_10 = l_Array_anyMAux___main___at_Lean_IR_ExplicitBoxing_requiresBoxedVersion___spec__1(x_6, x_3, x_5);
lean::dec(x_3);
uint8 x_9; uint8 x_10;
x_9 = l_Lean_IR_Decl_resultType___main(x_2);
x_10 = l_Lean_IR_IRType_isScalar___main(x_9);
if (x_10 == 0)
{
obj* x_11; uint8 x_12;
x_11 = l_Lean_IR_Decl_name___main(x_2);
x_12 = l_Lean_isExtern(x_1, x_11);
return x_12;
}
else
{
return x_6;
}
}
else
{
uint8 x_11;
x_11 = l_Array_anyMAux___main___at_Lean_IR_ExplicitBoxing_requiresBoxedVersion___spec__1(x_6, x_3, x_5);
lean::dec(x_3);
return x_6;
if (x_11 == 0)
{
obj* x_12; uint8 x_13;
x_12 = l_Lean_IR_Decl_name___main(x_2);
x_13 = l_Lean_isExtern(x_1, x_12);
if (x_13 == 0)
{
obj* x_14; uint8 x_15;
x_14 = l_Lean_closureMaxArgs;
x_15 = lean::nat_dec_lt(x_14, x_4);
lean::dec(x_4);
return x_15;
}
else
{
uint8 x_16;
lean::dec(x_4);
x_16 = 1;
return x_16;
}
}
else
{
uint8 x_17;
lean::dec(x_4);
x_17 = 1;
return x_17;
}
}
else
{
uint8 x_18;
lean::dec(x_4);
lean::dec(x_3);
x_18 = 1;
return x_18;
}
}
}
@ -6333,6 +6420,7 @@ return x_4;
}
obj* initialize_init_control_estate(obj*);
obj* initialize_init_control_reader(obj*);
obj* initialize_init_lean_runtime(obj*);
obj* initialize_init_lean_compiler_externattr(obj*);
obj* initialize_init_lean_compiler_ir_basic(obj*);
obj* initialize_init_lean_compiler_ir_compilerm(obj*);
@ -6346,6 +6434,8 @@ w = initialize_init_control_estate(w);
if (io_result_is_error(w)) return w;
w = initialize_init_control_reader(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_runtime(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_compiler_externattr(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_compiler_ir_basic(w);
@ -6357,6 +6447,7 @@ if (io_result_is_error(w)) return w;
l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1 = _init_l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1();
lean::mark_persistent(l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1);
REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "ExplicitBoxing"), "mkBoxedName"), 1, l_Lean_IR_ExplicitBoxing_mkBoxedName);
REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "ExplicitBoxing"), "isBoxedName"), 1, l_Lean_IR_ExplicitBoxing_isBoxedName___boxed);
REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "IR"), "ExplicitBoxing"), "requiresBoxedVersion"), 2, l_Lean_IR_ExplicitBoxing_requiresBoxedVersion___boxed);
l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1 = _init_l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1();
lean::mark_persistent(l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1);

3684
src/stage0/init/lean/compiler/ir/emitcpp.cpp generated
View file

File diff suppressed because it is too large Load diff

539
src/stage0/init/lean/parser/level.cpp generated
View file

@ -17,53 +17,70 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
obj* l_Lean_Parser_addBuiltinLeadingParser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_regBuiltinLevelParserAttr___closed__2;
obj* l_Lean_Parser_Level_paren;
obj* l_Lean_Parser_andthenFn___rarg(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Level_addLit___elambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_symbolInfo(obj*, obj*);
obj* l_Lean_Parser_andthenInfo(obj*, obj*);
obj* l_Lean_Parser_Level_max;
obj* l_Lean_Parser_builtinLevelParsingTable;
extern obj* l_Lean_Parser_appPrec;
obj* l_Lean_Parser_symbolFnAux(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_registerBuiltinParserAttribute(obj*, obj*, obj*);
obj* l_Lean_Parser_Level_addLit;
extern obj* l_Lean_Parser_symbolFn___rarg___closed__1;
obj* l___regBuiltinParser_Lean_Parser_Level_num___closed__1;
obj* l_ExceptT_lift___rarg___lambda__1(obj*);
obj* l_Lean_Parser_levelParserFn(uint8);
obj* l_Lean_Parser_mkAtomicInfo(obj*);
obj* l_Lean_Parser_Level_max___elambda__1(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_levelParser(uint8, obj*);
obj* l_Lean_Parser_Level_num;
obj* l___regBuiltinParser_Lean_Parser_Level_addLit(obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_hole(obj*);
obj* l_Lean_Parser_Level_paren___elambda__1(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_ParserState_mkNode(obj*, obj*, obj*);
obj* l_Lean_Parser_levelParserFn___rarg___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_runBuiltinParserUnsafe(obj*, obj*, obj*, obj*, obj*);
extern obj* l_Lean_Parser_Parser_inhabited___closed__1;
obj* l_Lean_Parser_many1Fn___boxed(obj*, obj*, obj*, obj*, obj*);
namespace lean {
obj* string_append(obj*, obj*);
}
obj* l_Lean_Parser_manyAux___main(uint8, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_addLit___closed__1;
obj* l_Lean_Parser_levelParser___boxed(obj*, obj*);
extern obj* l_Char_HasRepr___closed__1;
extern "C" obj* lean_name_mk_string(obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_imax(obj*);
extern obj* l_Lean_nullKind;
obj* l_Lean_Parser_addBuiltinTrailingParser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_levelParserFn___rarg___closed__1;
obj* l_Lean_Parser_symbolFn___rarg___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_numLitFn___rarg(obj*, obj*);
obj* l_Lean_Parser_ParserState_pushSyntax(obj*, obj*);
obj* l_Lean_Parser_Level_imax;
obj* l___regBuiltinParser_Lean_Parser_Level_hole___closed__1;
obj* l_Lean_Parser_regBuiltinLevelParserAttr(obj*);
obj* l_Lean_Parser_Level_hole___elambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_String_trim(obj*);
obj* l_Lean_Parser_numLitFn___boxed(obj*, obj*);
obj* l_Lean_Parser_levelParserFn___boxed(obj*);
obj* l_Lean_Parser_Level_addLit___elambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Level_hole___elambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_max(obj*);
obj* l_Lean_Parser_nodeInfo(obj*);
obj* l_Array_size(obj*, obj*);
obj* l_Lean_Parser_identFn___boxed(obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_ident___closed__1;
obj* l_Lean_Parser_levelParserFn___rarg(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_regBuiltinLevelParserAttr___closed__1;
obj* l_Lean_Parser_nodeFn___rarg(obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_num(obj*);
obj* l_Lean_Parser_Level_hole;
obj* l_Lean_Parser_Level_max___elambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_paren(obj*);
obj* l_Lean_Parser_Level_ident;
extern obj* l_Lean_Parser_epsilonInfo;
obj* l_Lean_Parser_Level_imax___elambda__1(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_max___closed__1;
obj* l_Lean_Parser_pushLeadingFn___boxed(obj*, obj*, obj*);
obj* l_Lean_Parser_Level_imax___elambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Level_paren___elambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l___regBuiltinParser_Lean_Parser_Level_imax___closed__1;
obj* l___regBuiltinParser_Lean_Parser_Level_paren___closed__1;
obj* l___regBuiltinParser_Lean_Parser_Level_ident(obj*);
@ -170,10 +187,64 @@ x_4 = l_Lean_Parser_levelParser(x_3, x_2);
return x_4;
}
}
obj* l_Lean_Parser_Level_paren___elambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14;
x_7 = lean::cnstr_get(x_6, 0);
lean::inc(x_7);
x_8 = lean::array_get_size(x_7);
lean::dec(x_7);
x_9 = l_Lean_Parser_symbolFn___rarg___closed__1;
x_10 = lean::string_append(x_9, x_2);
x_11 = l_Char_HasRepr___closed__1;
x_12 = lean::string_append(x_10, x_11);
lean::inc(x_5);
x_13 = l_Lean_Parser_symbolFnAux(x_2, x_12, x_5, x_6);
x_14 = lean::cnstr_get(x_13, 3);
lean::inc(x_14);
if (lean::obj_tag(x_14) == 0)
{
obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19;
x_15 = l_Lean_Parser_levelParserFn___rarg___closed__1;
x_16 = l_Lean_Parser_builtinLevelParsingTable;
x_17 = lean::mk_nat_obj(0u);
lean::inc(x_5);
x_18 = l_Lean_Parser_runBuiltinParserUnsafe(x_15, x_16, x_17, x_5, x_13);
x_19 = lean::cnstr_get(x_18, 3);
lean::inc(x_19);
if (lean::obj_tag(x_19) == 0)
{
obj* x_20; obj* x_21; obj* x_22; obj* x_23;
x_20 = lean::string_append(x_9, x_3);
x_21 = lean::string_append(x_20, x_11);
x_22 = l_Lean_Parser_symbolFnAux(x_3, x_21, x_5, x_18);
x_23 = l_Lean_Parser_ParserState_mkNode(x_22, x_1, x_8);
return x_23;
}
else
{
obj* x_24;
lean::dec(x_19);
lean::dec(x_5);
x_24 = l_Lean_Parser_ParserState_mkNode(x_18, x_1, x_8);
return x_24;
}
}
else
{
obj* x_25;
lean::dec(x_14);
lean::dec(x_5);
x_25 = l_Lean_Parser_ParserState_mkNode(x_13, x_1, x_8);
return x_25;
}
}
}
obj* _init_l_Lean_Parser_Level_paren() {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32;
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
x_1 = lean::box(0);
x_2 = lean::mk_string("Lean");
x_3 = lean_name_mk_string(x_1, x_2);
@ -191,40 +262,39 @@ x_13 = l_String_trim(x_12);
lean::dec(x_12);
lean::inc(x_13);
x_14 = l_Lean_Parser_symbolInfo(x_13, x_11);
x_15 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_15, 0, x_13);
x_16 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_17 = lean::box(1);
x_18 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_18, 0, x_16);
lean::cnstr_set(x_18, 1, x_17);
x_19 = lean::mk_nat_obj(0u);
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_levelParserFn___rarg___boxed), 4, 1);
lean::closure_set(x_20, 0, x_19);
x_21 = lean::box(0);
x_22 = lean::mk_string(")");
x_23 = l_String_trim(x_22);
lean::dec(x_22);
lean::inc(x_23);
x_24 = l_Lean_Parser_symbolInfo(x_23, x_21);
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_25, 0, x_23);
x_26 = l_Lean_Parser_andthenInfo(x_18, x_24);
x_27 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_27, 0, x_20);
lean::closure_set(x_27, 1, x_25);
x_28 = l_Lean_Parser_andthenInfo(x_14, x_26);
x_29 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_29, 0, x_15);
lean::closure_set(x_29, 1, x_27);
x_30 = l_Lean_Parser_nodeInfo(x_28);
x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_31, 0, x_9);
lean::closure_set(x_31, 1, x_29);
x_32 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_32, 0, x_30);
lean::cnstr_set(x_32, 1, x_31);
return x_32;
x_15 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_16 = lean::box(1);
x_17 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_17, 0, x_15);
lean::cnstr_set(x_17, 1, x_16);
x_18 = lean::box(0);
x_19 = lean::mk_string(")");
x_20 = l_String_trim(x_19);
lean::dec(x_19);
lean::inc(x_20);
x_21 = l_Lean_Parser_symbolInfo(x_20, x_18);
x_22 = l_Lean_Parser_andthenInfo(x_17, x_21);
x_23 = l_Lean_Parser_andthenInfo(x_14, x_22);
x_24 = l_Lean_Parser_nodeInfo(x_23);
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Level_paren___elambda__1___boxed), 6, 3);
lean::closure_set(x_25, 0, x_9);
lean::closure_set(x_25, 1, x_13);
lean::closure_set(x_25, 2, x_20);
x_26 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_26, 0, x_24);
lean::cnstr_set(x_26, 1, x_25);
return x_26;
}
}
obj* l_Lean_Parser_Level_paren___elambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7;
x_7 = l_Lean_Parser_Level_paren___elambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean::dec(x_4);
lean::dec(x_3);
lean::dec(x_2);
return x_7;
}
}
obj* _init_l___regBuiltinParser_Lean_Parser_Level_paren___closed__1() {
@ -254,10 +324,75 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Parser_Level_max___elambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14;
x_7 = lean::cnstr_get(x_6, 0);
lean::inc(x_7);
x_8 = lean::array_get_size(x_7);
lean::dec(x_7);
x_9 = l_Lean_Parser_symbolFn___rarg___closed__1;
x_10 = lean::string_append(x_9, x_2);
x_11 = l_Char_HasRepr___closed__1;
x_12 = lean::string_append(x_10, x_11);
lean::inc(x_5);
x_13 = l_Lean_Parser_symbolFnAux(x_2, x_12, x_5, x_6);
x_14 = lean::cnstr_get(x_13, 3);
lean::inc(x_14);
if (lean::obj_tag(x_14) == 0)
{
obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21;
x_15 = lean::cnstr_get(x_13, 0);
lean::inc(x_15);
x_16 = lean::array_get_size(x_15);
lean::dec(x_15);
x_17 = l_Lean_Parser_levelParserFn___rarg___closed__1;
x_18 = l_Lean_Parser_builtinLevelParsingTable;
x_19 = l_Lean_Parser_appPrec;
lean::inc(x_5);
x_20 = l_Lean_Parser_runBuiltinParserUnsafe(x_17, x_18, x_19, x_5, x_13);
x_21 = lean::cnstr_get(x_20, 3);
lean::inc(x_21);
if (lean::obj_tag(x_21) == 0)
{
uint8 x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
x_22 = 0;
x_23 = l_Lean_Parser_manyAux___main(x_22, x_3, x_4, x_5, x_20);
x_24 = l_Lean_nullKind;
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_16);
x_26 = l_Lean_Parser_ParserState_mkNode(x_25, x_1, x_8);
return x_26;
}
else
{
obj* x_27; obj* x_28; obj* x_29;
lean::dec(x_21);
lean::dec(x_5);
lean::dec(x_4);
lean::dec(x_3);
x_27 = l_Lean_nullKind;
x_28 = l_Lean_Parser_ParserState_mkNode(x_20, x_27, x_16);
x_29 = l_Lean_Parser_ParserState_mkNode(x_28, x_1, x_8);
return x_29;
}
}
else
{
obj* x_30;
lean::dec(x_14);
lean::dec(x_5);
lean::dec(x_4);
lean::dec(x_3);
x_30 = l_Lean_Parser_ParserState_mkNode(x_13, x_1, x_8);
return x_30;
}
}
}
obj* _init_l_Lean_Parser_Level_max() {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; uint8 x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21;
x_1 = lean::box(0);
x_2 = lean::mk_string("Lean");
x_3 = lean_name_mk_string(x_1, x_2);
@ -273,33 +408,33 @@ x_11 = l_String_trim(x_8);
lean::dec(x_8);
lean::inc(x_11);
x_12 = l_Lean_Parser_symbolInfo(x_11, x_10);
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_13, 0, x_11);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_15 = lean::box(1);
x_16 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_16, 0, x_14);
lean::cnstr_set(x_16, 1, x_15);
x_17 = l_Lean_Parser_appPrec;
x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_levelParserFn___rarg___boxed), 4, 1);
lean::closure_set(x_18, 0, x_17);
x_19 = 0;
x_20 = lean::box(x_19);
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_many1Fn___boxed), 5, 2);
lean::closure_set(x_21, 0, x_20);
lean::closure_set(x_21, 1, x_18);
x_22 = l_Lean_Parser_andthenInfo(x_12, x_16);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_23, 0, x_13);
lean::closure_set(x_23, 1, x_21);
x_24 = l_Lean_Parser_nodeInfo(x_22);
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_25, 0, x_9);
lean::closure_set(x_25, 1, x_23);
x_26 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_26, 0, x_24);
lean::cnstr_set(x_26, 1, x_25);
return x_26;
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_14 = lean::box(1);
x_15 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_15, 0, x_13);
lean::cnstr_set(x_15, 1, x_14);
x_16 = l_Lean_Parser_appPrec;
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_levelParserFn___rarg___boxed), 4, 1);
lean::closure_set(x_17, 0, x_16);
x_18 = l_Lean_Parser_andthenInfo(x_12, x_15);
x_19 = l_Lean_Parser_nodeInfo(x_18);
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Level_max___elambda__1___boxed), 6, 3);
lean::closure_set(x_20, 0, x_9);
lean::closure_set(x_20, 1, x_11);
lean::closure_set(x_20, 2, x_17);
x_21 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_21, 0, x_19);
lean::cnstr_set(x_21, 1, x_20);
return x_21;
}
}
obj* l_Lean_Parser_Level_max___elambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7;
x_7 = l_Lean_Parser_Level_max___elambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean::dec(x_2);
return x_7;
}
}
obj* _init_l___regBuiltinParser_Lean_Parser_Level_max___closed__1() {
@ -329,10 +464,75 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Parser_Level_imax___elambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14;
x_7 = lean::cnstr_get(x_6, 0);
lean::inc(x_7);
x_8 = lean::array_get_size(x_7);
lean::dec(x_7);
x_9 = l_Lean_Parser_symbolFn___rarg___closed__1;
x_10 = lean::string_append(x_9, x_2);
x_11 = l_Char_HasRepr___closed__1;
x_12 = lean::string_append(x_10, x_11);
lean::inc(x_5);
x_13 = l_Lean_Parser_symbolFnAux(x_2, x_12, x_5, x_6);
x_14 = lean::cnstr_get(x_13, 3);
lean::inc(x_14);
if (lean::obj_tag(x_14) == 0)
{
obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21;
x_15 = lean::cnstr_get(x_13, 0);
lean::inc(x_15);
x_16 = lean::array_get_size(x_15);
lean::dec(x_15);
x_17 = l_Lean_Parser_levelParserFn___rarg___closed__1;
x_18 = l_Lean_Parser_builtinLevelParsingTable;
x_19 = l_Lean_Parser_appPrec;
lean::inc(x_5);
x_20 = l_Lean_Parser_runBuiltinParserUnsafe(x_17, x_18, x_19, x_5, x_13);
x_21 = lean::cnstr_get(x_20, 3);
lean::inc(x_21);
if (lean::obj_tag(x_21) == 0)
{
uint8 x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
x_22 = 0;
x_23 = l_Lean_Parser_manyAux___main(x_22, x_3, x_4, x_5, x_20);
x_24 = l_Lean_nullKind;
x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_16);
x_26 = l_Lean_Parser_ParserState_mkNode(x_25, x_1, x_8);
return x_26;
}
else
{
obj* x_27; obj* x_28; obj* x_29;
lean::dec(x_21);
lean::dec(x_5);
lean::dec(x_4);
lean::dec(x_3);
x_27 = l_Lean_nullKind;
x_28 = l_Lean_Parser_ParserState_mkNode(x_20, x_27, x_16);
x_29 = l_Lean_Parser_ParserState_mkNode(x_28, x_1, x_8);
return x_29;
}
}
else
{
obj* x_30;
lean::dec(x_14);
lean::dec(x_5);
lean::dec(x_4);
lean::dec(x_3);
x_30 = l_Lean_Parser_ParserState_mkNode(x_13, x_1, x_8);
return x_30;
}
}
}
obj* _init_l_Lean_Parser_Level_imax() {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; uint8 x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21;
x_1 = lean::box(0);
x_2 = lean::mk_string("Lean");
x_3 = lean_name_mk_string(x_1, x_2);
@ -348,33 +548,33 @@ x_11 = l_String_trim(x_8);
lean::dec(x_8);
lean::inc(x_11);
x_12 = l_Lean_Parser_symbolInfo(x_11, x_10);
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_13, 0, x_11);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_15 = lean::box(1);
x_16 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_16, 0, x_14);
lean::cnstr_set(x_16, 1, x_15);
x_17 = l_Lean_Parser_appPrec;
x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_levelParserFn___rarg___boxed), 4, 1);
lean::closure_set(x_18, 0, x_17);
x_19 = 0;
x_20 = lean::box(x_19);
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_many1Fn___boxed), 5, 2);
lean::closure_set(x_21, 0, x_20);
lean::closure_set(x_21, 1, x_18);
x_22 = l_Lean_Parser_andthenInfo(x_12, x_16);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_23, 0, x_13);
lean::closure_set(x_23, 1, x_21);
x_24 = l_Lean_Parser_nodeInfo(x_22);
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_25, 0, x_9);
lean::closure_set(x_25, 1, x_23);
x_26 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_26, 0, x_24);
lean::cnstr_set(x_26, 1, x_25);
return x_26;
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_ExceptT_lift___rarg___lambda__1), 1, 0);
x_14 = lean::box(1);
x_15 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_15, 0, x_13);
lean::cnstr_set(x_15, 1, x_14);
x_16 = l_Lean_Parser_appPrec;
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_levelParserFn___rarg___boxed), 4, 1);
lean::closure_set(x_17, 0, x_16);
x_18 = l_Lean_Parser_andthenInfo(x_12, x_15);
x_19 = l_Lean_Parser_nodeInfo(x_18);
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Level_imax___elambda__1___boxed), 6, 3);
lean::closure_set(x_20, 0, x_9);
lean::closure_set(x_20, 1, x_11);
lean::closure_set(x_20, 2, x_17);
x_21 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_21, 0, x_19);
lean::cnstr_set(x_21, 1, x_20);
return x_21;
}
}
obj* l_Lean_Parser_Level_imax___elambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_7;
x_7 = l_Lean_Parser_Level_imax___elambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean::dec(x_2);
return x_7;
}
}
obj* _init_l___regBuiltinParser_Lean_Parser_Level_imax___closed__1() {
@ -404,10 +604,27 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Parser_Level_hole___elambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13;
x_6 = lean::cnstr_get(x_5, 0);
lean::inc(x_6);
x_7 = lean::array_get_size(x_6);
lean::dec(x_6);
x_8 = l_Lean_Parser_symbolFn___rarg___closed__1;
x_9 = lean::string_append(x_8, x_2);
x_10 = l_Char_HasRepr___closed__1;
x_11 = lean::string_append(x_9, x_10);
x_12 = l_Lean_Parser_symbolFnAux(x_2, x_11, x_4, x_5);
x_13 = l_Lean_Parser_ParserState_mkNode(x_12, x_1, x_7);
return x_13;
}
}
obj* _init_l_Lean_Parser_Level_hole() {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17;
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16;
x_1 = lean::box(0);
x_2 = lean::mk_string("Lean");
x_3 = lean_name_mk_string(x_1, x_2);
@ -423,16 +640,24 @@ x_12 = l_String_trim(x_11);
lean::dec(x_11);
lean::inc(x_12);
x_13 = l_Lean_Parser_symbolInfo(x_12, x_10);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_14, 0, x_12);
x_15 = l_Lean_Parser_nodeInfo(x_13);
x_16 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_16, 0, x_9);
lean::closure_set(x_16, 1, x_14);
x_17 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_17, 0, x_15);
lean::cnstr_set(x_17, 1, x_16);
return x_17;
x_14 = l_Lean_Parser_nodeInfo(x_13);
x_15 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Level_hole___elambda__1___boxed), 5, 2);
lean::closure_set(x_15, 0, x_9);
lean::closure_set(x_15, 1, x_12);
x_16 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_16, 0, x_14);
lean::cnstr_set(x_16, 1, x_15);
return x_16;
}
}
obj* l_Lean_Parser_Level_hole___elambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6;
x_6 = l_Lean_Parser_Level_hole___elambda__1(x_1, x_2, x_3, x_4, x_5);
lean::dec(x_3);
lean::dec(x_2);
return x_6;
}
}
obj* _init_l___regBuiltinParser_Lean_Parser_Level_hole___closed__1() {
@ -548,10 +773,60 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
obj* l_Lean_Parser_Level_addLit___elambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9;
x_6 = lean::cnstr_get(x_5, 0);
lean::inc(x_6);
x_7 = lean::array_get_size(x_6);
lean::dec(x_6);
lean::inc(x_5);
x_8 = l_Lean_Parser_ParserState_pushSyntax(x_5, x_3);
x_9 = lean::cnstr_get(x_5, 3);
lean::inc(x_9);
lean::dec(x_5);
if (lean::obj_tag(x_9) == 0)
{
obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15;
x_10 = l_Lean_Parser_symbolFn___rarg___closed__1;
x_11 = lean::string_append(x_10, x_2);
x_12 = l_Char_HasRepr___closed__1;
x_13 = lean::string_append(x_11, x_12);
lean::inc(x_4);
x_14 = l_Lean_Parser_symbolFnAux(x_2, x_13, x_4, x_8);
x_15 = lean::cnstr_get(x_14, 3);
lean::inc(x_15);
if (lean::obj_tag(x_15) == 0)
{
obj* x_16; obj* x_17;
x_16 = l_Lean_Parser_numLitFn___rarg(x_4, x_14);
x_17 = l_Lean_Parser_ParserState_mkNode(x_16, x_1, x_7);
return x_17;
}
else
{
obj* x_18;
lean::dec(x_15);
lean::dec(x_4);
x_18 = l_Lean_Parser_ParserState_mkNode(x_14, x_1, x_7);
return x_18;
}
}
else
{
obj* x_19;
lean::dec(x_9);
lean::dec(x_4);
x_19 = l_Lean_Parser_ParserState_mkNode(x_8, x_1, x_7);
return x_19;
}
}
}
obj* _init_l_Lean_Parser_Level_addLit() {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; uint8 x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29;
obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22;
x_1 = lean::box(0);
x_2 = lean::mk_string("Lean");
x_3 = lean_name_mk_string(x_1, x_2);
@ -569,32 +844,28 @@ x_13 = l_String_trim(x_12);
lean::dec(x_12);
lean::inc(x_13);
x_14 = l_Lean_Parser_symbolInfo(x_13, x_11);
x_15 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean::closure_set(x_15, 0, x_13);
x_16 = lean::mk_string("numLit");
x_17 = l_Lean_Parser_mkAtomicInfo(x_16);
x_18 = 1;
x_19 = lean::box(x_18);
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_numLitFn___boxed), 2, 1);
lean::closure_set(x_20, 0, x_19);
x_21 = l_Lean_Parser_andthenInfo(x_14, x_17);
x_22 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_22, 0, x_15);
lean::closure_set(x_22, 1, x_20);
x_23 = l_Lean_Parser_epsilonInfo;
x_24 = l_Lean_Parser_andthenInfo(x_23, x_21);
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_pushLeadingFn___boxed), 3, 0);
x_26 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_andthenFn___rarg), 5, 2);
lean::closure_set(x_26, 0, x_25);
lean::closure_set(x_26, 1, x_22);
x_27 = l_Lean_Parser_nodeInfo(x_24);
x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_28, 0, x_9);
lean::closure_set(x_28, 1, x_26);
x_29 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_29, 0, x_27);
lean::cnstr_set(x_29, 1, x_28);
return x_29;
x_15 = lean::mk_string("numLit");
x_16 = l_Lean_Parser_mkAtomicInfo(x_15);
x_17 = l_Lean_Parser_andthenInfo(x_14, x_16);
x_18 = l_Lean_Parser_epsilonInfo;
x_19 = l_Lean_Parser_andthenInfo(x_18, x_17);
x_20 = l_Lean_Parser_nodeInfo(x_19);
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Level_addLit___elambda__1___boxed), 5, 2);
lean::closure_set(x_21, 0, x_9);
lean::closure_set(x_21, 1, x_13);
x_22 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_22, 0, x_20);
lean::cnstr_set(x_22, 1, x_21);
return x_22;
}
}
obj* l_Lean_Parser_Level_addLit___elambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6;
x_6 = l_Lean_Parser_Level_addLit___elambda__1(x_1, x_2, x_3, x_4, x_5);
lean::dec(x_2);
return x_6;
}
}
obj* _init_l___regBuiltinParser_Lean_Parser_Level_addLit___closed__1() {

74
src/stage0/init/lean/parser/parser.cpp generated
View file

@ -397,6 +397,7 @@ obj* l_Lean_Parser_many(uint8, obj*);
obj* l_Lean_Parser_finishCommentBlock___main(obj*, obj*, obj*);
uint8 l_Lean_Parser_TokenConfig_beq(obj*, obj*);
obj* l___private_init_lean_parser_parser_4__tokenFnAux(obj*, obj*);
obj* l_Lean_Parser_node___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_mkCApp(obj*, obj*);
obj* l_Lean_Parser_numLitFn___rarg(obj*, obj*);
obj* l_Lean_Parser_noFirstTokenInfo(obj*);
@ -2292,23 +2293,36 @@ return x_5;
}
}
}
obj* l_Lean_Parser_node___lambda__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10;
x_6 = lean::cnstr_get(x_1, 1);
lean::inc(x_6);
lean::dec(x_1);
x_7 = lean::cnstr_get(x_5, 0);
lean::inc(x_7);
x_8 = lean::array_get_size(x_7);
lean::dec(x_7);
x_9 = lean::apply_3(x_6, x_3, x_4, x_5);
x_10 = l_Lean_Parser_ParserState_mkNode(x_9, x_2, x_8);
return x_10;
}
}
obj* l_Lean_Parser_node(uint8 x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8;
obj* x_4; obj* x_5; obj* x_6; obj* x_7;
x_4 = lean::cnstr_get(x_3, 0);
lean::inc(x_4);
x_5 = l_Lean_Parser_nodeInfo(x_4);
x_6 = lean::cnstr_get(x_3, 1);
lean::inc(x_6);
lean::dec(x_3);
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_7, 0, x_2);
lean::closure_set(x_7, 1, x_6);
x_8 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_8, 0, x_5);
lean::cnstr_set(x_8, 1, x_7);
return x_8;
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_node___lambda__1), 5, 2);
lean::closure_set(x_6, 0, x_3);
lean::closure_set(x_6, 1, x_2);
x_7 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_7, 0, x_5);
lean::cnstr_set(x_7, 1, x_6);
return x_7;
}
}
obj* l_Lean_Parser_node___boxed(obj* x_1, obj* x_2, obj* x_3) {
@ -2324,39 +2338,33 @@ return x_5;
obj* l_Lean_Parser_leadingNode(obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7;
obj* x_3; obj* x_4; obj* x_5; obj* x_6;
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_4 = l_Lean_Parser_nodeInfo(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_6, 0, x_1);
lean::closure_set(x_6, 1, x_5);
x_7 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_7, 0, x_4);
lean::cnstr_set(x_7, 1, x_6);
return x_7;
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_node___lambda__1), 5, 2);
lean::closure_set(x_5, 0, x_2);
lean::closure_set(x_5, 1, x_1);
x_6 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_6, 0, x_4);
lean::cnstr_set(x_6, 1, x_5);
return x_6;
}
}
obj* l_Lean_Parser_trailingNode(obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7;
obj* x_3; obj* x_4; obj* x_5; obj* x_6;
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_4 = l_Lean_Parser_nodeInfo(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_nodeFn___rarg), 5, 2);
lean::closure_set(x_6, 0, x_1);
lean::closure_set(x_6, 1, x_5);
x_7 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_7, 0, x_4);
lean::cnstr_set(x_7, 1, x_6);
return x_7;
x_5 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_node___lambda__1), 5, 2);
lean::closure_set(x_5, 0, x_2);
lean::closure_set(x_5, 1, x_1);
x_6 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_6, 0, x_4);
lean::cnstr_set(x_6, 1, x_5);
return x_6;
}
}
obj* l_Lean_Parser_orelseFn___main___rarg(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {

8764
src/stage0/init/lean/parser/term.cpp generated
View file

File diff suppressed because it is too large Load diff