fix: address review feedback for name demangling (round 2)

This PR addresses three issues raised in review:

1. Use `Name.toString` for correct escaping of demangled names (#9):
   replace manual `String.intercalate "."` formatting with
   `Name.toString`, which handles `«»` escaping for names containing
   special characters. Add `namePartsToName` helper and guard
   `formatNameParts` against empty input.

2. Use `Name.demangle?` for robust `lp_` package splitting (#8):
   replace `findLpSplit`/`hasUpperStart`/`unmanglePkg` with a simpler
   `demangleWithPkg` that tries each underscore as a split point and
   validates both package and body via `Name.demangle?` round-trip.

3. Fix suffix flags lost after hygienic sections: move suffix flag
   collection (`_boxed`, `_lam`, etc.) before `_@` hygienic suffix
   stripping, so flags appearing after hygienic sections are recognized.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Compiler/NameDemangling.lean

@@ -34,11 +34,15 @@ where
     | .str pre s, acc => go pre (NamePart.str s :: acc)
     | .num pre n, acc => go pre (NamePart.num n :: acc)
 
+private def namePartsToName (parts : Array NamePart) : Name :=
+  parts.foldl (fun acc p =>
+    match p with
+    | .str s => acc.mkStr s
+    | .num n => acc.mkNum n) .anonymous
+
+/-- Format name parts using `Name.toString` for correct escaping. -/
 private def formatNameParts (comps : Array NamePart) : String :=
-  comps.toList.map (fun
-    | NamePart.str s => s
-    | NamePart.num n => toString n)
-  |> String.intercalate "."
+  if comps.isEmpty then "" else (namePartsToName comps).toString
 
 private def matchSuffix (c : NamePart) : Option String :=
   match c with
@@ -82,7 +86,7 @@ private def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
       if comps[i]? == some (NamePart.num 0) && i + 1 < comps.size then
         begin_ := i + 1
         break
-  let mut nameParts : Array String := #[]
+  let mut parts : Array NamePart := #[]
   let mut flags : Array String := #[]
   for i in [begin_:comps.size] do
     let c := comps[i]!
@@ -92,10 +96,8 @@ private def processSpecContext (comps : Array NamePart) : SpecEntry := Id.run do
         flags := flags.push flag
     | none =>
       if isSpecIndex c then pure ()
-      else match c with
-        | NamePart.str s => nameParts := nameParts.push s
-        | NamePart.num n => nameParts := nameParts.push (toString n)
-  { name := String.intercalate "." nameParts.toList, flags }
+      else parts := parts.push c
+  { name := formatNameParts parts, flags }
 
 private def postprocessNameParts (components : Array NamePart) : String := Id.run do
   if components.isEmpty then return ""
@@ -103,6 +105,31 @@ private def postprocessNameParts (components : Array NamePart) : String := Id.ru
   let (privStart, isPrivate) := stripPrivate components 0 components.size
   let mut parts := components.extract privStart components.size
 
+  -- Collect suffix flags from the end first, before stripping hygienic suffixes,
+  -- since _boxed etc. may appear after _@ sections.
+  let mut flags : Array String := #[]
+  let mut cont := true
+  while cont && !parts.isEmpty do
+    let last := parts.back!
+    match matchSuffix last with
+    | some flag =>
+      flags := flags.push flag
+      parts := parts.pop
+    | none =>
+      match last with
+      | NamePart.num _ =>
+        if parts.size >= 2 then
+          match matchSuffix parts[parts.size - 2]! with
+          | some flag =>
+            flags := flags.push flag
+            parts := parts.pop.pop
+          | none => cont := false
+        else cont := false
+      | _ => cont := false
+
+  if isPrivate then
+    flags := flags.push "private"
+
   -- Strip hygienic suffixes (_@ onward)
   for i in [:parts.size] do
     match parts[i]! with
@@ -163,30 +190,6 @@ private def postprocessNameParts (components : Array NamePart) : String := Id.ru
 
     parts := base ++ remaining
 
-  -- Collect suffix flags from the end
-  let mut flags : Array String := #[]
-  let mut cont := true
-  while cont && !parts.isEmpty do
-    let last := parts.back!
-    match matchSuffix last with
-    | some flag =>
-      flags := flags.push flag
-      parts := parts.pop
-    | none =>
-      match last with
-      | NamePart.num _ =>
-        if parts.size >= 2 then
-          match matchSuffix parts[parts.size - 2]! with
-          | some flag =>
-            flags := flags.push flag
-            parts := parts.pop.pop
-          | none => cont := false
-        else cont := false
-      | _ => cont := false
-
-  if isPrivate then
-    flags := flags.push "private"
-
   let name := if parts.isEmpty then "?" else formatNameParts parts
   let mut result := name
 
@@ -203,54 +206,35 @@ private def postprocessNameParts (components : Array NamePart) : String := Id.ru
 
   return result
 
-private def hasUpperStart (s : String) : Bool :=
-  let s := ((s.dropPrefix? "00").map (·.toString)).getD s
-  go s s.startPos
-where
-  go (s : String) (pos : s.Pos) : Bool :=
-    if h : pos = s.endPos then false
-    else if pos.get h == '_' then go s (pos.next h)
-    else (pos.get h).isUpper
-  termination_by pos
+private def demangleBody (body : String) : String :=
+  let name := Name.demangle body
+  postprocessNameParts (nameToNameParts name)
 
-private def findLpSplit (s : String) : Option (String × String) := Id.run do
-  let mut validSplits : Array (String × String × Bool) := #[]
+/-- Split a `lp_`-prefixed symbol into (demangled body, package name).
+Tries each underscore as a split point; the first valid split (shortest single-component
+package where the remainder is a valid mangled name) is correct. -/
+private def demangleWithPkg (s : String) : Option (String × String) := do
   for ⟨pos, h⟩ in s.positions do
     if pos.get h == '_' && pos ≠ s.startPos then
       let nextPos := pos.next h
       if nextPos == s.endPos then continue
       let pkg := s.extract s.startPos pos
       let body := s.extract nextPos s.endPos
-      -- Package must be a valid single-component mangled name
       let validPkg := match Name.demangle? pkg with
         | some (.str .anonymous _) => true
         | _ => false
       if validPkg && (Name.demangle? body).isSome then
-        validSplits := validSplits.push (pkg, body, hasUpperStart body)
-  if validSplits.isEmpty then return none
-  -- Prefer: shortest valid package (first split point).
-  -- Among splits where body starts uppercase, pick the first.
-  -- If no uppercase, still pick the first.
-  let upperSplits := validSplits.filter (·.2.2)
-  if !upperSplits.isEmpty then
-    return some (upperSplits[0]!.1, upperSplits[0]!.2.1)
-  else
-    return some (validSplits[0]!.1, validSplits[0]!.2.1)
-
-private def unmanglePkg (s : String) : String :=
-  match Name.demangle s with
-  | .str .anonymous s => s
-  | _ => s
+        let pkgName := match Name.demangle pkg with
+          | .str .anonymous s => s
+          | _ => pkg
+        return (demangleBody body, pkgName)
+  none
 
 private def stripColdSuffix (s : String) : String × String :=
   match s.find? ".cold" with
   | some pos => (s.extract s.startPos pos, s.extract pos s.endPos)
   | none => (s, "")
 
-private def demangleBody (body : String) : String :=
-  let name := Name.demangle body
-  postprocessNameParts (nameToNameParts name)
-
 private def demangleCore (s : String) : Option String := do
   -- _init_l_
   if let some body := dropPrefix? s "_init_l_" then
@@ -258,8 +242,8 @@ private def demangleCore (s : String) : Option String := do
 
   -- _init_lp_
   if let some after := dropPrefix? s "_init_lp_" then
-    if let some (pkg, body) := findLpSplit after then
-      if !body.isEmpty then return s!"[init] {demangleBody body} ({unmanglePkg pkg})"
+    if let some (name, pkg) := demangleWithPkg after then
+      return s!"[init] {name} ({pkg})"
 
   -- initialize_l_
   if let some body := dropPrefix? s "initialize_l_" then
@@ -267,8 +251,8 @@ private def demangleCore (s : String) : Option String := do
 
   -- initialize_lp_
   if let some after := dropPrefix? s "initialize_lp_" then
-    if let some (pkg, body) := findLpSplit after then
-      if !body.isEmpty then return s!"[module_init] {demangleBody body} ({unmanglePkg pkg})"
+    if let some (name, pkg) := demangleWithPkg after then
+      return s!"[module_init] {name} ({pkg})"
 
   -- initialize_ (bare module init)
   if let some body := dropPrefix? s "initialize_" then
@@ -280,8 +264,8 @@ private def demangleCore (s : String) : Option String := do
 
   -- lp_
   if let some after := dropPrefix? s "lp_" then
-    if let some (pkg, body) := findLpSplit after then
-      if !body.isEmpty then return s!"{demangleBody body} ({unmanglePkg pkg})"
+    if let some (name, pkg) := demangleWithPkg after then
+      return s!"{name} ({pkg})"
 
   none
 

tests/lean/run/demangling.lean

@@ -171,6 +171,11 @@ private def checkRoundTrip (label : String) (parts : List (String ⊕ Nat)) : IO
   let mangled := Name.mangle `Lean.Meta.foo (s!"lp_{String.mangle "my_pkg"}_")
   checkSome "lp_ underscore pkg" (demangleSymbol mangled) "Lean.Meta.foo (my_pkg)"
 
+#eval do
+  -- Package with escaped chars (hyphen → _x2d): split must not break mid-escape
+  let mangled := Name.mangle `Lean.Meta.foo (s!"lp_{String.mangle "my-pkg"}_")
+  checkSome "lp_ escaped pkg" (demangleSymbol mangled) "Lean.Meta.foo (my-pkg)"
+
 #eval do
   let name := mkName [.inl "_private", .inl "X", .inr 0, .inl "Y", .inl "foo"]
   let mangled := name.mangle (s!"lp_{String.mangle "pkg"}_")
@@ -338,6 +343,21 @@ private def checkRoundTrip (label : String) (parts : List (String ⊕ Nat)) : IO
   checkSome "hygienic strip" (demangleSymbol (name.mangle "l_"))
     "Lean.Meta.foo"
 
+#eval do
+  -- _boxed after _@ hygienic section should still be recognized
+  let name := mkName [.inl "Lean", .inl "Meta", .inl "foo", .inl "_@",
+                       .inl "Lean", .inl "Meta", .inl "_hyg", .inr 42, .inl "_boxed"]
+  checkSome "hygienic + boxed" (demangleSymbol (name.mangle "l_"))
+    "Lean.Meta.foo [boxed]"
+
+#eval do
+  -- _lam + _boxed after _@ should both be recognized
+  let name := mkName [.inl "Lean", .inl "initFn", .inl "_@",
+                       .inl "Lean", .inl "Elab", .inl "_hyg", .inr 42,
+                       .inl "_lam", .inr 0, .inl "_boxed"]
+  checkSome "hygienic + lam + boxed" (demangleSymbol (name.mangle "l_"))
+    "Lean.initFn [boxed, λ]"
+
 -- ============================================================================
 -- Postprocessing: specialization contexts
 -- ============================================================================