From 31bbc6ee6d55022e4830433b6683cc948239e988 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Aug 2020 10:12:23 -0700
Subject: [PATCH] feat: add primitive for registering syntax node kinds that
 are not associated with any parser

@Kha I added this feature to implement match expressions. The idea is
to be able to create a temporary `Syntax` node using an internal kind that has
no parser associated with it. That is, users cannot create them.
However, we can still associate an elaboration function to this kind.
Without this feature, I would have to create some "arbitrary parser"
for representing this temporary `Syntax` node.
---
 src/Lean/Parser/Parser.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index a1408d1761..8ae8368f06 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -1616,6 +1616,18 @@ def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
 def mkBuiltinSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
 @[init mkBuiltinSyntaxNodeKindSetRef] constant builtinSyntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
 
+def registerBuiltinNodeKindSet (k : SyntaxNodeKind) : IO Unit :=
+builtinSyntaxNodeKindSetRef.modify fun s => s.insert k
+
+@[init] private def registerAuxiliaryNodeKindSets : IO Unit := do
+registerBuiltinNodeKindSet choiceKind;
+registerBuiltinNodeKindSet identKind;
+registerBuiltinNodeKindSet strLitKind;
+registerBuiltinNodeKindSet numLitKind;
+registerBuiltinNodeKindSet charLitKind;
+registerBuiltinNodeKindSet nameLitKind;
+pure ()
+
 def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
 @[init mkBuiltinParserCategories] constant builtinParserCategoriesRef : IO.Ref ParserCategories := arbitrary _
 
@@ -1887,7 +1899,7 @@ parserExtension.addEntry env $ ParserExtensionEntry.kind k
 
 def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
 let kinds := (parserExtension.getState env).kinds;
-kinds.contains k || k == choiceKind || k == identKind || isLitKind k
+kinds.contains k
 
 def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind := do
 let kinds := (parserExtension.getState env).kinds;