-- |
-- 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,forM)
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Maybe (fromMaybe)
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)
import System.FilePath ( addExtension
                       , isAbsolute
                       , joinPath
                       , (</>)
                       , normalise
                       , takeDirectory
                       , 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 (..))
import           Cryptol.Backend.FFI
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, 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.Backend.FFI.Error as FFI

import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                           , preludeReferenceName, interactiveName, modNameChunks
                           , 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 :: forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename ModName
modName NamingEnv
env RenameM a
m = do
  Map ModName (Either ModParamNames Iface)
ifaces <- ModuleM (Map ModName (Either ModParamNames Iface))
getIfaces
  (Either [RenamerError] a
res,[RenamerWarning]
ws) <- (Supply -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
-> ModuleT IO (Either [RenamerError] a, [RenamerWarning])
forall a. (Supply -> (a, Supply)) -> ModuleT IO a
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 ->
    let info :: RenamerInfo
info = R.RenamerInfo
                 { renSupply :: Supply
renSupply  = Supply
supply
                 , renContext :: ModPath
renContext = ModName -> ModPath
TopModule ModName
modName
                 , renEnv :: NamingEnv
renEnv     = NamingEnv
env
                 , renIfaces :: Map ModName (Either ModParamNames Iface)
renIfaces  = Map ModName (Either ModParamNames Iface)
ifaces
                 }
    in
    case RenamerInfo
-> RenameM a
-> (Either [RenamerError] (a, Supply), [RenamerWarning])
forall a.
RenamerInfo
-> RenameM a
-> (Either [RenamerError] (a, Supply), [RenamerWarning])
R.runRenamer RenamerInfo
info RenameM a
m of
      (Right (a
a,Supply
supply'),[RenamerWarning]
ws) -> ((a -> Either [RenamerError] a
forall a b. b -> Either a b
Right a
a,[RenamerWarning]
ws),Supply
supply')
      (Left [RenamerError]
errs,[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 a
r   -> a -> ModuleM a
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
    Left [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 R.RenamedModule
renameModule :: Module PName -> ModuleM RenamedModule
renameModule Module PName
m = ModName
-> NamingEnv -> RenameM RenamedModule -> ModuleM RenamedModule
forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename (Located ModName -> ModName
forall a. Located a -> a
thing (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
mName Module PName
m)) NamingEnv
forall a. Monoid a => a
mempty (Module PName -> RenameM RenamedModule
R.renameModule Module PName
m)

renameImpNameInCurrentEnv :: P.ImpName PName -> ModuleM (P.ImpName Name)
renameImpNameInCurrentEnv :: ImpName PName -> ModuleM (ImpName Name)
renameImpNameInCurrentEnv (P.ImpTop ModName
top) =
 do Bool
ok <- ModName -> ModuleM Bool
isLoaded ModName
top
    if Bool
ok then
      ImpName Name -> ModuleM (ImpName Name)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModName -> ImpName Name
forall name. ModName -> ImpName name
P.ImpTop ModName
top)
    else
      [Char] -> ModuleM (ImpName Name)
forall a. [Char] -> ModuleT IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Top-level module not loaded: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
top))
renameImpNameInCurrentEnv (P.ImpNested PName
pname) =
 do ModContext
env <- ModuleM ModContext
getFocusedEnv
    case Namespace -> PName -> NamingEnv -> [Name]
R.lookupListNS Namespace
NSModule PName
pname (ModContext -> NamingEnv
mctxNames ModContext
env) of
      [] -> do
        [Char] -> ModuleM (ImpName Name)
forall a. [Char] -> ModuleT IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Undefined submodule name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (PName -> Doc
forall a. PP a => a -> Doc
pp PName
pname))
      Name
_:Name
_:[Name]
_ -> do
        [Char] -> ModuleM (ImpName Name)
forall a. [Char] -> ModuleT IO a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Ambiguous submodule name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (PName -> Doc
forall a. PP a => a -> Doc
pp PName
pname))
      [Name
n] -> ImpName Name -> ModuleM (ImpName Name)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> ImpName Name
forall name. name -> ImpName name
P.ImpNested Name
n)

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

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
noPat :: forall a. RemovePatterns a => a -> ModuleM a
noPat a
a = do
  let (a
a',[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 a. [a] -> 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 a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a'

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

-- | Run the expandPropGuards pass.
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards Module PName
a =
  case ExpandPropGuardsM (Module PName)
-> ExpandPropGuardsM (Module PName)
forall a. ExpandPropGuardsM a -> ExpandPropGuardsM a
ExpandPropGuards.runExpandPropGuardsM (ExpandPropGuardsM (Module PName)
 -> ExpandPropGuardsM (Module PName))
-> ExpandPropGuardsM (Module PName)
-> ExpandPropGuardsM (Module PName)
forall a b. (a -> b) -> a -> b
$ Module PName -> ExpandPropGuardsM (Module PName)
forall mname.
ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
ExpandPropGuards.expandPropGuards Module PName
a of
    Left Error
err -> Error -> ModuleM (Module PName)
forall a. Error -> ModuleM a
expandPropGuardsError Error
err
    Right Module PName
a' -> Module PName -> ModuleM (Module PName)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Module PName
a'

-- 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 :: ModulePath
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
parseModule ModulePath
path = do
  [Char] -> IO ByteString
getBytes <- ModuleT IO ([Char] -> IO ByteString)
forall (m :: * -> *). Monad m => ModuleT m ([Char] -> m ByteString)
getByteReader

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

  let fp :: Fingerprint
fp = ByteString -> Fingerprint
fingerprint ByteString
bytes
  Text
txt <- case ByteString -> Either UnicodeException Text
decodeUtf8' ByteString
bytes of
    Right Text
txt -> Text -> ModuleT IO Text
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> ModuleT IO Text) -> Text -> ModuleT IO Text
forall a b. (a -> b) -> a -> b
$! HasCallStack => Text -> Text -> Text -> Text
Text -> Text -> Text -> Text
T.replace Text
"\r\n" Text
"\n" Text
txt
    Left UnicodeException
e    -> ModulePath -> Fingerprint -> UnicodeException -> ModuleT IO Text
forall a.
ModulePath -> Fingerprint -> UnicodeException -> ModuleM a
badUtf8 ModulePath
path Fingerprint
fp UnicodeException
e


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

  case Config -> Text -> Either ParseError [Module PName]
P.parseModule Config
cfg Text
txt of
    Right [Module PName]
pms ->
      do ([Module PName]
pm1,Map [Char] Fingerprint
deps) <-
           case ModulePath
path of
             InFile [Char]
p ->
               do [Char] -> IO ByteString
r <- ModuleT IO ([Char] -> IO ByteString)
forall (m :: * -> *). Monad m => ModuleT m ([Char] -> m ByteString)
getByteReader
                  ([Module PName]
mo,[Map [Char] Fingerprint]
d) <- [(Module PName, Map [Char] Fingerprint)]
-> ([Module PName], [Map [Char] Fingerprint])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Module PName, Map [Char] Fingerprint)]
 -> ([Module PName], [Map [Char] Fingerprint]))
-> ModuleT IO [(Module PName, Map [Char] Fingerprint)]
-> ModuleT IO ([Module PName], [Map [Char] Fingerprint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                    [Module PName]
-> (Module PName
    -> ModuleT IO (Module PName, Map [Char] Fingerprint))
-> ModuleT IO [(Module PName, Map [Char] Fingerprint)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Module PName]
pms \Module PName
pm ->
                    do Either [IncludeError] (Module PName, Map [Char] Fingerprint)
mb <- IO (Either [IncludeError] (Module PName, Map [Char] Fingerprint))
-> ModuleT
     IO (Either [IncludeError] (Module PName, Map [Char] Fingerprint))
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (([Char] -> IO ByteString)
-> [Char]
-> Module PName
-> IO
     (Either [IncludeError] (Module PName, Map [Char] Fingerprint))
removeIncludesModule [Char] -> IO ByteString
r [Char]
p Module PName
pm)
                       case Either [IncludeError] (Module PName, Map [Char] Fingerprint)
mb of
                         Right (Module PName, Map [Char] Fingerprint)
ok -> (Module PName, Map [Char] Fingerprint)
-> ModuleT IO (Module PName, Map [Char] Fingerprint)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module PName, Map [Char] Fingerprint)
ok
                         Left [IncludeError]
err -> [IncludeError] -> ModuleT IO (Module PName, Map [Char] Fingerprint)
forall a. [IncludeError] -> ModuleM a
noIncludeErrors [IncludeError]
err
                  ([Module PName], Map [Char] Fingerprint)
-> ModuleT IO ([Module PName], Map [Char] Fingerprint)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Module PName]
mo, [Map [Char] Fingerprint] -> Map [Char] Fingerprint
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
MapS.unions [Map [Char] Fingerprint]
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 {} -> ([Module PName], Map [Char] Fingerprint)
-> ModuleT IO ([Module PName], Map [Char] Fingerprint)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Module PName]
pms, Map [Char] Fingerprint
forall k a. Map k a
MapS.empty)

{-
         case path of
           InFile {} -> io $ print (T.vcat (map T.pp pm1))
           InMem {} -> pure ()
--}
         Fingerprint
