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

chore(library/init/lean/compiler): remove unnecessary [@export]s

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-02 15:04:28 -07:00
parent e3f32a6108
commit 2c4811a808
9 changed files with 366 additions and 244 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/lean/compiler/elimdead.lean
View file

@ -41,7 +41,6 @@ partial def FnBody.elimDead : FnBody → FnBody
reshapeWithoutDead bs term
/-- Eliminate dead let-declarations and join points -/
@[export lean.ir.decl_elim_dead_core]
def Decl.elimDead : Decl → Decl
| (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.elimDead
| other := other

2
library/init/lean/compiler/ir.lean
View file

@ -655,11 +655,9 @@ partial def collectDecl : Decl → Collector
end MaxVar
@[export lean.ir.fnbody_max_var_core]
def FnBody.maxVar (b : FnBody) : Index :=
MaxVar.collectFnBody b 0
@[export lean.ir.decl_max_var_core]
def Decl.maxVar (d : Decl) : Index :=
MaxVar.collectDecl d 0

1
library/init/lean/compiler/pushproj.lean
View file

@ -47,7 +47,6 @@ partial def FnBody.pushProj : FnBody → FnBody
| other := reshape bs term
/-- Push projections inside `case` branches. -/
@[export lean.ir.decl_push_proj_core]
def Decl.pushProj : Decl → Decl
| (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.pushProj
| other := other

1
library/init/lean/compiler/simpcase.lean
View file

@ -48,7 +48,6 @@ partial def FnBody.simpCase : FnBody → FnBody
- Remove unreachable branches.
- Remove `case` if there is only one branch.
- Merge most common branches using `Alt.default`. -/
@[export lean.ir.decl_simp_case_core]
def Decl.simpCase : Decl → Decl
| (Decl.fdecl f xs t b) := Decl.fdecl f xs t b.simpCase
| other := other

362
src/stage0/init/lean/compiler/default.cpp generated
View file

@ -26,8 +26,14 @@ obj* decl_to_string_core(obj*);
extern "C" obj* lean_io_prim_put_str(obj*, obj*);
obj* l_IO_println___at_Lean_IR_test___spec__1(obj*, obj*);
obj* l_Lean_IR_Decl_pushProj___main(obj*);
obj* l_Nat_repr(obj*);
obj* l_Lean_IR_MaxVar_collectDecl___main(obj*, obj*);
namespace lean {
obj* string_append(obj*, obj*);
}
obj* l_Lean_IR_test___closed__1;
obj* l_Lean_IR_Decl_elimDead___main(obj*);
obj* l_Lean_IR_test___closed__4;
obj* l_IO_println___at_HasRepr_HasEval___spec__1(obj*, obj*);
obj* l_IO_print___at_Lean_IR_test___spec__2(obj*, obj*);
obj* l_Lean_IR_Decl_simpCase___main(obj*);
@ -100,7 +106,7 @@ obj* _init_l_Lean_IR_test___closed__1() {
_start:
{
obj* x_0;
x_0 = lean::mk_string("=== After push projections ===");
x_0 = lean::mk_string("Max variable ");
return x_0;
}
}
@ -108,7 +114,7 @@ obj* _init_l_Lean_IR_test___closed__2() {
_start:
{
obj* x_0;
x_0 = lean::mk_string("=== After elim dead locals ===");
x_0 = lean::mk_string("=== After push projections ===");
return x_0;
}
}
@ -116,6 +122,14 @@ obj* _init_l_Lean_IR_test___closed__3() {
_start:
{
obj* x_0;
x_0 = lean::mk_string("=== After elim dead locals ===");
return x_0;
}
}
obj* _init_l_Lean_IR_test___closed__4() {
_start:
{
obj* x_0;
x_0 = lean::mk_string("=== After simplify case ===");
return x_0;
}
@ -130,7 +144,7 @@ lean::inc(x_0);
x_3 = l_IO_println___at_Lean_IR_test___spec__1(x_0, x_1);
if (lean::obj_tag(x_3) == 0)
{
obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11;
obj* x_4; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16;
x_4 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
lean::cnstr_release(x_3, 0);
@ -148,40 +162,25 @@ if (lean::is_scalar(x_6)) {
}
lean::cnstr_set(x_8, 0, x_7);
lean::cnstr_set(x_8, 1, x_4);
x_9 = l_Lean_IR_Decl_pushProj___main(x_0);
x_10 = l_Lean_IR_test___closed__1;
x_11 = l_IO_println___at_HasRepr_HasEval___spec__1(x_10, x_8);
if (lean::obj_tag(x_11) == 0)
{
obj* x_12; obj* x_14; obj* x_15; obj* x_17;
x_12 = lean::cnstr_get(x_11, 1);
if (lean::is_exclusive(x_11)) {
lean::cnstr_release(x_11, 0);
x_14 = x_11;
} else {
lean::inc(x_12);
lean::dec(x_11);
x_14 = lean::box(0);
}
if (lean::is_scalar(x_14)) {
x_15 = lean::alloc_cnstr(0, 2, 0);
} else {
x_15 = x_14;
}
lean::cnstr_set(x_15, 0, x_7);
lean::cnstr_set(x_15, 1, x_12);
lean::inc(x_9);
x_17 = l_IO_println___at_Lean_IR_test___spec__1(x_9, x_15);
if (lean::obj_tag(x_17) == 0)
x_9 = lean::mk_nat_obj(0ul);
lean::inc(x_0);
x_11 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_9);
x_12 = l_Nat_repr(x_11);
x_13 = l_Lean_IR_test___closed__1;
x_14 = lean::string_append(x_13, x_12);
lean::dec(x_12);
x_16 = l_IO_println___at_HasRepr_HasEval___spec__1(x_14, x_8);
lean::dec(x_14);
if (lean::obj_tag(x_16) == 0)
{
obj* x_18; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24;
x_18 = lean::cnstr_get(x_17, 1);
if (lean::is_exclusive(x_17)) {
lean::cnstr_release(x_17, 0);
x_20 = x_17;
x_18 = lean::cnstr_get(x_16, 1);
if (lean::is_exclusive(x_16)) {
lean::cnstr_release(x_16, 0);
x_20 = x_16;
} else {
lean::inc(x_18);
lean::dec(x_17);
lean::dec(x_16);
x_20 = lean::box(0);
}
if (lean::is_scalar(x_20)) {
@ -191,7 +190,7 @@ if (lean::is_scalar(x_20)) {
}
lean::cnstr_set(x_21, 0, x_7);
lean::cnstr_set(x_21, 1, x_18);
x_22 = l_Lean_IR_Decl_elimDead___main(x_9);
x_22 = l_Lean_IR_Decl_pushProj___main(x_0);
x_23 = l_Lean_IR_test___closed__2;
x_24 = l_IO_println___at_HasRepr_HasEval___spec__1(x_23, x_21);
if (lean::obj_tag(x_24) == 0)
@ -234,12 +233,12 @@ if (lean::is_scalar(x_33)) {
}
lean::cnstr_set(x_34, 0, x_7);
lean::cnstr_set(x_34, 1, x_31);
x_35 = l_Lean_IR_Decl_simpCase___main(x_22);
x_35 = l_Lean_IR_Decl_elimDead___main(x_22);
x_36 = l_Lean_IR_test___closed__3;
x_37 = l_IO_println___at_HasRepr_HasEval___spec__1(x_36, x_34);
if (lean::obj_tag(x_37) == 0)
{
obj* x_38; obj* x_40; obj* x_41; obj* x_42;
obj* x_38; obj* x_40; obj* x_41; obj* x_43;
x_38 = lean::cnstr_get(x_37, 1);
if (lean::is_exclusive(x_37)) {
lean::cnstr_release(x_37, 0);
@ -256,151 +255,218 @@ if (lean::is_scalar(x_40)) {
}
lean::cnstr_set(x_41, 0, x_7);
lean::cnstr_set(x_41, 1, x_38);
x_42 = l_IO_println___at_Lean_IR_test___spec__1(x_35, x_41);
return x_42;
}
else
lean::inc(x_35);
x_43 = l_IO_println___at_Lean_IR_test___spec__1(x_35, x_41);
if (lean::obj_tag(x_43) == 0)
{
obj* x_44; obj* x_46; obj* x_48; obj* x_49;
lean::dec(x_35);
x_44 = lean::cnstr_get(x_37, 0);
x_46 = lean::cnstr_get(x_37, 1);
if (lean::is_exclusive(x_37)) {
x_48 = x_37;
obj* x_44; obj* x_46; obj* x_47; obj* x_48; obj* x_49; obj* x_50;
x_44 = lean::cnstr_get(x_43, 1);
if (lean::is_exclusive(x_43)) {
lean::cnstr_release(x_43, 0);
x_46 = x_43;
} else {
lean::inc(x_44);
lean::inc(x_46);
lean::dec(x_37);
x_48 = lean::box(0);
lean::dec(x_43);
x_46 = lean::box(0);
}
if (lean::is_scalar(x_48)) {
x_49 = lean::alloc_cnstr(1, 2, 0);
if (lean::is_scalar(x_46)) {
x_47 = lean::alloc_cnstr(0, 2, 0);
} else {
x_49 = x_48;
x_47 = x_46;
}
lean::cnstr_set(x_49, 0, x_44);
lean::cnstr_set(x_49, 1, x_46);
return x_49;
}
}
else
lean::cnstr_set(x_47, 0, x_7);
lean::cnstr_set(x_47, 1, x_44);
x_48 = l_Lean_IR_Decl_simpCase___main(x_35);
x_49 = l_Lean_IR_test___closed__4;
x_50 = l_IO_println___at_HasRepr_HasEval___spec__1(x_49, x_47);
if (lean::obj_tag(x_50) == 0)
{
obj* x_51; obj* x_53; obj* x_55; obj* x_56;
lean::dec(x_22);
x_51 = lean::cnstr_get(x_30, 0);
x_53 = lean::cnstr_get(x_30, 1);
if (lean::is_exclusive(x_30)) {
x_55 = x_30;
obj* x_51; obj* x_53; obj* x_54; obj* x_55;
x_51 = lean::cnstr_get(x_50, 1);
if (lean::is_exclusive(x_50)) {
lean::cnstr_release(x_50, 0);
x_53 = x_50;
} else {
lean::inc(x_51);
lean::inc(x_53);
lean::dec(x_30);
x_55 = lean::box(0);
lean::dec(x_50);
x_53 = lean::box(0);
}
if (lean::is_scalar(x_55)) {
x_56 = lean::alloc_cnstr(1, 2, 0);
if (lean::is_scalar(x_53)) {
x_54 = lean::alloc_cnstr(0, 2, 0);
} else {
x_56 = x_55;
x_54 = x_53;
}
lean::cnstr_set(x_56, 0, x_51);
lean::cnstr_set(x_56, 1, x_53);
return x_56;
lean::cnstr_set(x_54, 0, x_7);
lean::cnstr_set(x_54, 1, x_51);
x_55 = l_IO_println___at_Lean_IR_test___spec__1(x_48, x_54);
return x_55;
}
else
{
obj* x_57; obj* x_59; obj* x_61; obj* x_62;
lean::dec(x_48);
x_57 = lean::cnstr_get(x_50, 0);
x_59 = lean::cnstr_get(x_50, 1);
if (lean::is_exclusive(x_50)) {
x_61 = x_50;
} else {
lean::inc(x_57);
lean::inc(x_59);
lean::dec(x_50);
x_61 = lean::box(0);
}
if (lean::is_scalar(x_61)) {
x_62 = lean::alloc_cnstr(1, 2, 0);
} else {
x_62 = x_61;
}
lean::cnstr_set(x_62, 0, x_57);
lean::cnstr_set(x_62, 1, x_59);
return x_62;
}
}
else
{
obj* x_58; obj* x_60; obj* x_62; obj* x_63;
obj* x_64; obj* x_66; obj* x_68; obj* x_69;
lean::dec(x_35);
x_64 = lean::cnstr_get(x_43, 0);
x_66 = lean::cnstr_get(x_43, 1);
if (lean::is_exclusive(x_43)) {
x_68 = x_43;
} else {
lean::inc(x_64);
lean::inc(x_66);
lean::dec(x_43);
x_68 = lean::box(0);
}
if (lean::is_scalar(x_68)) {
x_69 = lean::alloc_cnstr(1, 2, 0);
} else {
x_69 = x_68;
}
lean::cnstr_set(x_69, 0, x_64);
lean::cnstr_set(x_69, 1, x_66);
return x_69;
}
}
else
{
obj* x_71; obj* x_73; obj* x_75; obj* x_76;
lean::dec(x_35);
x_71 = lean::cnstr_get(x_37, 0);
x_73 = lean::cnstr_get(x_37, 1);
if (lean::is_exclusive(x_37)) {
x_75 = x_37;
} else {
lean::inc(x_71);
lean::inc(x_73);
lean::dec(x_37);
x_75 = lean::box(0);
}
if (lean::is_scalar(x_75)) {
x_76 = lean::alloc_cnstr(1, 2, 0);
} else {
x_76 = x_75;
}
lean::cnstr_set(x_76, 0, x_71);
lean::cnstr_set(x_76, 1, x_73);
return x_76;
}
}
else
{
obj* x_78; obj* x_80; obj* x_82; obj* x_83;
lean::dec(x_22);
x_58 = lean::cnstr_get(x_24, 0);
x_60 = lean::cnstr_get(x_24, 1);
x_78 = lean::cnstr_get(x_30, 0);
x_80 = lean::cnstr_get(x_30, 1);
if (lean::is_exclusive(x_30)) {
x_82 = x_30;
} else {
lean::inc(x_78);
lean::inc(x_80);
lean::dec(x_30);
x_82 = lean::box(0);
}
if (lean::is_scalar(x_82)) {
x_83 = lean::alloc_cnstr(1, 2, 0);
} else {
x_83 = x_82;
}
lean::cnstr_set(x_83, 0, x_78);
lean::cnstr_set(x_83, 1, x_80);
return x_83;
}
}
else
{
obj* x_85; obj* x_87; obj* x_89; obj* x_90;
lean::dec(x_22);
x_85 = lean::cnstr_get(x_24, 0);
x_87 = lean::cnstr_get(x_24, 1);
if (lean::is_exclusive(x_24)) {
x_62 = x_24;
x_89 = x_24;
} else {
lean::inc(x_58);
lean::inc(x_60);
lean::inc(x_85);
lean::inc(x_87);
lean::dec(x_24);
x_62 = lean::box(0);
x_89 = lean::box(0);
}
if (lean::is_scalar(x_62)) {
x_63 = lean::alloc_cnstr(1, 2, 0);
if (lean::is_scalar(x_89)) {
x_90 = lean::alloc_cnstr(1, 2, 0);
} else {
x_63 = x_62;
x_90 = x_89;
}
lean::cnstr_set(x_63, 0, x_58);
lean::cnstr_set(x_63, 1, x_60);
return x_63;
lean::cnstr_set(x_90, 0, x_85);
lean::cnstr_set(x_90, 1, x_87);
return x_90;
}
}
else
{
obj* x_65; obj* x_67; obj* x_69; obj* x_70;
lean::dec(x_9);
x_65 = lean::cnstr_get(x_17, 0);
x_67 = lean::cnstr_get(x_17, 1);
if (lean::is_exclusive(x_17)) {
x_69 = x_17;
} else {
lean::inc(x_65);
lean::inc(x_67);
lean::dec(x_17);
x_69 = lean::box(0);
}
if (lean::is_scalar(x_69)) {
x_70 = lean::alloc_cnstr(1, 2, 0);
} else {
x_70 = x_69;
}
lean::cnstr_set(x_70, 0, x_65);
lean::cnstr_set(x_70, 1, x_67);
return x_70;
}
}
else
{
obj* x_72; obj* x_74; obj* x_76; obj* x_77;
lean::dec(x_9);
x_72 = lean::cnstr_get(x_11, 0);
x_74 = lean::cnstr_get(x_11, 1);
if (lean::is_exclusive(x_11)) {
x_76 = x_11;
} else {
lean::inc(x_72);
lean::inc(x_74);
lean::dec(x_11);
x_76 = lean::box(0);
}
if (lean::is_scalar(x_76)) {
x_77 = lean::alloc_cnstr(1, 2, 0);
} else {
x_77 = x_76;
}
lean::cnstr_set(x_77, 0, x_72);
lean::cnstr_set(x_77, 1, x_74);
return x_77;
}
}
else
{
obj* x_79; obj* x_81; obj* x_83; obj* x_84;
obj* x_92; obj* x_94; obj* x_96; obj* x_97;
lean::dec(x_0);
x_79 = lean::cnstr_get(x_3, 0);
x_81 = lean::cnstr_get(x_3, 1);
x_92 = lean::cnstr_get(x_16, 0);
x_94 = lean::cnstr_get(x_16, 1);
if (lean::is_exclusive(x_16)) {
x_96 = x_16;
} else {
lean::inc(x_92);
lean::inc(x_94);
lean::dec(x_16);
x_96 = lean::box(0);
}
if (lean::is_scalar(x_96)) {
x_97 = lean::alloc_cnstr(1, 2, 0);
} else {
x_97 = x_96;
}
lean::cnstr_set(x_97, 0, x_92);
lean::cnstr_set(x_97, 1, x_94);
return x_97;
}
}
else
{
obj* x_99; obj* x_101; obj* x_103; obj* x_104;
lean::dec(x_0);
x_99 = lean::cnstr_get(x_3, 0);
x_101 = lean::cnstr_get(x_3, 1);
if (lean::is_exclusive(x_3)) {
x_83 = x_3;
x_103 = x_3;
} else {
lean::inc(x_79);
lean::inc(x_81);
lean::inc(x_99);
lean::inc(x_101);
lean::dec(x_3);
x_83 = lean::box(0);
x_103 = lean::box(0);
}
if (lean::is_scalar(x_83)) {
x_84 = lean::alloc_cnstr(1, 2, 0);
if (lean::is_scalar(x_103)) {
x_104 = lean::alloc_cnstr(1, 2, 0);
} else {
x_84 = x_83;
x_104 = x_103;
}
lean::cnstr_set(x_84, 0, x_79);
lean::cnstr_set(x_84, 1, x_81);
return x_84;
lean::cnstr_set(x_104, 0, x_99);
lean::cnstr_set(x_104, 1, x_101);
return x_104;
}
}
}
@ -431,5 +497,7 @@ lean::mark_persistent(l_Lean_IR_test___closed__1);
lean::mark_persistent(l_Lean_IR_test___closed__2);
l_Lean_IR_test___closed__3 = _init_l_Lean_IR_test___closed__3();
lean::mark_persistent(l_Lean_IR_test___closed__3);
l_Lean_IR_test___closed__4 = _init_l_Lean_IR_test___closed__4();
lean::mark_persistent(l_Lean_IR_test___closed__4);
return w;
}

10
src/stage0/init/lean/compiler/elimdead.cpp generated
View file

@ -30,10 +30,7 @@ obj* l_Lean_IR_reshapeWithoutDeadAux___main(obj*, obj*, obj*);
namespace lean {
uint8 nat_dec_lt(obj*, obj*);
}
namespace lean {
namespace ir {
obj* decl_elim_dead_core(obj*);
}}
obj* l_Lean_IR_Decl_elimDead(obj*);
obj* l_RBNode_findCore___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__1(obj*, obj*);
obj* l_Lean_IR_FnBody_flatten(obj*);
namespace lean {
@ -431,9 +428,7 @@ return x_0;
}
}
}
namespace lean {
namespace ir {
obj* decl_elim_dead_core(obj* x_0) {
obj* l_Lean_IR_Decl_elimDead(obj* x_0) {
_start:
{
obj* x_1;
@ -441,7 +436,6 @@ x_1 = l_Lean_IR_Decl_elimDead___main(x_0);
return x_1;
}
}
}}
obj* initialize_init_default(obj*);
obj* initialize_init_lean_compiler_ir(obj*);
static bool _G_initialized = false;

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

@ -150,10 +150,7 @@ obj* l_Lean_IR_declHasFormat;
obj* l___private_init_lean_compiler_ir_20__formatIRType___boxed(obj*);
obj* l___private_init_lean_compiler_ir_19__formatExpr___main___closed__2;
obj* l_Lean_IR_Alt_default(obj*);
namespace lean {
namespace ir {
obj* decl_max_var_core(obj*);
}}
obj* l_Lean_IR_Decl_maxVar(obj*);
obj* l___private_init_lean_compiler_ir_2__collectIndex(obj*, obj*, obj*);
namespace lean {
namespace ir {
@ -354,10 +351,7 @@ obj* l___private_init_lean_compiler_ir_8__withParams___boxed(obj*, obj*, obj*, o
obj* l_Lean_IR_VarId_lt___boxed(obj*, obj*);
obj* l_Lean_IR_mkDecl___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_formatFnBody___main___closed__16;
namespace lean {
namespace ir {
obj* fnbody_max_var_core(obj*);
}}
obj* l_Lean_IR_FnBody_maxVar(obj*);
uint8 l_Lean_IR_CtorInfo_beq___main(obj*, obj*);
uint8 l_Lean_IR_FnBody_beq(obj*, obj*);
obj* l___private_init_lean_compiler_ir_14__collectAlts___boxed(obj*, obj*, obj*, obj*);
@ -400,6 +394,7 @@ obj* l_Lean_IR_FnBody_isPure___main___boxed(obj*);
obj* l_Lean_IR_litValHasFormat;
uint8 l_Lean_IR_Alt_isDefault(obj*);
obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_16__formatArray___spec__1___boxed(obj*);
obj* l_Lean_IR_fnBodyHasToString(obj*);
obj* l_Lean_IR_FnBody_body___main(obj*);
extern obj* l_Lean_Name_toString___closed__1;
obj* l_Lean_IR_MaxVar_collectFnBody___main(obj*, obj*);
@ -10921,6 +10916,17 @@ lean::closure_set(x_1, 0, x_0);
return x_1;
}
}
obj* l_Lean_IR_fnBodyHasToString(obj* x_0) {
_start:
{
obj* x_1; obj* x_2; obj* x_3; obj* x_4;
x_1 = lean::mk_nat_obj(2ul);
x_2 = l_Lean_IR_formatFnBody___main(x_1, x_0);
x_3 = l_Lean_Options_empty;
x_4 = l_Lean_Format_pretty(x_2, x_3);
return x_4;
}
}
obj* _init_l_Lean_IR_formatDecl___main___closed__1() {
_start:
{
@ -12138,9 +12144,7 @@ x_2 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_1);
return x_2;
}
}
namespace lean {
namespace ir {
obj* fnbody_max_var_core(obj* x_0) {
obj* l_Lean_IR_FnBody_maxVar(obj* x_0) {
_start:
{
obj* x_1; obj* x_2;
@ -12149,10 +12153,7 @@ x_2 = l_Lean_IR_MaxVar_collectFnBody___main(x_0, x_1);
return x_2;
}
}
}}
namespace lean {
namespace ir {
obj* decl_max_var_core(obj* x_0) {
obj* l_Lean_IR_Decl_maxVar(obj* x_0) {
_start:
{
obj* x_1; obj* x_2;
@ -12161,7 +12162,6 @@ x_2 = l_Lean_IR_MaxVar_collectDecl___main(x_0, x_1);
return x_2;
}
}
}}
obj* initialize_init_lean_name(obj*);
obj* initialize_init_lean_kvmap(obj*);
obj* initialize_init_lean_format(obj*);

10
src/stage0/init/lean/compiler/pushproj.cpp generated
View file

@ -22,10 +22,7 @@ namespace lean {
obj* nat_sub(obj*, obj*);
}
extern obj* l_Lean_IR_vsetInh;
namespace lean {
namespace ir {
obj* decl_push_proj_core(obj*);
}}
obj* l_Lean_IR_Decl_pushProj(obj*);
obj* l_RBNode_ins___main___at___private_init_lean_compiler_ir_2__collectIndex___spec__2(obj*, obj*, obj*);
obj* l_Lean_IR_pushProjs___main___closed__1;
obj* l_Array_hmmapAux___main___at_Lean_IR_pushProjs___main___spec__4___boxed(obj*, obj*, obj*, obj*, obj*);
@ -829,9 +826,7 @@ return x_0;
}
}
}
namespace lean {
namespace ir {
obj* decl_push_proj_core(obj* x_0) {
obj* l_Lean_IR_Decl_pushProj(obj* x_0) {
_start:
{
obj* x_1;
@ -839,7 +834,6 @@ x_1 = l_Lean_IR_Decl_pushProj___main(x_0);
return x_1;
}
}
}}
obj* initialize_init_default(obj*);
obj* initialize_init_lean_compiler_ir(obj*);
static bool _G_initialized = false;

191
src/stage0/init/lean/compiler/simpcase.cpp generated
View file

@ -15,11 +15,11 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__2___boxed(obj*, obj*, obj*, obj*);
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(obj*, obj*, obj*);
obj* l_Lean_IR_FnBody_simpCase(obj*);
obj* l_Lean_IR_FnBody_simpCase___main(obj*);
obj* l_Array_anyAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__1___boxed(obj*, obj*);
obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__1___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1;
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__2___boxed(obj*, obj*, obj*, obj*);
obj* l_Lean_IR_reshape(obj*, obj*);
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__2(obj*, obj*, obj*, obj*);
@ -27,7 +27,6 @@ namespace lean {
uint8 nat_dec_lt(obj*, obj*);
}
obj* l_Array_miterateAux___main___at___private_init_lean_compiler_simpcase_1__maxOccs___spec__2(obj*, obj*, obj*, obj*);
obj* l___private_init_lean_compiler_simpcase_3__mkCase(obj*, obj*, obj*);
obj* l_Lean_IR_FnBody_flatten(obj*);
obj* l___private_init_lean_compiler_simpcase_2__addDefault(obj*);
namespace lean {
@ -37,13 +36,13 @@ namespace lean {
uint8 nat_dec_eq(obj*, obj*);
}
obj* l___private_init_lean_compiler_simpcase_1__maxOccs___boxed(obj*);
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(obj*, obj*, obj*);
extern obj* l_Lean_IR_altInh;
uint8 l_Lean_IR_Alt_isDefault___main(obj*);
uint8 l_Array_anyAux___main___at___private_init_lean_compiler_simpcase_2__addDefault___spec__1(obj*, obj*);
namespace lean {
namespace ir {
obj* decl_simp_case_core(obj*);
}}
obj* l_Lean_IR_Decl_simpCase(obj*);
obj* l___private_init_lean_compiler_simpcase_3__mkSimpCase(obj*, obj*, obj*);
obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(obj*, obj*);
obj* l_Array_shrink___main___rarg(obj*, obj*);
obj* l_Lean_IR_AltCore_body___main(obj*);
uint8 l_Lean_IR_FnBody_beq(obj*, obj*);
@ -253,47 +252,47 @@ x_13 = l_Lean_IR_AltCore_body___main(x_0);
x_14 = l_Lean_IR_FnBody_beq(x_11, x_13);
if (x_14 == 0)
{
obj* x_15; obj* x_16;
x_15 = lean::mk_nat_obj(1ul);
x_16 = lean::nat_add(x_2, x_15);
uint8 x_15;
x_15 = lean::nat_dec_lt(x_3, x_2);
if (x_15 == 0)
{
obj* x_16; obj* x_17; obj* x_19;
x_16 = lean::mk_nat_obj(1ul);
x_17 = lean::nat_add(x_2, x_16);
lean::dec(x_2);
x_2 = x_16;
x_19 = lean::nat_add(x_3, x_16);
lean::dec(x_3);
x_2 = x_17;
x_3 = x_19;
goto _start;
}
else
{
uint8 x_19;
x_19 = lean::nat_dec_lt(x_3, x_2);
if (x_19 == 0)
{
obj* x_20; obj* x_21; obj* x_23;
x_20 = lean::mk_nat_obj(1ul);
x_21 = lean::nat_add(x_2, x_20);
obj* x_22; obj* x_23; obj* x_24; obj* x_26;
x_22 = lean::array_fswap(x_1, x_2, x_3);
x_23 = lean::mk_nat_obj(1ul);
x_24 = lean::nat_add(x_2, x_23);
lean::dec(x_2);
x_23 = lean::nat_add(x_3, x_20);
x_26 = lean::nat_add(x_3, x_23);
lean::dec(x_3);
x_2 = x_21;
x_3 = x_23;
x_1 = x_22;
x_2 = x_24;
x_3 = x_26;
goto _start;
}
}
else
{
obj* x_26; obj* x_27; obj* x_28; obj* x_30;
x_26 = lean::array_fswap(x_1, x_2, x_3);
x_27 = lean::mk_nat_obj(1ul);
x_28 = lean::nat_add(x_2, x_27);
obj* x_29; obj* x_30;
x_29 = lean::mk_nat_obj(1ul);
x_30 = lean::nat_add(x_2, x_29);
lean::dec(x_2);
x_30 = lean::nat_add(x_3, x_27);
lean::dec(x_3);
x_1 = x_26;
x_2 = x_28;
x_3 = x_30;
x_2 = x_30;
goto _start;
}
}
}
}
}
obj* l___private_init_lean_compiler_simpcase_2__addDefault(obj* x_0) {
_start:
{
@ -349,7 +348,7 @@ lean::dec(x_0);
return x_4;
}
}
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(obj* x_0, obj* x_1, obj* x_2) {
obj* l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3; uint8 x_4;
@ -415,12 +414,12 @@ goto _start;
}
}
}
obj* l___private_init_lean_compiler_simpcase_3__mkCase(obj* x_0, obj* x_1, obj* x_2) {
obj* l___private_init_lean_compiler_simpcase_3__mkSimpCase(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_4; obj* x_5; obj* x_6; uint8 x_7;
x_3 = lean::mk_nat_obj(0ul);
x_4 = l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkCase___spec__1(x_2, x_3, x_3);
x_4 = l_Array_filterAux___main___at___private_init_lean_compiler_simpcase_3__mkSimpCase___spec__1(x_2, x_3, x_3);
x_5 = l___private_init_lean_compiler_simpcase_2__addDefault(x_4);
x_6 = lean::array_get_size(x_5);
x_7 = lean::nat_dec_eq(x_6, x_3);
@ -534,6 +533,90 @@ goto _start;
}
}
}
obj* _init_l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1() {
_start:
{
obj* x_0; obj* x_1;
x_0 = lean::box(12);
x_1 = lean::alloc_cnstr(1, 1, 0);
lean::cnstr_set(x_1, 0, x_0);
return x_1;
}
}
obj* l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(obj* x_0, obj* x_1) {
_start:
{
obj* x_2; uint8 x_3;
x_2 = lean::array_get_size(x_1);
x_3 = lean::nat_dec_lt(x_0, x_2);
lean::dec(x_2);
if (x_3 == 0)
{
lean::dec(x_0);
return x_1;
}
else
{
obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10;
x_6 = lean::array_fget(x_1, x_0);
x_7 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1;
x_8 = lean::array_fset(x_1, x_0, x_7);
x_9 = lean::mk_nat_obj(1ul);
x_10 = lean::nat_add(x_0, x_9);
if (lean::obj_tag(x_6) == 0)
{
obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17; obj* x_18;
x_11 = lean::cnstr_get(x_6, 0);
x_13 = lean::cnstr_get(x_6, 1);
if (lean::is_exclusive(x_6)) {
x_15 = x_6;
} else {
lean::inc(x_11);
lean::inc(x_13);
lean::dec(x_6);
x_15 = lean::box(0);
}
x_16 = l_Lean_IR_FnBody_simpCase___main(x_13);
if (lean::is_scalar(x_15)) {
x_17 = lean::alloc_cnstr(0, 2, 0);
} else {
x_17 = x_15;
}
lean::cnstr_set(x_17, 0, x_11);
lean::cnstr_set(x_17, 1, x_16);
x_18 = lean::array_fset(x_8, x_0, x_17);
lean::dec(x_0);
x_0 = x_10;
x_1 = x_18;
goto _start;
}
else
{
obj* x_21; obj* x_23; obj* x_24; obj* x_25; obj* x_26;
x_21 = lean::cnstr_get(x_6, 0);
if (lean::is_exclusive(x_6)) {
x_23 = x_6;
} else {
lean::inc(x_21);
lean::dec(x_6);
x_23 = lean::box(0);
}
x_24 = l_Lean_IR_FnBody_simpCase___main(x_21);
if (lean::is_scalar(x_23)) {
x_25 = lean::alloc_cnstr(1, 1, 0);
} else {
x_25 = x_23;
}
lean::cnstr_set(x_25, 0, x_24);
x_26 = lean::array_fset(x_8, x_0, x_25);
lean::dec(x_0);
x_0 = x_10;
x_1 = x_26;
goto _start;
}
}
}
}
obj* l_Lean_IR_FnBody_simpCase___main(obj* x_0) {
_start:
{
@ -549,35 +632,24 @@ x_8 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__1(x_7,
switch (lean::obj_tag(x_4)) {
case 9:
{
obj* x_9; obj* x_11; obj* x_13; obj* x_15; obj* x_16; obj* x_17;
obj* x_9; obj* x_11; obj* x_13; obj* x_16; obj* x_17; obj* x_18;
x_9 = lean::cnstr_get(x_4, 0);
lean::inc(x_9);
x_11 = lean::cnstr_get(x_4, 1);
lean::inc(x_11);
x_13 = lean::cnstr_get(x_4, 2);
if (lean::is_exclusive(x_4)) {
x_15 = x_4;
} else {
lean::inc(x_9);
lean::inc(x_11);
lean::inc(x_13);
lean::dec(x_4);
x_15 = lean::box(0);
}
if (lean::is_scalar(x_15)) {
x_16 = lean::alloc_cnstr(9, 3, 0);
} else {
x_16 = x_15;
}
lean::cnstr_set(x_16, 0, x_9);
lean::cnstr_set(x_16, 1, x_11);
lean::cnstr_set(x_16, 2, x_13);
x_17 = l_Lean_IR_reshape(x_8, x_16);
return x_17;
lean::inc(x_13);
lean::dec(x_4);
x_16 = l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2(x_7, x_13);
x_17 = l___private_init_lean_compiler_simpcase_3__mkSimpCase(x_9, x_11, x_16);
x_18 = l_Lean_IR_reshape(x_8, x_17);
return x_18;
}
default:
{
obj* x_18;
x_18 = l_Lean_IR_reshape(x_8, x_4);
return x_18;
obj* x_19;
x_19 = l_Lean_IR_reshape(x_8, x_4);
return x_19;
}
}
}
@ -628,9 +700,7 @@ return x_0;
}
}
}
namespace lean {
namespace ir {
obj* decl_simp_case_core(obj* x_0) {
obj* l_Lean_IR_Decl_simpCase(obj* x_0) {
_start:
{
obj* x_1;
@ -638,7 +708,6 @@ x_1 = l_Lean_IR_Decl_simpCase___main(x_0);
return x_1;
}
}
}}
obj* initialize_init_default(obj*);
obj* initialize_init_lean_compiler_ir(obj*);
static bool _G_initialized = false;
@ -650,5 +719,7 @@ w = initialize_init_default(w);
if (io_result_is_error(w)) return w;
w = initialize_init_lean_compiler_ir(w);
if (io_result_is_error(w)) return w;
l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1 = _init_l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1();
lean::mark_persistent(l_Array_hmmapAux___main___at_Lean_IR_FnBody_simpCase___main___spec__2___closed__1);
return w;
}