fix: inconsistency between syntax and kind names

TODO: remove staging workarounds

see #1090

src/Init/Conv.lean

@@ -55,7 +55,7 @@ macro "intro " xs:(colGt ident)* : conv => `(ext $(xs.getArgs)*)
 syntax enterArg := ident <|> num
 syntax "enter " "[" (colGt enterArg),+ "]": conv
 macro_rules
-  | `(conv| enter [$i:numLit]) => `(conv| arg $i)
+  | `(conv| enter [$i:num]) => `(conv| arg $i)
   | `(conv| enter [$id:ident]) => `(conv| ext $id)
   | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 

src/Init/Meta.lean

@@ -837,14 +837,14 @@ def evalPrec (stx : Syntax) : MacroM Nat :=
   Macro.withIncRecDepth stx do
     let stx ← expandMacros stx
     match stx with
-    | `(prec| $num:numLit) => return num.isNatLit?.getD 0
+    | `(prec| $num:num) => return num.isNatLit?.getD 0
     | _ => Macro.throwErrorAt stx "unexpected precedence"
 
 macro_rules
-  | `(prec| $a + $b) => do `(prec| $(quote <| (← evalPrec a) + (← evalPrec b)):numLit)
+  | `(prec| $a + $b) => do `(prec| $(quote <| (← evalPrec a) + (← evalPrec b)):num)
 
 macro_rules
-  | `(prec| $a - $b) => do `(prec| $(quote <| (← evalPrec a) - (← evalPrec b)):numLit)
+  | `(prec| $a - $b) => do `(prec| $(quote <| (← evalPrec a) - (← evalPrec b)):num)
 
 macro "eval_prec " p:prec:max : term => return quote (← evalPrec p)
 
@@ -853,20 +853,20 @@ def evalPrio (stx : Syntax) : MacroM Nat :=
   Macro.withIncRecDepth stx do
     let stx ← expandMacros stx
     match stx with
-    | `(prio| $num:numLit) => return num.isNatLit?.getD 0
+    | `(prio| $num:num) => return num.isNatLit?.getD 0
     | _ => Macro.throwErrorAt stx "unexpected priority"
 
 macro_rules
-  | `(prio| $a + $b) => do `(prio| $(quote <| (← evalPrio a) + (← evalPrio b)):numLit)
+  | `(prio| $a + $b) => do `(prio| $(quote <| (← evalPrio a) + (← evalPrio b)):num)
 
 macro_rules
-  | `(prio| $a - $b) => do `(prio| $(quote <| (← evalPrio a) - (← evalPrio b)):numLit)
+  | `(prio| $a - $b) => do `(prio| $(quote <| (← evalPrio a) - (← evalPrio b)):num)
 
 macro "eval_prio " p:prio:max : term => return quote (← evalPrio p)
 
 def evalOptPrio : Option Syntax → MacroM Nat
   | some prio => evalPrio prio
-  | none      => return eval_prio default
+  | none      => return 1000 -- TODO: FIX back eval_prio default
 
 end Lean
 

src/Init/Prelude.lean

@@ -1847,11 +1847,11 @@ def choiceKind : SyntaxNodeKind := `choice
 def nullKind : SyntaxNodeKind := `null
 def groupKind : SyntaxNodeKind := `group
 def identKind : SyntaxNodeKind := `ident
-def strLitKind : SyntaxNodeKind := `strLit
-def charLitKind : SyntaxNodeKind := `charLit
-def numLitKind : SyntaxNodeKind := `numLit
-def scientificLitKind : SyntaxNodeKind := `scientificLit
-def nameLitKind : SyntaxNodeKind := `nameLit
+def strLitKind : SyntaxNodeKind := `str
+def charLitKind : SyntaxNodeKind := `char
+def numLitKind : SyntaxNodeKind := `num
+def scientificLitKind : SyntaxNodeKind := `scientific
+def nameLitKind : SyntaxNodeKind := `name
 def fieldIdxKind : SyntaxNodeKind := `fieldIdx
 def interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind
 def interpolatedStrKind : SyntaxNodeKind := `interpolatedStrKind

src/Lean/Elab/DefView.lean

@@ -108,7 +108,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
   let attrKind        ← liftMacroM <| toAttributeKind stx[0]
   let prio            ← liftMacroM <| expandOptNamedPrio stx[2]
-  let attrStx         ← `(attr| instance $(quote prio):numLit)
+  let attrStx         ← `(attr| instance $(quote prio):num)
   let (binders, type) := expandDeclSig stx[4]
   let modifiers       := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
   let declId ← match stx[3].getOptional? with

src/Lean/Elab/MacroArgUtil.lean

@@ -17,14 +17,14 @@ def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do
     | `(macroArg| $stx:stx)       => pure (none, (← `(x)), stx)
     | _                           => Macro.throwUnsupported
   let pat ← match stx with
-    | `(stx| $s:strLit)      => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
-    | `(stx| &$s:strLit)     => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
+    | `(stx| $s:str)      => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
+    | `(stx| &$s:str)     => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
     | `(stx| optional($stx)) => pure <| mkSplicePat `optional id "?"
     | `(stx| many($stx))     => pure <| mkSplicePat `many id "*"
     | `(stx| many1($stx))    => pure <| mkSplicePat `many id "*"
-    | `(stx| sepBy($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
+    | `(stx| sepBy($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
       pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
-    | `(stx| sepBy1($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
+    | `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
       pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
     | _ => match id? with
       -- if there is a binding, we assume the user knows what they are doing

src/Lean/Elab/Mixfix.lean

@@ -12,17 +12,17 @@ namespace Lean.Elab.Command
     match stx with
     | `(infixl:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
       let prec1 := quote <| (← evalPrec prec) + 1
-      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec $op:strLit rhs:$prec1 => $f lhs rhs)
+      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec $op:str rhs:$prec1 => $f lhs rhs)
     | `(infix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
       let prec1 := quote <| (← evalPrec prec) + 1
-      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs:$prec1 => $f lhs rhs)
+      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:str rhs:$prec1 => $f lhs rhs)
     | `(infixr:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
       let prec1 := quote <| (← evalPrec prec) + 1
-      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs:$prec => $f lhs rhs)
+      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:str rhs:$prec => $f lhs rhs)
     | `(prefix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? $op:strLit arg:$prec => $f arg)
+      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? $op:str arg:$prec => $f arg)
     | `(postfix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
-      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? arg:$prec $op:strLit => $f arg)
+      `(notation:$prec $[(name := $name)]? $[(priority := $prio)]? arg:$prec $op:str => $f arg)
     | _ => Macro.throwUnsupported
 where
   -- set "global" `attrKind`, apply `f`, and restore `attrKind` to result

src/Lean/Elab/Notation.lean

@@ -90,7 +90,7 @@ private def expandNotationAux (ref : Syntax)
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
   let fullName := currNamespace ++ name
   let pat := mkNode fullName patArgs
-  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
+  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat)
   let mut macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
   if isLocalAttrKind attrKind then
     -- Make sure the quotation pre-checker takes section variables into account for local notation.

src/Lean/Elab/Print.lean

@@ -83,7 +83,7 @@ private def printId (id : Syntax) : CommandElabM Unit := do
 
 @[builtinCommandElab «print»] def elabPrint : CommandElab
   | `(#print%$tk $id:ident) => withRef tk <| printId id
-  | `(#print%$tk $s:strLit) => logInfoAt tk s.isStrLit?.get!
+  | `(#print%$tk $s:str) => logInfoAt tk s.isStrLit?.get!
   | _                       => throwError "invalid #print command"
 
 namespace CollectAxioms

src/Lean/Elab/Syntax.lean

@@ -323,10 +323,10 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let declName := mkIdentFrom stx name
   let d ←
     if let some lhsPrec := lhsPrec? then
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.TrailingParserDescr :=
+      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.TrailingParserDescr :=
         ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
     else
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.ParserDescr :=
+      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.ParserDescr :=
         ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
   trace `Elab fun _ => d
   withMacroExpansion stx d <| elabCommand d

src/Lean/Parser/Basic.lean

@@ -1272,7 +1272,7 @@ def numLitFn : ParserFn :=
 
 @[inline] def numLitNoAntiquot : Parser := {
   fn   := numLitFn,
-  info := mkAtomicInfo "numLit"
+  info := mkAtomicInfo "num"
 }
 
 def scientificLitFn : ParserFn :=
@@ -1284,7 +1284,7 @@ def scientificLitFn : ParserFn :=
 
 @[inline] def scientificLitNoAntiquot : Parser := {
   fn   := scientificLitFn,
-  info := mkAtomicInfo "scientificLit"
+  info := mkAtomicInfo "scientific"
 }
 
 def strLitFn : ParserFn := fun c s =>
@@ -1295,7 +1295,7 @@ def strLitFn : ParserFn := fun c s =>
 
 @[inline] def strLitNoAntiquot : Parser := {
   fn   := strLitFn,
-  info := mkAtomicInfo "strLit"
+  info := mkAtomicInfo "str"
 }
 
 def charLitFn : ParserFn := fun c s =>
@@ -1306,7 +1306,7 @@ def charLitFn : ParserFn := fun c s =>
 
 @[inline] def charLitNoAntiquot : Parser := {
   fn   := charLitFn,
-  info := mkAtomicInfo "charLit"
+  info := mkAtomicInfo "char"
 }
 
 def nameLitFn : ParserFn := fun c s =>
@@ -1317,7 +1317,7 @@ def nameLitFn : ParserFn := fun c s =>
 
 @[inline] def nameLitNoAntiquot : Parser := {
   fn   := nameLitFn,
-  info := mkAtomicInfo "nameLit"
+  info := mkAtomicInfo "name"
 }
 
 def identFn : ParserFn := fun c s =>

src/Lean/Parser/Extra.lean

@@ -34,19 +34,19 @@ attribute [runBuiltinParserAttributeHooks]
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
 @[runBuiltinParserAttributeHooks] def numLit : Parser :=
-  withAntiquot (mkAntiquot "numLit" numLitKind) numLitNoAntiquot
+  withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks] def scientificLit : Parser :=
-  withAntiquot (mkAntiquot "scientificLit" scientificLitKind) scientificLitNoAntiquot
+  withAntiquot (mkAntiquot "scientific" scientificLitKind) scientificLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks] def strLit : Parser :=
-  withAntiquot (mkAntiquot "strLit" strLitKind) strLitNoAntiquot
+  withAntiquot (mkAntiquot "str" strLitKind) strLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks] def charLit : Parser :=
-  withAntiquot (mkAntiquot "charLit" charLitKind) charLitNoAntiquot
+  withAntiquot (mkAntiquot "char" charLitKind) charLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks] def nameLit : Parser :=
-  withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot
+  withAntiquot (mkAntiquot "name" nameLitKind) nameLitNoAntiquot
 
 @[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser :=
   node groupKind p