paragon 0.1.3 → 0.1.4
raw patch · 11 files changed
+542/−354 lines, 11 files
Files
- paragon.cabal +5/−1
- src/Language/Java/Paragon/TypeCheck.hs +78/−78
- src/Language/Java/Paragon/TypeCheck/Constraints.hs +2/−2
- src/Language/Java/Paragon/TypeCheck/Evaluate.hs +6/−6
- src/Language/Java/Paragon/TypeCheck/Monad.hs +128/−132
- src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs +68/−0
- src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs +26/−25
- src/Language/Java/Paragon/TypeCheck/TcEnv.hs +9/−15
- src/Language/Java/Paragon/TypeCheck/TcExp.hs +136/−66
- src/Language/Java/Paragon/TypeCheck/TcStmt.hs +15/−15
- src/Language/Java/Paragon/TypeCheck/Types.hs +69/−14
paragon.cabal view
@@ -1,5 +1,5 @@ Name: paragon-Version: 0.1.3+Version: 0.1.4 License: BSD3 License-File: LICENSE Author: Niklas Broberg@@ -39,6 +39,7 @@ Language.Java.Paragon.TypeCheck.Locks, Language.Java.Paragon.TypeCheck.Monad, Language.Java.Paragon.TypeCheck.Monad.TcBase,+ Language.Java.Paragon.TypeCheck.Monad.TcCont, Language.Java.Paragon.TypeCheck.Monad.TcMonad, Language.Java.Paragon.TypeCheck.Policy, Language.Java.Paragon.TypeCheck.TcEnv,@@ -68,6 +69,9 @@ Language.Java.Paragon.TypeCheck.EvalEnv, Language.Java.Paragon.TypeCheck.Locks, Language.Java.Paragon.TypeCheck.Monad,+ Language.Java.Paragon.TypeCheck.Monad.TcBase,+ Language.Java.Paragon.TypeCheck.Monad.TcCont,+ Language.Java.Paragon.TypeCheck.Monad.TcMonad, Language.Java.Paragon.TypeCheck.Policy, Language.Java.Paragon.TypeCheck.TcEnv, Language.Java.Paragon.TypeCheck.TcExp,
src/Language/Java/Paragon/TypeCheck.hs view
@@ -36,7 +36,7 @@ typeCheck :: DirectoryPath -> CompilationUnit -> IO CompilationUnit typeCheck currentDir ast@(CompilationUnit pkg imps [td]) = do let (skoTd, skoTy) = skolemTypeDecl td- e <- runTcBase skoTy $ do+ e <- runTcCont skoTy $ do withEnvFromImps "" "" allImps $ do --debug "Import env setup" withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do@@ -55,7 +55,7 @@ where allImps = defaultImportDecls ++ imps -withExpandedNames :: TypeDecl -> (TypeDecl -> TcBase a) -> TcBase a+withExpandedNames :: TypeDecl -> (TypeDecl -> TcCont r a) -> TcCont r a withExpandedNames td tcbaf = do tm <- getTypeMap --debug $ "TypeMap: " ++ show tm@@ -110,7 +110,7 @@ ------------------------------------------------------------------ -withEnvFromImps :: DirectoryPath -> String -> [ImportDecl] -> TcBase a -> TcBase a+withEnvFromImps :: DirectoryPath -> String -> [ImportDecl] -> TcCont r a -> TcCont r a withEnvFromImps dir thisStr is tcba = do --debug ("withEnvFromImpsies: " ++ show is) --withEnvFromImps dir thisStr (imp:is) =@@ -118,7 +118,7 @@ -- withEnvFromImp dir thisStr imp . withEnvFromImps dir thisStr is -withEnvFromImp :: DirectoryPath -> String -> ImportDecl -> TcBase a -> TcBase a+withEnvFromImp :: DirectoryPath -> String -> ImportDecl -> TcCont r a -> TcCont r a -- import java.*; withEnvFromImp dir thisStr imp@(ImportDecl False (Name pkgNames) True) tcba = do --debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames)@@ -143,7 +143,7 @@ -withEnvFromPkg :: [Ident] -> [(FilePath, String)] -> TcBase a -> TcBase a+withEnvFromPkg :: [Ident] -> [(FilePath, String)] -> TcCont r a -> TcCont r a withEnvFromPkg [] [] tcba = tcba -- Hack for the "this" package withEnvFromPkg pkgPath [] tcba = do tm <- getTypeMap@@ -155,7 +155,7 @@ withEnvFromClass fp n . withEnvFromPkg pkgPath pns $ tcba -withEnvFromSingleClass :: [Ident] -> FilePath -> String -> TcBase a -> TcBase a+withEnvFromSingleClass :: [Ident] -> FilePath -> String -> TcCont r a -> TcCont r a withEnvFromSingleClass pkgPath fp n tcba = do withEnvFromClass fp n . withEnvFromPkg pkgPath [] $ tcba@@ -163,7 +163,7 @@ ------------------------------------------------------------------------- -- This is where the really fun stuff happens -withEnvFromClass :: FilePath -> String -> TcBase a -> TcBase a+withEnvFromClass :: FilePath -> String -> TcCont r a -> TcCont r a withEnvFromClass fp className tcba = do --debug $ "Checking imported class: " ++ className ClassDecl _ id@(Ident cuName) tps _super _impls (ClassBody ds) <- getClass fp@@ -185,7 +185,7 @@ --------------------------------------------------------------------- -- Working with actors -fetchActors :: [MemberDecl] -> TcBase a -> TcBase a+fetchActors :: [MemberDecl] -> TcCont r a -> TcCont r a fetchActors mDecls tcba = do --debug "fetchActors" let acts = [ (ms, vd) @@ -202,18 +202,18 @@ --debug "fetchActors complete" tcba - where spawnActor, evalActor, aliasActor :: ([Modifier],VarDecl) -> TcBase a -> TcBase a+ where spawnActor, evalActor, aliasActor :: ([Modifier],VarDecl) -> TcCont r a -> TcCont r a spawnActor (ms, VarDecl (VarId i) _) tcba = do a <- freshActorId p <- getReadPolicy ms- let vti = VTI actorT p (Static `elem` ms) (Final `elem` ms)+ let vti = VSig actorT p (Static `elem` ms) (Final `elem` ms) withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcba aliasActor (ms, VarDecl (VarId i) _) tcba = do p <- getReadPolicy ms- let vti = VTI actorT p (Static `elem` ms) (Final `elem` ms)+ let vti = VSig actorT p (Static `elem` ms) (Final `elem` ms) a <- aliasActorId withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),@@ -222,7 +222,7 @@ evalActor (ms, VarDecl (VarId i) (Just (InitExp e))) tcba = do p <- getReadPolicy ms- let vti = VTI actorT p (Static `elem` ms) (Final `elem` ms)+ let vti = VSig actorT p (Static `elem` ms) (Final `elem` ms) a <- case e of ExpName n -> do tm <- getTypeMap@@ -238,7 +238,7 @@ ---------------------------------------------------------------------- -- Working with policies -fetchPols :: [MemberDecl] -> TcBase a -> TcBase a+fetchPols :: [MemberDecl] -> TcCont r a -> TcCont r a fetchPols mds tcba = do --debug "fetchPols" --debug $ "all policy decls: " ++ show [ fd | fd@(FieldDecl _ (PrimType PolicyT) _) <- mds ]@@ -251,7 +251,7 @@ withFoldMap fetchPol pols $ tcba -fetchPol :: (Ident, Exp) -> TcBase a -> TcBase a+fetchPol :: (Ident, Exp) -> TcCont r a -> TcCont r a fetchPol (i,e) tcba = do p <- case e of ExpName n -> do@@ -268,7 +268,7 @@ ------------------------------------------------------------ -- Working with typemethods -fetchTMs :: [MemberDecl] -> TcBase a -> TcBase a+fetchTMs :: [MemberDecl] -> TcCont r a -> TcCont r a fetchTMs memberDecls tcba = do let ipbs = [ (i,(map paramIdent ps,body)) | MethodDecl ms _ _ i ps _ (MethodBody (Just body)) <-memberDecls,@@ -285,18 +285,18 @@ ------------------------------------------------------------ -- Working with locks -fetchSignatures :: [MemberDecl] -> TcBase a -> TcBase a+fetchSignatures :: [MemberDecl] -> TcCont r a -> TcCont r a fetchSignatures memberDecls tcba = withFoldMap fetchSignature memberDecls $ tcba -fetchSignature :: MemberDecl -> TcBase a -> TcBase a+fetchSignature :: MemberDecl -> TcCont r a -> TcCont r a fetchSignature memberDecl tcba = do --debug $ "fetchSignature: " ++ show memberDecl case memberDecl of FieldDecl ms ty vds -> do tcty <- evalSrcType ty pol <- getReadPolicy ms- let vti = VTI tcty pol (Static `elem` ms) (Final `elem` ms)+ let vti = VSig tcty pol (Static `elem` ms) (Final `elem` ms) withTypeMap (\tm -> tm { fields = foldl (\m (VarDecl (VarId i) _) -> Map.insert i vti m) @@ -313,7 +313,7 @@ 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 mti = MTI {+ let mti = MSig { mRetType = tcty, mRetPol = rPol, mPars = pPols,@@ -333,7 +333,7 @@ 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 = CTI {+ let cti = CSig { cPars = pPols, cWrites = wPol, cExpects = expects,@@ -347,7 +347,7 @@ lPol <- getLockPolicy ms --debug $ "lPol: " ++ show lPol -- TODO: Store lock properties!- let vti = VTI (lockT []) lPol True True+ let vti = VSig (lockT []) lPol True True arity = length mps withTypeMap (\tm -> tm { lockArities = Map.insert i arity (lockArities tm),@@ -355,7 +355,7 @@ tcba - where eSpecToSig :: ExceptionSpec -> TcBase (TcType, ExnSig)+ where eSpecToSig :: ExceptionSpec -> TcCont r (TcType, ExnSig) eSpecToSig (ExceptionSpec ms eType) = do ty <- evalSrcType (RefType eType) -- should use evalSrcRefType rPol <- getReadPolicy ms@@ -369,7 +369,7 @@ } return (ty, esig) - paramInfo :: FormalParam -> TcBase (TcType, TcPolicy)+ paramInfo :: FormalParam -> TcCont r (TcType, TcPolicy) paramInfo (FormalParam ms ty _ (VarId i)) = do pPol <- getParamPolicy i ms pTy <- evalSrcType ty@@ -382,7 +382,7 @@ tdIdentStr (ClassTypeDecl (ClassDecl _ (Ident str) _ _ _ _)) = str tdIdentStr (InterfaceTypeDecl (InterfaceDecl _ (Ident str) _ _ _)) = str --------------------------------------------------------------------------------------getClass :: String -> TcBase ClassDecl+getClass :: String -> TcCont r ClassDecl getClass piPath = do fc <- liftIO $ readFile piPath let east = parser compilationUnit fc@@ -414,11 +414,11 @@ ------------------------------------------------------------------------------------- -- TODO: The module structure needs refactoring -typeCheckTd :: TypeDecl -> TcBase ()+typeCheckTd :: TypeDecl -> TcCont r () typeCheckTd (ClassTypeDecl cd) = typeCheckCd cd typeCheckTd (InterfaceTypeDecl id) = typeCheckId id -typeCheckId :: InterfaceDecl -> TcBase ()+typeCheckId :: InterfaceDecl -> TcCont r () typeCheckId (InterfaceDecl ms i tps _supers (InterfaceBody memberDecls)) = do --debug "typeCheckId" withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do@@ -437,7 +437,7 @@ --debug "typeCheckMemberDecls start" typeCheckMemberDecls staticWPol constrWPol memberDecls -typeCheckCd :: ClassDecl -> TcBase ()+typeCheckCd :: ClassDecl -> TcCont r () typeCheckCd (ClassDecl ms i tps _super _impls (ClassBody decls)) = do --debug "typeCheckCd" withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do@@ -459,35 +459,35 @@ typeCheckMemberDecls staticWPol constrWPol memberDecls -withThisType :: Ident -> [TypeParam] -> TcBase a -> TcBase a+withThisType :: Ident -> [TypeParam] -> TcCont r a -> TcCont r a withThisType i tps = withTypeMap $ \tm -> -- We insert an empty typemap at first, -- since we are only using this when checking signatures tm { types = Map.insert i (tps,emptyTM) (types tm) } -withThisTypeSigs :: Ident -> [TypeParam] -> TcBase a -> TcBase a+withThisTypeSigs :: Ident -> [TypeParam] -> TcCont r a -> TcCont r a withThisTypeSigs i tps tcba = do tm <- getTypeMap let thisTm = tm { types = Map.empty, packages = Map.empty } extendTypeMapT i tps thisTm $ tcba -withTypeParam :: TypeParam -> TcBase a -> TcBase a+withTypeParam :: TypeParam -> TcCont r a -> TcCont r a withTypeParam tp tcba = case tp of ActorParam i -> do- let vti = VTI actorT top False True+ let vti = VSig actorT top False True withTypeMap (\tm -> tm { actors = Map.insert i (ActorTPVar i) (actors tm), fields = Map.insert i vti (fields tm) }) $ tcba PolicyParam i -> do- let vti = VTI policyT top False True+ let vti = VSig policyT top False True withTypeMap (\tm -> tm { policies = Map.insert i (TcRigidVar i) (policies tm), fields = Map.insert i vti (fields tm) }) $ tcba LockStateParam i -> do- let vti = VTI (lockT []) top False True+ let vti = VSig (lockT []) top False True withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) $ tcba TypeParam i _ -> do@@ -501,7 +501,7 @@ -- TODO: We may have a problem with boot-strapping here. -- We can stay clear of the problem for now, using careful -- Paragon coding, but we need to think about it and fix it eventually.-typeCheckActorFields :: [MemberDecl] -> TcBase a -> TcBase a+typeCheckActorFields :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckActorFields = fetchActors {- let acts = [ (ms, vd) | FieldDecl ms (PrimType ActorT) vds <- mDecls @@ -513,12 +513,12 @@ --------------------------------------------------------------- -- Locks -typeCheckLockDecls :: [MemberDecl] -> TcBase a -> TcBase a+typeCheckLockDecls :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckLockDecls mds tcba = do let ls = [ ld | ld@ LockDecl {} <- mds ] withFoldMap typeCheckLockDecl ls $ tcba -typeCheckLockDecl :: MemberDecl -> TcBase a -> TcBase a+typeCheckLockDecl :: MemberDecl -> TcCont r a -> TcCont r a typeCheckLockDecl (LockDecl ms i mps props) tcba = do -- lPol <- getLockPolicy ms -- TODO: Store lock properties!@@ -531,7 +531,7 @@ --------------------------------------------------------------- -- Typemethods -typeCheckTypeMethods :: [MemberDecl] -> TcBase a -> TcBase a+typeCheckTypeMethods :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckTypeMethods mds tcba = do let tms = [ tmd | tmd@(MethodDecl ms _ _ _ _ _ _) <- mds, Typemethod `elem` ms@@ -543,7 +543,7 @@ tcba -- Precondition: only applied on actual typemethods-typeCheckTMSig :: MemberDecl -> TcBase a -> TcBase a+typeCheckTMSig :: MemberDecl -> TcCont r a -> TcCont r a typeCheckTMSig (MethodDecl ms tps retT i ps exns _) tcba = do (tyPs, mti) <- withErrCtxt ("When checking signature of typemethod " ++ prettyPrint i ++ ":\n") $ do@@ -560,7 +560,7 @@ check (null exns) $ "Methods annotated with typemethod may not throw exceptions" tyPs <- mapM evalSrcType [ t | FormalParam _ t _ _ <- ps ] rTy <- evalReturnType retT- let mti = MTI {+ let mti = MSig { mRetType = rTy, mRetPol = bottom, mWrites = top,@@ -573,7 +573,7 @@ withTypeMap (\tm -> tm { methods = Map.insert (i,tyPs) ([],mti) (methods tm) }) $ tcba -addTMBody :: MemberDecl -> TcBase a -> TcBase a+addTMBody :: MemberDecl -> TcCont r a -> TcCont r a addTMBody (MethodDecl _ _ _ i ps _ (MethodBody (Just bl))) = let pis = [ pi | FormalParam _ _ _ (VarId pi) <- ps ] in withTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) }@@ -582,14 +582,14 @@ ------------------------------------------------------------------------------------- -- Policies -typeCheckPolicyFields :: [MemberDecl] -> TcBase a -> TcBase a+typeCheckPolicyFields :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckPolicyFields mds = let pfs = [ pf | pf@(FieldDecl _ (PrimType PolicyT) _) <- mds ] in -- The 'map' here means fields can only refer to things above them withFoldMap typeCheckPolicyField pfs -- Precondition: only apply on policies-typeCheckPolicyField :: MemberDecl -> TcBase a -> TcBase a+typeCheckPolicyField :: MemberDecl -> TcCont r a -> TcCont r a typeCheckPolicyField fd@(FieldDecl ms t vds) tcba = do --debug "typeCheckPolicyField" -- 0. Flatten@@ -604,7 +604,7 @@ "typeCheckPolicyField: Policy must have policy bottom" -- 3. Add signature to environment tcty <- evalSrcType t- return $ VTI {+ return $ VSig { varType = tcty, varPol = bottom, varStatic = Static `elem` ms,@@ -619,12 +619,12 @@ tcba where - addField :: VTypeInfo -> Ident -> TcBase a -> TcBase a+ addField :: VarFieldSig -> Ident -> TcCont r a -> TcCont r a addField vti i = withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) -evalAddInit :: (Ident, VarInit) -> TcBase a -> TcBase a+evalAddInit :: (Ident, VarInit) -> TcCont r a -> TcCont r a evalAddInit (i, InitExp eInit) tcba = do --debug $ "evalAddInit: " ++ show i tcPol <- withErrCtxt ("When evaluating the initializer of field " @@ -636,19 +636,19 @@ ------------------------------------------------------------------------------ -- Signatures -typeCheckSignatures :: [MemberDecl] -> (TcPolicy -> TcBase a) -> TcBase a+typeCheckSignatures :: [MemberDecl] -> (TcPolicy -> TcCont r a) -> TcCont r a typeCheckSignatures mds tcbaf = do st <- setupStartState withFoldMap (typeCheckSignature st) mds $ getConstrPol >>= tcbaf -getConstrPol :: TcBase TcPolicy+getConstrPol :: TcCont r TcPolicy getConstrPol = do mConstrs <- constrs <$> getTypeMap let wPols = map (cWrites . snd) $ Map.elems mConstrs return $ foldl join bottom wPols -typeCheckSignature :: TcState -> MemberDecl -> TcBase a -> TcBase a+typeCheckSignature :: TcState -> MemberDecl -> TcCont r a -> TcCont r a -- Fields typeCheckSignature st fd@(FieldDecl ms t vds) tcba | t /= PrimType PolicyT && t /= PrimType ActorT = do@@ -666,7 +666,7 @@ mapM_ (typeCheckPolicyMod st) rPolExps rPol <- getReadPolicy ms -- 3. Add signature to typemap- return $ VTI {+ return $ VSig { varType = ty, varPol = rPol, varStatic = Static `elem` ms,@@ -675,7 +675,7 @@ withFoldMap (addField vti) vds $ tcba - where addField :: VTypeInfo -> VarDecl -> TcBase a -> TcBase a+ where addField :: VarFieldSig -> VarDecl -> TcCont r a -> TcCont r a addField vti (VarDecl (VarId i) _) = withTypeMap $ \tm -> tm { fields = Map.insert i vti (fields tm) }@@ -706,7 +706,7 @@ -- 6. Add signature to typemap rPol <- getReturnPolicy ms pPols wPol <- getWritePolicy ms- let mti = MTI {+ let mti = MSig { mRetType = ty, mRetPol = rPol, mWrites = wPol,@@ -738,7 +738,7 @@ xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns -- 5. Add signature to typemap wPol <- getWritePolicy ms- let cti = CTI {+ let cti = CSig { cWrites = wPol, cPars = pPols, cExpects = es,@@ -755,21 +755,21 @@ --debug $ "typeCheckSignature: " ++ prettyPrint ld vti <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do pol <- getLockPolicy ms- return $ VTI (lockT []) pol True True+ return $ VSig (lockT []) pol True True withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) $ tcba typeCheckSignature _ _ tcba = tcba -withParam :: FormalParam -> TcBase a -> TcBase a+withParam :: FormalParam -> TcCont r a -> TcCont r a withParam (FormalParam _ _ _ (VarId i)) = withTypeMap $ \tm -> - tm { fields = Map.insert i (VTI err err err err) (fields tm) }+ tm { fields = Map.insert i (VSig err err err err) (fields tm) } where err = error "Use of parameter directly in modifier" -- TODO: UUUUGLY! -typeCheckExnSig :: TcState -> ExceptionSpec -> TcBase (TcType, ExnSig)+typeCheckExnSig :: TcState -> ExceptionSpec -> TcCont r (TcType, ExnSig) typeCheckExnSig st (ExceptionSpec ms xT) = do withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do ty <- TP.TcRefT <$> evalSrcRefType xT@@ -787,7 +787,7 @@ } return (ty, xSig) -checkPolicyMods :: TcState -> [Modifier] -> String -> TcBase ()+checkPolicyMods :: TcState -> [Modifier] -> String -> TcCont r () checkPolicyMods st ms failStr = do --debug $ "checkPolicyMods: " ++ show ms let rPolExps = [ e | Reads e <- ms ] @@ -795,7 +795,7 @@ check (length rPolExps <= 1 && length wPolExps <= 1) failStr mapM_ (typeCheckPolicyMod st) $ rPolExps ++ wPolExps -checkLMMods :: [Modifier] -> TcBase LockMods+checkLMMods :: [Modifier] -> TcCont r LockMods checkLMMods ms = do let cs = concat [ l | Closes l <- ms ] os = concat [ l | Opens l <- ms ]@@ -803,12 +803,12 @@ tcOs <- mapM evalLock os return (tcCs, tcOs) -checkExpectsMods :: [Modifier] -> TcBase [TcLock]+checkExpectsMods :: [Modifier] -> TcCont r [TcLock] checkExpectsMods ms = do let es = concat [ l | Expects l <- ms ] mapM evalLock es -typeCheckParam :: TcState -> FormalParam -> TcBase (TcType, TcPolicy)+typeCheckParam :: TcState -> FormalParam -> TcCont r (TcType, TcPolicy) typeCheckParam st (FormalParam ms t _ (VarId i)) = do withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do -- 1. Check parameter type@@ -819,7 +819,7 @@ rPol <- getParamPolicy i ms return (ty, rPol) -typeCheckPolicyMod :: TcState -> Policy -> TcBase ()+typeCheckPolicyMod :: TcState -> Policy -> TcCont r () typeCheckPolicyMod st polExp = do --debug $ "typeCheckPolicyMod " ++ show polExp ((ty, _pol), cs) <- runTc (simpleEnv top) st @@ -834,12 +834,12 @@ ------------------------------------------------------------------------------ -- Bodies -typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl] -> TcBase ()+typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl] -> TcCont r () typeCheckMemberDecls sLim cLim ms = do st <- setupStartState mapM_ (typeCheckMemberDecl sLim cLim st) ms -typeCheckMemberDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcBase ()+typeCheckMemberDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcCont r () typeCheckMemberDecl sLim cLim st fd@(FieldDecl {}) = typeCheckFieldDecl sLim cLim st fd typeCheckMemberDecl _ _ st md@(MethodDecl {}) =@@ -848,17 +848,17 @@ typeCheckConstrDecl st cd typeCheckMemberDecl _ _ _ _ = return () -typeCheckFieldDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcBase ()+typeCheckFieldDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcCont r () typeCheckFieldDecl staticLim constrLim st fd@(FieldDecl ms t vds) = do --debug $ "typeCheckFieldDecl:" ++ show fd let lim = if Static `elem` ms then staticLim else constrLim mapM_ (typeCheckVarDecl lim st) vds -typeCheckVarDecl :: TcPolicy -> TcState -> VarDecl -> TcBase ()+typeCheckVarDecl :: TcPolicy -> TcState -> VarDecl -> TcCont r () typeCheckVarDecl lim st (VarDecl (VarId i) mInit) = do --debug $ "typeCheckVarDecl:" ++ show i withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do- Just (VTI matchTy matchPol _ _) <- Map.lookup i . fields <$> getTypeMap + Just (VSig matchTy matchPol _ _) <- Map.lookup i . fields <$> getTypeMap case mInit of Nothing -> return () Just (InitExp e) -> do@@ -868,18 +868,18 @@ constraint_ pol matchPol solve cs -typeCheckMethodDecl :: TcState -> MemberDecl -> TcBase ()+typeCheckMethodDecl :: TcState -> MemberDecl -> TcCont r () typeCheckMethodDecl st (MethodDecl _ tps _ i ps _ mb) = do -- Lookup the correct function signature -- debug $ "Type-checking method " ++ prettyPrint i withErrCtxt ("When checking body of method " ++ prettyPrint i ++ ":\n") $ do withFoldMap withTypeParam tps $ do tysPs <- mapM evalSrcType $ [ t | FormalParam _ t _ _ <- ps ]- Just (tps, MTI tyRet pRet pPars pWri expLs lMods xSigs) <- + Just (tps, MSig tyRet pRet pPars pWri expLs lMods xSigs) <- Map.lookup (i,tysPs) . methods <$> getTypeMap -- Setup the environment in which to check the body- let parVtis = [ (i, VTI t p False (isFinal ms)) |+ let parVtis = [ (i, VSig t p False (isFinal ms)) | (FormalParam ms _ _ (VarId i), t, p) <- zip3 ps tysPs pPars ] pars = map fst parVtis exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs@@ -910,19 +910,19 @@ "Declared lock modifiers not general enough: " ++ show lMods mapM_ (checkExnMods endSt) exnLMods -typeCheckConstrDecl :: TcState -> MemberDecl -> TcBase ()+typeCheckConstrDecl :: TcState -> MemberDecl -> TcCont r () typeCheckConstrDecl st cd@(ConstructorDecl _ tps ci ps _ cb) = do withErrCtxt ("When checking body of constructor " ++ prettyPrint ci ++ ":\n") $ do --debug $ "Type-checking constructor:\n " ++ prettyPrint cd withFoldMap withTypeParam tps $ do -- Lookup the correct function signature tysPs <- mapM evalSrcType $ [ t | FormalParam _ t _ _ <- ps ]- Just (tps, CTI pPars pWri expLs lMods xSigs) <- + Just (tps, CSig pPars pWri expLs lMods xSigs) <- Map.lookup tysPs . constrs <$> getTypeMap -- Setup the environment in which to check the body tm <- getTypeMap- let parVtis = [ (i, VTI t p False (isFinal ms)) |+ let parVtis = [ (i, VSig t p False (isFinal ms)) | (FormalParam ms _ _ (VarId i), t, p) <- zip3 ps tysPs pPars ] pars = map fst parVtis exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs@@ -931,7 +931,7 @@ exnEnts = [ ExnEntity t | t <- map fst xSigs ] -- Assigning to non-static fields of 'this' in a constructor is a local write fieEnts = concat [ [ThisFieldEntity i,VarEntity (Name [i])] - | (i, VTI _ _ False _) <- Map.assocs (fields tm) ]+ | (i, VSig _ _ False _) <- Map.assocs (fields tm) ] --debug $ "fieEnts: " ++ show fieEnts let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat bottom) env = TcEnv {@@ -958,13 +958,13 @@ mapM_ (checkExnMods endSt) exnLMods -aliasIfActor :: (Ident, TcType) -> TcBase [(Ident, ActorId)]+aliasIfActor :: (Ident, TcType) -> TcCont r [(Ident, ActorId)] aliasIfActor (i, ty) | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)] | otherwise = return [] -checkExnMods :: TcState -> (TcType, LockMods) -> TcBase ()+checkExnMods :: TcState -> (TcType, LockMods) -> TcCont r () checkExnMods st (xTy, lms) = do let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st) maybeM mExnSt $ \sX -> do@@ -973,10 +973,10 @@ ++ show lms -tcMethodBody :: MethodBody -> Tc ()+tcMethodBody :: MethodBody -> Tc r () tcMethodBody (MethodBody mBlock) = maybeM mBlock $ tcBlock -tcConstrBody :: ConstructorBody -> Tc ()+tcConstrBody :: ConstructorBody -> Tc r () tcConstrBody (ConstructorBody Nothing stmts) = tcBlockStmts stmts @@ -1032,5 +1032,5 @@ _ -> False -debug :: String -> TcBase ()+debug :: String -> TcCont r () debug str = liftIO $ putStrLn $ "DEBUG: " ++ str
src/Language/Java/Paragon/TypeCheck/Constraints.hs view
@@ -2,10 +2,10 @@ import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Locks-import Language.Java.Paragon.TypeCheck.Monad.TcBase+import Language.Java.Paragon.TypeCheck.Monad.TcCont data Constraint = LRT TcPolicyRec TcPolicy TcPolicy deriving Show -solve :: [Constraint] -> TcBase ()+solve :: [Constraint] -> TcCont r () solve cs = liftIO $ mapM_ print cs -- DEBUG
src/Language/Java/Paragon/TypeCheck/Evaluate.hs view
@@ -19,7 +19,7 @@ -- Working with typemethods -- -------------------------------------------- {--readPol :: [Modifier] -> Tc (Maybe TcPolicy)+readPol :: [Modifier] -> Tc r (Maybe TcPolicy) readPol ms = do let rs = [ p | Reads p <- ms ] case rs of@@ -27,12 +27,12 @@ [p] -> Just <$> evaluate p _ -> fail "More than one read modifier found" -fieldPol, localVarPol :: [Modifier] -> Tc TcPolicy+fieldPol, localVarPol :: [Modifier] -> Tc r TcPolicy fieldPol ms = do mpol <- readPol ms return $ mpol `orUse` bottom -paramPol :: Ident -> [Modifier] -> Tc TcPolicy+paramPol :: Ident -> [Modifier] -> Tc r TcPolicy paramPol i ms = do mpol <- readPol ms case mpol of@@ -45,13 +45,13 @@ Nothing -> newMetaPolVar Just p -> return p -returnPol :: [Modifier] -> [TcPolicy] -> Tc TcPolicy+returnPol :: [Modifier] -> [TcPolicy] -> Tc r TcPolicy returnPol ms ppols = do mpol <- readPol ms let def = foldl join bottom ppols return $ mpol `orUse` def -}-evaluate :: Policy -> TcBase TcPolicy+evaluate :: Policy -> TcCont r TcPolicy evaluate (PolicyExp pe) = evalPolicyExp pe {-evaluate (ExpName n) = do polMap <- (policies . typemap) <$> getEnv@@ -69,7 +69,7 @@ evaluate (MethodInv mi) = evalTypeMethod mi evaluate e = fail $ "Unsupported type-level expression: " ++ prettyPrint e -evalTypeMethod :: MethodInvocation -> TcBase TcPolicy+evalTypeMethod :: MethodInvocation -> TcCont r TcPolicy evalTypeMethod = undefined orUse :: Maybe a -> a -> a
src/Language/Java/Paragon/TypeCheck/Monad.hs view
@@ -50,18 +50,20 @@ evalPolicy, evalPolicyExp, evalLock, evalActor, - Tc, (|||), getState, mergeWithState, liftBase,+ Tc, (|||), getState, mergeWithState, liftCont, runTc, setupStartState, - TcBase, runTcBase, liftIO, withErrCtxt+-- TcBase, runTcBase, liftIO, withErrCtxt+ TcCont, runTcCont, liftIO, withErrCtxt ) where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Pretty -import Language.Java.Paragon.TypeCheck.Monad.TcBase+--import Language.Java.Paragon.TypeCheck.Monad.TcBase+import Language.Java.Paragon.TypeCheck.Monad.TcCont import Language.Java.Paragon.TypeCheck.Monad.TcMonad import Language.Java.Paragon.TypeCheck.TcEnv@@ -83,7 +85,7 @@ import Data.List (union, intersperse) debug str = liftIO $ putStrLn $ "DEBUG: " ++ str-debugTc = liftBase . debug+debugTc = liftCont . debug -------------------------------------------- -- --@@ -123,159 +125,160 @@ -- this -getThisType :: Tc TcType-getThisType = liftBase getThisT+getThisType :: Tc r TcType+getThisType = liftCont getThisT -- returns -getReturn :: Tc (TcType, TcPolicy)+getReturn :: Tc r (TcType, TcPolicy) getReturn = returnI <$> getEnv {--registerReturn :: TcType -> TcPolicy -> Tc a -> Tc a+registerReturn :: TcType -> TcPolicy -> Tc r a -> Tc r a registerReturn ty p = withEnv $ \env -> env { returnI = (ty,p) } -} -- lookup entities ---fieldEnvToVars :: Tc a -> Tc a+--fieldEnvToVars :: Tc r a -> Tc r a --fieldEnvToVars = withEnv $ \env -> env { vars = fields (typemap env) } -extendVarEnvList :: [(Ident, VTypeInfo)] -> Tc a -> Tc a+extendVarEnvList :: [(Ident, VarFieldSig)] -> Tc r a -> Tc r a extendVarEnvList vs = withEnv $ \env -> let oldVmap = vars env newVmap = foldl (\m (i,vti) -> Map.insert i vti m) oldVmap vs in env { vars = newVmap } -extendVarEnv :: Ident -> VTypeInfo -> Tc a -> Tc a+extendVarEnv :: Ident -> VarFieldSig -> Tc r a -> Tc r a --extendVarEnv i = extendVarEnvN i---extendVarEnvN :: Ident -> VTypeInfo -> Tc a -> Tc a+--extendVarEnvN :: Ident -> VarFieldSig -> Tc r a -> Tc r a extendVarEnv i vti = withEnv $ \env -> let oldVmap = vars env newVmap = Map.insert i vti oldVmap in env { vars = newVmap } -lookupActorName :: ActorName -> Tc (TcType, TcPolicy)+lookupActorName :: ActorName -> Tc r (TcType, TcPolicy) lookupActorName (ActorName n) = lookupVar n lookupActorName (ActorTypeVar i) = lookupVar (Name [i]) -lookupVar :: Name -> Tc (TcType, TcPolicy)+lookupVar :: Name -> Tc r (TcType, TcPolicy) lookupVar (Name n@(i:is)) = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap (newTm,ty,pol,rest) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of- Just (VTI ty p _ _) -> do+ Just (VSig ty p _ _) -> do let tyTm = lookupTypeOfT ty tm return (tyTm, ty, p, is) Nothing -> return (tm,voidT,bottom,n) aux newTm ty pol rest - where aux :: TypeMap -> TcType -> TcPolicy -> [Ident] -> Tc (TcType, TcPolicy)+ where aux :: TypeMap -> TcType -> TcPolicy -> [Ident] -> Tc r (TcType, TcPolicy) aux _ ty pol [] = return (ty, pol) aux tm _ pol (i:is) = do (newTm,newTy,newPol) <- case Map.lookup i (fields tm) of- Just (VTI typ pol _ _) -> do- baseTm <- liftBase getTypeMap+ Just (VSig typ pol _ _) -> do+ baseTm <- liftCont getTypeMap return $ (lookupTypeOfT typ baseTm, typ, pol) Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (aTm,voidT,bottom)- Nothing -> fail $ "lookupVar: No such name: " ++ show (i:is)+ Nothing -> fail $ "lookupVar: No such name: " + ++ prettyPrint(Name (i:is)) aux newTm newTy (pol `join` newPol) is -lookupMethod :: Name -> [TcType] -> Tc (TcPolicy, [TypeParam], MTypeInfo)+lookupMethod :: Name -> [TcType] -> Tc r (TcPolicy, [TypeParam], MethodSig) lookupMethod (Name n@(i:is)) ts = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap (newTm,pol,rest) <- do varMap <- vars <$> getEnv case Map.lookup i varMap of- Just (VTI ty p _ _) -> do+ Just (VSig ty p _ _) -> do let tyTm = lookupTypeOfT ty tm return (tyTm, p, is) Nothing -> return (tm,bottom,n) aux newTm pol rest ts - where aux :: TypeMap -> TcPolicy -> [Ident] -> [TcType] -> Tc (TcPolicy, [TypeParam], MTypeInfo)+ where aux :: TypeMap -> TcPolicy -> [Ident] -> [TcType] -> Tc r (TcPolicy, [TypeParam], MethodSig) aux tm pol [i] ts = case Map.lookup (i,ts) (methods tm) of Just (tps, mti) -> return (pol, tps, mti)- Nothing -> fail $ "lookupMethod: No such name: " ++ show i- ++ "\nMethods: " ++ show (methods tm)+ Nothing -> fail $ "lookupMethod: No such name: " ++ prettyPrint i+-- ++ "\nMethods: " ++ show (methods tm) aux tm pol (i:is) ts = do (newTm,newPol) <- case Map.lookup i (fields tm) of- Just (VTI typ pol _ _) -> do- baseTm <- liftBase getTypeMap+ Just (VSig typ pol _ _) -> do+ baseTm <- liftCont getTypeMap return $ (lookupTypeOfT typ baseTm, pol) Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> return (aTm,bottom)- Nothing -> error "lookupTypeOfN: No such name"+ Nothing -> fail $ "lookupTypeOfN: No such name: " ++ prettyPrint i aux newTm (pol `join` newPol) is ts --- tm <- liftBase getTypeMap+-- tm <- liftCont getTypeMap -- case lookupNamedMethod n ts tm of -- Just tpsmti -> return tpsmti -- Nothing -> fail $ "Unknown method: " ++ prettyPrint n -- ++ "(" ++ concat (intersperse "," $ map show ts) ++ ")" -getPolicy :: Name -> Tc TcPolicy+getPolicy :: Name -> Tc r TcPolicy getPolicy n = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap case lookupNamed policies n tm of- Nothing -> fail $ "getPolicy: No such policy: " ++ show n+ Nothing -> fail $ "getPolicy: No such policy: " ++ prettyPrint n Just p -> return p -lookupFieldT :: TcType -> Ident -> Tc VTypeInfo+lookupFieldT :: TcType -> Ident -> Tc r VarFieldSig lookupFieldT typ i = do- check (isClassType typ) $ "Not a class type: " ++ show typ- tm <- liftBase getTypeMap+ check (isClassType typ) $ "Not a class type: " ++ prettyPrint typ+ tm <- liftCont getTypeMap let aTm = lookupTypeOfT typ tm case Map.lookup i (fields aTm) of Just vti -> return vti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a field '" ++ prettyPrint i ++ "'" -lookupMethodT :: TcType -> Ident -> [TcType] -> Tc ([TypeParam], MTypeInfo)+lookupMethodT :: TcType -> Ident -> [TcType] -> Tc r ([TypeParam], MethodSig) lookupMethodT typ i pts = do- check (isClassType typ) $ "Not a class type: " ++ show typ- tm <- liftBase getTypeMap+ check (isClassType typ) $ "Not a class type: " ++ prettyPrint typ+ tm <- liftCont getTypeMap let aTm = lookupTypeOfT typ tm case Map.lookup (i,pts) (methods aTm) of Just pmti -> return pmti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a method '" ++ prettyPrint i ++ "'" -lookupConstr :: TcClassType -> [TcType] -> Tc ([TypeParam], CTypeInfo)+lookupConstr :: TcClassType -> [TcType] -> Tc r ([TypeParam], ConstrSig) lookupConstr ctyp pts = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap let typ = clsTypeToType ctyp aTm = lookupTypeOfT typ tm case Map.lookup pts (constrs aTm) of Just pcti -> return pcti Nothing -> fail $ "Class " ++ prettyPrint (typeName_ typ) ++ " does not have a constructor with argument types "- ++ show pts+ ++ "(" ++ concat (intersperse ", " (map prettyPrint pts)) ++ ")" -lookupLockArity :: Name -> Tc Int+lookupLockArity :: Name -> Tc r Int lookupLockArity n = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap case lookupNamed lockArities n tm of Nothing -> fail $ "Unknown lock: " ++ prettyPrint n Just arity -> return arity -lookupExn :: TcType -> Tc (TcPolicy, TcPolicy)+lookupExn :: TcType -> Tc r (TcPolicy, TcPolicy) lookupExn tyX = do exnMap <- exnsE <$> getEnv case Map.lookup tyX exnMap of Just ps -> return ps- Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ show tyX+ Nothing -> fail $ "lookupExn: Unregistered exception type: " ++ prettyPrint tyX -registerExn :: TcType -> TcPolicy -> TcPolicy -> Tc a -> Tc a+registerExn :: TcType -> TcPolicy -> TcPolicy -> Tc r a -> Tc r a registerExn tyX rX wX = registerExns [(tyX, (rX,wX))] -registerExns :: [(TcType, (TcPolicy, TcPolicy))] -> Tc a -> Tc a+registerExns :: [(TcType, (TcPolicy, TcPolicy))] -> Tc r a -> Tc r a registerExns tysPols = withEnv $ \env -> let oldMap = exnsE env@@ -283,29 +286,29 @@ in env { exnsE = newMap } -extendLockEnv :: [TcLock] -> Tc a -> Tc a+extendLockEnv :: [TcLock] -> Tc r a -> Tc r a extendLockEnv locks = withEnv $ \env -> env { lockstate = lockstate env `union` locks } -getBranchPC :: Entity -> Tc TcPolicy+getBranchPC :: Entity -> Tc r TcPolicy getBranchPC e = do env <- getEnv return $ branchPC (Just e) env -getBranchPC_ :: Tc TcPolicy+getBranchPC_ :: Tc r TcPolicy getBranchPC_ = do env <- getEnv return $ branchPC Nothing env -extendBranchPC :: TcPolicy -> Tc a -> Tc a+extendBranchPC :: TcPolicy -> Tc r a -> Tc r a extendBranchPC = withEnv . joinBranchPC -addBranchPCList :: [Ident] -> Tc a -> Tc a+addBranchPCList :: [Ident] -> Tc r a -> Tc r a addBranchPCList is = withEnv $ \env -> let (bm, def) = branchPCE env newBm = foldl (\m i -> Map.insert (VarEntity (Name [i])) bottom m) bm is in env { branchPCE = (newBm, def) } -addBranchPC :: Entity -> TcPolicy -> Tc a -> Tc a+addBranchPC :: Entity -> TcPolicy -> Tc r a -> Tc r a addBranchPC ent pol = withEnv $ \env -> let (bm, def) = branchPCE env@@ -313,12 +316,12 @@ in env { branchPCE = (newBm, def) } {-- Tying the knot for member policies-setFieldPol :: Ident -> TcPolicy -> Tc ()+setFieldPol :: Ident -> TcPolicy -> Tc r () setFieldPol i pF = do fMap <- (fields . typemap) <$> getEnv case Map.lookup (Name [i]) fMap of Nothing -> fail "panic: lookup of field failed when tying the knot"- Just (VTI ty tempP stc fin) -> do+ Just (VSig ty tempP stc fin) -> do case tempP of TcPolicyVar (TcMetaVar i ref) -> do mpol <- lift $ readIORef ref@@ -327,7 +330,7 @@ Just _ -> fail "panic: field policy already written when tying the knot" _ -> fail "panic: field policy already set when tying the knot" -setMethodPols :: Ident -> TcPolicy -> TcPolicy -> Tc ()+setMethodPols :: Ident -> TcPolicy -> TcPolicy -> Tc r () setMethodPols i retM -} @@ -336,74 +339,74 @@ -------------------------------------------- {- -- Leave actor mappings from fields-startState :: Tc ()+startState :: Tc r () startState = updateState $ \s -> s { lockMods = noMods, exnS = Map.empty } -} -- Actor Analysis -getActorId :: Name -> Tc ActorId+getActorId :: Name -> Tc r ActorId getActorId n = do actorMap <- actorSt <$> getState case Map.lookup n actorMap of- Nothing -> liftBase $ aliasActorId+ Nothing -> liftCont $ aliasActorId Just ai -> return $ aID ai -setActorId :: Name -> ActorId -> Tc ()+setActorId :: Name -> ActorId -> Tc r () setActorId n aid = updateState setAct where setAct :: TcState -> TcState setAct s@(TcState { actorSt = actMap }) = s { actorSt = Map.adjust replId n actMap } replId (AI _ st) = AI aid st -newActorIdWith :: Ident -> ActorId -> Tc ()+newActorIdWith :: Ident -> ActorId -> Tc r () newActorIdWith i aid = do updateState (insertAct aid) where insertAct :: ActorId -> TcState -> TcState insertAct aid s@(TcState { actorSt = actMap }) = s { actorSt = Map.insert (Name [i]) (AI aid Stable) actMap } -newActorId :: Ident -> Tc ActorId+newActorId :: Ident -> Tc r ActorId newActorId i = do - aid <- liftBase freshActorId+ aid <- liftCont freshActorId newActorIdWith i aid return aid -newAliasId :: Ident -> Tc ActorId+newAliasId :: Ident -> Tc r ActorId newAliasId i = do- aid <- liftBase aliasActorId+ aid <- liftCont aliasActorId newActorIdWith i aid return aid -freshActorId, aliasActorId :: TcBase ActorId+freshActorId, aliasActorId :: TcCont r ActorId freshActorId = (liftIO . newFresh) =<< getUniqRef aliasActorId = (liftIO . newAlias) =<< getUniqRef -scrambleActors :: Maybe TcType -> Tc ()+scrambleActors :: Maybe TcType -> Tc r () scrambleActors mtc = do let stb = maybe FullV (FieldV . typeName_) mtc state <- getState- u <- liftBase getUniqRef- newState <- liftBase . liftIO $ scramble u stb state+ u <- liftCont getUniqRef+ newState <- liftCont . liftIO $ scramble u stb state setState newState -- Exception tracking -getExnPC :: Tc TcPolicy+getExnPC :: Tc r TcPolicy getExnPC = exnPC <$> getState -throwExn :: ExnType -> TcPolicy -> Tc ()+throwExn :: ExnType -> TcPolicy -> Tc r () throwExn et pX = do- uref <- liftBase getUniqRef+ uref <- liftCont getUniqRef state <- getState let oldXmap = exnS state newXmap = Map.fromList [(et, ExnPoint state pX)]- mergedXmap <- liftBase . liftIO $ mergeExns uref oldXmap newXmap+ mergedXmap <- liftCont . liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } -deactivateExn :: ExnType -> Tc ()+deactivateExn :: ExnType -> Tc r () deactivateExn et = updateState $ \s -> let oldEmap = exnS s@@ -411,58 +414,58 @@ in s { exnS = newEmap } -activateExns :: [(ExnType, ExnSig)] -> Tc ()+activateExns :: [(ExnType, ExnSig)] -> Tc r () activateExns exns = do- uref <- liftBase getUniqRef+ uref <- liftCont getUniqRef state <- getState let (ts, sigs) = unzip exns xPoints <- mapM (\sigX -> do- s <- liftBase . liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO+ s <- liftCont . liftIO $ scramble uref FullV $ -- FullV should be Nothing - TODO state { lockMods = lockMods state ||>> exnMods sigX } return (s, exnWrites sigX)) sigs let oldXmap = exnS state newXmap = Map.fromList $ zip ts (map (uncurry ExnPoint) xPoints)- mergedXmap <- liftBase . liftIO $ mergeExns uref oldXmap newXmap+ mergedXmap <- liftCont . liftIO $ mergeExns uref oldXmap newXmap setState $ state { exnS = mergedXmap } -getExnState :: ExnType -> Tc (Maybe TcState)+getExnState :: ExnType -> Tc r (Maybe TcState) getExnState et = do eMap <- exnS <$> getState return $ epState <$> Map.lookup et eMap -mergeActiveExnStates :: Tc ()+mergeActiveExnStates :: Tc r () mergeActiveExnStates = do exnMap <- exnS <$> getState mapM_ (mergeWithState . epState) $ Map.elems exnMap -useExnState :: TcState -> Tc ()+useExnState :: TcState -> Tc r () useExnState es = updateState (\s -> s { exnS = exnS es }) -- Lockstate tracking -getCurrentLockState :: Tc [TcLock]+getCurrentLockState :: Tc r [TcLock] getCurrentLockState = do base <- lockstate <$> getEnv mods <- lockMods <$> getState return $ snd $ ([], base) ||>> mods -applyLockMods :: LockMods -> Tc ()+applyLockMods :: LockMods -> Tc r () applyLockMods lms = do updateState $ \s -> s { lockMods = lockMods s ||>> lms } -openLock, closeLock :: TcLock -> Tc ()+openLock, closeLock :: TcLock -> Tc r () openLock l = applyLockMods ([],[l]) closeLock l = applyLockMods ([l],[]) -- Policy inference -newMetaPolVar :: Tc TcPolicy+newMetaPolVar :: Tc r TcPolicy newMetaPolVar = do- uniq <- liftBase $ liftIO . getUniq =<< getUniqRef- ref <- liftBase $ liftIO (newIORef Nothing)+ uniq <- liftCont $ liftIO . getUniq =<< getUniqRef+ ref <- liftCont $ liftIO (newIORef Nothing) return $ TcPolicyVar (TcMetaVar uniq ref) ---newRigidPolVar :: Tc TcPolicy+--newRigidPolVar :: Tc r TcPolicy --newRigidPolVar = do -- uniq <- lift . getUniq =<< getUniqRef -- return $ TcRigidVar uniq@@ -471,28 +474,32 @@ -- Working with constraints -- -------------------------------------------- -constraint :: [TcLock] -> TcPolicy -> TcPolicy -> Tc ()+constraint :: [TcLock] -> TcPolicy -> TcPolicy -> Tc r () constraint ls p1 p2 = do -- addConstraint $ LRT ls p1 p2 g <- getGlobalLockProps case lrt (g `recmeet` rls) p1 p2 of Left b -> do --debugTc $ "constraint: p1: " ++ show p1 --debugTc $ "constraint: p2: " ++ show p2- check b $ "Cannot solve constraint: " ++ show (LRT (g `recmeet` rls) p1 p2)+ check b $ "Cannot solve constraint p <= q where" ++ --show (LRT (g `recmeet` rls) p1 p2)+ "\n* p = " ++ prettyPrint p1 +++ "\n* q = " ++ prettyPrint p2 +++ "\nin the presence of lock state {" +++ concat (intersperse ", " (map prettyPrint ls)) ++ "}" Right c -> addConstraint c where rls = locksToRec ls -getGlobalLockProps :: Tc TcPolicyRec+getGlobalLockProps :: Tc r TcPolicyRec getGlobalLockProps = return (TcPolicyRec []) locksToRec :: [TcLock] -> TcPolicyRec locksToRec ls = TcPolicyRec (map (\x -> TcClause x []) (map lockToAtom ls)) -constraint_ :: TcPolicy -> TcPolicy -> Tc ()+constraint_ :: TcPolicy -> TcPolicy -> Tc r () constraint_ = constraint [] -exnConsistent :: TcType -> ExnSig -> Tc ()+exnConsistent :: TcType -> ExnSig -> Tc r () exnConsistent exnTy (ExnSig rX wX _) = do exnMap <- exnsE <$> getEnv --debugTc $ "Using exnMap: " ++ show exnMap@@ -502,23 +509,12 @@ constraint_ wX wE constraint_ rE rX -{--fetchConstraints :: Tc () -> Tc [Constraint]-fetchConstraints (Tc f) = - Tc $ \e s u -> do - ma <- f e s u- case ma of- Left errs -> return $ Left errs- Right ((),s',cs) -> return $ Right (cs,s',[]) -solveConstraints :: [Constraint] -> Tc ()-solveConstraints = lift . solve--} -------------------------------------------- -- Working with typemaps -- -------------------------------------------- -extendTypeMapP :: [Ident] -> TypeMap -> TcBase a -> TcBase a+extendTypeMapP :: [Ident] -> TypeMap -> TcCont r a -> TcCont r a extendTypeMapP [] leafTm = withTypeMap (const leafTm) -- WARNING: overwrites extendTypeMapP is leafTm = withTypeMap $ \tm ->@@ -537,26 +533,26 @@ newTm = go is leafTm eTm in tm { packages = Map.insert i newTm mTm } -extendTypeMapT :: Ident -> [TypeParam] -> TypeMap -> TcBase a -> TcBase a+extendTypeMapT :: Ident -> [TypeParam] -> TypeMap -> TcCont r a -> TcCont r a extendTypeMapT i tps leafTm = withTypeMap $ \tm -> tm { types = Map.insert i (tps, leafTm) (types tm) } -lookupPkgTypeMap :: [Ident] -> TcBase TypeMap+lookupPkgTypeMap :: [Ident] -> TcCont r TypeMap lookupPkgTypeMap is = lookupTypeOfN (Name is) <$> getTypeMap ------------------------------------------------------------------- -- Evaluating types -evalReturnType :: Maybe Type -> TcBase TcType+evalReturnType :: Maybe Type -> TcCont r TcType evalReturnType = maybe (return voidT) evalSrcType -evalSrcType :: Type -> TcBase TcType+evalSrcType :: Type -> TcCont r TcType evalSrcType (PrimType pt) = return $ TcPrimT pt evalSrcType (RefType rt) = TcRefT <$> evalSrcRefType rt -evalSrcRefType :: RefType -> TcBase TcRefType+evalSrcRefType :: RefType -> TcCont r TcRefType evalSrcRefType (TypeVariable i) = return $ TcTypeVar i evalSrcRefType (ArrayType t mp) = do ty <- evalSrcType t@@ -564,29 +560,29 @@ return $ TcArrayT ty mpol evalSrcRefType (ClassRefType ct) = TcClsRefT <$> evalSrcClsType ct -evalSrcClsType :: ClassType -> TcBase TcClassType+evalSrcClsType :: ClassType -> TcCont r TcClassType evalSrcClsType (ClassType iArgs) = TcClassT <$> mapM (\(i,tas) -> (\ts -> (i, ts)) <$> mapM evalSrcTypeArg tas) iArgs -evalSrcTypeArg :: TypeArgument -> TcBase TcTypeArg+evalSrcTypeArg :: TypeArgument -> TcCont r TcTypeArg evalSrcTypeArg (ActualArg a) = evalSrcNWTypeArg a evalSrcTypeArg _ = fail "evalSrcTypeArg: Wildcards not yet supported" -evalSrcNWTypeArg :: NonWildTypeArgument -> TcBase TcTypeArg+evalSrcNWTypeArg :: NonWildTypeArgument -> TcCont r TcTypeArg evalSrcNWTypeArg (ActualType rt) = TcActualType <$> evalSrcRefType rt evalSrcNWTypeArg (ActualPolicy p) = TcActualPolicy <$> evalPolicy p evalSrcNWTypeArg (ActualActor n) = TcActualActor <$> evalActorId n evalSrcNWTypeArg (ActualLockState ls) = TcActualLockState <$> mapM evalLock ls -evalPolicy :: Exp -> TcBase TcPolicy+evalPolicy :: Exp -> TcCont r TcPolicy evalPolicy e = case e of ExpName n -> do --debug $ "evalPolicy: " ++ show n tm <- getTypeMap case lookupNamed policies n tm of Just p -> return p- Nothing -> fail $ "evalPolicy: no such policy\n" ++ "TypeMap: " - ++ show (types tm)+ Nothing -> fail $ "evalPolicy: no such policy: " ++ prettyPrint n + ++ "\nTypeMap: " ++ show (types tm) PolicyExp pl -> evalPolicyExp pl BinOp p1 Add p2 -> do pol1 <- evalPolicy p1@@ -599,36 +595,36 @@ Paren p -> evalPolicy p _ -> fail "evalPolicy: More here!" -evalPolicyExp :: PolicyExp -> TcBase TcPolicy+evalPolicyExp :: PolicyExp -> TcCont r TcPolicy evalPolicyExp (PolicyLit cs) = TcPolicy <$> mapM evalClause cs evalPolicyExp (PolicyOf i) = return $ TcRigidVar i evalPolicyExp (PolicyTypeVar i) = return $ TcRigidVar i -evalClause :: Clause Actor -> TcBase (TcClause TcActor)+evalClause :: Clause Actor -> TcCont r (TcClause TcActor) evalClause (Clause h b) = do h' <- evalActor h b' <- mapM evalAtom b return $ TcClause h' b' -evalActorName :: ActorName -> TcBase ActorId+evalActorName :: ActorName -> TcCont r ActorId evalActorName (ActorName n) = evalActorId n evalActorName (ActorTypeVar i) = return $ ActorTPVar i -evalActor :: Actor -> TcBase TcActor+evalActor :: Actor -> TcCont r TcActor evalActor (Actor n) = TcActor <$> evalActorName n evalActor (Var i) = return $ TcVar i -evalActorId :: Name -> TcBase ActorId+evalActorId :: Name -> TcCont r ActorId evalActorId n = do tm <- getTypeMap case lookupNamed actors n tm of Just aid -> return aid Nothing -> fail $ "evalActor: No such actor: " ++ prettyPrint n -evalAtom :: Atom -> TcBase TcAtom+evalAtom :: Atom -> TcCont r TcAtom evalAtom (Atom n as) = TcAtom n <$> mapM evalActor as -evalLock :: Lock -> TcBase TcLock+evalLock :: Lock -> TcCont r TcLock evalLock (Lock n ans) = do tm <- getTypeMap case lookupNamed lockArities n tm of@@ -641,7 +637,7 @@ return $ TcLock n aids evalLock (LockVar i) = return $ TcLockVar i -getActor :: ActorName -> TcBase ActorId+getActor :: ActorName -> TcCont r ActorId getActor (ActorName n) = do tm <- getTypeMap case lookupNamed actors n tm of@@ -713,7 +709,7 @@ ------------------------------------------------------------------------------------- -getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier] -> TcBase TcPolicy+getReadPolicy, getWritePolicy, getLockPolicy :: [Modifier] -> TcCont r TcPolicy getReadPolicy mods = case [pol |Reads pol <- mods ] of -- !!0 -- Read Policy? what if no read policy? [pol] -> evalPolicy pol@@ -729,13 +725,13 @@ [pol] -> evalPolicy pol [] -> return top -getParamPolicy :: Ident -> [Modifier] -> TcBase TcPolicy+getParamPolicy :: Ident -> [Modifier] -> TcCont r TcPolicy getParamPolicy i mods = case [pol | Reads pol <- mods ] of [pol] -> evalPolicy pol [] -> return $ ofPol i -getReturnPolicy :: [Modifier] -> [TcPolicy] -> TcBase TcPolicy+getReturnPolicy :: [Modifier] -> [TcPolicy] -> TcCont r TcPolicy getReturnPolicy mods pPols = case [pol | Reads pol <- mods ] of [pol] -> evalPolicy pol@@ -760,7 +756,7 @@ {- Graveyard -lookupVar :: Name -> Tc VTypeInfo+lookupVar :: Name -> Tc r VarFieldSig lookupVar n = do tryVar n `orElse` tryField n@@ -769,9 +765,9 @@ where tryVar = tryVarField (vars <$> getEnv)- tryField = tryVarField (fields <$> liftBase getTypeMap)+ tryField = tryVarField (fields <$> liftCont getTypeMap) - --tryVarField :: Tc (Map Ident VTypeInfo) -> Name -> Tc (Maybe VTypeInfo)+ --tryVarField :: Tc r (Map Ident VarFieldSig) -> Name -> Tc r (Maybe VarFieldSig) tryVarField recfetch (Name [i]) = do varMap <- recfetch case Map.lookup i varMap of@@ -789,6 +785,6 @@ tryVarField _ n = return Nothing tryQual n = do- tm <- liftBase getTypeMap+ tm <- liftCont getTypeMap return $ lookupNamed fields n tm -}
+ src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs view
@@ -0,0 +1,68 @@+module Language.Java.Paragon.TypeCheck.Monad.TcCont where++import Language.Java.Paragon.Syntax++import Language.Java.Paragon.TypeCheck.Monad.TcBase (TcBase, runTcBase)+import qualified Language.Java.Paragon.TypeCheck.Monad.TcBase + as Base (getUniqRef, getTypeMap, getThisT, withTypeMap, liftIO, withErrCtxt)++import Language.Java.Paragon.TypeCheck.Uniq (Uniq)+import Language.Java.Paragon.TypeCheck.TcEnv (TypeMap)+import Language.Java.Paragon.TypeCheck.Types (TcType)++import Control.Monad (liftM) -- liftM only to instantiate fmap+++-----------------------------------------------+-- The TcCont monad --+-----------------------------------------------++newtype TcCont r a = TcCont ((a -> TcBase r) -> TcBase r)++runTcCont :: TcType -> TcCont a a -> IO (Either String a)+runTcCont typ tcca = runTcBase typ $ runCont2Base tcca return+ where runCont2Base :: TcCont r a -> (a -> TcBase r) -> TcBase r+ runCont2Base (TcCont f) k = f k++++instance Monad (TcCont r) where+ return x = TcCont $ \k -> k x+ TcCont f >>= h = TcCont $ \k ->+ f (\a -> let TcCont g = h a in g k)++instance Functor (TcCont r) where+ fmap = liftM++-----------------------------------------------+-- Here's the whole reason why we go through +-- this lifting charade++callCC :: ((a -> TcCont r b) -> TcCont r a) -> TcCont r a+callCC cont = TcCont $ \k -> + let TcCont g = cont (\a -> TcCont $ \_ -> k a) in g k+++-----------------------------------------------+-- Lifting the TcBase combinators to TcCont++liftBase :: TcBase a -> TcCont r a+liftBase tcba = TcCont $ \k -> tcba >>= k++getUniqRef :: TcCont r Uniq+getUniqRef = liftBase Base.getUniqRef++getTypeMap :: TcCont r TypeMap+getTypeMap = liftBase Base.getTypeMap++getThisT :: TcCont r TcType+getThisT = liftBase Base.getThisT++withTypeMap :: (TypeMap -> TypeMap) -> TcCont r a -> TcCont r a+withTypeMap tmf (TcCont f) = TcCont $ \k -> Base.withTypeMap tmf $ f k++liftIO :: IO a -> TcCont r a+liftIO = liftBase . Base.liftIO++withErrCtxt :: String -> TcCont r a -> TcCont r a+withErrCtxt str (TcCont f) = TcCont $ \k -> Base.withErrCtxt str $ f k
src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs view
@@ -3,7 +3,8 @@ import Language.Java.Paragon.Syntax --import Language.Java.Paragon.Pretty -import Language.Java.Paragon.TypeCheck.Monad.TcBase+--import Language.Java.Paragon.TypeCheck.Monad.TcBase+import Language.Java.Paragon.TypeCheck.Monad.TcCont import Language.Java.Paragon.TypeCheck.TcEnv import Language.Java.Paragon.TypeCheck.TcState import Language.Java.Paragon.TypeCheck.Constraints@@ -20,21 +21,21 @@ -- The Tc monad -- ------------------------------------------------ ----- A monad on top of TcBase for typechecking+-- A monad on top of TcCont for typechecking -- on the level of method declarations. -- Has a method environment, a mergeable state, -- and a writer for constraints -newtype Tc a =- Tc (TcEnv -> TcState -> TcBase (a, TcState, [Constraint]))+newtype Tc r a =+ Tc (TcEnv -> TcState -> TcCont r (a, TcState, [Constraint])) -runTc :: TcEnv -> TcState -> Tc a -> TcBase (a, [Constraint])+runTc :: TcEnv -> TcState -> Tc r a -> TcCont r (a, [Constraint]) runTc env state (Tc f) = do (a,_,cs) <- f env state return (a, cs) --------------------------------------setupStartState :: TcBase TcState+setupStartState :: TcCont r TcState setupStartState = do tm <- getTypeMap let aMap = gatherActorInfo tm@@ -52,11 +53,11 @@ tMap = gatherActorInfoT (Map.assocs $ pkgsAndTypes tm) in Map.union aMap tMap - where mkStab :: VTypeInfo -> Stability- mkStab (VTI _ _ _ final) = + where mkStab :: VarFieldSig -> Stability+ mkStab (VSig _ _ _ final) = if final then Stable else FieldV (Name []) -- UGLY - mkInfo :: Map Ident VTypeInfo -> (Ident,ActorId) -> ([Ident], ActorInfo)+ mkInfo :: Map Ident VarFieldSig -> (Ident,ActorId) -> ([Ident], ActorInfo) mkInfo fs (i,aid) = case Map.lookup i fs of Just vti -> ([i], AI aid (mkStab vti))@@ -74,7 +75,7 @@ ------------------------------------- -instance Monad Tc where+instance Monad (Tc r) where return x = Tc $ \_ s -> return (x, s, []) Tc f >>= k = Tc $ \e s0 -> do (a, s1, cs1) <- f e s0@@ -84,56 +85,56 @@ fail err = Tc $ \_ _ -> fail err -instance Functor Tc where+instance Functor (Tc r) where fmap = liftM -liftBase :: TcBase a -> Tc a-liftBase tcba = Tc $ \_ s -> do+liftCont :: TcCont r a -> Tc r a+liftCont tcba = Tc $ \_ s -> do a <- tcba return (a, s, []) -- Running in parallel infix 1 |||-(|||) :: Tc a -> Tc b -> Tc (a,b)+(|||) :: Tc r a -> Tc r b -> Tc r (a,b) (Tc f1) ||| (Tc f2) = Tc $ \te ts -> do (a, ts1, cs1) <- f1 te ts (b, ts2, cs2) <- f2 te ts- ts' <- mergeStatesBase ts1 ts2+ ts' <- mergeStatesCont ts1 ts2 return $ ((a,b), ts', cs1 ++ cs2) -mergeStatesBase :: TcState -> TcState -> TcBase TcState-mergeStatesBase s1 s2 = do+mergeStatesCont :: TcState -> TcState -> TcCont r TcState+mergeStatesCont s1 s2 = do u <- getUniqRef liftIO $ mergeStates u s1 s2 -- The environment -getEnv :: Tc TcEnv+getEnv :: Tc r TcEnv getEnv = Tc (\e s -> return (e,s,[])) -withEnv :: (TcEnv -> TcEnv) -> Tc a -> Tc a+withEnv :: (TcEnv -> TcEnv) -> Tc r a -> Tc r a withEnv k (Tc f) = Tc (f . k) -- The state -getState :: Tc TcState+getState :: Tc r TcState getState = Tc (\_ s -> return (s,s,[])) -setState :: TcState -> Tc ()+setState :: TcState -> Tc r () setState s = Tc (\_ _ -> return ((),s,[])) -updateState :: (TcState -> TcState) -> Tc ()+updateState :: (TcState -> TcState) -> Tc r () updateState f = getState >>= return . f >>= setState -mergeWithState :: TcState -> Tc ()+mergeWithState :: TcState -> Tc r () mergeWithState s = do sOld <- getState- sNew <- liftBase $ mergeStatesBase sOld s+ sNew <- liftCont $ mergeStatesCont sOld s setState sNew -- Constraints -addConstraint :: Constraint -> Tc ()+addConstraint :: Constraint -> Tc r () addConstraint c = Tc (\_ s -> return ((), s, [c]))
src/Language/Java/Paragon/TypeCheck/TcEnv.hs view
@@ -23,9 +23,9 @@ data TypeMap = TypeMap { -- signatures- fields :: Map Ident VTypeInfo,- methods :: Map (Ident, [TcType]) ([TypeParam], MTypeInfo),- constrs :: Map [TcType] ([TypeParam], CTypeInfo),+ fields :: Map Ident VarFieldSig,+ methods :: Map (Ident, [TcType]) ([TypeParam], MethodSig),+ constrs :: Map [TcType] ([TypeParam], ConstrSig), lockArities :: Map Ident Int, -- known policy-level entities policies :: Map Ident TcPolicy,@@ -60,7 +60,7 @@ data TcEnv = TcEnv { -- lockProps :: ??,- vars :: Map Ident VTypeInfo,+ vars :: Map Ident VarFieldSig, lockstate :: [TcLock], returnI :: (TcType, TcPolicy), exnsE :: Map TcType (TcPolicy, TcPolicy),@@ -101,7 +101,7 @@ continueE = ContinueE returnE = ReturnE -data VTypeInfo = VTI { +data VarFieldSig = VSig { varType :: TcType, varPol :: TcPolicy, varStatic :: Bool,@@ -109,7 +109,7 @@ } deriving (Show, Data, Typeable) -data MTypeInfo = MTI {+data MethodSig = MSig { mRetType :: TcType, mRetPol :: TcPolicy, mPars :: [TcPolicy],@@ -127,7 +127,7 @@ } deriving (Show, Data, Typeable) -data CTypeInfo = CTI {+data ConstrSig = CSig { cPars :: [TcPolicy], cWrites :: TcPolicy, cExpects :: [TcLock],@@ -136,13 +136,7 @@ } deriving (Show, Data, Typeable) ---data LTypeInfo = LTI { arity :: Int, lockPol :: TcPolicy }--- deriving (Show, Data, Typeable) ---data TcActorRep = TcActorRep ActorId | TcActorTPVar Ident--- deriving (Show, Eq, Ord, Data, Typeable)-- -------------------------------------- -- Type argument instantiation -- --------------------------------------@@ -212,7 +206,7 @@ let actualTm = lookupTypeOfN (Name $ init is) tm in Map.lookup (last is) (recf actualTm) -lookupNamedMethod :: Name -> [TcType] -> TypeMap -> Maybe ([TypeParam],MTypeInfo)+lookupNamedMethod :: Name -> [TcType] -> TypeMap -> Maybe ([TypeParam],MethodSig) lookupNamedMethod (Name is) ts tm = let actualTm = lookupTypeOfN (Name $ init is) tm in Map.lookup (last is, ts) (methods actualTm)@@ -229,7 +223,7 @@ aux (i:is) tm baseTm = let newTm = case Map.lookup i (fields tm) of- Just (VTI typ _ _ _) -> lookupTypeOfT typ baseTm+ Just (VSig typ _ _ _) -> lookupTypeOfT typ baseTm Nothing -> case Map.lookup i (pkgsAndTypes tm) of Just aTm -> aTm Nothing -> error "lookupTypeOfN: No such name"
src/Language/Java/Paragon/TypeCheck/TcExp.hs view
@@ -30,15 +30,15 @@ litType (Char _) = charT litType (String _) = stringT litType (Null) = nullT-litType l = error $ "litType: " ++ show l+--litType l = error $ "litType: " ++ show l ----------------------------------- -- Checking expressions -- ----------------------------------- -debugTc str = liftBase $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str+debugTc str = liftCont $ liftIO $ putStrLn $ "DEBUG: Tc: " ++ str -tcExp :: Exp -> Tc (TcType, TcPolicy)+tcExp :: Exp -> Tc r (TcType, TcPolicy) -- Rule PAREN tcExp (Paren e) = tcExp e@@ -82,21 +82,21 @@ Just o -> do -- FIELDASS (tyO,pO) <- lookupVar o let (Name [i]) = f- (VTI tyF pF _ _) <- lookupFieldT tyO i+ (VSig tyF pF _ _) <- lookupFieldT tyO i return (tyF, pF, Just tyO, Just pO, Just (varE n), Just n) FieldLhs (PrimaryFieldAccess e fi) -> do (tyE, pE) <- tcExp e- (VTI tyF pF _ _) <- lookupFieldT tyE fi+ (VSig tyF pF _ _) <- lookupFieldT tyE fi let eEnt = case e of This -> Just $ thisFE fi _ -> Nothing return (tyF, pF, Just tyE, Just pE, eEnt, Nothing)- _ -> fail $ "Lhs not supported: " ++ show lhs+ _ -> fail $ "Lhs not supported: " ++ prettyPrint lhs (tyRhs, pRhs) <- tcExp rhs -- Check all the necessary constraints:- check (tyRhs <: tyV) $ "Type mismatch: " ++ show tyRhs ++ " <=> " ++ show tyV+ check (tyRhs <: tyV) $ "Type mismatch: " ++ prettyPrint tyRhs ++ " <=> " ++ prettyPrint tyV -- Check: E[branchPC](n) <= pV bpc <- maybe getBranchPC_ getBranchPC mEnt @@ -124,19 +124,19 @@ -- Rule NEW tcExp e@(InstanceCreation tas ct args mBody) = do --debugTc $ "tcExp: " ++ show e- tyT <- liftBase $ evalSrcClsType ct+ tyT <- liftCont $ evalSrcClsType ct -- DEBUG --debugTc $ "Type: " ++ show tyT- --tm <- liftBase getTypeMap+ --tm <- liftCont getTypeMap --let tyTm = lookupTypeOfT (clsTypeToType tyT) tm --debugTc $ "TypeMap: " ++ show (Map.keys $ constrs tyTm) -- END DEBUG (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genCti) <- lookupConstr tyT tysArgs- tArgs <- liftBase $ mapM evalSrcTypeArg tas- -- tm <- liftBase getTypeMap+ tArgs <- liftCont $ mapM evalSrcTypeArg tas+ -- tm <- liftCont getTypeMap let cti = instantiate (zip tps tArgs) genCti- let (CTI psPars pW lExp lMods exns) = cti+ let (CSig psPars pW lExp lMods exns) = cti -- Check lockstates l <- getCurrentLockState@@ -176,37 +176,79 @@ pRep <- tcPolicyExp pl return (policyPolT pRep, bottom) ---tcExp (PostIncrement e) = error "tcExp: PostIncrement"+tcExp (PostIncrement e) = do+ (tyE, pE) <- tcExp e+ check (isNumConvertible tyE) $ + "Post-increment operator used at non-numeric type " ++ prettyPrint tyE+ return (tyE, pE)+tcExp (PostDecrement e) = do+ (tyE, pE) <- tcExp e+ check (isNumConvertible tyE) $ + "Post-decrement operator used at non-numeric type " ++ prettyPrint tyE+ return (tyE, pE)+tcExp (PreIncrement e) = do+ (tyE, pE) <- tcExp e+ check (isNumConvertible tyE) $ + "Pre-increment operator used at non-numeric type " ++ prettyPrint tyE+ return (tyE, pE)+tcExp (PreDecrement e) = do+ (tyE, pE) <- tcExp e+ check (isNumConvertible tyE) $ + "Pre-decrement operator used at non-numeric type " ++ prettyPrint tyE+ return (tyE, pE) +-- Unary promotion prefix operator++-- Rule PREP+tcExp (PrePlus e) = do+ (tyE, pE) <- tcExp e+ check (isNumConvertible tyE) $+ "Pre-plus operator used at non-numeric type " ++ prettyPrint tyE+ + return (unaryNumPromote_ tyE, pE)+ tcExp (PreMinus e) = do (tyE, pE) <- tcExp e- check (tyE <: intT) $ "Wrong use of unary minus"- return (tyE, pE)+ check (isNumConvertible tyE) $+ "Pre-minus operator used at non-numeric type " ++ prettyPrint tyE+ return (unaryNumPromote_ tyE, pE) +tcExp (PreBitCompl e) = do+ (tyE, pE) <- tcExp e+ check (isIntConvertible tyE) $+ "Pre-complement bit operator used at non-integral type " ++ prettyPrint tyE+ return (unaryNumPromote_ tyE, pE) +tcExp (PreNot e) = do+ (tyE, pE) <- tcExp e+ check (isBoolConvertible tyE) $+ "Pre-complement boolean operator used at non-boolean type " ++ prettyPrint tyE+ return (booleanT, pE)++ tcExp (Cast t e) = do (tyE, pE) <- tcExp e- tyC <- liftBase $ evalSrcType t+ tyC <- liftCont $ evalSrcType t check (tyE <: tyC) $ "Wrong type at cast" return (tyC, pE) tcExp (FieldAccess fa) = tcFieldAccess fa -tcExp e = fail $ "tcExp: Unsupported expression: " ++ show e+tcExp e = fail $ "tcExp: Unsupported expression: " ++ prettyPrint e -------------------------- -- Field Access -tcFieldAccess :: FieldAccess -> Tc (TcType, TcPolicy)+tcFieldAccess :: FieldAccess -> Tc r (TcType, TcPolicy) tcFieldAccess (PrimaryFieldAccess e fi) = do (tyE,pE) <- tcExp e- VTI tyF pFi _ _ <- lookupFieldT tyE fi+ VSig tyF pFi _ _ <- lookupFieldT tyE fi return (tyF, pE `join` pFi) -------------------------- -- Method invocations -tcMethodInv :: MethodInvocation -> Tc (TcType, TcPolicy)+tcMethodInv :: MethodInvocation -> Tc r (TcType, TcPolicy) tcMethodInv mi = do --debugTc $ "tcMethodInv: " ++ show mi (mti, psArgs, pE) <- @@ -219,12 +261,12 @@ (tyE, pE) <- tcExp e (tysArgs, psArgs) <- unzip <$> mapM tcExp args (tps,genMti) <- lookupMethodT tyE i tysArgs- tArgs <- liftBase $ mapM (evalSrcTypeArg . ActualArg) tas--- tm <- liftBase getTypeMap+ tArgs <- liftCont $ mapM (evalSrcTypeArg . ActualArg) tas+-- tm <- liftCont getTypeMap let mti = instantiate (zip tps tArgs) genMti return (mti, psArgs, pE) _ -> fail $ "tcMethodInv: Unsupported method call"- let (MTI tyR pR psPars pW lExp lMods exns) = mti+ let (MSig tyR pR psPars pW lExp lMods exns) = mti -- Check lockstates l <- getCurrentLockState@@ -253,7 +295,7 @@ -- Policy expressions -- Treat them as pure compile-time for now -tcPolicyExp :: PolicyExp -> Tc TcPolicy+tcPolicyExp :: PolicyExp -> Tc r TcPolicy tcPolicyExp (PolicyLit cs) = do tcCs <- mapM tcClause cs return $ TcPolicy tcCs@@ -264,24 +306,24 @@ _ <- lookupVar (Name [i]) return $ TcRigidVar i -tcClause :: Clause Actor -> Tc (TcClause TcActor)+tcClause :: Clause Actor -> Tc r (TcClause TcActor) tcClause (Clause h ats) = do tcH <- tcActor h tcAs <- mapM tcAtom ats return (TcClause tcH tcAs) -tcAtom :: Atom -> Tc TcAtom+tcAtom :: Atom -> Tc r TcAtom tcAtom (Atom n as) = do ar <- lookupLockArity n check (length as == ar) $ "Arity mismatch in policy" tcAs <- mapM tcActor as return (TcAtom n tcAs) -tcActor :: Actor -> Tc TcActor+tcActor :: Actor -> Tc r TcActor tcActor (Var i) = return $ TcVar i tcActor (Actor n) = TcActor <$> tcActorName n -tcActorName :: ActorName -> Tc ActorId+tcActorName :: ActorName -> Tc r ActorId tcActorName (ActorName n) = getActorId n tcActorName (ActorTypeVar i) = return $ ActorTPVar i @@ -289,49 +331,77 @@ -- Types of operators -- ----------------------------------- -opType :: Op -> TcType -> TcType -> Tc TcType-opType Add t1 t2 =- case (t1, t2) of- (TcPolicyPolT p1, TcPolicyPolT p2) -> return (TcPolicyPolT (p1 `meet` p2))- (TcPrimT IntT, TcPrimT IntT) -> return t1- _ -> fail "Operator applied at wrong types"-opType Mult t1 t2 =- case (t1, t2) of- (TcPolicyPolT p1, TcPolicyPolT p2) -> return (TcPolicyPolT (p1 `join` p2))- (TcPrimT IntT, TcPrimT IntT) -> return t1- _ -> fail "Operator applied at wrong types"-opType Div t1 t2 =- case (t1, t2) of- (TcPrimT IntT, TcPrimT IntT) -> return t1- _ -> fail "Div applied at wrong types"-opType And t1 t2 =- case (t1, t2) of- (TcLockT ls1, TcLockT ls2) -> return (TcLockT (ls1 ++ ls2))- _ | t1 <: booleanT && t2 <: booleanT -> return booleanT- _ -> fail "Operator applied at wrong types"-opType op t1 t2 | op `elem` [Equal, NotEq, LThan, GThan, LThanE, GThanE] = do- case (t1,t2) of- (TcPrimT pt1, TcPrimT pt2) | pt1 == pt2 -> return ()- (t1, t2) - | isRefType t1 && t2 == nullT || isRefType t2 && t1 == nullT - -> return ()- _ -> fail "Operator NotEq applied at wrong types"- return booleanT-opType op _ _ = fail $ "opType: Operator not supported: " ++ show op+opType :: Op -> TcType -> TcType -> Tc r TcType+-- 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 == stringT || t2 == stringT = return stringT +opType op t1 t2+ -- Numeric operators+ | op `elem` [Mult, Div, Rem, Add, Sub] = do+ check (isNumConvertible t1) $+ "Numeric operator " ++ prettyPrint op ++ + " used with non-numeric operand of type " ++ prettyPrint t1+ check (isNumConvertible t2) $+ "Numeric operator " ++ prettyPrint op ++ + " used with non-numeric operand of type " ++ prettyPrint t2+ return $ binaryNumPromote_ t1 t2 + -- Shift operators+ | op `elem` [LShift, RShift, RRShift] = do+ check (isIntConvertible t1) $+ "Shift operator " ++ prettyPrint op +++ " used with non-integral operand of type " ++ prettyPrint t1+ check (isIntConvertible t2) $+ "Shift operator " ++ prettyPrint op +++ " used with non-integral operand of type " ++ prettyPrint t2+ return $ unaryNumPromote_ t1 + -- Relational operators+ | op `elem` [LThan, GThan, LThanE, GThanE] = do+ check (isNumConvertible t1) $+ "Numerical comparison operator " ++ prettyPrint op ++ + " used with non-numeric operand of type " ++ prettyPrint t1+ check (isNumConvertible t2) $+ "Numerical comparison operator " ++ prettyPrint op ++ + " used with non-numeric operand of type " ++ prettyPrint t2+ return booleanT -(<:) :: TcType -> TcType -> Bool-t1 <: t2 - | t1 == t2 = True- | t1 == nullT && isRefType t2 = True- | isLockType t1 && t2 == booleanT = True- -- Should surely be more cases here- | isPolicyType t1 && t2 == policyT = True- -- When we add proper subtyping, it must also be in Tc- | otherwise = False+ | op `elem` [Equal, NotEq] = do+ case binaryNumPromote t1 t2 of+ Just _ -> return ()+ _ | isBoolConvertible t1 && isBoolConvertible t2 -> return ()+ | isRefType t1 && isRefType t2 -> return ()+ _ -> fail $ "Equality operator " ++ prettyPrint op +++ " used with incomparable operands of types " +++ prettyPrint t1 ++ " and " ++ prettyPrint t2+ return booleanT + | op `elem` [And, Or, Xor] =+ if isBoolConvertible t1 + then do+ check (isBoolConvertible t2) $ + "Logical operator " ++ prettyPrint op +++ " used with non-boolean operand of type " ++ prettyPrint t2+ return booleanT+ else if isIntConvertible t1+ then do+ check (isIntConvertible t2) $+ "Bitwise operator " ++ prettyPrint op +++ " used with non-integral operand of type " ++ prettyPrint t2+ return $ binaryNumPromote_ t1 t2+ else fail $ "Bitwise/logical operator " ++ prettyPrint op +++ " used with non-integral and non-boolean operand of type " +++ prettyPrint t1+ | op `elem` [CAnd, COr] = do+ check (isBoolConvertible t1) $+ "Logical operator " ++ prettyPrint op +++ " used with non-boolean operand of type " ++ prettyPrint t1+ check (isBoolConvertible t2) $+ "Logical operator " ++ prettyPrint op +++ " used with non-boolean operand of type " ++ prettyPrint t2+ return booleanT splitName :: Name -> (Maybe Name, Name)
src/Language/Java/Paragon/TypeCheck/TcStmt.hs view
@@ -21,7 +21,7 @@ -- Typechecking Statements -- ----------------------------------- -tcStmt :: Stmt -> Tc ()+tcStmt :: Stmt -> Tc r () -- Rule EMPTY tcStmt Empty = return ()@@ -103,7 +103,7 @@ tcStmt (Return (Just e)) = do (tyR, pR) <- getReturn (tyE, pE) <- tcExp e- check (tyE <: tyR) $ "Returned value has wrong type: " ++ show tyE+ check (tyE <: tyR) $ "Returned value has wrong type: " ++ prettyPrint tyE -- Check pE <=[L] pR l <- getCurrentLockState@@ -137,14 +137,14 @@ -- Rule TRYCATCH tcStmt (Try block [catch] Nothing) = do let Catch (FormalParam ms t isVar (VarId i)) cBlock = catch- tyP <- liftBase $ evalSrcType t+ tyP <- liftCont $ evalSrcType t -- TODO check tyP <: "Throwable"- pR <- liftBase $ getReadPolicy ms -- getParamPolicy i ms+ pR <- liftCont $ getReadPolicy ms -- getParamPolicy i ms pW <- newMetaPolVar -- \pi, where \pi is fresh addBranchPC (exnE tyP) bottom $ -- E' = E[branchPC{tyP +-> bottom}, registerExn tyP pR pW $ do -- exns{tyP +-> (pR, \pi)}] tcBlock block- extendVarEnv i (VTI tyP pR False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}]+ extendVarEnv i (VSig tyP pR False (isFinal ms)) $ do -- E* = E[vars{x +-> (tyP, pR)}] msX <- getExnState (ExnType tyP) maybeM msX $ mergeWithState -- S* = St <> St[exns](X)[state] tcBlock cBlock@@ -237,16 +237,16 @@ extendLockEnv [TcLock n aids] $ tcBlock block -tcStmt s = fail $ "Unsupported statement: " ++ show s+tcStmt s = fail $ "Unsupported statement: " ++ prettyPrint s ---------------------------------------- -- Typechecking Blocks and BlockStmts -- ---------------------------------------- -tcBlock :: Block -> Tc ()+tcBlock :: Block -> Tc r () tcBlock (Block bss) = tcBlockStmts bss -tcBlockStmts :: [BlockStmt] -> Tc ()+tcBlockStmts :: [BlockStmt] -> Tc r () -- Rule EMPTYBLOCK tcBlockStmts [] = return () @@ -256,31 +256,31 @@ -- Rule LOCALVARINIT tcBlockStmts (LocalVars ms t [VarDecl (VarId i) (Just (InitExp e))] : bss) = do (tyE, pE) <- tcExp e- tyV <- liftBase $ evalSrcType t- check (tyE <: tyV) $ "Type mismatch: " ++ show tyE ++ " <=> " ++ show tyV+ tyV <- liftCont $ evalSrcType t+ check (tyE <: tyV) $ "Type mismatch: " ++ prettyPrint tyE ++ " <=> " ++ prettyPrint tyV pV <- localVarPol ms tyV' <- case mActorId tyE of Nothing -> return tyV Just aid -> do newActorIdWith i aid return $ actorIdT aid- extendVarEnv i (VTI tyV' pV False (isFinal ms)) $ do+ extendVarEnv i (VSig tyV' pV False (isFinal ms)) $ do tcBlockStmts bss -- Rule LOCALVARDECL tcBlockStmts (LocalVars ms t [VarDecl (VarId i) Nothing] : bss) = do- tyV <- liftBase $ evalSrcType t+ tyV <- liftCont $ evalSrcType t pV <- localVarPol ms tyV' <- if tyV == actorT then actorIdT <$> newActorId i else return tyV- extendVarEnv i (VTI tyV' pV False (isFinal ms)) $ do+ extendVarEnv i (VSig tyV' pV False (isFinal ms)) $ do tcBlockStmts bss tcBlockStmts (b:bss) = fail $ "Unsupported block statement: " ++ prettyPrint b -localVarPol :: [Modifier] -> Tc TcPolicy+localVarPol :: [Modifier] -> Tc r TcPolicy localVarPol ms = case [ p | Reads p <- ms ] of [] -> return bottom --newMetaPolVar- [p] -> liftBase $ evalPolicy p+ [p] -> liftCont $ evalPolicy p
src/Language/Java/Paragon/TypeCheck/Types.hs view
@@ -17,35 +17,21 @@ import Data.Generics (Data(..),Typeable(..)) #endif --- | TcTypes must come in two varieties, depending--- on where in the pipeline they are used. data TcType = TcPrimT PrimType | TcRefT TcRefType | TcVoidT | TcActorIdT ActorId | TcPolicyPolT TcPolicy | TcLockT [TcLock] deriving (Eq, Ord, Show, Data, Typeable) --- | TcTypes used early in the pipe-line, before--- evaluation of actor ids and policies.--- type TcTypeExp = TcTypeRaw Exp Policy {- = Exp -} Lock---- | TcTypes used late in the pipe-line, after--- evaluation of actor ids and policies.--- type TcType = TcTypeRaw ActorId TcPolicy TcLock- data TcRefType = TcClsRefT TcClassType | TcArrayT TcType (Maybe TcPolicy) | TcTypeVar Ident deriving (Eq, Ord, Show, Data, Typeable) ---type TcRefType = TcRefTypeRaw ActorId TcPolicy TcLock- data TcClassType = TcClassT [(Ident, [TcTypeArg])] | TcNullT -- Ignore wildcards for now deriving (Eq, Ord, Show, Data, Typeable) ---type TcClassType = TcClassTypeRaw ActorId TcPolicy TcLock- data TcTypeArg = TcActualType TcRefType | TcActualPolicy TcPolicy@@ -154,6 +140,73 @@ isPolicyType = isJust . mPolicyPol +-------------------------------------------+-- Type operations++(<:) :: TcType -> TcType -> Bool+t1 <: t2 + | t1 == t2 = True+ | t1 == nullT && isRefType t2 = True+ | isLockType t1 && t2 == booleanT = True+ -- Should surely be more cases here+ | isPolicyType t1 && t2 == policyT = True+ -- When we add proper subtyping, it must also be in Tc+ | otherwise = False+++unboxConvert :: TcType -> Maybe PrimType+unboxConvert (TcPrimT t) = Just t+unboxConvert (TcRefT (TcClsRefT (TcClassT is))) =+ case map ((\(Ident x) -> x) . fst) is of+ ["java", "lang", "Boolean" ] -> Just BooleanT+ ["java", "lang", "Byte" ] -> Just ByteT+ ["java", "lang", "Character"] -> Just CharT+ ["java", "lang", "Short" ] -> Just ShortT+ ["java", "lang", "Integer" ] -> Just IntT+ ["java", "lang", "Long" ] -> Just LongT+ ["java", "lang", "Float" ] -> Just FloatT+ ["java", "lang", "Double" ] -> Just DoubleT+ _ -> Nothing++isNumConvertible :: TcType -> Bool+isNumConvertible t =+ case unboxConvert t of+ Just t | t `elem` [ByteT, ShortT, IntT, LongT, CharT, FloatT, DoubleT] -> True+ _ -> False++isIntConvertible :: TcType -> Bool+isIntConvertible t =+ case unboxConvert t of+ Just t | t `elem` [ByteT, ShortT, IntT, LongT, CharT] -> True+ _ -> False++isBoolConvertible :: TcType -> Bool+isBoolConvertible t = unboxConvert t == Just BooleanT++unaryNumPromote :: TcType -> Maybe PrimType+unaryNumPromote t =+ case unboxConvert t of+ Just t | t `elem` [ByteT, ShortT, IntT, CharT] -> Just IntT+ Just t | t `elem` [LongT, FloatT, DoubleT] -> Just t+ _ -> Nothing++unaryNumPromote_ :: TcType -> TcType+unaryNumPromote_ = TcPrimT . fromJust . unaryNumPromote++binaryNumPromote :: TcType -> TcType -> Maybe PrimType+binaryNumPromote t1 t2 = + case (unboxConvert t1, unboxConvert t2) of+ (Just tc1, Just tc2) -> Just $ + let tcs = [tc1, tc2]+ pts = [DoubleT, FloatT, LongT, IntT]+ in case break (`elem` tcs) pts of+ (_, []) -> IntT+ (_, t:_) -> t+ _ -> Nothing++binaryNumPromote_ :: TcType -> TcType -> TcType+binaryNumPromote_ t1 t2 = TcPrimT . fromJust $ binaryNumPromote t1 t2+ --------------------------------------------- -- Pretty printing @@ -227,3 +280,5 @@ ppArgs :: Pretty a => [a] -> Doc ppArgs = parens . hsep . punctuate comma . map pretty++