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-01-30 18:34:52 -08:00
parent 410d295429
commit f8dd8d80cc
12 changed files with 1308 additions and 1494 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,7 +23,7 @@ namespace Level
@[builtinLevelParser] def hole := parser! "_"
@[builtinLevelParser] def num := parser! numLit
@[builtinLevelParser] def ident := parser! ident
@[builtinLevelParser] def addLit := tparser! pushLeading >> symbol "+" (65:Nat) >> numLit
@[builtinLevelParser] def addLit := tparser! symbol "+" (65:Nat) >> numLit
end Level

1
stage0/src/Init/Lean/Parser/Parser.lean
View file

@ -1714,6 +1714,7 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
| _, ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂
| _, ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
| _, ParserDescr.node k d => node k <$> compileParserDescr d
| ParserKind.trailing, ParserDescr.trailingNode k d => trailingNode k <$> compileParserDescr d
| _, ParserDescr.symbol tk lbp => pure $ symbolAux tk lbp
| _, ParserDescr.numLit => pure $ numLit
| _, ParserDescr.strLit => pure $ strLit

8
stage0/src/Init/Lean/Parser/Syntax.lean
View file

@ -35,10 +35,10 @@ namespace Syntax
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser appPrec >> syntaxParser appPrec
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser appPrec >> syntaxParser appPrec
@[builtinSyntaxParser] def optional := tparser! pushLeading >> symbolAux "?" none
@[builtinSyntaxParser] def many := tparser! pushLeading >> symbolAux "*" none
@[builtinSyntaxParser] def many1 := tparser! pushLeading >> symbolAux "+" none
@[builtinSyntaxParser] def orelse := tparser! pushLeading >> " <|> " >> syntaxParser 1
@[builtinSyntaxParser] def optional := tparser! symbolAux "?" none
@[builtinSyntaxParser] def many := tparser! symbolAux "*" none
@[builtinSyntaxParser] def many1 := tparser! symbolAux "+" none
@[builtinSyntaxParser] def orelse := tparser! " <|> " >> syntaxParser 1
end Syntax

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

@ -54,7 +54,7 @@ def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "
@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1
@[builtinTacticParser] def orelse := tparser! " <|> " >> tacticParser 1
end Tactic

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

@ -17,16 +17,16 @@ namespace Term
/- Helper functions for defining simple parsers -/
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser (lbp - 1)
symbol sym lbp >> termParser (lbp - 1)
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
unicodeSymbol sym asciiSym lbp >> termParser lbp
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser lbp
symbol sym lbp >> termParser lbp
/- Built-in parsers -/
-- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
@ -122,18 +122,18 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def uminus := parser! "-" >> termParser 100
def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> many1 ((toTrailing namedArgument) <|> termParser appPrec)
@[builtinTermParser] def app := tparser! many1 ((toTrailing namedArgument) <|> termParser appPrec)
def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
@[builtinTermParser] def sortApp := tparser! checkIsSort >> pushLeading >> levelParser appPrec
@[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
@[builtinTermParser] def sortApp := tparser! checkIsSort >> levelParser appPrec
@[builtinTermParser] def proj := tparser! symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
@[builtinTermParser] def arrayRef := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]"
@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" (appPrec+1) >> termParser >>"]"
@[builtinTermParser] def dollar := tparser! try (pushLeading >> dollarSymbol >> checkWsBefore "space expected") >> termParser 0
@[builtinTermParser] def dollarProj := tparser! pushLeading >> symbol "$." 1 >> (fieldIdx <|> ident)
@[builtinTermParser] def dollar := tparser! try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
@[builtinTermParser] def dollarProj := tparser! symbol "$." 1 >> (fieldIdx <|> ident)
@[builtinTermParser] def «where» := tparser! pushLeading >> symbol " where " 1 >> sepBy1 (toTrailing letDecl) (group ("; " >> " where "))
@[builtinTermParser] def «where» := tparser! symbol " where " 1 >> sepBy1 (toTrailing letDecl) (group ("; " >> " where "))
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90

2
stage0/src/Init/LeanInit.lean
View file

@ -149,6 +149,7 @@ inductive ParserDescrCore : ParserKind → Type
| sepBy {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| sepBy1 {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| node {k : ParserKind} : Name → ParserDescrCore k → ParserDescrCore k
| trailingNode : Name → ParserDescrCore ParserKind.trailing → ParserDescrCore ParserKind.trailing
| symbol {k : ParserKind} : String → Option Nat → ParserDescrCore k
| nonReservedSymbol : String → Bool → ParserDescrCore ParserKind.leading
| numLit {k : ParserKind} : ParserDescrCore k
@ -174,6 +175,7 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
@[matchPattern] abbrev ParserDescr.sepBy := @ParserDescrCore.sepBy
@[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
@[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
@[matchPattern] abbrev ParserDescr.trailingNode := @ParserDescrCore.trailingNode
@[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
@[matchPattern] abbrev ParserDescr.numLit := @ParserDescrCore.numLit
@[matchPattern] abbrev ParserDescr.strLit := @ParserDescrCore.strLit

166
stage0/stdlib/Init/Lean/Parser/Level.c
View file

@ -108,7 +108,6 @@ lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1;
lean_object* l_Lean_Parser_Level_paren___closed__4;
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__3;
lean_object* l_Lean_Parser_Level_paren___closed__9;
lean_object* l_Lean_Parser_Level_addLit___closed__7;
lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6;
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__2;
@ -130,7 +129,6 @@ lean_object* l_Lean_Parser_Level_max___closed__5;
lean_object* l_Lean_Parser_Level_num___closed__3;
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__6;
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
extern lean_object* l_Lean_mkHole___closed__1;
@ -2081,7 +2079,7 @@ return x_3;
lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_4 = l_Lean_Parser_Level_addLit___elambda__1___closed__4;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
@ -2089,98 +2087,88 @@ x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
x_16 = lean_ctor_get(x_3, 1);
lean_inc(x_16);
lean_inc(x_2);
x_10 = l_Lean_Parser_tokenFn(x_2, x_3);
x_11 = lean_ctor_get(x_10, 3);
lean_inc(x_11);
if (lean_obj_tag(x_11) == 0)
x_17 = l_Lean_Parser_tokenFn(x_2, x_3);
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_12);
lean_dec(x_12);
if (lean_obj_tag(x_13) == 2)
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
x_20 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_19);
lean_dec(x_19);
if (lean_obj_tag(x_20) == 2)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_16 = lean_string_dec_eq(x_14, x_15);
lean_dec(x_14);
if (x_16 == 0)
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_23 = lean_string_dec_eq(x_21, x_22);
lean_dec(x_21);
if (x_23 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_17 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_18 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_17, x_9);
x_19 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_20 = l_Lean_Parser_ParserState_mkTrailingNode(x_18, x_19, x_7);
lean_dec(x_7);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_9);
x_21 = lean_apply_3(x_5, x_1, x_2, x_10);
x_22 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_7);
lean_dec(x_7);
return x_23;
}
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_13);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
lean_object* x_24; lean_object* x_25;
x_24 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_24, x_9);
x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_7);
lean_dec(x_7);
return x_27;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
x_8 = x_25;
goto block_15;
}
else
{
lean_dec(x_16);
x_8 = x_17;
goto block_15;
}
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
lean_dec(x_11);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
lean_object* x_26; lean_object* x_27;
lean_dec(x_20);
x_26 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_26, x_16);
x_8 = x_27;
goto block_15;
}
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_18);
x_28 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_10, x_28, x_9);
x_30 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_31 = l_Lean_Parser_ParserState_mkTrailingNode(x_29, x_30, x_7);
lean_dec(x_7);
return x_31;
x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_28, x_16);
x_8 = x_29;
goto block_15;
}
block_15:
{
lean_object* x_9;
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_apply_3(x_5, x_1, x_2, x_8);
x_11 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_12 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_11, x_7);
lean_dec(x_7);
return x_12;
}
else
{
lean_object* x_32; lean_object* x_33;
lean_dec(x_8);
lean_object* x_13; lean_object* x_14;
lean_dec(x_9);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_32 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_33 = l_Lean_Parser_ParserState_mkTrailingNode(x_3, x_32, x_7);
x_13 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_14 = l_Lean_Parser_ParserState_mkTrailingNode(x_8, x_13, x_7);
lean_dec(x_7);
return x_33;
return x_14;
}
}
}
}
@ -2220,23 +2208,13 @@ lean_object* _init_l_Lean_Parser_Level_addLit___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Level_addLit___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
x_2 = l_Lean_Parser_Level_addLit___closed__4;
x_2 = l_Lean_Parser_Level_addLit___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___closed__6() {
lean_object* _init_l_Lean_Parser_Level_addLit___closed__5() {
_start:
{
lean_object* x_1;
@ -2244,12 +2222,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Level_addLit___elambda__1), 3, 0)
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Level_addLit___closed__7() {
lean_object* _init_l_Lean_Parser_Level_addLit___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_addLit___closed__5;
x_2 = l_Lean_Parser_Level_addLit___closed__6;
x_1 = l_Lean_Parser_Level_addLit___closed__4;
x_2 = l_Lean_Parser_Level_addLit___closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -2260,7 +2238,7 @@ lean_object* _init_l_Lean_Parser_Level_addLit() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Level_addLit___closed__7;
x_1 = l_Lean_Parser_Level_addLit___closed__6;
return x_1;
}
}
@ -2504,8 +2482,6 @@ l_Lean_Parser_Level_addLit___closed__5 = _init_l_Lean_Parser_Level_addLit___clos
lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__5);
l_Lean_Parser_Level_addLit___closed__6 = _init_l_Lean_Parser_Level_addLit___closed__6();
lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__6);
l_Lean_Parser_Level_addLit___closed__7 = _init_l_Lean_Parser_Level_addLit___closed__7();
lean_mark_persistent(l_Lean_Parser_Level_addLit___closed__7);
l_Lean_Parser_Level_addLit = _init_l_Lean_Parser_Level_addLit();
lean_mark_persistent(l_Lean_Parser_Level_addLit);
res = l___regBuiltinParser_Lean_Parser_Level_addLit(lean_io_mk_world());

274
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

