paragon-0.1.19: src/Language/Java/Paragon/TypeCheck.hs
module Language.Java.Paragon.TypeCheck ( typeCheck ) 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 ())
typeCheck piDir (CompilationUnit _ pkg imps [td]) = do
let (fullTd, skoTy) = skolemTypeDecl td
runPiReader ["./",piDir] $ runTcDeclM skoTy $ do
typeCheckTd fullTd
return (CompilationUnit () pkg imps [fullTd])
typeCheck _ _ =
do fail $ "\n\n" ++ "Encountered multiple type declarations in the same file"
------------------------------------------------------------------
-- This is where the really fun stuff happens
{-
withEnvFromClass :: FilePath -> String -> TcDeclM r a -> TcDeclM r a
withEnvFromClass fp className tcba = do
--debug $ "Checking imported class: " ++ className
ClassDecl _ ms i@(Ident _ cuName) tps _super _impls (ClassBody _ ds) <- getClass fp
check (className == cuName) $
"File name " ++ className ++ " does not match class name " ++ cuName
let mDs = map unMemberDecl ds
fetchActors mDs $ -- actor ids,
fetchPols mDs $ -- policies,
fetchTMs mDs $ -- typemethod bodies,
fetchSignatures mDs $ do -- and signatures of fields, methods, constructors and locks
tm <- getTypeMap
let typeTm = tm { packages = Map.empty, types = Map.empty }
typeSig = TSig (clsTypeWArg (mkSimpleName TName i) [])
True (Final () `elem` ms) [] [] typeTm -- TODO: Insert actual values
withTypeMap clearToTypes $
extendTypeMapT (Ident () cuName) tps typeSig $ do
-- tm <- getTypeMap
--debug $ "TypeMap after adding " ++ className ++ ":\n" ++ show tm
tcba
where unMemberDecl :: Decl () -> MemberDecl ()
unMemberDecl (MemberDecl _ md) = md
unMemberDecl _ = panic (typeCheckerBase ++ ".withEnvFromClass") $
"Malformed PI-file contains initializer block"
---------------------------------------------------------------------
-- Working with actors
fetchActors :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
fetchActors mDecls tcba = do
--debug "fetchActors"
let acts = [ (ms, vd)
| FieldDecl _ ms (PrimType _ (ActorT _)) vds <- mDecls
, vd <- vds
, Static () `elem` ms -- Only statics exist ??
]
let (sfs,unstables) = partition (\(ms, _) -> Final () `elem` ms) acts
(spawns,stables) = partition (\(_,VarDecl _ _ initz) -> initz == Nothing) sfs
withFoldMap spawnActorVd spawns $
withFoldMap aliasActorVd unstables $
withFoldMap evalActorVd stables $ do
--debug "fetchActors complete"
tcba
where spawnActorVd, evalActorVd, aliasActorVd
:: ([Modifier ()],VarDecl ()) -> TcDeclM r a -> TcDeclM r a
-- Only Nothing for initializer
spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
a <- freshActorId (prettyPrint i)
p <- getReadPolicy ms
let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
withTypeMap (\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
aliasActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
p <- getReadPolicy ms
let vti = VSig actorT p False (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) }) $
tcra
aliasActorVd (_, 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 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 -> 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) }) $
tcra
evalActorVd (_, VarDecl _ _ Nothing) _ = panic (typeCheckerBase ++ ".evalActorVd") $ "No initializer"
evalActorVd (_, VarDecl _ arvid _) _ = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
-- end actors
----------------------------------------------------------------------
-- Working with policies
fetchPols :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
fetchPols mds tcba = do
--debug "fetchPols"
--debug $ "all policy decls: " ++ show [ fd | fd@(FieldDecl _ (PrimType PolicyT) _) <- mds ]
let pols = [ (i,initz) |
FieldDecl _ ms (PrimType _ (PolicyT _)) vds <- mds,
VarDecl _ (VarId _ i) (Just (InitExp _ initz)) <- vds,
Static () `elem` ms, Final () `elem` ms
]
--debug $ "pols: " ++ show pols
withFoldMap fetchPol pols $
tcba
fetchPol :: (Ident (), Exp ()) -> TcDeclM r a -> TcDeclM r a
fetchPol (i,e) tcba = do
{- p <- case e of
ExpName _ n -> do
tm <- getTypeMap
case lookupNamed policies n tm of
Just p -> return p
Nothing -> fail "fetchPol: no such policy"
PolicyExp _ pl -> evalPolicyExp pl
_ -> -}
p <- evalPolicy e
withTypeMap (\tm -> tm { policies = Map.insert i p (policies tm) }) $
tcba
-- end policies
------------------------------------------------------------
-- Working with typemethods
fetchTMs :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
fetchTMs memberDecls tcba = do
let ipbs = [ (i,(ps,body)) |
MethodDecl _ ms _ _ i ps _ (MethodBody _ (Just body)) <- memberDecls,
Typemethod () `elem` ms
]
ipidbs <- mapM paramsToIdents ipbs
withTypeMap (\tm ->
let newTM = foldl (\mtm (i,pb) -> Map.insert i pb mtm) (typemethods tm) ipidbs
in tm { typemethods = newTM }) $ tcba
where paramsToIdents (i, (ps,b)) = do
pids <- mapM paramIdent ps
return (i, (pids,b))
paramIdent :: FormalParam () -> TcDeclM r (Ident ())
paramIdent (FormalParam _ _ _ _ (VarId _ i)) = return i
paramIdent (FormalParam _ _ _ _ arvid) =
fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
-- end typemethods
------------------------------------------------------------
-- Working with locks
fetchSignatures :: [MemberDecl ()] -> TcDeclM r a -> TcDeclM r a
fetchSignatures memberDecls tcba =
withFoldMap fetchSignature memberDecls $ tcba
unVarDecl :: VarDecl () -> TcDeclM r (Ident ())
unVarDecl (VarDecl _ (VarId _ i) _) = return i
unVarDecl arvid = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
fetchSignature :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
fetchSignature memDecl tcba = do
--debug $ "fetchSignature: " ++ show memberDecl
case memDecl of
FieldDecl _ ms ty vds -> do
tcty <- evalSrcType ty
pol <- getReadPolicy ms
let vti = VSig tcty pol False (Static () `elem` ms) (Final () `elem` ms)
ids <- mapM unVarDecl vds
withTypeMap (\tm ->
tm { fields = foldl
(\m i -> Map.insert i vti m)
(fields tm) ids
}) $
tcba
MethodDecl _ ms tps retT i ps exns _ -> do
withFoldMap withTypeParam tps $ do
tcty <- evalReturnType retT
(pTys, pPols) <- unzip <$> mapM paramInfo ps
rPol <- getReturnPolicy ms pPols
wPol <- getWritePolicy ms
exs <- mapM eSpecToSig exns
expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ]
closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ]
opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ]
let mti = MSig {
mRetType = tcty,
mRetPol = rPol,
mPars = pPols,
mWrites = wPol,
mExpects = expects,
mLMods = (closes, opens),
mExns = exs
}
withTypeMap (\tm ->
tm { methods = Map.insert (i, pTys) (tps,mti) (methods tm) }) $
tcba
ConstructorDecl _ ms tps _ ps exns _ -> do
withFoldMap withTypeParam tps $ do
(pTys, pPols) <- unzip <$> mapM paramInfo ps
wPol <- getWritePolicy ms
exs <- mapM eSpecToSig exns
expects <- mapM evalLock $ concat [ l | Expects _ l <- ms ]
closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ]
opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ]
let cti = CSig {
cPars = pPols,
cWrites = wPol,
cExpects = expects,
cLMods = (closes, opens),
cExns = exs
}
withTypeMap (\tm ->
tm { constrs = Map.insert pTys (tps,cti) (constrs tm) }) $
tcba
LockDecl _ ms i mps Nothing -> do
pL <- getLockPolicy ms
-- TODO: Store lock properties!
let lsig = LSig pL (length mps)
withTypeMap (\tm ->
tm { locks = Map.insert i lsig (locks tm) }) $
tcba
LockDecl {} -> fail "Lock properties not yet supported"
_ -> fail "Inner classes not yet supported"
where eSpecToSig :: ExceptionSpec () -> TcDeclM r (TcType, ExnSig)
eSpecToSig (ExceptionSpec _ ms eType) = do
ty <- evalSrcType (RefType () eType) -- should use evalSrcRefType
rPol <- getReadPolicy ms
wPol <- getWritePolicy ms
opens <- mapM evalLock $ concat [ l | Opens _ l <- ms ]
closes <- mapM evalLock $ concat [ l | Closes _ l <- ms ]
let esig = ExnSig {
exnReads = rPol,
exnWrites = wPol,
exnMods = (closes, opens)
}
return (ty, esig)
paramInfo :: FormalParam () -> TcDeclM r (TcType, TcPolicy)
paramInfo (FormalParam _ ms ty _ (VarId _ i)) = do
pPol <- getParamPolicy i ms
pTy <- evalSrcType ty
return (pTy, pPol)
paramInfo (FormalParam _ _ _ _ arvid) =
fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
-}
{-------------------------------------------------------------------------------------
tdIdentStr :: TypeDecl () -> String
tdIdentStr (ClassTypeDecl _ (ClassDecl _ _ (Ident _ str) _ _ _ _)) = str
tdIdentStr (ClassTypeDecl _ (EnumDecl _ _ (Ident _ str) _ _)) = str
tdIdentStr (InterfaceTypeDecl _ (InterfaceDecl _ _ (Ident _ str) _ _ _)) = str
tdIdentStr _ = panic (typeCheckerBase ++ ".tdIdentStr")
"AntiQIdent should not appear in AST being type-checked"
-------------------------------------------------------------------------------------
getClass :: String -> TcDeclM r (ClassDecl ())
getClass piPath = do
fc <- liftIO $ readFile piPath
let east = parser compilationUnit fc
case east of
Left errs -> fail $ show errs
Right (CompilationUnit _ _ _ [(ClassTypeDecl _ cls)]) ->
-- assume there is only one type in each pi file and that is a class
return cls
_ -> fail $ "\nThere should be only one class type per Pi file!\n"
++ show east
-------------------------------------------------------------------------------------
-- [ d1 , d2 , x ] -> d1/d2/x , x can be folder or file (.class)
pathOf :: [Ident ()] -> String
pathOf = concat . intersperse [pSep] . map unIdent
--pathOf ((Ident name1):idents) = foldl (\p (Ident str) -> p ++ [pathSeparator]
-- ++ str ) name1 idents
-------------------------------------------------------------------------------------
-- testImportDecl = ImportDecl () False (Name () [Ident () "paragon",Ident () "util"]) True
pSep :: Char
pSep = pathSeparator
-------------------------------------------------------------------------------------}
-- Here goes TcTypeDecl.hs
typeCheckTd :: TypeDecl () -> TcDeclM r ()
typeCheckTd (ClassTypeDecl _ cdecl) = typeCheckCd cdecl
typeCheckTd (InterfaceTypeDecl _ idecl) = typeCheckId idecl
typeCheckId :: InterfaceDecl () -> TcDeclM r ()
typeCheckId (InterfaceDecl _ _ms i tps _supers (InterfaceBody _ memberDecls)) = do
--debug "typeCheckId"
withErrCtxt ("When checking interface " ++ prettyPrint i ++ ":\n") $ do
let staticWPol = top
withThisType i tps $ do
withFoldMap withTypeParam tps $
typeCheckActorFields memberDecls $ do
--debug "typeCheckLockDecls start"
typeCheckLockDecls memberDecls $ do
--debug "typeCheckTypeMethods start"
typeCheckTypeMethods memberDecls $ do
--debug "typeCheckPolicyFields start"
typeCheckPolicyFields memberDecls $ do
--debug "typeCheckSignatures start"
typeCheckSignatures memberDecls $ \constrWPol -> do
--debug "typeCheckMemberDecls start"
typeCheckMemberDecls staticWPol constrWPol memberDecls
typeCheckCd :: ClassDecl () -> TcDeclM r ()
typeCheckCd (ClassDecl _ ms i tps _super _impls (ClassBody _ decls)) = do
--debug "typeCheckCd"
withErrCtxt ("When checking class " ++ prettyPrint i ++ ":\n") $ do
staticWPol <- getWritePolicy ms
let memberDecls = [ mdecl | MemberDecl _ mdecl <- decls ]
inits = [ idecl | idecl@(InitDecl {}) <- decls ]
withThisType i tps $ do
withFoldMap withTypeParam tps $
typeCheckActorFields memberDecls $ do
--debug "typeCheckLockDecls start"
typeCheckLockDecls memberDecls $ do
--debug "typeCheckTypeMethods start"
typeCheckTypeMethods memberDecls $ do
--debug "typeCheckPolicyFields start"
typeCheckPolicyFields memberDecls $ do
--debug "typeCheckSignatures start"
typeCheckSignatures memberDecls $ \constrWPol -> do
withThisTypeSigs i tps $ do
--debug "typeCheckInitDecls start"
typeCheckInitDecls staticWPol constrWPol inits
--debug "typeCheckMemberDecls start"
typeCheckMemberDecls staticWPol constrWPol memberDecls
typeCheckCd _ = panic (typeCheckerBase ++ ".typeCheckCd")
"Enum decls not yet supported"
withThisType :: Ident () -> [TypeParam ()] -> TcDeclM r a -> TcDeclM r a
withThisType i tps =
withTypeMap $ \tm ->
-- We insert an empty typemap at first,
-- since we are only using this when checking signatures
let thisSig = TSig (clsTypeWArg (mkSimpleName TName i) [])
True False [] [] emptyTM
in tm { types = Map.insert i (tps,thisSig) (types tm) }
withThisTypeSigs :: Ident () -> [TypeParam ()] -> TcDeclM r a -> TcDeclM r a
withThisTypeSigs i tps tcba = do
tm <- getTypeMap
let thisTm = tm { types = Map.empty, packages = Map.empty }
thisSig = TSig (clsTypeWArg (mkSimpleName TName i) [])
True False [] [] thisTm -- TODO: Include proper values
withTypeMap (extendTypeMapT (Name () TName Nothing i) tps thisSig) $
tcba
withTypeParam :: TypeParam () -> TcDeclM r a -> TcDeclM r a
withTypeParam tp tcba =
case tp of
ActorParam _ i -> do
let vti = VSig actorT top False False True
withTypeMap (\tm ->
tm { actors = Map.insert i (ActorTPVar i) (actors tm),
fields = Map.insert i vti (fields tm) }) $ tcba
PolicyParam _ i -> do
let vti = VSig policyT top False False True
withTypeMap (\tm ->
tm { policies = Map.insert i (TcRigidVar i) (policies tm),
fields = Map.insert i vti (fields tm) }) $ tcba
LockStateParam _ i -> do
let vti = VSig (lockT []) top False 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 ()] -> TcDeclM r a -> TcDeclM r a
typeCheckActorFields 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 _ _ initz) -> initz == Nothing) sfs
withFoldMap spawnActorVd spawns $
withFoldMap aliasActorVd unstables $
withFoldMap evalActorVd stables $ do
--debug "fetchActors complete"
tcba
where spawnActorVd, evalActorVd, aliasActorVd
:: ([Modifier ()],VarDecl ()) -> TcDeclM r a -> TcDeclM r a
-- Only Nothing for initializer
spawnActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
a <- freshActorId (prettyPrint i)
p <- getReadPolicy ms
let vti = VSig actorT p False (Static () `elem` ms) (Final () `elem` ms)
withTypeMap (\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
aliasActorVd (ms, VarDecl _ (VarId _ i) _) tcra = do
p <- getReadPolicy ms
let vti = VSig actorT p False (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) }) $
tcra
aliasActorVd (_, 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 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 -> 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) }) $
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 r a -> TcDeclM r a
typeCheckLockDecls mds tcba = do
let ls = [ ld | ld@ LockDecl {} <- mds ]
withFoldMap typeCheckLockDecl ls $ tcba
typeCheckLockDecl :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
typeCheckLockDecl (LockDecl _ ms i mps Nothing) tcba = do
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
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 r a -> TcDeclM r a
typeCheckTypeMethods mds tcba = do
let tms = [ tmd | tmd@(MethodDecl _ ms _ _ _ _ _ _) <- mds,
Typemethod () `elem` ms
]
withFoldMap typeCheckTMSig tms $ do
st <- setupStartState
mapM_ (typeCheckMethodDecl st) tms
withFoldMap addTMBody tms $
tcba
-- Precondition: only applied on actual typemethods
typeCheckTMSig :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
typeCheckTMSig (MethodDecl _ ms tps retT i ps exns _) tcba = do
(tyPs, mti) <- withErrCtxt ("When checking signature of typemethod "
++ prettyPrint i ++ ":\n") $ do
-- 1. No type parameters
check (null tps) $ "No type parameters allowed on typemethod methods"
-- 2. No interaction with policies or lock states
check (all (\m -> not (isPolicyMod m || isLockStateMod m)) ms) $
"Methods annotated with typemethod cannot have policy or lock state modifiers"
-- 3. Same check for parameters
let plms = [ m | FormalParam _ pms _ _ _ <- ps, m <- pms,
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 = [ bottom | _ <- ps ],
mExpects = [],
mLMods = noMods,
mExns = []
}
return (tyPs, mti)
withTypeMap (\tm -> tm { methods = Map.insert (i,tyPs) ([],mti) (methods tm) }) $
tcba
typeCheckTMSig md _ = panic (typeCheckerBase ++ ".typeCheckTMSig") $
"Applied to non-method decl " ++ show md
addTMBody :: MemberDecl () -> TcDeclM r a -> TcDeclM r a
addTMBody (MethodDecl _ _ _ _ i ps _ (MethodBody _ (Just bl))) =
let pis = [ iP | FormalParam _ _ _ _ (VarId _ iP) <- ps ]
in withTypeMap $ \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 r a -> TcDeclM r a
typeCheckPolicyFields mds =
let pfs = [ pf | pf@(FieldDecl _ _ (PrimType _ (PolicyT _)) _) <- mds ] in
-- The 'map' here means fields can only refer to things above them
withFoldMap typeCheckPolicyField pfs
-- Precondition: only apply on policies
typeCheckPolicyField :: MemberDecl () -> TcDeclM r a -> TcDeclM r 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 r a -> TcDeclM r a
addField vti i =
withTypeMap (\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 r a -> TcDeclM r 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),_) <- 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
withTypeMap (\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 ()] -> (TcPolicy -> TcDeclM r a) -> TcDeclM r a
typeCheckSignatures mds tcbaf = do
st <- setupStartState
withFoldMap (typeCheckSignature st) mds $
getConstrPol >>= tcbaf
getConstrPol :: TcDeclM r TcPolicy
getConstrPol = do
mConstrs <- constrs <$> getTypeMap
let wPols = map (cWrites . snd) $ Map.elems mConstrs
return $ foldl join bottom wPols
typeCheckSignature :: CodeState -> MemberDecl () -> TcDeclM r a -> TcDeclM r 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
-- 3. Add signature to typemap
return $ VSig {
varType = ty,
varPol = rPol,
varParam = False,
varStatic = Static () `elem` ms,
varFinal = Final () `elem` ms
}
withFoldMap (addField vti) vds $
tcba
where addField :: VarFieldSig -> VarDecl () -> TcDeclM r a -> TcDeclM r a
addField vti (VarDecl _ (VarId _ i) _) =
withTypeMap $ \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))
(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
-- 2. Check parameter types and policy modifiers
(pTs,pPols) <- unzip <$> 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 = 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. Check parameter types and policy modifiers
(pTs,pPols) <- unzip <$> 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 = 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 -- 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, TcPolicy) -> TcDeclM r a -> TcDeclM r a
withParam (FormalParam _ ms _ _ (VarId _ i), ty, p) = do
let vsig = VSig ty p True (Static () `elem` ms) (Final () `elem` ms)
withTypeMap $ \tm ->
tm { fields = Map.insert i vsig (fields tm) }
withParam (FormalParam _ _ _ _ arvid, _, _) =
fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
typeCheckExnSig :: CodeState -> ExceptionSpec () -> TcDeclM r (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 = rPol,
exnWrites = wPol,
exnMods = lms
}
return (ty, xSig)
checkPolicyMods :: CodeState -> [Modifier ()] -> String -> TcDeclM r ()
checkPolicyMods st ms failStr = do
--debug $ "checkPolicyMods: " ++ show ms
let rPolExps = [ e | Reads _ e <- ms ]
wPolExps = [ e | Writes _ e <- ms ]
check (length rPolExps <= 1 && length wPolExps <= 1) failStr
mapM_ (typeCheckPolicyMod st) $ rPolExps ++ wPolExps
checkLMMods :: [Modifier ()] -> TcDeclM r LockMods
checkLMMods ms = do
let cs = concat [ l | Closes _ l <- ms ]
os = concat [ l | Opens _ l <- ms ]
tcCs <- mapM evalLock cs
tcOs <- mapM evalLock os
return (tcCs, tcOs)
checkExpectsMods :: [Modifier ()] -> TcDeclM r [TcLock]
checkExpectsMods ms = do
let es = concat [ l | Expects _ l <- ms ]
mapM evalLock es
typeCheckParam :: CodeState -> FormalParam () -> TcDeclM r (TcType, TcPolicy)
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 i ms
return (if ell then arrayType ty bottom else ty, rPol)
typeCheckParam _ (FormalParam _ _ _ _ arvid) =
fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid
typeCheckPolicyMod :: CodeState -> Policy () -> TcDeclM r ()
typeCheckPolicyMod st polExp = do
-- tm <- getTypeMap
-- debug $ show tm
-- debug $ "typeCheckPolicyMod " ++ show polExp
((ty, _pol), 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?!?"
checkM (ty <: policyT) $ "Wrong type for policy expression: " ++ prettyPrint ty
-- check that _pol is bottom shouldn't be necessary
-- end signatures
------------------------------------------------------------------------------
-- Initializers
-- Precondition: Only init decls
typeCheckInitDecls :: TcPolicy -> TcPolicy -> [Decl ()] -> TcDeclM r ()
typeCheckInitDecls sLim cLim is = do
setupStartState >>=
\st -> foldM (typeCheckInitDecl sLim) st [ bl | InitDecl _ True bl <- is ] >>=
\st' -> foldM (typeCheckInitDecl cLim) st' [ bl | InitDecl _ False bl <- is ] >>
return ()
typeCheckInitDecl :: TcPolicy -> CodeState -> Block () -> TcDeclM r CodeState
typeCheckInitDecl lim st bl = do
tm <- getTypeMap
(newSt,cs) <- runTcCodeM (simpleEnv lim $ "initializer block") st $
addBranchPCList (Map.keys (fields tm)) $ do
tcBlock bl
getState
solve cs
return newSt
------------------------------------------------------------------------------
-- Bodies
typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl ()] -> TcDeclM r ()
typeCheckMemberDecls sLim cLim ms = do
st <- setupStartState
mapM_ (typeCheckMemberDecl sLim cLim st) ms
typeCheckMemberDecl :: TcPolicy -> TcPolicy -> CodeState -> MemberDecl () -> TcDeclM r ()
typeCheckMemberDecl sLim cLim st fd@(FieldDecl {}) =
typeCheckFieldDecl sLim cLim st fd
typeCheckMemberDecl _ _ st md@(MethodDecl {}) =
typeCheckMethodDecl st md
typeCheckMemberDecl _ _ st cd@(ConstructorDecl {}) =
typeCheckConstrDecl st cd
typeCheckMemberDecl _ _ _ _ = return ()
typeCheckFieldDecl :: TcPolicy -> TcPolicy -> CodeState -> MemberDecl () -> TcDeclM r ()
typeCheckFieldDecl staticLim constrLim st (FieldDecl _ ms _t vds) = do
--debug $ "typeCheckFieldDecl:" ++ show fd
let lim = if Static () `elem` ms then staticLim else constrLim
mapM_ (typeCheckVarDecl lim st) vds
typeCheckFieldDecl _ _ _ md = panic (typeCheckerBase ++ ".typeCheckFieldDecl") $
"Applied to non-field decl " ++ show md
typeCheckVarDecl :: TcPolicy -> CodeState -> VarDecl () -> TcDeclM r ()
typeCheckVarDecl lim st (VarDecl _ (VarId _ i) mInit) = do
--debug $ "typeCheckVarDecl:" ++ show i
withErrCtxt ("When checking initializer of field " ++ prettyPrint i ++ ":\n") $ do
Just (VSig matchTy matchPol _ _ _) <- Map.lookup i . fields <$> getTypeMap
case mInit of
Nothing -> return ()
Just (InitExp _ e) -> do
(_,cs) <- runTcCodeM (simpleEnv lim $ "field initializer " ++ prettyPrint e) st $ do
(ty, pol) <- tcExp e
checkM (ty <: matchTy) $ "typeCheckVarDecl: type mismatch"
constraint [] pol matchPol $
"Cannot assign result of expression " ++ prettyPrint e ++
" with policy " ++ prettyPrint pol ++
" to location " ++ prettyPrint i ++
" with policy " ++ prettyPrint matchPol
solve cs
Just (InitArray _ arr) ->
case mArrayType matchTy of
Nothing -> fail $ "Field " ++ prettyPrint i
++ " of non-array type " ++ prettyPrint matchTy
++ " given literal array initializer"
Just (baseTy, pols) -> do
(_,cs) <- runTcCodeM (simpleEnv lim $ "array initializer " ++ prettyPrint arr) st $
tcArrayInit baseTy pols arr
solve cs
-- _ -> error $ "typeCheckVarDecl: Array syntax not yet supported"
typeCheckVarDecl _ _ vd = fail $ "Deprecated array syntax not supported: " ++ prettyPrint vd
typeCheckMethodDecl :: CodeState -> MemberDecl () -> TcDeclM r ()
typeCheckMethodDecl st (MethodDecl _ _ tps _ i ps _ 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 ]
Just (_, MSig tyRet pRet pPars pWri expLs lMods xSigs) <-
Map.lookup (i,tysPs) . methods <$> getTypeMap
-- Setup the environment in which to check the body
let parVsigs = [ (iP, VSig t p True False (isFinal ms)) |
(FormalParam _ ms _ _ (VarId _ iP), t, p) <- zip3 ps tysPs 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)])
}
-- 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 (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids
parSt = st { actorSt = parAMap `Map.union` actorSt st }
-- This little thing is what actually checks the body
(endSt,cs) <- runTcCodeM 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
typeCheckMethodDecl _ md = panic (typeCheckerBase ++ ".typeCheckMethodDecl") $
"Applied to non-method decl " ++ show md
typeCheckConstrDecl :: CodeState -> MemberDecl () -> TcDeclM r ()
typeCheckConstrDecl st (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 (_, CSig pPars pWri expLs lMods xSigs) <-
Map.lookup tysPs . constrs <$> getTypeMap
-- Setup the environment in which to check the body
tm <- getTypeMap
let parVsigs = [ (i, VSig t p True False (isFinal ms)) |
(FormalParam _ ms _ _ (VarId _ i), t, p) <- zip3 ps tysPs pPars ]
pars = map fst parVsigs
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)])
}
--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 (mkSimpleName EName *** (\aid -> AI aid Stable)) parAids
parSt = st { actorSt = parAMap `Map.union` actorSt st }
-- This little thing is what actually checks the body
(endSt,cs) <- runTcCodeM 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
typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $
"Applied to non-constructor decl " ++ show md
aliasIfActor :: (Ident (), TcType) -> TcDeclM r [(Ident (), ActorId)]
aliasIfActor (i, ty)
| ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]
| otherwise = return []
checkExnMods :: CodeState -> (TcType, LockMods) -> TcDeclM r ()
checkExnMods st (xTy, lms) = do
let mExnSt = epState <$> Map.lookup (ExnType xTy) (exnS st)
maybeM mExnSt $ \sX -> do
check (lms `models` lockMods sX) $
"Declared exception lock modifiers not general enough: "
++ show lms
tcMethodBody :: MethodBody () -> TcCodeM r ()
tcMethodBody (MethodBody _ mBlock) = maybeM mBlock $ tcBlock
tcConstrBody :: ConstructorBody () -> TcCodeM r ()
tcConstrBody (ConstructorBody _ Nothing stmts) = tcBlockStmts stmts
tcConstrBody (ConstructorBody _ (Just eci) _)
= fail $ "Explicit constructor invocation not yet supported: " ++ prettyPrint eci
------------------------------------------
-- 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)
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 ()] -> (TcType, [(TypeParam (), TcTypeArg)])
skolemType i tps =
let args = map skolemParam tps
in (clsTypeWArg (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 (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