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

feat: declare quotation parser for new parsing category

Browse source 
@Kha We can now delete the command
```
@[termParser] def childStxQuot : Parser :=
checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ symbol "`(child|" >> categoryParser `child 0 >> symbol ")")
```
from the web demo.
This commit is contained in:
Leonardo de Moura 2020-06-16 10:31:13 -07:00
parent b3d2e51aff
commit 392d078011
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -154,13 +154,24 @@ end Term
namespace Command
private def getCatSuffix (catName : Name) : String :=
match catName with
| Name.str _ s _ => s
| _ => unreachable!
private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
let quotSymbol := "`(" ++ getCatSuffix catName ++ "|";
cmd ← `(@[termParser] def catStxQuot : Lean.ParserDescr := Lean.ParserDescr.node `Lean.Parser.Term.stxQuot $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) (Lean.ParserDescr.andthen (Lean.ParserDescr.parser $(quote catName) 0) (Lean.ParserDescr.symbol ")"))));
elabCommand cmd
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
fun stx => do
let catName := stx.getIdAt 1;
let attrName := catName.appendAfter "Parser";
env ← getEnv;
env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
setEnv env
setEnv env;
declareSyntaxCatQuotParser catName
def mkKindName (catName : Name) : Name :=
`_kind ++ catName