From 7b801120b923f4e8b91e41443da07ee88fc00600 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 4 Mar 2022 16:32:08 +0000 Subject: [PATCH 1/7] test: show that SigAction can create holes in other defs --- primer/src/Primer/Action.hs | 1 + primer/test/Tests/Action/Prog.hs | 36 +++++++++++++++++++++++++++++++- 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index d028d6cf0..8459d7f59 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -401,6 +401,7 @@ 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. applyActionsToTypeSig :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index f6e2c8134..7d2b71746 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -9,7 +9,16 @@ import Control.Monad.Fresh import qualified Data.Map.Strict as Map import Optics import Primer.Action ( - Action (ConstructAnn, ConstructArrowL, ConstructGlobalVar, ConstructLet, Delete, EnterType, Move), + Action ( + ConstructAnn, + ConstructArrowL, + ConstructGlobalVar, + ConstructLet, + ConstructTCon, + Delete, + EnterType, + Move + ), Movement (Branch, Child1, Child2), ) import Primer.App ( @@ -364,6 +373,31 @@ unit_construct_arrow_in_sig = _ -> assertFailure "not a function" _ -> assertFailure "definition not found" +unit_sigaction_creates_holes :: Assertion +unit_sigaction_creates_holes = + let acts = + [ -- main :: Char + MoveToDef 0 + , SigAction [ConstructTCon "Char"] + , -- other :: Char; other = main + MoveToDef 2 + , SigAction [ConstructTCon "Char"] + , BodyAction [ConstructGlobalVar 0] + , -- main :: Int + -- We expect this to change 'other' to contain a hole + MoveToDef 0 + , SigAction [Delete, ConstructTCon "Int"] + ] + in progActionTest defaultPrimsProg acts $ + expectSuccess $ \_ prog' -> + case lookupASTDef 2 (progDefs prog') of + Just def -> + -- Check that the definition is a non-empty hole + case astDefExpr def of + Hole _ (GlobalVar _ 0) -> pure () + _ -> assertFailure "expected {? main ?}" + _ -> assertFailure "definition not found" + unit_copy_paste_duplicate :: Assertion unit_copy_paste_duplicate = do let ((p, fromDef, fromType, fromExpr, toDef, _toType, _toExpr), maxID) = create $ do From efd1651190f58bb6bef06fe824a9f748c3355090 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 4 Mar 2022 13:40:16 +0000 Subject: [PATCH 2/7] refactor!: Put Prog's code into a `Module` This is in preparation for having a Prog include imported modules. 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 | 14 +- primer/primer.cabal | 1 + primer/src/Primer/API.hs | 8 +- primer/src/Primer/Action.hs | 27 +-- primer/src/Primer/App.hs | 170 +++++++++------ primer/src/Primer/Module.hs | 12 ++ primer/test/Tests/Action/Prog.hs | 92 ++++---- primer/test/Tests/Serialization.hs | 8 +- .../serialization/edit_response_2.json | 200 +++++++++--------- primer/test/outputs/serialization/prog.json | 200 +++++++++--------- 10 files changed, 406 insertions(+), 326 deletions(-) create mode 100644 primer/src/Primer/Module.hs diff --git a/primer-rel8/test/TestUtils.hs b/primer-rel8/test/TestUtils.hs index 984887b6a..8f80a10c0 100644 --- a/primer-rel8/test/TestUtils.hs +++ b/primer-rel8/test/TestUtils.hs @@ -90,6 +90,13 @@ import Primer.Database.Rel8.Rel8Db ( runRel8Db, ) import Primer.Database.Rel8.Schema as Schema hiding (app) +import Primer.Module ( + Module ( + Module, + moduleDefs, + moduleTypes + ), + ) import Primer.Name (Name) import Primer.Primitives ( allPrimDefs, @@ -366,6 +373,9 @@ testApp = testProg :: Prog testProg = newEmptyProg - { progTypes = defaultTypeDefs - , progDefs = defs + { progModule = + Module + { moduleTypes = defaultTypeDefs + , moduleDefs = defs + } } diff --git a/primer/primer.cabal b/primer/primer.cabal index e166a7c77..fbe57708e 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -26,6 +26,7 @@ library Primer.Database Primer.Eval Primer.EvalFull + Primer.Module Primer.Name Primer.Name.Fresh Primer.Primitives diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs index af75d5c62..4d627d34c 100644 --- a/primer/src/Primer/API.hs +++ b/primer/src/Primer/API.hs @@ -70,8 +70,7 @@ import Primer.App ( handleMutationRequest, handleQuestion, initialApp, - progDefs, - progTypes, + progModule, runEditAppM, runQueryAppM, ) @@ -119,6 +118,7 @@ import qualified Primer.Database as Database ( Success ), ) +import Primer.Module (Module (moduleDefs, moduleTypes)) import Primer.Name (Name, unName) import qualified StmContainers.Map as StmMap @@ -326,7 +326,7 @@ instance ToJSON Def viewProg :: App.Prog -> Prog viewProg p = Prog - { types = typeDefName <$> progTypes p + { types = typeDefName <$> moduleTypes (progModule p) , defs = ( \d -> Def @@ -336,7 +336,7 @@ viewProg p = , term = viewTreeExpr . astDefExpr <$> defAST d } ) - <$> Map.elems (progDefs p) + <$> Map.elems (moduleDefs $ progModule p) } -- | A simple method to extract 'Tree's from 'Expr's. This is injective. diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 8459d7f59..1f47c9dd9 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -25,7 +25,7 @@ module Primer.Action ( uniquifyDefName, ) where -import Foreword +import Foreword hiding (mod) import Control.Monad.Fresh (MonadFresh) import Data.Aeson (Value) @@ -80,6 +80,7 @@ import Primer.Core.DSL ( import Primer.Core.Transform (renameTyVar, renameTyVarExpr, renameVar) import Primer.Core.Utils (forgetTypeIDs, generateTypeIDs) import Primer.JSON +import Primer.Module (Module (moduleDefs, moduleTypes)) import Primer.Name (Name, NameCounter, unName, unsafeMkName) import Primer.Name.Fresh ( isFresh, @@ -398,35 +399,37 @@ type ActionM m = , MonadReader TC.Cxt m -- has access to a typing context ) --- Apply a sequence of actions to the type signature of a definition +-- | 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. +-- 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. applyActionsToTypeSig :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> - [TypeDef] -> - Map ID Def -> + Module -> + -- | This must be one of the definitions in the @Module@ ASTDef -> [Action] -> - m (Either ActionError (ASTDef, Map ID Def, TypeZ)) -applyActionsToTypeSig smartHoles typeDefs defs def actions = - runReaderT go (buildTypingContext typeDefs defs smartHoles) + m (Either ActionError (ASTDef, Module, TypeZ)) +applyActionsToTypeSig smartHoles mod def actions = + runReaderT go (buildTypingContext (moduleTypes mod) (moduleDefs mod) smartHoles) & runExceptT where - go :: ActionM m => m (ASTDef, Map ID Def, 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) e <- check (forgetTypeIDs t) (astDefExpr def) let def' = def{astDefExpr = exprTtoExpr e, astDefType = t} - defs' = Map.insert (astDefID def) (DefAST def') defs + defs' = Map.insert (astDefID def) (DefAST def') $ moduleDefs mod + mod' = mod{moduleDefs = defs'} -- The actions were applied to the type successfully, and the definition body has been -- typechecked against the new type. -- Now we need to typecheck the whole program again, to check any uses of the definition -- We make sure that the updated type is present in the global context. - checkedDefs <- checkEverything smartHoles typeDefs defs' - pure (def', checkedDefs, zt) + checkedDefs <- checkEverything smartHoles (moduleTypes mod') (moduleDefs mod') + pure (def', mod'{moduleDefs = checkedDefs}, 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 aa92166d9..d907c6b89 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -47,7 +47,7 @@ module Primer.App ( defaultTypeDefs, ) where -import Foreword +import Foreword hiding (mod) import Control.Monad.Fresh (MonadFresh (..)) import Data.Aeson ( @@ -107,6 +107,7 @@ import Primer.Eval (EvalDetail, EvalError) import qualified Primer.Eval as Eval import Primer.EvalFull (Dir, EvalFullError (TimedOut), TerminationBound, evalFull) import Primer.JSON +import Primer.Module (Module (Module, moduleDefs, moduleTypes)) import Primer.Name (Name, NameCounter, freshName, unsafeMkName) import Primer.Primitives (allPrimDefs, allPrimTypeDefs) import Primer.Questions ( @@ -156,8 +157,9 @@ import Primer.Zipper ( -- need to send the log back and forth. -- But for now, to keep things simple, that's how it works. data Prog = Prog - { progTypes :: [TypeDef] - , progDefs :: Map ID Def -- The current program: a set of definitions indexed by ID + { -- In the future, we will also have some immutable imported modules + progModule :: Module + -- ^ The one editable "current" module , progSelection :: Maybe Selection , progSmartHoles :: SmartHoles , progLog :: Log -- The log of all actions @@ -165,6 +167,32 @@ data Prog = Prog deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON Prog +-- | Get all type definitions from all modules (including imports) +allTypes :: Prog -> [TypeDef] +allTypes = moduleTypes . progModule + +-- | Get all definitions from all modules (including imports) +allDefs :: Prog -> Map ID Def +allDefs = moduleDefs . progModule + +-- | Add a definition to the editable module +addDef :: ASTDef -> Prog -> Prog +addDef d p = + let mod = progModule p + defs = moduleDefs mod + defs' = Map.insert (astDefID d) (DefAST d) defs + mod' = mod{moduleDefs = defs'} + in p{progModule = mod'} + +-- | Add a type definition to the editable module +addTypeDef :: ASTTypeDef -> Prog -> Prog +addTypeDef t p = + let mod = progModule p + tydefs = moduleTypes mod + tydefs' = tydefs <> [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. @@ -263,18 +291,21 @@ data EvalFullResp -- * Request handlers -- | Handle a question +-- Note that these only consider the non-imported module as a location of which +-- to ask a question. However, they will return variables which are in scope by +-- dint of being imported. handleQuestion :: MonadQueryApp m => Question a -> m a handleQuestion = \case VariablesInScope defid exprid -> do node <- focusNode' defid exprid - progDefs <- asks $ progDefs . appProg + defs <- asks $ allDefs . appProg let (tyvars, termvars, globals) = case node of - Left zE -> variablesInScopeExpr progDefs zE + Left zE -> variablesInScopeExpr defs zE Right zT -> (variablesInScopeTy zT, [], []) pure ((tyvars, termvars), globals) GenerateName defid nodeid typeKind -> do - progTypeDefs <- asks $ progTypes . appProg - progDefs <- asks $ progDefs . appProg + progTypeDefs <- asks $ moduleTypes . progModule . appProg + progDefs <- asks $ moduleDefs . progModule . appProg names <- focusNode' defid nodeid <&> \case Left zE -> generateNameExpr typeKind zE @@ -286,9 +317,10 @@ handleQuestion = \case prog <- asks appProg focusNode prog defid nodeid +-- This only looks in the editable module, not in any imports focusNode :: MonadError ProgError m => Prog -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) focusNode prog defid nodeid = - case lookupASTDef defid (progDefs prog) of + case lookupASTDef defid (moduleDefs $ progModule prog) of Nothing -> throwError $ DefNotFound defid Just def -> let mzE = locToEither <$> focusOn nodeid (focus $ astDefExpr def) @@ -324,14 +356,14 @@ handleEditRequest actions = do handleEvalRequest :: MonadEditApp m => EvalReq -> m EvalResp handleEvalRequest req = do prog <- gets appProg - result <- Eval.step (progDefs prog) (evalReqExpr req) (evalReqRedex req) + result <- Eval.step (allDefs prog) (evalReqExpr req) (evalReqRedex req) case result of Left err -> throwError $ EvalError err Right (expr, detail) -> pure EvalResp { evalRespExpr = expr - , evalRespRedexes = Set.toList $ Eval.redexes (Map.mapMaybe defPrim $ progDefs prog) expr + , evalRespRedexes = Set.toList $ Eval.redexes (Map.mapMaybe defPrim $ allDefs prog) expr , evalRespDetail = detail } @@ -339,56 +371,61 @@ handleEvalRequest req = do handleEvalFullRequest :: MonadEditApp m => EvalFullReq -> m EvalFullResp handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do prog <- gets appProg - result <- evalFull (mkTypeDefMap $ progTypes prog) (progDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr + result <- evalFull (mkTypeDefMap $ allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr pure $ case result of Left (TimedOut e) -> EvalFullRespTimedOut e Right nf -> EvalFullRespNormal nf +-- Prog actions only affect the editable module applyProgAction :: MonadEditApp m => Prog -> Maybe ID -> ProgAction -> m (Prog, Maybe ID) applyProgAction prog mdefID = \case - MoveToDef id_ -> case Map.lookup id_ (progDefs prog) of + MoveToDef id_ -> case Map.lookup id_ (moduleDefs $ progModule prog) of Nothing -> throwError $ DefNotFound id_ Just _ -> pure (prog, Just id_) DeleteDef id_ - | Map.member id_ (progDefs prog) -> do - let defs = Map.delete id_ (progDefs prog) - prog' = prog{progDefs = defs, progSelection = Nothing} + | mod <- progModule prog + , Map.member id_ (moduleDefs mod) -> do + let modDefs' = Map.delete id_ $ moduleDefs mod + prog' = prog{progModule = mod{moduleDefs = modDefs'}, 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. - runExceptT (checkEverything @TypeError NoSmartHoles (progTypes prog) (progDefs prog')) >>= \case + -- TODO: when we add imports, we do not need to re-check those, as they will not have changed + runExceptT (checkEverything @TypeError NoSmartHoles (allTypes prog) (allDefs prog')) >>= \case Left _ -> throwError $ DefInUse id_ Right _ -> pure () pure (prog', Nothing) DeleteDef id_ -> throwError $ DefNotFound id_ - RenameDef id_ nameStr -> case lookupASTDef id_ (progDefs prog) of + RenameDef id_ nameStr -> case lookupASTDef id_ (moduleDefs $ progModule prog) of Nothing -> throwError $ DefNotFound id_ Just def -> do - let name = unsafeMkName nameStr - existingName = Map.lookupMin $ Map.filter ((== name) . defName) $ progDefs prog + let defs = moduleDefs $ progModule prog + name = unsafeMkName nameStr + existingName = Map.lookupMin $ Map.filter ((== name) . defName) defs case existingName of Just (existingID, _) -> throwError $ DefAlreadyExists name existingID Nothing -> do + -- Since references are by ID, which we do not change, there is no problem + -- if this definition is referenced anywhere let def' = def{astDefName = name} - let defs = Map.insert (astDefID def') (DefAST def') (progDefs prog) - pure (prog{progDefs = defs, progSelection = Just $ Selection def' Nothing}, mdefID) + pure (addDef def' prog{progSelection = Just $ Selection def' Nothing}, mdefID) CreateDef n -> do + let defs = moduleDefs $ progModule prog name <- case n of Just nameStr -> let name = unsafeMkName nameStr - existingName = Map.lookupMin $ Map.filter ((== name) . defName) $ progDefs prog + existingName = Map.lookupMin $ Map.filter ((== name) . defName) defs in case existingName of Just (existingID, _) -> throwError $ DefAlreadyExists name existingID Nothing -> pure name - Nothing -> freshName $ Set.fromList $ map defName $ Map.elems $ progDefs prog + Nothing -> freshName $ Set.fromList $ map defName $ Map.elems defs id_ <- fresh expr <- newExpr ty <- newType let def = ASTDef id_ name expr ty - defs = Map.insert id_ (DefAST def) (progDefs prog) - pure (prog{progDefs = defs, progSelection = Just $ Selection def Nothing}, Just id_) + pure (addDef def prog{progSelection = Just $ Selection def Nothing}, Just id_) AddTypeDef td -> do - runExceptT @TypeError (checkTypeDefs $ progTypes prog <> [TypeDefAST td]) >>= \case + runExceptT @TypeError (checkTypeDefs $ allTypes prog <> [TypeDefAST td]) >>= \case -- The frontend should never let this error case happen, -- so we just dump out a raw string for debugging/logging purposes -- (This is not currently true! We should synchronise the frontend with @@ -397,44 +434,44 @@ applyProgAction prog mdefID = \case -- but the TC rejects it. -- see https://github.com/hackworthltd/primer/issues/3) Left err -> throwError $ TypeDefError $ show err - Right _ -> pure (prog{progTypes = progTypes prog <> [TypeDefAST td]}, mdefID) + Right _ -> pure (addTypeDef td prog, mdefID) BodyAction actions -> do withDef mdefID prog $ \def -> do smartHoles <- gets $ progSmartHoles . appProg - res <- applyActionsToBody smartHoles (progTypes prog) (progDefs prog) def actions + res <- applyActionsToBody smartHoles (allTypes prog) (allDefs prog) def actions case res of Left err -> throwError $ ActionError err Right (def', z) -> do - let defs = Map.insert (astDefID def) (DefAST def') (progDefs prog) - meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z + let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z nodeId = either getID getID meta let prog' = - prog - { progDefs = defs - , progSelection = - Just $ - Selection def' $ - Just - NodeSelection - { nodeType = BodyNode - , nodeId - , meta - } - } + addDef + def' + prog + { progSelection = + Just $ + Selection def' $ + Just + NodeSelection + { nodeType = BodyNode + , nodeId + , meta + } + } pure (prog', mdefID) SigAction actions -> do withDef mdefID prog $ \def -> do smartHoles <- gets $ progSmartHoles . appProg - res <- applyActionsToTypeSig smartHoles (progTypes prog) (progDefs prog) def actions + res <- applyActionsToTypeSig smartHoles (progModule prog) def actions case res of Left err -> throwError $ ActionError err - Right (def', defs, zt) -> do + Right (def', mod', zt) -> do let node = target zt meta = view _typeMetaLens node nodeId = getID meta prog' = prog - { progDefs = defs + { progModule = mod' , progSelection = Just $ Selection def' $ @@ -459,12 +496,13 @@ applyProgAction prog mdefID = \case Just i -> (,mdefID) <$> copyPasteBody prog fromIds i setup -- Look up the definition by its given ID, then run the given action with it +-- only looks in the editable module withDef :: MonadEditApp m => Maybe ID -> Prog -> (ASTDef -> m a) -> m a withDef mdefID prog f = case mdefID of Nothing -> throwError NoDefSelected Just defid -> do - case lookupASTDef defid (progDefs prog) of + case lookupASTDef defid (moduleDefs $ progModule prog) of Nothing -> throwError $ DefNotFound defid Just def -> f def @@ -581,8 +619,11 @@ newEmptyProg = ty = TEmptyHole (Meta 2 Nothing Nothing) def = DefAST $ ASTDef 0 "main" expr ty in Prog - { progTypes = [] - , progDefs = Map.singleton 0 def + { progModule = + Module + { moduleTypes = [] + , moduleDefs = Map.singleton 0 def + } , progSelection = Nothing , progSmartHoles = SmartHoles , progLog = Log [] @@ -602,8 +643,11 @@ newEmptyApp = newProg :: Prog newProg = newEmptyProg - { progTypes = defaultTypeDefs - , progDefs = defaultDefs + { progModule = + Module + { moduleTypes = defaultTypeDefs + , moduleDefs = defaultDefs + } } defaultDefsNextId :: ID @@ -682,7 +726,7 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do -- 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 <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progTypes p) (progDefs p) def setup + doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progModule p) def setup tgt <- case doneSetup of Left err -> throwError $ ActionError err Right (_, _, tgt) -> pure $ focusOnlyType tgt @@ -698,11 +742,10 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do pasted <- case target tgt of TEmptyHole _ -> pure $ replace freshCopy tgt _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p) + oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p) let newDef = oldDef{astDefType = fromZipper pasted} - let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) - let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)} + let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)} tcWholeProg finalProg -- We cannot use bindersAbove as that works on names only, and different scopes @@ -764,8 +807,9 @@ tcWholeProg :: forall m. MonadEditApp m => Prog -> m Prog tcWholeProg p = let tc :: ReaderT Cxt (ExceptT ActionError m) Prog tc = do - defs' <- mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) (progDefs p) - let p' = p{progDefs = defs'} + defs' <- mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) (moduleDefs $ progModule p) + let mod' = (progModule p){moduleDefs = defs'} + let p' = p{progModule = mod'} -- We need to update the metadata cached in the selection let oldSel = progSelection p newSel <- case oldSel of @@ -789,7 +833,7 @@ tcWholeProg p = } pure $ p'{progSelection = newSel} in do - x <- runExceptT $ runReaderT tc $ buildTypingContext (progTypes p) (progDefs p) (progSmartHoles p) + x <- runExceptT $ runReaderT tc $ buildTypingContext (allTypes p) (allDefs p) (progSmartHoles p) case x of Left e -> throwError $ ActionError e Right prog -> pure prog @@ -805,7 +849,7 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do smartHoles <- gets $ progSmartHoles . appProg -- The Loc zipper captures all the changes, they are only reflected in the -- returned Def, which we thus ignore - doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToBody smartHoles (progTypes p) (progDefs p) def setup + doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToBody smartHoles (allTypes p) (allDefs p) def setup tgt <- case doneSetup of Left err -> throwError $ ActionError err Right (_, tgt) -> pure tgt @@ -826,11 +870,10 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do pasted <- case target tgtT of TEmptyHole _ -> pure $ replace freshCopy tgtT _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p) + oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p) let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted} - let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right) - let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)} + let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)} tcWholeProg finalProg (Left srcE, InExpr tgtE) -> do let sharedScope = @@ -880,11 +923,10 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do pasted <- case target tgtE of EmptyHole _ -> pure $ replace freshCopy tgtE _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole" - oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p) + oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p) let newDef = oldDef{astDefExpr = unfocusExpr pasted} - let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left) - let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)} + let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)} tcWholeProg finalProg lookupASTDef :: ID -> Map ID Def -> Maybe ASTDef diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs new file mode 100644 index 000000000..7c3e69e87 --- /dev/null +++ b/primer/src/Primer/Module.hs @@ -0,0 +1,12 @@ +module Primer.Module (Module (..)) where + +import Foreword +import Primer.Core (Def, ID, TypeDef) +import Primer.JSON + +data Module = Module + { moduleTypes :: [TypeDef] + , moduleDefs :: Map ID Def -- The current program: a set of definitions indexed by ID + } + deriving (Eq, Show, Generic) + deriving (FromJSON, ToJSON) via VJSON Module diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 7d2b71746..ed279d015 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -76,6 +76,7 @@ import Primer.Core.DSL ( tvar, var, ) +import Primer.Module (Module (moduleDefs, moduleTypes)) import Primer.Name import Primer.Primitives (allPrimTypeDefs) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=)) @@ -100,18 +101,18 @@ unit_move_to_def_and_construct_let :: Assertion unit_move_to_def_and_construct_let = progActionTest defaultEmptyProg [MoveToDef 2, BodyAction [ConstructLet (Just "x")]] $ expectSuccess $ \prog prog' -> - case astDefExpr <$> lookupASTDef 2 (progDefs prog') of + case astDefExpr <$> lookupASTDef 2 (moduleDefs $ progModule prog') of Just Let{} -> -- Check that main is unchanged - Map.lookup 0 (progDefs prog') @?= Map.lookup 0 (progDefs prog) + Map.lookup 0 (moduleDefs $ progModule prog') @?= Map.lookup 0 (moduleDefs $ progModule prog) _ -> assertFailure "definition not found" unit_rename_def :: Assertion unit_rename_def = progActionTest defaultEmptyProg [RenameDef 2 "foo"] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup 2 (progDefs prog')) @?= Just "foo" - fmap defName (Map.lookup 0 (progDefs prog')) @?= Just "main" + fmap defName (Map.lookup 2 (moduleDefs $ progModule prog')) @?= Just "foo" + fmap defName (Map.lookup 0 (moduleDefs $ progModule prog')) @?= Just "main" unit_rename_def_to_same_name_as_existing_def :: Assertion unit_rename_def_to_same_name_as_existing_def = @@ -127,8 +128,8 @@ unit_delete_def :: Assertion unit_delete_def = progActionTest defaultEmptyProg [DeleteDef 2] $ expectSuccess $ \_ prog' -> do - fmap defName (Map.lookup 2 (progDefs prog')) @?= Nothing - fmap defName (Map.lookup 0 (progDefs prog')) @?= Just "main" + fmap defName (Map.lookup 2 (moduleDefs $ progModule prog')) @?= Nothing + fmap defName (Map.lookup 0 (moduleDefs $ progModule prog')) @?= Just "main" unit_delete_def_unknown_id :: Assertion unit_delete_def_unknown_id = @@ -144,7 +145,7 @@ unit_delete_def_used_id = unit_delete_def_recursive :: Assertion unit_delete_def_recursive = progActionTest defaultEmptyProg [MoveToDef 0, BodyAction [ConstructGlobalVar 0], DeleteDef 0] $ - expectSuccess $ \prog prog' -> Map.delete 0 (progDefs prog) @?= progDefs prog' + expectSuccess $ \prog prog' -> Map.delete 0 (moduleDefs $ progModule prog) @?= moduleDefs (progModule prog') unit_move_to_unknown_def :: Assertion unit_move_to_unknown_def = @@ -161,8 +162,8 @@ unit_construct_let_without_moving_to_def_first = unit_create_def :: Assertion unit_create_def = progActionTest defaultEmptyProg [CreateDef $ Just "newDef"] $ expectSuccess $ \_ prog' -> do - case lookupASTDef 4 (progDefs prog') of - Nothing -> assertFailure $ show $ progDefs prog' + case lookupASTDef 4 (moduleDefs $ progModule prog') of + Nothing -> assertFailure $ show $ moduleDefs $ progModule prog' Just def -> do astDefID def @?= 4 astDefName def @?= "newDef" @@ -195,11 +196,11 @@ unit_create_typedef = in progActionTest defaultEmptyProg [AddTypeDef lst, AddTypeDef tree] $ expectSuccess $ \_ prog' -> do - case progTypes prog' of + case moduleTypes $ progModule prog' of [lst', tree'] -> do TypeDefAST lst @=? lst' TypeDefAST tree @=? tree' - _ -> assertFailure $ show $ progTypes prog' + _ -> assertFailure $ show $ moduleTypes $ progModule prog' -- "List" is unknown here unit_create_typedef_bad_1 :: Assertion @@ -333,7 +334,7 @@ unit_create_typedef_8 = , astTypeDefNameHints = [] } in progActionTest defaultEmptyProg [AddTypeDef td] $ - expectSuccess $ \_ prog' -> progTypes prog' @?= [TypeDefAST td] + expectSuccess $ \_ prog' -> moduleTypes (progModule prog') @?= [TypeDefAST td] -- Allow clash between type name and constructor name across types unit_create_typedef_9 :: Assertion @@ -353,13 +354,13 @@ unit_create_typedef_9 = , astTypeDefNameHints = [] } in progActionTest defaultEmptyProg [AddTypeDef td1, AddTypeDef td2] $ - expectSuccess $ \_ prog' -> progTypes prog' @?= [TypeDefAST td1, TypeDefAST td2] + expectSuccess $ \_ prog' -> moduleTypes (progModule prog') @?= [TypeDefAST td1, TypeDefAST td2] unit_construct_arrow_in_sig :: Assertion unit_construct_arrow_in_sig = progActionTest defaultEmptyProg [MoveToDef 2, SigAction [ConstructArrowL, Move Child1]] $ expectSuccess $ \_ prog' -> - case lookupASTDef 2 (progDefs prog') of + case lookupASTDef 2 (moduleDefs $ progModule prog') of Just def -> -- Check that the signature is an arrow type case astDefType def of @@ -390,7 +391,7 @@ unit_sigaction_creates_holes = ] in progActionTest defaultPrimsProg acts $ expectSuccess $ \_ prog' -> - case lookupASTDef 2 (progDefs prog') of + case lookupASTDef 2 (moduleDefs $ progModule prog') of Just def -> -- Check that the definition is a non-empty hole case astDefExpr def of @@ -408,7 +409,8 @@ unit_copy_paste_duplicate = do blankID <- fresh blankDef <- ASTDef blankID "blank" <$> emptyHole <*> tEmptyHole pure - ( newProg{progDefs = Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)], progSelection = Nothing} + ( newProg{progSelection = Nothing} + & #progModule % #moduleDefs .~ Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)] , mainID , getID mainType , getID mainExpr @@ -424,12 +426,12 @@ 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 (progDefs tcp) + let src = lookupASTDef fromDef (moduleDefs $ progModule tcp) clearIDs = set (_Just % _defIDs) 0 in do - src @?= lookupASTDef fromDef (progDefs r) - assertBool "equal to toDef" $ src /= lookupASTDef toDef (progDefs r) - clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (progDefs r)) + src @?= lookupASTDef fromDef (moduleDefs $ progModule r) + assertBool "equal to toDef" $ src /= lookupASTDef toDef (moduleDefs $ progModule r) + clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (moduleDefs $ progModule r)) -- ∀a . (∀b,c . a -> b -> ∀d. c -> d) -> ∀c. ? -- copy ^------------------^ @@ -452,10 +454,10 @@ unit_copy_paste_type_scoping = do defInitial <- ASTDef defID' "main" <$> emptyHole <*> skel tEmptyHole expected <- ASTDef defID' "main" <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d")) pure - ( newEmptyProg{progDefs = Map.fromList [(defID', DefAST defInitial)]} + ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] , defID' , getID toCopy - , newEmptyProg{progDefs = Map.fromList [(defID', DefAST expected)]} + , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Move Child2, Move Child1]] @@ -467,7 +469,7 @@ unit_copy_paste_type_scoping = do -- we need the cached kinds to match up let clearIDs = set (traversed % #_DefAST % _defIDs) 0 in -- clearIDs (set (_Just % #defName) "blank" src ) @?= clearIDs (Map.lookup toDef (progDefs r)) - clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected) + clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) -- ∀a b.a ~> ∀a.a unit_raise :: Assertion @@ -478,10 +480,10 @@ unit_raise = do defInitial <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy) expected <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tvar "a") pure - ( newEmptyProg{progDefs = Map.fromList [(defID', DefAST defInitial)]} + ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] , defID' , getID toCopy - , newEmptyProg{progDefs = Map.fromList [(defID', DefAST expected)]} + , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Delete]] @@ -492,7 +494,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 (progDefs r) @?= clearIDs (progDefs tcpExpected) + in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule 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 @@ -520,10 +522,10 @@ unit_copy_paste_expr_1 = do defInitial <- ASTDef defID' "main" <$> skel emptyHole <*> pure ty expected <- ASTDef defID' "main" <$> skel (pure expectPasted) <*> pure ty pure - ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]} + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] , defID' , getID toCopy - , newProg{progDefs = Map.fromList [(defID', DefAST expected)]} + , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [Move Child1, Move Child1, Move (Branch "Nil")]] @@ -534,7 +536,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 (progDefs r) @?= clearIDs (progDefs tcpExpected) + in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) unit_copy_paste_ann :: Assertion unit_copy_paste_ann = do @@ -545,7 +547,7 @@ unit_copy_paste_ann = do blankID <- fresh blankDef <- ASTDef blankID "blank" <$> emptyHole `ann` tEmptyHole <*> tEmptyHole pure - ( newProg{progDefs = Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)], progSelection = Nothing} + ( newProg{progSelection = Nothing} & #progModule % #moduleDefs .~ Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)] , mainID , getID toCopy , blankID @@ -558,12 +560,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 (progDefs tcp) + let src = lookupASTDef fromDef (moduleDefs $ progModule tcp) clearIDs = set (_Just % _defIDs) 0 in do - src @?= lookupASTDef fromDef (progDefs r) - assertBool "equal to toDef" $ src /= lookupASTDef toDef (progDefs r) - clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (progDefs r)) + src @?= lookupASTDef fromDef (moduleDefs $ progModule r) + assertBool "equal to toDef" $ src /= lookupASTDef toDef (moduleDefs $ progModule r) + clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (moduleDefs $ progModule r)) unit_copy_paste_ann2sig :: Assertion unit_copy_paste_ann2sig = do @@ -573,10 +575,10 @@ unit_copy_paste_ann2sig = do defInitial <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole expected <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tcon "Bool" pure - ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]} + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] , defID' , getID toCopy - , newProg{progDefs = Map.fromList [(defID', DefAST expected)]} + , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [MoveToDef defID, CopyPasteSig (defID, srcID) []] @@ -587,7 +589,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 (progDefs r) @?= clearIDs (progDefs tcpExpected) + in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) unit_copy_paste_sig2ann :: Assertion unit_copy_paste_sig2ann = do @@ -597,10 +599,10 @@ unit_copy_paste_sig2ann = do defInitial <- ASTDef defID' "main" <$> emptyHole <*> pure toCopy expected <- ASTDef defID' "main" <$> emptyHole `ann` tcon "Bool" <*> pure toCopy pure - ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]} + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] , defID' , getID toCopy - , newProg{progDefs = Map.fromList [(defID', DefAST expected)]} + , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] ) let a = newApp{appProg = pInitial} actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [ConstructAnn, EnterType]] @@ -611,7 +613,7 @@ 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 (progDefs r) @?= clearIDs (progDefs tcpExpected) + in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) -- * Utilities @@ -626,8 +628,7 @@ defaultEmptyProg = do otherDef = ASTDef 2 "other" otherExpr otherType in pure $ newEmptyProg - { progDefs = Map.fromList [(0, DefAST mainDef), (2, DefAST otherDef)] - , progSelection = + { progSelection = Just $ Selection mainDef $ Just @@ -637,6 +638,9 @@ defaultEmptyProg = do , meta = Left (Meta 1 Nothing Nothing) } } + & #progModule + % #moduleDefs + .~ Map.fromList [(0, DefAST mainDef), (2, DefAST otherDef)] -- `defaultEmptyProg`, plus all primitive definitions (types and terms) defaultPrimsProg :: MonadFresh ID m => m Prog @@ -644,8 +648,8 @@ defaultPrimsProg = do p <- defaultEmptyProg withPrimDefs $ \_ m -> pure $ - over #progTypes ((TypeDefPrim <$> toList allPrimTypeDefs) <>) - . over #progDefs ((DefPrim <$> m) <>) + over (#progModule % #moduleTypes) ((TypeDefPrim <$> toList allPrimTypeDefs) <>) + . over (#progModule % #moduleDefs) ((DefPrim <$> m) <>) $ p _defIDs :: Traversal' ASTDef ID diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 6e5d2703d..80324e30f 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -42,6 +42,7 @@ import Primer.Core ( TypeMeta, ValCon (..), ) +import Primer.Module (Module (Module, moduleDefs, moduleTypes)) import Primer.Name (unsafeMkName) import Primer.Typecheck (SmartHoles (SmartHoles)) import System.FilePath (takeBaseName) @@ -108,8 +109,11 @@ fixtures = progaction = MoveToDef 0 prog = Prog - { progTypes = [typeDef] - , progDefs = Map.singleton 1 (DefAST def) + { progModule = + Module + { moduleTypes = [typeDef] + , moduleDefs = Map.singleton 1 (DefAST def) + } , progSelection = Just selection , progSmartHoles = SmartHoles , progLog = log diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index d1e2c2178..6ba91e8d9 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -1,38 +1,5 @@ { "Right": { - "progDefs": { - "1": { - "contents": { - "astDefExpr": { - "contents": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "astDefID": 1, - "astDefName": "main", - "astDefType": { - "contents": [ - 0, - { - "tag": "KType" - }, - null - ], - "tag": "TEmptyHole" - } - }, - "tag": "DefAST" - } - }, "progLog": { "unlog": [ [ @@ -50,6 +17,106 @@ ] ] }, + "progModule": { + "moduleDefs": { + "1": { + "contents": { + "astDefExpr": { + "contents": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" + }, + null + ], + "tag": "EmptyHole" + }, + "astDefID": 1, + "astDefName": "main", + "astDefType": { + "contents": [ + 0, + { + "tag": "KType" + }, + null + ], + "tag": "TEmptyHole" + } + }, + "tag": "DefAST" + } + }, + "moduleTypes": [ + { + "contents": { + "astTypeDefConstructors": [ + { + "valConArgs": [ + { + "contents": [ + [], + { + "contents": [ + [], + "b" + ], + "tag": "TCon" + }, + { + "contents": [ + [], + "a" + ], + "tag": "TCon" + } + ], + "tag": "TApp" + }, + { + "contents": [ + [], + "Nat" + ], + "tag": "TCon" + } + ], + "valConName": "C" + } + ], + "astTypeDefName": "T", + "astTypeDefNameHints": [], + "astTypeDefParameters": [ + [ + "a", + { + "tag": "KType" + } + ], + [ + "b", + { + "contents": [ + { + "tag": "KType" + }, + { + "tag": "KType" + } + ], + "tag": "KFun" + } + ] + ] + }, + "tag": "TypeDefAST" + } + ] + }, "progSelection": { "selectedDef": { "astDefExpr": { @@ -101,71 +168,6 @@ }, "progSmartHoles": { "tag": "SmartHoles" - }, - "progTypes": [ - { - "contents": { - "astTypeDefConstructors": [ - { - "valConArgs": [ - { - "contents": [ - [], - { - "contents": [ - [], - "b" - ], - "tag": "TCon" - }, - { - "contents": [ - [], - "a" - ], - "tag": "TCon" - } - ], - "tag": "TApp" - }, - { - "contents": [ - [], - "Nat" - ], - "tag": "TCon" - } - ], - "valConName": "C" - } - ], - "astTypeDefName": "T", - "astTypeDefNameHints": [], - "astTypeDefParameters": [ - [ - "a", - { - "tag": "KType" - } - ], - [ - "b", - { - "contents": [ - { - "tag": "KType" - }, - { - "tag": "KType" - } - ], - "tag": "KFun" - } - ] - ] - }, - "tag": "TypeDefAST" - } - ] + } } } \ No newline at end of file diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index 470e2fce1..a5fb275cf 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -1,37 +1,4 @@ { - "progDefs": { - "1": { - "contents": { - "astDefExpr": { - "contents": [ - 0, - { - "contents": { - "contents": [], - "tag": "TEmptyHole" - }, - "tag": "TCSynthed" - }, - null - ], - "tag": "EmptyHole" - }, - "astDefID": 1, - "astDefName": "main", - "astDefType": { - "contents": [ - 0, - { - "tag": "KType" - }, - null - ], - "tag": "TEmptyHole" - } - }, - "tag": "DefAST" - } - }, "progLog": { "unlog": [ [ @@ -49,6 +16,106 @@ ] ] }, + "progModule": { + "moduleDefs": { + "1": { + "contents": { + "astDefExpr": { + "contents": [ + 0, + { + "contents": { + "contents": [], + "tag": "TEmptyHole" + }, + "tag": "TCSynthed" + }, + null + ], + "tag": "EmptyHole" + }, + "astDefID": 1, + "astDefName": "main", + "astDefType": { + "contents": [ + 0, + { + "tag": "KType" + }, + null + ], + "tag": "TEmptyHole" + } + }, + "tag": "DefAST" + } + }, + "moduleTypes": [ + { + "contents": { + "astTypeDefConstructors": [ + { + "valConArgs": [ + { + "contents": [ + [], + { + "contents": [ + [], + "b" + ], + "tag": "TCon" + }, + { + "contents": [ + [], + "a" + ], + "tag": "TCon" + } + ], + "tag": "TApp" + }, + { + "contents": [ + [], + "Nat" + ], + "tag": "TCon" + } + ], + "valConName": "C" + } + ], + "astTypeDefName": "T", + "astTypeDefNameHints": [], + "astTypeDefParameters": [ + [ + "a", + { + "tag": "KType" + } + ], + [ + "b", + { + "contents": [ + { + "tag": "KType" + }, + { + "tag": "KType" + } + ], + "tag": "KFun" + } + ] + ] + }, + "tag": "TypeDefAST" + } + ] + }, "progSelection": { "selectedDef": { "astDefExpr": { @@ -100,70 +167,5 @@ }, "progSmartHoles": { "tag": "SmartHoles" - }, - "progTypes": [ - { - "contents": { - "astTypeDefConstructors": [ - { - "valConArgs": [ - { - "contents": [ - [], - { - "contents": [ - [], - "b" - ], - "tag": "TCon" - }, - { - "contents": [ - [], - "a" - ], - "tag": "TCon" - } - ], - "tag": "TApp" - }, - { - "contents": [ - [], - "Nat" - ], - "tag": "TCon" - } - ], - "valConName": "C" - } - ], - "astTypeDefName": "T", - "astTypeDefNameHints": [], - "astTypeDefParameters": [ - [ - "a", - { - "tag": "KType" - } - ], - [ - "b", - { - "contents": [ - { - "tag": "KType" - }, - { - "tag": "KType" - } - ], - "tag": "KFun" - } - ] - ] - }, - "tag": "TypeDefAST" - } - ] + } } \ No newline at end of file From d5158c064ee429f5ed6333ae8215c47128e2ac1d Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 7 Mar 2022 18:13:57 +0000 Subject: [PATCH 3/7] refactor: rename local defID to avoid shadowing Core.defID We will shortly want to import Primer.Core(defID), and want to avoid CI failures due to -Werror -Wname-shadowing. --- primer/test/Tests/Action/Prog.hs | 80 ++++++++++++++++---------------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index ed279d015..18a7fe200 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -447,20 +447,20 @@ unit_copy_paste_duplicate = do -- - The d is bound within the copied subtree, so it is in-scope unit_copy_paste_type_scoping :: Assertion unit_copy_paste_type_scoping = do - let ((pInitial, defID, srcID, pExpected), maxID) = create $ do + let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do toCopy <- tvar "a" `tfun` tvar "b" `tfun` tforall "d" KType (tvar "c" `tfun` tvar "d") let skel r = tforall "a" KType $ tfun (tforall "b" KType $ tforall "c" KType $ pure toCopy) $ tforall "c" KType r - defID' <- fresh - defInitial <- ASTDef defID' "main" <$> emptyHole <*> skel tEmptyHole - expected <- ASTDef defID' "main" <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d")) + definitionID' <- fresh + defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> skel tEmptyHole + expected <- ASTDef definitionID' "main" <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d")) pure - ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] - , defID' + ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)] + , definitionID' , getID toCopy - , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] + , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} - actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Move Child2, Move Child1]] + actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) [Move Child1, Move Child2, Move Child1]] (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions case result of Left e -> assertFailure $ show e @@ -474,19 +474,19 @@ unit_copy_paste_type_scoping = do -- ∀a b.a ~> ∀a.a unit_raise :: Assertion unit_raise = do - let ((pInitial, defID, srcID, pExpected), maxID) = create $ do - defID' <- fresh + let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do + definitionID' <- fresh toCopy <- tvar "a" - defInitial <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy) - expected <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tvar "a") + defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy) + expected <- ASTDef definitionID' "main" <$> emptyHole <*> tforall "a" KType (tvar "a") pure - ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] - , defID' + ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)] + , definitionID' , getID toCopy - , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] + , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)] ) let a = newEmptyApp{appProg = pInitial} - actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Delete]] + actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) [Move Child1, Delete]] (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions case result of Left e -> assertFailure $ show e @@ -502,8 +502,8 @@ unit_raise = do -- /\a . λ x . case x of Nil -> lettype b = ? in let y = ? : a in Pair @a @b y z ; Cons y ys -> /\@b z -> Pair @a @b y z unit_copy_paste_expr_1 :: Assertion unit_copy_paste_expr_1 = do - let ((pInitial, defID, srcID, pExpected), maxID) = create $ do - defID' <- fresh + let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do + definitionID' <- fresh ty <- tforall "a" KType $ (tcon "List" `tapp` tvar "a") `tfun` tforall "b" KType (tvar "b" `tfun` (tcon "Pair" `tapp` tvar "a" `tapp` tvar "b")) let toCopy' = con "MakePair" `aPP` tvar "a" `aPP` tvar "b" `app` var "y" `app` var "z" -- want different IDs for the two occurences in expected toCopy <- toCopy' @@ -519,16 +519,16 @@ unit_copy_paste_expr_1 = do -- TODO: in the future we may want to insert let bindings for variables -- which are out of scope in the target, and produce something like -- expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy' - defInitial <- ASTDef defID' "main" <$> skel emptyHole <*> pure ty - expected <- ASTDef defID' "main" <$> skel (pure expectPasted) <*> pure ty + defInitial <- ASTDef definitionID' "main" <$> skel emptyHole <*> pure ty + expected <- ASTDef definitionID' "main" <$> skel (pure expectPasted) <*> pure ty pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] - , defID' + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)] + , definitionID' , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] + , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)] ) let a = newApp{appProg = pInitial} - actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [Move Child1, Move Child1, Move (Branch "Nil")]] + actions = [MoveToDef definitionID, CopyPasteBody (definitionID, srcID) [Move Child1, Move Child1, Move (Branch "Nil")]] (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions case result of Left e -> assertFailure $ show e @@ -569,19 +569,19 @@ unit_copy_paste_ann = do unit_copy_paste_ann2sig :: Assertion unit_copy_paste_ann2sig = do - let ((pInitial, defID, srcID, pExpected), maxID) = create $ do - defID' <- fresh + let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do + definitionID' <- fresh toCopy <- tcon "Bool" - defInitial <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole - expected <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tcon "Bool" + defInitial <- ASTDef definitionID' "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole + expected <- ASTDef definitionID' "main" <$> emptyHole `ann` pure toCopy <*> tcon "Bool" pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] - , defID' + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)] + , definitionID' , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] + , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)] ) let a = newApp{appProg = pInitial} - actions = [MoveToDef defID, CopyPasteSig (defID, srcID) []] + actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) []] (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions case result of Left e -> assertFailure $ show e @@ -593,19 +593,19 @@ unit_copy_paste_ann2sig = do unit_copy_paste_sig2ann :: Assertion unit_copy_paste_sig2ann = do - let ((pInitial, defID, srcID, pExpected), maxID) = create $ do - defID' <- fresh + let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do + definitionID' <- fresh toCopy <- tcon "Bool" - defInitial <- ASTDef defID' "main" <$> emptyHole <*> pure toCopy - expected <- ASTDef defID' "main" <$> emptyHole `ann` tcon "Bool" <*> pure toCopy + defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> pure toCopy + expected <- ASTDef definitionID' "main" <$> emptyHole `ann` tcon "Bool" <*> pure toCopy pure - ( newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST defInitial)] - , defID' + ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)] + , definitionID' , getID toCopy - , newProg & #progModule % #moduleDefs .~ Map.fromList [(defID', DefAST expected)] + , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)] ) let a = newApp{appProg = pInitial} - actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [ConstructAnn, EnterType]] + actions = [MoveToDef definitionID, CopyPasteBody (definitionID, srcID) [ConstructAnn, EnterType]] (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions case result of Left e -> assertFailure $ show e From 7edc13e1e6c48b56c929d58ab4e689e974a5af2b Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 4 Mar 2022 19:57:17 +0000 Subject: [PATCH 4/7] feat!: Progs can contain imported modules We enable Primer programs to import modules. This is achieved by adding a `progImports :: [Module]` field to `Prog`. The imported modules are each immutable (via the api). This immutability is ensured by having all the actions only operate on the one "current" module (that comprises the old `progDefs` and `progTypes`). (For now, the set itself is also immutable via the api.) For now we don't have any namespacing, we just lookup references in all modules and assume unique names. We leave adding hierarchical names for future work. We also leave having multiple editable modules for future work. 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/src/Primer/Action.hs | 19 +++++- primer/src/Primer/App.hs | 34 +++++++++-- primer/test/Tests/Action/Prog.hs | 60 ++++++++++++++++++- primer/test/Tests/Serialization.hs | 3 +- .../serialization/edit_response_2.json | 1 + primer/test/outputs/serialization/prog.json | 1 + 6 files changed, 107 insertions(+), 11 deletions(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index 1f47c9dd9..dd5ffefe4 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -407,13 +407,20 @@ type ActionM m = applyActionsToTypeSig :: (MonadFresh ID m, MonadFresh NameCounter m) => SmartHoles -> + [Module] -> Module -> -- | This must be one of the definitions in the @Module@ ASTDef -> [Action] -> m (Either ActionError (ASTDef, Module, TypeZ)) -applyActionsToTypeSig smartHoles mod def actions = - runReaderT go (buildTypingContext (moduleTypes mod) (moduleDefs mod) smartHoles) +applyActionsToTypeSig smartHoles imports mod def actions = + runReaderT + go + ( buildTypingContext + (concatMap moduleTypes $ mod : imports) + (foldMap moduleDefs $ mod : imports) + smartHoles + ) & runExceptT where go :: ActionM m => m (ASTDef, Module, TypeZ) @@ -428,7 +435,13 @@ applyActionsToTypeSig smartHoles mod def actions = -- typechecked against the new type. -- Now we need to typecheck the whole program again, to check any uses of the definition -- We make sure that the updated type is present in the global context. - checkedDefs <- checkEverything smartHoles (moduleTypes mod') (moduleDefs mod') + -- Here we just check the whole prog, including imports. + -- TODO: for efficiency, we should not check the immutable imports + checkedDefs <- + checkEverything + smartHoles + (concatMap moduleTypes $ mod' : imports) + (foldMap moduleDefs $ mod' : imports) pure (def', mod'{moduleDefs = checkedDefs}, zt) -- Actions expect that all ASTs have a top-level expression of some sort. -- Signatures don't have this: they're just a type. diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index d907c6b89..59debfd53 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -157,8 +157,9 @@ import Primer.Zipper ( -- need to send the log back and forth. -- But for now, to keep things simple, that's how it works. data Prog = Prog - { -- In the future, we will also have some immutable imported modules - progModule :: Module + { progImports :: [Module] + -- ^ Some immutable imported modules + , progModule :: Module -- ^ The one editable "current" module , progSelection :: Maybe Selection , progSmartHoles :: SmartHoles @@ -167,13 +168,31 @@ data Prog = Prog deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON Prog +-- Note [Modules] +-- The invariant is that the @progImports@ modules are never edited, but +-- one can insert new ones (and perhaps delete unneeded ones). +-- +-- Currently we assume that all Names and IDs are globally unique (across +-- all the imported and editable modules). We intend to lift this restriction +-- shortly by introducing unique module identifiers. Since the user has no +-- control over IDs, this means that importing modules is unsafe: either it may +-- break this invariant, or it could fail with no way for a end-user to fix it. +-- (Or it would have to do a lot of work to uniquify names and ids, and then +-- bear this in mind when importing further modules that may reference these.) +-- Since we do not yet expose any way for an end-user to import modules, this +-- restriction is not particularly severe in practice. +-- +-- All modules in a @Prog@ shall be well-typed, in the appropriate scope: +-- all the imports are in one mutual dependency group +-- the @progModule@ has all the imports in scope + -- | Get all type definitions from all modules (including imports) allTypes :: Prog -> [TypeDef] allTypes = moduleTypes . progModule -- | Get all definitions from all modules (including imports) allDefs :: Prog -> Map ID Def -allDefs = moduleDefs . progModule +allDefs p = foldMap moduleDefs $ progModule p : progImports p -- | Add a definition to the editable module addDef :: ASTDef -> Prog -> Prog @@ -462,7 +481,7 @@ applyProgAction prog mdefID = \case SigAction actions -> do withDef mdefID prog $ \def -> do smartHoles <- gets $ progSmartHoles . appProg - res <- applyActionsToTypeSig smartHoles (progModule prog) def actions + res <- applyActionsToTypeSig smartHoles (progImports prog) (progModule prog) def actions case res of Left err -> throwError $ ActionError err Right (def', mod', zt) -> do @@ -619,7 +638,8 @@ newEmptyProg = ty = TEmptyHole (Meta 2 Nothing Nothing) def = DefAST $ ASTDef 0 "main" expr ty in Prog - { progModule = + { progImports = mempty + , progModule = Module { moduleTypes = [] , moduleDefs = Map.singleton 0 def @@ -726,7 +746,7 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do -- 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 <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progModule p) def setup + doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progImports p) (progModule p) def setup tgt <- case doneSetup of Left err -> throwError $ ActionError err Right (_, _, tgt) -> pure $ focusOnlyType tgt @@ -803,6 +823,8 @@ 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. tcWholeProg :: forall m. MonadEditApp m => Prog -> m Prog tcWholeProg p = let tc :: ReaderT Cxt (ExceptT ActionError m) Prog diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 18a7fe200..607bd152b 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -7,6 +7,7 @@ import Foreword import Control.Monad.Fresh import qualified Data.Map.Strict as Map +import Data.Tuple.Extra (snd3) import Optics import Primer.Action ( Action ( @@ -29,8 +30,10 @@ import Primer.App ( Prog (..), ProgAction (..), ProgError (..), + Question (VariablesInScope), Selection (..), handleEditRequest, + handleQuestion, lookupASTDef, newApp, newEmptyApp, @@ -49,6 +52,7 @@ import Primer.Core ( Type' (..), TypeDef (..), ValCon (..), + defID, defName, getID, _exprMeta, @@ -76,7 +80,7 @@ import Primer.Core.DSL ( tvar, var, ) -import Primer.Module (Module (moduleDefs, moduleTypes)) +import Primer.Module (Module (Module, moduleDefs, moduleTypes)) import Primer.Name import Primer.Primitives (allPrimTypeDefs) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=)) @@ -615,8 +619,52 @@ unit_copy_paste_sig2ann = do let clearIDs = set (traversed % #_DefAST % _defIDs) 0 in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected) +-- VariablesInScope sees imported terms +unit_import_vars :: Assertion +unit_import_vars = + let (prog, maxID) = create defaultImportProg + a = newEmptyApp{appProg = prog} + test = do + prog' <- handleEditRequest [CreateDef Nothing] + case Map.assocs $ moduleDefs $ progModule prog' of + [(i, DefAST d)] -> do + a' <- get + (_, vs) <- runReaderT (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) a' + pure $ + assertBool "VariablesInScope did not report the imported Int.+" $ + any ((== "Int.+") . snd3) vs + _ -> pure $ assertFailure "Expected one def which was just created" + in case fst $ runAppTestM maxID a test of + Left err -> assertFailure $ show err + Right assertion -> assertion + +-- Can reference something in an imported module (both types and terms) +unit_import_reference :: Assertion +unit_import_reference = + let (prog, maxID) = create defaultImportProg + a = newEmptyApp{appProg = prog} + test = do + prog' <- handleEditRequest [CreateDef Nothing] + case (findGlobalByName prog' "toUpper", Map.assocs $ moduleDefs $ progModule prog') of + (Just toUpperDef, [(i, _)]) -> do + _ <- + handleEditRequest + [ MoveToDef i + , SigAction [ConstructTCon "Char"] + , BodyAction [ConstructGlobalVar $ defID toUpperDef] + ] + pure $ pure () + (Nothing, _) -> pure $ assertFailure "Could not find the imported toUpper" + (Just _, _) -> pure $ assertFailure "Expected one def which was just created" + in case fst $ runAppTestM maxID a test of + Left err -> assertFailure $ show err + Right assertion -> assertion + -- * Utilities +findGlobalByName :: Prog -> Name -> Maybe Def +findGlobalByName p n = find ((== n) . defName) $ concatMap (Map.elems . moduleDefs) $ progModule p : progImports p + -- We use a program with two defs: "main" and "other" defaultEmptyProg :: MonadFresh ID m => m Prog defaultEmptyProg = do @@ -652,6 +700,16 @@ defaultPrimsProg = do . over (#progModule % #moduleDefs) ((DefPrim <$> m) <>) $ p +-- has `defaultPrimsProg` as an imported module, and a blank editable module +defaultImportProg :: MonadFresh ID m => m Prog +defaultImportProg = do + p <- defaultPrimsProg + pure + p + { progImports = [progModule p] + , progModule = Module{moduleTypes = mempty, moduleDefs = mempty} + } + _defIDs :: Traversal' ASTDef ID _defIDs = #astDefID `adjoin` #astDefExpr % (_exprMeta % _id `adjoin` _exprTypeMeta % _id) `adjoin` #astDefType % _typeMeta % _id diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs index 80324e30f..5248cf43c 100644 --- a/primer/test/Tests/Serialization.hs +++ b/primer/test/Tests/Serialization.hs @@ -109,7 +109,8 @@ fixtures = progaction = MoveToDef 0 prog = Prog - { progModule = + { progImports = mempty + , progModule = Module { moduleTypes = [typeDef] , moduleDefs = Map.singleton 1 (DefAST def) diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json index 6ba91e8d9..5d733bf3a 100644 --- a/primer/test/outputs/serialization/edit_response_2.json +++ b/primer/test/outputs/serialization/edit_response_2.json @@ -1,5 +1,6 @@ { "Right": { + "progImports": [], "progLog": { "unlog": [ [ diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json index a5fb275cf..69a2ea088 100644 --- a/primer/test/outputs/serialization/prog.json +++ b/primer/test/outputs/serialization/prog.json @@ -1,4 +1,5 @@ { + "progImports": [], "progLog": { "unlog": [ [ From 05f502d6441d5e34a3556a3759e508fae953e881 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 4 Mar 2022 20:09:18 +0000 Subject: [PATCH 5/7] fix: CopyPaste* action can copy from imported modules --- primer/src/Primer/App.hs | 15 +++++++++++---- primer/test/Tests/Action/Prog.hs | 25 +++++++++++++++++++++++++ 2 files changed, 36 insertions(+), 4 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 59debfd53..ded96742d 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -338,8 +338,15 @@ handleQuestion = \case -- This only looks in the editable module, not in any imports focusNode :: MonadError ProgError m => Prog -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) -focusNode prog defid nodeid = - case lookupASTDef defid (moduleDefs $ progModule prog) of +focusNode prog = focusNodeDefs $ moduleDefs $ progModule prog + +-- This looks in the editable module and also in any imports +focusNodeImports :: MonadError ProgError m => Prog -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) +focusNodeImports prog = focusNodeDefs $ allDefs prog + +focusNodeDefs :: MonadError ProgError m => Map ID Def -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip) +focusNodeDefs defs defid nodeid = + case lookupASTDef defid defs of Nothing -> throwError $ DefNotFound defid Just def -> let mzE = locToEither <$> focusOn nodeid (focus $ astDefExpr def) @@ -734,7 +741,7 @@ instance MonadFresh NameCounter EditAppM where copyPasteSig :: MonadEditApp m => Prog -> (ID, ID) -> ID -> [Action] -> m Prog copyPasteSig p (fromDefId, fromTyId) toDefId setup = do - c' <- focusNode p fromDefId fromTyId + c' <- focusNodeImports p fromDefId fromTyId c <- case c' of Left (Left _) -> throwError $ CopyPasteError "tried to copy-paste an expression into a signature" Left (Right zt) -> pure $ Left zt @@ -862,7 +869,7 @@ tcWholeProg p = copyPasteBody :: MonadEditApp m => Prog -> (ID, ID) -> ID -> [Action] -> m Prog copyPasteBody p (fromDefId, fromId) toDefId setup = do - src' <- focusNode p fromDefId fromId + src' <- focusNodeImports p fromDefId fromId -- reassociate so get Expr+(Type+Type), rather than (Expr+Type)+Type let src = case src' of Left (Left e) -> Left e diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index 607bd152b..afb45d608 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -660,6 +660,31 @@ unit_import_reference = Left err -> assertFailure $ show err Right assertion -> assertion +-- Can copy and paste from an imported module +unit_copy_paste_import :: Assertion +unit_copy_paste_import = + let (prog, maxID) = create defaultImportProg + a = newApp{appProg = prog} + test = do + prog' <- handleEditRequest [CreateDef Nothing] + case (findGlobalByName prog' "other", Map.assocs $ moduleDefs $ progModule prog') of + (Just (DefAST other), [(i, _)]) -> do + let fromDef = astDefID other + fromType = getID $ astDefType other + fromExpr = getID $ astDefExpr other + _ <- + handleEditRequest + [ MoveToDef i + , CopyPasteSig (fromDef, fromType) [] + , CopyPasteBody (fromDef, fromExpr) [] + ] + pure $ pure () + (Nothing, _) -> pure $ assertFailure "Could not find the imported 'other'" + (Just _, _) -> pure $ assertFailure "Expected one def which was just created" + in case fst $ runAppTestM maxID a test of + Left err -> assertFailure $ show err + Right assertion -> assertion + -- * Utilities findGlobalByName :: Prog -> Name -> Maybe Def From e4f09050a9a2b54cea6d9f220cdff1d437227a02 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 7 Mar 2022 16:16:34 +0000 Subject: [PATCH 6/7] feat: `importModules` utility; refactor TC modules This is basically an action, except we don't expose it in the API. We will delay doing so until we have a nice way for a frontend to refer to a module. I.e. we would like to say "import the User1.ProjectFoo.ModuleBar" module, rather than having to explicitly give the code contained within the module. This utility does not check that imported modules have disjointly-named contents. We intend to shortly require a hierarchical naming scheme which will address this concern. At that point we will also address the issue of disjoint IDs of contents, and our freshness guarantees. The reason we delay worrying about disjointness/uniqueness is that both it and being able to expose this nicely in the API require the notion of a module having some short name, rather than having to explicitly pass around all the code contained in the module. --- primer/src/Primer/Action.hs | 21 +++++---- primer/src/Primer/App.hs | 55 +++++++++++++++++------- primer/src/Primer/Typecheck.hs | 73 ++++++++++++++++++++++---------- primer/test/Tests/Action/Prog.hs | 59 ++++++++++++-------------- primer/test/Tests/Primitives.hs | 4 +- 5 files changed, 131 insertions(+), 81 deletions(-) diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs index dd5ffefe4..91da88c2e 100644 --- a/primer/src/Primer/Action.hs +++ b/primer/src/Primer/Action.hs @@ -91,6 +91,7 @@ import Primer.Name.Fresh ( import Primer.Questions (Question) import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine) import Primer.Typecheck ( + CheckEverythingRequest (CheckEverything, toCheck, trusted), SmartHoles, TypeError, buildTypingContext, @@ -353,6 +354,12 @@ data ActionError -- a bug. It does not get thrown for "no valid refinement found" -- - see Note [No valid refinement] RefineError Text + | -- | Importing some modules failed. + -- This should be impossible as long as the requested modules are well-typed + -- and all of their dependencies are already imported + ImportFailed () TypeError + -- The extra unit is to avoid having two constructors with a single + -- TypeError field, breaking our MonadNestedError machinery... deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ActionError @@ -435,14 +442,12 @@ applyActionsToTypeSig smartHoles imports mod def actions = -- typechecked against the new type. -- Now we need to typecheck the whole program again, to check any uses of the definition -- We make sure that the updated type is present in the global context. - -- Here we just check the whole prog, including imports. - -- TODO: for efficiency, we should not check the immutable imports - checkedDefs <- - checkEverything - smartHoles - (concatMap moduleTypes $ mod' : imports) - (foldMap moduleDefs $ mod' : imports) - pure (def', mod'{moduleDefs = checkedDefs}, zt) + -- 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" -- 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 ded96742d..ffc2123eb 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -31,6 +31,7 @@ module Primer.App ( handleEditRequest, handleEvalRequest, handleEvalFullRequest, + importModules, MutationRequest (..), Selection (..), NodeSelection (..), @@ -62,10 +63,10 @@ import Data.Generics.Uniplate.Zipper ( ) import qualified Data.Map.Strict as Map import qualified Data.Set as Set -import Optics (re, traverseOf, view, (%), (.~), (^.), _Left, _Right) +import Optics (re, traverseOf, view, (%), (%~), (.~), (^.), _Left, _Right) import Primer.Action ( Action, - ActionError (IDNotFound), + ActionError (IDNotFound, ImportFailed), ProgAction (..), applyActionsToBody, applyActionsToTypeSig, @@ -118,6 +119,7 @@ import Primer.Questions ( variablesInScopeTy, ) import Primer.Typecheck ( + CheckEverythingRequest (CheckEverything, toCheck, trusted), Cxt, SmartHoles (NoSmartHoles, SmartHoles), TypeError, @@ -186,6 +188,24 @@ data Prog = Prog -- all the imports are in one mutual dependency group -- the @progModule@ has all the imports in scope +-- | Imports some explicitly-given modules, ensuring that they are well-typed +-- (and all their dependencies are already imported) +importModules :: MonadEditApp m => [Module] -> m () +importModules ms = do + -- NB: we do not enforce the invariant that IDs and Names are globally unique + -- (see Note [Modules]), because we plan to only use this function internally + -- until we add unique names to modules. + -- This means that any call to this function should ensure that the IDs/Names + -- in the imported module are distinct from those already existing in the + -- App. + p <- gets appProg + checkedImports' <- runExceptT $ checkEverything NoSmartHoles $ CheckEverything{trusted = progImports p, toCheck = ms} + checkedImports <- case checkedImports' of + Left err -> throwError $ ActionError $ ImportFailed () err + Right ci -> pure ci + let p' = p & #progImports %~ (<> checkedImports) + modify (\a -> a{appProg = p'}) + -- | Get all type definitions from all modules (including imports) allTypes :: Prog -> [TypeDef] allTypes = moduleTypes . progModule @@ -412,12 +432,12 @@ applyProgAction prog mdefID = \case | mod <- progModule prog , Map.member id_ (moduleDefs mod) -> do let modDefs' = Map.delete id_ $ moduleDefs mod - prog' = prog{progModule = mod{moduleDefs = modDefs'}, progSelection = Nothing} + mod' = mod{moduleDefs = modDefs'} + 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. - -- TODO: when we add imports, we do not need to re-check those, as they will not have changed - runExceptT (checkEverything @TypeError NoSmartHoles (allTypes prog) (allDefs prog')) >>= \case + runExceptT (checkEverything @TypeError NoSmartHoles CheckEverything{trusted = progImports prog, toCheck = [mod']}) >>= \case Left _ -> throwError $ DefInUse id_ Right _ -> pure () pure (prog', Nothing) @@ -451,16 +471,21 @@ applyProgAction prog mdefID = \case let def = ASTDef id_ name expr ty pure (addDef def prog{progSelection = Just $ Selection def Nothing}, Just id_) AddTypeDef td -> do - runExceptT @TypeError (checkTypeDefs $ allTypes prog <> [TypeDefAST td]) >>= \case - -- The frontend should never let this error case happen, - -- so we just dump out a raw string for debugging/logging purposes - -- (This is not currently true! We should synchronise the frontend with - -- the typechecker rules. For instance, the form allows to create - -- data T (T : *) = T - -- but the TC rejects it. - -- see https://github.com/hackworthltd/primer/issues/3) - Left err -> throwError $ TypeDefError $ show err - Right _ -> pure (addTypeDef td prog, mdefID) + runExceptT @TypeError + ( runReaderT + (checkTypeDefs [TypeDefAST td]) + (buildTypingContext (allTypes prog) mempty NoSmartHoles) + ) + >>= \case + -- The frontend should never let this error case happen, + -- so we just dump out a raw string for debugging/logging purposes + -- (This is not currently true! We should synchronise the frontend with + -- the typechecker rules. For instance, the form allows to create + -- data T (T : *) = T + -- but the TC rejects it. + -- see https://github.com/hackworthltd/primer/issues/3) + Left err -> throwError $ TypeDefError $ show err + Right _ -> pure (addTypeDef td prog, mdefID) BodyAction actions -> do withDef mdefID prog $ \def -> do smartHoles <- gets $ progSmartHoles . appProg diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index db4a3d394..02ef32f34 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -1,4 +1,6 @@ {-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE TypeApplications #-} -- | Typechecking for Core expressions. @@ -17,6 +19,7 @@ module Primer.Typecheck ( checkKind, checkTypeDefs, checkValidContext, + CheckEverythingRequest (..), checkEverything, Cxt (..), KindOrType (..), @@ -64,7 +67,8 @@ import qualified Data.Map as M import qualified Data.Map.Strict as Map import qualified Data.Set as S import Data.String (String) -import Optics (Lens', over, set, view, (%)) +import Optics (Lens', over, set, traverseOf, view, (%)) +import Optics.Traversal (traversed) import Primer.Core ( ASTDef (..), ASTTypeDef (..), @@ -85,7 +89,6 @@ import Primer.Core ( TypeMeta, ValCon (valConArgs, valConName), bindName, - defAST, defID, defName, defType, @@ -102,6 +105,7 @@ import Primer.Core ( import Primer.Core.DSL (branch, emptyHole, meta, meta') import Primer.Core.Utils (alphaEqTy, forgetTypeIDs, generateTypeIDs) import Primer.JSON (CustomJSON (CustomJSON), FromJSON, ToJSON, VJSON) +import Primer.Module (Module (moduleDefs, moduleTypes)) import Primer.Name (Name, NameCounter, freshName) import Primer.Subst (substTy) @@ -201,6 +205,9 @@ localTmVars = M.mapMaybe (\case T t -> Just t; K _ -> Nothing) . localCxt localTyVars :: Cxt -> Map Name Kind localTyVars = M.mapMaybe (\case K k -> Just k; T _ -> Nothing) . localCxt +noSmartHoles :: Cxt -> Cxt +noSmartHoles cxt = cxt{smartHoles = NoSmartHoles} + -- An empty typing context initialCxt :: SmartHoles -> Cxt initialCxt sh = @@ -255,12 +262,12 @@ annotate t (Meta i _ v) = Meta i t v -- | Check a context is valid checkValidContext :: - (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m), MonadNestedError TypeError e m) => + (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m)) => Cxt -> m () checkValidContext cxt = do let tds = typeDefs cxt - checkTypeDefsMap tds + runReaderT (checkTypeDefsMap tds) $ initialCxt NoSmartHoles runReaderT (checkGlobalCxt $ globalCxt cxt) $ (initialCxt NoSmartHoles){typeDefs = tds} checkLocalCxtTys $ localTyVars cxt runReaderT (checkLocalCxtTms $ localTmVars cxt) $ extendLocalCxtTys (M.toList $ localTyVars cxt) (initialCxt NoSmartHoles){typeDefs = tds} @@ -278,7 +285,7 @@ checkValidContext cxt = do -- This is the same as 'checkTypeDefs', except it also checks the keys of the -- map are consistent with the names in the 'TypeDef's checkTypeDefsMap :: - (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) => + TypeM e m => Map Name TypeDef -> m () checkTypeDefsMap tds = @@ -286,27 +293,29 @@ checkTypeDefsMap tds = then checkTypeDefs $ M.elems tds else throwError' $ InternalError "Inconsistent names in a Map Name TypeDef" --- | Check all type definitions, as one recursive group +-- | Check all type definitions, as one recursive group, in some monadic environment checkTypeDefs :: - (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) => + TypeM e m => [TypeDef] -> m () checkTypeDefs tds = do + existingTypes <- asks $ Map.elems . typeDefs -- NB: we expect the frontend to only submit acceptable typedefs, so all -- errors here are "internal errors" and should never be seen. -- (This is not quite true, see -- https://github.com/hackworthltd/primer/issues/3) - assert (distinct $ map typeDefName tds) "Duplicate-ly-named TypeDefs" + assert (distinct $ map typeDefName $ existingTypes <> tds) "Duplicate-ly-named TypeDefs" -- Note that constructors are synthesisable, so their names must be globally -- unique. We need to be able to work out the type of @TCon "C"@ without any -- extra information. let atds = mapMaybe typeDefAST tds + let allAtds = mapMaybe typeDefAST existingTypes <> atds assert - (distinct $ concatMap (map valConName . astTypeDefConstructors) atds) + (distinct $ concatMap (map valConName . astTypeDefConstructors) allAtds) "Duplicate-ly-named constructor (perhaps in different typedefs)" -- Note that these checks only apply to non-primitives: -- duplicate type names are checked elsewhere, kinds are correct by construction, and there are no constructors. - mapM_ checkTypeDef atds + local (extendTypeDefCxt tds) $ mapM_ checkTypeDef atds where -- In the core, we have many different namespaces, so the only name-clash -- checking we must do is @@ -334,10 +343,8 @@ checkTypeDefs tds = do assert (notElem (astTypeDefName td) $ map fst params) "Duplicate names in one tydef: between type-def-name and parameter-names" - runReaderT (mapM_ (checkKind KType <=< fakeMeta) $ concatMap valConArgs cons) $ - extendTypeDefCxt tds $ - extendLocalCxtTys params $ - initialCxt NoSmartHoles + local (noSmartHoles . extendLocalCxtTys params) $ + mapM_ (checkKind KType <=< fakeMeta) $ concatMap valConArgs cons -- We need metadata to use checkKind, but we don't care about the output, -- just a yes/no answer. In this case it is fine to put nonsense in the -- metadata as it won't be inspected. @@ -351,18 +358,38 @@ distinct = go mempty | x `S.member` seen = False | otherwise = go (S.insert x seen) xs --- | Check all type definitions and top-level definitions, in the empty context +data CheckEverythingRequest = CheckEverything + { trusted :: [Module] + , toCheck :: [Module] + } + +-- | Check a (mutually-recursive set of) module(s), in a given trusted +-- environment of modules. +-- Returns just the modules that were requested 'toCheck', with updated cached +-- type information etc. checkEverything :: forall e m. - (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) => + (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m)) => SmartHoles -> - [TypeDef] -> - Map ID Def -> - m (Map ID Def) -checkEverything sh tydefs defs = do - checkTypeDefs tydefs - let cxt = buildTypingContext tydefs defs sh - flip runReaderT cxt $ mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) defs + CheckEverythingRequest -> + m [Module] +checkEverything sh CheckEverything{trusted, toCheck} = + let cxt = + buildTypingContext + (concatMap moduleTypes trusted) + (foldMap moduleDefs trusted) + sh + in flip runReaderT cxt $ do + -- Check that the definition map has the right keys + for_ toCheck $ \m -> flip Map.traverseWithKey (moduleDefs m) $ \i d -> + unless (i == defID d) $ throwError' $ InternalError "Inconsistant IDs in moduleDefs map" + checkTypeDefs $ concatMap moduleTypes toCheck + let newTypes = foldMap moduleTypes toCheck + newDefs = + foldMap (\d -> [(defID d, (defName d, forgetTypeIDs $ defType d))]) $ + foldMap moduleDefs toCheck + local (extendGlobalCxt newDefs . extendTypeDefCxt newTypes) $ + traverseOf (traversed % #moduleDefs % traversed % #_DefAST) checkDef toCheck -- | Typecheck a definition. -- This checks that the type signature is well-formed, then checks the body diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs index afb45d608..c488bc629 100644 --- a/primer/test/Tests/Action/Prog.hs +++ b/primer/test/Tests/Action/Prog.hs @@ -34,6 +34,7 @@ import Primer.App ( Selection (..), handleEditRequest, handleQuestion, + importModules, lookupASTDef, newApp, newEmptyApp, @@ -46,7 +47,7 @@ import Primer.Core ( ASTTypeDef (..), Def (..), Expr' (..), - ID, + ID (ID), Kind (KType), Meta (..), Type' (..), @@ -80,7 +81,7 @@ import Primer.Core.DSL ( tvar, var, ) -import Primer.Module (Module (Module, moduleDefs, moduleTypes)) +import Primer.Module (Module (moduleDefs, moduleTypes)) import Primer.Name import Primer.Primitives (allPrimTypeDefs) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=)) @@ -622,30 +623,30 @@ unit_copy_paste_sig2ann = do -- VariablesInScope sees imported terms unit_import_vars :: Assertion unit_import_vars = - let (prog, maxID) = create defaultImportProg - a = newEmptyApp{appProg = prog} - test = do - prog' <- handleEditRequest [CreateDef Nothing] - case Map.assocs $ moduleDefs $ progModule prog' of + let test = do + p <- defaultPrimsProg + importModules [progModule p] + gets (Map.assocs . moduleDefs . progModule . appProg) >>= \case [(i, DefAST d)] -> do a' <- get (_, vs) <- runReaderT (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) a' pure $ assertBool "VariablesInScope did not report the imported Int.+" $ any ((== "Int.+") . snd3) vs - _ -> pure $ assertFailure "Expected one def which was just created" - in case fst $ runAppTestM maxID a test of + _ -> pure $ assertFailure "Expected one def 'main' from newEmptyApp" + a = newEmptyApp + in case fst $ runAppTestM (ID $ appIdCounter a) a test of Left err -> assertFailure $ show err Right assertion -> assertion -- Can reference something in an imported module (both types and terms) unit_import_reference :: Assertion unit_import_reference = - let (prog, maxID) = create defaultImportProg - a = newEmptyApp{appProg = prog} - test = do - prog' <- handleEditRequest [CreateDef Nothing] - case (findGlobalByName prog' "toUpper", Map.assocs $ moduleDefs $ progModule prog') of + let test = do + p <- defaultPrimsProg + importModules [progModule p] + prog <- gets appProg + case (findGlobalByName prog "toUpper", Map.assocs $ moduleDefs $ progModule prog) of (Just toUpperDef, [(i, _)]) -> do _ <- handleEditRequest @@ -655,19 +656,20 @@ unit_import_reference = ] pure $ pure () (Nothing, _) -> pure $ assertFailure "Could not find the imported toUpper" - (Just _, _) -> pure $ assertFailure "Expected one def which was just created" - in case fst $ runAppTestM maxID a test of + (Just _, _) -> pure $ assertFailure "Expected one def 'main' from newEmptyApp" + a = newEmptyApp + in case fst $ runAppTestM (ID $ appIdCounter a) a test of Left err -> assertFailure $ show err Right assertion -> assertion -- Can copy and paste from an imported module unit_copy_paste_import :: Assertion unit_copy_paste_import = - let (prog, maxID) = create defaultImportProg - a = newApp{appProg = prog} - test = do - prog' <- handleEditRequest [CreateDef Nothing] - case (findGlobalByName prog' "other", Map.assocs $ moduleDefs $ progModule prog') of + let test = do + p <- defaultPrimsProg + importModules [progModule p] + prog <- gets appProg + case (findGlobalByName prog "other", Map.assocs $ moduleDefs $ progModule prog) of (Just (DefAST other), [(i, _)]) -> do let fromDef = astDefID other fromType = getID $ astDefType other @@ -680,8 +682,9 @@ unit_copy_paste_import = ] pure $ pure () (Nothing, _) -> pure $ assertFailure "Could not find the imported 'other'" - (Just _, _) -> pure $ assertFailure "Expected one def which was just created" - in case fst $ runAppTestM maxID a test of + (Just _, _) -> pure $ assertFailure "Expected one def 'main' from newEmptyApp" + a = newEmptyApp + in case fst $ runAppTestM (ID $ appIdCounter a) a test of Left err -> assertFailure $ show err Right assertion -> assertion @@ -725,16 +728,6 @@ defaultPrimsProg = do . over (#progModule % #moduleDefs) ((DefPrim <$> m) <>) $ p --- has `defaultPrimsProg` as an imported module, and a blank editable module -defaultImportProg :: MonadFresh ID m => m Prog -defaultImportProg = do - p <- defaultPrimsProg - pure - p - { progImports = [progModule p] - , progModule = Module{moduleTypes = mempty, moduleDefs = mempty} - } - _defIDs :: Traversal' ASTDef ID _defIDs = #astDefID `adjoin` #astDefExpr % (_exprMeta % _id `adjoin` _exprTypeMeta % _id) `adjoin` #astDefType % _typeMeta % _id diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs index 8700d9404..a706adc27 100644 --- a/primer/test/Tests/Primitives.hs +++ b/primer/test/Tests/Primitives.hs @@ -28,7 +28,7 @@ import Primer.Typecheck ( TypeError (PrimitiveTypeNotInScope, UnknownTypeConstructor), buildTypingContext, checkKind, - checkTypeDefs, + checkValidContext, synth, ) @@ -56,7 +56,7 @@ unit_prim_con_scope = do unit_prim_con_scope_ast :: Assertion unit_prim_con_scope_ast = do -- Our type def is accepted - test (checkTypeDefs [charASTDef]) @?= Right () + test (checkValidContext =<< ask) @?= Right () -- Char is in scope (though the wrong kind to accept 'PrimChar's!) assertBool "Char is not in scope?" $ isRight $ From e67f0b976aa9f71ff94191fbe00023ea1c511590 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 8 Mar 2022 11:24:42 +0000 Subject: [PATCH 7/7] test: add tests for Eval{,Full} with modules --- primer/test/Tests/Eval.hs | 34 +++++++++++++++++++++++++++++- primer/test/Tests/EvalFull.hs | 39 ++++++++++++++++++++++++++++++++++- 2 files changed, 71 insertions(+), 2 deletions(-) diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs index 5f6560978..0fe70841f 100644 --- a/primer/test/Tests/Eval.hs +++ b/primer/test/Tests/Eval.hs @@ -8,14 +8,25 @@ import Data.Map ((!)) import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Optics (over, (^.)) +import Primer.App ( + App (appIdCounter, appProg), + EvalReq (EvalReq, evalReqExpr, evalReqRedex), + EvalResp (EvalResp, evalRespExpr), + Prog (progModule), + handleEvalRequest, + importModules, + newEmptyApp, + ) import Primer.Core ( ASTDef (..), Def (..), Expr, Expr', - ID, + ID (ID), Type, Type', + defID, + getID, _exprMeta, _exprTypeMeta, _id, @@ -41,9 +52,11 @@ import Primer.Eval ( ) import Primer.Name (Name) import Primer.Zipper (target) +import Protolude.Partial (fromJust) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=)) import TestM (evalTestM) import TestUtils (withPrimDefs) +import Tests.Action.Prog (defaultPrimsProg, findGlobalByName, runAppTestM) -- * 'tryReduce' tests @@ -801,6 +814,25 @@ unit_redexes_prim_ann = `ann` (tcon "Char" `tfun` tcon "Char") `app` (char 'a' `ann` tcon "Char") +-- Test that handleEvalRequest will reduce imported terms +unit_eval_modules :: Assertion +unit_eval_modules = + let test = do + p <- defaultPrimsProg + importModules [progModule p] + prog <- gets appProg + let toUpperId = defID $ fromJust $ findGlobalByName prog "toUpper" + foo <- global toUpperId `app` char 'a' + EvalResp{evalRespExpr = e} <- + handleEvalRequest + EvalReq{evalReqExpr = foo, evalReqRedex = getID foo} + expect <- char 'A' + pure $ e ~= expect + a = newEmptyApp + in case fst $ runAppTestM (ID $ appIdCounter a) a test of + Left err -> assertFailure $ show err + Right assertion -> assertion + -- * Misc helpers -- | Like '@?=' but specifically for expressions. diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs index 1758999c6..86250b300 100644 --- a/primer/test/Tests/EvalFull.hs +++ b/primer/test/Tests/EvalFull.hs @@ -14,7 +14,16 @@ import Hedgehog hiding (Var, test) import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range import Optics -import Primer.App (defaultTypeDefs) +import Primer.App ( + App (appIdCounter, appProg), + EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullReqExpr), + EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut), + Prog (progModule), + defaultTypeDefs, + handleEvalFullRequest, + importModules, + newEmptyApp, + ) import Primer.Core import Primer.Core.DSL import Primer.Core.Utils (forgetIDs, generateIDs, generateTypeIDs) @@ -27,9 +36,12 @@ import Primer.Typecheck ( mkTypeDefMap, typeDefs, ) +import Protolude.Partial (fromJust) import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=)) import TestM import TestUtils (withPrimDefs) +import Tests.Action.Prog (defaultPrimsProg, findGlobalByName, runAppTestM) +import Tests.Eval ((~=)) import Tests.Gen.Core.Typed (checkTest) unit_1 :: Assertion @@ -894,6 +906,31 @@ unit_prim_partial_map = map_ <- lAM "a" $ lAM "b" $ lam "f" $ letrec "go" worker ((tcon "List" `tapp` tvar "a") `tfun` (tcon "List" `tapp` tvar "b")) $ var "go" pure $ DefAST $ ASTDef mapID "map" map_ mapTy +-- Test that handleEvalFullRequest will reduce imported terms +unit_eval_full_modules :: Assertion +unit_eval_full_modules = + let test = do + p <- defaultPrimsProg + importModules [progModule p] + prog <- gets appProg + let toUpperId = defID $ fromJust $ findGlobalByName prog "toUpper" + foo <- global toUpperId `app` char 'a' + resp <- + handleEvalFullRequest + EvalFullReq + { evalFullReqExpr = foo + , evalFullCxtDir = Chk + , evalFullMaxSteps = 2 + } + expect <- char 'A' + pure $ case resp of + EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out" + EvalFullRespNormal e -> e ~= expect + a = newEmptyApp + in case fst $ runAppTestM (ID $ appIdCounter a) a test of + Left err -> assertFailure $ show err + Right assertion -> assertion + -- * Utilities evalFullTest :: ID -> M.Map Name TypeDef -> M.Map ID Def -> TerminationBound -> Dir -> Expr -> Either EvalFullError Expr