Base.hs

-- |
-- Module      :  Cryptol.ModuleSystem.Base
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This is the main driver---it provides entry points for the
-- various passes.

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# Language DisambiguateRecordFields #-}
{-# LANGUAGE BlockArguments #-}

module Cryptol.ModuleSystem.Base where

import qualified Control.Exception as X
import Control.Monad (unless,when,forM)
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Maybe (fromMaybe, maybeToList)
import Data.List(sortBy)
import qualified Data.List.NonEmpty as NE
import Data.List.NonEmpty (NonEmpty(..))
import Data.Function(on)
import Data.Monoid ((<>),Endo(..), Any(..))
import qualified Data.Text as T
import Data.Text.Encoding (decodeUtf8')
import System.Directory
  (doesFileExist, canonicalizePath, makeRelativeToCurrentDirectory)
import System.FilePath ( addExtension
                       , dropExtension
                       , isAbsolute
                       , joinPath
                       , splitDirectories
                       , (</>)
                       , normalise
                       , takeFileName
                       )
import qualified System.IO.Error as IOE
import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS

import Prelude ()
import Prelude.Compat hiding ( (<>) )



import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..),nameIdent)
import Cryptol.ModuleSystem.Env ( DynamicEnv(..),FileInfo(..),fileInfo
                                , lookupModule
                                , lookupTCEntity
                                , LoadedModuleG(..), lmInterface
                                , meCoreLint, CoreLint(..)
                                , ModContext(..), ModContextParams(..)
                                , ModulePath(..), modulePathLabel
                                , EvalForeignPolicy (..)
                                , PassName(..), DebugOpts(..))
import           Cryptol.Eval.FFI.ForeignSrc
import qualified Cryptol.Eval                 as E
import qualified Cryptol.Eval.Concrete as Concrete
import           Cryptol.Eval.Concrete (Concrete(..))
import           Cryptol.Eval.FFI
import qualified Cryptol.ModuleSystem.NamingEnv as R
import qualified Cryptol.ModuleSystem.Renamer as R
import qualified Cryptol.Parser               as P
import qualified Cryptol.Parser.Unlit         as P
import Cryptol.Parser.AST as P
import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))
import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards
  ( expandPropGuards, expandTopDecl, runExpandPropGuardsM )
import Cryptol.Parser.NoInclude (removeIncludesModule)
import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
import qualified Cryptol.TypeCheck     as T
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import qualified Cryptol.Eval.FFI.Error as FFI

import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                           , preludeReferenceName, interactiveName, modNameChunks
                           , modNameIsNormal
                           , modNamesMatch, Namespace(NSModule) )
import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
import Cryptol.Utils.Benchmark

import Cryptol.Prelude ( preludeContents, floatContents, arrayContents
                       , suiteBContents, primeECContents, preludeReferenceContents )
import Cryptol.Transform.MonoValues (rewModule)


-- Renaming --------------------------------------------------------------------

rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a
rename modName env m = do
  ifaces <- getIfaces
  (res,ws) <- liftSupply $ \ supply ->
    let info = R.RenamerInfo
                 { renSupply  = supply
                 , renContext = TopModule modName
                 , renEnv     = env
                 , renIfaces  = ifaces
                 }
    in
    case R.runRenamer info m of
      (Right (a,supply'),ws) -> ((Right a,ws),supply')
      (Left errs,ws)         -> ((Left errs,ws),supply)

  renamerWarnings ws
  case res of
    Right r   -> return r
    Left errs -> renamerErrors errs

-- | Rename a module in the context of its imported modules.
renameModule :: P.Module PName -> ModuleM R.RenamedModule
renameModule m = rename (thing (mName m)) mempty (R.renameModule m)

renameImpNameInCurrentEnv :: P.ImpName PName -> ModuleM (P.ImpName Name)
renameImpNameInCurrentEnv (P.ImpTop top) =
 do ok <- isLoaded top
    if ok then
      pure (P.ImpTop top)
    else
      fail ("Top-level module not loaded: " ++ show (pp top))
renameImpNameInCurrentEnv (P.ImpNested pname) =
 do env <- getFocusedEnv
    case R.lookupListNS NSModule pname (mctxNames env) of
      [] -> do
        fail ("Undefined submodule name: " ++ show (pp pname))
      _:_:_ -> do
        fail ("Ambiguous submodule name: " ++ show (pp pname))
      [n] -> pure (P.ImpNested n)

-- NoPat -----------------------------------------------------------------------

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
noPat a = do
  let (a',errs) = removePatterns a
  unless (null errs) (noPatErrors errs)
  return a'

-- ExpandPropGuards ------------------------------------------------------------

-- | Run the expandPropGuards pass.
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards a =
  case ExpandPropGuards.runExpandPropGuardsM $ ExpandPropGuards.expandPropGuards a of
    Left err -> expandPropGuardsError err
    Right a' -> pure a'

-- | Run the expandPropGuards pass on a group of top-level declarations.
expandPropGuardsDecls :: [P.TopDecl PName] -> ModuleM [P.TopDecl PName]
expandPropGuardsDecls ds =
  case ExpandPropGuards.runExpandPropGuardsM $
         concat <$> mapM ExpandPropGuards.expandTopDecl ds of
    Left err  -> expandPropGuardsError err
    Right ds' -> pure ds'

-- Parsing ---------------------------------------------------------------------

-- | Parse a module and expand includes
-- Returns a fingerprint of the module, and a set of dependencies due
-- to `include` directives.
parseModule ::
  ModulePath ->
  ModuleM (Fingerprint, MapS.Map FilePath Fingerprint, [P.Module PName])
parseModule path = do
  getBytes <- getByteReader

  bytesRes <- case path of
                InFile p -> io (X.try (getBytes p))
                InMem _ bs -> pure (Right bs)

  bytes <- case bytesRes of
    Right bytes -> return bytes
    Left exn ->
      case path of
        InFile p
          | IOE.isDoesNotExistError exn -> cantFindFile p
          | otherwise                   -> otherIOError p exn
        InMem p _ -> panic "parseModule"
                       [ "IOError for in-memory contents???"
                       , "Label: " ++ show p
                       , "Exception: " ++ show exn ]

  let fp = fingerprint bytes
  txt <- case decodeUtf8' bytes of
    Right txt -> return $! T.replace "\r\n" "\n" txt
    Left e    -> badUtf8 path fp e


  let cfg = P.defaultConfig
              { P.cfgSource  = case path of
                                 InFile p -> p
                                 InMem l _ -> l
              , P.cfgPreProc = P.guessPreProc (modulePathLabel path)
              }

  case P.parseModule cfg txt of
    Right pms ->
      do (pm1,deps) <-
           case path of
             InFile p ->
               do r <- getByteReader
                  (mo,d) <- unzip <$>
                    forM pms \pm ->
                    do mb <- io (removeIncludesModule r p pm)
                       case mb of
                         Right ok -> pure ok
                         Left err -> noIncludeErrors err
                  pure (mo, MapS.unions d)

             {- We don't do "include" resolution for in-memory files
                because at the moment the include resolution pass requires
                the path to the file to be known---this is used when
                looking for other inlcude files.  This could be
                generalized, but we can do it once we have a concrete use
                case as it would help guide the design. -}
             InMem {} -> pure (pms, MapS.empty)

{-
         case path of
           InFile {} -> io $ print (T.vcat (map T.pp pm1))
           InMem {} -> pure ()
--}
         fp `seq` return (fp, deps, pm1)

    Left err -> moduleParseError path fp err


-- Top Level Modules and Signatures --------------------------------------------


-- | Load a module by its path.
loadModuleByPath ::
  Bool {- ^ evaluate declarations in the module -} ->
  FilePath -> ModuleM T.TCTopEntity
loadModuleByPath eval path = do
  foundPath <- findFile path
  (fp, deps, pms) <- parseModule (InFile foundPath)
  extras <- case [ thing (P.mName pm) | pm <- pms
                                      , modNameIsNormal (thing (P.mName pm)) ] of
              n : _ -> checkPathLayout foundPath n
              []    -> pure Nothing
  withPrependedSearchPath (maybeToList extras) $
    last <$>
    forM pms \pm ->
    do let n = thing (P.mName pm)

       -- Check whether this module name has already been loaded from a
       -- different file
       env <- getModuleEnv
       -- path' is the resolved, absolute path, used only for checking
       -- whether it's already been loaded
       path' <- io (canonicalizePath foundPath)

       case lookupTCEntity n env of
         -- loadModule will calculate the canonical path again
         Nothing ->
           loadModuleAndDeps eval False
             (FromModule n) (InFile foundPath) fp deps pm
         Just lm
          | path' == loaded -> return (lmData lm)
          | otherwise       -> duplicateModuleName n path' loaded
          where loaded = lmModuleId lm

{- | Check whether the file's parent directories match the parent chunks of
the module's hierarchical name.  If they do, return the directory prefix
that should be prepended to the search path so that imports from a sibling
can be resolved.  If they do not, emit a warning and return 'Nothing',
leaving the search path alone. -}
checkPathLayout :: FilePath -> ModName -> ModuleM (Maybe FilePath)
checkPathLayout fp mname =
  case stripParentSuffix (modNameChunks mname)
                         (splitDirectories (dropExtension (normalise fp))) of
    Just root -> pure (Just (if null root then "." else root))
    Nothing   ->
      do relFp <- io (makeRelativeToCurrentDirectory fp)
         withLogger logPutStrLn $
           "[warning] " ++ show relFp ++ " does not match module name " ++
           pretty mname
         pure Nothing
  where
  stripParentSuffix chunks p =
    case (reverse chunks, reverse p) of
      -- We just check parent directories, not file name.
      (_ : rcs, _ : rds) -> go rds rcs
      _                  -> Nothing
    where
    go rest cs =
      case cs of
        []     -> Just (joinPath (reverse rest))
        c : cs' ->
          case rest of
            d : ds | d == c -> go ds cs'
            _               -> Nothing


-- | Load a module, unless it was previously loaded.
loadModuleFrom ::
  Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.TCTopEntity)
loadModuleFrom quiet isrc =
  do let n = importedModule isrc
     mb <- getLoadedMaybe n
     case mb of
       Just m -> return (lmFilePath m, lmData m)
       Nothing ->
         do path <- findModule isrc n
            errorInFile path $
              do (fp, deps, pms) <- parseModule path
                 ms <- mapM (loadModuleAndDeps True quiet isrc path fp deps) pms
                 return (path,last ms)

-- | Load dependencies, typecheck, and add to the eval environment.
loadModuleAndDeps ::
  Bool {- ^ evaluate declarations in the module -} ->
  Bool {- ^ quiet mode: true suppresses the "loading module" message -} ->
  ImportSource ->
  ModulePath ->
  Fingerprint ->
  MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} ->
  P.Module PName ->
  ModuleM T.TCTopEntity
