From da0e0e00ae546e905c0fbc823e509ce0f424ab24 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 12 Apr 2022 17:51:53 +0100
Subject: [PATCH 1/2] refactor: Split `renameVar` in to two passes

---
 primer/src/Primer/Core/Transform.hs | 91 ++++++++++++++++-------------
 primer/test/Tests/Action/Prog.hs    |  3 +-
 2 files changed, 52 insertions(+), 42 deletions(-)

diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs
index d2a994fcb..855ae4604 100644
--- a/primer/src/Primer/Core/Transform.hs
+++ b/primer/src/Primer/Core/Transform.hs
@@ -1,4 +1,5 @@
 module Primer.Core.Transform (
+  transformVar,
   renameVar,
   renameLocalVar,
   renameTyVar,
@@ -15,57 +16,67 @@ import Foreword
 
 import Control.Monad.Fresh (MonadFresh)
 import Data.Data (Data)
-import Data.Generics.Uniplate.Data (descendM)
+import Data.Generics.Uniplate.Data (children, descendM)
 import qualified Data.List.NonEmpty as NE
-import Primer.Core (CaseBranch' (..), Expr, Expr' (..), ID, LVarName, LocalName (unLocalName), TmVarRef (..), TyVarName, Type' (..), bindName, varRefName)
+import Primer.Core (CaseBranch' (..), Expr, Expr' (..), ID, LVarName, TmVarRef (..), TyVarName, Type' (..), bindName)
 import Primer.Core.DSL (meta)
 
 -- AST transformations.
 -- This module contains global transformations on expressions and types, in
 -- contrast to the focused, local transformations provided by the zipper.
 
+-- | Find all nodes at which the given variable is shadowed.
+checkShadowing :: (Data a, Data b) => TmVarRef -> Expr' a b -> [a]
+checkShadowing x = \case
+  Lam m v e
+    | LocalVarRef v == x -> pure m
+    | otherwise -> checkShadowing x e
+  Let m v e1 e2
+    | LocalVarRef v == x -> pure m
+    | otherwise -> checkShadowing x e1 <> checkShadowing x e2
+  Case m scrut branches -> checkShadowing x scrut <> concatMap checkBranch branches
+    where
+      checkBranch b@(CaseBranch _ _ rhs)
+        | LocalVarRef ly <- x, ly `elem` bindingNames b = pure m
+        | otherwise = checkShadowing x rhs
+      bindingNames (CaseBranch _ bs _) = map bindName bs
+  Var m v
+    | v == x -> pure m
+    | otherwise -> mempty
+  e -> concatMap (checkShadowing x) $ children e
+
+-- | Apply a function to all free occurrences of a variable.
+transformVar ::
+  (Monad m, Data a, Data b') =>
+  (a -> TmVarRef -> m (Expr' a b')) ->
+  TmVarRef ->
+  Expr' a b' ->
+  m (Expr' a b')
+transformVar f x = \case
+  Lam m v e
+    | LocalVarRef v == x -> pure $ Lam m v e
+    | otherwise -> Lam m v <$> transformVar f x e
+  Let m v e1 e2
+    | LocalVarRef v == x -> pure $ Let m v e1 e2
+    | otherwise -> Let m v <$> transformVar f x e1 <*> transformVar f x e2
+  Case m scrut branches -> Case m <$> transformVar f x scrut <*> mapM renameBranch branches
+    where
+      renameBranch b@(CaseBranch con termargs rhs)
+        | LocalVarRef lx <- x, lx `elem` bindingNames b = pure b
+        | otherwise = CaseBranch con termargs <$> transformVar f x rhs
+      bindingNames (CaseBranch _ bs _) = map bindName bs
+  Var m v
+    | v == x -> f m v
+    | otherwise -> pure $ Var m v
+  e -> descendM (transformVar f x) e
+
 -- | Attempt to replace all free ocurrences of @x@ in @e@ with @y@
 -- Returns 'Nothing' if replacement could result in variable capture.
 -- See the tests for explanation and examples.
 renameVar :: (Data a, Data b) => TmVarRef -> TmVarRef -> Expr' a b -> Maybe (Expr' a b)
-renameVar x y =
-  let xn = varRefName x
-      yn = varRefName y
-   in \case
-        Lam m v e
-          | LocalVarRef v == x -> pure $ Lam m v e
-          | LocalVarRef v == y -> Nothing
-          -- If we have the same Name, but different local/global scopes
-          -- also bail out as something has gone wrong.
-          | unLocalName v == xn || unLocalName v == yn -> Nothing
-          | otherwise -> Lam m v <$> renameVar x y e
-        Let m v e1 e2
-          | LocalVarRef v == x -> pure $ Let m v e1 e2
-          | LocalVarRef v == y -> Nothing
-          -- If we have the same Name, but different local/global scopes
-          -- also bail out as something has gone wrong.
-          | unLocalName v == xn || unLocalName v == yn -> Nothing
-          | otherwise -> Let m v <$> renameVar x y e1 <*> renameVar x y e2
-        Case m scrut branches -> Case m <$> renameVar x y scrut <*> mapM renameBranch branches
-          where
-            renameBranch b@(CaseBranch con termargs rhs)
-              | LocalVarRef lx <- x, lx `elem` bindingNames b = pure b
-              | LocalVarRef ly <- y, ly `elem` bindingNames b = Nothing
-              -- If we have the same Name, but different local/global scopes
-              -- also bail out as something has gone wrong.
-              | bns <- map unLocalName $ bindingNames b
-              , xn `elem` bns || yn `elem` bns =
-                  Nothing
-              | otherwise = CaseBranch con termargs <$> renameVar x y rhs
-            bindingNames (CaseBranch _ bs _) = map bindName bs
-        Var m v
-          | v == x -> pure $ Var m y
-          | v == y -> Nothing
-          -- If we have the same Name, but different local/global scopes
-          -- also bail out as something has gone wrong.
-          | varRefName v == xn || varRefName v == yn -> Nothing
-          | otherwise -> pure $ Var m v
-        e -> descendM (renameVar x y) e
+renameVar x y e = case checkShadowing y e of
+  [] -> transformVar (\m _ -> Just $ Var m y) x e
+  _ -> Nothing
 
 -- | As 'renameVar', but specialised to local variables
 renameLocalVar :: (Data a, Data b) => LVarName -> LVarName -> Expr' a b -> Maybe (Expr' a b)
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 445eb7512..06ab157de 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -20,7 +20,6 @@ import Primer.Action (
     EnterType,
     Move
   ),
-  ActionError (NameCapture),
   Movement (Branch, Child1, Child2),
  )
 import Primer.App (
@@ -712,7 +711,7 @@ unit_copy_paste_import =
 unit_rename_def_capture :: Assertion
 unit_rename_def_capture =
   progActionTest defaultEmptyProg [MoveToDef "other", BodyAction [ConstructLam $ Just "foo"], RenameDef "main" "foo"] $
-    expectError (@?= ActionError NameCapture)
+    expectSuccess mempty
 
 unit_RenameType :: Assertion
 unit_RenameType =

From 98e6ce0a773ee1e11632d90987112db5596d01e1 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 12 Apr 2022 18:20:16 +0100
Subject: [PATCH 2/2] fix: Remove `varRefName`

Weeder rightly points out that it's unused, due to the changes to `renameVar` in the previous commit.
---
 primer/src/Primer/Core.hs | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs
index 7d8184241..398872945 100644
--- a/primer/src/Primer/Core.hs
+++ b/primer/src/Primer/Core.hs
@@ -12,7 +12,6 @@ module Primer.Core (
   Expr' (..),
   Bind' (..),
   TmVarRef (..),
-  varRefName,
   CaseBranch,
   CaseBranch' (..),
   Def (..),
@@ -256,11 +255,6 @@ data TmVarRef
   deriving (Eq, Show, Data, Generic)
   deriving (FromJSON, ToJSON) via VJSON TmVarRef
 
-varRefName :: TmVarRef -> Name
-varRefName = \case
-  GlobalVarRef (GlobalName n) -> n
-  LocalVarRef (LocalName n) -> n
-
 -- Note [Synthesisable constructors]
 -- Whilst our calculus is heavily inspired by bidirectional type systems
 -- (especially McBride's principled rendition), we do not treat constructors