From 6be9a73e5197d142090322dd349f80b239bb2ec4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Feb 2020 20:15:00 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Parser/Parser.lean | 19 +- stage0/src/Init/Lean/Parser/Term.lean | 6 +- stage0/stdlib/Init/Lean/Parser/Parser.c | 170 ++++++++--- stage0/stdlib/Init/Lean/Parser/Term.c | 385 ++++++++++++++---------- 4 files changed, 364 insertions(+), 216 deletions(-) diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean index 4c05044a80..3359275793 100644 --- a/stage0/src/Init/Lean/Parser/Parser.lean +++ b/stage0/src/Init/Lean/Parser/Parser.lean @@ -1043,14 +1043,14 @@ let asciiSym := asciiSym.trim; fn := unicodeSymbolFn sym asciiSym } /- Succeeds if RBP > lower -/ -def checkRBPGreaterFn (lower : Nat) : ParserFn := +def checkRBPGreaterFn (lower : Nat) (errorMsg : String) : ParserFn := fun c s => - if c.rbp > lower then s.mkUnexpectedError "parentheses are needed" -- improve error message + if c.rbp > lower then s.mkUnexpectedError errorMsg else s -def checkRBPGreater (lower : Nat) : Parser := +def checkRBPGreater (lower : Nat) (errorMsg : String) : Parser := { info := epsilonInfo, - fn := checkRBPGreaterFn lower } + fn := checkRBPGreaterFn lower errorMsg } def mkAtomicInfo (k : String) : ParserInfo := { firstTokens := FirstTokens.tokens [ { val := k } ] } @@ -1399,6 +1399,17 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par let s := mkTrailingResult s iniSz; trailingLoop s +def checkTokenLBPFn : ParserFn := +fun c s => + let left := s.stxStack.back; + let (s, lbp) := currLbp left c s; + if c.rbp < lbp then s + else s.mkUnexpectedError "unexpected token" + +def checkTokenLBP : Parser := +{ info := epsilonInfo, + fn := checkTokenLBPFn } + /-- Implements a recursive precedence parser according to Pratt's algorithm. diff --git a/stage0/src/Init/Lean/Parser/Term.lean b/stage0/src/Init/Lean/Parser/Term.lean index fce1653073..32e0cd61db 100644 --- a/stage0/src/Init/Lean/Parser/Term.lean +++ b/stage0/src/Init/Lean/Parser/Term.lean @@ -78,7 +78,7 @@ def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}" def instBinder := parser! "[" >> optIdent >> termParser >> "]" def bracktedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder -@[builtinTermParser] def depArrow := parser! bracktedBinder true >> checkRBPGreater 25 >> unicodeSymbol " → " " -> " >> termParser +@[builtinTermParser] def depArrow := parser! bracktedBinder true >> checkRBPGreater 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser def simpleBinder := parser! many1 binderIdent @[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser @@ -116,7 +116,7 @@ def doExpr := parser! termParser def doElem := doLet <|> doId <|> doPat <|> doExpr def doSeq := sepBy1 doElem "; " def bracketedDoSeq := parser! "{" >> doSeq >> "}" -@[builtinTermParser] def liftMethod := parser! checkRBPGreater (appPrec-1) >> leftArrow >> termParser +@[builtinTermParser] def liftMethod := parser! checkRBPGreater (appPrec-1) "expected parentheses monad lift operator" >> leftArrow >> termParser @[builtinTermParser] def «do» := parser! "do " >> (bracketedDoSeq <|> doSeq) @[builtinTermParser] def not := parser! symbol "¬" 40 >> termParser 40 @@ -124,7 +124,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}" @[builtinTermParser] def uminus := parser! "-" >> termParser 100 def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")" -@[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec) +@[builtinTermParser] def app := tparser! many1 (namedArgument <|> (checkTokenLBP >> termParser appPrec)) def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort) @[builtinTermParser] def sortApp := tparser! checkIsSort >> levelParser appPrec diff --git a/stage0/stdlib/Init/Lean/Parser/Parser.c b/stage0/stdlib/Init/Lean/Parser/Parser.c index 3d9a2b4525..7e251b22d1 100644 --- a/stage0/stdlib/Init/Lean/Parser/Parser.c +++ b/stage0/stdlib/Init/Lean/Parser/Parser.c @@ -33,7 +33,7 @@ lean_object* l_Lean_Parser_symbolAux___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_hashOrelse; lean_object* l_Lean_Parser_hashAndthen___closed__1; lean_object* l_RBNode_ins___main___at_Lean_Parser_TokenMap_insert___spec__7___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*); size_t l_USize_add(size_t, size_t); lean_object* l_Lean_Parser_manyAux___main___closed__1; lean_object* l_Lean_Parser_numLit___elambda__1___closed__2; @@ -123,6 +123,7 @@ lean_object* l_Array_foldSepBy___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_numLit___elambda__1___closed__1; lean_object* l___private_Init_Lean_Parser_Parser_1__expectedToString___main(lean_object*); lean_object* l_Lean_Parser_longestMatchFn(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkTokenLBP___closed__1; lean_object* l_Lean_Parser_fieldIdx___closed__6; lean_object* l_Lean_Parser_registerBuiltinParserAttribute___closed__1; lean_object* l_Lean_Parser_nameLitNoAntiquot; @@ -167,7 +168,7 @@ lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*); lean_object* l_Lean_Parser_mkAntiquot___closed__17; lean_object* l_Lean_Syntax_foldSepArgsM(lean_object*, lean_object*); lean_object* l_Lean_Parser_builtinParserCategoriesRef; -lean_object* l_Lean_Parser_checkRBPGreater(lean_object*); +lean_object* l_Lean_Parser_checkRBPGreater(lean_object*, lean_object*); lean_object* lean_environment_find(lean_object*, lean_object*); lean_object* l_Lean_Parser_parserExtension; lean_object* l_Lean_Parser_unquotedSymbolFn___closed__1; @@ -265,6 +266,7 @@ lean_object* l_Lean_Parser_symbolFnAux___boxed(lean_object*, lean_object*, lean_ lean_object* l_Lean_Parser_mkNodeToken___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_initCacheForInput___boxed(lean_object*); lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_forArgsM___spec__1(lean_object*); +lean_object* l_Lean_Parser_checkTokenLBPFn(lean_object*, lean_object*); lean_object* l_Lean_Parser_symbolNoWs___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_isParserCategory___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_declareBuiltinParser___closed__2; @@ -478,7 +480,7 @@ lean_object* l_Lean_Parser_parserExtension___closed__4; lean_object* l_Lean_Parser_identFnAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_numLitKind___closed__1; -lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_optionaInfo(lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_11__mkTrailingResult(lean_object*, lean_object*); lean_object* l_Lean_Parser_FirstTokens_seq(lean_object*, lean_object*); @@ -610,6 +612,7 @@ lean_object* l___private_Init_Lean_Parser_Parser_15__antiquotExpr___closed__3; lean_object* l_Lean_Parser_parserExtension___elambda__2(lean_object*); lean_object* l_Lean_Parser_mkAntiquot___closed__13; extern lean_object* l_Lean_mkAppStx___closed__6; +lean_object* l_Lean_Parser_checkTokenLBP___closed__2; extern lean_object* l_Lean_Options_empty; extern lean_object* l_IO_Error_Inhabited___closed__1; lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_octalNumberFn___spec__1(lean_object*, lean_object*, lean_object*); @@ -649,9 +652,11 @@ lean_object* l_Lean_Parser_Error_toString___closed__2; lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__9; lean_object* l___private_Init_Lean_Data_Trie_3__findAux___main___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3; +lean_object* l_Lean_Parser_checkTokenLBPFn___closed__1; lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2; lean_object* l_IO_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkTokenLBP; lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_26__catNameToString(lean_object*); size_t l_USize_mul(size_t, size_t); @@ -820,7 +825,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_many1Indent___spec__1 lean_object* l_Lean_Parser_chFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Parser_isValidSyntaxNodeKind(lean_object*, lean_object*); lean_object* l_Lean_Parser_numLitNoAntiquot; -lean_object* l_Lean_Parser_checkRBPGreaterFn___closed__1; lean_object* l_Lean_Parser_Error_beq___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_orelseInfo___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_15__antiquotExpr; @@ -836,7 +840,7 @@ lean_object* l_Lean_Parser_quotedSymbolFn___boxed(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___closed__7; lean_object* l___private_Init_Lean_Parser_Parser_29__registerParserAttributeImplBuilder___closed__1; uint8_t l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_mkParserExtension___closed__5; lean_object* l_Lean_Parser_dollarSymbol___closed__3; lean_object* l_Lean_Parser_satisfySymbolFn(lean_object*, lean_object*, lean_object*, lean_object*); @@ -860,7 +864,7 @@ lean_object* l___private_Init_Lean_Parser_Parser_29__registerParserAttributeImpl lean_object* l_Lean_Parser_unquotedSymbol; lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1; lean_object* l_Lean_Parser_hashOrelse___closed__1; -lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_12__noImmediateColon___closed__1; lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2___boxed(lean_object*); lean_object* l_Lean_Parser_many1Indent(lean_object*, lean_object*); @@ -10594,72 +10598,65 @@ lean_dec(x_1); return x_4; } } -lean_object* _init_l_Lean_Parser_checkRBPGreaterFn___closed__1() { +lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_1; -x_1 = lean_mk_string("parentheses are needed"); -return x_1; -} -} -lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object* x_1, lean_object* x_2, lean_object* x_3) { -_start: +lean_object* x_5; uint8_t x_6; +x_5 = lean_ctor_get(x_3, 1); +x_6 = lean_nat_dec_lt(x_1, x_5); +if (x_6 == 0) { -lean_object* x_4; uint8_t x_5; -x_4 = lean_ctor_get(x_2, 1); -x_5 = lean_nat_dec_lt(x_1, x_4); -if (x_5 == 0) -{ -return x_3; +lean_dec(x_2); +return x_4; } else { -lean_object* x_6; lean_object* x_7; -x_6 = l_Lean_Parser_checkRBPGreaterFn___closed__1; -x_7 = l_Lean_Parser_ParserState_mkUnexpectedError(x_3, x_6); +lean_object* x_7; +x_7 = l_Lean_Parser_ParserState_mkUnexpectedError(x_4, x_2); return x_7; } } } -lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_checkRBPGreaterFn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_4; -x_4 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3); -lean_dec(x_2); +lean_object* x_5; +x_5 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3, x_4); +lean_dec(x_3); lean_dec(x_1); -return x_4; +return x_5; } } -lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_checkRBPGreater___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_4; -x_4 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3); -return x_4; +lean_object* x_5; +x_5 = l_Lean_Parser_checkRBPGreaterFn(x_1, x_2, x_3, x_4); +return x_5; } } -lean_object* l_Lean_Parser_checkRBPGreater(lean_object* x_1) { +lean_object* l_Lean_Parser_checkRBPGreater(lean_object* x_1, lean_object* x_2) { _start: { -lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = lean_alloc_closure((void*)(l_Lean_Parser_checkRBPGreater___elambda__1___boxed), 3, 1); -lean_closure_set(x_2, 0, x_1); -x_3 = l_Lean_Parser_epsilonInfo; -x_4 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_4, 0, x_3); -lean_ctor_set(x_4, 1, x_2); -return x_4; +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_alloc_closure((void*)(l_Lean_Parser_checkRBPGreater___elambda__1___boxed), 4, 2); +lean_closure_set(x_3, 0, x_1); +lean_closure_set(x_3, 1, x_2); +x_4 = l_Lean_Parser_epsilonInfo; +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_3); +return x_5; } } -lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_checkRBPGreater___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_4; -x_4 = l_Lean_Parser_checkRBPGreater___elambda__1(x_1, x_2, x_3); -lean_dec(x_2); +lean_object* x_5; +x_5 = l_Lean_Parser_checkRBPGreater___elambda__1(x_1, x_2, x_3, x_4); +lean_dec(x_3); lean_dec(x_1); -return x_4; +return x_5; } } lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object* x_1) { @@ -24408,6 +24405,77 @@ x_4 = l_Lean_Parser_trailingLoop___main(x_1, x_2, x_3); return x_4; } } +lean_object* _init_l_Lean_Parser_checkTokenLBPFn___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("unexpected token"); +return x_1; +} +} +lean_object* l_Lean_Parser_checkTokenLBPFn(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_7; lean_object* x_8; uint8_t x_9; +x_3 = lean_ctor_get(x_2, 0); +lean_inc(x_3); +x_4 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_3); +lean_dec(x_3); +lean_inc(x_1); +x_5 = l_Lean_Parser_currLbp(x_4, x_1, x_2); +lean_dec(x_4); +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_5, 1); +lean_inc(x_7); +lean_dec(x_5); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_dec(x_1); +x_9 = lean_nat_dec_lt(x_8, x_7); +lean_dec(x_7); +lean_dec(x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; +x_10 = l_Lean_Parser_checkTokenLBPFn___closed__1; +x_11 = l_Lean_Parser_ParserState_mkUnexpectedError(x_6, x_10); +return x_11; +} +else +{ +return x_6; +} +} +} +lean_object* _init_l_Lean_Parser_checkTokenLBP___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_checkTokenLBPFn), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_checkTokenLBP___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_checkTokenLBP___closed__1; +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_checkTokenLBP() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_checkTokenLBP___closed__2; +return x_1; +} +} lean_object* l_Lean_Parser_prattParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6) { _start: { @@ -37195,8 +37263,6 @@ l_Lean_Parser_unicodeSymbolInfo___closed__1 = _init_l_Lean_Parser_unicodeSymbolI lean_mark_persistent(l_Lean_Parser_unicodeSymbolInfo___closed__1); l_Lean_Parser_unicodeSymbolFn___closed__1 = _init_l_Lean_Parser_unicodeSymbolFn___closed__1(); lean_mark_persistent(l_Lean_Parser_unicodeSymbolFn___closed__1); -l_Lean_Parser_checkRBPGreaterFn___closed__1 = _init_l_Lean_Parser_checkRBPGreaterFn___closed__1(); -lean_mark_persistent(l_Lean_Parser_checkRBPGreaterFn___closed__1); l_Lean_Parser_mkAtomicInfo___closed__1 = _init_l_Lean_Parser_mkAtomicInfo___closed__1(); lean_mark_persistent(l_Lean_Parser_mkAtomicInfo___closed__1); l_Lean_Parser_mkAtomicInfo___closed__2 = _init_l_Lean_Parser_mkAtomicInfo___closed__2(); @@ -37293,6 +37359,14 @@ l_Lean_Parser_ParserCategory_inhabited___closed__1 = _init_l_Lean_Parser_ParserC lean_mark_persistent(l_Lean_Parser_ParserCategory_inhabited___closed__1); l_Lean_Parser_ParserCategory_inhabited = _init_l_Lean_Parser_ParserCategory_inhabited(); lean_mark_persistent(l_Lean_Parser_ParserCategory_inhabited); +l_Lean_Parser_checkTokenLBPFn___closed__1 = _init_l_Lean_Parser_checkTokenLBPFn___closed__1(); +lean_mark_persistent(l_Lean_Parser_checkTokenLBPFn___closed__1); +l_Lean_Parser_checkTokenLBP___closed__1 = _init_l_Lean_Parser_checkTokenLBP___closed__1(); +lean_mark_persistent(l_Lean_Parser_checkTokenLBP___closed__1); +l_Lean_Parser_checkTokenLBP___closed__2 = _init_l_Lean_Parser_checkTokenLBP___closed__2(); +lean_mark_persistent(l_Lean_Parser_checkTokenLBP___closed__2); +l_Lean_Parser_checkTokenLBP = _init_l_Lean_Parser_checkTokenLBP(); +lean_mark_persistent(l_Lean_Parser_checkTokenLBP); l_Lean_Parser_mkCategoryParserFnRef___closed__1 = _init_l_Lean_Parser_mkCategoryParserFnRef___closed__1(); lean_mark_persistent(l_Lean_Parser_mkCategoryParserFnRef___closed__1); res = l_Lean_Parser_mkCategoryParserFnRef(lean_io_mk_world()); diff --git a/stage0/stdlib/Init/Lean/Parser/Term.c b/stage0/stdlib/Init/Lean/Parser/Term.c index cf0a5f3a76..e188ba30e6 100644 --- a/stage0/stdlib/Init/Lean/Parser/Term.c +++ b/stage0/stdlib/Init/Lean/Parser/Term.c @@ -392,6 +392,7 @@ lean_object* l_Lean_Parser_Term_mod___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__6; lean_object* l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(lean_object*); lean_object* l_Lean_Parser_Term_instBinder___closed__3; +lean_object* l_Lean_Parser_Term_liftMethod___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_and; lean_object* l_Lean_Parser_Term_gt___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1(lean_object*, lean_object*); @@ -422,6 +423,7 @@ lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_simpleBinder___closed__3; lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_parser_x21___closed__5; +lean_object* l_Lean_Parser_checkTokenLBPFn(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__6; lean_object* lean_string_utf8_byte_size(lean_object*); @@ -1143,6 +1145,7 @@ lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_typeAscription___closed__3; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_matchAlts___elambda__1___spec__2___closed__5; lean_object* l_Lean_Parser_Term_have___closed__10; +lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__15; lean_object* l_Lean_Parser_Term_borrowed___closed__7; lean_object* l_Lean_Parser_Term_doLet___closed__5; lean_object* l___regBuiltinParser_Lean_Parser_Term_prod(lean_object*); @@ -1474,7 +1477,8 @@ lean_object* l_Lean_Parser_Term_letIdDecl___closed__5; lean_object* l_Lean_Parser_Term_match___closed__4; extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1; lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__5; -lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_app___closed__5; +lean_object* l_Lean_Parser_checkRBPGreaterFn(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_if___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_explicitUniv___closed__1; lean_object* l_Lean_Parser_Term_where___elambda__1___closed__1; @@ -18725,19 +18729,17 @@ return x_2; lean_object* _init_l_Lean_Parser_Term_depArrow___elambda__1___closed__10() { _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_Term_depArrow___elambda__1___closed__7; -x_3 = lean_string_append(x_1, x_2); -return x_3; +lean_object* x_1; +x_1 = lean_mk_string("expected parentheses around dependent arrow"); +return x_1; } } lean_object* _init_l_Lean_Parser_Term_depArrow___elambda__1___closed__11() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__10; -x_2 = l_Lean_Parser_unicodeSymbolFn___closed__1; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__7; x_3 = lean_string_append(x_1, x_2); return x_3; } @@ -18747,7 +18749,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__11; -x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9; +x_2 = l_Lean_Parser_unicodeSymbolFn___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } @@ -18757,7 +18759,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__12; -x_2 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9; x_3 = lean_string_append(x_1, x_2); return x_3; } @@ -18766,8 +18768,18 @@ lean_object* _init_l_Lean_Parser_Term_depArrow___elambda__1___closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_depArrow___elambda__1___closed__13; +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_depArrow___elambda__1___closed__15() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__13; +x_2 = l_Lean_Parser_Term_depArrow___elambda__1___closed__14; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); @@ -18837,67 +18849,68 @@ x_19 = lean_ctor_get(x_18, 3); lean_inc(x_19); if (lean_obj_tag(x_19) == 0) { -lean_object* x_20; lean_object* x_21; lean_object* x_22; +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; x_20 = lean_unsigned_to_nat(25u); -x_21 = l_Lean_Parser_checkRBPGreaterFn(x_20, x_1, x_18); -x_22 = lean_ctor_get(x_21, 3); -lean_inc(x_22); -if (lean_obj_tag(x_22) == 0) +x_21 = l_Lean_Parser_Term_depArrow___elambda__1___closed__10; +x_22 = l_Lean_Parser_checkRBPGreaterFn(x_20, x_21, x_1, x_18); +x_23 = lean_ctor_get(x_22, 3); +lean_inc(x_23); +if (lean_obj_tag(x_23) == 0) { -lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_23 = l_Lean_Parser_Term_depArrow___elambda__1___closed__7; -x_24 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9; -x_25 = l_Lean_Parser_Term_depArrow___elambda__1___closed__14; +lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; +x_24 = l_Lean_Parser_Term_depArrow___elambda__1___closed__7; +x_25 = l_Lean_Parser_Term_depArrow___elambda__1___closed__9; +x_26 = l_Lean_Parser_Term_depArrow___elambda__1___closed__15; lean_inc(x_1); -x_26 = l_Lean_Parser_unicodeSymbolFnAux(x_23, x_24, x_25, x_1, x_21); -x_27 = lean_ctor_get(x_26, 3); -lean_inc(x_27); -if (lean_obj_tag(x_27) == 0) +x_27 = l_Lean_Parser_unicodeSymbolFnAux(x_24, x_25, x_26, x_1, x_22); +x_28 = lean_ctor_get(x_27, 3); +lean_inc(x_28); +if (lean_obj_tag(x_28) == 0) { -lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; -x_28 = l_Lean_Parser_termParser___closed__2; -x_29 = lean_unsigned_to_nat(0u); -x_30 = l_Lean_Parser_categoryParser___elambda__1(x_28, x_29, x_1, x_26); -x_31 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; -x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_17); -x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_12, x_9); +lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; +x_29 = l_Lean_Parser_termParser___closed__2; +x_30 = lean_unsigned_to_nat(0u); +x_31 = l_Lean_Parser_categoryParser___elambda__1(x_29, x_30, x_1, x_27); +x_32 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; +x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_17); +x_34 = l_Lean_Parser_mergeOrElseErrors(x_33, x_12, x_9); lean_dec(x_9); -return x_33; +return x_34; } else { -lean_object* x_34; lean_object* x_35; lean_object* x_36; -lean_dec(x_27); +lean_object* x_35; lean_object* x_36; lean_object* x_37; +lean_dec(x_28); lean_dec(x_1); -x_34 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; -x_35 = l_Lean_Parser_ParserState_mkNode(x_26, x_34, x_17); -x_36 = l_Lean_Parser_mergeOrElseErrors(x_35, x_12, x_9); +x_35 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; +x_36 = l_Lean_Parser_ParserState_mkNode(x_27, x_35, x_17); +x_37 = l_Lean_Parser_mergeOrElseErrors(x_36, x_12, x_9); lean_dec(x_9); -return x_36; +return x_37; } } else { -lean_object* x_37; lean_object* x_38; lean_object* x_39; -lean_dec(x_22); +lean_object* x_38; lean_object* x_39; lean_object* x_40; +lean_dec(x_23); lean_dec(x_1); -x_37 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; -x_38 = l_Lean_Parser_ParserState_mkNode(x_21, x_37, x_17); -x_39 = l_Lean_Parser_mergeOrElseErrors(x_38, x_12, x_9); +x_38 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; +x_39 = l_Lean_Parser_ParserState_mkNode(x_22, x_38, x_17); +x_40 = l_Lean_Parser_mergeOrElseErrors(x_39, x_12, x_9); lean_dec(x_9); -return x_39; +return x_40; } } else { -lean_object* x_40; lean_object* x_41; lean_object* x_42; +lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_dec(x_19); lean_dec(x_1); -x_40 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; -x_41 = l_Lean_Parser_ParserState_mkNode(x_18, x_40, x_17); -x_42 = l_Lean_Parser_mergeOrElseErrors(x_41, x_12, x_9); +x_41 = l_Lean_Parser_Term_depArrow___elambda__1___closed__2; +x_42 = l_Lean_Parser_ParserState_mkNode(x_18, x_41, x_17); +x_43 = l_Lean_Parser_mergeOrElseErrors(x_42, x_12, x_9); lean_dec(x_9); -return x_42; +return x_43; } } } @@ -29104,6 +29117,14 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); return x_4; } } +lean_object* _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("expected parentheses monad lift operator"); +return x_1; +} +} lean_object* l_Lean_Parser_Term_liftMethod___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -29148,7 +29169,7 @@ return x_8; } else { -lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_inc(x_7); x_13 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7); lean_dec(x_6); @@ -29157,50 +29178,51 @@ lean_inc(x_14); x_15 = lean_array_get_size(x_14); lean_dec(x_14); x_16 = l_Lean_Parser_Term_borrowed___elambda__1___closed__7; -x_17 = l_Lean_Parser_checkRBPGreaterFn(x_16, x_1, x_13); -x_18 = lean_ctor_get(x_17, 3); -lean_inc(x_18); -if (lean_obj_tag(x_18) == 0) +x_17 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__5; +x_18 = l_Lean_Parser_checkRBPGreaterFn(x_16, x_17, x_1, x_13); +x_19 = lean_ctor_get(x_18, 3); +lean_inc(x_19); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_19; lean_object* x_20; +lean_object* x_20; lean_object* x_21; lean_inc(x_1); -x_19 = l_Lean_Parser_Term_leftArrow___elambda__1(x_1, x_17); -x_20 = lean_ctor_get(x_19, 3); -lean_inc(x_20); -if (lean_obj_tag(x_20) == 0) +x_20 = l_Lean_Parser_Term_leftArrow___elambda__1(x_1, x_18); +x_21 = lean_ctor_get(x_20, 3); +lean_inc(x_21); +if (lean_obj_tag(x_21) == 0) { -lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; -x_21 = l_Lean_Parser_termParser___closed__2; -x_22 = lean_unsigned_to_nat(0u); -x_23 = l_Lean_Parser_categoryParser___elambda__1(x_21, x_22, x_1, x_19); -x_24 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_15); -x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_10, x_7); +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; +x_22 = l_Lean_Parser_termParser___closed__2; +x_23 = lean_unsigned_to_nat(0u); +x_24 = l_Lean_Parser_categoryParser___elambda__1(x_22, x_23, x_1, x_20); +x_25 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; +x_26 = l_Lean_Parser_ParserState_mkNode(x_24, x_25, x_15); +x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_10, x_7); lean_dec(x_7); -return x_26; +return x_27; } else { -lean_object* x_27; lean_object* x_28; lean_object* x_29; -lean_dec(x_20); +lean_object* x_28; lean_object* x_29; lean_object* x_30; +lean_dec(x_21); lean_dec(x_1); -x_27 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_28 = l_Lean_Parser_ParserState_mkNode(x_19, x_27, x_15); -x_29 = l_Lean_Parser_mergeOrElseErrors(x_28, x_10, x_7); +x_28 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; +x_29 = l_Lean_Parser_ParserState_mkNode(x_20, x_28, x_15); +x_30 = l_Lean_Parser_mergeOrElseErrors(x_29, x_10, x_7); lean_dec(x_7); -return x_29; +return x_30; } } else { -lean_object* x_30; lean_object* x_31; lean_object* x_32; -lean_dec(x_18); +lean_object* x_31; lean_object* x_32; lean_object* x_33; +lean_dec(x_19); lean_dec(x_1); -x_30 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; -x_31 = l_Lean_Parser_ParserState_mkNode(x_17, x_30, x_15); -x_32 = l_Lean_Parser_mergeOrElseErrors(x_31, x_10, x_7); +x_31 = l_Lean_Parser_Term_liftMethod___elambda__1___closed__2; +x_32 = l_Lean_Parser_ParserState_mkNode(x_18, x_31, x_15); +x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_10, x_7); lean_dec(x_7); -return x_32; +return x_33; } } } @@ -31197,17 +31219,33 @@ goto block_16; } else { -lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_inc(x_5); x_22 = l_Lean_Parser_ParserState_restore(x_17, x_4, x_5); -x_23 = l_Lean_Parser_termParser___closed__2; -x_24 = l_Lean_Parser_appPrec; lean_inc(x_1); -x_25 = l_Lean_Parser_categoryParser___elambda__1(x_23, x_24, x_1, x_22); -x_26 = l_Lean_Parser_mergeOrElseErrors(x_25, x_19, x_5); -x_6 = x_26; +x_23 = l_Lean_Parser_checkTokenLBPFn(x_1, x_22); +x_24 = lean_ctor_get(x_23, 3); +lean_inc(x_24); +if (lean_obj_tag(x_24) == 0) +{ +lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; +x_25 = l_Lean_Parser_termParser___closed__2; +x_26 = l_Lean_Parser_appPrec; +lean_inc(x_1); +x_27 = l_Lean_Parser_categoryParser___elambda__1(x_25, x_26, x_1, x_23); +x_28 = l_Lean_Parser_mergeOrElseErrors(x_27, x_19, x_5); +x_6 = x_28; goto block_16; } +else +{ +lean_object* x_29; +lean_dec(x_24); +x_29 = l_Lean_Parser_mergeOrElseErrors(x_23, x_19, x_5); +x_6 = x_29; +goto block_16; +} +} } block_16: { @@ -31266,121 +31304,140 @@ return x_15; lean_object* l_Lean_Parser_Term_app___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_7; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_17; lean_object* x_18; lean_object* x_19; 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, 1); -lean_inc(x_5); +x_17 = lean_ctor_get(x_2, 1); +lean_inc(x_17); lean_inc(x_1); -x_6 = l_Lean_Parser_Term_namedArgument___elambda__1(x_1, x_2); -x_7 = lean_ctor_get(x_6, 3); -lean_inc(x_7); -if (lean_obj_tag(x_7) == 0) +x_18 = l_Lean_Parser_Term_namedArgument___elambda__1(x_1, x_2); +x_19 = lean_ctor_get(x_18, 3); +lean_inc(x_19); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; -lean_dec(x_5); -x_8 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_1, x_6); -x_9 = l_Lean_nullKind; -lean_inc(x_4); -x_10 = l_Lean_Parser_ParserState_mkNode(x_8, x_9, x_4); -x_11 = l_Lean_mkAppStx___closed__8; -x_12 = l_Lean_Parser_ParserState_mkTrailingNode(x_10, x_11, x_4); -lean_dec(x_4); -return x_12; +lean_dec(x_17); +x_5 = x_18; +goto block_16; } else { -lean_object* x_13; lean_object* x_14; uint8_t x_15; -x_13 = lean_ctor_get(x_7, 0); -lean_inc(x_13); -lean_dec(x_7); -x_14 = lean_ctor_get(x_6, 1); -lean_inc(x_14); -x_15 = lean_nat_dec_eq(x_14, x_5); -lean_dec(x_14); -if (x_15 == 0) +lean_object* x_20; lean_object* x_21; uint8_t x_22; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +lean_dec(x_19); +x_21 = lean_ctor_get(x_18, 1); +lean_inc(x_21); +x_22 = lean_nat_dec_eq(x_21, x_17); +lean_dec(x_21); +if (x_22 == 0) { -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; -lean_dec(x_13); -lean_dec(x_5); -lean_dec(x_1); -x_16 = l_Lean_nullKind; -lean_inc(x_4); -x_17 = l_Lean_Parser_ParserState_mkNode(x_6, x_16, x_4); -x_18 = l_Lean_mkAppStx___closed__8; -x_19 = l_Lean_Parser_ParserState_mkTrailingNode(x_17, x_18, x_4); -lean_dec(x_4); -return x_19; +lean_dec(x_20); +lean_dec(x_17); +x_5 = x_18; +goto block_16; } else { -lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; -lean_inc(x_5); -x_20 = l_Lean_Parser_ParserState_restore(x_6, x_4, x_5); -x_21 = l_Lean_Parser_termParser___closed__2; -x_22 = l_Lean_Parser_appPrec; +lean_object* x_23; lean_object* x_24; lean_object* x_25; +lean_inc(x_17); +x_23 = l_Lean_Parser_ParserState_restore(x_18, x_4, x_17); lean_inc(x_1); -x_23 = l_Lean_Parser_categoryParser___elambda__1(x_21, x_22, x_1, x_20); -x_24 = l_Lean_Parser_mergeOrElseErrors(x_23, x_13, x_5); -lean_dec(x_5); +x_24 = l_Lean_Parser_checkTokenLBPFn(x_1, x_23); x_25 = lean_ctor_get(x_24, 3); lean_inc(x_25); if (lean_obj_tag(x_25) == 0) { -lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; -x_26 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_1, x_24); -x_27 = l_Lean_nullKind; -lean_inc(x_4); -x_28 = l_Lean_Parser_ParserState_mkNode(x_26, x_27, x_4); -x_29 = l_Lean_mkAppStx___closed__8; -x_30 = l_Lean_Parser_ParserState_mkTrailingNode(x_28, x_29, x_4); -lean_dec(x_4); -return x_30; +lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; +x_26 = l_Lean_Parser_termParser___closed__2; +x_27 = l_Lean_Parser_appPrec; +lean_inc(x_1); +x_28 = l_Lean_Parser_categoryParser___elambda__1(x_26, x_27, x_1, x_24); +x_29 = l_Lean_Parser_mergeOrElseErrors(x_28, x_20, x_17); +lean_dec(x_17); +x_5 = x_29; +goto block_16; } else { -lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; +lean_object* x_30; lean_dec(x_25); -lean_dec(x_1); -x_31 = l_Lean_nullKind; -lean_inc(x_4); -x_32 = l_Lean_Parser_ParserState_mkNode(x_24, x_31, x_4); -x_33 = l_Lean_mkAppStx___closed__8; -x_34 = l_Lean_Parser_ParserState_mkTrailingNode(x_32, x_33, x_4); -lean_dec(x_4); -return x_34; +x_30 = l_Lean_Parser_mergeOrElseErrors(x_24, x_20, x_17); +lean_dec(x_17); +x_5 = x_30; +goto block_16; } } } +block_16: +{ +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_manyAux___main___at_Lean_Parser_Term_app___elambda__1___spec__1(x_1, x_5); +x_8 = l_Lean_nullKind; +lean_inc(x_4); +x_9 = l_Lean_Parser_ParserState_mkNode(x_7, x_8, x_4); +x_10 = l_Lean_mkAppStx___closed__8; +x_11 = l_Lean_Parser_ParserState_mkTrailingNode(x_9, x_10, x_4); +lean_dec(x_4); +return x_11; +} +else +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +lean_dec(x_6); +lean_dec(x_1); +x_12 = l_Lean_nullKind; +lean_inc(x_4); +x_13 = l_Lean_Parser_ParserState_mkNode(x_5, x_12, x_4); +x_14 = l_Lean_mkAppStx___closed__8; +x_15 = l_Lean_Parser_ParserState_mkTrailingNode(x_13, x_14, x_4); +lean_dec(x_4); +return x_15; +} +} } } lean_object* _init_l_Lean_Parser_Term_app___closed__1() { _start: { -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_namedArgument; +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_Term_namedPattern___closed__2; -x_4 = lean_ctor_get(x_3, 0); -lean_inc(x_4); -x_5 = l_Lean_Parser_orelseInfo(x_2, x_4); -return x_5; +x_3 = l_Lean_Parser_epsilonInfo; +x_4 = l_Lean_Parser_andthenInfo(x_3, x_2); +return x_4; } } lean_object* _init_l_Lean_Parser_Term_app___closed__2() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Term_namedArgument; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Term_app___closed__1; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Term_app___closed__3() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_mkAppStx___closed__8; -x_2 = l_Lean_Parser_Term_app___closed__1; +x_2 = l_Lean_Parser_Term_app___closed__2; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_app___closed__3() { +lean_object* _init_l_Lean_Parser_Term_app___closed__4() { _start: { lean_object* x_1; @@ -31388,12 +31445,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_app___elambda__1), 2, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_app___closed__4() { +lean_object* _init_l_Lean_Parser_Term_app___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_app___closed__2; -x_2 = l_Lean_Parser_Term_app___closed__3; +x_1 = l_Lean_Parser_Term_app___closed__3; +x_2 = l_Lean_Parser_Term_app___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); @@ -31404,7 +31461,7 @@ lean_object* _init_l_Lean_Parser_Term_app() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_app___closed__4; +x_1 = l_Lean_Parser_Term_app___closed__5; return x_1; } } @@ -39116,6 +39173,8 @@ l_Lean_Parser_Term_depArrow___elambda__1___closed__13 = _init_l_Lean_Parser_Term lean_mark_persistent(l_Lean_Parser_Term_depArrow___elambda__1___closed__13); l_Lean_Parser_Term_depArrow___elambda__1___closed__14 = _init_l_Lean_Parser_Term_depArrow___elambda__1___closed__14(); lean_mark_persistent(l_Lean_Parser_Term_depArrow___elambda__1___closed__14); +l_Lean_Parser_Term_depArrow___elambda__1___closed__15 = _init_l_Lean_Parser_Term_depArrow___elambda__1___closed__15(); +lean_mark_persistent(l_Lean_Parser_Term_depArrow___elambda__1___closed__15); l_Lean_Parser_Term_depArrow___closed__1 = _init_l_Lean_Parser_Term_depArrow___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_depArrow___closed__1); l_Lean_Parser_Term_depArrow___closed__2 = _init_l_Lean_Parser_Term_depArrow___closed__2(); @@ -39802,6 +39861,8 @@ l_Lean_Parser_Term_liftMethod___elambda__1___closed__3 = _init_l_Lean_Parser_Ter lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__3); l_Lean_Parser_Term_liftMethod___elambda__1___closed__4 = _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__4(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__4); +l_Lean_Parser_Term_liftMethod___elambda__1___closed__5 = _init_l_Lean_Parser_Term_liftMethod___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_liftMethod___elambda__1___closed__5); l_Lean_Parser_Term_liftMethod___closed__1 = _init_l_Lean_Parser_Term_liftMethod___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_liftMethod___closed__1); l_Lean_Parser_Term_liftMethod___closed__2 = _init_l_Lean_Parser_Term_liftMethod___closed__2(); @@ -39997,6 +40058,8 @@ l_Lean_Parser_Term_app___closed__3 = _init_l_Lean_Parser_Term_app___closed__3(); lean_mark_persistent(l_Lean_Parser_Term_app___closed__3); l_Lean_Parser_Term_app___closed__4 = _init_l_Lean_Parser_Term_app___closed__4(); lean_mark_persistent(l_Lean_Parser_Term_app___closed__4); +l_Lean_Parser_Term_app___closed__5 = _init_l_Lean_Parser_Term_app___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_app___closed__5); l_Lean_Parser_Term_app = _init_l_Lean_Parser_Term_app(); lean_mark_persistent(l_Lean_Parser_Term_app); res = l___regBuiltinParser_Lean_Parser_Term_app(lean_io_mk_world());