-- |
-- 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 RecordWildCards #-}

module Cryptol.ModuleSystem.Base where

import Cryptol.ModuleSystem.Env (DynamicEnv(..))
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
import Cryptol.ModuleSystem.Env (lookupModule
                                , LoadedModule(..)
                                , meCoreLint, CoreLint(..)
                                , ModContext(..)
                                , ModulePath(..), modulePathLabel)
import qualified Cryptol.Eval                 as E

import qualified Cryptol.Eval.Concrete as Concrete
import           Cryptol.Eval.Concrete (Concrete(..))
import qualified Cryptol.ModuleSystem.NamingEnv as R
import qualified Cryptol.ModuleSystem.Renamer as R
import qualified Cryptol.Parser               as P
import qualified Cryptol.Parser.Unlit         as P
import Cryptol.Parser.AST as P
import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))
import Cryptol.Parser.NoInclude (removeIncludesModule)
import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
import qualified Cryptol.TypeCheck     as T
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Transform.AddModParams (addModParams)
import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                           , preludeReferenceName, interactiveName, modNameChunks
                           , notParamInstModName, isParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)

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

import qualified Control.Exception as X
import Control.Monad (unless,when)
import Data.Maybe (fromMaybe)
import Data.Monoid ((<>))
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 Prelude ()
import Prelude.Compat hiding ( (<>) )


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