@ -32573,7 +32573,7 @@ return x_267;
}
}
}
case 10:
case 11:
{
lean_object* x_268; lean_object* x_269; lean_object* x_270; lean_object* x_271; lean_object* x_272; lean_object* x_273; lean_object* x_274;
lean_dec(x_1);
@ -32595,7 +32595,7 @@ x_274 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_274, 0, x_273);
return x_274;
}
case 11:
case 12:
{
lean_object* x_275; uint8_t x_276; lean_object* x_277; lean_object* x_278; lean_object* x_279; lean_object* x_280; lean_object* x_281;
lean_dec(x_1);
@ -32616,7 +32616,7 @@ x_281 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_281, 0, x_280);
return x_281;
}
case 12:
case 13:
{
lean_object* x_282; lean_object* x_283;
lean_dec(x_3);
@ -32626,7 +32626,7 @@ x_283 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_283, 0, x_282);
return x_283;
}
case 13:
case 14:
{
lean_object* x_284; lean_object* x_285;
lean_dec(x_3);
@ -32636,7 +32636,7 @@ x_285 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_285, 0, x_284);
return x_285;
}
case 14:
case 15:
{
lean_object* x_286; lean_object* x_287;
lean_dec(x_3);
@ -32646,7 +32646,7 @@ x_287 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_287, 0, x_286);
return x_287;
}
case 15:
case 16:
{
lean_object* x_288; lean_object* x_289;
lean_dec(x_3);
@ -32656,7 +32656,7 @@ x_289 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_289, 0, x_288);
return x_289;
}
case 16:
case 17:
{
lean_object* x_290; lean_object* x_291;
lean_dec(x_3);
@ -33712,110 +33712,194 @@ return x_561;
}
case 10:
{
lean_object* x_562; lean_object* x_563; lean_object* x_564; lean_object* x_565; lean_object* x_566; lean_object* x_567; lean_object* x_568;
lean_dec(x_1);
lean_object* x_562; lean_object* x_563; lean_object* x_564;
x_562 = lean_ctor_get(x_3, 0);
lean_inc(x_562);
x_563 = lean_ctor_get(x_3, 1);
lean_inc(x_563);
lean_dec(x_3);
x_564 = l_String_trim(x_562);
x_564 = l_Lean_Parser_compileParserDescr___main(x_1, x_2, x_563);
if (lean_obj_tag(x_564) == 0)
{
uint8_t x_565;
lean_dec(x_562);
lean_inc(x_564);
x_565 = l_Lean_Parser_symbolInfo(x_564, x_563);
x_566 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean_closure_set(x_566, 0, x_564);
x_567 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_567, 0, x_565);
lean_ctor_set(x_567, 1, x_566);
x_568 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_568, 0, x_567);
return x_568;
}
case 12:
x_565 = !lean_is_exclusive(x_564);
if (x_565 == 0)
{
lean_object* x_569; lean_object* x_570;
lean_dec(x_3);
lean_dec(x_1);
x_569 = l_Lean_Parser_numLit(x_2);
x_570 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_570, 0, x_569);
return x_570;
}
case 13:
{
lean_object* x_571; lean_object* x_572;
lean_dec(x_3);
lean_dec(x_1);
x_571 = l_Lean_Parser_strLit(x_2);
x_572 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_572, 0, x_571);
return x_572;
}
case 14:
{
lean_object* x_573; lean_object* x_574;
lean_dec(x_3);
lean_dec(x_1);
x_573 = l_Lean_Parser_charLit(x_2);
x_574 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_574, 0, x_573);
return x_574;
}
case 15:
{
lean_object* x_575; lean_object* x_576;
lean_dec(x_3);
lean_dec(x_1);
x_575 = l_Lean_Parser_nameLit(x_2);
x_576 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_576, 0, x_575);
return x_576;
}
case 16:
{
lean_object* x_577; lean_object* x_578;
lean_dec(x_3);
lean_dec(x_1);
x_577 = l_Lean_Parser_ident(x_2);
x_578 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_578, 0, x_577);
return x_578;
}
case 17:
{
lean_object* x_579;
lean_dec(x_1);
x_579 = l_Lean_Parser_compileParserDescr___main___closed__1;
return x_579;
}
default:
{
lean_object* x_580; lean_object* x_581; lean_object* x_582;
x_580 = lean_ctor_get(x_3, 0);
lean_inc(x_580);
x_581 = lean_ctor_get(x_3, 1);
lean_inc(x_581);
lean_dec(x_3);
x_582 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_580);
if (lean_obj_tag(x_582) == 0)
{
lean_object* x_583;
lean_dec(x_581);
x_583 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_580);
return x_583;
return x_564;
}
else
{
lean_object* x_584; lean_object* x_585;
lean_dec(x_582);
x_584 = l_Lean_Parser_categoryParser(x_2, x_580, x_581);
lean_object* x_566; lean_object* x_567;
x_566 = lean_ctor_get(x_564, 0);
lean_inc(x_566);
lean_dec(x_564);
x_567 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_567, 0, x_566);
return x_567;
}
}
else
{
uint8_t x_568;
x_568 = !lean_is_exclusive(x_564);
if (x_568 == 0)
{
lean_object* x_569; lean_object* x_570; lean_object* x_571; lean_object* x_572; uint8_t x_573; lean_object* x_574; lean_object* x_575; lean_object* x_576;
x_569 = lean_ctor_get(x_564, 0);
x_570 = lean_ctor_get(x_569, 0);
lean_inc(x_570);
lean_inc(x_562);
x_571 = l_Lean_Parser_nodeInfo(x_562, x_570);
x_572 = lean_ctor_get(x_569, 1);
lean_inc(x_572);
lean_dec(x_569);
x_573 = 1;
x_574 = lean_box(x_573);
x_575 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn___boxed), 6, 3);
lean_closure_set(x_575, 0, x_574);
lean_closure_set(x_575, 1, x_562);
lean_closure_set(x_575, 2, x_572);
x_576 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_576, 0, x_571);
lean_ctor_set(x_576, 1, x_575);
lean_ctor_set(x_564, 0, x_576);
return x_564;
}
else
{
lean_object* x_577; lean_object* x_578; lean_object* x_579; lean_object* x_580; uint8_t x_581; lean_object* x_582; lean_object* x_583; lean_object* x_584; lean_object* x_585;
x_577 = lean_ctor_get(x_564, 0);
lean_inc(x_577);
lean_dec(x_564);
x_578 = lean_ctor_get(x_577, 0);
lean_inc(x_578);
lean_inc(x_562);
x_579 = l_Lean_Parser_nodeInfo(x_562, x_578);
x_580 = lean_ctor_get(x_577, 1);
lean_inc(x_580);
lean_dec(x_577);
x_581 = 1;
x_582 = lean_box(x_581);
x_583 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn___boxed), 6, 3);
lean_closure_set(x_583, 0, x_582);
lean_closure_set(x_583, 1, x_562);
lean_closure_set(x_583, 2, x_580);
x_584 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_584, 0, x_579);
lean_ctor_set(x_584, 1, x_583);
x_585 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_585, 0, x_584);
return x_585;
}
}
}
case 11:
{
lean_object* x_586; lean_object* x_587; lean_object* x_588; lean_object* x_589; lean_object* x_590; lean_object* x_591; lean_object* x_592;
lean_dec(x_1);
x_586 = lean_ctor_get(x_3, 0);
lean_inc(x_586);
x_587 = lean_ctor_get(x_3, 1);
lean_inc(x_587);
lean_dec(x_3);
x_588 = l_String_trim(x_586);
lean_dec(x_586);
lean_inc(x_588);
x_589 = l_Lean_Parser_symbolInfo(x_588, x_587);
x_590 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
lean_closure_set(x_590, 0, x_588);
x_591 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_591, 0, x_589);
lean_ctor_set(x_591, 1, x_590);
x_592 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_592, 0, x_591);
return x_592;
}
case 13:
{
lean_object* x_593; lean_object* x_594;
lean_dec(x_3);
lean_dec(x_1);
x_593 = l_Lean_Parser_numLit(x_2);
x_594 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_594, 0, x_593);
return x_594;
}
case 14:
{
lean_object* x_595; lean_object* x_596;
lean_dec(x_3);
lean_dec(x_1);
x_595 = l_Lean_Parser_strLit(x_2);
x_596 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_596, 0, x_595);
return x_596;
}
case 15:
{
lean_object* x_597; lean_object* x_598;
lean_dec(x_3);
lean_dec(x_1);
x_597 = l_Lean_Parser_charLit(x_2);
x_598 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_598, 0, x_597);
return x_598;
}
case 16:
{
lean_object* x_599; lean_object* x_600;
lean_dec(x_3);
lean_dec(x_1);
x_599 = l_Lean_Parser_nameLit(x_2);
x_600 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_600, 0, x_599);
return x_600;
}
case 17:
{
lean_object* x_601; lean_object* x_602;
lean_dec(x_3);
lean_dec(x_1);
x_601 = l_Lean_Parser_ident(x_2);
x_602 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_602, 0, x_601);
return x_602;
}
case 18:
{
lean_object* x_603;
lean_dec(x_1);
x_603 = l_Lean_Parser_compileParserDescr___main___closed__1;
return x_603;
}
default:
{
lean_object* x_604; lean_object* x_605; lean_object* x_606;
x_604 = lean_ctor_get(x_3, 0);
lean_inc(x_604);
x_605 = lean_ctor_get(x_3, 1);
lean_inc(x_605);
lean_dec(x_3);
x_606 = l_PersistentHashMap_find_x3f___at_Lean_Parser_addLeadingParser___spec__1(x_1, x_604);
if (lean_obj_tag(x_606) == 0)
{
lean_object* x_607;
lean_dec(x_605);
x_607 = l_Lean_Parser_throwUnknownParserCategory___rarg(x_604);
return x_607;
}
else
{
lean_object* x_608; lean_object* x_609;
lean_dec(x_606);
x_608 = l_Lean_Parser_categoryParser(x_2, x_604, x_605);
x_609 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_609, 0, x_608);
return x_609;
}
}
}
}
}
}