fp Fingerprint
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
forall a b. a -> b -> b
`seq` (Fingerprint, Map [Char] Fingerprint, [Module PName])
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fingerprint
fp, Map [Char] Fingerprint
deps, [Module PName]
pm1)

    Left ParseError
err -> ModulePath
-> Fingerprint
-> ParseError
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
forall a. ModulePath -> Fingerprint -> ParseError -> ModuleM a
moduleParseError ModulePath
path Fingerprint
fp ParseError
err


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


-- | Load a module by its path.
loadModuleByPath ::
  Bool {- ^ evaluate declarations in the module -} ->
  FilePath -> ModuleM T.TCTopEntity
loadModuleByPath :: Bool -> [Char] -> ModuleM TCTopEntity
loadModuleByPath Bool
eval [Char]
path = [[Char]] -> ModuleM TCTopEntity -> ModuleM TCTopEntity
forall a. [[Char]] -> ModuleM a -> ModuleM a
withPrependedSearchPath [ [Char] -> [Char]
takeDirectory [Char]
path ] (ModuleM TCTopEntity -> ModuleM TCTopEntity)
-> ModuleM TCTopEntity -> ModuleM TCTopEntity
forall a b. (a -> b) -> a -> b
$ do
  let fileName :: [Char]
fileName = [Char] -> [Char]
takeFileName [Char]
path
  [Char]
foundPath <- [Char] -> ModuleM [Char]
findFile [Char]
fileName
  (Fingerprint
fp, Map [Char] Fingerprint
deps, [Module PName]
pms) <- ModulePath
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
parseModule ([Char] -> ModulePath
InFile [Char]
foundPath)
  [TCTopEntity] -> TCTopEntity
forall a. HasCallStack => [a] -> a
last ([TCTopEntity] -> TCTopEntity)
-> ModuleT IO [TCTopEntity] -> ModuleM TCTopEntity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [Module PName]
-> (Module PName -> ModuleM TCTopEntity)
-> ModuleT IO [TCTopEntity]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Module PName]
pms \Module PName
pm ->
    do let n :: ModName
n = Located ModName -> ModName
forall a. Located a -> a
thing (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
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
       [Char]
path' <- IO [Char] -> ModuleM [Char]
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO [Char]
canonicalizePath [Char]
foundPath)

       case ModName -> ModuleEnv -> Maybe (LoadedModuleG TCTopEntity)
lookupTCEntity ModName
n ModuleEnv
env of
         -- loadModule will calculate the canonical path again
         Maybe (LoadedModuleG TCTopEntity)
Nothing ->
           Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Map [Char] Fingerprint
-> Module PName
-> ModuleM TCTopEntity
loadModuleAndDeps Bool
eval Bool
False
             (ModName -> ImportSource
FromModule ModName
n) ([Char] -> ModulePath
InFile [Char]
foundPath) Fingerprint
fp Map [Char] Fingerprint
deps Module PName
pm
         Just LoadedModuleG TCTopEntity
lm
          | [Char]
path' [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
loaded -> TCTopEntity -> ModuleM TCTopEntity
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LoadedModuleG TCTopEntity -> TCTopEntity
forall a. LoadedModuleG a -> a
lmData LoadedModuleG TCTopEntity
lm)
          | Bool
otherwise       -> ModName -> [Char] -> [Char] -> ModuleM TCTopEntity
forall a. ModName -> [Char] -> [Char] -> ModuleM a
duplicateModuleName ModName
n [Char]
path' [Char]
loaded
          where loaded :: [Char]
loaded = LoadedModuleG TCTopEntity -> [Char]
forall a. LoadedModuleG a -> [Char]
lmModuleId LoadedModuleG TCTopEntity
lm


-- | Load a module, unless it was previously loaded.
loadModuleFrom ::
  Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.TCTopEntity)
loadModuleFrom :: Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
loadModuleFrom Bool
quiet ImportSource
isrc =
  do let n :: ModName
n = ImportSource -> ModName
importedModule ImportSource
isrc
     Maybe (LoadedModuleG TCTopEntity)
mb <- ModName -> ModuleM (Maybe (LoadedModuleG TCTopEntity))
getLoadedMaybe ModName
n
     case Maybe (LoadedModuleG TCTopEntity)
mb of
       Just LoadedModuleG TCTopEntity
m -> (ModulePath, TCTopEntity) -> ModuleM (ModulePath, TCTopEntity)
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LoadedModuleG TCTopEntity -> ModulePath
forall a. LoadedModuleG a -> ModulePath
lmFilePath LoadedModuleG TCTopEntity
m, LoadedModuleG TCTopEntity -> TCTopEntity
forall a. LoadedModuleG a -> a
lmData LoadedModuleG TCTopEntity
m)
       Maybe (LoadedModuleG TCTopEntity)
Nothing ->
         do ModulePath
path <- ModName -> ModuleM ModulePath
findModule ModName
n
            ModulePath
-> ModuleM (ModulePath, TCTopEntity)
-> ModuleM (ModulePath, TCTopEntity)
forall a. ModulePath -> ModuleM a -> ModuleM a
errorInFile ModulePath
path (ModuleM (ModulePath, TCTopEntity)
 -> ModuleM (ModulePath, TCTopEntity))
-> ModuleM (ModulePath, TCTopEntity)
-> ModuleM (ModulePath, TCTopEntity)
forall a b. (a -> b) -> a -> b
$
              do (Fingerprint
fp, Map [Char] Fingerprint
deps, [Module PName]
pms) <- ModulePath
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
parseModule ModulePath
path
                 [TCTopEntity]
ms <- (Module PName -> ModuleM TCTopEntity)
-> [Module PName] -> ModuleT IO [TCTopEntity]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Map [Char] Fingerprint
-> Module PName
-> ModuleM TCTopEntity
loadModuleAndDeps Bool
True Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Map [Char] Fingerprint
deps) [Module PName]
pms
                 (ModulePath, TCTopEntity) -> ModuleM (ModulePath, TCTopEntity)
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ModulePath
path,[TCTopEntity] -> TCTopEntity
forall a. HasCallStack => [a] -> a
last [TCTopEntity]
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 :: Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Map [Char] Fingerprint
-> Module PName
-> ModuleM TCTopEntity
loadModuleAndDeps Bool
eval Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Map [Char] Fingerprint
incDeps Module PName
pm0 =
  ImportSource -> ModuleM TCTopEntity -> ModuleM TCTopEntity
forall a. ImportSource -> ModuleM a -> ModuleM a
loading ImportSource
isrc (ModuleM TCTopEntity -> ModuleM TCTopEntity)
-> ModuleM TCTopEntity -> ModuleM TCTopEntity
forall a b. (a -> b) -> a -> b
$
  do let pm :: Module PName
pm = Module PName -> Module PName
addPrelude Module PName
pm0
     Set ModName
impDeps <- Module PName -> ModuleM (Set ModName)
forall mname name. ModuleG mname name -> ModuleM (Set ModName)
loadDeps Module PName
pm
     (TCTopEntity, FileInfo) -> TCTopEntity
forall a b. (a, b) -> a
fst ((TCTopEntity, FileInfo) -> TCTopEntity)
-> ModuleT IO (TCTopEntity, FileInfo) -> ModuleM TCTopEntity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Map [Char] Fingerprint
-> Module PName
-> Set ModName
-> ModuleT IO (TCTopEntity, FileInfo)
doLoadModule Bool
eval Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Map [Char] Fingerprint
incDeps Module PName
pm Set ModName
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 :: Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Map [Char] Fingerprint
-> Module PName
-> Set ModName
-> ModuleT IO (TCTopEntity, FileInfo)
doLoadModule Bool
eval Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Map [Char] Fingerprint
incDeps Module PName
pm Set ModName
impDeps =
  do let what :: [Char]
what = case Module PName -> ModuleDefinition PName
forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef Module PName
pm of
                  P.InterfaceModule {} -> [Char]
"interface module"
                  ModuleDefinition PName
_                    -> [Char]
"module"

     Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ (Logger -> [Char] -> IO ()) -> [Char] -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger Logger -> [Char] -> IO ()
logPutStrLn
       ([Char]
"Loading " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModName -> [Char]
forall a. PP a => a -> [Char]
pretty (Located ModName -> ModName
forall a. Located a -> a
P.thing (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
pm)))


     (NamingEnv
nameEnv,TCTopEntity
tcm) <- ImportSource -> Module PName -> ModuleM (NamingEnv, TCTopEntity)
checkModule ImportSource
isrc Module PName
pm

     -- extend the eval env, unless a functor.
     Map PrimIdent (Prim Concrete)
tbl <- IO EvalOpts -> Map PrimIdent (Prim Concrete)
Concrete.primTable (IO EvalOpts -> Map PrimIdent (Prim Concrete))
-> ModuleT IO (IO EvalOpts)
-> ModuleT IO (Map PrimIdent (Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleT IO (IO EvalOpts)
getEvalOptsAction
     let ?evalPrim = \PrimIdent
i -> Prim Concrete -> Either Expr (Prim Concrete)
forall a b. b -> Either a b
Right (Prim Concrete -> Either Expr (Prim Concrete))
-> Maybe (Prim Concrete) -> Maybe (Either Expr (Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent -> Map PrimIdent (Prim Concrete) -> Maybe (Prim Concrete)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
     Bool
callStacks <- ModuleM Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
     let ?callStacks = ?callStacks::Bool
Bool
callStacks
     let shouldEval :: Maybe (ModuleG ModName)
shouldEval =
           case TCTopEntity
tcm of
             T.TCTopModule ModuleG ModName
m | Bool
eval Bool -> Bool -> Bool
&& Bool -> Bool
not (ModuleG ModName -> Bool
forall mname. ModuleG mname -> Bool
T.isParametrizedModule ModuleG ModName
m) -> ModuleG ModName -> Maybe (ModuleG ModName)
forall a. a -> Maybe a
Just ModuleG ModName
m
             TCTopEntity
_ -> Maybe (ModuleG ModName)
forall a. Maybe a
Nothing

     Maybe ForeignSrc
foreignSrc <- case Maybe (ModuleG ModName)
shouldEval of
                      Just ModuleG ModName
m ->
                        do Maybe ForeignSrc
fsrc <- ModuleG ModName -> ModuleT IO (Maybe ForeignSrc)
evalForeign ModuleG ModName
m
                           (EvalEnv -> Eval EvalEnv) -> ModuleM ()
modifyEvalEnv (Concrete -> ModuleG ModName -> EvalEnv -> SEval Concrete EvalEnv
forall sym.
EvalPrims sym =>
sym
-> ModuleG ModName -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
E.moduleEnv Concrete
Concrete ModuleG ModName
m)
                           Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
fsrc
                      Maybe (ModuleG ModName)
Nothing -> Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
forall a. Maybe a
Nothing

     let fi :: FileInfo
fi = Fingerprint
-> Map [Char] Fingerprint
-> Set ModName
-> Maybe ForeignSrc
-> FileInfo
fileInfo Fingerprint
fp Map [Char] Fingerprint
incDeps Set ModName
impDeps Maybe ForeignSrc
foreignSrc
     ModulePath
-> FileInfo
-> NamingEnv
-> Maybe ForeignSrc
-> TCTopEntity
-> ModuleM ()
loadedModule ModulePath
path FileInfo
fi NamingEnv
nameEnv Maybe ForeignSrc
foreignSrc TCTopEntity
tcm

     (TCTopEntity, FileInfo) -> ModuleT IO (TCTopEntity, FileInfo)
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (TCTopEntity
tcm, FileInfo
fi)

  where
  evalForeign :: ModuleG ModName -> ModuleT IO (Maybe ForeignSrc)
evalForeign ModuleG ModName
tcm
    | Bool -> Bool
not ([Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
foreignFs) =
      ModName -> [FFILoadError] -> ModuleT IO (Maybe ForeignSrc)
forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) ((Name -> FFILoadError) -> [Name] -> [FFILoadError]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FFILoadError
FFI.FFIInFunctor [Name]
foreignFs)
    | Bool -> Bool
not ([NonEmpty Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NonEmpty Name]
dups) =
      ModName -> [FFILoadError] -> ModuleT IO (Maybe ForeignSrc)
forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) ((NonEmpty Name -> FFILoadError)
-> [NonEmpty Name] -> [FFILoadError]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty Name -> FFILoadError
FFI.FFIDuplicates [NonEmpty Name]
dups)
    | [(Name, FFIFunType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, FFIFunType)]
foreigns = Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
forall a. Maybe a
Nothing
    | Bool
otherwise =
      ModuleM EvalForeignPolicy
getEvalForeignPolicy ModuleM EvalForeignPolicy
-> (EvalForeignPolicy -> ModuleT IO (Maybe ForeignSrc))
-> ModuleT IO (Maybe ForeignSrc)
forall a b. ModuleT IO a -> (a -> ModuleT IO b) -> ModuleT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        EvalForeignPolicy
AlwaysEvalForeign -> ([FFILoadError] -> ModuleM ()) -> ModuleT IO (Maybe ForeignSrc)
doEvalForeign (ModName -> [FFILoadError] -> ModuleM ()
forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm))
        EvalForeignPolicy
PreferEvalForeign -> ([FFILoadError] -> ModuleM ()) -> ModuleT IO (Maybe ForeignSrc)
doEvalForeign \[FFILoadError]
errs ->
          (Logger -> Doc -> IO ()) -> Doc -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger Logger -> Doc -> IO ()
forall a. Show a => Logger -> a -> IO ()
logPrint (Doc -> ModuleM ()) -> Doc -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
            Doc -> Int -> Doc -> Doc
hang
              (Doc
"[warning] Could not load all foreign implementations for module"
                Doc -> Doc -> Doc
<+> ModName -> Doc
forall a. PP a => a -> Doc
pp (ModuleG ModName -> ModName
forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) Doc -> Doc -> Doc
<.> Doc
colon) Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
              [Doc] -> Doc
vcat ((FFILoadError -> Doc) -> [FFILoadError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map FFILoadError -> Doc
forall a. PP a => a -> Doc
pp [FFILoadError]
errs)
              Doc -> Doc -> Doc
$$ Doc
"Fallback cryptol implementations will be used if available"
        EvalForeignPolicy
NeverEvalForeign -> Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
forall a. Maybe a
Nothing

    where foreigns :: [(Name, FFIFunType)]
foreigns  = ModuleG ModName -> [(Name, FFIFunType)]
forall mname. ModuleG mname -> [(Name, FFIFunType)]
findForeignDecls ModuleG ModName
tcm
          foreignFs :: [Name]
foreignFs = ModuleG ModName -> [Name]
forall mname. ModuleG mname -> [Name]
T.findForeignDeclsInFunctors ModuleG ModName
tcm
          dups :: [NonEmpty Name]
dups      = [ NonEmpty Name
d | d :: NonEmpty Name
d@(Name
_ :| Name
_ : [Name]
_) <- (Name -> Name -> Bool) -> [Name] -> [NonEmpty Name]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NE.groupBy (Ident -> Ident -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Ident -> Ident -> Bool) -> (Name -> Ident) -> Name -> Name -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Ident
nameIdent)
                                            ([Name] -> [NonEmpty Name]) -> [Name] -> [NonEmpty Name]
forall a b. (a -> b) -> a -> b
$ (Name -> Name -> Ordering) -> [Name] -> [Name]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Ident -> Ident -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Ident -> Ident -> Ordering)
-> (Name -> Ident) -> Name -> Name -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Ident
nameIdent)
                                            ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ ((Name, FFIFunType) -> Name) -> [(Name, FFIFunType)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, FFIFunType) -> Name
forall a b. (a, b) -> a
fst [(Name, FFIFunType)]
foreigns ]
          doEvalForeign :: ([FFILoadError] -> ModuleM ()) -> ModuleT IO (Maybe ForeignSrc)
doEvalForeign [FFILoadError] -> ModuleM ()
handleErrs =
            case ModulePath
path of
              InFile [Char]
p -> IO (Either FFILoadError ForeignSrc)
-> ModuleT IO (Either FFILoadError ForeignSrc)
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc [Char]
p) ModuleT IO (Either FFILoadError ForeignSrc)
-> (Either FFILoadError ForeignSrc
    -> ModuleT IO (Maybe ForeignSrc))
-> ModuleT IO (Maybe ForeignSrc)
forall a b. ModuleT IO a -> (a -> ModuleT IO b) -> ModuleT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                \case

                  Right ForeignSrc
fsrc -> do
                    Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
                      case ForeignSrc -> Maybe [Char]
getForeignSrcPath ForeignSrc
fsrc of
                        Just [Char]
fpath -> (Logger -> [Char] -> IO ()) -> [Char] -> ModuleM ()
forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger Logger -> [Char] -> IO ()
logPutStrLn ([Char] -> ModuleM ()) -> [Char] -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
                          [Char]
"Loading dynamic library " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
takeFileName [Char]
fpath
                        Maybe [Char]
Nothing -> () -> ModuleM ()
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                    ([FFILoadError]
errs, ()) <-
                      (EvalEnv -> Eval ([FFILoadError], EvalEnv))
-> ModuleM ([FFILoadError], ())
forall (t :: * -> *).
Traversable t =>
(EvalEnv -> Eval (t EvalEnv)) -> ModuleM (t ())
modifyEvalEnvM (ForeignSrc
-> [(Name, FFIFunType)]
-> EvalEnv
-> Eval ([FFILoadError], EvalEnv)
evalForeignDecls ForeignSrc
fsrc [(Name, FFIFunType)]
foreigns)
                    Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FFILoadError] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FFILoadError]
errs) (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$
                      [FFILoadError] -> ModuleM ()
handleErrs [FFILoadError]
errs
                    Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc))
-> Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a b. (a -> b) -> a -> b
$ ForeignSrc -> Maybe ForeignSrc
forall a. a -> Maybe a
Just ForeignSrc
fsrc

                  Left FFILoadError
err -> do
                    [FFILoadError] -> ModuleM ()
handleErrs [FFILoadError
err]
                    Maybe ForeignSrc -> ModuleT IO (Maybe ForeignSrc)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
forall a. Maybe a
Nothing

              InMem [Char]
m ByteString
_ -> [Char] -> [[Char]] -> ModuleT IO (Maybe ForeignSrc)
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"doLoadModule"
                [[Char]
"Can't find foreign source of in-memory module", [Char]
m]

-- | 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 Import
i = Import
i { iAs = Just (iModule i) }

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


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

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

    [] -> ModuleM ModulePath
handleNotFound

  handleNotFound :: ModuleM ModulePath
handleNotFound =
    case ModName
n of
      ModName
m | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Cryptol" ByteString
preludeContents)
        | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
floatName   -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Float" ByteString
floatContents)
        | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
arrayName   -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Array" ByteString
arrayContents)
        | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
suiteBName  -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"SuiteB" ByteString
suiteBContents)
        | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
primeECName -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"PrimeEC" ByteString
primeECContents)
        | ModName
m ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeReferenceName -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Cryptol::Reference" ByteString
preludeReferenceContents)
      ModName
_ -> ModName -> [[Char]] -> ModuleM ModulePath
forall a. ModName -> [[Char]] -> ModuleM a
moduleNotFound ModName
n ([[Char]] -> ModuleM ModulePath)
-> ModuleM [[Char]] -> ModuleM ModulePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleM [[Char]]
getSearchPath

  -- generate all possible search paths
  possibleFiles :: [[Char]] -> [[Char]]
possibleFiles [[Char]]
paths = do
    [Char]
path <- [[Char]]
paths
    [Char]
ext  <- [[Char]]
P.knownExts
    [Char] -> [[Char]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
path [Char] -> [Char] -> [Char]
</> ModName -> [Char] -> [Char]
moduleFile ModName
n [Char]
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 :: [Char] -> ModuleM [Char]
findFile [Char]
path
  | [Char] -> Bool
isAbsolute [Char]
path =
    do -- No search path checking for absolute paths
       Bool
b <- IO Bool -> ModuleM Bool
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO Bool
doesFileExist [Char]
path)
       if Bool
b then [Char] -> ModuleM [Char]
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
path else [Char] -> ModuleM [Char]
forall a. [Char] -> ModuleT IO a
cantFindFile [Char]
path
  | Bool
otherwise =
    do [[Char]]
paths <- ModuleM [[Char]]
getSearchPath
       [[Char]] -> ModuleM [Char]
loop ([[Char]] -> [[Char]]
possibleFiles [[Char]]
paths)
       where
       loop :: [[Char]] -> ModuleM [Char]
loop [[Char]]
paths = case [[Char]]
paths of
                      [Char]
path' : [[Char]]
rest ->
                        do Bool
b <- IO Bool -> ModuleM Bool
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO Bool
doesFileExist [Char]
path')
                           if Bool
b then [Char] -> ModuleM [Char]
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> [Char]
normalise [Char]
path') else [[Char]] -> ModuleM [Char]
loop [[Char]]
rest
                      [] -> [Char] -> ModuleM [Char]
forall a. [Char] -> ModuleT IO a
cantFindFile [Char]
path
       possibleFiles :: [[Char]] -> [[Char]]
possibleFiles [[Char]]
paths = ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char] -> [Char]
</> [Char]
path) [[Char]]
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 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 mname name. ModuleG mname name -> Located mname
P.mName Module PName
m) = Module PName
m
  | ModName
preludeName ModName -> [ModName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModName]
importedMods    = Module PName
m
  | Bool
otherwise                          = Module PName
m { mDef = newDef }
  where
  newDef :: ModuleDefinition PName
newDef =
    case Module PName -> ModuleDefinition PName
forall mname name. ModuleG mname name -> ModuleDefinition name
mDef Module PName
m of
      NormalModule [TopDecl PName]
ds -> [TopDecl PName] -> ModuleDefinition PName
forall name. [TopDecl name] -> ModuleDefinition name
NormalModule (Located (ImportG (ImpName PName)) -> TopDecl PName
forall name. Located (ImportG (ImpName name)) -> TopDecl name
P.DImport Located (ImportG (ImpName PName))
forall {name}. Located (ImportG (ImpName name))
prel TopDecl PName -> [TopDecl PName] -> [TopDecl PName]
forall a. a -> [a] -> [a]
: [TopDecl PName]
ds)
      FunctorInstance Located (ImpName PName)
f ModuleInstanceArgs PName
as ModuleInstance PName
ins -> Located (ImpName PName)
-> ModuleInstanceArgs PName
-> ModuleInstance PName
-> ModuleDefinition PName
forall name.
Located (ImpName name)
-> ModuleInstanceArgs name
-> ModuleInstance name
-> ModuleDefinition name
FunctorInstance Located (ImpName PName)
f ModuleInstanceArgs PName
as ModuleInstance PName
ins
      InterfaceModule Signature PName
s -> Signature PName -> ModuleDefinition PName
forall name. Signature name -> ModuleDefinition name
InterfaceModule Signature PName
s { sigImports = prel
                                             : sigImports s }

  importedMods :: [ModName]
importedMods  = (Located Import -> ModName) -> [Located Import] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map (Import -> ModName
forall mname. ImportG mname -> mname
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 mname name. ModuleG mname name -> [Located Import]
P.mImports Module PName
m)
  prel :: Located (ImportG (ImpName name))
prel = P.Located
    { srcRange :: Range
P.srcRange = Range
emptyRange
    , thing :: ImportG (ImpName name)
P.thing    = P.Import
      { iModule :: ImpName name
iModule  = ModName -> ImpName name
forall name. ModName -> ImpName name
P.ImpTop ModName
preludeName
      , iAs :: Maybe ModName
iAs      = Maybe ModName
forall a. Maybe a
Nothing
      , iSpec :: Maybe ImportSpec
iSpec    = Maybe ImportSpec
forall a. Maybe a
Nothing
      , iInst :: Maybe (ModuleInstanceArgs PName)
iInst    = Maybe (ModuleInstanceArgs PName)
forall a. Maybe a
Nothing
      , iDoc :: Maybe (Located Text)
iDoc     = Maybe (Located Text)
forall a. Maybe a
Nothing
      }
    }

-- | Load the dependencies of a module into the environment.
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName)
loadDeps :: forall mname name. ModuleG mname name -> ModuleM (Set ModName)
loadDeps ModuleG mname name
m =
  do let ds :: [ImportSource]
ds = ModuleG mname name -> [ImportSource]
forall mname name. ModuleG mname name -> [ImportSource]
findDeps ModuleG mname name
m
     (ImportSource -> ModuleM (ModulePath, TCTopEntity))
-> [ImportSource] -> ModuleM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> ImportSource -> ModuleM (ModulePath, TCTopEntity)
loadModuleFrom Bool
False) [ImportSource]
ds
     Set ModName -> ModuleM (Set ModName)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ModName] -> Set ModName
forall a. Ord a => [a] -> Set a
Set.fromList ((ImportSource -> ModName) -> [ImportSource] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule [ImportSource]
ds))

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

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

findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
findDepsOf ModulePath
mpath' =
  do ModulePath
mpath <- case ModulePath
mpath' of
                InFile [Char]
file -> [Char] -> ModulePath
InFile ([Char] -> ModulePath) -> ModuleM [Char] -> ModuleM ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [Char] -> ModuleM [Char]
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO [Char]
canonicalizePath [Char]
file)
                InMem {}    -> ModulePath -> ModuleM ModulePath
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModulePath
mpath'
     (FileInfo
fi, [(Module PName, [ImportSource])]
_) <- ModulePath -> ModuleM (FileInfo, [(Module PName, [ImportSource])])
parseWithDeps ModulePath
mpath
     (ModulePath, FileInfo) -> ModuleM (ModulePath, FileInfo)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModulePath
mpath, FileInfo
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 :: ModulePath -> ModuleM (FileInfo, [(Module PName, [ImportSource])])
parseWithDeps ModulePath
mpath =
  do (Fingerprint
fp, Map [Char] Fingerprint
incs, [Module PName]
ms) <- ModulePath
-> ModuleM (Fingerprint, Map [Char] Fingerprint, [Module PName])
parseModule ModulePath
mpath
     let ms' :: [Module PName]
ms' = (Module PName -> Module PName) -> [Module PName] -> [Module PName]
forall a b. (a -> b) -> [a] -> [b]
map Module PName -> Module PName
addPrelude [Module PName]
ms
         depss :: [(Any, Endo [ImportSource])]
depss = (Module PName -> (Any, Endo [ImportSource]))
-> [Module PName] -> [(Any, Endo [ImportSource])]
forall a b. (a -> b) -> [a] -> [b]
map Module PName -> (Any, Endo [ImportSource])
forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' [Module PName]
ms'
     let (Any
anyF,Endo [ImportSource]
imps) = [(Any, Endo [ImportSource])] -> (Any, Endo [ImportSource])
forall a. Monoid a => [a] -> a
mconcat [(Any, Endo [ImportSource])]
depss
     Map [Char] Bool
fpath <- if Any -> Bool
getAny Any
anyF
                then do Maybe ([Char], Bool)
mb <- IO (Maybe ([Char], Bool)) -> ModuleT IO (Maybe ([Char], Bool))
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io case ModulePath
mpath of
                                   InFile [Char]
path -> [Char] -> IO (Maybe ([Char], Bool))
foreignLibPath [Char]
path
                                   InMem {}    -> Maybe ([Char], Bool) -> IO (Maybe ([Char], Bool))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ([Char], Bool)
forall a. Maybe a
Nothing
                        Map [Char] Bool -> ModuleT IO (Map [Char] Bool)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure case Maybe ([Char], Bool)
mb of
                               Maybe ([Char], Bool)
Nothing -> Map [Char] Bool
forall k a. Map k a
Map.empty
                               Just ([Char]
fpath, Bool
exists) ->
                                 [Char] -> Bool -> Map [Char] Bool
forall k a. k -> a -> Map k a
Map.singleton [Char]
fpath Bool
exists
                else Map [Char] Bool -> ModuleT IO (Map [Char] Bool)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map [Char] Bool
forall k a. Map k a
Map.empty
     (FileInfo, [(Module PName, [ImportSource])])
-> ModuleM (FileInfo, [(Module PName, [ImportSource])])
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
       ( FileInfo
           { fiFingerprint :: Fingerprint
fiFingerprint = Fingerprint
fp
           , fiIncludeDeps :: Map [Char] Fingerprint
fiIncludeDeps = Map [Char] Fingerprint
incs
           , fiImportDeps :: Set ModName
fiImportDeps  = [ModName] -> Set ModName
forall a. Ord a => [a] -> Set a
Set.fromList ((ImportSource -> ModName) -> [ImportSource] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule (Endo [ImportSource] -> [ImportSource] -> [ImportSource]
forall a. Endo a -> a -> a
appEndo Endo [ImportSource]
imps []))
           , fiForeignDeps :: Map [Char] Bool
fiForeignDeps = Map [Char] Bool
fpath
           }
       , [Module PName]
-> [[ImportSource]] -> [(Module PName, [ImportSource])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Module PName]
ms' ([[ImportSource]] -> [(Module PName, [ImportSource])])
-> [[ImportSource]] -> [(Module PName, [ImportSource])]
forall a b. (a -> b) -> a -> b
$ ((Any, Endo [ImportSource]) -> [ImportSource])
-> [(Any, Endo [ImportSource])] -> [[ImportSource]]
forall a b. (a -> b) -> [a] -> [b]
map ((Endo [ImportSource] -> [ImportSource] -> [ImportSource]
forall a. Endo a -> a -> a
`appEndo` []) (Endo [ImportSource] -> [ImportSource])
-> ((Any, Endo [ImportSource]) -> Endo [ImportSource])
-> (Any, Endo [ImportSource])
-> [ImportSource]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Any, Endo [ImportSource]) -> Endo [ImportSource]
forall a b. (a, b) -> b
snd) [(Any, Endo [ImportSource])]
depss
       )

-- | Find the set of top-level modules imported by a module.
findModuleDeps :: P.ModuleG mname name -> Set P.ModName
findModuleDeps :: forall mname name. ModuleG mname name -> Set ModName
findModuleDeps = [ModName] -> Set ModName
forall a. Ord a => [a] -> Set a
Set.fromList ([ModName] -> Set ModName)
-> (ModuleG mname name -> [ModName])
-> ModuleG mname name
-> Set ModName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ImportSource -> ModName) -> [ImportSource] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule ([ImportSource] -> [ModName])
-> (ModuleG mname name -> [ImportSource])
-> ModuleG mname name
-> [ModName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleG mname name -> [ImportSource]
forall mname name. ModuleG mname name -> [ImportSource]
findDeps

-- | A helper `findDeps` and `findModuleDeps` that actually does the searching.
findDeps' :: P.ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' :: forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' ModuleG mname name
m =
  case ModuleG mname name -> ModuleDefinition name
forall mname name. ModuleG mname name -> ModuleDefinition name
mDef ModuleG mname name
m of
    NormalModule [TopDecl name]
ds -> [(Any, Endo [ImportSource])] -> (Any, Endo [ImportSource])
forall a. Monoid a => [a] -> a
mconcat ((TopDecl name -> (Any, Endo [ImportSource]))
-> [TopDecl name] -> [(Any, Endo [ImportSource])]
forall a b. (a -> b) -> [a] -> [b]
map TopDecl name -> (Any, Endo [ImportSource])
forall {name}. TopDecl name -> (Any, Endo [ImportSource])
depsOfDecl [TopDecl name]
ds)
    FunctorInstance Located (ImpName name)
f ModuleInstanceArgs name
as ModuleInstance name
_ ->
      let fds :: (Any, Endo [ImportSource])
fds = (Located ModName -> ImportSource)
-> Located (ImpName name) -> (Any, Endo [ImportSource])
forall {a} {a} {name}.
Monoid a =>
(Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName Located ModName -> ImportSource
FromModuleInstance Located (ImpName name)
f
          ads :: (Any, Endo [ImportSource])
ads = case ModuleInstanceArgs name
as of
                  DefaultInstArg Located (ModuleInstanceArg name)
a -> Located (ModuleInstanceArg name) -> (Any, Endo [ImportSource])
forall {a} {name}.
Monoid a =>
Located (ModuleInstanceArg name) -> (a, Endo [ImportSource])
loadInstArg Located (ModuleInstanceArg name)
a
                  DefaultInstAnonArg [TopDecl name]
ds -> [(Any, Endo [ImportSource])] -> (Any, Endo [ImportSource])
forall a. Monoid a => [a] -> a
mconcat ((TopDecl name -> (Any, Endo [ImportSource]))
-> [TopDecl name] -> [(Any, Endo [ImportSource])]
forall a b. (a -> b) -> [a] -> [b]
map TopDecl name -> (Any, Endo [ImportSource])
forall {name}. TopDecl name -> (Any, Endo [ImportSource])
depsOfDecl [TopDecl name]
ds)
                  NamedInstArgs [ModuleInstanceNamedArg name]
args -> [(Any, Endo [ImportSource])] -> (Any, Endo [ImportSource])
forall a. Monoid a => [a] -> a
mconcat ((ModuleInstanceNamedArg name -> (Any, Endo [ImportSource]))
-> [ModuleInstanceNamedArg name] -> [(Any, Endo [ImportSource])]
forall a b. (a -> b) -> [a] -> [b]
map ModuleInstanceNamedArg name -> (Any, Endo [ImportSource])
forall {a} {name}.
Monoid a =>
ModuleInstanceNamedArg name -> (a, Endo [ImportSource])
loadNamedInstArg [ModuleInstanceNamedArg name]
args)
      in (Any, Endo [ImportSource])
fds (Any, Endo [ImportSource])
-> (Any, Endo [ImportSource]) -> (Any, Endo [ImportSource])
forall a. Semigroup a => a -> a -> a
<> (Any, Endo [ImportSource])
ads
    InterfaceModule Signature name
s -> [(Any, Endo [ImportSource])] -> (Any, Endo [ImportSource])
forall a. Monoid a => [a] -> a
mconcat ((Located (ImportG (ImpName name)) -> (Any, Endo [ImportSource]))
-> [Located (ImportG (ImpName name))]
-> [(Any, Endo [ImportSource])]
forall a b. (a -> b) -> [a] -> [b]
map Located (ImportG (ImpName name)) -> (Any, Endo [ImportSource])
forall {a} {name}.
Monoid a =>
Located (ImportG (ImpName name)) -> (a, Endo [ImportSource])
loadImpD (Signature name -> [Located (ImportG (ImpName name))]
forall name. Signature name -> [Located (ImportG (ImpName name))]
sigImports Signature name
s))
  where
  loadI :: a -> (a, Endo [a])
loadI a
i = (a
forall a. Monoid a => a
mempty, ([a] -> [a]) -> Endo [a]
forall a. (a -> a) -> Endo a
Endo (a
ia -> [a] -> [a]
forall a. a -> [a] -> [a]
:))

  loadImpName :: (Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName Located ModName -> a
src Located (ImpName name)
l =
    case Located (ImpName name) -> ImpName name
forall a. Located a -> a
thing Located (ImpName name)
l of
      ImpTop ModName
f -> a -> (a, Endo [a])
forall {a} {a}. Monoid a => a -> (a, Endo [a])
loadI (Located ModName -> a
src Located (ImpName name)
l { thing = f })
      ImpName name
_        -> (a, Endo [a])
forall a. Monoid a => a
mempty

  loadImpD :: Located (ImportG (ImpName name)) -> (a, Endo [ImportSource])
loadImpD Located (ImportG (ImpName name))
li = (Located ModName -> ImportSource)
-> Located (ImpName name) -> (a, Endo [ImportSource])
forall {a} {a} {name}.
Monoid a =>
(Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName (Located Import -> ImportSource
FromImport (Located Import -> ImportSource)
-> (Located ModName -> Located Import)
-> Located ModName
-> ImportSource
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located ModName -> Located Import
forall {mname}. Located mname -> Located (ImportG mname)
new) (ImportG (ImpName name) -> ImpName name
forall mname. ImportG mname -> mname
iModule (ImportG (ImpName name) -> ImpName name)
-> Located (ImportG (ImpName name)) -> Located (ImpName name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (ImportG (ImpName name))
li)
    where new :: Located mname -> Located (ImportG mname)
new Located mname
i = Located mname
i { thing = (thing li) { iModule = thing i } }

  loadNamedInstArg :: ModuleInstanceNamedArg name -> (a, Endo [ImportSource])
loadNamedInstArg (ModuleInstanceNamedArg Located Ident
_ Located (ModuleInstanceArg name)
f) = Located (ModuleInstanceArg name) -> (a, Endo [ImportSource])
forall {a} {name}.
Monoid a =>
Located (ModuleInstanceArg name) -> (a, Endo [ImportSource])
loadInstArg Located (ModuleInstanceArg name)
f
  loadInstArg :: Located (ModuleInstanceArg name) -> (a, Endo [ImportSource])
loadInstArg Located (ModuleInstanceArg name)
f =
    case Located (ModuleInstanceArg name) -> ModuleInstanceArg name
forall a. Located a -> a
thing Located (ModuleInstanceArg name)
f of
      ModuleArg ImpName name
mo -> (Located ModName -> ImportSource)
-> Located (ImpName name) -> (a, Endo [ImportSource])
forall {a} {a} {name}.
Monoid a =>
(Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName Located ModName -> ImportSource
FromModuleInstance Located (ModuleInstanceArg name)
f { thing = mo }
      ModuleInstanceArg name
_            -> (a, Endo [ImportSource])
forall a. Monoid a => a
mempty

  depsOfDecl :: TopDecl name -> (Any, Endo [ImportSource])
depsOfDecl TopDecl name
d =
    case TopDecl name
d of
      DImport Located (ImportG (ImpName name))
li -> Located (ImportG (ImpName name)) -> (Any, Endo [ImportSource])
forall {a} {name}.
Monoid a =>
Located (ImportG (ImpName name)) -> (a, Endo [ImportSource])
loadImpD Located (ImportG (ImpName name))
li

      DModule TopLevel { tlValue :: forall a. TopLevel a -> a
tlValue = NestedModule ModuleG name name
nm } -> ModuleG name name -> (Any, Endo [ImportSource])
forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' ModuleG name name
nm

      DModParam ModParam name
mo -> (Located ModName -> ImportSource)
-> Located (ImpName name) -> (Any, Endo [ImportSource])
forall {a} {a} {name}.
Monoid a =>
(Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName Located ModName -> ImportSource
FromSigImport Located (ImpName name)
s
        where s :: Located (ImpName name)
s = ModParam name -> Located (ImpName name)
forall name. ModParam name -> Located (ImpName name)
mpSignature ModParam name
mo

      Decl TopLevel (Decl name)
dd -> Decl name -> (Any, Endo [ImportSource])
forall {b} {name}. Monoid b => Decl name -> (Any, b)
depsOfDecl' (TopLevel (Decl name) -> Decl name
forall a. TopLevel a -> a
tlValue TopLevel (Decl name)
dd)

      TopDecl name
_ -> (Any, Endo [ImportSource])
forall a. Monoid a => a
mempty

  depsOfDecl' :: Decl name -> (Any, b)
depsOfDecl' Decl name
d =
    case Decl name
d of
      DLocated Decl name
d' Range
_ -> Decl name -> (Any, b)
depsOfDecl' Decl name
d'
      DBind Bind name
b ->
        case Located (BindDef name) -> BindDef name
forall a. Located a -> a
thing (Bind name -> Located (BindDef name)
forall name. Bind name -> Located (BindDef name)
bDef Bind name
b) of
          DForeign {} -> (Bool -> Any
Any Bool
True, b
forall a. Monoid a => a
mempty)
          BindDef name
_ -> (Any, b)
forall a. Monoid a => a
mempty
      Decl name
_ -> (Any, b)
forall a. Monoid a => a
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 :: Expr PName -> ModuleM (Expr Name, Expr, Schema)
checkExpr Expr PName
e = do

  ModContext
fe <- ModuleM ModContext
getFocusedEnv
  let params :: ModContextParams
params = ModContext -> ModContextParams
mctxParams ModContext
fe
      decls :: IfaceDecls
decls  = ModContext -> IfaceDecls
mctxDecls ModContext
fe
      names :: NamingEnv
names  = ModContext -> NamingEnv
mctxNames ModContext
fe

  -- 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 { 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 }
  (Expr
te,Schema
s) <- TCAction (Expr Name) (Expr, Schema)
-> Expr Name
-> ModContextParams
-> IfaceDecls
-> ModuleM (Expr, Schema)
forall i o.
(Show i, Show o, HasLoc i) =>
TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck TCAction (Expr Name) (Expr, Schema)
act Expr Name
re ModContextParams
params IfaceDecls
decls

  (Expr Name, Expr, Schema) -> ModuleM (Expr Name, Expr, Schema)
forall a. a -> ModuleT IO a
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], Map.Map Name T.TySyn)
checkDecls :: [TopDecl PName] -> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
checkDecls [TopDecl PName]
ds = do
  ModContext
fe <- ModuleM ModContext
getFocusedEnv
  let params :: ModContextParams
params = ModContext -> ModContextParams
mctxParams ModContext
fe
      decls :: IfaceDecls
decls  = ModContext -> IfaceDecls
mctxDecls  ModContext
fe
      names :: NamingEnv
names  = ModContext -> NamingEnv
mctxNames  ModContext
fe

  (NamingEnv
declsEnv,[TopDecl Name]
rds) <- ModName
-> NamingEnv
-> RenameM (NamingEnv, [TopDecl Name])
-> ModuleM (NamingEnv, [TopDecl Name])
forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename ModName
interactiveName NamingEnv
names
                  (RenameM (NamingEnv, [TopDecl Name])
 -> ModuleM (NamingEnv, [TopDecl Name]))
-> RenameM (NamingEnv, [TopDecl Name])
-> ModuleM (NamingEnv, [TopDecl Name])
forall a b. (a -> b) -> a -> b
$ ModName -> [TopDecl PName] -> RenameM (NamingEnv, [TopDecl Name])
R.renameTopDecls ModName
interactiveName [TopDecl PName]
ds
  PrimMap
prims <- ModuleM PrimMap
getPrimMap
  let act :: TCAction [TopDecl Name] ([DeclGroup], Map Name TySyn)
act  = TCAction { tcAction :: Act [TopDecl Name] ([DeclGroup], Map Name TySyn)
tcAction = Act [TopDecl Name] ([DeclGroup], Map Name TySyn)
T.tcDecls, tcLinter :: TCLinter ([DeclGroup], Map Name TySyn)
tcLinter = TCLinter ([DeclGroup], Map Name TySyn)
forall a. TCLinter ([DeclGroup], a)
declsLinter
                      , tcPrims :: PrimMap
tcPrims = PrimMap
prims }
  ([DeclGroup]
ds',Map Name TySyn
tyMap) <- TCAction [TopDecl Name] ([DeclGroup], Map Name TySyn)
-> [TopDecl Name]
-> ModContextParams
-> IfaceDecls
-> ModuleM ([DeclGroup], Map Name TySyn)
forall i o.
(Show i, Show o, HasLoc i) =>
TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck TCAction [TopDecl Name] ([DeclGroup], Map Name TySyn)
act [TopDecl Name]
rds ModContextParams
params IfaceDecls
decls
  (NamingEnv, [DeclGroup], Map Name TySyn)
-> ModuleM (NamingEnv, [DeclGroup], Map Name TySyn)
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamingEnv
declsEnv,[DeclGroup]
ds',Map Name TySyn
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 :: ModuleM PrimMap
getPrimMap  =
  do ModuleEnv
env <- ModuleT IO ModuleEnv
forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
     let mkPrims :: LoadedModule -> PrimMap
mkPrims = Iface -> PrimMap
ifacePrimMap (Iface -> PrimMap)
-> (LoadedModule -> Iface) -> LoadedModule -> PrimMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoadedModule -> Iface
lmInterface
         PrimMap
mp alsoPrimFrom :: PrimMap -> ModName -> PrimMap
`alsoPrimFrom` ModName
m =
           case ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule ModName
m ModuleEnv
env of
             Maybe LoadedModule
Nothing -> PrimMap
mp
             Just LoadedModule
lm -> LoadedModule -> PrimMap
mkPrims LoadedModule
lm PrimMap -> PrimMap -> PrimMap
forall a. Semigroup a => a -> a -> a
<> PrimMap
mp

     case ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule ModName
preludeName ModuleEnv
env of
       Just LoadedModule
prel -> PrimMap -> ModuleM PrimMap
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PrimMap -> ModuleM PrimMap) -> PrimMap -> ModuleM PrimMap
forall a b. (a -> b) -> a -> b
$ LoadedModule -> PrimMap
mkPrims LoadedModule
prel
                            PrimMap -> ModName -> PrimMap
`alsoPrimFrom` ModName
floatName
       Maybe LoadedModule
Nothing -> [Char] -> [[Char]] -> ModuleM PrimMap
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.ModuleSystem.Base.getPrimMap"
                  [ [Char]
"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)
checkModule :: ImportSource -> Module PName -> ModuleM (NamingEnv, TCTopEntity)
checkModule ImportSource
isrc 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 -> Bool
modNamesMatch ModName
nm (Located ModName -> ModName
forall a. Located a -> a
thing (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
m)))
         (ModName -> Located ModName -> ModuleM ()
forall a. ModName -> Located ModName -> ModuleM a
moduleNameMismatch ModName
nm (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
mName Module PName
m))

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

  -- run expandPropGuards
  Module PName
epgm <- Module PName -> ModuleM (Module PName)
expandPropGuards Module PName
npm

  -- rename everything
  RenamedModule
renMod <- Module PName -> ModuleM RenamedModule
renameModule Module PName
epgm


  {- dump renamed
  unless (thing (mName (R.rmModule renMod)) == preludeName)
       do (io $ print (T.pp renMod))
          -- io $ exitSuccess
  --}


  -- 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 mname name. ModuleG mname name -> Located mname
mName Module PName
m) ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName
              then PrimMap -> ModuleM PrimMap
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamingEnv -> PrimMap
R.toPrimMap (RenamedModule -> NamingEnv
R.rmDefines RenamedModule
renMod))
              else ModuleM PrimMap
getPrimMap

  -- typecheck
  let act :: TCAction (Module Name) TCTopEntity
act = TCAction { tcAction :: Act (Module Name) TCTopEntity
tcAction = Act (Module Name) TCTopEntity
T.tcModule
                     , tcLinter :: TCLinter TCTopEntity
tcLinter = ModName -> TCLinter TCTopEntity
tcTopEntitytLinter (Located ModName -> ModName
forall a. Located a -> a
P.thing (Module PName -> Located ModName
forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
m))
                     , tcPrims :: PrimMap
tcPrims  = PrimMap
prims }


  TCTopEntity
tcm <- TCAction (Module Name) TCTopEntity
-> Module Name
-> ModContextParams
-> IfaceDecls
-> ModuleM TCTopEntity
forall i o.
(Show i, Show o, HasLoc i) =>
TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck TCAction (Module Name) TCTopEntity
act (RenamedModule -> Module Name
R.rmModule RenamedModule
renMod) ModContextParams
NoParams (RenamedModule -> IfaceDecls
R.rmImported RenamedModule
renMod)

  TCTopEntity
rewMod <- case TCTopEntity
tcm of
              T.TCTopModule ModuleG ModName
mo -> ModuleG ModName -> TCTopEntity
T.TCTopModule (ModuleG ModName -> TCTopEntity)
-> ModuleT IO (ModuleG ModName) -> ModuleM TCTopEntity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Supply -> (ModuleG ModName, Supply))
-> ModuleT IO (ModuleG ModName)
forall a. (Supply -> (a, Supply)) -> ModuleT IO a
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Supply -> ModuleG ModName -> (ModuleG ModName, Supply)
`rewModule` ModuleG ModName
mo)
              T.TCTopSignature {} -> TCTopEntity -> ModuleM TCTopEntity
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCTopEntity
tcm
  let nameEnv :: NamingEnv
