{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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,groupBy)
import Data.Function(on)
import Data.Monoid ((<>),Endo(..), Any(..))
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 ( (<>) )
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)
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
, modNameToNormalModName )
import Cryptol.Utils.PP (pretty)
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)
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) <- forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply 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 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) -> ((forall a b. b -> Either a b
Right a
a,[RenamerWarning]
ws),Supply
supply')
(Left [RenamerError]
errs,[RenamerWarning]
ws) -> ((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 -> forall (m :: * -> *) a. Monad m => a -> m a
return a
r
Left [RenamerError]
errs -> forall a. [RenamerError] -> ModuleM a
renamerErrors [RenamerError]
errs
renameModule :: P.Module PName -> ModuleM R.RenamedModule
renameModule :: Module PName -> ModuleM RenamedModule
renameModule Module PName
m = forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
mName Module PName
m)) forall a. Monoid a => a
mempty (Module PName -> RenameM RenamedModule
R.renameModule Module PName
m)
noPat :: RemovePatterns a => a -> ModuleM a
noPat :: forall a. RemovePatterns a => a -> ModuleM a
noPat a
a = do
let (a
a',[Error]
errs) = forall t. RemovePatterns t => t -> (t, [Error])
removePatterns a
a
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Error]
errs) (forall a. [Error] -> ModuleM a
noPatErrors [Error]
errs)
forall (m :: * -> *) a. Monad m => a -> m a
return a
a'
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards Module PName
a =
case forall a. ExpandPropGuardsM a -> ExpandPropGuardsM a
ExpandPropGuards.runExpandPropGuardsM forall a b. (a -> b) -> a -> b
$ forall mname.
ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
ExpandPropGuards.expandPropGuards Module PName
a of
Left Error
err -> forall a. Error -> ModuleM a
expandPropGuardsError Error
err
Right Module PName
a' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Module PName
a'
parseModule ::
ModulePath -> ModuleM (Fingerprint, Set FilePath, [P.Module PName])
parseModule :: ModulePath -> ModuleM (Fingerprint, Set [Char], [Module PName])
parseModule ModulePath
path = do
[Char] -> IO ByteString
getBytes <- forall (m :: * -> *). Monad m => ModuleT m ([Char] -> m ByteString)
getByteReader
Either IOError ByteString
bytesRes <- case ModulePath
path of
InFile [Char]
p -> forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (forall e a. Exception e => IO a -> IO (Either e a)
X.try ([Char] -> IO ByteString
getBytes [Char]
p))
InMem [Char]
_ ByteString
bs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right ByteString
bs)
ByteString
bytes <- case Either IOError ByteString
bytesRes of
Right ByteString
bytes -> 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 -> forall a. [Char] -> ModuleM a
cantFindFile [Char]
p
| Bool
otherwise -> forall a. [Char] -> IOError -> ModuleM a
otherIOError [Char]
p IOError
exn
InMem [Char]
p ByteString
_ -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"parseModule"
[ [Char]
"IOError for in-memory contetns???"
, [Char]
"Label: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
p
, [Char]
"Exception: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show IOError
exn ]
Text
txt <- case ByteString -> Either UnicodeException Text
decodeUtf8' ByteString
bytes of
Right Text
txt -> forall (m :: * -> *) a. Monad m => a -> m a
return Text
txt
Left UnicodeException
e -> forall a. ModulePath -> UnicodeException -> ModuleM a
badUtf8 ModulePath
path UnicodeException
e
let cfg :: Config
cfg = Config
P.defaultConfig
{ cfgSource :: [Char]
P.cfgSource = case ModulePath
path of
InFile [Char]
p -> [Char]
p
InMem [Char]
l ByteString
_ -> [Char]
l
, cfgPreProc :: PreProc
P.cfgPreProc = [Char] -> PreProc
P.guessPreProc (ModulePath -> [Char]
modulePathLabel ModulePath
path)
}
case Config -> Text -> Either ParseError [Module PName]
P.parseModule Config
cfg Text
txt of
Right [Module PName]
pms ->
do let fp :: Fingerprint
fp = ByteString -> Fingerprint
fingerprint ByteString
bytes
([Module PName]
pm1,Set [Char]
deps) <-
case ModulePath
path of
InFile [Char]
p ->
do [Char] -> IO ByteString
r <- forall (m :: * -> *). Monad m => ModuleT m ([Char] -> m ByteString)
getByteReader
([Module PName]
mo,[Set [Char]]
d) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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, Set [Char])
mb <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (([Char] -> IO ByteString)
-> [Char]
-> Module PName
-> IO (Either [IncludeError] (Module PName, Set [Char]))
removeIncludesModule [Char] -> IO ByteString
r [Char]
p Module PName
pm)
case Either [IncludeError] (Module PName, Set [Char])
mb of
Right (Module PName, Set [Char])
ok -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module PName, Set [Char])
ok
Left [IncludeError]
err -> forall a. [IncludeError] -> ModuleM a
noIncludeErrors [IncludeError]
err
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Module PName]
mo, forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set [Char]]
d)
InMem {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Module PName]
pms, forall a. Set a
Set.empty)
Fingerprint
fp seq :: forall a b. a -> b -> b
`seq` forall (m :: * -> *) a. Monad m => a -> m a
return (Fingerprint
fp, Set [Char]
deps, [Module PName]
pm1)
Left ParseError
err -> forall a. ModulePath -> ParseError -> ModuleM a
moduleParseError ModulePath
path ParseError
err
loadModuleByPath ::
Bool ->
FilePath -> ModuleM T.TCTopEntity
loadModuleByPath :: Bool -> [Char] -> ModuleM TCTopEntity
loadModuleByPath Bool
eval [Char]
path = forall a. [[Char]] -> ModuleM a -> ModuleM a
withPrependedSearchPath [ [Char] -> [Char]
takeDirectory [Char]
path ] 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, Set [Char]
deps, [Module PName]
pms) <- ModulePath -> ModuleM (Fingerprint, Set [Char], [Module PName])
parseModule ([Char] -> ModulePath
InFile [Char]
foundPath)
forall a. [a] -> a
last forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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 = forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
pm)
ModuleEnv
env <- forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
[Char]
path' <- 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
Maybe (LoadedModuleG TCTopEntity)
Nothing ->
Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Set [Char]
-> Module PName
-> ModuleM TCTopEntity
doLoadModule Bool
eval Bool
False (ModName -> ImportSource
FromModule ModName
n) ([Char] -> ModulePath
InFile [Char]
foundPath) Fingerprint
fp Set [Char]
deps Module PName
pm
Just LoadedModuleG TCTopEntity
lm
| [Char]
path' forall a. Eq a => a -> a -> Bool
== [Char]
loaded -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LoadedModuleG a -> a
lmData LoadedModuleG TCTopEntity
lm)
| Bool
otherwise -> forall a. ModName -> [Char] -> [Char] -> ModuleM a
duplicateModuleName ModName
n [Char]
path' [Char]
loaded
where loaded :: [Char]
loaded = forall a. LoadedModuleG a -> [Char]
lmModuleId LoadedModuleG TCTopEntity
lm
loadModuleFrom ::
Bool -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LoadedModuleG a -> ModulePath
lmFilePath LoadedModuleG TCTopEntity
m, forall a. LoadedModuleG a -> a
lmData LoadedModuleG TCTopEntity
m)
Maybe (LoadedModuleG TCTopEntity)
Nothing ->
do ModulePath
path <- ModName -> ModuleM ModulePath
findModule ModName
n
forall a. ModulePath -> ModuleM a -> ModuleM a
errorInFile ModulePath
path forall a b. (a -> b) -> a -> b
$
do (Fingerprint
fp, Set [Char]
deps, [Module PName]
pms) <- ModulePath -> ModuleM (Fingerprint, Set [Char], [Module PName])
parseModule ModulePath
path
[TCTopEntity]
ms <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Set [Char]
-> Module PName
-> ModuleM TCTopEntity
doLoadModule Bool
True Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Set [Char]
deps) [Module PName]
pms
forall (m :: * -> *) a. Monad m => a -> m a
return (ModulePath
path,forall a. [a] -> a
last [TCTopEntity]
ms)
doLoadModule ::
Bool ->
Bool ->
ImportSource ->
ModulePath ->
Fingerprint ->
Set FilePath ->
P.Module PName ->
ModuleM T.TCTopEntity
doLoadModule :: Bool
-> Bool
-> ImportSource
-> ModulePath
-> Fingerprint
-> Set [Char]
-> Module PName
-> ModuleM TCTopEntity
doLoadModule Bool
eval Bool
quiet ImportSource
isrc ModulePath
path Fingerprint
fp Set [Char]
incDeps Module PName
pm0 =
forall a. ImportSource -> ModuleM a -> ModuleM a
loading ImportSource
isrc forall a b. (a -> b) -> a -> b
$
do let pm :: Module PName
pm = Module PName -> Module PName
addPrelude Module PName
pm0
Set ModName
impDeps <- forall mname name. ModuleG mname name -> ModuleM (Set ModName)
loadDeps Module PName
pm
let what :: [Char]
what = case forall mname name. ModuleG mname name -> ModuleDefinition name
P.mDef Module PName
pm of
P.InterfaceModule {} -> [Char]
"interface module"
ModuleDefinition PName
_ -> [Char]
"module"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet forall a b. (a -> b) -> a -> b
$ forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger Logger -> [Char] -> IO ()
logPutStrLn
([Char]
"Loading " forall a. [a] -> [a] -> [a]
++ [Char]
what forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty (forall a. Located a -> a
P.thing (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
Map PrimIdent (Prim Concrete)
tbl <- IO EvalOpts -> Map PrimIdent (Prim Concrete)
Concrete.primTable forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleM (IO EvalOpts)
getEvalOptsAction
let ?evalPrim = \PrimIdent
i -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
Bool
callStacks <- forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
let ?callStacks = 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 (forall mname. ModuleG mname -> Bool
T.isParametrizedModule ModuleG ModName
m) -> forall a. a -> Maybe a
Just ModuleG ModName
m
TCTopEntity
_ -> 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 (forall sym.
EvalPrims sym =>
sym
-> ModuleG ModName -> GenEvalEnv sym -> SEval sym (GenEvalEnv sym)
E.moduleEnv Concrete
Concrete ModuleG ModName
m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ForeignSrc
fsrc
Maybe (ModuleG ModName)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
let fi :: FileInfo
fi = Fingerprint
-> Set [Char] -> Set ModName -> Maybe ForeignSrc -> FileInfo
fileInfo Fingerprint
fp Set [Char]
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
forall (m :: * -> *) a. Monad m => a -> m a
return TCTopEntity
tcm
where
evalForeign :: ModuleG ModName -> ModuleT IO (Maybe ForeignSrc)
evalForeign ModuleG ModName
tcm
| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
foreignFs) =
forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) (forall a b. (a -> b) -> [a] -> [b]
map Name -> FFILoadError
FFI.FFIInFunctor [Name]
foreignFs)
| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Name]]
dups) =
forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) (forall a b. (a -> b) -> [a] -> [b]
map [Name] -> FFILoadError
FFI.FFIDuplicates [[Name]]
dups)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, FFIFunType)]
foreigns = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
| Bool
otherwise =
case ModulePath
path of
InFile [Char]
p -> forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO [Char]
canonicalizePath [Char]
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Char] -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
Right ForeignSrc
fsrc -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet forall a b. (a -> b) -> a -> b
$
case ForeignSrc -> Maybe [Char]
getForeignSrcPath ForeignSrc
fsrc of
Just [Char]
fpath -> forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger Logger -> [Char] -> IO ()
logPutStrLn forall a b. (a -> b) -> a -> b
$
[Char]
"Loading dynamic library " forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
takeFileName [Char]
fpath
Maybe [Char]
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
forall (t :: * -> *).
Traversable t =>
(EvalEnv -> Eval (t EvalEnv)) -> ModuleM (t ())
modifyEvalEnvM (ForeignSrc
-> [(Name, FFIFunType)]
-> EvalEnv
-> Eval (Either [FFILoadError] EvalEnv)
evalForeignDecls ForeignSrc
fsrc [(Name, FFIFunType)]
foreigns) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
Right () -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ForeignSrc
fsrc
Left [FFILoadError]
errs -> forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) [FFILoadError]
errs
Left FFILoadError
err -> forall a. ModName -> [FFILoadError] -> ModuleM a
ffiLoadErrors (forall mname. ModuleG mname -> mname
T.mName ModuleG ModName
tcm) [FFILoadError
err]
InMem [Char]
m ByteString
_ -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"doLoadModule"
[[Char]
"Can't find foreign source of in-memory module", [Char]
m]
where foreigns :: [(Name, FFIFunType)]
foreigns = forall mname. ModuleG mname -> [(Name, FFIFunType)]
findForeignDecls ModuleG ModName
tcm
foreignFs :: [Name]
foreignFs = forall mname. ModuleG mname -> [Name]
T.findForeignDeclsInFunctors ModuleG ModName
tcm
dups :: [[Name]]
dups = [ [Name]
d | d :: [Name]
d@(Name
_ : Name
_ : [Name]
_) <- forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Ident
nameIdent)
forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Ident
nameIdent)
forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, FFIFunType)]
foreigns ]
fullyQualified :: P.Import -> P.Import
fullyQualified :: Import -> Import
fullyQualified Import
i = Import
i { iAs :: Maybe ModName
iAs = forall a. a -> Maybe a
Just (forall mname. ImportG mname -> mname
iModule Import
i) }
moduleFile :: ModName -> String -> FilePath
moduleFile :: ModName -> [Char] -> [Char]
moduleFile ModName
n = [Char] -> [Char] -> [Char]
addExtension ([[Char]] -> [Char]
joinPath (ModName -> [[Char]]
modNameChunks ModName
n))
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 <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO Bool
doesFileExist [Char]
path)
if Bool
b then 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 forall a. Eq a => a -> a -> Bool
== ModName
preludeName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Cryptol" ByteString
preludeContents)
| ModName
m forall a. Eq a => a -> a -> Bool
== ModName
floatName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Float" ByteString
floatContents)
| ModName
m forall a. Eq a => a -> a -> Bool
== ModName
arrayName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Array" ByteString
arrayContents)
| ModName
m forall a. Eq a => a -> a -> Bool
== ModName
suiteBName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"SuiteB" ByteString
suiteBContents)
| ModName
m forall a. Eq a => a -> a -> Bool
== ModName
primeECName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"PrimeEC" ByteString
primeECContents)
| ModName
m forall a. Eq a => a -> a -> Bool
== ModName
preludeReferenceName -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ByteString -> ModulePath
InMem [Char]
"Cryptol::Reference" ByteString
preludeReferenceContents)
ModName
_ -> forall a. ModName -> [[Char]] -> ModuleM a
moduleNotFound ModName
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleM [[Char]]
getSearchPath
possibleFiles :: [[Char]] -> [[Char]]
possibleFiles [[Char]]
paths = do
[Char]
path <- [[Char]]
paths
[Char]
ext <- [[Char]]
P.knownExts
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char]
path [Char] -> [Char] -> [Char]
</> ModName -> [Char] -> [Char]
moduleFile ModName
n [Char]
ext)
findFile :: FilePath -> ModuleM FilePath
findFile :: [Char] -> ModuleM [Char]
findFile [Char]
path
| [Char] -> Bool
isAbsolute [Char]
path =
do
Bool
b <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO Bool
doesFileExist [Char]
path)
if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
path else forall a. [Char] -> ModuleM 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 <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO Bool
doesFileExist [Char]
path')
if Bool
b then forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> [Char]
normalise [Char]
path') else [[Char]] -> ModuleM [Char]
loop [[Char]]
rest
[] -> forall a. [Char] -> ModuleM a
cantFindFile [Char]
path
possibleFiles :: [[Char]] -> [[Char]]
possibleFiles [[Char]]
paths = forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char] -> [Char]
</> [Char]
path) [[Char]]
paths
addPrelude :: P.Module PName -> P.Module PName
addPrelude :: Module PName -> Module PName
addPrelude Module PName
m
| ModName
preludeName forall a. Eq a => a -> a -> Bool
== forall a. Located a -> a
P.thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
m) = Module PName
m
| ModName
preludeName forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModName]
importedMods = Module PName
m
| Bool
otherwise = Module PName
m { mDef :: ModuleDefinition PName
mDef = ModuleDefinition PName
newDef }
where
newDef :: ModuleDefinition PName
newDef =
case forall mname name. ModuleG mname name -> ModuleDefinition name
mDef Module PName
m of
NormalModule [TopDecl PName]
ds -> forall name. [TopDecl name] -> ModuleDefinition name
NormalModule (forall name. Located (ImportG (ImpName name)) -> TopDecl name
P.DImport forall {name}. Located (ImportG (ImpName name))
prel forall a. a -> [a] -> [a]
: [TopDecl PName]
ds)
FunctorInstance Located (ImpName PName)
f ModuleInstanceArgs PName
as ModuleInstance PName
ins -> 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 -> forall name. Signature name -> ModuleDefinition name
InterfaceModule Signature PName
s { sigImports :: [Located (ImportG (ImpName PName))]
sigImports = forall {name}. Located (ImportG (ImpName name))
prel
forall a. a -> [a] -> [a]
: forall name. Signature name -> [Located (ImportG (ImpName name))]
sigImports Signature PName
s }
importedMods :: [ModName]
importedMods = forall a b. (a -> b) -> [a] -> [b]
map (forall mname. ImportG mname -> mname
P.iModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
P.thing) (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 = forall name. ModName -> ImpName name
P.ImpTop ModName
preludeName
, iAs :: Maybe ModName
iAs = forall a. Maybe a
Nothing
, iSpec :: Maybe ImportSpec
iSpec = forall a. Maybe a
Nothing
, iInst :: Maybe (ModuleInstanceArgs PName)
iInst = forall a. Maybe a
Nothing
}
}
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 = forall mname name. ModuleG mname name -> [ImportSource]
findDeps ModuleG mname name
m
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
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule [ImportSource]
ds))
findDeps :: P.ModuleG mname name -> [ImportSource]
findDeps :: forall mname name. ModuleG mname name -> [ImportSource]
findDeps ModuleG mname name
m = forall a. Endo a -> a -> a
appEndo (forall a b. (a, b) -> b
snd (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io ([Char] -> IO [Char]
canonicalizePath [Char]
file)
InMem {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModulePath
mpath'
(Fingerprint
fp, Set [Char]
incs, [Module PName]
ms) <- ModulePath -> ModuleM (Fingerprint, Set [Char], [Module PName])
parseModule ModulePath
mpath
let (Any
anyF,Endo [ImportSource]
imps) = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map (forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module PName -> Module PName
addPrelude) [Module PName]
ms)
Set [Char]
fpath <- if Any -> Bool
getAny Any
anyF
then do Maybe [Char]
mb <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io case ModulePath
mpath of
InFile [Char]
can -> [Char] -> IO (Maybe [Char])
foreignLibPath [Char]
can
InMem {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
forall (f :: * -> *) a. Applicative f => a -> f a
pure case Maybe [Char]
mb of
Maybe [Char]
Nothing -> forall a. Set a
Set.empty
Just [Char]
f -> forall a. a -> Set a
Set.singleton [Char]
f
else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( ModulePath
mpath
, FileInfo
{ fiFingerprint :: Fingerprint
fiFingerprint = Fingerprint
fp
, fiIncludeDeps :: Set [Char]
fiIncludeDeps = Set [Char]
incs
, fiImportDeps :: Set ModName
fiImportDeps = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule (forall a. Endo a -> a -> a
appEndo Endo [ImportSource]
imps []))
, fiForeignDeps :: Set [Char]
fiForeignDeps = Set [Char]
fpath
}
)
findModuleDeps :: P.ModuleG mname name -> Set P.ModName
findModuleDeps :: forall mname name. ModuleG mname name -> Set ModName
findModuleDeps = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ImportSource -> ModName
importedModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall mname name. ModuleG mname name -> [ImportSource]
findDeps
findDeps' :: P.ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' :: forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' ModuleG mname name
m =
case forall mname name. ModuleG mname name -> ModuleDefinition name
mDef ModuleG mname name
m of
NormalModule [TopDecl name]
ds -> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map 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 = 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 -> forall {a} {name}.
Monoid a =>
Located (ModuleInstanceArg name) -> (a, Endo [ImportSource])
loadInstArg Located (ModuleInstanceArg name)
a
DefaultInstAnonArg [TopDecl name]
ds -> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall {name}. TopDecl name -> (Any, Endo [ImportSource])
depsOfDecl [TopDecl name]
ds)
NamedInstArgs [ModuleInstanceNamedArg name]
args -> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {name}.
Monoid a =>
ModuleInstanceNamedArg name -> (a, Endo [ImportSource])
loadNamedInstArg [ModuleInstanceNamedArg name]
args)
in (Any, Endo [ImportSource])
fds forall a. Semigroup a => a -> a -> a
<> (Any, Endo [ImportSource])
ads
InterfaceModule Signature name
s -> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {name}.
Monoid a =>
Located (ImportG (ImpName name)) -> (a, Endo [ImportSource])
loadImpD (forall name. Signature name -> [Located (ImportG (ImpName name))]
sigImports Signature name
s))
where
loadI :: a -> (a, Endo [a])
loadI a
i = (forall a. Monoid a => a
mempty, forall a. (a -> a) -> Endo a
Endo (a
iforall a. a -> [a] -> [a]
:))
loadImpName :: (Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName Located ModName -> a
src Located (ImpName name)
l =
case forall a. Located a -> a
thing Located (ImpName name)
l of
ImpTop ModName
f -> forall {a} {a}. Monoid a => a -> (a, Endo [a])
loadI (Located ModName -> a
src Located (ImpName name)
l { thing :: ModName
thing = ModName
f })
ImpName name
_ -> forall a. Monoid a => a
mempty
loadImpD :: Located (ImportG (ImpName name)) -> (a, Endo [ImportSource])
loadImpD Located (ImportG (ImpName name))
li = forall {a} {a} {name}.
Monoid a =>
(Located ModName -> a) -> Located (ImpName name) -> (a, Endo [a])
loadImpName (Located Import -> ImportSource
FromImport forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {mname}. Located mname -> Located (ImportG mname)
new) (forall mname. ImportG mname -> mname
iModule 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 :: ImportG mname
thing = (forall a. Located a -> a
thing Located (ImportG (ImpName name))
li) { iModule :: mname
iModule = forall a. Located a -> a
thing Located mname
i } }
loadNamedInstArg :: ModuleInstanceNamedArg name -> (a, Endo [ImportSource])
loadNamedInstArg (ModuleInstanceNamedArg Located Ident
_ Located (ModuleInstanceArg name)
f) = 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 forall a. Located a -> a
thing Located (ModuleInstanceArg name)
f of
ModuleArg ImpName name
mo -> 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 :: ImpName name
thing = ImpName name
mo }
ModuleInstanceArg name
_ -> 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 -> 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 } -> forall mname name. ModuleG mname name -> (Any, Endo [ImportSource])
findDeps' ModuleG name name
nm
DModParam ModParam name
mo -> 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 = forall name. ModParam name -> Located (ImpName name)
mpSignature ModParam name
mo
Decl TopLevel (Decl name)
dd -> forall {b} {name}. Monoid b => Decl name -> (Any, b)
depsOfDecl' (forall a. TopLevel a -> a
tlValue TopLevel (Decl name)
dd)
TopDecl name
_ -> 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 forall a. Located a -> a
thing (forall name. Bind name -> Located (BindDef name)
bDef Bind name
b) of
DForeign {} -> (Bool -> Any
Any Bool
True, forall a. Monoid a => a
mempty)
BindDef name
_ -> forall a. Monoid a => a
mempty
Decl name
_ -> forall a. Monoid a => a
mempty
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
Expr PName
npe <- forall a. RemovePatterns a => a -> ModuleM a
noPat Expr PName
e
Expr Name
re <- forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename ModName
interactiveName NamingEnv
names (forall (f :: * -> *). Rename f => f PName -> RenameM (f Name)
R.rename Expr PName
npe)
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) <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Name
re,Expr
te,Schema
s)
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) <- forall a. ModName -> NamingEnv -> RenameM a -> ModuleM a
rename ModName
interactiveName NamingEnv
names
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 = forall a. TCLinter ([DeclGroup], a)
declsLinter
, tcPrims :: PrimMap
tcPrims = PrimMap
prims }
([DeclGroup]
ds',Map Name TySyn
tyMap) <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return (NamingEnv
declsEnv,[DeclGroup]
ds',Map Name TySyn
tyMap)
getPrimMap :: ModuleM PrimMap
getPrimMap :: ModuleM PrimMap
getPrimMap =
do ModuleEnv
env <- forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
let mkPrims :: LoadedModule -> PrimMap
mkPrims = Iface -> PrimMap
ifacePrimMap 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 forall a. Semigroup a => a -> a -> a
<> PrimMap
mp
case ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule ModName
preludeName ModuleEnv
env of
Just LoadedModule
prel -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LoadedModule -> PrimMap
mkPrims LoadedModule
prel
PrimMap -> ModName -> PrimMap
`alsoPrimFrom` ModName
floatName
Maybe LoadedModule
Nothing -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Cryptol.ModuleSystem.Base.getPrimMap"
[ [Char]
"Unable to find the prelude" ]
checkModule ::
ImportSource ->
P.Module PName ->
ModuleM (R.NamingEnv,T.TCTopEntity)
checkModule :: ImportSource -> Module PName -> ModuleM (NamingEnv, TCTopEntity)
checkModule ImportSource
isrc Module PName
m = do
let nm :: ModName
nm = ImportSource -> ModName
importedModule ImportSource
isrc
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ModName -> ModName
modNameToNormalModName ModName
nm forall a. Eq a => a -> a -> Bool
==
ModName -> ModName
modNameToNormalModName (forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
m)))
(forall a. ModName -> Located ModName -> ModuleM a
moduleNameMismatch ModName
nm (forall mname name. ModuleG mname name -> Located mname
mName Module PName
m))
Module PName
npm <- forall a. RemovePatterns a => a -> ModuleM a
noPat Module PName
m
Module PName
epgm <- Module PName -> ModuleM (Module PName)
expandPropGuards Module PName
npm
RenamedModule
renMod <- Module PName -> ModuleM RenamedModule
renameModule Module PName
epgm
PrimMap
prims <- if forall a. Located a -> a
thing (forall mname name. ModuleG mname name -> Located mname
mName Module PName
m) forall a. Eq a => a -> a -> Bool
== ModName
preludeName
then forall (m :: * -> *) a. Monad m => a -> m a
return (NamingEnv -> PrimMap
R.toPrimMap (RenamedModule -> NamingEnv
R.rmDefines RenamedModule
renMod))
else ModuleM PrimMap
getPrimMap
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 (forall a. Located a -> a
P.thing (forall mname name. ModuleG mname name -> Located mname
P.mName Module PName
m))
, tcPrims :: PrimMap
tcPrims = PrimMap
prims }
TCTopEntity
tcm <- 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Supply -> ModuleG ModName -> (ModuleG ModName, Supply)
`rewModule` ModuleG ModName
mo)
T.TCTopSignature {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TCTopEntity
tcm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RenamedModule -> NamingEnv
R.rmInScope RenamedModule
renMod,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 -> forall a b. a -> Either a b
Left (Range, Error)
err
Right (Schema
s1,[Schema]
os)
| TcSanity.SameIf [Prop]
os' <- forall a. Same a => a -> a -> AreSame
TcSanity.same Schema
s Schema
s1 ->
forall a b. b -> Either a b
Right (forall a b. (a -> b) -> [a] -> [b]
map Prop -> Schema
T.tMono [Prop]
os' forall a. [a] -> [a] -> [a]
++ [Schema]
os)
| Bool
otherwise -> forall a b. a -> Either a b
Left ( forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (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 = 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 -> forall a b. a -> Either a b
Left (Range, Error)
err
Right [Schema]
os -> forall a b. b -> Either a b
Right [Schema]
os
, lintModule :: Maybe ModName
lintModule = 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 -> forall a b. a -> Either a b
Left (Range, Error)
err
Right [Schema]
os -> forall a b. b -> Either a b
Right [Schema]
os
, lintModule :: Maybe ModName
lintModule = 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 ->
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 {} -> forall a b. b -> Either a b
Right []
, lintModule :: Maybe ModName
lintModule = 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 = forall a. a -> Maybe a -> a
fromMaybe Range
emptyRange (forall t. HasLoc t => t -> Maybe Range
getLoc i
i)
InferInput
input <- Range
-> PrimMap -> ModContextParams -> IfaceDecls -> ModuleM InferInput
genInferInput Range
range (forall i o. TCAction i o -> PrimMap
tcPrims TCAction i o
act) ModContextParams
params IfaceDecls
env
InferOutput o
out <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io (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 <- forall (m :: * -> *). Monad m => ModuleT m ModuleEnv
getModuleEnv
case ModuleEnv -> CoreLint
meCoreLint ModuleEnv
menv of
CoreLint
NoCoreLint -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
CoreLint
CoreLint -> case forall o.
TCLinter o -> o -> InferInput -> Either (Range, Error) [Schema]
lintCheck (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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a. Show a => Logger -> a -> IO ()
logPrint Logger
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
T.pp)
in forall a b. (Logger -> a -> IO b) -> a -> ModuleM b
withLogger forall {t :: * -> *} {a}.
(Foldable t, PP a) =>
Logger -> t a -> IO ()
ppIt ([Schema] -> [Schema]
TcSanity.onlyNonTrivial [Schema]
as)
Left (Range
loc,Error
err) ->
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"Core lint failed:"
[ [Char]
"Location: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
T.pp Range
loc)
, forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
T.pp Error
err)
]
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
forall a. NameMap -> [(Range, Error)] -> ModuleM a
typeCheckingFailed NameMap
nameMap [(Range, Error)]
errs
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 <- forall (m :: * -> *). Monad m => ModuleT m Solver
getTCSolver
Supply
supply <- ModuleM Supply
getSupply
[[Char]]
searchPath <- ModuleM [[Char]]
getSearchPath
Bool
callStacks <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return T.InferInput
{ inpRange :: Range
T.inpRange = Range
r
, inpVars :: Map Name Schema
T.inpVars = 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
, 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 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
}
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 <- ModuleM (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 -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
let ?range = Range
emptyRange
Bool
callStacks <- forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
let ?callStacks = Bool
callStacks
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io forall a b. (a -> b) -> a -> b
$ forall a. CallStack -> Eval a -> IO a
E.runEval forall a. Monoid a => a
mempty (forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
E.evalExpr Concrete
Concrete (EvalEnv
env 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 <- ModuleM (IO EvalOpts)
getEvalOptsAction
let env' :: EvalEnv
env' = EvalEnv
env 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 -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
let ?range = Range
emptyRange
Bool
callStacks <- forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
let ?callStacks = Bool
callStacks
let eval :: Expr -> IO ()
eval Expr
expr = forall a. CallStack -> Eval a -> IO a
E.runEval forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
forall sym.
(?range::Range, EvalPrims sym) =>
sym -> GenEvalEnv sym -> Expr -> SEval sym (GenValue sym)
E.evalExpr Concrete
Concrete EvalEnv
env' Expr
expr forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall sym. Backend sym => GenValue sym -> SEval sym ()
E.forceValue
forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io forall a b. (a -> b) -> a -> b
$ 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 ()
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 <- ModuleM (IO EvalOpts)
getEvalOptsAction
let env' :: EvalEnv
env' = EvalEnv
env 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 -> forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PrimIdent
i Map PrimIdent (Prim Concrete)
tbl
Bool
callStacks <- forall (m :: * -> *). Monad m => ModuleT m Bool
getCallStacks
let ?callStacks = Bool
callStacks
EvalEnv
deEnv' <- forall (m :: * -> *) a. BaseM m IO => IO a -> ModuleT m a
io forall a b. (a -> b) -> a -> b
$ forall a. CallStack -> Eval a -> IO a
E.runEval forall a. Monoid a => a
mempty (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 forall a. [a] -> [a] -> [a]
++ [DeclGroup]
dgs
, deEnv :: EvalEnv
deEnv = EvalEnv
deEnv'
}
DynamicEnv -> ModuleM ()
setDynEnv DynamicEnv
denv'