589
stage0/stdlib/Init/Lean/Parser/Syntax.c
View file

@ -353,7 +353,6 @@ lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__3;
lean_object* l_Lean_Parser_precedenceLit___closed__1;
lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__3;
lean_object* l_Lean_Parser_Syntax_orelse___closed__6;
lean_object* l_Lean_Parser_Syntax_char___closed__1;
lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__3;
@ -445,7 +444,6 @@ lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__2;
lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_paren___closed__2;
lean_object* l_Lean_Parser_Command_mixfixKind___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_many1___closed__5;
extern lean_object* l_Lean_Parser_Term_haveAssign___closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_num(lean_object*);
lean_object* l_Lean_Parser_Command_macro___closed__6;
@ -483,7 +481,6 @@ lean_object* l_Lean_Parser_Syntax_many1___closed__3;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__2;
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
lean_object* l_Lean_Parser_Command_infix___closed__3;
lean_object* l_Lean_Parser_Syntax_optional___closed__5;
lean_object* l_Lean_Parser_Syntax_ident___closed__4;
lean_object* l_Lean_Parser_Syntax_atom___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__4;
@ -494,6 +491,7 @@ extern lean_object* l_Lean_Parser_Term_match___elambda__1___closed__9;
lean_object* l_Lean_Parser_maxPrec___closed__5;
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__6;
lean_object* l_Lean_Parser_Command_notation___closed__1;
extern lean_object* l_Lean_Parser_mkAntiquotAux___closed__11;
lean_object* l_Lean_Parser_Command_macroTailCommand___closed__4;
lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__7;
lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1(lean_object*, lean_object*, lean_object*);
@ -614,7 +612,6 @@ lean_object* l_Lean_Parser_Syntax_atom___closed__2;
lean_object* l_Lean_Parser_precedence___closed__2;
lean_object* l_Lean_Parser_Syntax_char___elambda__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
extern lean_object* l_Lean_Parser_mkAntiquotAux___closed__13;
lean_object* l_Lean_Parser_Command_optKind___closed__3;
lean_object* l_Lean_Parser_Command_infixr___closed__4;
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__3;
@ -4211,90 +4208,74 @@ return x_3;
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_object* x_8; lean_object* x_9;
x_8 = lean_ctor_get(x_6, 0);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 2)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
x_13 = lean_string_dec_eq(x_11, x_12);
lean_dec(x_11);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
x_16 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
lean_dec(x_4);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19;
lean_dec(x_6);
x_18 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
lean_dec(x_4);
return x_19;
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_10);
x_20 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
x_22 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
lean_dec(x_4);
return x_23;
}
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
lean_dec(x_8);
x_24 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
x_26 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
if (lean_obj_tag(x_9) == 2)
{
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_Parser_Term_namedHole___elambda__1___closed__5;
x_12 = lean_string_dec_eq(x_10, x_11);
lean_dec(x_10);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_13 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
x_15 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
lean_dec(x_4);
return x_27;
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_5);
x_17 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
lean_dec(x_4);
return x_18;
}
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_5);
lean_dec(x_1);
x_28 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_9);
x_19 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
x_21 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
lean_dec(x_4);
return x_29;
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_7);
x_23 = l_Lean_Parser_Term_namedHole___elambda__1___closed__8;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
x_25 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
lean_dec(x_4);
return x_26;
}
}
}
@ -4320,23 +4301,13 @@ lean_object* _init_l_Lean_Parser_Syntax_optional___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Syntax_optional___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_optional___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Syntax_optional___closed__2;
x_2 = l_Lean_Parser_Syntax_optional___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__3() {
_start:
{
lean_object* x_1;
@ -4344,12 +4315,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_optional___elambda__1___bo
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__5() {
lean_object* _init_l_Lean_Parser_Syntax_optional___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_optional___closed__3;
x_2 = l_Lean_Parser_Syntax_optional___closed__4;
x_1 = l_Lean_Parser_Syntax_optional___closed__2;
x_2 = l_Lean_Parser_Syntax_optional___closed__3;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -4360,7 +4331,7 @@ lean_object* _init_l_Lean_Parser_Syntax_optional() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Syntax_optional___closed__5;
x_1 = l_Lean_Parser_Syntax_optional___closed__4;
return x_1;
}
}
@ -4438,90 +4409,74 @@ return x_3;
lean_object* l_Lean_Parser_Syntax_many___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_object* x_8; lean_object* x_9;
x_8 = lean_ctor_get(x_6, 0);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 2)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Parser_mkAntiquotAux___closed__10;
x_13 = lean_string_dec_eq(x_11, x_12);
lean_dec(x_11);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
x_16 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
lean_dec(x_4);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19;
lean_dec(x_6);
x_18 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
lean_dec(x_4);
return x_19;
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_10);
x_20 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
x_22 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
lean_dec(x_4);
return x_23;
}
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
lean_dec(x_8);
x_24 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
x_26 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
if (lean_obj_tag(x_9) == 2)
{
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_Parser_mkAntiquotAux___closed__10;
x_12 = lean_string_dec_eq(x_10, x_11);
lean_dec(x_10);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_13 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
x_15 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
lean_dec(x_4);
return x_27;
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_5);
x_17 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
lean_dec(x_4);
return x_18;
}
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_5);
lean_dec(x_1);
x_28 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_9);
x_19 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
x_21 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
lean_dec(x_4);
return x_29;
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_7);
x_23 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__5;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
x_25 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
lean_dec(x_4);
return x_26;
}
}
}
@ -4538,7 +4493,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_many___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_mkAntiquotAux___closed__13;
x_2 = l_Lean_Parser_mkAntiquotAux___closed__11;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
@ -4613,90 +4568,74 @@ return x_3;
lean_object* l_Lean_Parser_Syntax_many1___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 3);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
x_6 = l_Lean_Parser_tokenFn(x_1, x_2);
x_7 = lean_ctor_get(x_6, 3);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_object* x_8; lean_object* x_9;
x_8 = lean_ctor_get(x_6, 0);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 2)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_13 = lean_string_dec_eq(x_11, x_12);
lean_dec(x_11);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
x_16 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
lean_dec(x_4);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19;
lean_dec(x_6);
x_18 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_7, x_18, x_4);
lean_dec(x_4);
return x_19;
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_10);
x_20 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_20, x_6);
x_22 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_23 = l_Lean_Parser_ParserState_mkTrailingNode(x_21, x_22, x_4);
lean_dec(x_4);
return x_23;
}
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_9 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_8);
lean_dec(x_8);
x_24 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_24, x_6);
x_26 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_27 = l_Lean_Parser_ParserState_mkTrailingNode(x_25, x_26, x_4);
if (lean_obj_tag(x_9) == 2)
{
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_Parser_Level_addLit___elambda__1___closed__3;
x_12 = lean_string_dec_eq(x_10, x_11);
lean_dec(x_10);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_13 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_14 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_13, x_5);
x_15 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_16 = l_Lean_Parser_ParserState_mkTrailingNode(x_14, x_15, x_4);
lean_dec(x_4);
return x_27;
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_5);
x_17 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_18 = l_Lean_Parser_ParserState_mkTrailingNode(x_6, x_17, x_4);
lean_dec(x_4);
return x_18;
}
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_5);
lean_dec(x_1);
x_28 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_29 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_28, x_4);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_9);
x_19 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_20 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_19, x_5);
x_21 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
lean_dec(x_4);
return x_29;
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_7);
x_23 = l_Lean_Parser_Level_addLit___elambda__1___closed__7;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_6, x_23, x_5);
x_25 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
lean_dec(x_4);
return x_26;
}
}
}
@ -4722,23 +4661,13 @@ lean_object* _init_l_Lean_Parser_Syntax_many1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Syntax_many1___closed__1;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_many1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_many1___elambda__1___rarg___closed__2;
x_2 = l_Lean_Parser_Syntax_many1___closed__2;
x_2 = l_Lean_Parser_Syntax_many1___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_many1___closed__4() {
lean_object* _init_l_Lean_Parser_Syntax_many1___closed__3() {
_start:
{
lean_object* x_1;
@ -4746,12 +4675,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_many1___elambda__1___boxed
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Syntax_many1___closed__5() {
lean_object* _init_l_Lean_Parser_Syntax_many1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_many1___closed__3;
x_2 = l_Lean_Parser_Syntax_many1___closed__4;
x_1 = l_Lean_Parser_Syntax_many1___closed__2;
x_2 = l_Lean_Parser_Syntax_many1___closed__3;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -4762,7 +4691,7 @@ lean_object* _init_l_Lean_Parser_Syntax_many1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Syntax_many1___closed__5;
x_1 = l_Lean_Parser_Syntax_many1___closed__4;
return x_1;
}
}
@ -4800,97 +4729,93 @@ return x_3;
lean_object* l_Lean_Parser_Syntax_orelse___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_inc(x_1);
x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
x_17 = lean_ctor_get(x_16, 3);
lean_inc(x_17);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 2)
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_16, 0);
lean_inc(x_18);
x_19 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_18);
lean_dec(x_18);
if (lean_obj_tag(x_19) == 2)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
x_13 = lean_string_dec_eq(x_11, x_12);
lean_dec(x_11);
if (x_13 == 0)
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
x_22 = lean_string_dec_eq(x_20, x_21);
lean_dec(x_20);
if (x_22 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_1);
x_14 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
x_16 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
lean_dec(x_4);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_6);
x_18 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
x_19 = lean_unsigned_to_nat(1u);
x_20 = l_Lean_Parser_categoryParserFn(x_18, x_19, x_1, x_7);
x_21 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
lean_dec(x_4);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_10);
lean_dec(x_1);
lean_object* x_23; lean_object* x_24;
x_23 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_23, x_6);
x_25 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
lean_dec(x_4);
return x_26;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
x_5 = x_24;
goto block_14;
}
else
{
lean_dec(x_15);
x_5 = x_16;
goto block_14;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_8);
lean_dec(x_1);
lean_object* x_25; lean_object* x_26;
lean_dec(x_19);
x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
x_5 = x_26;
goto block_14;
}
}
else
{
lean_object* x_27; lean_object* x_28;
lean_dec(x_17);
x_27 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_27, x_6);
x_29 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_4);
lean_dec(x_4);
return x_30;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
x_5 = x_28;
goto block_14;
}
block_14:
{
lean_object* x_6;
x_6 = lean_ctor_get(x_5, 3);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__4;
x_8 = lean_unsigned_to_nat(1u);
x_9 = l_Lean_Parser_categoryParserFn(x_7, x_8, x_1, x_5);
x_10 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_11 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_10, x_4);
lean_dec(x_4);
return x_11;
}
else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_5);
lean_object* x_12; lean_object* x_13;
lean_dec(x_6);
lean_dec(x_1);
x_31 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_32 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_31, x_4);
x_12 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_13 = l_Lean_Parser_ParserState_mkTrailingNode(x_5, x_12, x_4);
lean_dec(x_4);
return x_32;
return x_13;
}
}
}
}
@ -4929,23 +4854,13 @@ lean_object* _init_l_Lean_Parser_Syntax_orelse___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_Syntax_orelse___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_orelse___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Syntax_orelse___closed__3;
x_2 = l_Lean_Parser_Syntax_orelse___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__5() {
lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__4() {
_start:
{
lean_object* x_1;
@ -4953,12 +4868,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Syntax_orelse___elambda__1___boxe
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__6() {
lean_object* _init_l_Lean_Parser_Syntax_orelse___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_orelse___closed__4;
x_2 = l_Lean_Parser_Syntax_orelse___closed__5;
x_1 = l_Lean_Parser_Syntax_orelse___closed__3;
x_2 = l_Lean_Parser_Syntax_orelse___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);
@ -4969,7 +4884,7 @@ lean_object* _init_l_Lean_Parser_Syntax_orelse() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Syntax_orelse___closed__6;
x_1 = l_Lean_Parser_Syntax_orelse___closed__5;
return x_1;
}
}
@ -13622,8 +13537,6 @@ l_Lean_Parser_Syntax_optional___closed__3 = _init_l_Lean_Parser_Syntax_optional_
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__3);
l_Lean_Parser_Syntax_optional___closed__4 = _init_l_Lean_Parser_Syntax_optional___closed__4();
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__4);
l_Lean_Parser_Syntax_optional___closed__5 = _init_l_Lean_Parser_Syntax_optional___closed__5();
lean_mark_persistent(l_Lean_Parser_Syntax_optional___closed__5);
l_Lean_Parser_Syntax_optional = _init_l_Lean_Parser_Syntax_optional();
lean_mark_persistent(l_Lean_Parser_Syntax_optional);
res = l___regBuiltinParser_Lean_Parser_Syntax_optional(lean_io_mk_world());
@ -13662,8 +13575,6 @@ l_Lean_Parser_Syntax_many1___closed__3 = _init_l_Lean_Parser_Syntax_many1___clos
lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__3);
l_Lean_Parser_Syntax_many1___closed__4 = _init_l_Lean_Parser_Syntax_many1___closed__4();
lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__4);
l_Lean_Parser_Syntax_many1___closed__5 = _init_l_Lean_Parser_Syntax_many1___closed__5();
lean_mark_persistent(l_Lean_Parser_Syntax_many1___closed__5);
l_Lean_Parser_Syntax_many1 = _init_l_Lean_Parser_Syntax_many1();
lean_mark_persistent(l_Lean_Parser_Syntax_many1);
res = l___regBuiltinParser_Lean_Parser_Syntax_many1(lean_io_mk_world());
@ -13681,8 +13592,6 @@ l_Lean_Parser_Syntax_orelse___closed__4 = _init_l_Lean_Parser_Syntax_orelse___cl
lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__4);
l_Lean_Parser_Syntax_orelse___closed__5 = _init_l_Lean_Parser_Syntax_orelse___closed__5();
lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__5);
l_Lean_Parser_Syntax_orelse___closed__6 = _init_l_Lean_Parser_Syntax_orelse___closed__6();
lean_mark_persistent(l_Lean_Parser_Syntax_orelse___closed__6);
l_Lean_Parser_Syntax_orelse = _init_l_Lean_Parser_Syntax_orelse();
lean_mark_persistent(l_Lean_Parser_Syntax_orelse);
res = l___regBuiltinParser_Lean_Parser_Syntax_orelse(lean_io_mk_world());

