{-# Language FlexibleInstances, PatternGuards #-} -- | Assumes that local names do not shadow top level names. module Cryptol.ModuleSystem.InstantiateModule ( instantiateModule ) where import Data.Set (Set) import qualified Data.Set as Set import Data.Map (Map) import qualified Data.Map as Map import MonadLib(ReaderT,runReaderT,ask) import Cryptol.Parser.Position(Located(..)) import Cryptol.ModuleSystem.Name import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(listParamSubst, apSubst) import Cryptol.Utils.Ident(ModName,modParamIdent) {- XXX: Should we simplify constraints in the instantiated modules? If so, we also need to adjust the constraint parameters on terms appropriately, especially when working with dictionaries. -} -- | Convert a module instantiation into a partial module. -- The resulting module is incomplete because it is missing the definitions -- from the instantiation. instantiateModule :: FreshM m => Module {- ^ Parametrized module -} -> ModName {- ^ Name of the new module -} -> Map TParam Type {- ^ Type params -} -> Map Name Expr {- ^ Value parameters -} -> m ([Located Prop], Module) -- ^ Instantiated constraints, fresh module, new supply instantiateModule func newName tpMap vpMap = runReaderT newName $ do let oldVpNames = Map.keys vpMap newVpNames <- mapM freshParamName (Map.keys vpMap) let vpNames = Map.fromList (zip oldVpNames newVpNames) env <- computeEnv func tpMap vpNames let rnMp :: Inst a => (a -> Name) -> Map Name a -> Map Name a rnMp f m = Map.fromList [ (f x, x) | a <- Map.elems m , let x = inst env a ] renamedExports = inst env (mExports func) renamedTySyns = rnMp tsName (mTySyns func) renamedNewtypes = rnMp ntName (mNewtypes func) renamedPrimTys = rnMp atName (mPrimTypes func) su = listParamSubst (Map.toList (tyParamMap env)) goals = map (fmap (apSubst su)) (mParamConstraints func) -- Constraints to discharge about the type instances let renamedDecls = inst env (mDecls func) paramDecls = map (mkParamDecl su vpNames) (Map.toList vpMap) return ( goals , Module { mName = newName , mExports = renamedExports , mImports = mImports func , mTySyns = renamedTySyns , mNewtypes = renamedNewtypes , mPrimTypes = renamedPrimTys , mParamTypes = Map.empty , mParamConstraints = [] , mParamFuns = Map.empty , mDecls = paramDecls ++ renamedDecls } ) where mkParamDecl su vpNames (x,e) = NonRecursive Decl { dName = Map.findWithDefault (error "OOPS") x vpNames , dSignature = apSubst su $ mvpType $ Map.findWithDefault (error "UUPS") x (mParamFuns func) , dDefinition = DExpr e , dPragmas = [] -- XXX: which if any pragmas? , dInfix = False -- XXX: get from parameter? , dFixity = Nothing -- XXX: get from parameter , dDoc = Nothing -- XXX: get from parametr(or instance?) } -------------------------------------------------------------------------------- -- Things that need to be renamed class Defines t where defines :: t -> Set Name instance Defines t => Defines [t] where defines = Set.unions . map defines instance Defines Decl where defines = Set.singleton . dName instance Defines DeclGroup where defines d = case d of NonRecursive x -> defines x Recursive x -> defines x -------------------------------------------------------------------------------- type InstM = ReaderT ModName -- | Generate a new instance of a declared name. freshenName :: FreshM m => Name -> InstM m Name freshenName x = do m <- ask let sys = case nameInfo x of Declared _ s -> s _ -> UserName liftSupply (mkDeclared m sys (nameIdent x) (nameFixity x) (nameLoc x)) freshParamName :: FreshM m => Name -> InstM m Name freshParamName x = do m <- ask let newName = modParamIdent (nameIdent x) liftSupply (mkDeclared m UserName newName (nameFixity x) (nameLoc x)) -- | Compute renaming environment from a module instantiation. -- computeEnv :: ModInst -> InstM Env computeEnv :: FreshM m => Module {- ^ Functor being instantiated -} -> Map TParam Type {- replace type params by type -} -> Map Name Name {- replace value parameters by other names -} -> InstM m Env computeEnv m tpMap vpMap = do tss <- mapM freshTy (Map.toList (mTySyns m)) nts <- mapM freshTy (Map.toList (mNewtypes m)) let tnMap = Map.fromList (tss ++ nts) defHere <- mapM mkVParam (Set.toList (defines (mDecls m))) let fnMap = Map.union vpMap (Map.fromList defHere) return Env { funNameMap = fnMap , tyNameMap = tnMap , tyParamMap = tpMap } where freshTy (x,_) = do y <- freshenName x return (x,y) mkVParam x = do y <- freshenName x return (x,y) -------------------------------------------------------------------------------- -- Do the renaming data Env = Env { funNameMap :: Map Name Name , tyNameMap :: Map Name Name , tyParamMap :: Map TParam Type } deriving Show class Inst t where inst :: Env -> t -> t instance Inst a => Inst [a] where inst env = map (inst env) instance Inst Expr where inst env = go where go expr = case expr of EVar x -> case Map.lookup x (funNameMap env) of Just y -> EVar y _ -> expr EList xs t -> EList (inst env xs) (inst env t) ETuple es -> ETuple (inst env es) ERec xs -> ERec (fmap go xs) ESel e s -> ESel (go e) s ESet e x v -> ESet (go e) x (go v) EIf e1 e2 e3 -> EIf (go e1) (go e2) (go e3) EComp t1 t2 e mss -> EComp (inst env t1) (inst env t2) (go e) (inst env mss) ETAbs t e -> ETAbs t (go e) ETApp e t -> ETApp (go e) (inst env t) EApp e1 e2 -> EApp (go e1) (go e2) EAbs x t e -> EAbs x (inst env t) (go e) EProofAbs p e -> EProofAbs (inst env p) (go e) EProofApp e -> EProofApp (go e) EWhere e ds -> EWhere (go e) (inst env ds) instance Inst DeclGroup where inst env dg = case dg of NonRecursive d -> NonRecursive (inst env d) Recursive ds -> Recursive (inst env ds) instance Inst DeclDef where inst env d = case d of DPrim -> DPrim DExpr e -> DExpr (inst env e) instance Inst Decl where inst env d = d { dSignature = inst env (dSignature d) , dDefinition = inst env (dDefinition d) , dName = Map.findWithDefault (dName d) (dName d) (funNameMap env) } instance Inst Match where inst env m = case m of From x t1 t2 e -> From x (inst env t1) (inst env t2) (inst env e) Let d -> Let (inst env d) instance Inst Schema where inst env s = s { sProps = inst env (sProps s) , sType = inst env (sType s) } instance Inst Type where inst env ty = case ty of TCon tc ts -> TCon (inst env tc) (inst env ts) TVar tv -> case tv of TVBound tp | Just t <- Map.lookup tp (tyParamMap env) -> t _ -> ty TUser x ts t -> TUser y (inst env ts) (inst env t) where y = Map.findWithDefault x x (tyNameMap env) TRec fs -> TRec (fmap (inst env) fs) instance Inst TCon where inst env tc = case tc of TC x -> TC (inst env x) _ -> tc instance Inst TC where inst env tc = case tc of TCNewtype x -> TCNewtype (inst env x) TCAbstract x -> TCAbstract (inst env x) _ -> tc instance Inst UserTC where inst env (UserTC x t) = UserTC y t where y = Map.findWithDefault x x (tyNameMap env) instance Inst (ExportSpec Name) where inst env es = ExportSpec { eTypes = Set.map instT (eTypes es) , eBinds = Set.map instV (eBinds es) } where instT x = Map.findWithDefault x x (tyNameMap env) instV x = Map.findWithDefault x x (funNameMap env) instance Inst TySyn where inst env ts = TySyn { tsName = instTyName env x , tsParams = tsParams ts , tsConstraints = inst env (tsConstraints ts) , tsDef = inst env (tsDef ts) , tsDoc = tsDoc ts } where x = tsName ts instance Inst Newtype where inst env nt = Newtype { ntName = instTyName env x , ntParams = ntParams nt , ntConstraints = inst env (ntConstraints nt) , ntFields = [ (f,inst env t) | (f,t) <- ntFields nt ] , ntDoc = ntDoc nt } where x = ntName nt instance Inst AbstractType where inst env a = AbstractType { atName = instTyName env (atName a) , atKind = atKind a , atCtrs = case atCtrs a of (xs,ps) -> (xs, inst env ps) , atFixitiy = atFixitiy a , atDoc = atDoc a } instTyName :: Env -> Name -> Name instTyName env x = Map.findWithDefault x x (tyNameMap env)