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-11-17 13:35:01 -08:00
parent a13c036181
commit c64cc0f662
11 changed files with 3500 additions and 25809 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -45,8 +45,8 @@ private def markAsTrailingParser : ToParserDescrM Unit := set true
@[inline] private def withNotFirst {α} (x : ToParserDescrM α) : ToParserDescrM α :=
withReader (fun ctx => { ctx with first := false }) x
@[inline] private def withoutLeftRec {α} (x : ToParserDescrM α) : ToParserDescrM α :=
withReader (fun ctx => { ctx with leftRec := false }) x
@[inline] private def withNestedParser {α} (x : ToParserDescrM α) : ToParserDescrM α :=
withReader (fun ctx => { ctx with leftRec := false, first := false }) x
def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
let ctx ← read
@ -71,10 +71,10 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s
if (← checkLeftRec stx[0]) then
if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
let args := args.eraseIdx 0
let args ← args.mapIdxM fun i arg => withNotFirst $ toParserDescrAux arg
let args ← args.mapM fun arg => withNestedParser $ toParserDescrAux arg
mkParserSeq args
else
let args ← args.mapIdxM fun i arg => withNotFirst $ toParserDescrAux arg
let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) $ toParserDescrAux arg
mkParserSeq args
else if kind == choiceKind then
toParserDescrAux stx[0]
@ -83,13 +83,13 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s
else if kind == `Lean.Parser.Syntax.unary then
let aliasName := (stx[0].getId).eraseMacroScopes
liftIO $ Parser.ensureUnaryParserAlias aliasName
let d ← withoutLeftRec $ toParserDescrAux stx[2]
let d ← withNestedParser $ toParserDescrAux stx[2]
`(ParserDescr.unary $(quote aliasName) $d)
else if kind == `Lean.Parser.Syntax.binary then
let aliasName := (stx[0].getId).eraseMacroScopes
liftIO $ Parser.ensureBinaryParserAlias aliasName
let d₁ ← withoutLeftRec $ toParserDescrAux stx[2]
let d₂ ← withoutLeftRec $ toParserDescrAux stx[4]
let d₁ ← withNestedParser $ toParserDescrAux stx[2]
let d₂ ← withNestedParser $ toParserDescrAux stx[4]
`(ParserDescr.binary $(quote aliasName) $d₁ $d₂)
else if kind == `Lean.Parser.Syntax.cat then
let cat := stx[0].getId.eraseMacroScopes
@ -135,7 +135,9 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s
else if kind == `Lean.Parser.Syntax.atom then
match stx[0].isStrLit? with
| some atom =>
if (← read).leadingIdentAsSymbol then
/- For syntax categories where initialized with `leadingIdentAsSymbol` (e.g., `tactic`), we automatically mark
the first symbol as nonReserved. -/
if (← read).leadingIdentAsSymbol && (← read).first then
`(ParserDescr.nonReservedSymbol $(quote atom) false)
else
`(ParserDescr.symbol $(quote atom))

1
stage0/src/Lean/Parser/Extra.lean generated
View file

@ -72,7 +72,6 @@ macro "registerParserAlias!" aliasName:strLit declName:ident : term =>
PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
open PrettyPrinter in
builtin_initialize
registerParserAlias! "group" group
registerParserAlias! "ppHardSpace" ppHardSpace

62
stage0/src/Lean/Parser/Tactic.lean generated
View file

