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 2022-02-06 07:24:22 -08:00
parent 0ef5985b5f
commit e35235eec5
5 changed files with 468 additions and 657 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/CMakeLists.txt generated
View file

@ -515,6 +515,7 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
PATTERN temp EXCLUDE)
# symlink source into expected installation location for go-to-definition, if file system allows it
file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
if(${STAGE} EQUAL 0)
file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
else()

2
stage0/src/Init/System/IO.lean generated
View file

@ -421,7 +421,7 @@ where
if (← enter p) then
go p'
| FS.FileType.dir => go d.path
| _ => return ()
| _ => pure ()
end System.FilePath

16
stage0/src/Lean/Elab/LetRec.lean generated
View file

@ -59,13 +59,13 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
else
liftMacroM $ expandMatchAltsIntoMatch decl decl[3]
pure {
ref := decl,
attrs := attrs,
shortDeclName := shortDeclName,
declName := declName,
binderIds := binderIds,
type := type,
mvar := mvar,
ref := declId
attrs := attrs
shortDeclName := shortDeclName
declName := declName
binderIds := binderIds
type := type
mvar := mvar
valStx := valStx
: LetRecDeclView }
else
@ -120,7 +120,7 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
let view ← mkLetRecDeclView stx
withAuxLocalDecls view.decls fun fvars => do
for decl in view.decls, fvar in fvars do
addTermInfo (isBinder := true) decl.ref[0] fvar
addTermInfo (isBinder := true) decl.ref fvar
let values ← elabLetRecDeclValues view
let body ← elabTermEnsuringType view.body expectedType?
registerLetRecsToLift view.decls fvars values

950
stage0/stdlib/Init/System/IO.c generated
View file

File diff suppressed because it is too large Load diff

156
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

