From c763f72b791e46b8d86fcf677f06fbec5b1cd993 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Feb 2020 20:25:39 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Parser/Term.lean | 2 +- stage0/stdlib/Init/Lean/Parser/Term.c | 98 ++++++++------------------- 2 files changed, 28 insertions(+), 72 deletions(-) diff --git a/stage0/src/Init/Lean/Parser/Term.lean b/stage0/src/Init/Lean/Parser/Term.lean index 32e0cd61db..18e80a7d6c 100644 --- a/stage0/src/Init/Lean/Parser/Term.lean +++ b/stage0/src/Init/Lean/Parser/Term.lean @@ -116,7 +116,7 @@ def doExpr := parser! termParser def doElem := doLet <|> doId <|> doPat <|> doExpr def doSeq := sepBy1 doElem "; " def bracketedDoSeq := parser! "{" >> doSeq >> "}" -@[builtinTermParser] def liftMethod := parser! checkRBPGreater (appPrec-1) "expected parentheses monad lift operator" >> leftArrow >> termParser +@[builtinTermParser] def liftMethod := parser! leftArrow >> termParser @[builtinTermParser] def «do» := parser! "do " >> (bracketedDoSeq <|> doSeq) @[builtinTermParser] def not := parser! symbol "¬" 40 >> termParser 40 diff --git a/stage0/stdlib/Init/Lean/Parser/Term.c b/stage0/stdlib/Init/Lean/Parser/Term.c index e188ba30e6..b1be3fd1d9 100644 --- a/stage0/stdlib/Init/Lean/Parser/Term.c +++ b/stage0/stdlib/Init/Lean/Parser/Term.c @@ -392,7 +392,6 @@ lean_object* l_Lean_Parser_Term_mod___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__6; lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*); lean_object* l_Lean_Parser_Term_instBinder___closed__3; -lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_and; lean_object* l_Lean_Parser_Term_gt___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1(lean_object*, lean_object*); @@ -1082,7 +1081,6 @@ lean_object* l_Lean_Parser_Term_namedArgument___closed__2; lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_letEqnsDecl; lean_object* l_Lean_Parser_Term_cons___closed__2; -lean_object* l_Lean_Parser_Term_liftMethod___closed__6; lean_object* l_Lean_Parser_Term_dollarProj___closed__2; lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_binderDefault___closed__1; @@ -29117,14 +29115,6 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__5() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("expected parentheses monad lift operator"); -return x_1; -} -} lean_object* l_Lean_Parser_Term_liftMethod___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -29169,7 +29159,7 @@ return x_8; } else { -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_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_inc(x_7); x_13 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7); lean_dec(x_6); @@ -29177,52 +29167,32 @@ x_14 = lean_ctor_get(x_13, 0); lean_inc(x_14); x_15 = lean_array_get_size(x_14); lean_dec(x_14); -x_16 = l_Lean_Parser_Term_borrowed___elambda__1___closed__7; -x_17 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__5; -x_18 = l_Lean_Parser_checkRBPGreaterFn(x_16, x_17, x_1, x_13); -x_19 = lean_ctor_get(x_18, 3); -lean_inc(x_19); -if (lean_obj_tag(x_19) == 0) -{ -lean_object* x_20; lean_object* x_21; lean_inc(x_1); -x_20 = l_Lean_Parser_Term_leftArrow___elambda__1(x_1, x_18); -x_21 = lean_ctor_get(x_20, 3); -lean_inc(x_21); -if (lean_obj_tag(x_21) == 0) +x_16 = l_Lean_Parser_Term_leftArrow___elambda__1(x_1, x_13); +x_17 = lean_ctor_get(x_16, 3); +lean_inc(x_17); +if (lean_obj_tag(x_17) == 0) { -lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_22 = l_Lean_Parser_termParser___closed__2; -x_23 = lean_unsigned_to_nat(0u); -x_24 = l_Lean_Parser_categoryParser___elambda__1(x_22, x_23, x_1, x_20); -x_25 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_15); -x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_10, x_7); +lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_18 = l_Lean_Parser_termParser___closed__2; +x_19 = lean_unsigned_to_nat(0u); +x_20 = l_Lean_Parser_categoryParser___elambda__1(x_18, x_19, x_1, x_16); +x_21 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; +x_22 = l_Lean_Parser_ParserState_mkNode(x_20, x_21, x_15); +x_23 = l_Lean_Parser_mergeOrElseErrors(x_22, x_10, x_7); lean_dec(x_7); -return x_27; +return x_23; } else { -lean_object* x_28; lean_object* x_29; lean_object* x_30; -lean_dec(x_21); +lean_object* x_24; lean_object* x_25; lean_object* x_26; +lean_dec(x_17); lean_dec(x_1); -x_28 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_29 = l_Lean_Parser_ParserState_mkNode(x_20, x_28, x_15); -x_30 = l_Lean_Parser_mergeOrElseErrors(x_29, x_10, x_7); +x_24 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; +x_25 = l_Lean_Parser_ParserState_mkNode(x_16, x_24, x_15); +x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_10, x_7); lean_dec(x_7); -return x_30; -} -} -else -{ -lean_object* x_31; lean_object* x_32; lean_object* x_33; -lean_dec(x_19); -lean_dec(x_1); -x_31 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_32 = l_Lean_Parser_ParserState_mkNode(x_18, x_31, x_15); -x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_10, x_7); -lean_dec(x_7); -return x_33; +return x_26; } } } @@ -29246,35 +29216,25 @@ lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_epsilonInfo; +x_1 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; x_2 = l_Lean_Parser_Term_liftMethod___closed__1; -x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__3() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_liftMethod___closed__2; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__4() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_liftMethod___closed__3; +x_3 = l_Lean_Parser_Term_liftMethod___closed__2; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__5() { +lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__4() { _start: { lean_object* x_1; @@ -29282,12 +29242,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_liftMethod___elambda__1), 2, return x_1; } } -lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__6() { +lean_object* _init_l_Lean_Parser_Term_liftMethod___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_liftMethod___closed__4; -x_2 = l_Lean_Parser_Term_liftMethod___closed__5; +x_1 = l_Lean_Parser_Term_liftMethod___closed__3; +x_2 = l_Lean_Parser_Term_liftMethod___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); @@ -29298,7 +29258,7 @@ lean_object* _init_l_Lean_Parser_Term_liftMethod() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_liftMethod___closed__6; +x_1 = l_Lean_Parser_Term_liftMethod___closed__5; return x_1; } } @@ -39861,8 +39821,6 @@ l_Lean_Parser_Term_liftMethod___elambda__1___closed__3 = _init_l_Lean_Parser_Ter lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__3); l_Lean_Parser_Term_liftMethod___elambda__1___closed__4 = _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__4(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__4); -l_Lean_Parser_Term_liftMethod___elambda__1___closed__5 = _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__5); l_Lean_Parser_Term_liftMethod___closed__1 = _init_l_Lean_Parser_Term_liftMethod___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod___closed__1); l_Lean_Parser_Term_liftMethod___closed__2 = _init_l_Lean_Parser_Term_liftMethod___closed__2(); @@ -39873,8 +39831,6 @@ l_Lean_Parser_Term_liftMethod___closed__4 = _init_l_Lean_Parser_Term_liftMethod_ lean_mark_persistent(l_Lean_Parser_Term_liftMethod___closed__4); l_Lean_Parser_Term_liftMethod___closed__5 = _init_l_Lean_Parser_Term_liftMethod___closed__5(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod___closed__5); -l_Lean_Parser_Term_liftMethod___closed__6 = _init_l_Lean_Parser_Term_liftMethod___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_liftMethod___closed__6); l_Lean_Parser_Term_liftMethod = _init_l_Lean_Parser_Term_liftMethod(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod); res = l___regBuiltinParser_Lean_Parser_Term_liftMethod(lean_io_mk_world());