164
stage0/stdlib/Init/Lean/Parser/Tactic.c
View file

@ -79,7 +79,6 @@ lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__6;
lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__7;
lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__1;
lean_object* l_Lean_Parser_Tactic_orelse___closed__7;
lean_object* l_Lean_Parser_regTacticParserAttribute___closed__1;
lean_object* l_Lean_Parser_Tactic_underscore(uint8_t);
lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__4;
@ -289,7 +288,6 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__4;
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_underscoreFn___rarg___closed__2;
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__4;
lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__7;
@ -4884,97 +4882,93 @@ return x_3;
lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_array_get_size(x_3);
lean_dec(x_3);
x_5 = lean_ctor_get(x_2, 3);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
x_15 = lean_ctor_get(x_2, 1);
lean_inc(x_15);
lean_inc(x_1);
x_7 = l_Lean_Parser_tokenFn(x_1, x_2);
x_8 = lean_ctor_get(x_7, 3);
lean_inc(x_8);
if (lean_obj_tag(x_8) == 0)
x_16 = l_Lean_Parser_tokenFn(x_1, x_2);
x_17 = lean_ctor_get(x_16, 3);
lean_inc(x_17);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
x_10 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_9);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 2)
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_16, 0);
lean_inc(x_18);
x_19 = l_Array_back___at_Lean_Parser_checkLeadingFn___spec__1(x_18);
lean_dec(x_18);
if (lean_obj_tag(x_19) == 2)
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
x_13 = lean_string_dec_eq(x_11, x_12);
lean_dec(x_11);
if (x_13 == 0)
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__2;
x_22 = lean_string_dec_eq(x_20, x_21);
lean_dec(x_20);
if (x_22 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_1);
x_14 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_15 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_14, x_6);
x_16 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_17 = l_Lean_Parser_ParserState_mkTrailingNode(x_15, x_16, x_4);
lean_dec(x_4);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_6);
x_18 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
x_19 = lean_unsigned_to_nat(1u);
x_20 = l_Lean_Parser_categoryParserFn(x_18, x_19, x_1, x_7);
x_21 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_22 = l_Lean_Parser_ParserState_mkTrailingNode(x_20, x_21, x_4);
lean_dec(x_4);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_10);
lean_dec(x_1);
lean_object* x_23; lean_object* x_24;
x_23 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_23, x_6);
x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_26 = l_Lean_Parser_ParserState_mkTrailingNode(x_24, x_25, x_4);
lean_dec(x_4);
return x_26;
x_24 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_23, x_15);
x_5 = x_24;
goto block_14;
}
else
{
lean_dec(x_15);
x_5 = x_16;
goto block_14;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_8);
lean_dec(x_1);
lean_object* x_25; lean_object* x_26;
lean_dec(x_19);
x_25 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_26 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_25, x_15);
x_5 = x_26;
goto block_14;
}
}
else
{
lean_object* x_27; lean_object* x_28;
lean_dec(x_17);
x_27 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__5;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_7, x_27, x_6);
x_29 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_4);
lean_dec(x_4);
return x_30;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_16, x_27, x_15);
x_5 = x_28;
goto block_14;
}
block_14:
{
lean_object* x_6;
x_6 = lean_ctor_get(x_5, 3);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
x_8 = lean_unsigned_to_nat(1u);
x_9 = l_Lean_Parser_categoryParserFn(x_7, x_8, x_1, x_5);
x_10 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_11 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_10, x_4);
lean_dec(x_4);
return x_11;
}
else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_5);
lean_object* x_12; lean_object* x_13;
lean_dec(x_6);
lean_dec(x_1);
x_31 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_32 = l_Lean_Parser_ParserState_mkTrailingNode(x_2, x_31, x_4);
x_12 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_13 = l_Lean_Parser_ParserState_mkTrailingNode(x_5, x_12, x_4);
lean_dec(x_4);
return x_32;
return x_13;
}
}
}
}
@ -5023,23 +5017,13 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_epsilonInfo;
x_2 = l_Lean_Parser_Tactic_orelse___closed__3;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_orelse___elambda__1___rarg___closed__1;
x_2 = l_Lean_Parser_Tactic_orelse___closed__4;
x_2 = l_Lean_Parser_Tactic_orelse___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() {
lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__5() {
_start:
{
lean_object* x_1;
@ -5047,12 +5031,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_orelse___elambda__1___boxe
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__7() {
lean_object* _init_l_Lean_Parser_Tactic_orelse___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_orelse___closed__5;
x_2 = l_Lean_Parser_Tactic_orelse___closed__6;
x_1 = l_Lean_Parser_Tactic_orelse___closed__4;
x_2 = l_Lean_Parser_Tactic_orelse___closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -5063,7 +5047,7 @@ lean_object* _init_l_Lean_Parser_Tactic_orelse() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Tactic_orelse___closed__7;
x_1 = l_Lean_Parser_Tactic_orelse___closed__6;
return x_1;
}
}
@ -6281,8 +6265,6 @@ l_Lean_Parser_Tactic_orelse___closed__5 = _init_l_Lean_Parser_Tactic_orelse___cl
lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__5);
l_Lean_Parser_Tactic_orelse___closed__6 = _init_l_Lean_Parser_Tactic_orelse___closed__6();
lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__6);
l_Lean_Parser_Tactic_orelse___closed__7 = _init_l_Lean_Parser_Tactic_orelse___closed__7();
lean_mark_persistent(l_Lean_Parser_Tactic_orelse___closed__7);
l_Lean_Parser_Tactic_orelse = _init_l_Lean_Parser_Tactic_orelse();
lean_mark_persistent(l_Lean_Parser_Tactic_orelse);
res = l___regBuiltinParser_Lean_Parser_Tactic_orelse(lean_io_mk_world());

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

