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

feat: allow ident, num (numeric literals) and str (string literals) as macro argument types

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 19:19:18 -08:00
parent 60a9aa52c5
commit ac2fb7e149
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Lean/Parser/Syntax.lean
View file

@ -62,8 +62,9 @@ def identPrec := parser! ident >> optPrecedence
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgSimple := parser! ident >> ":" >> ident >> optPrecedence
def macroArg := try strLitPrec <|> try macroArgSimple
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> (ident >> optPrecedence)
def macroArgSimple := parser! ident >> ":" >> macroArgType
def macroArg := try strLitPrec <|> try macroArgSimple
def macroHead := try strLitPrec <|> try identPrec
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"