From b4e0d3ba4b8aa480d1e222cb00a91d09895586b7 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Wed, 27 Apr 2022 14:49:53 +0100 Subject: [PATCH 1/6] refactor: error handling in applyProgAction We consistently handle "not found" errors. This is in preparation for adding multiple editable modules. Thus we add some new errors `ModuleNotFound` and `ModuleReadonly` and use these as appropriate. Note that this may change some errors the API returns. --- primer/src/Primer/App.hs | 512 ++++++++++++++++++++------------------- 1 file changed, 259 insertions(+), 253 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index afaeb537e..ba414feee 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -122,7 +122,6 @@ import Primer.Core ( defName, defPrim, getID, - moduleNamePretty, qualifyName, typeDefAST, typesInExpr, @@ -268,16 +267,6 @@ addDef d p = mod' = insertDef mod $ DefAST d in p{progModule = mod'} --- | Add a type definition to the editable module --- assumes the def has the correct name to go in the editable module -addTypeDef :: ASTTypeDef -> Prog -> Prog -addTypeDef t p = - let mod = progModule p - tydefs = moduleTypes mod - tydefs' = tydefs <> mkTypeDefMap [TypeDefAST t] - mod' = mod{moduleTypes = tydefs'} - in p{progModule = mod'} - -- | The action log -- This is the canonical store of the program - we can recreate any current or -- past program state by replaying this log. @@ -353,6 +342,9 @@ data ProgError | IndexOutOfRange Int | -- | Cannot rename a module to the same name as some other module RenameModuleNameClash + | ModuleNotFound ModuleName + | -- | Cannot edit an imported module + ModuleReadonly ModuleName deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ProgError @@ -487,14 +479,15 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS -- provided for convenience: it is the same as the one in the progSelection. applyProgAction :: MonadEdit m => Prog -> Maybe GVarName -> ProgAction -> m Prog applyProgAction prog mdefName = \case - MoveToDef d -> case Map.lookup d (moduleDefsQualified $ progModule prog) of - Nothing -> throwError $ DefNotFound d - Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing - DeleteDef d -> - case deleteDef (progModule prog) d of + MoveToDef d -> do + m <- lookupEditableModule (qualifiedModule d) prog + case Map.lookup d $ moduleDefsQualified m of + Nothing -> throwError $ DefNotFound d + Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing + DeleteDef d -> editModule (qualifiedModule d) prog $ \m -> + case deleteDef m d of Nothing -> throwError $ DefNotFound d Just mod' -> do - let prog' = prog{progModule = mod', progSelection = Nothing} -- Run a full TC solely to ensure that no references to the removed id -- remain. This is rather inefficient and could be improved in the -- future. @@ -502,30 +495,24 @@ applyProgAction prog mdefName = \case checkEverything @TypeError NoSmartHoles CheckEverything{trusted = progImports prog, toCheck = [mod']} - pure prog' - RenameDef d nameStr -> case lookupASTDef d (moduleDefsQualified $ progModule prog) of - Nothing -> throwError $ DefNotFound d - Just def -> do - let defs = moduleDefs $ progModule prog - oldNameBase = baseName d - newNameBase = unsafeMkName nameStr - newName = qualifyName (moduleName $ progModule prog) newNameBase - if Map.member newNameBase defs - then throwError $ DefAlreadyExists newName - else do - let def' = DefAST def{astDefName = newName} - defs' <- - maybe (throwError $ ActionError NameCapture) pure $ - traverse - ( traverseOf (#_DefAST % #astDefExpr) $ - renameVar (GlobalVarRef d) (GlobalVarRef newName) - ) - (Map.insert newNameBase def' $ Map.delete oldNameBase defs) - let prog' = - prog - & #progSelection ?~ Selection (defName def') Nothing - & #progModule % #moduleDefs .~ defs' - pure prog' + pure (mod', Nothing) + RenameDef d nameStr -> editModuleOf (Just d) prog $ \m def -> do + let defs = moduleDefs m + oldNameBase = baseName d + newNameBase = unsafeMkName nameStr + newName = qualifyName (moduleName m) newNameBase + if Map.member newNameBase defs + then throwError $ DefAlreadyExists newName + else do + let def' = DefAST def{astDefName = newName} + defs' <- + maybe (throwError $ ActionError NameCapture) pure $ + traverse + ( traverseOf (#_DefAST % #astDefExpr) $ + renameVar (GlobalVarRef d) (GlobalVarRef newName) + ) + (Map.insert newNameBase def' $ Map.delete oldNameBase defs) + pure (m{moduleDefs = defs'}, Just $ Selection (defName def') Nothing) CreateDef n -> do let mod = progModule prog let modName = moduleName mod @@ -542,13 +529,9 @@ applyProgAction prog mdefName = \case ty <- newType let def = ASTDef name expr ty pure $ addDef def prog{progSelection = Just $ Selection name Nothing} - AddTypeDef td -> do - -- The frontend should never let this error happen, - -- so we just dump out a raw string for debugging/logging purposes - let m = moduleName $ progModule prog - unless (m == qualifiedModule (astTypeDefName td)) $ - throwError $ TypeDefError $ "Cannot create a type definition with incorrect module name: expected " <> moduleNamePretty m - addTypeDef td prog + AddTypeDef td -> editModuleSameSelection (qualifiedModule $ astTypeDefName td) prog $ \m -> do + let tydefs' = moduleTypes m <> mkTypeDefMap [TypeDefAST td] + m{moduleTypes = tydefs'} <$ liftError -- The frontend should never let this error case happen, -- so we just dump out a raw string for debugging/logging purposes @@ -562,13 +545,9 @@ applyProgAction prog mdefName = \case (checkTypeDefs $ mkTypeDefMapQualified [TypeDefAST td]) (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) ) - RenameType old (unsafeMkName -> nameRaw) -> do - traverseOf - #progModule - ( traverseOf #moduleTypes (updateType <=< pure . updateRefsInTypes) - <=< pure . over (#moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) - ) - prog + RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelection (qualifiedModule old) prog $ \m -> do + m' <- traverseOf #moduleTypes (updateType <=< pure . updateRefsInTypes) m + pure $ over (#moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) m' where new = qualifyName (qualifiedModule old) nameRaw updateType m = do @@ -593,14 +572,11 @@ applyProgAction prog mdefName = \case #astDefExpr $ transform $ over typesInExpr $ transform $ over (#_TCon % _2) updateName updateName n = if n == old then new else n - RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> do - when (new `elem` allConNames prog) $ throwError $ ConAlreadyExists new - traverseOf - #progModule - ( updateType - <=< traverseOf #moduleDefs (pure . updateDefs) - ) - prog + RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> + editModuleSameSelection (qualifiedModule type_) prog $ \m -> do + when (new `elem` allConNames prog) $ throwError $ ConAlreadyExists new + m' <- updateType m + pure $ over #moduleDefs updateDefs m' where updateType = alterTypeDef @@ -617,11 +593,8 @@ applyProgAction prog mdefName = \case over (#_Con % _2) updateName . over (#_Case % _3 % traversed % #_CaseBranch % _1) updateName updateName n = if n == old then new else n - RenameTypeParam type_ old (unsafeMkLocalName -> new) -> do - traverseOf - #progModule - updateType - prog + RenameTypeParam type_ old (unsafeMkLocalName -> new) -> + editModuleSameSelection (qualifiedModule type_) prog updateType where updateType = alterTypeDef @@ -647,16 +620,14 @@ applyProgAction prog mdefName = \case ) $ over _freeVarsTy $ \(_, v) -> TVar () $ updateName v updateName n = if n == old then new else n - AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> do - when (con `elem` allConNames prog) $ throwError $ ConAlreadyExists con - traverseOf - #progModule - ( traverseOf - (#moduleDefs % traversed % #_DefAST % #astDefExpr) - updateDefs - <=< updateType - ) - prog + AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> + editModuleSameSelection (qualifiedModule type_) prog $ \m -> do + when (con `elem` allConNames prog) $ throwError $ ConAlreadyExists con + m' <- updateType m + traverseOf + (#moduleDefs % traversed % #_DefAST % #astDefExpr) + updateDefs + m' where updateDefs = transformCaseBranches prog type_ $ \bs -> do m' <- DSL.meta @@ -668,13 +639,9 @@ applyProgAction prog mdefName = \case (maybe (throwError $ IndexOutOfRange index) pure . insertAt index (ValCon con [])) ) type_ - SetConFieldType type_ con index new -> do - traverseOf - #progModule - ( traverseOf #moduleDefs updateDefs - <=< updateType - ) - prog + SetConFieldType type_ con index new -> + editModuleSameSelection (qualifiedModule type_) prog $ + traverseOf #moduleDefs updateDefs <=< updateType where updateType = alterTypeDef @@ -721,13 +688,9 @@ applyProgAction prog mdefName = \case ) e else pure cb - AddConField type_ con index new -> do - traverseOf - #progModule - ( traverseOf #moduleDefs updateDefs - <=< updateType - ) - prog + AddConField type_ con index new -> + editModuleSameSelection (qualifiedModule type_) prog $ + traverseOf #moduleDefs updateDefs <=< updateType where updateType = alterTypeDef @@ -768,54 +731,45 @@ applyProgAction prog mdefName = \case binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds pure $ CaseBranch vc binds' e else pure cb - BodyAction actions -> do - withDef mdefName prog $ \def -> do - let smartHoles = progSmartHoles prog - res <- applyActionsToBody smartHoles (progAllModules prog) def actions - case res of - Left err -> throwError $ ActionError err - Right (def', z) -> do - let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z - nodeId = either getID getID meta - let prog' = - addDef - def' - prog - { progSelection = - Just $ - Selection (astDefName def') $ - Just - NodeSelection - { nodeType = BodyNode - , nodeId - , meta - } + BodyAction actions -> editModuleOf mdefName prog $ \m def -> do + let smartHoles = progSmartHoles prog + res <- applyActionsToBody smartHoles (progAllModules prog) def actions + case res of + Left err -> throwError $ ActionError err + Right (def', z) -> do + let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z + nodeId = either getID getID meta + pure + ( insertDef m (DefAST def') + , Just $ + Selection (astDefName def') $ + Just + NodeSelection + { nodeType = BodyNode + , nodeId + , meta } - pure prog' - SigAction actions -> do - withDef mdefName prog $ \def -> do - let smartHoles = progSmartHoles prog - res <- applyActionsToTypeSig smartHoles (progImports prog) (progModule prog) def actions - case res of - Left err -> throwError $ ActionError err - Right (def', mod', zt) -> do - let node = target zt - meta = view _typeMetaLens node - nodeId = getID meta - prog' = - prog - { progModule = mod' - , progSelection = - Just $ - Selection (astDefName def') $ - Just - NodeSelection - { nodeType = SigNode - , nodeId - , meta = Right meta - } - } - in pure prog' + ) + SigAction actions -> editModuleOf mdefName prog $ \m def -> do + let smartHoles = progSmartHoles prog + res <- applyActionsToTypeSig smartHoles (progImports prog) m def actions + case res of + Left err -> throwError $ ActionError err + Right (def', mod', zt) -> do + let node = target zt + meta = view _typeMetaLens node + nodeId = getID meta + in pure + ( mod' + , Just $ + Selection (astDefName def') $ + Just + NodeSelection + { nodeType = SigNode + , nodeId + , meta = Right meta + } + ) SetSmartHoles smartHoles -> pure $ prog & #progSmartHoles .~ smartHoles CopyPasteSig fromIds setup -> case mdefName of @@ -850,16 +804,53 @@ applyProgAction prog mdefName = \case data RenameMods a = RM {imported :: [a], editable :: a} deriving (Functor, Foldable, Traversable) --- Look up the definition by its given Name, then run the given action with it --- only looks in the editable module -withDef :: MonadError ProgError m => Maybe GVarName -> Prog -> (ASTDef -> m a) -> m a -withDef mdefName prog f = - case mdefName of - Nothing -> throwError NoDefSelected - Just defname -> do - case lookupASTDef defname (moduleDefsQualified $ progModule prog) of - Nothing -> throwError $ DefNotFound defname - Just def -> f def +lookupEditableModule :: MonadError ProgError m => ModuleName -> Prog -> m Module +lookupEditableModule n p = + lookupModule' n p >>= \case + Editable m -> pure m + Imported _ -> throwError $ ModuleReadonly n + +-- | Describes return type of successfully looking a module up in the program. +-- We get the module and also whether it is imported or not. +data ModuleLookup = Editable Module | Imported Module + +lookupModule' :: MonadError ProgError m => ModuleName -> Prog -> m ModuleLookup +lookupModule' n p = case (n == moduleName (progModule p), find ((n ==) . moduleName) (progImports p)) of + (True, _) -> pure $ Editable (progModule p) + (False, Just m) -> pure $ Imported m + (False, Nothing) -> throwError $ ModuleNotFound n + +editModule :: + MonadError ProgError m => + ModuleName -> + Prog -> + (Module -> m (Module, Maybe Selection)) -> + m Prog +editModule n p f = do + m <- lookupEditableModule n p + (m', s) <- f m + pure $ p{progModule = m', progSelection = s} + +editModuleSameSelection :: + MonadError ProgError m => + ModuleName -> + Prog -> + (Module -> m Module) -> + m Prog +editModuleSameSelection n p f = editModule n p (fmap (,progSelection p) . f) + +editModuleOf :: + MonadError ProgError m => + Maybe GVarName -> + Prog -> + (Module -> ASTDef -> m (Module, Maybe Selection)) -> + m Prog +editModuleOf mdefName prog f = case mdefName of + Nothing -> throwError NoDefSelected + Just defname -> editModule (qualifiedModule defname) prog $ \m -> + case Map.lookup (baseName defname) (moduleDefs m) of + Just (DefAST def) -> f m def + _ -> throwError $ DefNotFound defname -- | Undo the last block of actions. -- If there are no actions in the log we return the program unchanged. @@ -1077,31 +1068,35 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do Left (Right zt) -> pure $ Left zt Right zt -> pure $ Right zt let smartHoles = progSmartHoles p - -- We intentionally throw away any changes in doneSetup other than via 'tgt' - -- as these could be in other definitions referencing this one, due to - -- types changing. However, we are going to do a full tc pass anyway, - -- which will pick up any problems. It is better to do it in one batch, - -- in case the intermediate state after 'setup' causes more problems - -- than the final state does. - (oldDef, doneSetup) <- withDef (Just toDefName) p $ \def -> (def,) <$> applyActionsToTypeSig smartHoles (progImports p) (progModule p) def setup - tgt <- case doneSetup of - Left err -> throwError $ ActionError err - Right (_, _, tgt) -> pure $ focusOnlyType tgt - let sharedScope = - if fromDefName == toDefName -- optimization only - then getSharedScopeTy c $ Right tgt - else mempty - -- Delete unbound vars - let cTgt = either target target c - f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) - cScoped <- traverseOf _freeVarsTy f cTgt - freshCopy <- traverseOf (_typeMeta % _id) (const fresh) cScoped - pasted <- case target tgt of - TEmptyHole _ -> pure $ replace freshCopy tgt - _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - let newDef = oldDef{astDefType = fromZipper pasted} - let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) - let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)} + finalProg <- editModuleOf (Just toDefName) p $ \mod oldDef -> do + -- We intentionally throw away any changes in doneSetup other than via 'tgt' + -- as these could be in other definitions referencing this one, due to + -- types changing. However, we are going to do a full tc pass anyway, + -- which will pick up any problems. It is better to do it in one batch, + -- in case the intermediate state after 'setup' causes more problems + -- than the final state does. + doneSetup <- applyActionsToTypeSig smartHoles (progImports p) mod oldDef setup + tgt <- case doneSetup of + Left err -> throwError $ ActionError err + Right (_, _, tgt) -> pure $ focusOnlyType tgt + let sharedScope = + if fromDefName == toDefName -- optimization only + then getSharedScopeTy c $ Right tgt + else mempty + -- Delete unbound vars + let cTgt = either target target c + f (m, n) = + if Set.member (unLocalName n) sharedScope + then pure $ TVar m n + else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) + cScoped <- traverseOf _freeVarsTy f cTgt + freshCopy <- traverseOf (_typeMeta % _id) (const fresh) cScoped + pasted <- case target tgt of + TEmptyHole _ -> pure $ replace freshCopy tgt + _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" + let newDef = oldDef{astDefType = fromZipper pasted} + let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) + pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel)) tcWholeProg finalProg -- We cannot use bindersAbove as that works on names only, and different scopes @@ -1200,85 +1195,96 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do Left (Right t) -> Right (Left t) Right t -> Right (Right t) let smartHoles = progSmartHoles p - -- The Loc zipper captures all the changes, they are only reflected in the - -- returned Def, which we thus ignore - (oldDef, doneSetup) <- withDef (Just toDefName) p $ \def -> (def,) <$> applyActionsToBody smartHoles (progAllModules p) def setup - tgt <- case doneSetup of - Left err -> throwError $ ActionError err - Right (_, tgt) -> pure tgt - case (src, tgt) of - (_, InBind _) -> throwError $ CopyPasteError "tried to paste an expression into a binder" - (Left _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type" - (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression" - (Right srcT, InType tgtT) -> do - let sharedScope = - if fromDefName == toDefName -- optimization only - then getSharedScopeTy srcT $ Left tgtT - else mempty - -- Delete unbound vars. TODO: we may want to let-bind them? - let srcSubtree = either target target srcT - f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) - scopedCopy <- traverseOf _freeVarsTy f srcSubtree - freshCopy <- traverseOf (_typeMeta % _id) (const fresh) scopedCopy - pasted <- case target tgtT of - TEmptyHole _ -> pure $ replace freshCopy tgtT - _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted} - let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) - let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)} - tcWholeProg finalProg - (Left srcE, InExpr tgtE) -> do - let sharedScope = - if fromDefName == toDefName -- optimization only - then getSharedScope srcE tgtE - else mempty - -- Delete unbound vars. TODO: we may want to let-bind them? - let tm (m, n) = if Set.member (unLocalName n) sharedScope then pure $ Var m $ LocalVarRef n else fresh <&> \i -> EmptyHole (Meta i Nothing Nothing) - ty (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) - scopedCopy <- traverseOf _freeTyVars ty =<< traverseOf _freeTmVars tm (target srcE) - freshCopy <- traverseOf (_exprTypeMeta % _id) (const fresh) =<< traverseOf (_exprMeta % _id) (const fresh) scopedCopy - -- TODO: need to care about types and directions here (and write tests for this caring!) - {- - - Currently, with smart holes, nothing will go too wrong (i.e. no crashes/rejections happen), but if - - smartholes were turned off (which currently needs changing in the source code, then things could go wrong, and the TC throws errors. - - The cases we need to consider are (note that the metadata gives us what type each subtree was chk/syn (could be Nothing, due to our - - represention, but we can consider that as a hole) - - NB: as we always paste into a hole, it will always synth ?, but it may also have been checked against a concrete type - - From To Want - - e ∈ T ∈ ? e if T is ? (or maybe don't special-case this, for consistency?) - - {? e ?} otherwise, to avoid "jumpy holes" (paste a 2∈Nat into '? True', would get '2 {? True ?}', but want '{? 2 ?} True', probably? - - T ∋ t ∈ ? t : ? if T is ? (or maybe don't special-case this, for consistency?) - - {? t : T ?} otherwise (avoid jumpy holes, as above) - - e ∈ T R ∋ e if this would TC (i.e. T and R are consistent) - - {? e ?} otherwise - - T ∋ t R ∋ t if this would TC (i.e. if T is more specific than R, I expect) - - {? t : T ?} otherwise - - - - Let's also tabulate what smartholes would give - - From To Want SH gives Example ('raise' the term in >e<) - - e ∈ T ∈ ? e if T is ? e - -!!! {? e ?} otherwise e, and jumpy holes. (? : ? -> Bool -> ?) >Succ< True - - T ∋ t ∈ ? t : ? if T is ? t : ? ? >λx.?< ? - -!!! {? t : T ?} otherwise t : ? (? : (Bool -> Bool) -> ?) >λx.?< ? - - e ∈ T R ∋ e if would TC e Bool ∋ not >not True< [using extra not so obv. syn, even if ctors are chk only] - - {? e ?} otherwise {? e ?} Bool ∋ >isEven< ? - - T ∋ t R ∋ t if would TC t Bool -> Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)< - -!!! {? t : T ?} otherwise {? t : ? ?} Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)< - - - - We could also consider what to do with embeddings: R ∋ e ∈ T: what happens for - - Bool ∋ even >(add 0 0)< [use add so obv. syn, even if ctors are chk only] - - ? - - - - so with SH, we are almost doing well, except we have a case of jumpy holes, and some cases of losing type information, - - denoted by !!! above - -} - pasted <- case target tgtE of - EmptyHole _ -> pure $ replace freshCopy tgtE - _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - let newDef = oldDef{astDefExpr = unfocusExpr pasted} - let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left) - let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)} - tcWholeProg finalProg + finalProg <- editModuleOf (Just toDefName) p $ \mod oldDef -> do + -- The Loc zipper captures all the changes, they are only reflected in the + -- returned Def, which we thus ignore + doneSetup <- applyActionsToBody smartHoles (progAllModules p) oldDef setup + tgt <- case doneSetup of + Left err -> throwError $ ActionError err + Right (_, tgt) -> pure tgt + case (src, tgt) of + (_, InBind _) -> throwError $ CopyPasteError "tried to paste an expression into a binder" + (Left _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type" + (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression" + (Right srcT, InType tgtT) -> do + let sharedScope = + if fromDefName == toDefName -- optimization only + then getSharedScopeTy srcT $ Left tgtT + else mempty + -- Delete unbound vars. TODO: we may want to let-bind them? + let srcSubtree = either target target srcT + f (m, n) = + if Set.member (unLocalName n) sharedScope + then pure $ TVar m n + else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) + scopedCopy <- traverseOf _freeVarsTy f srcSubtree + freshCopy <- traverseOf (_typeMeta % _id) (const fresh) scopedCopy + pasted <- case target tgtT of + TEmptyHole _ -> pure $ replace freshCopy tgtT + _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" + let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted} + let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) + pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel)) + (Left srcE, InExpr tgtE) -> do + let sharedScope = + if fromDefName == toDefName -- optimization only + then getSharedScope srcE tgtE + else mempty + -- Delete unbound vars. TODO: we may want to let-bind them? + let tm (m, n) = + if Set.member (unLocalName n) sharedScope + then pure $ Var m $ LocalVarRef n + else fresh <&> \i -> EmptyHole (Meta i Nothing Nothing) + ty (m, n) = + if Set.member (unLocalName n) sharedScope + then pure $ TVar m n + else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing) + scopedCopy <- traverseOf _freeTyVars ty =<< traverseOf _freeTmVars tm (target srcE) + freshCopy <- + traverseOf (_exprTypeMeta % _id) (const fresh) + =<< traverseOf (_exprMeta % _id) (const fresh) scopedCopy + -- TODO: need to care about types and directions here (and write tests for this caring!) + {- + - Currently, with smart holes, nothing will go too wrong (i.e. no crashes/rejections happen), but if + - smartholes were turned off (which currently needs changing in the source code, then things could go wrong, and the TC throws errors. + - The cases we need to consider are (note that the metadata gives us what type each subtree was chk/syn (could be Nothing, due to our + - represention, but we can consider that as a hole) + - NB: as we always paste into a hole, it will always synth ?, but it may also have been checked against a concrete type + - From To Want + - e ∈ T ∈ ? e if T is ? (or maybe don't special-case this, for consistency?) + - {? e ?} otherwise, to avoid "jumpy holes" (paste a 2∈Nat into '? True', would get '2 {? True ?}', but want '{? 2 ?} True', probably? + - T ∋ t ∈ ? t : ? if T is ? (or maybe don't special-case this, for consistency?) + - {? t : T ?} otherwise (avoid jumpy holes, as above) + - e ∈ T R ∋ e if this would TC (i.e. T and R are consistent) + - {? e ?} otherwise + - T ∋ t R ∋ t if this would TC (i.e. if T is more specific than R, I expect) + - {? t : T ?} otherwise + - + - Let's also tabulate what smartholes would give + - From To Want SH gives Example ('raise' the term in >e<) + - e ∈ T ∈ ? e if T is ? e + -!!! {? e ?} otherwise e, and jumpy holes. (? : ? -> Bool -> ?) >Succ< True + - T ∋ t ∈ ? t : ? if T is ? t : ? ? >λx.?< ? + -!!! {? t : T ?} otherwise t : ? (? : (Bool -> Bool) -> ?) >λx.?< ? + - e ∈ T R ∋ e if would TC e Bool ∋ not >not True< [using extra not so obv. syn, even if ctors are chk only] + - {? e ?} otherwise {? e ?} Bool ∋ >isEven< ? + - T ∋ t R ∋ t if would TC t Bool -> Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)< + -!!! {? t : T ?} otherwise {? t : ? ?} Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)< + - + - We could also consider what to do with embeddings: R ∋ e ∈ T: what happens for + - Bool ∋ even >(add 0 0)< [use add so obv. syn, even if ctors are chk only] + - ? + - + - so with SH, we are almost doing well, except we have a case of jumpy holes, and some cases of losing type information, + - denoted by !!! above + -} + pasted <- case target tgtE of + EmptyHole _ -> pure $ replace freshCopy tgtE + _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" + let newDef = oldDef{astDefExpr = unfocusExpr pasted} + let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left) + pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel)) + tcWholeProg finalProg lookupASTDef :: GVarName -> DefMap -> Maybe ASTDef lookupASTDef name = defAST <=< Map.lookup name From 14f1e149748c47006152e516775c37e8d97df884 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Thu, 5 May 2022 15:20:23 +0100 Subject: [PATCH 2/6] feat!: CreateDef, RenameModule can target any module Currently they will return an error if they target anything other than the one editable module. However, we will shortly enable multiple editable modules, at which point we need to explicitly state what module they should affect. BREAKING CHANGE: this change requires a database migration, as it changes the representation of `Log`. However, since this is just serialised to json and stored as a blob in the DB, it requires no schema changes. Since we have no programs we need to preserve, we decided not to bother with a migration. This means that DBs created before this commit will not load with a primer containing this commit. This commit also changes Primer's API. --- primer/src/Primer/Action.hs | 4 +-- primer/src/Primer/Action/Available.hs | 2 +- primer/src/Primer/App.hs | 20 ++++-------- primer/test/Tests/Action/Prog.hs | 44 ++++++++++++++++++++++++--- 4 files changed, 49 insertions(+), 21 deletions(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 1b75720f6..756f546e8 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -387,7 +387,7 @@ data ProgAction | -- | Rename the definition with the given (base) Name RenameDef GVarName Text | -- | Create a new definition - CreateDef (Maybe Text) + CreateDef ModuleName (Maybe Text) | -- | Delete a new definition DeleteDef GVarName | -- | Add a new type definition @@ -423,7 +423,7 @@ data ProgAction CopyPasteSig (GVarName, ID) [Action] | CopyPasteBody (GVarName, ID) [Action] | -- | Renames the sole editable module - RenameModule (NonEmpty Text) + RenameModule ModuleName (NonEmpty Text) deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ProgAction diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs index 5d065ae93..22b471460 100644 --- a/primer/src/Primer/Action/Available.hs +++ b/primer/src/Primer/Action/Available.hs @@ -100,7 +100,7 @@ actionsForDef l defs def = qn = astDefName def copyName = uniquifyDefName (qualifiedModule qn) (unName (baseName qn) <> "Copy") defs in NoInputRequired - [ CreateDef (Just copyName) + [ CreateDef (qualifiedModule $ astDefName def) (Just copyName) , CopyPasteSig (astDefName def, sigID) [] , CopyPasteBody (astDefName def, bodyID) [] ] diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index ba414feee..d3b8f5068 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -259,14 +259,6 @@ allTypes p = foldMap moduleTypesQualified $ progAllModules p allDefs :: Prog -> DefMap allDefs p = foldMap moduleDefsQualified $ progAllModules p --- | Add a definition to the editable module --- assumes the def has the correct name to go in the editable module -addDef :: ASTDef -> Prog -> Prog -addDef d p = - let mod = progModule p - mod' = insertDef mod $ DefAST d - in p{progModule = mod'} - -- | The action log -- This is the canonical store of the program - we can recreate any current or -- past program state by replaying this log. @@ -513,9 +505,7 @@ applyProgAction prog mdefName = \case ) (Map.insert newNameBase def' $ Map.delete oldNameBase defs) pure (m{moduleDefs = defs'}, Just $ Selection (defName def') Nothing) - CreateDef n -> do - let mod = progModule prog - let modName = moduleName mod + CreateDef modName n -> editModule modName prog $ \mod -> do let defs = moduleDefs mod name <- case n of Just nameStr -> @@ -528,7 +518,7 @@ applyProgAction prog mdefName = \case expr <- newExpr ty <- newType let def = ASTDef name expr ty - pure $ addDef def prog{progSelection = Just $ Selection name Nothing} + pure (insertDef mod $ DefAST def, Just $ Selection name Nothing) AddTypeDef td -> editModuleSameSelection (qualifiedModule $ astTypeDefName td) prog $ \m -> do let tydefs' = moduleTypes m <> mkTypeDefMap [TypeDefAST td] m{moduleTypes = tydefs'} @@ -778,9 +768,11 @@ applyProgAction prog mdefName = \case CopyPasteBody fromIds setup -> case mdefName of Nothing -> throwError NoDefSelected Just i -> copyPasteBody prog fromIds i setup - RenameModule newName -> + RenameModule oldName newName -> do + -- Call editModuleSameSelection solely for checking that 'oldName' + -- is an editable module + _ <- editModuleSameSelection oldName prog pure let n = ModuleName $ unsafeMkName <$> newName - oldName = moduleName $ progModule prog curMods = RM{imported = progImports prog, editable = progModule prog} in if n == oldName then pure prog diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 50cafd414..65121f783 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -217,7 +217,7 @@ unit_construct_let_without_moving_to_def_first = progActionTest defaultEmptyProg [BodyAction [ConstructLet (Just "x")]] $ expectError (@?= NoDefSelected) unit_create_def :: Assertion -unit_create_def = progActionTest defaultEmptyProg [CreateDef $ Just "newDef"] $ +unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] $ expectSuccess $ \_ prog' -> do case lookupASTDef' "newDef" (moduleDefs $ progModule prog') of Nothing -> assertFailure $ show $ moduleDefs $ progModule prog' @@ -227,9 +227,27 @@ unit_create_def = progActionTest defaultEmptyProg [CreateDef $ Just "newDef"] $ unit_create_def_clash_prim :: Assertion unit_create_def_clash_prim = - progActionTest defaultFullProg [CreateDef $ Just "toUpper"] $ + progActionTest defaultFullProg [CreateDef mainModuleName $ Just "toUpper"] $ expectError (@?= DefAlreadyExists (gvn "toUpper")) +unit_create_def_nonexistant_module :: Assertion +unit_create_def_nonexistant_module = + let nonExistantModule = ModuleName ["NonExistantModule"] + in progActionTest defaultEmptyProg [CreateDef nonExistantModule $ Just "newDef"] $ + expectError (@?= ModuleNotFound nonExistantModule) + +unit_create_def_imported_module :: Assertion +unit_create_def_imported_module = + let builtins = ModuleName ["Builtins"] + test = do + importModules [builtinModule] + handleEditRequest [CreateDef builtins $ Just "newDef"] + a = newEmptyApp + in do + case fst $ runAppTestM (ID $ appIdCounter a) a test of + Left err -> err @?= ModuleReadonly builtins + Right _ -> assertFailure "Expected CreateDef to complain about module being read-only" + unit_create_typedef :: Assertion unit_create_typedef = let lst = @@ -1265,7 +1283,7 @@ unit_rename_module = handleEditRequest [ moveToDef "main" , BodyAction [ConstructVar $ globalVarRef "main"] - , RenameModule ["Module2"] + , RenameModule mainModuleName ["Module2"] ] a = newEmptyApp in case fst $ runAppTestM (ID $ appIdCounter a) a test of @@ -1286,7 +1304,7 @@ unit_rename_module_clash :: Assertion unit_rename_module_clash = let test = do importModules [builtinModule] - handleEditRequest [RenameModule ["Builtins"]] + handleEditRequest [RenameModule mainModuleName ["Builtins"]] a = newEmptyApp in do unModuleName (moduleName builtinModule) @?= ["Builtins"] @@ -1294,6 +1312,24 @@ unit_rename_module_clash = Left err -> err @?= RenameModuleNameClash Right _ -> assertFailure "Expected RenameModule to error, since module names clash with prior import" +unit_rename_module_nonexistant :: Assertion +unit_rename_module_nonexistant = + let nonExistantModule = ModuleName ["NonExistantModule"] + in progActionTest defaultEmptyProg [RenameModule nonExistantModule ["Builtins"]] $ + expectError (@?= ModuleNotFound nonExistantModule) + +unit_rename_module_imported :: Assertion +unit_rename_module_imported = + let builtins = ModuleName ["Builtins"] + test = do + importModules [builtinModule] + handleEditRequest [RenameModule builtins ["NewModule"]] + a = newEmptyApp + in do + case fst $ runAppTestM (ID $ appIdCounter a) a test of + Left err -> err @?= ModuleReadonly builtins + Right _ -> assertFailure "Expected RenameModule to complain about module being read-only" + _defIDs :: Traversal' ASTDef ID _defIDs = #astDefExpr % (_exprMeta % _id `adjoin` _exprTypeMeta % _id) `adjoin` #astDefType % _typeMeta % _id From ad31513b4bcd9659dfe989ffa79a9c27c330e05a Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 6 May 2022 14:55:12 +0100 Subject: [PATCH 3/6] feat!: GET /api/program displays all modules Previously we only viewed the contents of the one editable module. We now give the contents of every module, and also tag them with whether they are editable or imported. BREAKING CHANGE: this changes the response to an api endpoint, and this is reflected in the generated openapi schema. --- primer-service/src/Primer/OpenAPI.hs | 6 ++-- primer/src/Primer/API.hs | 51 +++++++++++++++++++--------- 2 files changed, 39 insertions(+), 18 deletions(-) diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs index b448654d7..2f6f5d661 100644 --- a/primer-service/src/Primer/OpenAPI.hs +++ b/primer-service/src/Primer/OpenAPI.hs @@ -9,9 +9,9 @@ module Primer.OpenAPI ( import Data.OpenApi (ToSchema) import Data.Text (Text) import Data.Typeable (Typeable) -import Primer.API (Def, Prog, Tree) +import Primer.API (Def, Module, Prog, Tree) import Primer.App (InitialApp) -import Primer.Core (GlobalName, ID (..), LVarName) +import Primer.Core (GlobalName, ID (..), LVarName, ModuleName) import Primer.Database (Session, SessionName) import Primer.Name (Name) @@ -40,4 +40,6 @@ deriving via Name instance Typeable k => ToSchema (GlobalName k) deriving via Name instance (ToSchema LVarName) instance ToSchema Tree instance ToSchema Def +instance ToSchema ModuleName +instance ToSchema Module instance ToSchema Prog diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 9a16aac71..8966bac31 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -21,6 +21,7 @@ module Primer.API ( getVersion, Tree, Prog, + Module, Def, getProgram, getSessionName, @@ -70,6 +71,7 @@ import Primer.App ( handleMutationRequest, handleQuestion, initialApp, + progImports, progModule, runEditAppM, runQueryAppM, @@ -83,6 +85,7 @@ import Primer.Core ( ID, Kind, LVarName, + ModuleName, PrimCon (..), TmVarRef (GlobalVarRef, LocalVarRef), TyConName, @@ -123,7 +126,7 @@ import qualified Primer.Database as Database ( Success ), ) -import Primer.Module (Module (moduleDefs, moduleTypes)) +import Primer.Module (moduleDefs, moduleName, moduleTypes) import Primer.Name (Name, unName) import qualified StmContainers.Map as StmMap @@ -301,8 +304,19 @@ instance ToJSON Tree -- | This type is the API's view of a 'App.Prog' -- (this is expected to evolve as we flesh out the API) -data Prog = Prog - { types :: [TyConName] +newtype Prog = Prog + { modules :: [Module] + } + deriving (Generic) + +instance ToJSON Prog + +-- | This type is the API's view of a 'Module.Module' +-- (this is expected to evolve as we flesh out the API) +data Module = Module + { modname :: ModuleName + , editable :: Bool + , types :: [TyConName] , -- We don't use Map Name Def as it is rather redundant since each -- Def carries a name field, and it is difficult to enforce that -- "the keys of this object match the name field of the @@ -311,7 +325,7 @@ data Prog = Prog } deriving (Generic) -instance ToJSON Prog +instance ToJSON Module -- | This type is the api's view of a 'Primer.Core.Def' -- (this is expected to evolve as we flesh out the API) @@ -327,18 +341,23 @@ instance ToJSON Def viewProg :: App.Prog -> Prog viewProg p = - Prog - { types = typeDefName <$> Map.elems (moduleTypes $ progModule p) - , defs = - ( \d -> - Def - { name = defName d - , type_ = viewTreeType $ defType d - , term = viewTreeExpr . astDefExpr <$> defAST d - } - ) - <$> Map.elems (moduleDefs $ progModule p) - } + Prog{modules = viewModule True (progModule p) : map (viewModule False) (progImports p)} + where + viewModule e m = + Module + { modname = moduleName m + , editable = e + , types = typeDefName <$> Map.elems (moduleTypes m) + , defs = + ( \d -> + Def + { name = defName d + , type_ = viewTreeType $ defType d + , term = viewTreeExpr . astDefExpr <$> defAST d + } + ) + <$> Map.elems (moduleDefs m) + } -- | A simple method to extract 'Tree's from 'Expr's. This is injective. -- Currently it is designed to be simple and just enough to enable From 195565db965c3280c1a38d7ab424e026d28a0199 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 6 May 2022 16:06:23 +0100 Subject: [PATCH 4/6] refactor: concise utilities for Action/Prog tests --- primer/test/Tests/Action/Prog.hs | 55 +++++++++++++++++--------------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 65121f783..61615e4e3 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -130,19 +130,19 @@ unit_move_to_def_and_construct_let :: Assertion unit_move_to_def_and_construct_let = progActionTest defaultEmptyProg [moveToDef "other", BodyAction [ConstructLet (Just "x")]] $ expectSuccess $ \prog prog' -> - case astDefExpr <$> lookupASTDef' "other" (moduleDefs $ progModule prog') of + case astDefExpr <$> lookupASTDef' "other" prog' of Just Let{} -> -- Check that main is unchanged - Map.lookup "main" (moduleDefs $ progModule prog') @?= Map.lookup "main" (moduleDefs $ progModule prog) + lookupDef' "main" prog' @?= lookupDef' "main" prog _ -> assertFailure "definition not found" unit_rename_def :: Assertion unit_rename_def = progActionTest defaultEmptyProg [renameDef "other" "foo"] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing - fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo") - fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main") + fmap defName (lookupDef' "other" prog') @?= Nothing + fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo") + fmap defName (lookupDef' "main" prog') @?= Just (gvn "main") unit_rename_def_to_same_name_as_existing_def :: Assertion unit_rename_def_to_same_name_as_existing_def = @@ -163,10 +163,10 @@ unit_rename_def_referenced = , renameDef "other" "foo" ] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing - fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo") - fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main") - fmap (set _exprMeta () . astDefExpr) (defAST =<< Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (Var () $ globalVarRef "foo") + fmap defName (lookupDef' "other" prog') @?= Nothing + fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo") + fmap defName (lookupDef' "main" prog') @?= Just (gvn "main") + fmap (set _exprMeta () . astDefExpr) (defAST =<< lookupDef' "main" prog') @?= Just (Var () $ globalVarRef "foo") unit_rename_def_recursive :: Assertion unit_rename_def_recursive = @@ -177,16 +177,16 @@ unit_rename_def_recursive = , renameDef "main" "foo" ] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Nothing - fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo") - fmap (set _exprMeta () . astDefExpr) (defAST =<< Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (Var () $ globalVarRef "foo") + fmap defName (lookupDef' "main" prog') @?= Nothing + fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo") + fmap (set _exprMeta () . astDefExpr) (defAST =<< lookupDef' "foo" prog') @?= Just (Var () $ globalVarRef "foo") unit_delete_def :: Assertion unit_delete_def = progActionTest defaultEmptyProg [deleteDef "other"] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing - fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main") + fmap defName (lookupDef' "other" prog') @?= Nothing + fmap defName (lookupDef' "main" prog') @?= Just (gvn "main") unit_delete_def_unknown_id :: Assertion unit_delete_def_unknown_id = @@ -219,7 +219,7 @@ unit_construct_let_without_moving_to_def_first = unit_create_def :: Assertion unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] $ expectSuccess $ \_ prog' -> do - case lookupASTDef' "newDef" (moduleDefs $ progModule prog') of + case lookupASTDef' "newDef" prog' of Nothing -> assertFailure $ show $ moduleDefs $ progModule prog' Just def -> do astDefName def @?= gvn "newDef" @@ -434,7 +434,7 @@ unit_construct_arrow_in_sig :: Assertion unit_construct_arrow_in_sig = progActionTest defaultEmptyProg [moveToDef "other", SigAction [ConstructArrowL, Move Child1]] $ expectSuccess $ \_ prog' -> - case lookupASTDef' "other" (moduleDefs $ progModule prog') of + case lookupASTDef' "other" prog' of Just def -> -- Check that the signature is an arrow type case astDefType def of @@ -465,7 +465,7 @@ unit_sigaction_creates_holes = ] in progActionTest defaultFullProg acts $ expectSuccess $ \_ prog' -> - case lookupASTDef' "other" (moduleDefs $ progModule prog') of + case lookupASTDef' "other" prog' of Just def -> -- Check that the definition is a non-empty hole case astDefExpr def of @@ -502,8 +502,8 @@ unit_copy_paste_duplicate = do clearIDs = set (_Just % _defIDs) 0 in do src @?= lookupASTDef fromDef (moduleDefsQualified $ progModule r) - assertBool "equal to toDef" $ src /= lookupASTDef' "blank" (moduleDefs $ progModule r) - clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' "blank" (moduleDefs $ progModule r)) + assertBool "equal to toDef" $ src /= lookupASTDef' "blank" r + clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' "blank" r) -- ∀a . (∀b,c . a -> b -> ∀d. c -> d) -> ∀c. ? -- copy ^------------------^ @@ -630,12 +630,12 @@ unit_copy_paste_ann = do Right (tcp, r) -> -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up - let src = lookupASTDef' fromDef' (moduleDefs $ progModule tcp) + let src = lookupASTDef' fromDef' tcp clearIDs = set (_Just % _defIDs) 0 in do - src @?= lookupASTDef' fromDef' (moduleDefs $ progModule r) - assertBool "equal to blank" $ src /= lookupASTDef' toDef' (moduleDefs $ progModule r) - clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' toDef' (moduleDefs $ progModule r)) + src @?= lookupASTDef' fromDef' r + assertBool "equal to blank" $ src /= lookupASTDef' toDef' r + clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' toDef' r) unit_copy_paste_ann2sig :: Assertion unit_copy_paste_ann2sig = do @@ -1369,11 +1369,14 @@ runAppTestM startID a m = Left err -> (Left err, a) Right (res, app') -> (Right res, app') --- Looks up a definition, ignoring any module prefix +-- Looks up a definition in the main module -- Useful in these tests so we don't have to specify -- the name of the module all the time -lookupASTDef' :: Name -> Map Name Def -> Maybe ASTDef -lookupASTDef' name = defAST <=< Map.lookup name +lookupDef' :: Name -> Prog -> Maybe Def +lookupDef' = flip findGlobalByName . qualifyName mainModuleName + +lookupASTDef' :: Name -> Prog -> Maybe ASTDef +lookupASTDef' name = defAST <=< lookupDef' name astDefBaseName :: ASTDef -> Name astDefBaseName = baseName . astDefName From 3e4737132f820f0960210d3d1e93f049950d374f Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 9 May 2022 14:44:57 +0100 Subject: [PATCH 5/6] refactor: tcWholeProg checks typedefs also --- primer/src/Primer/App.hs | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d3b8f5068..f47641c73 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -85,7 +85,7 @@ import Optics ( _Right, ) import Primer.Action ( - Action, + Action (NoOp), ActionError (..), ProgAction (..), applyActionsToBody, @@ -168,7 +168,6 @@ import Primer.Typecheck ( SmartHoles (NoSmartHoles, SmartHoles), TypeError, buildTypingContextFromModules, - checkDef, checkEverything, checkTypeDefs, mkTypeDefMapQualified, @@ -1146,14 +1145,23 @@ loopM f a = Left a' -> loopM f a' Right b -> pure b --- | Checks every term definition in the editable module. --- Does not check typedefs or imported modules. +-- | Checks every term and type definition in the editable module. +-- Does not check imported modules. tcWholeProg :: forall m. MonadEdit m => Prog -> m Prog tcWholeProg p = let tc :: ReaderT Cxt (ExceptT ActionError m) Prog tc = do - defs' <- mapM checkDef (moduleDefs $ progModule p) - let mod' = (progModule p){moduleDefs = defs'} + mods' <- + checkEverything + (progSmartHoles p) + CheckEverything + { trusted = progImports p + , toCheck = [progModule p] + } + mod' <- case mods' of + [checkedMod] -> pure checkedMod + -- This internal error will go away when we allow Progs to contain multiple mutable modules + _ -> throwError $ CustomFailure NoOp "Internal error: checkEverything returned a different number of module as were passed in" let p' = p{progModule = mod'} -- We need to update the metadata cached in the selection let oldSel = progSelection p From a43420da5f89bfc0b0fb3f9fc7cfb8972f69d5cd Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 6 May 2022 15:40:46 +0100 Subject: [PATCH 6/6] feat!: multiple editable modules NB: lots of this commit is fairly trivial testsuite churn BREAKING CHANGE: this change requires a database migration, as it changes the representation of `Prog`. However, since this is just serialised to json and stored as a blob in the DB, it requires no schema changes. Since we have no programs we need to preserve, we decided not to bother with a migration. This means that DBs created before this commit will not load with a primer containing this commit. --- primer-rel8/test/TestUtils.hs | 13 +- primer/src/Primer/API.hs | 4 +- primer/src/Primer/Action.hs | 24 +- primer/src/Primer/App.hs | 171 +++++++---- primer/test/Tests/Action/Prog.hs | 277 ++++++++++++++---- primer/test/Tests/Serialization.hs | 13 +- primer/test/Tests/Typecheck.hs | 8 +- .../serialization/edit_response_2.json | 214 +++++++------- primer/test/outputs/serialization/prog.json | 214 +++++++------- 9 files changed, 582 insertions(+), 356 deletions(-) diff --git a/primer-rel8/test/TestUtils.hs b/primer-rel8/test/TestUtils.hs index fc9a46a13..02cef5668 100644 --- a/primer-rel8/test/TestUtils.hs +++ b/primer-rel8/test/TestUtils.hs @@ -363,10 +363,11 @@ testApp = testProg = newEmptyProg { progImports = [builtinModule, primitiveModule] - , progModule = - Module - { moduleName = ModuleName $ "TestModule" :| [] - , moduleTypes = mempty - , moduleDefs = Map.singleton (baseName $ astDefName testASTDef) (DefAST testASTDef) - } + , progModules = + [ Module + { moduleName = ModuleName $ "TestModule" :| [] + , moduleTypes = mempty + , moduleDefs = Map.singleton (baseName $ astDefName testASTDef) (DefAST testASTDef) + } + ] } diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index 8966bac31..6a18608f9 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -72,7 +72,7 @@ import Primer.App ( handleQuestion, initialApp, progImports, - progModule, + progModules, runEditAppM, runQueryAppM, ) @@ -341,7 +341,7 @@ instance ToJSON Def viewProg :: App.Prog -> Prog viewProg p = - Prog{modules = viewModule True (progModule p) : map (viewModule False) (progImports p)} + Prog{modules = map (viewModule True) (progModules p) <> map (viewModule False) (progImports p)} where viewModule e m = Module diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 756f546e8..ee952c863 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -422,7 +422,7 @@ data ProgAction -- At the start of the actions, the cursor starts at the root of the definition's type/expression CopyPasteSig (GVarName, ID) [Action] | CopyPasteBody (GVarName, ID) [Action] - | -- | Renames the sole editable module + | -- | Renames an editable module (will return an error if asked to rename an imported module) RenameModule ModuleName (NonEmpty Text) deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ProgAction @@ -439,24 +439,26 @@ type ActionM m = -- | Apply a sequence of actions to the type signature of a definition -- We apply the actions to the type, then typecheck the body of the definition against the new type. -- We must then typecheck the whole program to check any uses of the definition. --- Note that this may introduce new holes when using SmartHoles, and thus we return a whole module --- as well as the one definition we wanted to change. +-- Note that this may introduce new holes when using SmartHoles, and thus we +-- return a whole set of modules as well as the one definition we wanted to +-- change. applyActionsToTypeSig :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> [Module] -> - Module -> + -- | The @Module@ we are focused on, and all the other editable modules + (Module, [Module]) -> -- | This must be one of the definitions in the @Module@ ASTDef -> [Action] -> - m (Either ActionError (ASTDef, Module, TypeZ)) -applyActionsToTypeSig smartHoles imports mod def actions = + m (Either ActionError (ASTDef, [Module], TypeZ)) +applyActionsToTypeSig smartHoles imports (mod, mods) def actions = runReaderT go - (buildTypingContextFromModules (mod : imports) smartHoles) + (buildTypingContextFromModules (mod : mods <> imports) smartHoles) & runExceptT where - go :: ActionM m => m (ASTDef, Module, TypeZ) + go :: ActionM m => m (ASTDef, [Module], TypeZ) go = do zt <- withWrappedType (astDefType def) (\zt -> foldM (flip applyActionAndSynth) (InType zt) actions) let t = target (top zt) @@ -469,10 +471,8 @@ applyActionsToTypeSig smartHoles imports mod def actions = -- We make sure that the updated type is present in the global context. -- Here we just check the whole of the mutable prog, excluding imports. -- (for efficiency, we need not check the type definitions, but we do not implement this optimisation) - checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = [mod']}) >>= \case - [checkedMod] -> pure (def', checkedMod, zt) - -- This internal error will go away when we allow Progs to contain multiple mutable modules - _ -> throwError $ CustomFailure NoOp "Internal error: checkEverything returned a different number of module as were passed in" + checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}) + >>= \checkedMods -> pure (def', checkedMods, zt) -- Actions expect that all ASTs have a top-level expression of some sort. -- Signatures don't have this: they're just a type. -- We fake it by wrapping the type in a top-level annotation node, then unwrapping afterwards. diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index f47641c73..aba82842f 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -70,6 +70,7 @@ import Optics ( Field2 (_2), Field3 (_3), ReversibleOptic (re), + mapped, over, toListOf, traverseOf, @@ -85,7 +86,7 @@ import Optics ( _Right, ) import Primer.Action ( - Action (NoOp), + Action, ActionError (..), ProgAction (..), applyActionsToBody, @@ -205,8 +206,8 @@ import Primer.Zipper ( data Prog = Prog { progImports :: [Module] -- ^ Some immutable imported modules - , progModule :: Module - -- ^ The one editable "current" module + , progModules :: [Module] + -- ^ The editable "home" modules , progSelection :: Maybe Selection , progSmartHoles :: SmartHoles , progLog :: Log -- The log of all actions @@ -215,7 +216,7 @@ data Prog = Prog deriving (FromJSON, ToJSON) via VJSON Prog progAllModules :: Prog -> [Module] -progAllModules p = progModule p : progImports p +progAllModules p = progModules p <> progImports p -- Note [Modules] -- The invariant is that the @progImports@ modules are never edited, but @@ -242,7 +243,7 @@ importModules ms = do ActionError $ ImportNameClash $ (currentNames `intersect` newNames) <> (newNames \\ ordNub newNames) - -- Imports must be well-typed (and cannot depend on the editable module) + -- Imports must be well-typed (and cannot depend on the editable modules) checkedImports <- liftError (ActionError . ImportFailed ()) $ checkEverything NoSmartHoles $ @@ -396,11 +397,11 @@ handleQuestion = \case prog <- asks appProg focusNode prog defname nodeid --- This only looks in the editable module, not in any imports +-- This only looks in the editable modules, not in any imports focusNode :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) -focusNode prog = focusNodeDefs $ moduleDefsQualified $ progModule prog +focusNode prog = focusNodeDefs $ foldMap moduleDefsQualified $ progModules prog --- This looks in the editable module and also in any imports +-- This looks in the editable modules and also in any imports focusNodeImports :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) focusNodeImports prog = focusNodeDefs $ allDefs prog @@ -465,7 +466,6 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS Right nf -> EvalFullRespNormal nf -- | Handle a 'ProgAction' --- These actions only affect the editable module -- The 'GVarName' argument is the currently-selected definition, which is -- provided for convenience: it is the same as the one in the progSelection. applyProgAction :: MonadEdit m => Prog -> Maybe GVarName -> ProgAction -> m Prog @@ -475,7 +475,7 @@ applyProgAction prog mdefName = \case case Map.lookup d $ moduleDefsQualified m of Nothing -> throwError $ DefNotFound d Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing - DeleteDef d -> editModule (qualifiedModule d) prog $ \m -> + DeleteDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) -> case deleteDef m d of Nothing -> throwError $ DefNotFound d Just mod' -> do @@ -485,9 +485,9 @@ applyProgAction prog mdefName = \case void . liftError (const $ DefInUse d) $ checkEverything @TypeError NoSmartHoles - CheckEverything{trusted = progImports prog, toCheck = [mod']} - pure (mod', Nothing) - RenameDef d nameStr -> editModuleOf (Just d) prog $ \m def -> do + CheckEverything{trusted = progImports prog, toCheck = mod' : ms} + pure (mod' : ms, Nothing) + RenameDef d nameStr -> editModuleOfCross (Just d) prog $ \(m, ms) def -> do let defs = moduleDefs m oldNameBase = baseName d newNameBase = unsafeMkName nameStr @@ -496,14 +496,14 @@ applyProgAction prog mdefName = \case then throwError $ DefAlreadyExists newName else do let def' = DefAST def{astDefName = newName} - defs' <- + let m' = m{moduleDefs = Map.insert newNameBase def' $ Map.delete oldNameBase defs} + renamedModules <- maybe (throwError $ ActionError NameCapture) pure $ - traverse - ( traverseOf (#_DefAST % #astDefExpr) $ - renameVar (GlobalVarRef d) (GlobalVarRef newName) - ) - (Map.insert newNameBase def' $ Map.delete oldNameBase defs) - pure (m{moduleDefs = defs'}, Just $ Selection (defName def') Nothing) + traverseOf + (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) + (renameVar (GlobalVarRef d) (GlobalVarRef newName)) + (m' : ms) + pure (renamedModules, Just $ Selection (defName def') Nothing) CreateDef modName n -> editModule modName prog $ \mod -> do let defs = moduleDefs mod name <- case n of @@ -534,9 +534,10 @@ applyProgAction prog mdefName = \case (checkTypeDefs $ mkTypeDefMapQualified [TypeDefAST td]) (buildTypingContextFromModules (progAllModules prog) NoSmartHoles) ) - RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelection (qualifiedModule old) prog $ \m -> do - m' <- traverseOf #moduleTypes (updateType <=< pure . updateRefsInTypes) m - pure $ over (#moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) m' + RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelectionCross (qualifiedModule old) prog $ \(m, ms) -> do + m' <- traverseOf #moduleTypes updateType m + let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms + pure $ over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes where new = qualifyName (qualifiedModule old) nameRaw updateType m = do @@ -562,10 +563,10 @@ applyProgAction prog mdefName = \case $ transform $ over typesInExpr $ transform $ over (#_TCon % _2) updateName updateName n = if n == old then new else n RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> - editModuleSameSelection (qualifiedModule type_) prog $ \m -> do + editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do when (new `elem` allConNames prog) $ throwError $ ConAlreadyExists new m' <- updateType m - pure $ over #moduleDefs updateDefs m' + pure $ over (mapped % #moduleDefs) updateDefs (m' : ms) where updateType = alterTypeDef @@ -610,13 +611,13 @@ applyProgAction prog mdefName = \case $ over _freeVarsTy $ \(_, v) -> TVar () $ updateName v updateName n = if n == old then new else n AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> - editModuleSameSelection (qualifiedModule type_) prog $ \m -> do + editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do when (con `elem` allConNames prog) $ throwError $ ConAlreadyExists con m' <- updateType m traverseOf - (#moduleDefs % traversed % #_DefAST % #astDefExpr) + (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr) updateDefs - m' + $ m' : ms where updateDefs = transformCaseBranches prog type_ $ \bs -> do m' <- DSL.meta @@ -629,8 +630,9 @@ applyProgAction prog mdefName = \case ) type_ SetConFieldType type_ con index new -> - editModuleSameSelection (qualifiedModule type_) prog $ - traverseOf #moduleDefs updateDefs <=< updateType + editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do + m' <- updateType m + traverseOf (traversed % #moduleDefs) updateDefs (m' : ms) where updateType = alterTypeDef @@ -678,8 +680,9 @@ applyProgAction prog mdefName = \case e else pure cb AddConField type_ con index new -> - editModuleSameSelection (qualifiedModule type_) prog $ - traverseOf #moduleDefs updateDefs <=< updateType + editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do + m' <- updateType m + traverseOf (traversed % #moduleDefs) updateDefs (m' : ms) where updateType = alterTypeDef @@ -739,7 +742,7 @@ applyProgAction prog mdefName = \case , meta } ) - SigAction actions -> editModuleOf mdefName prog $ \m def -> do + SigAction actions -> editModuleOfCross mdefName prog $ \m def -> do let smartHoles = progSmartHoles prog res <- applyActionsToTypeSig smartHoles (progImports prog) m def actions case res of @@ -772,7 +775,7 @@ applyProgAction prog mdefName = \case -- is an editable module _ <- editModuleSameSelection oldName prog pure let n = ModuleName $ unsafeMkName <$> newName - curMods = RM{imported = progImports prog, editable = progModule prog} + curMods = RM{imported = progImports prog, editable = progModules prog} in if n == oldName then pure prog else case renameModule oldName n curMods of @@ -781,7 +784,7 @@ applyProgAction prog mdefName = \case if imported curMods == imported renamedMods then pure $ - prog & #progModule .~ editable renamedMods + prog & #progModules .~ editable renamedMods & #progSelection % _Just %~ renameModule' oldName n else throwError $ @@ -792,7 +795,7 @@ applyProgAction prog mdefName = \case InternalFailure "RenameModule: imported modules were edited by renaming" -- Helper for RenameModule action -data RenameMods a = RM {imported :: [a], editable :: a} +data RenameMods a = RM {imported :: [a], editable :: [a]} deriving (Functor, Foldable, Traversable) lookupEditableModule :: MonadError ProgError m => ModuleName -> Prog -> m Module @@ -806,10 +809,10 @@ lookupEditableModule n p = data ModuleLookup = Editable Module | Imported Module lookupModule' :: MonadError ProgError m => ModuleName -> Prog -> m ModuleLookup -lookupModule' n p = case (n == moduleName (progModule p), find ((n ==) . moduleName) (progImports p)) of - (True, _) -> pure $ Editable (progModule p) - (False, Just m) -> pure $ Imported m - (False, Nothing) -> throwError $ ModuleNotFound n +lookupModule' n p = case (find ((n ==) . moduleName) (progModules p), find ((n ==) . moduleName) (progImports p)) of + (Just m, _) -> pure $ Editable m + (Nothing, Just m) -> pure $ Imported m + (Nothing, Nothing) -> throwError $ ModuleNotFound n editModule :: MonadError ProgError m => @@ -820,7 +823,28 @@ editModule :: editModule n p f = do m <- lookupEditableModule n p (m', s) <- f m - pure $ p{progModule = m', progSelection = s} + pure $ + p + { progModules = m' : filter ((/= n) . moduleName) (progModules p) + , progSelection = s + } + +-- A variant of 'editModule' for actions which can affect multiple modules +editModuleCross :: + MonadError ProgError m => + ModuleName -> + Prog -> + ((Module, [Module]) -> m ([Module], Maybe Selection)) -> + m Prog +editModuleCross n p f = do + m <- lookupEditableModule n p + let otherModules = filter ((/= n) . moduleName) (progModules p) + (m', s) <- f (m, otherModules) + pure $ + p + { progModules = m' + , progSelection = s + } editModuleSameSelection :: MonadError ProgError m => @@ -830,6 +854,15 @@ editModuleSameSelection :: m Prog editModuleSameSelection n p f = editModule n p (fmap (,progSelection p) . f) +-- A variant of 'editModuleSameSelection' for actions which can affect multiple modules +editModuleSameSelectionCross :: + MonadError ProgError m => + ModuleName -> + Prog -> + ((Module, [Module]) -> m [Module]) -> + m Prog +editModuleSameSelectionCross n p f = editModuleCross n p (fmap (,progSelection p) . f) + editModuleOf :: MonadError ProgError m => Maybe GVarName -> @@ -843,6 +876,20 @@ editModuleOf mdefName prog f = case mdefName of Just (DefAST def) -> f m def _ -> throwError $ DefNotFound defname +-- A variant of 'editModuleOf' for actions which can affect multiple modules +editModuleOfCross :: + MonadError ProgError m => + Maybe GVarName -> + Prog -> + ((Module, [Module]) -> ASTDef -> m ([Module], Maybe Selection)) -> + m Prog +editModuleOfCross mdefName prog f = case mdefName of + Nothing -> throwError NoDefSelected + Just defname -> editModuleCross (qualifiedModule defname) prog $ \ms@(m, _) -> + case Map.lookup (baseName defname) (moduleDefs m) of + Just (DefAST def) -> f ms def + _ -> throwError $ DefNotFound defname + -- | Undo the last block of actions. -- If there are no actions in the log we return the program unchanged. -- We undo by replaying the whole log from the start. @@ -963,12 +1010,13 @@ newEmptyProg = def = DefAST $ ASTDef (qualifyName (ModuleName $ "Main" :| []) "main") expr ty in Prog { progImports = mempty - , progModule = - Module - { moduleName = ModuleName $ "Main" :| [] - , moduleTypes = mempty - , moduleDefs = Map.singleton (baseName $ defName def) def - } + , progModules = + [ Module + { moduleName = ModuleName $ "Main" :| [] + , moduleTypes = mempty + , moduleDefs = Map.singleton (baseName $ defName def) def + } + ] , progSelection = Nothing , progSmartHoles = SmartHoles , progLog = Log [] @@ -989,12 +1037,13 @@ newProg :: Prog newProg = newEmptyProg { progImports = [builtinModule, primitiveModule] - , progModule = - Module - { moduleName = ModuleName $ "Main" :| [] - , moduleTypes = mempty - , moduleDefs = defaultDefs $ ModuleName $ "Main" :| [] - } + , progModules = + [ Module + { moduleName = ModuleName $ "Main" :| [] + , moduleTypes = mempty + , moduleDefs = defaultDefs $ ModuleName $ "Main" :| [] + } + ] } -- Since IDs should be unique in a module, we record 'defaultDefsNextID' @@ -1060,13 +1109,14 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do Right zt -> pure $ Right zt let smartHoles = progSmartHoles p finalProg <- editModuleOf (Just toDefName) p $ \mod oldDef -> do + let otherModules = filter ((/= moduleName mod) . moduleName) (progModules p) -- We intentionally throw away any changes in doneSetup other than via 'tgt' -- as these could be in other definitions referencing this one, due to -- types changing. However, we are going to do a full tc pass anyway, -- which will pick up any problems. It is better to do it in one batch, -- in case the intermediate state after 'setup' causes more problems -- than the final state does. - doneSetup <- applyActionsToTypeSig smartHoles (progImports p) mod oldDef setup + doneSetup <- applyActionsToTypeSig smartHoles (progImports p) (mod, otherModules) oldDef setup tgt <- case doneSetup of Left err -> throwError $ ActionError err Right (_, _, tgt) -> pure $ focusOnlyType tgt @@ -1145,7 +1195,7 @@ loopM f a = Left a' -> loopM f a' Right b -> pure b --- | Checks every term and type definition in the editable module. +-- | Checks every term and type definition in the editable modules. -- Does not check imported modules. tcWholeProg :: forall m. MonadEdit m => Prog -> m Prog tcWholeProg p = @@ -1156,13 +1206,9 @@ tcWholeProg p = (progSmartHoles p) CheckEverything { trusted = progImports p - , toCheck = [progModule p] + , toCheck = progModules p } - mod' <- case mods' of - [checkedMod] -> pure checkedMod - -- This internal error will go away when we allow Progs to contain multiple mutable modules - _ -> throwError $ CustomFailure NoOp "Internal error: checkEverything returned a different number of module as were passed in" - let p' = p{progModule = mod'} + let p' = p{progModules = mods'} -- We need to update the metadata cached in the selection let oldSel = progSelection p newSel <- case oldSel of @@ -1343,7 +1389,8 @@ liftError f = runExceptT >=> either (throwError . f) pure allConNames :: Prog -> [ValConName] allConNames = toListOf $ - #progModule + #progModules + % traversed % #moduleTypes % traversed % #_TypeDefAST diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 61615e4e3..c293ba200 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -13,7 +13,9 @@ import Optics import Primer.Action ( Action ( ConstructAnn, + ConstructApp, ConstructArrowL, + ConstructCase, ConstructLet, ConstructTCon, ConstructVar, @@ -22,7 +24,7 @@ import Primer.Action ( Move ), ActionError (ImportNameClash), - Movement (Branch, Child1, Child2), + Movement (Branch, Child1, Child2, Parent), ) import Primer.App ( App (..), @@ -45,7 +47,21 @@ import Primer.App ( progAllModules, tcWholeProg, ) -import Primer.Builtins (builtinModule, cCons, cJust, cMakePair, cNil, tBool, tList, tMaybe, tPair) +import Primer.Builtins ( + builtinModule, + cCons, + cJust, + cMakePair, + cNil, + cSucc, + cTrue, + cZero, + tBool, + tList, + tMaybe, + tNat, + tPair, + ) import Primer.Core ( ASTDef (..), ASTTypeDef (..), @@ -67,6 +83,7 @@ import Primer.Core ( ValConName, defAST, defName, + defType, getID, qualifyName, typeDefAST, @@ -101,12 +118,13 @@ import Primer.Core.Utils (forgetIDs) import Primer.Module (Module (Module, moduleDefs, moduleName, moduleTypes), mkTypeDefMap, moduleDefsQualified, moduleTypesQualified) import Primer.Name import Primer.Primitives (primitiveGVar, primitiveModule, tChar) -import Primer.Typecheck (TypeError (UnknownTypeConstructor)) +import Primer.Typecheck (SmartHoles (NoSmartHoles, SmartHoles), TypeError (UnknownTypeConstructor)) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=)) import TestM (TestM, evalTestM) -import TestUtils (constructTCon) +import TestUtils (constructCon, constructTCon) import qualified TestUtils import Tests.Typecheck (checkProgWellFormed) +import Prelude (error) unit_empty_actions_only_change_the_log :: Assertion unit_empty_actions_only_change_the_log = progActionTest defaultEmptyProg [] $ @@ -198,11 +216,35 @@ 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 (qualifyM "foo") 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 = progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "main"], deleteDef "main"] $ - expectSuccess $ \prog prog' -> Map.delete "main" (moduleDefs $ progModule prog) @?= moduleDefs (progModule prog') + expectSuccess $ \prog prog' -> + Map.delete + (qualifyName mainModuleName "main") + (foldMap moduleDefsQualified $ progModules prog) + @?= foldMap moduleDefsQualified (progModules prog') unit_move_to_unknown_def :: Assertion unit_move_to_unknown_def = @@ -220,7 +262,7 @@ unit_create_def :: Assertion unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] $ expectSuccess $ \_ prog' -> do case lookupASTDef' "newDef" prog' of - Nothing -> assertFailure $ show $ moduleDefs $ progModule prog' + Nothing -> assertFailure $ show $ moduleDefs <$> progModules prog' Just def -> do astDefName def @?= gvn "newDef" astDefExpr def @?= EmptyHole (Meta 4 Nothing Nothing) @@ -270,11 +312,11 @@ unit_create_typedef = in progActionTest defaultEmptyProg [AddTypeDef lst, AddTypeDef tree] $ expectSuccess $ \_ prog' -> do - case Map.elems $ moduleTypes $ progModule prog' of + case Map.elems $ foldMap moduleTypes $ progModules prog' of [lst', tree'] -> do TypeDefAST lst @=? lst' TypeDefAST tree @=? tree' - _ -> assertFailure $ show $ moduleTypes $ progModule prog' + _ -> assertFailure $ show $ moduleTypes <$> progModules prog' -- "List" is unknown here unit_create_typedef_bad_1 :: Assertion @@ -408,7 +450,7 @@ unit_create_typedef_8 = , astTypeDefNameHints = [] } in progActionTest defaultEmptyProg [AddTypeDef td] $ - expectSuccess $ \_ prog' -> Map.elems (moduleTypes (progModule prog')) @?= [TypeDefAST td] + expectSuccess $ \_ prog' -> Map.elems (foldMap moduleTypes (progModules prog')) @?= [TypeDefAST td] -- Allow clash between type name and constructor name across types unit_create_typedef_9 :: Assertion @@ -428,7 +470,7 @@ unit_create_typedef_9 = , astTypeDefNameHints = [] } in progActionTest defaultEmptyProg [AddTypeDef td1, AddTypeDef td2] $ - expectSuccess $ \_ prog' -> Map.elems (moduleTypes (progModule prog')) @?= [TypeDefAST td2, TypeDefAST td1] + expectSuccess $ \_ prog' -> Map.elems (foldMap moduleTypes (progModules prog')) @?= [TypeDefAST td2, TypeDefAST td1] unit_construct_arrow_in_sig :: Assertion unit_construct_arrow_in_sig = @@ -484,7 +526,7 @@ unit_copy_paste_duplicate = do blankDef <- ASTDef toDef <$> emptyHole <*> tEmptyHole pure ( newProg{progSelection = Nothing} - & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)] + & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)] , getID mainType , getID mainExpr , getID (astDefType blankDef) @@ -498,10 +540,10 @@ unit_copy_paste_duplicate = do Right (tcp, r) -> -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up - let src = lookupASTDef fromDef (moduleDefsQualified $ progModule tcp) + let src = lookupASTDef fromDef (foldMap moduleDefsQualified $ progModules tcp) clearIDs = set (_Just % _defIDs) 0 in do - src @?= lookupASTDef fromDef (moduleDefsQualified $ progModule r) + src @?= lookupASTDef fromDef (foldMap moduleDefsQualified $ progModules r) assertBool "equal to toDef" $ src /= lookupASTDef' "blank" r clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' "blank" r) @@ -526,9 +568,9 @@ unit_copy_paste_type_scoping = do defInitial <- ASTDef mainName <$> emptyHole <*> skel tEmptyHole expected <- ASTDef mainName <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d")) pure - ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] + ( newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] , getID toCopy - , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)] + , newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} actions = [MoveToDef mainName, CopyPasteSig (mainName, srcID) [Move Child1, Move Child2, Move Child1]] @@ -539,7 +581,7 @@ unit_copy_paste_type_scoping = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 - in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) + in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected) -- ∀a b.a ~> ∀a.a unit_raise :: Assertion @@ -551,9 +593,9 @@ unit_raise = do defInitial <- ASTDef mainName <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy) expected <- ASTDef mainName <$> emptyHole <*> tforall "a" KType (tvar "a") pure - ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)] + ( newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)] , getID toCopy - , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)] + , newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} actions = [MoveToDef mainName, CopyPasteSig (mainName, srcID) [Move Child1, Delete]] @@ -564,7 +606,7 @@ unit_raise = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 - in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) + in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected) -- ∀a. List a -> ∀b. b -> Pair a b -- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\@b z -> Pair @a @b y z @@ -593,9 +635,9 @@ unit_copy_paste_expr_1 = do defInitial <- ASTDef mainName <$> skel emptyHole <*> pure ty expected <- ASTDef mainName <$> skel (pure expectPasted) <*> pure ty pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)] + ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)] , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)] + , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [MoveToDef mainName, CopyPasteBody (mainName, srcID) [Move Child1, Move Child1, Move (Branch cNil)]] @@ -606,7 +648,7 @@ unit_copy_paste_expr_1 = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 - in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) + in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected) unit_copy_paste_ann :: Assertion unit_copy_paste_ann = do @@ -619,7 +661,7 @@ unit_copy_paste_ann = do mainDef <- ASTDef fromDef <$> emptyHole `ann` pure toCopy <*> tEmptyHole blankDef <- ASTDef toDef <$> emptyHole `ann` tEmptyHole <*> tEmptyHole pure - ( newProg{progSelection = Nothing} & #progModule % #moduleDefs .~ Map.fromList [(fromDef', DefAST mainDef), ("blank", DefAST blankDef)] + ( newProg{progSelection = Nothing} & #progModules % _head % #moduleDefs .~ Map.fromList [(fromDef', DefAST mainDef), ("blank", DefAST blankDef)] , getID toCopy ) let a = newApp{appProg = p} @@ -644,9 +686,9 @@ unit_copy_paste_ann2sig = do defInitial <- astDef "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole expected <- astDef "main" <$> emptyHole `ann` pure toCopy <*> tcon tBool pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] + ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)] + , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [moveToDef "main", copyPasteSig ("main", srcID) []] @@ -657,7 +699,7 @@ unit_copy_paste_ann2sig = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 - in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) + in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected) unit_copy_paste_sig2ann :: Assertion unit_copy_paste_sig2ann = do @@ -666,9 +708,9 @@ unit_copy_paste_sig2ann = do defInitial <- astDef "main" <$> emptyHole <*> pure toCopy expected <- astDef "main" <$> emptyHole `ann` tcon tBool <*> pure toCopy pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] + ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)] , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)] + , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [moveToDef "main", copyPasteBody ("main", srcID) [ConstructAnn, EnterType]] @@ -679,15 +721,15 @@ unit_copy_paste_sig2ann = do -- use the typechecked input p, as the result will have had a typecheck run, so -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 - in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) + in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected) -- VariablesInScope sees imported terms unit_import_vars :: Assertion unit_import_vars = let test = do importModules [builtinModule, primitiveModule] - gets (Map.assocs . moduleDefsQualified . progModule . appProg) >>= \case - [(i, DefAST d)] -> do + gets (fmap (Map.assocs . moduleDefsQualified) . progModules . appProg) >>= \case + [[(i, DefAST d)]] -> do a' <- get (_, vs) <- runReaderT (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) a' pure $ @@ -705,8 +747,8 @@ unit_import_reference = let test = do importModules [builtinModule, primitiveModule] prog <- gets appProg - case (findGlobalByName prog $ primitiveGVar "toUpper", Map.assocs $ moduleDefsQualified $ progModule prog) of - (Just toUpperDef, [(i, _)]) -> do + case (findGlobalByName prog $ primitiveGVar "toUpper", Map.assocs . moduleDefsQualified <$> progModules prog) of + (Just toUpperDef, [[(i, _)]]) -> do _ <- handleEditRequest [ MoveToDef i @@ -756,8 +798,8 @@ unit_copy_paste_import = } importModules [m] prog <- gets appProg - case (findGlobalByName prog $ TestUtils.gvn ["M"] "foo", Map.assocs $ moduleDefsQualified $ progModule prog) of - (Just (DefAST fooDef), [(i, _)]) -> do + case (findGlobalByName prog $ TestUtils.gvn ["M"] "foo", Map.assocs . moduleDefsQualified <$> progModules prog) of + (Just (DefAST fooDef), [[(i, _)]]) -> do let fromDef = astDefName fooDef fromType = getID $ astDefType fooDef fromExpr = getID $ astDefExpr fooDef @@ -1158,8 +1200,8 @@ unit_generate_names_import :: Assertion unit_generate_names_import = let test = do importModules [builtinModule] - gets (Map.assocs . moduleDefsQualified . progModule . appProg) >>= \case - [(i, DefAST d)] -> do + gets (fmap (Map.assocs . moduleDefsQualified) . progModules . appProg) >>= \case + [[(i, DefAST d)]] -> do a' <- get ns <- runReaderT @@ -1198,7 +1240,8 @@ defaultEmptyProg = do , meta = Left (Meta 1 Nothing Nothing) } } - & #progModule + & #progModules + % _head % #moduleDefs .~ Map.fromList [(astDefBaseName mainDef, DefAST mainDef), (astDefBaseName otherDef, DefAST otherDef)] @@ -1206,7 +1249,7 @@ unit_good_defaultEmptyProg :: Assertion unit_good_defaultEmptyProg = checkProgWellFormed defaultEmptyProg -- `defaultEmptyProg`, plus all primitive definitions (types and terms) --- and all builtin types, all moved into the editable module +-- and all builtin types, all moved into an editable module -- NB: this means that primitive constructors are unusable, since they -- will not typecheck (we now have only a "Main.Char" type, not a -- "Primitive.Char" type), but we can now test our error handling for @@ -1214,7 +1257,7 @@ unit_good_defaultEmptyProg = checkProgWellFormed defaultEmptyProg defaultFullProg :: MonadFresh ID m => m Prog defaultFullProg = do p <- defaultEmptyProg - let m = moduleName $ progModule p + let m = moduleName $ unsafeHead $ progModules p -- We need to move the primitives, which requires renaming -- unit_defaultFullModule_no_clash ensures that there will be no clashes renamed :: [Module] @@ -1222,14 +1265,14 @@ defaultFullProg = do renamedTypes = renamed ^.. folded % #moduleTypes % folded renamedDefs = foldOf (folded % #moduleDefs) renamed pure $ - p & #progModule % #moduleTypes %~ (mkTypeDefMap renamedTypes <>) - & #progModule % #moduleDefs %~ (renamedDefs <>) + p & #progModules % _head % #moduleTypes %~ (mkTypeDefMap renamedTypes <>) + & #progModules % _head % #moduleDefs %~ (renamedDefs <>) findTypeDef :: TyConName -> Prog -> IO ASTTypeDef -findTypeDef d p = maybe (assertFailure "couldn't find typedef") pure $ (typeDefAST <=< Map.lookup d) $ p ^. (#progModule % to moduleTypesQualified) +findTypeDef d p = maybe (assertFailure "couldn't find typedef") pure $ (typeDefAST <=< Map.lookup d) $ foldMap moduleTypesQualified $ progModules p findDef :: GVarName -> Prog -> IO ASTDef -findDef d p = maybe (assertFailure "couldn't find def") pure $ (defAST <=< Map.lookup d) $ p ^. (#progModule % to moduleDefsQualified) +findDef d p = maybe (assertFailure "couldn't find def") pure $ (defAST <=< Map.lookup d) $ foldMap moduleDefsQualified $ progModules p -- We use the same type definition for all tests related to editing type definitions -- (This is added to `defaultFullProg`) @@ -1249,8 +1292,8 @@ defaultProgEditableTypeDefs ds = do ] pure $ p - & (#progModule % #moduleTypes) %~ (mkTypeDefMap tds <>) - & (#progModule % #moduleDefs) %~ (Map.fromList ((\d -> (baseName $ astDefName d, DefAST d)) <$> ds') <>) + & (#progModules % _head % #moduleTypes) %~ (mkTypeDefMap tds <>) + & (#progModules % _head % #moduleDefs) %~ (Map.fromList ((\d -> (baseName $ astDefName d, DefAST d)) <$> ds') <>) tT :: TyConName tT = tcn "T" @@ -1268,7 +1311,7 @@ unit_good_defaultFullProg = checkProgWellFormed defaultFullProg unit_defaultFullProg_no_clash :: Assertion unit_defaultFullProg_no_clash = let (p, _) = create defaultEmptyProg - ms = progModule p : [builtinModule, primitiveModule] + ms = progModules p <> [builtinModule, primitiveModule] typeNames = ms ^.. folded % #moduleTypes % folded % to typeDefName % #baseName termNames = ms ^.. folded % #moduleDefs % to Map.keys % folded in do @@ -1289,10 +1332,10 @@ unit_rename_module = in case fst $ runAppTestM (ID $ appIdCounter a) a test of Left err -> assertFailure $ show err Right p -> do - unModuleName (moduleName $ progModule p) @?= ["Module2"] + fmap (unModuleName . moduleName) (progModules p) @?= [["Module2"]] selectedDef <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main") - case Map.elems (moduleDefs $ progModule p) of - [DefAST d] -> do + case fmap (Map.elems . moduleDefsQualified) (progModules p) of + [[DefAST d]] -> do let expectedName = qualifyName (ModuleName ["Module2"]) "main" astDefName d @?= expectedName case astDefExpr d of @@ -1330,6 +1373,134 @@ unit_rename_module_imported = Left err -> err @?= ModuleReadonly builtins Right _ -> assertFailure "Expected RenameModule to complain about module being read-only" +-- test actions update multiple modules where appropriate +unit_cross_module_actions :: Assertion +unit_cross_module_actions = + let test = do + importModules [builtinModule] + -- Setup: define Main.main :: T = case foo (C Zero) of {C p -> C (Succ p)} + handleAndTC + [ MoveToDef $ gvn "main" + , SigAction [constructTCon (qualifyM "T")] + , BodyAction + [ ConstructApp + , Move Child1 + , ConstructVar (GlobalVarRef $ qualifyM "foo") + , Move Parent + , Move Child2 + , ConstructApp + , Move Child1 + , constructCon (qualifyM "C") + , Move Parent + , Move Child2 + , constructCon cZero + , Move Parent + , Move Parent + , ConstructCase + , Move (Branch (qualifyM "C")) + , ConstructApp + , Move Child1 + , constructCon (qualifyM "C") + , Move Parent + , Move Child2 + , ConstructApp + , Move Child1 + , constructCon cSucc + , Move Parent + , Move Child2 + , ConstructVar (LocalVarRef "a26") + ] + ] + handleAndTC [RenameDef (qualifyM "foo") "bar"] + handleAndTC [RenameType (qualifyM "T") "R"] + handleAndTC [RenameCon (qualifyM "R") (qualifyM "C") "D"] + handleAndTC [AddCon (qualifyM "R") 1 "X"] + handleAndTC [SetConFieldType (qualifyM "R") (qualifyM "D") 0 (TCon () tBool)] + handleAndTC [AddConField (qualifyM "R") (qualifyM "D") 0 (TCon () tNat)] + handleAndTC [RenameModule (moduleName m) ["AnotherModule"]] + -- NB: SigAction relies on SmartHoles to fix any introduced inconsistencies + oldSH <- gets (progSmartHoles . appProg) + handleAndTC + [ SetSmartHoles SmartHoles + , MoveToDef $ qualifyName (ModuleName ["AnotherModule"]) "bar" + , SigAction + [ Move Child1 + , Delete + , constructTCon tBool + , Move Parent + , Move Child2 + , Delete + ] + , SetSmartHoles oldSH + ] + -- A bit of setup to test CopyPasteSig: main :: Nat = bar True (Note bar :: Bool -> ?) + handleAndTC + [ MoveToDef $ gvn "main" + , SigAction [Delete, constructTCon tNat] + , BodyAction + [ Delete + , ConstructApp + , Move Child1 + , ConstructVar $ GlobalVarRef $ qualifyName (ModuleName ["AnotherModule"]) "bar" + , Move Parent + , Move Child2 + , constructCon cTrue + ] + ] + -- Copy-paste within the sig of bar to make bar :: Bool -> Bool + -- NB: CopyPasteSig relies on SmartHoles to fix any introduced inconsistencies + barTy <- + gets $ + fmap defType . flip findGlobalByName (qualifyName (ModuleName ["AnotherModule"]) "bar") + . appProg + let srcId = case barTy of + Just (TFun _ src _) -> getID src + _ -> error "Unexpected shape of 'barTy'" + handleAndTC + [ SetSmartHoles SmartHoles + , MoveToDef $ qualifyName (ModuleName ["AnotherModule"]) "bar" + , CopyPasteSig + (qualifyName (ModuleName ["AnotherModule"]) "bar", srcId) + [Move Child2] + , SetSmartHoles oldSH + ] + gets appProg + handleAndTC acts = void $ tcWholeProg =<< handleEditRequest acts + n = ["Module2"] + qualifyM :: Name -> GlobalName k + qualifyM = qualifyName $ moduleName m + m = fst $ + create $ do + let ty = + ASTTypeDef + { astTypeDefName = qualifyM "T" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon (qualifyM "C") [TCon () tNat]] + , astTypeDefNameHints = [] + } + defTy <- tcon (astTypeDefName ty) `tfun` tcon (astTypeDefName ty) + defExpr <- emptyHole + let def = + ASTDef + { astDefName = qualifyM "foo" + , astDefType = defTy + , astDefExpr = defExpr + } + pure + Module + { moduleName = ModuleName n + , moduleTypes = Map.singleton "T" (TypeDefAST ty) + , moduleDefs = Map.singleton "foo" (DefAST def) + } + -- We turn off smartholes, as we want to test our actions work without it + a = + newEmptyApp & #appProg % #progModules %~ (m :) + & #appProg % #progSmartHoles .~ NoSmartHoles + in do + case fst $ runAppTestM (ID $ appIdCounter a) a test of + Left err -> assertFailure $ show err + Right _ -> pure () + _defIDs :: Traversal' ASTDef ID _defIDs = #astDefExpr % (_exprMeta % _id `adjoin` _exprTypeMeta % _id) `adjoin` #astDefType % _typeMeta % _id @@ -1381,9 +1552,11 @@ lookupASTDef' name = defAST <=< lookupDef' name astDefBaseName :: ASTDef -> Name astDefBaseName = baseName . astDefName --- Some helpers to run actions on the current module +-- Some helpers to run actions on the "main" module mainModuleName :: ModuleName -mainModuleName = moduleName $ progModule newEmptyProg +mainModuleName = case progModules newEmptyProg of + [m] -> moduleName m + _ -> error "expected exactly one module in newEmptyProg" mainModuleNameText :: NonEmpty Text mainModuleNameText = unName <$> unModuleName mainModuleName diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 1ed56b51b..5720376cf 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -129,12 +129,13 @@ fixtures = prog = Prog { progImports = mempty - , progModule = - Module - { moduleName = ModuleName ["M"] - , moduleTypes = mkTypeDefMap [typeDef] - , moduleDefs = Map.singleton (baseName $ astDefName def) (DefAST def) - } + , progModules = + [ Module + { moduleName = ModuleName ["M"] + , moduleTypes = mkTypeDefMap [typeDef] + , moduleDefs = Map.singleton (baseName $ astDefName def) (DefAST def) + } + ] , progSelection = Just selection , progSmartHoles = SmartHoles , progLog = log diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index b441ad0bf..4a39a6885 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -26,7 +26,7 @@ import Primer.App ( newEmptyProg, newProg, progAllModules, - progModule, + progModules, ) import Primer.Builtins ( boolDef, @@ -549,7 +549,7 @@ unit_bad_prim_map_base = case runTypecheckTestM NoSmartHoles $ do checkEverything NoSmartHoles CheckEverything - { trusted = [progModule newProg] + { trusted = progModules newProg , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo] } of Left err -> err @?= InternalError "Inconsistant names in moduleDefs map for module M" @@ -562,7 +562,7 @@ unit_bad_prim_map_module = case runTypecheckTestM NoSmartHoles $ do checkEverything NoSmartHoles CheckEverything - { trusted = [progModule newProg] + { trusted = progModules newProg , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo] } of Left err -> err @?= InternalError "Inconsistant names in moduleDefs map for module M" @@ -575,7 +575,7 @@ unit_bad_prim_type = case runTypecheckTestM NoSmartHoles $ do checkEverything NoSmartHoles CheckEverything - { trusted = [progModule newProg] + { trusted = progModules newProg , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo] } of Left err -> err @?= UnknownTypeConstructor (tcn ["M"] "NonExistant") diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index bf346e651..bceb1b4a7 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -18,128 +18,130 @@ ] ] }, - "progModule": { - "moduleDefs": { - "main": { - "contents": { - "astDefExpr": { - "contents": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "astDefName": { - "baseName": "main", - "qualifiedModule": [ - "M" - ] - }, - "astDefType": { - "contents": [ - 0, - { - "tag": "KType" - }, - null - ], - "tag": "TEmptyHole" - } - }, - "tag": "DefAST" - } - }, - "moduleName": [ - "M" - ], - "moduleTypes": { - "T": { - "contents": { - "astTypeDefConstructors": [ - { - "valConArgs": [ + "progModules": [ + { + "moduleDefs": { + "main": { + "contents": { + "astDefExpr": { + "contents": [ + 0, { - "contents": [ - [], - { - "contents": [ - [], - "b" - ], - "tag": "TVar" - }, - { - "contents": [ - [], - "a" - ], - "tag": "TVar" - } - ], - "tag": "TApp" + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" }, + null + ], + "tag": "EmptyHole" + }, + "astDefName": { + "baseName": "main", + "qualifiedModule": [ + "M" + ] + }, + "astDefType": { + "contents": [ + 0, { - "contents": [ - [], - { - "baseName": "Nat", - "qualifiedModule": [ - "Builtins" - ] - } - ], - "tag": "TCon" - } + "tag": "KType" + }, + null ], - "valConName": { - "baseName": "C", - "qualifiedModule": [ - "M" - ] - } + "tag": "TEmptyHole" } - ], - "astTypeDefName": { - "baseName": "T", - "qualifiedModule": [ - "M" - ] }, - "astTypeDefNameHints": [], - "astTypeDefParameters": [ - [ - "a", - { - "tag": "KType" - } - ], - [ - "b", + "tag": "DefAST" + } + }, + "moduleName": [ + "M" + ], + "moduleTypes": { + "T": { + "contents": { + "astTypeDefConstructors": [ { - "contents": [ + "valConArgs": [ { - "tag": "KType" + "contents": [ + [], + { + "contents": [ + [], + "b" + ], + "tag": "TVar" + }, + { + "contents": [ + [], + "a" + ], + "tag": "TVar" + } + ], + "tag": "TApp" }, { - "tag": "KType" + "contents": [ + [], + { + "baseName": "Nat", + "qualifiedModule": [ + "Builtins" + ] + } + ], + "tag": "TCon" } ], - "tag": "KFun" + "valConName": { + "baseName": "C", + "qualifiedModule": [ + "M" + ] + } } + ], + "astTypeDefName": { + "baseName": "T", + "qualifiedModule": [ + "M" + ] + }, + "astTypeDefNameHints": [], + "astTypeDefParameters": [ + [ + "a", + { + "tag": "KType" + } + ], + [ + "b", + { + "contents": [ + { + "tag": "KType" + }, + { + "tag": "KType" + } + ], + "tag": "KFun" + } + ] ] - ] - }, - "tag": "TypeDefAST" + }, + "tag": "TypeDefAST" + } } } - }, + ], "progSelection": { "selectedDef": { "baseName": "main", diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index c8d0188c9..c6ccbe444 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -17,128 +17,130 @@ ] ] }, - "progModule": { - "moduleDefs": { - "main": { - "contents": { - "astDefExpr": { - "contents": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "astDefName": { - "baseName": "main", - "qualifiedModule": [ - "M" - ] - }, - "astDefType": { - "contents": [ - 0, - { - "tag": "KType" - }, - null - ], - "tag": "TEmptyHole" - } - }, - "tag": "DefAST" - } - }, - "moduleName": [ - "M" - ], - "moduleTypes": { - "T": { - "contents": { - "astTypeDefConstructors": [ - { - "valConArgs": [ + "progModules": [ + { + "moduleDefs": { + "main": { + "contents": { + "astDefExpr": { + "contents": [ + 0, { - "contents": [ - [], - { - "contents": [ - [], - "b" - ], - "tag": "TVar" - }, - { - "contents": [ - [], - "a" - ], - "tag": "TVar" - } - ], - "tag": "TApp" + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" }, + null + ], + "tag": "EmptyHole" + }, + "astDefName": { + "baseName": "main", + "qualifiedModule": [ + "M" + ] + }, + "astDefType": { + "contents": [ + 0, { - "contents": [ - [], - { - "baseName": "Nat", - "qualifiedModule": [ - "Builtins" - ] - } - ], - "tag": "TCon" - } + "tag": "KType" + }, + null ], - "valConName": { - "baseName": "C", - "qualifiedModule": [ - "M" - ] - } + "tag": "TEmptyHole" } - ], - "astTypeDefName": { - "baseName": "T", - "qualifiedModule": [ - "M" - ] }, - "astTypeDefNameHints": [], - "astTypeDefParameters": [ - [ - "a", - { - "tag": "KType" - } - ], - [ - "b", + "tag": "DefAST" + } + }, + "moduleName": [ + "M" + ], + "moduleTypes": { + "T": { + "contents": { + "astTypeDefConstructors": [ { - "contents": [ + "valConArgs": [ { - "tag": "KType" + "contents": [ + [], + { + "contents": [ + [], + "b" + ], + "tag": "TVar" + }, + { + "contents": [ + [], + "a" + ], + "tag": "TVar" + } + ], + "tag": "TApp" }, { - "tag": "KType" + "contents": [ + [], + { + "baseName": "Nat", + "qualifiedModule": [ + "Builtins" + ] + } + ], + "tag": "TCon" } ], - "tag": "KFun" + "valConName": { + "baseName": "C", + "qualifiedModule": [ + "M" + ] + } } + ], + "astTypeDefName": { + "baseName": "T", + "qualifiedModule": [ + "M" + ] + }, + "astTypeDefNameHints": [], + "astTypeDefParameters": [ + [ + "a", + { + "tag": "KType" + } + ], + [ + "b", + { + "contents": [ + { + "tag": "KType" + }, + { + "tag": "KType" + } + ], + "tag": "KFun" + } + ] ] - ] - }, - "tag": "TypeDefAST" + }, + "tag": "TypeDefAST" + } } } - }, + ], "progSelection": { "selectedDef": { "baseName": "main",