module Language.Java.Paragon.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.Constraints
import Language.Java.Paragon.TypeCheck.TcExp
import Language.Java.Paragon.TypeCheck.TcStmt
import Language.Java.Paragon.TypeCheck.Monad
import Language.Java.Paragon.TypeCheck.TcEnv
import Language.Java.Paragon.TypeCheck.TcState
import Language.Java.Paragon.TypeCheck.Types
import Language.Java.Paragon.TypeCheck.Locks
import Language.Java.Paragon.TypeCheck.Policy
import Language.Java.Paragon.TypeCheck.Evaluate
--import Language.Java.Paragon.TypeCheck.Interpreter
import qualified Language.Java.Paragon.TypeCheck.Types as TP

import System.FilePath
import System.Directory
import System.Exit
import Control.Monad (when, foldM)
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 :: DirectoryPath -> DirectoryPath -> CompilationUnit () -> IO (CompilationUnit ())
typeCheck currentDir piDir (CompilationUnit _ pkg imps [td]) = do
      finePrint $ "Current dir: " ++ show currentDir
      let (skoTd, skoTy) = skolemTypeDecl td
      e <- runTcCont skoTy $ do
             withEnvFromImps piDir "" allImps $ do
               debug "Import env setup"
               withEnvFromImp currentDir (tdIdentStr skoTd) thisPackage $ do
                 debug "Initial type map completed"
                 tm <- getTypeMap
                 debug $ "Initial type map: " ++ show tm
                 withExpandedNames piDir allImps skoTd $ \fullTd -> do
                    --debug $ "Full AST:\n" ++ prettyPrint fullTd
                    typeCheckTd fullTd
                    -- debug $ "Type checking completed!"
                    return (CompilationUnit () pkg imps [fullTd])
      case e of
        Left str -> do putStrLn $ "\n\n" ++ str
                       exitWith (ExitFailure (-1))
        Right tast -> return tast

   where allImps = defaultImportDecls ++ imps

typeCheck _ _ _ = do putStrLn $ "\n\n" ++ "Encountered multiple type declarations in the same file"
                     exitWith (ExitFailure (-1))

withExpandedNames :: DirectoryPath -> [ImportDecl ()] -> TypeDecl () -> (TypeDecl () -> TcCont r a) -> TcCont r a
withExpandedNames piDir imps td tcbaf = do
  mNames <- buildExpansionMap piDir imps
  -- tm <- getTypeMap
  --debug $ "TypeMap: " ++ show tm
  -- let mNames = buildExpansionMap tm
  let fullTd = expandNames mNames td
  --debug $ "ExpansionMap: " ++ show mNames
  tcbaf fullTd

expandNames :: Data a => Map (Ident ()) [Ident ()] -> a -> a
expandNames mNames = transformBi expandN . transformBi expandCT 
  where expandN :: Name () -> Name ()
        expandN n@(Name _ is@(i:_)) =
            case Map.lookup i mNames of
              Just qi -> Name () $ qi ++ is
              Nothing -> n
        expandN n = n
        expandCT :: ClassType () -> ClassType ()
        expandCT ct@(ClassType _ ias@((i,_as):_)) =
            case Map.lookup i mNames of
              Just qi -> ClassType () $ (zip qi (repeat [])) ++ ias
              Nothing -> ct
        expandCT ct = ct

buildExpansionMap :: DirectoryPath -> [ImportDecl ()] -> TcCont r (Map (Ident ()) [Ident ()])
buildExpansionMap piDir imps = foldM (buildExpMapFromImp piDir) Map.empty imps

buildExpMapFromImp :: DirectoryPath 
                   -> Map (Ident ()) [Ident ()] 
                   -> ImportDecl () 
                   -> TcCont r (Map (Ident ()) [Ident ()])
buildExpMapFromImp piDir em imp@(ImportDecl _ stat (Name _ is) onDemand) = 
    case (stat, onDemand) of
      (False, False) -> do -- Single-type: import pkg.path.TypeName;
          let relative  = pathOf is
              absoluteFile = piDir ++ pSep:relative ++ ".pi"
              className = last is
          checkM (liftIO $ doesFileExist absoluteFile) $
                     "Cannot find interface file for import " ++ prettyPrint imp
          return $ Map.insert className is em
      (False, True) -> do -- On-demand package: import pkg.path.*;
          let relative  = pathOf is
              absoluteDir = piDir ++ pSep:relative ++ [pSep]
          checkM (liftIO $ doesDirectoryExist absoluteDir) $
                     "Cannot find package for import " ++ prettyPrint imp
          names <- liftIO $ getDirectoryContents absoluteDir
          let classNames = 
                  [ Ident () base
                    | name <- names
                    , let (base, extn) = (takeBaseName name, takeExtension name)
                    , extn == ".pi"
                  --  , base /= thisStr 
                  ]
              newMap = Map.fromList (zip classNames (map ((is++) . return) classNames))
          return $ Map.union em newMap
      (True, _) -> fail $ "Static imports not yet implemented"
buildExpMapFromImp _ _ _ = panic (typeCheckerBase ++ ".buildExpMapFromImp") $
                           "AntiQName should not appear in AST being type-checked"

{-
buildExpansionMap :: TypeMap -> Map (Ident ()) [Ident ()]
buildExpansionMap tm = 
  let fs = Map.keys (fields tm)
      (ms, _) = unzip $ Map.keys (methods tm)
      ts = Map.keys (types tm)
      m1 = Map.fromList (zip (fs ++ ms ++ ts) (repeat []))
      pts = Map.assocs (pkgsAndTypes tm)
      ptms = map (second buildExpansionMap) pts
      mps = map (\(i,mp) -> Map.map (i:) mp) ptms
  in foldl Map.union m1 mps
-}
------------------------------------------------------------------
-- Implicitly imported core packages
-- TODO: Not yet used.

defaultImportDecls :: [ImportDecl ()]
defaultImportDecls = []
{-
defaultImportDecls = 
    [ ImportDecl False (Name [Ident "paragon"]) True
    , ImportDecl False (Name [Ident "paragon", Ident "util"]) True
    , ImportDecl False (Name [Ident "paragon", Ident "io"]) True]
-}

thisPackage :: ImportDecl ()
thisPackage = ImportDecl () False (Name () []) True

------------------------------------------------------------------


withEnvFromImps :: DirectoryPath -> String -> [ImportDecl ()] -> TcCont r a -> TcCont r a
withEnvFromImps piDir thisStr is tcba = do
    --debug ("withEnvFromImpsies: " ++ show is) 
--withEnvFromImps dir thisStr (imp:is) =
    withFoldMap (withEnvFromImp piDir thisStr) is $ tcba
--    withEnvFromImp dir thisStr imp . withEnvFromImps dir thisStr is


withEnvFromImp :: DirectoryPath -> String -> (ImportDecl ()) -> TcCont r a -> TcCont r a
-- import java.*;
withEnvFromImp piDir thisStr (ImportDecl _ False (Name _ pkgNames) True) tcba = do
    when (null pkgNames) $
         debug $ "Setting up import from current dir: " ++ show piDir
    --debug $ "Setting up import of: " ++ prettyPrint (Name pkgNames)
    let relative    = pathOf pkgNames
        absoluteDir = piDir ++ pSep:relative ++ [pSep]
    names <- liftIO $ getDirectoryContents absoluteDir
    let classPathsAndNames = [ (absoluteDir ++ nam, takeBaseName nam)
                               | nam <- names 
                               , let (base, extn) = (takeBaseName nam, takeExtension nam)
                               , extn == ".pi"
                               , base /= thisStr ]
    debug $ "Found files: " ++ show classPathsAndNames
    withEnvFromPkg pkgNames classPathsAndNames $ tcba

-- import java.TypeName;
withEnvFromImp piDir _ (ImportDecl _ False (Name _ clsPkgName) False) tcba = do
    --debug $ "Setting up single import of: " ++ show clsPkgName
    let relative     = pathOf clsPkgName
        absoluteFile = piDir ++ pSep:relative ++ ".pi"
        (Ident _ className) = last clsPkgName
        pkgNames = init clsPkgName
    withEnvFromSingleClass pkgNames absoluteFile className $ tcba

-- import static java.TypeName.Ident;
withEnvFromImp _piDir _ (ImportDecl _ True (Name _ _pathToIdent) False) _tcba = do
   fail "Single static import not yet supported" 

