paragon 0.1.24 → 0.1.25
raw patch · 18 files changed
+387/−308 lines, 18 files
Files
- paragon.cabal +1/−1
- src/Language/Java/Paragon/Interaction.hs +1/−1
- src/Language/Java/Paragon/NameResolution.hs +20/−20
- src/Language/Java/Paragon/Parser.hs +3/−1
- src/Language/Java/Paragon/TypeCheck.hs +47/−29
- src/Language/Java/Paragon/TypeCheck/Constraints.hs +26/−28
- src/Language/Java/Paragon/TypeCheck/Containment.hs +43/−26
- src/Language/Java/Paragon/TypeCheck/Evaluate.hs +1/−1
- src/Language/Java/Paragon/TypeCheck/Monad.hs +53/−37
- src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs +9/−7
- src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs +2/−2
- src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs +5/−2
- src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs +64/−62
- src/Language/Java/Paragon/TypeCheck/Policy.hs +9/−10
- src/Language/Java/Paragon/TypeCheck/TcExp.hs +58/−50
- src/Language/Java/Paragon/TypeCheck/TcStmt.hs +14/−10
- src/Language/Java/Paragon/TypeCheck/TypeMap.hs +23/−16
- src/Language/Java/Paragon/TypeCheck/Types.hs +8/−5
paragon.cabal view
@@ -1,5 +1,5 @@ Name: paragon-Version: 0.1.24+Version: 0.1.25 License: BSD3 License-File: LICENSE Author: Niklas Broberg
src/Language/Java/Paragon/Interaction.hs view
@@ -49,7 +49,7 @@ issueTracker = "http://code.google.com/p/paragon-java/issues/entry" versionString :: String-versionString = "0.1.24"+versionString = "0.1.25" libraryBase, typeCheckerBase :: String libraryBase = "Language.Java.Paragon"
src/Language/Java/Paragon/NameResolution.hs view
@@ -47,8 +47,8 @@ type Resolve ast = ast () -> NameRes (ast ()) -rnTypeDecl :: Resolve TypeDecl-rnTypeDecl (ClassTypeDecl _ (ClassDecl _ ms ci tps mSuper impls cb)) = do+mkTpsExpn :: [TypeParam ()] -> Expansion+mkTpsExpn tps = let acts = [ aI | ActorParam _ aI <- tps ] pols = [ pI | PolicyParam _ pI <- tps ] lsts = [ lI | LockStateParam _ lI <- tps ]@@ -59,8 +59,11 @@ concatMap mkEExpansion pols ++ concatMap mkLExpansion lsts ++ concatMap mkTExpansion typs+ in expns - extendExpansion expns $+rnTypeDecl :: Resolve TypeDecl+rnTypeDecl (ClassTypeDecl _ (ClassDecl _ ms ci tps mSuper impls cb)) = do+ extendExpansion (mkTpsExpn tps) $ ClassTypeDecl () <$> (ClassDecl () <$> mapM rnModifier ms@@ -70,18 +73,7 @@ <*> mapM rnClassType impls <*> rnClassBody cb) rnTypeDecl (InterfaceTypeDecl _ (InterfaceDecl _ ms ii tps supers ib)) = do- let acts = [ aI | ActorParam _ aI <- tps ]- pols = [ pI | PolicyParam _ pI <- tps ]- lsts = [ lI | LockStateParam _ lI <- tps ]- typs = [ tI | TypeParam _ tI _ <- tps ]- - expns = Map.fromList $- concatMap mkEExpansion acts ++- concatMap mkEExpansion pols ++- concatMap mkLExpansion lsts ++- concatMap mkTExpansion typs-- extendExpansion expns $+ extendExpansion (mkTpsExpn tps) $ InterfaceTypeDecl () <$> (InterfaceDecl () <$> mapM rnModifier ms@@ -471,6 +463,13 @@ rnPolicyExp pe = case pe of PolicyLit _ cs -> PolicyLit () <$> mapM rnClause cs+ PolicyOf _ i -> do+ -- just see if it exists+ _ <- rnName (Name () EName Nothing i)+ return pe+ PolicyTypeVar _ i -> do+ _ <- rnName (Name () EName Nothing i)+ return pe _ -> return pe -- Types@@ -687,11 +686,12 @@ buildMapFromTd :: TypeDecl () -> Expansion -> PiReader (Expansion, Expansion) buildMapFromTd td expn = do --return . Map.fromList $- (i, supers) <- case td of- ClassTypeDecl _ (ClassDecl _ _ i _ mSuper _ _) -> return (i, maybe [] (:[]) mSuper)- InterfaceTypeDecl _ (InterfaceDecl _ _ i _ supers _ ) -> return (i, supers)- _ -> fail $ "Enums not yet supported"- rnSups <- runNameRes (mapM rnClassType supers) expn+ (i, tps, supers) <- + case td of+ ClassTypeDecl _ (ClassDecl _ _ i tps mSuper _ _) -> return (i, tps, maybe [] (:[]) mSuper)+ InterfaceTypeDecl _ (InterfaceDecl _ _ i tps supers _ ) -> return (i, tps, supers)+ _ -> fail $ "Enums not yet supported"+ rnSups <- runNameRes (mapM rnClassType supers) (Map.union expn (mkTpsExpn tps)) superExpns <- mapM buildMapFromSuper rnSups let iExpn = Map.fromList $ mkTExpansion i return $ (iExpn, unionExpnMaps superExpns)
src/Language/Java/Paragon/Parser.hs view
@@ -1193,7 +1193,9 @@ arrPols :: P (Maybe (Policy ())) arrPols = do _ <- arrBrackets - opt $ ExpName () <$> angles (nameRaw eName) + opt $ angles argExp1 +-- ExpName () <$> angles (nameRaw eName) +-- <|> PolicyExp () <$> policyExp nonArrayType :: P (Type ()) nonArrayType = PrimType () <$> primType <|>
src/Language/Java/Paragon/TypeCheck.hs view
@@ -77,7 +77,7 @@ typeCheckCd (ClassDecl _ ms i tps mSuper _impls (ClassBody _ decls)) = do --debug "typeCheckCd" withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do- staticWPol <- getWritePolicy ms+ staticWPol <- RealPolicy <$> getWritePolicy ms let memberDecls = [ mdecl | MemberDecl _ mdecl <- decls ] inits = [ idecl | idecl@(InitDecl {}) <- decls ]@@ -175,7 +175,8 @@ spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do a <- freshActorId (prettyPrint i) p <- getReadPolicy ms- let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)+ let vti = VSig actorT (RealPolicy p) False + (Static () `elem` ms) (Final () `elem` ms) withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra@@ -197,7 +198,8 @@ -- Final, with explicit initializer evalActorVd (ms, VarDecl _ (VarId _ i) (Just (InitExp _ e))) tcra = do p <- getReadPolicy ms- let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)+ let vti = VSig actorT (RealPolicy p) False + (Static () `elem` ms) (Final () `elem` ms) a <- case e of ExpName _ n -> do tm <- getTypeMap@@ -226,7 +228,7 @@ lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do pol <- getLockPolicy ms prs <- evalSrcLockProps i mProps- return $ LSig pol (length mps) prs+ return $ LSig (RealPolicy pol) (length mps) prs withCurrentTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $ tcba @@ -271,7 +273,7 @@ mRetPol = bottom, mWrites = top, mPars = pis,- mParPols = [ bottom | _ <- ps ],+ mParBounds = [ bottom | _ <- ps ], mExpects = [], mLMods = noMods, mExns = []@@ -398,7 +400,7 @@ -- 3. Add signature to typemap return $ VSig { varType = ty,- varPol = rPol,+ varPol = RealPolicy rPol, varParam = False, varStatic = Static () `elem` ms, varFinal = Final () `elem` ms@@ -438,10 +440,10 @@ wPol <- getWritePolicy ms let mti = MSig { mRetType = ty,- mRetPol = rPol,- mWrites = wPol,+ mRetPol = RealPolicy rPol,+ mWrites = RealPolicy wPol, mPars = pIs,- mParPols = pPols,+ mParBounds = map RealPolicy pPols, mExpects = es, mLMods = lms, mExns = xSigs@@ -474,9 +476,9 @@ -- 5. Add signature to typemap wPol <- getWritePolicy ms let cti = CSig {- cWrites = wPol,+ cWrites = RealPolicy wPol, cPars = pIs,- cParPols = pPols,+ cParBounds = map RealPolicy pPols, cExpects = es, cLMods = lms, cExns = xSigs@@ -502,9 +504,9 @@ typeCheckSignature _ _ tcba = tcba -withParam :: (FormalParam (), TcType, ActorPolicy) -> TcDeclM a -> TcDeclM a+withParam :: (FormalParam (), TcType, PrgPolicy TcActor) -> TcDeclM a -> TcDeclM a withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do- let vsig = VSig ty p True (Static () `elem` ms) (Final () `elem` ms)+ let vsig = VSig ty (RealPolicy p) True (Static () `elem` ms) (Final () `elem` ms) withCurrentTypeMap $ \tm -> tm { fields = Map.insert i vsig (fields tm) } @@ -528,8 +530,8 @@ wPol <- getWritePolicy ms lms <- checkLMMods ms let xSig = ExnSig {- exnReads = rPol,- exnWrites = wPol,+ exnReads = RealPolicy rPol,+ exnWrites = RealPolicy wPol, exnMods = lms } return (ty, xSig)@@ -555,7 +557,7 @@ let es = concat [ l | Expects _ l <- ms ] mapM evalLock es -typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), PrgPolicy TcActor) typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do -- 1. Check parameter type@@ -563,7 +565,7 @@ -- 2. Typecheck and evaluate policy modifier checkPolicyMods st ms "typeCheckSignature: At most one read modifier allowed per parameter"- rPol <- getParamPolicy i ms+ rPol <- getParamPolicy ms return (if ell then arrayType ty bottom else ty, i, rPol) typeCheckParam _ (FormalParam _ _ _ _ arvid) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid@@ -615,7 +617,9 @@ ------------------------------------------------------------------------------ -- Bodies -typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM [MemberDecl T]+typeCheckMemberDecls :: ActorPolicy + -> ActorPolicy + -> [MemberDecl ()] -> TcDeclM [MemberDecl T] typeCheckMemberDecls sLim cLim ms = do st <- setupStartState mapM (typeCheckMemberDecl sLim cLim st) ms@@ -683,15 +687,18 @@ let isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b- Just (MSig tyRet pRet _pIs pPars pWri expLs lMods xSigs) <- do+ Just (MSig tyRet pRet pIs pPars pWri expLs lMods xSigs) <- do mMap <- fromJust . Map.lookup i . methods <$> getTypeMap return $ Map.lookup (tps, tysPs, isVarArity) mMap -- Setup the environment in which to check the body- let parVsigs = [ (iP, VSig t p True False (isFinal ms)) |- (FormalParam _ ms _ _ (VarId _ iP), t, p) <- zip3 ps tysPs pPars ]+ let parMods = [ (iP, ms) | (FormalParam _ ms _ _ (VarId _ iP)) <- ps ]+ parVsigs = [ (iP, VSig t (ofPol iP) True False (isFinal ms)) |+ ((iP, ms), t) <- zip parMods tysPs ]+ pBs = zip pIs pPars pars = map fst parVsigs- exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs+ exnPols = map (second $ + \es -> (exnReads es, exnWrites es)) xSigs exnLMods = map (second exnMods) xSigs parEnts = [ (VarEntity $ mkSimpleName EName iP, []) | iP <- pars ] exnEnts = [ (ExnEntity t, []) | t <- map fst xSigs ]@@ -702,7 +709,8 @@ lockstate = expLs, returnI = Just (tyRet, pRet), exnsE = Map.fromList exnPols,- branchPCE = (branchMap, [(pWri, writeErr)])+ branchPCE = (branchMap, [(pWri, writeErr)]),+ parBounds = pBs } -- debug $ "Using env: " ++ show env@@ -743,10 +751,12 @@ -- Setup the environment in which to check the body tm <- getTypeMap- let parVsigs = [ (i, VSig t p True False (isFinal ms)) |- (FormalParam _ ms _ _ (VarId _ i), t, p) <- zip3 ps tysPs pPars ]+ let parVsigs = [ (i, VSig t (ofPol i) True False (isFinal ms)) |+ (FormalParam _ ms _ _ (VarId _ i), t) <- zip ps tysPs ] pars = map fst parVsigs- exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs+ pBs = zip pars pPars+ exnPols = map (second $ + \es -> (exnReads es, exnWrites es)) xSigs exnLMods = map (second exnMods) xSigs parEnts = [ VarEntity $ mkSimpleName EName i | i <- pars ] exnEnts = [ ExnEntity t | t <- map fst xSigs ]@@ -761,7 +771,8 @@ lockstate = expLs, returnI = error "Cannot return from constructor", exnsE = Map.fromList exnPols,- branchPCE = (branchMap, [(pWri, writeErr)])+ branchPCE = (branchMap, [(pWri, writeErr)]),+ parBounds = pBs } --debug $ "Using branch map: " ++ show (branchPCE env)@@ -791,8 +802,10 @@ unknownIfActor (i, ty) | ty == actorT = unknownActorId >>= \aid -> return [(i, aid)] | otherwise = return []- +ofPol :: Ident () -> ActorPolicy+ofPol = RealPolicy . TcRigidVar+ checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM () checkExnMods st (xTy, lms) = do let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st)@@ -800,7 +813,12 @@ check (lms `models` lockMods sX) $ "Declared exception lock modifiers not general enough: " ++ show lms-+{-+getParamBound :: ActorPolicy -> PrgPolicy TcActor+getParamBound (RealPolicy (TcRigidVar _)) = top+getParamBound (RealPolicy p) = p+getParamBound _ = top+-} tcMethodBody :: TypeCheck (TcCodeM) MethodBody tcMethodBody (MethodBody _ mBlock) =
src/Language/Java/Paragon/TypeCheck/Constraints.hs view
@@ -3,27 +3,29 @@ import qualified Data.Map as Map +--import Language.Java.Paragon.Syntax (Ident) -- get rid of!+ import Language.Java.Paragon.TypeCheck.Policy --import Language.Java.Paragon.TypeCheck.Containment import Language.Java.Paragon.TypeCheck.Locks --import Language.Java.Paragon.TypeCheck.Monad.TcCont import Language.Java.Paragon.Interaction-import Data.IORef-import Data.List (partition, union)-import Language.Java.Paragon.Monad.Base (orM)---import Control.Monad (filterM)+import Data.List (union)+import Language.Java.Paragon.Syntax (Ident) constraintsModule :: String constraintsModule = typeCheckerBase ++ ".Constraints" -data Constraint = LRT [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor)+data Constraint = + LRT [(Ident (), ActorPolicy)] + [TcClause TcAtom] [TcLock] (TcPolicy TcActor) (TcPolicy TcActor) deriving (Show, Eq) type ConstraintWMsg = (Constraint, String) splitCstrs :: Constraint -> [Constraint]-splitCstrs (LRT g ls p q) = map (\x -> LRT g ls x q) (disjoin p)+splitCstrs (LRT bs g ls p q) = map (\x -> LRT bs g ls x q) (disjoin p) where disjoin :: (TcPolicy TcActor) -> [TcPolicy TcActor] disjoin (Join p1 p2) = (disjoin p1)++(disjoin p2) disjoin (Meet p1 _p2) = disjoin p1 -- TODO: Ugly strategy!!@@ -33,28 +35,23 @@ --Check if a given constraint p<=q verifies that q is an unknown policy of a variable-isCstrVar :: Constraint -> IO Bool-isCstrVar (LRT _ _ _ (RealPolicy _)) = return False-isCstrVar (LRT _ _ _ (VarPolicy (TcMetaVar _ ref))) = do- mpol <- readIORef ref- case mpol of- Nothing -> return True - Just _ -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""-isCstrVar (LRT _ _ _ _) +isCstrVar :: Constraint -> Bool+isCstrVar (LRT _ _ _ _ (RealPolicy _)) = False+isCstrVar (LRT _ _ _ _ (VarPolicy (TcMetaVar _ _))) = True+isCstrVar (LRT _ _ _ _ _) = panic (constraintsModule ++ ".isCstrVar") "Right-side of a constraint shouldn't be a join or meet!" --Check if a given constraint p<=q verifies that q is an unknown policy of a variable-noVarLeft :: Constraint -> IO Bool-noVarLeft (LRT _ _ (RealPolicy _) _) = return True-noVarLeft (LRT _ _ (VarPolicy (TcMetaVar _ ref)) _) = do- mpol <- readIORef ref- case mpol of- Nothing -> return False- Just _ -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""-noVarLeft (LRT g ls (Join p q) r) = noVarLeft (LRT g ls p r) `orM` noVarLeft (LRT g ls q r)-noVarLeft (LRT g ls (Meet p q) r) = noVarLeft (LRT g ls p r) `orM` noVarLeft (LRT g ls q r)+noVarLeft :: Constraint -> Bool+noVarLeft (LRT _ _ _ (RealPolicy _) _) = True+noVarLeft (LRT _ _ _ (VarPolicy (TcMetaVar _ _)) _) = False+noVarLeft (LRT bs g ls (Join p q) r) = + noVarLeft (LRT bs g ls p r) || noVarLeft (LRT bs g ls q r)+noVarLeft (LRT bs g ls (Meet p q) r) = + noVarLeft (LRT bs g ls p r) || noVarLeft (LRT bs g ls q r) +{- partitionM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint], [Constraint]) partitionM f xs = do xs' <- mapM (\x -> do @@ -63,6 +60,7 @@ xs xs'' <- return $ partition fst xs' return $ ((map snd $ fst xs''), (map snd $ snd xs''))+-} {- filterM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint])@@ -76,9 +74,9 @@ -} linker :: (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))]) -> Constraint -> (Map.Map (TcMetaVar TcActor) [([TcLock], (TcPolicy TcActor))])-linker m (LRT _ ls p (VarPolicy x)) = case (Map.lookup x m) of- Nothing -> Map.insert x [(ls, p)] m- Just ps -> Map.insert x ((ls, p):ps) m+linker m (LRT _ _ ls p (VarPolicy x)) = case (Map.lookup x m) of+ Nothing -> Map.insert x [(ls, p)] m+ Just ps -> Map.insert x ((ls, p):ps) m linker _ _ = panic "linker shouldn't be called on a non-variable constraint" "" @@ -94,8 +92,8 @@ -- Add to a set of constraints the ones obtained by substituting a policy to a MetaVariable substitution :: (TcMetaVar TcActor) -> ([TcLock], (TcPolicy TcActor)) -> [Constraint] -> [Constraint] substitution _ _ [] = []-substitution x (ls, px) ((c@(LRT g ls' p q)):cs) = +substitution x (ls, px) ((c@(LRT bs g ls' p q)):cs) = let (ls'', psubst) = substPol x (ls, px) (ls',p) in case ((psubst == p) && (ls'' == ls')) of True -> c:(substitution x (ls, px) cs)- False -> (LRT g ls'' psubst q):c:(substitution x (ls, px) cs)+ False -> (LRT bs g ls'' psubst q):c:(substitution x (ls, px) cs)
src/Language/Java/Paragon/TypeCheck/Containment.hs view
@@ -20,56 +20,73 @@ containmentModule :: String containmentModule = typeCheckerBase ++ ".Containment" -lrt :: [TcClause TcAtom] -> - [TcLock] -> - TcPolicy TcActor -> - TcPolicy TcActor -> +lrt :: [(Ident (), ActorPolicy)] -> -- upper bounds of rigid vars + [TcClause TcAtom] -> -- global recursive properties + [TcLock] -> -- current lock state + TcPolicy TcActor -> -- p + TcPolicy TcActor -> -- q Either Bool Constraint -lrt g ls p q = +lrt bs g ls p q = case (p, q) of - (_, Join _ _) -> Right (LRT g ls p q) - (Meet _ _, _) -> Right (LRT g ls p q) - (RealPolicy rp, RealPolicy rq) -> Left $ lrtReal g ls rp rq + (_, Join _ _) -> Right (LRT bs g ls p q) + (Meet _ _, _) -> Right (LRT bs g ls p q) + (RealPolicy rp, RealPolicy rq) -> lrtReal bs g ls rp rq (Join p1 p2, _) -> let - ap1 = lrt g ls p1 q - ap2 = lrt g ls p2 q + ap1 = lrt bs g ls p1 q + ap2 = lrt bs g ls p2 q in case (ap1, ap2) of _ | Left False `elem` [ap1, ap2] -> Left False (Left True, _) -> ap2 (_, Left True) -> ap1 - _ -> Right (LRT g ls p q) + _ -> Right (LRT bs g ls p q) (_, Meet q1 q2) -> let - ap1 = lrt g ls p q1 - ap2 = lrt g ls p q2 + ap1 = lrt bs g ls p q1 + ap2 = lrt bs g ls p q2 in case (ap1, ap2) of _ | Left False `elem` [ap1, ap2] -> Left False (Left True, _) -> ap2 (_, Left True) -> ap1 - _ -> Right (LRT g ls p q) - (VarPolicy _, _) -> Right (LRT g ls p q) - (_, VarPolicy _) -> Right (LRT g ls p q) + _ -> Right (LRT bs g ls p q) + (VarPolicy _, _) -> Right (LRT bs g ls p q) + (_, VarPolicy _) -> Right (LRT bs g ls p q) -lrtReal :: [TcClause TcAtom] +lrtReal :: [(Ident (), ActorPolicy)] + -> [TcClause TcAtom] -> [TcLock] -> PrgPolicy TcActor -> PrgPolicy TcActor - -> Bool + -> Either Bool Constraint --lrtReal _ _ p q | any includesThis [p,q] = -- panic (containmentModule ++ ".lrtReal") -- $ "THIS in containment check: " ++ show (p,q) -lrtReal g ls (TcPolicy p) (TcPolicy q) = lrtC g ls p q -lrtReal g ls (TcJoin p1 p2) q = lrtReal g ls p1 q && lrtReal g ls p2 q -lrtReal g ls p (TcMeet q1 q2) = lrtReal g ls p q1 && lrtReal g ls p q2 -lrtReal g ls p q +lrtReal _bs g ls (TcPolicy p) (TcPolicy q) = Left $ lrtC g ls p q +lrtReal bs g ls (TcJoin p1 p2) q = + lrt bs g ls (Join (RealPolicy p1) (RealPolicy p2)) (RealPolicy q) +lrtReal bs g ls p (TcMeet q1 q2) = + lrt bs g ls (RealPolicy p) (Meet (RealPolicy q1) (RealPolicy q2)) +lrtReal bs g ls p q | Just i <- firstRigid (TcJoin p q) = let subi pol x = substPolicy [(i, x)] pol - [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, top]) [p,q] - in lrtReal g ls pb qb && lrtReal g ls pt qt + bound = maybe top id $ lookup i bs + [[pb,pt],[qb,qt]] = map (\y -> map (subi y) [bottom, bound]) [p,q] + ap1 = lrt bs g ls pb qb + ap2 = lrt bs g ls pt qt + in case (ap1, ap2) of + _ | Left False `elem` [ap1, ap2] -> Left False + (Left True, _) -> ap2 + (_, Left True) -> ap1 + _ -> Right (LRT bs g ls (RealPolicy p) (RealPolicy q)) | any includesThis [p,q] = let [[pb,pt],[qb,qt]] = map (\y -> map (flip substThis y) [bottom, top]) [p,q] - in lrtReal g ls pb qb && lrtReal g ls pt qt -lrtReal _ _ p q = + ap1 = lrt bs g ls pb qb + ap2 = lrt bs g ls pt qt + in case (ap1, ap2) of + _ | Left False `elem` [ap1, ap2] -> Left False + (Left True, _) -> ap2 + (_, Left True) -> ap1 + _ -> Right (LRT bs g ls (RealPolicy p) (RealPolicy q)) +lrtReal _ _ _ p q = panic (containmentModule ++ ".lrtReal") $ "Error: Non-computed policy provided to lrt: " ++ show (p, q)
src/Language/Java/Paragon/TypeCheck/Evaluate.hs view
@@ -55,7 +55,7 @@ let def = foldl join bottom ppols return $ mpol `orUse` def -}-evaluate :: Policy () -> TcDeclM (TcPolicy TcActor)+evaluate :: Policy () -> TcDeclM (PrgPolicy TcActor) evaluate = evalPolicy {-evaluate (PolicyExp _ pe) = evalPolicyExp pe evaluate (ExpName _ n) = -- getPolicy n
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -96,8 +96,8 @@ import Control.Applicative ( (<$>), (<*>) ) --import Control.Arrow ( first, second ) import qualified Data.Map as Map-import Data.IORef-import Data.List (union, intersperse)+--import Data.IORef+import Data.List (union, intersperse, partition) --debug :: String -> TcDeclM () --debug str = liftIO $ finePrint $ "DEBUG: " ++ str@@ -176,7 +176,7 @@ debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ show sty tm <- getTypeMap case lookupTypeOfStateT sty tm of- Right newSig -> return (Just sty, tMembers newSig, p)+ Right newSig -> return (Just sty, instThis p $ tMembers newSig, p) Left (Just err) -> fail err _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown variable or field: " ++ show n@@ -193,7 +193,7 @@ debugPrint $ "lookupPrefixName: EName: " ++ prettyPrint n ++ " :: " ++ prettyPrint ty -- debugPrint $ show (packages baseTm2) ++ "\n"- sty <- getStateType (Just n) mPreSty ty + sty <- getStateType (Just n) mPreSty ty case lookupTypeOfStateT sty baseTm2 of Right tsig -> return (Just sty, tMembers tsig, prePol `joinWThis` p) Left (Just err) -> fail err@@ -387,14 +387,14 @@ case Map.lookup i $ locks preTm of Just lsig -> return lsig Nothing -> fail $ "Lock " ++ prettyPrint (Name () LName mPre i) ++ " not in scope"--getPolicy :: Name () -> TcCodeM ActorPolicy+{-+getPolicy :: Name () -> TcCodeM (PrgPolicy TcActor) getPolicy n = do tm <- getTypeMap case lookupNamed policies n tm of Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n Just p -> return p-+-} lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig lookupFieldT typ i = do@@ -486,6 +486,9 @@ Just ps -> return ps Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX +registerExn_ :: TcType -> PrgPolicy TcActor -> PrgPolicy TcActor -> TcCodeM a -> TcCodeM a+registerExn_ tyX rX wX = registerExn tyX (RealPolicy rX) (RealPolicy wX)+ registerExn :: TcType -> ActorPolicy -> ActorPolicy -> TcCodeM a -> TcCodeM a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] @@ -643,7 +646,8 @@ case mSty of Just sty | Just pbs <- mPolicyPol sty -> do -}-updateStateType _mN _mTyO _ty (Just sty) = return sty+updateStateType _mN _mTyO ty _mSty | isPrimType (stateType ty) = return $ stateType ty+updateStateType _mN _mTyO _ty (Just sty) = return sty -- BOGUS!!! updateStateType _mN _mTyO ty Nothing = return $ stateType ty @@ -657,7 +661,7 @@ (iaps, _) <- lookupTypeOfType (clsTypeToType ct) mapM (instanceActorId . Name () EName (Just tyN)) iaps Just aids -> return aids- + -- Policy Analysis getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds@@ -668,7 +672,7 @@ (Just styO, Just (Name _ _ _ i)) -> do tsig <- lookupTypeOfStateType styO case Map.lookup i $ policies $ tMembers tsig of- Just pol -> return $ KnownPolicy pol+ Just pol -> return $ KnownPolicy $ RealPolicy pol Nothing -> return $ PolicyBounds bottom top _ -> return $ PolicyBounds bottom top Just pif -> return pif@@ -726,10 +730,10 @@ -- Exception tracking -getExnPC :: TcCodeM [(ActorPolicy, String)]+getExnPC :: TcCodeM [(TcPolicy TcActor, String)] getExnPC = exnPC <$> getState -throwExn :: ExnType -> ActorPolicy -> TcCodeM ()+throwExn :: ExnType -> TcPolicy TcActor -> TcCodeM () throwExn et pX = do uref <- getUniqRef state <- getState@@ -746,15 +750,15 @@ in s { exnS = newEmap } -activateExns :: [(ExnType, ExnSig)] -> TcCodeM ()+activateExns :: [(ExnType, (ActorPolicy, LockMods))] -> TcCodeM () activateExns exns = do uref <- getUniqRef state <- getState let (ts, sigs) = unzip exns- xPoints <- mapM (\sigX -> do+ xPoints <- mapM (\(wX, modsX) -> do s <- liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO- state { lockMods = lockMods state ||>> exnMods sigX }- return (s, exnWrites sigX)) sigs+ state { lockMods = lockMods state ||>> modsX }+ return (s, wX)) sigs let oldXmap = exnS state newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints) mergedXmap <- liftIO $ mergeExns uref oldXmap newXmap@@ -791,11 +795,10 @@ -- Policy inference -newMetaPolVar :: TcCodeM ActorPolicy-newMetaPolVar = do+newMetaPolVar :: Ident () -> TcCodeM ActorPolicy+newMetaPolVar i = do uniq <- liftIO . getUniq =<< getUniqRef- ref <- liftIO (newIORef Nothing)- return $ VarPolicy (TcMetaVar uniq ref)+ return $ VarPolicy (TcMetaVar uniq i) --newRigidPolVar :: TcCodeM TcPolicy --newRigidPolVar = do@@ -809,7 +812,8 @@ constraint :: [TcLock] -> ActorPolicy -> ActorPolicy -> String -> TcCodeM () constraint ls p q str = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps- case lrt g ls p q of+ bs <- getParamPolicyBounds+ case lrt bs g ls p q of Left b -> do -- debugTc $ "constraint: p1: " ++ show p1 -- debugTc $ "constraint: p2: " ++ show p2@@ -817,6 +821,9 @@ check b (str {-++ "\n\nState: " ++ show st -}) Right c -> addConstraint c str +getParamPolicyBounds :: TcCodeM [(Ident (), ActorPolicy)]+getParamPolicyBounds = parBounds <$> getEnv+ getGlobalLockProps :: TcCodeM [TcClause TcAtom] getGlobalLockProps = do cs <- go <$> getTypeMap@@ -844,8 +851,9 @@ -exnConsistent :: Either (Name ()) TcClassType -> TcType -> ExnSig -> TcCodeM ()-exnConsistent caller exnTy (ExnSig rX wX _) = do+exnConsistent :: Either (Name ()) TcClassType+ -> TcType -> (ActorPolicy, ActorPolicy) -> TcCodeM ()+exnConsistent caller exnTy (rX,wX) = do exnMap <- exnsE <$> getEnv --debugTc $ "Using exnMap: " ++ show exnMap let (callerName, callerSort) = @@ -975,28 +983,36 @@ ------------------------------------------ -- 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+solve :: [ConstraintWMsg] -> TcDeclM ()+solve cs = do+ let wcs = [c | (c, _) <- cs] --Extract constraints+ wcs' = concat $ map splitCstrs wcs --Split them : (Join p q <= r)<=>((p<=r)/\(q<=r))+ --print "wcs"+ --mapM_ print wcs+ --print "wcs'"+ --mapM_ print wcs'+ cvars = filter isCstrVar wcs' --Get the "p<=X" constraints, X MetaVar+ --print "cvars"+ --mapM_ print cvars+ 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+ (_toInfer, ccstright) = partition isCstrVar csubsts+ toBeChecked = filter noVarLeft ccstright+ mapM_ (checkCstr ("The system failed to infer the set of unspecified policies ")) toBeChecked -checkCstr :: String -> Constraint -> IO ()-checkCstr str (LRT g ls p q) = do- case lrt g ls p q of+++checkCstr :: String -> Constraint -> TcDeclM ()+checkCstr str (LRT bs g ls p q) = do+ case lrt bs g ls p q of Left b -> do check b str- Right _ -> panic "This set of constraint should be solved !" ""+ Right _ -> panic (monadModule ++ ".checkCstr")+ $ "This set of constraint should be solved !" {-
src/Language/Java/Paragon/TypeCheck/Monad/CodeEnv.hs view
@@ -22,22 +22,24 @@ data CodeEnv = CodeEnv { vars :: Map (Ident ()) VarFieldSig, lockstate :: [TcLock],- returnI :: Maybe (TcType, (TcPolicy TcActor)),- exnsE :: Map TcType ((TcPolicy TcActor), (TcPolicy TcActor)),- branchPCE :: (Map Entity [((TcPolicy TcActor), String)], [((TcPolicy TcActor), String)])+ returnI :: Maybe (TcType, ActorPolicy),+ exnsE :: Map TcType (ActorPolicy, ActorPolicy),+ branchPCE :: (Map Entity [(ActorPolicy, String)], [(ActorPolicy, String)]),+ parBounds :: [(Ident (), ActorPolicy)] } deriving (Show, Data, Typeable) -- Env to use when typechecking expressions not inside method -- bodies, e.g. in field initializers and policy modifiers-simpleEnv :: (TcPolicy TcActor) -> String -> CodeEnv+simpleEnv :: ActorPolicy -> String -> CodeEnv simpleEnv brPol str = CodeEnv { vars = Map.empty, lockstate = [], returnI = Nothing, exnsE = Map.empty,- branchPCE = (Map.empty, [(brPol,str)])+ branchPCE = (Map.empty, [(brPol,str)]),+ parBounds = [] } data Entity = VarEntity (Name ())@@ -66,11 +68,11 @@ -- Working with the branchPC -- -------------------------------------- -branchPC :: Maybe Entity -> CodeEnv -> [((TcPolicy TcActor), String)]+branchPC :: Maybe Entity -> CodeEnv -> [(ActorPolicy, String)] branchPC men (CodeEnv { branchPCE = (bm, def) }) = flip (maybe def) men $ \en -> maybe def id (Map.lookup en bm) -joinBranchPC :: (TcPolicy TcActor) -> String -> CodeEnv -> CodeEnv+joinBranchPC :: ActorPolicy -> String -> CodeEnv -> CodeEnv joinBranchPC p str env = let (bm, def) = branchPCE env in env { branchPCE = (Map.map ((p, str):) bm, (p,str):def) }
src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs view
@@ -183,7 +183,7 @@ type ExnsMap = Map.Map ExnType ExnPoint data ExnType = ExnType TcType | ExnContinue | ExnBreak | ExnReturn deriving (Eq, Ord, Show)-data ExnPoint = ExnPoint { epState :: CodeState, epWrite :: (TcPolicy TcActor) }+data ExnPoint = ExnPoint { epState :: CodeState, epWrite :: TcPolicy TcActor } deriving (Eq, Show) @@ -207,7 +207,7 @@ "Both ExnPoint arguments cannot be missing!" -- This should probably be pre-computed each time the map is updated instead-exnPC :: CodeState -> [((TcPolicy TcActor), String)]+exnPC :: CodeState -> [(ActorPolicy, String)] exnPC s = map (\(tyX,ptX) -> (epWrite ptX, errorSrc tyX)) $ Map.assocs $ exnS s errorSrc :: ExnType -> String
src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs view
@@ -27,10 +27,12 @@ import Language.Java.Paragon.TypeCheck.Constraints (ConstraintWMsg, Constraint) import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Locks (noMods)+import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.TypeMap import Control.Monad import Control.Applicative+import Control.Arrow (second) import qualified Data.Map as Map @@ -88,8 +90,9 @@ gatherPolicyBounds = gatherPolicyBounds' Nothing where gatherPolicyBounds' mPre tm =- let pols = Map.assocs $ policies tm -- :: [(Ident, ActorPolicy)]- aMap = Map.fromList $ map (mkPols mPre $ fields tm) pols+ let pols = Map.assocs $ policies tm -- :: [(Ident, PrgPolicy)]+ aMap = Map.fromList $ map (mkPols mPre $ fields tm) + $ map (second RealPolicy) pols tMap = gatherPolicyBoundsAux TName mPre (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm) pMap = gatherPolicyBoundsAux PName mPre (Map.assocs $ packages tm)
src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs view
@@ -107,33 +107,35 @@ check (typName == cuName) $ "File name " ++ prettyPrint typName ++ " does not match class name " ++ prettyPrint cuName- superTys <- --map (TcRefT . TcClsRefT) <$>+ withFoldMap withTypeParam tps $ do+ superTys <- --map (TcRefT . TcClsRefT) <$> mapM evalSrcClsType (maybe [] (:[]) mSuper)- implsTys <- --map (TcRefT . TcClsRefT) <$>+ implsTys <- --map (TcRefT . TcClsRefT) <$> mapM evalSrcClsType impls - -- Remove this line, and set tMembers to emptyTM,- -- if using "clever lookup" instead of "clever setup"- superTm <- case superTys of- [] -> return emptyTM- [superTy] -> tMembers . snd <$> lookupTypeOfType (clsTypeToType superTy)- _ -> panic (tcDeclMModule ++ ".fetchType")+ -- Remove this line, and set tMembers to emptyTM,+ -- if using "clever lookup" instead of "clever setup"+ superTm <- case superTys of+ [] -> return emptyTM+ [superTy] -> tMembers . snd <$> + lookupTypeOfType (clsTypeToType superTy)+ _ -> panic (tcDeclMModule ++ ".fetchType") $ "More than one super class for class:" ++ show superTys - let tsig = TSig {- tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],- tIsClass = True,- tIsFinal = Final () `elem` ms,- tSupers = superTys,- tImpls = implsTys,- tMembers = superTm { constrs = Map.empty }- }- mDs = map unMemberDecl ds- iaps = findImplActorParams mDs- extendGlobalTypeMap (extendTypeMapT n tps iaps tsig)+ let tsig = TSig {+ tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],+ tIsClass = True,+ tIsFinal = Final () `elem` ms,+ tSupers = superTys,+ tImpls = implsTys,+ tMembers = superTm { constrs = Map.empty }+ }+ mDs = map unMemberDecl ds+ iaps = findImplActorParams mDs+ extendGlobalTypeMap (extendTypeMapT n tps iaps tsig) -- (rtps,rsig) <- withTypeMapAlways (extendTypeMapT n tps tsig) $ do- withFoldMap withTypeParam tps $ do+-- withFoldMap withTypeParam tps $ do fetchActors n mDs $ do fetchLocks n mDs $ do fetchPols n mDs $ do@@ -245,7 +247,7 @@ -- Static, only Nothing for initializer spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do a <- freshActorId (prettyPrint i)- p <- getReadPolicy ms+ p <- RealPolicy <$> getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms) return ((i,a),(i,vti)) spawnActorVd (_, VarDecl _ arvid _) =@@ -253,7 +255,7 @@ paramActorVd (ms, VarDecl _ (VarId _ i) _) = do let a = ActorTPVar i- p <- getReadPolicy ms+ p <- RealPolicy <$> getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms) return ((i,a),(i,vti)) paramActorVd (_, VarDecl _ arvid _) =@@ -271,7 +273,7 @@ -} -- Final, with explicit initializer evalActorVd (ms, VarDecl _ (VarId _ i) (Just (InitExp _ e))) = do- p <- getReadPolicy ms+ p <- RealPolicy <$> getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms) a <- case e of ExpName _ nam -> do@@ -299,7 +301,7 @@ pol <- getLockPolicy ms modPrs <- getLockModProps i ms prs <- evalSrcLockProps i mProps- return (i, LSig pol (length mps) (modPrs ++ prs))+ return (i, LSig (RealPolicy pol) (length mps) (modPrs ++ prs)) let newTM = emptyTM { locks = Map.fromList lsigs } extendGlobalTypeMap (extendTypeMapN n $ merge newTM) withCurrentTypeMap (merge newTM) $ do@@ -342,7 +344,7 @@ -- debugPrint $ "Policies fetched" tdra - where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)+ where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), PrgPolicy TcActor) fetchPol (i,e,_) = (i,) <$> evalPolicy e -- end policies @@ -403,7 +405,7 @@ FieldDecl _ ms ty vds -> do tcty <- evalSrcType ty pol <- getReadPolicy ms- let vti = VSig tcty pol + let vti = VSig tcty (RealPolicy pol) False (Static () `elem` ms) (Final () `elem` ms) ids <- mapM unVarDecl vds let newFm = foldl (\m i -> Map.insert i vti m) fm ids@@ -430,14 +432,14 @@ closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ] opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ] let mti = MSig {- mRetType = tcty,- mRetPol = rPol,- mPars = pIs,- mParPols = pPols,- mWrites = wPol,- mExpects = expects,- mLMods = (closes, opens),- mExns = exs+ mRetType = tcty,+ mRetPol = RealPolicy rPol,+ mPars = pIs,+ mParBounds = map RealPolicy pPols,+ mWrites = RealPolicy wPol,+ mExpects = expects,+ mLMods = (closes, opens),+ mExns = exs } isVarArity = case reverse ps of [] -> False@@ -464,12 +466,12 @@ closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ] opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ] let cti = CSig {- cPars = pIs,- cParPols = pPols,- cWrites = wPol,- cExpects = expects,- cLMods = (closes, opens),- cExns = exs+ cPars = pIs,+ cParBounds = map RealPolicy pPols,+ cWrites = RealPolicy wPol,+ cExpects = expects,+ cLMods = (closes, opens),+ cExns = exs } isVarArity = case reverse ps of [] -> False@@ -488,15 +490,15 @@ opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ] closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ] let esig = ExnSig {- exnReads = rPol,- exnWrites = wPol,+ exnReads = RealPolicy rPol,+ exnWrites = RealPolicy wPol, exnMods = (closes, opens) } return (ty, esig) - paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy)+ paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), PrgPolicy TcActor) paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do- pPol <- getParamPolicy i ms+ pPol <- getParamPolicy ms pTy <- evalSrcType ty return (pTy, i, pPol) paramInfo (FormalParam _ _ _ _ arvid) = @@ -513,7 +515,7 @@ PolicyParam _ i -> do let vti = VSig policyT top False False True withCurrentTypeMap (\tm ->- tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm),+ tm { policies = Map.insert i (TcRigidVar i) (policies tm), fields = Map.insert i vti (fields tm) }) $ tcba LockStateParam _ i -> do let lti = LSig top 0 []@@ -620,7 +622,7 @@ ------------------------------------------------------------ ------------------------------------------------------------------------------------- -getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM ActorPolicy+getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier ()] -> TcDeclM (PrgPolicy TcActor) getReadPolicy mods = case [pol |Reads _ pol <- mods ] of -- !!0 -- Read Policy? what if no read policy? [pol] -> evalPolicy pol@@ -639,23 +641,20 @@ [] -> return top _ -> fail "At most one read modifier allowed per lock" -getParamPolicy :: Ident () -> [Modifier ()] -> TcDeclM ActorPolicy-getParamPolicy i mods =+getParamPolicy :: [Modifier ()] -> TcDeclM (PrgPolicy TcActor)+getParamPolicy mods = case [pol | Reads _ pol <- mods ] of [pol] -> evalPolicy pol- [] -> return $ ofPol i+ [] -> return top _ -> fail "At most one read modifier allowed per parameter" -getReturnPolicy :: [Modifier ()] -> [ActorPolicy] -> TcDeclM ActorPolicy+getReturnPolicy :: [Modifier ()] -> [PrgPolicy TcActor] -> TcDeclM (PrgPolicy TcActor) getReturnPolicy mods pPols = case [pol | Reads _ pol <- mods ] of [pol] -> evalPolicy pol [] -> return $ foldl join bottom pPols _ -> fail "At most one return modifier allowed per method" -ofPol :: Ident () -> ActorPolicy-ofPol = RealPolicy . TcRigidVar- ------------------------------------------------------------------- -- Evaluating types @@ -731,10 +730,13 @@ -- 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+evalSrcNWTypeArg (PolicyParam {}) (ActualName _ n) = + TcActualPolicy . RealPolicy <$> evalPolicy (ExpName () n)+evalSrcNWTypeArg (PolicyParam {}) (ActualExp _ e) = + TcActualPolicy . RealPolicy <$> evalPolicy e -- Lock states must be locks-evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls+evalSrcNWTypeArg (LockStateParam {}) (ActualLockState _ ls) = + TcActualLockState <$> mapM evalLock ls evalSrcNWTypeArg tp nwta = fail $ "Trying to instantiate type parameter " ++ prettyPrint tp ++@@ -747,7 +749,7 @@ evalSrcNWTypeArg (ActualLockState _ ls) = TcActualLockState <$> mapM evalLock ls -} -evalPolicy :: Exp () -> TcDeclM ActorPolicy+evalPolicy :: Exp () -> TcDeclM (PrgPolicy TcActor) evalPolicy e = case e of ExpName _ n -> do -- debug $ "evalPolicy: " ++ show n@@ -770,11 +772,11 @@ Paren _ p -> evalPolicy p _ -> fail "evalPolicy: More here!" -evalPolicyExp :: PolicyExp () -> TcDeclM ActorPolicy-evalPolicyExp (PolicyLit _ cs) = (RealPolicy . TcPolicy) <$> mapM evalClause cs-evalPolicyExp (PolicyOf _ i) = return $ RealPolicy $ TcRigidVar i-evalPolicyExp (PolicyThis _) = return $ RealPolicy $ TcThis-evalPolicyExp (PolicyTypeVar _ i) = return $ RealPolicy $ TcRigidVar i+evalPolicyExp :: PolicyExp () -> TcDeclM (PrgPolicy TcActor)+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 () -> TcDeclM (TcClause TcActor) evalClause (Clause _ h b) = do
src/Language/Java/Paragon/TypeCheck/Policy.hs view
@@ -20,7 +20,6 @@ import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Locks -import Data.IORef import Data.List ( (\\) {-, groupBy, nub-} ) import Data.Maybe @@ -65,7 +64,7 @@ type AtomPolicy = TcPolicy TcAtom -data TcMetaVar a = TcMetaVar Int (IORef (Maybe (TcPolicy a))) +data TcMetaVar a = TcMetaVar Int (Ident ()) -- deriving (Data, Typeable) instance Data (TcMetaVar a) where @@ -422,18 +421,18 @@ -- Policy substitution -- Invariant: policies are always closed by the env -substPolicy :: [(Ident (), PrgPolicy TcActor)] -> PrgPolicy TcActor -> PrgPolicy TcActor +substPolicy :: [(Ident (), ActorPolicy)] -> PrgPolicy TcActor -> ActorPolicy substPolicy env (TcRigidVar i) | Just q <- lookup i env = q substPolicy env (TcJoin p1 p2) = let pol1 = substPolicy env p1 pol2 = substPolicy env p2 - in pol1 `lub` pol2 + in pol1 `join` pol2 substPolicy env (TcMeet p1 p2) = let pol1 = substPolicy env p1 pol2 = substPolicy env p2 - in pol1 `glb` pol2 -substPolicy _ p = p + in pol1 `meet` pol2 +substPolicy _ p = RealPolicy p firstRigid :: PrgPolicy a -> Maybe (Ident ()) firstRigid (TcRigidVar i) = Just i @@ -441,17 +440,17 @@ firstRigid (TcMeet p q) = listToMaybe $ catMaybes $ map firstRigid [p,q] firstRigid _ = Nothing -substThis :: PrgPolicy TcActor -> PrgPolicy TcActor -> PrgPolicy TcActor +substThis :: ActorPolicy -> PrgPolicy TcActor -> ActorPolicy substThis p TcThis = p substThis p (TcJoin p1 p2) = let pol1 = substThis p p1 pol2 = substThis p p2 - in pol1 `lub` pol2 + in pol1 `join` pol2 substThis p (TcMeet p1 p2) = let pol1 = substThis p p1 pol2 = substThis p p2 - in pol1 `glb` pol2 -substThis _ p = p + in pol1 `meet` pol2 +substThis _ p = RealPolicy p {- mkPolicySubst :: [TcPolicy] -> [TcPolicy] -> [(Ident (), TcPolicy)]
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -17,7 +17,7 @@ import Data.Maybe (fromJust) import qualified Data.Map as Map import Control.Applicative ( (<$>) )-import Control.Arrow ( first, second )+-- import Control.Arrow ( first, second ) import Control.Monad ( when ) tcExpModule :: String@@ -153,14 +153,14 @@ " has policy " ++ prettyPrint pA ++ "\n" ++ "Index: " ++ prettyPrint iE ++ "\n" ++ " has policy " ++ prettyPrint pI- constraint [] pA pElem $+ constraint [] pA (RealPolicy pElem) $ "Cannot update element in array resulting from expression " ++ prettyPrint arrE ++ ": policy of elements must be no less restrictive than that of the " ++ "array itself when updating\n" ++ "Array policy: " ++ prettyPrint pA ++ "\n" ++ "Element policy: " ++ prettyPrint pElem- return (tyElem, pElem, Just $ unStateType tyA, Nothing, Nothing, + return (tyElem, RealPolicy pElem, Just $ unStateType tyA, Nothing, Nothing, ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE@@ -324,7 +324,8 @@ -- Check that the remaining dimexprs each conform to -- the policy given at the level outside it- (polEDims, dimEsRest) <- checkDimExprs [] [] dimEsPsRest =<< evalMaybePol mDimP1+ (polEDims, dimEsRest) <- checkDimExprs [] [] dimEsPsRest + =<< evalMaybePol mDimP1 -- Evaluate given policies for implicit dimensions polIDims <- mapM evalMaybePol dimImplPs@@ -337,17 +338,17 @@ return (stateType ty, pol1, ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs') - where checkDimExprs :: [ActorPolicy] -- Accumulated policies of earlier dimensions+ where checkDimExprs :: [PrgPolicy TcActor] -- Accumulated policies of earlier dimensions -> [Exp T] -- Accumulated annotated expressions -> [(Exp (), Maybe (Policy ()))] -- Remaining dimexprs/pols- -> ActorPolicy -- Policy of previous dimension- -> TcCodeM ([ActorPolicy], [Exp T])+ -> PrgPolicy TcActor -- Policy of previous dimension+ -> TcCodeM ([PrgPolicy TcActor], [Exp T]) checkDimExprs accP accE [] pPrev = return $ (reverse (pPrev:accP), reverse accE) checkDimExprs accP accE ((e,mp):emps) pPrev = do (tyE,pE,e') <- tcExp e check (isIntConvertible tyE) $ nonIntErr tyE -- Each dimexpr must satisfy the policy of the outer dim- constraintLS pE pPrev $+ constraintLS pE (RealPolicy pPrev) $ "Array dimension expression has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ "\n" ++ " with policy: " ++ prettyPrint pE ++ "\n" ++@@ -384,7 +385,7 @@ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression" styElem <- getStateType Nothing Nothing tyElem- return (styElem, pElem `join` pA `join` pI, + return (styElem, RealPolicy pElem `join` pA `join` pI, ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE@@ -396,10 +397,10 @@ -------------------------- -- Array initializers -tcArrayInit :: TcType -> [ActorPolicy] -> TypeCheck TcCodeM ArrayInit+tcArrayInit :: TcType -> [PrgPolicy TcActor] -> TypeCheck TcCodeM ArrayInit tcArrayInit baseType (pol1:pols) (ArrayInit _ inits) = do (ps, inits') <- unzip <$> mapM (tcVarInit baseType pols) inits- mapM_ (\(p,e) -> constraintLS p pol1 $+ mapM_ (\(p,e) -> constraintLS p (RealPolicy pol1) $ "Expression in array initializer has too restrictive policy:\n" ++ "Expression: " ++ prettyPrint e ++ " with policy: " ++ prettyPrint p ++@@ -408,7 +409,7 @@ return $ ArrayInit Nothing inits' tcArrayInit _ [] _ = fail $ "Array initializer has too many dimensions" -tcVarInit :: TcType -> [ActorPolicy] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T)+tcVarInit :: TcType -> [PrgPolicy TcActor] -> VarInit () -> TcCodeM (ActorPolicy, VarInit T) tcVarInit baseType pols (InitExp _ e) = do -- debugPrint $ "Pols: " ++ show pols -- debugPrint $ "Exp: " ++ show e@@ -423,7 +424,7 @@ arr' <- tcArrayInit baseType pols arr return (bottom, InitArray Nothing arr') -evalMaybePol :: Maybe (Policy ()) -> TcCodeM ActorPolicy+evalMaybePol :: Maybe (Policy ()) -> TcCodeM (PrgPolicy TcActor) evalMaybePol = maybe (return bottom) (liftTcDeclM . evalPolicy) --------------------------@@ -432,7 +433,7 @@ tcFieldAccess :: FieldAccess () -> TcCodeM (TcStateType, ActorPolicy, FieldAccess T) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE,e') <- tcExp e- VSig tyF pFi _ _ _ <- lookupFieldT tyE fi+ VSig tyF pFi _ _ _ <- instThis pE <$> lookupFieldT tyE fi styF <- getStateType Nothing Nothing tyF return (styF, pE `join` pFi, PrimaryFieldAccess (toT styF) e' (notAppl fi)) @@ -460,7 +461,7 @@ -- tm <- getTypeMap let cti = instantiate (zip (tps++itps) (tArgs++itas)) genCti- (CSig _psIs psPars pW lExp lMods exns) = cti+ (CSig psIs psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState@@ -469,6 +470,14 @@ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints+ let subst = zip psIs psArgs+ (pW':psPars') = map (substParPols subst) (pW:psPars)+ (exnPs, exnAcs) = + unzip [ ((t, (rX', wX')), (ExnType t, (wX', modsX))) |+ (t, ExnSig rX wX modsX) <- exns,+ let rX' = substParPols subst rX, + let wX' = substParPols subst wX + ] mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Constructor applied to argument with too restrictive policy:\n" ++ @@ -476,28 +485,27 @@ "Argument: " ++ prettyPrint arg ++ " with policy: " ++ prettyPrint argP ++ "Declared policy bound: " ++ prettyPrint parP- ) (zip3 args psArgs psPars)+ ) (zip3 args psArgs psPars') -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_- constraintPC bpcs pW $ \p src ->+ constraintPC bpcs pW' $ \p src -> "Constructor " ++ prettyPrint ctyT ++ - " with declared write effect " ++ prettyPrint pW +++ " with declared write effect " ++ prettyPrint pW' ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check exnPC(S) <= pW epc <- getExnPC- constraintPC epc pW $ \p src ->+ constraintPC epc pW' $ \p src -> "Constructor " ++ prettyPrint ctyT ++ - " with declared write effect " ++ prettyPrint pW +++ " with declared write effect " ++ prettyPrint pW' ++ " not allowed in " ++ src ++ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] - mapM_ (uncurry $ exnConsistent (Right ctyT)) exns+ mapM_ (uncurry $ exnConsistent (Right ctyT)) exnPs -- Fix outgoing state- let exns' = map (first ExnType) exns- activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]+ activateExns exnAcs -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] @@ -568,7 +576,7 @@ (tyE, pE, e') <- tcExp e (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args let tas' = map (ActualArg ()) tas- (tps, genMSig) <- lookupMethodT tyE i tas' (map unStateType tysArgs)+ (tps, genMSig) <- instThis pE <$> lookupMethodT tyE i tas' (map unStateType tysArgs) tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ zip tps tas' let msig = instantiate (zip tps tArgs) genMSig@@ -584,15 +592,14 @@ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l -- Check argument constraints- debugPrint $ "psIs: " ++ show psIs- debugPrint $ "psArgs: " ++ show psArgs- debugPrint $ "psPars: " ++ show psPars- debugPrint $ "pR: " ++ show pR ++ "\n" let subst = zip psIs psArgs (pR':pW':psPars') = map (substParPols subst) (pR:pW:psPars)- exns' = map (second (substExnParPols subst)) exns- debugPrint $ "psPars': " ++ show psPars'- debugPrint $ "pR': " ++ show pR'+ (exnPs, exnAcs) = + unzip [ ((t, (rX', wX')), (ExnType t, (wX', modsX))) |+ (t, ExnSig rX wX modsX) <- exns,+ let rX' = substParPols subst rX, + let wX' = substParPols subst wX + ] mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Method applied to argument with too restrictive policy:\n" ++ @@ -615,38 +622,39 @@ " with write effect bound " ++ prettyPrint p -- Check Exns(X)[write] <= E[exns](X)[write] AND -- Check Exns(X)[read] >= E[exns](X)[read] - mapM_ (uncurry $ exnConsistent (Left n)) exns'+ mapM_ (uncurry $ exnConsistent (Left n)) exnPs -- Fix outgoing state- let exnsT = map (first ExnType) exns'- activateExns exnsT -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]+-- let exnsT = [ (ExnType tX, (wX, modsX)) | ((tX, (_, wX)), modsX) <- zip exnsPs ]+-- exnsT = map (first ExnType) exnPs+ activateExns exnAcs -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] styR <- getStateType Nothing Nothing tyR- return (styR, pE `join` pR, ef styR)+ return (styR, pE `join` pR', ef styR) -substExnParPols :: [(Ident (), ActorPolicy)] -> ExnSig -> ExnSig-substExnParPols subst (ExnSig rX wX _ms) = - ExnSig (substParPols subst rX) (substParPols subst wX) _ms+--substExnParPols :: [(Ident (), ActorPolicy)] -> ExnSig -> (ActorPolicy, ActorPolicy)+--substExnParPols subst (ExnSig rX wX _ms) = +-- (substParPrgPols subst rX, substParPrgPols subst wX) substParPols :: [(Ident (), ActorPolicy)] -> ActorPolicy -> ActorPolicy-substParPols subst (RealPolicy pol) = substParPrgPols pol- where substParPrgPols :: PrgPolicy TcActor -> ActorPolicy- substParPrgPols p@(TcRigidVar i) = - case lookup i subst of- Just newP -> newP- Nothing -> RealPolicy p- substParPrgPols (TcJoin p q) = - substParPrgPols p `join` substParPrgPols q- substParPrgPols (TcMeet p q) = - substParPrgPols p `meet` substParPrgPols q- substParPrgPols p = RealPolicy p-+substParPols subst (RealPolicy pol) = substParPrgPols subst pol substParPols subst (Join p q) = substParPols subst p `join` substParPols subst q substParPols subst (Meet p q) = substParPols subst p `meet` substParPols subst q substParPols _ p = p++substParPrgPols :: [(Ident (), ActorPolicy)] -> PrgPolicy TcActor -> ActorPolicy+substParPrgPols subst p@(TcRigidVar i) = + case lookup i subst of+ Just newP -> newP+ Nothing -> RealPolicy p+substParPrgPols subst (TcJoin p q) = + substParPrgPols subst p `join` substParPrgPols subst q+substParPrgPols subst (TcMeet p q) = + substParPrgPols subst p `meet` substParPrgPols subst q+substParPrgPols _ p = RealPolicy p -----------------------------------
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -47,7 +47,8 @@ $ "if-statement requires a condition of type compatible with boolean\n" ++ "Found type: " ++ prettyPrint tyC extendBranchPC pC ("branch dependent on condition " ++ prettyPrint c) $ do- (s1', s2') <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) ||| tcStmt s2+ (s1', s2') <- (maybeM (mLocks tyC) (\ls -> applyLockMods ([],ls)) >> tcStmt s1) + ||| tcStmt s2 return $ IfThenElse Nothing c' s1' s2' -- Rule IFTHEN@@ -219,11 +220,12 @@ tyP <- liftTcDeclM $ evalSrcType t -- TODO check tyP <: "Throwable" pR <- liftTcDeclM $ getReadPolicy ms -- getParamPolicy i ms- pW <- newMetaPolVar -- \pi, where \pi is fresh+ pW <- newMetaPolVar i -- \pi, where \pi is fresh addBranchPC (exnE tyP) $ -- E' = E[branchPC{tyP +-> bottom},- registerExn tyP pR pW $ do -- exns{tyP +-> (pR, \pi)}]+ registerExn tyP (RealPolicy pR) pW $ do -- exns{tyP +-> (pR, \pi)}] block' <- tcBlock block- extendVarEnv i (VSig tyP pR True False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}]+ extendVarEnv i (VSig tyP (RealPolicy pR) True False (isFinal ms)) $ do + -- E* = E[vars{x +-> (tyP, pR)}] msX <- getExnState (ExnType tyP) maybeM msX $ mergeWithState -- S* = St <> St[exns](X)[state] cBlock' <- tcBlock cBlock@@ -359,7 +361,7 @@ (_,_,es') <- unzip3 <$> mapM tcExp es (Just $ ForInitExps Nothing es',) <$> tca withInits (Just (ForLocalVars _ ms t vds)) tca = do- pV <- localVarPol ms+ pV <- localVarPol ms vds tyV <- liftTcDeclM $ evalSrcType t (vds', a) <- tcLocalVars pV tyV (isFinal ms) vds [] $ tca return $ (Just $ ForLocalVars Nothing (map notAppl ms) (notAppl t) vds', a)@@ -384,7 +386,7 @@ -- Rule LOCALVARINIT/LOCALVARDECL tcBlockStmts (LocalVars _ ms t vds : bss) = do- pV <- localVarPol ms+ pV <- localVarPol ms vds tyV <- liftTcDeclM $ evalSrcType t -- debugTc $ "Array type pre: " ++ prettyPrint t (vds', bss') <- tcLocalVars pV tyV (isFinal ms) vds [] $ @@ -452,11 +454,13 @@ fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd -localVarPol :: [Modifier ()] -> TcCodeM ActorPolicy-localVarPol ms = +localVarPol :: [Modifier ()] -> [VarDecl ()] -> TcCodeM ActorPolicy+localVarPol ms vds = case [ p | Reads _ p <- ms ] of- [] -> newMetaPolVar --return bottom- [p] -> liftTcDeclM $ evalPolicy p+ [] -> newMetaPolVar . getVarId . head $ vds -- TODO a TcVarPolicy for each variable, or a shared one ?+ where getVarId (VarDecl _ (VarId _ i) _) = i+ getVarId (VarDecl _ (VarDeclArray _ vdi) _) = getVarId $ VarDecl () vdi Nothing + [p] -> liftTcDeclM $ RealPolicy <$> evalPolicy p _ -> fail $ "Only one read policy allowed on local variable" ---------------------------------------------------
src/Language/Java/Paragon/TypeCheck/TypeMap.hs view
@@ -47,14 +47,14 @@ deriving (Show, Data, Typeable) data MethodSig = MSig {- mRetType :: TcType,- mRetPol :: ActorPolicy,- mPars :: [Ident ()],- mParPols :: [ActorPolicy],- mWrites :: ActorPolicy,- mExpects :: [TcLock],- mLMods :: ([TcLock],[TcLock]),- mExns :: [(TcType, ExnSig)]+ mRetType :: TcType,+ mRetPol :: ActorPolicy,+ mPars :: [Ident ()],+ mParBounds :: [ActorPolicy],+ mWrites :: ActorPolicy,+ mExpects :: [TcLock],+ mLMods :: ([TcLock],[TcLock]),+ mExns :: [(TcType, ExnSig)] } deriving (Show, Data, Typeable) @@ -66,12 +66,12 @@ deriving (Show, Data, Typeable) data ConstrSig = CSig {- cPars :: [Ident ()],- cParPols :: [ActorPolicy],- cWrites :: ActorPolicy,- cExpects :: [TcLock],- cLMods :: ([TcLock],[TcLock]),- cExns :: [(TcType, ExnSig)]+ cPars :: [Ident ()],+ cParBounds :: [ActorPolicy],+ cWrites :: ActorPolicy,+ cExpects :: [TcLock],+ cLMods :: ([TcLock],[TcLock]),+ cExns :: [(TcType, ExnSig)] } deriving (Show, Data, Typeable) @@ -105,7 +105,7 @@ constrs :: ConstrMap, locks :: Map (Ident ()) LockSig, -- known policy-level entities- policies :: Map (Ident ()) ActorPolicy,+ policies :: Map (Ident ()) (PrgPolicy TcActor), actors :: Map (Ident ()) ActorId, -- typemethod eval info typemethods :: Map (Ident ()) ([Ident ()], Block ()),@@ -128,7 +128,7 @@ packages = Map.empty } -hardCodedArrayTM :: TcType -> ActorPolicy -> TypeSig+hardCodedArrayTM :: TcType -> PrgPolicy TcActor -> TypeSig hardCodedArrayTM ty p = let memTM = emptyTM { fields = Map.fromList [(Ident () "length", VSig intT thisP False False True)]@@ -365,3 +365,10 @@ as = [ (i, n ) | (ActorParam _ i, TcActualActor n) <- pas ] ps = [ (i, p ) | (PolicyParam _ i, TcActualPolicy p) <- pas ] locs = [ (i, ls) | (LockStateParam _ i, TcActualLockState ls) <- pas ]+++instThis :: Data a => ActorPolicy -> a -> a+instThis p = transformBi instThisPol+ where instThisPol :: ActorPolicy -> ActorPolicy+ instThisPol (RealPolicy q) = substThis p q+ instThisPol q = q
src/Language/Java/Paragon/TypeCheck/Types.hs view
@@ -44,7 +44,7 @@ data TcRefType = TcClsRefT TcClassType- | TcArrayT TcType ActorPolicy+ | TcArrayT TcType (PrgPolicy TcActor) | TcTypeVar (Ident ()) | TcNullT deriving (Eq, Ord, Show, Data, Typeable)@@ -129,10 +129,10 @@ clsTypeToType :: TcClassType -> TcType clsTypeToType = TcRefT . TcClsRefT -arrayType :: TcType -> ActorPolicy -> TcType+arrayType :: TcType -> PrgPolicy TcActor -> TcType arrayType = (TcRefT .) . TcArrayT -mkArrayType :: TcType -> [ActorPolicy] -> TcType+mkArrayType :: TcType -> [PrgPolicy TcActor] -> TcType mkArrayType = foldr (flip arrayType) @@ -155,7 +155,7 @@ -- Just n -> n -- Nothing -> error $ "typeName_: " ++ show typ -isClassType, isRefType, isNullType :: TcStateType -> Bool+isClassType, isRefType, isPrimType, isNullType :: TcStateType -> Bool isClassType (TcType (TcRefT (TcClsRefT (TcClassT{})))) = True isClassType (TcInstance{}) = True isClassType _ = False@@ -164,6 +164,9 @@ isRefType (TcInstance{}) = True isRefType _ = False +isPrimType (TcType (TcPrimT _)) = True+isPrimType _ = False+ mNameRefType :: TcRefType -> Maybe (Name ()) mNameRefType (TcClsRefT (TcClassT n as)) = if null as then Just (mkUniformName_ AmbName $ flattenName n) else Nothing@@ -193,7 +196,7 @@ isPolicyType :: TcStateType -> Bool isPolicyType = isJust . mPolicyPol -mArrayType :: TcType -> Maybe (TcType, [ActorPolicy])+mArrayType :: TcType -> Maybe (TcType, [PrgPolicy TcActor]) mArrayType (TcRefT (TcArrayT ty p)) = Just $ case mArrayType ty of Nothing -> (ty, [p])