chore: remove workarounds for #1090

src/Init/Meta.lean

@@ -524,7 +524,7 @@ def decodeNatLitVal? (s : String) : Option Nat :=
     else if c.isDigit then decodeDecimalLitAux s 0 0
     else none
 
-def isLitCore? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=
+def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=
   match stx with
   | Syntax.node _ k args =>
     if k == litKind && args.size == 1 then
@@ -535,18 +535,6 @@ def isLitCore? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=
       none
   | _ => none
 
-def isLit? (litKind : SyntaxNodeKind) (stx : Syntax) : Option String :=  -- TODO remove staging hack
-  if litKind == `num || litKind == `numLit then
-    isLitCore? `num stx <|> isLitCore? `numLit stx
-  else if litKind == `str || litKind == `strLit then
-    isLitCore? `str stx <|> isLitCore? `strLit stx
-  else if litKind == `char || litKind == `charLit then
-    isLitCore? `char stx <|> isLitCore? `charLit stx
-  else if litKind == `name || litKind == `nameLit then
-    isLitCore? `name stx <|> isLitCore? `nameLit stx
-  else
-    isLitCore? litKind stx
-
 private def isNatLitAux (litKind : SyntaxNodeKind) (stx : Syntax) : Option Nat :=
   match isLit? litKind stx with
   | some val => decodeNatLitVal? val

src/Init/Prelude.lean

@@ -1873,16 +1873,8 @@ def setKind (stx : Syntax) (k : SyntaxNodeKind) : Syntax :=
   | Syntax.node info _ args => Syntax.node info k args
   | _                       => stx
 
-def isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool := -- TODO remove staging hack
-  cond (or (beq k `num) (beq k `numLit))
-    (or (beq stx.getKind `num) (beq stx.getKind `numLit))
-  (cond (or (beq k `str) (beq k `strLit))
-    (or (beq stx.getKind `str) (beq stx.getKind `strLit))
-  (cond (or (beq k `char) (beq k `charLit))
-    (or (beq stx.getKind `char) (beq stx.getKind `charLit))
-  (cond (or (beq k `name) (beq k `nameLit))
-    (or (beq stx.getKind `name) (beq stx.getKind `nameLit))
-    (beq stx.getKind k))))
+def isOfKind (stx : Syntax) (k : SyntaxNodeKind) : Bool :=
+  beq stx.getKind k
 
 def getArg (stx : Syntax) (i : Nat) : Syntax :=
   match stx with
@@ -1924,24 +1916,13 @@ def matchesNull (stx : Syntax) (n : Nat) : Bool :=
 def matchesIdent (stx : Syntax) (id : Name) : Bool :=
   and stx.isIdent (beq stx.getId id)
 
-def matchesLitCore (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool :=
+def matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool :=
   match stx with
   | Syntax.node _ k' args => and (beq k k') (match args.getD 0 Syntax.missing with
     | Syntax.atom _ val' => beq val val'
     | _                  => false)
   | _                     => false
 
-def matchesLit (stx : Syntax) (k : SyntaxNodeKind) (val : String) : Bool := -- TODO remove staging hack
-  cond (or (beq k `num) (beq k `numLit))
-    (or (matchesLitCore stx `num val) (matchesLitCore stx `numLit val))
-  (cond (or (beq k `str) (beq k `strLit))
-    (or (matchesLitCore stx `str val) (matchesLitCore stx `strLit val))
-  (cond (or (beq k `char) (beq k `charLit))
-    (or (matchesLitCore stx `char val) (matchesLitCore stx `charLit val))
-  (cond (or (beq k `name) (beq k `nameLit))
-    (or (matchesLitCore stx `name val) (matchesLitCore stx `nameLit val))
-    (matchesLitCore stx k val))))
-
 def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
   match stx with
   | node info k _ => node info k args

src/Lean/Elab/Level.lean

@@ -65,7 +65,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
       return mkLevelIMax' (← elabLevel stx) lvl
   else if kind == ``Lean.Parser.Level.hole then
     mkFreshLevelMVar
-  else if kind == numLitKind || kind == `num || kind == `numLit then -- TODO remove staging hack
+  else if kind == numLitKind then
     match stx.isNatLit? with
     | some val => checkUniverseOffset val; return Level.ofNat val
     | none     => throwIllFormedSyntax

