chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
d75cd49ea2
commit
6be9a73e51
4 changed files with 364 additions and 216 deletions
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue