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

chore: prepare to add optional priorities to the notation and mixfix commands

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-29 07:59:49 -08:00
parent 05fc1e8bbf
commit ee5679c77c
1 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -42,20 +42,29 @@ end Term
namespace Command
def optPrio := optional ("[" >> numLit >> "]")
def «prefix» := parser! "prefix"
def «infix» := parser! "infix"
def «infixl» := parser! "infixl"
def «infixr» := parser! "infixr"
def «postfix» := parser! "postfix"
def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> optPrecedence >> ppSpace >> strLit >> darrow >> termParser
@[builtinCommandParser] def «mixfix» := parser!
(checkOutsideQuot >> mixfixKind >> optPrecedence >> ppSpace >> strLit >> darrow >> termParser)
<|>
(checkInsideQuot >> mixfixKind >> optPrecedence >> optPrio >> ppSpace >> strLit >> darrow >> termParser)
-- NOTE: We use `suppressInsideQuot` in the following parsers because quotations inside them are evaluated in the same stage and
-- thus should be ignored when we use `checkInsideQuot` to prepare the next stage for a builtin syntax change
def identPrec := parser! ident >> optPrecedence
def optKind : Parser := optional ("[" >> ident >> "]")
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := parser! "notation" >> optPrecedence >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «notation» := parser!
(checkOutsideQuot >> "notation" >> optPrecedence >> many notationItem >> darrow >> termParser)
<|>
(checkInsideQuot >> "notation" >> optPrecedence >> optPrio >> many notationItem >> darrow >> termParser)
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (parser! "macro_rules" >> optKind >> Term.matchAlts)
def parserKind := parser! ident
def parserPrio := parser! numLit
@ -71,7 +80,6 @@ def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
def optPrio := optional ("[" >> numLit >> "]")
@[builtinCommandParser] def «macro» := parser! suppressInsideQuot ("macro " >> optPrecedence >> optPrio >> macroHead >> many macroArg >> macroTail)
@[builtinCommandParser] def «elab_rules» := parser! suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)