chore: udpate stage0

This commit is contained in:
Leonardo de Moura 2020-08-26 09:39:01 -07:00
parent d129d93dde
commit 524eca4d7f
3 changed files with 1674 additions and 129 deletions

View file

@ -125,6 +125,7 @@ def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts fa
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (letIdDecl <|> letPatDecl <|> letEqnsDecl)
@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «letrec» := parser!:leadPrec "letrec " >> optional ("partial ") >> letDecl >> many (", " >> letDecl) >> "; " >> termParser
def leftArrow : Parser := unicodeSymbol " ← " " <- "
def doLet := parser! "let ">> letDecl

View file

@ -205,7 +205,6 @@ lean_object* l_Lean_Parser_Command_declaration_formatter___closed__7;
lean_object* l_Lean_Parser_Command_mutualElement_formatter___closed__1;
lean_object* l_Lean_Parser_Command_mutual___closed__8;
lean_object* l_Lean_Parser_Command_visibility_formatter___closed__2;
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_export___closed__8;
lean_object* l_Lean_Parser_Command_variables_formatter___closed__3;
lean_object* l_Lean_Parser_Command_mutualElement___closed__5;
@ -260,6 +259,7 @@ lean_object* l_Lean_Parser_Command_ctor_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_declaration_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_end_formatter___closed__3;
extern lean_object* l_Lean_Parser_Term_letrec_formatter___closed__3;
lean_object* l_Lean_Parser_Command_ctor___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_open_formatter___closed__9;
lean_object* l___regBuiltin_Lean_Parser_Command_universe_parenthesizer(lean_object*);
@ -583,7 +583,6 @@ lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__1
lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_openHiding___closed__5;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_partial_formatter___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Command_end_parenthesizer___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Command_variables_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_ctor_parenthesizer___closed__4;
@ -752,6 +751,7 @@ lean_object* l_Lean_Parser_Command_openSimple___closed__1;
lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_structInstBinder;
lean_object* l_Lean_Parser_Command_attribute_parenthesizer___closed__3;
extern lean_object* l_Lean_Parser_Term_letrec___closed__2;
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__3;
lean_object* l_Lean_Parser_manyAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_export_parenthesizer___closed__1;
@ -769,7 +769,6 @@ lean_object* l_Lean_Parser_Command_structure___closed__10;
lean_object* l_Lean_Parser_Command_attrArg_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_attribute_formatter___closed__8;
lean_object* l_Lean_Parser_nonReservedSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_structure_formatter___closed__1;
lean_object* l_Lean_Parser_Command_declaration_formatter___closed__6;
@ -865,6 +864,7 @@ lean_object* l_Lean_Parser_Command_openHiding___elambda__1(lean_object*, lean_ob
lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_mutual_formatter___closed__5;
extern lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__11;
lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_example___closed__7;
@ -1210,7 +1210,6 @@ lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_eval___closed__3;
lean_object* l_Lean_Parser_Command_attributes_parenthesizer___closed__6;
lean_object* l___regBuiltin_Lean_Parser_Command_variable_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__8;
lean_object* l___regBuiltin_Lean_Parser_Command_namespace_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_structure_parenthesizer___closed__12;
lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__7;
@ -1495,7 +1494,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__11;
lean_object* l_Lean_Parser_Command_structImplicitBinder;
lean_object* l_Lean_Parser_Command_openRenaming_formatter___closed__5;
extern lean_object* l_Lean_Parser_Term_doPat_formatter___closed__4;
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_set__option___closed__8;
lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_export_parenthesizer___closed__5;
@ -1544,6 +1542,7 @@ lean_object* l_Lean_Parser_Command_structCtor___closed__5;
lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_open_formatter___closed__1;
lean_object* l_Lean_Parser_Command_private___closed__4;
extern lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_structure_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__5;
@ -1946,7 +1945,6 @@ lean_object* l_Lean_Parser_Command_structFields_parenthesizer(lean_object*, lean
lean_object* l_Lean_Parser_Command_exit;
lean_object* l_Lean_Parser_Command_namespace___closed__1;
lean_object* l_Lean_Parser_Command_structFields_formatter___closed__4;
lean_object* l_Lean_Parser_Command_partial___closed__6;
lean_object* l_Lean_Parser_Command_declaration_parenthesizer___closed__7;
lean_object* l_Lean_Parser_Command_synth_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__1;
@ -2199,7 +2197,6 @@ lean_object* l_Lean_Parser_Command_declModifiers_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_set__option___closed__6;
lean_object* l_Lean_Parser_Command_variables_formatter___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_andthen_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_structCtor___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Term_optType_formatter___closed__1;
@ -6865,55 +6862,6 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("partial ");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__5;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_partial___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Command_partial___elambda__1___closed__8;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Command_partial___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -6957,13 +6905,13 @@ lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_15, 1);
lean_inc(x_16);
lean_dec(x_15);
x_17 = l_Lean_Parser_Command_partial___elambda__1___closed__6;
x_17 = l_Lean_Parser_Term_letrec___elambda__1___closed__8;
x_18 = lean_string_dec_eq(x_16, x_17);
lean_dec(x_16);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_19 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_19, x_11);
x_21 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_22 = l_Lean_Parser_ParserState_mkNode(x_20, x_21, x_10);
@ -6982,7 +6930,7 @@ else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
lean_dec(x_15);
x_25 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_25 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_25, x_11);
x_27 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_10);
@ -6993,7 +6941,7 @@ else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_13);
x_29 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_29 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_12, x_29, x_11);
x_31 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_10);
@ -7080,13 +7028,13 @@ lean_object* x_52; lean_object* x_53; uint8_t x_54;
x_52 = lean_ctor_get(x_51, 1);
lean_inc(x_52);
lean_dec(x_51);
x_53 = l_Lean_Parser_Command_partial___elambda__1___closed__6;
x_53 = l_Lean_Parser_Term_letrec___elambda__1___closed__8;
x_54 = lean_string_dec_eq(x_52, x_53);
lean_dec(x_52);
if (x_54 == 0)
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_55 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_55 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_56 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_55, x_47);
x_57 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_58 = l_Lean_Parser_ParserState_mkNode(x_56, x_57, x_46);
@ -7109,7 +7057,7 @@ else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
lean_dec(x_51);
x_63 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_63 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_64 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_63, x_47);
x_65 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_66 = l_Lean_Parser_ParserState_mkNode(x_64, x_65, x_46);
@ -7122,7 +7070,7 @@ else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72;
lean_dec(x_49);
x_68 = l_Lean_Parser_Command_partial___elambda__1___closed__9;
x_68 = l_Lean_Parser_Term_letrec___elambda__1___closed__11;
x_69 = l_Lean_Parser_ParserState_mkErrorsAt(x_48, x_68, x_47);
x_70 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_71 = l_Lean_Parser_ParserState_mkNode(x_69, x_70, x_46);
@ -7148,45 +7096,36 @@ return x_73;
lean_object* _init_l_Lean_Parser_Command_partial___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__6;
x_2 = l_Lean_Parser_symbolInfo(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_letrec___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_partial___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Command_partial___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_partial___closed__3;
x_3 = l_Lean_Parser_Command_partial___closed__2;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___closed__5() {
lean_object* _init_l_Lean_Parser_Command_partial___closed__4() {
_start:
{
lean_object* x_1;
@ -7194,12 +7133,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_partial___elambda__1), 2,
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_partial___closed__6() {
lean_object* _init_l_Lean_Parser_Command_partial___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_partial___closed__4;
x_2 = l_Lean_Parser_Command_partial___closed__5;
x_1 = l_Lean_Parser_Command_partial___closed__3;
x_2 = l_Lean_Parser_Command_partial___closed__4;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -7210,7 +7149,7 @@ lean_object* _init_l_Lean_Parser_Command_partial() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_partial___closed__6;
x_1 = l_Lean_Parser_Command_partial___closed__5;
return x_1;
}
}
@ -25826,20 +25765,10 @@ return x_5;
lean_object* _init_l_Lean_Parser_Command_partial_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__5;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter___boxed), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_partial_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_partial___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Command_partial_formatter___closed__2;
x_3 = l_Lean_Parser_Term_letrec_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -25852,7 +25781,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Command_partial_formatter___closed__1;
x_7 = l_Lean_Parser_Command_partial_formatter___closed__3;
x_7 = l_Lean_Parser_Command_partial_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
}
@ -50610,16 +50539,6 @@ l_Lean_Parser_Command_partial___elambda__1___closed__3 = _init_l_Lean_Parser_Com
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__3);
l_Lean_Parser_Command_partial___elambda__1___closed__4 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__4);
l_Lean_Parser_Command_partial___elambda__1___closed__5 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__5);
l_Lean_Parser_Command_partial___elambda__1___closed__6 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__6);
l_Lean_Parser_Command_partial___elambda__1___closed__7 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__7);
l_Lean_Parser_Command_partial___elambda__1___closed__8 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__8);
l_Lean_Parser_Command_partial___elambda__1___closed__9 = _init_l_Lean_Parser_Command_partial___elambda__1___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_partial___elambda__1___closed__9);
l_Lean_Parser_Command_partial___closed__1 = _init_l_Lean_Parser_Command_partial___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_partial___closed__1);
l_Lean_Parser_Command_partial___closed__2 = _init_l_Lean_Parser_Command_partial___closed__2();
@ -50630,8 +50549,6 @@ l_Lean_Parser_Command_partial___closed__4 = _init_l_Lean_Parser_Command_partial_
lean_mark_persistent(l_Lean_Parser_Command_partial___closed__4);
l_Lean_Parser_Command_partial___closed__5 = _init_l_Lean_Parser_Command_partial___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_partial___closed__5);
l_Lean_Parser_Command_partial___closed__6 = _init_l_Lean_Parser_Command_partial___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_partial___closed__6);
l_Lean_Parser_Command_partial = _init_l_Lean_Parser_Command_partial();
lean_mark_persistent(l_Lean_Parser_Command_partial);
l_Lean_Parser_Command_declModifiers___elambda__1___closed__1 = _init_l_Lean_Parser_Command_declModifiers___elambda__1___closed__1();
@ -51577,8 +51494,6 @@ l_Lean_Parser_Command_partial_formatter___closed__1 = _init_l_Lean_Parser_Comman
lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__1);
l_Lean_Parser_Command_partial_formatter___closed__2 = _init_l_Lean_Parser_Command_partial_formatter___closed__2();
lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__2);
l_Lean_Parser_Command_partial_formatter___closed__3 = _init_l_Lean_Parser_Command_partial_formatter___closed__3();
lean_mark_persistent(l_Lean_Parser_Command_partial_formatter___closed__3);
l_Lean_Parser_Command_declModifiers_formatter___closed__1 = _init_l_Lean_Parser_Command_declModifiers_formatter___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_declModifiers_formatter___closed__1);
l_Lean_Parser_Command_declModifiers_formatter___closed__2 = _init_l_Lean_Parser_Command_declModifiers_formatter___closed__2();

File diff suppressed because it is too large Load diff