@ -10,70 +10,10 @@ namespace Parser
namespace Tactic
builtin_initialize
registerParserAlias! "tacticSeq" tacticSeq
registerParserAlias! "tacticSeq" tacticSeq
def ident' : Parser := ident <|> "_"
@[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> many (checkColGt >> termParser maxPrec)
@[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many (checkColGt >> ident')
@[builtinTacticParser] def «revert» := parser! nonReservedSymbol "revert " >> many1 (checkColGt >> ident)
@[builtinTacticParser] def «clear» := parser! nonReservedSymbol "clear " >> many1 (checkColGt >> ident)
@[builtinTacticParser] def «subst» := parser! nonReservedSymbol "subst " >> many1 (checkColGt >> ident)
@[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
@[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
@[builtinTacticParser] def «exact» := parser! nonReservedSymbol "exact " >> termParser
@[builtinTacticParser] def «refine» := parser! nonReservedSymbol "refine " >> termParser
@[builtinTacticParser] def «refine!» := parser! nonReservedSymbol "refine! " >> termParser
@[builtinTacticParser] def «case» := parser! nonReservedSymbol "case " >> ident >> darrow >> tacticSeq
@[builtinTacticParser] def «allGoals» := parser! nonReservedSymbol "allGoals " >> tacticSeq
@[builtinTacticParser] def «focus» := parser! nonReservedSymbol "focus " >> tacticSeq
@[builtinTacticParser] def «skip» := parser! nonReservedSymbol "skip"
@[builtinTacticParser] def «done» := parser! nonReservedSymbol "done"
@[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
@[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq
@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional (atomic (ident >> " : ")) >> termParser 51 >> " = " >> ident
@[builtinTacticParser] def «unknown» := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
def locationWildcard := parser! "*"
def locationTarget := parser! unicodeSymbol "⊢" "|-"
def locationHyp := parser! many1 (checkColGt >> ident)
def location := parser! withPosition ("at " >> (locationWildcard <|> locationTarget <|> locationHyp))
@[builtinTacticParser] def change := parser! nonReservedSymbol "change " >> termParser >> optional location
@[builtinTacticParser] def changeWith := parser! nonReservedSymbol "change " >> termParser >> " with " >> termParser >> optional location
def rwRule := parser! optional (unicodeSymbol "←" "<-") >> termParser
def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
@[builtinTacticParser] def «rewrite» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRule >> optional location
@[builtinTacticParser 1] def «rewriteSeq» := parser! (nonReservedSymbol "rewrite" <|> nonReservedSymbol "rw") >> rwRuleSeq >> optional location
def altRHS := Term.hole <|> Term.syntheticHole <|> tacticSeq
def inductionAlt : Parser := parser! ident' >> many ident' >> darrow >> altRHS
def inductionAlts : Parser := parser! withPosition ("| " >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|"))
def usingRec : Parser := optional (" using " >> ident)
def generalizingVars := optional (" generalizing " >> many1 ident)
@[builtinTacticParser] def «induction» := parser! nonReservedSymbol "induction " >> sepBy1 termParser ", " >> usingRec >> generalizingVars >> optional inductionAlts
def casesTarget := parser! optional (atomic (ident >> " : ")) >> termParser
@[builtinTacticParser] def «cases» := parser! nonReservedSymbol "cases " >> sepBy1 casesTarget ", " >> usingRec >> optional inductionAlts
def matchAlt : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS
def matchAlts : Parser := parser! withPosition $ "| " >> sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "| ")
@[builtinTacticParser] def «match» := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
@[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> matchAlts
def withIds : Parser := optional (" with " >> many1 (checkColGt >> ident'))
@[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds
@[builtinTacticParser] def paren := parser! "(" >> tacticSeq >> ")"
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
/- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/
@[builtinTacticParser] def «have» := parser! "have " >> Term.haveDecl
@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.sufficesDecl
@[builtinTacticParser] def «show» := parser! "show " >> termParser
@[builtinTacticParser] def «let» := parser! "let " >> Term.letDecl
@[builtinTacticParser] def «let!» := parser! "let! " >> Term.letDecl
@[builtinTacticParser] def «letrec» := parser! withPosition (group ("let " >> nonReservedSymbol "rec ") >> Term.letRecDecls)
end Tactic
end Parser

1
stage0/src/Lean/Parser/Term.lean generated
View file

@ -218,6 +218,7 @@ builtin_initialize
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
registerParserAlias! "matchDiscr" Term.matchDiscr
end Parser
end Lean

5515
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Lean/Parser/Command.c generated
View file

@ -58,6 +58,7 @@ lean_object* l_Lean_Parser_Command_structure_formatter(lean_object*, lean_object
lean_object* l_Lean_Parser_Command_open___closed__3;
lean_object* l_Lean_Parser_Command_printAxioms___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_structCtor___closed__8;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
lean_object* l_Lean_Parser_Command_structExplicitBinder_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_quot_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_structExplicitBinder___elambda__1___closed__5;
@ -119,7 +120,6 @@ lean_object* l_Lean_Parser_Command_open___closed__5;
lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_instance_parenthesizer___closed__5;
lean_object* l_Lean_Parser_Command_docComment___closed__3;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_mutual_formatter___closed__2;
lean_object* l_Lean_Parser_Command_structFields_parenthesizer___closed__7;
@ -1662,6 +1662,7 @@ lean_object* l_Lean_Parser_Command_attribute___closed__1;
lean_object* l_Lean_Parser_Command_structImplicitBinder_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_initialize_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Command_end___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
lean_object* l_Lean_Parser_Command_declModifiers_formatter___closed__12;
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1___closed__11;
@ -1863,7 +1864,6 @@ lean_object* l_Lean_Parser_Command_open___closed__6;
lean_object* l_Lean_Parser_Command_declModifiers___closed__12;
lean_object* l_Lean_Parser_Command_noncomputable___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_attribute___closed__8;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
extern lean_object* l_Lean_Parser_Term_letIdLhs___closed__4;
lean_object* l_Lean_Parser_Command_structureTk___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_open___elambda__1(lean_object*, lean_object*);
@ -10968,7 +10968,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_docComment_formatter___closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -11437,7 +11437,7 @@ static lean_object* _init_l_Lean_Parser_Command_declModifiers_formatter___closed
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_2 = lean_alloc_closure((void*)(l_Lean_ppDedent_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -13521,7 +13521,7 @@ static lean_object* _init_l_Lean_Parser_Command_structFields_formatter___closed_
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_2 = l_Lean_Parser_Command_structFields_formatter___closed__6;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -14073,7 +14073,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_docComment_parenthesizer___closed__2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -14480,7 +14480,7 @@ static lean_object* _init_l_Lean_Parser_Command_declModifiers_parenthesizer___cl
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_ppDedent_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -16216,7 +16216,7 @@ static lean_object* _init_l_Lean_Parser_Command_structFields_parenthesizer___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_2 = l_Lean_Parser_Command_structFields_parenthesizer___closed__6;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);

516
stage0/stdlib/Lean/Parser/Extra.c generated
View file

File diff suppressed because it is too large Load diff

20
stage0/stdlib/Lean/Parser/Module.c generated
View file

@ -15,6 +15,7 @@ extern "C" {
#endif
lean_object* lean_string_push(lean_object*, uint32_t);
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__5;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
lean_object* l_Lean_Parser_Module_header_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Module_module_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Module_module_formatter___closed__2;
@ -27,7 +28,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Parser_Module_0__Lean
lean_object* l_Lean_Parser_Module_updateTokens___closed__2;
lean_object* l___private_Lean_Parser_Module_0__Lean_Parser_testModuleParserAux_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserContext(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_prelude_parenthesizer___closed__2;
@ -235,6 +235,7 @@ extern lean_object* l_Lean_Parser_Level_ident_formatter___closed__1;
lean_object* l_Lean_Parser_parseCommand_parse(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_header___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
lean_object* l_Lean_Parser_Module_module___closed__9;
lean_object* l_Lean_Parser_Error_toString(lean_object*);
lean_object* l___private_Lean_Parser_Module_0__Lean_Parser_consumeInput_match__1(lean_object*);
@ -263,7 +264,6 @@ lean_object* l_Lean_Parser_symbolInfo(lean_object*);
lean_object* l_Lean_Parser_orelseFnCore(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__4;
lean_object* l_Lean_Parser_Module_prelude___closed__2;
lean_object* l_Lean_Parser_topLevelCommandParserFn___closed__1;
@ -1237,7 +1237,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_formatter___closed__2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1267,7 +1267,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_formatter___closed__5;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1289,7 +1289,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_formatter___closed__7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1379,7 +1379,7 @@ static lean_object* _init_l_Lean_Parser_Module_module_formatter___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__24;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__24;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_2, 0, x_1);
lean_closure_set(x_2, 1, x_1);
@ -1576,7 +1576,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_parenthesizer___closed__2;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1606,7 +1606,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_parenthesizer___closed__5;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1628,7 +1628,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Module_header_parenthesizer___closed__7;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -1688,7 +1688,7 @@ static lean_object* _init_l_Lean_Parser_Module_module_parenthesizer___closed__2(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__26;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__26;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_2, 0, x_1);
lean_closure_set(x_2, 1, x_1);

30
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -227,7 +227,6 @@ lean_object* l_Lean_Parser_Command_macroArgSimple___closed__4;
lean_object* l_Lean_Parser_Command_elab_formatter___closed__8;
extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Syntax_atom_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__18;
lean_object* l_Lean_Parser_Command_macroArgSimple_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_macroTailCommand___closed__5;
lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__10;
@ -236,6 +235,7 @@ lean_object* l_Lean_Parser_Command_parserKindPrio___elambda__1(lean_object*, lea
lean_object* l_Lean_Parser_Command_elabTail_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Command_elab__rules_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Command_elab__rules_formatter___closed__6;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__18;
lean_object* l___regBuiltinParser_Lean_Parser_Term_stx_quot(lean_object*);
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__13;
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7;
@ -288,7 +288,6 @@ lean_object* l_Lean_Parser_maxSymbol___closed__6;
lean_object* l_Lean_Parser_Command_optPrio___closed__2;
lean_object* l_Lean_Parser_Syntax_paren_parenthesizer___closed__1;
lean_object* l_Lean_Parser_atomicFn(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_elab___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Syntax_nonReserved_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Command_syntax_formatter___closed__1;
@ -668,6 +667,7 @@ lean_object* l_Lean_Parser_Command_parserKind_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_notationItem___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_stx_quot___closed__1;
lean_object* l_Lean_Parser_Command_parserKindPrio___closed__1;
extern lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_syntaxCat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_nonReserved_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_nonReserved___closed__7;
@ -741,7 +741,6 @@ lean_object* l_Lean_Parser_precedence_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_syntax_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__12;
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Syntax_paren_formatter___closed__2;
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_optKindPrio_parenthesizer___closed__1;
@ -894,7 +893,6 @@ lean_object* l___regBuiltin_Lean_Parser_Syntax_paren_parenthesizer(lean_object*)
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_optKind___elambda__1___closed__1;
lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Syntax_cat___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
@ -940,6 +938,7 @@ lean_object* l_Lean_Parser_Command_mixfixKind_parenthesizer(lean_object*, lean_o
lean_object* l_Lean_Parser_Command_infixl___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_atom_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_postfix___closed__4;
extern lean_object* l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__12;
lean_object* l_Lean_Parser_Command_notation___closed__2;
lean_object* l_Lean_Parser_precedenceLit_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1238,6 +1237,7 @@ lean_object* l_Lean_Parser_Command_elab__rules_formatter___closed__1;
lean_object* l_Lean_Parser_Command_prefix_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Syntax_atom___closed__2;
lean_object* l_Lean_Parser_precedence___closed__2;
extern lean_object* l_Lean_Parser_Command_openHiding_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Command_parserKind___closed__2;
lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_optKind___closed__3;
@ -1274,10 +1274,10 @@ lean_object* l_Lean_PrettyPrinter_Formatter_suppressInsideQuot_formatter(lean_ob
lean_object* l_Lean_Parser_Command_syntax___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_atom(lean_object*);
lean_object* l_Lean_Parser_Command_elabTail___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__20;
lean_object* l_Lean_Parser_maxSymbol___closed__4;
lean_object* l_Lean_Parser_Command_elabTail___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Syntax_cat_formatter___closed__1;
extern lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__20;
lean_object* l_Lean_Parser_Command_mixfixKind___closed__5;
lean_object* l_Lean_Parser_Command_infix_formatter___closed__2;
lean_object* l_Lean_Parser_Syntax_atom___closed__5;
@ -6390,7 +6390,7 @@ static lean_object* _init_l_Lean_Parser_Command_mixfix_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__18;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__18;
x_2 = l_Lean_Parser_Command_mixfix_formatter___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -6773,7 +6773,7 @@ static lean_object* _init_l_Lean_Parser_Command_mixfix_parenthesizer___closed__3
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__20;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__20;
x_2 = l_Lean_Parser_Command_mixfix_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -7597,7 +7597,7 @@ lean_object* l_Lean_Parser_Command_notationItem_formatter(lean_object* x_1, lean
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__18;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__18;
x_7 = l_Lean_Parser_Command_notationItem_formatter___closed__4;
x_8 = l_Lean_PrettyPrinter_Formatter_andthen_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
@ -7811,7 +7811,7 @@ lean_object* l_Lean_Parser_Command_notationItem_parenthesizer(lean_object* x_1,
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_571____closed__20;
x_6 = l_Lean_Parser_initFn____x40_Lean_Parser_Extra___hyg_567____closed__20;
x_7 = l_Lean_Parser_Command_notationItem_parenthesizer___closed__4;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
@ -8302,7 +8302,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
x_2 = l_Lean_Parser_Command_openHiding_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -9696,7 +9696,7 @@ static lean_object* _init_l_Lean_Parser_Command_parserKindPrio_parenthesizer___c
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
x_1 = l_Lean_Parser_Command_openHiding_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Level_num_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
@ -9901,7 +9901,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Syntax_paren_parenthesizer___closed__3;
x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_2 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 7, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
@ -10708,7 +10708,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_3 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
lean_closure_set(x_4, 0, x_1);
lean_closure_set(x_4, 1, x_2);
@ -13008,7 +13008,7 @@ static lean_object* _init_l_Lean_Parser_Command_macroTailDefault_parenthesizer__
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_1 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_atomic_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -13719,7 +13719,7 @@ static lean_object* _init_l_Lean_Parser_Command_elab__rules_parenthesizer___clos
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
x_1 = l_Lean_Parser_Command_namespace_parenthesizer___closed__2;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;

22520
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

File diff suppressed because it is too large Load diff

610
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff