{-# LANGUAGE TupleSections #-} module Language.Java.Paragon.TypeCheck.Monad ( check, checkM, ignore, orElse, maybeM, withFold, withFoldMap, getThisType, getReturn, extendVarEnvList, extendVarEnv, lookupVar, lookupActorName, -- lookupField, lookupFieldT, lookupMethod, lookupMethodT, lookupConstr, lookupLock, lookupExn, registerExn, registerExns, extendLockEnv, getBranchPC, getBranchPC_, extendBranchPC, addBranchPC, addBranchPCList, getActorId, setActorId, newActorId, newActorIdWith, newAliasId, freshActorId, aliasActorId, scrambleActors, getPolicy, getExnPC, throwExn, activateExns, deactivateExn, getExnState, mergeActiveExnStates, useExnState, getCurrentPC, getCurrentLockState, applyLockMods, openLock, closeLock, newMetaPolVar, constraint, constraintPC, constraintLS, 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.Verbosity --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 $ finePrint $ "DEBUG: " ++ str -- debug _ = return () 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 = do mRet <- returnI <$> getEnv case mRet of Nothing -> fail "Attempting to use 'return' in a simple expression context" Just ret -> return ret {- 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 nam@(Name _ n@(i:is)) = do tm <- liftCont getTypeMap -- debugTc $ show tm -- If a variable is involved, it can only appear as the first -- ident in the name, so account for that first. (mNewTm,ty,pol,rest) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of -- This is not a variable, so go for a field instead Nothing -> return (Just tm,voidT,bottom,n) -- This is a variable: see what the rest is Just (VSig ty p _ _) -> case is of [] -> return (Nothing, ty, p, []) _ -> do -- There's more, so the variable is -- being dereferenced let eTyTm = lookupTypeOfT ty tm case eTyTm of Right tyTm -> return (Just tyTm, ty, p, is) Left Nothing -> fail $ "Trying to dereference variable " ++ prettyPrint i ++ " but its type " ++ prettyPrint ty ++ " is not a (known) object type" Left (Just err) -> fail err case mNewTm of Nothing -> return (ty, pol) -- We're done Just newTm -> aux newTm ty pol rest -- Keep traversing the chain where aux :: TypeMap -> TcType -> TcPolicy -> [Ident ()] -> Tc r (TcType, TcPolicy) aux _ ty pol [] = return (ty, pol) aux tm _ pol (i:is) = do (mNewTm,newTy,newPol) <- case Map.lookup i (fields tm) of Just (VSig typ p _ _) -> do case is of [] -> return (Nothing, typ, p) _ -> do -- There's more, so the field is being dereferenced baseTm <- liftCont getTypeMap case lookupTypeOfT typ baseTm of Right tyTm -> return $ (Just tyTm, typ, p) Left Nothing -> fail $ "Trying to dereference variable " ++ prettyPrint i ++ " but its type " ++ prettyPrint typ ++ " is not a (known) object type" Left (Just err) -> fail err Nothing -> case Map.lookup i (locks tm) of Just (LSig pol ar) -> do check (ar == 0) $ "Lock " ++ prettyPrint i ++ " expects " ++ show ar ++ " arguments but has been given none." check (null is) $ "Trying to dereference lock " ++ prettyPrint i ++ " but locks cannot be dereferenced" return (Nothing, lockT [], pol) Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (Just aTm,voidT,bottom) Nothing -> fail failStr -- $ "lookupVar: No such name: " -- ++ prettyPrint name -- (Name () (i:is)) case mNewTm of Nothing -> return (newTy, pol `joinWThis` newPol) Just newTm -> aux newTm newTy (pol `joinWThis` newPol) is failStr = prettyPrint nam ++ " is not a known variable, field or lock" lookupMethod :: Name () -> [TcType] -> Tc r (Either (TcPolicy, [TypeParam ()], MethodSig) (TcPolicy, LockSig)) lookupMethod nam@(Name _ n@(i:is)) ts = do tm <- liftCont getTypeMap -- If a variable is involved, it can only appear as the first -- ident in the name, so account for that first. (mTy,newTm,pol,rest,allowPkgT) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of Just (VSig ty p _ _) -> do -- debugTc $ "Type found: " ++ prettyPrint ty let eTyTm = lookupTypeOfT ty tm case eTyTm of -- We found the variable, and it -- has an object type Right tyTm -> return (Just ty, tyTm, p, is, False) -- We found the variable, but its -- type is not derefereceable, or -- we don't know about it at all Left Nothing -> fail $ "Trying to dereference variable " ++ prettyPrint (Name () (init n)) ++ " but its type " ++ prettyPrint ty ++ " is not a (known) object type" Left (Just err) -> fail err Nothing -> return (Nothing,tm,bottom,n,True) aux mTy newTm allowPkgT pol rest ts where aux :: Maybe TcType -- Type of parent if any (for error reporting) -> TypeMap -- Typemap of parent, or top-level -> Bool -- If True, still ok to check for pkgs/types -> TcPolicy -- Accumulated policy of chain up to here -> [Ident ()] -- Remaining links in ident chain -> [TcType] -- Types of method arguments -> Tc r (Either (TcPolicy, [TypeParam ()], MethodSig) -- For methods (TcPolicy, LockSig)) -- For locks -- The remaining idents in the name must all be fields, -- except the last one which must denote a method or lock name aux mTy tm _ pol [i] ts = -- This must be the method 'i' with arguments 'ts', -- or the lock 'i' with actor arguments 'ts' case Map.lookup (i,ts) (methods tm) of Just (tps, mti) -> return $ Left (pol, tps, mti) Nothing -> -- Only remaining alternative is a lock case Map.lookup i (locks tm) of Just lsig -> return $ Right (pol, lsig) _ -> fail $ "Cannot find method " ++ prettyPrint i ++ maybe "" (\ty -> " in class " ++ prettyPrint ty) mTy aux mTy tm allowPkgT pol (i:is) ts = do -- 'i' is not the last link in the chain, -- hence must be a field (or pkg/type) (newMTy,newTm,newPol,stillAllowPkgT) <- case Map.lookup i (fields tm) of Just (VSig typ pol _ _) -> do -- field exists, so find its related typemap baseTm <- liftCont getTypeMap case lookupTypeOfT typ baseTm of Right newTm -> return $ (Just typ, newTm, pol, False) Left Nothing -> fail $ "Trying to dereference field " ++ prettyPrint i ++ maybe "" (\ty -> " of class " ++ prettyPrint ty) mTy ++ " but its type " ++ prettyPrint typ ++ " is not a (known) object type" Nothing -> if allowPkgT then case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (Nothing, aTm, bottom, True) Nothing -> fail $ -- couldn't find field, pkg or type case mTy of Just ty -> fail "Internal error: lookupMethod: Please report as a bug!" _ -> fail $ "Unknown type or field " ++ prettyPrint i -- "lookupTypeOfN: No such name: " ++ prettyPrint i else fail $ case mTy of Nothing -> "Unknown field " ++ prettyPrint i Just ty -> "Type " ++ prettyPrint ty ++ " does not have a field " ++ prettyPrint i aux newMTy newTm stillAllowPkgT (pol `joinWThis` 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 (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ eATm <- lookupTypeOfT typ <$> liftCont getTypeMap case eATm of Left (Just err) -> fail err Left Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ Right aTm -> case Map.lookup i (fields aTm) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a field " ++ prettyPrint i lookupMethodT :: TcType -> Ident () -> [TcType] -> Tc r ([TypeParam ()], MethodSig) lookupMethodT typ i pts = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ eATm <- lookupTypeOfT typ <$> liftCont getTypeMap case eATm of Left (Just err) -> fail err Left Nothing -> fail $ "Unknown reference type: " ++ prettyPrint typ Right aTm -> case Map.lookup (i,pts) (methods aTm) of Just pmti -> return pmti Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a method " ++ prettyPrint i lookupConstr :: TcClassType -> [TcType] -> Tc r ([TypeParam ()], ConstrSig) lookupConstr ctyp pts = do eATm <- lookupTypeOfT (clsTypeToType ctyp) <$> liftCont getTypeMap case eATm of Left (Just err) -> fail err Left Nothing -> fail $ "Unknown class type: " ++ prettyPrint ctyp Right aTm -> case Map.lookup pts (constrs aTm) of Just pcti -> return pcti Nothing -> fail $ "Class " ++ prettyPrint ctyp ++ " does not have a constructor matching argument types " ++ "(" ++ concat (intersperse ", " (map prettyPrint pts)) ++ ")" lookupLock :: Name () -> Tc r LockSig lookupLock n = do tm <- liftCont getTypeMap -- debugTc $ show tm case lookupNamed locks n tm of Nothing -> fail $ "Unknown lock: " ++ prettyPrint n Just lsig -> return lsig 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, String)] getBranchPC e = do env <- getEnv -- debugTc $ "Env: " ++ show env return $ branchPC (Just e) env getBranchPC_ :: Tc r [(TcPolicy, String)] getBranchPC_ = do env <- getEnv return $ branchPC Nothing env extendBranchPC :: TcPolicy -> String -> Tc r a -> Tc r a extendBranchPC p str = withEnv $ joinBranchPC p str 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])) [] m) bm is in env { branchPCE = (newBm, def) } addBranchPC :: Entity -> Tc r a -> Tc r a addBranchPC ent = withEnv $ \env -> let (bm, def) = branchPCE env newBm = Map.insert ent [] bm in env { branchPCE = (newBm, def) } getCurrentPC :: Entity -> Tc r TcPolicy getCurrentPC ent = do bpcs <- fst . unzip <$> getBranchPC ent epcs <- fst . unzip <$> getExnPC return $ foldl join bottom (bpcs ++ epcs) {-- 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 (prettyPrint i) newActorIdWith i aid return aid newAliasId :: Ident () -> Tc r ActorId newAliasId i = do aid <- liftCont aliasActorId newActorIdWith i aid return aid freshActorId :: String -> TcCont r ActorId freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef aliasActorId :: TcCont r ActorId 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, String)] 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 -> String -> Tc r () constraint ls p1 p2 str = 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 str {- $ "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 str where rls = locksToRec ls getGlobalLockProps :: Tc r TcPolicyRec getGlobalLockProps = return (TcPolicyRec []) locksToRec :: [TcLock] -> TcPolicyRec locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls)) constraintLS :: TcPolicy -> TcPolicy -> String -> Tc r () constraintLS p1 p2 str = do l <- getCurrentLockState withErrCtxtTc ("In the context of lock state: " ++ prettyPrint l ++ "\n") $ constraint l p1 p2 str constraintPC :: [(TcPolicy, String)] -> TcPolicy -> (TcPolicy -> String -> String) -> Tc r () constraintPC bpcs pW msgf = mapM_ (uncurry $ constraintPC_ pW msgf) bpcs where constraintPC_ :: TcPolicy -> (TcPolicy -> String -> String) -> TcPolicy -> String -> Tc r () -- Don't take lock state into account constraintPC_ pW msgf pPC src = constraint [] pPC pW (msgf pPC src) exnConsistent :: Either (Name ()) (ClassType ()) -> TcType -> ExnSig -> Tc r () exnConsistent caller exnTy (ExnSig rX wX _) = do exnMap <- exnsE <$> getEnv --debugTc $ "Using exnMap: " ++ show exnMap let (callerName, callerSort) = case caller of Left n -> (prettyPrint n , "method" ) Right ct -> (prettyPrint ct, "constructor") case Map.lookup exnTy exnMap of Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy) Just (rE, wE) -> do constraint [] wX wE $ "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++ callerSort ++ " " ++ callerName ++ ", has write effect " ++ prettyPrint wX ++ " but the context in which the " ++ callerSort ++ " is invoked expects its write effect to be no less restrictive than " ++ prettyPrint wE constraint [] rE rX $ -- constraintLS? "Exception " ++ prettyPrint exnTy ++ ", thrown by invocation of " ++ callerSort ++ " " ++ callerName ++ ", has policy " ++ prettyPrint rX ++ " but the context in which the " ++ callerSort ++ " is invoked expects its policy to be no less restrictive than " ++ prettyPrint rE -------------------------------------------- -- 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 = do eTm <- lookupTypeOfN (Name () is) <$> getTypeMap case eTm of Right tm -> return tm Left _ -> fail $ "Unknown package: " ++ prettyPrint (Name () is) ------------------------------------------------------------------- -- 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 mps) = do ty <- evalSrcType t pols <- mapM (maybe (return bottom) evalPolicy) mps let (TcRefT arrTy) = mkArrayType ty pols return arrTy evalSrcRefType (ClassRefType _ ct) = TcClsRefT <$> evalSrcClsType ct evalSrcClsType :: ClassType () -> TcCont r TcClassType evalSrcClsType ct@(ClassType _ iArgs) = do debug $ "Evaluating class type: " ++ show ct baseTm <- getTypeMap debug $ "Current type map: " ++ show baseTm TcClassT <$> aux baseTm [] iArgs where aux :: TypeMap -- Typemap of outer type (or top-level) -> [(Ident (), [TcTypeArg])] -- Accumulated type (reversed) -> [(Ident (), [TypeArgument ()])] -- Type to traverse -> TcCont r [(Ident (), [TcTypeArg])] -- Result (re-reversed) aux _ accTy [] = return $ reverse accTy aux tm accTy ((i,tas):rest) = do debug $ "Looking up type: " ++ show i debug $ "Types field: " ++ show (types tm) (newTm, tArgs) <- case Map.lookup i (types tm) of Just (pars, tsig) -> do debug $ "Type found" tArgs <- mapM (uncurry evalSrcTypeArg) (zip pars tas) debug "Type arguments evaluated" return (instantiate (zip pars tArgs) (tMembers tsig), tArgs) Nothing -> case Map.lookup i (packages tm) of Just tm -> do check (null tas) $ "Packages cannot have type arguments" return (tm, []) Nothing -> fail $ "Unknown type: " ++ prettyPrint i debug $ "Rest of type to evaluate: " ++ show rest aux newTm ((i,tArgs):accTy) rest -- TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs evalSrcTypeArg :: TypeParam () -> TypeArgument () -> TcCont r TcTypeArg evalSrcTypeArg tp (ActualArg _ a) = evalSrcNWTypeArg tp a evalSrcTypeArg _ _ = fail "evalSrcTypeArg: Wildcards not yet supported" evalSrcNWTypeArg :: TypeParam () -> NonWildTypeArgument () -> TcCont r TcTypeArg -- Types may be names or types -- TODO: Check bounds evalSrcNWTypeArg tp@(TypeParam {}) (ActualName _ (Name _ is)) = do TcActualType . TcClsRefT <$> evalSrcClsType (ClassType () $ map (,[]) is) evalSrcNWTypeArg (TypeParam {}) (ActualType _ rt) = TcActualType <$> evalSrcRefType rt -- Actors may only be names -- TODO: must be final evalSrcNWTypeArg (ActorParam {}) (ActualName _ n) = TcActualActor <$> evalActorId n -- Policies may be names, or special expressions -- TODO: names must be final evalSrcNWTypeArg (PolicyParam {}) (ActualName _ n) = TcActualPolicy <$> evalPolicy (ExpName () n) evalSrcNWTypeArg (PolicyParam {}) (ActualExp _ e) = TcActualPolicy <$> evalPolicy e -- Lock states must be locks evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls evalSrcNWTypeArg tp nwta = fail $ "Trying to instantiate type parameter " ++ prettyPrint tp ++ " with incompatible type argument " ++ prettyPrint nwta {- 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 (PolicyThis _) = return $ TcThis evalPolicyExp (PolicyTypeVar _ i) = return $ TcRigidVar i evalClause :: Clause () -> 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 locks n tm of Just lsig -> do check (length ans == lArity lsig) $ "Lock " ++ prettyPrint n ++ " expects " ++ show (lArity lsig) ++ " 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 mps) = let pols = map (maybe bottom (fromSrcPolicy tm)) mps (TcRefT arrT) = mkArrayType (fromSrcType tm t) pols in arrT 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 () -> 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 -}