Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow typedef deletions regardless of whether type is in use #1153

Merged
merged 4 commits into from
Nov 28, 2023
Merged

Allow typedef deletions regardless of whether type is in use #1153

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
900315f
refactor: Generalise `deleteAt` to return deleted value
georgefst Sep 28, 2023
be24ee1
fix: Use updated module in `ParamKindAction` TC context
georgefst Sep 28, 2023
775651d
refactor: Factor out running typechecking pass for applying actions
georgefst Sep 28, 2023
26aaa83
feat: Allow typedef deletions regardless of whether type is in use
georgefst Nov 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions primer/src/Foreword.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,9 +122,9 @@ insertAt n y xs =

-- | Delete an element at some index, returning 'Nothing' if it is out
-- of bounds.
deleteAt :: Int -> [a] -> Maybe [a]
deleteAt :: Int -> [b] -> Maybe ([b], b)
deleteAt n xs = case splitAt n xs of
(a, _ : b) -> Just $ a ++ b
(a, b : bs) -> Just (a ++ bs, b)
_ -> Nothing

-- | Apply a function to the element at some index, returning
Expand Down
26 changes: 12 additions & 14 deletions primer/src/Primer/Action/Available.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,14 +377,11 @@ forTypeDef l Editable tydefs defs tdName td =
sortByPriority l
$ [ Input RenameType
, Input AddCon
, NoInput DeleteTypeDef
]
<> mwhen
(not $ typeInUse tdName td tydefs defs)
( [NoInput DeleteTypeDef]
<> mwhen
(l == Expert)
[Input AddTypeParam]
)
(l == Expert && not (typeInUse tdName td tydefs defs))
[Input AddTypeParam]

forTypeDefParamNode ::
TyVarName ->
Expand Down Expand Up @@ -443,12 +440,13 @@ forTypeDefConsNode ::
ASTTypeDef TypeMeta KindMeta ->
[Action]
forTypeDefConsNode _ NonEditable _ _ _ _ = mempty
forTypeDefConsNode l Editable tydefs defs tdName td =
sortByPriority l
$ [ NoInput AddConField
, Input RenameCon
]
<> mwhen (not $ typeInUse tdName td tydefs defs) [NoInput DeleteCon]
forTypeDefConsNode l Editable _ _ _ _ =
sortByPriority
l
[ NoInput AddConField
, Input RenameCon
, NoInput DeleteCon
]

forTypeDefConsFieldNode ::
ValConName ->
Expand All @@ -462,9 +460,9 @@ forTypeDefConsFieldNode ::
ASTTypeDef TypeMeta KindMeta ->
[Action]
forTypeDefConsFieldNode _ _ _ _ NonEditable _ _ _ _ = mempty
forTypeDefConsFieldNode con index id l Editable tydefs defs tdName td =
forTypeDefConsFieldNode con index id l Editable _ _ _ td =
Comment on lines -465 to +463
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe worth removing these arguments entirely?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe. I suspect we may well re-add them at some point, and even with them unused, the uniformity helps in simplifying the definition of Primer.API.availableActions. Ideally we'd probably refactor this to pass around a record for the common fields, in which case we'd be unlikely to complain that not all fields of the record are used in every function which receives it.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fair point. I don't have strong opinions either way.

sortByPriority l
$ mwhen ((view _id <$> fieldType) == Just id && not (typeInUse tdName td tydefs defs)) [NoInput DeleteConField]
$ mwhen ((view _id <$> fieldType) == Just id) [NoInput DeleteConField]
<> case findTypeOrKind id =<< fieldType of
Nothing -> mempty
Just (Left t) -> forType l t
Expand Down
168 changes: 118 additions & 50 deletions primer/src/Primer/App.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ import Primer.Core (
CaseBranch,
CaseBranch' (CaseBranch),
CaseFallback,
CaseFallback' (CaseExhaustive),
Expr,
Expr' (Case, Con, EmptyHole, Var),
GVarName,
Expand Down Expand Up @@ -176,7 +177,7 @@ import Primer.Core (
_type,
_typeMetaLens,
)
import Primer.Core.DSL (S, create)
import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
import Primer.Core.DSL qualified as DSL
import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp)
import Primer.Core.Utils (
Expand Down Expand Up @@ -633,7 +634,7 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS
Right nf -> EvalFullRespNormal nf

-- | Handle a 'ProgAction'
applyProgAction :: MonadEdit m ProgError => Prog -> ProgAction -> m Prog
applyProgAction :: forall m. MonadEdit m ProgError => Prog -> ProgAction -> m Prog
applyProgAction prog = \case
MoveToDef d -> do
m <- lookupEditableModule (qualifiedModule d) prog
Expand Down Expand Up @@ -698,14 +699,45 @@ applyProgAction prog = \case
( m{moduleTypes = tydefs'}
, Just $ SelectionTypeDef $ TypeDefSelection tc Nothing
)
DeleteTypeDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) ->
case moduleTypesQualified m Map.!? d of
Nothing -> throwError $ TypeDefNotFound d
Just (TypeDefPrim _) -> throwError $ TypeDefIsPrim d
Just (TypeDefAST td) -> do
checkTypeNotInUse d td $ m : ms
let m' = m{moduleTypes = Map.delete (baseName d) (moduleTypes m)}
pure (m' : ms, Nothing)
DeleteTypeDef d -> editModuleOfCrossType (Just d) prog $ \(m, ms) defName def -> do
let updateExpr = \case
Con _ c _ | c `elem` map valConName (astTypeDefConstructors def) -> emptyHole
e -> pure e
ms' <-
georgefst marked this conversation as resolved.
Show resolved Hide resolved
((m & over #moduleTypes (Map.delete defName)) : ms)
& ( traverseOf
(traversed % #moduleDefs % traversed % #_DefAST)
( traverseOf
#astDefExpr
( transformM (traverseOf typesInExpr updateType)
<=< transformM updateExpr
)
<=< traverseOf #astDefType updateType
)
<=< traverseOf
( traversed
% #moduleTypes
% traversed
% #_TypeDefAST
% #astTypeDefConstructors
% traversed
% #valConArgs
% traversed
)
updateType
)
-- There would otherwise be some awkward cases to patch up, such as modifying metadata in type annotations
-- to reflect the change from `KType` to `KHole`.
-- Note that this also automatically cleans up all pattern matches on this type,
-- since we will have set the type of the scrutinee to a hole,
-- and thus the typechecker removes all branches.
-- This is why we don't bother explicitly fixing up patterns in the above traversals.
ms'' <- runFullTCPass (progSmartHoles prog) (progImports prog) ms'
pure (ms'', Nothing)
where
updateType = transformM \case
TCon _ n | n == d -> tEmptyHole
e -> pure e
Comment on lines +738 to +740
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is somewhat odd to have updateExpr defined above in a let, but updateType defined below in a where. Any particular reason?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, but we mostly use where in the other cases, but updateExpr can't go there because then def would be out of scope. It's a bit weird, but I don't think it's worth changing.

RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do
when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
m' <- traverseOf #moduleTypes updateTypeDef m
Expand Down Expand Up @@ -830,24 +862,41 @@ applyProgAction prog = \case
td
)
type_
DeleteCon tdName vcName -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
m' <-
alterTypeDef
( \td -> do
checkTypeNotInUse tdName td $ m : ms
traverseOf
#astTypeDefConstructors
( \cons -> do
unless
(vcName `elem` map valConName cons)
(throwError $ ConNotFound vcName)
pure $ filter ((/= vcName) . valConName) cons
)
td
DeleteCon tdName vcName -> editModuleOfCrossType (Just tdName) prog $ \(m, ms) defName def -> do
def' <-
traverseOf
#astTypeDefConstructors
( \cons -> do
unless
(vcName `elem` map valConName cons)
(throwError $ ConNotFound vcName)
pure $ filter ((/= vcName) . valConName) cons
)
tdName
m
pure (m' : ms, Just $ SelectionTypeDef $ TypeDefSelection tdName Nothing)
def
ms' <-
((m & over #moduleTypes (Map.insert defName $ TypeDefAST def')) : ms)
& traverseOf
(traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
( transformCaseBranches
tdName
( \_ (bs, fb) ->
let bs' =
bs
& filter \case
CaseBranch (PatCon vcName') _ _ | vcName' == vcName -> False
_ -> True
in pure
( bs'
, if map (PatCon . valConName) (astTypeDefConstructors def') == map caseBranchName bs'
then CaseExhaustive
else fb
)
)
<=< transformM \case
Con _ c _ | c == vcName -> emptyHole
e -> pure e
)
pure (ms', Just $ SelectionTypeDef $ TypeDefSelection tdName Nothing)
AddConField type_ con index new ->
editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
m' <- updateTypeDef m
Expand Down Expand Up @@ -900,31 +949,47 @@ applyProgAction prog = \case
newName <- LocalName <$> freshName (freeVars e)
binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
pure $ CaseBranch vc binds' e
DeleteConField tdName vcName index -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
m' <-
alterTypeDef
( \td -> do
checkTypeNotInUse tdName td $ m : ms
traverseOf
#astTypeDefConstructors
( maybe (throwError $ ConNotFound vcName) pure
<=< findAndAdjustA
((== vcName) . valConName)
(traverseOf #valConArgs $ maybe (throwError $ IndexOutOfRange index) pure . deleteAt index)
)
td
DeleteConField tdName vcName index -> editModuleOfCrossType (Just tdName) prog $ \(m, ms) defName def -> do
def' <-
traverseOf
#astTypeDefConstructors
( maybe (throwError $ ConNotFound vcName) pure
<=< findAndAdjustA
((== vcName) . valConName)
(traverseOf #valConArgs $ map fst . deleteIndex)
)
tdName
m
def
ms' <-
((m & over #moduleTypes (Map.insert defName $ TypeDefAST def')) : ms)
& traverseOf
(traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
( transformNamedCaseBranch
tdName
vcName
( \_ (CaseBranch vc binds e) -> do
(binds', Bind _ var) <- deleteIndex binds
CaseBranch vc binds'
<$> ( e & traverseOf _freeTmVars \case
(_, v) | v == var -> emptyHole
(meta, v) -> pure $ Var meta $ LocalVarRef v
)
)
<=< transformM \case
Con meta c es | c == vcName -> map (Con meta c . fst) $ deleteIndex es
e -> pure e
)
pure
( m' : ms
( ms'
, Just
. SelectionTypeDef
. TypeDefSelection tdName
. Just
. TypeDefConsNodeSelection
$ TypeDefConsSelection vcName Nothing
)
where
deleteIndex :: [a] -> m ([a], a)
deleteIndex = maybe (throwError $ IndexOutOfRange index) pure . deleteAt index
AddTypeParam tdName index paramName0 k -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
let paramName = unsafeMkLocalName paramName0
m' <-
Expand Down Expand Up @@ -1043,13 +1108,7 @@ applyProgAction prog = \case
Right (def', kz) -> do
let mod' = mod & over #moduleTypes (Map.insert defName $ TypeDefAST def')
imports = progImports prog
mods' <-
runExceptT
( runReaderT
(checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}))
(buildTypingContextFromModules (mod : mods <> imports) smartHoles)
)
>>= either (throwError . ActionError) pure
mods' <- runFullTCPass smartHoles imports (mod' : mods)
pure
( mods'
, Just
Expand Down Expand Up @@ -1981,3 +2040,12 @@ allTyConNames = fmap fst . allConNames
-- change in the future.
nextProgID :: Prog -> ID
nextProgID p = foldl' (\id_ m -> max (nextModuleID m) id_) minBound (progModules p)

runFullTCPass :: MonadEdit m ProgError => SmartHoles -> [Module] -> [Module] -> m [Module]
runFullTCPass smartHoles imports mods =
runExceptT
( runReaderT
(checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mods}))
(buildTypingContextFromModules (mods <> imports) smartHoles)
)
>>= either (throwError . ActionError) pure
5 changes: 4 additions & 1 deletion primer/test/Tests/Action/Available.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ import Primer.App (
)
import Primer.App qualified as App
import Primer.App.Base (TypeDefConsFieldSelection (..))
import Primer.App.Utils (forgetProgTypecache)
import Primer.Builtins (builtinModuleName, cCons, cFalse, cTrue, tBool, tList, tNat)
import Primer.Core (
Expr,
Expand Down Expand Up @@ -533,7 +534,9 @@ data SucceedOrCapture a
ensureSHNormal :: App -> PropertyT WT ()
ensureSHNormal a = case checkAppWellFormed a of
Left err -> annotateShow err >> failure
Right a' -> TypeCacheAlpha a === TypeCacheAlpha a'
Right a' ->
TypeCacheAlpha (forgetProgTypecache $ appProg a)
=== TypeCacheAlpha (forgetProgTypecache $ appProg a')

genLoc ::
forall m.
Expand Down
Loading