paragon-0.1.3: src/Language/Java/Paragon/TypeCheck.hs
module Language.Java.Paragon.TypeCheck where
import Language.Java.Paragon.Syntax
import Language.Java.Paragon.Parser
import Language.Java.Paragon.Pretty
import Language.Java.Paragon.TypeCheck.Actors
import Language.Java.Paragon.TypeCheck.Constraints
import Language.Java.Paragon.TypeCheck.Locks
import Language.Java.Paragon.TypeCheck.Monad
import Language.Java.Paragon.TypeCheck.TcExp
import Language.Java.Paragon.TypeCheck.TcStmt
import Language.Java.Paragon.TypeCheck.Monad
import Language.Java.Paragon.TypeCheck.TcEnv
import Language.Java.Paragon.TypeCheck.TcState
import Language.Java.Paragon.TypeCheck.Types
import Language.Java.Paragon.TypeCheck.Locks
import Language.Java.Paragon.TypeCheck.Policy
import Language.Java.Paragon.TypeCheck.Uniq
import Language.Java.Paragon.TypeCheck.Evaluate
--import Language.Java.Paragon.TypeCheck.Interpreter
import qualified Language.Java.Paragon.TypeCheck.Types as TP
import System.FilePath
import System.Environment
import System.Directory
import Control.Monad (when)
import qualified Data.Map as Map
import Data.Maybe
import Data.List (partition, intersperse)
import Control.Applicative ( (<$>) )
import Control.Arrow ( (***), first, second )
import Data.Generics.Uniplate.Data (transformBi)
typeCheck :: DirectoryPath -> CompilationUnit -> IO CompilationUnit
typeCheck currentDir ast@(CompilationUnit pkg imps [td]) = do
let (skoTd, skoTy) = skolemTypeDecl td
e <- runTcBase skoTy $ do
withEnvFromImps "" "" allImps $ do
--debug "Import env setup"
withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do
--debug "TypeMap completed"
tm <- getTypeMap
--debug $ "TypeMap: " ++ show tm
withExpandedNames skoTd $ \fullTd -> do
--debug $ "Full AST:\n" ++ prettyPrint fullTd
typeCheckTd fullTd
-- debug $ "Type checking completed!"
return (CompilationUnit pkg imps [fullTd])
case e of
Left str -> fail str
Right ast -> return ast
where allImps = defaultImportDecls ++ imps
withExpandedNames :: TypeDecl -> (TypeDecl -> TcBase a) -> TcBase 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] -> TcBase a -> TcBase a
withEnvFromImps dir thisStr is tcba = do
--debug ("withEnvFromImpsies: " ++ show is)
--withEnvFromImps dir thisStr (imp:is) =
withFoldMap (withEnvFromImp dir thisStr) is $ tcba
-- withEnvFromImp dir thisStr imp . withEnvFromImps dir thisStr is
withEnvFromImp :: DirectoryPath -> String -> ImportDecl -> TcBase a -> TcBase a
-- import java.*;
withEnvFromImp dir thisStr imp@(ImportDecl False (Name pkgNames) True) tcba = do
--debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames)
let relative = pathOf pkgNames
absoluteDir = dir ++ 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 dir _ imp@(ImportDecl False (Name clsPkgName) False) tcba = do
--debug $ "Setting up single import of: " ++ show clsPkgName
let relative = pathOf clsPkgName
absoluteFile = dir ++ pSep:relative ++ ".pi"
(Ident className) = last clsPkgName
pkgNames = init clsPkgName
withEnvFromSingleClass pkgNames absoluteFile className $ tcba
withEnvFromPkg :: [Ident] -> [(FilePath, String)] -> TcBase a -> TcBase 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 -> TcBase a -> TcBase a
withEnvFromSingleClass pkgPath fp n tcba = do
withEnvFromClass fp n .
withEnvFromPkg pkgPath [] $ tcba
-------------------------------------------------------------------------
-- This is where the really fun stuff happens
withEnvFromClass :: FilePath -> String -> TcBase a -> TcBase a
withEnvFromClass fp className tcba = do
--debug $ "Checking imported class: " ++ className
ClassDecl _ 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 }
withTypeMap clearToTypes $
extendTypeMapT (Ident cuName) tps typeTm $ do
tm <- getTypeMap
--debug $ "TypeMap after adding " ++ className ++ ":\n" ++ show tm
tcba
---------------------------------------------------------------------
-- Working with actors
fetchActors :: [MemberDecl] -> TcBase a -> TcBase 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) -> TcBase a -> TcBase a
spawnActor (ms, VarDecl (VarId i) _) tcba = do
a <- freshActorId
p <- getReadPolicy ms
let vti = VTI actorT p (Static `elem` ms) (Final `elem` ms)
withTypeMap (\tm -> tm { actors = Map.insert i a (actors tm),
fields = Map.insert i vti (fields tm) }) $
tcba
aliasActor (ms, VarDecl (VarId i) _) tcba = do
p <- getReadPolicy ms
let vti = VTI actorT p (Static `elem` ms) (Final `elem` ms)
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 = VTI 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] -> TcBase a -> TcBase 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) -> TcBase a -> TcBase 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] -> TcBase a -> TcBase 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] -> TcBase a -> TcBase a
fetchSignatures memberDecls tcba =
withFoldMap fetchSignature memberDecls $ tcba
fetchSignature :: MemberDecl -> TcBase a -> TcBase a
fetchSignature memberDecl tcba = do
--debug $ "fetchSignature: " ++ show memberDecl
case memberDecl of
FieldDecl ms ty vds -> do
tcty <- evalSrcType ty
pol <- getReadPolicy ms
let vti = VTI tcty pol (Static `elem` ms) (Final `elem` ms)
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 = MTI {
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 = CTI {
cPars = pPols,
cWrites = wPol,
cExpects = expects,
cLMods = (closes, opens),
cExns = exs
}
withTypeMap (\tm ->
tm { constrs = Map.insert pTys (tps,cti) (constrs tm) }) $
tcba
LockDecl ms i mps props -> do
lPol <- getLockPolicy ms
--debug $ "lPol: " ++ show lPol
-- TODO: Store lock properties!
let vti = VTI (lockT []) lPol True True
arity = length mps
withTypeMap (\tm ->
tm { lockArities = Map.insert i arity (lockArities tm),
fields = Map.insert i vti (fields tm) }) $
tcba
where eSpecToSig :: ExceptionSpec -> TcBase (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 -> TcBase (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 -> TcBase 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 -> TcBase ()
typeCheckTd (ClassTypeDecl cd) = typeCheckCd cd
typeCheckTd (InterfaceTypeDecl id) = typeCheckId id
typeCheckId :: InterfaceDecl -> TcBase ()
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 -> TcBase ()
typeCheckCd (ClassDecl ms i tps _super _impls (ClassBody decls)) = do
--debug "typeCheckCd"
withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do
staticWPol <- getWritePolicy ms
let memberDecls = map (\(MemberDecl d) -> d) decls
withThisType i tps $ do
withFoldMap withTypeParam tps $
typeCheckActorFields memberDecls $ do
--debug "typeCheckLockDecls start"
typeCheckLockDecls memberDecls $ do
--debug "typeCheckTypeMethods start"
typeCheckTypeMethods memberDecls $ do
--debug "typeCheckPolicyFields start"
typeCheckPolicyFields memberDecls $ do
--debug "typeCheckSignatures start"
typeCheckSignatures memberDecls $ \constrWPol -> do
withThisTypeSigs i tps $ do
--debug "typeCheckMemberDecls start"
typeCheckMemberDecls staticWPol constrWPol memberDecls
withThisType :: Ident -> [TypeParam] -> TcBase a -> TcBase a
withThisType i tps =
withTypeMap $ \tm ->
-- We insert an empty typemap at first,
-- since we are only using this when checking signatures
tm { types = Map.insert i (tps,emptyTM) (types tm) }
withThisTypeSigs :: Ident -> [TypeParam] -> TcBase a -> TcBase a
withThisTypeSigs i tps tcba = do
tm <- getTypeMap
let thisTm = tm { types = Map.empty, packages = Map.empty }
extendTypeMapT i tps thisTm $
tcba
withTypeParam :: TypeParam -> TcBase a -> TcBase a
withTypeParam tp tcba =
case tp of
ActorParam i -> do
let vti = VTI actorT top False True
withTypeMap (\tm ->
tm { actors = Map.insert i (ActorTPVar i) (actors tm),
fields = Map.insert i vti (fields tm) }) $ tcba
PolicyParam i -> do
let vti = VTI policyT top False True
withTypeMap (\tm ->
tm { policies = Map.insert i (TcRigidVar i) (policies tm),
fields = Map.insert i vti (fields tm) }) $ tcba
LockStateParam i -> do
let vti = VTI (lockT []) top False True
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] -> TcBase a -> TcBase a
typeCheckActorFields = fetchActors
{- let acts = [ (ms, vd)
| FieldDecl ms (PrimType ActorT) vds <- mDecls
, vd <- vds
, Static `elem` ms -- Only statics exist ??
]
-}
---------------------------------------------------------------
-- Locks
typeCheckLockDecls :: [MemberDecl] -> TcBase a -> TcBase a
typeCheckLockDecls mds tcba = do
let ls = [ ld | ld@ LockDecl {} <- mds ]
withFoldMap typeCheckLockDecl ls $ tcba
typeCheckLockDecl :: MemberDecl -> TcBase a -> TcBase 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] -> TcBase a -> TcBase 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 -> TcBase a -> TcBase 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 = MTI {
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 -> TcBase a -> TcBase 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] -> TcBase a -> TcBase a
typeCheckPolicyFields mds =
let pfs = [ pf | pf@(FieldDecl _ (PrimType PolicyT) _) <- mds ] in
-- The 'map' here means fields can only refer to things above them
withFoldMap typeCheckPolicyField pfs
-- Precondition: only apply on policies
typeCheckPolicyField :: MemberDecl -> TcBase a -> TcBase a
typeCheckPolicyField 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 $ VTI {
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 :: VTypeInfo -> Ident -> TcBase a -> TcBase a
addField vti i =
withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) })
evalAddInit :: (Ident, VarInit) -> TcBase a -> TcBase 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 -> TcBase a) -> TcBase a
typeCheckSignatures mds tcbaf = do
st <- setupStartState
withFoldMap (typeCheckSignature st) mds $
getConstrPol >>= tcbaf
getConstrPol :: TcBase TcPolicy
getConstrPol = do
mConstrs <- constrs <$> getTypeMap
let wPols = map (cWrites . snd) $ Map.elems mConstrs
return $ foldl join bottom wPols
typeCheckSignature :: TcState -> MemberDecl -> TcBase a -> TcBase a
-- Fields
typeCheckSignature st fd@(FieldDecl ms t vds) tcba
| t /= PrimType PolicyT && t /= PrimType ActorT = do
--debug $ "typeCheckSignature: " ++ prettyPrint fd
let fis = [ i | VarDecl (VarId i) _ <- vds ]
vti <- withErrCtxt ("When checking signature for fields "
++ concat (intersperse ", " (map prettyPrint fis)) ++ ":\n") $ do
-- 1. Check field type
ty <- evalSrcType t
_ <- lookupTypeOfT ty <$> getTypeMap -- TODO
-- 2. Typecheck and evaluate field policy
let rPolExps = [ e | Reads e <- ms ]
check (length rPolExps <= 1) $
"typeCheckSignature: At most one read modifier allowed per field"
mapM_ (typeCheckPolicyMod st) rPolExps
rPol <- getReadPolicy ms
-- 3. Add signature to typemap
return $ VTI {
varType = ty,
varPol = rPol,
varStatic = Static `elem` ms,
varFinal = Final `elem` ms
}
withFoldMap (addField vti) vds $
tcba
where addField :: VTypeInfo -> VarDecl -> TcBase a -> TcBase a
addField vti (VarDecl (VarId i) _) =
withTypeMap $ \tm ->
tm { fields = Map.insert i vti (fields tm) }
-- Methods
typeCheckSignature st md@(MethodDecl ms tps retT i ps exns mb) tcba
| not (Typemethod `elem` ms) = do
--debug $ "typeCheckSignature: " ++ prettyPrint (MethodDecl ms tps retT i ps exns (MethodBody Nothing))
(pTs, mti) <- withErrCtxt ("When checking signature of method " ++ prettyPrint i ++ "("
++ concat (intersperse ", " [prettyPrint t | FormalParam _ t _ _ <- ps ]) ++ "):\n") $ do
-- 0. Setup type params
withFoldMap withTypeParam tps $ do
-- 1. Check return type
ty <- evalReturnType retT
when (isClassType ty) (do TypeMap {} <- lookupTypeOfT ty <$> getTypeMap
return ())
--debug $ " type = " ++ show ty
-- 2. Typecheck and evaluate policy modifiers
withFoldMap withParam ps $ checkPolicyMods st ms
"typeCheckSignature: At most one return/write modifier allowed per method"
-- 3. Typecheck and evaluate lock modifiers
lms <- checkLMMods ms
es <- checkExpectsMods ms
-- 4. Check parameter types and policy modifiers
(pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps
-- 5. Typecheck and evaluate exception signatures
xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns
-- 6. Add signature to typemap
rPol <- getReturnPolicy ms pPols
wPol <- getWritePolicy ms
let mti = MTI {
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 = CTI {
cWrites = wPol,
cPars = pPols,
cExpects = es,
cLMods = lms,
cExns = xSigs
}
return (pTs, cti)
withTypeMap (\tm -> tm { constrs = Map.insert pTs (tps,cti) (constrs tm) }) $
tcba
-- Locks
typeCheckSignature st ld@(LockDecl ms i mps mprops) tcba = do
--debug $ "typeCheckSignature: " ++ prettyPrint ld
vti <- withErrCtxt ("When checking signature of lock " ++ prettyPrint i ++ ":\n") $ do
pol <- getLockPolicy ms
return $ VTI (lockT []) pol True True
withTypeMap (\tm -> tm { fields = Map.insert i vti (fields tm) }) $
tcba
typeCheckSignature _ _ tcba = tcba
withParam :: FormalParam -> TcBase a -> TcBase a
withParam (FormalParam _ _ _ (VarId i)) =
withTypeMap $ \tm ->
tm { fields = Map.insert i (VTI err err err err) (fields tm) }
where err = error "Use of parameter directly in modifier" -- TODO: UUUUGLY!
typeCheckExnSig :: TcState -> ExceptionSpec -> TcBase (TcType, ExnSig)
typeCheckExnSig st (ExceptionSpec ms xT) = do
withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do
ty <- TP.TcRefT <$> evalSrcRefType xT
-- Check that type exists
TypeMap {} <- lookupTypeOfT ty <$> getTypeMap
checkPolicyMods st ms
"typeCheckSignature: At most one read/write modifier allowed per exception"
rPol <- getReadPolicy ms
wPol <- getWritePolicy ms
lms <- checkLMMods ms
let xSig = ExnSig {
exnReads = rPol,
exnWrites = wPol,
exnMods = lms
}
return (ty, xSig)
checkPolicyMods :: TcState -> [Modifier] -> String -> TcBase ()
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] -> TcBase 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] -> TcBase [TcLock]
checkExpectsMods ms = do
let es = concat [ l | Expects l <- ms ]
mapM evalLock es
typeCheckParam :: TcState -> FormalParam -> TcBase (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 -> TcBase ()
typeCheckPolicyMod st polExp = do
--debug $ "typeCheckPolicyMod " ++ show polExp
((ty, _pol), cs) <- runTc (simpleEnv top) st
(--liftBase (debug "inside runTC") >>
tcExp polExp)
check (null cs) $ "Internal WTF: typeCheckPolicyMod: Constraints in policy exp?!?"
check (ty <: policyT) $ "Wrong type for policy expression: " ++ prettyPrint ty
-- check that _pol is bottom shouldn't be necessary
-- end signatures
------------------------------------------------------------------------------
-- Bodies
typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl] -> TcBase ()
typeCheckMemberDecls sLim cLim ms = do
st <- setupStartState
mapM_ (typeCheckMemberDecl sLim cLim st) ms
typeCheckMemberDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl -> TcBase ()
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 -> TcBase ()
typeCheckFieldDecl staticLim constrLim st fd@(FieldDecl ms t vds) = do
--debug $ "typeCheckFieldDecl:" ++ show fd
let lim = if Static `elem` ms then staticLim else constrLim
mapM_ (typeCheckVarDecl lim st) vds
typeCheckVarDecl :: TcPolicy -> TcState -> VarDecl -> TcBase ()
typeCheckVarDecl lim st (VarDecl (VarId i) mInit) = do
--debug $ "typeCheckVarDecl:" ++ show i
withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do
Just (VTI matchTy matchPol _ _) <- Map.lookup i . fields <$> getTypeMap
case mInit of
Nothing -> return ()
Just (InitExp e) -> do
(_,cs) <- runTc (simpleEnv lim) st $ do
(ty, pol) <- tcExp e
check (ty <: matchTy) $ "typeCheckVarDecl: type mismatch"
constraint_ pol matchPol
solve cs
typeCheckMethodDecl :: TcState -> MemberDecl -> TcBase ()
typeCheckMethodDecl st (MethodDecl _ tps _ i ps _ mb) = do
-- Lookup the correct function signature
-- debug $ "Type-checking method " ++ prettyPrint i
withErrCtxt ("When checking body of method " ++ prettyPrint i ++ ":\n") $ do
withFoldMap withTypeParam tps $ do
tysPs <- mapM evalSrcType $ [ t | FormalParam _ t _ _ <- ps ]
Just (tps, MTI tyRet pRet pPars pWri expLs lMods xSigs) <-
Map.lookup (i,tysPs) . methods <$> getTypeMap
-- Setup the environment in which to check the body
let parVtis = [ (i, VTI t p False (isFinal ms)) |
(FormalParam ms _ _ (VarId i), t, p) <- zip3 ps tysPs pPars ]
pars = map fst parVtis
exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
exnLMods = map (second exnMods) xSigs
parEnts = [ (VarEntity $ Name [i], bottom) | i <- pars ]
exnEnts = [ (ExnEntity t, bottom) | t <- map fst xSigs ]
branchMap = Map.insert returnE bottom $ Map.fromList (parEnts ++ exnEnts)
env = TcEnv {
vars = Map.fromList parVtis,
lockstate = expLs,
returnI = (tyRet, pRet),
exnsE = Map.fromList exnPols,
branchPCE = (branchMap, pWri)
}
--debug $ "Using env: " ++ show env
-- Setup the state in which to check the body
parAids <- concat <$> mapM aliasIfActor (zip pars tysPs)
let parAMap = Map.fromList $ map ((Name . return) *** (\aid -> AI aid Stable)) parAids
parSt = st { actorSt = parAMap `Map.union` actorSt st }
-- This little thing is what actually checks the body
(endSt,cs) <- runTc env parSt $ tcMethodBody mb >> getState
-- ... and then we need to check the end result
solve cs
check (lMods `models` lockMods endSt) $
"Declared lock modifiers not general enough: " ++ show lMods
mapM_ (checkExnMods endSt) exnLMods
typeCheckConstrDecl :: TcState -> MemberDecl -> TcBase ()
typeCheckConstrDecl st cd@(ConstructorDecl _ tps ci ps _ cb) = do
withErrCtxt ("When checking body of constructor " ++ prettyPrint ci ++ ":\n") $ do
--debug $ "Type-checking constructor:\n " ++ prettyPrint cd
withFoldMap withTypeParam tps $ do
-- Lookup the correct function signature
tysPs <- mapM evalSrcType $ [ t | FormalParam _ t _ _ <- ps ]
Just (tps, CTI pPars pWri expLs lMods xSigs) <-
Map.lookup tysPs . constrs <$> getTypeMap
-- Setup the environment in which to check the body
tm <- getTypeMap
let parVtis = [ (i, VTI t p False (isFinal ms)) |
(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, VTI _ _ 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) -> TcBase [(Ident, ActorId)]
aliasIfActor (i, ty)
| ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]
| otherwise = return []
checkExnMods :: TcState -> (TcType, LockMods) -> TcBase ()
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 ()
tcMethodBody (MethodBody mBlock) = maybeM mBlock $ tcBlock
tcConstrBody :: ConstructorBody -> Tc ()
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 -> TcBase ()
debug str = liftIO $ putStrLn $ "DEBUG: " ++ str