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

feat: allow user to set nodeKind at syntax command

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-14 18:51:31 -08:00
parent 1e8291bf7e
commit b14c7cb69b
3 changed files with 17 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/Lean/Elab/Syntax.lean
View file

@ -98,16 +98,26 @@ fun stx => do
env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
setEnv env
private def elabKind (stx : Syntax) (catName : Name) : CommandElabM Name := do
if stx.isNone then do
env ← getEnv;
let (env, kind) := Parser.mkFreshKind env catName;
setEnv env;
pure kind
else do
let kind := stx.getIdAt 1;
currNamespace ← getCurrNamespace;
pure (currNamespace ++ kind)
@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
fun stx => do
env ← getEnv;
let cat := stx.getIdAt 3;
unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 3) ("unknown category '" ++ cat ++ "'");
let (env, kind) := Parser.mkFreshKind env cat;
setEnv env;
let cat := stx.getIdAt 4;
unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 4) ("unknown category '" ++ cat ++ "'");
kind ← elabKind (stx.getArg 1) cat;
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
type ← `(Lean.ParserDescr);
val ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 1);
val ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 2);
d ← `(@[$catParserId:ident] private def $catParserId:ident : $type := ParserDescr.node $(quote kind) $val);
trace `Elab stx $ fun _ => d;
withMacroExpansion stx $ elabCommand d

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

@ -39,7 +39,7 @@ end Syntax
namespace Command
@[builtinCommandParser] def «syntax» := parser! "syntax " >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
end Command

5
tests/lean/run/termParserAttr.lean
View file

@ -53,16 +53,13 @@ new_frontend
declare_syntax_cat foo
syntax "⟨|" term "|⟩" : foo
syntax [tst3] "FOO " foo : term
open Lean
open Lean.Parser
open Lean.Elab
open Lean.Elab.Term
def fooParser (rbp : Nat := 0) : Parser := categoryParser (mkNameSimple "foo") rbp
@[termParser] def tst3 := parser! symbol "FOO " 0 >> fooParser 0
@[termElab tst3] def elabTst3 : TermElab :=
fun stx expected? =>
elabTerm ((stx.getArg 1).getArg 1) expected?