diff --git a/primer/primer.cabal b/primer/primer.cabal index 1f7f3dd44..ac52a18a0 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 @@ -26,6 +27,7 @@ library Primer.Database Primer.Eval Primer.EvalFull + Primer.Import Primer.Name Primer.Name.Fresh Primer.Primitives @@ -34,6 +36,7 @@ library Primer.Subst Primer.Typecheck Primer.Unification + Primer.Utils Primer.Zipper Primer.ZipperCxt @@ -104,6 +107,7 @@ test-suite primer-test Tests.EvalFull Tests.FreeVars Tests.Gen.Core.Typed + Tests.Import Tests.Primitives Tests.Question Tests.Refine @@ -112,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/src/Primer/App.hs b/primer/src/Primer/App.hs index 936e1bb2f..84a5dbcae 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,16 +49,12 @@ module Primer.App ( listDef, eitherDef, defaultTypeDefs, + MonadEditApp, ) where 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 +70,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 +92,17 @@ 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.Import ( + ImportActionConfig (..), + ImportError (..), + importFromApp', + ) import Primer.JSON import Primer.Name (Name, NameCounter, freshName, unsafeMkName) -import Primer.Primitives (allPrimDefs, allPrimTypeDefs) import Primer.Questions ( Question (..), generateNameExpr, @@ -151,52 +145,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 @@ -227,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 @@ -501,6 +450,19 @@ 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 + -- 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. -- @@ -541,106 +503,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 @@ -760,6 +622,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 @@ -889,84 +762,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 = [] + } diff --git a/primer/src/Primer/Core.hs b/primer/src/Primer/Core.hs index c4db411b0..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, @@ -35,6 +38,7 @@ module Primer.Core ( TypeDef (..), typeDefAST, typeDefKind, + _typeDefName, typeDefName, typeDefNameHints, typeDefParameters, @@ -347,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 @@ -454,6 +477,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/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 new file mode 100644 index 000000000..deb32bd00 --- /dev/null +++ b/primer/src/Primer/Import.hs @@ -0,0 +1,491 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedLabels #-} + +module Primer.Import ( + ImportError (..), + importFromApp', + 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 Data.List (elemIndex) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import Foreword +import Optics ( + AffineTraversal', + Field1 (_1), + Field2 (_2), + Field3 (_3), + traverseOf, + traversed, + (%), + (%~), + (.~), + ) +import Primer.App.Core ( + App (appProg), + Prog (progDefs, progTypes), + ) +import Primer.Core ( + CaseBranch, + CaseBranch' (CaseBranch), + 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, forgetTypeIDs, _exprTypeChildren) +import Primer.JSON +import Primer.Name (Name) +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 + -- 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 + | -- | 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) + 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 + | -- | 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) + 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 +-- 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. +-- +-- (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 + , iacImportRenamingTerms :: Map ID Name + , iacDepsTerms :: Map ID ID + } + +-- | 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, MonadFresh ID m) => + Prog -> + ImportActionConfig -> + m Prog +importFromApp' srcProg iac = do + curProg <- asks appProg + (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, 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: + - 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, 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 + -- 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 + , ctorPerm + , 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' = rewriteTCons tyrn pure + + -- 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 + rejiggedTypeDefs <- + traverseOf + (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed) + rewriteTCons' + tydefs + + pure (rejiggedTypeDefs, tyrn, ctorrn1 <> ctorrn2, ctorperm) + +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 + tconName + ( \tc -> + lookupOrThrow tc tyrn $ ReferencedTypeNotHandled tc + ) + <=< traverseOf _typeMetaLens f + where + 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 -> + Map [Name] [Name] -> + m [Def] +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 () + + -- 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 + -- 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 + (#_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/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs index 852a6d048..f7c9e621a 100644 --- a/primer/src/Primer/Typecheck.hs +++ b/primer/src/Primer/Typecheck.hs @@ -42,7 +42,9 @@ module Primer.Typecheck ( getGlobalNames, lookupGlobal, lookupLocal, + primConInScope, mkTypeDefMap, + mkDefMap, consistentKinds, consistentTypes, extendLocalCxtTy, @@ -76,6 +78,7 @@ import Primer.Core ( ID, Kind (..), Meta (..), + PrimCon, Type' (..), TypeCache (..), TypeCacheBoth (..), @@ -102,6 +105,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 @@ -128,6 +132,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 @@ -217,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 @@ -338,14 +350,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. @@ -484,8 +488,12 @@ 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 + (inScope, tyCon) <- asks (primConInScope pc) + -- We expect any frontend to avoid this situation, and thus we do not + -- try to recover with SmartHoles + unless inScope $ throwError' $ PrimitiveTypeNotInScope tyCon + pure $ annSynth0 (TCon () tyCon) i (\m -> PrimCon m pc) e -> asks smartHoles >>= \case NoSmartHoles -> throwError' $ CannotSynthesiseType e @@ -503,6 +511,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/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/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/Import.hs b/primer/test/Tests/Import.hs new file mode 100644 index 000000000..56bea1a57 --- /dev/null +++ b/primer/test/Tests/Import.hs @@ -0,0 +1,860 @@ +{-# 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.Core.DSL +import Primer.Core.Utils (noHoles, noHolesTm) +import Primer.Name +import Primer.Primitives (allPrimDefs, allPrimTypeDefs) +import Primer.Typecheck (mkDefMap) +import Test.Tasty.HUnit + +unitDef :: ASTTypeDef +unitDef = + ASTTypeDef + { astTypeDefName = "Unit" + , astTypeDefParameters = [] + , astTypeDefConstructors = [ValCon "MkUnit" []] + , 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 + 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 + { progTypes = [TypeDefAST natDef] + , 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 + 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 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 [boolDef, stringDef] <> map TypeDefPrim (Map.elems allPrimTypeDefs) + , progDefs = primMap <> Map.singleton wrapperId (DefAST wrapper) + } + , primNames + , wrapperId + ) + 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, plusID, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("Nat", Map.fromList [("Zero", "Zero"), ("Succ", "Succ")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.singleton plusID "plus" + , iacDepsTerms = mempty + } + importFromApp p iac + result <- gets appProg + return $ do + progTypes result @?= progTypes p + -- 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 - 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"] + +holeFree :: Def -> Bool +holeFree def = + noHoles (defType def) + && maybe True noHolesTm (def ^? #_DefAST % #astDefExpr) + +-- We can rename types, ctors and terms when importing +unit_import_import_renaming :: Assertion +unit_import_import_renaming = runImportTest $ do + (p, plusId, multId) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = Map.singleton "Nat" ("N", Map.fromList [("Zero", "Z"), ("Succ", "S")]) + , iacDepsTypes = mempty + , iacImportRenamingTerms = Map.fromList [(plusId, "add"), (multId, "mult")] + , iacDepsTerms = mempty + } + 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", "mult"] + +-- Importing and renaming primitives works +unit_import_primitive :: Assertion +unit_import_primitive = runImportTest $ do + (p, prims, fooId) <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = + Map.fromList + [ ("Char", ("Char", mempty)) + , ("Bool", ("B", Map.fromList [("True", "tt"), ("False", "ff")])) + ] + , iacDepsTypes = 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) @?= ["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 +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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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_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 = + 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 + expect <- srcProg2 ("L", "Nil", "Cons") ("T", "C") + return $ result @?= expect + +unit_import_rewire_primitive :: Assertion +unit_import_rewire_primitive = runImportTest $ do + (p, prims, fooId) <- primSrcProg + let iac = + IAC + { iacImportRenamingTypes = Map.fromList [("Char", ("Char", mempty))] + , iacDepsTypes = 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.fromList + [ ("Bool", ("B", Map.fromList [("True", "tt"), ("False", "ff")])) + , ("String", ("S", Map.fromList [("Empty", "Nil"), ("HeadAnd", "Cons")])) + ] + , iacDepsTypes = Map.singleton "Char" ("Char", 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", "B", "S"] + assertBool "There are holes in the resultant program" $ + 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"] + +-- 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 + 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 = 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 = 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/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 + 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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 + , iacImportRenamingTerms = mempty + , 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 + 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") + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + +-- cannot both import and rename the same type/term +unit_import_import_rename_clash :: Assertion +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/term, 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (UnknownRewrittenSrcType "Nonexistent") $ do + (p, _, _) <- srcProg + let iac = + IAC + { iacImportRenamingTypes = mempty + , iacDepsTypes = Map.singleton "Nonexistent" ("T", mempty) + , iacImportRenamingTerms = mempty + , iacDepsTerms = 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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")]) + , iacImportRenamingTerms = mempty + , 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 +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")]) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + 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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (CannotRenamePrimitiveType "Char") $ do + (p, _, _) <- primSrcProg + let iac = + 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' + +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 + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (PrimitiveTypeHasNoCtor "Char") $ do + (p, _, _) <- primSrcProg + let iac = + 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' + +-- 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) + , iacImportRenamingTerms = mempty + , iacDepsTerms = mempty + } + importFromApp p iac + runImportTestError (RewriteTypePrimitiveMismatch "Char" "Char") $ do + (p, _, _) <- primSrcProg + let iac = + 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 + 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 diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs index 7b6fbc840..8700d9404 100644 --- a/primer/test/Tests/Primitives.hs +++ b/primer/test/Tests/Primitives.hs @@ -7,13 +7,70 @@ 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 (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 + 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 +-- 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..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 @@ -527,18 +554,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 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