From 580e1f6f7fc4ee4ce04d81cf838091158c9a66aa Mon Sep 17 00:00:00 2001 From: Ben Price Date: Fri, 18 Feb 2022 19:13:48 +0000 Subject: [PATCH 01/12] fix: Prim type must be in scope to use a prim con Since primitive constructors are hard-wired into the Expr type, they are always in scope. However, the corresponding primitive type definitions may not be in scope. Since we have a hard-wired map `primConName` that gives the type any PrimCon constructs we could infer a non-existant type for primitive constructors! Previously, we would infer a type of `Char` for `'a'`, even when the type `Char` did not exist in the current program, or even if it had been arbitrarily defined by the user. We now check that the type-name given by the hard-wired map exists in the current program, and is a primitive type. Note that this design relies on the fact that primitive types cannot be renamed. --- primer/src/Primer/Typecheck.hs | 26 ++++++++++++-- primer/test/Tests/Primitives.hs | 61 +++++++++++++++++++++++++++++++-- primer/test/Tests/Typecheck.hs | 15 ++++---- 3 files changed, 90 insertions(+), 12 deletions(-) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 852a6d048..bdddce1ee 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -128,6 +128,9 @@ data TypeError | UnknownGlobalVariable ID | UnknownConstructor Name | UnknownTypeConstructor Name + | -- | Cannot use a PrimCon when either no type of the appropriate name is + -- in scope, or it is a user-defined type + PrimitiveTypeNotInScope Name | CannotSynthesiseType Expr | InconsistentTypes Type Type | TypeDoesNotMatchArrow Type @@ -484,8 +487,27 @@ synth = \case -- Extend the context with the binding, and synthesise the body (bT, b') <- local ctx' $ synth b pure $ annSynth4 bT i Letrec x a' tA' b' - PrimCon i pc -> - pure $ annSynth0 (TCon () $ primConName pc) i (\m -> PrimCon m pc) + PrimCon i pc -> do + -- There is a hard-wired map 'primConName' which associates each PrimCon to + -- its PrimTypeDef (by name -- PrimTypeDefs have hardwired names). + -- However, these PrimTypeDefs may or may not be in the Cxt. + -- If they are not (and in that case, also if a user has defined some + -- other type with the same name), we should reject the use of the + -- primitive constructor. + -- Essentially, PrimCons are always-in-scope terms whose type is one of + -- the primitive types. Normally we ensure that the types of all global + -- definitions are well-kinded (in particular, only refer to types that + -- are in scope). This is just the analogue that check, but we have to + -- do it lazily (i.e. on use) for primitive constructors. + let tyCon = primConName pc + typeDef <- asks $ M.lookup tyCon . typeDefs + -- We expect any frontend to avoid this situation, and thus we do not + -- try to recover with SmartHoles + case typeDef of + Nothing -> throwError' $ PrimitiveTypeNotInScope tyCon + Just (TypeDefAST _) -> throwError' $ PrimitiveTypeNotInScope tyCon + Just (TypeDefPrim _) -> pure () + pure $ annSynth0 (TCon () tyCon) i (\m -> PrimCon m pc) e -> asks smartHoles >>= \case NoSmartHoles -> throwError' $ CannotSynthesiseType e diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs index 7b6fbc840..21cf9c728 100644 --- a/primer/test/Tests/Primitives.hs +++ b/primer/test/Tests/Primitives.hs @@ -9,11 +9,68 @@ import Gen.Core.Typed (forAllT, genPrimCon, propertyWT) import Hedgehog (Property, assert) import Hedgehog.Gen (element) import Primer.App (defaultTypeDefs) -import Primer.Core (primConName) +import Primer.Core ( + ASTTypeDef ( + ASTTypeDef, + astTypeDefConstructors, + astTypeDefName, + astTypeDefNameHints, + astTypeDefParameters + ), + Kind (KFun, KType), + TypeDef (TypeDefAST), + primConName, + ) +import Primer.Core.DSL (char, tcon) import Primer.Primitives (allPrimTypeDefs) -import Primer.Typecheck (SmartHoles (NoSmartHoles), buildTypingContext) +import Primer.Typecheck ( + SmartHoles (NoSmartHoles), + TypeError (PrimitiveTypeNotInScope, UnknownTypeConstructor), + buildTypingContext, + checkKind, + checkTypeDefs, + synth, + ) + +import Test.Tasty.HUnit (Assertion, assertBool, (@?=)) +import Tests.Typecheck (runTypecheckTestMFromIn) hprop_all_prim_cons_have_typedef :: Property hprop_all_prim_cons_have_typedef = propertyWT (buildTypingContext defaultTypeDefs mempty NoSmartHoles) $ do c <- forAllT $ element =<< genPrimCon assert $ primConName c `elem` M.keys allPrimTypeDefs + +-- If we use a prim con, then we need the corresponding prim type +-- in scope +unit_prim_con_scope :: Assertion +unit_prim_con_scope = do + -- Char is indeed not in scope + test (checkKind KType =<< tcon "Char") @?= Left (UnknownTypeConstructor "Char") + test (synth =<< char 'a') @?= Left (PrimitiveTypeNotInScope "Char") + where + cxt = buildTypingContext mempty mempty NoSmartHoles + test = runTypecheckTestMFromIn 0 cxt + +-- If we use a prim con, then we need the corresponding prim type +-- in scope, and not some other type of that name +unit_prim_con_scope_ast :: Assertion +unit_prim_con_scope_ast = do + -- Our type def is accepted + test (checkTypeDefs [charASTDef]) @?= Right () + -- Char is in scope (though the wrong kind to accept 'PrimChar's!) + assertBool "Char is not in scope?" $ + isRight $ + test $ checkKind (KType `KFun` KType) =<< tcon "Char" + test (synth =<< char 'a') @?= Left (PrimitiveTypeNotInScope "Char") + where + charASTDef = + TypeDefAST $ + ASTTypeDef + { astTypeDefName = "Char" + , astTypeDefParameters = [("a", KType)] + , astTypeDefConstructors = mempty + , astTypeDefNameHints = mempty + } + + cxt = buildTypingContext [charASTDef] mempty NoSmartHoles + test = runTypecheckTestMFromIn 0 cxt diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index ebf8dd861..6a539e237 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -527,18 +527,17 @@ newtype TypecheckTestM a = TypecheckTestM {unTypecheckTestM :: ExceptT TypeError , MonadError TypeError ) -runTypecheckTestM :: SmartHoles -> TypecheckTestM a -> Either TypeError a -runTypecheckTestM sh = - evalTestM 0 - . flip runReaderT (buildTypingContext testingTypeDefs mempty sh) +runTypecheckTestMFromIn :: ID -> Cxt -> TypecheckTestM a -> Either TypeError a +runTypecheckTestMFromIn nextFresh cxt = + evalTestM nextFresh + . flip runReaderT cxt . runExceptT . unTypecheckTestM +runTypecheckTestM :: SmartHoles -> TypecheckTestM a -> Either TypeError a +runTypecheckTestM sh = runTypecheckTestMFromIn 0 (buildTypingContext testingTypeDefs mempty sh) runTypecheckTestMWithPrims :: SmartHoles -> (Map Name ID -> TypecheckTestM a) -> Either TypeError a runTypecheckTestMWithPrims sh = - evalTestM n - . flip runReaderT (buildTypingContext testingTypeDefs defs sh) - . runExceptT - . unTypecheckTestM + runTypecheckTestMFromIn n (buildTypingContext testingTypeDefs defs sh) . ($ globals) where ((defs, globals), n) = create $ withPrimDefs $ \m1 m2 -> pure $ (,m1) $ DefPrim <$> m2 From 6843e2b764dbf7ae58464e0442f07957ccd1a93c Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 21 Feb 2022 17:27:20 +0000 Subject: [PATCH 02/12] fix: genPrimCon cares about which primitive types are in scope Otherwise it will generate ill-typed terms in the empty context: it will generate primitve constructors but they are not considered to be in scope as their corresponding types are not. --- primer/src/Primer/Typecheck.hs | 44 ++++++++++++++--------- primer/test/Gen/Core/Typed.hs | 64 +++++++++++++++++++-------------- primer/test/Tests/Primitives.hs | 4 +-- 3 files changed, 66 insertions(+), 46 deletions(-) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index bdddce1ee..5fcff971f 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -42,6 +42,7 @@ module Primer.Typecheck ( getGlobalNames, lookupGlobal, lookupLocal, + primConInScope, mkTypeDefMap, consistentKinds, consistentTypes, @@ -76,6 +77,7 @@ import Primer.Core ( ID, Kind (..), Meta (..), + PrimCon, Type' (..), TypeCache (..), TypeCacheBoth (..), @@ -488,25 +490,10 @@ synth = \case (bT, b') <- local ctx' $ synth b pure $ annSynth4 bT i Letrec x a' tA' b' PrimCon i pc -> do - -- There is a hard-wired map 'primConName' which associates each PrimCon to - -- its PrimTypeDef (by name -- PrimTypeDefs have hardwired names). - -- However, these PrimTypeDefs may or may not be in the Cxt. - -- If they are not (and in that case, also if a user has defined some - -- other type with the same name), we should reject the use of the - -- primitive constructor. - -- Essentially, PrimCons are always-in-scope terms whose type is one of - -- the primitive types. Normally we ensure that the types of all global - -- definitions are well-kinded (in particular, only refer to types that - -- are in scope). This is just the analogue that check, but we have to - -- do it lazily (i.e. on use) for primitive constructors. - let tyCon = primConName pc - typeDef <- asks $ M.lookup tyCon . typeDefs + (inScope, tyCon) <- asks (primConInScope pc) -- We expect any frontend to avoid this situation, and thus we do not -- try to recover with SmartHoles - case typeDef of - Nothing -> throwError' $ PrimitiveTypeNotInScope tyCon - Just (TypeDefAST _) -> throwError' $ PrimitiveTypeNotInScope tyCon - Just (TypeDefPrim _) -> pure () + unless inScope $ throwError' $ PrimitiveTypeNotInScope tyCon pure $ annSynth0 (TCon () tyCon) i (\m -> PrimCon m pc) e -> asks smartHoles >>= \case @@ -525,6 +512,29 @@ synth = \case annSynth3 t i c = annSynth2 t i . flip c annSynth4 t i c = annSynth3 t i . flip c +-- There is a hard-wired map 'primConName' which associates each PrimCon to +-- its PrimTypeDef (by name -- PrimTypeDefs have hardwired names). +-- However, these PrimTypeDefs may or may not be in the Cxt. +-- If they are not (and in that case, also if a user has defined some +-- other type with the same name), we should reject the use of the +-- primitive constructor. +-- Essentially, PrimCons are always-in-scope terms whose type is one of +-- the primitive types. Normally we ensure that the types of all global +-- definitions are well-kinded (in particular, only refer to types that +-- are in scope). This is just the analogue that check, but we have to +-- do it lazily (i.e. on use) for primitive constructors. +-- +-- returns: whether it is in scope or not, and also the type of which it +-- (should) construct a value +primConInScope :: PrimCon -> Cxt -> (Bool, Name) +primConInScope pc cxt = + let tyCon = primConName pc + typeDef = M.lookup tyCon $ typeDefs cxt + in case typeDef of + Nothing -> (False, tyCon) + Just (TypeDefAST _) -> (False, tyCon) + Just (TypeDefPrim _) -> (True, tyCon) + -- | Similar to synth, but for checking rather than synthesis. check :: TypeM e m => Type -> Expr -> m ExprT check t = \case diff --git a/primer/test/Gen/Core/Typed.hs b/primer/test/Gen/Core/Typed.hs index e6afb976a..772d1c20a 100644 --- a/primer/test/Gen/Core/Typed.hs +++ b/primer/test/Gen/Core/Typed.hs @@ -52,7 +52,6 @@ import Primer.Core ( Type' (..), TypeDef (..), ValCon (..), - primConName, typeDefKind, typeDefName, typeDefParameters, @@ -79,6 +78,7 @@ import Primer.Typecheck ( matchArrowType, matchForallType, mkTypeDefMap, + primConInScope, typeDefs, ) import TestM (TestM, evalTestM, isolateTestM) @@ -137,7 +137,7 @@ freshNameForCxt = do genSyns :: TypeG -> GenT WT (ExprG, TypeG) genSyns ty = do genSpine' <- lift genSpine - Gen.recursive Gen.choice [genEmptyHole, genAnn] [genHole, genApp, genAPP, genLet, genSpine'] + Gen.recursive Gen.choice [genEmptyHole, genAnn] $ [genHole, genApp, genAPP, genLet] ++ catMaybes [genSpine'] where genEmptyHole = pure (EmptyHole (), TEmptyHole ()) genAnn = do @@ -146,9 +146,9 @@ genSyns ty = do genHole = do (e, _) <- genSyn pure (Hole () e, TEmptyHole ()) - genSpine :: WT (GenT WT (ExprG, TypeG)) - genSpine = fmap Gen.justT genSpineHeadFirst - genSpineHeadFirst :: WT (GenT WT (Maybe (ExprG, TypeG))) + genSpine :: WT (Maybe (GenT WT (ExprG, TypeG))) + genSpine = fmap (fmap Gen.justT) genSpineHeadFirst + genSpineHeadFirst :: WT (Maybe (GenT WT (Maybe (ExprG, TypeG)))) -- todo: maybe add some lets in as post-processing? I could even add them to the locals for generation in the head genSpineHeadFirst = do localTms <- asks localTmVars @@ -157,19 +157,23 @@ genSyns ty = do let globals' = map (first (GlobalVar ())) $ M.toList globals cons <- asks allCons let cons' = map (first (Con ())) $ M.toList cons - let hs = locals' ++ globals' ++ cons' - pure $ do - primCons <- (\con -> (PrimCon () con, TCon () $ primConName con)) <<$>> genPrimCon - (he, hT) <- Gen.element $ hs ++ primCons - cxt <- ask - runExceptT (refine cxt ty hT) >>= \case - -- This error case indicates a bug. Crash and fail loudly! - Left err -> panic $ "Internal refine/unify error: " <> show err - Right Nothing -> pure Nothing - Right (Just (inst, instTy)) -> do - (sb, is) <- genInstApp inst - let f e = \case Right tm -> App () e tm; Left ty' -> APP () e ty' - Just . (foldl f he is,) <$> substTys sb instTy + let hsPure = locals' ++ globals' ++ cons' + primCons <- fmap (bimap (PrimCon ()) (TCon ())) <<$>> genPrimCon + let hs = map pure hsPure ++ primCons + if null hs + then pure Nothing + else pure $ + Just $ do + (he, hT) <- Gen.choice hs + cxt <- ask + runExceptT (refine cxt ty hT) >>= \case + -- This error case indicates a bug. Crash and fail loudly! + Left err -> panic $ "Internal refine/unify error: " <> show err + Right Nothing -> pure Nothing + Right (Just (inst, instTy)) -> do + (sb, is) <- genInstApp inst + let f e = \case Right tm -> App () e tm; Left ty' -> APP () e ty' + Just . (foldl f he is,) <$> substTys sb instTy genApp = do s <- genWTType KType (f, fTy) <- genSyns (TFun () s ty) @@ -445,16 +449,22 @@ genCxtExtendingLocal = do ] local cxtE $ go (n - 1) -genPrimCon :: MonadGen m => m [PrimCon] -genPrimCon = do - char <- Gen.unicode - let intBound = fromIntegral (maxBound :: Word64) -- arbitrary - n <- Gen.integral $ Range.linear (-intBound) intBound - pure - [ PrimChar char - , PrimInt n - ] +-- We have to be careful to only generate primitive constructors which are +-- in scope (i.e. their type is in scope) +genPrimCon :: forall mc mg. (MonadReader Cxt mc, MonadGen mg) => mc [mg (PrimCon, Name)] +genPrimCon = catMaybes <$> sequence [genChar, genInt] where + genChar = whenInScope PrimChar 'a' Gen.unicode + intBound = fromIntegral (maxBound :: Word64) -- arbitrary + genInt = whenInScope PrimInt 0 $ Gen.integral $ Range.linear (-intBound) intBound + -- The 'tst' is arbitrary, only used for checking if the primcon is in scope + -- and does not affect the generator. + whenInScope :: (a -> PrimCon) -> a -> mg a -> mc (Maybe (mg (PrimCon, Name))) + whenInScope f tst g = do + s <- asks $ primConInScope (f tst) + pure $ case s of + (False, _) -> Nothing + (True, tc) -> Just $ (\x -> (f x, tc)) <$> g -- This ensures that when we modify the constructors of `PrimCon` (i.e. we add/remove primitive types), -- we are alerted that we need to update this generator. _ = \case diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs index 21cf9c728..8700d9404 100644 --- a/primer/test/Tests/Primitives.hs +++ b/primer/test/Tests/Primitives.hs @@ -7,7 +7,7 @@ import Foreword import qualified Data.Map as M import Gen.Core.Typed (forAllT, genPrimCon, propertyWT) import Hedgehog (Property, assert) -import Hedgehog.Gen (element) +import Hedgehog.Gen (choice) import Primer.App (defaultTypeDefs) import Primer.Core ( ASTTypeDef ( @@ -37,7 +37,7 @@ import Tests.Typecheck (runTypecheckTestMFromIn) hprop_all_prim_cons_have_typedef :: Property hprop_all_prim_cons_have_typedef = propertyWT (buildTypingContext defaultTypeDefs mempty NoSmartHoles) $ do - c <- forAllT $ element =<< genPrimCon + c <- forAllT $ (fmap fst . choice) =<< genPrimCon assert $ primConName c `elem` M.keys allPrimTypeDefs -- If we use a prim con, then we need the corresponding prim type From 15a300145de03172d4c4e728baf196f8066f1e87 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Mon, 21 Feb 2022 16:21:47 +0000 Subject: [PATCH 03/12] feat: add tests that when synth we get a KType When we successfully synthesise a type for some term, that type should kind-check at the kind KType. I.e. the types we synthesise are actually recognised as types by our kind checker. --- primer/test/Tests/Typecheck.hs | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs index 6a539e237..99068d571 100644 --- a/primer/test/Tests/Typecheck.hs +++ b/primer/test/Tests/Typecheck.hs @@ -12,6 +12,11 @@ import Gen.Core.Raw ( genName, genType, ) +import Gen.Core.Typed ( + forAllT, + genSyn, + propertyWT, + ) import Hedgehog hiding (check) import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range @@ -46,6 +51,7 @@ import Primer.Core ( _typeMeta, ) import Primer.Core.DSL +import Primer.Core.Utils (generateIDs, generateTypeIDs) import Primer.Name (Name, NameCounter) import Primer.Typecheck ( Cxt, @@ -61,6 +67,7 @@ import Primer.Typecheck ( import Test.Tasty.HUnit (Assertion, assertFailure, (@?=)) import TestM (TestM, evalTestM) import TestUtils (withPrimDefs) +import Tests.Gen.Core.Typed unit_identity :: Assertion unit_identity = @@ -450,6 +457,26 @@ unit_prim_fun_applied :: Assertion unit_prim_fun_applied = expectTypedWithPrims $ \m -> ann (app (global (m ! "hexToNat")) (char 'a')) (tapp (tcon "Maybe") (tcon "Nat")) +-- Whenever we synthesise a type, then it kind-checks against KType +hprop_synth_well_typed_extcxt :: Property +hprop_synth_well_typed_extcxt = withTests 1000 $ + withDiscards 2000 $ + propertyWTInExtendedLocalGlobalCxt (buildTypingContext defaultTypeDefs mempty NoSmartHoles) $ do + (e, _ty) <- forAllT genSyn + ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e + void $ checkKindTest KType ty' + +-- As hprop_synth_well_typed_extcxt, but in the empty context +-- this is in case there are problems with primitive constructors +-- (which cannot be used unless their corresponding type is in scope) +hprop_synth_well_typed_defcxt :: Property +hprop_synth_well_typed_defcxt = withTests 1000 $ + withDiscards 2000 $ + propertyWT (buildTypingContext mempty mempty NoSmartHoles) $ do + (e, _ty) <- forAllT genSyn + ty' <- generateTypeIDs . fst =<< synthTest =<< generateIDs e + void $ checkKindTest KType ty' + -- * Helpers expectTyped :: TypecheckTestM Expr -> Assertion From e5712f5bc128265455c11870a29011da05fd5e7a Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 15:23:02 +0000 Subject: [PATCH 04/12] refactor: App module We split the module in two, to enable creation of a Primer.Import module which depends on some basic definitions in Primer.App, but should provide a new handler for Primer.App to use. If we did not do this refactor, we would create a import cycle. --- primer/primer.cabal | 1 + primer/src/Primer/App.hs | 245 +--------------------------- primer/src/Primer/App/Core.hs | 291 ++++++++++++++++++++++++++++++++++ 3 files changed, 293 insertions(+), 244 deletions(-) create mode 100644 primer/src/Primer/App/Core.hs diff --git a/primer/primer.cabal b/primer/primer.cabal index 1f7f3dd44..15585ca01 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -19,6 +19,7 @@ library Primer.Action.Priorities Primer.API Primer.App + Primer.App.Core Primer.Core Primer.Core.DSL Primer.Core.Transform diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 936e1bb2f..57b8d73d7 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -50,11 +50,6 @@ module Primer.App ( import Foreword import Control.Monad.Fresh (MonadFresh (..)) -import Data.Aeson ( - ToJSON (toEncoding), - defaultOptions, - genericToEncoding, - ) import Data.Bitraversable (bimapM) import Data.Generics.Product (position) import Data.Generics.Uniplate.Zipper ( @@ -70,30 +65,21 @@ import Primer.Action ( applyActionsToBody, applyActionsToTypeSig, ) - +import Primer.App.Core import Primer.Core ( ASTDef (..), - ASTTypeDef (..), Def (..), Expr, Expr' (EmptyHole, Var), - ExprMeta, ID (..), - Kind (..), Meta (..), - PrimDef (..), Type, Type' (..), TypeDef (..), - TypeMeta, - ValCon (..), defAST, - defID, defName, defPrim, getID, - primDefID, - primFunType, _exprMeta, _exprMetaLens, _exprTypeMeta, @@ -101,14 +87,12 @@ import Primer.Core ( _typeMeta, _typeMetaLens, ) -import Primer.Core.DSL (create, emptyHole, tEmptyHole) import Primer.Core.Utils (_freeTmVars, _freeTyVars, _freeVarsTy) import Primer.Eval (EvalDetail, EvalError) import qualified Primer.Eval as Eval import Primer.EvalFull (Dir, EvalFullError (TimedOut), TerminationBound, evalFull) import Primer.JSON import Primer.Name (Name, NameCounter, freshName, unsafeMkName) -import Primer.Primitives (allPrimDefs, allPrimTypeDefs) import Primer.Questions ( Question (..), generateNameExpr, @@ -151,52 +135,6 @@ import Primer.Zipper ( _target, ) --- | The program state, shared between the frontend and backend --- This is much more info than we need to send - for example we probably don't --- 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 - , progSelection :: Maybe Selection - , progSmartHoles :: SmartHoles - , progLog :: Log -- The log of all actions - } - deriving (Eq, Show, Generic) - deriving (FromJSON, ToJSON) via VJSON Prog - --- | The action log --- This is the canonical store of the program - we can recreate any current or --- past program state by replaying this log. --- Each item is a sequence of Core actions which should be applied atomically. --- Items are stored in reverse order so it's quick to add new ones. -newtype Log = Log {unlog :: [[ProgAction]]} - deriving (Eq, Show, Generic) - deriving (FromJSON, ToJSON) via VJSON Log - --- | Describes what interface element the user has selected. --- A definition in the left hand nav bar, and possibly a node in that definition. -data Selection = Selection - { selectedDef :: ASTDef - , selectedNode :: Maybe NodeSelection - } - deriving (Eq, Show, Generic) - deriving (ToJSON, FromJSON) via VJSON Selection - --- | A selected node, in the body or type signature of some definition. --- We have the following invariant: @nodeType = SigNode ==> isRight meta@ -data NodeSelection = NodeSelection - { nodeType :: NodeType - , nodeId :: ID - , meta :: Either ExprMeta TypeMeta - } - deriving (Eq, Show, Generic) - deriving (ToJSON, FromJSON) via VJSON NodeSelection - -data NodeType = BodyNode | SigNode - deriving (Eq, Show, Generic) - deriving (ToJSON, FromJSON) via VJSON NodeType - -- | The type of requests which can mutate the application state. -- -- Note that `Reset` is not undo-able, as it wipes the log along with @@ -541,106 +479,6 @@ runQueryAppM (QueryAppM m) appState = case runExcept (runReaderT m appState) of Left err -> Left err Right res -> Right res --- | We use this type to remember which "new app" was used to --- initialize the session. We need this so that program resets and --- undo know which baseline app to start with when performing their --- corresponding action. -data InitialApp - = NewApp - | NewEmptyApp - deriving (Eq, Show, Generic) - deriving (FromJSON, ToJSON) via VJSON InitialApp - --- | Given an 'InitialApp', return the corresponding new app instance. -initialApp :: InitialApp -> App -initialApp NewApp = newApp -initialApp NewEmptyApp = newEmptyApp - --- | The global App state --- --- Note that the 'ToJSON' and 'FromJSON' instances for this type are --- not used in the frontend, and therefore we can use "Data.Aeson"s --- generic instances for them. -data App = App - { appIdCounter :: Int - , appNameCounter :: NameCounter - , appProg :: Prog - , appInit :: InitialApp - } - deriving (Eq, Show, Generic) - -instance ToJSON App where - toEncoding = genericToEncoding defaultOptions - -instance FromJSON App - --- | An empty initial program. -newEmptyProg :: Prog -newEmptyProg = - let expr = EmptyHole (Meta 1 Nothing Nothing) - ty = TEmptyHole (Meta 2 Nothing Nothing) - def = DefAST $ ASTDef 0 "main" expr ty - in Prog - { progTypes = [] - , progDefs = Map.singleton 0 def - , progSelection = Nothing - , progSmartHoles = SmartHoles - , progLog = Log [] - } - --- | An initial app whose program is completely empty. -newEmptyApp :: App -newEmptyApp = - App - { appIdCounter = 3 - , appNameCounter = toEnum 0 - , appProg = newEmptyProg - , appInit = NewEmptyApp - } - --- | An initial program with some useful typedefs. -newProg :: Prog -newProg = - newEmptyProg - { progTypes = defaultTypeDefs - , progDefs = defaultDefs - } - -defaultDefsNextId :: ID -defaultDefs :: Map ID Def -(defaultDefs, defaultDefsNextId) = - let (defs, nextID) = create $ do - mainExpr <- emptyHole - mainType <- tEmptyHole - let astDefs = - [ ASTDef - { astDefID = 0 - , astDefName = "main" - , astDefExpr = mainExpr - , astDefType = mainType - } - ] - primDefs <- for (Map.toList allPrimDefs) $ \(primDefName, def) -> do - primDefType <- primFunType def - primDefID <- fresh - pure $ - PrimDef - { primDefID - , primDefName - , primDefType - } - pure $ map DefAST astDefs <> map DefPrim primDefs - in (Map.fromList $ (\d -> (defID d, d)) <$> defs, nextID) - --- | An initial app whose program includes some useful definitions. -newApp :: App -newApp = - newEmptyApp - { appProg = newProg - , appInit = NewApp - , appIdCounter = fromEnum defaultDefsNextId - } - -- | Construct a new, empty expression newExpr :: MonadEditApp m => m Expr newExpr = do @@ -889,84 +727,3 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do lookupASTDef :: ID -> Map ID Def -> Maybe ASTDef lookupASTDef id = defAST <=< Map.lookup id - -defaultTypeDefs :: [TypeDef] -defaultTypeDefs = - map - TypeDefAST - [boolDef, natDef, listDef, maybeDef, pairDef, eitherDef] - <> map - TypeDefPrim - (Map.elems allPrimTypeDefs) - --- | A definition of the Bool type -boolDef :: ASTTypeDef -boolDef = - ASTTypeDef - { astTypeDefName = "Bool" - , astTypeDefParameters = [] - , astTypeDefConstructors = - [ ValCon "True" [] - , ValCon "False" [] - ] - , astTypeDefNameHints = ["p", "q"] - } - --- | A definition of the Nat type -natDef :: ASTTypeDef -natDef = - ASTTypeDef - { astTypeDefName = "Nat" - , astTypeDefParameters = [] - , astTypeDefConstructors = - [ ValCon "Zero" [] - , ValCon "Succ" [TCon () "Nat"] - ] - , astTypeDefNameHints = ["i", "j", "n", "m"] - } - --- | A definition of the List type -listDef :: ASTTypeDef -listDef = - ASTTypeDef - { astTypeDefName = "List" - , astTypeDefParameters = [("a", KType)] - , astTypeDefConstructors = - [ ValCon "Nil" [] - , ValCon "Cons" [TVar () "a", TApp () (TCon () "List") (TVar () "a")] - ] - , astTypeDefNameHints = ["xs", "ys", "zs"] - } - --- | A definition of the Maybe type -maybeDef :: ASTTypeDef -maybeDef = - ASTTypeDef - { astTypeDefName = "Maybe" - , astTypeDefParameters = [("a", KType)] - , astTypeDefConstructors = - [ ValCon "Nothing" [] - , ValCon "Just" [TVar () "a"] - ] - , astTypeDefNameHints = ["mx", "my", "mz"] - } - --- | A definition of the Pair type -pairDef :: ASTTypeDef -pairDef = - ASTTypeDef - { astTypeDefName = "Pair" - , astTypeDefParameters = [("a", KType), ("b", KType)] - , astTypeDefConstructors = [ValCon "MakePair" [TVar () "a", TVar () "b"]] - , astTypeDefNameHints = [] - } - --- | A definition of the Either type -eitherDef :: ASTTypeDef -eitherDef = - ASTTypeDef - { astTypeDefName = "Either" - , astTypeDefParameters = [("a", KType), ("b", KType)] - , astTypeDefConstructors = [ValCon "Left" [TVar () "a"], ValCon "Right" [TVar () "b"]] - , astTypeDefNameHints = [] - } diff --git a/primer/src/Primer/App/Core.hs b/primer/src/Primer/App/Core.hs new file mode 100644 index 000000000..e7c97ac88 --- /dev/null +++ b/primer/src/Primer/App/Core.hs @@ -0,0 +1,291 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} + +-- This module defines the high level application functions. + +module Primer.App.Core ( + Log (..), + App (..), + InitialApp (..), + initialApp, + newProg, + newEmptyProg, + newApp, + newEmptyApp, + Prog (..), + Selection (..), + NodeSelection (..), + NodeType (..), + boolDef, + natDef, + listDef, + eitherDef, + defaultTypeDefs, +) where + +import Foreword + +import Control.Monad.Fresh (MonadFresh (..)) +import Data.Aeson ( + ToJSON (toEncoding), + defaultOptions, + genericToEncoding, + ) +import qualified Data.Map.Strict as Map +import Primer.Action ( + ProgAction (..), + ) + +import Primer.Core ( + ASTDef (..), + ASTTypeDef (..), + Def (..), + Expr' (EmptyHole), + ExprMeta, + ID (..), + Kind (..), + Meta (..), + PrimDef (..), + Type' (..), + TypeDef (..), + TypeMeta, + ValCon (..), + defID, + primDefID, + primFunType, + ) +import Primer.Core.DSL (create, emptyHole, tEmptyHole) +import Primer.JSON +import Primer.Name (NameCounter) +import Primer.Primitives (allPrimDefs, allPrimTypeDefs) +import Primer.Typecheck ( + SmartHoles (SmartHoles), + ) + +-- | The program state, shared between the frontend and backend +-- This is much more info than we need to send - for example we probably don't +-- 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 + , progSelection :: Maybe Selection + , progSmartHoles :: SmartHoles + , progLog :: Log -- The log of all actions + } + deriving (Eq, Show, Generic) + deriving (FromJSON, ToJSON) via VJSON Prog + +-- | The action log +-- This is the canonical store of the program - we can recreate any current or +-- past program state by replaying this log. +-- Each item is a sequence of Core actions which should be applied atomically. +-- Items are stored in reverse order so it's quick to add new ones. +newtype Log = Log {unlog :: [[ProgAction]]} + deriving (Eq, Show, Generic) + deriving (FromJSON, ToJSON) via VJSON Log + +-- | Describes what interface element the user has selected. +-- A definition in the left hand nav bar, and possibly a node in that definition. +data Selection = Selection + { selectedDef :: ASTDef + , selectedNode :: Maybe NodeSelection + } + deriving (Eq, Show, Generic) + deriving (ToJSON, FromJSON) via VJSON Selection + +-- | A selected node, in the body or type signature of some definition. +-- We have the following invariant: @nodeType = SigNode ==> isRight meta@ +data NodeSelection = NodeSelection + { nodeType :: NodeType + , nodeId :: ID + , meta :: Either ExprMeta TypeMeta + } + deriving (Eq, Show, Generic) + deriving (ToJSON, FromJSON) via VJSON NodeSelection + +data NodeType = BodyNode | SigNode + deriving (Eq, Show, Generic) + deriving (ToJSON, FromJSON) via VJSON NodeType + +-- | We use this type to remember which "new app" was used to +-- initialize the session. We need this so that program resets and +-- undo know which baseline app to start with when performing their +-- corresponding action. +data InitialApp + = NewApp + | NewEmptyApp + deriving (Eq, Show, Generic) + deriving (FromJSON, ToJSON) via VJSON InitialApp + +-- | Given an 'InitialApp', return the corresponding new app instance. +initialApp :: InitialApp -> App +initialApp NewApp = newApp +initialApp NewEmptyApp = newEmptyApp + +-- | The global App state +-- +-- Note that the 'ToJSON' and 'FromJSON' instances for this type are +-- not used in the frontend, and therefore we can use "Data.Aeson"s +-- generic instances for them. +data App = App + { appIdCounter :: Int + , appNameCounter :: NameCounter + , appProg :: Prog + , appInit :: InitialApp + } + deriving (Eq, Show, Generic) + +instance ToJSON App where + toEncoding = genericToEncoding defaultOptions + +instance FromJSON App + +-- | An empty initial program. +newEmptyProg :: Prog +newEmptyProg = + let expr = EmptyHole (Meta 1 Nothing Nothing) + ty = TEmptyHole (Meta 2 Nothing Nothing) + def = DefAST $ ASTDef 0 "main" expr ty + in Prog + { progTypes = [] + , progDefs = Map.singleton 0 def + , progSelection = Nothing + , progSmartHoles = SmartHoles + , progLog = Log [] + } + +-- | An initial app whose program is completely empty. +newEmptyApp :: App +newEmptyApp = + App + { appIdCounter = 3 + , appNameCounter = toEnum 0 + , appProg = newEmptyProg + , appInit = NewEmptyApp + } + +-- | An initial program with some useful typedefs. +newProg :: Prog +newProg = + newEmptyProg + { progTypes = defaultTypeDefs + , progDefs = defaultDefs + } + +defaultDefsNextId :: ID +defaultDefs :: Map ID Def +(defaultDefs, defaultDefsNextId) = + let (defs, nextID) = create $ do + mainExpr <- emptyHole + mainType <- tEmptyHole + let astDefs = + [ ASTDef + { astDefID = 0 + , astDefName = "main" + , astDefExpr = mainExpr + , astDefType = mainType + } + ] + primDefs <- for (Map.toList allPrimDefs) $ \(primDefName, def) -> do + primDefType <- primFunType def + primDefID <- fresh + pure $ + PrimDef + { primDefID + , primDefName + , primDefType + } + pure $ map DefAST astDefs <> map DefPrim primDefs + in (Map.fromList $ (\d -> (defID d, d)) <$> defs, nextID) + +-- | An initial app whose program includes some useful definitions. +newApp :: App +newApp = + newEmptyApp + { appProg = newProg + , appInit = NewApp + , appIdCounter = fromEnum defaultDefsNextId + } + +defaultTypeDefs :: [TypeDef] +defaultTypeDefs = + map + TypeDefAST + [boolDef, natDef, listDef, maybeDef, pairDef, eitherDef] + <> map + TypeDefPrim + (Map.elems allPrimTypeDefs) + +-- | A definition of the Bool type +boolDef :: ASTTypeDef +boolDef = + ASTTypeDef + { astTypeDefName = "Bool" + , astTypeDefParameters = [] + , astTypeDefConstructors = + [ ValCon "True" [] + , ValCon "False" [] + ] + , astTypeDefNameHints = ["p", "q"] + } + +-- | A definition of the Nat type +natDef :: ASTTypeDef +natDef = + ASTTypeDef + { astTypeDefName = "Nat" + , astTypeDefParameters = [] + , astTypeDefConstructors = + [ ValCon "Zero" [] + , ValCon "Succ" [TCon () "Nat"] + ] + , astTypeDefNameHints = ["i", "j", "n", "m"] + } + +-- | A definition of the List type +listDef :: ASTTypeDef +listDef = + ASTTypeDef + { astTypeDefName = "List" + , astTypeDefParameters = [("a", KType)] + , astTypeDefConstructors = + [ ValCon "Nil" [] + , ValCon "Cons" [TVar () "a", TApp () (TCon () "List") (TVar () "a")] + ] + , astTypeDefNameHints = ["xs", "ys", "zs"] + } + +-- | A definition of the Maybe type +maybeDef :: ASTTypeDef +maybeDef = + ASTTypeDef + { astTypeDefName = "Maybe" + , astTypeDefParameters = [("a", KType)] + , astTypeDefConstructors = + [ ValCon "Nothing" [] + , ValCon "Just" [TVar () "a"] + ] + , astTypeDefNameHints = ["mx", "my", "mz"] + } + +-- | A definition of the Pair type +pairDef :: ASTTypeDef +pairDef = + ASTTypeDef + { astTypeDefName = "Pair" + , astTypeDefParameters = [("a", KType), ("b", KType)] + , astTypeDefConstructors = [ValCon "MakePair" [TVar () "a", TVar () "b"]] + , astTypeDefNameHints = [] + } + +-- | A definition of the Either type +eitherDef :: ASTTypeDef +eitherDef = + ASTTypeDef + { astTypeDefName = "Either" + , astTypeDefParameters = [("a", KType), ("b", KType)] + , astTypeDefConstructors = [ValCon "Left" [TVar () "a"], ValCon "Right" [TVar () "b"]] + , astTypeDefNameHints = [] + } From ae70998bfdf99c47ea5c53272c3da0c29d9403d7 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 15 Feb 2022 19:19:39 +0000 Subject: [PATCH 05/12] feat: Support importing (i.e. copying the definiton) types The reason that srcProg and primSrcProg have been put into an Applicative context is that later we will want to import terms, and to test we will define some terms in these programs. This will need a MonadFresh context. To avoid changing all use sites later, we will write it monadically now. --- primer/primer.cabal | 3 + primer/src/Primer/App.hs | 31 ++ primer/src/Primer/Core.hs | 14 + primer/src/Primer/Import.hs | 304 +++++++++++++++++++ primer/src/Primer/Typecheck.hs | 9 +- primer/src/Primer/Utils.hs | 20 ++ primer/test/Tests/Import.hs | 525 +++++++++++++++++++++++++++++++++ 7 files changed, 898 insertions(+), 8 deletions(-) create mode 100644 primer/src/Primer/Import.hs create mode 100644 primer/src/Primer/Utils.hs create mode 100644 primer/test/Tests/Import.hs diff --git a/primer/primer.cabal b/primer/primer.cabal index 15585ca01..1d43cea8e 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -27,6 +27,7 @@ library Primer.Database Primer.Eval Primer.EvalFull + Primer.Import Primer.Name Primer.Name.Fresh Primer.Primitives @@ -35,6 +36,7 @@ library Primer.Subst Primer.Typecheck Primer.Unification + Primer.Utils Primer.Zipper Primer.ZipperCxt @@ -105,6 +107,7 @@ test-suite primer-test Tests.EvalFull Tests.FreeVars Tests.Gen.Core.Typed + Tests.Import Tests.Primitives Tests.Question Tests.Refine diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 57b8d73d7..550069014 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -21,8 +21,12 @@ module Primer.App ( runEditAppM, runQueryAppM, Prog (..), + tcEverything, tcWholeProg, ProgAction (..), + ImportActionConfig (..), + ImportError (..), + importFromApp, ProgError (..), Question (..), handleQuestion, @@ -45,6 +49,7 @@ module Primer.App ( listDef, eitherDef, defaultTypeDefs, + MonadEditApp, ) where import Foreword @@ -91,6 +96,11 @@ import Primer.Core.Utils (_freeTmVars, _freeTyVars, _freeVarsTy) import Primer.Eval (EvalDetail, EvalError) import qualified Primer.Eval as Eval import Primer.EvalFull (Dir, EvalFullError (TimedOut), TerminationBound, evalFull) +import Primer.Import ( + ImportActionConfig (..), + ImportError (..), + importFromApp', + ) import Primer.JSON import Primer.Name (Name, NameCounter, freshName, unsafeMkName) import Primer.Questions ( @@ -165,6 +175,7 @@ data ProgError -- (However, this is not entirely true currently, see -- https://github.com/hackworthltd/primer/issues/3) TypeDefError Text + | ImportError ImportError deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ProgError @@ -439,6 +450,15 @@ handleResetRequest = do put app pure $ appProg app +importFromApp :: forall m. MonadEditApp m => Prog -> ImportActionConfig -> m () +importFromApp srcProg iac = do + curProg <- get + finalProg <- runReaderT (importFromApp' srcProg iac) curProg + -- We typecheck the final result, but this should pass + -- if the conditions in importFromApp' are satisfied + prog' <- tcEverything finalProg + modify (\s -> s{appProg = prog'}) + -- | A shorthand for the constraints we need when performing mutation -- operations on the application. -- @@ -598,6 +618,17 @@ loopM f a = Left a' -> loopM f a' Right b -> pure b +-- | As 'tcWholeProg', but also checks type definitions +tcEverything :: MonadEditApp m => Prog -> m Prog +tcEverything p = do + x <- runExceptT $ checkTypeDefs $ progTypes p + case x of + Left e -> throwError $ ActionError e + Right () -> pure () + tcWholeProg p + +-- | Checks every term definition, but not typedefs. +-- returns the same program but with typecaches updated tcWholeProg :: forall m. MonadEditApp m => Prog -> m Prog tcWholeProg p = let tc :: ReaderT Cxt (ExceptT ActionError m) Prog diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index c4db411b0..622574875 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -35,6 +35,7 @@ module Primer.Core ( TypeDef (..), typeDefAST, typeDefKind, + _typeDefName, typeDefName, typeDefNameHints, typeDefParameters, @@ -454,6 +455,19 @@ valConType td vc = foralls = foldr (\(n, k) t -> TForall () n k t) args (astTypeDefParameters td) in foralls +typeDefLens :: Lens' PrimTypeDef a -> Lens' ASTTypeDef a -> Lens' TypeDef a +typeDefLens lp la = lens getter setter + where + getter = \case + TypeDefPrim d -> view lp d + TypeDefAST d -> view la d + setter = \case + TypeDefPrim d -> TypeDefPrim . flip (set lp) d + TypeDefAST d -> TypeDefAST . flip (set la) d + +_typeDefName :: Lens' TypeDef Name +_typeDefName = typeDefLens #primTypeDefName #astTypeDefName + typeDefName :: TypeDef -> Name typeDefName = \case TypeDefPrim t -> primTypeDefName t diff --git a/primer/src/Primer/Import.hs b/primer/src/Primer/Import.hs new file mode 100644 index 000000000..38e6284de --- /dev/null +++ b/primer/src/Primer/Import.hs @@ -0,0 +1,304 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedLabels #-} + +module Primer.Import ( + ImportError (..), + importFromApp', + ImportActionConfig (..), +) where + +import Control.Monad.NestedError (MonadNestedError (throwError')) +import Data.Generics.Uniplate.Data (transformM) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import Foreword +import Optics ( + AffineTraversal', + Field2 (_2), + traverseOf, + traversed, + (%), + (%~), + (.~), + ) +import Primer.App.Core ( + App (appProg), + Prog (progTypes), + ) +import Primer.Core ( + Type', + TypeDef, + ValCon (valConArgs, valConName), + astTypeDefConstructors, + typeDefAST, + typeDefKind, + typeDefName, + _typeDefName, + ) +import Primer.Core.Utils (alphaEqTy) +import Primer.JSON +import Primer.Name (Name) +import Primer.Typecheck (mkTypeDefMap) +import Primer.Utils (distinct') + +data ImportError + = -- | Cannot both import and rename a type + ImportRenameType Name + | -- | Cannot import two types under the same name, or something that clashes with an existing type + DuplicateTypes [Name] + | -- | Cannot import two ctors under the same name, or something that clashes with an existing ctors + DuplicateCtors [Name] + | -- | Cannot import something that does not exist + UnknownImportedType Name + | -- | Cannot import something that does not exist (args: an imported type, and its non-existent constructor) + UnknownImportedCtor Name Name + | -- | We cannot currently rename primitive types (as the types of primitive constructors are + -- hardcoded by name) + CannotRenamePrimitiveType Name + | -- | Have asked to import a primitive type, but also to rewrite its constructors + PrimitiveTypeHasNoCtor Name + | -- | Must import all constructors of any imported type (args: an imported type, and a non-imported constructor) + MissedImportCtor Name Name + | -- | Cannot rewrite a dep which does not exist (although, since it cannot be referred to, nothing would go wrong if we allowed it...) + UnknownRewrittenSrcType Name + | -- | Cannot rewrite into a type that does not exist + UnknownRewrittenTgtType Name + | -- | Tried to rewrite the first arg to the second, but they are of different kinds + RewriteTypeKindMismatch Name Name + | -- | Tried to rewrite a primitive to a non-primitive, or vice versa + RewriteTypePrimitiveMismatch Name Name + | -- | Must rewrite all constructors of any rewritten type: args are type its (first) ctor that were missed + MissedRewriteCtor Name Name + | -- | In a rewritten type (first arg), cannot rewrite two ctors to the same thing (second arg) + DuplicateRewriteCtor Name [Name] + | -- | The constructor rewrites for this type rewriting did not cover all constructors of the target + RewriteCtorsNotSurjective Name Name + | -- | We attempted to rewrite a ctor that does not exist. Args: the type, and its non-existent ctor + RewriteCtorSrcNotExist Name Name + | -- | We attempted to rewrite into a ctor that does not exist. Args: the type, and its non-existent ctor + RewriteCtorTgtNotExist Name Name + | -- | This type was referenced in the source, but we have neither imported it nor rewritten it + ReferencedTypeNotHandled Name + | -- | @RewrittenCtorTypeDiffers ty1 con1 ty2 con2@: we tried to rewrite @ty1@ into @ty2@, mapping @con1@ to @con2@, but their types do not match + RewrittenCtorTypeDiffers Name Name Name Name + deriving (Eq, Show, Generic) + deriving (FromJSON, ToJSON) via VJSON ImportError + +-- | How to rename a type, and each of its ctors +type TypeImportDetails = Map Name (Name, Map Name Name) + +-- | The generic "import" is +-- "Given +-- - an App (actually, Prog) 'A' +-- - a bunch of type/term defs in 'A' and some free local names +-- - a mapping from dependencies of the stuff in 'A' to appropriate local stuff +-- we will copy the code out of 'A' into your own app, renaming as asked" +-- +-- The keys of the iacImport* maps must exist in the appropriate external App +-- The values of the iacImport* maps must be free (type/term names) in the current App +-- For types, the fst of the value must be free, and the snd map must be +-- keys are exactly the ctors of the type in 'A', values are free constructor names +-- The keys of iacDeps* must cover all free vars of the defs in 'A' named by iacImport* +-- For types, the constructor map must be a bijection +-- The values of iacDeps* must exist in the current App, and have the same Kind/Type (after substituting types according to iacDeps) as the key does. +-- +-- (The reason we require a bijection for rewriting constructors is for +-- translating pattern matches: +-- - It needs to be injective for the translation, as previously distinguished +-- cases are now identified +-- - It needs to be surjective for the translated match to be exhaustive) +-- +-- We will typecheck the final result, but this should pass if the conditions above are satisfied +data ImportActionConfig = IAC + { iacImportRenamingTypes :: TypeImportDetails + , iacDepsTypes :: TypeImportDetails + } + +-- | Computes the new program with a copy of the requested imports, +-- but does not typecheck it +-- +-- See 'App.importFromApp' for a version that typechecks and updates an App +-- state. +importFromApp' :: + (MonadNestedError ImportError e m, MonadReader App m) => + Prog -> + ImportActionConfig -> + m Prog +importFromApp' srcProg iac = do + curProg <- asks appProg + newTypeDefs <- getImportTypesFromApp curProg (srcProg, iac) + pure $ curProg & #progTypes %~ (++ newTypeDefs) + +getImportTypesFromApp :: forall m e. MonadNestedError ImportError e m => Prog -> (Prog, ImportActionConfig) -> m [TypeDef] +getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes}) = + {- We check requirements, to give nice error messages, rather than "typechecker says no" + - Things need to exist in srcProg: + - types in iacImportRenamingTypes + - constructors in iacImportRenamingTypes + - types/constructors in iacDepsTypes + - all these can only be mentioned once (either one import, or one rename-deps) + - Things that we are creating need to have names distinct from each other and everything in curProg + - types/constructors in iacImportRenamingTypes + - Referenced things (i.e. types appearing in imported constructor args) need to be "covered": either + - imported, no further checks + - or renamed as a dep: then their type/kind must match + - iacImportRenamingTypes and iacDepsTypes: for each type T ~> (T',ctorMap) + - The keys of the ctorMap are exactly the ctors of T + -} + do + -- Not allowed to both import and dep-rename some type + for_ (Map.intersection iacImportRenamingTypes iacDepsTypes) $ throwError' . ImportRenameType . fst + + -- things we create have distinct names, and don't appear in curProg + let createdTypes = fst <$> Map.elems iacImportRenamingTypes + let createdCtors = concatMap (Map.elems . snd) $ Map.elems iacImportRenamingTypes + let extantTypes = typeDefName <$> progTypes curProg + let extantCtors = + concatMap (fmap valConName . astTypeDefConstructors) $ + mapMaybe typeDefAST $ + progTypes curProg + case distinct' $ createdTypes ++ extantTypes of + Left dups -> throwError' $ DuplicateTypes dups + Right _ -> pure () + case distinct' $ createdCtors ++ extantCtors of + Left dups -> throwError' $ DuplicateCtors dups + Right _ -> pure () + + -- make renaming map, and grab the typedefs, with the new type/ctor name. NB: the argument types still need rewriting! + let srcTypes = mkTypeDefMap $ progTypes srcProg + (tyrn1, _ctorrn1, tydefs) <- getAp $ + flip Map.foldMapWithKey iacImportRenamingTypes $ \srcTyName (tgtTyName, ctorMap) -> Ap $ do + -- imported type exists in srcProg + srcTy <- + lookupOrThrow srcTyName srcTypes $ + UnknownImportedType srcTyName + -- must import all the constructors (and nothing else) + case typeDefAST srcTy of + Nothing -> do + unless (srcTyName == tgtTyName) $ throwError' $ CannotRenamePrimitiveType srcTyName + unless (Map.null ctorMap) $ throwError' $ PrimitiveTypeHasNoCtor srcTyName + Just srcADT -> do + let srcCtors = Set.fromList (valConName <$> astTypeDefConstructors srcADT) + let importedCtors = Map.keysSet ctorMap + -- cannot import a non-existant constructor + for_ (importedCtors Set.\\ srcCtors) $ + throwError' . UnknownImportedCtor srcTyName + + renamedTy <- + traverseOf + (#_TypeDefAST % #astTypeDefConstructors % traversed % #valConName) + -- we must import all constructors + (\c -> lookupOrThrow c ctorMap $ MissedImportCtor srcTyName c) + $ srcTy & _typeDefName .~ tgtTyName + + pure + ( Map.singleton srcTyName tgtTyName + , ctorMap + , [renamedTy] + ) + + -- renaming map for deps rewriting + let curTypes = mkTypeDefMap $ progTypes curProg + (tyrn2, _ctorrn2, toCheckRewriteCtorsTypes) <- getAp $ + flip Map.foldMapWithKey iacDepsTypes $ \srcTyName (tgtTyName, ctorMap) -> Ap $ do + -- the rewritten thing must exist in the imported program + -- (nothing would go wrong if we elided this check, but it catches + -- that our caller is broken) + srcTy <- + lookupOrThrow srcTyName srcTypes $ + UnknownRewrittenSrcType srcTyName + -- We must rewrite it to an existing type ... + tgtTy <- + lookupOrThrow tgtTyName curTypes $ + UnknownRewrittenTgtType tgtTyName + -- ... of the same kind + unless (typeDefKind srcTy == typeDefKind tgtTy) $ + throwError' $ RewriteTypeKindMismatch srcTyName tgtTyName + + (_ctorPerm, toCheckRewriteCtorsTypes) <- case (typeDefAST srcTy, typeDefAST tgtTy) of + (Nothing, Nothing) -> do + unless (srcTyName == tgtTyName) $ throwError' $ CannotRenamePrimitiveType srcTyName + -- primitives have no constructors + pure (Map.empty, []) + (Nothing, Just _) -> throwError' $ RewriteTypePrimitiveMismatch srcTyName tgtTyName + (Just _, Nothing) -> throwError' $ RewriteTypePrimitiveMismatch srcTyName tgtTyName + (Just srcADT, Just tgtADT) -> do + let mkCtorMap ty = Map.fromList (map (\c -> (valConName c, c)) $ astTypeDefConstructors ty) + let srcCtorMap = mkCtorMap srcADT + let tgtCtorMap = mkCtorMap tgtADT + let srcCtors = Map.keysSet srcCtorMap + let rewriteSrcCtors = Map.keysSet ctorMap + -- must rewrite every constructor + for_ (srcCtors Set.\\ rewriteSrcCtors) $ throwError' . MissedRewriteCtor srcTyName + -- cannot rewrite two ctors to the same thing (else cannot translate exhaustive pattern matching) + case distinct' $ Map.elems ctorMap of + Left dups -> throwError' $ DuplicateRewriteCtor srcTyName dups + Right _ -> pure () + -- must hit all of the target ctors (else cannot translate exhaustive pattern matching) + unless (Map.keysSet tgtCtorMap `Set.isSubsetOf` Set.fromList (Map.elems ctorMap)) $ + throwError' $ RewriteCtorsNotSurjective srcTyName tgtTyName + + -- for each s->t, check s and t exist respectively, and types same + -- however, we need to rename types to check the ctor types match + -- which we cannot do yet, as we have not built the renaming map, + -- so actually just record what we need to check + toCheck <- for (Map.toList ctorMap) $ \(srcCtor, tgtCtor) -> do + s <- + lookupOrThrow srcCtor srcCtorMap $ + RewriteCtorSrcNotExist srcTyName srcCtor + t <- + lookupOrThrow tgtCtor tgtCtorMap $ + RewriteCtorTgtNotExist tgtTyName tgtCtor + pure (srcTyName, s, tgtTyName, t) + pure + ( Map.singleton + (valConName <$> astTypeDefConstructors srcADT) + (valConName <$> astTypeDefConstructors tgtADT) + , toCheck + ) + + pure + ( Map.singleton srcTyName tgtTyName + , ctorMap + , toCheckRewriteCtorsTypes + ) + + let tyrn = Map.union tyrn1 tyrn2 + + -- Rename the types referenced: + -- everywhere we see a 'TCon', replace it with its image in the 'tyrn' map + -- (We throw an error if they do not exist in our + -- renaming map, i.e. the imported types, or the rewritten deps) + let rewriteTCons :: Type' () -> m (Type' ()) + rewriteTCons = transformM $ + traverseOf tconName $ \tc -> + lookupOrThrow tc tyrn $ ReferencedTypeNotHandled tc + + -- Now check that rewritten constructors have the same type + for_ toCheckRewriteCtorsTypes $ \(srcTy, srcCtor, tgtTy, tgtCtor) -> do + srcCtorArgs <- traverse rewriteTCons $ valConArgs srcCtor + let tgtCtorArgs = valConArgs tgtCtor + unless + ( length srcCtorArgs == length tgtCtorArgs + && and (zipWith alphaEqTy srcCtorArgs tgtCtorArgs) + ) + $ throwError' $ + RewrittenCtorTypeDiffers + srcTy + (valConName srcCtor) + tgtTy + (valConName tgtCtor) + + -- Rename the types referenced. These are now ready to insert into curProg + traverseOf + (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed) + rewriteTCons + tydefs + where + lookupOrThrow :: Ord k => k -> Map k v -> ImportError -> m v + lookupOrThrow k m e = case m Map.!? k of + Nothing -> throwError' e + Just v -> pure v + + tconName :: AffineTraversal' (Type' ()) Name + tconName = #_TCon % _2 diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 5fcff971f..caa198e36 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -104,6 +104,7 @@ import Primer.Core.Utils (alphaEqTy, forgetTypeIDs, generateTypeIDs) import Primer.JSON (CustomJSON (CustomJSON), FromJSON, ToJSON, VJSON) import Primer.Name (Name, NameCounter, freshName) import Primer.Subst (substTy) +import Primer.Utils (distinct) -- | Typechecking takes as input an Expr with 'Maybe Type' annotations and -- produces an Expr with 'Type' annotations - i.e. every node in the output is @@ -343,14 +344,6 @@ checkTypeDefs tds = do -- metadata as it won't be inspected. fakeMeta = generateTypeIDs -distinct :: Ord a => [a] -> Bool -distinct = go mempty - where - go _ [] = True - go seen (x : xs) - | x `S.member` seen = False - | otherwise = go (S.insert x seen) xs - -- | Check all type definitions and top-level definitions, in the empty context checkEverything :: forall e m. diff --git a/primer/src/Primer/Utils.hs b/primer/src/Primer/Utils.hs new file mode 100644 index 000000000..f724701a3 --- /dev/null +++ b/primer/src/Primer/Utils.hs @@ -0,0 +1,20 @@ +module Primer.Utils (distinct, distinct') where + +import qualified Data.Set as S +import Foreword + +distinct :: Ord a => [a] -> Bool +distinct = isRight . distinct' + +-- | Returns either the duplicate items, or the input as a set (if no duplicates) +distinct' :: Ord a => [a] -> Either [a] (S.Set a) +distinct' l = case go mempty l of + ([], s) -> Right s + (dups, _) -> Left dups + where + go seen [] = ([], seen) + go seen (x : xs) = + let r = go (S.insert x seen) xs + in if x `S.member` seen + then first (x :) r + else r diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs new file mode 100644 index 000000000..5336ac6a2 --- /dev/null +++ b/primer/test/Tests/Import.hs @@ -0,0 +1,525 @@ +{-# LANGUAGE OverloadedLabels #-} + +module Tests.Import where + +import Control.Monad.Fresh +import qualified Data.Map.Strict as Map +import Foreword +import Optics +import Primer.App +import Primer.Core +import Primer.Name +import Primer.Primitives (allPrimTypeDefs) +import Test.Tasty.HUnit + +unitDef :: ASTTypeDef +unitDef = + ASTTypeDef + { astTypeDefName = "Unit" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon "MkUnit" []] + , astTypeDefNameHints = [] + } + +srcProg :: (Applicative m) => m Prog +srcProg = + pure + newEmptyProg + { progTypes = [TypeDefAST natDef] + , progDefs = mempty + } + +srcProg2 :: (MonadFresh ID m) => (Name, Name, Name) -> (Name, Name) -> m Prog +srcProg2 (listName, nilName, consName) (roseTyName, roseConName) = do + let listTyDef = + ASTTypeDef + { astTypeDefName = listName + , astTypeDefParameters = [("a", KType)] + , astTypeDefConstructors = + [ ValCon nilName [] + , ValCon consName [TVar () "a", TApp () (TCon () listName) (TVar () "a")] + ] + , astTypeDefNameHints = [] + } + let roseTyDef = + ASTTypeDef + { astTypeDefName = roseTyName + , astTypeDefParameters = [("a", KType)] + , astTypeDefConstructors = + [ ValCon + roseConName + [ TVar () "a" + , TApp () (TCon () listName) (TApp () (TCon () roseTyName) (TVar () "a")) + ] + ] + , astTypeDefNameHints = [] + } + pure + newEmptyProg + { progTypes = [TypeDefAST listTyDef, TypeDefAST roseTyDef] + , progDefs = mempty + } + +-- A program with all primitive types +-- and also String (which depends on "Char") +primSrcProg :: Applicative m => m Prog +primSrcProg = + pure + newEmptyProg + { progTypes = map TypeDefAST [stringDef] <> map TypeDefPrim (Map.elems allPrimTypeDefs) + } + where + stringDef :: ASTTypeDef + stringDef = + ASTTypeDef + { astTypeDefName = "String" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon "Empty" [], ValCon "HeadAnd" [TCon () "Char", TCon () "String"]] + , astTypeDefNameHints = [] + } + +-- Import without renaming works +unit_import_import_simple :: Assertion +unit_import_import_simple = runImportTest $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + } + importFromApp p iac + result <- gets appProg + return $ do + progTypes result @?= progTypes p + progDefs result @?= mempty + +-- We can rename types and ctors when importing +unit_import_import_renaming :: Assertion +unit_import_import_renaming = runImportTest $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + , iacDepsTypes = mempty + } + importFromApp p iac + result <- gets appProg + return $ do + progTypes result + @?= [ TypeDefAST $ + ASTTypeDef + { astTypeDefName = "N" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon "Z" [], ValCon "S" [TCon () "N"]] + , astTypeDefNameHints = astTypeDefNameHints natDef + } + ] + progDefs result @?= mempty + +-- Importing and renaming primitives works +unit_import_primitive :: Assertion +unit_import_primitive = runImportTest $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) + , iacDepsTypes = mempty + } + importFromApp p iac + result <- gets appProg + return $ do + map typeDefName (progTypes result) @?= ["Char"] + progDefs result @?= mempty + +-- test deep subst in ctor types +unit_import_ctor_type :: Assertion +unit_import_ctor_type = runImportTest $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = + Map.fromList + [ ("Rose", ("T", Map.fromList [("MkRose", "C")])) + , ("List", ("List", Map.fromList [("Nil", "Nil"), ("Cons", "Cons")])) + ] + , iacDepsTypes = mempty + } + importFromApp p iac + result <- gets appProg + expect <- srcProg2 ("List", "Nil", "Cons") ("T", "C") + return $ result @?= expect + +-- test rewiring dependencies +-- Here we have mimiced importing a library 'A' +-- and then later a library 'B' which itself depends on 'A' +unit_import_rewire_deps :: Assertion +unit_import_rewire_deps = runImportTest $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let listRenaming = Map.singleton "List" ("L", Map.fromList [("Nil", "Nil"), ("Cons", "Cons")]) + let iac = + IAC + { iacImportRenamingTypes = listRenaming + , iacDepsTypes = mempty + } + importFromApp p iac + let iac' = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = listRenaming + } + importFromApp p iac' + result <- gets appProg + expect <- srcProg2 ("L", "Nil", "Cons") ("T", "C") + return $ result @?= expect + +unit_import_rewire_primitive :: Assertion +unit_import_rewire_primitive = runImportTest $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Char", ("Char", mempty))] + , iacDepsTypes = mempty + } + importFromApp p iac + let iac' = + IAC + { iacImportRenamingTypes = Map.singleton "String" ("S", Map.fromList [("Empty", "Nil"), ("HeadAnd", "Cons")]) + , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + } + importFromApp p iac' + result <- gets appProg + return $ do + map typeDefName (progTypes result) @?= ["Char", "S"] + progDefs result @?= mempty + +-- cannot import without deps +unit_import_ref_not_handled :: Assertion +unit_import_ref_not_handled = runImportTestError (ReferencedTypeNotHandled "List") $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = mempty + } + importFromApp p iac + +-- cannot claim to support deps with free name +unit_import_rewire_tgt_exist :: Assertion +unit_import_rewire_tgt_exist = runImportTestError (UnknownRewrittenTgtType "L") $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = Map.singleton "List" ("L", mempty) + } + importFromApp p iac + +-- cannot claim to support deps with wrong kind +unit_import_rewire_kind_match :: Assertion +unit_import_rewire_kind_match = runImportTestError (RewriteTypeKindMismatch "List" "Unit") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = Map.singleton "List" ("Unit", mempty) + } + importFromApp p iac + +-- cannot import two types/ctors with the same name, or one the same as an existing one +unit_import_name_clash :: Assertion +unit_import_name_clash = do + runImportTestError (DuplicateTypes ["T"]) $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = + Map.fromList + [ ("List", ("T", Map.fromList [("Nil", "Nil"), ("Cons", "Cons")])) + , ("Rose", ("T", Map.fromList [("MkRose", "MkRose")])) + ] + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (DuplicateTypes ["Unit"]) $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- p' + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("T", ("Unit", Map.fromList [("A", "A"), ("B", "B")]))] + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (DuplicateCtors ["C"]) $ do + p <- p' + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("T", ("S", Map.fromList [("A", "C"), ("B", "C")]))] + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (DuplicateCtors ["MkUnit"]) $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- p' + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("T", ("S", Map.fromList [("A", "A"), ("B", "MkUnit")]))] + , iacDepsTypes = mempty + } + importFromApp p iac + where + p' :: (MonadFresh ID m) => m Prog + p' = do + let tyDep = + ASTTypeDef + { astTypeDefName = "T" + , astTypeDefParameters = [] + , astTypeDefConstructors = + [ ValCon "A" [] + , ValCon "B" [] + ] + , astTypeDefNameHints = [] + } + pure + newEmptyProg + { progTypes = [TypeDefAST tyDep] + , progDefs = mempty + } + +-- Test that rewiring dependencies only maps types to isomorphic types +unit_import_rewire_iso :: Assertion +unit_import_rewire_iso = do + runImportTestError (RewriteCtorsNotSurjective "Unit" "Nat") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef natDef] + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Unit" ("Nat", Map.singleton "MkUnit" "Zero") + } + importFromApp + newEmptyProg + { progTypes = [TypeDefAST unitDef] + , progDefs = mempty + } + iac + runImportTestError (RewriteCtorSrcNotExist "Nat" "Nonexistent") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef natDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "Nonexistent")]) + } + importFromApp p iac + runImportTestError (RewriteCtorTgtNotExist "Unit" "Succ") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Succ")]) + } + importFromApp p iac + runImportTestError (DuplicateRewriteCtor "Nat" ["MkUnit"]) $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "MkUnit")]) + } + importFromApp p iac + runImportTestError (RewrittenCtorTypeDiffers "Nat" "Succ" "Nat" "Zero") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef natDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Succ"), ("Succ", "Zero")]) + } + importFromApp p iac + +-- cannot both import and rename the same type +unit_import_import_rename_clash :: Assertion +unit_import_import_rename_clash = runImportTestError (ImportRenameType "Nat") $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + } + importFromApp p iac + +-- cannot import/rewrite nonexistent type/ctor, and have to import/rewrite all ctors of a type +unit_import_nonexist :: Assertion +unit_import_nonexist = do + runImportTestError (UnknownImportedType "Nonexistent") $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nonexistent" ("T", mempty) + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (UnknownImportedCtor "Nat" "Nonexistent") $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "C")]) + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (MissedImportCtor "Nat" "Succ") $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero")]) + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (UnknownRewrittenSrcType "Nonexistent") $ do + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nonexistent" ("T", mempty) + } + importFromApp p iac + runImportTestError (RewriteCtorSrcNotExist "Nat" "Nonexistent") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef natDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "C")]) + } + importFromApp p iac + runImportTestError (RewriteCtorTgtNotExist "Unit" "Nonexistent") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Nonexistent")]) + } + importFromApp p iac + runImportTestError (MissedRewriteCtor "Nat" "Succ") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit")]) + } + importFromApp p iac + +-- Cannot rewrite a ctor to ctor of different type +-- this will hit "unknown ctor" error +unit_import_rewire_cross_type :: Assertion +unit_import_rewire_cross_type = do + runImportTestError (RewriteCtorTgtNotExist "Unit" "Succ") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Succ")]) + } + importFromApp p iac + +-- Cannot rename primitive types (either in import or rewire) +unit_import_rename_prim_type :: Assertion +unit_import_rename_prim_type = do + runImportTestError (CannotRenamePrimitiveType "Char") $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Char" ("C", mempty) + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (CannotRenamePrimitiveType "Char") $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Int" ("Int", mempty) + , iacDepsTypes = mempty + } + importFromApp p iac + let iac' = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Char" ("Int", mempty) + } + importFromApp p iac' + +unit_import_prim_type_ctor :: Assertion +unit_import_prim_type_ctor = do + runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") + , iacDepsTypes = mempty + } + importFromApp p iac + runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") + , iacDepsTypes = mempty + } + importFromApp p iac + let iac' = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") + } + importFromApp p iac' + +-- Cannot rewire a primitive type to a user-defined type of the same name (or vv) +unit_import_prim_user_type :: Assertion +unit_import_prim_user_type = do + runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef{astTypeDefName = "Char"}] + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + } + importFromApp p iac + runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do + p <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) + , iacDepsTypes = mempty + } + importFromApp p iac + let iac' = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + } + importFromApp p' iac' + where + p' = + newEmptyProg + { progTypes = [TypeDefAST unitDef{astTypeDefName = "Char"}] + } + +-- runs in an initially empty prog. you can add stuff monadically, I hope... not yet tried to use that feature +runImportTest :: EditAppM Assertion -> Assertion +runImportTest ma = case runEditAppM ma reallyEmptyApp of + (Left err, _) -> assertFailure $ "running actions failed! " <> show err + (Right a, _) -> a + +runImportTestError :: ImportError -> EditAppM () -> Assertion +runImportTestError expect ma = case runEditAppM ma reallyEmptyApp of + (Left err, _) -> err @?= ImportError expect + (Right _, _) -> assertFailure $ "running actions unexpectedly succeeded, expected " <> show expect + +reallyEmptyApp :: App +reallyEmptyApp = newEmptyApp & #appProg % #progDefs .~ mempty From 14409e35bd4dfa9db2be02afa1cdaa3a1ad6e2dc Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 12:24:00 +0000 Subject: [PATCH 06/12] Add unit fields to IAC The point of this trivial rejigging is to set up for importing terms (which will change these fields's type), so that commit will be less cluttered. --- primer/src/Primer/Import.hs | 2 + primer/test/Tests/Import.hs | 76 +++++++++++++++++++++++++++++++++++++ 2 files changed, 78 insertions(+) diff --git a/primer/src/Primer/Import.hs b/primer/src/Primer/Import.hs index 38e6284de..3a8968166 100644 --- a/primer/src/Primer/Import.hs +++ b/primer/src/Primer/Import.hs @@ -112,6 +112,8 @@ type TypeImportDetails = Map Name (Name, Map Name Name) data ImportActionConfig = IAC { iacImportRenamingTypes :: TypeImportDetails , iacDepsTypes :: TypeImportDetails + , iacImportRenamingTerms :: () + , iacDepsTerms :: () } -- | Computes the new program with a copy of the requested imports, diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index 5336ac6a2..11b60e222 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -86,6 +86,8 @@ unit_import_import_simple = runImportTest $ do IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg @@ -101,6 +103,8 @@ unit_import_import_renaming = runImportTest $ do IAC { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg @@ -124,6 +128,8 @@ unit_import_primitive = runImportTest $ do IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg @@ -143,6 +149,8 @@ unit_import_ctor_type = runImportTest $ do , ("List", ("List", Map.fromList [("Nil", "Nil"), ("Cons", "Cons")])) ] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg @@ -160,12 +168,16 @@ unit_import_rewire_deps = runImportTest $ do IAC { iacImportRenamingTypes = listRenaming , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac let iac' = IAC { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] , iacDepsTypes = listRenaming + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac' result <- gets appProg @@ -179,12 +191,16 @@ unit_import_rewire_primitive = runImportTest $ do IAC { iacImportRenamingTypes = Map.fromList [("Char", ("Char", mempty))] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac let iac' = IAC { iacImportRenamingTypes = Map.singleton "String" ("S", Map.fromList [("Empty", "Nil"), ("HeadAnd", "Cons")]) , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac' result <- gets appProg @@ -200,6 +216,8 @@ unit_import_ref_not_handled = runImportTestError (ReferencedTypeNotHandled "List IAC { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -211,6 +229,8 @@ unit_import_rewire_tgt_exist = runImportTestError (UnknownRewrittenTgtType "L") IAC { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] , iacDepsTypes = Map.singleton "List" ("L", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -223,6 +243,8 @@ unit_import_rewire_kind_match = runImportTestError (RewriteTypeKindMismatch "Lis IAC { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] , iacDepsTypes = Map.singleton "List" ("Unit", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -239,6 +261,8 @@ unit_import_name_clash = do , ("Rose", ("T", Map.fromList [("MkRose", "MkRose")])) ] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (DuplicateTypes ["Unit"]) $ do @@ -248,6 +272,8 @@ unit_import_name_clash = do IAC { iacImportRenamingTypes = Map.fromList [("T", ("Unit", Map.fromList [("A", "A"), ("B", "B")]))] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (DuplicateCtors ["C"]) $ do @@ -256,6 +282,8 @@ unit_import_name_clash = do IAC { iacImportRenamingTypes = Map.fromList [("T", ("S", Map.fromList [("A", "C"), ("B", "C")]))] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (DuplicateCtors ["MkUnit"]) $ do @@ -265,6 +293,8 @@ unit_import_name_clash = do IAC { iacImportRenamingTypes = Map.fromList [("T", ("S", Map.fromList [("A", "A"), ("B", "MkUnit")]))] , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac where @@ -295,6 +325,8 @@ unit_import_rewire_iso = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Unit" ("Nat", Map.singleton "MkUnit" "Zero") + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp newEmptyProg @@ -309,6 +341,8 @@ unit_import_rewire_iso = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "Nonexistent")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (RewriteCtorTgtNotExist "Unit" "Succ") $ do @@ -318,6 +352,8 @@ unit_import_rewire_iso = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Succ")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (DuplicateRewriteCtor "Nat" ["MkUnit"]) $ do @@ -327,6 +363,8 @@ unit_import_rewire_iso = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "MkUnit")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (RewrittenCtorTypeDiffers "Nat" "Succ" "Nat" "Zero") $ do @@ -336,6 +374,8 @@ unit_import_rewire_iso = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Succ"), ("Succ", "Zero")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -347,6 +387,8 @@ unit_import_import_rename_clash = runImportTestError (ImportRenameType "Nat") $ IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -359,6 +401,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = Map.singleton "Nonexistent" ("T", mempty) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (UnknownImportedCtor "Nat" "Nonexistent") $ do @@ -367,6 +411,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "C")]) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (MissedImportCtor "Nat" "Succ") $ do @@ -375,6 +421,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero")]) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (UnknownRewrittenSrcType "Nonexistent") $ do @@ -383,6 +431,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nonexistent" ("T", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (RewriteCtorSrcNotExist "Nat" "Nonexistent") $ do @@ -392,6 +442,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "C")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (RewriteCtorTgtNotExist "Unit" "Nonexistent") $ do @@ -401,6 +453,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Nonexistent")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (MissedRewriteCtor "Nat" "Succ") $ do @@ -410,6 +464,8 @@ unit_import_nonexist = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -424,6 +480,8 @@ unit_import_rewire_cross_type = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Nat" ("Unit", Map.fromList [("Zero", "MkUnit"), ("Succ", "Succ")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac @@ -436,6 +494,8 @@ unit_import_rename_prim_type = do IAC { iacImportRenamingTypes = Map.singleton "Char" ("C", mempty) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (CannotRenamePrimitiveType "Char") $ do @@ -444,12 +504,16 @@ unit_import_rename_prim_type = do IAC { iacImportRenamingTypes = Map.singleton "Int" ("Int", mempty) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac let iac' = IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Char" ("Int", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac' @@ -461,6 +525,8 @@ unit_import_prim_type_ctor = do IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do @@ -469,12 +535,16 @@ unit_import_prim_type_ctor = do IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac let iac' = IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac' @@ -488,6 +558,8 @@ unit_import_prim_user_type = do IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do @@ -496,12 +568,16 @@ unit_import_prim_user_type = do IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p iac let iac' = IAC { iacImportRenamingTypes = mempty , iacDepsTypes = Map.singleton "Char" ("Char", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty } importFromApp p' iac' where From e763d461604b586bdef53d7505da1a354bd46b07 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 12:24:05 +0000 Subject: [PATCH 07/12] Add some (ignored) terms to {primS,s}rcProg Similarly to the previous commit, set up for tests of importing terms. We need to return the ID of the new definitions, but this requires lots of knock-on changes in the tests. We do those now rather than in the commit that adds the ability to import terms. --- primer/src/Primer/Typecheck.hs | 6 ++ primer/test/Tests/Import.hs | 136 ++++++++++++++++++++++++--------- 2 files changed, 108 insertions(+), 34 deletions(-) diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index caa198e36..f7c9e621a 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -44,6 +44,7 @@ module Primer.Typecheck ( lookupLocal, primConInScope, mkTypeDefMap, + mkDefMap, consistentKinds, consistentTypes, extendLocalCxtTy, @@ -223,6 +224,11 @@ buildTypingContext tydefs defs sh = mkTypeDefMap :: [TypeDef] -> Map Name TypeDef mkTypeDefMap defs = M.fromList $ map (\d -> (typeDefName d, d)) defs +-- | Create a mapping of ID to Def for fast lookup. +-- Helpful for use with 'buildTypingContext' +mkDefMap :: [Def] -> Map ID Def +mkDefMap = Map.fromList . map (\d -> (defID d, d)) + -- | A shorthand for the constraints needed when typechecking type TypeM e m = ( Monad m diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index 11b60e222..653b928ee 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -8,8 +8,10 @@ import Foreword import Optics import Primer.App import Primer.Core +import Primer.Core.DSL import Primer.Name -import Primer.Primitives (allPrimTypeDefs) +import Primer.Primitives (allPrimDefs, allPrimTypeDefs) +import Primer.Typecheck (mkDefMap) import Test.Tasty.HUnit unitDef :: ASTTypeDef @@ -21,13 +23,52 @@ unitDef = , astTypeDefNameHints = [] } -srcProg :: (Applicative m) => m Prog -srcProg = +srcProg :: (MonadFresh ID m) => m (Prog, ID, ID) +srcProg = do + plusId <- fresh + plusType <- tcon "Nat" `tfun` (tcon "Nat" `tfun` tcon "Nat") + plusExpr <- + lam "x" $ + lam "y" $ + case_ + (var "y") + [ branch "Zero" [] $ var "x" + , branch "Succ" [("z", Nothing)] $ + con "Succ" `app` (global plusId `app` var "x" `app` var "z") + ] + let plus = + ASTDef + { astDefID = plusId + , astDefName = "plus" + , astDefType = plusType + , astDefExpr = plusExpr + } + multId <- fresh + multType <- tcon "Nat" `tfun` (tcon "Nat" `tfun` tcon "Nat") + multExpr <- + lam "x" $ + lam "y" $ + case_ + (var "y") + [ branch "Zero" [] $ con "Zero" + , branch "Succ" [("z", Nothing)] $ + global plusId `app` var "x" `app` (global multId `app` var "x" `app` var "y") + ] + let mult = + ASTDef + { astDefID = multId + , astDefName = "mult" + , astDefType = multType + , astDefExpr = multExpr + } pure - newEmptyProg + ( newEmptyProg { progTypes = [TypeDefAST natDef] - , progDefs = mempty + , progDefs = mkDefMap $ DefAST <$> [plus, mult] } + , plusId + , multId + ) srcProg2 :: (MonadFresh ID m) => (Name, Name, Name) -> (Name, Name) -> m Prog srcProg2 (listName, nilName, consName) (roseTyName, roseConName) = do @@ -60,14 +101,41 @@ srcProg2 (listName, nilName, consName) (roseTyName, roseConName) = do , progDefs = mempty } --- A program with all primitive types --- and also String (which depends on "Char") -primSrcProg :: Applicative m => m Prog -primSrcProg = +-- A program with all primitive types and definitions, +-- along with a map of primitive-definition-name to primitive-definition-id +-- and the id of one non-primitive def, that depends on +-- primitive types "Char" and terms "eqChar", "toUpper" +-- and also Bool and String (which depends on "Char") +primSrcProg :: (MonadFresh ID m) => m (Prog, Map Name ID, ID) +primSrcProg = do + primGlobals <- for (Map.toList allPrimDefs) $ \(n, f) -> do + i <- fresh + t <- primFunType f + pure (t, n, i) + let (primNames, primMap) = flip foldMap primGlobals $ \(t, n, i) -> + (Map.singleton n i, Map.singleton i $ DefPrim $ PrimDef i n t) + wrapperId <- fresh + wrapperType <- tcon "Char" `tfun` tcon "Bool" + wrapperExpr <- + lam "x" $ + global (primNames Map.! "eqChar") + `app` (global (primNames Map.! "toUpper") `app` var "x") + `app` char 'a' + let wrapper = + ASTDef + { astDefID = wrapperId + , astDefName = "wrappedPrim" + , astDefType = wrapperType + , astDefExpr = wrapperExpr + } pure - newEmptyProg - { progTypes = map TypeDefAST [stringDef] <> map TypeDefPrim (Map.elems allPrimTypeDefs) + ( newEmptyProg + { progTypes = map TypeDefAST [boolDef, stringDef] <> map TypeDefPrim (Map.elems allPrimTypeDefs) + , progDefs = primMap <> Map.singleton wrapperId (DefAST wrapper) } + , primNames + , wrapperId + ) where stringDef :: ASTTypeDef stringDef = @@ -81,7 +149,7 @@ primSrcProg = -- Import without renaming works unit_import_import_simple :: Assertion unit_import_import_simple = runImportTest $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) @@ -98,7 +166,7 @@ unit_import_import_simple = runImportTest $ do -- We can rename types and ctors when importing unit_import_import_renaming :: Assertion unit_import_import_renaming = runImportTest $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) @@ -123,7 +191,7 @@ unit_import_import_renaming = runImportTest $ do -- Importing and renaming primitives works unit_import_primitive :: Assertion unit_import_primitive = runImportTest $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) @@ -186,7 +254,7 @@ unit_import_rewire_deps = runImportTest $ do unit_import_rewire_primitive :: Assertion unit_import_rewire_primitive = runImportTest $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.fromList [("Char", ("Char", mempty))] @@ -336,7 +404,7 @@ unit_import_rewire_iso = do iac runImportTestError (RewriteCtorSrcNotExist "Nat" "Nonexistent") $ do _ <- handleMutationRequest $ Edit [AddTypeDef natDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -347,7 +415,7 @@ unit_import_rewire_iso = do importFromApp p iac runImportTestError (RewriteCtorTgtNotExist "Unit" "Succ") $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -358,7 +426,7 @@ unit_import_rewire_iso = do importFromApp p iac runImportTestError (DuplicateRewriteCtor "Nat" ["MkUnit"]) $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -369,7 +437,7 @@ unit_import_rewire_iso = do importFromApp p iac runImportTestError (RewrittenCtorTypeDiffers "Nat" "Succ" "Nat" "Zero") $ do _ <- handleMutationRequest $ Edit [AddTypeDef natDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -382,7 +450,7 @@ unit_import_rewire_iso = do -- cannot both import and rename the same type unit_import_import_rename_clash :: Assertion unit_import_import_rename_clash = runImportTestError (ImportRenameType "Nat") $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) @@ -396,7 +464,7 @@ unit_import_import_rename_clash = runImportTestError (ImportRenameType "Nat") $ unit_import_nonexist :: Assertion unit_import_nonexist = do runImportTestError (UnknownImportedType "Nonexistent") $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nonexistent" ("T", mempty) @@ -406,7 +474,7 @@ unit_import_nonexist = do } importFromApp p iac runImportTestError (UnknownImportedCtor "Nat" "Nonexistent") $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ"), ("Nonexistent", "C")]) @@ -416,7 +484,7 @@ unit_import_nonexist = do } importFromApp p iac runImportTestError (MissedImportCtor "Nat" "Succ") $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero")]) @@ -426,7 +494,7 @@ unit_import_nonexist = do } importFromApp p iac runImportTestError (UnknownRewrittenSrcType "Nonexistent") $ do - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -437,7 +505,7 @@ unit_import_nonexist = do importFromApp p iac runImportTestError (RewriteCtorSrcNotExist "Nat" "Nonexistent") $ do _ <- handleMutationRequest $ Edit [AddTypeDef natDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -448,7 +516,7 @@ unit_import_nonexist = do importFromApp p iac runImportTestError (RewriteCtorTgtNotExist "Unit" "Nonexistent") $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -459,7 +527,7 @@ unit_import_nonexist = do importFromApp p iac runImportTestError (MissedRewriteCtor "Nat" "Succ") $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -475,7 +543,7 @@ unit_import_rewire_cross_type :: Assertion unit_import_rewire_cross_type = do runImportTestError (RewriteCtorTgtNotExist "Unit" "Succ") $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg + (p, _, _) <- srcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -489,7 +557,7 @@ unit_import_rewire_cross_type = do unit_import_rename_prim_type :: Assertion unit_import_rename_prim_type = do runImportTestError (CannotRenamePrimitiveType "Char") $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Char" ("C", mempty) @@ -499,7 +567,7 @@ unit_import_rename_prim_type = do } importFromApp p iac runImportTestError (CannotRenamePrimitiveType "Char") $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Int" ("Int", mempty) @@ -520,7 +588,7 @@ unit_import_rename_prim_type = do unit_import_prim_type_ctor :: Assertion unit_import_prim_type_ctor = do runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") @@ -530,7 +598,7 @@ unit_import_prim_type_ctor = do } importFromApp p iac runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", Map.singleton "a" "a") @@ -553,7 +621,7 @@ unit_import_prim_user_type :: Assertion unit_import_prim_user_type = do runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do _ <- handleMutationRequest $ Edit [AddTypeDef unitDef{astTypeDefName = "Char"}] - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = mempty @@ -563,7 +631,7 @@ unit_import_prim_user_type = do } importFromApp p iac runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do - p <- primSrcProg + (p, _, _) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) From 67c7641e5a47674d5959370fcc4ee459d743b5ec Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 20:35:24 +0000 Subject: [PATCH 08/12] feat: Support importing (i.e. copying the definiton) terms --- primer/src/Primer/Core.hs | 22 +++ primer/src/Primer/Core/Utils.hs | 39 ++++- primer/src/Primer/Import.hs | 202 ++++++++++++++++++++++---- primer/test/Tests/Import.hs | 246 ++++++++++++++++++++++++-------- 4 files changed, 424 insertions(+), 85 deletions(-) diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index 622574875..00f6bf10d 100644 --- a/primer/src/Primer/Core.hs +++ b/primer/src/Primer/Core.hs @@ -13,8 +13,11 @@ module Primer.Core ( CaseBranch, CaseBranch' (..), Def (..), + _defID, defID, + _defName, defName, + _defType, defType, ASTDef (..), defAST, @@ -348,6 +351,25 @@ data ASTDef = ASTDef deriving (Eq, Show, Generic) deriving (FromJSON, ToJSON) via VJSON ASTDef +defLens :: Lens' PrimDef a -> Lens' ASTDef a -> Lens' Def a +defLens lp la = lens getter setter + where + getter = \case + DefPrim d -> view lp d + DefAST d -> view la d + setter = \case + DefPrim d -> DefPrim . flip (set lp) d + DefAST d -> DefAST . flip (set la) d + +_defID :: Lens' Def ID +_defID = defLens #primDefID #astDefID + +_defName :: Lens' Def Name +_defName = defLens #primDefName #astDefName + +_defType :: Lens' Def Type +_defType = defLens #primDefType #astDefType + defID :: Def -> ID defID = \case DefPrim d -> primDefID d diff --git a/primer/src/Primer/Core/Utils.hs b/primer/src/Primer/Core/Utils.hs index a1b73ef9b..d24f68353 100644 --- a/primer/src/Primer/Core/Utils.hs +++ b/primer/src/Primer/Core/Utils.hs @@ -1,9 +1,13 @@ +{-# LANGUAGE OverloadedLabels #-} + module Primer.Core.Utils ( generateTypeIDs, forgetTypeIDs, generateIDs, forgetIDs, noHoles, + noHolesTm, + _exprTypeChildren, _freeTmVars, _freeTyVars, _freeVars, @@ -22,7 +26,24 @@ import Data.Generics.Uniplate.Data (universe) import qualified Data.Map.Strict as M import qualified Data.Set as S import Data.Set.Optics (setOf) -import Optics (Fold, Traversal, getting, hasn't, set, summing, to, traversalVL, traverseOf, (%), _2) +import Optics ( + Field3 (_3), + Field4 (_4), + Fold, + Traversal, + Traversal', + adjoin, + allOf, + getting, + hasn't, + set, + summing, + to, + traversalVL, + traverseOf, + (%), + _2, + ) import Primer.Core ( CaseBranch' (..), Expr, @@ -67,6 +88,22 @@ noHoles t = flip all (universe t) $ \case _ -> True _ -> True +-- | The immediate 'Type' children of an 'Expr' +_exprTypeChildren :: Traversal' (Expr' a b) (Type' b) +_exprTypeChildren = + #_Ann % _3 + `adjoin` (#_APP % _3) + `adjoin` (#_Letrec % _4) + `adjoin` (#_LetType % _3) + +-- | Test whether an term contains any holes +-- (empty or non-empty, or inside a type) +noHolesTm :: (Data a, Data b) => Expr' a b -> Bool +noHolesTm e = flip all (universe e) $ \case + EmptyHole{} -> False + Hole{} -> False + n -> allOf _exprTypeChildren noHoles n + freeVarsTy :: Type' a -> Set Name freeVarsTy = setOf (getting _freeVarsTy % _2) diff --git a/primer/src/Primer/Import.hs b/primer/src/Primer/Import.hs index 3a8968166..6aba5896f 100644 --- a/primer/src/Primer/Import.hs +++ b/primer/src/Primer/Import.hs @@ -7,7 +7,9 @@ module Primer.Import ( ImportActionConfig (..), ) where +import Control.Monad.Fresh (MonadFresh (fresh)) import Control.Monad.NestedError (MonadNestedError (throwError')) +import Data.Data (Data) import Data.Generics.Uniplate.Data (transformM) import qualified Data.Map.Strict as Map import qualified Data.Set as Set @@ -23,33 +25,53 @@ import Optics ( ) import Primer.App.Core ( App (appProg), - Prog (progTypes), + Prog (progDefs, progTypes), ) import Primer.Core ( + Def, + Expr, + ID, + Meta, Type', TypeDef, ValCon (valConArgs, valConName), + astDefExpr, astTypeDefConstructors, + defName, + defType, typeDefAST, typeDefKind, typeDefName, + _defID, + _defName, + _defType, + _exprMetaLens, + _id, + _type, _typeDefName, + _typeMetaLens, ) -import Primer.Core.Utils (alphaEqTy) +import Primer.Core.Utils (alphaEqTy, forgetTypeIDs, _exprTypeChildren) import Primer.JSON import Primer.Name (Name) -import Primer.Typecheck (mkTypeDefMap) +import Primer.Typecheck (mkDefMap, mkTypeDefMap) import Primer.Utils (distinct') data ImportError = -- | Cannot both import and rename a type ImportRenameType Name + | -- | Cannot both import and rename a term + ImportRenameTerm Name | -- | Cannot import two types under the same name, or something that clashes with an existing type DuplicateTypes [Name] + | -- | Cannot import two terms under the same name, or something that clashes with an existing term + DuplicateTerm [Name] | -- | Cannot import two ctors under the same name, or something that clashes with an existing ctors DuplicateCtors [Name] | -- | Cannot import something that does not exist UnknownImportedType Name + | -- | Cannot import something that does not exist + UnknownImportedTerm ID | -- | Cannot import something that does not exist (args: an imported type, and its non-existent constructor) UnknownImportedCtor Name Name | -- | We cannot currently rename primitive types (as the types of primitive constructors are @@ -63,10 +85,16 @@ data ImportError UnknownRewrittenSrcType Name | -- | Cannot rewrite into a type that does not exist UnknownRewrittenTgtType Name + | -- | Cannot rewrite a dep which does not exist (although, since it cannot be referred to, nothing would go wrong if we allowed it...) + UnknownRewrittenSrcTerm ID + | -- | Cannot rewrite into a term that does not exist + UnknownRewrittenTgtTerm ID | -- | Tried to rewrite the first arg to the second, but they are of different kinds RewriteTypeKindMismatch Name Name | -- | Tried to rewrite a primitive to a non-primitive, or vice versa RewriteTypePrimitiveMismatch Name Name + | -- | Tried to rewrite the first arg to the second, but they are of different types + RewriteTermTypeMismatch ID ID | -- | Must rewrite all constructors of any rewritten type: args are type its (first) ctor that were missed MissedRewriteCtor Name Name | -- | In a rewritten type (first arg), cannot rewrite two ctors to the same thing (second arg) @@ -79,6 +107,10 @@ data ImportError RewriteCtorTgtNotExist Name Name | -- | This type was referenced in the source, but we have neither imported it nor rewritten it ReferencedTypeNotHandled Name + | -- | This constructor was referenced in the source, but we have neither imported it nor rewritten it + ReferencedConstructorNotHandled Name + | -- | This global was referenced in the source, but we have neither imported it nor rewritten it + ReferencedGlobalNotHandled ID | -- | @RewrittenCtorTypeDiffers ty1 con1 ty2 con2@: we tried to rewrite @ty1@ into @ty2@, mapping @con1@ to @con2@, but their types do not match RewrittenCtorTypeDiffers Name Name Name Name deriving (Eq, Show, Generic) @@ -98,6 +130,7 @@ type TypeImportDetails = Map Name (Name, Map Name Name) -- The values of the iacImport* maps must be free (type/term names) in the current App -- For types, the fst of the value must be free, and the snd map must be -- keys are exactly the ctors of the type in 'A', values are free constructor names +-- Terms are similar, but simpler as they don't have any analogue to "constructor" -- The keys of iacDeps* must cover all free vars of the defs in 'A' named by iacImport* -- For types, the constructor map must be a bijection -- The values of iacDeps* must exist in the current App, and have the same Kind/Type (after substituting types according to iacDeps) as the key does. @@ -112,8 +145,8 @@ type TypeImportDetails = Map Name (Name, Map Name Name) data ImportActionConfig = IAC { iacImportRenamingTypes :: TypeImportDetails , iacDepsTypes :: TypeImportDetails - , iacImportRenamingTerms :: () - , iacDepsTerms :: () + , iacImportRenamingTerms :: Map ID Name + , iacDepsTerms :: Map ID ID } -- | Computes the new program with a copy of the requested imports, @@ -122,16 +155,19 @@ data ImportActionConfig = IAC -- See 'App.importFromApp' for a version that typechecks and updates an App -- state. importFromApp' :: - (MonadNestedError ImportError e m, MonadReader App m) => + (MonadNestedError ImportError e m, MonadReader App m, MonadFresh ID m) => Prog -> ImportActionConfig -> m Prog importFromApp' srcProg iac = do curProg <- asks appProg - newTypeDefs <- getImportTypesFromApp curProg (srcProg, iac) - pure $ curProg & #progTypes %~ (++ newTypeDefs) + (newTypeDefs, typeRenaming, ctorRenaming) <- getImportTypesFromApp curProg (srcProg, iac) + newTerms <- getImportTermsFromApp curProg (srcProg, iac) typeRenaming ctorRenaming + pure $ + curProg & #progTypes %~ (++ newTypeDefs) + & #progDefs %~ (<> mkDefMap newTerms) -getImportTypesFromApp :: forall m e. MonadNestedError ImportError e m => Prog -> (Prog, ImportActionConfig) -> m [TypeDef] +getImportTypesFromApp :: forall m e. MonadNestedError ImportError e m => Prog -> (Prog, ImportActionConfig) -> m ([TypeDef], Map Name Name, Map Name Name) getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes}) = {- We check requirements, to give nice error messages, rather than "typechecker says no" - Things need to exist in srcProg: @@ -168,7 +204,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes -- make renaming map, and grab the typedefs, with the new type/ctor name. NB: the argument types still need rewriting! let srcTypes = mkTypeDefMap $ progTypes srcProg - (tyrn1, _ctorrn1, tydefs) <- getAp $ + (tyrn1, ctorrn1, tydefs) <- getAp $ flip Map.foldMapWithKey iacImportRenamingTypes $ \srcTyName (tgtTyName, ctorMap) -> Ap $ do -- imported type exists in srcProg srcTy <- @@ -201,7 +237,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes -- renaming map for deps rewriting let curTypes = mkTypeDefMap $ progTypes curProg - (tyrn2, _ctorrn2, toCheckRewriteCtorsTypes) <- getAp $ + (tyrn2, ctorrn2, toCheckRewriteCtorsTypes) <- getAp $ flip Map.foldMapWithKey iacDepsTypes $ \srcTyName (tgtTyName, ctorMap) -> Ap $ do -- the rewritten thing must exist in the imported program -- (nothing would go wrong if we elided this check, but it catches @@ -271,14 +307,11 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes -- everywhere we see a 'TCon', replace it with its image in the 'tyrn' map -- (We throw an error if they do not exist in our -- renaming map, i.e. the imported types, or the rewritten deps) - let rewriteTCons :: Type' () -> m (Type' ()) - rewriteTCons = transformM $ - traverseOf tconName $ \tc -> - lookupOrThrow tc tyrn $ ReferencedTypeNotHandled tc + let rewriteTCons' = rewriteTCons tyrn pure -- Now check that rewritten constructors have the same type for_ toCheckRewriteCtorsTypes $ \(srcTy, srcCtor, tgtTy, tgtCtor) -> do - srcCtorArgs <- traverse rewriteTCons $ valConArgs srcCtor + srcCtorArgs <- traverse rewriteTCons' $ valConArgs srcCtor let tgtCtorArgs = valConArgs tgtCtor unless ( length srcCtorArgs == length tgtCtorArgs @@ -292,15 +325,134 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes (valConName tgtCtor) -- Rename the types referenced. These are now ready to insert into curProg + rejiggedTypeDefs <- + traverseOf + (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed) + rewriteTCons' + tydefs + + pure (rejiggedTypeDefs, tyrn, ctorrn1 <> ctorrn2) + +lookupOrThrow :: + (MonadNestedError ImportError e m, Ord k) => + k -> + Map k v -> + ImportError -> + m v +lookupOrThrow k m e = case m Map.!? k of + Nothing -> throwError' e + Just v -> pure v + +-- Rename the types referenced: +-- everywhere we see a 'TCon', replace it with its image in the 'tyrn' map +-- (We throw an error if they do not exist in our +-- renaming map, i.e. the imported types, or the rewritten deps) +-- We also modify the metadata at each node +rewriteTCons :: + (Data a, MonadNestedError ImportError e m) => + Map Name Name -> + (a -> m a) -> + Type' a -> + m (Type' a) +rewriteTCons tyrn f = + transformM $ traverseOf - (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed) - rewriteTCons - tydefs + tconName + ( \tc -> + lookupOrThrow tc tyrn $ ReferencedTypeNotHandled tc + ) + <=< traverseOf _typeMetaLens f where - lookupOrThrow :: Ord k => k -> Map k v -> ImportError -> m v - lookupOrThrow k m e = case m Map.!? k of - Nothing -> throwError' e - Just v -> pure v - - tconName :: AffineTraversal' (Type' ()) Name + tconName :: AffineTraversal' (Type' a) Name tconName = #_TCon % _2 + +getImportTermsFromApp :: + forall m e. + (MonadFresh ID m, MonadNestedError ImportError e m) => + Prog -> + (Prog, ImportActionConfig) -> + Map Name Name -> + Map Name Name -> + m [Def] +getImportTermsFromApp curProg (srcProg, IAC{iacImportRenamingTerms, iacDepsTerms}) tconRename conRename = do + {- We need that: + - created terms are freshly named + (this is not necessary for the typechecker, as globals are referred to by ID, + and we will create fresh IDs, but we include it for consistency with manually + allowed actions, which forbid creating two definitions with the same name) + - rewritten deps exist in curProg, and have the correct type + - created and rewritten things exist in srcProg (and are all distinct) + - all referenced things (global terms,types,constructors) are + - either imported or rewritten for terms + - covered in the tconRename and conRename maps for types and constructors respectively + If we have those properties, the typechecker should not complain. + We explicitly check them so we get nicer error messages than we would get from the typechecker + -} + -- Not allowed to both import and dep-rename some type + for_ (Map.intersection iacImportRenamingTerms iacDepsTerms) $ throwError' . ImportRenameTerm + + -- things we create have distinct names, and don't appear in curProg + let created = Map.elems iacImportRenamingTerms + let extant = fmap defName $ Map.elems $ progDefs curProg + case distinct' $ created ++ extant of + Left dups -> throwError' $ DuplicateTerm dups + Right _ -> pure () + + -- Create renaming map for imported terms, and grab the defs and its new name + (rn1, toImport) <- getAp $ + flip Map.foldMapWithKey iacImportRenamingTerms $ \srcID tgtName -> Ap $ do + -- imported type exists in srcProg + srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownImportedTerm srcID + newID <- fresh + pure + ( Map.singleton srcID newID + , [(srcDef, newID, tgtName)] + ) + + -- Create renaming map for rewritten dependencies + rn2 <- getAp $ + flip Map.foldMapWithKey iacDepsTerms $ \srcID tgtID -> Ap $ do + -- the rewritten thing must exist in the imported program + -- (nothing would go wrong if we elided this check, but it catches + -- that our caller is broken) + srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownRewrittenSrcTerm srcID + -- We must rewrite it to an existing term ... + tgtDef <- lookupOrThrow tgtID (progDefs curProg) $ UnknownRewrittenTgtTerm tgtID + -- ... of the same type (taking into account the renaming of types) + srcType' <- rewriteTCons tconRename pure $ forgetTypeIDs $ defType srcDef + unless (srcType' `alphaEqTy` forgetTypeIDs (defType tgtDef)) $ throwError' $ RewriteTermTypeMismatch srcID tgtID + + pure $ Map.singleton srcID tgtID + + let globalRename = rn1 <> rn2 + + -- Rename the referenced globals,constructors and types. + -- These are now ready to be inserted into curProg + for toImport $ \(def, newID, newName) -> do + let rejigMeta :: Meta (Maybe a) -> m (Meta (Maybe a)) + rejigMeta m = + m & _type .~ Nothing + & traverseOf _id (const fresh) + rejigType = rewriteTCons tconRename rejigMeta + def' <- traverseOf _defType rejigType def + let rejigExpr :: Expr -> m Expr + rejigExpr = + transformM $ + traverseOf + (#_GlobalVar % _2) + ( \origGlobal -> + lookupOrThrow origGlobal globalRename $ + ReferencedGlobalNotHandled origGlobal + ) + <=< traverseOf + (#_Con % _2) + ( \origCon -> + lookupOrThrow origCon conRename $ + ReferencedConstructorNotHandled origCon + ) + <=< traverseOf _exprTypeChildren rejigType + <=< traverseOf _exprMetaLens rejigMeta + def'' <- traverseOf (#_DefAST % #astDefExpr) rejigExpr def' + pure $ + def'' & _defID .~ newID + & _defName .~ newName diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index 653b928ee..2f0a73a06 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -9,6 +9,7 @@ import Optics import Primer.App import Primer.Core import Primer.Core.DSL +import Primer.Core.Utils (noHoles, noHolesTm) import Primer.Name import Primer.Primitives (allPrimDefs, allPrimTypeDefs) import Primer.Typecheck (mkDefMap) @@ -149,19 +150,31 @@ primSrcProg = do -- Import without renaming works unit_import_import_simple :: Assertion unit_import_import_simple = runImportTest $ do - (p, _, _) <- srcProg + (p, plusID, _) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) , iacDepsTypes = mempty - , iacImportRenamingTerms = mempty + , iacImportRenamingTerms = Map.singleton plusID "plus" , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg return $ do progTypes result @?= progTypes p - progDefs result @?= mempty + -- It is difficult to say exactly what the imported terms are without + -- basically doing the import-renaming again. We instead just check + -- we have the expected definitions, and they do not contain any holes + -- (as one may worry would happen if they were imported badly, and then + -- smartholes kicked in) + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["plus"] + +holeFree :: Def -> Bool +holeFree def = + noHoles (defType def) + && maybe True noHolesTm (def ^? #_DefAST % #astDefExpr) -- We can rename types and ctors when importing unit_import_import_renaming :: Assertion @@ -191,19 +204,25 @@ unit_import_import_renaming = runImportTest $ do -- Importing and renaming primitives works unit_import_primitive :: Assertion unit_import_primitive = runImportTest $ do - (p, _, _) <- primSrcProg + (p, prims, fooId) <- primSrcProg let iac = IAC - { iacImportRenamingTypes = Map.singleton "Char" ("Char", mempty) + { iacImportRenamingTypes = + Map.fromList + [ ("Char", ("Char", mempty)) + , ("Bool", ("B", Map.fromList [("True", "tt"), ("False", "ff")])) + ] , iacDepsTypes = mempty - , iacImportRenamingTerms = mempty + , iacImportRenamingTerms = Map.fromList [(prims Map.! "toUpper", "UPPER"), (prims Map.! "eqChar", "=="), (fooId, "foo")] , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg return $ do - map typeDefName (progTypes result) @?= ["Char"] - progDefs result @?= mempty + map typeDefName (progTypes result) @?= ["B", "Char"] + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["==", "UPPER", "foo"] -- test deep subst in ctor types unit_import_ctor_type :: Assertion @@ -254,69 +273,124 @@ unit_import_rewire_deps = runImportTest $ do unit_import_rewire_primitive :: Assertion unit_import_rewire_primitive = runImportTest $ do - (p, _, _) <- primSrcProg + (p, prims, fooId) <- primSrcProg let iac = IAC { iacImportRenamingTypes = Map.fromList [("Char", ("Char", mempty))] , iacDepsTypes = mempty - , iacImportRenamingTerms = mempty + , iacImportRenamingTerms = Map.fromList [(prims Map.! "toUpper", "UPPER")] , iacDepsTerms = mempty } importFromApp p iac + upperId <- gets $ defID . unsafeHead . filter ((== "UPPER") . defName) . Map.elems . progDefs . appProg let iac' = IAC - { iacImportRenamingTypes = Map.singleton "String" ("S", Map.fromList [("Empty", "Nil"), ("HeadAnd", "Cons")]) + { iacImportRenamingTypes = + Map.fromList + [ ("Bool", ("B", Map.fromList [("True", "tt"), ("False", "ff")])) + , ("String", ("S", Map.fromList [("Empty", "Nil"), ("HeadAnd", "Cons")])) + ] , iacDepsTypes = Map.singleton "Char" ("Char", mempty) - , iacImportRenamingTerms = mempty - , iacDepsTerms = mempty + , iacImportRenamingTerms = Map.fromList [(prims Map.! "eqChar", "=="), (fooId, "foo")] + , iacDepsTerms = Map.singleton (prims Map.! "toUpper") upperId } importFromApp p iac' result <- gets appProg return $ do - map typeDefName (progTypes result) @?= ["Char", "S"] - progDefs result @?= mempty + map typeDefName (progTypes result) @?= ["Char", "B", "S"] + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["UPPER", "==", "foo"] -- cannot import without deps unit_import_ref_not_handled :: Assertion -unit_import_ref_not_handled = runImportTestError (ReferencedTypeNotHandled "List") $ do - p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") - let iac = - IAC - { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] - , iacDepsTypes = mempty - , iacImportRenamingTerms = mempty - , iacDepsTerms = mempty - } - importFromApp p iac +unit_import_ref_not_handled = do + runImportTestError (ReferencedTypeNotHandled "List") $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (ReferencedTypeNotHandled "Nat") $ do + (p, plusId, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton plusId "plus" + , iacDepsTerms = mempty + } + importFromApp p iac + -- The '3' here is _plusId, which is hardcoded as it is not in scope + -- This may be fragile! + runImportTestError (ReferencedGlobalNotHandled 3) $ do + (p, _plusId, multId) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton multId "mult" + , iacDepsTerms = mempty + } + importFromApp p iac -- cannot claim to support deps with free name unit_import_rewire_tgt_exist :: Assertion -unit_import_rewire_tgt_exist = runImportTestError (UnknownRewrittenTgtType "L") $ do - p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") - let iac = - IAC - { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] - , iacDepsTypes = Map.singleton "List" ("L", mempty) - , iacImportRenamingTerms = mempty - , iacDepsTerms = mempty - } - importFromApp p iac +unit_import_rewire_tgt_exist = do + runImportTestError (UnknownRewrittenTgtType "L") $ do + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = Map.singleton "List" ("L", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (UnknownRewrittenTgtTerm 0) $ do + (p, plusId, multId) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton multId "mult" + , iacDepsTerms = Map.singleton plusId 0 + } + importFromApp p iac -- cannot claim to support deps with wrong kind unit_import_rewire_kind_match :: Assertion -unit_import_rewire_kind_match = runImportTestError (RewriteTypeKindMismatch "List" "Unit") $ do - _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] - p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") - let iac = - IAC - { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] - , iacDepsTypes = Map.singleton "List" ("Unit", mempty) - , iacImportRenamingTerms = mempty - , iacDepsTerms = mempty - } - importFromApp p iac +unit_import_rewire_kind_match = do + runImportTestError (RewriteTypeKindMismatch "List" "Unit") $ do + _ <- handleMutationRequest $ Edit [AddTypeDef unitDef] + p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Rose", ("T", Map.fromList [("MkRose", "C")]))] + , iacDepsTypes = Map.singleton "List" ("Unit", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + -- 3 is plusId, 43 is fooId. Hardcoded as not in scope. These may be fragile + runImportTestError (RewriteTermTypeMismatch 3 43) $ do + (p, plusId, multId) <- srcProg + _ <- handleMutationRequest $ Edit [CreateDef $ Just "foo"] + fooId <- gets $ defID . unsafeHead . filter ((== "foo") . defName) . Map.elems . progDefs . appProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton multId "times" + , iacDepsTerms = Map.singleton plusId fooId + } + importFromApp p iac --- cannot import two types/ctors with the same name, or one the same as an existing one +-- cannot import two types/ctors/terms with the same name, or one the same as an existing one unit_import_name_clash :: Assertion unit_import_name_clash = do runImportTestError (DuplicateTypes ["T"]) $ do @@ -365,6 +439,27 @@ unit_import_name_clash = do , iacDepsTerms = mempty } importFromApp p iac + runImportTestError (DuplicateTerm ["f"]) $ do + (p, plusId, multId) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.fromList [(plusId, "f"), (multId, "f")] + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (DuplicateTerm ["f"]) $ do + _ <- handleEditRequest [CreateDef $ Just "f"] + (p, plusId, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.fromList [(plusId, "f")] + , iacDepsTerms = mempty + } + importFromApp p iac where p' :: (MonadFresh ID m) => m Prog p' = do @@ -447,20 +542,33 @@ unit_import_rewire_iso = do } importFromApp p iac --- cannot both import and rename the same type +-- cannot both import and rename the same type/term unit_import_import_rename_clash :: Assertion -unit_import_import_rename_clash = runImportTestError (ImportRenameType "Nat") $ do - (p, _, _) <- srcProg - let iac = - IAC - { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) - , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) - , iacImportRenamingTerms = mempty - , iacDepsTerms = mempty - } - importFromApp p iac +unit_import_import_rename_clash = do + runImportTestError (ImportRenameType "Nat") $ do + (p, _, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (ImportRenameTerm "f") $ do + _ <- handleEditRequest [CreateDef Nothing] + fId <- gets $ fst . Map.findMin . progDefs . appProg + (p, plusId, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton plusId "f" + , iacDepsTerms = Map.singleton plusId fId + } + importFromApp p iac --- cannot import/rewrite nonexistent type/ctor, and have to import/rewrite all ctors of a type +-- cannot import/rewrite nonexistent type/ctor/term, and have to import/rewrite all ctors of a type unit_import_nonexist :: Assertion unit_import_nonexist = do runImportTestError (UnknownImportedType "Nonexistent") $ do @@ -536,6 +644,26 @@ unit_import_nonexist = do , iacDepsTerms = mempty } importFromApp p iac + runImportTestError (UnknownImportedTerm 0) $ do + (p, _, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton 0 "foo" + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (UnknownRewrittenSrcTerm 0) $ do + (p, _, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = mempty + , iacImportRenamingTerms = mempty + , iacDepsTerms = Map.singleton 0 0 + } + importFromApp p iac -- Cannot rewrite a ctor to ctor of different type -- this will hit "unknown ctor" error From 50adfaa9145458fddf2ed3e3aac9e18347543eba Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 12:11:16 +0000 Subject: [PATCH 09/12] test that universe and transform are "deep" I.e. that they look through explicit mutual recursion. When implementing importing terms, I worried whether these combinators would recuse into branches of a case expression, as that requires going from an Expr to a CaseBranch back to an Expr, and we very much need to replace names inside branches. These functions do indeed recurse into and out of other mutually recursive types in this manner. --- primer/primer.cabal | 1 + primer/test/Tests/Uniplate.hs | 26 ++++++++++++++++++++++++++ 2 files changed, 27 insertions(+) create mode 100644 primer/test/Tests/Uniplate.hs diff --git a/primer/primer.cabal b/primer/primer.cabal index 1d43cea8e..ac52a18a0 100644 --- a/primer/primer.cabal +++ b/primer/primer.cabal @@ -116,6 +116,7 @@ test-suite primer-test Tests.Transform Tests.Typecheck Tests.Unification + Tests.Uniplate Tests.Zipper Tests.Zipper.BindersAbove TestUtils diff --git a/primer/test/Tests/Uniplate.hs b/primer/test/Tests/Uniplate.hs new file mode 100644 index 000000000..ff9401c4f --- /dev/null +++ b/primer/test/Tests/Uniplate.hs @@ -0,0 +1,26 @@ +module Tests.Uniplate where + +import Data.Generics.Uniplate.Data (transform, universe) +import Foreword +import Primer.Core +import Primer.Core.DSL +import Test.Tasty.HUnit + +-- In some places, but notably in importing, I rely on the fact +-- that 'universe' will look at the whole expression. However, it is +-- not totally clear that uniplate will do that, as we have mutual +-- recursion between the types Expr' and CaseBranch. +-- This tests that it does indeed look through this mutual recursion +unit_expr_universe_looks_in_branches :: Assertion +unit_expr_universe_looks_in_branches = [c | Con _ c <- universe e] @?= ["A"] + where + e = fst $ create $ case_ emptyHole [branch "C" [] $ con "A"] + +-- similar to universe test, but for transform +unit_expr_transform_looks_in_branches :: Assertion +unit_expr_transform_looks_in_branches = transform f (e "A") @?= e "B" + where + e n = fst $ create $ case_ emptyHole [branch "C" [] $ con n] + f = \case + Con m "A" -> Con m "B" + expr -> expr From 72c9294f1ace995ab465126338180e2bff5adc4c Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 12:24:21 +0000 Subject: [PATCH 10/12] fix: import: rename constructors in pattern matches Since the left hand side of a pattern match (the "C" in case x of C -> e ) is a Name in a CaseBranch, rather than a Con, it was not being updated. --- primer/src/Primer/Import.hs | 8 +++++ primer/test/Tests/Import.hs | 62 ++++++++++++++++++++++++++++--------- 2 files changed, 55 insertions(+), 15 deletions(-) diff --git a/primer/src/Primer/Import.hs b/primer/src/Primer/Import.hs index 6aba5896f..6b08a04b1 100644 --- a/primer/src/Primer/Import.hs +++ b/primer/src/Primer/Import.hs @@ -16,7 +16,9 @@ import qualified Data.Set as Set import Foreword import Optics ( AffineTraversal', + Field1 (_1), Field2 (_2), + Field3 (_3), traverseOf, traversed, (%), @@ -450,6 +452,12 @@ getImportTermsFromApp curProg (srcProg, IAC{iacImportRenamingTerms, iacDepsTerms lookupOrThrow origCon conRename $ ReferencedConstructorNotHandled origCon ) + <=< traverseOf + (#_Case % _3 % traversed % #_CaseBranch % _1) + ( \origCon -> + lookupOrThrow origCon conRename $ + ReferencedConstructorNotHandled origCon + ) <=< traverseOf _exprTypeChildren rejigType <=< traverseOf _exprMetaLens rejigMeta def'' <- traverseOf (#_DefAST % #astDefExpr) rejigExpr def' diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index 2f0a73a06..d16cf36ff 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -24,6 +24,16 @@ unitDef = , astTypeDefNameHints = [] } +natDef' :: Name -> Name -> Name -> TypeDef +natDef' tyName zeroName succName = + TypeDefAST $ + ASTTypeDef + { astTypeDefName = tyName + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon zeroName [], ValCon succName [TCon () tyName]] + , astTypeDefNameHints = astTypeDefNameHints natDef + } + srcProg :: (MonadFresh ID m) => m (Prog, ID, ID) srcProg = do plusId <- fresh @@ -176,30 +186,24 @@ holeFree def = noHoles (defType def) && maybe True noHolesTm (def ^? #_DefAST % #astDefExpr) --- We can rename types and ctors when importing +-- We can rename types, ctors and terms when importing unit_import_import_renaming :: Assertion unit_import_import_renaming = runImportTest $ do - (p, _, _) <- srcProg + (p, plusId, multId) <- srcProg let iac = IAC { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) , iacDepsTypes = mempty - , iacImportRenamingTerms = mempty + , iacImportRenamingTerms = Map.fromList [(plusId, "add"), (multId, "mult")] , iacDepsTerms = mempty } importFromApp p iac result <- gets appProg return $ do - progTypes result - @?= [ TypeDefAST $ - ASTTypeDef - { astTypeDefName = "N" - , astTypeDefParameters = [] - , astTypeDefConstructors = [ValCon "Z" [], ValCon "S" [TCon () "N"]] - , astTypeDefNameHints = astTypeDefNameHints natDef - } - ] - progDefs result @?= mempty + progTypes result @?= [natDef' "N" "Z" "S"] + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["add", "mult"] -- Importing and renaming primitives works unit_import_primitive :: Assertion @@ -247,8 +251,8 @@ unit_import_ctor_type = runImportTest $ do -- test rewiring dependencies -- Here we have mimiced importing a library 'A' -- and then later a library 'B' which itself depends on 'A' -unit_import_rewire_deps :: Assertion -unit_import_rewire_deps = runImportTest $ do +unit_import_rewire_deps_type :: Assertion +unit_import_rewire_deps_type = runImportTest $ do p <- srcProg2 ("List", "Nil", "Cons") ("Rose", "MkRose") let listRenaming = Map.singleton "List" ("L", Map.fromList [("Nil", "Nil"), ("Cons", "Cons")]) let iac = @@ -302,6 +306,34 @@ unit_import_rewire_primitive = runImportTest $ do all holeFree (Map.elems $ progDefs result) defName <$> Map.elems (progDefs result) @?= ["UPPER", "==", "foo"] +unit_import_rewire_deps_term :: Assertion +unit_import_rewire_deps_term = runImportTest $ do + (p, plusId, multId) <- srcProg + let natRenaming = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + let iac = + IAC + { iacImportRenamingTypes = natRenaming + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton plusId "add" + , iacDepsTerms = mempty + } + importFromApp p iac + addId <- gets $ defID . unsafeHead . filter ((== "add") . defName) . Map.elems . progDefs . appProg + let iac' = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = natRenaming + , iacImportRenamingTerms = Map.singleton multId "times" + , iacDepsTerms = Map.singleton plusId addId + } + importFromApp p iac' + result <- gets appProg + return $ do + progTypes result @?= [natDef' "N" "Z" "S"] + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["add", "times"] + -- cannot import without deps unit_import_ref_not_handled :: Assertion unit_import_ref_not_handled = do From 2b982cd07d3cc0504d84552348a7e908857814e0 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 13:24:44 +0000 Subject: [PATCH 11/12] fix: import: reordering case branches if necessary Since we allow rewiring imported type dependencies to any compatible existing type, with any compatible bijection of their constructors, we need to handle the case where the constructors get reordered. This is important since the typechecker enforces that the branches of a pattern match are in the order that constructors are declared in the corresponding type definition. For example, if we imported and rewired the type data T = A | B to data R = C | D via A -> D and B -> C, then we would need to reorder the import of case x of A -> t B -> some_other_rhs to case x of C -> some_other_rhs D -> t (Note that much of this commit only changes indentation) --- primer/src/Primer/Import.hs | 199 ++++++++++++++++++++---------------- primer/test/Tests/Import.hs | 30 ++++++ 2 files changed, 142 insertions(+), 87 deletions(-) diff --git a/primer/src/Primer/Import.hs b/primer/src/Primer/Import.hs index 6b08a04b1..deb32bd00 100644 --- a/primer/src/Primer/Import.hs +++ b/primer/src/Primer/Import.hs @@ -11,6 +11,7 @@ import Control.Monad.Fresh (MonadFresh (fresh)) import Control.Monad.NestedError (MonadNestedError (throwError')) import Data.Data (Data) import Data.Generics.Uniplate.Data (transformM) +import Data.List (elemIndex) import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Foreword @@ -30,6 +31,8 @@ import Primer.App.Core ( Prog (progDefs, progTypes), ) import Primer.Core ( + CaseBranch, + CaseBranch' (CaseBranch), Def, Expr, ID, @@ -163,13 +166,13 @@ importFromApp' :: m Prog importFromApp' srcProg iac = do curProg <- asks appProg - (newTypeDefs, typeRenaming, ctorRenaming) <- getImportTypesFromApp curProg (srcProg, iac) - newTerms <- getImportTermsFromApp curProg (srcProg, iac) typeRenaming ctorRenaming + (newTypeDefs, typeRenaming, ctorRenaming, ctorPerm) <- getImportTypesFromApp curProg (srcProg, iac) + newTerms <- getImportTermsFromApp curProg (srcProg, iac) typeRenaming ctorRenaming ctorPerm pure $ curProg & #progTypes %~ (++ newTypeDefs) & #progDefs %~ (<> mkDefMap newTerms) -getImportTypesFromApp :: forall m e. MonadNestedError ImportError e m => Prog -> (Prog, ImportActionConfig) -> m ([TypeDef], Map Name Name, Map Name Name) +getImportTypesFromApp :: forall m e. MonadNestedError ImportError e m => Prog -> (Prog, ImportActionConfig) -> m ([TypeDef], Map Name Name, Map Name Name, Map [Name] [Name]) getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes}) = {- We check requirements, to give nice error messages, rather than "typechecker says no" - Things need to exist in srcProg: @@ -239,7 +242,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes -- renaming map for deps rewriting let curTypes = mkTypeDefMap $ progTypes curProg - (tyrn2, ctorrn2, toCheckRewriteCtorsTypes) <- getAp $ + (tyrn2, ctorrn2, ctorperm, toCheckRewriteCtorsTypes) <- getAp $ flip Map.foldMapWithKey iacDepsTypes $ \srcTyName (tgtTyName, ctorMap) -> Ap $ do -- the rewritten thing must exist in the imported program -- (nothing would go wrong if we elided this check, but it catches @@ -255,7 +258,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes unless (typeDefKind srcTy == typeDefKind tgtTy) $ throwError' $ RewriteTypeKindMismatch srcTyName tgtTyName - (_ctorPerm, toCheckRewriteCtorsTypes) <- case (typeDefAST srcTy, typeDefAST tgtTy) of + (ctorPerm, toCheckRewriteCtorsTypes) <- case (typeDefAST srcTy, typeDefAST tgtTy) of (Nothing, Nothing) -> do unless (srcTyName == tgtTyName) $ throwError' $ CannotRenamePrimitiveType srcTyName -- primitives have no constructors @@ -300,6 +303,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes pure ( Map.singleton srcTyName tgtTyName , ctorMap + , ctorPerm , toCheckRewriteCtorsTypes ) @@ -333,7 +337,7 @@ getImportTypesFromApp curProg (srcProg, IAC{iacImportRenamingTypes, iacDepsTypes rewriteTCons' tydefs - pure (rejiggedTypeDefs, tyrn, ctorrn1 <> ctorrn2) + pure (rejiggedTypeDefs, tyrn, ctorrn1 <> ctorrn2, ctorperm) lookupOrThrow :: (MonadNestedError ImportError e m, Ord k) => @@ -375,92 +379,113 @@ getImportTermsFromApp :: (Prog, ImportActionConfig) -> Map Name Name -> Map Name Name -> + Map [Name] [Name] -> m [Def] -getImportTermsFromApp curProg (srcProg, IAC{iacImportRenamingTerms, iacDepsTerms}) tconRename conRename = do - {- We need that: - - created terms are freshly named - (this is not necessary for the typechecker, as globals are referred to by ID, - and we will create fresh IDs, but we include it for consistency with manually - allowed actions, which forbid creating two definitions with the same name) - - rewritten deps exist in curProg, and have the correct type - - created and rewritten things exist in srcProg (and are all distinct) - - all referenced things (global terms,types,constructors) are - - either imported or rewritten for terms - - covered in the tconRename and conRename maps for types and constructors respectively - If we have those properties, the typechecker should not complain. - We explicitly check them so we get nicer error messages than we would get from the typechecker - -} - -- Not allowed to both import and dep-rename some type - for_ (Map.intersection iacImportRenamingTerms iacDepsTerms) $ throwError' . ImportRenameTerm +getImportTermsFromApp + curProg + (srcProg, IAC{iacImportRenamingTerms, iacDepsTerms}) + tconRename + conRename + conPerm = do + {- We need that: + - created terms are freshly named + (this is not necessary for the typechecker, as globals are referred to by ID, + and we will create fresh IDs, but we include it for consistency with manually + allowed actions, which forbid creating two definitions with the same name) + - rewritten deps exist in curProg, and have the correct type + - created and rewritten things exist in srcProg (and are all distinct) + - all referenced things (global terms,types,constructors) are + - either imported or rewritten for terms + - covered in the tconRename and conRename maps for types and constructors respectively + If we have those properties, the typechecker should not complain. + We explicitly check them so we get nicer error messages than we would get from the typechecker + -} + -- Not allowed to both import and dep-rename some type + for_ (Map.intersection iacImportRenamingTerms iacDepsTerms) $ throwError' . ImportRenameTerm - -- things we create have distinct names, and don't appear in curProg - let created = Map.elems iacImportRenamingTerms - let extant = fmap defName $ Map.elems $ progDefs curProg - case distinct' $ created ++ extant of - Left dups -> throwError' $ DuplicateTerm dups - Right _ -> pure () + -- things we create have distinct names, and don't appear in curProg + let created = Map.elems iacImportRenamingTerms + let extant = fmap defName $ Map.elems $ progDefs curProg + case distinct' $ created ++ extant of + Left dups -> throwError' $ DuplicateTerm dups + Right _ -> pure () - -- Create renaming map for imported terms, and grab the defs and its new name - (rn1, toImport) <- getAp $ - flip Map.foldMapWithKey iacImportRenamingTerms $ \srcID tgtName -> Ap $ do - -- imported type exists in srcProg - srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownImportedTerm srcID - newID <- fresh - pure - ( Map.singleton srcID newID - , [(srcDef, newID, tgtName)] - ) + -- Create renaming map for imported terms, and grab the defs and its new name + (rn1, toImport) <- getAp $ + flip Map.foldMapWithKey iacImportRenamingTerms $ \srcID tgtName -> Ap $ do + -- imported type exists in srcProg + srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownImportedTerm srcID + newID <- fresh + pure + ( Map.singleton srcID newID + , [(srcDef, newID, tgtName)] + ) - -- Create renaming map for rewritten dependencies - rn2 <- getAp $ - flip Map.foldMapWithKey iacDepsTerms $ \srcID tgtID -> Ap $ do - -- the rewritten thing must exist in the imported program - -- (nothing would go wrong if we elided this check, but it catches - -- that our caller is broken) - srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownRewrittenSrcTerm srcID - -- We must rewrite it to an existing term ... - tgtDef <- lookupOrThrow tgtID (progDefs curProg) $ UnknownRewrittenTgtTerm tgtID - -- ... of the same type (taking into account the renaming of types) - srcType' <- rewriteTCons tconRename pure $ forgetTypeIDs $ defType srcDef - unless (srcType' `alphaEqTy` forgetTypeIDs (defType tgtDef)) $ throwError' $ RewriteTermTypeMismatch srcID tgtID + -- Create renaming map for rewritten dependencies + rn2 <- getAp $ + flip Map.foldMapWithKey iacDepsTerms $ \srcID tgtID -> Ap $ do + -- the rewritten thing must exist in the imported program + -- (nothing would go wrong if we elided this check, but it catches + -- that our caller is broken) + srcDef <- lookupOrThrow srcID (progDefs srcProg) $ UnknownRewrittenSrcTerm srcID + -- We must rewrite it to an existing term ... + tgtDef <- lookupOrThrow tgtID (progDefs curProg) $ UnknownRewrittenTgtTerm tgtID + -- ... of the same type (taking into account the renaming of types) + srcType' <- rewriteTCons tconRename pure $ forgetTypeIDs $ defType srcDef + unless (srcType' `alphaEqTy` forgetTypeIDs (defType tgtDef)) $ throwError' $ RewriteTermTypeMismatch srcID tgtID - pure $ Map.singleton srcID tgtID + pure $ Map.singleton srcID tgtID - let globalRename = rn1 <> rn2 + let globalRename = rn1 <> rn2 - -- Rename the referenced globals,constructors and types. - -- These are now ready to be inserted into curProg - for toImport $ \(def, newID, newName) -> do - let rejigMeta :: Meta (Maybe a) -> m (Meta (Maybe a)) - rejigMeta m = - m & _type .~ Nothing - & traverseOf _id (const fresh) - rejigType = rewriteTCons tconRename rejigMeta - def' <- traverseOf _defType rejigType def - let rejigExpr :: Expr -> m Expr - rejigExpr = - transformM $ - traverseOf - (#_GlobalVar % _2) - ( \origGlobal -> - lookupOrThrow origGlobal globalRename $ - ReferencedGlobalNotHandled origGlobal - ) - <=< traverseOf - (#_Con % _2) - ( \origCon -> - lookupOrThrow origCon conRename $ - ReferencedConstructorNotHandled origCon - ) - <=< traverseOf - (#_Case % _3 % traversed % #_CaseBranch % _1) - ( \origCon -> - lookupOrThrow origCon conRename $ - ReferencedConstructorNotHandled origCon + -- Rename the referenced globals,constructors and types. + -- These are now ready to be inserted into curProg + for toImport $ \(def, newID, newName) -> do + let rejigMeta :: Meta (Maybe a) -> m (Meta (Maybe a)) + rejigMeta m = + m & _type .~ Nothing + & traverseOf _id (const fresh) + rejigType = rewriteTCons tconRename rejigMeta + -- We need to rename the constructors that we branch on + -- and also reorder the branches to keep the invariant + -- that branches are in same order as constructors + -- declared in type def + rejigCaseBranches :: [CaseBranch] -> m [CaseBranch] + rejigCaseBranches bs = + let branchName = \case CaseBranch c _ _ -> c + cons = map branchName bs + perm = Map.lookup cons conPerm + sortToMatch = case perm of + Nothing -> identity + Just p -> sortOn (flip elemIndex p . branchName) + in sortToMatch + <$> traverseOf + (traversed % #_CaseBranch % _1) + ( \origCon -> + lookupOrThrow origCon conRename $ + ReferencedConstructorNotHandled origCon + ) + bs + def' <- traverseOf _defType rejigType def + let rejigExpr :: Expr -> m Expr + rejigExpr = + transformM $ + traverseOf + (#_GlobalVar % _2) + ( \origGlobal -> + lookupOrThrow origGlobal globalRename $ + ReferencedGlobalNotHandled origGlobal ) - <=< traverseOf _exprTypeChildren rejigType - <=< traverseOf _exprMetaLens rejigMeta - def'' <- traverseOf (#_DefAST % #astDefExpr) rejigExpr def' - pure $ - def'' & _defID .~ newID - & _defName .~ newName + <=< traverseOf + (#_Con % _2) + ( \origCon -> + lookupOrThrow origCon conRename $ + ReferencedConstructorNotHandled origCon + ) + <=< traverseOf (#_Case % _3) rejigCaseBranches + <=< traverseOf _exprTypeChildren rejigType + <=< traverseOf _exprMetaLens rejigMeta + def'' <- traverseOf (#_DefAST % #astDefExpr) rejigExpr def' + pure $ + def'' & _defID .~ newID + & _defName .~ newName diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index d16cf36ff..f64ef75f1 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -334,6 +334,36 @@ unit_import_rewire_deps_term = runImportTest $ do all holeFree (Map.elems $ progDefs result) defName <$> Map.elems (progDefs result) @?= ["add", "times"] +-- We can rewrite types with ctors in different order +-- (recall, we enforce an ordering in case branches) +unit_import_reorder_ctors :: Assertion +unit_import_reorder_ctors = runImportTest $ do + _ <- handleMutationRequest $ Edit [AddTypeDef natDefSwap] + (p, plusId, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + , iacImportRenamingTerms = Map.fromList [(plusId, "add")] + , iacDepsTerms = mempty + } + importFromApp p iac + result <- gets appProg + return $ do + progTypes result + @?= [TypeDefAST natDefSwap] + assertBool "There are holes in the resultant program" $ + all holeFree (Map.elems $ progDefs result) + defName <$> Map.elems (progDefs result) @?= ["add"] + where + natDefSwap = + ASTTypeDef + { astTypeDefName = "N" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon "S" [TCon () "N"], ValCon "Z" []] + , astTypeDefNameHints = astTypeDefNameHints natDef + } + -- cannot import without deps unit_import_ref_not_handled :: Assertion unit_import_ref_not_handled = do From ab3ad49d1811402eeb963a5ffa959eca316adfc8 Mon Sep 17 00:00:00 2001 From: Ben Price Date: Tue, 22 Feb 2022 12:11:06 +0000 Subject: [PATCH 12/12] fix: import: typecheck with smartholes off --- primer/src/Primer/App.hs | 8 ++++++-- primer/test/Tests/Import.hs | 3 ++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs index 550069014..84a5dbcae 100644 --- a/primer/src/Primer/App.hs +++ b/primer/src/Primer/App.hs @@ -456,8 +456,12 @@ importFromApp srcProg iac = do finalProg <- runReaderT (importFromApp' srcProg iac) curProg -- We typecheck the final result, but this should pass -- if the conditions in importFromApp' are satisfied - prog' <- tcEverything finalProg - modify (\s -> s{appProg = prog'}) + -- We make sure to do so with smartholes disabled, + -- as we want to error out if something has gone wrong, + -- rather than editing the code to make it acceptable + let sh = progSmartHoles finalProg + prog' <- tcEverything finalProg{progSmartHoles = NoSmartHoles} + modify (\s -> s{appProg = prog'{progSmartHoles = sh}}) -- | A shorthand for the constraints we need when performing mutation -- operations on the application. diff --git a/primer/test/Tests/Import.hs b/primer/test/Tests/Import.hs index f64ef75f1..56bea1a57 100644 --- a/primer/test/Tests/Import.hs +++ b/primer/test/Tests/Import.hs @@ -176,7 +176,8 @@ unit_import_import_simple = runImportTest $ do -- basically doing the import-renaming again. We instead just check -- we have the expected definitions, and they do not contain any holes -- (as one may worry would happen if they were imported badly, and then - -- smartholes kicked in) + -- smartholes kicked in - nb: we TC with smartholes off so this shouldn't + -- happen). assertBool "There are holes in the resultant program" $ all holeFree (Map.elems $ progDefs result) defName <$> Map.elems (progDefs result) @?= ["plus"]