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

chore: remove temporary workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-19 17:57:59 -07:00
parent e52f50b2fb
commit f0ab743ad0
3 changed files with 14 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Parser/Extension.lean
View file

@ -141,18 +141,12 @@ builtinParserCategoriesRef.set categories;
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds;
updateBuiltinTokens p.info declName
def addBuiltinLeadingParserNew (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName true p prio
def addBuiltinTrailingParserNew (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName false p prio
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) : IO Unit :=
addBuiltinParser catName declName true p 0
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) : IO Unit :=
addBuiltinParser catName declName false p 0
private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=
match e with
| ParserExtensionEntry.token tk =>
@ -379,10 +373,10 @@ match env.addAndCompile {} decl with
| Except.ok env => IO.ofExcept (setInitAttr env name)
def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParserNew catName declName prio
declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser catName declName prio
def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParserNew catName declName prio
declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser catName declName prio
def getParserPriority (args : Syntax) : Except String Nat :=
match args.getNumArgs with

14
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -141,18 +141,12 @@ builtinParserCategoriesRef.set categories;
builtinSyntaxNodeKindSetRef.modify p.info.collectKinds;
updateBuiltinTokens p.info declName
def addBuiltinLeadingParserNew (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName true p prio
def addBuiltinTrailingParserNew (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit :=
addBuiltinParser catName declName false p prio
def addBuiltinLeadingParser (catName : Name) (declName : Name) (p : Parser) : IO Unit :=
addBuiltinParser catName declName true p 0
def addBuiltinTrailingParser (catName : Name) (declName : Name) (p : TrailingParser) : IO Unit :=
addBuiltinParser catName declName false p 0
private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=
match e with
| ParserExtensionEntry.token tk =>
@ -379,10 +373,10 @@ match env.addAndCompile {} decl with
| Except.ok env => IO.ofExcept (setInitAttr env name)
def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParserNew catName declName prio
declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser catName declName prio
def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParserNew catName declName prio
declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser catName declName prio
def getParserPriority (args : Syntax) : Except String Nat :=
match args.getNumArgs with

34
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -117,7 +117,6 @@ lean_object* l_Lean_Parser_declareBuiltinParser___closed__2;
lean_object* l_Lean_Parser_registerRunParserAttributeHooksAttribute___closed__3;
extern lean_object* l_Lean_mkAppStx___closed__4;
lean_object* l___private_Lean_Parser_Extension_11__BuiltinParserAttribute_add___closed__1;
lean_object* l_Lean_Parser_addBuiltinLeadingParserNew(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_parserExtension___closed__1;
extern lean_object* l___private_Init_LeanInit_14__quoteName___main___closed__2;
extern lean_object* l_Lean_nameLitKind;
@ -270,7 +269,7 @@ lean_object* l_Lean_Parser_addTrailingParser(lean_object*, lean_object*, lean_ob
lean_object* l_List_forM___main___at___private_Lean_Parser_Extension_12__ParserAttribute_add___spec__1___closed__4;
lean_object* l_Lean_ConstantInfo_type(lean_object*);
lean_object* l_Lean_Parser_trailingNodeFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserExtension___closed__7;
lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__1;
lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*);
@ -363,11 +362,10 @@ lean_object* l_Lean_registerTagAttribute(lean_object*, lean_object*, lean_object
lean_object* l_Std_PersistentHashMap_insert___at___private_Lean_Parser_Extension_3__addParserCategoryCore___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Extension_11__BuiltinParserAttribute_add(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_parserExtension___elambda__1(lean_object*);
lean_object* l_Lean_Parser_addBuiltinTrailingParserNew(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Extension_2__throwParserCategoryAlreadyDefined___rarg___closed__2;
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*);
lean_object* l_Lean_Parser_addBuiltinTrailingParser(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_addParser___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Parser_mkBuiltinParserCategories___spec__1(lean_object*, lean_object*);
@ -2663,7 +2661,7 @@ x_8 = l_Lean_Parser_addBuiltinParser(x_1, x_2, x_7, x_4, x_5, x_6);
return x_8;
}
}
lean_object* l_Lean_Parser_addBuiltinLeadingParserNew(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
@ -2672,7 +2670,7 @@ x_7 = l_Lean_Parser_addBuiltinParser(x_1, x_2, x_6, x_3, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_Parser_addBuiltinTrailingParserNew(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Lean_Parser_addBuiltinTrailingParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
@ -2681,26 +2679,6 @@ x_7 = l_Lean_Parser_addBuiltinParser(x_1, x_2, x_6, x_3, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6; lean_object* x_7;
x_5 = 1;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Parser_addBuiltinParser(x_1, x_2, x_5, x_3, x_6, x_4);
return x_7;
}
}
lean_object* l_Lean_Parser_addBuiltinTrailingParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6; lean_object* x_7;
x_5 = 0;
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_Parser_addBuiltinParser(x_1, x_2, x_5, x_3, x_6, x_4);
return x_7;
}
}
lean_object* l___private_Lean_Parser_Extension_9__ParserExtension_addEntry(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -8141,7 +8119,7 @@ lean_object* _init_l_Lean_Parser_declareLeadingBuiltinParser___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("addBuiltinLeadingParserNew");
x_1 = lean_mk_string("addBuiltinLeadingParser");
return x_1;
}
}
@ -8168,7 +8146,7 @@ lean_object* _init_l_Lean_Parser_declareTrailingBuiltinParser___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("addBuiltinTrailingParserNew");
x_1 = lean_mk_string("addBuiltinTrailingParser");
return x_1;
}
}