From 900315f4182ca4277d16c60e76d8d19bc2a1fec0 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 28 Sep 2023 11:23:34 +0100 Subject: [PATCH 1/4] refactor: Generalise `deleteAt` to return deleted value Signed-off-by: George Thomas --- primer/src/Foreword.hs | 4 ++-- primer/src/Primer/App.hs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/primer/src/Foreword.hs b/primer/src/Foreword.hs index b1a9bedf6..fb934d872 100644 --- a/primer/src/Foreword.hs +++ b/primer/src/Foreword.hs @@ -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 diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8b7f0e88f..8dd9f6752 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -910,7 +910,7 @@ applyProgAction prog = \case ( maybe (throwError $ ConNotFound vcName) pure <=< findAndAdjustA ((== vcName) . valConName) - (traverseOf #valConArgs $ maybe (throwError $ IndexOutOfRange index) pure . deleteAt index) + (traverseOf #valConArgs $ maybe (throwError $ IndexOutOfRange index) pure . map fst . deleteAt index) ) td ) From be24ee196675ff5c778f2511d931cc6d61a03538 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 28 Sep 2023 14:52:50 +0100 Subject: [PATCH 2/4] fix: Use updated module in `ParamKindAction` TC context I haven't found any particular test case which is affected by this, but it seems safer, and will also make it easier to factor out this code. This appears to be an oversight from `257cb77: feat: Implement actions for editing type parameter kinds`. Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 8dd9f6752..e6d03726a 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1047,7 +1047,7 @@ applyProgAction prog = \case runExceptT ( runReaderT (checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods})) - (buildTypingContextFromModules (mod : mods <> imports) smartHoles) + (buildTypingContextFromModules (mod' : mods <> imports) smartHoles) ) >>= either (throwError . ActionError) pure pure From 775651db69e3774e5b72c5ca86c7c6fef807e418 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Thu, 28 Sep 2023 14:53:02 +0100 Subject: [PATCH 3/4] refactor: Factor out running typechecking pass for applying actions Signed-off-by: George Thomas --- primer/src/Primer/App.hs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index e6d03726a..c7c94de72 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -1043,13 +1043,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 @@ -1981,3 +1975,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 From 26aaa835f03067552098fa29898222ec76053fe8 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 28 Nov 2023 11:28:14 +0000 Subject: [PATCH 4/4] feat: Allow typedef deletions regardless of whether type is in use This includes fixing up expressions utilising the deleted type/constructor/field so that they still make sense. Mostly this involves replacing subexpressions with holes. Note that this does not yet include deleting type parameters, which we still cannot modify at all when the type is in use. But we aim to relax this restriction as well shortly. We add a unit tests for each action. Note that we didn't actually have any for the old behaviour, due to time constraints when that was implemented. Although the `tasty_available_actions_accepted` property test caught a lot of issues for us. Signed-off-by: George Thomas --- primer/src/Primer/Action/Available.hs | 26 ++--- primer/src/Primer/App.hs | 151 ++++++++++++++++++-------- primer/test/Tests/Action/Available.hs | 5 +- primer/test/Tests/Action/Prog.hs | 128 ++++++++++++++++++++++ 4 files changed, 252 insertions(+), 58 deletions(-) diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index be1cf5d4d..401bee8ec 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -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 -> @@ -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 -> @@ -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 = 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 diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index c7c94de72..7c3fa7e96 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -140,6 +140,7 @@ import Primer.Core ( CaseBranch, CaseBranch' (CaseBranch), CaseFallback, + CaseFallback' (CaseExhaustive), Expr, Expr' (Case, Con, EmptyHole, Var), GVarName, @@ -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 ( @@ -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 @@ -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' <- + ((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 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 @@ -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 @@ -900,24 +949,37 @@ 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 . map fst . 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 @@ -925,6 +987,9 @@ applyProgAction prog = \case . 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' <- diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs index 486288dff..ca36cbccb 100644 --- a/primer/test/Tests/Action/Available.hs +++ b/primer/test/Tests/Action/Available.hs @@ -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, @@ -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. diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index e891f52cc..1779f1417 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -875,6 +875,57 @@ unit_copy_paste_import = Left err -> assertFailure $ show err Right assertion -> assertion +unit_DeleteTypeDef :: Assertion +unit_DeleteTypeDef = progActionTest + ( defaultProgEditableTypeDefs + $ sequence + [ do + x <- emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) + astDef "def1" x <$> tEmptyHole + , do + x <- con cA $ replicate 3 emptyHole + astDef "def2" x <$> tEmptyHole + , do + x <- + lam "a" + $ case_ + (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) + [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole + , branch cB [("s", Nothing), ("t", Nothing)] emptyHole + ] + astDef "def3" x <$> tEmptyHole + ] + ) + [DeleteTypeDef tT] + $ expectSuccess + $ \_ prog' -> do + assertBool "type deleted" $ Map.notMember tT $ foldMap' moduleTypesQualified $ progModules prog' + def1 <- findDef (gvn "def1") prog' + forgetMetadata (astDefExpr def1) + @?= forgetMetadata + ( create' + $ emptyHole + `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tEmptyHole) + ) + def2 <- findDef (gvn "def2") prog' + forgetMetadata (astDefExpr def2) + @?= forgetMetadata + ( create' + emptyHole + ) + def3 <- findDef (gvn "def3") prog' + forgetMetadata (astDefExpr def3) + @?= forgetMetadata + ( create' + $ lam "a" + $ case_ + ( hole + $ emptyHole + `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")) + ) + [] + ) + unit_RenameType :: Assertion unit_RenameType = progActionTest @@ -1078,6 +1129,37 @@ unit_AddCon_sparse = emptyHole ) +unit_DeleteCon :: Assertion +unit_DeleteCon = progActionTest + ( defaultProgEditableTypeDefs + $ sequence + [ do + x <- + case_ + (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) + [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole + , branch cB [("s", Nothing), ("t", Nothing)] $ con cA $ replicate 3 emptyHole + ] + astDef "def" x <$> tEmptyHole + ] + ) + [DeleteCon tT cA] + $ expectSuccess + $ \_ prog' -> do + td <- findTypeDef tT prog' + astTypeDefConstructors td + @?= [ ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"] + ] + def <- findDef (gvn "def") prog' + forgetMetadata (astDefExpr def) + @?= forgetMetadata + ( create' + $ case_ + (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int"))) + [ branch cB [("s", Nothing), ("t", Nothing)] emptyHole + ] + ) + unit_AddConField :: Assertion unit_AddConField = progActionTest @@ -1160,6 +1242,52 @@ unit_AddConField_case_ann = ] ) +unit_DeleteConField :: Assertion +unit_DeleteConField = + progActionTest + ( defaultProgEditableTypeDefs $ do + x <- + case_ + ( con + cA + [ con0 (vcn "True") + , con0 (vcn "False") + , con0 (vcn "True") + ] + `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) + ) + [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole + , branch cB [("s", Nothing), ("t", Nothing)] emptyHole + ] + sequence + [ astDef "def" x <$> tEmptyHole + ] + ) + [DeleteConField tT cA 1] + $ expectSuccess + $ \_ prog' -> do + td <- findTypeDef tT prog' + astTypeDefConstructors td + @?= [ ValCon cA [TCon () (tcn "Bool"), TCon () (tcn "Bool")] + , ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"] + ] + def <- findDef (gvn "def") prog' + forgetMetadata (astDefExpr def) + @?= forgetMetadata + ( create' + $ case_ + ( con + cA + [ con0 (vcn "True") + , con0 (vcn "True") + ] + `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole) + ) + [ branch cA [("x", Nothing), ("z", Nothing)] emptyHole + , branch cB [("s", Nothing), ("t", Nothing)] emptyHole + ] + ) + unit_ConFieldAction :: Assertion unit_ConFieldAction = progActionTest