nameEnv = case TCTopEntity
tcm of
                  T.TCTopModule ModuleG ModName
mo -> ModuleG ModName -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
T.mInScope ModuleG ModName
mo
                  -- Name env for signatures does not change after typechecking
                  T.TCTopSignature {} -> Module Name -> NamingEnv
forall mname name. ModuleG mname name -> NamingEnv
mInScope (RenamedModule -> Module Name
R.rmModule RenamedModule
renMod)
  (NamingEnv, TCTopEntity) -> ModuleM (NamingEnv, TCTopEntity)
forall a. a -> ModuleT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NamingEnv
nameEnv,TCTopEntity
rewMod)

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


exprLinter :: TCLinter (T.Expr, T.Schema)
exprLinter :: TCLinter (Expr, Schema)
exprLinter = TCLinter
  { lintCheck :: (Expr, Schema) -> InferInput -> Either (Range, Error) [Schema]
lintCheck = \(Expr
e',Schema
s) InferInput
i ->
      case InferInput -> Expr -> Either (Range, Error) (Schema, [Schema])
TcSanity.tcExpr InferInput
i Expr
e' of
        Left (Range, Error)
err     -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
        Right (Schema
s1,[Schema]
os)
          | TcSanity.SameIf [Prop]
os' <- Schema -> Schema -> AreSame
forall a. Same a => a -> a -> AreSame
TcSanity.same Schema
s Schema
s1 ->
                                        [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right ((Prop -> Schema) -> [Prop] -> [Schema]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Schema
T.tMono [Prop]
os' [Schema] -> [Schema] -> [Schema]
forall a. [a] -> [a] -> [a]
++ [Schema]
os)
          | Bool
otherwise -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left ( Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (Expr -> Maybe Range
forall t. HasLoc t => t -> Maybe Range
getLoc Expr
e')
                              , [Char] -> Schema -> Schema -> Error
TcSanity.TypeMismatch [Char]
"exprLinter" Schema
s Schema
s1
                              )
  , lintModule :: Maybe ModName
lintModule = Maybe ModName
forall a. Maybe a
Nothing
  }

declsLinter :: TCLinter ([ T.DeclGroup ], a)
declsLinter :: forall a. TCLinter ([DeclGroup], a)
declsLinter = TCLinter
  { lintCheck :: ([DeclGroup], a) -> InferInput -> Either (Range, Error) [Schema]
lintCheck = \([DeclGroup]
ds',a
_) InferInput
i -> case InferInput -> [DeclGroup] -> Either (Range, Error) [Schema]
TcSanity.tcDecls InferInput
i [DeclGroup]
ds' of
                                Left (Range, Error)
err -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
                                Right [Schema]
os -> [Schema] -> Either (Range, 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 (ModuleG ModName)
moduleLinter ModName
m = TCLinter
  { lintCheck :: ModuleG ModName -> InferInput -> Either (Range, Error) [Schema]
lintCheck   = \ModuleG ModName
m' InferInput
i -> case InferInput -> ModuleG ModName -> Either (Range, Error) [Schema]
TcSanity.tcModule InferInput
i ModuleG ModName
m' of
                            Left (Range, Error)
err -> (Range, Error) -> Either (Range, Error) [Schema]
forall a b. a -> Either a b
Left (Range, Error)
err
                            Right [Schema]
os -> [Schema] -> Either (Range, 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
  }

tcTopEntitytLinter :: P.ModName -> TCLinter T.TCTopEntity
tcTopEntitytLinter :: ModName -> TCLinter TCTopEntity
tcTopEntitytLinter ModName
m = TCLinter
  { lintCheck :: TCTopEntity -> InferInput -> Either (Range, Error) [Schema]
lintCheck   = \TCTopEntity
m' InferInput
i -> case TCTopEntity
m' of
                             T.TCTopModule ModuleG ModName
mo ->
                               TCLinter (ModuleG ModName)
-> ModuleG ModName -> InferInput -> Either (Range, Error) [Schema]
forall o.
TCLinter o -> o -> InferInput -> Either (Range, Error) [Schema]
lintCheck (ModName -> TCLinter (ModuleG ModName)
moduleLinter ModName
m) ModuleG ModName
mo InferInput
i
                             T.TCTopSignature {} -> [Schema] -> Either (Range, Error) [Schema]
forall a b. b -> Either a b
Right []
                                -- XXX: what can we lint about module interfaces
  , 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
  { forall i o. TCAction i o -> Act i o
tcAction :: Act i o
  , forall i o. TCAction i o -> TCLinter o
tcLinter :: TCLinter o
  , forall i o. TCAction i o -> PrimMap
tcPrims  :: PrimMap
  }

typecheck ::
  (Show i, Show o, HasLoc i) =>
  TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck :: forall i o.
(Show i, Show o, HasLoc i) =>
TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
typecheck TCAction i o
act i
i ModContextParams
params 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 -> ModContextParams -> IfaceDecls -> ModuleM InferInput
genInferInput Range
range (TCAction i o -> PrimMap
forall i o. TCAction i o -> PrimMap
tcPrims TCAction i o
act) ModContextParams
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 NameMap
nameMap [(Range, Warning)]
warns NameSeeds
seeds Supply
supply' o
o ->
      do NameSeeds -> ModuleM ()
setNameSeeds NameSeeds
seeds
         Supply -> ModuleM ()
setSupply Supply
supply'
         NameMap -> [(Range, Warning)] -> ModuleM ()
typeCheckWarnings NameMap
nameMap [(Range, Warning)]
warns
         ModuleEnv
menv <- ModuleT IO ModuleEnv
forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
         case ModuleEnv -> CoreLint
meCoreLint ModuleEnv
menv of
           CoreLint
NoCoreLint -> () -> ModuleM ()
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
           CoreLint
CoreLint   -> case TCLinter o -> o -> InferInput -> Either (Range, Error) [Schema]
forall o.
TCLinter o -> o -> InferInput -> Either (Range, 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 [Schema]
as ->
                             let ppIt :: Logger -> t a -> IO ()
ppIt 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] -> [Schema]
TcSanity.onlyNonTrivial [Schema]
as)
                           Left (Range
loc,Error
err) ->
                            [Char] -> [[Char]] -> ModuleM ()
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Core lint failed:"
                              [ [Char]
"Location: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Range -> Doc
forall a. PP a => a -> Doc
T.pp Range
loc)
                              , Doc -> [Char]
forall a. Show a => a -> [Char]
show (Error -> Doc
forall a. PP a => a -> Doc
T.pp Error
err)
                              ]
         o -> ModuleM o
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return o
o

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

-- | Generate input for the typechecker.
genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls ->
                                                          ModuleM T.InferInput
genInferInput :: Range
-> PrimMap -> ModContextParams -> IfaceDecls -> ModuleM InferInput
genInferInput Range
r PrimMap
prims ModContextParams
params IfaceDecls
env = do
  NameSeeds
seeds <- ModuleM NameSeeds
getNameSeeds
  Bool
monoBinds <- ModuleM Bool
getMonoBinds
  Solver
solver <- ModuleT IO Solver
forall (m :: * -> *). Monad m => ModuleT m Solver
getTCSolver
  Supply
supply <- ModuleM Supply
getSupply
  [[Char]]
searchPath <- ModuleM [[Char]]
getSearchPath
  Bool
callStacks <- ModuleM Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks

  ModName -> Maybe (ModuleG (), IfaceG ())
topMods <- ModuleM (ModName -> Maybe (ModuleG (), IfaceG ()))
getAllLoaded
  ModName -> Maybe ModParamNames
topSigs <- ModuleM (ModName -> Maybe ModParamNames)
getAllLoadedSignatures

  InferInput -> ModuleM InferInput
forall a. a -> ModuleT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return 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
    , inpNominalTypes :: Map Name NominalType
T.inpNominalTypes     = IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
env
    , inpSignatures :: Map Name ModParamNames
T.inpSignatures       = IfaceDecls -> Map Name ModParamNames
ifSignatures IfaceDecls
env
    , inpNameSeeds :: NameSeeds
T.inpNameSeeds        = NameSeeds
seeds
    , inpMonoBinds :: Bool
T.inpMonoBinds        = Bool
monoBinds
    , inpCallStacks :: Bool
T.inpCallStacks       = Bool
callStacks
    , inpSearchPath :: [[Char]]
T.inpSearchPath       = [[Char]]
searchPath
    , inpSupply :: Supply
T.inpSupply           = Supply
supply
    , inpParams :: ModParamNames
T.inpParams           = case ModContextParams
params of
                                ModContextParams
NoParams -> FunctorParams -> ModParamNames
T.allParamNames FunctorParams
forall a. Monoid a => a
mempty
                                FunctorParams FunctorParams
ps -> FunctorParams -> ModParamNames
T.allParamNames FunctorParams
ps
                                InterfaceParams ModParamNames
ps -> ModParamNames
ps
    , inpPrimNames :: PrimMap
T.inpPrimNames        = PrimMap
prims
    , inpSolver :: Solver
T.inpSolver           = Solver
solver
    , inpTopModules :: ModName -> Maybe (ModuleG (), IfaceG ())
T.inpTopModules       = ModName -> Maybe (ModuleG (), IfaceG ())
topMods
    , inpTopSignatures :: ModName -> Maybe ModParamNames
T.inpTopSignatures    = ModName -> Maybe ModParamNames
topSigs
    }


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

evalExpr :: T.Expr -> ModuleM Concrete.Value
evalExpr :: Expr -> ModuleM Value
evalExpr Expr
e = do
  EvalEnv
env <- ModuleM EvalEnv
getEvalEnv
  DynamicEnv
denv <- ModuleM DynamicEnv
getDynEnv
  IO EvalOpts
evopts <- ModuleT IO (IO EvalOpts)
getEvalOptsAction
  let tbl :: Map PrimIdent (Prim Concrete)
tbl = IO EvalOpts -> Map PrimIdent (Prim Concrete)
Concrete.primTable IO EvalOpts
evopts
  let ?evalPrim = \PrimIdent
i -> Prim Concrete -> Either Expr (Prim Concrete)
forall a b. b -> Either a b
Right (Prim Concrete -> Either Expr (Prim Concrete))
-> Maybe (Prim Concrete) -> Maybe (Either Expr (Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent -> Map PrimIdent (Prim Concrete) -> Maybe (Prim Concrete)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
  let ?range = ?range::Range
Range
emptyRange
  Bool
callStacks <- ModuleM Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
  let ?callStacks = ?callStacks::Bool
Bool
callStacks

  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
$ CallStack -> Eval Value -> IO Value
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty (Concrete -> EvalEnv -> Expr -> SEval Concrete Value
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
E.evalExpr Concrete
Concrete (EvalEnv
env EvalEnv -> EvalEnv -> EvalEnv
forall a. Semigroup a => a -> a -> a
<> DynamicEnv -> EvalEnv
deEnv DynamicEnv
denv) Expr
e)

benchmarkExpr :: Double -> T.Expr -> ModuleM BenchmarkStats
benchmarkExpr :: Double -> Expr -> ModuleM BenchmarkStats
benchmarkExpr Double
period Expr
e = do
  EvalEnv
env <- ModuleM EvalEnv
getEvalEnv
  DynamicEnv
denv <- ModuleM DynamicEnv
getDynEnv
  IO EvalOpts
evopts <- ModuleT IO (IO EvalOpts)
getEvalOptsAction
  let env' :: EvalEnv
env' = EvalEnv
env EvalEnv -> EvalEnv -> EvalEnv
forall a. Semigroup a => a -> a -> a
<> DynamicEnv -> EvalEnv
deEnv DynamicEnv
denv
  let tbl :: Map PrimIdent (Prim Concrete)
tbl = IO EvalOpts -> Map PrimIdent (Prim Concrete)
Concrete.primTable IO EvalOpts
evopts
  let ?evalPrim = \PrimIdent
i -> Prim Concrete -> Either Expr (Prim Concrete)
forall a b. b -> Either a b
Right (Prim Concrete -> Either Expr (Prim Concrete))
-> Maybe (Prim Concrete) -> Maybe (Either Expr (Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent -> Map PrimIdent (Prim Concrete) -> Maybe (Prim Concrete)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
  let ?range = ?range::Range
Range
emptyRange
  Bool
callStacks <- ModuleM Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
  let ?callStacks = ?callStacks::Bool
Bool
callStacks

  let eval :: Expr -> IO ()
eval Expr
expr = CallStack -> Eval () -> IO ()
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty (Eval () -> IO ()) -> Eval () -> IO ()
forall a b. (a -> b) -> a -> b
$
        Concrete -> EvalEnv -> Expr -> SEval Concrete Value
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
E.evalExpr Concrete
Concrete EvalEnv
env' Expr
expr Eval Value -> (Value -> Eval ()) -> Eval ()
forall a b. Eval a -> (a -> Eval b) -> Eval b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Value -> Eval ()
Value -> SEval Concrete ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
E.forceValue
  IO BenchmarkStats -> ModuleM BenchmarkStats
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (IO BenchmarkStats -> ModuleM BenchmarkStats)
-> IO BenchmarkStats -> ModuleM BenchmarkStats
forall a b. (a -> b) -> a -> b
$ Double -> (Expr -> IO ()) -> Expr -> IO BenchmarkStats
forall a b. Double -> (a -> IO b) -> a -> IO BenchmarkStats
benchmark Double
period (?range::Range,
 ?evalPrim::PrimIdent -> Maybe (Either Expr (Prim Concrete)),
 ?callStacks::Bool) =>
Expr -> IO ()
Expr -> IO ()
eval Expr
e

evalDecls :: [T.DeclGroup] -> ModuleM ()
evalDecls :: [DeclGroup] -> ModuleM ()
evalDecls [DeclGroup]
dgs = do
  EvalEnv
env <- ModuleM EvalEnv
getEvalEnv
  DynamicEnv
denv <- ModuleM DynamicEnv
getDynEnv
  IO EvalOpts
evOpts <- ModuleT IO (IO EvalOpts)
getEvalOptsAction
  let env' :: EvalEnv
env' = EvalEnv
env EvalEnv -> EvalEnv -> EvalEnv
forall a. Semigroup a => a -> a -> a
<> DynamicEnv -> EvalEnv
deEnv DynamicEnv
denv
  let tbl :: Map PrimIdent (Prim Concrete)
tbl = IO EvalOpts -> Map PrimIdent (Prim Concrete)
Concrete.primTable IO EvalOpts
evOpts
  let ?evalPrim = \PrimIdent
i -> Prim Concrete -> Either Expr (Prim Concrete)
forall a b. b -> Either a b
Right (Prim Concrete -> Either Expr (Prim Concrete))
-> Maybe (Prim Concrete) -> Maybe (Either Expr (Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimIdent -> Map PrimIdent (Prim Concrete) -> Maybe (Prim Concrete)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
  Bool
callStacks <- ModuleM Bool
forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
  let ?callStacks = ?callStacks::Bool
Bool
callStacks

  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
$ CallStack -> Eval EvalEnv -> IO EvalEnv
forall a. CallStack -> Eval a -> IO a
E.runEval CallStack
forall a. Monoid a => a
mempty (Concrete -> [DeclGroup] -> EvalEnv -> SEval Concrete EvalEnv
forall sym.
EvalPrims sym =>
sym -> [DeclGroup] -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
E.evalDecls Concrete
Concrete [DeclGroup]
dgs EvalEnv
env')
  let denv' :: DynamicEnv
denv' = DynamicEnv
denv { deDecls = deDecls denv ++ dgs
                   , deEnv = deEnv'
                   }
  DynamicEnv -> ModuleM ()
setDynEnv DynamicEnv
denv'