mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-29 10:53:31 +03:00
Group file related information together.
This also changes us to keep track of the names of imported modules rather than the files. This makes it possible to print a whole dependency tree, as we already have a way to get the filename and figerpreint of loaded modules
This commit is contained in:
parent
74ceb6b11f
commit
ef8391ffd0
@ -44,7 +44,7 @@ import Prelude.Compat hiding ( (<>) )
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..))
|
import Cryptol.ModuleSystem.Env (DynamicEnv(..),fileInfo)
|
||||||
import Cryptol.ModuleSystem.Fingerprint
|
import Cryptol.ModuleSystem.Fingerprint
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Monad
|
import Cryptol.ModuleSystem.Monad
|
||||||
@ -287,7 +287,8 @@ doLoadModule eval quiet isrc path fp incDeps pm0 =
|
|||||||
pure fsrc
|
pure fsrc
|
||||||
Nothing -> pure Nothing
|
Nothing -> pure Nothing
|
||||||
|
|
||||||
loadedModule path fp nameEnv incDeps impDeps foreignSrc tcm
|
let fi = fileInfo fp incDeps impDeps foreignSrc
|
||||||
|
loadedModule path fi nameEnv foreignSrc tcm
|
||||||
|
|
||||||
return tcm
|
return tcm
|
||||||
|
|
||||||
@ -411,7 +412,7 @@ addPrelude m
|
|||||||
}
|
}
|
||||||
|
|
||||||
-- | Load the dependencies of a module into the environment.
|
-- | Load the dependencies of a module into the environment.
|
||||||
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModulePath)
|
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName)
|
||||||
loadDeps m =
|
loadDeps m =
|
||||||
case mDef m of
|
case mDef m of
|
||||||
NormalModule ds -> Set.unions <$> mapM depsOfDecl ds
|
NormalModule ds -> Set.unions <$> mapM depsOfDecl ds
|
||||||
@ -425,7 +426,8 @@ loadDeps m =
|
|||||||
pure (Set.union fds ads)
|
pure (Set.union fds ads)
|
||||||
InterfaceModule s -> Set.unions <$> mapM loadImpD (sigImports s)
|
InterfaceModule s -> Set.unions <$> mapM loadImpD (sigImports s)
|
||||||
where
|
where
|
||||||
loadI i = Set.singleton . fst <$> loadModuleFrom False i
|
loadI i = do _ <- loadModuleFrom False i
|
||||||
|
pure (Set.singleton (importedModule i))
|
||||||
|
|
||||||
loadImpName src l =
|
loadImpName src l =
|
||||||
case thing l of
|
case thing l of
|
||||||
|
@ -410,11 +410,7 @@ data LoadedModuleG a = LoadedModule
|
|||||||
, lmNamingEnv :: !R.NamingEnv
|
, lmNamingEnv :: !R.NamingEnv
|
||||||
-- ^ What's in scope in this module
|
-- ^ What's in scope in this module
|
||||||
|
|
||||||
, lmFingerprint :: Fingerprint
|
, lmFileInfo :: !FileInfo
|
||||||
|
|
||||||
, lmIncludeDeps :: !(Set FilePath) -- ^ Files that were included
|
|
||||||
, lmImportDeps :: !(Set ModulePath) -- ^ Files that were imported
|
|
||||||
, lmForeignDeps :: !(Set FilePath) -- ^ Foreign libraries
|
|
||||||
|
|
||||||
, lmData :: a
|
, lmData :: a
|
||||||
} deriving (Show, Generic, NFData)
|
} deriving (Show, Generic, NFData)
|
||||||
@ -475,11 +471,11 @@ lookupSignature mn me =
|
|||||||
|
|
||||||
addLoadedSignature ::
|
addLoadedSignature ::
|
||||||
ModulePath -> String ->
|
ModulePath -> String ->
|
||||||
Fingerprint -> Set FilePath -> Set ModulePath ->
|
FileInfo ->
|
||||||
R.NamingEnv ->
|
R.NamingEnv ->
|
||||||
ModName -> T.ModParamNames ->
|
ModName -> T.ModParamNames ->
|
||||||
LoadedModules -> LoadedModules
|
LoadedModules -> LoadedModules
|
||||||
addLoadedSignature path ident fp incDeps impDeps nameEnv nm si lm
|
addLoadedSignature path ident fi nameEnv nm si lm
|
||||||
| isLoaded nm lm = lm
|
| isLoaded nm lm = lm
|
||||||
| otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }
|
| otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }
|
||||||
where
|
where
|
||||||
@ -489,10 +485,7 @@ addLoadedSignature path ident fp incDeps impDeps nameEnv nm si lm
|
|||||||
, lmModuleId = ident
|
, lmModuleId = ident
|
||||||
, lmNamingEnv = nameEnv
|
, lmNamingEnv = nameEnv
|
||||||
, lmData = si
|
, lmData = si
|
||||||
, lmFingerprint = fp
|
, lmFileInfo = fi
|
||||||
, lmIncludeDeps = incDeps
|
|
||||||
, lmImportDeps = impDeps
|
|
||||||
, lmForeignDeps = Set.empty
|
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Add a freshly loaded module. If it was previously loaded, then
|
-- | Add a freshly loaded module. If it was previously loaded, then
|
||||||
@ -500,13 +493,11 @@ addLoadedSignature path ident fp incDeps impDeps nameEnv nm si lm
|
|||||||
addLoadedModule ::
|
addLoadedModule ::
|
||||||
ModulePath ->
|
ModulePath ->
|
||||||
String ->
|
String ->
|
||||||
Fingerprint ->
|
FileInfo ->
|
||||||
Set FilePath ->
|
|
||||||
Set ModulePath ->
|
|
||||||
R.NamingEnv ->
|
R.NamingEnv ->
|
||||||
Maybe ForeignSrc ->
|
Maybe ForeignSrc ->
|
||||||
T.Module -> LoadedModules -> LoadedModules
|
T.Module -> LoadedModules -> LoadedModules
|
||||||
addLoadedModule path ident fp incDeps impDeps nameEnv fsrc tm lm
|
addLoadedModule path ident fi nameEnv fsrc tm lm
|
||||||
| isLoaded (T.mName tm) lm = lm
|
| isLoaded (T.mName tm) lm = lm
|
||||||
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
||||||
lmLoadedParamModules lm }
|
lmLoadedParamModules lm }
|
||||||
@ -523,12 +514,7 @@ addLoadedModule path ident fp incDeps impDeps nameEnv fsrc tm lm
|
|||||||
, lmdModule = tm
|
, lmdModule = tm
|
||||||
, lmForeignSrc = fsrc
|
, lmForeignSrc = fsrc
|
||||||
}
|
}
|
||||||
, lmFingerprint = fp
|
, lmFileInfo = fi
|
||||||
, lmIncludeDeps = incDeps
|
|
||||||
, lmImportDeps = impDeps
|
|
||||||
, lmForeignDeps = fromMaybe Set.empty
|
|
||||||
do fs <- fsrc
|
|
||||||
Set.singleton <$> getForeignSrcPath fs
|
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Remove a previously loaded module.
|
-- | Remove a previously loaded module.
|
||||||
@ -543,6 +529,33 @@ removeLoadedModule rm lm =
|
|||||||
, lmLoadedSignatures = filter (not . rm) (lmLoadedSignatures lm)
|
, lmLoadedSignatures = filter (not . rm) (lmLoadedSignatures lm)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
-- FileInfo --------------------------------------------------------------------
|
||||||
|
|
||||||
|
data FileInfo = FileInfo
|
||||||
|
{ fiFingerprint :: Fingerprint
|
||||||
|
, fiIncludeDeps :: Set FilePath
|
||||||
|
, fiImportDeps :: Set ModName
|
||||||
|
, fiForeignDeps :: Set FilePath
|
||||||
|
} deriving (Show,Generic,NFData)
|
||||||
|
|
||||||
|
|
||||||
|
fileInfo ::
|
||||||
|
Fingerprint ->
|
||||||
|
Set FilePath ->
|
||||||
|
Set ModName ->
|
||||||
|
Maybe ForeignSrc ->
|
||||||
|
FileInfo
|
||||||
|
fileInfo fp incDeps impDeps fsrc =
|
||||||
|
FileInfo
|
||||||
|
{ fiFingerprint = fp
|
||||||
|
, fiIncludeDeps = incDeps
|
||||||
|
, fiImportDeps = impDeps
|
||||||
|
, fiForeignDeps = fromMaybe Set.empty
|
||||||
|
do src <- fsrc
|
||||||
|
Set.singleton <$> getForeignSrcPath src
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
-- Dynamic Environments --------------------------------------------------------
|
-- Dynamic Environments --------------------------------------------------------
|
||||||
|
|
||||||
-- | Extra information we need to carry around to dynamically extend
|
-- | Extra information we need to carry around to dynamically extend
|
||||||
|
@ -14,8 +14,6 @@
|
|||||||
{-# LANGUAGE BlockArguments #-}
|
{-# LANGUAGE BlockArguments #-}
|
||||||
module Cryptol.ModuleSystem.Monad where
|
module Cryptol.ModuleSystem.Monad where
|
||||||
|
|
||||||
import Data.Set(Set)
|
|
||||||
|
|
||||||
import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
||||||
|
|
||||||
import Cryptol.Backend.FFI (ForeignSrc)
|
import Cryptol.Backend.FFI (ForeignSrc)
|
||||||
@ -24,7 +22,6 @@ import qualified Cryptol.Backend.Monad as E
|
|||||||
|
|
||||||
import Cryptol.ModuleSystem.Env
|
import Cryptol.ModuleSystem.Env
|
||||||
import qualified Cryptol.ModuleSystem.Env as MEnv
|
import qualified Cryptol.ModuleSystem.Env as MEnv
|
||||||
import Cryptol.ModuleSystem.Fingerprint
|
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
|
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
|
||||||
import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning())
|
import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning())
|
||||||
@ -533,14 +530,12 @@ unloadModule rm = ModuleT $ do
|
|||||||
|
|
||||||
loadedModule ::
|
loadedModule ::
|
||||||
ModulePath ->
|
ModulePath ->
|
||||||
Fingerprint ->
|
FileInfo ->
|
||||||
NamingEnv ->
|
NamingEnv ->
|
||||||
Set FilePath {- ^ includes -} ->
|
|
||||||
Set ModulePath {- ^ imports -} ->
|
|
||||||
Maybe ForeignSrc ->
|
Maybe ForeignSrc ->
|
||||||
T.TCTopEntity ->
|
T.TCTopEntity ->
|
||||||
ModuleM ()
|
ModuleM ()
|
||||||
loadedModule path fp nameEnv incDeps impDeps fsrc m = ModuleT $ do
|
loadedModule path fi nameEnv fsrc m = ModuleT $ do
|
||||||
env <- get
|
env <- get
|
||||||
ident <- case path of
|
ident <- case path of
|
||||||
InFile p -> unModuleT $ io (canonicalizePath p)
|
InFile p -> unModuleT $ io (canonicalizePath p)
|
||||||
@ -548,10 +543,8 @@ loadedModule path fp nameEnv incDeps impDeps fsrc m = ModuleT $ do
|
|||||||
|
|
||||||
let newLM =
|
let newLM =
|
||||||
case m of
|
case m of
|
||||||
T.TCTopModule mo ->
|
T.TCTopModule mo -> addLoadedModule path ident fi nameEnv fsrc mo
|
||||||
addLoadedModule path ident fp incDeps impDeps nameEnv fsrc mo
|
T.TCTopSignature x s -> addLoadedSignature path ident fi nameEnv x s
|
||||||
T.TCTopSignature x s ->
|
|
||||||
addLoadedSignature path ident fp incDeps impDeps nameEnv x s
|
|
||||||
|
|
||||||
set $! env { meLoadedModules = newLM (meLoadedModules env) }
|
set $! env { meLoadedModules = newLM (meLoadedModules env) }
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user