rename :: ModName -> R.NamingEnv -> R.RenameM a -> ModuleM a
rename :: ModName -> NamingEnv -> RenameM a -> ModuleM a
rename ModName
modName NamingEnv
env RenameM a
m = do
  (Either [RenamerError] a
res,[RenamerWarning]
ws) <- (Supply -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
-> ModuleT IO (Either [RenamerError] a, [RenamerWarning])
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply ((Supply -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
 -> ModuleT IO (Either [RenamerError] a, [RenamerWarning]))
-> (Supply
    -> ((Either [RenamerError] a, [RenamerWarning]), Supply))
-> ModuleT IO (Either [RenamerError] a, [RenamerWarning])
forall a b. (a -> b) -> a -> b
$ \ Supply
supply ->
    case Supply
-> ModName
-> NamingEnv
-> RenameM a
-> (Either [RenamerError] (a, Supply), [RenamerWarning])
forall a.
Supply
-> ModName
-> NamingEnv
-> RenameM a
-> (Either [RenamerError] (a, Supply), [RenamerWarning])
R.runRenamer Supply
supply ModName
modName NamingEnv
env RenameM a
m of
      (Right (a
a,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 (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 (IfaceDecls,R.NamingEnv,P.Module Name)
renameModule :: Module PName -> ModuleM (IfaceDecls, NamingEnv, Module Name)
renameModule Module PName
m = do
  (IfaceDecls
decls,NamingEnv
menv) <- [Import] -> ModuleM (IfaceDecls, NamingEnv)
importIfaces ((Located Import -> Import) -> [Located Import] -> [Import]
forall a b. (a -> b) -> [a] -> [b]
map Located Import -> Import
forall a. Located a -> a
thing (Module PName -> [Located Import]
forall name. Module name -> [Located Import]
P.mImports Module PName
m))
  (NamingEnv
declsEnv,Module Name
rm) <- ModName
-> NamingEnv
-> RenameM (NamingEnv, Module Name)
-> ModuleM (NamingEnv, Module Name)
forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename (Located ModName -> ModName
forall a. Located a -> a
thing (Module PName -> Located ModName
forall name. Module name -> Located ModName
mName Module PName
m)) NamingEnv
menv (Module PName -> RenameM (NamingEnv, Module Name)
R.renameModule Module PName
m)
  (IfaceDecls, NamingEnv, Module Name)
-> ModuleM (IfaceDecls, NamingEnv, Module Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls
decls,NamingEnv
declsEnv,Module Name
rm)


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

-- | Run the noPat pass.
noPat :: RemovePatterns a => a -> ModuleM a
noPat :: a -> ModuleM a
noPat a
a = 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 (t :: * -> *) a. Foldable t => t a -> Bool
null [Error]
errs) ([Error] -> ModuleM ()
forall a. [Error] -> ModuleM a
noPatErrors [Error]
errs)
  a -> ModuleM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a'


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

parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
parseModule :: ModulePath -> ModuleM (Fingerprint, Module PName)
parseModule ModulePath
path = do
  FilePath -> IO ByteString
getBytes <- ModuleT IO (FilePath -> IO ByteString)
forall (m :: * -> *).
Monad m =>
ModuleT m (FilePath -> m ByteString)
getByteReader

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

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

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

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

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


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

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

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

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


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

-- | Load dependencies, typecheck, and add to the eval environment.
doLoadModule ::
  Bool {- ^ quiet mode: true suppresses the "loading module" message -} ->
  ImportSource ->
  ModulePath ->
  Fingerprint ->
  P.Module PName ->
  ModuleM T.Module
doLoadModule :: Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Module PName
-> ModuleM Module
doLoadModule Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Module PName
pm0 =
  ImportSource -> ModuleM Module -> ModuleM Module
forall a. ImportSource -> ModuleM a -> ModuleM a
loading ImportSource
isrc (ModuleM Module -> ModuleM Module)
-> ModuleM Module -> ModuleM Module
forall a b. (a -> b) -> a -> b
$
  do let pm :: Module PName
pm = Module PName -> Module PName
addPrelude Module PName
pm0
     Module PName -> ModuleM ()
forall name. Module name -> ModuleM ()
loadDeps Module PName
pm

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

     -- extend the eval env, unless a functor.
     Map PrimIdent Value
tbl <- EvalOpts -> Map PrimIdent Value
Concrete.primTable (EvalOpts -> Map PrimIdent Value)
-> ModuleT IO EvalOpts -> ModuleT IO (Map PrimIdent Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleT IO EvalOpts
getEvalOpts
     let ?evalPrim = \i -> Right <$> Map.lookup i tbl
     Bool -> ModuleM () -> ModuleM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Module -> Bool
T.isParametrizedModule Module
tcm) (ModuleM () -> ModuleM ()) -> ModuleM () -> ModuleM ()
forall a b. (a -> b) -> a -> b
$ (EvalEnv -> Eval EvalEnv) -> ModuleM ()
modifyEvalEnv (Concrete -> Module -> EvalEnv -> SEval Concrete EvalEnv
forall sym.
EvalPrims sym =>
sym -> Module -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
E.moduleEnv Concrete
Concrete Module
tcm)
     ModulePath -> Fingerprint -> Module -> ModuleM ()
loadedModule ModulePath
path Fingerprint
fp Module
tcm

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





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

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

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

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


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

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

    [] -> ModuleM ModulePath
handleNotFound

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

  -- generate all possible search paths
  possibleFiles :: [FilePath] -> [FilePath]
possibleFiles [FilePath]
paths = do
    FilePath
path <- [FilePath]
paths
    FilePath
ext  <- [FilePath]
P.knownExts
    FilePath -> [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath
path FilePath -> FilePath -> FilePath
</> ModName -> FilePath -> FilePath
moduleFile ModName
n FilePath
ext)

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

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

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



-- 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 :: IfaceParams
params = ModContext -> IfaceParams
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 :: forall i o. Act i o -> TCLinter o -> PrimMap -> TCAction i o
TCAction { tcAction :: Act (Expr Name) (Expr, Schema)
tcAction = Act (Expr Name) (Expr, Schema)
T.tcExpr, tcLinter :: TCLinter (Expr, Schema)
tcLinter = TCLinter (Expr, Schema)
exprLinter
                      , tcPrims :: PrimMap
tcPrims = PrimMap
prims }
  (Expr
te,Schema
s) <- TCAction (Expr Name) (Expr, Schema)
-> Expr Name -> IfaceParams -> IfaceDecls -> ModuleM (Expr, Schema)
forall i o.
(Show i, Show o, HasLoc i) =>
TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o
typecheck TCAction (Expr Name) (Expr, Schema)
act Expr Name
re IfaceParams
params IfaceDecls
decls

  (Expr Name, Expr, Schema) -> ModuleM (Expr Name, Expr, Schema)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name
re,Expr
te,Schema
s)

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

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

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

-- | Generate the primitive map. If the prelude is currently being loaded, this
-- should be generated directly from the naming environment given to the renamer
-- instead.
getPrimMap :: ModuleM PrimMap
getPrimMap :: ModuleM PrimMap
getPrimMap  =
  do ModuleEnv
env <- ModuleT IO ModuleEnv
forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
     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 (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 -> FilePath -> [FilePath] -> ModuleM PrimMap
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"Cryptol.ModuleSystem.Base.getPrimMap"
                  [ FilePath
"Unable to find the prelude" ]

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


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

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

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

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

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

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

  -- when generating the prim map for the typechecker, if we're checking the
  -- prelude, we have to generate the map from the renaming environment, as we
  -- don't have the interface yet.
  PrimMap
prims <- if Located ModName -> ModName
forall a. Located a -> a
thing (Module PName -> Located ModName
forall name. Module name -> Located ModName
mName Module PName
m) ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName
              then PrimMap -> ModuleM PrimMap
forall (m :: * -> *) a. Monad m => a -> m a
return (NamingEnv -> PrimMap
R.toPrimMap NamingEnv
declsEnv)
              else ModuleM PrimMap
getPrimMap

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


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

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

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

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


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

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

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

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

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

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

typecheck ::
  (Show i, Show o, HasLoc i) => TCAction i o -> i ->
                                  IfaceParams -> IfaceDecls -> ModuleM o
typecheck :: TCAction i o -> i -> IfaceParams -> IfaceDecls -> ModuleM o
typecheck TCAction i o
act i
i IfaceParams
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 -> IfaceParams -> IfaceDecls -> ModuleM InferInput
genInferInput Range
range (TCAction i o -> PrimMap
forall i o. TCAction i o -> PrimMap
tcPrims TCAction i o
act) IfaceParams
params IfaceDecls
env
  InferOutput o
out   <- IO (InferOutput o) -> ModuleT IO (InferOutput o)
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (TCAction i o -> Act i o
forall i o. TCAction i o -> Act i o
tcAction TCAction i o
act i
i InferInput
input)

  case InferOutput o
out of

    T.InferOK 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 (m :: * -> *) a. Monad m => a -> m a
return ()
           CoreLint
CoreLint   -> case TCLinter o -> o -> InferInput -> Either Error [Schema]
forall o. TCLinter o -> o -> InferInput -> Either Error [Schema]
lintCheck (TCAction i o -> TCLinter o
forall i o. TCAction i o -> TCLinter o
tcLinter TCAction i o
act) o
o InferInput
input of
                           Right [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]
as
                           Left Error
err -> FilePath -> [FilePath] -> ModuleM ()
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"Core lint failed:" [Error -> FilePath
forall a. Show a => a -> FilePath
show Error
err]
         o -> ModuleM o
forall (m :: * -> *) a. Monad m => a -> m a
return o
o

    T.InferFailed 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 ->
                          IfaceParams -> IfaceDecls -> ModuleM T.InferInput
genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM InferInput
genInferInput Range
r PrimMap
prims IfaceParams
params IfaceDecls
env = do
  NameSeeds
seeds <- ModuleM NameSeeds
getNameSeeds
  Bool
monoBinds <- ModuleT IO Bool
getMonoBinds
  SolverConfig
cfg <- ModuleM SolverConfig
getSolverConfig
  Supply
supply <- ModuleM Supply
getSupply
  [FilePath]
searchPath <- ModuleM [FilePath]
getSearchPath

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



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

evalExpr :: T.Expr -> ModuleM Concrete.Value
evalExpr :: Expr -> ModuleM Value
evalExpr Expr
e = do
  EvalEnv
env <- ModuleM EvalEnv
getEvalEnv
  DynamicEnv
denv <- ModuleM DynamicEnv
getDynEnv
  EvalOpts
evopts <- ModuleT IO EvalOpts
getEvalOpts
  let tbl :: Map PrimIdent Value
tbl = EvalOpts -> Map PrimIdent Value
Concrete.primTable EvalOpts
evopts
  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
  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
$ Eval Value -> IO Value
forall a. Eval a -> IO a
E.runEval (Eval Value -> IO Value) -> Eval Value -> IO Value
forall a b. (a -> b) -> a -> b
$ (Concrete -> EvalEnv -> Expr -> SEval Concrete Value
forall sym.
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)

evalDecls :: [T.DeclGroup] -> ModuleM ()
evalDecls :: [DeclGroup] -> ModuleM ()
evalDecls [DeclGroup]
dgs = do
  EvalEnv
env <- ModuleM EvalEnv
getEvalEnv
  DynamicEnv
denv <- ModuleM DynamicEnv
getDynEnv
  EvalOpts
evOpts <- ModuleT IO EvalOpts
getEvalOpts
  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 Value
tbl = EvalOpts -> Map PrimIdent Value
Concrete.primTable EvalOpts
evOpts
  let ?evalPrim = \i -> Right <$> Map.lookup i tbl
  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
$ Eval EvalEnv -> IO EvalEnv
forall a. Eval a -> IO a
E.runEval (Eval EvalEnv -> IO EvalEnv) -> Eval EvalEnv -> IO EvalEnv
forall a b. (a -> b) -> a -> b
$ 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 :: [DeclGroup]
deDecls = DynamicEnv -> [DeclGroup]
deDecls DynamicEnv
denv [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++ [DeclGroup]
dgs
                   , deEnv :: EvalEnv
deEnv = EvalEnv
deEnv'
                   }
  DynamicEnv -> ModuleM ()
setDynEnv DynamicEnv
denv'