File diff suppressed because it is too large Load diff

31
stage0/stdlib/Init/LeanInit.c
View file

@ -267,6 +267,7 @@ lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
uint8_t l_Lean_Name_hasMacroScopes___main(lean_object*);
lean_object* l_Lean_ParserDescr_strLit___boxed(lean_object*);
lean_object* l_Lean_identKind;
lean_object* l_Lean_ParserDescr_trailingNode(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_mkCTermId(lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
@ -1536,7 +1537,7 @@ _start:
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_box(0);
x_3 = l_String_splitAux___main___closed__1;
x_4 = lean_alloc_ctor(10, 2, 1);
x_4 = lean_alloc_ctor(11, 2, 1);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
@ -1758,11 +1759,21 @@ x_5 = l_Lean_ParserDescr_node(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_trailingNode(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_symbol(uint8_t x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(10, 2, 1);
x_4 = lean_alloc_ctor(11, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
@ -1783,7 +1794,7 @@ lean_object* l_Lean_ParserDescr_numLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(12, 0, 1);
x_2 = lean_alloc_ctor(13, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
@ -1802,7 +1813,7 @@ lean_object* l_Lean_ParserDescr_strLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(13, 0, 1);
x_2 = lean_alloc_ctor(14, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
@ -1821,7 +1832,7 @@ lean_object* l_Lean_ParserDescr_charLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(14, 0, 1);
x_2 = lean_alloc_ctor(15, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
@ -1840,7 +1851,7 @@ lean_object* l_Lean_ParserDescr_nameLit(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(15, 0, 1);
x_2 = lean_alloc_ctor(16, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
@ -1859,7 +1870,7 @@ lean_object* l_Lean_ParserDescr_ident(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(16, 0, 1);
x_2 = lean_alloc_ctor(17, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
@ -1878,7 +1889,7 @@ lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object* x_1, uint8_t x_2)
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(11, 1, 1);
x_3 = lean_alloc_ctor(12, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
@ -1898,7 +1909,7 @@ lean_object* _init_l_Lean_ParserDescr_pushLeading() {
_start:
{
lean_object* x_1;
x_1 = lean_box(17);
x_1 = lean_box(18);
return x_1;
}
}
@ -1906,7 +1917,7 @@ lean_object* l_Lean_ParserDescr_parser(uint8_t x_1, lean_object* x_2, lean_objec
_start:
{
lean_object* x_4;
x_4 = lean_alloc_ctor(18, 2, 1);
x_4 = lean_alloc_ctor(19, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);