module Language.Java.Paragon.TypeCheck.Monad ( check, checkM, ignore, orElse, maybeM, withFold, withFoldMap, getThisType, getReturn, extendVarEnvList, extendVarEnv, lookupVar, lookupActorName, -- lookupField, lookupFieldT, lookupMethod, lookupMethodT, lookupConstr, lookupLockArity, lookupExn, registerExn, registerExns, extendLockEnv, getBranchPC, getBranchPC_, extendBranchPC, addBranchPC, addBranchPCList, getActorId, setActorId, newActorId, newActorIdWith, newAliasId, freshActorId, aliasActorId, scrambleActors, getExnPC, throwExn, activateExns, deactivateExn, getExnState, mergeActiveExnStates, useExnState, getCurrentLockState, applyLockMods, openLock, closeLock, newMetaPolVar, constraint, constraint_, exnConsistent, extendTypeMapP, extendTypeMapT, lookupPkgTypeMap, getTypeMap, withTypeMap, evalSrcType, evalSrcRefType, evalSrcClsType, evalSrcTypeArg, evalSrcNWTypeArg, evalReturnType, getReadPolicy, getWritePolicy, getLockPolicy, getParamPolicy, getReturnPolicy, fromSrcType, (<:), evalPolicy, evalPolicyExp, evalLock, evalActor, Tc, (|||), getState, mergeWithState, liftCont, runTc, setupStartState, -- TcBase, runTcBase, liftIO, withErrCtxt TcCont, runTcCont, liftIO, withErrCtxt ) where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty --import Language.Java.Paragon.TypeCheck.Monad.TcBase import Language.Java.Paragon.TypeCheck.Monad.TcCont import Language.Java.Paragon.TypeCheck.Monad.TcMonad import Language.Java.Paragon.TypeCheck.TcEnv import Language.Java.Paragon.TypeCheck.TcState import Language.Java.Paragon.TypeCheck.Uniq import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Constraints import Language.Java.Paragon.TypeCheck.Containment --import Language.Java.Paragon.TypeCheck.Interpreter import Control.Monad (liftM, msum) -- liftM only to instantiate fmap import Control.Applicative ( (<$>) ) -- ... so we can use <$> instead import Control.Arrow ( first, second ) import qualified Data.Map as Map import Data.IORef import Data.List (union, intersperse) debug str = liftIO $ putStrLn $ "DEBUG: " ++ str debugTc = liftCont . debug -------------------------------------------- -- -- -- Monad-independent helpers -- -- -- -------------------------------------------- check :: Monad m => Bool -> String -> m () check b err = if b then return () else fail err checkM :: Monad m => m Bool -> String -> m () checkM mb err = mb >>= flip check err ignore :: Monad m => m a -> m () ignore = (>> return ()) orElse :: Monad m => m (Maybe a) -> m a -> m a orElse monma mona = do ma <- monma case ma of Just a -> return a Nothing -> mona infixr 3 `orElse` maybeM :: Monad m => Maybe a -> (a -> m ()) -> m () maybeM ma f = maybe (return ()) f ma withFold :: Monad m => [m a -> m a] -> m a -> m a withFold = foldr (.) id withFoldMap :: Monad m => (a -> m b -> m b) -> [a] -> m b -> m b withFoldMap f = withFold . map f -------------------------------------------- -- Working with the env -- -------------------------------------------- -- this getThisType :: Tc r TcType getThisType = liftCont getThisT -- returns getReturn :: Tc r (TcType, TcPolicy) getReturn = returnI <$> getEnv {- registerReturn :: TcType -> TcPolicy -> Tc r a -> Tc r a registerReturn ty p = withEnv $ \env -> env { returnI = (ty,p) } -} -- lookup entities --fieldEnvToVars :: Tc r a -> Tc r a --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) } extendVarEnvList :: [(Ident, VarFieldSig)] -> Tc r a -> Tc r a extendVarEnvList vs = withEnv $ \env -> let oldVmap = vars env newVmap = foldl (\m (i,vti) -> Map.insert i vti m) oldVmap vs in env { vars = newVmap } extendVarEnv :: Ident -> VarFieldSig -> Tc r a -> Tc r a --extendVarEnv i = extendVarEnvN i --extendVarEnvN :: Ident -> VarFieldSig -> Tc r a -> Tc r a extendVarEnv i vti = withEnv $ \env -> let oldVmap = vars env newVmap = Map.insert i vti oldVmap in env { vars = newVmap } lookupActorName :: ActorName -> Tc r (TcType, TcPolicy) lookupActorName (ActorName n) = lookupVar n lookupActorName (ActorTypeVar i) = lookupVar (Name [i]) lookupVar :: Name -> Tc r (TcType, TcPolicy) lookupVar (Name n@(i:is)) = do tm <- liftCont getTypeMap (newTm,ty,pol,rest) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of Just (VSig ty p _ _) -> do let tyTm = lookupTypeOfT ty tm return (tyTm, ty, p, is) Nothing -> return (tm,voidT,bottom,n) aux newTm ty pol rest where aux :: TypeMap -> TcType -> TcPolicy -> [Ident] -> Tc r (TcType, TcPolicy) aux _ ty pol [] = return (ty, pol) aux tm _ pol (i:is) = do (newTm,newTy,newPol) <- case Map.lookup i (fields tm) of Just (VSig typ pol _ _) -> do baseTm <- liftCont getTypeMap return $ (lookupTypeOfT typ baseTm, typ, pol) Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (aTm,voidT,bottom) Nothing -> fail $ "lookupVar: No such name: " ++ prettyPrint(Name (i:is)) aux newTm newTy (pol `join` newPol) is lookupMethod :: Name -> [TcType] -> Tc r (TcPolicy, [TypeParam], MethodSig) lookupMethod (Name n@(i:is)) ts = do tm <- liftCont getTypeMap (newTm,pol,rest) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of Just (VSig ty p _ _) -> do let tyTm = lookupTypeOfT ty tm return (tyTm, p, is) Nothing -> return (tm,bottom,n) aux newTm pol rest ts where aux :: TypeMap -> TcPolicy -> [Ident] -> [TcType] -> Tc r (TcPolicy, [TypeParam], MethodSig) aux tm pol [i] ts = case Map.lookup (i,ts) (methods tm) of Just (tps, mti) -> return (pol, tps, mti) Nothing -> fail $ "lookupMethod: No such name: " ++ prettyPrint i -- ++ "\nMethods: " ++ show (methods tm) aux tm pol (i:is) ts = do (newTm,newPol) <- case Map.lookup i (fields tm) of Just (VSig typ pol _ _) -> do baseTm <- liftCont getTypeMap return $ (lookupTypeOfT typ baseTm, pol) Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (aTm,bottom) Nothing -> fail $ "lookupTypeOfN: No such name: " ++ prettyPrint i aux newTm (pol `join` newPol) is ts -- tm <- liftCont getTypeMap -- case lookupNamedMethod n ts tm of -- Just tpsmti -> return tpsmti -- Nothing -> fail $ "Unknown method: " ++ prettyPrint n -- ++ "(" ++ concat (intersperse "," $ map show ts) ++ ")" getPolicy :: Name -> Tc r TcPolicy getPolicy n = do tm <- liftCont getTypeMap case lookupNamed policies n tm of Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n Just p -> return p lookupFieldT :: TcType -> Ident -> Tc r VarFieldSig lookupFieldT typ i = do check (isClassType typ) $ "Not a class type: " ++ prettyPrint typ tm <- liftCont getTypeMap let aTm = lookupTypeOfT typ tm case Map.lookup i (fields aTm) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a field '" ++ prettyPrint i ++ "'" lookupMethodT :: TcType -> Ident -> [TcType] -> Tc r ([TypeParam], MethodSig) lookupMethodT typ i pts = do check (isClassType typ) $ "Not a class type: " ++ prettyPrint typ tm <- liftCont getTypeMap let aTm = lookupTypeOfT typ tm case Map.lookup (i,pts) (methods aTm) of Just pmti -> return pmti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a method '" ++ prettyPrint i ++ "'" lookupConstr :: TcClassType -> [TcType] -> Tc r ([TypeParam], ConstrSig) lookupConstr ctyp pts = do tm <- liftCont getTypeMap let typ = clsTypeToType ctyp aTm = lookupTypeOfT typ tm case Map.lookup pts (constrs aTm) of Just pcti -> return pcti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a constructor with argument types " ++ "(" ++ concat (intersperse ", " (map prettyPrint pts)) ++ ")" lookupLockArity :: Name -> Tc r Int lookupLockArity n = do tm <- liftCont getTypeMap case lookupNamed lockArities n tm of Nothing -> fail $ "Unknown lock: " ++ prettyPrint n Just arity -> return arity lookupExn :: TcType -> Tc r (TcPolicy, TcPolicy) lookupExn tyX = do exnMap <- exnsE <$> getEnv case Map.lookup tyX exnMap of Just ps -> return ps Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX registerExn :: TcType -> TcPolicy -> TcPolicy -> Tc r a -> Tc r a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] registerExns :: [(TcType, (TcPolicy, TcPolicy))] -> Tc r a -> Tc r a registerExns tysPols = withEnv $ \env -> let oldMap = exnsE env newMap = foldl (\m (t,ps) -> Map.insert t ps m) oldMap tysPols in env { exnsE = newMap } extendLockEnv :: [TcLock] -> Tc r a -> Tc r a extendLockEnv locks = withEnv $ \env -> env { lockstate = lockstate env `union` locks } getBranchPC :: Entity -> Tc r TcPolicy getBranchPC e = do env <- getEnv return $ branchPC (Just e) env getBranchPC_ :: Tc r TcPolicy getBranchPC_ = do env <- getEnv return $ branchPC Nothing env extendBranchPC :: TcPolicy -> Tc r a -> Tc r a extendBranchPC = withEnv . joinBranchPC addBranchPCList :: [Ident] -> Tc r a -> Tc r a addBranchPCList is = withEnv $ \env -> let (bm, def) = branchPCE env newBm = foldl (\m i -> Map.insert (VarEntity (Name [i])) bottom m) bm is in env { branchPCE = (newBm, def) } addBranchPC :: Entity -> TcPolicy -> Tc r a -> Tc r a addBranchPC ent pol = withEnv $ \env -> let (bm, def) = branchPCE env newBm = Map.insert ent pol bm in env { branchPCE = (newBm, def) } {-- Tying the knot for member policies setFieldPol :: Ident -> TcPolicy -> Tc r () setFieldPol i pF = do fMap <- (fields . typemap) <$> getEnv case Map.lookup (Name [i]) fMap of Nothing -> fail "panic: lookup of field failed when tying the knot" Just (VSig ty tempP stc fin) -> do case tempP of TcPolicyVar (TcMetaVar i ref) -> do mpol <- lift $ readIORef ref case mpol of Nothing -> do lift $ writeIORef ref (Just pF) Just _ -> fail "panic: field policy already written when tying the knot" _ -> fail "panic: field policy already set when tying the knot" setMethodPols :: Ident -> TcPolicy -> TcPolicy -> Tc r () setMethodPols i retM -} -------------------------------------------- -- Working with states -- -------------------------------------------- {- -- Leave actor mappings from fields startState :: Tc r () startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -} -- Actor Analysis getActorId :: Name -> Tc r ActorId getActorId n = do actorMap <- actorSt <$> getState case Map.lookup n actorMap of Nothing -> liftCont $ aliasActorId Just ai -> return $ aID ai setActorId :: Name -> ActorId -> Tc r () setActorId n aid = updateState setAct where setAct :: TcState -> TcState setAct s@(TcState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap } replId (AI _ st) = AI aid st newActorIdWith :: Ident -> ActorId -> Tc r () newActorIdWith i aid = do updateState (insertAct aid) where insertAct :: ActorId -> TcState -> TcState insertAct aid s@(TcState { actorSt = actMap }) = s { actorSt = Map.insert (Name [i]) (AI aid Stable) actMap } newActorId :: Ident -> Tc r ActorId newActorId i = do aid <- liftCont freshActorId newActorIdWith i aid return aid newAliasId :: Ident -> Tc r ActorId newAliasId i = do aid <- liftCont aliasActorId newActorIdWith i aid return aid freshActorId, aliasActorId :: TcCont r ActorId freshActorId = (liftIO . newFresh) =<< getUniqRef aliasActorId = (liftIO . newAlias) =<< getUniqRef scrambleActors :: Maybe TcType -> Tc r () scrambleActors mtc = do let stb = maybe FullV (FieldV . typeName_) mtc state <- getState u <- liftCont getUniqRef newState <- liftCont . liftIO $ scramble u stb state setState newState -- Exception tracking getExnPC :: Tc r TcPolicy getExnPC = exnPC <$> getState throwExn :: ExnType -> TcPolicy -> Tc r () throwExn et pX = do uref <- liftCont getUniqRef state <- getState let oldXmap = exnS state newXmap = Map.fromList [(et, ExnPoint state pX)] mergedXmap <- liftCont . liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } deactivateExn :: ExnType -> Tc r () deactivateExn et = updateState $ \s -> let oldEmap = exnS s newEmap = Map.delete et oldEmap in s { exnS = newEmap } activateExns :: [(ExnType, ExnSig)] -> Tc r () activateExns exns = do uref <- liftCont getUniqRef state <- getState let (ts, sigs) = unzip exns xPoints <- mapM (\sigX -> do s <- liftCont . liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO state { lockMods = lockMods state ||>> exnMods sigX } return (s, exnWrites sigX)) sigs let oldXmap = exnS state newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints) mergedXmap <- liftCont . liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } getExnState :: ExnType -> Tc r (Maybe TcState) getExnState et = do eMap <- exnS <$> getState return $ epState <$> Map.lookup et eMap mergeActiveExnStates :: Tc r () mergeActiveExnStates = do exnMap <- exnS <$> getState mapM_ (mergeWithState . epState) $ Map.elems exnMap useExnState :: TcState -> Tc r () useExnState es = updateState (\s -> s { exnS = exnS es }) -- Lockstate tracking getCurrentLockState :: Tc r [TcLock] getCurrentLockState = do base <- lockstate <$> getEnv mods <- lockMods <$> getState return $ snd $ ([], base) ||>> mods applyLockMods :: LockMods -> Tc r () applyLockMods lms = do updateState $ \s -> s { lockMods = lockMods s ||>> lms } openLock, closeLock :: TcLock -> Tc r () openLock l = applyLockMods ([],[l]) closeLock l = applyLockMods ([l],[]) -- Policy inference newMetaPolVar :: Tc r TcPolicy newMetaPolVar = do uniq <- liftCont $ liftIO . getUniq =<< getUniqRef ref <- liftCont $ liftIO (newIORef Nothing) return $ TcPolicyVar (TcMetaVar uniq ref) --newRigidPolVar :: Tc r TcPolicy --newRigidPolVar = do -- uniq <- lift . getUniq =<< getUniqRef -- return $ TcRigidVar uniq -------------------------------------------- -- Working with constraints -- -------------------------------------------- constraint :: [TcLock] -> TcPolicy -> TcPolicy -> Tc r () constraint ls p1 p2 = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps case lrt (g `recmeet` rls) p1 p2 of Left b -> do --debugTc $ "constraint: p1: " ++ show p1 --debugTc $ "constraint: p2: " ++ show p2 check b $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2) "\n* p = " ++ prettyPrint p1 ++ "\n* q = " ++ prettyPrint p2 ++ "\nin the presence of lock state {" ++ concat (intersperse ", " (map prettyPrint ls)) ++ "}" Right c -> addConstraint c where rls = locksToRec ls getGlobalLockProps :: Tc r TcPolicyRec getGlobalLockProps = return (TcPolicyRec []) locksToRec :: [TcLock] -> TcPolicyRec locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls)) constraint_ :: TcPolicy -> TcPolicy -> Tc r () constraint_ = constraint [] exnConsistent :: TcType -> ExnSig -> Tc r () exnConsistent exnTy (ExnSig rX wX _) = do exnMap <- exnsE <$> getEnv --debugTc $ "Using exnMap: " ++ show exnMap case Map.lookup exnTy exnMap of Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy) Just (rE, wE) -> do constraint_ wX wE constraint_ rE rX -------------------------------------------- -- Working with typemaps -- -------------------------------------------- extendTypeMapP :: [Ident] -> TypeMap -> TcCont r a -> TcCont r a extendTypeMapP [] leafTm = withTypeMap (const leafTm) -- WARNING: overwrites extendTypeMapP is leafTm = withTypeMap $ \tm -> go is leafTm tm where go :: [Ident] -> TypeMap -> TypeMap -> TypeMap go [i] leafTm tm = let mTm = packages tm in case Map.lookup i mTm of Nothing -> tm { packages = Map.insert i leafTm mTm } Just _ -> tm -- TODO: This means we were already here go (i:is) leafTm tm = let mTm = packages tm eTm = case Map.lookup i mTm of Just innerTm -> innerTm Nothing -> emptyTM newTm = go is leafTm eTm in tm { packages = Map.insert i newTm mTm } extendTypeMapT :: Ident -> [TypeParam] -> TypeSig -> TcCont r a -> TcCont r a extendTypeMapT i tps tSig = withTypeMap $ \tm -> tm { types = Map.insert i (tps, tSig) (types tm) } lookupPkgTypeMap :: [Ident] -> TcCont r TypeMap lookupPkgTypeMap is = lookupTypeOfN (Name is) <$> getTypeMap ------------------------------------------------------------------- -- Evaluating types evalReturnType :: Maybe Type -> TcCont r TcType evalReturnType = maybe (return voidT) evalSrcType evalSrcType :: Type -> TcCont r TcType evalSrcType (PrimType pt) = return $ TcPrimT pt evalSrcType (RefType rt) = TcRefT <$> evalSrcRefType rt evalSrcRefType :: RefType -> TcCont r TcRefType evalSrcRefType (TypeVariable i) = return $ TcTypeVar i evalSrcRefType (ArrayType t mp) = do ty <- evalSrcType t mpol <- maybe (return Nothing) (fmap Just . evalPolicy) mp return $ TcArrayT ty mpol evalSrcRefType (ClassRefType ct) = TcClsRefT <$> evalSrcClsType ct evalSrcClsType :: ClassType -> TcCont r TcClassType evalSrcClsType (ClassType iArgs) = TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs evalSrcTypeArg :: TypeArgument -> TcCont r TcTypeArg evalSrcTypeArg (ActualArg a) = evalSrcNWTypeArg a evalSrcTypeArg _ = fail "evalSrcTypeArg: Wildcards not yet supported" evalSrcNWTypeArg :: NonWildTypeArgument -> TcCont r TcTypeArg evalSrcNWTypeArg (ActualType rt) = TcActualType <$> evalSrcRefType rt evalSrcNWTypeArg (ActualPolicy p) = TcActualPolicy <$> evalPolicy p evalSrcNWTypeArg (ActualActor n) = TcActualActor <$> evalActorId n evalSrcNWTypeArg (ActualLockState ls) = TcActualLockState <$> mapM evalLock ls evalPolicy :: Exp -> TcCont r TcPolicy evalPolicy e = case e of ExpName n -> do --debug $ "evalPolicy: " ++ show n tm <- getTypeMap case lookupNamed policies n tm of Just p -> return p Nothing -> fail $ "evalPolicy: no such policy: " ++ prettyPrint n ++ "\nTypeMap: " ++ show (types tm) PolicyExp pl -> evalPolicyExp pl BinOp p1 Add p2 -> do pol1 <- evalPolicy p1 pol2 <- evalPolicy p2 return $ pol1 `meet` pol2 BinOp p1 Mult p2 -> do pol1 <- evalPolicy p1 pol2 <- evalPolicy p2 return $ pol1 `join` pol2 Paren p -> evalPolicy p _ -> fail "evalPolicy: More here!" evalPolicyExp :: PolicyExp -> TcCont r TcPolicy evalPolicyExp (PolicyLit cs) = TcPolicy <$> mapM evalClause cs evalPolicyExp (PolicyOf i) = return $ TcRigidVar i evalPolicyExp (PolicyTypeVar i) = return $ TcRigidVar i evalClause :: Clause Actor -> TcCont r (TcClause TcActor) evalClause (Clause h b) = do h' <- evalActor h b' <- mapM evalAtom b return $ TcClause h' b' evalActorName :: ActorName -> TcCont r ActorId evalActorName (ActorName n) = evalActorId n evalActorName (ActorTypeVar i) = return $ ActorTPVar i evalActor :: Actor -> TcCont r TcActor evalActor (Actor n) = TcActor <$> evalActorName n evalActor (Var i) = return $ TcVar i evalActorId :: Name -> TcCont r ActorId evalActorId n = do tm <- getTypeMap case lookupNamed actors n tm of Just aid -> return aid Nothing -> fail $ "evalActor: No such actor: " ++ prettyPrint n evalAtom :: Atom -> TcCont r TcAtom evalAtom (Atom n as) = TcAtom n <$> mapM evalActor as evalLock :: Lock -> TcCont r TcLock evalLock (Lock n ans) = do tm <- getTypeMap case lookupNamed lockArities n tm of Just arL -> do check (length ans == arL) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given " ++ show (length ans) Nothing -> fail $ "No such lock: " ++ prettyPrint n aids <- mapM getActor ans return $ TcLock n aids evalLock (LockVar i) = return $ TcLockVar i getActor :: ActorName -> TcCont r ActorId getActor (ActorName n) = do tm <- getTypeMap case lookupNamed actors n tm of Just aid -> return aid Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n getActor (ActorTypeVar i) = return $ ActorTPVar i -- From source fromSrcType :: TypeMap -> Type -> TcType fromSrcType tm (PrimType pt) = TcPrimT pt fromSrcType tm (RefType rt) = TcRefT $ fromSrcRefType tm rt fromSrcRefType :: TypeMap -> RefType -> TcRefType fromSrcRefType tm (ClassRefType ct) = TcClsRefT $ fromSrcClsType tm ct fromSrcRefType tm (ArrayType t mp) = TcArrayT (fromSrcType tm t) (fmap (fromSrcPolicy tm) mp) fromSrcRefType tm (TypeVariable i) = TcTypeVar i fromSrcClsType :: TypeMap -> ClassType -> TcClassType fromSrcClsType tm (ClassType iArgs) = TcClassT $ map (\(i,tas) -> (i, map (fromSrcTypeArg tm) tas)) iArgs -- Ignore wildcards for now fromSrcTypeArg :: TypeMap -> TypeArgument -> TcTypeArg fromSrcTypeArg tm (ActualArg a) = fromSrcArgument tm a fromSrcTypeArg tm _ = error "Wildcards not yet supported" fromSrcArgument :: TypeMap -> NonWildTypeArgument -> TcTypeArg fromSrcArgument tm (ActualType rt) = TcActualType $ fromSrcRefType tm rt fromSrcArgument tm (ActualPolicy p) = TcActualPolicy $ fromSrcPolicy tm p fromSrcArgument tm (ActualActor n) = TcActualActor $ fromSrcActorN tm n fromSrcArgument tm (ActualLockState ls) = TcActualLockState $ map (fromSrcLock tm) ls fromSrcLock :: TypeMap -> Lock -> TcLock fromSrcLock tm (LockVar i) = TcLockVar i fromSrcLock tm (Lock n ans) = let aids = map (fromSrcActorName tm) ans in TcLock n aids fromSrcActor :: TypeMap -> Actor -> TcActor fromSrcActor tm (Actor an) = TcActor $ fromSrcActorName tm an fromSrcActor tm (Var i) = TcVar i fromSrcActorName :: TypeMap -> ActorName -> ActorId fromSrcActorName tm (ActorName n) = fromSrcActorN tm n fromSrcActorName tm (ActorTypeVar i) = ActorTPVar i fromSrcActorN :: TypeMap -> Name -> ActorId fromSrcActorN tm n = case lookupNamed actors n tm of Just aid -> aid Nothing -> error "fromSrcActor: No such actor" fromSrcPolicy :: TypeMap -> Policy -> TcPolicy fromSrcPolicy tm (ExpName n) = case lookupNamed policies n tm of Just p -> p Nothing -> error "fromSrcPolicy: No such policy" fromSrcPolicy tm (PolicyExp e) = fromSrcPolicyExp tm e fromSrcPolicyExp :: TypeMap -> PolicyExp -> TcPolicy fromSrcPolicyExp tm (PolicyLit cs) = TcPolicy $ map (fromSrcClause tm) cs fromSrcPolicyExp tm (PolicyOf i) = TcRigidVar i fromSrcPolicyExp tm (PolicyTypeVar i) = TcRigidVar i fromSrcClause :: TypeMap -> Clause Actor -> TcClause TcActor fromSrcClause tm (Clause h b) = TcClause (fromSrcActor tm h) (map (fromSrcAtom tm) b) fromSrcAtom :: TypeMap -> Atom -> TcAtom fromSrcAtom tm (Atom n as) = TcAtom n $ map (fromSrcActor tm) as ------------------------------------------------------------------------------------- getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier] -> TcCont r TcPolicy getReadPolicy mods = case [pol |Reads pol <- mods ] of -- !!0 -- Read Policy? what if no read policy? [pol] -> evalPolicy pol [] -> return bottom getWritePolicy mods = case [pol | Writes pol <- mods] of [pol] -> evalPolicy pol [] -> return top getLockPolicy mods = case [pol | Reads pol <- mods] of [pol] -> evalPolicy pol [] -> return top getParamPolicy :: Ident -> [Modifier] -> TcCont r TcPolicy getParamPolicy i mods = case [pol | Reads pol <- mods ] of [pol] -> evalPolicy pol [] -> return $ ofPol i getReturnPolicy :: [Modifier] -> [TcPolicy] -> TcCont r TcPolicy getReturnPolicy mods pPols = case [pol | Reads pol <- mods ] of [pol] -> evalPolicy pol [] -> return $ foldl join bottom pPols ofPol :: Ident -> TcPolicy ofPol = TcRigidVar ------------------------------------------------------------ -- Subtyping (<:) :: TcType -> TcType -> TcCont r Bool -- Short-cut for the most common case. t1 <: t2 | t1 == t2 = return True -- Sub-typing for primitive types. TcPrimT pt1 <: TcPrimT pt2 = return $ pt1 <<: pt2 t1 <: t2 | isPolicyType t1 && t2 == policyT = return True | isLockType t1 && t2 == booleanT = return True | isActorType t1 && t2 == actorT = return True -- Sub-typing for reference types. -- - Null. TcRefT (TcClsRefT TcNullT) <: TcRefT _ = return True _ <: _ = return False (<<:) :: PrimType -> PrimType -> Bool ByteT <<: ShortT = True t <<: IntT = t `elem` [ShortT, ByteT, CharT] t <<: LongT = t == IntT || t <<: IntT t <<: FloatT = t == LongT || t <<: LongT t <<: DoubleT = t == FloatT || t <<: FloatT _ <<: _ = False {- | t1 == nullT && isRefType t2 = True | isLockType t1 && t2 == booleanT = True -- Should surely be more cases here | isPolicyType t1 && t2 == policyT = True -- When we add proper subtyping, it must also be in Tc | otherwise = False -} {- Graveyard lookupVar :: Name -> Tc r VarFieldSig lookupVar n = do tryVar n `orElse` tryField n `orElse` tryQual n `orElse` fail ("Unknown variable: " ++ prettyPrint n) where tryVar = tryVarField (vars <$> getEnv) tryField = tryVarField (fields <$> liftCont getTypeMap) --tryVarField :: Tc r (Map Ident VarFieldSig) -> Name -> Tc r (Maybe VarFieldSig) tryVarField recfetch (Name [i]) = do varMap <- recfetch case Map.lookup i varMap of Just vti -> if varType vti == actorT then -- We should check *which* actor do aid <- getActorId n return $ Just $ vti { varType = actorIdT aid } else if varType vti == policyT then do -- ... which policy pol <- getPolicy n return $ Just $ vti { varType = policyPolT pol } else return $ Just vti Nothing -> return Nothing tryVarField _ n = return Nothing tryQual n = do tm <- liftCont getTypeMap return $ lookupNamed fields n tm -}