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, foldM) 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 $ "\n\n" ++ 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 lsig = LSig lPol (length mps) -- let vti = VSig (lockT []) lPol True True -- arity = length mps withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks 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 = [ md | MemberDecl _ md <- decls ] inits = [ id | id@(InitDecl {}) <- 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 "typeCheckInitDecls start" typeCheckInitDecls staticWPol constrWPol inits --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) $ "At most one read modifier allowed per field" mapM_ (typeCheckPolicyMod st) rPolExps rPol <- getReadPolicy ms check (Final () `elem` ms || (not $ includesThis rPol)) $ "Non-final field may not reference " ++ prettyPrint thisP -- 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 (isRefType ty) $ do mTm <- lookupTypeOfT ty <$> getTypeMap case mTm of Just _ -> return () Nothing -> fail $ "Unknown type: " ++ prettyPrint 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 lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do pol <- getLockPolicy ms -- return $ VSig (lockT []) pol True True -- TODO: Check properties! return $ LSig pol (length mps) withTypeMap (\tm -> tm { locks = Map.insert i lsig (locks 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 " ++ prettyPrint i ++ " 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 mTm <- lookupTypeOfT ty <$> getTypeMap case mTm of Just _ -> return () Nothing -> fail $ "Unknown exception type: " ++ prettyPrint ty 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 -- tm <- getTypeMap -- debug $ show tm -- 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 ------------------------------------------------------------------------------ -- Initializers -- Precondition: Only init decls typeCheckInitDecls :: TcPolicy -> TcPolicy -> [Decl ()] -> TcCont r TcState typeCheckInitDecls sLim cLim is = do setupStartState >>= \st -> foldM (typeCheckInitDecl sLim) st [ bl | InitDecl _ True bl <- is ] >>= \st' -> foldM (typeCheckInitDecl cLim) st' [ bl | InitDecl _ False bl <- is ] typeCheckInitDecl :: TcPolicy -> TcState -> Block () -> TcCont r TcState typeCheckInitDecl lim st bl = do tm <- getTypeMap (st,cs) <- runTc (simpleEnv lim) st $ addBranchPCList (Map.keys (fields tm)) $ do tcBlock bl getState solve cs return st ------------------------------------------------------------------------------ -- 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 Just (InitArray _ arr) -> case mArrayType matchTy of Nothing -> fail $ "Field " ++ prettyPrint i ++ " of non-array type " ++ prettyPrint matchTy ++ " given literal array initializer" Just (baseTy, pols) -> do (_,cs) <- runTc (simpleEnv lim) st $ tcArrayInit baseTy pols arr solve cs -- _ -> error $ "typeCheckVarDecl: Array syntax not yet supported" 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 = Just (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