max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-25 14:37:42 -08:00
parent 7b6caba457
commit 0d0f2f7c96
17 changed files with 11334 additions and 11220 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/Lean/Elab/TermBinders.lean
View file

@ -170,7 +170,7 @@ private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → T
getFunBinderIdsAux? true a acc
| `(_) => do ident ← mkFreshAnonymousIdent stx; pure (some (acc.push ident))
| stx =>
match stx.isSimpleTermId? with
match stx.isSimpleTermId? true with
| some id => pure (some (acc.push id))
| _ => pure none
@ -215,7 +215,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
| some idents => expandFunBindersAux body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
| none => processAsPattern ()
| binder =>
match binder.isTermId? with
match binder.isTermId? true with
| some (ident, extra) => do
unless extra.isNone $ throwError binder "invalid binder, simple identifier expected";
let type := mkHole binder;

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

@ -14,24 +14,6 @@ import Init.Lean.Message
import Init.Lean.Compiler.InitAttr
namespace Lean
namespace Syntax
def isNone (stx : Syntax) : Bool :=
stx.ifNode (fun n => n.getKind == nullKind && n.getNumArgs == 0) (fun n => false)
def getOptional? (s : Syntax) : Option Syntax :=
s.ifNode
(fun n => if n.getKind == nullKind && n.getNumArgs == 1 then some (n.getArg 0) else none)
(fun _ => none)
def getOptionalIdent? (stx : Syntax) : Option Name :=
match stx.getOptional? with
| some stx => some stx.getId
| none => none
end Syntax
namespace Parser
def isLitKind (k : SyntaxNodeKind) : Bool :=
@ -1376,12 +1358,12 @@ match stx with
| some (Syntax.ident _ _ val _) =>
if leadingIdentAsSymbol then
match map.find val with
| some as => match map.find `ident with
| some as => match map.find identKind with
| some as' => (s, as ++ as')
| _ => (s, as)
| none => find `ident
| none => find identKind
else
find `ident
find identKind
| some (Syntax.node k _) => find k
| _ => (s, [])
@ -1509,11 +1491,11 @@ node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotE
/- ===================== -/
def ident {k : ParserKind} : Parser k :=
mkAntiquot "ident" `ident <|> identNoAntiquot
mkAntiquot "ident" identKind <|> identNoAntiquot
-- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
def rawIdent {k : ParserKind} : Parser k :=
mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
mkAntiquot "ident" identKind <|> rawIdentNoAntiquot
def numLit {k : ParserKind} : Parser k :=
mkAntiquot "numLit" numLitKind <|> numLitNoAntiquot
@ -1825,7 +1807,7 @@ parserExtension.addEntry env $ ParserExtensionEntry.kind k
def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
let kinds := (parserExtension.getState env).kinds;
kinds.contains k || k == choiceKind || isLitKind k
kinds.contains k || k == choiceKind || k == identKind || isLitKind k
def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind := do
let kinds := (parserExtension.getState env).kinds;

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

@ -176,25 +176,4 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
end Term
end Parser
open Parser
def Syntax.isTermId? (stx : Syntax) : Option (Syntax × Syntax) :=
stx.ifNode
(fun node =>
if node.getKind == `Lean.Parser.Term.id && node.getNumArgs == 2 then
some (node.getArg 0, node.getArg 1)
else
none)
(fun _ => none)
def Syntax.isSimpleTermId? (stx : Syntax) : Option Syntax :=
stx.ifNode
(fun node =>
if node.getKind == `Lean.Parser.Term.id && node.getNumArgs == 2 && (node.getArg 1).isNone then
some (node.getArg 0)
else
none)
(fun _ => none)
end Lean

12
stage0/src/Init/Lean/Syntax.lean
View file

@ -92,18 +92,6 @@ match stx with
| Syntax.node k args => if k == kind then hyes ⟨Syntax.node k args, IsNode.mk k args⟩ else hno ()
| _ => hno ()
def isAtom : Syntax → Bool
| atom _ _ => true
| _ => false
def isIdent : Syntax → Bool
| ident _ _ _ _ => true
| _ => false
def getId : Syntax → Name
| ident _ _ val _ => val
| _ => Name.anonymous
def asNode : Syntax → SyntaxNode
| Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩
| _ => ⟨Syntax.node nullKind #[], IsNode.mk nullKind #[]⟩

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

@ -206,6 +206,16 @@ inductive Syntax
instance Syntax.inhabited : Inhabited Syntax :=
⟨Syntax.missing⟩
/- Builtin kinds -/
def choiceKind : SyntaxNodeKind := `choice
def nullKind : SyntaxNodeKind := `null
def identKind : SyntaxNodeKind := `ident
def strLitKind : SyntaxNodeKind := `strLit
def charLitKind : SyntaxNodeKind := `charLit
def numLitKind : SyntaxNodeKind := `numLit
def nameLitKind : SyntaxNodeKind := `nameLit
def fieldIdxKind : SyntaxNodeKind := `fieldIdx
namespace Syntax
def getKind (stx : Syntax) : SyntaxNodeKind :=
@ -216,7 +226,7 @@ match stx with
-- is compiled to ``if stx.isOfKind `ident ...``
| Syntax.missing => `missing
| Syntax.atom _ v => mkNameSimple v
| Syntax.ident _ _ _ _ => `ident
| Syntax.ident _ _ _ _ => identKind
def isOfKind : Syntax → SyntaxNodeKind → Bool
| stx, k => stx.getKind == k
@ -402,16 +412,6 @@ instance MacroM.monadQuotation : MonadQuotation MacroM :=
abbrev Macro := Syntax → MacroM Syntax
/- Builtin kinds -/
@[matchPattern] def choiceKind : SyntaxNodeKind := `choice
@[matchPattern] def nullKind : SyntaxNodeKind := `null
def strLitKind : SyntaxNodeKind := `strLit
def charLitKind : SyntaxNodeKind := `charLit
def numLitKind : SyntaxNodeKind := `numLit
def nameLitKind : SyntaxNodeKind := `nameLit
def fieldIdxKind : SyntaxNodeKind := `fieldIdx
/- Helper functions for processing Syntax programmatically -/
/--
@ -700,6 +700,56 @@ match stx.isStrLit? with
def termIdToAntiquot (var : Syntax) (catName : String) : Syntax :=
Syntax.node `Lean.Parser.antiquot #[mkAtomFrom var "$", var, mkAtomFrom var ":", mkAtomFrom var catName, mkNullNode]
def isAtom : Syntax → Bool
| atom _ _ => true
| _ => false
def isIdent : Syntax → Bool
| ident _ _ _ _ => true
| _ => false
def getId : Syntax → Name
| ident _ _ val _ => val
| _ => Name.anonymous
def isNone (stx : Syntax) : Bool :=
match stx with
| Syntax.node k args => k == nullKind && args.size == 0
| _ => false
def getOptional? (stx : Syntax) : Option Syntax :=
match stx with
| Syntax.node k args => if k == nullKind && args.size == 1 then some (args.get! 0) else none
| _ => none
def getOptionalIdent? (stx : Syntax) : Option Name :=
match stx.getOptional? with
| some stx => some stx.getId
| none => none
/--
Return `some (id, opt)` if `stx` is a Lean term id.
The `Lean.Parser.Term.id` parser is `ident >> optional (explicitUniv <|> namedPattern)`.
If `relaxed == true` and `stx` is a raw identifier `<id>`, it returns `some (<id>, noneStx)`.
This feature is useful when we want to implement elaboration functions and macros
that have support for raw identifiers where a term is expected. -/
def isTermId? (stx : Syntax) (relaxed : Bool := false) : Option (Syntax × Syntax) :=
match stx with
| Syntax.node k args =>
if k == `Lean.Parser.Term.id && args.size == 2 then
some (args.get! 0, args.get! 1)
else
none
| id@(Syntax.ident _ _ _ _) => if relaxed then some (id, mkNullNode) else none
| _ => none
/-- Similar to `isTermId?`, but succeeds only if the optional part is a `none`. -/
def isSimpleTermId? (stx : Syntax) (relaxed : Bool := false) : Option Syntax :=
match stx.isTermId? relaxed with
| some (id, opt) => if opt.isNone then some id else none
| none => none
end Syntax
end Lean

4
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -82,6 +82,7 @@ lean_object* l_Lean_Elab_Term_elabAnoymousCtor___closed__14;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabShow___closed__2;
lean_object* l_Lean_Elab_Term_elabDollar___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_seqLeft___elambda__1___closed__1;
extern lean_object* l_Lean_identKind___closed__2;
lean_object* l_Lean_Elab_Term_elabseqLeft___closed__3;
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAnd(lean_object*);
@ -210,7 +211,6 @@ lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__21;
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHave___closed__2;
extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__2;
extern lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__1;
@ -791,7 +791,7 @@ else
{
lean_object* x_17; lean_object* x_18; uint8_t x_19; uint8_t x_20;
x_17 = l_Lean_Syntax_getArg(x_13, x_12);
x_18 = l_Lean_Syntax_getKind___closed__4;
x_18 = l_Lean_identKind___closed__2;
lean_inc(x_17);
x_19 = l_Lean_Syntax_isOfKind(x_17, x_18);
x_20 = l_coeDecidableEq(x_19);

4
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -75,6 +75,7 @@ lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_commandElabAttribute;
lean_object* l_Lean_Elab_Command_elabUniverse(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__2;
lean_object* l_Lean_Elab_Command_withNamespace___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
lean_object* l___private_Init_Lean_Elab_Command_10__toCommandResult(lean_object*, lean_object*);
@ -198,7 +199,6 @@ lean_object* l_Lean_Elab_Command_mkBuiltinCommandElabTable(lean_object*);
lean_object* l_Lean_Elab_Command_addOpenDecl(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariables___closed__3;
extern lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__9;
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSynth___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -9304,7 +9304,7 @@ lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; uint8_t x
x_44 = lean_unsigned_to_nat(0u);
x_45 = l_Lean_Syntax_getArg(x_9, x_44);
lean_dec(x_9);
x_46 = l_Lean_Syntax_getKind___closed__4;
x_46 = l_Lean_identKind___closed__2;
lean_inc(x_45);
x_47 = l_Lean_Syntax_isOfKind(x_45, x_46);
x_48 = l_coeDecidableEq(x_47);

6
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

@ -53,6 +53,7 @@ extern lean_object* l_Lean_nameToExprAux___main___closed__2;
lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__2___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_13__toPreterm___main___lambda__2___closed__1;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__26;
extern lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices___main(lean_object*);
lean_object* l_Array_eraseIdx___rarg(lean_object*, lean_object*);
@ -506,7 +507,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed
extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4;
lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_13__toPreterm___main___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___spec__1___closed__1;
extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_13__toPreterm___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_findMAux___main___at___private_Init_Lean_Elab_Quotation_4__elimAntiquotChoices___main___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Init_Lean_Elab_Quotation_10__getPatternVarsAux___main___spec__1(lean_object*);
@ -2398,7 +2398,7 @@ _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__14;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2408,7 +2408,7 @@ _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__16;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

12
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -56,6 +56,7 @@ lean_object* l_unreachable_x21___rarg(lean_object*);
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__26;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
extern lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__92;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Command_expandNotation___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__1;
@ -71,6 +72,7 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabReserve___closed__1
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__3;
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__2;
lean_object* l_Lean_Elab_Command_elabMacroRules___lambda__1___closed__37;
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
extern lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
@ -174,7 +176,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__100;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__53;
lean_object* l_Lean_Elab_Command_expandMacroHeadIntoPattern(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_toParserDescrAux___main___spec__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__42;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__112;
lean_object* l_Lean_Elab_Command_elabMacroRules___lambda__1___closed__2;
@ -451,7 +452,6 @@ lean_object* l_Lean_Elab_Command_setEnv(lean_object*, lean_object*, lean_object*
extern lean_object* l___private_Init_Lean_Elab_Term_5__expandCDot___closed__4;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Syntax_7__antiquote___main___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabReserve___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat___closed__3;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__130;
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__9;
@ -1837,7 +1837,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__4;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1847,7 +1847,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__mkParserSeq___spec__1___closed__6;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -11239,7 +11239,7 @@ else
lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17; uint8_t x_18;
x_14 = lean_unsigned_to_nat(0u);
x_15 = l_Lean_Syntax_getArg(x_2, x_14);
x_16 = l_Lean_Syntax_getKind___closed__4;
x_16 = l_Lean_identKind___closed__2;
lean_inc(x_15);
x_17 = l_Lean_Syntax_isOfKind(x_15, x_16);
x_18 = l_coeDecidableEq(x_17);
@ -12466,7 +12466,7 @@ lean_object* x_15; lean_object* x_16; uint8_t x_17;
lean_dec(x_1);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
x_16 = l_Lean_Syntax_getKind___closed__3;
x_16 = l_Lean_identKind___closed__1;
x_17 = lean_string_dec_eq(x_15, x_16);
if (x_17 == 0)
{

6
stage0/stdlib/Init/Lean/Elab/TermApp.c
View file

@ -50,6 +50,7 @@ extern lean_object* l_Option_get_x21___rarg___closed__3;
lean_object* l___private_Init_Lean_Elab_TermApp_20__regTraceClasses(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__2;
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__2;
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__7;
@ -119,7 +120,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_4__elabAppArgsAux___boxed(lean_o
extern lean_object* l_Array_HasRepr___rarg___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayRef___closed__1;
lean_object* l_Lean_Elab_Term_elabLevel(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* l___private_Init_Lean_Elab_TermApp_3__elabArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__3;
@ -6461,7 +6461,7 @@ x_209 = l_coeDecidableEq(x_208);
if (x_209 == 0)
{
lean_object* x_210; uint8_t x_211; uint8_t x_212;
x_210 = l_Lean_Syntax_getKind___closed__4;
x_210 = l_Lean_identKind___closed__2;
lean_inc(x_206);
x_211 = l_Lean_Syntax_isOfKind(x_206, x_210);
x_212 = l_coeDecidableEq(x_211);
@ -7501,7 +7501,7 @@ else
lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73; uint8_t x_74;
x_70 = lean_unsigned_to_nat(0u);
x_71 = l_Lean_Syntax_getArg(x_2, x_70);
x_72 = l_Lean_Syntax_getKind___closed__4;
x_72 = l_Lean_identKind___closed__2;
lean_inc(x_71);
x_73 = l_Lean_Syntax_isOfKind(x_71, x_72);
x_74 = l_coeDecidableEq(x_73);

21018
stage0/stdlib/Init/Lean/Elab/TermBinders.c
View file

File diff suppressed because it is too large Load diff

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

@ -24,6 +24,7 @@ extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Parser_Level_paren___closed__2;
lean_object* l_Lean_Parser_Level_num___closed__2;
lean_object* l_Lean_Parser_Level_num___elambda__1___closed__2;
extern lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_Parser_Level_num___closed__4;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__6;
lean_object* l_Lean_Parser_regBuiltinLevelParserAttr(lean_object*);
@ -151,7 +152,6 @@ lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Level_max___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Level_ident(lean_object*);
lean_object* l_Lean_Parser_Level_addLit;
extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l_Lean_Parser_mkAntiquot(uint8_t, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__5;
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__7;
@ -1840,7 +1840,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__2;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -1860,7 +1860,7 @@ _start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = l_Lean_Parser_Level_ident___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);

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

@ -94,11 +94,11 @@ lean_object* l_Lean_Parser_strLitNoAntiquot(uint8_t);
lean_object* l_Lean_Parser_octalNumberFn___closed__1;
lean_object* l_Lean_Parser_many1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_many(uint8_t, lean_object*);
extern lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_Parser_FirstTokens_toStr(lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Array_foldSepBy___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_checkLeadingFn(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_fieldIdxKind___closed__2;
lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
lean_object* l_Lean_Parser_strAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_rawCh___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_rawFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -406,7 +406,6 @@ lean_object* l_Lean_Parser_identNoAntiquot___closed__1;
lean_object* l_Lean_Parser_ParserState_setPos(lean_object*, lean_object*);
lean_object* l_Lean_Parser_quotedSymbol___elambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_mkTokenAndFixPos___closed__1;
extern lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg(lean_object*);
lean_object* l_Lean_Parser_strLitFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserAttributeImpl___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
@ -586,7 +585,6 @@ lean_object* l_IO_ofExcept___at___private_Init_Lean_Parser_Parser_18__addBuiltin
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_chFn___spec__1(uint32_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Parser_rawCh___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_getNext___boxed(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Parser_Parser_17__addParserCategoryCore___spec__6(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -798,6 +796,7 @@ lean_object* l_Lean_Parser_tryFn___boxed(lean_object*);
lean_object* l_Array_foldSepByM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_nonReservedSymbol___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserExtension___closed__3;
extern lean_object* l_Lean_identKind;
lean_object* l_Lean_Parser_ParserState_mkErrorAt(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_fieldIdxFn___closed__1;
lean_object* l_Lean_Parser_ident___elambda__1(uint8_t);
@ -899,7 +898,6 @@ lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_binNumberFn___spec__2(le
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4;
lean_object* l_Lean_Parser_TokenConfig_toStr(lean_object*);
lean_object* l_Lean_Parser_numLitFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getOptionalIdent_x3f(lean_object*);
lean_object* l_Lean_Parser_fieldIdx___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Fn(uint8_t, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_octalNumberFn___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -992,7 +990,6 @@ lean_object* l_String_trim(lean_object*);
lean_object* l_RBNode_find___main___at_Lean_Parser_indexed___spec__1___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_forSepArgsM___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_rawFn(uint8_t);
lean_object* l_Lean_Syntax_getOptionalIdent_x3f___boxed(lean_object*);
lean_object* l_Lean_Parser_charLitFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_compileParserDescr___main(lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Parser_regBuiltinTermParserAttr(lean_object*);
@ -1012,7 +1009,6 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkLongestNodeAlt(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Parser_Parser_28__ParserAttribute_add___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isNone___boxed(lean_object*);
lean_object* l_Lean_Parser_currLbp(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserOfConstant(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeWhile1Fn(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1035,7 +1031,6 @@ lean_object* l_Lean_Parser_numLit___elambda__1___rarg(lean_object*, lean_object*
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkParserExtension___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_Parser_getSyntaxNodeKinds(lean_object*);
lean_object* l_Lean_Parser_addBuiltinTrailingParser(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l_Lean_Parser_nameLitFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkCategoryParserFnExtension___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_string2basic(uint8_t, lean_object*);
@ -1065,7 +1060,6 @@ extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Parser_Parser_inhabited___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgsM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_chFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object*);
lean_object* l_PersistentHashMap_foldlM___at___private_Init_Lean_Parser_Parser_28__ParserAttribute_add___spec__2(lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Syntax_foldSepRevArgsM___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_sepBy1Info___elambda__2(lean_object*, lean_object*, lean_object*);
@ -1234,156 +1228,6 @@ uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__1;
lean_object* l_Lean_Parser_ParserFn_inhabited___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_andthenFn(uint8_t);
uint8_t l_Lean_Syntax_isNone(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = l_Lean_nullKind;
x_5 = lean_name_eq(x_2, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = 0;
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_array_get_size(x_3);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_eq(x_7, x_8);
lean_dec(x_7);
return x_9;
}
}
else
{
uint8_t x_10;
x_10 = 0;
return x_10;
}
}
}
lean_object* l_Lean_Syntax_isNone___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Syntax_isNone(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Syntax_getOptional_x3f(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = l_Lean_nullKind;
x_5 = lean_name_eq(x_2, x_4);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_array_get_size(x_3);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_dec_eq(x_7, x_8);
lean_dec(x_7);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_box(0);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_11 = l_Lean_Syntax_inhabited;
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_array_get(x_11, x_3, x_12);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_13);
return x_14;
}
}
}
else
{
lean_object* x_15;
x_15 = lean_box(0);
return x_15;
}
}
}
lean_object* l_Lean_Syntax_getOptional_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_getOptional_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Syntax_getOptionalIdent_x3f(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_getOptional_x3f(x_1);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
else
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_2, 0);
x_6 = l_Lean_Syntax_getId(x_5);
lean_dec(x_5);
lean_ctor_set(x_2, 0, x_6);
return x_2;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
lean_dec(x_2);
x_8 = l_Lean_Syntax_getId(x_7);
lean_dec(x_7);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_8);
return x_9;
}
}
}
}
lean_object* l_Lean_Syntax_getOptionalIdent_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_getOptionalIdent_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
uint8_t l_Lean_Parser_isLitKind(lean_object* x_1) {
_start:
{
@ -10231,7 +10075,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -12042,7 +11886,7 @@ lean_object* _init_l_Lean_Parser_identNoAntiquot___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Syntax_getKind___closed__3;
x_1 = l_Lean_identKind___closed__1;
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
return x_2;
}
@ -25181,7 +25025,7 @@ if (x_4 == 0)
{
lean_object* x_25;
lean_dec(x_18);
x_25 = l_Lean_Syntax_getKind___closed__4;
x_25 = l_Lean_identKind;
x_9 = x_25;
goto block_15;
}
@ -25196,7 +25040,7 @@ lean_dec(x_26);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28;
x_28 = l_Lean_Syntax_getKind___closed__4;
x_28 = l_Lean_identKind;
x_9 = x_28;
goto block_15;
}
@ -25207,7 +25051,7 @@ lean_dec(x_8);
x_29 = lean_ctor_get(x_27, 0);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_Lean_Syntax_getKind___closed__4;
x_30 = l_Lean_identKind;
x_31 = l_RBNode_find___main___at_Lean_Parser_indexed___spec__3___rarg(x_1, x_30);
if (lean_obj_tag(x_31) == 0)
{
@ -27296,7 +27140,7 @@ lean_object* _init_l_Lean_Parser_ident___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Syntax_getKind___closed__4;
x_1 = l_Lean_identKind;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -27306,7 +27150,7 @@ lean_object* l_Lean_Parser_ident(uint8_t x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t 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; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = l_Lean_Parser_ident___closed__1;
x_4 = 1;
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
@ -27419,7 +27263,7 @@ lean_object* l_Lean_Parser_rawIdent(uint8_t x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t 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; lean_object* x_11; lean_object* x_12;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = l_Lean_Parser_ident___closed__1;
x_4 = 1;
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
@ -36429,23 +36273,35 @@ x_7 = l_Lean_choiceKind;
x_8 = lean_name_eq(x_2, x_7);
if (x_8 == 0)
{
uint8_t x_9;
x_9 = l_Lean_Parser_isLitKind(x_2);
return x_9;
}
else
{
uint8_t x_10;
x_10 = 1;
return x_10;
}
}
else
lean_object* x_9; uint8_t x_10;
x_9 = l_Lean_identKind;
x_10 = lean_name_eq(x_2, x_9);
if (x_10 == 0)
{
uint8_t x_11;
x_11 = 1;
x_11 = l_Lean_Parser_isLitKind(x_2);
return x_11;
}
else
{
uint8_t x_12;
x_12 = 1;
return x_12;
}
}
else
{
uint8_t x_13;
x_13 = 1;
return x_13;
}
}
else
{
uint8_t x_14;
x_14 = 1;
return x_14;
}
}
}
lean_object* l_PersistentHashMap_containsAtAux___main___at_Lean_Parser_isValidSyntaxNodeKind___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

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

@ -55,6 +55,7 @@ lean_object* l_Lean_Parser_Syntax_paren___closed__6;
lean_object* l_Lean_Parser_Command_syntax___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_str___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_macroTail___elambda__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__1;
lean_object* l_Lean_Parser_maxPrec___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__3;
@ -591,7 +592,6 @@ lean_object* l_Lean_Parser_Command_macro__rules___closed__3;
lean_object* l_Lean_Parser_Command_syntaxCat___closed__4;
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__7;
lean_object* l_Lean_Parser_Syntax_char___closed__5;
extern lean_object* l_Lean_Syntax_getKind___closed__3;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_macro___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot(uint8_t, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_Command_macroTailCommand;
@ -2963,7 +2963,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -2983,7 +2983,7 @@ _start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_Syntax_getKind___closed__3;
x_2 = l_Lean_identKind___closed__1;
x_3 = l_Lean_Parser_Syntax_ident___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
@ -2994,7 +2994,7 @@ lean_object* _init_l_Lean_Parser_Syntax_ident___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Syntax_getKind___closed__3;
x_1 = l_Lean_identKind___closed__1;
x_2 = l_String_trim(x_1);
return x_2;
}

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

@ -182,7 +182,6 @@ extern lean_object* l_Lean_List_format___rarg___closed__2;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_iff___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_have___closed__2;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_do___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__4;
@ -545,7 +544,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match__syntax___
lean_object* l_Lean_Parser_Term_cdot___closed__3;
lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__3;
lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object*);
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___closed__1;
lean_object* l_Lean_Parser_Term_str___elambda__1___closed__5;
@ -743,7 +741,6 @@ lean_object* l_Lean_Parser_checkWsBeforeFn(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Parser_Term_le___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isSimpleTermId_x3f___boxed(lean_object*);
lean_object* l_Lean_Parser_Term_where___closed__9;
lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__4;
lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -802,7 +799,6 @@ lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_bnot___closed__5;
lean_object* l_Lean_Parser_Term_structInstField___elambda__1___closed__3;
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_paren___closed__4;
lean_object* l_Lean_Parser_Term_mul;
lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__1;
@ -1288,7 +1284,6 @@ lean_object* l_Lean_Parser_Term_uminus___closed__2;
lean_object* l_Lean_Parser_Term_str___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_fromTerm___closed__4;
extern lean_object* l_Lean_Syntax_inhabited;
lean_object* l_Lean_Parser_Term_matchAlt___closed__9;
lean_object* l_Lean_Parser_Term_arrayLit;
lean_object* l_Lean_Parser_Term_mul___closed__2;
@ -1396,7 +1391,6 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_listLit___closed__10;
lean_object* l_Lean_Parser_Term_inaccessible___closed__7;
lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__12;
lean_object* l_Lean_Syntax_isTermId_x3f(lean_object*);
lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_infixL(lean_object*, lean_object*);
@ -1478,7 +1472,6 @@ lean_object* l_Lean_Parser_Term_explicitUniv___closed__2;
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Term_have___closed__4;
lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__3;
lean_object* l_Lean_Syntax_isTermId_x3f___boxed(lean_object*);
lean_object* l_Lean_Parser_Term_append___elambda__1___closed__2;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_num___closed__3;
@ -1567,7 +1560,6 @@ lean_object* l_Lean_Parser_Term_parser_x21___closed__2;
lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_typeSpec___closed__4;
lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__1;
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_Parser_Term_app___closed__6;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__1;
lean_object* l_Lean_Parser_Term_dollarProj___closed__6;
@ -36933,141 +36925,6 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Syntax_isTermId_x3f(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = l_Lean_mkTermIdFromIdent___closed__2;
x_5 = lean_name_eq(x_2, x_4);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_array_get_size(x_3);
x_8 = lean_unsigned_to_nat(2u);
x_9 = lean_nat_dec_eq(x_7, x_8);
lean_dec(x_7);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_box(0);
return x_10;
}
else
{
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;
x_11 = l_Lean_Syntax_inhabited;
x_12 = lean_unsigned_to_nat(0u);
x_13 = lean_array_get(x_11, x_3, x_12);
x_14 = lean_unsigned_to_nat(1u);
x_15 = lean_array_get(x_11, x_3, x_14);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_13);
lean_ctor_set(x_16, 1, x_15);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_16);
return x_17;
}
}
}
else
{
lean_object* x_18;
x_18 = lean_box(0);
return x_18;
}
}
}
lean_object* l_Lean_Syntax_isTermId_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_isTermId_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 1)
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
x_4 = l_Lean_mkTermIdFromIdent___closed__2;
x_5 = lean_name_eq(x_2, x_4);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_array_get_size(x_3);
x_8 = lean_unsigned_to_nat(2u);
x_9 = lean_nat_dec_eq(x_7, x_8);
lean_dec(x_7);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_box(0);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_11 = l_Lean_Syntax_inhabited;
x_12 = lean_unsigned_to_nat(1u);
x_13 = lean_array_get(x_11, x_3, x_12);
x_14 = l_Lean_Syntax_isNone(x_13);
lean_dec(x_13);
if (x_14 == 0)
{
lean_object* x_15;
x_15 = lean_box(0);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_unsigned_to_nat(0u);
x_17 = lean_array_get(x_11, x_3, x_16);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
return x_18;
}
}
}
}
else
{
lean_object* x_19;
x_19 = lean_box(0);
return x_19;
}
}
}
lean_object* l_Lean_Syntax_isSimpleTermId_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_isSimpleTermId_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* initialize_Init_Lean_Parser_Parser(lean_object*);
lean_object* initialize_Init_Lean_Parser_Level(lean_object*);
static bool _G_initialized = false;

86
stage0/stdlib/Init/Lean/Syntax.c
View file

@ -28,7 +28,6 @@ lean_object* l_Lean_Syntax_modifyArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___main___closed__5;
lean_object* l_Lean_Syntax_ifNodeKind___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isAtom___boxed(lean_object*);
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailWithInfo___main___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
@ -84,7 +83,6 @@ lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, le
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId___boxed(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Syntax_formatStxAux___main___spec__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_unreachIsNodeMissing(lean_object*, lean_object*);
@ -125,7 +123,6 @@ lean_object* l_Lean_Syntax_formatStxAux___main___closed__11;
lean_object* l_Lean_SyntaxNode_getNumArgs___boxed(lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_updateTrailing___main(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isAtom(lean_object*);
lean_object* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStxAux___main___spec__2(lean_object*, lean_object*);
extern lean_object* l_Lean_Format_sbracket___closed__3;
lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*, lean_object*);
@ -202,10 +199,8 @@ lean_object* l_Lean_Syntax_formatStxAux___main___closed__7;
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint(lean_object*);
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isIdent___boxed(lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isIdent(lean_object*);
lean_object* l_Lean_SourceInfo_updateTrailing(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -793,87 +788,6 @@ lean_dec(x_2);
return x_5;
}
}
uint8_t l_Lean_Syntax_isAtom(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 2)
{
uint8_t x_2;
x_2 = 1;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 0;
return x_3;
}
}
}
lean_object* l_Lean_Syntax_isAtom___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Syntax_isAtom(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Syntax_isIdent(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 3)
{
uint8_t x_2;
x_2 = 1;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 0;
return x_3;
}
}
}
lean_object* l_Lean_Syntax_isIdent___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Syntax_isIdent(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_Syntax_getId(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 3)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 2);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
}
lean_object* l_Lean_Syntax_getId___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Syntax_getId(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Syntax_asNode(lean_object* x_1) {
_start:
{

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

File diff suppressed because it is too large Load diff