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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-03 15:33:02 -07:00
parent 5f0dae3fcb
commit cd4affd129
5 changed files with 466 additions and 360 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
stage0/src/Lean/Elab/Term.lean
View file

@ -974,11 +974,21 @@ match ctx.declName? with
@[builtinTermElab «prop»] def elabProp : TermElab :=
fun _ _ => pure $ mkSort levelZero
private def elabOptLevel (stx : Syntax) : TermElabM Level :=
if stx.isNone then
pure levelZero
else
elabLevel $ stx.getArg 0
@[builtinTermElab «sort»] def elabSort : TermElab :=
fun _ _ => pure $ mkSort levelZero
fun stx _ => do
u ← elabOptLevel $ stx.getArg 1;
pure $ mkSort u
@[builtinTermElab «type»] def elabTypeStx : TermElab :=
fun _ _ => pure $ mkSort levelOne
fun stx _ => do
u ← elabOptLevel $ stx.getArg 1;
pure $ mkSort (mkLevelSucc u)
@[builtinTermElab «hole»] def elabHole : TermElab :=
fun stx expectedType? => mkFreshExprMVar stx expectedType?

379
stage0/stdlib/Lean/Delaborator.c
View file

@ -35,7 +35,6 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Level_quote___main___lambda__1___closed__5;
lean_object* l_Lean_Delaborator_annotatePos(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Delaborator_delabFor___main___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabSort___closed__12;
lean_object* l_Lean_Delaborator_annotatePos___main(lean_object*, lean_object*);
lean_object* l_Lean_mkTermIdFromIdent(lean_object*);
lean_object* l_Lean_LocalDecl_userName(lean_object*);
@ -226,7 +225,6 @@ uint8_t l_Lean_Elab_Term_blockImplicitLambda(lean_object*);
lean_object* l_Lean_Delaborator_delabOfNat___closed__2;
lean_object* l___regBuiltin_Lean_Delaborator_delabLit(lean_object*);
lean_object* l_Lean_Delaborator_delabAttribute___closed__2;
lean_object* l_Lean_Delaborator_delabSort___closed__14;
lean_object* l_Lean_Delaborator_mkDelabAttribute___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabForall___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_delabAppImplicit___closed__5;
@ -242,7 +240,6 @@ lean_object* l_Lean_Delaborator_delabFor___main(lean_object*, lean_object*, lean
extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Delaborator_delabProjectionApp___closed__3;
lean_object* l_Lean_Delaborator_delabSort___closed__15;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Delaborator_delabForall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Delaborator_withAppFnArgs(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -262,7 +259,6 @@ lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lea
extern lean_object* l_Lean_numLitKind___closed__2;
lean_object* l_Lean_Level_getOffsetAux___main(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_evalNat___main___closed__6;
extern lean_object* l_Lean_mkAppStx___closed__6;
lean_object* l_Lean_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_failure___at_Lean_Delaborator_DelabM_inhabited___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_attrParamSyntaxToIdentifier(lean_object*);
@ -358,7 +354,6 @@ lean_object* l_Lean_Delaborator_delabAppImplicit___lambda__1(lean_object*, lean_
uint8_t l_Lean_BinderInfo_isExplicit(uint8_t);
lean_object* l_Lean_Delaborator_delabMVar___closed__1;
lean_object* l_Lean_Level_quote___main___lambda__1___closed__2;
lean_object* l_Lean_Delaborator_delabSort___closed__13;
extern lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1;
lean_object* l___regBuiltin_Lean_Delaborator_delabCoeFun___closed__1;
lean_object* l_Lean_Delaborator_delabMVar___closed__2;
@ -8199,18 +8194,22 @@ return x_5;
lean_object* _init_l_Lean_Delaborator_delabSort___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("sortApp");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__5;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Delaborator_delabSort___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
@ -8219,7 +8218,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_Lean_Parser_Term_sort___elambda__1___closed__5;
x_2 = l_Lean_Parser_Term_prop___elambda__1___closed__5;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -8240,7 +8239,7 @@ lean_object* _init_l_Lean_Delaborator_delabSort___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
x_1 = l_Lean_Parser_Term_prop___elambda__1___closed__2;
x_2 = l_Lean_Delaborator_delabSort___closed__4;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -8251,11 +8250,11 @@ return x_3;
lean_object* _init_l_Lean_Delaborator_delabSort___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Delaborator_delabSort___closed__5;
x_3 = lean_array_push(x_1, x_2);
return x_3;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Delaborator_delabSort___closed__5;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__7() {
@ -8263,7 +8262,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_Lean_Parser_Term_prop___elambda__1___closed__5;
x_2 = l_Lean_Parser_Term_type___elambda__1___closed__5;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -8284,78 +8283,34 @@ lean_object* _init_l_Lean_Delaborator_delabSort___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_prop___elambda__1___closed__2;
x_2 = l_Lean_Delaborator_delabSort___closed__8;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
x_1 = l_Lean_Delaborator_delabSort___closed__8;
x_2 = l___private_Lean_Elab_Term_5__expandCDot___main___closed__4;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Delaborator_delabSort___closed__9;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_Lean_Parser_Term_type___elambda__1___closed__5;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Delaborator_delabSort___closed__11;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_type___elambda__1___closed__2;
x_2 = l_Lean_Delaborator_delabSort___closed__12;
x_2 = l_Lean_Delaborator_delabSort___closed__9;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__14() {
lean_object* _init_l_Lean_Delaborator_delabSort___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Delaborator_delabSort___closed__13;
x_1 = l_Lean_Delaborator_delabSort___closed__10;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Delaborator_delabSort___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Delaborator_delabSort___closed__13;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Delaborator_delabSort(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -8393,190 +8348,220 @@ lean_dec(x_6);
switch (lean_obj_tag(x_10)) {
case 0:
{
lean_object* x_20; lean_object* x_21;
lean_object* x_24; lean_object* x_25;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
x_20 = l_Lean_Delaborator_delabSort___closed__10;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_8);
return x_21;
x_24 = l_Lean_Delaborator_delabSort___closed__6;
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_8);
return x_25;
}
case 1:
{
lean_object* x_22;
x_22 = lean_ctor_get(x_10, 0);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24;
lean_dec(x_22);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
x_23 = l_Lean_Delaborator_delabSort___closed__14;
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_8);
return x_24;
}
else
{
lean_object* x_25;
lean_dec(x_22);
x_25 = l_Lean_Level_dec___main(x_10);
if (lean_obj_tag(x_25) == 0)
{
lean_object* x_26;
x_26 = lean_box(0);
x_11 = x_26;
goto block_19;
}
else
x_26 = lean_ctor_get(x_10, 0);
lean_inc(x_26);
if (lean_obj_tag(x_26) == 0)
{
uint8_t x_27;
lean_object* x_27; lean_object* x_28;
lean_dec(x_26);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
x_27 = !lean_is_exclusive(x_25);
if (x_27 == 0)
{
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;
x_28 = lean_ctor_get(x_25, 0);
x_29 = l_Lean_Level_quote___main(x_28);
x_30 = l_Lean_Delaborator_delabSort___closed__15;
x_31 = lean_array_push(x_30, x_29);
x_32 = l_Lean_Delaborator_delabSort___closed__2;
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_31);
lean_ctor_set(x_25, 0, x_33);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_25);
lean_ctor_set(x_34, 1, x_8);
return x_34;
x_27 = l_Lean_Delaborator_delabSort___closed__11;
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_8);
return x_28;
}
else
{
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;
x_35 = lean_ctor_get(x_25, 0);
lean_inc(x_35);
lean_dec(x_25);
x_36 = l_Lean_Level_quote___main(x_35);
x_37 = l_Lean_Delaborator_delabSort___closed__15;
x_38 = lean_array_push(x_37, x_36);
x_39 = l_Lean_Delaborator_delabSort___closed__2;
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = lean_alloc_ctor(1, 1, 0);
lean_object* x_29;
lean_dec(x_26);
x_29 = l_Lean_Level_dec___main(x_10);
if (lean_obj_tag(x_29) == 0)
{
lean_object* x_30;
x_30 = lean_box(0);
x_11 = x_30;
goto block_23;
}
else
{
uint8_t x_31;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
x_31 = !lean_is_exclusive(x_29);
if (x_31 == 0)
{
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;
x_32 = lean_ctor_get(x_29, 0);
x_33 = l_Lean_Level_quote___main(x_32);
x_34 = l_Array_empty___closed__1;
x_35 = lean_array_push(x_34, x_33);
x_36 = l_Lean_nullKind___closed__2;
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_35);
x_38 = l_Lean_Delaborator_delabSort___closed__8;
x_39 = lean_array_push(x_38, x_37);
x_40 = l_Lean_Parser_Term_type___elambda__1___closed__2;
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_39);
lean_ctor_set(x_29, 0, x_41);
x_42 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 0, x_29);
lean_ctor_set(x_42, 1, x_8);
return x_42;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_43 = lean_ctor_get(x_29, 0);
lean_inc(x_43);
lean_dec(x_29);
x_44 = l_Lean_Level_quote___main(x_43);
x_45 = l_Array_empty___closed__1;
x_46 = lean_array_push(x_45, x_44);
x_47 = l_Lean_nullKind___closed__2;
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_46);
x_49 = l_Lean_Delaborator_delabSort___closed__8;
x_50 = lean_array_push(x_49, x_48);
x_51 = l_Lean_Parser_Term_type___elambda__1___closed__2;
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
x_53 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_53, 0, x_52);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_8);
return x_54;
}
}
}
}
default:
{
lean_object* x_43;
x_43 = l_Lean_Level_dec___main(x_10);
if (lean_obj_tag(x_43) == 0)
lean_object* x_55;
x_55 = l_Lean_Level_dec___main(x_10);
if (lean_obj_tag(x_55) == 0)
{
lean_object* x_44;
x_44 = lean_box(0);
x_11 = x_44;
goto block_19;
lean_object* x_56;
x_56 = lean_box(0);
x_11 = x_56;
goto block_23;
}
else
{
uint8_t x_45;
uint8_t x_57;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
x_45 = !lean_is_exclusive(x_43);
if (x_45 == 0)
x_57 = !lean_is_exclusive(x_55);
if (x_57 == 0)
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_46 = lean_ctor_get(x_43, 0);
x_47 = l_Lean_Level_quote___main(x_46);
x_48 = l_Lean_Delaborator_delabSort___closed__15;
x_49 = lean_array_push(x_48, x_47);
x_50 = l_Lean_Delaborator_delabSort___closed__2;
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_50);
lean_ctor_set(x_51, 1, x_49);
lean_ctor_set(x_43, 0, x_51);
x_52 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_52, 0, x_43);
lean_ctor_set(x_52, 1, x_8);
return x_52;
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;
x_58 = lean_ctor_get(x_55, 0);
x_59 = l_Lean_Level_quote___main(x_58);
x_60 = l_Array_empty___closed__1;
x_61 = lean_array_push(x_60, x_59);
x_62 = l_Lean_nullKind___closed__2;
x_63 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_63, 0, x_62);
lean_ctor_set(x_63, 1, x_61);
x_64 = l_Lean_Delaborator_delabSort___closed__8;
x_65 = lean_array_push(x_64, x_63);
x_66 = l_Lean_Parser_Term_type___elambda__1___closed__2;
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_66);
lean_ctor_set(x_67, 1, x_65);
lean_ctor_set(x_55, 0, x_67);
x_68 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_68, 0, x_55);
lean_ctor_set(x_68, 1, x_8);
return x_68;
}
else
{
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;
x_53 = lean_ctor_get(x_43, 0);
lean_inc(x_53);
lean_dec(x_43);
x_54 = l_Lean_Level_quote___main(x_53);
x_55 = l_Lean_Delaborator_delabSort___closed__15;
x_56 = lean_array_push(x_55, x_54);
x_57 = l_Lean_Delaborator_delabSort___closed__2;
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_56);
x_59 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_59, 0, x_58);
x_60 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_8);
return x_60;
lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
x_69 = lean_ctor_get(x_55, 0);
lean_inc(x_69);
lean_dec(x_55);
x_70 = l_Lean_Level_quote___main(x_69);
x_71 = l_Array_empty___closed__1;
x_72 = lean_array_push(x_71, x_70);
x_73 = l_Lean_nullKind___closed__2;
x_74 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_74, 0, x_73);
lean_ctor_set(x_74, 1, x_72);
x_75 = l_Lean_Delaborator_delabSort___closed__8;
x_76 = lean_array_push(x_75, x_74);
x_77 = l_Lean_Parser_Term_type___elambda__1___closed__2;
x_78 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_78, 0, x_77);
lean_ctor_set(x_78, 1, x_76);
x_79 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_79, 0, x_78);
x_80 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_8);
return x_80;
}
}
}
}
block_19:
block_23:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_11);
x_12 = l_Lean_Level_quote___main(x_10);
x_13 = l_Lean_Delaborator_delabSort___closed__6;
x_13 = l_Array_empty___closed__1;
x_14 = lean_array_push(x_13, x_12);
x_15 = l_Lean_Delaborator_delabSort___closed__2;
x_15 = l_Lean_nullKind___closed__2;
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = l_Lean_Delaborator_delabSort___closed__2;
x_18 = lean_array_push(x_17, x_16);
x_19 = l_Lean_Parser_Term_sort___elambda__1___closed__2;
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
if (lean_is_scalar(x_7)) {
x_17 = lean_alloc_ctor(1, 1, 0);
x_21 = lean_alloc_ctor(1, 1, 0);
} else {
x_17 = x_7;
x_21 = x_7;
}
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_21, 0, x_20);
if (lean_is_scalar(x_9)) {
x_18 = lean_alloc_ctor(0, 2, 0);
x_22 = lean_alloc_ctor(0, 2, 0);
} else {
x_18 = x_9;
x_22 = x_9;
}
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_8);
return x_18;
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_8);
return x_22;
}
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64;
lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84;
lean_dec(x_7);
lean_dec(x_6);
x_61 = lean_ctor_get(x_4, 1);
lean_inc(x_61);
x_81 = lean_ctor_get(x_4, 1);
lean_inc(x_81);
lean_dec(x_4);
x_62 = l_Lean_Delaborator_DelabM_inhabited___closed__1;
x_63 = l_unreachable_x21___rarg(x_62);
x_64 = lean_apply_3(x_63, x_1, x_2, x_61);
return x_64;
x_82 = l_Lean_Delaborator_DelabM_inhabited___closed__1;
x_83 = l_unreachable_x21___rarg(x_82);
x_84 = lean_apply_3(x_83, x_1, x_2, x_81);
return x_84;
}
}
}
@ -18877,14 +18862,6 @@ l_Lean_Delaborator_delabSort___closed__10 = _init_l_Lean_Delaborator_delabSort__
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__10);
l_Lean_Delaborator_delabSort___closed__11 = _init_l_Lean_Delaborator_delabSort___closed__11();
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__11);
l_Lean_Delaborator_delabSort___closed__12 = _init_l_Lean_Delaborator_delabSort___closed__12();
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__12);
l_Lean_Delaborator_delabSort___closed__13 = _init_l_Lean_Delaborator_delabSort___closed__13();
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__13);
l_Lean_Delaborator_delabSort___closed__14 = _init_l_Lean_Delaborator_delabSort___closed__14();
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__14);
l_Lean_Delaborator_delabSort___closed__15 = _init_l_Lean_Delaborator_delabSort___closed__15();
lean_mark_persistent(l_Lean_Delaborator_delabSort___closed__15);
l___regBuiltin_Lean_Delaborator_delabSort___closed__1 = _init_l___regBuiltin_Lean_Delaborator_delabSort___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSort___closed__1);
res = l___regBuiltin_Lean_Delaborator_delabSort(lean_io_mk_world());

