{-# LANGUAGE TupleSections, PatternGuards #-} module Language.Java.Paragon.TypeCheck.Monad ( {- check, checkM, ignore, orElse, maybeM, withFold, withFoldMap, getReturn, extendVarEnvList, extendVarEnv, lookupPrefixName, 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, -} module Language.Java.Paragon.TypeCheck.Monad.TcCodeM, module Language.Java.Paragon.TypeCheck.Monad, {- debug, debugTc, solve -} ) where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction --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.Monad.Uniq import Language.Java.Paragon.TypeCheck.Monad.TcDeclM import Language.Java.Paragon.TypeCheck.Monad.TcCodeM import Language.Java.Paragon.TypeCheck.Monad.CodeEnv import Language.Java.Paragon.TypeCheck.Monad.CodeState import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.TypeMap import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Containment import Language.Java.Paragon.TypeCheck.Constraints import Control.Monad (filterM, zipWithM) import Control.Applicative ( (<$>), (<*>) ) --import Control.Arrow ( first, second ) import qualified Data.Map as Map import Data.IORef import Data.List (union, intersperse) --debug :: String -> TcDeclM r () --debug str = liftIO $ finePrint $ "DEBUG: " ++ str --debugTc :: String -> TcCodeM r () --debugTc = liftTcDeclM . debug monadModule :: String monadModule = typeCheckerBase ++ ".Monad" -------------------------------------------- -- Working with the env -- -------------------------------------------- -- this --getThisType :: TcCodeM r TcType --getThisType = liftCont getThisT -- returns getReturn :: TcCodeM r (TcType, ActorPolicy) 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 -> TcCodeM r a -> TcCodeM r a registerReturn ty p = withEnv $ \env -> env { returnI = (ty,p) } -} -- lookup entities --fieldEnvToVars :: TcCodeM r a -> TcCodeM r a --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) } extendVarEnvList :: [(Ident (), VarFieldSig)] -> TcCodeM r a -> TcCodeM 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 -> TcCodeM r a -> TcCodeM r a --extendVarEnv i = extendVarEnvN i --extendVarEnvN :: Ident -> VarFieldSig -> TcCodeM r a -> TcCodeM r a extendVarEnv i vti = withEnv $ \env -> let oldVmap = vars env newVmap = Map.insert i vti oldVmap in env { vars = newVmap } lookupActorName :: ActorName () -> TcCodeM r (TcType, ActorPolicy) lookupActorName (ActorName _ nam@(Name _ nt mPre i)) | nt == EName = do (ty, pol, _) <- lookupVar mPre i return (ty, pol) | otherwise = panic (monadModule ++ ".lookupActorName") $ "Not an EName: " ++ show nam lookupActorName (ActorTypeVar _ i) = do (ty, pol, _) <- lookupVar Nothing i return (ty, pol) lookupActorName n = panic (monadModule ++ ".lookupActorName") $ "Unexpected AntiQName: " ++ show n -- | Lookup the prefix part of a name, which has to be dereferenceable. -- Returns the relevant type (Nothing if package), its typemap -- and the accumulated policy of the name access path. lookupPrefixName :: Name () -> TcCodeM r (Maybe TcType, TypeMap, ActorPolicy) lookupPrefixName n@(Name _ EName Nothing i) = do -- Special case: This *could* be a var, since those can only -- appear first in the name, i.e. prefix == Nothing -- We can piggyback on lookupVar since its preconditions are met (ty, p, _) <- lookupVar Nothing i tm <- getTypeMap case lookupTypeOfT ty tm of Right newSig -> return (Just ty, tMembers newSig, p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown variable or field: " ++ show n lookupPrefixName n@(Name _ nt mPre i) = do baseTm <- getTypeMap (preTm, prePol) <- case mPre of Nothing -> do return (baseTm, bottom) Just pre -> do (_, preTm, prePol) <- lookupPrefixName pre return (preTm, prePol) baseTm2 <- getTypeMap case nt of EName -> case Map.lookup i $ fields preTm of Just (VSig ty p _ _ _) -> do debugPrint $ "lookupPrefixName: EName: " ++ prettyPrint n ++ " :: " ++ prettyPrint ty debugPrint $ show (packages baseTm2) ++ "\n" case lookupTypeOfT ty baseTm2 of Right tsig -> return (Just ty, tMembers tsig, prePol `joinWThis` p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown type: " ++ show ty Nothing -> panic (monadModule ++ ".lookupPrefixName") $ "Not a field: " ++ show n TName -> do (tps, tsig) <- case Map.lookup i $ types preTm of Nothing -> liftTcDeclM $ fetchType n -- panic (monadModule ++ ".lookupPrefixName") -- $ "Not a type: " ++ show n Just tinfo -> return tinfo check (null tps) $ "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++ " but has been given none." return (Just $ TcRefT $ tType tsig, tMembers tsig, prePol) PName -> case Map.lookup i $ packages preTm of Nothing -> do liftTcDeclM $ fetchPkg n return (Nothing, emptyTM, prePol) -- panic (monadModule ++ ".lookupPrefixName") -- $ "Not a package: " ++ show n Just tm -> return (Nothing, tm, prePol) _ -> panic (monadModule ++ ".lookupPrefixName") $ "Malformed prefix name: " ++ show n lookupPrefixName n = panic (monadModule ++ ".lookupPrefixName") $ "Malformed prefix name: " ++ show n -- | Lookup the type and policy of a field or variable access path. -- Precondition: Name is the decomposition of an EName lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM r (TcType, ActorPolicy, Bool) lookupVar Nothing i = do -- Could be a single variable varMap <- vars <$> getEnv case Map.lookup i varMap of -- Is a variable Just (VSig ty p param _ _) -> return (ty, p, param) -- Not a variable, must be a field Nothing -> do tm <- getTypeMap case Map.lookup i $ fields tm of Just (VSig ty p _ _ _) -> return (ty, p, False) Nothing -> panic (monadModule ++ ".lookupVar") $ "Not a var or field: " ++ show i lookupVar (Just pre) i = do (mPreTy, preTm, prePol) <- lookupPrefixName pre case Map.lookup i $ fields preTm of Just (VSig ty p _ _ _) -> return (ty, prePol `joinWThis` p, False) Nothing -> case mPreTy of Just preTy -> fail $ "Type " ++ prettyPrint preTy ++ " does not have a field named " ++ prettyPrint i Nothing -> panic (monadModule ++ ".lookupVar") $ "EName as direct child of PName: " ++ show (Name () EName (Just pre) i) type Sig = ([TypeParam ()], [TcType], Bool) findBestMethod :: [TypeArgument ()] -> [TcType] -> [Sig] -- Works for both methods and constrs -> TcCodeM r [Sig] findBestMethod tArgs argTys candidates = findBestFit =<< filterM isApplicable candidates where isApplicable :: Sig -> TcCodeM r Bool isApplicable (tps, pTys, isVA) = (&&) <$> checkArgs tps tArgs <*> checkTys isVA pTys argTys checkArgs :: [TypeParam ()] -> [TypeArgument ()] -> TcCodeM r Bool checkArgs [] [] = return True checkArgs (tp:tps) (ta:tas) = (&&) <$> checkArg tp ta <*> checkArgs tps tas checkArgs _ _ = return False checkArg :: TypeParam () -> TypeArgument () -> TcCodeM r Bool checkArg _ _ = return True -- TODO: Type arguments not yet handled correctly checkTys _ [] [] = return True checkTys b ps as | not b && length ps /= length as = return False | b && length ps > length as + 1 = return False checkTys True [p] [a] = (p =<: a) `orM` (arrayType p bottom =<: a) checkTys True [p] as = and <$> mapM (p =<:) as checkTys b (p:ps) (a:as) = (&&) <$> (p =<: a) <*> checkTys b ps as checkTys _ _ _ = return False findBestFit :: [Sig] -> TcCodeM r [Sig] findBestFit [] = return [] findBestFit (x:xs) = go [x] xs go :: [Sig] -> [Sig] -> TcCodeM r [Sig] go xs [] = return xs go xs (y:ys) = do bs0 <- mapM (\x -> y `moreSpecificThan` x) xs if and bs0 then go [y] ys else do bs1 <- mapM (\x -> x `moreSpecificThan` y) xs if and bs1 then go xs ys else go (y:xs) ys moreSpecificThan :: Sig -> Sig -> TcCodeM r Bool moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (=<:) ps2 ps1 moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do let n = length ps1 k = length ps2 undefined n k moreSpecificThan _ _ = undefined -- | Lookup the signature of a method, and the policy of its access path. lookupMethod :: Maybe (Name ()) -- Access path -> Ident () -- Method name -> [TypeArgument ()] -- Type arguments -> [TcType] -- Argument types -> TcCodeM r (ActorPolicy, [TypeParam ()], MethodSig) lookupMethod mPre i tArgs argTys = do baseTm <- getTypeMap (mPreTy, preTm, prePol) <- case mPre of Nothing -> return (Nothing, baseTm, bottom) Just pre -> lookupPrefixName pre case Map.lookup i $ methods preTm of Nothing -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " does not have a method named " ++ prettyPrint i Nothing -> "No method named " ++ prettyPrint i ++ " is in scope" Just methodMap -> do bests <- findBestMethod tArgs argTys (Map.keys methodMap) case bests of [] -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " does not have a method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" Nothing -> "No method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ") is in scope" (_:_:_) -> fail $ case mPreTy of Just preTy -> "Type " ++ prettyPrint preTy ++ " has more than one most specific method " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" Nothing -> "More than one most specific method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ") is in scope" [sig@(tps, _, _)] -> case Map.lookup sig methodMap of Nothing -> panic (monadModule ++ ".lookupMethod") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> return (prePol, tps, msig) -- | Lookup the signature of a lock -- note that all locks are static, -- so the policy of the access path is irrelevant. lookupLock :: Maybe (Name ()) -- Access path -> Ident () -- Name of lock -> TcCodeM r LockSig lookupLock mPre i = do baseTm <- getTypeMap preTm <- case mPre of Nothing -> return baseTm Just pre -> do (_, preTm, _) <- lookupPrefixName pre return preTm case Map.lookup i $ locks preTm of Just lsig -> return lsig Nothing -> panic (monadModule ++ ".lookupLock") $ "Not a lock: " ++ show (Name () LName mPre i) getPolicy :: Name () -> TcCodeM r ActorPolicy getPolicy n = do tm <- getTypeMap case lookupNamed policies n tm of Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n Just p -> return p lookupFieldT :: TcType -> Ident () -> TcCodeM r VarFieldSig lookupFieldT typ i = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ aSig <- lookupTypeOfType typ case Map.lookup i (fields $ tMembers aSig) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a field named " ++ prettyPrint i lookupMethodT :: TcType -> Ident () -> [TypeArgument ()] -> [TcType] -> TcCodeM r ([TypeParam ()], MethodSig) lookupMethodT typ i tArgs argTys = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ aSig <- lookupTypeOfType typ case Map.lookup i (methods $ tMembers aSig) of Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a method named " ++ prettyPrint i Just mMap -> do bests <- findBestMethod tArgs argTys (Map.keys mMap) case bests of [] -> fail $ "Type " ++ prettyPrint typ ++ " does not have a method named " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" (_:_:_) -> fail $ "Type " ++ prettyPrint typ ++ " has more than one most specific method " ++ prettyPrint i ++ " matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" [sig@(tps, _, _)] -> case Map.lookup sig mMap of Nothing -> panic (monadModule ++ ".lookupMethodT") $ "Sig must be one of the keys of methodMap: " ++ show sig Just msig -> return (tps, msig) lookupConstr :: TcClassType -> [TypeArgument ()] -> [TcType] -> TcCodeM r ([TypeParam ()], ConstrSig) lookupConstr ctyp tArgs argTys = do debugPrint $ "\n\n######## Looking up constructor! ######## \n" let typ = clsTypeToType ctyp debugPrint $ "typ: " ++ show typ aSig <- lookupTypeOfType typ debugPrint $ "aSig: " ++ show aSig let cMap = constrs $ tMembers aSig debugPrint $ "cMap: " ++ show cMap bests <- findBestMethod tArgs argTys (Map.keys cMap) case bests of [] -> fail $ "Type " ++ prettyPrint ctyp ++ " does not have a constructor \ \matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" (_:_:_) -> fail $ "Type " ++ prettyPrint ctyp ++ " has more than one most specific \ \constructor matching argument types (" ++ (unwords $ intersperse ", " $ map prettyPrint argTys) ++ ")" [sig@(tps,_,_)] -> case Map.lookup sig cMap of Nothing -> panic (monadModule ++ ".lookupConstr") $ "Sig must be one of the keys of constrMap: " ++ show sig Just csig -> return (tps, csig) --lookupLock :: Name () -> TcCodeM r LockSig --lookupLock n = do -- tm <- getTypeMap -- -- debugTcCodeM $ show tm -- case lookupNamed locks n tm of -- Nothing -> fail $ "Unknown lock: " ++ prettyPrint n -- Just lsig -> return lsig lookupExn :: TcType -> TcCodeM r (ActorPolicy, ActorPolicy) 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 -> ActorPolicy -> ActorPolicy -> TcCodeM r a -> TcCodeM r a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] registerExns :: [(TcType, (ActorPolicy, ActorPolicy))] -> TcCodeM r a -> TcCodeM 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] -> TcCodeM r a -> TcCodeM r a extendLockEnv locs = withEnv $ \env -> env { lockstate = lockstate env `union` locs } getBranchPC :: Entity -> TcCodeM r [(ActorPolicy, String)] getBranchPC e = do env <- getEnv -- debugTcCodeM $ "Env: " ++ show env return $ branchPC (Just e) env getBranchPC_ :: TcCodeM r [(ActorPolicy, String)] getBranchPC_ = do env <- getEnv return $ branchPC Nothing env extendBranchPC :: ActorPolicy -> String -> TcCodeM r a -> TcCodeM r a extendBranchPC p str = withEnv $ joinBranchPC p str addBranchPCList :: [Ident ()] -> TcCodeM r a -> TcCodeM r a addBranchPCList is = withEnv $ \env -> let (bm, def) = branchPCE env newBm = foldl (\m i -> Map.insert (VarEntity (mkSimpleName EName i)) [] m) bm is in env { branchPCE = (newBm, def) } addBranchPC :: Entity -> TcCodeM r a -> TcCodeM r a addBranchPC ent = withEnv $ \env -> let (bm, def) = branchPCE env newBm = Map.insert ent [] bm in env { branchPCE = (newBm, def) } getCurrentPC :: Entity -> TcCodeM r ActorPolicy 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 -> TcCodeM 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 -> TcCodeM r () setMethodPols i retM -} -------------------------------------------- -- Working with states -- -------------------------------------------- {- -- Leave actor mappings from fields startState :: TcCodeM r () startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -} -- Actor Analysis getActorId :: Name () -> TcCodeM r ActorId getActorId n = do actorMap <- actorSt <$> getState case Map.lookup n actorMap of Nothing -> liftTcDeclM $ aliasActorId Just ai -> return $ aID ai setActorId :: Name () -> ActorId -> TcCodeM r () setActorId n aid = updateState setAct where setAct :: CodeState -> CodeState setAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap } replId (AI _ st) = AI aid st newActorIdWith :: Ident () -> ActorId -> TcCodeM r () newActorIdWith i aid = do updateState insertAct where insertAct :: CodeState -> CodeState insertAct s@(CodeState { actorSt = actMap }) = s { actorSt = Map.insert (mkSimpleName EName i) (AI aid Stable) actMap } newActorId :: Ident () -> TcCodeM r ActorId newActorId i = do aid <- liftTcDeclM $ freshActorId (prettyPrint i) newActorIdWith i aid return aid newAliasId :: Ident () -> TcCodeM r ActorId newAliasId i = do aid <- liftTcDeclM aliasActorId newActorIdWith i aid return aid scrambleActors :: Maybe TcType -> TcCodeM r () scrambleActors mtc = do let stb = maybe FullV (FieldV . Just . typeName_) mtc state <- getState u <- getUniqRef newState <- liftIO $ scramble u stb state setState newState -- Exception tracking getExnPC :: TcCodeM r [(ActorPolicy, String)] getExnPC = exnPC <$> getState throwExn :: ExnType -> ActorPolicy -> TcCodeM r () throwExn et pX = do uref <- getUniqRef state <- getState let oldXmap = exnS state newXmap = Map.fromList [(et, ExnPoint state pX)] mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } deactivateExn :: ExnType -> TcCodeM r () deactivateExn et = updateState $ \s -> let oldEmap = exnS s newEmap = Map.delete et oldEmap in s { exnS = newEmap } activateExns :: [(ExnType, ExnSig)] -> TcCodeM r () activateExns exns = do uref <- getUniqRef state <- getState let (ts, sigs) = unzip exns xPoints <- mapM (\sigX -> do s <- 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 <- liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } getExnState :: ExnType -> TcCodeM r (Maybe CodeState) getExnState et = do eMap <- exnS <$> getState return $ epState <$> Map.lookup et eMap mergeActiveExnStates :: TcCodeM r () mergeActiveExnStates = do exnMap <- exnS <$> getState mapM_ (mergeWithState . epState) $ Map.elems exnMap useExnState :: CodeState -> TcCodeM r () useExnState es = updateState (\s -> s { exnS = exnS es }) -- Lockstate tracking getCurrentLockState :: TcCodeM r [TcLock] getCurrentLockState = do base <- lockstate <$> getEnv mods <- lockMods <$> getState return $ snd $ ([], base) ||>> mods applyLockMods :: LockMods -> TcCodeM r () applyLockMods lms = do updateState $ \s -> s { lockMods = lockMods s ||>> lms } openLock, closeLock :: TcLock -> TcCodeM r () openLock l = applyLockMods ([],[l]) closeLock l = applyLockMods ([l],[]) -- Policy inference newMetaPolVar :: TcCodeM r ActorPolicy newMetaPolVar = do uniq <- liftIO . getUniq =<< getUniqRef ref <- liftIO (newIORef Nothing) return $ VarPolicy (TcMetaVar uniq ref) --newRigidPolVar :: TcCodeM r TcPolicy --newRigidPolVar = do -- uniq <- lift . getUniq =<< getUniqRef -- return $ TcRigidVar uniq -------------------------------------------- -- Working with constraints -- -------------------------------------------- constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM r () constraint ls p q str = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps case lrt g ls p q 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 getGlobalLockProps :: TcCodeM r (PrgPolicy TcAtom) getGlobalLockProps = do cs <- go <$> getTypeMap debugPrint $ "Fetching global lock props: " ++ show cs return $ TcPolicy cs where go :: TypeMap -> [TcClause TcAtom] go tm = let lps = map lProps $ Map.elems $ locks tm tlps = map (go . tMembers . snd) $ Map.elems $ types tm plps = map go $ Map.elems $ packages tm in concat $ lps ++ tlps ++ plps locksToRec :: [TcLock] -> (PrgPolicy TcAtom) locksToRec ls = TcPolicy (map (\x -> TcClause x []) (map lockToAtom ls)) constraintLS :: ActorPolicy -> ActorPolicy -> String -> TcCodeM r () constraintLS p1 p2 str = do l <- getCurrentLockState withErrCtxt ("In the context of lock state: " ++ prettyPrint l ++ "\n") $ constraint l p1 p2 str constraintPC :: [(ActorPolicy, String)] -> ActorPolicy -> (ActorPolicy -> String -> String) -> TcCodeM r () constraintPC bpcs pW msgf = mapM_ (uncurry constraintPC_) bpcs where constraintPC_ :: ActorPolicy -> String -> TcCodeM r () -- Don't take lock state into account constraintPC_ pPC src = constraint [] pPC pW (msgf pPC src) exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM 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 ------------------------------------------------------------ -- Subtyping/conversion/promotion -- Note that we do NOT allow unchecked conversion or capture conversion. -- We don't give crap about backwards compatibility here, and even if we -- did, we would have to rule it out because it would be unsound. isAssignableTo, (=<:) :: (Monad (m r), MonadTcDeclM m) => TcType -> TcType -> m r Bool isAssignableTo t1 t2 = liftTcDeclM $ if t1 == t2 -- identity conversion then return True else t1 `widensTo` t2 -- widening conversion (=<:) = flip isAssignableTo isCastableTo, (<<:) :: (Monad (m r), MonadTcDeclM m) => TcType -> TcType -> m r (Bool, Bool) -- (Can be cast, needs reference narrowing) isCastableTo t1 t2 = liftTcDeclM $ do -- 'isAssignableTo' handles the cases of identity, primitive widening, -- boxing + reference widening and unboxing + primitive widening. -- It also handles reference widening, but not with subsequent unboxing. b <- isAssignableTo t1 t2 if b then return (True, False) else do -- What we have left is primitive narrowing, primitive widening+narrowing, -- reference widening + unboxing, and reference narrowing + optional unboxing. -- Only the last one, that includes reference narrowing, can throw a ClassCastException. case (t1, t2) of (TcPrimT pt1, TcPrimT pt2) -> -- primitive (widening +) narrowing return $ (pt2 `elem` narrowConvert pt1 ++ widenNarrowConvert pt1, False) (TcRefT rt1, TcPrimT pt2) | Just ct2 <- box pt2 -> do -- reference widening + unboxing AND -- reference narrowing + unboxing -- We cheat and compare to the boxing of the target instead -- since box/unbox are inverses. let rt2 = TcClsRefT ct2 bWide <- rt1 `subTypeOf` rt2 if bWide then return (True, False) else return (True, True) (TcRefT _rt1, TcRefT _rt2) -> do -- reference narrowing, no unboxing -- TODO: There are restrictions here, but not relevant at this point return (True, True) _ -> return (False, False) (<<:) = flip isCastableTo -- widening conversion can come in four basic shapes: -- 1) pt/pt -> widening primitive conversion -- 2) rt/rt -> widening reference conversion -- 3) pt/rt -> boxing conversion + widening reference conversion -- 4) rt/pt -> unboxing conversion + widening primitive conversion widensTo :: TcType -> TcType -> TcDeclM r Bool widensTo (TcPrimT pt1) (TcPrimT pt2) = return $ pt2 `elem` widenConvert pt1 widensTo (TcRefT rt1) (TcRefT rt2) = rt1 `subTypeOf` rt2 widensTo (TcPrimT pt1) t2@(TcRefT _) = maybe (return False) (\ct -> clsTypeToType ct `widensTo` t2) (box pt1) widensTo (TcRefT rt1) t2@(TcPrimT _) = case rt1 of TcClsRefT ct -> maybe (return False) (\pt -> TcPrimT pt `widensTo` t2) (unbox ct) _ -> return False -- 5) Paragon-specific types widensTo t1 t2 | isPolicyType t1 && t2 == policyT = return True | isLockType t1 && t2 == booleanT = return True | isActorType t1 && t2 == actorT = return True widensTo _ _ = return False subTypeOf :: TcRefType -> TcRefType -> TcDeclM r Bool subTypeOf TcNullT _ = return True subTypeOf rt1 rt2 = (rt2 `elem`) <$> ([TcClsRefT objectT] ++) <$> superTypes rt1 where superTypes :: TcRefType -> TcDeclM r [TcRefType] superTypes rt = do tm <- getTypeMap tsig <- case lookupTypeOfRefT rt tm of Left Nothing -> do case rt of TcClsRefT (TcClassT n tas) -> do (tps, tsig) <- fetchType n return $ instantiate (zip tps tas) tsig _ -> panic (monadModule ++ ".subTypeOf") $ show rt Left err -> panic (monadModule ++ ".subTypeOf") $ "Looking up type:" ++ show rt ++ "\nError: " ++ show err Right tsig -> return tsig let sups = tSupers tsig impls = tImpls tsig -- obj = if null sups then [objectT] else [] allS = map TcClsRefT $ sups ++ impls -- ++ obj supsups <- mapM superTypes allS return $ concat $ allS:supsups ------------------------------------------ -- Constraints resolution -- ------------------------------------------ -- Resolution thanks to the transitive closure. solve :: MonadIO m => [ConstraintWMsg] -> m () solve cs = liftIO $ do let wcs = [c | (c, _) <- cs] --Extract constraints wcs' = concat $ map splitCstrs wcs --Split them : (Join p q <= r)<=>((p<=r)/\(q<=r)) cvars <- filterM isCstrVar wcs' --Get the "p<=X" constraints, X MetaVar let cvarsm = foldl linker Map.empty cvars --Map to X the list of p s.t. p<=X csubsts = Map.foldrWithKey --Realize the substitutions (\x pxs cs' -> foldr (\px cs'' -> substitution x px cs'') cs' pxs) wcs' cvarsm (_toInfer, ccstright) <- partitionM isCstrVar csubsts toBeChecked <- filterM noVarLeft ccstright mapM_ (checkCstr ("The system failed to infer the set of unspecified policies " ++ (Map.foldrWithKey (\x _ s -> (show x) ++ " , " ++ s) "" cvarsm))) toBeChecked checkCstr :: String -> Constraint -> IO () checkCstr str (LRT g ls p q) = do case lrt g ls p q of Left b -> do check b str Right _ -> panic "This set of constraint should be solved !" "" {- solve :: [ConstraintWMsg] -> TcDeclM r () solve cs = liftIO $ do wcs <- return [(p, q) | (LRT _ p q, _) <- cs] cvars <- filterM isCstrVar wcs cvarsm <- return (foldl linker Map.empty cvars) csubsts <- return (Map.foldlWithKey (\cs' x pxs -> foldl (\cs'' px-> (substitution x px cs'')) cs' pxs) wcs cvarsm) tobechecked <- filterM (\c -> do b <- (isCstrVar c); return $ not b) csubsts mapM_ print tobechecked mapM_ (checkCstr "The unspecified variable's policies inference leads, without taking into account the global policy, to an unsolvable system. Please explicite them.") tobechecked -}