mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-28 18:32:07 +03:00
Keep track of the files used by a module
This commit is contained in:
parent
fe00904e38
commit
74ceb6b11f
@ -255,10 +255,10 @@ doLoadModule ::
|
||||
Set FilePath {- ^ `include` dependencies -} ->
|
||||
P.Module PName ->
|
||||
ModuleM T.TCTopEntity
|
||||
doLoadModule eval quiet isrc path fp deps pm0 =
|
||||
doLoadModule eval quiet isrc path fp incDeps pm0 =
|
||||
loading isrc $
|
||||
do let pm = addPrelude pm0
|
||||
loadDeps pm
|
||||
impDeps <- loadDeps pm
|
||||
|
||||
let what = case P.mDef pm of
|
||||
P.InterfaceModule {} -> "interface module"
|
||||
@ -287,31 +287,38 @@ doLoadModule eval quiet isrc path fp deps pm0 =
|
||||
pure fsrc
|
||||
Nothing -> pure Nothing
|
||||
|
||||
loadedModule path fp nameEnv foreignSrc tcm
|
||||
loadedModule path fp nameEnv incDeps impDeps foreignSrc tcm
|
||||
|
||||
return tcm
|
||||
|
||||
where
|
||||
evalForeign tcm
|
||||
| not (null foreignFs) = ffiLoadErrors (T.mName tcm) (map FFI.FFIInFunctor foreignFs)
|
||||
| not (null dups) = ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)
|
||||
| not (null foreignFs) =
|
||||
ffiLoadErrors (T.mName tcm) (map FFI.FFIInFunctor foreignFs)
|
||||
| not (null dups) =
|
||||
ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)
|
||||
| null foreigns = pure Nothing
|
||||
| otherwise = case path of
|
||||
InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=
|
||||
\case
|
||||
Right fsrc -> do
|
||||
unless quiet $
|
||||
case getForeignSrcPath fsrc of
|
||||
Just fpath -> withLogger logPutStrLn $
|
||||
"Loading dynamic library " ++ takeFileName fpath
|
||||
Nothing -> pure ()
|
||||
modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>=
|
||||
\case
|
||||
Right () -> pure $ Just fsrc
|
||||
Left errs -> ffiLoadErrors (T.mName tcm) errs
|
||||
Left err -> ffiLoadErrors (T.mName tcm) [err]
|
||||
InMem m _ -> panic "doLoadModule"
|
||||
["Can't find foreign source of in-memory module", m]
|
||||
| otherwise =
|
||||
case path of
|
||||
InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=
|
||||
\case
|
||||
|
||||
Right fsrc -> do
|
||||
unless quiet $
|
||||
case getForeignSrcPath fsrc of
|
||||
Just fpath -> withLogger logPutStrLn $
|
||||
"Loading dynamic library " ++ takeFileName fpath
|
||||
Nothing -> pure ()
|
||||
modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>=
|
||||
\case
|
||||
Right () -> pure $ Just fsrc
|
||||
Left errs -> ffiLoadErrors (T.mName tcm) errs
|
||||
|
||||
Left err -> ffiLoadErrors (T.mName tcm) [err]
|
||||
|
||||
InMem m _ -> panic "doLoadModule"
|
||||
["Can't find foreign source of in-memory module", m]
|
||||
|
||||
where foreigns = findForeignDecls tcm
|
||||
foreignFs = T.findForeignDeclsInFunctors tcm
|
||||
dups = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)
|
||||
@ -404,25 +411,26 @@ addPrelude m
|
||||
}
|
||||
|
||||
-- | Load the dependencies of a module into the environment.
|
||||
loadDeps :: P.ModuleG mname name -> ModuleM ()
|
||||
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModulePath)
|
||||
loadDeps m =
|
||||
case mDef m of
|
||||
NormalModule ds -> mapM_ depsOfDecl ds
|
||||
NormalModule ds -> Set.unions <$> mapM depsOfDecl ds
|
||||
FunctorInstance f as _ ->
|
||||
do loadImpName FromModuleInstance f
|
||||
case as of
|
||||
DefaultInstArg a -> loadInstArg a
|
||||
DefaultInstAnonArg ds -> mapM_ depsOfDecl ds
|
||||
NamedInstArgs args -> mapM_ loadNamedInstArg args
|
||||
InterfaceModule s -> mapM_ loadImpD (sigImports s)
|
||||
do fds <- loadImpName FromModuleInstance f
|
||||
ads <- case as of
|
||||
DefaultInstArg a -> loadInstArg a
|
||||
DefaultInstAnonArg ds -> Set.unions <$> mapM depsOfDecl ds
|
||||
NamedInstArgs args ->
|
||||
Set.unions <$> mapM loadNamedInstArg args
|
||||
pure (Set.union fds ads)
|
||||
InterfaceModule s -> Set.unions <$> mapM loadImpD (sigImports s)
|
||||
where
|
||||
loadI i = do _ <- loadModuleFrom False i
|
||||
pure ()
|
||||
loadI i = Set.singleton . fst <$> loadModuleFrom False i
|
||||
|
||||
loadImpName src l =
|
||||
case thing l of
|
||||
ImpTop f -> loadI (src l { thing = f })
|
||||
_ -> pure ()
|
||||
_ -> pure Set.empty
|
||||
|
||||
loadImpD li = loadImpName (FromImport . new) (iModule <$> li)
|
||||
where new i = i { thing = (thing li) { iModule = thing i } }
|
||||
@ -431,7 +439,7 @@ loadDeps m =
|
||||
loadInstArg f =
|
||||
case thing f of
|
||||
ModuleArg mo -> loadImpName FromModuleInstance f { thing = mo }
|
||||
_ -> pure ()
|
||||
_ -> pure Set.empty
|
||||
|
||||
depsOfDecl d =
|
||||
case d of
|
||||
@ -442,7 +450,7 @@ loadDeps m =
|
||||
DModParam mo -> loadImpName FromSigImport s
|
||||
where s = mpSignature mo
|
||||
|
||||
_ -> pure ()
|
||||
_ -> pure Set.empty
|
||||
|
||||
|
||||
|
||||
|
@ -7,6 +7,7 @@
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
@ -19,7 +20,7 @@ module Cryptol.ModuleSystem.Env where
|
||||
import Paths_cryptol (getDataDir)
|
||||
#endif
|
||||
|
||||
import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc)
|
||||
import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc, getForeignSrcPath)
|
||||
import Cryptol.Eval (EvalEnv)
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
@ -40,6 +41,7 @@ import qualified Data.Set as Set
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Semigroup
|
||||
import Data.Maybe(fromMaybe)
|
||||
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
|
||||
import System.Environment(getExecutablePath)
|
||||
import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
|
||||
@ -319,6 +321,17 @@ instance Eq ModulePath where
|
||||
(InMem a _, InMem b _) -> a == b
|
||||
_ -> False
|
||||
|
||||
-- | In-memory things are compared by label.
|
||||
instance Ord ModulePath where
|
||||
compare p1 p2 =
|
||||
case (p1,p2) of
|
||||
(InFile x, InFile y) -> compare x y
|
||||
(InMem a _, InMem b _) -> compare a b
|
||||
(InMem {}, InFile {}) -> LT
|
||||
(InFile {}, InMem {}) -> GT
|
||||
|
||||
|
||||
|
||||
instance PP ModulePath where
|
||||
ppPrec _ e =
|
||||
case e of
|
||||
@ -399,6 +412,10 @@ data LoadedModuleG a = LoadedModule
|
||||
|
||||
, lmFingerprint :: Fingerprint
|
||||
|
||||
, lmIncludeDeps :: !(Set FilePath) -- ^ Files that were included
|
||||
, lmImportDeps :: !(Set ModulePath) -- ^ Files that were imported
|
||||
, lmForeignDeps :: !(Set FilePath) -- ^ Foreign libraries
|
||||
|
||||
, lmData :: a
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
@ -457,10 +474,12 @@ lookupSignature mn me =
|
||||
List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me))
|
||||
|
||||
addLoadedSignature ::
|
||||
ModulePath -> String -> Fingerprint -> R.NamingEnv ->
|
||||
ModulePath -> String ->
|
||||
Fingerprint -> Set FilePath -> Set ModulePath ->
|
||||
R.NamingEnv ->
|
||||
ModName -> T.ModParamNames ->
|
||||
LoadedModules -> LoadedModules
|
||||
addLoadedSignature path ident fp nameEnv nm si lm
|
||||
addLoadedSignature path ident fp incDeps impDeps nameEnv nm si lm
|
||||
| isLoaded nm lm = lm
|
||||
| otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }
|
||||
where
|
||||
@ -471,14 +490,23 @@ addLoadedSignature path ident fp nameEnv nm si lm
|
||||
, lmNamingEnv = nameEnv
|
||||
, lmData = si
|
||||
, lmFingerprint = fp
|
||||
, lmIncludeDeps = incDeps
|
||||
, lmImportDeps = impDeps
|
||||
, lmForeignDeps = Set.empty
|
||||
}
|
||||
|
||||
-- | Add a freshly loaded module. If it was previously loaded, then
|
||||
-- the new version is ignored.
|
||||
addLoadedModule ::
|
||||
ModulePath -> String -> Fingerprint -> R.NamingEnv -> Maybe ForeignSrc ->
|
||||
ModulePath ->
|
||||
String ->
|
||||
Fingerprint ->
|
||||
Set FilePath ->
|
||||
Set ModulePath ->
|
||||
R.NamingEnv ->
|
||||
Maybe ForeignSrc ->
|
||||
T.Module -> LoadedModules -> LoadedModules
|
||||
addLoadedModule path ident fp nameEnv fsrc tm lm
|
||||
addLoadedModule path ident fp incDeps impDeps nameEnv fsrc tm lm
|
||||
| isLoaded (T.mName tm) lm = lm
|
||||
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
||||
lmLoadedParamModules lm }
|
||||
@ -496,6 +524,11 @@ addLoadedModule path ident fp nameEnv fsrc tm lm
|
||||
, lmForeignSrc = fsrc
|
||||
}
|
||||
, lmFingerprint = fp
|
||||
, lmIncludeDeps = incDeps
|
||||
, lmImportDeps = impDeps
|
||||
, lmForeignDeps = fromMaybe Set.empty
|
||||
do fs <- fsrc
|
||||
Set.singleton <$> getForeignSrcPath fs
|
||||
}
|
||||
|
||||
-- | Remove a previously loaded module.
|
||||
|
@ -14,6 +14,8 @@
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
module Cryptol.ModuleSystem.Monad where
|
||||
|
||||
import Data.Set(Set)
|
||||
|
||||
import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
||||
|
||||
import Cryptol.Backend.FFI (ForeignSrc)
|
||||
@ -530,9 +532,15 @@ unloadModule rm = ModuleT $ do
|
||||
set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
|
||||
|
||||
loadedModule ::
|
||||
ModulePath -> Fingerprint -> NamingEnv -> Maybe ForeignSrc -> T.TCTopEntity ->
|
||||
ModulePath ->
|
||||
Fingerprint ->
|
||||
NamingEnv ->
|
||||
Set FilePath {- ^ includes -} ->
|
||||
Set ModulePath {- ^ imports -} ->
|
||||
Maybe ForeignSrc ->
|
||||
T.TCTopEntity ->
|
||||
ModuleM ()
|
||||
loadedModule path fp nameEnv fsrc m = ModuleT $ do
|
||||
loadedModule path fp nameEnv incDeps impDeps fsrc m = ModuleT $ do
|
||||
env <- get
|
||||
ident <- case path of
|
||||
InFile p -> unModuleT $ io (canonicalizePath p)
|
||||
@ -540,8 +548,10 @@ loadedModule path fp nameEnv fsrc m = ModuleT $ do
|
||||
|
||||
let newLM =
|
||||
case m of
|
||||
T.TCTopModule mo -> addLoadedModule path ident fp nameEnv fsrc mo
|
||||
T.TCTopSignature x s -> addLoadedSignature path ident fp nameEnv x s
|
||||
T.TCTopModule mo ->
|
||||
addLoadedModule path ident fp incDeps impDeps nameEnv fsrc mo
|
||||
T.TCTopSignature x s ->
|
||||
addLoadedSignature path ident fp incDeps impDeps nameEnv x s
|
||||
|
||||
set $! env { meLoadedModules = newLM (meLoadedModules env) }
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user