From b14c7cb69bdc9fbada92961c93e4eee41e1bf6bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Jan 2020 18:51:31 -0800
Subject: [PATCH] feat: allow user to set nodeKind at `syntax` command

---
 src/Init/Lean/Elab/Syntax.lean     | 20 +++++++++++++++-----
 src/Init/Lean/Parser/Syntax.lean   |  2 +-
 tests/lean/run/termParserAttr.lean |  5 +----
 3 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index 2fc3197b30..86d544e464 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -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
diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean
index d3f206de5d..7d51d01982 100644
--- a/src/Init/Lean/Parser/Syntax.lean
+++ b/src/Init/Lean/Parser/Syntax.lean
@@ -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
 
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index d4e8ea94a8..1c1de4e6ee 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -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?