module Language.Java.Paragon.TypeCheck ( typeCheck, T ) where import Language.Java.Paragon.Syntax --import Language.Java.Paragon.Parser (parser, compilationUnit) import Language.Java.Paragon.Pretty import Language.Java.Paragon.Interaction import Language.Java.Paragon.TypeCheck.Actors import Language.Java.Paragon.TypeCheck.TcExp import Language.Java.Paragon.TypeCheck.TcStmt import Language.Java.Paragon.TypeCheck.Monad import Language.Java.Paragon.TypeCheck.Types import Language.Java.Paragon.TypeCheck.Locks import Language.Java.Paragon.TypeCheck.Policy import Language.Java.Paragon.TypeCheck.Evaluate import Language.Java.Paragon.TypeCheck.TypeMap --import System.FilePath --import System.Exit --import Control.Monad hiding (join) import qualified Data.Map as Map import Data.Maybe import Data.List (partition, intersperse) import Control.Applicative ( (<$>) ) import Control.Arrow ( (***), second ) -- import Data.Data () -- import Data.Generics.Uniplate.Data (transformBi) --typeCheck :: FilePath -> CompilationUnit () -> BaseM (CompilationUnit T) typeCheck :: PiPath -> TypeCheck BaseM CompilationUnit typeCheck piDirs (CompilationUnit _ pkg imps [td]) = do let (fullTd, skoTy) = skolemTypeDecl td runPiReader piDirs $ runTcDeclM skoTy $ do typedTd <- typeCheckTd fullTd return (CompilationUnit Nothing (fmap notAppl pkg) (map notAppl imps) [typedTd]) typeCheck _ _ = do fail $ "\n\n" ++ "Encountered multiple type declarations in the same file" ------------------------------------------------------------------------------------- -- Here goes TcTypeDecl.hs typeCheckTd :: TypeCheck TcDeclM TypeDecl typeCheckTd (ClassTypeDecl _ cdecl) = ClassTypeDecl Nothing <$> typeCheckCd cdecl typeCheckTd (InterfaceTypeDecl _ idecl) = InterfaceTypeDecl Nothing <$> typeCheckId idecl typeCheckId :: TypeCheck TcDeclM InterfaceDecl typeCheckId (InterfaceDecl _ _ms i tps supers (InterfaceBody _ memberDecls)) = do --debug "typeCheckId" withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do let staticWPol = top registerThisType i tps supers 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 registerThisTypeSigs i tps supers --debug "typeCheckMemberDecls start" InterfaceDecl Nothing (map notAppl _ms) (notAppl i) (map notAppl tps) (map notAppl supers) . InterfaceBody Nothing <$> typeCheckMemberDecls staticWPol constrWPol memberDecls typeCheckCd :: TypeCheck TcDeclM ClassDecl typeCheckCd (ClassDecl _ ms i tps mSuper _impls (ClassBody _ decls)) = do --debug "typeCheckCd" withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do staticWPol <- RealPolicy <$> getWritePolicy ms let memberDecls = [ mdecl | MemberDecl _ mdecl <- decls ] inits = [ idecl | idecl@(InitDecl {}) <- decls ] supers = maybe [] (:[]) mSuper withFoldMap withTypeParam tps $ do registerThisType i tps supers -- withFoldMap withSuperType (maybe [] (:[]) mSuper) $ do typeCheckActorFields memberDecls $ do debugPrint "typeCheckLockDecls start" typeCheckLockDecls memberDecls $ do debugPrint "typeCheckTypeMethods start" typeCheckTypeMethods memberDecls $ do debugPrint "typeCheckPolicyFields start" typeCheckPolicyFields memberDecls $ do debugPrint "typeCheckSignatures start" typeCheckSignatures memberDecls $ \constrWPol -> do registerThisTypeSigs i tps supers ClassDecl Nothing (map notAppl ms) (notAppl i) (map notAppl tps) (fmap notAppl mSuper) (map notAppl _impls) . ClassBody Nothing <$> do --debug "typeCheckInitDecls start" inits' <- typeCheckInitDecls staticWPol constrWPol inits --debug "typeCheckMemberDecls start" mDs' <- typeCheckMemberDecls staticWPol constrWPol memberDecls return (inits' ++ map (MemberDecl Nothing) mDs') typeCheckCd _ = panic (typeCheckerBase ++ ".typeCheckCd") "Enum decls not yet supported" registerThisType :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM () registerThisType i tps supers = do cTys <- mapM evalSrcClsType supers baseTm <- getTypeMap let superTMs = flip map cTys $ \cTy -> case lookupTypeOfT (clsTypeToType cTy) baseTm of Left mErr -> panic (typeCheckerBase ++ ".withSuperType") $ "Super type evaluated but now doesn't exist: " ++ show mErr Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty } extendGlobalTypeMap (\tm -> -- We insert an empty typemap at first, -- since we are only using this when checking signatures let thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) True False cTys [] emptyTM newTm = tm { types = Map.insert i (tps,[],thisSig) (types tm) } in foldl merge newTm superTMs) registerThisTypeSigs :: Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM () registerThisTypeSigs i tps supers = do cTys <- mapM evalSrcClsType supers baseTm <- getTypeMap let superTMs = flip map cTys $ \cTy -> case lookupTypeOfT (clsTypeToType cTy) baseTm of Left mErr -> panic (typeCheckerBase ++ ".withSuperType") $ "Super type evaluated but now doesn't exist: " ++ show mErr Right (_,superSig) -> (tMembers superSig) { constrs = Map.empty } let thisTm = baseTm { types = Map.empty, packages = Map.empty } resTm = foldl merge thisTm superTMs thisSig = TSig (TcClsRefT $ TcClassT (mkSimpleName TName i) []) True False cTys [] resTm -- TODO: Include proper values extendGlobalTypeMap (extendTypeMapT (Name () TName Nothing i) tps [] thisSig) --------------------------------------------------------------- -- 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 ()] -> TcDeclM a -> TcDeclM a typeCheckActorFields mDecls tcba = do --debug "fetchActors" let acts = [ (ms, vd) | FieldDecl _ ms (PrimType _ (ActorT _)) vds <- mDecls , vd <- vds -- Only final ones can be used in policies , Final () `elem` ms ] let -- (sfs,unstables) = partition (\(ms, _) -> Static () `elem` ms) acts (spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) acts -- sfs withFoldMap spawnActorVd spawns $ -- withFoldMap unknownActorVd unstables $ withFoldMap evalActorVd stables $ do --debug "fetchActors complete" tcba where spawnActorVd, evalActorVd -- , unknownActorVd :: ([Modifier ()],VarDecl ()) -> TcDeclM a -> TcDeclM a -- Only Nothing for initializer spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do a <- freshActorId (prettyPrint i) p <- getReadPolicy ms let vti = VSig actorT (RealPolicy p) False (Static () `elem` ms) (Final () `elem` ms) withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra spawnActorVd (_, VarDecl _ arvid _) _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid {- -- All non-final OR non-static unknownActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do p <- getReadPolicy ms let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms) a <- unknownActorId withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra unknownActorVd (_, VarDecl _ arvid _) _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -} -- Final, with explicit initializer evalActorVd (ms, VarDecl _ (VarId _ i) (Just (InitExp _ e))) tcra = do p <- getReadPolicy ms let vti = VSig actorT (RealPolicy p) False (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 -> unknownActorId --fail "Internal error: no such actor" _ -> unknownActorId withCurrentTypeMap (\tm -> tm { actors = Map.insert i a (actors tm), fields = Map.insert i vti (fields tm) }) $ tcra evalActorVd (_, VarDecl _ _ Nothing) _ = panic (typeCheckerBase ++ ".evalActorVd") $ "No initializer" evalActorVd (_, VarDecl _ arvid _) _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid -- end actors --------------------------------------------------------------- -- Locks typeCheckLockDecls :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckLockDecls mds tcba = do let ls = [ ld | ld@ LockDecl {} <- mds ] withFoldMap typeCheckLockDecl ls $ tcba typeCheckLockDecl :: MemberDecl () -> TcDeclM a -> TcDeclM a typeCheckLockDecl (LockDecl _ ms i mps mProps) tcba = do lsig <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do pol <- getLockPolicy ms prs <- evalSrcLockProps i mProps return $ LSig (RealPolicy pol) (length mps) prs withCurrentTypeMap (\tm -> tm { locks = Map.insert i lsig (locks tm) }) $ tcba --typeCheckLockDecl (LockDecl _ _ _ _ _) _ = fail $ "Lock properties not yet supported" typeCheckLockDecl md _ = panic (typeCheckerBase ++ ".typeCheckLockDecl") $ "Applied to non-lock decl " ++ show md -- end Locks --------------------------------------------------------------- -- Typemethods typeCheckTypeMethods :: [MemberDecl ()] -> TcDeclM a -> TcDeclM 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 () -> TcDeclM a -> TcDeclM a typeCheckTMSig (MethodDecl _ ms tps retT i ps exns _) tcba = do newMethMap <- 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 (pis, pmss) = unzip [ (pI, pms) | FormalParam _ pms _ _ (VarId _ pI) <- ps ] plms = [ m | m <- concat pmss, isPolicyMod m, isLockStateMod m ] check (null plms) $ "Parameters to typemethods must not have policy modifiers" -- 4. No exceptions may be thrown check (null exns) $ "Methods annotated with typemethod may not throw exceptions" tyPs <- mapM evalSrcType [ t | FormalParam _ _ t _ _ <- ps ] rTy <- evalReturnType retT let mti = MSig { mRetType = rTy, mRetPol = bottom, mWrites = top, mPars = pis, mParBounds = [ bottom | _ <- ps ], mExpects = [], mLMods = noMods, mExns = [] } isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b newMethMap = Map.singleton (tps, tyPs, isVarArity) mti return newMethMap withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $ tcba typeCheckTMSig md _ = panic (typeCheckerBase ++ ".typeCheckTMSig") $ "Applied to non-method decl " ++ show md addTMBody :: MemberDecl () -> TcDeclM a -> TcDeclM a addTMBody (MethodDecl _ _ _ _ i ps _ (MethodBody _ (Just bl))) = let pis = [ iP | FormalParam _ _ _ _ (VarId _ iP) <- ps ] in withCurrentTypeMap $ \tm -> tm { typemethods = Map.insert i (pis,bl) (typemethods tm) } addTMBody md = panic (typeCheckerBase ++ ".addTMBody") $ "Applied to non-method decl " ++ show md -- end Typemethods ------------------------------------------------------------------------------------- -- Policies typeCheckPolicyFields :: [MemberDecl ()] -> TcDeclM a -> TcDeclM 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 () -> TcDeclM a -> TcDeclM a typeCheckPolicyField fd@(FieldDecl _ ms t vds) tcba = do --debug "typeCheckPolicyField" -- 0. Flatten let pols = [ (i, initz) | VarDecl _ (VarId _ i) initz <- 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, varParam = False, 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 (evalAddPolicyInit st) (map (second fromJust) pols) $ tcba where addField :: VarFieldSig -> Ident () -> TcDeclM a -> TcDeclM a addField vti i = withCurrentTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) typeCheckPolicyField fd _ = panic (typeCheckerBase ++ ".typeCheckPolicyField") $ "Applied to non-policy decl " ++ show fd evalAddPolicyInit :: CodeState -> (Ident (), VarInit ()) -> TcDeclM a -> TcDeclM a evalAddPolicyInit st (i, InitExp _ eInit) tcba = do --debug $ "evalAddInit: " ++ show i tcPol <- withErrCtxt ("When evaluating the initializer of field " ++ prettyPrint i ++ ":\n") $ evaluate eInit ((tyInit, _pInit, _eInit'),_) <- runTcCodeM (simpleEnv top "policy initializer") st $ tcExp eInit check (isPolicyType tyInit) $ "Cannot initialize policy field " ++ prettyPrint i ++ " with non-policy expression " ++ prettyPrint eInit ++ " of type " ++ prettyPrint tyInit withCurrentTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $ tcba evalAddPolicyInit _ (i, arrInit) _ = fail $ "Cannot initialize policy field " ++ prettyPrint i ++ " with array " ++ prettyPrint arrInit -- end policies ------------------------------------------------------------------------------ -- Signatures typeCheckSignatures :: [MemberDecl ()] -> (ActorPolicy -> TcDeclM a) -> TcDeclM a typeCheckSignatures mds tcbaf = do st <- setupStartState withFoldMap (typeCheckSignature st) mds $ getConstrPol >>= tcbaf getConstrPol :: TcDeclM ActorPolicy getConstrPol = do mConstrs <- constrs <$> getTypeMap let wPols = map cWrites $ Map.elems mConstrs return $ foldl join bottom wPols typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM a -> TcDeclM a -- Fields typeCheckSignature st (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 debugPrint $ "Type evaluated to: " ++ show ty -- _ <- 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 :: PrgPolicy TcActor) -- 3. Add signature to typemap return $ VSig { varType = ty, varPol = RealPolicy rPol, varParam = False, varStatic = Static () `elem` ms, varFinal = Final () `elem` ms } withFoldMap (addField vti) vds $ tcba where addField :: VarFieldSig -> VarDecl () -> TcDeclM a -> TcDeclM a addField vti (VarDecl _ (VarId _ i) _) = withCurrentTypeMap $ \tm -> tm { fields = Map.insert i vti (fields tm) } addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd -- Methods typeCheckSignature st (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)) newMethMap <- 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 -- 2. Check parameter types and policy modifiers (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps let pInfos = zip3 ps pTs pPols -- 3. Typecheck and evaluate policy modifiers withFoldMap withParam pInfos $ checkPolicyMods st ms "typeCheckSignature: At most one return/write modifier allowed per method" -- 4. Typecheck and evaluate lock modifiers lms <- checkLMMods ms es <- checkExpectsMods ms -- 5. Typecheck and evaluate exception signatures xSigs <- withFoldMap withParam pInfos $ mapM (typeCheckExnSig st) exns -- 6. Add signature to typemap rPol <- getReturnPolicy ms pPols wPol <- getWritePolicy ms let mti = MSig { mRetType = ty, mRetPol = RealPolicy rPol, mWrites = RealPolicy wPol, mPars = pIs, mParBounds = map RealPolicy pPols, mExpects = es, mLMods = lms, mExns = xSigs } isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b return $ Map.singleton (tps, pTs, isVarArity) mti withCurrentTypeMap (\tm -> tm { methods = Map.insertWith Map.union i newMethMap (methods tm) }) $ tcba -- Constructors typeCheckSignature st (ConstructorDecl _ ms tps i ps exns _mb) tcba = do (pTs, isVA, 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. Check parameter types and policy modifiers (pTs,pIs,pPols) <- unzip3 <$> mapM (typeCheckParam st) ps let pInfos = zip3 ps pTs pPols -- 2. Typecheck and evaluate policy modifiers withFoldMap withParam pInfos $ checkPolicyMods st ms "typeCheckSignature: At most one return/write modifier allowed per constructor" -- 3. Typecheck and evaluate lock modifiers lms <- checkLMMods ms es <- checkExpectsMods ms -- 4. Typecheck and evaluate exception signatures xSigs <- withFoldMap withParam pInfos $ mapM (typeCheckExnSig st) exns -- 5. Add signature to typemap wPol <- getWritePolicy ms let cti = CSig { cWrites = RealPolicy wPol, cPars = pIs, cParBounds = map RealPolicy pPols, cExpects = es, cLMods = lms, cExns = xSigs } isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b return (pTs, isVarArity, cti) withCurrentTypeMap (\tm -> tm { constrs = Map.insert (tps, pTs, isVA) cti (constrs tm) }) $ tcba -- Locks -- already handled -- typeCheckSignature st ld@(LockDecl _ ms i mps mprops) tcba = tcba --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 (), TcType, PrgPolicy TcActor) -> TcDeclM a -> TcDeclM a withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do let vsig = VSig ty (RealPolicy p) True (Static () `elem` ms) (Final () `elem` ms) withCurrentTypeMap $ \tm -> tm { fields = Map.insert i vsig (fields tm) } withParam (FormalParam _ _ _ _ arvid, _, _) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM (TcType, ExnSig) typeCheckExnSig st (ExceptionSpec _ ms xT) = do withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do ty <- TcRefT <$> evalSrcRefType xT {-- Check that type exists - now done in evalSrcRefType 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 = RealPolicy rPol, exnWrites = RealPolicy wPol, exnMods = lms } return (ty, xSig) checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM () 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 ()] -> TcDeclM 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 ()] -> TcDeclM [TcLock] checkExpectsMods ms = do let es = concat [ l | Expects _ l <- ms ] mapM evalLock es typeCheckParam :: CodeState -> FormalParam () -> TcDeclM (TcType, Ident (), PrgPolicy TcActor) typeCheckParam st (FormalParam _ ms t ell (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 ms return (if ell then arrayType ty bottom else ty, i, rPol) typeCheckParam _ (FormalParam _ _ _ _ arvid) = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM (Policy T) typeCheckPolicyMod st polExp = do -- tm <- getTypeMap -- debug $ show tm -- debug $ "typeCheckPolicyMod " ++ show polExp ((ty, _pol, polExp'), cs) <- runTcCodeM (simpleEnv top $ "policy modifier " ++ prettyPrint polExp) st (--liftBase (debug "inside runTC") >> tcExp polExp) check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?" check (isPolicyType ty) $ "Wrong type for policy expression: " ++ prettyPrint ty -- check that _pol is bottom shouldn't be necessary return polExp' -- end signatures ------------------------------------------------------------------------------ -- Initializers -- Precondition: Only init decls typeCheckInitDecls :: ActorPolicy -> ActorPolicy -> [Decl ()] -> TcDeclM [Decl T] typeCheckInitDecls sLim cLim is = do stSt <- setupStartState (sIs, st) <- go (typeCheckInitDecl sLim) stSt [] [ bl | InitDecl _ True bl <- is ] (iIs, _ ) <- go (typeCheckInitDecl cLim) st [] [ bl | InitDecl _ False bl <- is ] return (map (InitDecl Nothing True) sIs ++ map (InitDecl Nothing False) iIs) where go :: (CodeState -> Block () -> TcDeclM (CodeState, Block T)) -> CodeState -> [Block T] -> [Block ()] -> TcDeclM ([Block T], CodeState) go _ st acc [] = return (reverse acc, st) go f st acc (bl:bls) = do (st', blT) <- f st bl go f st' (blT:acc) bls typeCheckInitDecl :: ActorPolicy -> CodeState -> Block () -> TcDeclM (CodeState, Block T) typeCheckInitDecl lim st bl = do tm <- getTypeMap (newSB,cs) <- runTcCodeM (simpleEnv lim $ "initializer block") st $ addBranchPCList (Map.keys (fields tm)) $ do bl' <- tcBlock bl s <- getState return (s, bl') solve cs return newSB ------------------------------------------------------------------------------ -- Bodies typeCheckMemberDecls :: ActorPolicy -> ActorPolicy -> [MemberDecl ()] -> TcDeclM [MemberDecl T] typeCheckMemberDecls sLim cLim ms = do st <- setupStartState mapM (typeCheckMemberDecl sLim cLim st) ms typeCheckMemberDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl 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 _ _ _ md = return $ notAppl md typeCheckFieldDecl :: ActorPolicy -> ActorPolicy -> CodeState -> TypeCheck TcDeclM MemberDecl typeCheckFieldDecl staticLim constrLim st (FieldDecl _ ms _t vds) = do --debug $ "typeCheckFieldDecl:" ++ show fd let lim = if Static () `elem` ms then staticLim else constrLim vds' <- mapM (typeCheckVarDecl lim st) vds return $ FieldDecl Nothing (map notAppl ms) (notAppl _t) vds' typeCheckFieldDecl _ _ _ md = panic (typeCheckerBase ++ ".typeCheckFieldDecl") $ "Applied to non-field decl " ++ show md typeCheckVarDecl :: ActorPolicy -> CodeState -> TypeCheck TcDeclM VarDecl typeCheckVarDecl lim st vd@(VarDecl _ (VarId _ i) mInit) = do --debug $ "typeCheckVarDecl:" ++ show i withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do Just (VSig fieldTy fieldPol _ _ _) <- Map.lookup i . fields <$> getTypeMap case mInit of Nothing -> return $ notAppl vd Just (InitExp _ e) -> do (e',cs) <- runTcCodeM (simpleEnv lim $ "field initializer " ++ prettyPrint e) st $ do (rhsTy, rhsPol, e') <- tcExp e checkM (fieldTy =<: rhsTy) $ "typeCheckVarDecl: type mismatch" constraint [] rhsPol fieldPol $ "Cannot assign result of expression " ++ prettyPrint e ++ " with policy " ++ prettyPrint rhsPol ++ " to location " ++ prettyPrint i ++ " with policy " ++ prettyPrint fieldPol return e' solve cs return $ VarDecl Nothing (VarId Nothing $ notAppl i) $ Just $ InitExp Nothing e' Just (InitArray _ arr) -> case mArrayType fieldTy of Nothing -> fail $ "Field " ++ prettyPrint i ++ " of non-array type " ++ prettyPrint fieldTy ++ " given literal array initializer" Just (baseTy, pols) -> do (arr',cs) <- runTcCodeM (simpleEnv lim $ "array initializer " ++ prettyPrint arr) st $ tcArrayInit baseTy pols arr solve cs return $ VarDecl Nothing (VarId Nothing $ notAppl i) $ Just $ InitArray Nothing arr' -- _ -> error $ "typeCheckVarDecl: Array syntax not yet supported" typeCheckVarDecl _ _ vd = fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd typeCheckMethodDecl :: CodeState -> TypeCheck TcDeclM MemberDecl typeCheckMethodDecl st (MethodDecl _ _ms tps _rt i ps _exs mb) = do -- Lookup the correct function signature debugPrint $ "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 ] let isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b Just (MSig tyRet pRet pIs pPars pWri expLs lMods xSigs) <- do mMap <- fromJust . Map.lookup i . methods <$> getTypeMap return $ Map.lookup (tps, tysPs, isVarArity) mMap -- Setup the environment in which to check the body let parMods = [ (iP, ms) | (FormalParam _ ms _ _ (VarId _ iP)) <- ps ] parVsigs = [ (iP, VSig t (ofPol iP) True False (isFinal ms)) | ((iP, ms), t) <- zip parMods tysPs ] pBs = zip pIs pPars pars = map fst parVsigs exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs exnLMods = map (second exnMods) xSigs parEnts = [ (VarEntity $ mkSimpleName EName iP, []) | iP <- pars ] exnEnts = [ (ExnEntity t, []) | t <- map fst xSigs ] branchMap = Map.insert returnE [] $ Map.fromList (parEnts ++ exnEnts) writeErr = "body of method " ++ prettyPrint i env = CodeEnv { vars = Map.fromList parVsigs, lockstate = expLs, returnI = Just (tyRet, pRet), exnsE = Map.fromList exnPols, branchPCE = (branchMap, [(pWri, writeErr)]), parBounds = pBs } -- debug $ "Using env: " ++ show env -- Setup the state in which to check the body parAids <- concat <$> mapM unknownIfActor (zip pars tysPs) let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } -- This little thing is what actually checks the body ((mb', endSt),cs) <- runTcCodeM env parSt $ do mb' <- tcMethodBody mb eSt <- getState return (mb', eSt) -- ... 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 return $ MethodDecl Nothing (map notAppl _ms) (map notAppl tps) (notAppl _rt) (notAppl i) (map notAppl ps) (map notAppl _exs) mb' typeCheckMethodDecl _ md = panic (typeCheckerBase ++ ".typeCheckMethodDecl") $ "Applied to non-method decl " ++ show md typeCheckConstrDecl :: CodeState -> TypeCheck TcDeclM MemberDecl typeCheckConstrDecl st (ConstructorDecl _ _ms tps ci ps _exs 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 ] let isVarArity = case reverse ps of [] -> False (FormalParam _ _ _ b _ : _) -> b Just (CSig _pIs pPars pWri expLs lMods xSigs) <- Map.lookup (tps, tysPs, isVarArity) . constrs <$> getTypeMap -- Setup the environment in which to check the body tm <- getTypeMap let parVsigs = [ (i, VSig t (ofPol i) True False (isFinal ms)) | (FormalParam _ ms _ _ (VarId _ i), t) <- zip ps tysPs ] pars = map fst parVsigs pBs = zip pars pPars exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs exnLMods = map (second exnMods) xSigs parEnts = [ VarEntity $ mkSimpleName EName 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 (mkSimpleName EName i)] | (i, VSig _ _ _ False _) <- Map.assocs (fields tm) ] --debug $ "fieEnts: " ++ show fieEnts let branchMap = Map.fromList $ zip (parEnts ++ exnEnts ++ fieEnts) (repeat []) writeErr = "body of constructor " ++ prettyPrint ci env = CodeEnv { vars = Map.fromList parVsigs, lockstate = expLs, returnI = error "Cannot return from constructor", exnsE = Map.fromList exnPols, branchPCE = (branchMap, [(pWri, writeErr)]), parBounds = pBs } --debug $ "Using branch map: " ++ show (branchPCE env) -- Setup the state in which to check the body parAids <- concat <$> mapM unknownIfActor (zip pars tysPs) let parAMap = Map.fromList $ map (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids parSt = st { actorSt = parAMap `Map.union` actorSt st } -- This little thing is what actually checks the body ((cb',endSt),cs) <- runTcCodeM env parSt $ do cb' <- tcConstrBody cb eSt <- getState return (cb', eSt) -- ... 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 return $ ConstructorDecl Nothing (map notAppl _ms) (map notAppl tps) (notAppl ci) (map notAppl ps) (map notAppl _exs) cb' typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $ "Applied to non-constructor decl " ++ show md unknownIfActor :: (Ident (), TcType) -> TcDeclM [(Ident (), ActorId)] unknownIfActor (i, ty) | ty == actorT = unknownActorId >>= \aid -> return [(i, aid)] | otherwise = return [] ofPol :: Ident () -> ActorPolicy ofPol = RealPolicy . TcRigidVar checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM () 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 {- getParamBound :: ActorPolicy -> PrgPolicy TcActor getParamBound (RealPolicy (TcRigidVar _)) = top getParamBound (RealPolicy p) = p getParamBound _ = top -} tcMethodBody :: TypeCheck (TcCodeM) MethodBody tcMethodBody (MethodBody _ mBlock) = MethodBody Nothing <$> maybe (return Nothing) ((Just <$>) . tcBlock) mBlock tcConstrBody :: TypeCheck (TcCodeM) ConstructorBody tcConstrBody (ConstructorBody _ mEci stmts) = do mEci' <- maybe (return Nothing) ((Just <$>) . tcEci) mEci stmts' <- tcBlockStmts stmts return $ ConstructorBody Nothing mEci' stmts' --tcConstrBody (ConstructorBody _ Just eci) _) = tc -- = fail $ "Explicit constructor invocation not yet supported: " ++ prettyPrint eci ------------------------------------------ -- The stuff down here should likely live somewhere else skolemTypeDecl :: TypeDecl () -> (TypeDecl (), TcClassType) 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) ClassTypeDecl _ (EnumDecl _ ms i impl eb) -> -- Cannot be parameterized let (ty, _subst) = skolemType i [] in (ClassTypeDecl () $ EnumDecl () ms i impl eb, 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 ()] -> (TcClassType, [(TypeParam (), TcTypeArg)]) skolemType i tps = let args = map skolemParam tps in (TcClassT (mkSimpleName TName i) args, zip tps args) skolemParam :: TypeParam () -> TcTypeArg skolemParam tp = case tp of TypeParam _ i _ -> TcActualType (TcClsRefT (TcClassT (mkSimpleName TName i) [])) ActorParam _ i -> TcActualActor (ActorTPVar i) PolicyParam _ i -> TcActualPolicy (RealPolicy $ 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