feat: add mkFreshKind

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