From a095dabb17493f59695e04e7eaa95981b6d1b4f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Nov 2022 23:06:04 -0800
Subject: [PATCH] feat: `Name.append` and macro scopes

---
 src/Init/Prelude.lean                  | 48 ++++++++++++++++++--------
 src/Lean/Elab/Deriving/FromToJson.lean | 13 +++----
 src/lake                               |  2 +-
 3 files changed, 41 insertions(+), 22 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 32d3b709bb3f..e516444b4af5 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3459,19 +3459,13 @@ instance : BEq Name where
   beq := Name.beq
 
 /--
-Append two hierarchical names. Example:
-```lean
-`Lean.Meta ++ `Tactic.simp
-```
-return `Lean.Meta.Tactic.simp`
+This function does not have special support for macro scopes.
+See `Name.append`.
 -/
-protected def append : Name → Name → Name
-  | n, anonymous => n
-  | n, str p s => Name.mkStr (Name.append n p) s
-  | n, num p d => Name.mkNum (Name.append n p) d
-
-instance : Append Name where
-  append := Name.append
+def appendCore : Name → Name → Name
+  | n, .anonymous => n
+  | n, .str p s => .str (appendCore n p) s
+  | n, .num p d => .num (appendCore n p) d
 
 end Name
 
@@ -4146,7 +4140,7 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
   match view.scopes with
   | List.nil      => view.name
   | List.cons _ _ =>
-    let base := (Name.mkStr (hAppend (hAppend (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
+    let base := (Name.mkStr (Name.appendCore (Name.appendCore (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
     view.scopes.foldl Name.mkNum base
 
 private def assembleParts : List Name → Name → Name
@@ -4194,12 +4188,36 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     | true  => Name.mkNum n scp
     | false =>
       { view with
-        imported   := view.scopes.foldl Name.mkNum (hAppend view.imported view.mainModule)
+        imported   := view.scopes.foldl Name.mkNum (Name.appendCore view.imported view.mainModule)
         mainModule := mainModule
         scopes     := List.cons scp List.nil
       }.review
   | false =>
-    Name.mkNum (Name.mkStr (hAppend (Name.mkStr n "_@") mainModule) "_hyg") scp
+    Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
+
+/--
+Append two names that may have macro scopes. The macro scopes in `b` are always erased.
+If `a` has macro scopes, then the are propagated to result of `append a b`
+-/
+def Name.append (a b : Name) : Name :=
+  match a.hasMacroScopes, b.hasMacroScopes with
+  | true, true  =>
+    /-
+    TODO: this case should be unreachable. Many interactive tests reach this code. We should fix them.
+    The following workaround erases `b`s macro scopes and keeps the one from `a`.
+    -/
+    let view := extractMacroScopes a
+    { view with name := appendCore view.name b.eraseMacroScopes }.review
+  | true, false =>
+    let view := extractMacroScopes a
+    { view with name := appendCore view.name b }.review
+  | false, true =>
+    let view := extractMacroScopes b
+    { view with name := appendCore a view.name }.review
+  | false, false => appendCore a b
+
+instance : Append Name where
+  append := Name.append
 
 /--
 Add a new macro scope onto the name `n`, using the monad state to supply the
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 0e6bc16f6361..f233b3fb3ef4 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -48,16 +48,17 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let header ← mkHeader ``ToJson 1 ctx.typeInfos[0]!
         let discrs ← mkDiscrs header indVal
         let alts ← mkAlts indVal fun ctor args userNames => do
+          let ctorStr := ctor.name.eraseMacroScopes.getString!
           match args, userNames with
-          | #[], _ => ``(toJson $(quote ctor.name.getString!))
-          | #[(x, t)], none => ``(mkObj [($(quote ctor.name.getString!), $(← mkToJson x t))])
+          | #[], _ => ``(toJson $(quote ctorStr))
+          | #[(x, t)], none => ``(mkObj [($(quote ctorStr), $(← mkToJson x t))])
           | xs, none =>
             let xs ← xs.mapM fun (x, t) => mkToJson x t
-            ``(mkObj [($(quote ctor.name.getString!), Json.arr #[$[$xs:term],*])])
+            ``(mkObj [($(quote ctorStr), Json.arr #[$[$xs:term],*])])
           | xs, some userNames =>
             let xs ← xs.mapIdxM fun idx (x, t) => do
-              `(($(quote userNames[idx]!.getString!), $(← mkToJson x t)))
-            ``(mkObj [($(quote ctor.name.getString!), mkObj [$[$xs:term],*])])
+              `(($(quote userNames[idx]!.eraseMacroScopes.getString!), $(← mkToJson x t)))
+            ``(mkObj [($(quote ctorStr), mkObj [$[$xs:term],*])])
         let auxTerm ← `(match $[$discrs],* with $alts:matchAlt*)
         let auxCmd ←
           if ctx.usePartial then
@@ -177,7 +178,7 @@ where
         else
           ``(none)
         let stx ←
-          `((Json.parseTagged json $(quote ctor.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
+          `((Json.parseTagged json $(quote ctor.eraseMacroScopes.getString!) $(quote ctorInfo.numFields) $(quote userNamesOpt)).bind
             (fun jsons => do
               $[let $identNames:ident ← $fromJsons:doExpr]*
               return $(mkIdent ctor):ident $identNames*))
diff --git a/src/lake b/src/lake
index 86a95c342bfb..5724ef636b1f 160000
--- a/src/lake
+++ b/src/lake
@@ -1 +1 @@
-Subproject commit 86a95c342bfb85babaf41f593c73b49d5a13ca21
+Subproject commit 5724ef636b1fcb0e1565e260d5d153e7e5d62746