From b5dff38ecf83cb5d479a54e1e3032144aa7fc661 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jun 2020 16:22:32 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Parser/Level.lean | 2 +- stage0/src/Lean/Parser/Syntax.lean | 2 +- stage0/src/Lean/Parser/Tactic.lean | 2 +- stage0/src/Lean/Parser/Term.lean | 45 +- stage0/stdlib/Lean/Parser/Syntax.c | 66 +- stage0/stdlib/Lean/Parser/Term.c | 1192 ++++++++++++++++++---------- 6 files changed, 833 insertions(+), 476 deletions(-) diff --git a/stage0/src/Lean/Parser/Level.lean b/stage0/src/Lean/Parser/Level.lean index 181445c20b..cf2601e40e 100644 --- a/stage0/src/Lean/Parser/Level.lean +++ b/stage0/src/Lean/Parser/Level.lean @@ -23,7 +23,7 @@ namespace Level @[builtinLevelParser] def hole := parser! "_" @[builtinLevelParser] def num := parser! numLit @[builtinLevelParser] def ident := parser! ident -@[builtinLevelParser] def addLit := tparser! [65] "+" >> numLit +@[builtinLevelParser] def addLit := tparser!:65 "+" >> numLit end Level diff --git a/stage0/src/Lean/Parser/Syntax.lean b/stage0/src/Lean/Parser/Syntax.lean index 6cdcfba2f4..1b6a48ffb1 100644 --- a/stage0/src/Lean/Parser/Syntax.lean +++ b/stage0/src/Lean/Parser/Syntax.lean @@ -39,7 +39,7 @@ namespace Syntax @[builtinSyntaxParser] def optional := tparser! "?" @[builtinSyntaxParser] def many := tparser! "*" @[builtinSyntaxParser] def many1 := tparser! "+" -@[builtinSyntaxParser] def orelse := tparser! [2] " <|> " >> syntaxParser 1 +@[builtinSyntaxParser] def orelse := tparser!:2 " <|> " >> syntaxParser 1 end Syntax diff --git a/stage0/src/Lean/Parser/Tactic.lean b/stage0/src/Lean/Parser/Tactic.lean index 003e3cd640..4f27ab627b 100644 --- a/stage0/src/Lean/Parser/Tactic.lean +++ b/stage0/src/Lean/Parser/Tactic.lean @@ -51,7 +51,7 @@ def withIds : Parser := optional (" with " >> many1 ident') @[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")" @[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end" @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}" -@[builtinTacticParser] def orelse := tparser! [2] " <|> " >> tacticParser 1 +@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1 end Tactic end Parser diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean index de9a338075..ea886a885e 100644 --- a/stage0/src/Lean/Parser/Term.lean +++ b/stage0/src/Lean/Parser/Term.lean @@ -66,12 +66,12 @@ def parenSpecial : Parser := optional (tupleTail <|> typeAscription) @[builtinTermParser] def paren := parser! "(" >> optional (termParser >> parenSpecial) >> ")" @[builtinTermParser] def anonymousCtor := parser! "⟨" >> sepBy termParser ", " >> "⟩" def optIdent : Parser := optional (try (ident >> " : ")) -@[builtinTermParser] def «if» := parser! [leadPrec] "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser +@[builtinTermParser] def «if» := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser def fromTerm := parser! " from " >> termParser def haveAssign := parser! " := " >> termParser -@[builtinTermParser] def «have» := parser! [leadPrec] "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser -@[builtinTermParser] def «suffices» := parser! [leadPrec] "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser -@[builtinTermParser] def «show» := parser! [leadPrec] "show " >> termParser >> fromTerm +@[builtinTermParser] def «have» := parser!:leadPrec "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser +@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser +@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> fromTerm def structInstArrayRef := parser! "[" >> termParser >>"]" def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef) def structInstField := parser! structInstLVal >> " := " >> termParser @@ -93,10 +93,10 @@ def instBinder := parser! "[" >> optIdent >> termParser >> "]" def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder @[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser def simpleBinder := parser! many1 binderIdent -@[builtinTermParser] def «forall» := parser! [leadPrec] unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser +@[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser def funBinder : Parser := implicitBinder <|> instBinder <|> termParser appPrec -@[builtinTermParser] def «fun» := parser! [leadPrec] unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser +@[builtinTermParser] def «fun» := parser!:leadPrec unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser def matchAlt : Parser := nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ @@ -107,14 +107,15 @@ withPosition $ fun pos => (if optionalFirstBar then optional "|" else "|") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|") -@[builtinTermParser] def «match» := parser! [leadPrec] "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts -@[builtinTermParser] def «nomatch» := parser! [leadPrec] "nomatch " >> termParser -@[builtinTermParser] def «parser!» := parser! [leadPrec] "parser! " >> termParser -- TODO optional prec -@[builtinTermParser] def «tparser!» := parser! [leadPrec] "tparser! " >> termParser +@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts +@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser +def optExprPrecedence := optional (try ":" >> termParser appPrec) +@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser +@[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser @[builtinTermParser] def borrowed := parser! "@&" >> termParser (appPrec - 1) @[builtinTermParser] def quotedName := parser! nameLit -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command -@[builtinTermParser] def «match_syntax» := parser! [leadPrec] "match_syntax" >> termParser >> " with " >> matchAlts +@[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracketedBinder >> optType @@ -122,8 +123,8 @@ def letIdDecl : Parser := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl def letPatDecl : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl -@[builtinTermParser] def «let» := parser! [leadPrec] "let " >> letDecl >> "; " >> termParser -@[builtinTermParser] def «let!» := parser! [leadPrec] "let! " >> letDecl >> "; " >> termParser +@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser +@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser def leftArrow : Parser := unicodeSymbol " ← " " <- " def doLet := parser! "let ">> letDecl @@ -133,8 +134,8 @@ def doExpr := parser! termParser def doElem := doLet <|> doId <|> doPat <|> doExpr def doSeq := sepBy1 doElem "; " def bracketedDoSeq := parser! "{" >> doSeq >> "}" -@[builtinTermParser] def liftMethod := parser! [0] leftArrow >> termParser -@[builtinTermParser] def «do» := parser! [leadPrec] "do " >> (bracketedDoSeq <|> doSeq) +@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser +@[builtinTermParser] def «do» := parser!:leadPrec "do " >> (bracketedDoSeq <|> doSeq) @[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser appPrec @@ -143,19 +144,19 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}" @[builtinTermParser] def not := parser! "¬" >> termParser 40 @[builtinTermParser] def bnot := parser! "!" >> termParser 40 -- symbol precedence should be higher, but must match the one of `sub` below -@[builtinTermParser] def uminus := parser! [65] "-" >> termParser 100 +@[builtinTermParser] def uminus := parser!:65 "-" >> termParser 100 def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" -@[builtinTermParser] def app := tparser! [appPrec-1] many1 (namedArgument <|> termParser appPrec) +@[builtinTermParser] def app := tparser!:(appPrec-1) many1 (namedArgument <|> termParser appPrec) @[builtinTermParser] def proj := tparser! symbolNoWs "." >> (fieldIdx <|> ident) @[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25 @[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" >> termParser >>"]" -@[builtinTermParser] def dollar := tparser! [0] try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0 -@[builtinTermParser] def dollarProj := tparser! [0] "$." >> (fieldIdx <|> ident) +@[builtinTermParser] def dollar := tparser!:0 try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0 +@[builtinTermParser] def dollarProj := tparser!:0 "$." >> (fieldIdx <|> ident) -@[builtinTermParser] def «where» := tparser! [0] " where " >> sepBy1 letDecl (group ("; " >> symbol " where ")) +@[builtinTermParser] def «where» := tparser!:0 " where " >> sepBy1 letDecl (group ("; " >> symbol " where ")) @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90 @@ -180,7 +181,7 @@ def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" @[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50 @[builtinTermParser] def equiv := tparser! infixL " ≈ " 50 -@[builtinTermParser] def subst := tparser! [75] " ▸ " >> sepBy1 (termParser 75) " ▸ " +@[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ " @[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35 @[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30 @@ -206,7 +207,7 @@ def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" @[builtinTermParser] def mapConstRev := tparser! infixR " $> " 100 @[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end" -@[builtinTermParser] def byTactic := parser! [leadPrec] "by " >> Tactic.nonEmptySeq +@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.nonEmptySeq -- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot` @[builtinTermParser] def tacticStxQuot : Parser := checkPrec appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")") diff --git a/stage0/stdlib/Lean/Parser/Syntax.c b/stage0/stdlib/Lean/Parser/Syntax.c index 9e58926f09..6fc27b15c1 100644 --- a/stage0/stdlib/Lean/Parser/Syntax.c +++ b/stage0/stdlib/Lean/Parser/Syntax.c @@ -37,7 +37,6 @@ lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_notation___closed__7; lean_object* l_Lean_Parser_Command_macroArgSimple___closed__3; lean_object* l_Lean_Parser_Command_macroTailTactic___closed__1; -lean_object* l_Lean_Parser_precedence___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_mixfixKind___closed__2; lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__3; @@ -106,6 +105,7 @@ lean_object* l_Lean_Parser_Command_infixr___closed__1; extern lean_object* l_Lean_Parser_ident; lean_object* l_Lean_Parser_Syntax_lookahead___closed__5; lean_object* l_Lean_Parser_precedence___elambda__1___closed__2; +extern lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; lean_object* l_Lean_Parser_Syntax_str___closed__3; lean_object* l_Lean_Parser_Syntax_sepBy; lean_object* l_Lean_Parser_Syntax_sepBy___closed__5; @@ -312,7 +312,6 @@ lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3; lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1; lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__9; -lean_object* l_Lean_Parser_precedence___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_identPrec___closed__3; lean_object* l_Lean_Parser_Command_macroArgType; @@ -400,7 +399,6 @@ lean_object* l_Lean_Parser_Syntax_ident___closed__2; lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_macroTailDefault___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_object*); -lean_object* l_Lean_Parser_precedence___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__5; lean_object* l_Lean_Parser_Syntax_many___closed__3; lean_object* l_Lean_Parser_Syntax_optional___elambda__1(lean_object*, lean_object*); @@ -1147,38 +1145,6 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_precedence___elambda__1___closed__5() { -_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_mkAntiquot___closed__4; -x_3 = lean_string_append(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_precedence___elambda__1___closed__6() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_precedence___elambda__1___closed__5; -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_precedence___elambda__1___closed__7() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Parser_precedence___elambda__1___closed__6; -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_precedence___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -1229,7 +1195,7 @@ lean_dec(x_24); if (x_26 == 0) { lean_object* x_27; lean_object* x_28; -x_27 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_27 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_27, x_19); x_11 = x_28; goto block_18; @@ -1245,7 +1211,7 @@ else { lean_object* x_29; lean_object* x_30; lean_dec(x_23); -x_29 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_29 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_29, x_19); x_11 = x_30; goto block_18; @@ -1255,7 +1221,7 @@ else { lean_object* x_31; lean_object* x_32; lean_dec(x_21); -x_31 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_31 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_31, x_19); x_11 = x_32; goto block_18; @@ -1371,7 +1337,7 @@ lean_dec(x_62); if (x_64 == 0) { lean_object* x_65; lean_object* x_66; -x_65 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_65 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_66 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_65, x_57); x_47 = x_66; goto block_56; @@ -1387,7 +1353,7 @@ else { lean_object* x_67; lean_object* x_68; lean_dec(x_61); -x_67 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_67 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_68 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_67, x_57); x_47 = x_68; goto block_56; @@ -1397,7 +1363,7 @@ else { lean_object* x_69; lean_object* x_70; lean_dec(x_59); -x_69 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_69 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_70 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_69, x_57); x_47 = x_70; goto block_56; @@ -13137,7 +13103,7 @@ if (x_23 == 0) { lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_dec(x_1); -x_24 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_24 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16); x_26 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_10); @@ -13158,7 +13124,7 @@ else lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_dec(x_20); lean_dec(x_1); -x_31 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_31 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_31, x_16); x_33 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_34 = l_Lean_Parser_ParserState_mkNode(x_32, x_33, x_10); @@ -13170,7 +13136,7 @@ else lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_dec(x_18); lean_dec(x_1); -x_35 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_35 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_35, x_16); x_37 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_38 = l_Lean_Parser_ParserState_mkNode(x_36, x_37, x_10); @@ -13299,7 +13265,7 @@ if (x_69 == 0) { lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_dec(x_1); -x_70 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_70 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_71 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_70, x_62); x_72 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_73 = l_Lean_Parser_ParserState_mkNode(x_71, x_72, x_56); @@ -13324,7 +13290,7 @@ else lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_dec(x_66); lean_dec(x_1); -x_79 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_79 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_80 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_79, x_62); x_81 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_82 = l_Lean_Parser_ParserState_mkNode(x_80, x_81, x_56); @@ -13338,7 +13304,7 @@ else lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_dec(x_64); lean_dec(x_1); -x_84 = l_Lean_Parser_precedence___elambda__1___closed__7; +x_84 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; x_85 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_84, x_62); x_86 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2; x_87 = l_Lean_Parser_ParserState_mkNode(x_85, x_86, x_56); @@ -16165,12 +16131,6 @@ l_Lean_Parser_precedence___elambda__1___closed__3 = _init_l_Lean_Parser_preceden lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__3); l_Lean_Parser_precedence___elambda__1___closed__4 = _init_l_Lean_Parser_precedence___elambda__1___closed__4(); lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__4); -l_Lean_Parser_precedence___elambda__1___closed__5 = _init_l_Lean_Parser_precedence___elambda__1___closed__5(); -lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__5); -l_Lean_Parser_precedence___elambda__1___closed__6 = _init_l_Lean_Parser_precedence___elambda__1___closed__6(); -lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__6); -l_Lean_Parser_precedence___elambda__1___closed__7 = _init_l_Lean_Parser_precedence___elambda__1___closed__7(); -lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__7); l_Lean_Parser_precedence___closed__1 = _init_l_Lean_Parser_precedence___closed__1(); lean_mark_persistent(l_Lean_Parser_precedence___closed__1); l_Lean_Parser_precedence___closed__2 = _init_l_Lean_Parser_precedence___closed__2(); diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c index b1785a048d..b3b297e58f 100644 --- a/stage0/stdlib/Lean/Parser/Term.c +++ b/stage0/stdlib/Lean/Parser/Term.c @@ -315,6 +315,7 @@ lean_object* l_Lean_Parser_Term_quotedName___closed__3; lean_object* l_Lean_Parser_Term_subst___closed__6; extern lean_object* l_Lean_Parser_ident; lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__10(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_quotedName(lean_object*); lean_object* l_Lean_Parser_Term_show___elambda__1___closed__6; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_simpleBinder___elambda__1___spec__1(lean_object*, lean_object*); @@ -414,6 +415,7 @@ lean_object* l_Lean_Parser_Term_let___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_not___closed__3; lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_matchAlts___elambda__1___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Parser_mkAntiquot___closed__4; lean_object* l_Lean_Parser_addBuiltinParser(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_optIdent___closed__4; @@ -623,6 +625,7 @@ lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_match___elambda__1___closed__15; +extern lean_object* l_Lean_Parser_mkAntiquot___closed__5; lean_object* l_Lean_Parser_Term_listLit___closed__6; lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_paren___closed__1; @@ -799,6 +802,7 @@ lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_ge___closed__2; extern lean_object* l_Lean_Parser_antiquotNestedExpr___closed__1; +lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_typeSpec___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_andM(lean_object*); lean_object* l_Lean_Parser_Term_parenSpecial___closed__3; @@ -1199,6 +1203,7 @@ lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_liftMethod___closed__1; lean_object* l_Lean_Parser_Term_explicitUniv___closed__4; lean_object* l_Lean_Parser_Term_append___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_optExprPrecedence___closed__3; lean_object* l_Lean_Parser_Term_proj___closed__2; lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_iff___closed__4; @@ -1337,6 +1342,7 @@ lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_not___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_doElem___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_id___closed__5; +lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_structInstField___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_prop___closed__3; @@ -1439,8 +1445,10 @@ lean_object* l_Lean_Parser_Term_namedArgument___closed__8; lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_dollarProj___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_do___elambda__1___closed__7; +lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_sort___closed__3; lean_object* l_Lean_Parser_Term_let___closed__7; +lean_object* l_Lean_Parser_Term_optExprPrecedence___closed__4; lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_mul___closed__1; lean_object* l_Lean_Parser_nodeWithAntiquot(lean_object*, lean_object*, lean_object*); @@ -1471,6 +1479,7 @@ lean_object* l_Lean_Parser_Term_mul___closed__2; extern lean_object* l_Lean_Parser_numLit; lean_object* l_Lean_Parser_Term_mod___closed__2; lean_object* l_Lean_Parser_Term_leftArrow; +lean_object* l_Lean_Parser_Term_optExprPrecedence___closed__1; lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__2; lean_object* l_Lean_Parser_Term_have___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__8; @@ -1599,6 +1608,7 @@ lean_object* l_Lean_Parser_Term_anonymousCtor; lean_object* l_Lean_Parser_Term_dollarProj___closed__4; lean_object* l_Lean_Parser_Term_iff___closed__3; lean_object* l_Lean_Parser_Term_forall___closed__9; +lean_object* l_Lean_Parser_Term_parser_x21___closed__8; lean_object* l_Lean_Parser_Term_parser_x21___closed__1; lean_object* l_Lean_Parser_Term_inaccessible___closed__3; lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__4; @@ -1700,6 +1710,7 @@ lean_object* l_Lean_Parser_Term_gt___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11; lean_object* l_Lean_Parser_Term_letDecl___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_letEqnsDecl___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_optExprPrecedence___closed__2; lean_object* l_Lean_Parser_Term_letIdLhs___closed__4; lean_object* l_Lean_Parser_Term_doLet___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_if___elambda__1___closed__17; @@ -1824,6 +1835,7 @@ lean_object* l_Lean_Parser_Term_funBinder___closed__1; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_explicitUniv___closed__12; lean_object* l_String_trim(lean_object*); +lean_object* l_Lean_Parser_Term_optExprPrecedence; lean_object* l___regBuiltinParser_Lean_Parser_Term_prop(lean_object*); lean_object* l___private_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2(uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__4; @@ -33493,6 +33505,290 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1); return x_6; } } +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1() { +_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_mkAntiquot___closed__4; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1; +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_Term_optExprPrecedence___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2; +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_Term_optExprPrecedence___elambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_36; lean_object* x_37; +x_3 = lean_ctor_get(x_2, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_2, 1); +lean_inc(x_4); +x_5 = lean_array_get_size(x_3); +lean_dec(x_3); +lean_inc(x_1); +x_36 = l_Lean_Parser_tokenFn(x_1, x_2); +x_37 = lean_ctor_get(x_36, 3); +lean_inc(x_37); +if (lean_obj_tag(x_37) == 0) +{ +lean_object* x_38; lean_object* x_39; +x_38 = lean_ctor_get(x_36, 0); +lean_inc(x_38); +x_39 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_38); +lean_dec(x_38); +if (lean_obj_tag(x_39) == 2) +{ +lean_object* x_40; lean_object* x_41; uint8_t x_42; +x_40 = lean_ctor_get(x_39, 1); +lean_inc(x_40); +lean_dec(x_39); +x_41 = l_Lean_Parser_mkAntiquot___closed__4; +x_42 = lean_string_dec_eq(x_40, x_41); +lean_dec(x_40); +if (x_42 == 0) +{ +lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; +x_43 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; +lean_inc(x_4); +x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_36, x_43, x_4); +x_45 = lean_ctor_get(x_44, 0); +lean_inc(x_45); +x_46 = lean_ctor_get(x_44, 2); +lean_inc(x_46); +x_47 = lean_ctor_get(x_44, 3); +lean_inc(x_47); +x_29 = x_44; +x_30 = x_45; +x_31 = x_46; +x_32 = x_47; +goto block_35; +} +else +{ +lean_object* x_48; lean_object* x_49; lean_object* x_50; +x_48 = lean_ctor_get(x_36, 0); +lean_inc(x_48); +x_49 = lean_ctor_get(x_36, 2); +lean_inc(x_49); +x_50 = lean_ctor_get(x_36, 3); +lean_inc(x_50); +x_29 = x_36; +x_30 = x_48; +x_31 = x_49; +x_32 = x_50; +goto block_35; +} +} +else +{ +lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; +lean_dec(x_39); +x_51 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; +lean_inc(x_4); +x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_36, x_51, x_4); +x_53 = lean_ctor_get(x_52, 0); +lean_inc(x_53); +x_54 = lean_ctor_get(x_52, 2); +lean_inc(x_54); +x_55 = lean_ctor_get(x_52, 3); +lean_inc(x_55); +x_29 = x_52; +x_30 = x_53; +x_31 = x_54; +x_32 = x_55; +goto block_35; +} +} +else +{ +lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; +lean_dec(x_37); +x_56 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3; +lean_inc(x_4); +x_57 = l_Lean_Parser_ParserState_mkErrorsAt(x_36, x_56, x_4); +x_58 = lean_ctor_get(x_57, 0); +lean_inc(x_58); +x_59 = lean_ctor_get(x_57, 2); +lean_inc(x_59); +x_60 = lean_ctor_get(x_57, 3); +lean_inc(x_60); +x_29 = x_57; +x_30 = x_58; +x_31 = x_59; +x_32 = x_60; +goto block_35; +} +block_28: +{ +lean_object* x_7; +x_7 = lean_ctor_get(x_6, 3); +lean_inc(x_7); +if (lean_obj_tag(x_7) == 0) +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_8 = l_Lean_Parser_termParser___closed__2; +x_9 = l_Lean_Parser_appPrec; +x_10 = l_Lean_Parser_categoryParser___elambda__1(x_8, x_9, x_1, x_6); +x_11 = lean_ctor_get(x_10, 3); +lean_inc(x_11); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; lean_object* x_13; +lean_dec(x_4); +x_12 = l_Lean_nullKind; +x_13 = l_Lean_Parser_ParserState_mkNode(x_10, x_12, x_5); +return x_13; +} +else +{ +lean_object* x_14; uint8_t x_15; +lean_dec(x_11); +x_14 = lean_ctor_get(x_10, 1); +lean_inc(x_14); +x_15 = lean_nat_dec_eq(x_14, x_4); +lean_dec(x_14); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; +lean_dec(x_4); +x_16 = l_Lean_nullKind; +x_17 = l_Lean_Parser_ParserState_mkNode(x_10, x_16, x_5); +return x_17; +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; +x_18 = l_Lean_Parser_ParserState_restore(x_10, x_5, x_4); +x_19 = l_Lean_nullKind; +x_20 = l_Lean_Parser_ParserState_mkNode(x_18, x_19, x_5); +return x_20; +} +} +} +else +{ +lean_object* x_21; uint8_t x_22; +lean_dec(x_7); +lean_dec(x_1); +x_21 = lean_ctor_get(x_6, 1); +lean_inc(x_21); +x_22 = lean_nat_dec_eq(x_21, x_4); +lean_dec(x_21); +if (x_22 == 0) +{ +lean_object* x_23; lean_object* x_24; +lean_dec(x_4); +x_23 = l_Lean_nullKind; +x_24 = l_Lean_Parser_ParserState_mkNode(x_6, x_23, x_5); +return x_24; +} +else +{ +lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_25 = l_Lean_Parser_ParserState_restore(x_6, x_5, x_4); +x_26 = l_Lean_nullKind; +x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_5); +return x_27; +} +} +} +block_35: +{ +if (lean_obj_tag(x_32) == 0) +{ +lean_dec(x_31); +lean_dec(x_30); +x_6 = x_29; +goto block_28; +} +else +{ +lean_object* x_33; lean_object* x_34; +lean_dec(x_29); +x_33 = l_Array_shrink___main___rarg(x_30, x_5); +lean_inc(x_4); +x_34 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_34, 0, x_33); +lean_ctor_set(x_34, 1, x_4); +lean_ctor_set(x_34, 2, x_31); +lean_ctor_set(x_34, 3, x_32); +x_6 = x_34; +goto block_28; +} +} +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_namedPattern___closed__2; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_mkAntiquot___closed__5; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_optExprPrecedence___closed__1; +x_2 = l_Lean_Parser_optionaInfo(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_optExprPrecedence___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_optExprPrecedence___closed__2; +x_2 = l_Lean_Parser_Term_optExprPrecedence___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); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_optExprPrecedence() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Term_optExprPrecedence___closed__4; +return x_1; +} +} lean_object* _init_l_Lean_Parser_Term_parser_x21___elambda__1___closed__1() { _start: { @@ -33601,90 +33897,107 @@ x_8 = lean_ctor_get(x_7, 3); lean_inc(x_8); if (lean_obj_tag(x_8) == 0) { -lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_21; lean_object* x_22; lean_object* x_23; +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_25; lean_object* x_26; lean_object* x_27; x_9 = lean_ctor_get(x_7, 0); lean_inc(x_9); x_10 = lean_array_get_size(x_9); lean_dec(x_9); -x_21 = lean_ctor_get(x_7, 1); -lean_inc(x_21); +x_25 = lean_ctor_get(x_7, 1); +lean_inc(x_25); lean_inc(x_1); -x_22 = l_Lean_Parser_tokenFn(x_1, x_7); -x_23 = lean_ctor_get(x_22, 3); -lean_inc(x_23); -if (lean_obj_tag(x_23) == 0) +x_26 = l_Lean_Parser_tokenFn(x_1, x_7); +x_27 = lean_ctor_get(x_26, 3); +lean_inc(x_27); +if (lean_obj_tag(x_27) == 0) { -lean_object* x_24; lean_object* x_25; -x_24 = lean_ctor_get(x_22, 0); -lean_inc(x_24); -x_25 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_24); -lean_dec(x_24); -if (lean_obj_tag(x_25) == 2) +lean_object* x_28; lean_object* x_29; +x_28 = lean_ctor_get(x_26, 0); +lean_inc(x_28); +x_29 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_28); +lean_dec(x_28); +if (lean_obj_tag(x_29) == 2) { -lean_object* x_26; lean_object* x_27; uint8_t x_28; -x_26 = lean_ctor_get(x_25, 1); -lean_inc(x_26); -lean_dec(x_25); -x_27 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__6; -x_28 = lean_string_dec_eq(x_26, x_27); -lean_dec(x_26); -if (x_28 == 0) -{ -lean_object* x_29; lean_object* x_30; -x_29 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_29, x_21); -x_11 = x_30; -goto block_20; -} -else -{ -lean_dec(x_21); -x_11 = x_22; -goto block_20; -} -} -else -{ -lean_object* x_31; lean_object* x_32; -lean_dec(x_25); -x_31 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_31, x_21); -x_11 = x_32; -goto block_20; -} -} -else +lean_object* x_30; lean_object* x_31; uint8_t x_32; +x_30 = lean_ctor_get(x_29, 1); +lean_inc(x_30); +lean_dec(x_29); +x_31 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__6; +x_32 = lean_string_dec_eq(x_30, x_31); +lean_dec(x_30); +if (x_32 == 0) { lean_object* x_33; lean_object* x_34; -lean_dec(x_23); x_33 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_33, x_21); +x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_33, x_25); x_11 = x_34; -goto block_20; +goto block_24; } -block_20: +else +{ +lean_dec(x_25); +x_11 = x_26; +goto block_24; +} +} +else +{ +lean_object* x_35; lean_object* x_36; +lean_dec(x_29); +x_35 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; +x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_35, x_25); +x_11 = x_36; +goto block_24; +} +} +else +{ +lean_object* x_37; lean_object* x_38; +lean_dec(x_27); +x_37 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; +x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_37, x_25); +x_11 = x_38; +goto block_24; +} +block_24: { lean_object* x_12; x_12 = lean_ctor_get(x_11, 3); lean_inc(x_12); if (lean_obj_tag(x_12) == 0) { -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_13 = l_Lean_Parser_termParser___closed__2; -x_14 = lean_unsigned_to_nat(0u); -x_15 = l_Lean_Parser_categoryParser___elambda__1(x_13, x_14, x_1, x_11); -x_16 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; -x_17 = l_Lean_Parser_ParserState_mkNode(x_15, x_16, x_10); -return x_17; +lean_object* x_13; lean_object* x_14; +lean_inc(x_1); +x_13 = l_Lean_Parser_Term_optExprPrecedence___elambda__1(x_1, x_11); +x_14 = lean_ctor_get(x_13, 3); +lean_inc(x_14); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_15 = l_Lean_Parser_termParser___closed__2; +x_16 = lean_unsigned_to_nat(0u); +x_17 = l_Lean_Parser_categoryParser___elambda__1(x_15, x_16, x_1, x_13); +x_18 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_10); +return x_19; } else { -lean_object* x_18; lean_object* x_19; +lean_object* x_20; lean_object* x_21; +lean_dec(x_14); +lean_dec(x_1); +x_20 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_21 = l_Lean_Parser_ParserState_mkNode(x_13, x_20, x_10); +return x_21; +} +} +else +{ +lean_object* x_22; lean_object* x_23; lean_dec(x_12); lean_dec(x_1); -x_18 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; -x_19 = l_Lean_Parser_ParserState_mkNode(x_11, x_18, x_10); -return x_19; +x_22 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_23 = l_Lean_Parser_ParserState_mkNode(x_11, x_22, x_10); +return x_23; } } } @@ -33697,153 +34010,172 @@ return x_7; } else { -lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; -x_35 = lean_ctor_get(x_2, 0); -lean_inc(x_35); -x_36 = lean_array_get_size(x_35); -lean_dec(x_35); -x_37 = lean_ctor_get(x_2, 1); -lean_inc(x_37); -lean_inc(x_1); -x_38 = lean_apply_2(x_4, x_1, x_2); -x_39 = lean_ctor_get(x_38, 3); +lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_39 = lean_ctor_get(x_2, 0); lean_inc(x_39); -if (lean_obj_tag(x_39) == 0) -{ -lean_dec(x_37); -lean_dec(x_36); -lean_dec(x_1); -return x_38; -} -else -{ -lean_object* x_40; lean_object* x_41; uint8_t x_42; -x_40 = lean_ctor_get(x_39, 0); -lean_inc(x_40); +x_40 = lean_array_get_size(x_39); lean_dec(x_39); -x_41 = lean_ctor_get(x_38, 1); +x_41 = lean_ctor_get(x_2, 1); lean_inc(x_41); -x_42 = lean_nat_dec_eq(x_41, x_37); -lean_dec(x_41); -if (x_42 == 0) -{ -lean_dec(x_40); -lean_dec(x_37); -lean_dec(x_36); -lean_dec(x_1); -return x_38; -} -else -{ -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; -lean_inc(x_37); -x_43 = l_Lean_Parser_ParserState_restore(x_38, x_36, x_37); -lean_dec(x_36); -x_44 = l_Lean_Parser_Term_leadPrec; -x_45 = l_Lean_Parser_checkPrecFn(x_44, x_1, x_43); -x_46 = lean_ctor_get(x_45, 3); -lean_inc(x_46); -if (lean_obj_tag(x_46) == 0) -{ -lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_61; lean_object* x_62; lean_object* x_63; -x_47 = lean_ctor_get(x_45, 0); -lean_inc(x_47); -x_48 = lean_array_get_size(x_47); -lean_dec(x_47); -x_61 = lean_ctor_get(x_45, 1); -lean_inc(x_61); lean_inc(x_1); -x_62 = l_Lean_Parser_tokenFn(x_1, x_45); -x_63 = lean_ctor_get(x_62, 3); -lean_inc(x_63); -if (lean_obj_tag(x_63) == 0) +x_42 = lean_apply_2(x_4, x_1, x_2); +x_43 = lean_ctor_get(x_42, 3); +lean_inc(x_43); +if (lean_obj_tag(x_43) == 0) { -lean_object* x_64; lean_object* x_65; -x_64 = lean_ctor_get(x_62, 0); -lean_inc(x_64); -x_65 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_64); -lean_dec(x_64); -if (lean_obj_tag(x_65) == 2) -{ -lean_object* x_66; lean_object* x_67; uint8_t x_68; -x_66 = lean_ctor_get(x_65, 1); -lean_inc(x_66); -lean_dec(x_65); -x_67 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__6; -x_68 = lean_string_dec_eq(x_66, x_67); -lean_dec(x_66); -if (x_68 == 0) -{ -lean_object* x_69; lean_object* x_70; -x_69 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_70 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_69, x_61); -x_49 = x_70; -goto block_60; +lean_dec(x_41); +lean_dec(x_40); +lean_dec(x_1); +return x_42; } else { -lean_dec(x_61); -x_49 = x_62; -goto block_60; -} +lean_object* x_44; lean_object* x_45; uint8_t x_46; +x_44 = lean_ctor_get(x_43, 0); +lean_inc(x_44); +lean_dec(x_43); +x_45 = lean_ctor_get(x_42, 1); +lean_inc(x_45); +x_46 = lean_nat_dec_eq(x_45, x_41); +lean_dec(x_45); +if (x_46 == 0) +{ +lean_dec(x_44); +lean_dec(x_41); +lean_dec(x_40); +lean_dec(x_1); +return x_42; } else { -lean_object* x_71; lean_object* x_72; -lean_dec(x_65); -x_71 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_72 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_71, x_61); -x_49 = x_72; -goto block_60; -} -} -else -{ -lean_object* x_73; lean_object* x_74; -lean_dec(x_63); -x_73 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; -x_74 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_73, x_61); -x_49 = x_74; -goto block_60; -} -block_60: -{ -lean_object* x_50; +lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; +lean_inc(x_41); +x_47 = l_Lean_Parser_ParserState_restore(x_42, x_40, x_41); +lean_dec(x_40); +x_48 = l_Lean_Parser_Term_leadPrec; +x_49 = l_Lean_Parser_checkPrecFn(x_48, x_1, x_47); x_50 = lean_ctor_get(x_49, 3); lean_inc(x_50); if (lean_obj_tag(x_50) == 0) { -lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; -x_51 = l_Lean_Parser_termParser___closed__2; -x_52 = lean_unsigned_to_nat(0u); -x_53 = l_Lean_Parser_categoryParser___elambda__1(x_51, x_52, x_1, x_49); -x_54 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; -x_55 = l_Lean_Parser_ParserState_mkNode(x_53, x_54, x_48); -x_56 = l_Lean_Parser_mergeOrElseErrors(x_55, x_40, x_37); -lean_dec(x_37); -return x_56; +lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_70; lean_object* x_71; lean_object* x_72; +x_51 = lean_ctor_get(x_49, 0); +lean_inc(x_51); +x_52 = lean_array_get_size(x_51); +lean_dec(x_51); +x_70 = lean_ctor_get(x_49, 1); +lean_inc(x_70); +lean_inc(x_1); +x_71 = l_Lean_Parser_tokenFn(x_1, x_49); +x_72 = lean_ctor_get(x_71, 3); +lean_inc(x_72); +if (lean_obj_tag(x_72) == 0) +{ +lean_object* x_73; lean_object* x_74; +x_73 = lean_ctor_get(x_71, 0); +lean_inc(x_73); +x_74 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_73); +lean_dec(x_73); +if (lean_obj_tag(x_74) == 2) +{ +lean_object* x_75; lean_object* x_76; uint8_t x_77; +x_75 = lean_ctor_get(x_74, 1); +lean_inc(x_75); +lean_dec(x_74); +x_76 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__6; +x_77 = lean_string_dec_eq(x_75, x_76); +lean_dec(x_75); +if (x_77 == 0) +{ +lean_object* x_78; lean_object* x_79; +x_78 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; +x_79 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_78, x_70); +x_53 = x_79; +goto block_69; } else { -lean_object* x_57; lean_object* x_58; lean_object* x_59; +lean_dec(x_70); +x_53 = x_71; +goto block_69; +} +} +else +{ +lean_object* x_80; lean_object* x_81; +lean_dec(x_74); +x_80 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; +x_81 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_80, x_70); +x_53 = x_81; +goto block_69; +} +} +else +{ +lean_object* x_82; lean_object* x_83; +lean_dec(x_72); +x_82 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__9; +x_83 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_82, x_70); +x_53 = x_83; +goto block_69; +} +block_69: +{ +lean_object* x_54; +x_54 = lean_ctor_get(x_53, 3); +lean_inc(x_54); +if (lean_obj_tag(x_54) == 0) +{ +lean_object* x_55; lean_object* x_56; +lean_inc(x_1); +x_55 = l_Lean_Parser_Term_optExprPrecedence___elambda__1(x_1, x_53); +x_56 = lean_ctor_get(x_55, 3); +lean_inc(x_56); +if (lean_obj_tag(x_56) == 0) +{ +lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; +x_57 = l_Lean_Parser_termParser___closed__2; +x_58 = lean_unsigned_to_nat(0u); +x_59 = l_Lean_Parser_categoryParser___elambda__1(x_57, x_58, x_1, x_55); +x_60 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_61 = l_Lean_Parser_ParserState_mkNode(x_59, x_60, x_52); +x_62 = l_Lean_Parser_mergeOrElseErrors(x_61, x_44, x_41); +lean_dec(x_41); +return x_62; +} +else +{ +lean_object* x_63; lean_object* x_64; lean_object* x_65; +lean_dec(x_56); +lean_dec(x_1); +x_63 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_64 = l_Lean_Parser_ParserState_mkNode(x_55, x_63, x_52); +x_65 = l_Lean_Parser_mergeOrElseErrors(x_64, x_44, x_41); +lean_dec(x_41); +return x_65; +} +} +else +{ +lean_object* x_66; lean_object* x_67; lean_object* x_68; +lean_dec(x_54); +lean_dec(x_1); +x_66 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_67 = l_Lean_Parser_ParserState_mkNode(x_53, x_66, x_52); +x_68 = l_Lean_Parser_mergeOrElseErrors(x_67, x_44, x_41); +lean_dec(x_41); +return x_68; +} +} +} +else +{ +lean_object* x_84; lean_dec(x_50); lean_dec(x_1); -x_57 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; -x_58 = l_Lean_Parser_ParserState_mkNode(x_49, x_57, x_48); -x_59 = l_Lean_Parser_mergeOrElseErrors(x_58, x_40, x_37); -lean_dec(x_37); -return x_59; -} -} -} -else -{ -lean_object* x_75; -lean_dec(x_46); -lean_dec(x_1); -x_75 = l_Lean_Parser_mergeOrElseErrors(x_45, x_40, x_37); -lean_dec(x_37); -return x_75; +x_84 = l_Lean_Parser_mergeOrElseErrors(x_49, x_44, x_41); +lean_dec(x_41); +return x_84; } } } @@ -33862,22 +34194,24 @@ return x_2; lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Parser_Term_optExprPrecedence; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_parser_x21___closed__1; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; +x_3 = l_Lean_Parser_antiquotNestedExpr___closed__2; +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +x_5 = l_Lean_Parser_andthenInfo(x_2, x_4); +return x_5; } } lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__2; +x_1 = l_Lean_Parser_Term_parser_x21___closed__1; x_2 = l_Lean_Parser_Term_parser_x21___closed__2; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } @@ -33885,25 +34219,35 @@ lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__4() { _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_parser_x21___elambda__1___closed__2; x_2 = l_Lean_Parser_Term_parser_x21___closed__3; -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_parser_x21___closed__5() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_epsilonInfo; +x_2 = l_Lean_Parser_Term_parser_x21___closed__4; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__6() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Term_parser_x21___elambda__1___closed__4; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_parser_x21___closed__4; +x_3 = l_Lean_Parser_Term_parser_x21___closed__5; x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); return x_4; } } -lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__6() { +lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__7() { _start: { lean_object* x_1; @@ -33911,12 +34255,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_parser_x21___elambda__1), 2, return x_1; } } -lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__7() { +lean_object* _init_l_Lean_Parser_Term_parser_x21___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_parser_x21___closed__5; -x_2 = l_Lean_Parser_Term_parser_x21___closed__6; +x_1 = l_Lean_Parser_Term_parser_x21___closed__6; +x_2 = l_Lean_Parser_Term_parser_x21___closed__7; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -33927,7 +34271,7 @@ lean_object* _init_l_Lean_Parser_Term_parser_x21() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_parser_x21___closed__7; +x_1 = l_Lean_Parser_Term_parser_x21___closed__8; return x_1; } } @@ -34051,90 +34395,107 @@ x_8 = lean_ctor_get(x_7, 3); lean_inc(x_8); if (lean_obj_tag(x_8) == 0) { -lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_21; lean_object* x_22; lean_object* x_23; +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_25; lean_object* x_26; lean_object* x_27; x_9 = lean_ctor_get(x_7, 0); lean_inc(x_9); x_10 = lean_array_get_size(x_9); lean_dec(x_9); -x_21 = lean_ctor_get(x_7, 1); -lean_inc(x_21); +x_25 = lean_ctor_get(x_7, 1); +lean_inc(x_25); lean_inc(x_1); -x_22 = l_Lean_Parser_tokenFn(x_1, x_7); -x_23 = lean_ctor_get(x_22, 3); -lean_inc(x_23); -if (lean_obj_tag(x_23) == 0) +x_26 = l_Lean_Parser_tokenFn(x_1, x_7); +x_27 = lean_ctor_get(x_26, 3); +lean_inc(x_27); +if (lean_obj_tag(x_27) == 0) { -lean_object* x_24; lean_object* x_25; -x_24 = lean_ctor_get(x_22, 0); -lean_inc(x_24); -x_25 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_24); -lean_dec(x_24); -if (lean_obj_tag(x_25) == 2) +lean_object* x_28; lean_object* x_29; +x_28 = lean_ctor_get(x_26, 0); +lean_inc(x_28); +x_29 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_28); +lean_dec(x_28); +if (lean_obj_tag(x_29) == 2) { -lean_object* x_26; lean_object* x_27; uint8_t x_28; -x_26 = lean_ctor_get(x_25, 1); -lean_inc(x_26); -lean_dec(x_25); -x_27 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__6; -x_28 = lean_string_dec_eq(x_26, x_27); -lean_dec(x_26); -if (x_28 == 0) -{ -lean_object* x_29; lean_object* x_30; -x_29 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_29, x_21); -x_11 = x_30; -goto block_20; -} -else -{ -lean_dec(x_21); -x_11 = x_22; -goto block_20; -} -} -else -{ -lean_object* x_31; lean_object* x_32; -lean_dec(x_25); -x_31 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_31, x_21); -x_11 = x_32; -goto block_20; -} -} -else +lean_object* x_30; lean_object* x_31; uint8_t x_32; +x_30 = lean_ctor_get(x_29, 1); +lean_inc(x_30); +lean_dec(x_29); +x_31 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__6; +x_32 = lean_string_dec_eq(x_30, x_31); +lean_dec(x_30); +if (x_32 == 0) { lean_object* x_33; lean_object* x_34; -lean_dec(x_23); x_33 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_22, x_33, x_21); +x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_33, x_25); x_11 = x_34; -goto block_20; +goto block_24; } -block_20: +else +{ +lean_dec(x_25); +x_11 = x_26; +goto block_24; +} +} +else +{ +lean_object* x_35; lean_object* x_36; +lean_dec(x_29); +x_35 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_35, x_25); +x_11 = x_36; +goto block_24; +} +} +else +{ +lean_object* x_37; lean_object* x_38; +lean_dec(x_27); +x_37 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_37, x_25); +x_11 = x_38; +goto block_24; +} +block_24: { lean_object* x_12; x_12 = lean_ctor_get(x_11, 3); lean_inc(x_12); if (lean_obj_tag(x_12) == 0) { -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_13 = l_Lean_Parser_termParser___closed__2; -x_14 = lean_unsigned_to_nat(0u); -x_15 = l_Lean_Parser_categoryParser___elambda__1(x_13, x_14, x_1, x_11); -x_16 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; -x_17 = l_Lean_Parser_ParserState_mkNode(x_15, x_16, x_10); -return x_17; +lean_object* x_13; lean_object* x_14; +lean_inc(x_1); +x_13 = l_Lean_Parser_Term_optExprPrecedence___elambda__1(x_1, x_11); +x_14 = lean_ctor_get(x_13, 3); +lean_inc(x_14); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_15 = l_Lean_Parser_termParser___closed__2; +x_16 = lean_unsigned_to_nat(0u); +x_17 = l_Lean_Parser_categoryParser___elambda__1(x_15, x_16, x_1, x_13); +x_18 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_19 = l_Lean_Parser_ParserState_mkNode(x_17, x_18, x_10); +return x_19; } else { -lean_object* x_18; lean_object* x_19; +lean_object* x_20; lean_object* x_21; +lean_dec(x_14); +lean_dec(x_1); +x_20 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_21 = l_Lean_Parser_ParserState_mkNode(x_13, x_20, x_10); +return x_21; +} +} +else +{ +lean_object* x_22; lean_object* x_23; lean_dec(x_12); lean_dec(x_1); -x_18 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; -x_19 = l_Lean_Parser_ParserState_mkNode(x_11, x_18, x_10); -return x_19; +x_22 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_23 = l_Lean_Parser_ParserState_mkNode(x_11, x_22, x_10); +return x_23; } } } @@ -34147,153 +34508,172 @@ return x_7; } else { -lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; -x_35 = lean_ctor_get(x_2, 0); -lean_inc(x_35); -x_36 = lean_array_get_size(x_35); -lean_dec(x_35); -x_37 = lean_ctor_get(x_2, 1); -lean_inc(x_37); -lean_inc(x_1); -x_38 = lean_apply_2(x_4, x_1, x_2); -x_39 = lean_ctor_get(x_38, 3); +lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; +x_39 = lean_ctor_get(x_2, 0); lean_inc(x_39); -if (lean_obj_tag(x_39) == 0) -{ -lean_dec(x_37); -lean_dec(x_36); -lean_dec(x_1); -return x_38; -} -else -{ -lean_object* x_40; lean_object* x_41; uint8_t x_42; -x_40 = lean_ctor_get(x_39, 0); -lean_inc(x_40); +x_40 = lean_array_get_size(x_39); lean_dec(x_39); -x_41 = lean_ctor_get(x_38, 1); +x_41 = lean_ctor_get(x_2, 1); lean_inc(x_41); -x_42 = lean_nat_dec_eq(x_41, x_37); -lean_dec(x_41); -if (x_42 == 0) -{ -lean_dec(x_40); -lean_dec(x_37); -lean_dec(x_36); -lean_dec(x_1); -return x_38; -} -else -{ -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; -lean_inc(x_37); -x_43 = l_Lean_Parser_ParserState_restore(x_38, x_36, x_37); -lean_dec(x_36); -x_44 = l_Lean_Parser_Term_leadPrec; -x_45 = l_Lean_Parser_checkPrecFn(x_44, x_1, x_43); -x_46 = lean_ctor_get(x_45, 3); -lean_inc(x_46); -if (lean_obj_tag(x_46) == 0) -{ -lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_61; lean_object* x_62; lean_object* x_63; -x_47 = lean_ctor_get(x_45, 0); -lean_inc(x_47); -x_48 = lean_array_get_size(x_47); -lean_dec(x_47); -x_61 = lean_ctor_get(x_45, 1); -lean_inc(x_61); lean_inc(x_1); -x_62 = l_Lean_Parser_tokenFn(x_1, x_45); -x_63 = lean_ctor_get(x_62, 3); -lean_inc(x_63); -if (lean_obj_tag(x_63) == 0) +x_42 = lean_apply_2(x_4, x_1, x_2); +x_43 = lean_ctor_get(x_42, 3); +lean_inc(x_43); +if (lean_obj_tag(x_43) == 0) { -lean_object* x_64; lean_object* x_65; -x_64 = lean_ctor_get(x_62, 0); -lean_inc(x_64); -x_65 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_64); -lean_dec(x_64); -if (lean_obj_tag(x_65) == 2) -{ -lean_object* x_66; lean_object* x_67; uint8_t x_68; -x_66 = lean_ctor_get(x_65, 1); -lean_inc(x_66); -lean_dec(x_65); -x_67 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__6; -x_68 = lean_string_dec_eq(x_66, x_67); -lean_dec(x_66); -if (x_68 == 0) -{ -lean_object* x_69; lean_object* x_70; -x_69 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_70 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_69, x_61); -x_49 = x_70; -goto block_60; +lean_dec(x_41); +lean_dec(x_40); +lean_dec(x_1); +return x_42; } else { -lean_dec(x_61); -x_49 = x_62; -goto block_60; -} +lean_object* x_44; lean_object* x_45; uint8_t x_46; +x_44 = lean_ctor_get(x_43, 0); +lean_inc(x_44); +lean_dec(x_43); +x_45 = lean_ctor_get(x_42, 1); +lean_inc(x_45); +x_46 = lean_nat_dec_eq(x_45, x_41); +lean_dec(x_45); +if (x_46 == 0) +{ +lean_dec(x_44); +lean_dec(x_41); +lean_dec(x_40); +lean_dec(x_1); +return x_42; } else { -lean_object* x_71; lean_object* x_72; -lean_dec(x_65); -x_71 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_72 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_71, x_61); -x_49 = x_72; -goto block_60; -} -} -else -{ -lean_object* x_73; lean_object* x_74; -lean_dec(x_63); -x_73 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; -x_74 = l_Lean_Parser_ParserState_mkErrorsAt(x_62, x_73, x_61); -x_49 = x_74; -goto block_60; -} -block_60: -{ -lean_object* x_50; +lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; +lean_inc(x_41); +x_47 = l_Lean_Parser_ParserState_restore(x_42, x_40, x_41); +lean_dec(x_40); +x_48 = l_Lean_Parser_Term_leadPrec; +x_49 = l_Lean_Parser_checkPrecFn(x_48, x_1, x_47); x_50 = lean_ctor_get(x_49, 3); lean_inc(x_50); if (lean_obj_tag(x_50) == 0) { -lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; -x_51 = l_Lean_Parser_termParser___closed__2; -x_52 = lean_unsigned_to_nat(0u); -x_53 = l_Lean_Parser_categoryParser___elambda__1(x_51, x_52, x_1, x_49); -x_54 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; -x_55 = l_Lean_Parser_ParserState_mkNode(x_53, x_54, x_48); -x_56 = l_Lean_Parser_mergeOrElseErrors(x_55, x_40, x_37); -lean_dec(x_37); -return x_56; +lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_70; lean_object* x_71; lean_object* x_72; +x_51 = lean_ctor_get(x_49, 0); +lean_inc(x_51); +x_52 = lean_array_get_size(x_51); +lean_dec(x_51); +x_70 = lean_ctor_get(x_49, 1); +lean_inc(x_70); +lean_inc(x_1); +x_71 = l_Lean_Parser_tokenFn(x_1, x_49); +x_72 = lean_ctor_get(x_71, 3); +lean_inc(x_72); +if (lean_obj_tag(x_72) == 0) +{ +lean_object* x_73; lean_object* x_74; +x_73 = lean_ctor_get(x_71, 0); +lean_inc(x_73); +x_74 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_73); +lean_dec(x_73); +if (lean_obj_tag(x_74) == 2) +{ +lean_object* x_75; lean_object* x_76; uint8_t x_77; +x_75 = lean_ctor_get(x_74, 1); +lean_inc(x_75); +lean_dec(x_74); +x_76 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__6; +x_77 = lean_string_dec_eq(x_75, x_76); +lean_dec(x_75); +if (x_77 == 0) +{ +lean_object* x_78; lean_object* x_79; +x_78 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +x_79 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_78, x_70); +x_53 = x_79; +goto block_69; } else { -lean_object* x_57; lean_object* x_58; lean_object* x_59; +lean_dec(x_70); +x_53 = x_71; +goto block_69; +} +} +else +{ +lean_object* x_80; lean_object* x_81; +lean_dec(x_74); +x_80 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +x_81 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_80, x_70); +x_53 = x_81; +goto block_69; +} +} +else +{ +lean_object* x_82; lean_object* x_83; +lean_dec(x_72); +x_82 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__9; +x_83 = l_Lean_Parser_ParserState_mkErrorsAt(x_71, x_82, x_70); +x_53 = x_83; +goto block_69; +} +block_69: +{ +lean_object* x_54; +x_54 = lean_ctor_get(x_53, 3); +lean_inc(x_54); +if (lean_obj_tag(x_54) == 0) +{ +lean_object* x_55; lean_object* x_56; +lean_inc(x_1); +x_55 = l_Lean_Parser_Term_optExprPrecedence___elambda__1(x_1, x_53); +x_56 = lean_ctor_get(x_55, 3); +lean_inc(x_56); +if (lean_obj_tag(x_56) == 0) +{ +lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; +x_57 = l_Lean_Parser_termParser___closed__2; +x_58 = lean_unsigned_to_nat(0u); +x_59 = l_Lean_Parser_categoryParser___elambda__1(x_57, x_58, x_1, x_55); +x_60 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_61 = l_Lean_Parser_ParserState_mkNode(x_59, x_60, x_52); +x_62 = l_Lean_Parser_mergeOrElseErrors(x_61, x_44, x_41); +lean_dec(x_41); +return x_62; +} +else +{ +lean_object* x_63; lean_object* x_64; lean_object* x_65; +lean_dec(x_56); +lean_dec(x_1); +x_63 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_64 = l_Lean_Parser_ParserState_mkNode(x_55, x_63, x_52); +x_65 = l_Lean_Parser_mergeOrElseErrors(x_64, x_44, x_41); +lean_dec(x_41); +return x_65; +} +} +else +{ +lean_object* x_66; lean_object* x_67; lean_object* x_68; +lean_dec(x_54); +lean_dec(x_1); +x_66 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; +x_67 = l_Lean_Parser_ParserState_mkNode(x_53, x_66, x_52); +x_68 = l_Lean_Parser_mergeOrElseErrors(x_67, x_44, x_41); +lean_dec(x_41); +return x_68; +} +} +} +else +{ +lean_object* x_84; lean_dec(x_50); lean_dec(x_1); -x_57 = l_Lean_Parser_Term_tparser_x21___elambda__1___closed__2; -x_58 = l_Lean_Parser_ParserState_mkNode(x_49, x_57, x_48); -x_59 = l_Lean_Parser_mergeOrElseErrors(x_58, x_40, x_37); -lean_dec(x_37); -return x_59; -} -} -} -else -{ -lean_object* x_75; -lean_dec(x_46); -lean_dec(x_1); -x_75 = l_Lean_Parser_mergeOrElseErrors(x_45, x_40, x_37); -lean_dec(x_37); -return x_75; +x_84 = l_Lean_Parser_mergeOrElseErrors(x_49, x_44, x_41); +lean_dec(x_41); +return x_84; } } } @@ -34312,13 +34692,11 @@ return x_2; lean_object* _init_l_Lean_Parser_Term_tparser_x21___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_antiquotNestedExpr___closed__2; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Term_tparser_x21___closed__1; -x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_tparser_x21___closed__1; +x_2 = l_Lean_Parser_Term_parser_x21___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Term_tparser_x21___closed__3() { @@ -57281,6 +57659,22 @@ lean_mark_persistent(l_Lean_Parser_Term_nomatch); res = l___regBuiltinParser_Lean_Parser_Term_nomatch(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1 = _init_l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__1); +l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2 = _init_l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__2); +l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3 = _init_l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3); +l_Lean_Parser_Term_optExprPrecedence___closed__1 = _init_l_Lean_Parser_Term_optExprPrecedence___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___closed__1); +l_Lean_Parser_Term_optExprPrecedence___closed__2 = _init_l_Lean_Parser_Term_optExprPrecedence___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___closed__2); +l_Lean_Parser_Term_optExprPrecedence___closed__3 = _init_l_Lean_Parser_Term_optExprPrecedence___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___closed__3); +l_Lean_Parser_Term_optExprPrecedence___closed__4 = _init_l_Lean_Parser_Term_optExprPrecedence___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence___closed__4); +l_Lean_Parser_Term_optExprPrecedence = _init_l_Lean_Parser_Term_optExprPrecedence(); +lean_mark_persistent(l_Lean_Parser_Term_optExprPrecedence); l_Lean_Parser_Term_parser_x21___elambda__1___closed__1 = _init_l_Lean_Parser_Term_parser_x21___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_parser_x21___elambda__1___closed__1); l_Lean_Parser_Term_parser_x21___elambda__1___closed__2 = _init_l_Lean_Parser_Term_parser_x21___elambda__1___closed__2(); @@ -57313,6 +57707,8 @@ l_Lean_Parser_Term_parser_x21___closed__6 = _init_l_Lean_Parser_Term_parser_x21_ lean_mark_persistent(l_Lean_Parser_Term_parser_x21___closed__6); l_Lean_Parser_Term_parser_x21___closed__7 = _init_l_Lean_Parser_Term_parser_x21___closed__7(); lean_mark_persistent(l_Lean_Parser_Term_parser_x21___closed__7); +l_Lean_Parser_Term_parser_x21___closed__8 = _init_l_Lean_Parser_Term_parser_x21___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_parser_x21___closed__8); l_Lean_Parser_Term_parser_x21 = _init_l_Lean_Parser_Term_parser_x21(); lean_mark_persistent(l_Lean_Parser_Term_parser_x21); res = l___regBuiltinParser_Lean_Parser_Term_parser_x21(lean_io_mk_world());