-- import static java.TypeName.*;
withEnvFromImp piDir _ (ImportDecl _ True (Name _ clsPkgName) True) tcba = do
   let relative = pathOf clsPkgName
       absoluteFile = piDir ++ pSep:relative ++ ".pi"
       (Ident _ className) = last clsPkgName
       -- pkgNames = init clsPkgName
   withEnvFromSingleClass [] absoluteFile className $ tcba
  
withEnvFromImp _ _ _ _ = panic (typeCheckerBase ++ ".withEnvFromImp") $
                         "AntiQName should not appear in AST being type-checked"


withEnvFromPkg :: [Ident ()] -> [(FilePath, String)] -> TcCont r a -> TcCont r a
withEnvFromPkg [] [] tcba = tcba -- Hack for the "this" package
withEnvFromPkg pkgPath [] tcba = do
  tm <- getTypeMap
  let pkgTm = tm { packages = Map.empty }
  withTypeMap clearToPkgs $
    extendTypeMapP pkgPath pkgTm $
      tcba
withEnvFromPkg pkgPath ((fp,n):pns) tcba =
    withEnvFromClass fp n . 
      withEnvFromPkg pkgPath pns $ tcba

withEnvFromSingleClass :: [Ident ()] -> FilePath -> String -> TcCont r a -> TcCont r a
withEnvFromSingleClass pkgPath fp n tcba = do
  withEnvFromClass fp n .
    withEnvFromPkg pkgPath [] $ tcba

-------------------------------------------------------------------------
-- This is where the really fun stuff happens

withEnvFromClass :: FilePath -> String -> TcCont r a -> TcCont r a
withEnvFromClass fp className tcba = do
  --debug $ "Checking imported class: " ++ className
  ClassDecl _ ms (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 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 ()] -> TcCont r a -> TcCont 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 ()) -> TcCont r a -> TcCont 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 (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 (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 (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 ()] -> TcCont r a -> TcCont 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 ()) -> TcCont r a -> TcCont 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 ()] -> TcCont r a -> TcCont 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 () -> TcCont 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 ()] -> TcCont r a -> TcCont r a
fetchSignatures memberDecls tcba =
    withFoldMap fetchSignature memberDecls $ tcba

unVarDecl :: VarDecl () -> TcCont r (Ident ())
unVarDecl (VarDecl _ (VarId _ i) _) = return i
unVarDecl arvid = fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid


fetchSignature :: MemberDecl () -> TcCont r a -> TcCont 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 (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 () -> TcCont 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 () -> TcCont 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 -> TcCont 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

type DirectoryPath = String
type ClassPath = String
-------------------------------------------------------------------------------------
-- testImportDecl = ImportDecl () False (Name () [Ident () "paragon",Ident () "util"]) True

pSep :: Char
pSep = pathSeparator

-------------------------------------------------------------------------------------
-- Here goes TcTypeDecl.hs
-------------------------------------------------------------------------------------
-- TODO: The module structure needs refactoring

typeCheckTd :: TypeDecl () -> TcCont r ()
typeCheckTd (ClassTypeDecl     _ cdecl) = typeCheckCd cdecl
typeCheckTd (InterfaceTypeDecl _ idecl) = typeCheckId idecl

typeCheckId :: InterfaceDecl () -> TcCont 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 () -> TcCont 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"

--testIt :: Decl () -> MemberDecl ()
--testIt (MemberDecl _ d) = d
--testIt d = error $ "Not member decl: " ++ prettyPrint d

withThisType :: Ident () -> [TypeParam ()] -> TcCont r a -> TcCont 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 True False [] [] emptyTM
        in tm { types = Map.insert i (tps,thisSig) (types tm) }

withThisTypeSigs :: Ident () -> [TypeParam ()] -> TcCont r a -> TcCont r a
withThisTypeSigs i tps tcba = do
  tm <- getTypeMap
  let thisTm = tm { types = Map.empty, packages = Map.empty }
      thisSig = TSig True False [] [] thisTm -- TODO: Include proper values
  extendTypeMapT i tps thisSig $
    tcba

withTypeParam :: TypeParam () -> TcCont r a -> TcCont r a
withTypeParam tp tcba = 
    case tp of
      ActorParam _ i -> do
          let vti = VSig actorT top False True
          withTypeMap (\tm -> 
              tm { actors = Map.insert i (ActorTPVar i) (actors tm),
                   fields = Map.insert i vti (fields tm) }) $ tcba
      PolicyParam _ i -> do
           let vti = VSig policyT top False True
           withTypeMap (\tm ->
              tm { policies = Map.insert i (TcRigidVar i) (policies tm),
                   fields = Map.insert i vti (fields tm) }) $ tcba
      LockStateParam _ i -> do
          let vti = VSig (lockT []) top False True
          withTypeMap (\tm ->
              tm { fields = Map.insert i vti (fields tm) }) $ tcba
      TypeParam _ _i _ -> do
          --withTypeMap (\tm ->
          --    tm { types = Map.insert i ([],Map.empty) (types tm) }) $ 
            tcba

---------------------------------------------------------------
-- Actors

-- TODO: We may have a problem with boot-strapping here.
-- We can stay clear of the problem for now, using careful
-- Paragon coding, but we need to think about it and fix it eventually.
typeCheckActorFields :: [MemberDecl ()] -> TcCont r a -> TcCont r a
typeCheckActorFields = fetchActors
{-    let acts = [ (ms, vd) 
                     | FieldDecl ms (PrimType ActorT) vds <- mDecls 
                     , vd <- vds 
                     , Static `elem` ms -- Only statics exist ??
               ]
-}

---------------------------------------------------------------
-- Locks

typeCheckLockDecls :: [MemberDecl ()] -> TcCont r a -> TcCont r a
typeCheckLockDecls mds tcba = do
  let ls = [ ld | ld@ LockDecl {} <- mds ]
  withFoldMap typeCheckLockDecl ls $ tcba

typeCheckLockDecl :: MemberDecl () -> TcCont r a -> TcCont 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 ()] -> TcCont r a -> TcCont 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 () -> TcCont r a -> TcCont 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 () -> TcCont r a -> TcCont 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 ()] -> TcCont r a -> TcCont 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 () -> TcCont r a -> TcCont 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,
                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 () -> TcCont r a -> TcCont 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 :: TcState -> (Ident (), VarInit ()) -> TcCont r a -> TcCont 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),_) <- runTc (simpleEnv top "policy initializer") st $ tcExp eInit
  check (tyInit == policyT) $
        "Cannot initialize policy field " ++ prettyPrint i ++
        " with non-policy expression " ++ prettyPrint eInit
  withTypeMap (\tm -> tm { policies = Map.insert i tcPol (policies tm) }) $
    tcba
evalAddPolicyInit _ (i, arrInit) _ = 
    fail $ "Cannot initializer policy field " ++ prettyPrint i ++
           " with array " ++ prettyPrint arrInit
-- end policies
------------------------------------------------------------------------------
-- Signatures

typeCheckSignatures :: [MemberDecl ()] -> (TcPolicy -> TcCont r a) -> TcCont r a
typeCheckSignatures mds tcbaf = do
  st <- setupStartState
  withFoldMap (typeCheckSignature st) mds $
    getConstrPol >>= tcbaf

getConstrPol :: TcCont r TcPolicy
getConstrPol = do
  mConstrs <- constrs <$> getTypeMap
  let wPols = map (cWrites . snd) $ Map.elems mConstrs
  return $ foldl join bottom wPols

typeCheckSignature :: TcState -> MemberDecl () -> TcCont r a -> TcCont 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
    debug $ "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,
                 varStatic = Static () `elem` ms,
                 varFinal  = Final  () `elem` ms
               }
  withFoldMap (addField vti) vds $
    tcba

        where addField :: VarFieldSig -> VarDecl () -> TcCont r a -> TcCont 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
    {- We've checked this in evalReturnType already
    when (isRefType ty) $ do 
      mTm <- lookupTypeOfT ty <$> getTypeMap
      case mTm of
        Just _ -> return ()
        Nothing -> fail $ "Unknown type: " ++ prettyPrint ty
    -}
    -- 2. Typecheck and evaluate policy modifiers
    withFoldMap withParam ps $ checkPolicyMods st ms 
      "typeCheckSignature: At most one return/write modifier allowed per method"
    -- 3. Typecheck and evaluate lock modifiers
    lms <- checkLMMods ms
    es  <- checkExpectsMods ms
    -- 4. Check parameter types and policy modifiers
    (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps
    -- 5. Typecheck and evaluate exception signatures
    xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns
    -- 6. Add signature to typemap
    rPol <- getReturnPolicy ms pPols
    wPol <- getWritePolicy ms
    let mti = 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. Typecheck and evaluate policy modifiers
    withFoldMap withParam ps $ checkPolicyMods st ms 
      "typeCheckSignature: At most one return/write modifier allowed per constructor"
    -- 2. Typecheck and evaluate lock modifiers
    lms <- checkLMMods ms
    es  <- checkExpectsMods ms
    -- 3. Check parameter types and policy modifiers
    (pTs,pPols) <- unzip <$> mapM (typeCheckParam st) ps
    -- 4. Typecheck and evaluate exception signatures
    xSigs <- withFoldMap withParam ps $ mapM (typeCheckExnSig st) exns
    -- 5. Add signature to typemap
    wPol <- getWritePolicy ms
    let cti = 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 () -> TcCont r a -> TcCont r a
withParam (FormalParam _ _ _ _ (VarId _ i)) = 
    withTypeMap $ \tm -> 
        tm { fields = Map.insert i (VSig err err err err) (fields tm) }
            -- TODO: UUUUGLY!
            where err = error $ "Use of parameter " ++ prettyPrint i ++ " directly in modifier" 
withParam (FormalParam _ _ _ _ arvid) =
    fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid


typeCheckExnSig :: TcState -> ExceptionSpec () -> TcCont r (TcType, ExnSig)
typeCheckExnSig st (ExceptionSpec _ ms xT) = do
  withErrCtxt ("When checking signature for declared exception " ++ prettyPrint xT ++ ":\n") $ do
    ty <- TP.TcRefT <$> evalSrcRefType xT
    {-- Check that type exists - 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 :: TcState -> [Modifier ()] -> String -> TcCont 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 ()] -> TcCont 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 ()] -> TcCont r [TcLock]
checkExpectsMods ms = do
  let es = concat [ l | Expects _ l <- ms ]
  mapM evalLock es

typeCheckParam :: TcState -> FormalParam () -> TcCont r (TcType, TcPolicy)
typeCheckParam st (FormalParam _ ms t _ (VarId _ i)) = do
  withErrCtxt ("When checking signature of parameter " ++ prettyPrint i ++ ":\n") $ do
    -- 1. Check parameter type
    ty <- evalSrcType t
    -- 2. Typecheck and evaluate policy modifier
    checkPolicyMods st ms 
       "typeCheckSignature: At most one read modifier allowed per parameter"
    rPol <- getParamPolicy i ms
    return (ty, rPol)
typeCheckParam _ (FormalParam _ _ _ _ arvid) =
    fail $ "Deprecated array syntax not supported: " ++ prettyPrint arvid

typeCheckPolicyMod :: TcState -> Policy () -> TcCont r ()
typeCheckPolicyMod st polExp = do
  -- tm <- getTypeMap
  -- debug $ show tm
  -- debug $ "typeCheckPolicyMod " ++ show polExp
  ((ty, _pol), cs) <- runTc (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 ()] -> TcCont 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 -> TcState -> Block () -> TcCont r TcState
typeCheckInitDecl lim st bl = do
    tm <- getTypeMap
    (newSt,cs) <- runTc (simpleEnv lim $ "initializer block") st $
                      addBranchPCList (Map.keys (fields tm)) $ do
                        tcBlock bl
                        getState
    solve cs
    return newSt

------------------------------------------------------------------------------
-- Bodies

typeCheckMemberDecls :: TcPolicy -> TcPolicy -> [MemberDecl ()] -> TcCont r ()
typeCheckMemberDecls sLim cLim ms = do
  st <- setupStartState
  mapM_ (typeCheckMemberDecl sLim cLim st) ms

