    -- |
    -- 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 RecordWildCards #-}
    {-# LANGUAGE FlexibleContexts #-}

    module Cryptol.ModuleSystem.Base where

    import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
    import Cryptol.ModuleSystem.Fingerprint
    import Cryptol.ModuleSystem.Interface
    import Cryptol.ModuleSystem.Monad
    import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
    import Cryptol.ModuleSystem.Env (lookupModule
                                    , LoadedModule(..)
                                    , meCoreLint, CoreLint(..)
                                    , ModulePath(..), modulePathLabel)
    import qualified Cryptol.Eval                 as E
    import qualified Cryptol.Eval.Value           as E
    import           Cryptol.Prims.Eval ()
    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 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 Cryptol.Transform.AddModParams (addModParams)
    import Cryptol.Utils.Ident (preludeName, interactiveName
                               , modNameChunks, notParamInstModName
                               , isParamInstModName )
    import Cryptol.Utils.PP (pretty)
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.Logger(logPutStrLn, logPrint)

    import Cryptol.Prelude (preludeContents)

    import Cryptol.Transform.MonoValues (rewModule)

    import qualified Control.Exception as X
    import Control.Monad (unless,when)
    import qualified Data.ByteString as B
    import Data.Maybe (fromMaybe)
    import Data.Monoid ((<>))
    import Data.Text.Encoding (decodeUtf8')
    import System.Directory (doesFileExist, canonicalizePath)
    import System.FilePath ( addExtension
                           , isAbsolute
                           , joinPath
                           , (</>)
                           , takeDirectory
                           , takeFileName
                           )
    import qualified System.IO.Error as IOE
    import qualified Data.Map as Map

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

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

    rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a
    rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a
    rename modName :: ModName
    modName env :: NamingEnv
    env m :: RenameM a
    m = do
      (res :: Either [RenamerError] a
    res,ws :: [RenamerWarning]
    ws) <- (Supply -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
    -> ModuleT IO (Either [RenamerError] a, [RenamerWarning])
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply ((Supply -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
     -> ModuleT IO (Either [RenamerError] a, [RenamerWarning]))
    -> (Supply
        -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
    -> ModuleT IO (Either [RenamerError] a, [RenamerWarning])
    forall a b. (a -> b) -> a -> b
    $ \ supply :: Supply
    supply ->
        case Supply
    -> ModName
    -> NamingEnv
    -> RenameM a
    -> (Either [RenamerError] (a, Supply), [RenamerWarning])
    forall a.
    Supply
    -> ModName
    -> NamingEnv
    -> RenameM a
    -> (Either [RenamerError] (a, Supply), [RenamerWarning])
    R.runRenamer Supply
    supply ModName
    modName NamingEnv
    env RenameM a
    m of
          (Right (a :: a
    a,supply' :: Supply
    supply'),ws :: [RenamerWarning]
    ws) -> ((a -> Either [RenamerError] a
    forall a b. b -> Either a b
    Right a
    a,[RenamerWarning]
    ws),Supply
    supply')
          (Left errs :: [RenamerError]
    errs,ws :: [RenamerWarning]
    ws)         -> (([RenamerError] -> Either [RenamerError] a
    forall a b. a -> Either a b
    Left [RenamerError]
    errs,[RenamerWarning]
    ws),Supply
    supply)

      [RenamerWarning] -> ModuleM ()
    renamerWarnings [RenamerWarning]
    ws
      case Either [RenamerError] a
    res of
        Right r :: a
    r   -> a -> ModuleM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    r
        Left errs :: [RenamerError]
    errs -> [RenamerError] -> ModuleM a
    forall a. [RenamerError] -> ModuleM a
    renamerErrors [RenamerError]
    errs

    -- | Rename a module in the context of its imported modules.
    renameModule :: P.Module PName
                 -> ModuleM (IfaceDecls,R.NamingEnv,P.Module Name)
    renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)
    renameModule m :: Module PName
    m = do
      (decls :: IfaceDecls
    decls,menv :: NamingEnv
    menv) <- [Import] -> ModuleM (IfaceDecls, NamingEnv)
    importIfaces ((Located Import -> Import) -> [Located Import] -> [Import]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Import -> Import
    forall a. Located a -> a
    thing (Module PName -> [Located Import]
    forall name. Module name -> [Located Import]
    P.mImports Module PName
    m))
      (declsEnv :: NamingEnv
    declsEnv,rm :: Module Name
    rm) <- ModName
    -> NamingEnv
    -> RenameM (NamingEnv, Module Name)
    -> ModuleM (NamingEnv, Module Name)
    forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
    rename (Located ModName -> ModName
    forall a. Located a -> a
    thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    mName Module PName
    m)) NamingEnv
    menv (Module PName -> RenameM (NamingEnv, Module Name)
    R.renameModule Module PName
    m)
      (IfaceDecls, NamingEnv, Module Name)
    -> ModuleM (IfaceDecls, NamingEnv, Module Name)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceDecls
    decls,NamingEnv
    declsEnv,Module Name
    rm)

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

    -- | Run the noPat pass.
    noPat :: RemovePatterns a => a -> ModuleM a
    noPat :: a -> ModuleM a
    noPat a :: a
    a = do
      let (a' :: a
    a',errs :: [Error]
    errs) = a -> (a, [Error])
    forall t. RemovePatterns t => t -> (t, [Error])
    removePatterns a
    a
      Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Error] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Error]
    errs) ([Error] -> ModuleM ()
    forall a. [Error] -> ModuleM a
    noPatErrors [Error]
    errs)
      a -> ModuleM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a'

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

    parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
    parseModule :: ModulePath -> ModuleM (Fingerprint, Module PName)
    parseModule path :: ModulePath
    path = do

      Either IOError ByteString
    bytesRes <- case ModulePath
    path of
                    InFile p :: FilePath
    p -> IO (Either IOError ByteString)
    -> ModuleT IO (Either IOError ByteString)
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (IO ByteString -> IO (Either IOError ByteString)
    forall e a. Exception e => IO a -> IO (Either e a)
    X.try (FilePath -> IO ByteString
    B.readFile FilePath
    p))
                    InMem _ bs :: ByteString
    bs -> Either IOError ByteString -> ModuleT IO (Either IOError ByteString)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ByteString -> Either IOError ByteString
    forall a b. b -> Either a b
    Right ByteString
    bs)

      ByteString
    bytes <- case Either IOError ByteString
    bytesRes of
        Right bytes :: ByteString
    bytes -> ByteString -> ModuleT IO ByteString
    forall (m :: * -> *) a. Monad m => a -> m a
    return ByteString
    bytes
        Left exn :: IOError
    exn ->
          case ModulePath
    path of
            InFile p :: FilePath
    p
              | IOError -> Bool
    IOE.isDoesNotExistError IOError
    exn -> FilePath -> ModuleT IO ByteString
    forall a. FilePath -> ModuleM a
    cantFindFile FilePath
    p
              | Bool
    otherwise                   -> FilePath -> IOError -> ModuleT IO ByteString
    forall a. FilePath -> IOError -> ModuleM a
    otherIOError FilePath
    p IOError
    exn
            InMem p :: FilePath
    p _ -> FilePath -> [FilePath] -> ModuleT IO ByteString
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "parseModule"
                           [ "IOError for in-memory contetns???"
                           , "Label: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    p
                           , "Exception: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ IOError -> FilePath
    forall a. Show a => a -> FilePath
    show IOError
    exn ]

      Text
    txt <- case ByteString -> Either UnicodeException Text
    decodeUtf8' ByteString
    bytes of
        Right txt :: Text
    txt -> Text -> ModuleT IO Text
    forall (m :: * -> *) a. Monad m => a -> m a
    return Text
    txt
        Left e :: UnicodeException
    e    -> ModulePath -> UnicodeException -> ModuleT IO Text
    forall a. ModulePath -> UnicodeException -> ModuleM a
    badUtf8 ModulePath
    path UnicodeException
    e

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

      case Config -> Text -> Either ParseError (Module PName)
    P.parseModule Config
    cfg Text
    txt of
        Right pm :: Module PName
    pm -> let fp :: Fingerprint
    fp = ByteString -> Fingerprint
    fingerprint ByteString
    bytes
                    in Fingerprint
    fp Fingerprint
    -> ModuleM (Fingerprint, Module PName)
    -> ModuleM (Fingerprint, Module PName)
    forall a b. a -> b -> b
    `seq` (Fingerprint, Module PName) -> ModuleM (Fingerprint, Module PName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Fingerprint
    fp, Module PName
    pm)
        Left err :: ParseError
    err -> ModulePath -> ParseError -> ModuleM (Fingerprint, Module PName)
    forall a. ModulePath -> ParseError -> ModuleM a
    moduleParseError ModulePath
    path ParseError
    err

    -- Modules ---------------------------------------------------------------------

    -- | Load a module by its path.
    loadModuleByPath :: FilePath -> ModuleM T.Module
    loadModuleByPath :: FilePath -> ModuleM Module
    loadModuleByPath path :: FilePath
    path = [FilePath] -> ModuleM Module -> ModuleM Module
    forall a. [FilePath] -> ModuleM a -> ModuleM a
    withPrependedSearchPath [ FilePath -> FilePath
    takeDirectory FilePath
    path ] (ModuleM Module -> ModuleM Module)
    -> ModuleM Module -> ModuleM Module
    forall a b. (a -> b) -> a -> b
    $ do
      let fileName :: FilePath
    fileName = FilePath -> FilePath
    takeFileName FilePath
    path
      FilePath
    foundPath <- FilePath -> ModuleM FilePath
    findFile FilePath
    fileName
      (fp :: Fingerprint
    fp, pm :: Module PName
    pm) <- ModulePath -> ModuleM (Fingerprint, Module PName)
    parseModule (FilePath -> ModulePath
    InFile FilePath
    foundPath)
      let n :: ModName
    n = Located ModName -> ModName
    forall a. Located a -> a
    thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module PName
    pm)

      -- Check whether this module name has already been loaded from a different file
      ModuleEnv
    env <- ModuleT IO ModuleEnv
    forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
    getModuleEnv
      -- path' is the resolved, absolute path, used only for checking
      -- whether it's already been loaded
      FilePath
    path' <- IO FilePath -> ModuleM FilePath
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (FilePath -> IO FilePath
    canonicalizePath FilePath
    foundPath)

      case ModName -> ModuleEnv -> Maybe LoadedModule
    lookupModule ModName
    n ModuleEnv
    env of
        -- loadModule will calculate the canonical path again
        Nothing -> ImportSource
    -> ModulePath -> Fingerprint -> Module PName -> ModuleM Module
    doLoadModule (ModName -> ImportSource
    FromModule ModName
    n) (FilePath -> ModulePath
    InFile FilePath
    foundPath) Fingerprint
    fp Module PName
    pm
        Just lm :: LoadedModule
    lm
         | FilePath
    path' FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    loaded -> Module -> ModuleM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LoadedModule -> Module
    lmModule LoadedModule
    lm)
         | Bool
    otherwise       -> ModName -> FilePath -> FilePath -> ModuleM Module
    forall a. ModName -> FilePath -> FilePath -> ModuleM a
    duplicateModuleName ModName
    n FilePath
    path' FilePath
    loaded
         where loaded :: FilePath
    loaded = LoadedModule -> FilePath
    lmModuleId LoadedModule
    lm

    -- | Load a module, unless it was previously loaded.
    loadModuleFrom :: ImportSource -> ModuleM (ModulePath,T.Module)
    loadModuleFrom :: ImportSource -> ModuleM (ModulePath, Module)
    loadModuleFrom isrc :: ImportSource
    isrc =
      do let n :: ModName
    n = ImportSource -> ModName
    importedModule ImportSource
    isrc
         Maybe LoadedModule
    mb <- ModName -> ModuleM (Maybe LoadedModule)
    getLoadedMaybe ModName
    n
         case Maybe LoadedModule
    mb of
           Just m :: LoadedModule
    m -> (ModulePath, Module) -> ModuleM (ModulePath, Module)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (LoadedModule -> ModulePath
    lmFilePath LoadedModule
    m, LoadedModule -> Module
    lmModule LoadedModule
    m)
           Nothing ->
             do ModulePath
    path <- ModName -> ModuleM ModulePath
    findModule ModName
    n
                ModulePath
    -> ModuleM (ModulePath, Module) -> ModuleM (ModulePath, Module)
    forall a. ModulePath -> ModuleM a -> ModuleM a
    errorInFile ModulePath
    path (ModuleM (ModulePath, Module) -> ModuleM (ModulePath, Module))
    -> ModuleM (ModulePath, Module) -> ModuleM (ModulePath, Module)
    forall a b. (a -> b) -> a -> b
    $
                  do (fp :: Fingerprint
    fp, pm :: Module PName
    pm) <- ModulePath -> ModuleM (Fingerprint, Module PName)
    parseModule ModulePath
    path
                     Module
    m        <- ImportSource
    -> ModulePath -> Fingerprint -> Module PName -> ModuleM Module
    doLoadModule ImportSource
    isrc ModulePath
    path Fingerprint
    fp Module PName
    pm
                     (ModulePath, Module) -> ModuleM (ModulePath, Module)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ModulePath
    path,Module
    m)

    -- | Load dependencies, typecheck, and add to the eval environment.
    doLoadModule ::
      ImportSource ->
      ModulePath ->
      Fingerprint ->
      P.Module PName ->
      ModuleM T.Module
    doLoadModule :: ImportSource
    -> ModulePath -> Fingerprint -> Module PName -> ModuleM Module
    doLoadModule isrc :: ImportSource
    isrc path :: ModulePath
    path fp :: Fingerprint
    fp pm0 :: Module PName
    pm0 =
      ImportSource -> ModuleM Module -> ModuleM Module
    forall a. ImportSource -> ModuleM a -> ModuleM a
    loading ImportSource
    isrc (ModuleM Module -> ModuleM Module)
    -> ModuleM Module -> ModuleM Module
    forall a b. (a -> b) -> a -> b
    $
      do let pm :: Module PName
    pm = Module PName -> Module PName
    addPrelude Module PName
    pm0
         Module PName -> ModuleM ()
    forall name. Module name -> ModuleM ()
    loadDeps Module PName
    pm

         (Logger -> FilePath -> IO ()) -> FilePath -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    withLogger Logger -> FilePath -> IO ()
    logPutStrLn
           ("Loading module " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ModName -> FilePath
    forall a. PP a => a -> FilePath
    pretty (Located ModName -> ModName
    forall a. Located a -> a
    P.thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module PName
    pm)))
         Module
    tcm <- Module -> ModuleM Module
    optionalInstantiate (Module -> ModuleM Module) -> ModuleM Module -> ModuleM Module
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ImportSource -> ModulePath -> Module PName -> ModuleM Module
    checkModule ImportSource
    isrc ModulePath
    path Module PName
    pm

         -- extend the eval env, unless a functor.
         Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Module -> Bool
    T.isParametrizedModule Module
    tcm) (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ (EvalEnv -> Eval EvalEnv) -> ModuleM ()
    modifyEvalEnv (Module -> EvalEnv -> Eval EvalEnv
    forall b w i.
    EvalPrims b w i =>
    Module -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    E.moduleEnv Module
    tcm)
         ModulePath -> Fingerprint -> Module -> ModuleM ()
    loadedModule ModulePath
    path Fingerprint
    fp Module
    tcm

         Module -> ModuleM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return Module
    tcm
      where
      optionalInstantiate :: Module -> ModuleM Module
    optionalInstantiate tcm :: Module
    tcm
        | ModName -> Bool
    isParamInstModName (ImportSource -> ModName
    importedModule ImportSource
    isrc) =
          if Module -> Bool
    T.isParametrizedModule Module
    tcm then
            case Module -> Either [Name] Module
    addModParams Module
    tcm of
              Right tcm1 :: Module
    tcm1 -> Module -> ModuleM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return Module
    tcm1
              Left xs :: [Name]
    xs    -> ModName -> [Name] -> ModuleM Module
    forall a. ModName -> [Name] -> ModuleM a
    failedToParameterizeModDefs (Module -> ModName
    T.mName Module
    tcm) [Name]
    xs
          else ModName -> ModuleM Module
    forall a. ModName -> ModuleM a
    notAParameterizedModule (Module -> ModName
    T.mName Module
    tcm)
        | Bool
    otherwise = Module -> ModuleM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return Module
    tcm

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

    -- | Find the interface referenced by an import, and generate the naming
    -- environment that it describes.
    importIface :: P.Import -> ModuleM (IfaceDecls,R.NamingEnv)
    importIface :: Import -> ModuleM (IfaceDecls, NamingEnv)
    importIface imp :: Import
    imp =
      do Iface { .. } <- ModName -> ModuleM Iface
    getIface (Import -> ModName
    T.iModule Import
    imp)
         (IfaceDecls, NamingEnv) -> ModuleM (IfaceDecls, NamingEnv)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceDecls
    ifPublic, Import -> IfaceDecls -> NamingEnv
    R.interpImport Import
    imp IfaceDecls
    ifPublic)

    -- | Load a series of interfaces, merging their public interfaces.
    importIfaces :: [P.Import] -> ModuleM (IfaceDecls,R.NamingEnv)
    importIfaces :: [Import] -> ModuleM (IfaceDecls, NamingEnv)
    importIfaces is :: [Import]
    is = [(IfaceDecls, NamingEnv)] -> (IfaceDecls, NamingEnv)
    forall a. Monoid a => [a] -> a
    mconcat ([(IfaceDecls, NamingEnv)] -> (IfaceDecls, NamingEnv))
    -> ModuleT IO [(IfaceDecls, NamingEnv)]
    -> ModuleM (IfaceDecls, NamingEnv)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (Import -> ModuleM (IfaceDecls, NamingEnv))
    -> [Import] -> ModuleT IO [(IfaceDecls, NamingEnv)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Import -> ModuleM (IfaceDecls, NamingEnv)
    importIface [Import]
    is

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

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

        path :: FilePath
    path:rest :: [FilePath]
    rest -> do
          Bool
    b <- IO Bool -> ModuleT IO Bool
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (FilePath -> IO Bool
    doesFileExist FilePath
    path)
          if Bool
    b then ModulePath -> ModuleM ModulePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath -> ModulePath
    InFile FilePath
    path) else [FilePath] -> ModuleM ModulePath
    loop [FilePath]
    rest

        [] -> ModuleM ModulePath
    handleNotFound

      handleNotFound :: ModuleM ModulePath
    handleNotFound =
        case ModName
    n of
          m :: ModName
    m | ModName
    m ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName
    preludeName -> ModulePath -> ModuleM ModulePath
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (FilePath -> ByteString -> ModulePath
    InMem "Cryptol" ByteString
    preludeContents)
          _ -> ModName -> [FilePath] -> ModuleM ModulePath
    forall a. ModName -> [FilePath] -> ModuleM a
    moduleNotFound ModName
    n ([FilePath] -> ModuleM ModulePath)
    -> ModuleM [FilePath] -> ModuleM ModulePath
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ModuleM [FilePath]
    getSearchPath

      -- generate all possible search paths
      possibleFiles :: [FilePath] -> [FilePath]
    possibleFiles paths :: [FilePath]
    paths = do
        FilePath
    path <- [FilePath]
    paths
        FilePath
    ext  <- [FilePath]
    P.knownExts
        FilePath -> [FilePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath
    path FilePath -> FilePath -> FilePath
    </> ModName -> FilePath -> FilePath
    moduleFile ModName
    n FilePath
    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 :: FilePath -> ModuleM FilePath
    findFile path :: FilePath
    path | FilePath -> Bool
    isAbsolute FilePath
    path = do
      -- No search path checking for absolute paths
      Bool
    b <- IO Bool -> ModuleT IO Bool
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (FilePath -> IO Bool
    doesFileExist FilePath
    path)
      if Bool
    b then FilePath -> ModuleM FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return FilePath
    path else FilePath -> ModuleM FilePath
    forall a. FilePath -> ModuleM a
    cantFindFile FilePath
    path
    findFile path :: FilePath
    path = do
      [FilePath]
    paths <- ModuleM [FilePath]
    getSearchPath
      [FilePath] -> ModuleM FilePath
    loop ([FilePath] -> [FilePath]
    possibleFiles [FilePath]
    paths)
      where
      loop :: [FilePath] -> ModuleM FilePath
    loop paths :: [FilePath]
    paths = case [FilePath]
    paths of
        path' :: FilePath
    path':rest :: [FilePath]
    rest -> do
          Bool
    b <- IO Bool -> ModuleT IO Bool
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (FilePath -> IO Bool
    doesFileExist FilePath
    path')
          if Bool
    b then FilePath -> ModuleM FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return FilePath
    path' else [FilePath] -> ModuleM FilePath
    loop [FilePath]
    rest
        [] -> FilePath -> ModuleM FilePath
    forall a. FilePath -> ModuleM a
    cantFindFile FilePath
    path
      possibleFiles :: [FilePath] -> [FilePath]
    possibleFiles paths :: [FilePath]
    paths = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (FilePath -> FilePath -> FilePath
    </> FilePath
    path) [FilePath]
    paths

    -- | Add the prelude to the import list if it's not already mentioned.
    addPrelude :: P.Module PName -> P.Module PName
    addPrelude :: Module PName -> Module PName
    addPrelude m :: Module PName
    m
      | ModName
    preludeName ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Located ModName -> ModName
    forall a. Located a -> a
    P.thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module PName
    m) = Module PName
    m
      | ModName
    preludeName ModName -> [ModName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ModName]
    importedMods    = Module PName
    m
      | Bool
    otherwise                          = Module PName
    m { mImports :: [Located Import]
    mImports = Located Import
    importPrelude Located Import -> [Located Import] -> [Located Import]
    forall a. a -> [a] -> [a]
    : Module PName -> [Located Import]
    forall name. Module name -> [Located Import]
    mImports Module PName
    m }
      where
      importedMods :: [ModName]
    importedMods  = (Located Import -> ModName) -> [Located Import] -> [ModName]
    forall a b. (a -> b) -> [a] -> [b]
    map (Import -> ModName
    P.iModule (Import -> ModName)
    -> (Located Import -> Import) -> Located Import -> ModName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Located Import -> Import
    forall a. Located a -> a
    P.thing) (Module PName -> [Located Import]
    forall name. Module name -> [Located Import]
    P.mImports Module PName
    m)
      importPrelude :: Located Import
    importPrelude = $WLocated :: forall a. Range -> a -> Located a
    P.Located
        { srcRange :: Range
    P.srcRange = Range
    emptyRange
        , thing :: Import
    P.thing    = $WImport :: ModName -> Maybe ModName -> Maybe ImportSpec -> Import
    P.Import
          { iModule :: ModName
    iModule    = ModName
    preludeName
          , iAs :: Maybe ModName
    iAs        = Maybe ModName
    forall a. Maybe a
    Nothing
          , iSpec :: Maybe ImportSpec
    iSpec      = Maybe ImportSpec
    forall a. Maybe a
    Nothing
          }
        }

    -- | Load the dependencies of a module into the environment.
    loadDeps :: P.Module name -> ModuleM ()
    loadDeps :: Module name -> ModuleM ()
    loadDeps m :: Module name
    m =
      do (Located Import -> ModuleM ()) -> [Located Import] -> ModuleM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Located Import -> ModuleM ()
    loadI (Module name -> [Located Import]
    forall name. Module name -> [Located Import]
    P.mImports Module name
    m)
         (Located ModName -> ModuleM ())
    -> Maybe (Located ModName) -> ModuleM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Located ModName -> ModuleM ()
    loadF (Module name -> Maybe (Located ModName)
    forall name. Module name -> Maybe (Located ModName)
    P.mInstance Module name
    m)
      where
      loadI :: Located Import -> ModuleM ()
    loadI i :: Located Import
    i = do (_,m1 :: Module
    m1)  <- ImportSource -> ModuleM (ModulePath, Module)
    loadModuleFrom (Located Import -> ImportSource
    FromImport Located Import
    i)
                   Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Module -> Bool
    T.isParametrizedModule Module
    m1) (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ ModName -> ModuleM ()
    forall a. ModName -> ModuleM a
    importParamModule (ModName -> ModuleM ()) -> ModName -> ModuleM ()
    forall a b. (a -> b) -> a -> b
    $ Module -> ModName
    T.mName Module
    m1
      loadF :: Located ModName -> ModuleM ()
    loadF f :: Located ModName
    f = do (ModulePath, Module)
    _ <- ImportSource -> ModuleM (ModulePath, Module)
    loadModuleFrom (Located ModName -> ImportSource
    FromModuleInstance Located ModName
    f)
                   () -> ModuleM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

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

    -- | Load the local environment, which consists of the environment for the
    -- currently opened module, shadowed by the dynamic environment.
    getLocalEnv :: ModuleM (IfaceParams,IfaceDecls,R.NamingEnv)
    getLocalEnv :: ModuleM (IfaceParams, IfaceDecls, NamingEnv)
    getLocalEnv  =
      do (params :: IfaceParams
    params,decls :: IfaceDecls
    decls,fNames :: NamingEnv
    fNames,_) <- ModuleM (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
         DynamicEnv
    denv             <- ModuleM DynamicEnv
    getDynEnv
         let dynDecls :: IfaceDecls
    dynDecls = DynamicEnv -> IfaceDecls
    deIfaceDecls DynamicEnv
    denv
         (IfaceParams, IfaceDecls, NamingEnv)
    -> ModuleM (IfaceParams, IfaceDecls, NamingEnv)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceParams
    params,IfaceDecls
    dynDecls IfaceDecls -> IfaceDecls -> IfaceDecls
    forall a. Monoid a => a -> a -> a
    `mappend` IfaceDecls
    decls, DynamicEnv -> NamingEnv
    deNames DynamicEnv
    denv NamingEnv -> NamingEnv -> NamingEnv
    `R.shadowing` NamingEnv
    fNames)

    -- | 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 :: Expr PName -> ModuleM (Expr Name, Expr, Schema)
    checkExpr e :: Expr PName
    e = do

      (params :: IfaceParams
    params,decls :: IfaceDecls
    decls,names :: NamingEnv
    names) <- ModuleM (IfaceParams, IfaceDecls, NamingEnv)
    getLocalEnv

      -- run NoPat
      Expr PName
    npe <- Expr PName -> ModuleM (Expr PName)
    forall a. RemovePatterns a => a -> ModuleM a
    noPat Expr PName
    e

      -- rename the expression with dynamic names shadowing the opened environment
      Expr Name
    re  <- ModName -> NamingEnv -> RenameM (Expr Name) -> ModuleM (Expr Name)
    forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
    rename ModName
    interactiveName NamingEnv
    names (Expr PName -> RenameM (Expr Name)
    forall (f :: * -> *). Rename f => f PName -> RenameM (f Name)
    R.rename Expr PName
    npe)

      -- merge the dynamic and opened environments for typechecking
      PrimMap
    prims <- ModuleM PrimMap
    getPrimMap
      let act :: TCAction (Expr Name) (Expr, Schema)
    act  = TCAction :: forall i o. Act i o -> TCLinter o -> PrimMap -> TCAction i o
    TCAction { tcAction :: Act (Expr Name) (Expr, Schema)
    tcAction = Act (Expr Name) (Expr, Schema)
    T.tcExpr, tcLinter :: TCLinter (Expr, Schema)
    tcLinter = TCLinter (Expr, Schema)
    exprLinter
                          , tcPrims :: PrimMap
    tcPrims = PrimMap
    prims }
      (te :: Expr
    te,s :: Schema
    s) <- TCAction (Expr Name) (Expr, Schema)
    -> Expr Name -> IfaceParams -> IfaceDecls -> ModuleM (Expr, Schema)
    forall i o.
    (Show i, Show o, HasLoc i) =>
    TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o
    typecheck TCAction (Expr Name) (Expr, Schema)
    act Expr Name
    re IfaceParams
    params IfaceDecls
    decls

      (Expr Name, Expr, Schema) -> ModuleM (Expr Name, Expr, Schema)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Expr Name
    re,Expr
    te,Schema
    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])
    checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup])
    checkDecls ds :: [TopDecl PName]
    ds = do
      (params :: IfaceParams
    params,decls :: IfaceDecls
    decls,names :: NamingEnv
    names) <- ModuleM (IfaceParams, IfaceDecls, NamingEnv)
    getLocalEnv

      -- introduce names for the declarations before renaming them
      NamingEnv
    declsEnv <- (Supply -> (NamingEnv, Supply)) -> ModuleT IO NamingEnv
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply ([InModule (TopDecl PName)] -> Supply -> (NamingEnv, Supply)
    forall a. BindsNames a => a -> Supply -> (NamingEnv, Supply)
    R.namingEnv' ((TopDecl PName -> InModule (TopDecl PName))
    -> [TopDecl PName] -> [InModule (TopDecl PName)]
    forall a b. (a -> b) -> [a] -> [b]
    map (ModName -> TopDecl PName -> InModule (TopDecl PName)
    forall a. ModName -> a -> InModule a
    R.InModule ModName
    interactiveName) [TopDecl PName]
    ds))
      [TopDecl Name]
    rds <- ModName
    -> NamingEnv -> RenameM [TopDecl Name] -> ModuleM [TopDecl Name]
    forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
    rename ModName
    interactiveName (NamingEnv
    declsEnv NamingEnv -> NamingEnv -> NamingEnv
    `R.shadowing` NamingEnv
    names)
                 ((TopDecl PName -> RenameM (TopDecl Name))
    -> [TopDecl PName] -> RenameM [TopDecl Name]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse TopDecl PName -> RenameM (TopDecl Name)
    forall (f :: * -> *). Rename f => f PName -> RenameM (f Name)
    R.rename [TopDecl PName]
    ds)

      PrimMap
    prims <- ModuleM PrimMap
    getPrimMap
      let act :: TCAction [TopDecl Name] [DeclGroup]
    act  = TCAction :: forall i o. Act i o -> TCLinter o -> PrimMap -> TCAction i o
    TCAction { tcAction :: Act [TopDecl Name] [DeclGroup]
    tcAction = Act [TopDecl Name] [DeclGroup]
    forall d.
    FromDecl d =>
    [d] -> InferInput -> IO (InferOutput [DeclGroup])
    T.tcDecls, tcLinter :: TCLinter [DeclGroup]
    tcLinter = TCLinter [DeclGroup]
    declsLinter
                          , tcPrims :: PrimMap
    tcPrims = PrimMap
    prims }
      [DeclGroup]
    ds' <- TCAction [TopDecl Name] [DeclGroup]
    -> [TopDecl Name]
    -> IfaceParams
    -> IfaceDecls
    -> ModuleM [DeclGroup]
    forall i o.
    (Show i, Show o, HasLoc i) =>
    TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o
    typecheck TCAction [TopDecl Name] [DeclGroup]
    act [TopDecl Name]
    rds IfaceParams
    params IfaceDecls
    decls
      (NamingEnv, [DeclGroup]) -> ModuleM (NamingEnv, [DeclGroup])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamingEnv
    declsEnv,[DeclGroup]
    ds')

    -- | 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 :: ModuleM PrimMap
    getPrimMap  =
      do ModuleEnv
    env <- ModuleT IO ModuleEnv
    forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
    getModuleEnv
         case ModName -> ModuleEnv -> Maybe LoadedModule
    lookupModule ModName
    preludeName ModuleEnv
    env of
           Just lm :: LoadedModule
    lm -> PrimMap -> ModuleM PrimMap
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Iface -> PrimMap
    ifacePrimMap (LoadedModule -> Iface
    lmInterface LoadedModule
    lm))
           Nothing -> FilePath -> [FilePath] -> ModuleM PrimMap
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "Cryptol.ModuleSystem.Base.getPrimMap"
                      [ "Unable to find the prelude" ]

    -- | Load a module, be it a normal module or a functor instantiation.
    checkModule :: ImportSource -> ModulePath -> P.Module PName -> ModuleM T.Module
    checkModule :: ImportSource -> ModulePath -> Module PName -> ModuleM Module
    checkModule isrc :: ImportSource
    isrc path :: ModulePath
    path m :: Module PName
    m =
      case Module PName -> Maybe (Located ModName)
    forall name. Module name -> Maybe (Located ModName)
    P.mInstance Module PName
    m of
        Nothing -> Act (Module Name) Module
    -> ImportSource -> ModulePath -> Module PName -> ModuleM Module
    checkSingleModule Act (Module Name) Module
    T.tcModule ImportSource
    isrc ModulePath
    path Module PName
    m
        Just fmName :: Located ModName
    fmName -> do Module
    tf <- ModName -> ModuleM Module
    getLoaded (Located ModName -> ModName
    forall a. Located a -> a
    thing Located ModName
    fmName)
                          Act (Module Name) Module
    -> ImportSource -> ModulePath -> Module PName -> ModuleM Module
    checkSingleModule (Module -> Act (Module Name) Module
    T.tcModuleInst Module
    tf) ImportSource
    isrc ModulePath
    path Module PName
    m

    -- | Typecheck a single module.  If the module is an instantiation
    -- of a functor, then this just type-checks the instantiating parameters.
    -- See 'checkModule'
    checkSingleModule ::
      Act (P.Module Name) T.Module {- ^ how to check -} ->
      ImportSource                 {- ^ why are we loading this -} ->
      ModulePath                   {- path -} ->
      P.Module PName               {- ^ module to check -} ->
      ModuleM T.Module
    checkSingleModule :: Act (Module Name) Module
    -> ImportSource -> ModulePath -> Module PName -> ModuleM Module
    checkSingleModule how :: Act (Module Name) Module
    how isrc :: ImportSource
    isrc path :: ModulePath
    path m :: Module PName
    m = do

      -- check that the name of the module matches expectations
      let nm :: ModName
    nm = ImportSource -> ModName
    importedModule ImportSource
    isrc
      Bool -> ModuleM () -> ModuleM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ModName -> ModName
    notParamInstModName ModName
    nm ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Located ModName -> ModName
    forall a. Located a -> a
    thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module PName
    m))
             (ModName -> Located ModName -> ModuleM ()
    forall a. ModName -> Located ModName -> ModuleM a
    moduleNameMismatch ModName
    nm (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    mName Module PName
    m))

      -- remove includes first; we only do this for actual files.
      -- it is less clear what should happen for in-memory things, and since
      -- this is a more-or-less obsolete feature, we are just not doing
      -- ot for now.
      Either [IncludeError] (Module PName)
    e   <- case ModulePath
    path of
               InFile p :: FilePath
    p -> IO (Either [IncludeError] (Module PName))
    -> ModuleT IO (Either [IncludeError] (Module PName))
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (FilePath
    -> Module PName -> IO (Either [IncludeError] (Module PName))
    removeIncludesModule FilePath
    p Module PName
    m)
               InMem {} -> Either [IncludeError] (Module PName)
    -> ModuleT IO (Either [IncludeError] (Module PName))
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Module PName -> Either [IncludeError] (Module PName)
    forall a b. b -> Either a b
    Right Module PName
    m)

      Module PName
    nim <- case Either [IncludeError] (Module PName)
    e of
               Right nim :: Module PName
    nim  -> Module PName -> ModuleT IO (Module PName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Module PName
    nim
               Left ierrs :: [IncludeError]
    ierrs -> [IncludeError] -> ModuleT IO (Module PName)
    forall a. [IncludeError] -> ModuleM a
    noIncludeErrors [IncludeError]
    ierrs

      -- remove pattern bindings
      Module PName
    npm <- Module PName -> ModuleT IO (Module PName)
    forall a. RemovePatterns a => a -> ModuleM a
    noPat Module PName
    nim

      -- rename everything
      (tcEnv :: IfaceDecls
    tcEnv,declsEnv :: NamingEnv
    declsEnv,scm :: Module Name
    scm) <- Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)
    renameModule Module PName
    npm

      -- 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.
      PrimMap
    prims <- if Located ModName -> ModName
    forall a. Located a -> a
    thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    mName Module PName
    m) ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName
    preludeName
                  then PrimMap -> ModuleM PrimMap
    forall (m :: * -> *) a. Monad m => a -> m a
    return (NamingEnv -> PrimMap
    R.toPrimMap NamingEnv
    declsEnv)
                  else ModuleM PrimMap
    getPrimMap

      -- typecheck
      let act :: TCAction (Module Name) Module
    act = TCAction :: forall i o. Act i o -> TCLinter o -> PrimMap -> TCAction i o
    TCAction { tcAction :: Act (Module Name) Module
    tcAction = Act (Module Name) Module
    how
                         , tcLinter :: TCLinter Module
    tcLinter = ModName -> TCLinter Module
    moduleLinter (Located ModName -> ModName
    forall a. Located a -> a
    P.thing (Module PName -> Located ModName
    forall name. Module name -> Located ModName
    P.mName Module PName
    m))
                         , tcPrims :: PrimMap
    tcPrims  = PrimMap
    prims }

      Module
    tcm0 <- TCAction (Module Name) Module
    -> Module Name -> IfaceParams -> IfaceDecls -> ModuleM Module
    forall i o.
    (Show i, Show o, HasLoc i) =>
    TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o
    typecheck TCAction (Module Name) Module
    act Module Name
    scm IfaceParams
    noIfaceParams IfaceDecls
    tcEnv

      let tcm :: Module
    tcm = Module
    tcm0 -- fromMaybe tcm0 (addModParams tcm0)

      (Supply -> (Module, Supply)) -> ModuleM Module
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply (Supply -> Module -> (Module, Supply)
    `rewModule` Module
    tcm)

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

    exprLinter :: TCLinter (T.Expr, T.Schema)
    exprLinter :: TCLinter (Expr, Schema)
    exprLinter = TCLinter :: forall o.
    (o -> InferInput -> Either Error [Schema])
    -> Maybe ModName -> TCLinter o
    TCLinter
      { lintCheck :: (Expr, Schema) -> InferInput -> Either Error [Schema]
    lintCheck = \(e' :: Expr
    e',s :: Schema
    s) i :: InferInput
    i ->
          case InferInput -> Expr -> Either Error (Schema, [Schema])
    TcSanity.tcExpr InferInput
    i Expr
    e' of
            Left err :: Error
    err     -> Error -> Either Error [Schema]
    forall a b. a -> Either a b
    Left Error
    err
            Right (s1 :: Schema
    s1,os :: [Schema]
    os)
              | Schema -> Schema -> Bool
    forall a. Same a => a -> a -> Bool
    TcSanity.same Schema
    s Schema
    s1  -> [Schema] -> Either Error [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    os
              | Bool
    otherwise -> Error -> Either Error [Schema]
    forall a b. a -> Either a b
    Left (FilePath -> Schema -> Schema -> Error
    TcSanity.TypeMismatch "exprLinter" Schema
    s Schema
    s1)
      , lintModule :: Maybe ModName
    lintModule = Maybe ModName
    forall a. Maybe a
    Nothing
      }

    declsLinter :: TCLinter [ T.DeclGroup ]
    declsLinter :: TCLinter [DeclGroup]
    declsLinter = TCLinter :: forall o.
    (o -> InferInput -> Either Error [Schema])
    -> Maybe ModName -> TCLinter o
    TCLinter
      { lintCheck :: [DeclGroup] -> InferInput -> Either Error [Schema]
    lintCheck = \ds' :: [DeclGroup]
    ds' i :: InferInput
    i -> case InferInput -> [DeclGroup] -> Either Error [Schema]
    TcSanity.tcDecls InferInput
    i [DeclGroup]
    ds' of
                                Left err :: Error
    err -> Error -> Either Error [Schema]
    forall a b. a -> Either a b
    Left Error
    err
                                Right os :: [Schema]
    os -> [Schema] -> Either Error [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    os

      , lintModule :: Maybe ModName
    lintModule = Maybe ModName
    forall a. Maybe a
    Nothing
      }

    moduleLinter :: P.ModName -> TCLinter T.Module
    moduleLinter :: ModName -> TCLinter Module
    moduleLinter m :: ModName
    m = TCLinter :: forall o.
    (o -> InferInput -> Either Error [Schema])
    -> Maybe ModName -> TCLinter o
    TCLinter
      { lintCheck :: Module -> InferInput -> Either Error [Schema]
    lintCheck   = \m' :: Module
    m' i :: InferInput
    i -> case InferInput -> Module -> Either Error [Schema]
    TcSanity.tcModule InferInput
    i Module
    m' of
                                Left err :: Error
    err -> Error -> Either Error [Schema]
    forall a b. a -> Either a b
    Left Error
    err
                                Right os :: [Schema]
    os -> [Schema] -> Either Error [Schema]
    forall a b. b -> Either a b
    Right [Schema]
    os
      , lintModule :: Maybe ModName
    lintModule  = ModName -> Maybe ModName
    forall a. a -> Maybe a
    Just ModName
    m
      }

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

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

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

      let range :: Range
    range = Range -> Maybe Range -> Range
    forall a. a -> Maybe a -> a
    fromMaybe Range
    emptyRange (i -> Maybe Range
    forall t. HasLoc t => t -> Maybe Range
    getLoc i
    i)
      InferInput
    input <- Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput
    genInferInput Range
    range (TCAction i o -> PrimMap
    forall i o. TCAction i o -> PrimMap
    tcPrims TCAction i o
    act) IfaceParams
    params IfaceDecls
    env
      InferOutput o
    out   <- IO (InferOutput o) -> ModuleT IO (InferOutput o)
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (TCAction i o -> Act i o
    forall i o. TCAction i o -> Act i o
    tcAction TCAction i o
    act i
    i InferInput
    input)

      case InferOutput o
    out of

        T.InferOK warns :: [(Range, Warning)]
    warns seeds :: NameSeeds
    seeds supply' :: Supply
    supply' o :: o
    o ->
          do NameSeeds -> ModuleM ()
    setNameSeeds NameSeeds
    seeds
             Supply -> ModuleM ()
    setSupply Supply
    supply'
             [(Range, Warning)] -> ModuleM ()
    typeCheckWarnings [(Range, Warning)]
    warns
             ModuleEnv
    menv <- ModuleT IO ModuleEnv
    forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
    getModuleEnv
             case ModuleEnv -> CoreLint
    meCoreLint ModuleEnv
    menv of
               NoCoreLint -> () -> ModuleM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
               CoreLint   -> case TCLinter o -> o -> InferInput -> Either Error [Schema]
    forall o. TCLinter o -> o -> InferInput -> Either Error [Schema]
    lintCheck (TCAction i o -> TCLinter o
    forall i o. TCAction i o -> TCLinter o
    tcLinter TCAction i o
    act) o
    o InferInput
    input of
                               Right as :: [Schema]
    as ->
                                 let ppIt :: Logger -> t a -> IO ()
    ppIt l :: Logger
    l = (a -> IO ()) -> t a -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Logger -> Doc -> IO ()
    forall a. Show a => Logger -> a -> IO ()
    logPrint Logger
    l (Doc -> IO ()) -> (a -> Doc) -> a -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Doc
    forall a. PP a => a -> Doc
    T.pp)
                                 in (Logger -> [Schema] -> IO ()) -> [Schema] -> ModuleM ()
    forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
    withLogger Logger -> [Schema] -> IO ()
    forall (t :: * -> *) a.
    (Foldable t, PP a) =>
    Logger -> t a -> IO ()
    ppIt [Schema]
    as
                               Left err :: Error
    err -> FilePath -> [FilePath] -> ModuleM ()
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "Core lint failed:" [Error -> FilePath
    forall a. Show a => a -> FilePath
    show Error
    err]
             o -> ModuleM o
    forall (m :: * -> *) a. Monad m => a -> m a
    return o
    o

        T.InferFailed warns :: [(Range, Warning)]
    warns errs :: [(Range, Error)]
    errs ->
          do [(Range, Warning)] -> ModuleM ()
    typeCheckWarnings [(Range, Warning)]
    warns
             [(Range, Error)] -> ModuleM o
    forall a. [(Range, Error)] -> ModuleM a
    typeCheckingFailed [(Range, Error)]
    errs

    -- | Generate input for the typechecker.
    genInferInput :: Range -> PrimMap ->
                              IfaceParams -> IfaceDecls -> ModuleM T.InferInput
    genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput
    genInferInput r :: Range
    r prims :: PrimMap
    prims params :: IfaceParams
    params env :: IfaceDecls
    env = do
      NameSeeds
    seeds <- ModuleM NameSeeds
    getNameSeeds
      Bool
    monoBinds <- ModuleT IO Bool
    getMonoBinds
      SolverConfig
    cfg <- ModuleM SolverConfig
    getSolverConfig
      Supply
    supply <- ModuleM Supply
    getSupply
      [FilePath]
    searchPath <- ModuleM [FilePath]
    getSearchPath

      -- TODO: include the environment needed by the module
      InferInput -> ModuleM InferInput
    forall (m :: * -> *) a. Monad m => a -> m a
    return $WInferInput :: Range
    -> Map Name Schema
    -> Map Name TySyn
    -> Map Name Newtype
    -> Map Name AbstractType
    -> Map Name ModTParam
    -> [Located Prop]
    -> Map Name ModVParam
    -> NameSeeds
    -> Bool
    -> SolverConfig
    -> [FilePath]
    -> PrimMap
    -> Supply
    -> InferInput
    T.InferInput
        { inpRange :: Range
    T.inpRange     = Range
    r
        , inpVars :: Map Name Schema
    T.inpVars      = (IfaceDecl -> Schema) -> Map Name IfaceDecl -> Map Name Schema
    forall a b k. (a -> b) -> Map k a -> Map k b
    Map.map IfaceDecl -> Schema
    ifDeclSig (IfaceDecls -> Map Name IfaceDecl
    ifDecls IfaceDecls
    env)
        , inpTSyns :: Map Name TySyn
    T.inpTSyns     = IfaceDecls -> Map Name TySyn
    ifTySyns IfaceDecls
    env
        , inpNewtypes :: Map Name Newtype
    T.inpNewtypes  = IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    env
        , inpAbstractTypes :: Map Name AbstractType
    T.inpAbstractTypes = IfaceDecls -> Map Name AbstractType
    ifAbstractTypes IfaceDecls
    env
        , inpNameSeeds :: NameSeeds
    T.inpNameSeeds = NameSeeds
    seeds
        , inpMonoBinds :: Bool
    T.inpMonoBinds = Bool
    monoBinds
        , inpSolverConfig :: SolverConfig
    T.inpSolverConfig = SolverConfig
    cfg
        , inpSearchPath :: [FilePath]
    T.inpSearchPath = [FilePath]
    searchPath
        , inpSupply :: Supply
    T.inpSupply    = Supply
    supply
        , inpPrimNames :: PrimMap
    T.inpPrimNames = PrimMap
    prims
        , inpParamTypes :: Map Name ModTParam
    T.inpParamTypes       = IfaceParams -> Map Name ModTParam
    ifParamTypes IfaceParams
    params
        , inpParamConstraints :: [Located Prop]
    T.inpParamConstraints = IfaceParams -> [Located Prop]
    ifParamConstraints IfaceParams
    params
        , inpParamFuns :: Map Name ModVParam
    T.inpParamFuns        = IfaceParams -> Map Name ModVParam
    ifParamFuns IfaceParams
    params
        }

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

    evalExpr :: T.Expr -> ModuleM E.Value
    evalExpr :: Expr -> ModuleM Value
    evalExpr e :: Expr
    e = do
      EvalEnv
    env <- ModuleM EvalEnv
    getEvalEnv
      DynamicEnv
    denv <- ModuleM DynamicEnv
    getDynEnv
      EvalOpts
    evopts <- ModuleM EvalOpts
    getEvalOpts
      IO Value -> ModuleM Value
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (IO Value -> ModuleM Value) -> IO Value -> ModuleM Value
    forall a b. (a -> b) -> a -> b
    $ EvalOpts -> Eval Value -> IO Value
    forall a. EvalOpts -> Eval a -> IO a
    E.runEval EvalOpts
    evopts (Eval Value -> IO Value) -> Eval Value -> IO Value
    forall a b. (a -> b) -> a -> b
    $ (EvalEnv -> Expr -> Eval Value
    forall b w i.
    EvalPrims b w i =>
    GenEvalEnv b w i -> Expr -> Eval (GenValue b w i)
    E.evalExpr (EvalEnv
    env EvalEnv -> EvalEnv -> EvalEnv
    forall a. Semigroup a => a -> a -> a
    <> DynamicEnv -> EvalEnv
    deEnv DynamicEnv
    denv) Expr
    e)

    evalDecls :: [T.DeclGroup] -> ModuleM ()
    evalDecls :: [DeclGroup] -> ModuleM ()
    evalDecls dgs :: [DeclGroup]
    dgs = do
      EvalEnv
    env <- ModuleM EvalEnv
    getEvalEnv
      DynamicEnv
    denv <- ModuleM DynamicEnv
    getDynEnv
      EvalOpts
    evOpts <- ModuleM EvalOpts
    getEvalOpts
      let env' :: EvalEnv
    env' = EvalEnv
    env EvalEnv -> EvalEnv -> EvalEnv
    forall a. Semigroup a => a -> a -> a
    <> DynamicEnv -> EvalEnv
    deEnv DynamicEnv
    denv
      EvalEnv
    deEnv' <- IO EvalEnv -> ModuleM EvalEnv
    forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
    io (IO EvalEnv -> ModuleM EvalEnv) -> IO EvalEnv -> ModuleM EvalEnv
    forall a b. (a -> b) -> a -> b
    $ EvalOpts -> Eval EvalEnv -> IO EvalEnv
    forall a. EvalOpts -> Eval a -> IO a
    E.runEval EvalOpts
    evOpts (Eval EvalEnv -> IO EvalEnv) -> Eval EvalEnv -> IO EvalEnv
    forall a b. (a -> b) -> a -> b
    $ [DeclGroup] -> EvalEnv -> Eval EvalEnv
    forall b w i.
    EvalPrims b w i =>
    [DeclGroup] -> GenEvalEnv b w i -> Eval (GenEvalEnv b w i)
    E.evalDecls [DeclGroup]
    dgs EvalEnv
    env'
      let denv' :: DynamicEnv
    denv' = DynamicEnv
    denv { deDecls :: [DeclGroup]
    deDecls = DynamicEnv -> [DeclGroup]
    deDecls DynamicEnv
    denv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    dgs
                       , deEnv :: EvalEnv
    deEnv = EvalEnv
    deEnv'
                       }
      DynamicEnv -> ModuleM ()
    setDynEnv DynamicEnv
    denv'