From 570ae2ff0e9b229deded67c87bef734d007295d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Jan 2020 18:07:14 -0800
Subject: [PATCH] feat: add `mkFreshKind`

---
 src/Init/Lean/Parser/Parser.lean | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index edfdfe0365..db0c0b6ffb 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1395,10 +1395,11 @@ inductive ParserExtensionEntry
 | parser   (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
 
 structure ParserExtensionState :=
-(tokens     : TokenTable := {})
-(kinds      : SyntaxNodeKindSet := {})
-(categories : ParserCategories := {})
-(newEntries : List ParserExtensionOleanEntry := [])
+(tokens      : TokenTable := {})
+(kinds       : SyntaxNodeKindSet := {})
+(categories  : ParserCategories := {})
+(newEntries  : List ParserExtensionOleanEntry := [])
+(nextKindIdx : Nat := 1)
 
 instance ParserExtensionState.inhabited : Inhabited ParserExtensionState := ⟨{}⟩
 
@@ -1590,6 +1591,18 @@ registerPersistentEnvExtension {
 @[init mkParserExtension]
 constant parserExtension : ParserExtension := arbitrary _
 
+partial def mkFreshKindAux (kinds : SyntaxNodeKindSet) (base : Name) : Nat → Name × Nat
+| currIdx =>
+  let candidate := base.appendIndexAfter currIdx;
+  if kinds.contains candidate then mkFreshKindAux (currIdx+1)
+  else (candidate, currIdx)
+
+def mkFreshKind (env : Environment) (part : Name) : Environment × Name :=
+let s := parserExtension.getState env;
+let (kind, idx) := mkFreshKindAux s.kinds (`_kind ++ env.mainModule ++ part) s.nextKindIdx;
+let env := parserExtension.setState env { nextKindIdx := idx+1, .. s };
+(env, kind)
+
 def isParserCategory (env : Environment) (catName : Name) : Bool :=
 (parserExtension.getState env).categories.contains catName