module Language.Java.Paragon.TypeCheck where import Language.Java.Paragon.Syntax import Language.Java.Paragon.Parser import Language.Java.Paragon.Pretty import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.Constraints import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.TcExp import Language.Java.Paragon.TypeCheck.TcStmt import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.TcEnv import Language.Java.Paragon.TypeCheck.TcState import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Uniq import Language.Java.Paragon.TypeCheck.Evaluate --import Language.Java.Paragon.TypeCheck.Interpreter import qualified Language.Java.Paragon.TypeCheck.Types as TP import System.FilePath import System.Environment import System.Directory import Control.Monad (when) import qualified Data.Map as Map import Data.Maybe import Data.List (partition, intersperse) import Control.Applicative ( (<$>) ) import Control.Arrow ( (***), first, second ) import Data.Generics.Uniplate.Data (transformBi) typeCheck :: DirectoryPath -> DirectoryPath -> CompilationUnit -> IO CompilationUnit typeCheck currentDir piDir ast@(CompilationUnit pkg imps [td]) = do let (skoTd, skoTy) = skolemTypeDecl td e <- runTcCont skoTy $ do withEnvFromImps piDir "" allImps $ do --debug "Import env setup" withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do --debug "TypeMap completed" tm <- getTypeMap --debug $ "TypeMap: " ++ show tm withExpandedNames skoTd $ \fullTd -> do --debug $ "Full AST:\n" ++ prettyPrint fullTd typeCheckTd fullTd -- debug $ "Type checking completed!" return (CompilationUnit pkg imps [fullTd]) case e of Left str -> fail str Right ast -> return ast where allImps = defaultImportDecls ++ imps withExpandedNames :: TypeDecl -> (TypeDecl -> TcCont r a) -> TcCont r a withExpandedNames td tcbaf = do tm <- getTypeMap --debug $ "TypeMap: " ++ show tm let mNames = buildExpansionMap tm fullTd = expandNames mNames td --debug $ "ExpansionMap: " ++ show mNames tcbaf fullTd -- Not writing signature, to avoid a CPP import of Data --expandNames :: Data a => Map Ident [Ident] -> a -> a expandNames mNames = transformBi expandN . transformBi expandCT where expandN :: Name -> Name expandN n@(Name is@(i:_)) = case Map.lookup i mNames of Just qi -> Name $ qi ++ is Nothing -> n expandN n = n expandCT :: ClassType -> ClassType expandCT ct@(ClassType ias@((i,as):_)) = case Map.lookup i mNames of Just qi -> ClassType $ (zip qi (repeat [])) ++ ias Nothing -> ct expandCT ct = ct buildExpansionMap :: TypeMap -> Map Ident [Ident] buildExpansionMap tm = let fs = Map.keys (fields tm) (ms, _) = unzip $ Map.keys (methods tm) ts = Map.keys (types tm) m1 = Map.fromList (zip (fs ++ ms ++ ts) (repeat [])) pts = Map.assocs (pkgsAndTypes tm) ptms = map (second buildExpansionMap) pts mps = map (\(i,mp) -> Map.map (i:) mp) ptms in foldl Map.union m1 mps ------------------------------------------------------------------ -- Implicitly imported core packages -- TODO: Not yet used. defaultImportDecls :: [ImportDecl] defaultImportDecls = [] {- defaultImportDecls = [ ImportDecl False (Name [Ident "paragon"]) True , ImportDecl False (Name [Ident "paragon", Ident "util"]) True , ImportDecl False (Name [Ident "paragon", Ident "io"]) True] -} thisPackage :: ImportDecl thisPackage = ImportDecl False (Name []) True ------------------------------------------------------------------ withEnvFromImps :: DirectoryPath -> String -> [ImportDecl] -> TcCont r a -> TcCont r a withEnvFromImps piDir thisStr is tcba = do --debug ("withEnvFromImpsies: " ++ show is) --withEnvFromImps dir thisStr (imp:is) = withFoldMap (withEnvFromImp piDir thisStr) is $ tcba -- withEnvFromImp dir thisStr imp . withEnvFromImps dir thisStr is withEnvFromImp :: DirectoryPath -> String -> ImportDecl -> TcCont r a -> TcCont r a -- import java.*; withEnvFromImp piDir thisStr imp@(ImportDecl False (Name pkgNames) True) tcba = do --debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames) let relative = pathOf pkgNames absoluteDir = piDir ++ pSep:relative ++ [pSep] names <- liftIO $ getDirectoryContents absoluteDir let classPathsAndNames = [ (absoluteDir ++ name, takeBaseName name) | name <- names , let (base, extn) = (takeBaseName name, takeExtension name) , extn == ".pi" , base /= thisStr ] withEnvFromPkg pkgNames classPathsAndNames $ tcba -- import java.TypeName; withEnvFromImp piDir _ imp@(ImportDecl False (Name clsPkgName) False) tcba = do --debug $ "Setting up single import of: " ++ show clsPkgName let relative = pathOf clsPkgName absoluteFile = piDir ++ pSep:relative ++ ".pi" (Ident className) = last clsPkgName pkgNames = init clsPkgName withEnvFromSingleClass pkgNames absoluteFile className $ tcba withEnvFromPkg :: [Ident] -> [(FilePath, String)] -> TcCont r a -> TcCont r a withEnvFromPkg [] [] tcba = tcba -- Hack for the "this" package withEnvFromPkg pkgPath [] tcba = do tm <- getTypeMap let pkgTm = tm { packages = Map.empty } withTypeMap clearToPkgs $ extendTypeMapP pkgPath pkgTm $ tcba withEnvFromPkg pkgPath ((fp,n):pns) tcba = withEnvFromClass fp n . withEnvFromPkg pkgPath pns $ tcba withEnvFromSingleClass :: [Ident] -> FilePath -> String -> TcCont r a -> TcCont r a withEnvFromSingleClass pkgPath fp n tcba = do withEnvFromClass fp n . withEnvFromPkg pkgPath [] $ tcba ------------------------------------------------------------------------- -- This is where the really fun stuff happens withEnvFromClass :: FilePath -> String -> TcCont r a -> TcCont r a withEnvFromClass fp className tcba = do --debug $ "Checking imported class: " ++ className ClassDecl ms id@(Ident cuName) tps _super _impls (ClassBody ds) <- getClass fp check (className == cuName) $ "File name " ++ className ++ " does not match class name " ++ cuName let mDs = map (\(MemberDecl d) -> d) ds fetchActors mDs $ -- actor ids, fetchPols mDs $ -- policies, fetchTMs mDs $ -- typemethod bodies, fetchSignatures mDs $ do -- and signatures of fields, methods, constructors and locks tm <- getTypeMap let typeTm = tm { packages = Map.empty, types = Map.empty } typeSig = TSig True (Final `elem` ms) [] [] typeTm -- TODO: Insert actual values withTypeMap clearToTypes $ extendTypeMapT (Ident cuName) tps typeSig $ do tm <- getTypeMap --debug $ "TypeMap after adding " ++ className ++ ":\n" ++ show tm tcba --------------------------------------------------------------------- -- Working with actors fetchActors :: [MemberDecl] -> TcCont r a -> TcCont r a fetchActors mDecls tcba = do --debug "fetchActors" let acts = [ (ms, vd) | FieldDecl ms (PrimType ActorT) vds <- mDecls , vd <- vds , Static `elem` ms -- Only statics exist ?? ] let (sfs,unstables) = partition (\(ms, _) -> Final `elem` ms) acts (spawns,stables) = partition (\(_,VarDecl _ init) -> init == Nothing) sfs withFoldMap spawnActor spawns $ withFoldMap aliasActor unstables $ withFoldMap evalActor stables $ do --debug "fetchActors complete" tcba 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 = 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 = VSig actorT p (Static `elem` ms) (Final `elem` ms) a <- aliasActorId withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcba evalActor (ms, VarDecl (VarId i) (Just (InitExp e))) tcba = do p <- getReadPolicy ms let vti = VSig actorT p (Static `elem` ms) (Final `elem` ms) a <- case e of ExpName n -> do tm <- getTypeMap case lookupNamed actors n tm of Just a -> return a Nothing -> aliasActorId --fail "Internal error: no such actor" _ -> aliasActorId withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcba -- end actors ---------------------------------------------------------------------- -- Working with policies 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 ] let pols = [ (i,init) | FieldDecl ms (PrimType PolicyT) vds <- mds, VarDecl (VarId i) (Just (InitExp init)) <- vds, Static `elem` ms, Final `elem` ms ] --debug $ "pols: " ++ show pols withFoldMap fetchPol pols $ tcba fetchPol :: (Ident, Exp) -> TcCont r a -> TcCont r a fetchPol (i,e) tcba = do p <- case e of ExpName n -> do tm <- getTypeMap case lookupNamed policies n tm of Just p -> return p Nothing -> fail "fetchPol: no such policy" PolicyExp pl -> evalPolicyExp pl withTypeMap (\tm -> tm { policies = Map.insert i p (policies tm) }) $ tcba -- end policies ------------------------------------------------------------ -- Working with typemethods 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, Typemethod `elem` ms ] withTypeMap (\tm -> let newTM = foldl (\mtm (i,pb) -> Map.insert i pb mtm) (typemethods tm) ipbs in tm { typemethods = newTM }) $ tcba where paramIdent :: FormalParam -> Ident paramIdent (FormalParam _ _ _ (VarId i)) = i -- end typemethods ------------------------------------------------------------ -- Working with locks fetchSignatures :: [MemberDecl] -> TcCont r a -> TcCont r a fetchSignatures memberDecls tcba = withFoldMap fetchSignature memberDecls $ tcba 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 = VSig tcty pol (Static `elem` ms) (Final `elem` ms) withTypeMap (\tm -> tm { fields = foldl (\m (VarDecl (VarId i) _) -> Map.insert i vti m) (fields tm) vds }) $ tcba MethodDecl ms tps retT i ps exns _ -> do withFoldMap withTypeParam tps $ do tcty <- evalReturnType retT (pTys, pPols) <- unzip <$> mapM paramInfo ps rPol <- getReturnPolicy ms pPols wPol <- getWritePolicy ms exs <- mapM eSpecToSig exns expects <- mapM evalLock $ concat [ l | Expects l <- ms ] closes <- mapM evalLock $ concat [ l | Closes l <- ms ] opens <- mapM evalLock $ concat [ l | Opens l <- ms ] let mti = MSig { mRetType = tcty, mRetPol = rPol, mPars = pPols, mWrites = wPol, mExpects = expects, mLMods = (closes, opens), mExns = exs } withTypeMap (\tm -> tm { methods = Map.insert (i, pTys) (tps,mti) (methods tm) }) $ tcba ConstructorDecl ms tps _ ps exns _ -> do withFoldMap withTypeParam tps $ do (pTys, pPols) <- unzip <$> mapM paramInfo ps wPol <- getWritePolicy ms exs <- mapM eSpecToSig exns expects <- mapM evalLock $ concat [ l | Expects l <- ms ] closes <- mapM evalLock $ concat [ l | Closes l <- ms ] opens <- mapM evalLock $ concat [ l | Opens l <- ms ] let cti = CSig { cPars = pPols, cWrites = wPol, cExpects = expects, cLMods = (closes, opens), cExns = exs } withTypeMap (\tm -> tm { constrs = Map.insert pTys (tps,cti) (constrs tm) }) $ tcba LockDecl ms i mps props -> do lPol <- getLockPolicy ms --debug $ "lPol: " ++ show lPol -- TODO: Store lock properties! let vti = VSig (lockT []) lPol True True arity = length mps withTypeMap (\tm -> tm { lockArities = Map.insert i arity (lockArities tm), fields = Map.insert i vti (fields tm) }) $ tcba where eSpecToSig :: ExceptionSpec -> TcCont r (TcType, ExnSig) eSpecToSig (ExceptionSpec ms eType) = do ty <- evalSrcType (RefType eType) -- should use evalSrcRefType rPol <- getReadPolicy ms wPol <- getWritePolicy ms opens <- mapM evalLock $ concat [ l | Opens l <- ms ] closes <- mapM evalLock $ concat [ l | Closes l <- ms ] let esig = ExnSig { exnReads = rPol, exnWrites = wPol, exnMods = (closes, opens) } return (ty, esig) paramInfo :: FormalParam -> TcCont r (TcType, TcPolicy) paramInfo (FormalParam ms ty _ (VarId i)) = do pPol <- getParamPolicy i ms pTy <- evalSrcType ty return (pTy, pPol) ------------------------------------------------------------------------------------- tdIdentStr :: TypeDecl -> String tdIdentStr (ClassTypeDecl (ClassDecl _ (Ident str) _ _ _ _)) = str tdIdentStr (InterfaceTypeDecl (InterfaceDecl _ (Ident str) _ _ _)) = str ------------------------------------------------------------------------------------- getClass :: String -> TcCont r ClassDecl getClass piPath = do fc <- liftIO $ readFile piPath let east = parser compilationUnit fc case east of Left errs -> fail $ show errs Right (CompilationUnit _ _ [(ClassTypeDecl cls)]) -> -- assume there is only one type in each pi file and that is a class return cls _ -> fail $ "\nThere should be only one class type per Pi file!\n" ++ show east ------------------------------------------------------------------------------------- -- [ d1 , d2 , x ] -> d1/d2/x , x can be folder or file (.class) pathOf :: [Ident] -> String pathOf = concat . intersperse [pSep] . map (\(Ident i) -> i) --pathOf ((Ident name1):idents) = foldl (\p (Ident str) -> p ++ [pathSeparator] -- ++ str ) name1 idents type DirectoryPath = String type ClassPath = String ------------------------------------------------------------------------------------- testImportDecl = ImportDecl False (Name [Ident "paragon",Ident "util"]) True pSep = pathSeparator ------------------------------------------------------------------------------------- -- Here goes TcTypeDecl.hs ------------------------------------------------------------------------------------- -- TODO: The module structure needs refactoring typeCheckTd :: TypeDecl -> TcCont r () typeCheckTd (ClassTypeDecl cd) = typeCheckCd cd typeCheckTd (InterfaceTypeDecl id) = typeCheckId id typeCheckId :: InterfaceDecl -> TcCont r () typeCheckId (InterfaceDecl ms i tps _supers (InterfaceBody memberDecls)) = do --debug "typeCheckId" withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do let staticWPol = top withThisType i tps $ do withFoldMap withTypeParam tps $ typeCheckActorFields memberDecls $ do --debug "typeCheckLockDecls start" typeCheckLockDecls memberDecls $ do --debug "typeCheckTypeMethods start" typeCheckTypeMethods memberDecls $ do --debug "typeCheckPolicyFields start" typeCheckPolicyFields memberDecls $ do --debug "typeCheckSignatures start" typeCheckSignatures memberDecls $ \constrWPol -> do --debug "typeCheckMemberDecls start" typeCheckMemberDecls staticWPol constrWPol memberDecls typeCheckCd :: ClassDecl -> TcCont r () typeCheckCd (ClassDecl ms i tps _super _impls (ClassBody decls)) = do --debug "typeCheckCd" withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do staticWPol <- getWritePolicy ms let memberDecls = map testIt decls withThisType i tps $ do withFoldMap withTypeParam tps $ typeCheckActorFields memberDecls $ do --debug "typeCheckLockDecls start" typeCheckLockDecls memberDecls $ do --debug "typeCheckTypeMethods start" typeCheckTypeMethods memberDecls $ do --debug "typeCheckPolicyFields start" typeCheckPolicyFields memberDecls $ do --debug "typeCheckSignatures start" typeCheckSignatures memberDecls $ \constrWPol -> do withThisTypeSigs i tps $ do --debug "typeCheckMemberDecls start" typeCheckMemberDecls staticWPol constrWPol memberDecls testIt :: Decl -> MemberDecl testIt (MemberDecl d) = d testIt d = error $ "Not member decl: " ++ prettyPrint d 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 let thisSig = TSig True False [] [] emptyTM in tm { types = Map.insert i (tps,thisSig) (types tm) } 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 } thisSig = TSig True False [] [] thisTm -- TODO: Include proper values extendTypeMapT i tps thisSig $ tcba withTypeParam :: TypeParam -> TcCont r a -> TcCont r a withTypeParam tp tcba = case tp of ActorParam i -> do 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 = 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 = VSig (lockT []) top False True withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) $ tcba TypeParam i _ -> do --withTypeMap (\tm -> -- tm { types = Map.insert i ([],Map.empty) (types tm) }) $ tcba --------------------------------------------------------------- -- Actors -- 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] -> TcCont r a -> TcCont r a typeCheckActorFields = fetchActors {- let acts = [ (ms, vd) | FieldDecl ms (PrimType ActorT) vds <- mDecls , vd <- vds , Static `elem` ms -- Only statics exist ?? ] -} --------------------------------------------------------------- -- Locks typeCheckLockDecls :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckLockDecls mds tcba = do let ls = [ ld | ld@ LockDecl {} <- mds ] withFoldMap typeCheckLockDecl ls $ tcba typeCheckLockDecl :: MemberDecl -> TcCont r a -> TcCont r a typeCheckLockDecl (LockDecl ms i mps props) tcba = do -- lPol <- getLockPolicy ms -- TODO: Store lock properties! let arity = length mps withTypeMap (\tm -> tm { lockArities = Map.insert i arity (lockArities tm) }) $ tcba -- end Locks --------------------------------------------------------------- -- Typemethods typeCheckTypeMethods :: [MemberDecl] -> TcCont r a -> TcCont r a typeCheckTypeMethods mds tcba = do let tms = [ tmd | tmd@(MethodDecl ms _ _ _ _ _ _) <- mds, Typemethod `elem` ms ] withFoldMap typeCheckTMSig tms $ do st <- setupStartState mapM_ (typeCheckMethodDecl st) tms withFoldMap addTMBody tms $ tcba -- Precondition: only applied on actual typemethods 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 -- 1. No type parameters check (null tps) $ "No type parameters allowed on typemethod methods" -- 2. No interaction with policies or lock states check (all (\m -> not (isPolicyMod m || isLockStateMod m)) ms) $ "Methods annotated with typemethod cannot have policy or lock state modifiers" -- 3. Same check for parameters let pms = [ m | FormalParam pms _ _ _ <- ps, m <- pms, isPolicyMod m, isLockStateMod m ] check (null pms) $ "Parameters to typemethods must not have policy modifiers" -- 4. No exceptions may be thrown check (null exns) $ "Methods annotated with typemethod may not throw exceptions" tyPs <- mapM evalSrcType [ t | FormalParam _ t _ _ <- ps ] rTy <- evalReturnType retT let mti = MSig { mRetType = rTy, mRetPol = bottom, mWrites = top, mPars = [ bottom | _ <- ps ], mExpects = [], mLMods = noMods, mExns = [] } return (tyPs, mti) withTypeMap (\tm -> tm { methods = Map.insert (i,tyPs) ([],mti) (methods tm) }) $ tcba 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) } -- end Typemethods ------------------------------------------------------------------------------------- -- Policies 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 -> TcCont r a -> TcCont r a typeCheckPolicyField fd@(FieldDecl ms t vds) tcba = do --debug "typeCheckPolicyField" -- 0. Flatten let pols = [ (i, init) | VarDecl (VarId i) init <- vds ] vti <- withErrCtxt ("When checking policy fields " ++ concat (intersperse ", " (map (prettyPrint . fst) pols)) ++ ":\n") $ do -- 1. Check that initializer exists check (all ((/= Nothing) . snd) pols) $ "typeCheckPolicyField: Uninitialized policy" -- 2. Check that policy is bottom check (null [ () | Reads _ <- ms ]) $ "typeCheckPolicyField: Policy must have policy bottom" -- 3. Add signature to environment tcty <- evalSrcType t return $ VSig { varType = tcty, varPol = bottom, varStatic = Static `elem` ms, varFinal = Final `elem` ms } withFoldMap (addField vti) (map fst pols) $ do -- 4. Typecheck the field normally st <- setupStartState typeCheckFieldDecl top top st fd -- 5. Evaluate the initializers withFoldMap evalAddInit (map (second fromJust) pols) $ tcba where 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) -> TcCont r a -> TcCont r a evalAddInit (i, InitExp eInit) tcba = do --debug $ "evalAddInit: " ++ show i tcPol <- withErrCtxt ("When evaluating the initializer of field " ++ prettyPrint i ++ ":\n") $ evaluate eInit withTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $ tcba -- end policies ------------------------------------------------------------------------------ -- Signatures typeCheckSignatures :: [MemberDecl] -> (TcPolicy -> TcCont r a) -> TcCont r a typeCheckSignatures mds tcbaf = do st <- setupStartState withFoldMap (typeCheckSignature st) mds $ getConstrPol >>= tcbaf 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 -> TcCont r a -> TcCont r a -- Fields typeCheckSignature st fd@(FieldDecl ms t vds) tcba | t /= PrimType PolicyT && t /= PrimType ActorT = do --debug $ "typeCheckSignature: " ++ prettyPrint fd let fis = [ i | VarDecl (VarId i) _ <- vds ] vti <- withErrCtxt ("When checking signature for fields " ++ concat (intersperse ", " (map prettyPrint fis)) ++ ":\n") $ do -- 1. Check field type ty <- evalSrcType t _ <- lookupTypeOfT ty <$> getTypeMap -- TODO -- 2. Typecheck and evaluate field policy let rPolExps = [ e | Reads e <- ms ] check (length rPolExps <= 1) $ "typeCheckSignature: At most one read modifier allowed per field" mapM_ (typeCheckPolicyMod st) rPolExps rPol <- getReadPolicy ms -- 3. Add signature to typemap return $ VSig { varType = ty, varPol = rPol, varStatic = Static `elem` ms, varFinal = Final `elem` ms } withFoldMap (addField vti) vds $ tcba 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) } -- Methods typeCheckSignature st md@(MethodDecl ms tps retT i ps exns mb) tcba | not (Typemethod `elem` ms) = do --debug $ "typeCheckSignature: " ++ prettyPrint (MethodDecl ms tps retT i ps exns (MethodBody Nothing)) (pTs, mti) <- withErrCtxt ("When checking signature of method " ++ prettyPrint i ++ "(" ++ concat (intersperse ", " [prettyPrint t | FormalParam _ t _ _ <- ps ]) ++ "):\n") $ do -- 0. Setup type params withFoldMap withTypeParam tps $ do -- 1. Check return type ty <- evalReturnType retT when (isClassType ty) (do TypeMap {} <- lookupTypeOfT ty <$> getTypeMap return ()) --debug $ " type = " ++ show ty -- 2. Typecheck and evaluate policy modifiers withFoldMap withParam ps $ checkPolicyMods st ms "typeCheckSignature: At most one return/write modifier allowed per method" -- 3. Typecheck and evaluate lock modifiers lms <- checkLMMods ms es <- checkExpectsMods ms -- 4. Check parameter types and policy modifiers (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps -- 5. Typecheck and evaluate exception signatures xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns -- 6. Add signature to typemap rPol <- getReturnPolicy ms pPols wPol <- getWritePolicy ms let mti = MSig { mRetType = ty, mRetPol = rPol, mWrites = wPol, mPars = pPols, mExpects = es, mLMods = lms, mExns = xSigs } return (pTs, mti) withTypeMap (\tm -> tm { methods = Map.insert (i,pTs) (tps,mti) (methods tm) }) $ tcba -- Constructors typeCheckSignature st (ConstructorDecl ms tps i ps exns mb) tcba = do (pTs, cti) <- withErrCtxt ("When checking signature of constructor " ++ prettyPrint i ++ "(" ++ concat (intersperse ", " [prettyPrint t | FormalParam _ t _ _ <- ps ]) ++ "):\n") $ do -- 0. Setup type parameters withFoldMap withTypeParam tps $ do -- 1. Typecheck and evaluate policy modifiers withFoldMap withParam ps $ checkPolicyMods st ms "typeCheckSignature: At most one return/write modifier allowed per constructor" -- 2. Typecheck and evaluate lock modifiers lms <- checkLMMods ms es <- checkExpectsMods ms -- 3. Check parameter types and policy modifiers (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps -- 4. Typecheck and evaluate exception signatures xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns -- 5. Add signature to typemap wPol <- getWritePolicy ms let cti = CSig { cWrites = wPol, cPars = pPols, cExpects = es, cLMods = lms, cExns = xSigs } return (pTs, cti) withTypeMap (\tm -> tm { constrs = Map.insert pTs (tps,cti) (constrs tm) }) $ tcba -- Locks typeCheckSignature st ld@(LockDecl ms i mps mprops) tcba = do --debug $ "typeCheckSignature: " ++ prettyPrint ld vti <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do pol <- getLockPolicy ms return $ VSig (lockT []) pol True True withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) $ tcba typeCheckSignature _ _ tcba = tcba withParam :: FormalParam -> TcCont r a -> TcCont r a withParam (FormalParam _ _ _ (VarId i)) = withTypeMap $ \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 -> 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 -- Check that type exists TypeMap {} <- lookupTypeOfT ty <$> getTypeMap checkPolicyMods st ms "typeCheckSignature: At most one read/write modifier allowed per exception" rPol <- getReadPolicy ms wPol <- getWritePolicy ms lms <- checkLMMods ms let xSig = ExnSig { exnReads = rPol, exnWrites = wPol, exnMods = lms } return (ty, xSig) checkPolicyMods :: TcState -> [Modifier] -> String -> TcCont r () checkPolicyMods st ms failStr = do --debug $ "checkPolicyMods: " ++ show ms let rPolExps = [ e | Reads e <- ms ] wPolExps = [ e | Writes e <- ms ] check (length rPolExps <= 1 && length wPolExps <= 1) failStr mapM_ (typeCheckPolicyMod st) $ rPolExps ++ wPolExps checkLMMods :: [Modifier] -> TcCont r LockMods checkLMMods ms = do let cs = concat [ l | Closes l <- ms ] os = concat [ l | Opens l <- ms ] tcCs <- mapM evalLock cs tcOs <- mapM evalLock os return (tcCs, tcOs) checkExpectsMods :: [Modifier] -> TcCont r [TcLock] checkExpectsMods ms = do let es = concat [ l | Expects l <- ms ] mapM evalLock es 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 ty <- evalSrcType t -- 2. Typecheck and evaluate policy modifier checkPolicyMods st ms "typeCheckSignature: At most one read modifier allowed per parameter" rPol <- getParamPolicy i ms return (ty, rPol) typeCheckPolicyMod :: TcState -> Policy -> TcCont r () typeCheckPolicyMod st polExp = do --debug $ "typeCheckPolicyMod " ++ show polExp ((ty, _pol), cs) <- runTc (simpleEnv top) st (--liftBase (debug "inside runTC") >> tcExp polExp) check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?" checkM (ty <: policyT) $ "Wrong type for policy expression: " ++ prettyPrint ty -- check that _pol is bottom shouldn't be necessary -- end signatures ------------------------------------------------------------------------------ -- Bodies typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl] -> TcCont r () typeCheckMemberDecls sLim cLim ms = do st <- setupStartState mapM_ (typeCheckMemberDecl sLim cLim st) ms typeCheckMemberDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcCont r () typeCheckMemberDecl sLim cLim st fd@(FieldDecl {}) = typeCheckFieldDecl sLim cLim st fd typeCheckMemberDecl _ _ st md@(MethodDecl {}) = typeCheckMethodDecl st md typeCheckMemberDecl _ _ st cd@(ConstructorDecl {}) = typeCheckConstrDecl st cd typeCheckMemberDecl _ _ _ _ = return () 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 -> 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 (VSig matchTy matchPol _ _) <- Map.lookup i . fields <$> getTypeMap case mInit of Nothing -> return () Just (InitExp e) -> do (_,cs) <- runTc (simpleEnv lim) st $ do (ty, pol) <- tcExp e checkM (liftCont $ ty <: matchTy) $ "typeCheckVarDecl: type mismatch" constraint_ pol matchPol solve cs 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, 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, 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 exnLMods = map (second exnMods) xSigs parEnts = [ (VarEntity $ Name [i], bottom) | i <- pars ] exnEnts = [ (ExnEntity t, bottom) | t <- map fst xSigs ] branchMap = Map.insert returnE bottom $ Map.fromList (parEnts ++ exnEnts) env = TcEnv { vars = Map.fromList parVtis, lockstate = expLs, returnI = (tyRet, pRet), exnsE = Map.fromList exnPols, branchPCE = (branchMap, pWri) } --debug $ "Using env: " ++ show env -- Setup the state in which to check the body parAids <- concat <$> mapM aliasIfActor (zip pars tysPs) let parAMap = Map.fromList $ map ((Name . return) *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } -- This little thing is what actually checks the body (endSt,cs) <- runTc env parSt $ tcMethodBody mb >> getState -- ... and then we need to check the end result solve cs check (lMods `models` lockMods endSt) $ "Declared lock modifiers not general enough: " ++ show lMods mapM_ (checkExnMods endSt) exnLMods 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, 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, 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 exnLMods = map (second exnMods) xSigs parEnts = [ VarEntity $ Name [i] | i <- pars ] 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, VSig _ _ False _) <- Map.assocs (fields tm) ] --debug $ "fieEnts: " ++ show fieEnts let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat bottom) env = TcEnv { vars = Map.fromList parVtis, lockstate = expLs, returnI = error "Cannot return from constructor", exnsE = Map.fromList exnPols, branchPCE = (branchMap, pWri) } --debug $ "Using branch map: " ++ show (branchPCE env) -- Setup the state in which to check the body parAids <- concat <$> mapM aliasIfActor (zip pars tysPs) let parAMap = Map.fromList $ map ((Name . return) *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } -- This little thing is what actually checks the body (endSt,cs) <- runTc env parSt $ tcConstrBody cb >> getState -- ... and then we need to check the end result solve cs check (lMods `models` lockMods endSt) $ "Declared lock modifiers not general enough: " ++ show lMods mapM_ (checkExnMods endSt) exnLMods aliasIfActor :: (Ident, TcType) -> TcCont r [(Ident, ActorId)] aliasIfActor (i, ty) | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)] | otherwise = return [] checkExnMods :: TcState -> (TcType, LockMods) -> TcCont r () checkExnMods st (xTy, lms) = do let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st) maybeM mExnSt $ \sX -> do check (lms `models` lockMods sX) $ "Declared exception lock modifiers not general enough: " ++ show lms tcMethodBody :: MethodBody -> Tc r () tcMethodBody (MethodBody mBlock) = maybeM mBlock $ tcBlock tcConstrBody :: ConstructorBody -> Tc r () tcConstrBody (ConstructorBody Nothing stmts) = tcBlockStmts stmts ------------------------------------------ -- The stuff down here should likely live somewhere else skolemTypeDecl :: TypeDecl -> (TypeDecl, TcType) skolemTypeDecl td = case td of ClassTypeDecl (ClassDecl ms i tps sup impl cb) -> let (ty, subst) = skolemType i tps newCb = instantiate subst cb in (ClassTypeDecl $ ClassDecl ms i tps sup impl newCb, ty) InterfaceTypeDecl (InterfaceDecl ms i tps sups ib) -> let (ty, subst) = skolemType i tps newIb = instantiate subst ib in (InterfaceTypeDecl $ InterfaceDecl ms i tps sups newIb, ty) skolemType :: Ident -> [TypeParam] -> (TcType, [(TypeParam,TcTypeArg)]) skolemType i tps = let args = map skolemParam tps in (clsTypeWArg [(i, args)], zip tps args) skolemParam :: TypeParam -> TcTypeArg skolemParam tp = case tp of TypeParam i _ -> TcActualType (TcClsRefT (TcClassT [(i,[])])) ActorParam i -> TcActualActor (ActorTPVar i) PolicyParam i -> TcActualPolicy (TcRigidVar i) LockStateParam i -> TcActualLockState [TcLockVar i] isPolicyMod, isLockStateMod :: Modifier -> Bool isPolicyMod m = case m of Reads _ -> True Writes _ -> True _ -> False isLockStateMod m = case m of Expects _ -> True Opens _ -> True Closes _ -> True _ -> False debug :: String -> TcCont r () debug str = liftIO $ putStrLn $ "DEBUG: " ++ str