From 98879f15809bee23dd415e870e0a02728ce80ae7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2019 14:51:59 -0700
Subject: [PATCH] refactor(library/init/lean/parser/parser): simplify
 `SyntaxNodeKind`

The numeric `id` generation is works well for builtin parsers, but it
creates problems when defining dynamic ones.
---
 library/init/lean/parser/parser.lean |  7 +---
 library/init/lean/syntax.lean        | 56 ++--------------------------
 tests/playground/parser1.lean        | 18 ++-------
 3 files changed, 9 insertions(+), 72 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 7dc4d49e07..6094d1850a 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -452,11 +452,8 @@ def quotedCharFn : BasicParserFn
     else
       s.mkError "invalid escape sequence"
 
-def mkStrLitKind : IO SyntaxNodeKind := nextKind `strLit
-@[init mkStrLitKind] constant strLitKind : SyntaxNodeKind := default _
-
-def mkNumberKind : IO SyntaxNodeKind := nextKind `numLit
-@[init mkNumberKind] constant numLitKind : SyntaxNodeKind := default _
+def strLitKind : SyntaxNodeKind := { name := `strLit }
+def numLitKind : SyntaxNodeKind := { name := `numLit }
 
 /-- Push `(Syntax.node tk <new-atom>)` into syntax stack -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn :=
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 4752a68562..3ab8ad227c 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -29,48 +29,14 @@ def SourceInfo.updateTrailing : SourceInfo → Substring → SourceInfo
 
 /- Node kind generation -/
 
-def mkUniqIdRef : IO (IO.Ref Nat) :=
-IO.mkRef 0
-
-@[init mkUniqIdRef]
-constant nextUniqId : IO.Ref Nat := default _
-
 structure SyntaxNodeKind :=
-(name : Name) (id : Nat)
-
-instance stxKindInh : Inhabited SyntaxNodeKind :=
-⟨{name := default _, id := default _}⟩
+(name : Name)
 
 instance stxKindBeq : HasBeq SyntaxNodeKind :=
-⟨λ k₁ k₂, k₁.id == k₂.id⟩
+⟨λ k₁ k₂, k₁.name == k₂.name⟩
 
-def mkNameToKindTable : IO (IO.Ref (NameMap Nat)) :=
-IO.mkRef {}
-
-@[init mkNameToKindTable]
-constant nameToKindTable : IO.Ref (NameMap Nat) := default _
-
-def nextKind (k : Name) : IO SyntaxNodeKind :=
-do m ← nameToKindTable.get,
-   when (m.contains k) (throw $ IO.userError ("kind '" ++ toString k ++ "' already exists")),
-   id ← nextUniqId.get,
-   nameToKindTable.set (m.insert k id),
-   nextUniqId.set (id+1),
-   pure { name := k, id := id }
-
-/- Basic node kinds -/
-
-def mkNullKind : IO SyntaxNodeKind := nextKind `null
-@[init mkNullKind] constant nullKind : SyntaxNodeKind := default _
-def mkChoiceKind : IO SyntaxNodeKind := nextKind `choice
-@[init mkChoiceKind] constant choiceKind : SyntaxNodeKind := default _
-def mkOptionSomeKind : IO SyntaxNodeKind := nextKind `some
-@[init mkOptionSomeKind] constant optionSomeKind : SyntaxNodeKind := default _
-def mkOptionNoneKind : IO SyntaxNodeKind := nextKind `none
-@[init mkOptionNoneKind] constant optionNoneKind : SyntaxNodeKind := default _
-def mkManyKind : IO SyntaxNodeKind := nextKind `many
-@[init mkManyKind] constant manyKind : SyntaxNodeKind := default _
-def mkHoleKind : IO SyntaxNodeKind := nextKind `hole
+@[pattern] def choiceKind : SyntaxNodeKind := ⟨`choice⟩
+@[pattern] def nullKind : SyntaxNodeKind := ⟨`null⟩
 
 /- Syntax AST -/
 
@@ -87,20 +53,6 @@ def Syntax.isMissing : Syntax → Bool
 | Syntax.missing := true
 | _ := false
 
-def SyntaxNodeKind.fix : SyntaxNodeKind → IO SyntaxNodeKind
-| {name := n, ..} := do
-  m ← nameToKindTable.get,
-  match m.find n with
-  | some id := pure {name := n, id := id}
-  | none    := throw $ IO.userError ("Error unknown Syntax kind '" ++ toString n ++ "'")
-
-partial def Syntax.fixKinds : Syntax → IO Syntax
-| (Syntax.node k args scopes) := do
-  k ← k.fix,
-  args ← args.mmap Syntax.fixKinds,
-  pure (Syntax.node k args scopes)
-| other                       := pure other
-
 inductive IsNode : Syntax → Prop
 | mk (kind : SyntaxNodeKind) (args : Array Syntax) (scopes : MacroScopes) : IsNode (Syntax.node kind args scopes)
 
diff --git a/tests/playground/parser1.lean b/tests/playground/parser1.lean
index 36e38ba95d..443a259d15 100644
--- a/tests/playground/parser1.lean
+++ b/tests/playground/parser1.lean
@@ -2,30 +2,18 @@ import init.lean.parser.parser
 open Lean
 open Lean.Parser
 
-def mkPairKind : IO SyntaxNodeKind := nextKind `pair
-@[init mkPairKind]
-constant pairKind : SyntaxNodeKind := default _
-
-def mkPairsKind : IO SyntaxNodeKind := nextKind `pairs
-@[init mkPairsKind]
-constant pairsKind : SyntaxNodeKind := default _
-
-def mkFunKind : IO SyntaxNodeKind := nextKind `fun
-@[init mkFunKind]
-constant funKind : SyntaxNodeKind := default _
-
 local infixl `>>`:50 := Lean.Parser.andthen
 
 @[builtinTestParser] def pairParser : Parser :=
-node pairKind $
+node ⟨`pairKind⟩ $
   "(" >> number >> "," >> ident >> ")"
 
 @[builtinTestParser] def pairsParser : Parser :=
-node pairsKind $
+node ⟨`pairsKind⟩ $
   "{" >> sepBy1 testParser "," >> "}"
 
 @[builtinTestParser] def functionParser : Parser :=
-node funKind $
+node ⟨`funKind⟩ $
   "fun" >> ident >> "," >> testParser
 
 @[builtinTestParser] def identParser : Parser :=