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