src/Lean/Elab/PatternVar.lean

@@ -209,13 +209,13 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     return stx.setArg 2 lhs |>.setArg 3 rhs
   else if k == ``Lean.Parser.Term.inaccessible then
     return stx
-  else if k == strLitKind || k == `str || k == `strLit then -- TODO remove staging hack
+  else if k == strLitKind then
     return stx
-  else if k == numLitKind || k == `num || k == `numLit then -- TODO remove staging hack
+  else if k == numLitKind then
     return stx
   else if k == scientificLitKind then
     return stx
-  else if k == charLitKind || k == `char || k == `charLit then -- TODO remove staging hack
+  else if k == charLitKind then
     return stx
   else if k == ``Lean.Parser.Term.quotedName then
     /- Quoted names have an elaboration function associated with them, and they will not be macro expanded.

src/Lean/Elab/Syntax.lean

@@ -339,22 +339,8 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let stx' ← `($[$doc?:docComment]? def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
   withMacroExpansion stx stx' <| elabCommand stx'
 
--- TODO remove staging hack
-def normKindCore (k : SyntaxNodeKind) : SyntaxNodeKind :=
-  if k == `num || k == `numLit then numLitKind
-  else if k == `char || k == `charLit then charLitKind
-  else if k == `str || k == `strLit then strLitKind
-  else if k == `name || k == `nameLit then nameLitKind
-  else k
-
--- TODO remove staging hack
-def normKind (k : SyntaxNodeKind) : SyntaxNodeKind :=
-  match k with
-  | Name.str s "antiquot" .. => normKindCore s ++ `antiquot
-  | _ => k
-
 def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
-  normKind given == normKind expected || normKind given == normKind (expected ++ `antiquot)
+  given == expected || given == expected ++ `antiquot
 
 def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
   | `(matchAltExpr| | $pat:term => $rhs) => do

src/Lean/Parser/Basic.lean

@@ -1725,14 +1725,7 @@ instance : Coe String Parser := ⟨fun s => symbol s ⟩
   produces the syntax tree for `$e`. -/
 def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser :=
   let kind := (kind.getD Name.anonymous) ++ `antiquot
-  -- TODO remove staging hack
-  let kindP :=
-    if name == "strLit" then nonReservedSymbol "strLit" <|> nonReservedSymbol "str"
-    else if name == "numLit" then nonReservedSymbol "numLit" <|> nonReservedSymbol "num"
-    else if name == "nameLit" then nonReservedSymbol "nameLit" <|> nonReservedSymbol "name"
-    else if name == "charLit" then nonReservedSymbol "charLit" <|> nonReservedSymbol "char"
-    else nonReservedSymbol name
-  let nameP := node `antiquotName $ checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> kindP
+  let nameP := node `antiquotName $ checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name
   -- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
   -- antiquotation kind via `noImmediateColon`
   let nameP := if anonymous then nameP <|> checkNoImmediateColon >> pushNone else nameP

src/Lean/Parser/Extension.lean

@@ -32,12 +32,6 @@ builtin_initialize
   registerBuiltinNodeKind scientificLitKind
   registerBuiltinNodeKind charLitKind
   registerBuiltinNodeKind nameLitKind
-  -- TODO remove staging hack
-  registerBuiltinNodeKind `str
-  registerBuiltinNodeKind `num
-  registerBuiltinNodeKind `scientific
-  registerBuiltinNodeKind `char
-  registerBuiltinNodeKind `name
 
 builtin_initialize builtinParserCategoriesRef : IO.Ref ParserCategories ← IO.mkRef {}
 

src/Lean/Syntax.lean

@@ -25,9 +25,6 @@ def unreachIsNodeIdent {β info rawVal val preresolved} (h : IsNode (Syntax.iden
 
 def isLitKind (k : SyntaxNodeKind) : Bool :=
   k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == scientificLitKind
-  -- TODO remove staging hack
-  || k == `str || k == `num || k == `char || k == `name || k == `scientific
-  || k == `strLit || k == `numLit || k == `charLit || k == `nameLit || k == `scientificLit
 
 namespace SyntaxNode