17
stage0/stdlib/Lean/Elab/Definition.c
View file

@ -20,6 +20,7 @@ lean_object* l_Lean_extractMacroScopes(lean_object*);
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_8__checkTypesAndAssign___closed__7;
lean_object* l_Lean_Elab_Command_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Elab_Command_withUsedWhen_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -28,6 +29,7 @@ lean_object* l_Lean_Elab_Term_inferType(lean_object*, lean_object*, lean_object*
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_collectUsedFVarsAtFVars___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabDefLike___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1;
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabDefLike___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabDefLike___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__4;
@ -86,7 +88,6 @@ lean_object* l_Lean_Elab_Command_mkDef___lambda__1___boxed(lean_object*, lean_ob
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_withUsedWhen(lean_object*);
lean_object* l_Lean_Elab_Term_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_elabTypeStx___rarg___closed__1;
lean_object* l_Lean_Elab_Command_collectUsedFVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_withUsedWhen___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__1;
@ -137,6 +138,7 @@ uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
extern lean_object* l_ShareCommon_State_empty;
lean_object* lean_state_sharecommon(lean_object*, lean_object*);
extern lean_object* l_Lean_levelOne;
lean_object* lean_task_pure(lean_object*);
lean_object* l___private_Lean_Elab_Command_12__addScopes___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_CollectLevelParams_main___main(lean_object*, lean_object*);
@ -1319,11 +1321,20 @@ lean_dec(x_1);
return x_11;
}
}
lean_object* _init_l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_levelOne;
x_2 = l_Lean_mkSort(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Command_withUsedWhen_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_Elab_Term_elabTypeStx___rarg___closed__1;
x_9 = l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1;
x_10 = l_Lean_Elab_Command_withUsedWhen___rarg(x_1, x_2, x_3, x_4, x_9, x_5, x_6, x_7, x_8);
return x_10;
}
@ -6885,6 +6896,8 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_removeUnused___closed__1 = _init_l_Lean_Elab_Command_removeUnused___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_removeUnused___closed__1);
l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1 = _init_l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_withUsedWhen_x27___rarg___closed__1);
l_Lean_Elab_Command_mkDef___lambda__1___closed__1 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_mkDef___lambda__1___closed__1);
l_Lean_Elab_Command_mkDef___lambda__1___closed__2 = _init_l_Lean_Elab_Command_mkDef___lambda__1___closed__2();

4
stage0/stdlib/Lean/Elab/Quotation.c
View file

@ -313,6 +313,7 @@ lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3___close
lean_object* l_List_map___main___at_Lean_Elab_Term_Quotation_oldExpandMatchSyntax___spec__1(lean_object*);
lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__41;
lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__13;
extern lean_object* l___private_Lean_Elab_Term_18__mkPairsAux___main___closed__4;
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -438,7 +439,6 @@ lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__8;
lean_object* lean_panic_fn(lean_object*, lean_object*);
extern lean_object* l_Lean_setOptionFromString___closed__1;
lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__28;
extern lean_object* l___private_Lean_Elab_Term_17__mkPairsAux___main___closed__4;
lean_object* l_ReaderT_pure___at_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__30;
lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__11;
@ -1568,7 +1568,7 @@ x_9 = l___private_Lean_Syntax_8__quoteList___main___at___private_Lean_Elab_Quota
x_10 = l_Lean_mkAppStx___closed__9;
x_11 = lean_array_push(x_10, x_8);
x_12 = lean_array_push(x_11, x_9);
x_13 = l___private_Lean_Elab_Term_17__mkPairsAux___main___closed__4;
x_13 = l___private_Lean_Elab_Term_18__mkPairsAux___main___closed__4;
x_14 = l_Lean_mkCAppStx(x_13, x_12);
x_15 = lean_array_push(x_10, x_14);
x_16 = lean_array_push(x_15, x_5);

412
stage0/stdlib/Lean/Elab/Term.c
View file

File diff suppressed because it is too large Load diff