chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
17811a9286
commit
125af9134a
14 changed files with 5616 additions and 1669 deletions
|
|
@ -917,12 +917,16 @@ fun c s =>
|
|||
@[inline] def nonReservedSymbolFn (sym : String) : BasicParserFn :=
|
||||
nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")
|
||||
|
||||
def nonReservedSymbolInfo (sym : String) : ParserInfo :=
|
||||
{ firstTokens := FirstTokens.tokens [ { val := sym }, { val := "ident" } ] }
|
||||
def nonReservedSymbolInfo (sym : String) (includeIdent : Bool) : ParserInfo :=
|
||||
{ firstTokens :=
|
||||
if includeIdent then
|
||||
FirstTokens.tokens [ { val := sym }, { val := "ident" } ]
|
||||
else
|
||||
FirstTokens.tokens [ { val := sym } ] }
|
||||
|
||||
@[inline] def nonReservedSymbol {k : ParserKind} (sym : String) : Parser k :=
|
||||
@[inline] def nonReservedSymbol {k : ParserKind} (sym : String) (includeIdent := false) : Parser k :=
|
||||
let sym := sym.trim;
|
||||
{ info := nonReservedSymbolInfo sym,
|
||||
{ info := nonReservedSymbolInfo sym includeIdent,
|
||||
fn := fun _ => nonReservedSymbolFn sym }
|
||||
|
||||
partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
|
||||
|
|
@ -1242,7 +1246,7 @@ instance ParsingTables.inhabited : Inhabited ParsingTables := ⟨{}⟩
|
|||
just executes the parsers associated with the auxiliary token "ident".
|
||||
If `leadingIdentAsSymbol == true` and the leading token is an identifier `<foo>`, then `prattParser`
|
||||
combines the parsers associated with the token `<foo>` with the parsers associated with the auxiliary token "ident".
|
||||
We use this feature and a variant of the `nonReservedSymbol` parser to implement the `tactic` parsers.
|
||||
We use this feature and the `nonReservedSymbol` parser to implement the `tactic` parsers.
|
||||
We use this approach to avoid creating a reserved symbol for each builtin tactic (e.g., `apply`, `assumption`, etc.).
|
||||
That is, users may still use these symbols as identifiers (e.g., naming a function).
|
||||
-/
|
||||
|
|
@ -1252,20 +1256,6 @@ structure ParserCategory :=
|
|||
|
||||
abbrev ParserCategories := PersistentHashMap Name ParserCategory
|
||||
|
||||
def tacticSymbolInfo (sym : String) : ParserInfo :=
|
||||
{ firstTokens := FirstTokens.tokens [ { val := sym } ] }
|
||||
|
||||
/-
|
||||
Variant of `nonReservedSymbol sym` which only register this parser as a leading parser with first token `sym`.
|
||||
This parser only makes sense for categories that set `leadingIdentAsSymbol == true`, as the `tactic` category.
|
||||
|
||||
TODO: when defining convenient notation for writing new tactics, we should use `tacticSymbol` instead of `symbol`.
|
||||
-/
|
||||
@[inline] def tacticSymbol (sym : String) : Parser :=
|
||||
let sym := sym.trim;
|
||||
{ info := tacticSymbolInfo sym,
|
||||
fn := fun _ => nonReservedSymbolFn sym }
|
||||
|
||||
def currLbp (left : Syntax) (c : ParserContext) (s : ParserState) : ParserState × Nat :=
|
||||
let (s, stx) := peekToken c s;
|
||||
match stx with
|
||||
|
|
@ -1524,7 +1514,8 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
|
|||
| _, ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
|
||||
| _, ParserDescr.node k d => node k <$> compileParserDescr d
|
||||
| _, ParserDescr.symbol tk lbp => pure $ symbol tk lbp
|
||||
| ParserKind.leading, ParserDescr.tacticSymbol tk => pure $ tacticSymbol tk
|
||||
| ParserKind.leading,
|
||||
ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent
|
||||
| _, ParserDescr.unicodeSymbol tk₁ tk₂ lbp => pure $ unicodeSymbol tk₁ tk₂ lbp
|
||||
| ParserKind.leading, ParserDescr.parser catName rbp =>
|
||||
match categories.find? catName with
|
||||
|
|
@ -1818,6 +1809,20 @@ mkAntiquot "fieldIdx" `fieldIdx <|>
|
|||
{ fn := fun _ => fieldIdxFn,
|
||||
info := mkAtomicInfo "fieldIdx" }
|
||||
|
||||
/- Helper functions for defining simple parsers -/
|
||||
|
||||
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
|
||||
|
||||
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> symbol sym lbp >> termParser (lbp - 1)
|
||||
|
||||
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
|
||||
|
||||
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> symbol sym lbp >> termParser lbp
|
||||
|
||||
end Parser
|
||||
|
||||
namespace Syntax
|
||||
|
|
|
|||
|
|
@ -4,13 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
prelude
|
||||
import Init.Lean.Parser.Parser
|
||||
import Init.Lean.Parser.Command
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
@[init] def regBuiltinSyntaxParserAttr : IO Unit :=
|
||||
registerBuiltinParserAttribute `builtinSyntaxParser `syntax
|
||||
let leadingIdentAsSymbol := true;
|
||||
registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol
|
||||
|
||||
@[init] def regSyntaxParserAttribute : IO Unit :=
|
||||
registerBuiltinDynamicParserAttribute `syntaxParser `syntax
|
||||
|
|
@ -20,7 +21,28 @@ categoryParser `syntax rbp
|
|||
|
||||
namespace Syntax
|
||||
|
||||
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
|
||||
@[builtinSyntaxParser] def cat := parser! ident
|
||||
@[builtinSyntaxParser] def atom := parser! strLit
|
||||
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
|
||||
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
|
||||
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser
|
||||
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser
|
||||
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser >> syntaxParser
|
||||
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser >> syntaxParser
|
||||
|
||||
@[builtinSyntaxParser] def many := tparser! pushLeading >> symbolAux "*" none
|
||||
@[builtinSyntaxParser] def many1 := tparser! pushLeading >> symbolAux "+" none
|
||||
@[builtinSyntaxParser] def optional := tparser! pushLeading >> symbolAux "?" none
|
||||
@[builtinSyntaxParser] def orelse := tparser! infixR " <|> " 2
|
||||
|
||||
end Syntax
|
||||
|
||||
namespace Command
|
||||
|
||||
@[builtinCommandParser] def «syntax» := parser! "syntax " >> many1 syntaxParser >> " : " >> ident
|
||||
|
||||
end Command
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -24,10 +24,10 @@ sepBy1 tacticParser "; " true
|
|||
|
||||
namespace Tactic
|
||||
|
||||
@[builtinTacticParser] def «intro» := parser! tacticSymbol "intro " >> optional ident
|
||||
@[builtinTacticParser] def «intros» := parser! tacticSymbol "intros " >> many ident
|
||||
@[builtinTacticParser] def «assumption» := parser! tacticSymbol "assumption"
|
||||
@[builtinTacticParser] def «apply» := parser! tacticSymbol "apply " >> termParser
|
||||
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident
|
||||
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident
|
||||
@[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
|
||||
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
|
||||
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
|
||||
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
|
||||
@[builtinTacticParser] def orelse := tparser! infixR " <|> " 2
|
||||
|
|
|
|||
|
|
@ -9,20 +9,6 @@ import Init.Lean.Parser.Level
|
|||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
/- Helper functions for defining simple parsers -/
|
||||
|
||||
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
|
||||
|
||||
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> symbol sym lbp >> termParser (lbp - 1)
|
||||
|
||||
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
|
||||
|
||||
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
|
||||
pushLeading >> symbol sym lbp >> termParser lbp
|
||||
|
||||
namespace Term
|
||||
|
||||
/- Built-in parsers -/
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ inductive ParserDescrCore : ParserKind → Type
|
|||
| node {k : ParserKind} : Name → ParserDescrCore k → ParserDescrCore k
|
||||
| symbol {k : ParserKind} : String → Nat → ParserDescrCore k
|
||||
| unicodeSymbol {k : ParserKind} : String → String → Nat → ParserDescrCore k
|
||||
| tacticSymbol : String → ParserDescrCore ParserKind.leading
|
||||
| nonReservedSymbol : String → Bool → ParserDescrCore ParserKind.leading
|
||||
| pushLeading : ParserDescrCore ParserKind.trailing
|
||||
| parser : Name → Nat → ParserDescrCore ParserKind.leading
|
||||
|
||||
|
|
@ -62,7 +62,7 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
|
|||
@[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
|
||||
@[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
|
||||
@[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
|
||||
@[matchPattern] abbrev ParserDescr.tacticSymbol := @ParserDescrCore.tacticSymbol
|
||||
@[matchPattern] abbrev ParserDescr.nonReservedSymbol := @ParserDescrCore.nonReservedSymbol
|
||||
@[matchPattern] abbrev ParserDescr.unicodeSymbol := @ParserDescrCore.unicodeSymbol
|
||||
@[matchPattern] abbrev ParserDescr.pushLeading := @ParserDescrCore.pushLeading
|
||||
@[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ lean_object* l_Lean_Elab_Term_elabAdd___boxed(lean_object*, lean_object*, lean_o
|
|||
lean_object* l_Lean_Elab_Term_elabShow___lambda__1___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabseqLeft___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabBind___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabShow___closed__1;
|
||||
lean_object* l_Lean_extractMacroScopes(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabAdd___closed__1;
|
||||
|
|
@ -105,7 +104,7 @@ lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__6;
|
|||
lean_object* l_Lean_Elab_Term_elabHave___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv___closed__1;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAdd(lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_andM___elambda__1___closed__1;
|
||||
|
|
@ -129,6 +128,7 @@ extern lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2;
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__1;
|
||||
lean_object* lean_array_get_size(lean_object*);
|
||||
|
|
@ -217,6 +217,7 @@ lean_object* l_Lean_Elab_Term_elabseq___closed__2;
|
|||
extern lean_object* l_Lean_Parser_Term_band___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqRight___closed__3;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
|
||||
extern lean_object* l_Lean_Parser_Term_id___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSub(lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__2;
|
||||
|
|
@ -278,7 +279,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv___closed__3;
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__35;
|
||||
lean_object* l_Lean_Elab_Term_elabMapRev___closed__1;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__7;
|
||||
|
|
@ -322,6 +322,7 @@ extern lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__2;
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabLE(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabDollar___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
|
||||
lean_object* l_Lean_Elab_Term_elabOr___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabMap___closed__3;
|
||||
|
|
@ -459,7 +460,6 @@ extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_append___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMul(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
|
||||
lean_object* l_Lean_Elab_Term_elabGE___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__10;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__2;
|
||||
|
|
@ -542,13 +542,13 @@ lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_elabCons(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabMod(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAnoymousCtor___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__10;
|
||||
lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__5;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
lean_object* l_Lean_Elab_Term_elabIf___lambda__1___closed__9;
|
||||
lean_object* l_Lean_Elab_Term_elabBEq___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLT___closed__2;
|
||||
|
|
@ -1392,9 +1392,9 @@ x_117 = lean_array_push(x_116, x_98);
|
|||
x_118 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_118, 0, x_69);
|
||||
lean_ctor_set(x_118, 1, x_117);
|
||||
x_119 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_119 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_120 = lean_array_push(x_119, x_118);
|
||||
x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_122 = lean_array_push(x_120, x_121);
|
||||
x_123 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_124 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -1478,9 +1478,9 @@ x_167 = lean_array_push(x_166, x_148);
|
|||
x_168 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_168, 0, x_69);
|
||||
lean_ctor_set(x_168, 1, x_167);
|
||||
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_170 = lean_array_push(x_169, x_168);
|
||||
x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_172 = lean_array_push(x_170, x_171);
|
||||
x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_174 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -1830,9 +1830,9 @@ x_36 = l_Lean_nullKind___closed__2;
|
|||
x_37 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_37, 0, x_36);
|
||||
lean_ctor_set(x_37, 1, x_35);
|
||||
x_38 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_38 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_39 = lean_array_push(x_38, x_37);
|
||||
x_40 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_40 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_41 = lean_array_push(x_39, x_40);
|
||||
x_42 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_43 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -1903,9 +1903,9 @@ x_80 = l_Lean_nullKind___closed__2;
|
|||
x_81 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_81, 0, x_80);
|
||||
lean_ctor_set(x_81, 1, x_79);
|
||||
x_82 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_82 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_83 = lean_array_push(x_82, x_81);
|
||||
x_84 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_84 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_85 = lean_array_push(x_83, x_84);
|
||||
x_86 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_87 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2063,9 +2063,9 @@ x_149 = lean_array_push(x_142, x_148);
|
|||
x_150 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_150, 0, x_108);
|
||||
lean_ctor_set(x_150, 1, x_149);
|
||||
x_151 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_151 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_152 = lean_array_push(x_151, x_150);
|
||||
x_153 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_153 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_154 = lean_array_push(x_152, x_153);
|
||||
x_155 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_156 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2144,9 +2144,9 @@ x_197 = lean_array_push(x_190, x_196);
|
|||
x_198 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_198, 0, x_108);
|
||||
lean_ctor_set(x_198, 1, x_197);
|
||||
x_199 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_199 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_200 = lean_array_push(x_199, x_198);
|
||||
x_201 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_201 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_202 = lean_array_push(x_200, x_201);
|
||||
x_203 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_204 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2842,9 +2842,9 @@ x_29 = lean_array_push(x_21, x_28);
|
|||
x_30 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_30, 0, x_27);
|
||||
lean_ctor_set(x_30, 1, x_29);
|
||||
x_31 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_31 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_32 = lean_array_push(x_31, x_30);
|
||||
x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_34 = lean_array_push(x_32, x_33);
|
||||
x_35 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_36 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2907,9 +2907,9 @@ x_67 = lean_array_push(x_59, x_66);
|
|||
x_68 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_68, 0, x_65);
|
||||
lean_ctor_set(x_68, 1, x_67);
|
||||
x_69 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_69 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_70 = lean_array_push(x_69, x_68);
|
||||
x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_72 = lean_array_push(x_70, x_71);
|
||||
x_73 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_74 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3173,9 +3173,9 @@ x_37 = lean_array_push(x_29, x_36);
|
|||
x_38 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_35);
|
||||
lean_ctor_set(x_38, 1, x_37);
|
||||
x_39 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_39 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_40 = lean_array_push(x_39, x_38);
|
||||
x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_42 = lean_array_push(x_40, x_41);
|
||||
x_43 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_44 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3237,9 +3237,9 @@ x_75 = lean_array_push(x_67, x_74);
|
|||
x_76 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_76, 0, x_73);
|
||||
lean_ctor_set(x_76, 1, x_75);
|
||||
x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_78 = lean_array_push(x_77, x_76);
|
||||
x_79 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_79 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_80 = lean_array_push(x_78, x_79);
|
||||
x_81 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_82 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3344,9 +3344,9 @@ x_129 = lean_array_push(x_121, x_128);
|
|||
x_130 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_130, 0, x_127);
|
||||
lean_ctor_set(x_130, 1, x_129);
|
||||
x_131 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_131 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_132 = lean_array_push(x_131, x_130);
|
||||
x_133 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_133 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_134 = lean_array_push(x_132, x_133);
|
||||
x_135 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_136 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3408,9 +3408,9 @@ x_167 = lean_array_push(x_159, x_166);
|
|||
x_168 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_168, 0, x_165);
|
||||
lean_ctor_set(x_168, 1, x_167);
|
||||
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_169 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_170 = lean_array_push(x_169, x_168);
|
||||
x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_172 = lean_array_push(x_170, x_171);
|
||||
x_173 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_174 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3556,9 +3556,9 @@ x_236 = lean_array_push(x_229, x_235);
|
|||
x_237 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_237, 0, x_204);
|
||||
lean_ctor_set(x_237, 1, x_236);
|
||||
x_238 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_238 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_239 = lean_array_push(x_238, x_237);
|
||||
x_240 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_240 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_241 = lean_array_push(x_239, x_240);
|
||||
x_242 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_243 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3619,9 +3619,9 @@ x_273 = lean_array_push(x_266, x_272);
|
|||
x_274 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_274, 0, x_204);
|
||||
lean_ctor_set(x_274, 1, x_273);
|
||||
x_275 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_275 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_276 = lean_array_push(x_275, x_274);
|
||||
x_277 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_277 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_278 = lean_array_push(x_276, x_277);
|
||||
x_279 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_280 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3726,9 +3726,9 @@ x_327 = lean_array_push(x_320, x_326);
|
|||
x_328 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_328, 0, x_204);
|
||||
lean_ctor_set(x_328, 1, x_327);
|
||||
x_329 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_329 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_330 = lean_array_push(x_329, x_328);
|
||||
x_331 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_331 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_332 = lean_array_push(x_330, x_331);
|
||||
x_333 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_334 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3789,9 +3789,9 @@ x_364 = lean_array_push(x_357, x_363);
|
|||
x_365 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_365, 0, x_204);
|
||||
lean_ctor_set(x_365, 1, x_364);
|
||||
x_366 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_366 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_367 = lean_array_push(x_366, x_365);
|
||||
x_368 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_368 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_369 = lean_array_push(x_367, x_368);
|
||||
x_370 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_371 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -4428,7 +4428,7 @@ lean_object* _init_l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__33() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__35;
|
||||
x_1 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
|
||||
x_2 = l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__29;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -4633,10 +4633,10 @@ x_72 = lean_alloc_ctor(1, 2, 0);
|
|||
lean_ctor_set(x_72, 0, x_44);
|
||||
lean_ctor_set(x_72, 1, x_71);
|
||||
x_73 = lean_array_push(x_36, x_72);
|
||||
x_74 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
|
||||
x_74 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
|
||||
x_75 = lean_name_mk_numeral(x_74, x_52);
|
||||
x_76 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
|
||||
x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38;
|
||||
x_76 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
|
||||
x_77 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
|
||||
x_78 = lean_alloc_ctor(3, 4, 0);
|
||||
lean_ctor_set(x_78, 0, x_21);
|
||||
lean_ctor_set(x_78, 1, x_76);
|
||||
|
|
@ -4657,9 +4657,9 @@ x_86 = l_Lean_nullKind___closed__2;
|
|||
x_87 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_87, 0, x_86);
|
||||
lean_ctor_set(x_87, 1, x_85);
|
||||
x_88 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_88 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_89 = lean_array_push(x_88, x_87);
|
||||
x_90 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_90 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_91 = lean_array_push(x_89, x_90);
|
||||
x_92 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_93 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -4722,10 +4722,10 @@ x_120 = lean_alloc_ctor(1, 2, 0);
|
|||
lean_ctor_set(x_120, 0, x_44);
|
||||
lean_ctor_set(x_120, 1, x_119);
|
||||
x_121 = lean_array_push(x_36, x_120);
|
||||
x_122 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__33;
|
||||
x_122 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
|
||||
x_123 = lean_name_mk_numeral(x_122, x_99);
|
||||
x_124 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__32;
|
||||
x_125 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__38;
|
||||
x_124 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__30;
|
||||
x_125 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__36;
|
||||
x_126 = lean_alloc_ctor(3, 4, 0);
|
||||
lean_ctor_set(x_126, 0, x_21);
|
||||
lean_ctor_set(x_126, 1, x_124);
|
||||
|
|
@ -4746,9 +4746,9 @@ x_134 = l_Lean_nullKind___closed__2;
|
|||
x_135 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_135, 0, x_134);
|
||||
lean_ctor_set(x_135, 1, x_133);
|
||||
x_136 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_136 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_137 = lean_array_push(x_136, x_135);
|
||||
x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_139 = lean_array_push(x_137, x_138);
|
||||
x_140 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_141 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -4841,9 +4841,9 @@ x_185 = l_Lean_nullKind___closed__2;
|
|||
x_186 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_186, 0, x_185);
|
||||
lean_ctor_set(x_186, 1, x_184);
|
||||
x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_188 = lean_array_push(x_187, x_186);
|
||||
x_189 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_189 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_190 = lean_array_push(x_188, x_189);
|
||||
x_191 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_192 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -4945,9 +4945,9 @@ x_242 = l_Lean_nullKind___closed__2;
|
|||
x_243 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_243, 0, x_242);
|
||||
lean_ctor_set(x_243, 1, x_241);
|
||||
x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__58;
|
||||
x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__56;
|
||||
x_245 = lean_array_push(x_244, x_243);
|
||||
x_246 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__66;
|
||||
x_246 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
|
||||
x_247 = lean_array_push(x_245, x_246);
|
||||
x_248 = l_Lean_Parser_Term_paren___elambda__1___closed__1;
|
||||
x_249 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -509,7 +509,7 @@ lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__7;
|
|||
lean_object* l_Lean_Parser_Command_prefix___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
|
||||
lean_object* l_Lean_Parser_Command_example___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_declId___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_declModifiers___closed__15;
|
||||
|
|
@ -21685,19 +21685,21 @@ return x_3;
|
|||
lean_object* _init_l_Lean_Parser_Command_set__option___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Command_set__option___elambda__1___closed__7;
|
||||
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Command_set__option___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Command_set__option___elambda__1___closed__8;
|
||||
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Command_set__option___closed__4() {
|
||||
|
|
@ -26205,10 +26207,11 @@ return x_22;
|
|||
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Command_maxPrec___elambda__1___closed__5;
|
||||
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Command_maxPrec___closed__2() {
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
|
||||
lean_object* l_Lean_Parser_Level_paren;
|
||||
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Level_paren___closed__10;
|
||||
|
|
@ -1017,10 +1017,11 @@ return x_41;
|
|||
lean_object* _init_l_Lean_Parser_Level_max___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Level_max___elambda__1___closed__5;
|
||||
x_2 = l_Lean_Parser_nonReservedSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Level_max___closed__2() {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -94,6 +94,7 @@ lean_object* l_Lean_Parser_tacticSeq___closed__1;
|
|||
lean_object* l_Lean_Parser_Tactic_apply___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_intros(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__12;
|
||||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__6;
|
||||
|
|
@ -142,7 +143,6 @@ lean_object* l_Lean_Parser_tacticSeq(uint8_t);
|
|||
lean_object* l_Lean_Parser_Tactic_intros___closed__4;
|
||||
lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_tacticSymbolInfo(lean_object*);
|
||||
extern lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___closed__2;
|
||||
|
|
@ -616,10 +616,11 @@ return x_48;
|
|||
lean_object* _init_l_Lean_Parser_Tactic_intro___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_intro___elambda__1___closed__8;
|
||||
x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_intro___closed__2() {
|
||||
|
|
@ -885,10 +886,11 @@ return x_34;
|
|||
lean_object* _init_l_Lean_Parser_Tactic_intros___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_intros___elambda__1___closed__6;
|
||||
x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_intros___closed__2() {
|
||||
|
|
@ -1110,10 +1112,11 @@ return x_22;
|
|||
lean_object* _init_l_Lean_Parser_Tactic_assumption___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_assumption___elambda__1___closed__5;
|
||||
x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_assumption___closed__2() {
|
||||
|
|
@ -1343,10 +1346,11 @@ return x_29;
|
|||
lean_object* _init_l_Lean_Parser_Tactic_apply___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
lean_object* x_1; uint8_t x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
|
||||
x_2 = l_Lean_Parser_tacticSymbolInfo(x_1);
|
||||
return x_2;
|
||||
x_2 = 0;
|
||||
x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_Tactic_apply___closed__2() {
|
||||
|
|
|
|||
|
|
@ -45,7 +45,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__5;
|
|||
lean_object* l_Lean_Parser_Term_subst;
|
||||
lean_object* l_Lean_Parser_Term_quotedName___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_unicodeInfixL___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_doSeq___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_app___elambda__1___closed__1;
|
||||
|
|
@ -161,7 +160,6 @@ lean_object* l_Lean_Parser_Term_char___closed__3;
|
|||
lean_object* l_Lean_Parser_Term_listLit___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_match___closed__7;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Term_pow(lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__16;
|
||||
|
|
@ -343,7 +341,6 @@ lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Term_doPat___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_doId___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_infixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match__syntax___elambda__1___spec__1___closed__1;
|
||||
|
|
@ -584,11 +581,9 @@ lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__4;
|
|||
lean_object* l_Lean_Parser_Term_hole___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_fun___closed__6;
|
||||
lean_object* l_Lean_Parser_infixR___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_num___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Term_binderDefault;
|
||||
lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Term_uminus___elambda__1___closed__1;
|
||||
|
|
@ -799,7 +794,6 @@ lean_object* l_Lean_Parser_Term_orM___closed__1;
|
|||
lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_infixL___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_doElem___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_seqLeft___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1423,7 +1417,6 @@ lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Term_binderType___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_borrowed___closed__5;
|
||||
lean_object* l_Lean_Parser_Term_explicitUniv___closed__8;
|
||||
lean_object* l_Lean_Parser_unicodeInfixR___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_equiv___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_not___closed__7;
|
||||
|
|
@ -1739,7 +1732,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__12;
|
|||
lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_structInst___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_fcomp___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_where___closed__3;
|
||||
lean_object* l_Lean_Parser_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__9;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Term_gt(lean_object*);
|
||||
|
|
@ -1824,7 +1816,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_or(lean_object*);
|
|||
lean_object* l_Lean_Parser_Term_iff___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_antiquot___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_doPat___closed__5;
|
||||
lean_object* l_Lean_Parser_categoryParser___elambda__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_binderDefault___closed__3;
|
||||
|
|
@ -1915,7 +1906,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda
|
|||
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_suffices___closed__3;
|
||||
lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_infixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__8;
|
||||
|
|
@ -1928,304 +1918,6 @@ lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Term_letIdDecl___closed__6;
|
||||
lean_object* l_Lean_Parser_Term_app___closed__4;
|
||||
extern lean_object* l_Lean_Parser_mkAntiquot___closed__1;
|
||||
lean_object* l_Lean_Parser_unicodeInfixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
|
||||
x_6 = lean_ctor_get(x_4, 3);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_4);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_unicodeInfixR(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
lean_inc(x_3);
|
||||
x_4 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
x_5 = l_String_trim(x_1);
|
||||
x_6 = l_String_trim(x_2);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_7 = l_Lean_Parser_unicodeSymbolInfo(x_5, x_6, x_4);
|
||||
x_8 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeSymbolFn___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_8, 0, x_5);
|
||||
lean_closure_set(x_8, 1, x_6);
|
||||
x_9 = lean_unsigned_to_nat(1u);
|
||||
x_10 = lean_nat_sub(x_3, x_9);
|
||||
lean_dec(x_3);
|
||||
x_11 = 1;
|
||||
x_12 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
|
||||
lean_inc(x_10);
|
||||
x_13 = l_Lean_Parser_categoryParser(x_11, x_12, x_10);
|
||||
x_14 = lean_ctor_get(x_13, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_13);
|
||||
x_15 = l_Lean_Parser_andthenInfo(x_7, x_14);
|
||||
x_16 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_16, 0, x_12);
|
||||
lean_closure_set(x_16, 1, x_10);
|
||||
x_17 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_17, 0, x_8);
|
||||
lean_closure_set(x_17, 1, x_16);
|
||||
x_18 = l_Lean_Parser_epsilonInfo;
|
||||
x_19 = l_Lean_Parser_andthenInfo(x_18, x_15);
|
||||
x_20 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeInfixR___elambda__1), 4, 1);
|
||||
lean_closure_set(x_20, 0, x_17);
|
||||
x_21 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_19);
|
||||
lean_ctor_set(x_21, 1, x_20);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_unicodeInfixR___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_Parser_unicodeInfixR(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixR___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
|
||||
x_6 = lean_ctor_get(x_4, 3);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_4);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixR(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; lean_object* x_10; lean_object* x_11; lean_object* x_12; 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_2);
|
||||
x_3 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_3, 0, x_2);
|
||||
x_4 = l_String_trim(x_1);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_symbolInfo(x_4, x_3);
|
||||
x_6 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
|
||||
lean_closure_set(x_6, 0, x_4);
|
||||
x_7 = lean_unsigned_to_nat(1u);
|
||||
x_8 = lean_nat_sub(x_2, x_7);
|
||||
lean_dec(x_2);
|
||||
x_9 = 1;
|
||||
x_10 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
|
||||
lean_inc(x_8);
|
||||
x_11 = l_Lean_Parser_categoryParser(x_9, x_10, x_8);
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_11);
|
||||
x_13 = l_Lean_Parser_andthenInfo(x_5, x_12);
|
||||
x_14 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_14, 0, x_10);
|
||||
lean_closure_set(x_14, 1, x_8);
|
||||
x_15 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_15, 0, x_6);
|
||||
lean_closure_set(x_15, 1, x_14);
|
||||
x_16 = l_Lean_Parser_epsilonInfo;
|
||||
x_17 = l_Lean_Parser_andthenInfo(x_16, x_13);
|
||||
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_infixR___elambda__1), 4, 1);
|
||||
lean_closure_set(x_18, 0, x_15);
|
||||
x_19 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_19, 0, x_17);
|
||||
lean_ctor_set(x_19, 1, x_18);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixR___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_infixR(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_unicodeInfixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
|
||||
x_6 = lean_ctor_get(x_4, 3);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_4);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_unicodeInfixL(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; 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_3);
|
||||
x_4 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
x_5 = l_String_trim(x_1);
|
||||
x_6 = l_String_trim(x_2);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_7 = l_Lean_Parser_unicodeSymbolInfo(x_5, x_6, x_4);
|
||||
x_8 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeSymbolFn___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_8, 0, x_5);
|
||||
lean_closure_set(x_8, 1, x_6);
|
||||
x_9 = 1;
|
||||
x_10 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
|
||||
lean_inc(x_3);
|
||||
x_11 = l_Lean_Parser_categoryParser(x_9, x_10, x_3);
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_11);
|
||||
x_13 = l_Lean_Parser_andthenInfo(x_7, x_12);
|
||||
x_14 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_14, 0, x_10);
|
||||
lean_closure_set(x_14, 1, x_3);
|
||||
x_15 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_15, 0, x_8);
|
||||
lean_closure_set(x_15, 1, x_14);
|
||||
x_16 = l_Lean_Parser_epsilonInfo;
|
||||
x_17 = l_Lean_Parser_andthenInfo(x_16, x_13);
|
||||
x_18 = lean_alloc_closure((void*)(l_Lean_Parser_unicodeInfixL___elambda__1), 4, 1);
|
||||
lean_closure_set(x_18, 0, x_15);
|
||||
x_19 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_19, 0, x_17);
|
||||
lean_ctor_set(x_19, 1, x_18);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_unicodeInfixL___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_Parser_unicodeInfixL(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixL___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_ParserState_pushSyntax(x_4, x_2);
|
||||
x_6 = lean_ctor_get(x_4, 3);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_4);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = lean_apply_3(x_1, x_2, x_3, x_5);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixL(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; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
lean_inc(x_2);
|
||||
x_3 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_3, 0, x_2);
|
||||
x_4 = l_String_trim(x_1);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Lean_Parser_symbolInfo(x_4, x_3);
|
||||
x_6 = lean_alloc_closure((void*)(l_Lean_Parser_symbolFn___rarg___boxed), 4, 1);
|
||||
lean_closure_set(x_6, 0, x_4);
|
||||
x_7 = 1;
|
||||
x_8 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
|
||||
lean_inc(x_2);
|
||||
x_9 = l_Lean_Parser_categoryParser(x_7, x_8, x_2);
|
||||
x_10 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_9);
|
||||
x_11 = l_Lean_Parser_andthenInfo(x_5, x_10);
|
||||
x_12 = lean_alloc_closure((void*)(l_Lean_Parser_categoryParser___elambda__1___rarg___boxed), 5, 2);
|
||||
lean_closure_set(x_12, 0, x_8);
|
||||
lean_closure_set(x_12, 1, x_2);
|
||||
x_13 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn___rarg), 5, 2);
|
||||
lean_closure_set(x_13, 0, x_6);
|
||||
lean_closure_set(x_13, 1, x_12);
|
||||
x_14 = l_Lean_Parser_epsilonInfo;
|
||||
x_15 = l_Lean_Parser_andthenInfo(x_14, x_11);
|
||||
x_16 = lean_alloc_closure((void*)(l_Lean_Parser_infixL___elambda__1), 4, 1);
|
||||
lean_closure_set(x_16, 0, x_13);
|
||||
x_17 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_17, 0, x_15);
|
||||
lean_ctor_set(x_17, 1, x_16);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_infixL___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_infixL(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ extern lean_object* l_String_splitAux___main___closed__1;
|
|||
lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
|
||||
lean_object* l_Lean_ParserDescr_tacticSymbol(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -35,6 +34,7 @@ lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object*, lean_object*, lean_
|
|||
lean_object* l_Lean_ParserDescr_node(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_try___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_node___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_unicodeSymbol___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -42,6 +42,7 @@ lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object*, lean_object*, lean_
|
|||
lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object*, uint8_t);
|
||||
lean_object* l_Lean_ParserDescr_sepBy1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t x_1) {
|
||||
_start:
|
||||
|
|
@ -292,13 +293,24 @@ x_5 = l_Lean_ParserDescr_symbol(x_4, x_2, x_3);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_ParserDescr_tacticSymbol(lean_object* x_1) {
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object* x_1, uint8_t x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_ctor(12, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_ctor(12, 1, 1);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3; lean_object* x_4;
|
||||
x_3 = lean_unbox(x_2);
|
||||
lean_dec(x_2);
|
||||
x_4 = l_Lean_ParserDescr_nonReservedSymbol(x_1, x_3);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue