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 (when) import qualified Data.Map.Strict as Map import qualified Data.ByteString.Char8 as B 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 let mPkgPrefix = fmap (\(PackageDecl _ n) -> n) pkg typedTd <- typeCheckTd mPkgPrefix 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 :: Maybe (Name ()) -> TypeCheck TcDeclM TypeDecl typeCheckTd mpkg (ClassTypeDecl _ cdecl) = ClassTypeDecl Nothing <$> typeCheckCd mpkg cdecl typeCheckTd mpkg (InterfaceTypeDecl _ idecl) = InterfaceTypeDecl Nothing <$> typeCheckId mpkg idecl typeCheckId :: Maybe (Name ()) -> TypeCheck TcDeclM InterfaceDecl typeCheckId mpkg (InterfaceDecl _ _ms i tps supers (InterfaceBody _ memberDecls)) = do --debug "typeCheckId" withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do let staticWPol = top registerThisType mpkg i tps supers withFoldMap withTypeParam tps $ typeCheckActorFields memberDecls $ do --debug "typeCheckLockDecls start" typeCheckTMPolLocks memberDecls $ do {- typeCheckLockDecls memberDecls $ do --debug "typeCheckTypeMethods start" typeCheckTypeMethods memberDecls $ do --debug "typeCheckPolicyFields start" typeCheckPolicyFields memberDecls $ do -} --debug "typeCheckSignatures start" typeCheckSignatures memberDecls $ \constrWPol -> do registerThisTypeSigs mpkg 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 :: Maybe (Name ()) -> TypeCheck TcDeclM ClassDecl typeCheckCd mpkg (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 mpkg i tps supers -- withFoldMap withSuperType (maybe [] (:[]) mSuper) $ do typeCheckActorFields memberDecls $ do -- debugPrint "typeCheckLockDecls start" typeCheckTMPolLocks 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 mpkg 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 :: Maybe (Name ()) -> Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM () registerThisType pkgPre 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 } -- We insert an empty typemap at first, -- since we are only using this when checking signatures let iN = Name () TName Nothing i fullN = Name () TName pkgPre i thisTM = foldl merge emptyTM superTMs thisSig = TSig (TcClsRefT $ TcClassT fullN []) True False cTys [] thisTM --debugPrint $ "regThisType: " ++ show (methods thisTM) extendGlobalTypeMap (extendTypeMapT iN tps [] thisSig) when (not (pkgPre == Nothing)) $ extendGlobalTypeMap (extendTypeMapT fullN tps [] thisSig) registerThisTypeSigs :: Maybe (Name ()) -> Ident () -> [TypeParam ()] -> [ClassType ()] -> TcDeclM () registerThisTypeSigs pkgPre i tps supers = do cTys <- mapM evalSrcClsType supers baseTm <- getTypeMap -- debugPrint $ "Current typemap: " ++ show baseTm 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 iN = Name () TName Nothing i fullN = Name () TName pkgPre i thisTm = baseTm { types = Map.empty, packages = Map.empty } -- Should be identity transformation resTm = foldl merge thisTm superTMs thisSig = TSig (TcClsRefT $ TcClassT fullN []) True False cTys [] resTm -- TODO: Include proper values --debugPrint $ "regThisTypeSigs: " ++ show (methods resTm) extendGlobalTypeMap (merge resTm) extendGlobalTypeMap (extendTypeMapT iN tps [] thisSig) when (not (pkgPre == Nothing)) $ extendGlobalTypeMap (extendTypeMapT fullN 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 (unIdent i) a (actors tm), fields = Map.insert (unIdent 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 (unIdent i) a (actors tm), fields = Map.insert (unIdent 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 --------------------------------------------------------------- -- Policies, typemethods and locks typeCheckTMPolLocks :: [MemberDecl ()] -> TcDeclM a -> TcDeclM a typeCheckTMPolLocks = withFoldMap typeCheckTMPolLock typeCheckTMPolLock :: MemberDecl () -> TcDeclM a -> TcDeclM a typeCheckTMPolLock md@(LockDecl{}) tcba = typeCheckLockDecl md tcba typeCheckTMPolLock md@(MethodDecl _ ms _ _ _ _ _ _) tcba | Typemethod () `elem` ms = typeCheckTMSig md $ do st <- setupStartState _ <- typeCheckMethodDecl st md addTMBody md $ tcba typeCheckTMPolLock md@(FieldDecl _ ms (PrimType _ (PolicyT _)) _) tcba | Final () `elem` ms = typeCheckPolicyField md tcba typeCheckTMPolLock _ tcba = tcba --------------------------------------------------------------- -- 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 let rPolExps = [ e | Reads _ e <- ms ] check (length rPolExps <= 1) $ "At most one read modifier allowed per field" mapM_ (typeCheckPolicyMod emptyCodeState) rPolExps pol <- getLockPolicy ms prs <- evalSrcLockProps i mProps return $ LSig (RealPolicy pol) (length mps) prs withCurrentTypeMap (\tm -> tm { locks = Map.insert (unIdent 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 [ (unIdent 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 (unIdent 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 = [ unIdent iP | FormalParam _ _ _ _ (VarId _ iP) <- ps ] in withCurrentTypeMap $ \tm -> tm { typemethods = Map.insert (unIdent 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 _ ms (PrimType _ (PolicyT _)) _) <- mds, Final () `elem` ms ] 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 (unIdent 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 (unIdent 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)) $ prettyPrint (thisP :: PrgPolicy TcActor) ++ " may not be used as the policy of non-final fields" check (not $ typeIncludesThis ty) $ prettyPrint (thisP :: PrgPolicy TcActor) ++ " may not be used in the type arguments of a field type" -- 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 (unIdent i) vti (fields tm) } addField _ vd = \_ -> fail $ "Deprecated declaration: " ++ prettyPrint vd typeIncludesThis :: TcType -> Bool typeIncludesThis (TcRefT rt) = refTypeIncludesThis rt typeIncludesThis _ = False refTypeIncludesThis :: TcRefType -> Bool refTypeIncludesThis rTy = case rTy of TcArrayT arrTy arrPol -> typeIncludesThis arrTy || includesThis arrPol TcClsRefT (TcClassT _ targs) -> any argIncludesThis targs _ -> False argIncludesThis :: TcTypeArg -> Bool argIncludesThis targ = case targ of TcActualType rt -> refTypeIncludesThis rt TcActualPolicy p -> includesThis p _ -> False -- 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 -- IF GENERIC: map (TcRigidVar True) pIs wPol <- getWritePolicy ms --debugPrint $ "Method " ++ prettyPrint i ++ " has wPol: " ++ show wPol 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 (unIdent 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 (unIdent 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, B.ByteString, 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 (unIdent i) ms return (if ell then arrayType ty bottom else ty, unIdent 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 (Ident ()) (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 (unIdent 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 mps <- fieldTy =<: rhsTy case mps of Nothing -> fail $ "typeCheckVarDecl: type mismatch" Just ps -> do mapM_ (\(p,q) -> do constraint [] p q "Cannot unify policy type parameters at method call" constraint [] q p "Cannot unify policy type parameters at method call") ps 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 (MethodDecl () _ms tps _rt i ps _exs (MethodBody () Nothing)) 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 (unIdent i) . methods <$> getTypeMap return $ Map.lookup (tps, tysPs, isVarArity) mMap --debugPrint $ "pRet: " ++ show pRet -- Setup the environment in which to check the body let parMods = [ (iP, ms) | (FormalParam _ ms _ _ (VarId _ iP)) <- ps ] parVsigs = [ (unIdent iP, VSig t _pol {-(ofPol iP)-} True False (isFinal ms)) | ((iP, ms), t, _pol) <- zip3 parMods tysPs pPars ] 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 (Ident () 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 (id *** (\aid -> AI True aid)) parAids -- parSt = st { varMapSt = emptyVM { actorSt = parAMap } } -- This little thing is what actually checks the body ((mb', endSt),cs) <- runTcCodeM env st $ do mapM_ (uncurry registerParamType) $ zip (map (Ident ()) pIs) tysPs 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 = [ (unIdent i, VSig t _pol {-(ofPol i)-} True False (isFinal ms)) | (FormalParam _ ms _ _ (VarId _ i), t, _pol) <- zip3 ps tysPs pPars ] 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 (Ident () 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 (Ident () 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 = Just (voidT, top), 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 st $ do mapM_ (uncurry registerParamType) $ zip (map (Ident ()) pIs) tysPs 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 True . unIdent 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 $ unIdent i) PolicyParam _ i -> TcActualPolicy (RealPolicy $ TcRigidVar False $ unIdent i) LockStateParam _ i -> TcActualLockState [TcLockVar $ unIdent 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