@ -2573,6 +2573,7 @@ x_37 = l_Lean_Syntax_getArg(x_14, x_36);
x_38 = l_Lean_Syntax_getArgs(x_37);
lean_dec(x_37);
x_39 = l_Lean_Syntax_getArg(x_14, x_11);
lean_inc(x_20);
x_40 = l_Lean_Elab_Term_expandOptType(x_20, x_39);
lean_dec(x_39);
x_41 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__20___lambda__1___boxed), 9, 1);
@ -2616,7 +2617,6 @@ x_53 = lean_unsigned_to_nat(3u);
x_54 = l_Lean_Syntax_getArg(x_14, x_53);
x_55 = 0;
x_56 = lean_box(x_55);
lean_inc(x_14);
x_57 = lean_alloc_closure((void*)(l_Lean_Elab_Term_expandMatchAltsIntoMatch___boxed), 5, 3);
lean_closure_set(x_57, 0, x_14);
lean_closure_set(x_57, 1, x_54);
@ -2636,7 +2636,7 @@ lean_inc(x_59);
x_60 = lean_ctor_get(x_58, 1);
lean_inc(x_60);
lean_dec(x_58);
x_61 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__20___lambda__2(x_14, x_3, x_21, x_26, x_46, x_45, x_51, x_59, x_4, x_5, x_6, x_7, x_8, x_9, x_60);
x_61 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__20___lambda__2(x_20, x_3, x_21, x_26, x_46, x_45, x_51, x_59, x_4, x_5, x_6, x_7, x_8, x_9, x_60);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -2653,7 +2653,7 @@ lean_dec(x_46);
lean_dec(x_45);
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_14);
lean_dec(x_20);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -2691,7 +2691,8 @@ lean_inc(x_67);
lean_dec(x_50);
x_68 = lean_unsigned_to_nat(4u);
x_69 = l_Lean_Syntax_getArg(x_14, x_68);
x_70 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__20___lambda__2(x_14, x_3, x_21, x_26, x_46, x_45, x_66, x_69, x_4, x_5, x_6, x_7, x_8, x_9, x_67);
lean_dec(x_14);
x_70 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__20___lambda__2(x_20, x_3, x_21, x_26, x_46, x_45, x_66, x_69, x_4, x_5, x_6, x_7, x_8, x_9, x_67);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -2706,6 +2707,7 @@ else
uint8_t x_71;
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_20);
lean_dec(x_14);
lean_dec(x_9);
lean_dec(x_8);
@ -4370,7 +4372,7 @@ uint8_t x_20;
x_20 = !lean_is_exclusive(x_4);
if (x_20 == 0)
{
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; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; lean_object* x_33;
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; lean_object* x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31;
x_21 = lean_ctor_get(x_4, 2);
lean_dec(x_21);
x_22 = lean_ctor_get(x_4, 1);
@ -4385,34 +4387,31 @@ lean_ctor_set(x_4, 1, x_26);
x_27 = lean_ctor_get(x_14, 0);
lean_inc(x_27);
lean_dec(x_14);
x_28 = lean_unsigned_to_nat(0u);
x_29 = l_Lean_Syntax_getArg(x_27, x_28);
lean_dec(x_27);
x_30 = lean_box(0);
x_31 = lean_box(0);
x_32 = 1;
x_28 = lean_box(0);
x_29 = lean_box(0);
x_30 = 1;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_33 = l_Lean_Elab_Term_addTermInfo(x_29, x_24, x_30, x_30, x_31, x_32, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_33) == 0)
x_31 = l_Lean_Elab_Term_addTermInfo(x_27, x_24, x_28, x_28, x_29, x_30, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_34; size_t x_35; size_t x_36;
x_34 = lean_ctor_get(x_33, 1);
lean_inc(x_34);
lean_dec(x_33);
x_35 = 1;
x_36 = lean_usize_add(x_3, x_35);
x_3 = x_36;
x_11 = x_34;
lean_object* x_32; size_t x_33; size_t x_34;
x_32 = lean_ctor_get(x_31, 1);
lean_inc(x_32);
lean_dec(x_31);
x_33 = 1;
x_34 = lean_usize_add(x_3, x_33);
x_3 = x_34;
x_11 = x_32;
goto _start;
}
else
{
uint8_t x_38;
uint8_t x_36;
lean_dec(x_4);
lean_dec(x_10);
lean_dec(x_9);
@ -4420,97 +4419,94 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_38 = !lean_is_exclusive(x_33);
if (x_38 == 0)
x_36 = !lean_is_exclusive(x_31);
if (x_36 == 0)
{
return x_33;
return x_31;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_33, 0);
x_40 = lean_ctor_get(x_33, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_33);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_31, 0);
x_38 = lean_ctor_get(x_31, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_31);
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
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51; lean_object* x_52;
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; lean_object* x_48;
lean_dec(x_4);
x_42 = lean_array_fget(x_15, x_16);
x_43 = lean_unsigned_to_nat(1u);
x_44 = lean_nat_add(x_16, x_43);
x_40 = lean_array_fget(x_15, x_16);
x_41 = lean_unsigned_to_nat(1u);
x_42 = lean_nat_add(x_16, x_41);
lean_dec(x_16);
x_45 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_45, 0, x_15);
lean_ctor_set(x_45, 1, x_44);
lean_ctor_set(x_45, 2, x_17);
x_46 = lean_ctor_get(x_14, 0);
lean_inc(x_46);
x_43 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_43, 0, x_15);
lean_ctor_set(x_43, 1, x_42);
lean_ctor_set(x_43, 2, x_17);
x_44 = lean_ctor_get(x_14, 0);
lean_inc(x_44);
lean_dec(x_14);
x_47 = lean_unsigned_to_nat(0u);
x_48 = l_Lean_Syntax_getArg(x_46, x_47);
lean_dec(x_46);
x_49 = lean_box(0);
x_50 = lean_box(0);
x_51 = 1;
x_45 = lean_box(0);
x_46 = lean_box(0);
x_47 = 1;
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_52 = l_Lean_Elab_Term_addTermInfo(x_48, x_42, x_49, x_49, x_50, x_51, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_52) == 0)
x_48 = l_Lean_Elab_Term_addTermInfo(x_44, x_40, x_45, x_45, x_46, x_47, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_48) == 0)
{
lean_object* x_53; size_t x_54; size_t x_55;
x_53 = lean_ctor_get(x_52, 1);
lean_inc(x_53);
lean_dec(x_52);
x_54 = 1;
x_55 = lean_usize_add(x_3, x_54);
x_3 = x_55;
x_4 = x_45;
x_11 = x_53;
lean_object* x_49; size_t x_50; size_t x_51;
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
lean_dec(x_48);
x_50 = 1;
x_51 = lean_usize_add(x_3, x_50);
x_3 = x_51;
x_4 = x_43;
x_11 = x_49;
goto _start;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
lean_dec(x_45);
lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56;
lean_dec(x_43);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
x_57 = lean_ctor_get(x_52, 0);
lean_inc(x_57);
x_58 = lean_ctor_get(x_52, 1);
lean_inc(x_58);
if (lean_is_exclusive(x_52)) {
lean_ctor_release(x_52, 0);
lean_ctor_release(x_52, 1);
x_59 = x_52;
x_53 = lean_ctor_get(x_48, 0);
lean_inc(x_53);
x_54 = lean_ctor_get(x_48, 1);
lean_inc(x_54);
if (lean_is_exclusive(x_48)) {
lean_ctor_release(x_48, 0);
lean_ctor_release(x_48, 1);
x_55 = x_48;
} else {
lean_dec_ref(x_52);
x_59 = lean_box(0);
lean_dec_ref(x_48);
x_55 = lean_box(0);
}
if (lean_is_scalar(x_59)) {
x_60 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_55)) {
x_56 = lean_alloc_ctor(1, 2, 0);
} else {
x_60 = x_59;
x_56 = x_55;
}
lean_ctor_set(x_60, 0, x_57);
lean_ctor_set(x_60, 1, x_58);
return x_60;
lean_ctor_set(x_56, 0, x_53);
lean_ctor_set(x_56, 1, x_54);
return x_56;
}
}
}