Skip to content

Commit

Permalink
Remove filter as that wasn't root cause issue, change module environm…
Browse files Browse the repository at this point in the history
…ent to only grab public IfaceDecls.
  • Loading branch information
mccleeary-galois committed Mar 14, 2024
1 parent 6c3bcc5 commit 9512396
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 19 deletions.
43 changes: 25 additions & 18 deletions src/Cryptol/ModuleSystem/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@
{-# LANGUAGE RankNTypes #-}
module Cryptol.ModuleSystem.Env where

#ifndef RELOCATABLE

import Paths_cryptol (getDataDir)
#endif


import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc, getForeignSrcPath)
import Cryptol.Eval (EvalEnv)
Expand Down Expand Up @@ -122,11 +122,11 @@ data EvalForeignPolicy

defaultEvalForeignPolicy :: EvalForeignPolicy
defaultEvalForeignPolicy =
#ifdef FFI_ENABLED
PreferEvalForeign
#else



NeverEvalForeign
#endif


resetModuleEnv :: ModuleEnv -> IO ModuleEnv
resetModuleEnv env = do
Expand All @@ -145,9 +145,9 @@ resetModuleEnv env = do
initialModuleEnv :: IO ModuleEnv
initialModuleEnv = do
curDir <- getCurrentDirectory
#ifndef RELOCATABLE

dataDir <- getDataDir
#endif

binDir <- takeDirectory `fmap` getExecutablePath
let instDir = normalise . joinPath . init . splitPath $ binDir
-- looking up this directory can fail if no HOME is set, as in some
Expand All @@ -158,21 +158,21 @@ initialModuleEnv = do
let searchPath = [ curDir
-- something like $HOME/.cryptol
, userDir
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-- ../cryptol on win32
, instDir </> "cryptol"
#else




-- ../share/cryptol on others
, instDir </> "share" </> "cryptol"
#endif

#ifndef RELOCATABLE


-- Cabal-defined data directory. Since this
-- is usually a global location like
-- /usr/local, search this one last in case
-- someone has multiple Cryptols
, dataDir
#endif

]

return ModuleEnv
Expand Down Expand Up @@ -279,15 +279,16 @@ modContextOf mname me =
localNames = lmNamingEnv lm

-- XXX: do we want only public ones here?
loadedDecls = map (ifDefines . lmInterface)
loadedPublicDecls = map getPublicDecls
$ getLoadedModules (meLoadedModules me)


params = ifParams localIface
pure ModContext
{ mctxParams = if Map.null params then NoParams
else FunctorParams params
, mctxExported = ifsPublic (ifNames localIface)
, mctxDecls = mconcat (ifDefines localIface : loadedDecls)
, mctxDecls = mconcat (ifDefines localIface : loadedPublicDecls)
, mctxNames = localNames
, mctxNameDisp = R.toNameDisp localNames
}
Expand All @@ -304,7 +305,12 @@ modContextOf mname me =
, mctxNames = localNames
, mctxNameDisp = R.toNameDisp localNames
}

where getPublicDecls :: LoadedModule -> IfaceDecls
getPublicDecls lm = do
let allDecls = ifDefines . lmInterface $ lm
publicNames = ifsPublic . ifNames . lmInterface $ lm
publicDecls = filterIfaceDecls (`Set.member` publicNames) allDecls
publicDecls


dynModContext :: ModuleEnv -> ModContext
Expand Down Expand Up @@ -636,3 +642,4 @@ deIfaceDecls DEnv { deDecls = dgs, deTySyns = tySyns } =
| decl <- concatMap T.groupDecls dgs
, let ifd = T.mkIfaceDecl decl
]

2 changes: 1 addition & 1 deletion src/Cryptol/REPL/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -642,7 +642,7 @@ getTypeNames =
getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
getPropertyNames =
do fe <- getFocusedEnv
let xs = Map.filterWithKey (\n _ -> Set.member n (M.mctxExported fe)) (M.ifDecls (M.mctxDecls fe))
let xs = M.ifDecls (M.mctxDecls fe)
ps = sortBy (comparing (from . M.nameLoc . fst))
[ (x,d) | (x,d) <- Map.toList xs,
T.PragmaProperty `elem` M.ifDeclPragmas d ]
Expand Down

0 comments on commit 9512396

Please sign in to comment.