typeCheckMemberDecl :: TcPolicy -> TcPolicy -> TcState -> MemberDecl () -> TcCont 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 -> TcState -> MemberDecl () -> TcCont 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 -> TcState -> VarDecl () -> TcCont 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) <- runTc (simpleEnv lim $ "field initializer " ++ prettyPrint e) st $ do
                  (ty, pol) <- tcExp e
                  checkM (liftCont $ 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) <- runTc (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 :: TcState -> MemberDecl () -> TcCont r ()
typeCheckMethodDecl st (MethodDecl _ _ tps _ i ps _ mb) = do
  -- Lookup the correct function signature
  -- debug $ "Type-checking method " ++ prettyPrint i
  withErrCtxt ("When checking body of method " ++ prettyPrint i ++ ":\n") $ do
  withFoldMap withTypeParam tps $ do
  tysPs <- mapM evalSrcType $ [ t | FormalParam _ _ t _ _ <- ps ]
  Just (_, MSig tyRet pRet pPars pWri expLs lMods xSigs) <- 
      Map.lookup (i,tysPs) . methods <$> getTypeMap

  -- Setup the environment in which to check the body
  let parVtis = [ (iP, VSig t p False (isFinal ms)) |
                    (FormalParam _ ms _ _ (VarId _ iP), t, p) <- zip3 ps tysPs pPars ]
      pars = map fst parVtis
      exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
      exnLMods = map (second exnMods) xSigs
      parEnts = [ (VarEntity $ Name () [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 = TcEnv {
              vars = Map.fromList parVtis,
              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 ((Name () . return) *** (\aid -> AI aid Stable)) parAids
      parSt = st { actorSt = parAMap `Map.union` actorSt st }

  -- This little thing is what actually checks the body
  (endSt,cs) <- runTc env parSt $ tcMethodBody mb >> getState
  -- ... and then we need to check the end result
  solve cs
  check (lMods `models` lockMods endSt) $ 
              "Declared lock modifiers not general enough: " ++ show lMods
  mapM_ (checkExnMods endSt) exnLMods

typeCheckMethodDecl _ md = panic (typeCheckerBase ++ ".typeCheckMethodDecl") $
                            "Applied to non-method decl " ++ show md


typeCheckConstrDecl :: TcState -> MemberDecl () -> TcCont 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 parVtis = [ (i, VSig t p False (isFinal ms)) |
                    (FormalParam _ ms _ _ (VarId _ i), t, p) <- zip3 ps tysPs pPars ]
      pars = map fst parVtis
      exnPols = map (second $ \es -> (exnReads es, exnWrites es)) xSigs
      exnLMods = map (second exnMods) xSigs
      parEnts = [ VarEntity $ Name () [i] | i <- pars ]
      exnEnts = [ ExnEntity t | t <- map fst xSigs ]
      -- Assigning to non-static fields of 'this' in a constructor is a local write
      fieEnts = concat [ [ThisFieldEntity i,VarEntity (Name () [i])] 
                             | (i, 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 = TcEnv {
              vars = Map.fromList parVtis,
              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 ((Name () . return) *** (\aid -> AI aid Stable)) parAids
      parSt = st { actorSt = parAMap `Map.union` actorSt st }

  -- This little thing is what actually checks the body
  (endSt,cs) <- runTc env parSt $ tcConstrBody cb >> getState

  -- ... and then we need to check the end result
  solve cs
  check (lMods `models` lockMods endSt) $ 
              "Declared lock modifiers not general enough: " ++ show lMods
  mapM_ (checkExnMods endSt) exnLMods

typeCheckConstrDecl _ md = panic (typeCheckerBase ++ ".typeCheckConstrDecl") $
                            "Applied to non-constructor decl " ++ show md

aliasIfActor :: (Ident (), TcType) -> TcCont r [(Ident (), ActorId)]
aliasIfActor (i, ty)
    | ty == actorT = aliasActorId >>= \aid -> return [(i, aid)]
    | otherwise = return []
                

checkExnMods :: TcState -> (TcType, LockMods) -> TcCont 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 () -> Tc r ()
tcMethodBody (MethodBody _ mBlock) = maybeM mBlock $ tcBlock

tcConstrBody :: ConstructorBody () -> Tc 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 [(i, args)], zip tps args)

skolemParam :: TypeParam () -> TcTypeArg
skolemParam tp = case tp of
                   TypeParam _ i _    -> TcActualType (TcClsRefT (TcClassT [(i,[])]))
                   ActorParam  _ i    -> TcActualActor (ActorTPVar i)
                   PolicyParam _ i    -> TcActualPolicy (TcRigidVar i)
                   LockStateParam _ i -> TcActualLockState [TcLockVar i]

isPolicyMod, isLockStateMod :: Modifier () -> Bool
isPolicyMod m =
    case m of
      Reads _ _ -> True
      Writes _ _ -> True
      _ -> False
isLockStateMod m = 
    case m of
      Expects _ _ -> True
      Opens   _ _ -> True
      Closes  _ _ -> True
      _ -> False


--debug :: String -> TcCont r ()
--debug str = liftIO $ finePrint $ "DEBUG: " ++ str