1-- | 2-- Module : Cryptol.ModuleSystem.Env 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE CPP #-} 10{-# LANGUAGE DeriveAnyClass #-} 11{-# LANGUAGE DeriveGeneric #-} 12{-# LANGUAGE PatternGuards #-} 13{-# LANGUAGE RecordWildCards #-} 14module Cryptol.ModuleSystem.Env where 15 16#ifndef RELOCATABLE 17import Paths_cryptol (getDataDir) 18#endif 19 20import Cryptol.Eval (EvalEnv) 21import Cryptol.ModuleSystem.Fingerprint 22import Cryptol.ModuleSystem.Interface 23import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply) 24import qualified Cryptol.ModuleSystem.NamingEnv as R 25import Cryptol.Parser.AST 26import qualified Cryptol.TypeCheck as T 27import qualified Cryptol.TypeCheck.AST as T 28import Cryptol.Utils.PP (PP(..),text,parens,NameDisp) 29 30import Data.ByteString(ByteString) 31import Control.Monad (guard,mplus) 32import qualified Control.Exception as X 33import Data.Function (on) 34import Data.Map (Map) 35import qualified Data.Map as Map 36import Data.Semigroup 37import System.Directory (getAppUserDataDirectory, getCurrentDirectory) 38import System.Environment(getExecutablePath) 39import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory) 40import qualified Data.List as List 41 42import GHC.Generics (Generic) 43import Control.DeepSeq 44 45import Prelude () 46import Prelude.Compat 47 48import Cryptol.Utils.Panic(panic) 49import Cryptol.Utils.PP(pp) 50 51-- Module Environment ---------------------------------------------------------- 52 53-- | This is the current state of the interpreter. 54data ModuleEnv = ModuleEnv 55 { meLoadedModules :: LoadedModules 56 -- ^ Information about all loaded modules. See 'LoadedModule'. 57 -- Contains information such as the file where the module was loaded 58 -- from, as well as the module's interface, used for type checking. 59 60 , meNameSeeds :: T.NameSeeds 61 -- ^ A source of new names for the type checker. 62 63 , meSolverConfig :: T.SolverConfig 64 -- ^ Configuration settings for the SMT solver used for type-checking. 65 66 , meEvalEnv :: EvalEnv 67 -- ^ The evaluation environment. Contains the values for all loaded 68 -- modules, both public and private. 69 70 , meCoreLint :: CoreLint 71 -- ^ Should we run the linter to ensure sanity. 72 73 , meMonoBinds :: !Bool 74 -- ^ Are we assuming that local bindings are monomorphic. 75 -- XXX: We should probably remove this flag, and set it to 'True'. 76 77 78 79 , meFocusedModule :: Maybe ModName 80 -- ^ The "current" module. Used to decide how to print names, for example. 81 82 , meSearchPath :: [FilePath] 83 -- ^ Where we look for things. 84 85 , meDynEnv :: DynamicEnv 86 -- ^ This contains additional definitions that were made at the command 87 -- line, and so they don't reside in any module. 88 89 , meSupply :: !Supply 90 -- ^ Name source for the renamer 91 92 } deriving Generic 93 94instance NFData ModuleEnv where 95 rnf x = meLoadedModules x `seq` meEvalEnv x `seq` meDynEnv x `seq` () 96 97-- | Should we run the linter? 98data CoreLint = NoCoreLint -- ^ Don't run core lint 99 | CoreLint -- ^ Run core lint 100 deriving (Generic, NFData) 101 102resetModuleEnv :: ModuleEnv -> ModuleEnv 103resetModuleEnv env = env 104 { meLoadedModules = mempty 105 , meNameSeeds = T.nameSeeds 106 , meEvalEnv = mempty 107 , meFocusedModule = Nothing 108 , meDynEnv = mempty 109 } 110 111initialModuleEnv :: IO ModuleEnv 112initialModuleEnv = do 113 curDir <- getCurrentDirectory 114#ifndef RELOCATABLE 115 dataDir <- getDataDir 116#endif 117 binDir <- takeDirectory `fmap` getExecutablePath 118 let instDir = normalise . joinPath . init . splitPath $ binDir 119 -- looking up this directory can fail if no HOME is set, as in some 120 -- CI settings 121 let handle :: X.IOException -> IO String 122 handle _e = return "" 123 userDir <- X.catch (getAppUserDataDirectory "cryptol") handle 124 let searchPath = [ curDir 125 -- something like $HOME/.cryptol 126 , userDir 127#if defined(mingw32_HOST_OS) || defined(__MINGW32__) 128 -- ../cryptol on win32 129 , instDir </> "cryptol" 130#else 131 -- ../share/cryptol on others 132 , instDir </> "share" </> "cryptol" 133#endif 134 135#ifndef RELOCATABLE 136 -- Cabal-defined data directory. Since this 137 -- is usually a global location like 138 -- /usr/local, search this one last in case 139 -- someone has multiple Cryptols 140 , dataDir 141#endif 142 ] 143 144 return ModuleEnv 145 { meLoadedModules = mempty 146 , meNameSeeds = T.nameSeeds 147 , meEvalEnv = mempty 148 , meFocusedModule = Nothing 149 -- we search these in order, taking the first match 150 , meSearchPath = searchPath 151 , meDynEnv = mempty 152 , meMonoBinds = True 153 , meSolverConfig = T.SolverConfig 154 { T.solverPath = "z3" 155 , T.solverArgs = [ "-smt2", "-in" ] 156 , T.solverVerbose = 0 157 , T.solverPreludePath = searchPath 158 } 159 , meCoreLint = NoCoreLint 160 , meSupply = emptySupply 161 } 162 163-- | Try to focus a loaded module in the module environment. 164focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv 165focusModule n me = do 166 guard (isLoaded n (meLoadedModules me)) 167 return me { meFocusedModule = Just n } 168 169-- | Get a list of all the loaded modules. Each module in the 170-- resulting list depends only on other modules that precede it. 171-- Note that this includes parameterized modules. 172loadedModules :: ModuleEnv -> [T.Module] 173loadedModules = map lmModule . getLoadedModules . meLoadedModules 174 175-- | Get a list of all the loaded non-parameterized modules. 176-- These are the modules that can be used for evaluation, proving etc. 177loadedNonParamModules :: ModuleEnv -> [T.Module] 178loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules 179 180loadedNewtypes :: ModuleEnv -> Map Name IfaceNewtype 181loadedNewtypes menv = Map.unions 182 [ ifNewtypes (ifPublic i) <> ifNewtypes (ifPrivate i) 183 | i <- map lmInterface (getLoadedModules (meLoadedModules menv)) 184 ] 185 186-- | Are any parameterized modules loaded? 187hasParamModules :: ModuleEnv -> Bool 188hasParamModules = not . null . lmLoadedParamModules . meLoadedModules 189 190allDeclGroups :: ModuleEnv -> [T.DeclGroup] 191allDeclGroups = concatMap T.mDecls . loadedNonParamModules 192 193-- | Contains enough information to browse what's in scope, 194-- or type check new expressions. 195data ModContext = ModContext 196 { mctxParams :: IfaceParams 197 , mctxDecls :: IfaceDecls 198 , mctxNames :: R.NamingEnv 199 , mctxNameDisp :: NameDisp 200 , mctxTypeProvenace :: Map Name DeclProvenance 201 , mctxValueProvenance :: Map Name DeclProvenance 202 } 203 204-- | Specifies how a declared name came to be in scope. 205data DeclProvenance = 206 NameIsImportedFrom ModName 207 | NameIsLocalPublic 208 | NameIsLocalPrivate 209 | NameIsParameter 210 | NameIsDynamicDecl 211 deriving (Eq,Ord) 212 213 214-- | Given the state of the environment, compute information about what's 215-- in scope on the REPL. This includes what's in the focused module, plus any 216-- additional definitions from the REPL (e.g., let bound names, and @it@). 217focusedEnv :: ModuleEnv -> ModContext 218focusedEnv me = 219 ModContext 220 { mctxParams = parameters 221 , mctxDecls = mconcat (dynDecls : localDecls : importedDecls) 222 , mctxNames = namingEnv 223 , mctxNameDisp = R.toNameDisp namingEnv 224 , mctxTypeProvenace = fst provenance 225 , mctxValueProvenance = snd provenance 226 } 227 228 where 229 (importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports) 230 localDecls = publicDecls `mappend` privateDecls 231 localNames = R.unqualifiedEnv localDecls `mappend` 232 R.modParamsNamingEnv parameters 233 dynDecls = deIfaceDecls (meDynEnv me) 234 dynNames = deNames (meDynEnv me) 235 236 namingEnv = dynNames `R.shadowing` 237 localNames `R.shadowing` 238 mconcat importedNames 239 240 provenance = shadowProvs 241 $ declsProv NameIsDynamicDecl dynDecls 242 : declsProv NameIsLocalPublic publicDecls 243 : declsProv NameIsLocalPrivate privateDecls 244 : paramProv parameters 245 : importedProvs 246 247 (imports, parameters, publicDecls, privateDecls) = 248 case meFocusedModule me of 249 Nothing -> (mempty, noIfaceParams, mempty, mempty) 250 Just fm -> 251 case lookupModule fm me of 252 Just lm -> 253 let Iface { .. } = lmInterface lm 254 in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate) 255 Nothing -> panic "focusedEnv" ["Focused module is not loaded."] 256 257 loadImport imp = 258 case lookupModule (iModule imp) me of 259 Just lm -> 260 let decls = ifPublic (lmInterface lm) 261 in ( R.interpImport imp decls 262 , decls 263 , declsProv (NameIsImportedFrom (iModule imp)) decls 264 ) 265 Nothing -> panic "focusedEnv" 266 [ "Missing imported module: " ++ show (pp (iModule imp)) ] 267 268 269 -- earlier ones shadow 270 shadowProvs ps = let (tss,vss) = unzip ps 271 in (Map.unions tss, Map.unions vss) 272 273 paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns) 274 where doMap mp = const NameIsParameter <$> mp 275 276 declsProv prov IfaceDecls { .. } = 277 ( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ] 278 , doMap ifDecls 279 ) 280 where doMap mp = const prov <$> mp 281 282 283-- Loaded Modules -------------------------------------------------------------- 284 285-- | The location of a module 286data ModulePath = InFile FilePath 287 | InMem String ByteString -- ^ Label, content 288 deriving (Show, Generic, NFData) 289 290-- | In-memory things are compared by label. 291instance Eq ModulePath where 292 p1 == p2 = 293 case (p1,p2) of 294 (InFile x, InFile y) -> x == y 295 (InMem a _, InMem b _) -> a == b 296 _ -> False 297 298instance PP ModulePath where 299 ppPrec _ e = 300 case e of 301 InFile p -> text p 302 InMem l _ -> parens (text l) 303 304 305 306-- | The name of the content---either the file path, or the provided label. 307modulePathLabel :: ModulePath -> String 308modulePathLabel p = 309 case p of 310 InFile path -> path 311 InMem lab _ -> lab 312 313 314 315data LoadedModules = LoadedModules 316 { lmLoadedModules :: [LoadedModule] 317 -- ^ Invariants: 318 -- 1) All the dependencies of any module `m` must precede `m` in the list. 319 -- 2) Does not contain any parameterized modules. 320 321 , lmLoadedParamModules :: [LoadedModule] 322 -- ^ Loaded parameterized modules. 323 324 } deriving (Show, Generic, NFData) 325 326getLoadedModules :: LoadedModules -> [LoadedModule] 327getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x 328 329instance Semigroup LoadedModules where 330 l <> r = LoadedModules 331 { lmLoadedModules = List.unionBy ((==) `on` lmName) 332 (lmLoadedModules l) (lmLoadedModules r) 333 , lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r } 334 335instance Monoid LoadedModules where 336 mempty = LoadedModules { lmLoadedModules = [] 337 , lmLoadedParamModules = [] 338 } 339 mappend l r = l <> r 340 341data LoadedModule = LoadedModule 342 { lmName :: ModName 343 -- ^ The name of this module. Should match what's in 'lmModule' 344 345 , lmFilePath :: ModulePath 346 -- ^ The file path used to load this module (may not be canonical) 347 348 , lmModuleId :: String 349 -- ^ An identifier used to identify the source of the bytes for the module. 350 -- For files we just use the cononical path, for in memory things we 351 -- use their label. 352 353 , lmInterface :: Iface 354 -- ^ The module's interface. This is for convenient. At the moment 355 -- we have the whole module in 'lmModule', so this could be computer. 356 357 , lmModule :: T.Module 358 -- ^ The actual type-checked module 359 360 , lmFingerprint :: Fingerprint 361 } deriving (Show, Generic, NFData) 362 363-- | Has this module been loaded already. 364isLoaded :: ModName -> LoadedModules -> Bool 365isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm) 366 367-- | Is this a loaded parameterized module. 368isLoadedParamMod :: ModName -> LoadedModules -> Bool 369isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln) 370 371-- | Try to find a previously loaded module 372lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule 373lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules 374 where 375 search how = List.find ((mn ==) . lmName) (how (meLoadedModules me)) 376 377 378-- | Add a freshly loaded module. If it was previously loaded, then 379-- the new version is ignored. 380addLoadedModule :: 381 ModulePath -> String -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules 382addLoadedModule path ident fp tm lm 383 | isLoaded (T.mName tm) lm = lm 384 | T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded : 385 lmLoadedParamModules lm } 386 | otherwise = lm { lmLoadedModules = 387 lmLoadedModules lm ++ [loaded] } 388 where 389 loaded = LoadedModule 390 { lmName = T.mName tm 391 , lmFilePath = path 392 , lmModuleId = ident 393 , lmInterface = genIface tm 394 , lmModule = tm 395 , lmFingerprint = fp 396 } 397 398-- | Remove a previously loaded module. 399-- Note that this removes exactly the modules specified by the predicate. 400-- One should be carfule to preserve the invariant on 'LoadedModules'. 401removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules 402removeLoadedModule rm lm = 403 LoadedModules 404 { lmLoadedModules = filter (not . rm) (lmLoadedModules lm) 405 , lmLoadedParamModules = filter (not . rm) (lmLoadedParamModules lm) 406 } 407 408-- Dynamic Environments -------------------------------------------------------- 409 410-- | Extra information we need to carry around to dynamically extend 411-- an environment outside the context of a single module. Particularly 412-- useful when dealing with interactive declarations as in @let@ or 413-- @it@. 414data DynamicEnv = DEnv 415 { deNames :: R.NamingEnv 416 , deDecls :: [T.DeclGroup] 417 , deEnv :: EvalEnv 418 } deriving Generic 419 420instance Semigroup DynamicEnv where 421 de1 <> de2 = DEnv 422 { deNames = deNames de1 <> deNames de2 423 , deDecls = deDecls de1 <> deDecls de2 424 , deEnv = deEnv de1 <> deEnv de2 425 } 426 427instance Monoid DynamicEnv where 428 mempty = DEnv 429 { deNames = mempty 430 , deDecls = mempty 431 , deEnv = mempty 432 } 433 mappend de1 de2 = de1 <> de2 434 435-- | Build 'IfaceDecls' that correspond to all of the bindings in the 436-- dynamic environment. 437-- 438-- XXX: if we ever add type synonyms or newtypes at the REPL, revisit 439-- this. 440deIfaceDecls :: DynamicEnv -> IfaceDecls 441deIfaceDecls DEnv { deDecls = dgs } = 442 mconcat [ IfaceDecls 443 { ifTySyns = Map.empty 444 , ifNewtypes = Map.empty 445 , ifAbstractTypes = Map.empty 446 , ifDecls = Map.singleton (ifDeclName ifd) ifd 447 } 448 | decl <- concatMap T.groupDecls dgs 449 , let ifd = mkIfaceDecl decl 450 ] 451