From 437e1b7245afe4d3085e012f8d768cc1323c44e2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 6 Jan 2020 21:54:58 +0100
Subject: [PATCH] fix: elaboration of macro-generated defs

---
 src/Init/Lean/Elab/Command.lean | 12 +++++++++---
 src/Init/Lean/Hygiene.lean      | 16 +++++++++++++++-
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index f33284b5d3..0a42b3ae52 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -586,10 +586,16 @@ levelNames      ←
       savedLevelNames
   };
 let ref := declId;
+-- extract (optional) namespace part of id, after decoding macro scopes that would interfere with the check
+let (id, scps) := extractMacroScopes id;
 match id with
-| Name.str pre s _ => withNamespace ref pre $ do
-  modifyScope $ fun scope => { levelNames := levelNames, .. scope };
-  finally (f (mkNameSimple s)) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
+| Name.str pre s _ =>
+  /- Add back macro scopes. We assume a declaration like `def a.b[1,2] ...` with macro scopes `[1,2]`
+     is always meant to mean `namespace a def b[1,2] ...`. -/
+  let id := addMacroScopes (mkNameSimple s) scps;
+  withNamespace ref pre $ do
+    modifyScope $ fun scope => { levelNames := levelNames, .. scope };
+    finally (f id) (modifyScope $ fun scope => { levelNames := savedLevelNames, .. scope })
 | _                => throwError ref "invalid declaration name"
 
 /--
diff --git a/src/Init/Lean/Hygiene.lean b/src/Init/Lean/Hygiene.lean
index 5c10103bf4..1c4cbd8dfb 100644
--- a/src/Init/Lean/Hygiene.lean
+++ b/src/Init/Lean/Hygiene.lean
@@ -38,10 +38,24 @@ class MonadQuotation (m : Type → Type) :=
 (withFreshMacroScope {α : Type} : m α → m α)
 export MonadQuotation
 
-def addMacroScope (n : Name) (scp : MacroScope) : Name :=
 -- TODO: try harder to avoid clashes with other autogenerated names
+def addMacroScope (n : Name) (scp : MacroScope) : Name :=
 mkNameNum n scp
 
+def addMacroScopes (n : Name) (scps : List MacroScope) : Name :=
+scps.foldl addMacroScope n
+
+private def extractMacroScopesAux : Name → List MacroScope → Name × List MacroScope
+| Name.num n scp _, acc => extractMacroScopesAux n (scp::acc)
+| n               , acc => (n, acc.reverse)
+
+/--
+  Revert all `addMacroScope` calls. `(n', scps) = extractMacroScopes n → n = addMacroScopes n' scps`.
+  This operation is useful for analyzing/transforming the original identifiers, then adding back
+  the scopes (via `addMacroScopes`). -/
+def extractMacroScopes (n : Name) : Name × List MacroScope :=
+extractMacroScopesAux n []
+
 /-- Simplistic MonadQuotation that does not guarantee globally fresh names, that
     is, between different runs of this or other MonadQuotation implementations.
     It is only safe if the syntax quotations do not introduce bindings around