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

feat(library/init/lean/parser/parser): builtin parser attributes must be applied after compilation

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-20 09:22:03 -07:00
parent e0ddacfd3e
commit 8724a8cfd5
2 changed files with 9 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/parser.lean
View file

@ -1012,7 +1012,7 @@ def registerBuiltinParserAttribute (attrName : Name) (refDeclName : Name) : IO U
registerAttribute {
name := attrName,
descr := "Builtin parser",
add := λ env declName args persistent, do
add := λ env declName args persistent, do {
unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument")),
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent")),
match env.find declName with
@ -1025,6 +1025,8 @@ registerAttribute {
declareLeadingBuiltinParser env refDeclName declName
| _ :=
throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
},
applicationTime := AttributeApplicationTime.afterCompilation
}
@[init mkBultinParsingTablesRef]

24
tests/playground/parser1.lean
View file

@ -16,39 +16,27 @@ constant funKind : SyntaxNodeKind := default _
local infixl `>>`:50 := Lean.Parser.andthen
def pairParser : Parser :=
@[builtinTestParser] def pairParser : Parser :=
node pairKind $
"(" >> number >> "," >> ident >> ")"
attribute [builtinTestParser] pairParser
def pairsParser : Parser :=
@[builtinTestParser] def pairsParser : Parser :=
node pairsKind $
"{" >> sepBy1 testParser "," >> "}"
attribute [builtinTestParser] pairsParser
def functionParser : Parser :=
@[builtinTestParser] def functionParser : Parser :=
node funKind $
"fun" >> ident >> "," >> testParser
attribute [builtinTestParser] functionParser
def identParser : Parser :=
@[builtinTestParser] def identParser : Parser :=
ident
attribute [builtinTestParser] identParser
def numParser : Parser :=
@[builtinTestParser] def numParser : Parser :=
number
attribute [builtinTestParser] numParser
def strParser : Parser :=
@[builtinTestParser] def strParser : Parser :=
strLit
attribute [builtinTestParser] strParser
def testParser (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment,