diff --git a/paragon.cabal b/paragon.cabal --- a/paragon.cabal +++ b/paragon.cabal @@ -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, diff --git a/src/Language/Java/Paragon/TypeCheck.hs b/src/Language/Java/Paragon/TypeCheck.hs --- a/src/Language/Java/Paragon/TypeCheck.hs +++ b/src/Language/Java/Paragon/TypeCheck.hs @@ -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 diff --git a/src/Language/Java/Paragon/TypeCheck/Constraints.hs b/src/Language/Java/Paragon/TypeCheck/Constraints.hs --- a/src/Language/Java/Paragon/TypeCheck/Constraints.hs +++ b/src/Language/Java/Paragon/TypeCheck/Constraints.hs @@ -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 diff --git a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs --- a/src/Language/Java/Paragon/TypeCheck/Evaluate.hs +++ b/src/Language/Java/Paragon/TypeCheck/Evaluate.hs @@ -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 diff --git a/src/Language/Java/Paragon/TypeCheck/Monad.hs b/src/Language/Java/Paragon/TypeCheck/Monad.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad.hs @@ -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 -} diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs new file mode 100644 --- /dev/null +++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcCont.hs @@ -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 diff --git a/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs b/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs --- a/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs +++ b/src/Language/Java/Paragon/TypeCheck/Monad/TcMonad.hs @@ -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])) diff --git a/src/Language/Java/Paragon/TypeCheck/TcEnv.hs b/src/Language/Java/Paragon/TypeCheck/TcEnv.hs --- a/src/Language/Java/Paragon/TypeCheck/TcEnv.hs +++ b/src/Language/Java/Paragon/TypeCheck/TcEnv.hs @@ -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" diff --git a/src/Language/Java/Paragon/TypeCheck/TcExp.hs b/src/Language/Java/Paragon/TypeCheck/TcExp.hs --- a/src/Language/Java/Paragon/TypeCheck/TcExp.hs +++ b/src/Language/Java/Paragon/TypeCheck/TcExp.hs @@ -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) diff --git a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs --- a/src/Language/Java/Paragon/TypeCheck/TcStmt.hs +++ b/src/Language/Java/Paragon/TypeCheck/TcStmt.hs @@ -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 diff --git a/src/Language/Java/Paragon/TypeCheck/Types.hs b/src/Language/Java/Paragon/TypeCheck/Types.hs --- a/src/Language/Java/Paragon/TypeCheck/Types.hs +++ b/src/Language/Java/Paragon/TypeCheck/Types.hs @@ -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 + +