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