From 8f1345dc5375dd394f2fd1b899061a8e849ca9ab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Jun 2019 14:24:44 -0700
Subject: [PATCH] chore(library/init/lean/syntax): simplify `SyntaxNodeKind`

---
 library/init/lean/parser/parser.lean |  6 +++---
 library/init/lean/syntax.lean        | 14 +++++---------
 tests/playground/parser1.lean        |  6 +++---
 3 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 080858ea1e..87808105f7 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -458,8 +458,8 @@ def quotedCharFn : BasicParserFn
     else
       s.mkError "invalid escape sequence"
 
-def strLitKind : SyntaxNodeKind := { name := `strLit }
-def numLitKind : SyntaxNodeKind := { name := `numLit }
+def strLitKind : SyntaxNodeKind := `strLit
+def numLitKind : SyntaxNodeKind := `numLit
 
 /-- Push `(Syntax.node tk <new-atom>)` into syntax stack -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn :=
@@ -895,7 +895,7 @@ let find (n : Name) : ParserState × List α :=
 match stx with
 | some (Syntax.atom _ sym)      := find (mkSimpleName sym)
 | some (Syntax.ident _ _ _ _ _) := find `ident
-| some (Syntax.node k _ _)      := find k.name
+| some (Syntax.node k _ _)      := find k
 | _                             := (s, [])
 
 private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 3ab8ad227c..6a72fb9c8b 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -29,14 +29,10 @@ def SourceInfo.updateTrailing : SourceInfo → Substring → SourceInfo
 
 /- Node kind generation -/
 
-structure SyntaxNodeKind :=
-(name : Name)
+abbrev SyntaxNodeKind := Name
 
-instance stxKindBeq : HasBeq SyntaxNodeKind :=
-⟨λ k₁ k₂, k₁.name == k₂.name⟩
-
-@[pattern] def choiceKind : SyntaxNodeKind := ⟨`choice⟩
-@[pattern] def nullKind : SyntaxNodeKind := ⟨`null⟩
+@[pattern] def choiceKind : SyntaxNodeKind := `choice
+@[pattern] def nullKind : SyntaxNodeKind := `null
 
 /- Syntax AST -/
 
@@ -203,10 +199,10 @@ protected partial def formatStx : Syntax → Format
   format "`" ++ format val ++ scopes
 | (node kind args scopes) :=
   let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes.reverse ", ") "}" in
-  if kind.name = `Lean.Parser.noKind then
+  if kind = `Lean.Parser.noKind then
     sbracket $ scopes ++ joinSep (args.toList.map formatStx) line
   else
-    let shorterName := kind.name.replacePrefix `Lean.Parser Name.anonymous in
+    let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous in
     paren $ joinSep ((format shorterName ++ scopes) :: args.toList.map formatStx) line
 | missing := "<missing>"
 
diff --git a/tests/playground/parser1.lean b/tests/playground/parser1.lean
index 1f8e149e9d..fdf6421a39 100644
--- a/tests/playground/parser1.lean
+++ b/tests/playground/parser1.lean
@@ -5,15 +5,15 @@ open Lean.Parser
 local infixl `>>`:50 := Lean.Parser.andthen
 
 @[builtinTestParser] def pairParser : Parser :=
-node ⟨`pairKind⟩ $
+node `pairKind $
   "(" >> numLit >> "," >> 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 :=