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

feat: allow user to set "behavior" at declare_syntax_cat

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-01 13:28:12 -07:00
parent d69b8a79ca
commit d67c633ca1
3 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Syntax.lean
View file

@ -231,9 +231,16 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do
let catName := stx[1].getId
let catBehavior :=
if stx[2].isNone then
Parser.LeadingIdentBehavior.default
else if stx[2][3].getKind == ``Parser.Command.catBehaviorBoth then
Parser.LeadingIdentBehavior.both
else
Parser.LeadingIdentBehavior.symbol
let attrName := catName.appendAfter "Parser"
let env ← getEnv
let env ← liftIO $ Parser.registerParserCategory env attrName catName
let env ← Parser.registerParserCategory env attrName catName catBehavior
setEnv env
declareSyntaxCatQuotParser catName

3
src/Lean/Parser/Basic.lean
View file

@ -1593,8 +1593,7 @@ inductive LeadingIdentBehavior where
| default
| symbol
| both
deriving Inhabited, BEq
deriving Inhabited, BEq, Repr
/--
Each parser category is implemented using a Pratt's parser.

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

@ -71,7 +71,10 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident
def catBehaviorBoth := leading_parser nonReservedSymbol "both"
def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol"
def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")")
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident >> catBehavior
def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec
def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> termParser
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1