Skip to content

Commit

Permalink
More information when browsing.
Browse files Browse the repository at this point in the history
This implements the feature request in #689
  • Loading branch information
yav committed Mar 24, 2020
1 parent ec36d1a commit fcc7a19
Show file tree
Hide file tree
Showing 7 changed files with 312 additions and 166 deletions.
22 changes: 10 additions & 12 deletions src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,15 @@

module Cryptol.ModuleSystem.Base where

import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
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.Value as E
Expand Down Expand Up @@ -313,21 +314,15 @@ loadDeps m =

-- Type Checking ---------------------------------------------------------------

-- | Load the local environment, which consists of the environment for the
-- currently opened module, shadowed by the dynamic environment.
getLocalEnv :: ModuleM (IfaceParams,IfaceDecls,R.NamingEnv)
getLocalEnv =
do (params,decls,fNames,_) <- getFocusedEnv
denv <- getDynEnv
let dynDecls = deIfaceDecls denv
return (params,dynDecls `mappend` decls, deNames denv `R.shadowing` fNames)

-- | 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 e = do

(params,decls,names) <- getLocalEnv
fe <- getFocusedEnv
let params = mctxParams fe
decls = mctxDecls fe
names = mctxNames fe

-- run NoPat
npe <- noPat e
Expand All @@ -348,7 +343,10 @@ checkExpr e = do
-- INVARIANT: This assumes that NoPat has already been run on the declarations.
checkDecls :: [P.TopDecl PName] -> ModuleM (R.NamingEnv,[T.DeclGroup])
checkDecls ds = do
(params,decls,names) <- getLocalEnv
fe <- getFocusedEnv
let params = mctxParams fe
decls = mctxDecls fe
names = mctxNames fe

-- introduce names for the declarations before renaming them
declsEnv <- liftSupply (R.namingEnv' (map (R.InModule interactiveName) ds))
Expand Down
145 changes: 103 additions & 42 deletions src/Cryptol/ModuleSystem/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import Paths_cryptol (getDataDir)
import Cryptol.Eval (EvalEnv)
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name (Supply,emptySupply)
import Cryptol.ModuleSystem.Name (Name,Supply,emptySupply)
import qualified Cryptol.ModuleSystem.NamingEnv as R
import Cryptol.Parser.AST
import qualified Cryptol.TypeCheck as T
Expand All @@ -31,8 +31,8 @@ import Data.ByteString(ByteString)
import Control.Monad (guard,mplus)
import qualified Control.Exception as X
import Data.Function (on)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe(fromMaybe)
import Data.Semigroup
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
import System.Environment(getExecutablePath)
Expand All @@ -45,6 +45,9 @@ import Control.DeepSeq
import Prelude ()
import Prelude.Compat

import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP(pp)

-- Module Environment ----------------------------------------------------------

-- | This is the current state of the interpreter.
Expand Down Expand Up @@ -178,47 +181,95 @@ hasParamModules :: ModuleEnv -> Bool
hasParamModules = not . null . lmLoadedParamModules . meLoadedModules


-- | Produce an ifaceDecls that represents the focused environment of the module
-- system, as well as a 'NameDisp' for pretty-printing names according to the
-- imports.
--
-- XXX This could really do with some better error handling, just returning
-- mempty when one of the imports fails isn't really desirable.
--
-- XXX: This is not quite right. For example, it does not take into
-- account *how* things were imported in a module (e.g., qualified).
-- It would be simpler to simply store the naming environment that was
-- actually used when we renamed the module.
focusedEnv :: ModuleEnv -> (IfaceParams,IfaceDecls,R.NamingEnv,NameDisp)

-- | Contains enough information to browse what's in scope,
-- or type check new expressions.
data ModContext = ModContext
{ mctxParams :: IfaceParams
, mctxDecls :: IfaceDecls
, mctxNames :: R.NamingEnv
, mctxNameDisp :: NameDisp
, mctxTypeProvenace :: Map Name DeclProvenance
, mctxValueProvenance :: Map Name DeclProvenance
}

-- | Specifies how a declared name came to be in scope.
data DeclProvenance =
NameIsImportedFrom ModName
| NameIsLocalPublic
| NameIsLocalPrivate
| NameIsParameter
| NameIsDynamicDecl
deriving (Eq,Ord)


-- | Given the state of the environment, compute information about what's
-- in scope on the REPL. This includes what's in the focused module, plus any
-- additional definitions from the REPL (e.g., let bound names, and @it@).
focusedEnv :: ModuleEnv -> ModContext
focusedEnv me =
fromMaybe (noIfaceParams, mempty, mempty, mempty) $
do fm <- meFocusedModule me
lm <- lookupModule fm me
deps <- mapM loadImport (T.mImports (lmModule lm))
let (ifaces,names) = unzip deps
Iface { .. } = lmInterface lm
localDecls = ifPublic `mappend` ifPrivate
localNames = R.unqualifiedEnv localDecls `mappend`
R.modParamsNamingEnv ifParams
namingEnv = localNames `R.shadowing` mconcat names

return ( ifParams
, mconcat (localDecls:ifaces)
, namingEnv
, R.toNameDisp namingEnv)
ModContext
{ mctxParams = parameters
, mctxDecls = mconcat (dynDecls : localDecls : importedDecls)
, mctxNames = namingEnv
, mctxNameDisp = R.toNameDisp namingEnv
, mctxTypeProvenace = fst provenance
, mctxValueProvenance = snd provenance
}

where
(importedNames,importedDecls,importedProvs) = unzip3 (map loadImport imports)
localDecls = publicDecls `mappend` privateDecls
localNames = R.unqualifiedEnv localDecls `mappend`
R.modParamsNamingEnv parameters
dynDecls = deIfaceDecls (meDynEnv me)
dynNames = deNames (meDynEnv me)

namingEnv = dynNames `R.shadowing`
localNames `R.shadowing`
mconcat importedNames

provenance = shadowProvs
$ declsProv NameIsDynamicDecl dynDecls
: declsProv NameIsLocalPublic publicDecls
: declsProv NameIsLocalPrivate privateDecls
: paramProv parameters
: importedProvs

(imports, parameters, publicDecls, privateDecls) =
case meFocusedModule me of
Nothing -> (mempty, noIfaceParams, mempty, mempty)
Just fm ->
case lookupModule fm me of
Just lm ->
let Iface { .. } = lmInterface lm
in (T.mImports (lmModule lm), ifParams, ifPublic, ifPrivate)
Nothing -> panic "focusedEnv" ["Focused module is not loaded."]

loadImport imp =
do lm <- lookupModule (iModule imp) me
let decls = ifPublic (lmInterface lm)
return (decls,R.interpImport imp decls)

-- | The unqualified declarations and name environment for the dynamic
-- environment.
dynamicEnv :: ModuleEnv -> (IfaceDecls,R.NamingEnv,NameDisp)
dynamicEnv me = (decls,names,R.toNameDisp names)
where
decls = deIfaceDecls (meDynEnv me)
names = R.unqualifiedEnv decls
case lookupModule (iModule imp) me of
Just lm ->
let decls = ifPublic (lmInterface lm)
in ( R.interpImport imp decls
, decls
, declsProv (NameIsImportedFrom (iModule imp)) decls
)
Nothing -> panic "focusedEnv"
[ "Missing imported module: " ++ show (pp (iModule imp)) ]


-- earlier ones shadow
shadowProvs ps = let (tss,vss) = unzip ps
in (Map.unions tss, Map.unions vss)

paramProv IfaceParams { .. } = (doMap ifParamTypes, doMap ifParamFuns)
where doMap mp = const NameIsParameter <$> mp

declsProv prov IfaceDecls { .. } =
( Map.unions [ doMap ifTySyns, doMap ifNewtypes, doMap ifAbstractTypes ]
, doMap ifDecls
)
where doMap mp = const prov <$> mp


-- Loaded Modules --------------------------------------------------------------
Expand Down Expand Up @@ -281,14 +332,23 @@ instance Monoid LoadedModules where

data LoadedModule = LoadedModule
{ lmName :: ModName
-- ^ The name of this module. Should match what's in 'lmModule'

, lmFilePath :: ModulePath
-- ^ The file path used to load this module (may not be canonical)

, lmModuleId :: String
-- ^ An identifier used to identify the source of the bytes for the module.
-- For files we just use the cononical path, for in memory things we
-- use their label.

, lmInterface :: Iface
-- ^ The module's interface. This is for convenient. At the moment
-- we have the whole module in 'lmModule', so this could be computer.

, lmModule :: T.Module
-- ^ The actual type-checked module

, lmFingerprint :: Fingerprint
} deriving (Show, Generic, NFData)

Expand Down Expand Up @@ -328,6 +388,8 @@ addLoadedModule path ident fp tm lm
}

