paragon 0.1.22 → 0.1.23
raw patch · 20 files changed
+929/−455 lines, 20 files
Files
- paragon.cabal +1/−1
- src/Language/Java/Paragon/Interaction.hs +1/−1
- src/Language/Java/Paragon/NameResolution.hs +12/−8
- src/Language/Java/Paragon/Parser.hs +16/−7
- src/Language/Java/Paragon/Pretty.hs +11/−6
- src/Language/Java/Paragon/QuasiQuoter/Lift.hs +1/−0
- src/Language/Java/Paragon/Syntax.hs +7/−2
- src/Language/Java/Paragon/TypeCheck.hs +31/−28
- src/Language/Java/Paragon/TypeCheck/Actors.hs +24/−13
- src/Language/Java/Paragon/TypeCheck/Constraints.hs +5/−3
- src/Language/Java/Paragon/TypeCheck/Containment.hs +10/−3
- src/Language/Java/Paragon/TypeCheck/Monad.hs +201/−69
- src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs +105/−12
- src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs +36/−2
- src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs +93/−50
- src/Language/Java/Paragon/TypeCheck/Policy.hs +58/−27
- src/Language/Java/Paragon/TypeCheck/TcExp.hs +139/−98
- src/Language/Java/Paragon/TypeCheck/TcStmt.hs +19/−12
- src/Language/Java/Paragon/TypeCheck/TypeMap.hs +64/−26
- src/Language/Java/Paragon/TypeCheck/Types.hs +95/−87
paragon.cabal view
@@ -1,5 +1,5 @@ Name: paragon-Version: 0.1.22+Version: 0.1.23 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.22"+versionString = "0.1.23" libraryBase, typeCheckerBase :: String libraryBase = "Language.Java.Paragon"
src/Language/Java/Paragon/NameResolution.hs view
@@ -36,7 +36,7 @@ (tnExpnMap,supExpnMap) <- buildMapFromTd td jipExpnMap -- We need to take the current name take precedence let expnMap = Map.union tnExpnMap (unionExpnMaps [jipExpnMap,supExpnMap])- debugPrint $ "Expansions: " ++ show expnMap+-- debugPrint $ "Expansions: " ++ show expnMap td' <- runNameRes (rnTypeDecl td) expnMap return $ CompilationUnit () _pkg imps' [td'] @@ -139,13 +139,13 @@ rnMemberDecl :: Resolve MemberDecl rnMemberDecl md = do- debugPrint $ "Resolving member decl: " ++ prettyPrint md- debugPrint $ show md ++ "\n"+-- debugPrint $ "Resolving member decl: " ++ prettyPrint md+-- debugPrint $ show md ++ "\n" case md of FieldDecl _ ms t vds -> FieldDecl () <$> mapM rnModifier ms <*> rnType t <*> mapM rnVarDecl vds - MethodDecl _ ms tps mRet mI fps exns mbody -> do+ MethodDecl _ ms tps ret mI fps exns mbody -> do let ps = [ pI | FormalParam _ _ _ _ (VarId _ pI) <- fps ] paramsE = Map.fromList $ concatMap mkEExpansion ps@@ -153,7 +153,7 @@ MethodDecl () <$> mapM rnModifier ms <*> mapM rnTypeParam tps- <*> mapM rnType mRet+ <*> rnReturnType ret <*> pure mI <*> mapM rnFormalParam fps <*> mapM rnExceptionSpec exns@@ -179,7 +179,7 @@ <*> pure arity <*> mapM rnLockProperties mProps _ -> do- debugPrint $ show md+-- debugPrint $ show md fail $ "Inner types not supported" rnConstructorBody :: Resolve ConstructorBody@@ -475,6 +475,10 @@ -- Types +rnReturnType :: Resolve ReturnType+rnReturnType (Type _ t) = Type () <$> rnType t+rnReturnType rt = return rt+ rnType :: Resolve Type rnType (RefType _ rt) = RefType () <$> rnRefType rt rnType t = return t@@ -741,7 +745,7 @@ -> PiReader (ImportDecl (), Expansion) buildMapFromImportName imp = do finePrint $ "Resolving import: " ++ prettyPrint imp- debugPrint $ show imp+-- debugPrint $ show imp case imp of SingleTypeImport _ tn@(Name _ TName mPre i) -> do mPre' <- resolvePre mPre@@ -771,7 +775,7 @@ isP <- doesPkgExist resName if isP then do -- resolve as package- debugPrint $ "Package exists: " ++ show resName+ --debugPrint $ "Package exists: " ++ show resName piTypeIdents <- getPkgContents resName let resExpn = Map.fromList $ concatMap (\x -> [((x, TName ), return (Just resName, TName)),
src/Language/Java/Paragon/Parser.hs view
@@ -20,7 +20,7 @@ stmtExp, exp, primary, literal, lhs, - ttype, primType, refType, classType, resultType, + ttype, primType, refType, classType, returnType, typeParams, typeParam, @@ -280,7 +280,7 @@ methodDeclM :: P (Mod (MemberDecl ())) methodDeclM = do tps <- lopt typeParams - rt <- resultType + rt <- returnType i <- ident fps <- formalParams thr <- lopt throws @@ -389,7 +389,7 @@ absMethodDeclM :: P (Mod (MemberDecl ())) absMethodDeclM = do tps <- lopt typeParams - rt <- resultType + rt <- returnType i <- ident fps <- formalParams thr <- lopt throws @@ -837,9 +837,10 @@ LockExp () <$> (tok Op_Query >> lock) <|> -- TODO: These two following should probably be merged more (try $ do - rt <- resultType + rt <- returnType + mt <- checkClassLit rt period >> tok KW_Class - return $ ClassLit () rt) <|> + return $ ClassLit () mt) <|> (try $ do n <- nameRaw tName period >> tok KW_This @@ -854,6 +855,12 @@ AntiQExpTok s -> Just s _ -> Nothing) +checkClassLit :: ReturnType () -> P (Maybe (Type ())) +checkClassLit (LockType ()) = fail "Lock is not a class type!" +checkClassLit (VoidType ()) = return Nothing +checkClassLit (Type _ t) = return $ Just t + + primarySuffix :: P (Exp () -> Exp ()) primarySuffix = try instanceCreationSuffix <|> try ((ArrayAccess () .) <$> arrayAccessSuffix) <|> @@ -1207,8 +1214,10 @@ return (i, tas) -} -resultType :: P (Maybe (Type ())) -resultType = tok KW_Void >> return Nothing <|> Just <$> ttype <?> "resultType" +returnType :: P (ReturnType ()) +returnType = tok KW_Void >> return (VoidType ()) <|> + tok KW_P_Lock >> return (LockType ()) <|> + Type () <$> ttype <?> "returnType" classTypeList :: P [ClassType ()] classTypeList = seplist1 classType comma
src/Language/Java/Paragon/Pretty.hs view
@@ -116,10 +116,10 @@ pretty (FieldDecl _ mods t vds) = hsep (map pretty mods ++ pretty t:map pretty vds) <> semi - pretty (MethodDecl _ mods tParams mt ident fParams throws body) = + pretty (MethodDecl _ mods tParams ret ident fParams throws body) = hsep [hsep (map pretty mods) , ppTypeParams tParams - , ppResultType mt + , pretty ret , pretty ident <> ppArgs fParams , ppThrows throws ] $$ pretty body @@ -364,7 +364,7 @@ pretty (Lit _ l) = pretty l pretty (ClassLit _ mT) = - ppResultType mT <> text ".class" + maybe (text "void") pretty mT <> text ".class" pretty (This _) = text "this" @@ -624,9 +624,14 @@ pretty (ExceptionSpec _ mods t) = hsep (map pretty mods) <+> pretty t -ppResultType :: Maybe (Type x) -> Doc -ppResultType Nothing = text "void" -ppResultType (Just a) = pretty a +instance Pretty (ReturnType a) where + pretty (VoidType _) = text "void" + pretty (LockType _) = text "lock" + pretty (Type _ ty ) = pretty ty + +--ppResultType :: Maybe (Type x) -> Doc +--ppResultType Nothing = text "void" +--ppResultType (Just a) = pretty a ----------------------------------------------------------------------- -- Paragon Policies
src/Language/Java/Paragon/QuasiQuoter/Lift.hs view
@@ -89,6 +89,7 @@ ''WildcardBound,''Decl,''VarInit, ''Clause, ''LClause, ''PrimType,+ ''ReturnType, ''Atom, ''Actor, ''ActorName,
src/Language/Java/Paragon/Syntax.hs view
@@ -104,7 +104,7 @@ -- | The variables of a class type are introduced by field declarations. = FieldDecl a [Modifier a] (Type a) [VarDecl a] -- | A method declares executable code that can be invoked, passing a fixed number of values as arguments. - | MethodDecl a [Modifier a] [TypeParam a] (Maybe (Type a)) (Ident a) [FormalParam a] [ExceptionSpec a] (MethodBody a) + | MethodDecl a [Modifier a] [TypeParam a] (ReturnType a) (Ident a) [FormalParam a] [ExceptionSpec a] (MethodBody a) -- | A constructor is used in the creation of an object that is an instance of a class. | ConstructorDecl a [Modifier a] [TypeParam a] (Ident a) [FormalParam a] [ExceptionSpec a] (ConstructorBody a) -- | A member class is a class whose declaration is directly enclosed in another class or interface declaration. @@ -467,6 +467,11 @@ ----------------------------------------------------------------------- -- Types +data ReturnType a + = VoidType a + | LockType a + | Type a (Type a) + deriving (Eq,Ord,Show,Typeable,Data,Functor) -- | There are two kinds of types in the Java programming language: primitive types and reference types. data Type a @@ -696,7 +701,7 @@ ''Catch, ''SwitchBlock, ''SwitchLabel, ''ForInit, ''ExceptionSpec, ''Exp, ''Literal, ''Op, ''AssignOp, ''Lhs, ''ArrayIndex, ''FieldAccess, ''MethodInvocation, - ''Type, ''PrimType, ''RefType, ''ClassType, + ''Type, ''PrimType, ''RefType, ''ClassType, ''ReturnType, ''TypeArgument, ''NonWildTypeArgument, ''WildcardBound, ''TypeParam, ''PolicyExp, ''LockProperties, ''Clause, ''LClause, ''Actor, ''ActorName, ''Atom, ''Lock, ''Ident, ''Name])
src/Language/Java/Paragon/TypeCheck.hs view
@@ -116,14 +116,14 @@ Left mErr -> panic (typeCheckerBase ++ ".withSuperType") $ "Super type evaluated but now doesn't exist: " ++ show mErr- Right superSig -> (tMembers superSig) { constrs = Map.empty }+ Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty } extendGlobalTypeMap (\tm -> -- We insert an empty typemap at first, -- since we are only using this when checking signatures let thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) True False cTys [] emptyTM- newTm = tm { types = Map.insert i (tps,thisSig) (types tm) } + newTm = tm { types = Map.insert i (tps,[],thisSig) (types tm) } in foldl merge newTm superTMs) @@ -136,13 +136,13 @@ Left mErr -> panic (typeCheckerBase ++ ".withSuperType") $ "Super type evaluated but now doesn't exist: " ++ show mErr- Right superSig -> (tMembers superSig) { constrs = Map.empty }+ Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty } let thisTm = baseTm { types = Map.empty, packages = Map.empty } resTm = foldl merge thisTm superTMs thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) True False cTys [] resTm -- TODO: Include proper values- extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig)+ extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps [] thisSig) ---------------------------------------------------------------@@ -164,12 +164,12 @@ (spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs withFoldMap spawnActorVd spawns $--- withFoldMap aliasActorVd unstables $+-- withFoldMap unknownActorVd unstables $ withFoldMap evalActorVd stables $ do --debug "fetchActors complete" tcba - where spawnActorVd, evalActorVd -- , aliasActorVd + where spawnActorVd, evalActorVd -- , unknownActorVd :: ([Modifier ()],VarDecl ()) -> TcDeclM a -> TcDeclM a -- Only Nothing for initializer spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do@@ -183,15 +183,15 @@ fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid {- -- All non-final OR non-static- aliasActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do+ unknownActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do p <- getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)- a <- aliasActorId+ a <- unknownActorId withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra- aliasActorVd (_, VarDecl _ arvid _) _ =+ unknownActorVd (_, VarDecl _ arvid _) _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -} -- Final, with explicit initializer@@ -203,8 +203,8 @@ tm <- getTypeMap case lookupNamed actors n tm of Just a -> return a- Nothing -> aliasActorId --fail "Internal error: no such actor"- _ -> aliasActorId+ Nothing -> unknownActorId --fail "Internal error: no such actor"+ _ -> unknownActorId withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra@@ -259,8 +259,8 @@ check (all (\m -> not (isPolicyMod m || isLockStateMod m)) ms) $ "Methods annotated with typemethod cannot have policy or lock state modifiers" -- 3. Same check for parameters- let plms = [ m | FormalParam _ pms _ _ _ <- ps, m <- pms, - isPolicyMod m, isLockStateMod m ]+ let (pis, pmss) = unzip [ (pI, pms) | FormalParam _ pms _ _ (VarId _ pI) <- ps ]+ plms = [ m | m <- concat pmss, isPolicyMod m, isLockStateMod m ] check (null plms) $ "Parameters to typemethods must not have policy modifiers" -- 4. No exceptions may be thrown check (null exns) $ "Methods annotated with typemethod may not throw exceptions"@@ -270,7 +270,8 @@ mRetType = rTy, mRetPol = bottom, mWrites = top,- mPars = [ bottom | _ <- ps ],+ mPars = pis,+ mParPols = [ bottom | _ <- ps ], mExpects = [], mLMods = noMods, mExns = []@@ -422,7 +423,7 @@ -- 1. Check return type ty <- evalReturnType retT -- 2. Check parameter types and policy modifiers- (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps+ (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps let pInfos = zip3 ps pTs pPols -- 3. Typecheck and evaluate policy modifiers withFoldMap withParam pInfos $ checkPolicyMods st ms @@ -439,7 +440,8 @@ mRetType = ty, mRetPol = rPol, mWrites = wPol,- mPars = pPols,+ mPars = pIs,+ mParPols = pPols, mExpects = es, mLMods = lms, mExns = xSigs@@ -459,7 +461,7 @@ -- 0. Setup type parameters withFoldMap withTypeParam tps $ do -- 1. Check parameter types and policy modifiers- (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps+ (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps let pInfos = zip3 ps pTs pPols -- 2. Typecheck and evaluate policy modifiers withFoldMap withParam pInfos $ checkPolicyMods st ms @@ -473,7 +475,8 @@ wPol <- getWritePolicy ms let cti = CSig { cWrites = wPol,- cPars = pPols,+ cPars = pIs,+ cParPols = pPols, cExpects = es, cLMods = lms, cExns = xSigs@@ -552,7 +555,7 @@ let es = concat [ l | Expects _ l <- ms ] mapM evalLock es -typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, ActorPolicy)+typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy) typeCheckParam st (FormalParam _ ms t ell (VarId _ i)) = do withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do -- 1. Check parameter type@@ -561,7 +564,7 @@ checkPolicyMods st ms "typeCheckSignature: At most one read modifier allowed per parameter" rPol <- getParamPolicy i ms- return (if ell then arrayType ty bottom else ty, rPol)+ return (if ell then arrayType ty bottom else ty, i, rPol) typeCheckParam _ (FormalParam _ _ _ _ arvid) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid @@ -680,7 +683,7 @@ let isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b- Just (MSig tyRet pRet 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 @@ -704,7 +707,7 @@ -- debug $ "Using env: " ++ show env -- Setup the state in which to check the body- parAids <- concat <$> mapM aliasIfActor (zip pars tysPs)+ parAids <- concat <$> mapM unknownIfActor (zip pars tysPs) let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } @@ -719,7 +722,7 @@ "Declared lock modifiers not general enough: " ++ show lMods mapM_ (checkExnMods endSt) exnLMods return $ MethodDecl Nothing (map notAppl _ms) (map notAppl tps) - (fmap notAppl _rt) (notAppl i) (map notAppl ps) (map notAppl _exs) mb'+ (notAppl _rt) (notAppl i) (map notAppl ps) (map notAppl _exs) mb' typeCheckMethodDecl _ md = panic (typeCheckerBase ++ ".typeCheckMethodDecl") $ "Applied to non-method decl " ++ show md@@ -735,7 +738,7 @@ let isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b- Just (CSig pPars pWri expLs lMods xSigs) <- + Just (CSig _pIs pPars pWri expLs lMods xSigs) <- Map.lookup (tps, tysPs, isVarArity) . constrs <$> getTypeMap -- Setup the environment in which to check the body@@ -763,7 +766,7 @@ --debug $ "Using branch map: " ++ show (branchPCE env) -- Setup the state in which to check the body- parAids <- concat <$> mapM aliasIfActor (zip pars tysPs)+ parAids <- concat <$> mapM unknownIfActor (zip pars tysPs) let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } @@ -784,9 +787,9 @@ typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $ "Applied to non-constructor decl " ++ show md -aliasIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)]-aliasIfActor (i, ty)- | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]+unknownIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)]+unknownIfActor (i, ty)+ | ty == actorT = unknownActorId >>= \aid -> return [(i, aid)] | otherwise = return []
src/Language/Java/Paragon/TypeCheck/Actors.hs view
@@ -21,12 +21,16 @@ -- which actor(s) it can represent, we list that. -- Otherwise an empty list means it could be an alias -- of any other actor.-data ActorId = Fresh Int String | Alias Int | ActorTPVar (Ident ())+data ActorId = Fresh Int String + | Instance (Name ()) Int + | Unknown Int+ | ActorTPVar (Ident ()) deriving (Show, Eq, Ord, Data, Typeable) instance Pretty ActorId where pretty (Fresh k s) = text s <> text ('#':show k)- pretty (Alias k) = text ('@':show k)+ pretty (Instance n k) = pretty n <> text ('#':'#':show k) + pretty (Unknown k) = text ('@':show k) pretty (ActorTPVar i) = pretty i @@ -36,12 +40,16 @@ unifies :: ActorId -> ActorId -> Bool -- If we have the exact (fresh) ids, we can tell exactly unifies (Fresh x _) (Fresh y _) = x == y-unifies _ _ = True+-- If we have two fresh instance ids, they could be aliases of the same instance+unifies (Instance n1 _) (Instance n2 _) = n1 == n2+unifies (Unknown _) _ = True+unifies _ (Unknown _) = True+unifies _ _ = False -- If either side is an alias, check if it could represent the fresh side.---unifies (Alias x xs) (Fresh y) = null xs || y `elem` xs---unifies (Fresh x) (Alias y ys) = null ys || x `elem` ys+--unifies (Unknown x xs) (Fresh y) = null xs || y `elem` xs+--unifies (Fresh x) (Unknown y ys) = null ys || x `elem` ys -- If both are aliases, check if they could represent the same fresh actor.---unifies (Alias x xs) (Alias y ys) = null xs || null ys || (not . null) (xs `intersect` ys)+--unifies (Unknown x xs) (Unknown y ys) = null xs || null ys || (not . null) (xs `intersect` ys) unify :: [ActorId] -> [ActorId] -> Bool unify xs ys = all (uncurry unifies) $ zip xs ys @@ -49,30 +57,33 @@ {- equals :: ActorId -> ActorId -> Bool equals (Fresh x) (Fresh y) = x == y-equals (Alias x _) (Alias y _) = x == y+equals (Unknown x _) (Unknown y _) = x == y equals _ _ = False reprs :: ActorId -> [Int] reprs (Fresh x) = [x]-reprs (Alias x xs) = x:xs+reprs (Unknown x xs) = x:xs -} getId :: ActorId -> Int getId (Fresh x _) = x-getId (Alias x ) = x+getId (Unknown x ) = x getId _ = panic "getId" "Trying to get ActorId of ActorTPVar, which should have been instantiated" {- reprName :: ActorId -> Name reprName (Fresh _ n) = n-reprName (Alias _ _ n) = n+reprName (Unknown _ _ n) = n -} -newAlias :: Uniq -> IO ActorId-newAlias u = do uniq <- getUniq u- return $ Alias uniq+newUnknown :: Uniq -> IO ActorId+newUnknown u = do uniq <- getUniq u+ return $ Unknown uniq newFresh :: Uniq -> String -> IO ActorId newFresh u str = do uniq <- getUniq u return $ Fresh uniq str +newInstance :: Uniq -> Name () -> IO ActorId+newInstance u n = do uniq <- getUniq u+ return $ Instance n uniq
src/Language/Java/Paragon/TypeCheck/Constraints.hs view
@@ -26,6 +26,7 @@ splitCstrs (LRT g ls p q) = map (\x -> LRT 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!! disjoin p' = [p'] @@ -39,9 +40,9 @@ case mpol of Nothing -> return True Just _ -> panic "MetaVar assigned to a Policy : shouldn't occur here." ""-isCstrVar (LRT _ _ _ (Join _ _)) +isCstrVar (LRT _ _ _ _) = panic (constraintsModule ++ ".isCstrVar") - "Right-side of a constrain shouldn't be a join !"+ "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@@ -51,7 +52,8 @@ 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 (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) partitionM :: (Constraint -> IO Bool) -> [Constraint] -> IO([Constraint], [Constraint]) partitionM f xs = do
src/Language/Java/Paragon/TypeCheck/Containment.hs view
@@ -27,8 +27,8 @@ Either Bool Constraint lrt g ls p q = case (p, q) of - (_, Join _ _) -> panic (containmentModule ++ ".lrt") - $ "Join occuring on the right-hand side of an lrt check: " ++ show q + (_, 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 p1 p2, _) -> let ap1 = lrt g ls p1 q @@ -38,7 +38,14 @@ (Left True, _) -> ap2 (_, Left True) -> ap1 _ -> Right (LRT g ls p q) - + (_, Meet q1 q2) -> let + ap1 = lrt g ls p q1 + ap2 = lrt 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)
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -23,8 +23,8 @@ addBranchPC, addBranchPCList, getActorId, setActorId, - newActorId, newActorIdWith, newAliasId,- freshActorId, aliasActorId,+ newActorId, newActorIdWith, newUnknownId,+ freshActorId, unknownActorId, scrambleActors, getPolicy,@@ -91,7 +91,8 @@ import Language.Java.Paragon.TypeCheck.Containment import Language.Java.Paragon.TypeCheck.Constraints -import Control.Monad (filterM, zipWithM)+import Control.Monad hiding (join) -- (filterM, zipWithM, when)+--import qualified Control.Monad (join) as Monad import Control.Applicative ( (<$>), (<*>) ) --import Control.Arrow ( first, second ) import qualified Data.Map as Map@@ -149,7 +150,7 @@ newVmap = Map.insert i vti oldVmap in env { vars = newVmap } -lookupActorName :: ActorName () -> TcCodeM (TcType, ActorPolicy)+lookupActorName :: ActorName () -> TcCodeM (TcStateType, ActorPolicy) lookupActorName (ActorName _ nam@(Name _ nt mPre i)) | nt == EName = do (ty, pol, _) <- lookupVar mPre i@@ -166,35 +167,35 @@ -- | 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 (Maybe TcType, TypeMap, ActorPolicy)+lookupPrefixName :: Name () -> TcCodeM (Maybe TcStateType, 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+ (sty, p, _) <- lookupVar Nothing i+ debugPrint $ "lookupPrefixName: " ++ prettyPrint i ++ " :: " ++ show sty tm <- getTypeMap- case lookupTypeOfT ty tm of- Right newSig -> return (Just ty, tMembers newSig, p)+ case lookupTypeOfStateT sty tm of+ Right newSig -> return (Just sty, 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)+ (mPreSty, preTm, prePol) <- case mPre of+ Nothing -> do return (Nothing, baseTm, bottom)+ Just pre -> lookupPrefixName pre 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)+ -- debugPrint $ show (packages baseTm2) ++ "\n"+ 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 _ -> panic (monadModule ++ ".lookupPrefixName") $ "Unknown type: " ++ show ty@@ -202,15 +203,17 @@ $ "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)+ (_tps, _iaps, tsig) <- case Map.lookup i $ types preTm of+ Nothing -> liftTcDeclM $ fetchType n+ -- panic (monadModule ++ ".lookupPrefixName")+ -- $ "Not a type: " ++ show n+ Just tinfo -> return tinfo+-- This lookup arises from refering to static fields, and then type arguments aren't given.+-- TODO: Check that field *is* static.+-- check (null tps) $+-- "Type " ++ prettyPrint n ++ " expects " ++ +-- show (length tps) ++ " but has been given none."+ return (Just . stateType . TcRefT $ tType tsig, tMembers tsig, prePol) PName -> case Map.lookup i $ packages preTm of Nothing -> do liftTcDeclM $ fetchPkg n@@ -228,25 +231,34 @@ -- | 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 (TcType, ActorPolicy, Bool)+lookupVar :: Maybe (Name ()) -> Ident () -> TcCodeM (TcStateType, ActorPolicy, Bool) lookupVar Nothing i = do -- Could be a single variable+ let nam = Name () EName Nothing i -- Reconstructing for lookups varMap <- vars <$> getEnv case Map.lookup i varMap of -- Is a variable- Just (VSig ty p param _ _) -> return (ty, p, param)+ Just (VSig ty p param _ _) -> do+ sty <- getStateType (Just nam) Nothing ty+ return (sty, p, param) -- Not a variable, must be a field Nothing -> do tm <- getTypeMap case Map.lookup i $ fields tm of- Just (VSig ty p param _ _) -> return (ty, p, param)+ Just (VSig ty p param _ _) -> do+ sty <- getStateType (Just nam) Nothing ty+ return (sty, p, param) 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)+ Just (VSig ty p _ _ _) -> do+ sty <- getStateType (Just (Name () EName (Just pre) i)) mPreTy ty+ debugPrint $ "lookupVar: " ++ prettyPrint pre ++ "." ++ prettyPrint i+ ++ " :: " ++ show sty+ return (sty, prePol `joinWThis` p, False) Nothing -> case mPreTy of Just preTy -> fail $ "Type " ++ prettyPrint preTy ++@@ -282,9 +294,9 @@ | 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+ (a `isAssignableTo` p) `orM` (a `isAssignableTo` arrayType p bottom)+ checkTys True [p] as = and <$> mapM (`isAssignableTo` p) as+ checkTys b (p:ps) (a:as) = (&&) <$> (a `isAssignableTo` p) <*> checkTys b ps as checkTys _ _ _ = return False findBestFit :: [Sig] -> TcCodeM [Sig]@@ -300,7 +312,7 @@ if and bs1 then go xs ys else go (y:xs) ys moreSpecificThan :: Sig -> Sig -> TcCodeM Bool- moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (=<:) ps2 ps1+ moreSpecificThan (_,ps1,False) (_,ps2,False) = and <$> zipWithM (isAssignableTo) ps1 ps2 moreSpecificThan (_,ps1,True ) (_,ps2,True ) = do let n = length ps1 k = length ps2@@ -314,6 +326,7 @@ -> [TcType] -- Argument types -> TcCodeM (ActorPolicy, [TypeParam ()], MethodSig) lookupMethod mPre i tArgs argTys = do+ debugPrint $ "lookupMethod: " ++ show (mPre, i, argTys) baseTm <- getTypeMap (mPreTy, preTm, prePol) <- case mPre of Nothing -> return (Nothing, baseTm, bottom)@@ -383,23 +396,23 @@ Just p -> return p -lookupFieldT :: TcType -> Ident () -> TcCodeM VarFieldSig+lookupFieldT :: TcStateType -> Ident () -> TcCodeM VarFieldSig lookupFieldT typ i = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ- aSig <- lookupTypeOfType typ+ aSig <- lookupTypeOfStateType 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 +lookupMethodT :: TcStateType -> Ident () -> [TypeArgument ()] -> [TcType] -> TcCodeM ([TypeParam ()], MethodSig) lookupMethodT typ i tArgs argTys = do check (isRefType typ) $ "Not a reference type: " ++ prettyPrint typ- aSig <- lookupTypeOfType typ+ aSig <- lookupTypeOfStateType typ case Map.lookup i (methods $ tMembers aSig) of Nothing -> fail $ "Class " ++ prettyPrint typ ++ " does not have a method named " ++ prettyPrint i@@ -429,15 +442,15 @@ lookupConstr :: TcClassType -> [TypeArgument ()] -> [TcType] - -> TcCodeM ([TypeParam ()], ConstrSig)+ -> TcCodeM ([TypeParam ()], [Ident ()], ConstrSig) lookupConstr ctyp tArgs argTys = do- debugPrint $ "\n\n######## Looking up constructor! ######## \n"+-- debugPrint $ "\n\n######## Looking up constructor! ######## \n" let typ = clsTypeToType ctyp- debugPrint $ "typ: " ++ show typ- aSig <- lookupTypeOfType typ- debugPrint $ "aSig: " ++ show aSig+-- debugPrint $ "typ: " ++ show typ+ (iaps, aSig) <- lookupTypeOfType typ+-- debugPrint $ "aSig: " ++ show aSig let cMap = constrs $ tMembers aSig- debugPrint $ "cMap: " ++ show cMap+-- debugPrint $ "cMap: " ++ show cMap bests <- findBestMethod tArgs argTys (Map.keys cMap) case bests of [] -> fail $ "Type " ++ prettyPrint ctyp ++@@ -455,7 +468,7 @@ 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)+ Just csig -> return (tps, iaps, csig) --lookupLock :: Name () -> TcCodeM LockSig@@ -548,13 +561,131 @@ startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -} +-- Instance analysis++getStateType :: Maybe (Name ()) -- field/var name (if decidable) + -> Maybe TcStateType -- containing object state type+ -> TcType -- field/var/cell type+ -> TcCodeM TcStateType+getStateType mn mtyO ty + | ty == actorT = do actorIdT <$> getActorId mn mtyO+ | ty == policyT = do policyPolT <$> getPolicyBounds mn mtyO+ | Just ct <- mClassType ty = instanceT ct <$> getInstanceActors mn ct+ | otherwise = return $ stateType ty++registerStateType :: Ident ()+ -> TcType+ -> Maybe (TcStateType) -> TcCodeM TcStateType+registerStateType i tyV mSty | tyV == actorT = do+ case mSty of+ Nothing -> actorIdT <$> newActorId i -- fresh generation+ Just sty -> case mActorId sty of+ Nothing -> panic (monadModule ++ ".registerStateType")+ $ "Actor state but non-actor target type: " + ++ show (tyV, sty)+ Just aid -> do+ newActorIdWith i aid+ return $ actorIdT aid++registerStateType i tyV mSty | tyV == policyT = do+ let pbs = case mSty of+ Nothing -> PolicyBounds bottom top+ Just sty -> case mPolicyPol sty of+ Nothing -> panic (monadModule ++ ".registerStateType")+ $ "Policy state but non-policy target type: "+ ++ show (tyV, sty)+ Just bs -> bs+ updateState $ \s -> + s { policySt = Map.insert (mkSimpleName EName i) pbs $ policySt s }+ return $ policyPolT pbs++registerStateType i tyV mSty | Just ct <- mClassType tyV = do+ debugPrint $ "registerStateType: " ++ show (i, tyV, mSty)+ case mSty of+ -- no initialiser+ Nothing -> return $ instanceT ct [] -- ??+ Just sty -> case mInstanceType sty of+ Just (_, aids) -> do+ updateState $ \s ->+ s { instanceSt = Map.insert (mkSimpleName EName i) aids + $ instanceSt s }+ return $ instanceT ct aids+ Nothing | isNullType sty -> return $ instanceT ct []+ | otherwise -> panic (monadModule ++ ".registerStateType")+ $ "Instance state but non-instance target type: "+ ++ show (tyV, sty)+ +++registerStateType _i tyV _mSty = return $ stateType tyV++updateStateType :: Maybe (Name ()) -- field/var name (if decidable)+ -> Maybe (TcType) -- Containing object type+ -> TcType -- field/var/cell type+ -> Maybe TcStateType -- rhs state type (Nothing if no init)+ -> TcCodeM TcStateType+updateStateType mN mTyO tyV mSty | tyV == actorT = do+ case mSty of+ Just sty | Just aid <- mActorId sty -> do+ maybeM mTyO $ \tyO -> scrambleActors (Just tyO)+ maybeM mN $ \n -> setActorId n aid+ return sty++ | otherwise -> panic (monadModule ++ ".updateStateType")+ $ "Actor state but non-actor target type: " + ++ show (tyV, sty)+ Nothing -> panic (monadModule ++ ".updateStateType")+ $ "No state for actor assignment: " ++ show mN++-- TODO+{-+updateStateType mN mTyO tyV mSty | tyV == policyT = do+ case mSty of+ Just sty | Just pbs <- mPolicyPol sty -> do+-}+updateStateType _mN _mTyO _ty (Just sty) = return sty+updateStateType _mN _mTyO ty Nothing = return $ stateType ty+++-- Instance Analysis++getInstanceActors :: Maybe (Name ()) -> TcClassType -> TcCodeM [ActorId]+getInstanceActors mn ct@(TcClassT tyN _) = do+ instanceMap <- instanceSt <$> getState+ case maybe Nothing (\n -> Map.lookup n instanceMap) mn of+ Nothing -> do+ (iaps, _) <- lookupTypeOfType (clsTypeToType ct)+ mapM (instanceActorId . Name () EName (Just tyN)) iaps+ Just aids -> return aids+ +-- Policy Analysis++getPolicyBounds :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorPolicyBounds+getPolicyBounds mn mtyO = do+ policyMap <- policySt <$> getState+ case maybe Nothing (\n -> Map.lookup n policyMap) mn of+ Nothing -> case (mtyO, mn) of+ (Just styO, Just (Name _ _ _ i)) -> do+ tsig <- lookupTypeOfStateType styO+ case Map.lookup i $ policies $ tMembers tsig of+ Just pol -> return $ KnownPolicy pol+ Nothing -> return $ PolicyBounds bottom top+ _ -> return $ PolicyBounds bottom top+ Just pif -> return pif+ -- Actor Analysis -getActorId :: Name () -> TcCodeM ActorId-getActorId n = do- actorMap <- actorSt <$> getState- case Map.lookup n actorMap of- Nothing -> liftTcDeclM $ aliasActorId+getActorId :: Maybe (Name ()) -> Maybe TcStateType -> TcCodeM ActorId+getActorId mn mtyO = do+ actorMap <- actorSt <$> getState + case maybe Nothing (\n -> Map.lookup n actorMap) mn of+ Nothing -> case (mtyO, mn) of+ (Just styO, Just (Name _ _ _ i)) -> do+ tsig <- lookupTypeOfStateType styO+ case Map.lookup i $ actors $ tMembers tsig of+ Just aid -> return aid+ Nothing -> liftTcDeclM $ unknownActorId+ _ -> liftTcDeclM $ unknownActorId Just ai -> return $ aID ai setActorId :: Name () -> ActorId -> TcCodeM ()@@ -577,9 +708,9 @@ newActorIdWith i aid return aid -newAliasId :: Ident () -> TcCodeM ActorId-newAliasId i = do- aid <- liftTcDeclM aliasActorId+newUnknownId :: Ident () -> TcCodeM ActorId+newUnknownId i = do+ aid <- liftTcDeclM unknownActorId newActorIdWith i aid return aid @@ -689,11 +820,10 @@ getGlobalLockProps :: TcCodeM [TcClause TcAtom] getGlobalLockProps = do cs <- go <$> getTypeMap- debugPrint $ "Fetching global lock props: " ++ show cs return 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+ tlps = map (go . tMembers . (\(_,_,x) -> x)) $ Map.elems $ types tm plps = map go $ Map.elems $ packages tm in concat $ lps ++ tlps ++ plps @@ -725,18 +855,18 @@ case Map.lookup exnTy exnMap of Nothing -> fail $ "Unchecked exception: " ++ prettyPrint (typeName_ exnTy) Just (rE, wE) -> do- constraint [] wX wE $+ constraint [] wE wX $ "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?+ constraint [] rX rE $ -- 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 " ++ + " is invoked expects its policy to be no more restrictive than " ++ prettyPrint rE @@ -748,18 +878,19 @@ -- 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, (=<:) :: MonadTcDeclM m => TcType -> TcType -> m Bool+isAssignableTo :: MonadTcDeclM m => TcType -> TcType -> m Bool isAssignableTo t1 t2 = liftTcDeclM $ if t1 == t2 -- identity conversion then return True else t1 `widensTo` t2 -- widening conversion -(=<:) = flip isAssignableTo+(=<:) :: MonadTcDeclM m => TcType -> TcStateType -> m Bool+lhs =<: rhs = isAssignableTo (unStateType rhs) lhs -isCastableTo, (<<:) :: MonadTcDeclM m- => TcType - -> TcType - -> m (Bool, Bool) -- (Can be cast, needs reference narrowing)+isCastableTo :: MonadTcDeclM m+ => TcType + -> TcType + -> m (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.@@ -787,7 +918,8 @@ return (True, True) _ -> return (False, False) -(<<:) = flip isCastableTo+(<<:) :: MonadTcDeclM m => TcType -> TcStateType -> m (Bool, Bool)+lhs <<: rhs = isCastableTo (unStateType rhs) lhs -- widening conversion can come in four basic shapes:@@ -806,10 +938,11 @@ TcClsRefT ct -> maybe (return False) (\pt -> TcPrimT pt `widensTo` t2) (unbox ct) _ -> return False--- 5) Paragon-specific types+{-- 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 Bool@@ -822,18 +955,17 @@ Left Nothing -> do case rt of TcClsRefT (TcClassT n tas) -> do- (tps, tsig) <- fetchType n+ (tps, _iaps, 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+ Right (_,tsig) -> return tsig let sups = tSupers tsig impls = tImpls tsig--- obj = if null sups then [objectT] else []- allS = map TcClsRefT $ sups ++ impls -- ++ obj+ allS = map TcClsRefT $ sups ++ impls supsups <- mapM superTypes allS return $ concat $ allS:supsups
src/Language/Java/Paragon/TypeCheck/Monad/CodeState.hs view
@@ -1,4 +1,8 @@-module Language.Java.Paragon.TypeCheck.Monad.CodeState where+module Language.Java.Paragon.TypeCheck.Monad.CodeState+ (+ module Language.Java.Paragon.TypeCheck.Monad.CodeState,+ PolicyBounds(..), ActorPolicy, ActorPolicyBounds+ ) where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty@@ -14,14 +18,17 @@ import qualified Data.Map as Map import Data.List (intersect, union) import Data.Maybe (fromJust)+import Control.Monad (zipWithM {-, when -}) codeStateModule :: String codeStateModule = typeCheckerBase ++ ".Monad.CodeState" data CodeState = CodeState {- actorSt :: ActorMap,- lockMods :: LockMods,- exnS :: ExnsMap+ actorSt :: ActorMap,+ policySt :: PolicyMap,+ instanceSt :: InstanceMap,+ lockMods :: LockMods,+ exnS :: ExnsMap } deriving (Eq, Show) @@ -32,15 +39,101 @@ mergeStates :: Uniq -> CodeState -> CodeState -> IO CodeState mergeStates u s1 s2 = do- newActors <- mergeActors u (actorSt s1) (actorSt s2)- newExns <- mergeExns u (exnS s1) (exnS s2)+ newActors <- mergeActors u (actorSt s1) (actorSt s2)+ newPols <- mergePolicies (policySt s1) (policySt s2)+ newInsts <- mergeInstances u (instanceSt s1) (instanceSt s2)+ newExns <- mergeExns u (exnS s1) (exnS s2) return $ CodeState { - actorSt = newActors,- lockMods = lockMods s1 <++> lockMods s2,- exnS = newExns+ actorSt = newActors,+ policySt = newPols,+ instanceSt = newInsts,+ lockMods = lockMods s1 <++> lockMods s2,+ exnS = newExns } ------------------------------------------+-- Instance tracking+------------------------------------------++type InstanceMap = Map.Map (Name ()) [ActorId]+{-type InstanceMap = Map.Map (Ident ()) InstanceSig++data InstanceSig = ISig {+ iType :: TcType,+ iImplActorArgs :: [ActorId],+ iMembers :: InstanceMap+ }+ deriving (Show, Eq)+ +mergeInstances :: Uniq -> InstanceMap -> InstanceMap -> IO InstanceMap+mergeInstances u im1 im2 = do+ let newKeys = Map.keys im1 `intersect` Map.keys im2+ oldVals = map (\k -> (fromJust (Map.lookup k im1), fromJust (Map.lookup k im2))) newKeys+ newVals <- mapM mergeISigs oldVals+ return $ Map.fromList $ zip newKeys newVals+ where mergeISigs :: (InstanceSig, InstanceSig) -> IO InstanceSig+ mergeISigs (is1, is2) = do+ when (iType is1 /= iType is2) $+ panic (codeStateModule ++ ".mergeInstances:mergeISigs")+ $ show (is1, is2)+ as <- mergeIas (iImplActorArgs is1) (iImplActorArgs is2)+ newMems <- mergeInstances u (iMembers is1) (iMembers is2)+ return $ ISig (iType is1) as newMems++ mergeIas :: [ActorId] -> [ActorId] -> IO [ActorId]+ mergeIas ias1 ias2 = zipWithM mergeIa ias1 ias2+ + mergeIa :: ActorId -> ActorId -> IO ActorId+ mergeIa ai1 ai2 + | ai1 == ai2 = return ai1+ mergeIa (Instance n _) _ = newInstance u n+ mergeIa ai _ = panic (codeStateModule ++ ".mergeIas")+ $ "Instance has non-instance implicit argument: " ++ show ai++-}++mergeInstances :: Uniq -> InstanceMap -> InstanceMap -> IO InstanceMap+mergeInstances u im1 im2 = do+ let newKeys = Map.keys im1 `intersect` Map.keys im2+ oldVals = map (\k -> (fromJust (Map.lookup k im1), fromJust (Map.lookup k im2))) newKeys+ newVals <- mapM (uncurry mergeIas) oldVals+ return $ Map.fromList $ zip newKeys newVals+ where mergeIas :: [ActorId] -> [ActorId] -> IO [ActorId]+ mergeIas ias1 ias2 = zipWithM mergeIa ias1 ias2+ + mergeIa :: ActorId -> ActorId -> IO ActorId+ mergeIa ai1 ai2 + | ai1 == ai2 = return ai1+ mergeIa (Instance n _) _ = newInstance u n+ mergeIa ai _ = panic (codeStateModule ++ ".mergeIas")+ $ "Instance has non-instance implicit argument: " ++ show ai++------------------------------------------+-- Policy tracking+------------------------------------------++type PolicyMap = Map.Map (Name ()) ActorPolicyBounds++mergePolicies :: PolicyMap -> PolicyMap -> IO PolicyMap+mergePolicies pm1 pm2 = do+ let newKeys = Map.keys pm1 `intersect` Map.keys pm2+ oldVals = map (\k -> (fromJust (Map.lookup k pm1), fromJust (Map.lookup k pm2))) newKeys+ newVals = map mergePs oldVals+ return $ Map.fromList $ zip newKeys newVals++mergePs :: (ActorPolicyBounds, ActorPolicyBounds) -> ActorPolicyBounds+mergePs pis =+ case pis of+ (KnownPolicy p, KnownPolicy q)+ | p == q -> KnownPolicy p+ | otherwise -> mkBounds p q p q+ (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2+ (KnownPolicy p, PolicyBounds q1 q2) -> mkBounds p q1 p q2+ (PolicyBounds p1 p2, KnownPolicy q ) -> mkBounds p1 q p2 q++ where mkBounds a b c d = PolicyBounds (a `meet` b) (c `join` d)++------------------------------------------ -- Actor analysis ------------------------------------------ @@ -65,7 +158,7 @@ scramble' :: Uniq -> Stability -> ActorInfo -> IO ActorInfo scramble' u stab a@(AI _ stab') = if scrambles stab stab' - then do aid' <- newAlias u+ then do aid' <- newUnknown u return $ AI aid' stab' else return a @@ -73,14 +166,14 @@ mergeActors :: Uniq -> ActorMap -> ActorMap -> IO ActorMap mergeActors u a1 a2 = do let newKeys = Map.keys a1 `intersect` Map.keys a2- oldVals = map (\k -> (fromJust (Map.lookup k a1), fromJust (Map.lookup k a1))) newKeys+ oldVals = map (\k -> (fromJust (Map.lookup k a1), fromJust (Map.lookup k a2))) newKeys newVals <- mapM (mergeInfo u) oldVals return $ Map.fromList $ zip newKeys newVals mergeInfo :: Uniq -> (ActorInfo, ActorInfo) -> IO ActorInfo mergeInfo _ (ai1,ai2) | ai1 == ai2 = return ai1 mergeInfo u ((AI _ st),_) = do- aid <- newAlias u+ aid <- newUnknown u return $ AI aid st ------------------------------------------
src/Language/Java/Paragon/TypeCheck/Monad/TcCodeM.hs view
@@ -44,7 +44,8 @@ setupStartState = do tm <- getTypeMap let aMap = gatherActorInfo tm- return $ CodeState aMap noMods Map.empty+ pMap = gatherPolicyBounds tm+ return $ CodeState aMap pMap Map.empty noMods Map.empty -- TODO: Will fields affect instances? gatherActorInfo :: TypeMap -> Map (Name ()) ActorInfo@@ -54,7 +55,7 @@ let acts = Map.assocs $ actors tm -- :: [(Ident, ActorId)] aMap = Map.fromList $ map (mkInfo mPre $ fields tm) acts tMap = gatherActorInfoAux TName mPre - (Map.assocs $ Map.map (tMembers . snd) $ types tm)+ (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm) pMap = gatherActorInfoAux PName mPre (Map.assocs $ packages tm) in foldl1 Map.union [aMap, tMap, pMap] @@ -81,6 +82,39 @@ aux (i,tm) = let pre = Name () nt mPre i in gatherActorInfo' (Just pre) tm++-- TODO: non-final policies should have bounds bottom/top+gatherPolicyBounds :: TypeMap -> Map (Name ()) ActorPolicyBounds+gatherPolicyBounds = gatherPolicyBounds' Nothing++ where gatherPolicyBounds' mPre tm =+ let pols = Map.assocs $ policies tm -- :: [(Ident, ActorPolicy)]+ aMap = Map.fromList $ map (mkPols mPre $ fields tm) pols+ tMap = gatherPolicyBoundsAux TName mPre+ (Map.assocs $ Map.map (tMembers . (\(_,_,x) -> x)) $ types tm)+ pMap = gatherPolicyBoundsAux PName mPre (Map.assocs $ packages tm)+ in foldl1 Map.union [aMap, tMap, pMap]++ mkPols :: Maybe (Name ())+ -> Map (Ident ()) VarFieldSig + -> (Ident (), ActorPolicy) + -> (Name (), ActorPolicyBounds)+ mkPols mPre fs (i,p) = + case Map.lookup i fs of+ Just _ -> (Name () EName mPre i, KnownPolicy p)+ _ -> panic (tcCodeMonadModule ++ ".gatherActorInfo") $ + "No field for corresponding actor " ++ show i++ gatherPolicyBoundsAux :: NameType + -> Maybe (Name ()) + -> [(Ident (), TypeMap)] + -> Map (Name ()) ActorPolicyBounds+ gatherPolicyBoundsAux nt mPre = foldl Map.union Map.empty . map aux+ where aux :: (Ident (), TypeMap) -> Map (Name ()) ActorPolicyBounds+ aux (i,tm) = + let pre = Name () nt mPre i+ in gatherPolicyBounds' (Just pre) tm+ -- Running in parallel
src/Language/Java/Paragon/TypeCheck/Monad/TcDeclM.hs view
@@ -9,7 +9,8 @@ fetchPkg, fetchType, - getTypeMap, getThisType, getSuperType, lookupTypeOfType,+ getThisType, getThisStateType, getSuperType, + getTypeMap, lookupTypeOfType, lookupTypeOfStateType, withTypeParam, extendGlobalTypeMap, @@ -21,7 +22,7 @@ evalLock, evalActor, evalSrcLockProps, - freshActorId, aliasActorId,+ freshActorId, unknownActorId, instanceActorId, getReadPolicy, getWritePolicy, getLockPolicy, getParamPolicy, getReturnPolicy,@@ -47,16 +48,31 @@ import qualified Data.Map as Map import Data.List (partition)+import Data.Maybe (catMaybes) tcDeclMModule :: String tcDeclMModule = typeCheckerBase ++ ".Monad.TcDeclM" type TypeCheck m ast = ast () -> m (ast T) -lookupTypeOfType :: MonadTcDeclM m => TcType -> m TypeSig+lookupTypeOfStateType :: MonadTcDeclM m => TcStateType -> m TypeSig+lookupTypeOfStateType sty {-@(TcInstance{})-} = liftTcDeclM $ do+ tm <- getTypeMap+ case lookupTypeOfStateT sty tm of+ Right tsig -> return tsig+ Left Nothing -> fail $ "Unknown type: " ++ prettyPrint sty+ Left (Just err) -> fail err+{-+lookupTypeOfStateType _sty@(TcType ty) = liftTcDeclM $ do+ tm <- getTypeMap+ case lookupTypeOfT ty tm of+ Right (is, tsig) -> do+ ias <- mapM (instanceActorId . Name () EName +-}+lookupTypeOfType :: MonadTcDeclM m => TcType -> m ([Ident ()], TypeSig) lookupTypeOfType ty = liftTcDeclM $ do tm <- getTypeMap- debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm+-- debugPrint $ "lookupTypeOfType -- TypeMap:\n" ++ show tm case lookupTypeOfT ty tm of Right tsig -> return tsig Left Nothing -> fail $ "Unknown type: " ++ prettyPrint ty@@ -75,7 +91,7 @@ return () -fetchType :: Name () -> TcDeclM ([TypeParam ()], TypeSig)+fetchType :: Name () -> TcDeclM ([TypeParam ()],[Ident ()],TypeSig) fetchType n@(Name _ _ _ typName) = do withFreshCurrentTypeMap $ do debugPrint $ "Fetching type " ++ prettyPrint n ++ " ..."@@ -100,7 +116,7 @@ -- if using "clever lookup" instead of "clever setup" superTm <- case superTys of [] -> return emptyTM- [superTy] -> tMembers <$> lookupTypeOfType (clsTypeToType superTy)+ [superTy] -> tMembers . snd <$> lookupTypeOfType (clsTypeToType superTy) _ -> panic (tcDeclMModule ++ ".fetchType") $ "More than one super class for class:" ++ show superTys @@ -112,11 +128,12 @@ tImpls = implsTys, tMembers = superTm { constrs = Map.empty } }- extendGlobalTypeMap (extendTypeMapT n tps tsig)+ 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- let mDs = map unMemberDecl ds fetchActors n mDs $ do fetchLocks n mDs $ do fetchPols n mDs $ do@@ -151,7 +168,7 @@ -- Remove this line, and set tMembers to emptyTM, -- if using "clever lookup" instead of "clever setup" superTm <- foldl merge emptyTM <$> - mapM ((tMembers <$>) . lookupTypeOfType . clsTypeToType) superTys+ mapM ((tMembers . snd <$>) . lookupTypeOfType . clsTypeToType) superTys let tsig = TSig { tType = TcClsRefT $ TcClassT (mkSimpleName TName typName) [],@@ -162,7 +179,7 @@ tMembers = superTm } - extendGlobalTypeMap (extendTypeMapT n tps tsig)+ extendGlobalTypeMap (extendTypeMapT n tps [] tsig) -- withTypeMapAlways (extendTypeMapT n tps tsig) $ do withFoldMap withTypeParam tps $ do@@ -185,6 +202,11 @@ fetchType n = panic (tcDeclMModule ++ ".fetchType") $ show n +findImplActorParams :: [MemberDecl ()] -> [Ident ()]+findImplActorParams mds = [ i | FieldDecl _ ms [typeQQ| actor |] vds <- mds,+ Final () `elem` ms, not (Static () `elem` ms),+ VarDecl _ (VarId _ i) Nothing <- vds ]+ -- Actors fetchActors :: Name () -> [MemberDecl ()] -> TcDeclM a -> TcDeclM a@@ -201,26 +223,26 @@ (sstables, fstables) = partition (\(ms,_) -> Static () `elem` ms) stables (ssas, ssvs) <- unzip <$> mapM spawnActorVd sspawns- (fsas, fsvs) <- unzip <$> mapM spawnActorVd fspawns+ (fsas, fsvs) <- unzip <$> mapM paramActorVd fspawns (seas, sevs) <- unzip <$> mapM evalActorVd sstables (feas, fevs) <- unzip <$> mapM evalActorVd fstables--- (aas, avs) <- unzip <$> mapM aliasActorVd unstables+-- (aas, avs) <- unzip <$> mapM unknownActorVd unstables -- (eas, evs) <- unzip <$> mapM evalActorVd stables- let globTM = emptyTM { actors = Map.fromList (ssas ++ seas),+ let globTM = emptyTM { actors = Map.fromList (ssas ++ fsas ++ seas ++ feas), fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) } loclTM = emptyTM { actors = Map.fromList (ssas ++ fsas ++ seas ++ feas), fields = Map.fromList (ssvs ++ fsvs ++ sevs ++ fevs) } extendGlobalTypeMap (extendTypeMapN n $ merge globTM) withCurrentTypeMap (merge loclTM) $ do- debugPrint "Actors fetched"+-- debugPrint "Actors fetched" tdra - where spawnActorVd, evalActorVd --, aliasActorVd+ where spawnActorVd, evalActorVd, paramActorVd --, unknownActorVd :: ([Modifier ()], VarDecl ()) -> TcDeclM ((Ident (), ActorId), (Ident (),VarFieldSig))- -- Only Nothing for initializer+ -- Static, only Nothing for initializer spawnActorVd (ms, VarDecl _ (VarId _ i) _) = do a <- freshActorId (prettyPrint i) p <- getReadPolicy ms@@ -229,14 +251,22 @@ spawnActorVd (_, VarDecl _ arvid _) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid + paramActorVd (ms, VarDecl _ (VarId _ i) _) = do+ let a = ActorTPVar i+ p <- getReadPolicy ms+ let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)+ return ((i,a),(i,vti))+ paramActorVd (_, VarDecl _ arvid _) =+ fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid+ {- -- All non-final- aliasActorVd (ms, VarDecl _ (VarId _ i) _) = do+ unknownActorVd (ms, VarDecl _ (VarId _ i) _) = do p <- getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)- a <- aliasActorId+ a <- unknownActorId return ((i,a),(i,vti)) - aliasActorVd (_, VarDecl _ arvid _) =+ unknownActorVd (_, VarDecl _ arvid _) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -} -- Final, with explicit initializer@@ -248,8 +278,8 @@ tm <- getTypeMap case lookupNamed actors nam tm of Just a -> return a- Nothing -> aliasActorId --fail "Internal error: no such actor"- _ -> aliasActorId+ Nothing -> unknownActorId --fail "Internal error: no such actor"+ _ -> unknownActorId return ((i,a),(i,vti)) evalActorVd (_, VarDecl _ _ Nothing) @@ -273,7 +303,7 @@ let newTM = emptyTM { locks = Map.fromList lsigs } extendGlobalTypeMap (extendTypeMapN n $ merge newTM) withCurrentTypeMap (merge newTM) $ do- debugPrint $ "Locks fetched"+-- debugPrint $ "Locks fetched" tdra getLockModProps :: Ident () -> [Modifier ()] -> TcDeclM [TcClause TcAtom]@@ -309,7 +339,7 @@ extendGlobalTypeMap $ extendTypeMapN n $ merge globTM withCurrentTypeMap (merge loclTM) $ do -- withTypeMapAlways (extendTypeMapN n (merge $ emptyTM { policies = Map.fromList ips })) $ do- debugPrint $ "Policies fetched"+-- debugPrint $ "Policies fetched" tdra where fetchPol :: (Ident (), Exp (), a) -> TcDeclM (Ident (), ActorPolicy)@@ -329,7 +359,7 @@ withCurrentTypeMap (merge newTM) $ do -- withTypeMapAlways (extendTypeMapN n -- (merge $ emptyTM { typemethods = Map.fromList ipidbs })) $ do- debugPrint "TypeMethods fetched"+-- debugPrint "TypeMethods fetched" tdra where paramsToIdents (i, (ps,b)) = do@@ -354,7 +384,7 @@ methods = methodMap, constrs = constrMap } extendGlobalTypeMap $ extendTypeMapN n $ merge newTM- debugPrint "Signatures fetched"+-- debugPrint "Signatures fetched" return () where@@ -392,8 +422,8 @@ MethodDecl _ ms tps retT i ps exns _ -> do withFoldMap withTypeParam tps $ do tcty <- evalReturnType retT- (pTys, pPols) <- unzip <$> mapM paramInfo ps- rPol <- getReturnPolicy ms pPols + (pTys, pIs, pPols) <- unzip3 <$> mapM paramInfo ps+ rPol <- getReturnPolicy ms pPols wPol <- getWritePolicy ms exs <- mapM eSpecToSig exns expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ]@@ -402,7 +432,8 @@ let mti = MSig { mRetType = tcty, mRetPol = rPol,- mPars = pPols,+ mPars = pIs,+ mParPols = pPols, mWrites = wPol, mExpects = expects, mLMods = (closes, opens),@@ -426,14 +457,15 @@ case md of ConstructorDecl _ ms tps _ ps exns _ -> do withFoldMap withTypeParam tps $ do- (pTys, pPols) <- unzip <$> mapM paramInfo ps+ (pTys, pIs, pPols) <- unzip3 <$> mapM paramInfo ps wPol <- getWritePolicy ms exs <- mapM eSpecToSig exns expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ] closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ] opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ] let cti = CSig {- cPars = pPols,+ cPars = pIs,+ cParPols = pPols, cWrites = wPol, cExpects = expects, cLMods = (closes, opens),@@ -462,11 +494,11 @@ } return (ty, esig) - paramInfo :: FormalParam () -> TcDeclM (TcType, ActorPolicy)+ paramInfo :: FormalParam () -> TcDeclM (TcType, Ident (), ActorPolicy) paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do pPol <- getParamPolicy i ms pTy <- evalSrcType ty- return (pTy, pPol)+ return (pTy, i, pPol) paramInfo (FormalParam _ _ _ _ arvid) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid @@ -484,9 +516,9 @@ tm { policies = Map.insert i (RealPolicy $ TcRigidVar i) (policies tm), fields = Map.insert i vti (fields tm) }) $ tcba LockStateParam _ i -> do- let vti = VSig (lockT []) top False False True+ let lti = LSig top 0 [] withCurrentTypeMap (\tm ->- tm { fields = Map.insert i vti (fields tm) }) $ tcba+ tm { locks = Map.insert i lti (locks tm) }) $ tcba TypeParam _ _i _ -> do --withCurrentTypeMap (\tm -> -- tm { types = Map.insert i ([],Map.empty) (types tm) }) $ @@ -627,8 +659,10 @@ ------------------------------------------------------------------- -- Evaluating types -evalReturnType :: Maybe (Type ()) -> TcDeclM TcType-evalReturnType = maybe (return voidT) evalSrcType+evalReturnType :: ReturnType () -> TcDeclM TcType+evalReturnType (VoidType _) = return voidT+evalReturnType (LockType _) = fail $ "lock as return type not yet implemented" -- return TcLockRetT+evalReturnType (Type _ t) = evalSrcType t evalSrcType :: Type () -> TcDeclM TcType evalSrcType (PrimType _ pt) = return $ TcPrimT pt@@ -650,15 +684,15 @@ debugPrint $ "Evaluating class type: " ++ show ct baseTm <- getTypeMap -- debugPrint $ "Current type map: " ++ show baseTm- (tps, _tsig) <- case lookupNamed types n baseTm of- Nothing -> fetchType n - -- fail $ "Unknown type: " ++ prettyPrint n- Just res -> return res+ (tps,_iaps,_tsig) <- case lookupNamed types n baseTm of+ Nothing -> fetchType n + -- fail $ "Unknown type: " ++ prettyPrint n+ Just res -> return res - debugPrint $ "Type found"+-- debugPrint $ "Type found" tArgs <- mapM (uncurry evalSrcTypeArg) (zip tps tas)- debugPrint "Type arguments evaluated"- return $ TcClassT n tArgs+-- debugPrint "Type arguments evaluated"+ return $ TcClassT n tArgs -- TODO: Is this where I evaluate? Likely not. {- where aux :: TypeMap -- Typemap of outer type (or top-level) -> [(Ident (), [TcTypeArg])] -- Accumulated type (reversed)@@ -761,7 +795,7 @@ tm <- getTypeMap case lookupNamed actors n tm of Just aid -> return aid- Nothing -> aliasActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n+ Nothing -> unknownActorId -- fail $ "evalActor: No such actor: " ++ prettyPrint n evalAtom :: Atom () -> TcDeclM TcAtom evalAtom (Atom _ n as) = TcAtom n <$> mapM evalActor as@@ -780,7 +814,7 @@ " but now it doesn't exist!" Left (Just err) -> panic (tcDeclMModule ++ ".evalLock") $ err- Right tsig -> return $ tMembers tsig+ Right (_, tsig) -> return $ tMembers tsig case Map.lookup i $ locks tm of Just lsig -> do@@ -798,7 +832,7 @@ evalSrcLockProps _ Nothing = return [] evalSrcLockProps i (Just (LockProperties _ lcs)) = do cs <- mapM (evalLClause i) lcs- debugPrint $ "Properties: " ++ show cs+-- debugPrint $ "Properties: " ++ show cs return cs evalLClause :: Ident () -> LClause () -> TcDeclM (TcClause TcAtom)@@ -820,12 +854,14 @@ Nothing -> fail $ "getActor: No such actor: " ++ prettyPrint n getActor (ActorTypeVar _ i) = return $ ActorTPVar i -freshActorId :: String -> TcDeclM ActorId+freshActorId :: MonadBase m => String -> m ActorId freshActorId str = (liftIO . flip newFresh str) =<< getUniqRef -aliasActorId :: TcDeclM ActorId-aliasActorId = (liftIO . newAlias) =<< getUniqRef+unknownActorId :: MonadBase m => m ActorId+unknownActorId = (liftIO . newUnknown) =<< getUniqRef +instanceActorId :: MonadBase m => Name () -> m ActorId+instanceActorId n = (liftIO . flip newInstance n) =<< getUniqRef {----------------------------------------------------- -- The continuation monad@@ -957,10 +993,17 @@ getThisType :: MonadTcDeclM m => m TcClassType getThisType = liftTcDeclM getThisTypeTB +getThisStateType :: MonadTcDeclM m => m TcStateType+getThisStateType = do+ ct <- getThisType+ (is, tsig) <- lookupTypeOfType $ clsTypeToType ct+ let aids = catMaybes $ map (\i -> Map.lookup i $ actors $ tMembers tsig) is+ return $ instanceT ct aids+ getSuperType :: MonadTcDeclM m => m TcClassType getSuperType = do thisTy <- getThisType- thisSig <- lookupTypeOfType (clsTypeToType thisTy)+ (_, thisSig) <- lookupTypeOfType (clsTypeToType thisTy) case tSupers thisSig of [] -> return objectT [s] -> return s
src/Language/Java/Paragon/TypeCheck/Policy.hs view
@@ -1,14 +1,16 @@ {-# LANGUAGE CPP, DeriveDataTypeable, PatternGuards #-} module Language.Java.Paragon.TypeCheck.Policy ( - bottom, top, thisP, join, joinWThis, meet, {-recmeet,-} isTop, isBottom, includesThis, - TcPolicy(..), PrgPolicy(..),{-TcPolicyRec(..),-} TcClause(..), TcAtom(..), TcActor(..), TcMetaVar(..), + IsPolicy(..), + bottom, top, thisP, joinWThis, isTop, isBottom, + TcPolicy(..), PrgPolicy(..), PolicyBounds(..), + TcClause(..), TcAtom(..), TcActor(..), TcMetaVar(..), {- toPolicyLit, -} {-toRecPolicy,-} lockToAtom, {-zonkPolicy,-} substPolicy, firstRigid, substThis, flowAtomString, - ActorPolicy, AtomPolicy + ActorPolicy, AtomPolicy, ActorPolicyBounds ) where import Language.Java.Paragon.Syntax @@ -39,6 +41,7 @@ data TcPolicy a = RealPolicy (PrgPolicy a) | Join (TcPolicy a) (TcPolicy a) + | Meet (TcPolicy a) (TcPolicy a) | VarPolicy (TcMetaVar a) deriving (Eq, Ord, Show, Data, Typeable) @@ -50,17 +53,15 @@ deriving (Eq,Ord,Show,Data,Typeable) -{- -data VarPolicy a = VPolicy [TcClause a] - | VRigidVar (Ident ()) - | VThis - | VJoin (VarPolicy a) (VarPolicy a) - | VMeet (VarPolicy a) (VarPolicy a) - | VMetaVar a - deriving (Eq,Ord,Show,Data,Typeable) --} +data PolicyBounds a + = KnownPolicy (TcPolicy a) + -- | Invariant: For 'PolicyBounds p q', p <= q + | PolicyBounds (TcPolicy a) (TcPolicy a) + deriving (Eq, Ord, Show, Data, Typeable) + type ActorPolicy = TcPolicy TcActor +type ActorPolicyBounds = PolicyBounds TcActor type AtomPolicy = TcPolicy TcAtom @@ -113,6 +114,7 @@ instance Pretty a => Pretty (TcPolicy a) where pretty (RealPolicy p) = pretty p pretty (Join p1 p2) = pretty p1 <+> char '*' <+> pretty p2 + pretty (Meet p1 p2) = pretty p1 <+> char '+' <+> pretty p2 pretty (VarPolicy mv) = pretty mv instance Pretty (TcMetaVar a) where @@ -128,6 +130,10 @@ pretty (TcActor aid) = pretty aid pretty (TcVar i) = char '\'' <> pretty i +instance Pretty a => Pretty (PolicyBounds a) where + pretty (KnownPolicy p) = pretty p + pretty (PolicyBounds p q) = pretty p <> char '/' <> pretty q + mkSimpleLName :: Ident () -> Name () mkSimpleLName i = Name () LName Nothing i @@ -178,6 +184,8 @@ toPolicy :: PrgPolicy a -> p a fromPolicy :: p a -> Maybe (PrgPolicy a) includesThis :: p a -> Bool + join :: p TcActor -> p TcActor -> p TcActor + meet :: p TcActor -> p TcActor -> p TcActor instance IsPolicy PrgPolicy where toPolicy = id @@ -188,6 +196,9 @@ includesThis (TcMeet p q) = any includesThis [p,q] includesThis _ = False + join = lub + meet = glb + instance IsPolicy TcPolicy where toPolicy = RealPolicy fromPolicy (RealPolicy p) = Just p @@ -197,6 +208,34 @@ includesThis (RealPolicy p) = includesThis p includesThis _ = False + join (RealPolicy p) (RealPolicy q) = RealPolicy $ p `lub` q + join p q = Join p q + + meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q + meet p q = Meet p q + +instance IsPolicy PolicyBounds where + toPolicy = KnownPolicy . toPolicy + fromPolicy (KnownPolicy p) = fromPolicy p + fromPolicy _ = Nothing + + includesThis (KnownPolicy p) = includesThis p + includesThis (PolicyBounds pb pt) = any includesThis [pb,pt] + + join pb qb = case (pb,qb) of + (KnownPolicy p, KnownPolicy q) -> KnownPolicy $ p `join` q + (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2 + (KnownPolicy p, PolicyBounds q1 q2) -> mkBounds p q1 p q2 + (PolicyBounds p1 p2, KnownPolicy q ) -> mkBounds p1 q p2 q + where mkBounds a b c d = PolicyBounds (a `join` b) (c `join` d) + meet pb qb = case (pb,qb) of + (KnownPolicy p, KnownPolicy q) -> KnownPolicy $ p `meet` q + (PolicyBounds p1 p2, PolicyBounds q1 q2) -> mkBounds p1 q1 p2 q2 + (KnownPolicy p, PolicyBounds q1 q2) -> mkBounds p q1 p q2 + (PolicyBounds p1 p2, KnownPolicy q ) -> mkBounds p1 q p2 q + where mkBounds a b c d = PolicyBounds (a `meet` b) (c `meet` d) + + bottom, top, thisP :: IsPolicy pol => pol TcActor bottom = toPolicy $ TcPolicy [TcClause (TcVar $ Ident () "x") []] top = toPolicy $ TcPolicy [] @@ -224,6 +263,7 @@ lubWThis p q = lub p q lub :: (PrgPolicy TcActor) -> (PrgPolicy TcActor) -> (PrgPolicy TcActor) +lub p1 p2 | p1 == p2 = p1 -- fake shortcut, we can do better! lub (TcPolicy cs1) (TcPolicy cs2) = let sameFixedCs = [ TcClause (TcActor aid) (as ++ substAll senv bs) | TcClause (TcActor aid) as <- cs1, @@ -246,10 +286,6 @@ lub p1 p2 = TcJoin p1 p2 -join :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor) -join (RealPolicy p) (RealPolicy q) = RealPolicy $ p `lub` q -join p q = Join p q - type Subst = [(Ident (), TcActor)] @@ -284,18 +320,13 @@ -- This one could be smartified glb (TcPolicy as) (TcPolicy bs) = TcPolicy $ as ++ bs glb p1 p2 = TcMeet p1 p2 - -meet :: (TcPolicy TcActor) -> (TcPolicy TcActor) -> (TcPolicy TcActor) -meet (RealPolicy p) (RealPolicy q) = RealPolicy $ glb p q -meet _ _ = panic (policyModule ++ ".meet") - "meet used on non-programmable policies" - -{-TO FIX -recmeet :: TcPolicyRec -> TcPolicyRec -> TcPolicyRec -recmeet (TcPolicyRec cs1) (TcPolicyRec cs2) = TcPolicyRec $ cs1 ++ cs2 -recmeet p1 p2 = TcMeetRec p1 p2 +{- +includesVar :: ActorPolicy -> Bool +includesVar (VarPolicy _) = True +includesVar (Join p q) = includesVar p || includesVar q +includesVar (Meet p q) = includesVar p || includesVar q +includesVar _ = False -} - ---------------------------------------------- {-- Specialisation
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE PatternGuards #-} module Language.Java.Paragon.TypeCheck.TcExp where import Language.Java.Paragon.Syntax@@ -16,7 +17,7 @@ import Data.Maybe (fromJust) import qualified Data.Map as Map import Control.Applicative ( (<$>) )-import Control.Arrow ( first )+import Control.Arrow ( first, second ) import Control.Monad ( when ) tcExpModule :: String@@ -45,47 +46,43 @@ --debugTc str = liftIO $ putStrLn $ "DEBUG: Tc: " ++ str --debugTc _ = return () -tcExp :: Exp () -> TcCodeM (TcType, ActorPolicy, Exp T)+tcExp :: Exp () -> TcCodeM (TcStateType, ActorPolicy, Exp T) -- Rule PAREN tcExp (Paren _ e) = do (ty, p, e') <- tcExp e- return (ty, p, Paren (Just ty) e')+ return (ty, p, Paren (toT ty) e') -- Rule LIT-tcExp (Lit _ l) = let ty = litType l in return (ty, bottom, Lit (Just ty) (notAppl l))+tcExp (Lit _ l) = let ty = stateType $ litType l in return (ty, bottom, Lit (toT ty) (notAppl l)) -- Rule THIS tcExp (This _) = do- ty <- getThisType+ tTy <- getThisStateType --debugPrint $ "getThisType: " ++ show ty- let tTy = clsTypeToType ty- return (tTy, bottom, This $ Just tTy)+-- let tTy = stateType $ clsTypeToType ty+ return (tTy, bottom, This $ toT tTy) -- Rule BINOP tcExp (BinOp _ e1 op e2) = do (ty1, p1, e1') <- tcExp e1 (ty2, p2, e2') <- tcExp e2 tyRes <- opType op ty1 ty2- return (tyRes, p1 `join` p2, BinOp (Just tyRes) e1' (notAppl op) e2')+ return (tyRes, p1 `join` p2, BinOp (toT tyRes) e1' (notAppl op) e2') -- Rule VAR/FIELD tcExp (ExpName _ n) = case n of Name _ EName mPre i -> do- (ty1, pol, _) <- lookupVar mPre i- ty <- case ty1 of- TcPrimT (PolicyT _) -> policyPolT <$> getPolicy n- TcPrimT (ActorT _) -> actorIdT <$> getActorId n- _ -> return ty1- return (ty, pol, ExpName (Just ty) (notAppl n))+ (ty, pol, _) <- lookupVar mPre i+ return (ty, pol, ExpName (toT ty) (notAppl n)) Name _ LName mPre i -> do LSig pL arL _ <- lookupLock mPre i check (arL == 0) $ "Lock " ++ prettyPrint n ++ " expects " ++ show arL ++ " arguments but has been given none." let ty = lockT [TcLock n []]- return $ (ty, pL, ExpName (Just ty) (notAppl n))+ return $ (ty, pL, ExpName (toT ty) (notAppl n)) Name _ EOrLName mPre i -> do tryCatch (tcExp $ ExpName () $ Name () EName mPre i) (\_ -> tcExp $ ExpName () $ Name () LName mPre i)@@ -95,14 +92,15 @@ -- Rule VARASS/FIELDASS tcExp ex@(Assign _ lhs _op rhs) = do- debugPrint $ prettyPrint ex+ debugPrint $ "\n## " ++ prettyPrint ex ++ " ##\n" (tyV, pV, mtyO, mEnt, mN, lhs') <- case lhs of NameLhs _ n@(Name _ EName mPre iF) -> do case mPre of Nothing -> do -- VARASS (tyV, pV, _) <- lookupVar Nothing iF- return (tyV, pV, Nothing, Just (varE n), Just n, NameLhs (Just tyV) (notAppl n))+ return (unStateType tyV, pV, Nothing, Just (varE n), Just n, + NameLhs (toT tyV) (notAppl n)) Just pre -> do -- FIELDASS (Just tyO, tmO, pO) <- lookupPrefixName pre case Map.lookup iF $ fields tmO of@@ -114,7 +112,8 @@ "object when updating\n" ++ "Object policy: " ++ prettyPrint pO ++ "\n" ++ "Field policy: " ++ prettyPrint pF- return (tyF, pF, Just tyO, Just (varE n), Just n, NameLhs (Just tyF) (notAppl n))+ return (tyF, pF, Just $ unStateType tyO, Just (varE n), Just n, + NameLhs (Just tyF) (notAppl n)) Nothing -> fail $ "Object " ++ prettyPrint pre ++ " of type " ++ prettyPrint tyO ++ " does not have a field named " ++ prettyPrint iF@@ -134,11 +133,11 @@ "object when updating\n" ++ "Object policy: " ++ prettyPrint pE ++ "\n" ++ "Field policy: " ++ prettyPrint pF- return (tyF, pF, Just tyE, eEnt, Nothing, + return (tyF, pF, Just $ unStateType tyE, eEnt, Nothing, FieldLhs (Just tyF) (PrimaryFieldAccess (Just tyF) e' (notAppl fi))) ArrayLhs _ (ArrayIndex _ arrE iE) -> do (tyA, pA, arrE') <- tcExp arrE- case tyA of+ case unStateType tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI, iE') <- tcExp iE check (isIntConvertible tyI) $@@ -159,7 +158,7 @@ "array itself when updating\n" ++ "Array policy: " ++ prettyPrint pA ++ "\n" ++ "Element policy: " ++ prettyPrint pElem- return (tyElem, pElem, Just tyA, Nothing, Nothing, + return (tyElem, pElem, Just $ unStateType tyA, Nothing, Nothing, ArrayLhs (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE@@ -198,24 +197,26 @@ -- "be less restrictive than the policy of the object\n" ++ -- " + styV <- updateStateType mN mtyO tyV (Just tyRhs) -- Update actor tracker if applicable+{- -- TODO: This should go into updateStateType maybeM (mActorId tyRhs) $ \aid -> do- maybeM mtyO $ \tyO -> scrambleActors (Just tyO)+ maybeM mtyO $ \tyO -> scrambleActors (Just $ unStateType tyO) maybeM mN $ \n -> setActorId n aid- - return (tyV, pV, Assign (Just tyV) lhs' (notAppl _op) rhs')+-} + return (styV, pV, Assign (Just tyV) lhs' (notAppl _op) rhs') -- Rule CALL tcExp (MethodInv _ mi) = do (ty, p, mi') <- tcMethodOrLockInv mi- return (ty, p, MethodInv (Just ty) mi')+ return (ty, p, MethodInv (toT ty) mi') -- Rule NEW tcExp (InstanceCreation _ tas ct args Nothing) = do -- debugPrint $ "tcExp: " ++ show e tyT <- liftTcDeclM $ evalSrcClsType ct- (ty, p, args') <- tcCreate tyT tas args- return (ty, p, InstanceCreation (Just ty) (map notAppl tas) (notAppl ct) + (sty, p, args') <- tcCreate tyT tas args+ return (sty, p, InstanceCreation (toT sty) (map notAppl tas) (notAppl ct) args' Nothing) -- Rule COND@@ -230,33 +231,33 @@ (maybeM (mLocks tyC) (\ls -> applyLockMods ([], ls)) >> tcExp e1) ||| tcExp e2 check (ty1 == ty2) $ "Types of branches don't match" - return (ty1, pC `join` p1 `join` p2, Cond (Just ty1) c' e1' e2')+ return (ty1, pC `join` p1 `join` p2, Cond (toT ty1) c' e1' e2') tcExp (PolicyExp _ pl) = do pRep <- tcPolicyExp pl- let ty = policyPolT $ RealPolicy pRep- return (ty, bottom, PolicyExp (Just ty) (notAppl pl))+ let ty = policyPolT $ KnownPolicy $ RealPolicy pRep+ return (ty, bottom, PolicyExp (toT ty) (notAppl pl)) tcExp (PostIncrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Post-increment operator used at non-numeric type " ++ prettyPrint tyE- return (tyE, pE, PostIncrement (Just tyE) e')+ return (tyE, pE, PostIncrement (toT tyE) e') tcExp (PostDecrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE- return (tyE, pE, PostDecrement (Just tyE) e')+ return (tyE, pE, PostDecrement (toT tyE) e') tcExp (PreIncrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE- return (tyE, pE, PreIncrement (Just tyE) e')+ return (tyE, pE, PreIncrement (toT tyE) e') tcExp (PreDecrement _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE- return (tyE, pE, PreDecrement (Just tyE) e')+ return (tyE, pE, PreDecrement (toT tyE) e') -- Unary promotion prefix operator @@ -266,27 +267,27 @@ check (isNumConvertible tyE) $ "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE- return (ty, pE, PrePlus (Just ty) e')+ return (ty, pE, PrePlus (toT ty) e') tcExp (PreMinus _ e) = do (tyE, pE, e') <- tcExp e check (isNumConvertible tyE) $ "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE- return (ty, pE, PreMinus (Just ty) e')+ return (ty, pE, PreMinus (toT ty) e') tcExp (PreBitCompl _ e) = do (tyE, pE, e') <- tcExp e check (isIntConvertible tyE) $ "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE let ty = unaryNumPromote_ tyE- return (ty, pE, PreBitCompl (Just ty) e')+ return (ty, pE, PreBitCompl (toT ty) e') tcExp (PreNot _ e) = do (tyE, pE, e') <- tcExp e check (isBoolConvertible tyE) $ "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE- return (booleanT, pE, PreNot (Just booleanT) e')+ return (stateType booleanT, pE, PreNot (Just booleanT) e') tcExp (Cast _ t e) = do@@ -296,11 +297,12 @@ check canCast $ "Wrong type at cast" when (canExn) $ -- TODO: could throw ClassCastException return ()- return (tyC, pE, Cast (Just tyC) (notAppl t) e')+ styC <- updateStateType Nothing Nothing tyC (Just tyE)+ return (styC, pE, Cast (Just tyC) (notAppl t) e') tcExp (FieldAccess _ fa) = do (ty, p, fa') <- tcFieldAccess fa- return (ty, p, FieldAccess (Just ty) fa')+ return (ty, p, FieldAccess (toT ty) fa') -- Arrays @@ -330,7 +332,7 @@ dimPs' = map (fmap notAppl) $ snd $ unzip dimEsPs dimEsPs' = zip (dimE1':dimEsRest) dimPs' dimImplPs' = map (fmap notAppl) dimImplPs- return (ty, pol1, + return (stateType ty, pol1, ArrayCreate (Just ty) (notAppl bt) dimEsPs' dimImplPs') where checkDimExprs :: [ActorPolicy] -- Accumulated policies of earlier dimensions@@ -351,7 +353,7 @@ pNext <- evalMaybePol mp checkDimExprs (pPrev:accP) (e':accE) emps pNext - nonIntErr :: TcType -> String+ nonIntErr :: TcStateType -> String nonIntErr ty = "Non-integral expression of type " ++ prettyPrint ty ++ " used as dimension expression in array creation"@@ -368,19 +370,19 @@ -- Literal array initializers have known length, -- so their apparent policy is bottom let ty = mkArrayType baseTy dimPols- return (ty, bottom, + return (stateType ty, bottom, ArrayCreateInit (Just ty) (notAppl bt) (map (fmap notAppl) dimImplPs) arrInit') tcExp (ArrayAccess _ (ArrayIndex _ arrE iE)) = do (tyA, pA, arrE') <- tcExp arrE- case tyA of+ case unStateType tyA of TcRefT (TcArrayT tyElem pElem) -> do (tyI, pI, iE') <- tcExp iE check (isIntConvertible tyI) $ "Non-integral expression of type " ++ prettyPrint tyI ++ " used as array index expression"--- constraintLS pI pA $ " " -- Not true: pI just adds to the outgoing level- return (tyElem, pElem `join` pA `join` pI, + styElem <- getStateType Nothing Nothing tyElem+ return (styElem, pElem `join` pA `join` pI, ArrayAccess (Just tyElem) (ArrayIndex (Just tyElem) arrE' iE')) _ -> fail $ "Cannot index non-array expression " ++ prettyPrint arrE@@ -409,7 +411,7 @@ -- debugPrint $ "Pols: " ++ show pols -- debugPrint $ "Exp: " ++ show e (tyE,pE,e') <- tcExp e- let elemType = mkArrayType baseType pols+ let elemType = stateType $ mkArrayType baseType pols check (tyE == elemType) $ "Expression " ++ prettyPrint e ++ " in array initializer has type " ++ prettyPrint tyE@@ -425,19 +427,12 @@ -------------------------- -- Field Access -tcFieldAccess :: FieldAccess () -> TcCodeM (TcType, ActorPolicy, FieldAccess T)+tcFieldAccess :: FieldAccess () -> TcCodeM (TcStateType, ActorPolicy, FieldAccess T) tcFieldAccess (PrimaryFieldAccess _ e fi) = do (tyE,pE,e') <- tcExp e- case tyE of- -- Ugly hack to get the oft-used "length" function working-{- TcRefT (TcArrayT tyElem pElem) ->- if fi == Ident () "length" - then return (intT, pE)- else fail $ "Unsupported array field: " ++ prettyPrint fi--} - _ -> do- VSig tyF pFi _ _ _ <- lookupFieldT tyE fi- return (tyF, pE `join` pFi, PrimaryFieldAccess (Just tyF) e' (notAppl fi))+ VSig tyF pFi _ _ _ <- lookupFieldT tyE fi+ styF <- getStateType Nothing Nothing tyF+ return (styF, pE `join` pFi, PrimaryFieldAccess (toT styF) e' (notAppl fi)) tcFieldAccess fa = error $ "Unsupported field access: " ++ prettyPrint fa @@ -445,10 +440,10 @@ -- Instance creation tcCreate :: TcClassType -> [TypeArgument ()] -> [Argument ()] - -> TcCodeM (TcType, ActorPolicy, [Argument T])-tcCreate ctyT tas args = do+ -> TcCodeM (TcStateType, ActorPolicy, [Argument T])+tcCreate ctyT@(TcClassT tyN _) tas args = do (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args- (tps,genCti) <- lookupConstr ctyT tas tysArgs+ (tps,iaps,genCti) <- lookupConstr ctyT tas (map unStateType tysArgs) -- TODO: Check that the arguments in tyT -- match those expected by the type -- TODO: Type argument inference@@ -457,9 +452,13 @@ "Constructor expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas) tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) (zip tps tas)+ iaas <- mapM (instanceActorId . Name () EName (Just tyN)) iaps+ let itps = map (ActorParam ()) iaps+ itas = map TcActualActor iaas+ -- tm <- getTypeMap- let cti = instantiate (zip tps tArgs) genCti- let (CSig psPars pW lExp lMods exns) = cti+ let cti = instantiate (zip (tps++itps) (tArgs++itas)) genCti+ (CSig _psIs psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState@@ -500,14 +499,16 @@ applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] - return (clsTypeToType ctyT, bottom, args')+ styT <- getStateType Nothing Nothing $ clsTypeToType ctyT + return (styT, bottom, args')+ -------------------------- -- Method invocations -- | Check a method invocation, which could possibly represent -- a lock query expression.-tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)+tcMethodOrLockInv :: MethodInvocation () -> TcCodeM (TcStateType, ActorPolicy, MethodInvocation T) tcMethodOrLockInv (MethodCallOrLockQuery _ (Name _ MOrLName mPre i) args) = do -- We couldn't resolve without type information whether -- this truly is a method or a lock.@@ -530,20 +531,20 @@ ++ " arguments but has been given " ++ show (length args) (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args- debugPrint $ "args': " ++ show args'+ -- debugPrint $ "args': " ++ show args' mapM_ (\ty -> check (isActorType ty) $ "Trying to query lock with argument of type " ++ prettyPrint ty ++ "\n" ++ "All arguments to lock query must be of type actor") tysArgs let tyR = lockT [TcLock nam $ map (fromJust . mActorId) tysArgs]- debugPrint $ "tyR: " ++ show tyR+ -- debugPrint $ "tyR: " ++ show tyR return (tyR, foldl1 join (pL:psArgs),- MethodCallOrLockQuery (Just tyR) (notAppl nam) args')+ MethodCallOrLockQuery (toT tyR) (notAppl nam) args') tcMethodOrLockInv mi = tcMethodInv mi -- | Check a true method invocation-tcMethodInv :: MethodInvocation () -> TcCodeM (TcType, ActorPolicy, MethodInvocation T)+tcMethodInv :: MethodInvocation () -> TcCodeM (TcStateType, ActorPolicy, MethodInvocation T) tcMethodInv mi = do debugPrint $ "tcMethodInv: " ++ prettyPrint mi (n, msig, args, psArgs, pE, ef) <-@@ -551,35 +552,45 @@ MethodCallOrLockQuery _ n@(Name _ MName mPre i) args -> do -- This is a true method call (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args- (pPath, tps, msig) <- lookupMethod mPre i [] tysArgs+ (pPath, tps, msig) <- lookupMethod mPre i [] (map unStateType tysArgs)+ debugPrint $ "msig: " ++ show msig check (null tps) $ "Method " ++ prettyPrint i ++ " expects " ++ show (length tps) ++ " type arguments but has been\ \ given 0" return $ (n, msig, args, psArgs, pPath, - \ty -> MethodCallOrLockQuery (Just ty) (notAppl n) args')+ \ty -> MethodCallOrLockQuery (toT ty) (notAppl n) args') MethodCallOrLockQuery _ n _ -> panic (tcExpModule ++ ".tcMethodInv") $ "Unexpected name: " ++ show n PrimaryMethodCall _ e tas i args -> do (tyE, pE, e') <- tcExp e (tysArgs, psArgs, args') <- unzip3 <$> mapM tcExp args let tas' = map (ActualArg ()) tas- (tps, genMSig) <- lookupMethodT tyE i tas' tysArgs+ (tps, genMSig) <- lookupMethodT tyE i tas' (map unStateType tysArgs) tArgs <- liftTcDeclM $ mapM (uncurry evalSrcTypeArg) $ zip tps tas' let msig = instantiate (zip tps tArgs) genMSig return $ (mkSimpleName MName i, msig, args, psArgs, pE,- \ty -> PrimaryMethodCall (Just ty) e' (map notAppl tas) (notAppl i) args')+ \ty -> PrimaryMethodCall (toT ty) e' (map notAppl tas) (notAppl i) args') _ -> fail $ "tcMethodInv: Unsupported method call" - let (MSig tyR pR psPars pW lExp lMods exns) = msig+ let (MSig tyR pR psIs psPars pW lExp lMods exns) = msig -- Check lockstates l <- getCurrentLockState check (null (lExp \\ l)) $ "Lockstate too weak when calling method " ++ prettyPrint n ++ ":\n" ++ "Required lock state: " ++ prettyPrint lExp ++ "\n" ++ "Current lock state: " ++ prettyPrint l- -- Check argument constraints+ -- 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' mapM_ (\(arg,argP,parP) -> constraintLS argP parP $ "Method applied to argument with too restrictive policy:\n" ++ @@ -587,31 +598,55 @@ "Argument: " ++ prettyPrint arg ++ "\n" ++ " with policy: " ++ prettyPrint argP ++ "\n" ++ "Declared policy bound: " ++ prettyPrint parP- ) (zip3 args psArgs psPars)+ ) (zip3 args psArgs psPars') -- Check E[branchPC](*) <= pW bpcs <- getBranchPC_- constraintPC bpcs pW $ \p src ->- "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW +++ constraintPC bpcs pW' $ \p src ->+ "Method " ++ prettyPrint n ++ " 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 -> - "Method " ++ prettyPrint n ++ " with declared write effect " ++ prettyPrint pW +++ constraintPC epc pW' $ \p src -> + "Method " ++ prettyPrint n ++ " 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 (Left n)) exns+ mapM_ (uncurry $ exnConsistent (Left n)) exns' -- Fix outgoing state- let exns' = map (first ExnType) exns- activateExns exns' -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}]+ let exnsT = map (first ExnType) exns'+ activateExns exnsT -- ==> S' = Sn[exns{X +-> (Sx, exns(X)[write])}] applyLockMods lMods -- ==> S'' = S'[lockMods ||>>= lMods, scrambleActors Nothing -- ==> actors scrambled] - return (tyR, pE `join` pR, ef tyR)+ styR <- getStateType Nothing Nothing tyR+ 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++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 (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++ ----------------------------------- -- Policy expressions -- Treat them as pure compile-time for now@@ -621,12 +656,12 @@ tcCs <- mapM tcClause cs return (TcPolicy tcCs) tcPolicyExp pe@(PolicyOf _ i) = do- vi@(_, _, param) <- lookupVar Nothing i- debugPrint $ "tcPolicyExp: vi: " ++ show vi- tm <- getTypeMap- debugPrint $ "tcPolicyExp: TypeMap: " ++ show tm- vm <- vars <$> getEnv- debugPrint $ "tcPolicyExp: VarMap: " ++ show vm+ (_, _, param) <- lookupVar Nothing i+ -- debugPrint $ "tcPolicyExp: vi: " ++ show vi+ --tm <- getTypeMap+ -- debugPrint $ "tcPolicyExp: TypeMap: " ++ show tm+ --vm <- vars <$> getEnv+ -- debugPrint $ "tcPolicyExp: VarMap: " ++ show vm check param $ "policyof may only be used on parameters: " ++ prettyPrint pe return $ TcRigidVar i@@ -655,19 +690,25 @@ tcActor (Actor _ n) = TcActor <$> tcActorName n tcActorName :: ActorName () -> TcCodeM ActorId-tcActorName (ActorName _ n) = getActorId n+tcActorName (ActorName _ n) = do+ (sty,_,_) <- tcExp $ ExpName () n --getActorId (Just n) Nothing -- TODO: Look up preTy?+ case mActorId sty of+ Just aid -> return aid+ Nothing -> panic (tcExpModule ++ ".tcActorName")+ $ "Non-actor type for actor name: " ++ show (n, sty)+ tcActorName (ActorTypeVar _ i) = return $ ActorTPVar i ----------------------------------- -- Types of operators -- ----------------------------------- -opType :: Op () -> TcType -> TcType -> TcCodeM TcType+opType :: Op () -> TcStateType -> TcStateType -> TcCodeM TcStateType -- First the special cases: policy operators, and String conversion opType (Mult _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `join` p2)) opType (Add _) (TcPolicyPolT p1) (TcPolicyPolT p2) = return (TcPolicyPolT (p1 `meet` p2))-opType (Add _) t1 t2 | t1 == clsTypeToType stringT || t2 == clsTypeToType stringT - = return $ clsTypeToType stringT+opType (Add _) t1 t2 | let sT = stateType (clsTypeToType stringT),+ t1 == sT || t2 == sT = return sT opType op t1 t2 -- Numeric operators@@ -698,7 +739,7 @@ check (isNumConvertible t2) $ "Numerical comparison operator " ++ prettyPrint op ++ " used with non-numeric operand of type " ++ prettyPrint t2- return booleanT+ return $ stateType booleanT | op `elem` [Equal (), NotEq ()] = do case binaryNumPromote t1 t2 of@@ -708,7 +749,7 @@ _ -> fail $ "Equality operator " ++ prettyPrint op ++ " used with incomparable operands of types " ++ prettyPrint t1 ++ " and " ++ prettyPrint t2- return booleanT+ return $ stateType booleanT | op `elem` [And (), Or (), Xor ()] = if isBoolConvertible t1 @@ -716,7 +757,7 @@ check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2- return booleanT+ return $ stateType booleanT else if isIntConvertible t1 then do check (isIntConvertible t2) $@@ -733,7 +774,7 @@ check (isBoolConvertible t2) $ "Logical operator " ++ prettyPrint op ++ " used with non-boolean operand of type " ++ prettyPrint t2- return booleanT+ return $ stateType booleanT opType op _ _ = panic (tcExpModule ++ ".opType") $ show op {-
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -92,7 +92,7 @@ (mForInit', forf) <- withInits mForInit $ do s <- getState (tyC, pC, mTest') <- case mTest of- Nothing -> return (booleanT, bottom, Nothing)+ Nothing -> return (stateType booleanT, bottom, Nothing) Just test -> do (ty, p, test') <- tcExp test return (ty, p, Just test')@@ -147,11 +147,11 @@ -- Rule RETURNVOID tcStmt (Return _ Nothing) = do- (tyR, pR) <- getReturn+ (tyR, _pR) <- getReturn check (tyR == voidT) $ "Encountered unexpected empty return statement"- check (pR == top) $ "Internal error: tcStmt: " - ++ "void return with non-top return policy should never happen"-+{- check (pR == top) $ "Internal error: tcStmt: " + ++ "void return with non-top return policy should never happen: " ++ show pR+-} pc <- getCurrentPC returnE throwExn ExnReturn pc return $ Return Nothing Nothing@@ -187,7 +187,8 @@ -- Rule THROW tcStmt (Throw _ eX) = do- (tyX, pX, eX') <- tcExp eX+ (styX, pX, eX') <- tcExp eX+ let tyX = unStateType styX -- TODO: check (tyX <: "Throwable") (rX, wX) <- lookupExn tyX -- Check E[branchPC](X) <= E[exns](X)[write]@@ -401,15 +402,18 @@ -- Rule LOCALVARDECL tcLocalVars pV tyV fin (vd@(VarDecl _ (VarId _ i) Nothing):vds) acc cont = do+ _styV <- registerStateType i tyV Nothing+{- -- TODO: Merge this into updateStateType tyV' <- if tyV == actorT then actorIdT <$> newActorId i- else return tyV- extendVarEnv i (VSig tyV' pV False False fin) $ do+ else return $ stateType tyV -}+ extendVarEnv i (VSig tyV pV False False fin) $ do addBranchPC (varE (mkSimpleName EName i)) $ do tcLocalVars pV tyV fin vds (notAppl vd : acc) cont -- Rule LOCALVARINIT (Exp)-tcLocalVars pV tyV fin (VarDecl _ (VarId _ i) (Just (InitExp _ e)):vds) acc cont = do+tcLocalVars pV tyV fin (vd0@(VarDecl _ (VarId _ i) (Just (InitExp _ e))):vds) acc cont = do+ debugPrint $ "\n## " ++ prettyPrint vd0 ++ " ##\n" (tyE, pE, e') <- tcExp e checkM (tyV =<: tyE) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV@@ -417,12 +421,15 @@ "Cannot assign result of expression " ++ prettyPrint e ++ " with policy " ++ prettyPrint pE ++ " to variable " ++ prettyPrint i ++ " with policy " ++ prettyPrint pV ++ _styV <- registerStateType i tyV (Just tyE)+{- -- TODO: Merge this into updateStateType tyV' <- case mActorId tyE of- Nothing -> return tyV+ Nothing -> return $ stateType tyV Just aid -> do newActorIdWith i aid- return $ actorIdT aid- extendVarEnv i (VSig tyV' pV False False fin) $ do+ return $ actorIdT aid -}+ extendVarEnv i (VSig tyV pV False False fin) $ do addBranchPC (varE (mkSimpleName EName i)) $ do let vd = VarDecl Nothing (VarId Nothing $ notAppl i) (Just (InitExp Nothing e')) tcLocalVars pV tyV fin vds (vd:acc) cont
src/Language/Java/Paragon/TypeCheck/TypeMap.hs view
@@ -49,7 +49,8 @@ data MethodSig = MSig { mRetType :: TcType, mRetPol :: ActorPolicy,- mPars :: [ActorPolicy],+ mPars :: [Ident ()],+ mParPols :: [ActorPolicy], mWrites :: ActorPolicy, mExpects :: [TcLock], mLMods :: ([TcLock],[TcLock]),@@ -65,7 +66,8 @@ deriving (Show, Data, Typeable) data ConstrSig = CSig {- cPars :: [ActorPolicy],+ cPars :: [Ident ()],+ cParPols :: [ActorPolicy], cWrites :: ActorPolicy, cExpects :: [TcLock], cLMods :: ([TcLock],[TcLock]),@@ -108,7 +110,7 @@ -- typemethod eval info typemethods :: Map (Ident ()) ([Ident ()], Block ()), -- types and packages- types :: Map (Ident ()) ([TypeParam ()], TypeSig),+ types :: Map (Ident ()) ([TypeParam ()], [Ident ()], TypeSig), packages :: Map (Ident ()) TypeMap } deriving (Show, Data, Typeable)@@ -150,7 +152,7 @@ pkgsAndTypes :: TypeMap -> Map (Ident ()) TypeMap pkgsAndTypes tm = Map.union (packages tm) -- disregard type parameters- (Map.map (tMembers . snd) $ types tm)+ (Map.map (tMembers . (\(_,_,x) -> x)) $ types tm) merge :: TypeMap -> TypeMap -> TypeMap@@ -185,20 +187,20 @@ newTm = go is leafTm eTm in tm { packages = Map.insert i newTm mTm } -extendTypeMapT :: Name () -> [TypeParam ()] -> TypeSig -> TypeMap -> TypeMap+extendTypeMapT :: Name () -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap extendTypeMapT = go . flattenName where- go :: [Ident ()] -> [TypeParam ()] -> TypeSig -> TypeMap -> TypeMap- go [] _ _ _ = panic (typeMapModule ++ ".extendTypeMapT")- "Empty ident list"- go [i] tps tSig tm =- tm { types = Map.insert i (tps, tSig) (types tm) }- go (i:is) tps tSig tm =+ go :: [Ident ()] -> [TypeParam ()] -> [Ident ()] -> TypeSig -> TypeMap -> TypeMap+ go [] _ _ _ _ = panic (typeMapModule ++ ".extendTypeMapT")+ "Empty ident list"+ go [i] tps iaps tSig tm =+ tm { types = Map.insert i (tps,iaps,tSig) (types tm) }+ go (i:is) tps iaps tSig tm = let mTm = packages tm eTm = case Map.lookup i mTm of Just innerTm -> innerTm Nothing -> emptyTM- newTm = go is tps tSig eTm+ newTm = go is tps iaps tSig eTm in tm { packages = Map.insert i newTm mTm } extendTypeMapN :: Name () -> (TypeMap -> TypeMap) -> TypeMap -> TypeMap@@ -209,13 +211,13 @@ "Empty ident list" go [i] tmf tm = let mTm = types tm- (tps,tSig) = case Map.lookup i mTm of- Just tyInfo -> tyInfo- Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $- "Type not yet initialized: " ++ prettyPrint i+ (tps,iaps,tSig) = case Map.lookup i mTm of+ Just tyInfo -> tyInfo+ Nothing -> panic (typeMapModule ++ ".extendTypeMapN") $+ "Type not yet initialized: " ++ prettyPrint i tTm = tMembers tSig newSig = tSig { tMembers = tmf tTm }- in tm { types = Map.insert i (tps, newSig) mTm }+ in tm { types = Map.insert i (tps,iaps,newSig) mTm } go (i:is) tmf tm = let mTm = packages tm@@ -230,12 +232,13 @@ -- Working with the lookups -- -------------------------------------- +-- TODO: This is an anomaly!!! lookupNamed :: (TypeMap -> Map (Ident ()) a) -> Name () -> TypeMap -> Maybe a lookupNamed recf (Name _ _ Nothing i) tm = Map.lookup i (recf tm) lookupNamed recf nam@(Name _ _ (Just pre) i) tm = do newTm <- case nameType pre of TName -> do- (_tps, tsig) <- lookupNamed types pre tm+ (_tps, _iaps, tsig) <- lookupNamed types pre tm --if not (null tps) --then Nothing --else @@ -253,17 +256,49 @@ lookupNamed _ _ _ = panic (typeMapModule ++ ".lookupNamed") "AntiQName should not appear in AST being type-checked" ++lookupTypeOfStateT :: TcStateType -> TypeMap -> Either (Maybe String) TypeSig+lookupTypeOfStateT (TcInstance (TcClassT n tas) iaas) startTm = + case n of+ Name _ TName _ _ -> + let mSig = lookupNamed types n startTm+ in case mSig of+ Nothing -> Left Nothing+ Just (tps, iaps, tsig) + -- TODO: Type argument inference+ | length tps /= length tas -> Left $ Just $ + "Wrong number of type arguments in class type.\n" +++ "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) +++ " arguments but has been given " ++ show (length tas)+ | length iaps /= length iaas -> panic (typeMapModule ++ ".lookupTypeOfStateT")+ $ "Too few implicit arguments: " ++ show (iaps, iaas)+ | otherwise -> let itps = map (ActorParam ()) iaps+ itas = map TcActualActor iaas+ in Right $ instantiate (zip (tps++itps) (tas++itas)) tsig++ Name _ _ _ _ -> Left Nothing+ _ -> panic (typeMapModule ++ ".lookupTypeOfT") $ show n++lookupTypeOfStateT (TcType t) tm = + case lookupTypeOfT t tm of+ Right (is, tsig) | null is -> Right tsig+ | otherwise -> panic (typeMapModule ++ ".lookupTypeOfStateT")+ $ "Needs implicit actor arguments: " ++ show (t, is)+ Left err -> Left err+ +lookupTypeOfStateT _ _ = Left Nothing+ -- | lookupTypeOfT will, given a type T and a top-level type environment, -- return the type environment for T tagged with Right. -- Left denotes an error, which wraps: -- * If T is not a refType, return Nothing -- * If T is given the wrong number of type arguments, return Just errorMessage.-lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) TypeSig+lookupTypeOfT :: TcType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig) lookupTypeOfT (TcRefT refT) = lookupTypeOfRefT refT lookupTypeOfT _ = const $ Left Nothing -lookupTypeOfRefT :: TcRefType -> TypeMap -> Either (Maybe String) TypeSig-lookupTypeOfRefT (TcArrayT ty pol) _ = Right $ hardCodedArrayTM ty pol+lookupTypeOfRefT :: TcRefType -> TypeMap -> Either (Maybe String) ([Ident ()], TypeSig)+lookupTypeOfRefT (TcArrayT ty pol) _ = Right $ ([], hardCodedArrayTM ty pol) lookupTypeOfRefT (TcTypeVar _ ) _ = panic (typeMapModule ++ ".lookupTypeOfRefT") "TcTypeVar should have been instantiated" lookupTypeOfRefT TcNullT _ = Left $ Just $ "Cannot dereference null"@@ -273,15 +308,18 @@ let mSig = lookupNamed types n startTm in case mSig of Nothing -> Left Nothing- Just (tps, tsig) -> - if length tps == length tas- then Right $ instantiate (zip tps tas) tsig- else Left $ Just $ + Just (tps, iaps, tsig) + -- TODO: Type argument inference+ | length tps /= length tas -> Left $ Just $ "Wrong number of type arguments in class type.\n" ++ "Type " ++ prettyPrint n ++ " expects " ++ show (length tps) ++ " arguments but has been given " ++ show (length tas)+-- | not (null iaps) -> panic (typeMapModule ++ ".lookupTypeOfRefT")+-- $ "Too many implicit arguments: " ++ show iaps+ | otherwise -> Right $ (iaps, instantiate (zip tps tas) tsig)+ Name _ _ _ _ -> Left Nothing- _ -> panic (typeMapModule ++ ".lookupTypeOfT") $ show n+ _ -> panic (typeMapModule ++ ".lookupTypeOfRefT") $ show n -------------------------------------- -- Type argument instantiation --
src/Language/Java/Paragon/TypeCheck/Types.hs view
@@ -22,13 +22,24 @@ typesModule = typeCheckerBase ++ ".Types" type T = Maybe TcType -- Used for annotated AST+ notAppl :: Functor f => f a -> f T notAppl = fmap (const Nothing) +toT :: TcStateType -> T+toT = Just . unStateType +data TcStateType+ = TcInstance TcClassType [ActorId]+ | TcActorIdT ActorId+ | TcPolicyPolT ActorPolicyBounds+ | TcLockT [TcLock]+ | TcType TcType+ deriving (Eq, Ord, Show, Data, Typeable)+ data TcType- = TcPrimT (PrimType ()) | TcRefT TcRefType | TcVoidT- | TcActorIdT ActorId | TcPolicyPolT ActorPolicy | TcLockT [TcLock]+ = TcPrimT (PrimType ()) | TcRefT TcRefType | TcVoidT -- | TcLockRetT+-- | TcActorIdT ActorId | TcPolicyPolT ActorPolicy | TcLockT [TcLock] deriving (Eq, Ord, Show, Data, Typeable) data TcRefType@@ -39,7 +50,7 @@ deriving (Eq, Ord, Show, Data, Typeable) data TcClassType- = TcClassT (Name ()) [TcTypeArg] -- | TcNullT -- Ignore wildcards for now+ = TcClassT (Name ()) [TcTypeArg] -- [ActorId] -- Ignore wildcards for now deriving (Eq, Ord, Show, Data, Typeable) data TcTypeArg@@ -49,8 +60,6 @@ | TcActualLockState [TcLock] deriving (Eq, Ord, Show, Data, Typeable) --- type TcTypeArg = TcTypeArgRaw ActorId TcPolicy TcLock- ------------------------------------ -- Constructors @@ -67,19 +76,33 @@ actorT = TcPrimT (ActorT ()) policyT = TcPrimT (PolicyT ()) +stateType :: TcType -> TcStateType+stateType = TcType++unStateType :: TcStateType -> TcType+unStateType tcst = case tcst of+ TcInstance ct _ -> TcRefT $ TcClsRefT ct+ TcActorIdT _ -> actorT+ TcPolicyPolT _ -> policyT+ TcLockT _ -> booleanT+ TcType t -> t+ nullT, voidT :: TcType nullT = TcRefT TcNullT voidT = TcVoidT -actorIdT :: ActorId -> TcType+actorIdT :: ActorId -> TcStateType actorIdT = TcActorIdT -policyPolT :: ActorPolicy -> TcType+policyPolT :: ActorPolicyBounds -> TcStateType policyPolT = TcPolicyPolT -lockT :: [TcLock] -> TcType+lockT :: [TcLock] -> TcStateType lockT = TcLockT +instanceT :: TcClassType -> [ActorId] -> TcStateType+instanceT = TcInstance+ {- clsTypeWArg :: Name () -> [TcTypeArg] -> TcType clsTypeWArg n = TcClassT n@@ -132,11 +155,13 @@ -- Just n -> n -- Nothing -> error $ "typeName_: " ++ show typ -isClassType, isRefType, isNullType :: TcType -> Bool-isClassType (TcRefT (TcClsRefT (TcClassT _ _))) = True+isClassType, isRefType, isNullType :: TcStateType -> Bool+isClassType (TcType (TcRefT (TcClsRefT (TcClassT{})))) = True+isClassType (TcInstance{}) = True isClassType _ = False -isRefType (TcRefT _) = True+isRefType (TcType (TcRefT _)) = True+isRefType (TcInstance{}) = True isRefType _ = False mNameRefType :: TcRefType -> Maybe (Name ())@@ -144,28 +169,28 @@ if null as then Just (mkUniformName_ AmbName $ flattenName n) else Nothing mNameRefType _ = Nothing -isNullType (TcRefT TcNullT) = True+isNullType (TcType (TcRefT TcNullT)) = True isNullType _ = False -mActorId :: TcType -> Maybe ActorId+mActorId :: TcStateType -> Maybe ActorId mActorId (TcActorIdT aid) = Just aid mActorId _ = Nothing -mLocks :: TcType -> Maybe [TcLock]+mLocks :: TcStateType -> Maybe [TcLock] mLocks (TcLockT ls) = Just ls mLocks _ = Nothing -mPolicyPol :: TcType -> Maybe ActorPolicy+mPolicyPol :: TcStateType -> Maybe ActorPolicyBounds mPolicyPol (TcPolicyPolT p) = Just p mPolicyPol _ = Nothing -isLockType :: TcType -> Bool+isLockType :: TcStateType -> Bool isLockType = isJust . mLocks -isActorType :: TcType -> Bool+isActorType :: TcStateType -> Bool isActorType = isJust . mActorId -isPolicyType :: TcType -> Bool+isPolicyType :: TcStateType -> Bool isPolicyType = isJust . mPolicyPol mArrayType :: TcType -> Maybe (TcType, [ActorPolicy])@@ -175,6 +200,14 @@ Just (t, ps) -> (t, p:ps) mArrayType _ = Nothing +mClassType :: TcType -> Maybe TcClassType+mClassType (TcRefT (TcClsRefT (ct@TcClassT{}))) = Just ct+mClassType _ = Nothing++mInstanceType :: TcStateType -> Maybe (TcClassType, [ActorId])+mInstanceType (TcInstance ct aids) = Just (ct, aids)+mInstanceType _ = Nothing+ ------------------------------------------- -- Type operations @@ -204,48 +237,17 @@ box :: PrimType () -> Maybe (TcClassType)-box pt = case pt of- BooleanT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Boolean"])- []- ByteT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Byte"])- []- ShortT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Short"])- []- CharT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Character"])- []- IntT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Integer"])- []- LongT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Long"])- []- FloatT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Float"])- []- DoubleT () -> - Just $- TcClassT - (mkName_ TName PName $ map (Ident ()) ["java", "lang", "Double"])- []- _ -> Nothing+box pt = let mkClassType str = Just $ TcClassT (mkName_ TName PName $ map (Ident ()) ["java", "lang", str]) []+ in case pt of+ BooleanT () -> mkClassType "Boolean"+ ByteT () -> mkClassType "Byte"+ ShortT () -> mkClassType "Short"+ CharT () -> mkClassType "Character"+ IntT () -> mkClassType "Integer"+ LongT () -> mkClassType "Long"+ FloatT () -> mkClassType "Float"+ DoubleT () -> mkClassType "Double"+ _ -> Nothing unbox :: TcClassType -> Maybe (PrimType ()) unbox (TcClassT n _) =@@ -262,40 +264,39 @@ --unbox TcNullT = Nothing -unboxType :: TcType -> Maybe (PrimType ())-unboxType (TcRefT (TcClsRefT ct)) = unbox ct+unboxType :: TcStateType -> Maybe (PrimType ())+unboxType sty | TcRefT (TcClsRefT ct) <- unStateType sty = unbox ct unboxType _ = Nothing unIdent :: Ident a -> String unIdent (Ident _ x) = x-unIdent _ = panic (typesModule ++ ".unIdent")- "AntiQIdent should not appear in AST being typechecked"+unIdent (AntiQIdent _ str) = panic (typesModule ++ ".unIdent")+ $ "AntiQIdent should not appear in AST being typechecked: " ++ str -isNumConvertible :: TcType -> Bool-isNumConvertible ty = - ty `elem` [byteT, shortT, intT, longT, charT, floatT, doubleT] ||- case unboxType ty of+isNumConvertible :: TcStateType -> Bool+isNumConvertible sty = + unStateType sty `elem` [byteT, shortT, intT, longT, charT, floatT, doubleT] ||+ case unboxType sty of Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT]) -> True _ -> False -isIntConvertible :: TcType -> Bool-isIntConvertible ty =- ty `elem` [byteT, shortT, intT, longT, charT] ||- case unboxType ty of+isIntConvertible :: TcStateType -> Bool+isIntConvertible sty =+ unStateType sty `elem` [byteT, shortT, intT, longT, charT] ||+ case unboxType sty of Just t | t `elem` (map ($()) [ByteT, ShortT, IntT, LongT, CharT]) -> True _ -> False -isBoolConvertible :: TcType -> Bool-isBoolConvertible t = t == booleanT +isBoolConvertible :: TcStateType -> Bool+isBoolConvertible t = unStateType t == booleanT -- includes lock types || unboxType t == Just (BooleanT ())- || isLockType t -unaryNumPromote :: TcType -> Maybe (PrimType ())-unaryNumPromote ty- | TcPrimT pt <- ty = numPromote pt- | Just pt <- unboxType ty = numPromote pt+unaryNumPromote :: TcStateType -> Maybe (PrimType ())+unaryNumPromote sty+ | TcPrimT pt <- unStateType sty = numPromote pt+ | Just pt <- unboxType sty = numPromote pt | otherwise = Nothing where numPromote :: PrimType () -> Maybe (PrimType ())@@ -304,32 +305,39 @@ | pt `elem` map ($()) [ByteT, ShortT, IntT, CharT] = Just $ IntT () | otherwise = Nothing -unaryNumPromote_ :: TcType -> TcType-unaryNumPromote_ = TcPrimT . fromJust . unaryNumPromote+unaryNumPromote_ :: TcStateType -> TcStateType+unaryNumPromote_ = stateType . TcPrimT . fromJust . unaryNumPromote -binaryNumPromote :: TcType -> TcType -> Maybe (PrimType ())+binaryNumPromote :: TcStateType -> TcStateType -> Maybe (PrimType ()) binaryNumPromote t1 t2 = do pt1 <- unaryNumPromote t1 pt2 <- unaryNumPromote t2 return $ max pt1 pt2 -binaryNumPromote_ :: TcType -> TcType -> TcType-binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2+binaryNumPromote_ :: TcStateType -> TcStateType -> TcStateType+binaryNumPromote_ t1 t2 = stateType . TcPrimT . fromJust $ binaryNumPromote t1 t2 --------------------------------------------- -- Pretty printing +instance Pretty TcStateType where+ pretty tcst =+ case tcst of+ TcActorIdT aid -> text "actor[" <> pretty aid <> text "]"+ TcPolicyPolT p -> text "policy[" <> pretty p <> text "]"+ TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]"+ TcInstance ct aids -> pretty ct <> + (hsep $ char '[' : punctuate (char ',') (map pretty aids)) <> char ']'+ TcType ty -> pretty ty+ instance Pretty TcType where pretty tct = case tct of TcPrimT pt -> pretty pt TcRefT rt -> pretty rt TcVoidT -> text "void"- TcActorIdT aid -> text "actor[" <> pretty aid <> text "]"- TcPolicyPolT p -> text "policy[" <> pretty p <> text "]"- TcLockT ls -> (hsep $ text "lock[" : punctuate (text ",") (map pretty ls)) <> text "]" instance Pretty TcRefType where pretty tcrt =