feat: macroScope parser (aka this 2.0)

Author: digama0

src/Init/Meta.lean

@@ -271,10 +271,11 @@ abbrev CharLit := TSyntax charLitKind
 abbrev NameLit := TSyntax nameLitKind
 abbrev ScientificLit := TSyntax scientificLitKind
 abbrev NumLit := TSyntax numLitKind
+abbrev MacroScopeLit := TSyntax macroScopeKind
 
 end Syntax
 
-export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit)
+export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit MacroScopeLit)
 
 namespace TSyntax
 
@@ -921,6 +922,14 @@ def getChar (s : CharLit) : Char :=
 def getName (s : NameLit) : Name :=
   s.raw.isNameLit?.getD .anonymous
 
+def getMacroScope (s : MacroScopeLit) : Name :=
+  s.raw[0].getId
+
+def mkIdent (s : MacroScopeLit) (val : Name) (canonical := false) : Ident :=
+  let src := s.raw[0]
+  let id := { extractMacroScopes src.getId with name := val.eraseMacroScopes }.review
+  ⟨Syntax.ident (SourceInfo.fromRef src canonical) (toString val).toSubstring id []⟩
+
 namespace Compat
 
 scoped instance : CoeTail (Array Syntax) (Syntax.TSepArray k sep) where

src/Init/Prelude.lean

@@ -3721,6 +3721,12 @@ abbrev nameLitKind : SyntaxNodeKind := `name
 /-- `fieldIdx` is the node kind of projection indices like the `2` in `x.2`. -/
 abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
+/--
+`macroScope` is the node kind of macro scopes, which are "invisible tokens"
+which capture the hygiene information at the current point without parsing anything.
+-/
+abbrev macroScopeKind : SyntaxNodeKind := `macroScope
+
 /--
 `interpolatedStrLitKind` is the node kind of interpolated string literal
 fragments like `"value = {` and `}"` in `s!"value = {x}"`.

src/Lean/Elab/Syntax.lean

@@ -260,7 +260,7 @@ open Lean.Parser.Command
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
   if let .str _ suffix := catName then
-    let quotSymbol := "`(" ++ suffix ++ "|"
+    let quotSymbol := "`(" ++ suffix ++ "| "
     let name := catName ++ `quot
     let cmd ← `(
       @[term_parser] def $(mkIdent name) : Lean.ParserDescr :=

src/Lean/Parser.lean

@@ -27,7 +27,8 @@ builtin_initialize
   register_parser_alias (kind := charLitKind) "char" charLit
   register_parser_alias (kind := nameLitKind) "name" nameLit
   register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
-  register_parser_alias (kind := identKind) "ident" ident
+  register_parser_alias (kind := identKind) ident
+  register_parser_alias (kind := macroScopeKind) macroScope
   register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
   register_parser_alias "colGe" checkColGe { stackSz? := some 0 }
   register_parser_alias "colEq" checkColEq { stackSz? := some 0 }

src/Lean/Parser/Basic.lean

@@ -1072,6 +1072,18 @@ def identEq (id : Name) : Parser := {
   info := mkAtomicInfo "ident"
 }
 
+def macroScopeFn : ParserFn := fun _ s =>
+  let pos   := s.pos
+  let info  := SourceInfo.original "".toSubstring pos "".toSubstring pos
+  let ident := mkIdent info "".toSubstring .anonymous
+  let stx   := mkNode macroScopeKind #[ident]
+  s.pushSyntax stx
+
+def macroScopeNoAntiquot : Parser := {
+  fn   := macroScopeFn
+  info := nodeInfo macroScopeKind epsilonInfo
+}
+
 namespace ParserState
 
 def keepTop (s : SyntaxStack) (startStackSize : Nat) : SyntaxStack :=

src/Lean/Parser/Extra.lean

@@ -37,6 +37,9 @@ attribute [run_builtin_parser_attribute_hooks]
 @[run_builtin_parser_attribute_hooks] def rawIdent : Parser :=
   withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
 
+@[run_builtin_parser_attribute_hooks] def macroScope : Parser :=
+  withAntiquot (mkAntiquot "macroScope" macroScopeKind) macroScopeNoAntiquot
+
 @[run_builtin_parser_attribute_hooks] def numLit : Parser :=
   withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
 

src/Lean/PrettyPrinter/Formatter.lean

@@ -489,6 +489,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter skip] def skip.formatter : Formatter := pure ()
 
 @[combinator_formatter pushNone] def pushNone.formatter : Formatter := goLeft
+@[combinator_formatter macroScopeNoAntiquot] def macroScopeNoAntiquot.formatter : Formatter := goLeft
 
 @[combinator_formatter interpolatedStr]
 def interpolatedStr.formatter (p : Formatter) : Formatter := do

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -492,6 +492,7 @@ def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
 @[combinator_parenthesizer skip] def skip.parenthesizer : Parenthesizer := pure ()
 
 @[combinator_parenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
+@[combinator_parenthesizer macroScopeNoAntiquot] def macroScopeNoAntiquot.parenthesizer : Parenthesizer := goLeft
 
 @[combinator_parenthesizer interpolatedStr]
 def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do

tests/lean/interactive/1265.lean.expected.out

@@ -2,6 +2,9 @@
  "position": {"line": 0, "character": 51}}
 {"items":
  [{"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
+  {"label": "getMacroScope",
+   "kind": 3,
+   "detail": "Lean.MacroScopeLit → Lean.Name"},
   {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"},
   {"label": "expandInterpolatedStr",
    "kind": 3,
@@ -13,6 +16,10 @@
    "kind": 3,
    "detail": "Lean.ScientificLit → Nat × Bool × Nat"},
   {"label": "getString", "kind": 3, "detail": "Lean.StrLit → String"},
+  {"label": "mkIdent",
+   "kind": 3,
+   "detail":
+   "Lean.MacroScopeLit → Lean.Name → optParam Bool false → Lean.Ident"},
   {"label": "raw",
    "kind": 5,
    "documentation":
@@ -23,6 +30,9 @@
  "position": {"line": 2, "character": 53}}
 {"items":
  [{"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"},
+  {"label": "getMacroScope",
+   "kind": 3,
+   "detail": "Lean.MacroScopeLit → Lean.Name"},
   {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"},
   {"label": "expandInterpolatedStr",
    "kind": 3,
@@ -34,6 +44,10 @@
    "kind": 3,
    "detail": "Lean.ScientificLit → Nat × Bool × Nat"},
   {"label": "getString", "kind": 3, "detail": "Lean.StrLit → String"},
+  {"label": "mkIdent",
+   "kind": 3,
+   "detail":
+   "Lean.MacroScopeLit → Lean.Name → optParam Bool false → Lean.Ident"},
   {"label": "raw",
    "kind": 5,
    "documentation":