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-02-03 20:25:39 -08:00
parent 1f359b9844
commit c763f72b79
2 changed files with 28 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Lean/Parser/Term.lean
View file

@ -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

98
stage0/stdlib/Init/Lean/Parser/Term.c
View file

@ -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());