feat: Always allow deleting a term definition

Use sites will be replaced with holes. This is consistent with the behaviour we now have for type definitions.

Signed-off-by: George Thomas <georgefsthomas@gmail.com>

primer/src/Primer/Action/Available.hs

@@ -98,7 +98,7 @@ import Primer.Def (
   ASTDef (..),
   DefMap,
  )
-import Primer.Def.Utils (globalInUse, typeInUse)
+import Primer.Def.Utils (typeInUse)
 import Primer.JSON (CustomJSON (..), FromJSON, PrimerJSON, ToJSON)
 import Primer.Name (unName)
 import Primer.Primitives (tChar, tInt)
@@ -212,13 +212,10 @@ forDef ::
   GVarName ->
   [Action]
 forDef _ _ NonEditable _ = mempty
-forDef defs l Editable defName =
-  sortByPriority l
-    $ [Input RenameDef, NoInput DuplicateDef]
-    <> mwhen
-      -- ensure the definition is not in use, otherwise the action will not succeed
-      (not $ globalInUse defName $ Map.delete defName defs)
-      [NoInput DeleteDef]
+forDef _ l Editable _ =
+  sortByPriority
+    l
+    [Input RenameDef, NoInput DuplicateDef, NoInput DeleteDef]
 
 forBody ::
   TypeDefMap ->

primer/src/Primer/Action/ProgError.hs

@@ -14,7 +14,6 @@ data ProgError
   | NoTypeDefSelected
   | DefNotFound GVarName
   | DefAlreadyExists GVarName
-  | DefInUse GVarName
   | TypeDefIsPrim TyConName
   | TypeDefNotFound TyConName
   | TypeDefAlreadyExists TyConName

primer/src/Primer/App.hs

@@ -197,7 +197,7 @@ import Primer.Def (
   DefMap,
   defAST,
  )
-import Primer.Def.Utils (globalInUse, typeInUse)
+import Primer.Def.Utils (typeInUse)
 import Primer.Eval (AvoidShadowing (AvoidShadowing))
 import Primer.Eval qualified as Eval
 import Primer.Eval.Detail (EvalDetail)
@@ -645,10 +645,17 @@ applyProgAction prog = \case
     case deleteDef m d of
       Nothing -> throwError $ DefNotFound d
       Just mod' -> do
-        when (globalInUse d $ foldMap' moduleDefs $ mod' : ms)
-          $ throwError
-          $ DefInUse d
-        pure (mod' : ms, Nothing)
+        ms' <-
+          (mod' : ms)
+            & traverseOf
+              (traversed % #moduleDefs % traversed % #_DefAST)
+              ( traverseOf
+                  #astDefExpr
+                  $ transformM \case
+                    Var _ (GlobalVarRef v) | v == d -> emptyHole
+                    e -> pure e
+              )
+        pure (ms', Nothing)
   RenameDef d nameStr -> editModuleOfCross (Just d) prog $ \(m, ms) defName def -> do
     let defs = moduleDefs m
         newNameBase = unsafeMkName nameStr

primer/src/Primer/Def/Utils.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE OverloadedLabels #-}
 
-module Primer.Def.Utils (nextID, nextIDTypeDef, globalInUse, typeInUse) where
+module Primer.Def.Utils (nextID, nextIDTypeDef, typeInUse) where
 
 import Foreword
 
@@ -9,9 +9,9 @@ import Data.Generics.Uniplate.Operations (universe)
 import Data.Set qualified as Set
 import Optics (anyOf, folded, foldlOf', to, toListOf, (%), _2)
 import Primer.Core (Expr' (..), KindMeta, Type' (..), TypeMeta, typesInExpr)
-import Primer.Core.Meta (GVarName, ID, TyConName)
+import Primer.Core.Meta (ID, TyConName)
 import Primer.Core.Type.Utils (kindIDs)
-import Primer.Core.Utils (exprIDs, freeGlobalVars, typeIDs)
+import Primer.Core.Utils (exprIDs, typeIDs)
 import Primer.Def (ASTDef (..), Def (..), defAST, defType)
 import Primer.TypeDef (ASTTypeDef (..), PrimTypeDef (PrimTypeDef), TypeDef (..), ValCon (..))
 
@@ -40,12 +40,6 @@ nextIDTypeDef (TypeDefPrim (PrimTypeDef ps _)) =
   succ $ foldlOf' (folded % _2 % kindIDs) max minBound ps
 {-# INLINE nextIDTypeDef #-}
 
-globalInUse :: Foldable f => GVarName -> f Def -> Bool
-globalInUse v =
-  anyOf
-    (folded % #_DefAST % #astDefExpr % to freeGlobalVars)
-    (Set.member v)
-
 -- | Is this type (including any of its constructors) in use in the given definitions?
 typeInUse :: (Foldable f, Foldable g, Data a', Data b') => TyConName -> ASTTypeDef a b -> f (TypeDef a' b') -> g Def -> Bool
 typeInUse defName def ts ds =

primer/test/Tests/Action/Available.hs

@@ -107,7 +107,7 @@ import Primer.Core (
   ID,
   Kind' (..),
   KindMeta,
-  ModuleName (ModuleName, unModuleName),
+  ModuleName (unModuleName),
   Pattern (PatPrim),
   TyConName,
   Type,
@@ -292,24 +292,6 @@ mkTests deps (defName, DefAST def') =
                   , sigActions
                   }
 
--- We should not offer to delete a definition that is in use, as that
--- action cannot possibly succeed
-unit_def_in_use :: Assertion
-unit_def_in_use =
-  let (d, defs) = create' $ do
-        let foo = qualifyName (ModuleName ["M"]) "foo"
-        fooDef <- ASTDef <$> emptyHole <*> tEmptyHole
-        let bar = qualifyName (ModuleName ["M"]) "bar"
-        barDef <- ASTDef <$> gvar foo <*> tEmptyHole
-        let ds = [(foo, DefAST fooDef), (bar, DefAST barDef)]
-        pure (foo, Map.fromList ds)
-   in for_
-        enumerate
-        ( \l ->
-            Available.forDef defs l Editable d
-              @?= [Available.Input Available.RenameDef, Available.NoInput Available.DuplicateDef]
-        )
-
 -- Any offered action will complete successfully,
 -- other than one with a student-specified name that introduces capture.
 tasty_available_actions_accepted :: Property

primer/test/Tests/Action/Prog.hs

@@ -250,36 +250,24 @@ unit_delete_def =
       assertNothing (lookupDef' "other" prog')
       assertJust (lookupDef' "main" prog')
 
+unit_delete_def_referenced :: Assertion
+unit_delete_def_referenced =
+  progActionTest
+    defaultEmptyProg
+    [ moveToDef "main"
+    , BodyAction [ConstructVar $ globalVarRef "other"]
+    , deleteDef "other"
+    ]
+    $ expectSuccess
+    $ \_ prog' -> do
+      assertNothing (lookupDef' "other" prog')
+      fmap (forgetMetadata . astDefExpr) (defAST =<< lookupDef' "main" prog') @?= Just (EmptyHole ())
+
 unit_delete_def_unknown_id :: Assertion
 unit_delete_def_unknown_id =
   progActionTest defaultEmptyProg [deleteDef "unknown"]
     $ expectError (@?= DefNotFound (gvn "unknown"))
 
-unit_delete_def_used_id :: Assertion
-unit_delete_def_used_id =
-  progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "other"], deleteDef "other"]
-    $ expectError (@?= DefInUse (gvn "other"))
-
-unit_delete_def_used_id_cross_module :: Assertion
-unit_delete_def_used_id_cross_module =
-  progActionTest
-    prog
-    [moveToDef "main", BodyAction [ConstructVar $ GlobalVarRef $ qualifyM "foo"], DeleteDef $ qualifyM "foo"]
-    $ expectError (@?= DefInUse (qualifyM "foo"))
-  where
-    n = ModuleName ["Module2"]
-    qualifyM = qualifyName n
-    prog = do
-      p <- defaultEmptyProg
-      e <- emptyHole
-      t <- tEmptyHole
-      let m =
-            Module n mempty
-              $ Map.singleton "foo"
-              $ DefAST
-              $ ASTDef e t
-      pure $ p & #progModules %~ (m :)
-
 -- 'foo = foo' shouldn't count as "in use" and block deleting itself
 unit_delete_def_recursive :: Assertion
 unit_delete_def_recursive =