loadModuleAndDeps eval quiet isrc path fp incDeps pm0 =
  loading isrc $
  do let pm = addPrelude pm0
     impDeps <- loadDeps pm
     fst <$> doLoadModule eval quiet isrc path fp incDeps pm impDeps

-- | Typecheck and add to the eval environment.
doLoadModule ::
  Bool {- ^ evaluate declarations in the module -} ->
  Bool {- ^ quiet mode: true suppresses the "loading module" message -} ->
  ImportSource ->
  ModulePath ->
  Fingerprint ->
  MapS.Map FilePath Fingerprint {- ^ `include` dependencies -} ->
  P.Module PName ->
  Set ModName ->
  ModuleM (T.TCTopEntity, FileInfo)
doLoadModule eval quiet isrc path fp incDeps pm impDeps =
  do let what = case P.mDef pm of
                  P.InterfaceModule {} -> "interface module"
                  _                    -> "module"

     unless quiet $ withLogger logPutStrLn
       ("Loading " ++ what ++ " " ++ pretty (P.thing (P.mName pm)))


     (nameEnv,tcm,renMod) <- checkModule isrc pm

     -- extend the eval env, unless a functor.
     tbl <- Concrete.primTable <$> getEvalOptsAction
     let ?evalPrim = \i -> Right <$> Map.lookup i tbl
     callStacks <- getCallStacks
     let ?callStacks = callStacks
     let shouldEval =
           case tcm of
             T.TCTopModule m | eval && not (T.isParametrizedModule m) -> Just m
             _ -> Nothing

     foreignSrc <- case shouldEval of
                      Just m ->
                        do fsrc <- evalForeign m
                           modifyEvalEnv (E.moduleEnv Concrete m)
                           pure fsrc
                      Nothing -> pure Nothing

     let fi = fileInfo fp incDeps impDeps foreignSrc
     saveRen <- getSaveRenamed
     loadedModule path fi nameEnv foreignSrc tcm $!
       if saveRen then Just renMod else Nothing

     return (tcm, fi)

  where
  evalForeign tcm
    | not (null foreignFs) =
      ffiLoadErrors (T.mName tcm) (map FFI.FFIInFunctor foreignFs)
    | not (null dups) =
      ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)
    | null foreigns = pure Nothing
    | otherwise =
      getEvalForeignPolicy >>= \case
        AlwaysEvalForeign -> doEvalForeign (ffiLoadErrors (T.mName tcm))
        PreferEvalForeign -> doEvalForeign \errs ->
          withLogger logPrint $
            hang
              ("[warning] Could not load all foreign implementations for module"
                <+> pp (T.mName tcm) <.> colon) 4 $
              vcat (map pp errs)
              $$ "Fallback cryptol implementations will be used if available"
        NeverEvalForeign -> pure Nothing

    where foreigns  = findForeignDecls tcm
          foreignFs = T.findForeignDeclsInFunctors tcm
          dups      = [ d | d@(_ :| _ : _) <- NE.groupBy ((==) `on` nameIdent)
                                            $ sortBy (compare `on` nameIdent)
                                            $ map fst foreigns ]
          doEvalForeign handleErrs =
            case path of
              InFile p -> io (loadForeignSrc p) >>=
                \case

                  Right fsrc -> do
                    unless quiet $
                      case getForeignSrcPath fsrc of
                        Just fpath -> withLogger logPutStrLn $
                          "Loading dynamic library " ++ takeFileName fpath
                        Nothing -> pure ()
                    (errs, ()) <-
                      modifyEvalEnvM (evalForeignDecls fsrc foreigns)
                    unless (null errs) $
                      handleErrs errs
                    pure $ Just fsrc

                  Left err -> do
                    handleErrs [err]
                    pure Nothing

              InMem m _ -> panic "doLoadModule"
                ["Can't find foreign source of in-memory module", m]

-- | Rewrite an import declaration to be of the form:
--
-- > import foo as foo [ [hiding] (a,b,c) ]
fullyQualified :: P.Import -> P.Import
fullyQualified i = i { iAs = Just (thing (iModule i)) }

moduleFile :: ModName -> String -> FilePath
moduleFile n = addExtension (joinPath (modNameChunks n))


-- | Discover a module.
findModule :: ImportSource -> ModName -> ModuleM ModulePath
findModule isrc n = do
  paths <- getSearchPath
  loop (possibleFiles paths)
  where
  loop paths = case paths of

    path:rest -> do
      b <- io (doesFileExist path)
      if b then return (InFile path) else loop rest

    [] -> handleNotFound

  handleNotFound =
    case n of
      m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
        | m == floatName   -> pure (InMem "Float" floatContents)
        | m == arrayName   -> pure (InMem "Array" arrayContents)
        | m == suiteBName  -> pure (InMem "SuiteB" suiteBContents)
        | m == primeECName -> pure (InMem "PrimeEC" primeECContents)
        | m == preludeReferenceName -> pure (InMem "Cryptol::Reference" preludeReferenceContents)
      _ -> moduleNotFound isrc n =<< getSearchPath

  -- generate all possible search paths
  possibleFiles paths = do
    path <- paths
    ext  <- P.knownExts
    return (path </> moduleFile n ext)

-- | Discover a file. This is distinct from 'findModule' in that we
-- assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath
findFile path
  | isAbsolute path =
    do -- No search path checking for absolute paths
       b <- io (doesFileExist path)
       if b then return path else cantFindFile path
  | otherwise =
    do paths <- getSearchPath
       loop (possibleFiles paths)
       where
       loop paths = case paths of
                      path' : rest ->
                        do b <- io (doesFileExist path')
                           if b then return (normalise path') else loop rest
                      [] -> cantFindFile path
       possibleFiles paths = map (</> path) paths

-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: P.Module PName -> P.Module PName
addPrelude m
  | preludeName == P.thing (P.mName m) = m
  | preludeName `elem` importedMods    = m
  | otherwise                          = m { mDef = newDef }
  where
  newDef =
    case mDef m of
      NormalModule ds -> NormalModule (P.DImport prel : ds)
      FunctorInstance f as ins k -> FunctorInstance f as ins k
      InterfaceModule s -> InterfaceModule s { sigImports = P.SigImport prel
                                             : sigImports s }
      ModuleAlias t -> ModuleAlias t

  importedMods  = map (P.thing . P.iModule . P.thing) (P.mImports m)
  prel = P.Located
    { P.srcRange = emptyRange
    , P.thing    = P.Import
      { iModule  = Located emptyRange (P.ImpTop preludeName)
      , iAs      = Nothing
      , iSpec    = Nothing
      , iInst    = Nothing
      , iDoc     = Nothing
      }
    }

-- | Load the dependencies of a module into the environment.
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName)
loadDeps m =
  do let ds = findDeps m
     mapM_ (loadModuleFrom False) ds
     pure (Set.fromList (map importedModule ds))

-- | Find all imports in a module.
findDeps :: P.ModuleG mname name -> [ImportSource]
findDeps m = appEndo (snd (findDeps' m)) []

findDepsOfModule :: ModName -> ModuleM (ModulePath, FileInfo)
findDepsOfModule m =
  do mpath <- findModule (FromModule m) m
     findDepsOf mpath

findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
findDepsOf mpath' =
  do mpath <- case mpath' of
                InFile file -> InFile <$> io (canonicalizePath file)
                InMem {}    -> pure mpath'
     (fi, _) <- parseWithDeps mpath
     pure (mpath, fi)

{- | Parse the given module path and find its dependencies.
The reason we return a list here, is that sometime files may
contain multiple modules (e.g., due to desugaring `parameter` blocks
in functors. -}
parseWithDeps ::
  ModulePath ->
  ModuleM (FileInfo, [(Module PName, [ImportSource])])
parseWithDeps mpath =
  do (fp, incs, ms) <- parseModule mpath
     let ms' = map addPrelude ms
         depss = map findDeps' ms'
     let (anyF,imps) = mconcat depss
     fpath <- if getAny anyF
                then do mb <- io case mpath of
                                   InFile path -> foreignLibPath path
                                   InMem {}    -> pure Nothing
                        pure case mb of
                               Nothing -> Map.empty
                               Just (fpath, exists) ->
                                 Map.singleton fpath exists
                else pure Map.empty
     pure
       ( FileInfo
           { fiFingerprint = fp
           , fiIncludeDeps = incs
           , fiImportDeps  = Set.fromList (map importedModule (appEndo imps []))
           , fiForeignDeps = fpath
           }
       , zip ms' $ map ((`appEndo` []) . snd) depss
       )

-- | Find the set of top-level modules imported by a module.
findModuleDeps :: P.ModuleG mname name -> Set P.ModName
findModuleDeps = Set.fromList . map importedModule . findDeps

-- | A helper `findDeps` and `findModuleDeps` that actually does the searching.
findDeps' :: P.ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' m =
  case mDef m of
    NormalModule ds -> mconcat (map depsOfDecl ds)
    FunctorInstance f as _ _k ->
      let fds = loadImpName FromModuleInstance f
          ads = case as of
                  DefaultInstArg a -> loadInstArg a
                  DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds)
                  NamedInstArgs args -> mconcat (map loadNamedInstArg args)
      in fds <> ads
    InterfaceModule s -> mconcat (map loadSigImp (sigImports s))
    ModuleAlias t -> loadImpName FromModuleAlias t
  where
  loadI i = (mempty, Endo (i:))

  loadImpName src l =
    case thing l of
      ImpTop f -> loadI (src l { thing = f })
      _        -> mempty

  loadImpD li = loadImpName (FromImport . new) (thing . iModule <$> li)
    where new i = i { thing = (thing li) { iModule = i } }

  loadIfaceParam mp = loadImpName FromSigImport (mpSignature mp)

  loadSigImp si =
    case si of
      P.SigImport li     -> loadImpD li
      P.SigIfaceImport mp -> loadIfaceParam mp

  loadNamedInstArg (ModuleInstanceNamedArg _ f) = loadInstArg f
  loadInstArg f =
    case thing f of
      ModuleArg mo -> loadImpName FromModuleInstance f { thing = mo }
      _            -> mempty

  depsOfDecl d =
    case d of
      DImport li -> loadImpD li

      DModule TopLevel { tlValue = NestedModule nm } -> findDeps' nm

      DModParam mo -> loadImpName FromSigImport s
        where s = mpSignature mo

      Decl dd -> depsOfDecl' (tlValue dd)

      _ -> mempty

  depsOfDecl' d =
    case d of
      DLocated d' _ -> depsOfDecl' d'
      DBind b ->
        case thing (bDef b) of
          DForeign {} -> (Any True, mempty)
          _ -> mempty
      _ -> mempty






-- Type Checking ---------------------------------------------------------------

-- | Typecheck a single expression, yielding a renamed parsed expression,
-- typechecked core expression, and a type schema.
checkExpr :: P.Expr PName -> ModuleM (P.Expr Name,T.Expr,T.Schema)
checkExpr e = do

  fe <- getFocusedEnv
  let params = mctxParams fe
      decls  = mctxDecls fe
      names  = mctxNames fe

  -- run NoPat
  npe <- noPat e

  -- rename the expression with dynamic names shadowing the opened environment
  re  <- rename interactiveName names (R.rename npe)

  -- merge the dynamic and opened environments for typechecking
  prims <- getPrimMap
  let act  = TCAction { tcAction = T.tcExpr, tcLinter = exprLinter
                      , tcPrims = prims }
  (te,s) <- typecheck act re params decls

  return (re,te,s)

-- | Typecheck a group of declarations.
--
-- INVARIANT: This assumes that NoPat has already been run on the declarations.
checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup], Map.Map Name T.TySyn)
checkDecls ds = do
  fe <- getFocusedEnv
  let params = mctxParams fe
      decls  = mctxDecls  fe
      names  = mctxNames  fe

  epgds <- expandPropGuardsDecls ds

  (declsEnv,rds) <- rename interactiveName names
                  $ R.renameTopDecls epgds
  prims <- getPrimMap
  let act  = TCAction { tcAction = T.tcDecls, tcLinter = declsLinter
                      , tcPrims = prims }
  (ds',tyMap) <- typecheck act rds params decls
  return (declsEnv,ds',tyMap)

-- | Generate the primitive map. If the prelude is currently being loaded, this
-- should be generated directly from the naming environment given to the renamer
-- instead.
getPrimMap :: ModuleM PrimMap
getPrimMap  =
  do env <- getModuleEnv
     let mkPrims = ifacePrimMap . lmInterface
         mp `alsoPrimFrom` m =
           case lookupModule m env of
             Nothing -> mp
             Just lm -> mkPrims lm <> mp

     case lookupModule preludeName env of
       Just prel -> return $ mkPrims prel
                            `alsoPrimFrom` floatName
       Nothing -> panic "Cryptol.ModuleSystem.Base.getPrimMap"
                  [ "Unable to find the prelude" ]

-- | Typecheck a single module.
-- Note: we assume that @include@s have already been processed
checkModule ::
  ImportSource                      {- ^ why are we loading this -} ->
  P.Module PName                    {- ^ module to check -} ->
  ModuleM (R.NamingEnv,T.TCTopEntity, Module Name)
checkModule isrc m = do

  dbgOpts <- getDebugOpts
  let prelOk = dbgIncludePrelude dbgOpts || thing (mName m) /= preludeName
      setting = if dbgIncludePrelude dbgOpts then id else T.debugHidePreludeNames
      dump nm dbg =
        when (prelOk && (nm `Set.member` dbgDumpAfter dbgOpts))
          (io (print (setting (T.debugShowUniques dbg))))

  dump PassParser (pp m) 

  -- check that the name of the module matches expectations
  let nm = importedModule isrc
  unless (modNamesMatch nm (thing (P.mName m)))
         (moduleNameMismatch nm (mName m))

  -- remove pattern bindings
  npm <- noPat m
  dump PassNoPat (pp npm) 

  -- run expandPropGuards
  epgm <- expandPropGuards npm
  dump PassPropGuards (pp epgm)

  -- rename everything
  renMod <- renameModule epgm
  dump PassRename (pp renMod)

  -- when generating the prim map for the typechecker, if we're checking the
  -- prelude, we have to generate the map from the renaming environment, as we
  -- don't have the interface yet.
  prims <- if thing (mName m) == preludeName
              then return (R.toPrimMap (R.rmDefines renMod))
              else getPrimMap

  -- typecheck
  let act = TCAction { tcAction = T.tcModule
                     , tcLinter = tcTopEntitytLinter (P.thing (P.mName m))
                     , tcPrims  = prims }


  tcm <- typecheck act (R.rmModule renMod) NoParams (R.rmImported renMod)
  dump PassTC (pp tcm)

  rewMod <- case tcm of
              T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)
              T.TCTopSignature {} -> pure tcm
  dump PassREW (pp tcm)

  let nameEnv = case tcm of
                  T.TCTopModule mo -> T.mInScope mo
                  -- Name env for signatures does not change after typechecking
                  T.TCTopSignature {} -> mInScope (R.rmModule renMod)
  pure (nameEnv,rewMod, R.rmModule renMod)

data TCLinter o = TCLinter
  { lintCheck ::
      o -> T.InferInput ->
                    Either (Range, TcSanity.Error) [TcSanity.ProofObligation]
  , lintModule :: Maybe P.ModName
  }


exprLinter :: TCLinter (T.Expr, T.Schema)
exprLinter = TCLinter
  { lintCheck = \(e',s) i ->
      case TcSanity.tcExpr i e' of
        Left err     -> Left err
        Right (s1,os)
          | TcSanity.SameIf os' <- TcSanity.same s s1 ->
                                        Right (map T.tMono os' ++ os)
          | otherwise -> Left ( fromMaybe emptyRange (getLoc e')
                              , TcSanity.TypeMismatch "exprLinter" s s1
                              )
  , lintModule = Nothing
  }

declsLinter :: TCLinter ([ T.DeclGroup ], a)
declsLinter = TCLinter
  { lintCheck = \(ds',_) i -> case TcSanity.tcDecls i ds' of
                                Left err -> Left err
                                Right os -> Right os

  , lintModule = Nothing
  }

moduleLinter :: P.ModName -> TCLinter T.Module
moduleLinter m = TCLinter
  { lintCheck   = \m' i -> case TcSanity.tcModule i m' of
                            Left err -> Left err
                            Right os -> Right os
  , lintModule  = Just m
  }

tcTopEntitytLinter :: P.ModName -> TCLinter T.TCTopEntity
tcTopEntitytLinter m = TCLinter
  { lintCheck   = \m' i -> case m' of
                             T.TCTopModule mo ->
                               lintCheck (moduleLinter m) mo i
                             T.TCTopSignature {} -> Right []
                                -- XXX: what can we lint about module interfaces
  , lintModule  = Just m
  }


type Act i o = i -> T.InferInput -> IO (T.InferOutput o)

data TCAction i o = TCAction
  { tcAction :: Act i o
  , tcLinter :: TCLinter o
  , tcPrims  :: PrimMap
  }

typecheck ::
  (Show i, Show o, HasLoc i) =>
  TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck act i params env = do

  let range = fromMaybe emptyRange (getLoc i)
  input <- genInferInput range (tcPrims act) params env
  out   <- io (tcAction act i input)

  case out of

    T.InferOK nameMap warns seeds supply' o ->
      do setNameSeeds seeds
         setSupply supply'
         typeCheckWarnings nameMap warns
         menv <- getModuleEnv
         case meCoreLint menv of
           NoCoreLint -> return ()
           CoreLint   -> case lintCheck (tcLinter act) o input of
                           Right as ->
                             let ppIt l = mapM_ (logPrint l . T.pp)
                             in withLogger ppIt (TcSanity.onlyNonTrivial as)
                           Left (loc,err) ->
                            panic "Core lint failed:"
                              [ "Location: " ++ show (T.pp loc)
                              , show (T.pp err)
                              ]
         return o

    T.InferFailed nameMap warns errs ->
      do typeCheckWarnings nameMap warns
         typeCheckingFailed nameMap errs

-- | Generate input for the typechecker.
genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls ->
                                                          ModuleM T.InferInput
genInferInput r prims params env = do
  seeds <- getNameSeeds
  monoBinds <- getMonoBinds
  solver <- getTCSolver
  supply <- getSupply
  searchPath <- getSearchPath
  callStacks <- getCallStacks

  topMods <- getAllLoaded
  topSigs <- getAllLoadedSignatures

  return T.InferInput
    { T.inpRange            = r
    , T.inpVars             = Map.map ifDeclSig (ifDecls env)
    , T.inpTSyns            = ifTySyns env
    , T.inpNominalTypes     = ifNominalTypes env
    , T.inpSignatures       = ifSignatures env
    , T.inpNameSeeds        = seeds
    , T.inpMonoBinds        = monoBinds
    , T.inpCallStacks       = callStacks
    , T.inpSearchPath       = searchPath
    , T.inpSupply           = supply
    , T.inpParams           = case params of
                                NoParams -> T.allParamNames mempty
                                FunctorParams ps -> T.allParamNames ps
                                InterfaceParams ps -> ps
    , T.inpPrimNames        = prims
    , T.inpSolver           = solver
    , T.inpTopModules       = topMods
    , T.inpTopSignatures    = topSigs
    }


-- Evaluation ------------------------------------------------------------------

evalExpr :: T.Expr -> ModuleM Concrete.Value
evalExpr e = do
  env <- getEvalEnv
  denv <- getDynEnv
  evopts <- getEvalOptsAction
  let tbl = Concrete.primTable evopts
  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
  let ?range = emptyRange
  callStacks <- getCallStacks
  let ?callStacks = callStacks

  io $ E.runEval mempty (E.evalExpr Concrete (env <> deEnv denv) e)

benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats
benchmarkExpr period e = do
  env <- getEvalEnv
  denv <- getDynEnv
  evopts <- getEvalOptsAction
  let env' = env <> deEnv denv
  let tbl = Concrete.primTable evopts
  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
  let ?range = emptyRange
  callStacks <- getCallStacks
  let ?callStacks = callStacks

  let eval expr = E.runEval mempty $
        E.evalExpr Concrete env' expr >>= E.forceValue
  io $ benchmark period eval e

evalDecls :: [T.DeclGroup] -> ModuleM ()
evalDecls dgs = do
  env <- getEvalEnv
  denv <- getDynEnv
  evOpts <- getEvalOptsAction
  let env' = env <> deEnv denv
  let tbl = Concrete.primTable evOpts
  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
  callStacks <- getCallStacks
  let ?callStacks = callStacks

  deEnv' <- io $ E.runEval mempty (E.evalDecls Concrete dgs env')
  let denv' = denv { deDecls = deDecls denv ++ dgs
                   , deEnv = deEnv'
                   }
  setDynEnv denv'