-- | Remove a previously loaded module.
-- Note that this removes exactly the modules specified by the predicate.
-- One should be carfule to preserve the invariant on 'LoadedModules'.
removeLoadedModule :: (LoadedModule -> Bool) -> LoadedModules -> LoadedModules
removeLoadedModule rm lm =
LoadedModules
Expand All @@ -340,9 +402,8 @@ removeLoadedModule rm lm =

-- | Extra information we need to carry around to dynamically extend
-- an environment outside the context of a single module. Particularly
-- useful when dealing with interactive declarations as in @:let@ or
-- useful when dealing with interactive declarations as in @let@ or
-- @it@.

data DynamicEnv = DEnv
{ deNames :: R.NamingEnv
, deDecls :: [T.DeclGroup]
Expand Down
6 changes: 2 additions & 4 deletions src/Cryptol/ModuleSystem/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ import Cryptol.ModuleSystem.Env
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
import Cryptol.ModuleSystem.Renamer
(RenamerError(),RenamerWarning(),NamingEnv)
import Cryptol.ModuleSystem.Renamer (RenamerError(),RenamerWarning())
import qualified Cryptol.Parser as Parser
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position (Located)
Expand Down Expand Up @@ -508,8 +507,7 @@ withPrependedSearchPath fps m = ModuleT $ do
set $! env { meSearchPath = fps0 }
return x

-- XXX improve error handling here
getFocusedEnv :: ModuleM (IfaceParams,IfaceDecls,NamingEnv,NameDisp)
getFocusedEnv :: ModuleM ModContext
getFocusedEnv = ModuleT (focusedEnv `fmap` get)

getDynEnv :: ModuleM DynamicEnv
Expand Down
Loading

0 comments on commit fcc7a19

Please sign in to comment.