Skip to content

Commit

Permalink
Only grab public IfaceDecls from other modules.
Browse files Browse the repository at this point in the history
  • Loading branch information
mccleeary-galois committed Mar 14, 2024
1 parent 5bbc3dc commit 5293c51
Show file tree
Hide file tree
Showing 5 changed files with 40 additions and 3 deletions.
11 changes: 8 additions & 3 deletions src/Cryptol/ModuleSystem/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -278,16 +278,15 @@ modContextOf mname me =
let localIface = lmInterface lm
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,6 +303,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



Expand Down
5 changes: 5 additions & 0 deletions tests/issues/issue1621/a.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module a where

private

property x = True
3 changes: 3 additions & 0 deletions tests/issues/issue1621/b.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module b where

import a
7 changes: 7 additions & 0 deletions tests/issues/issue1621/issue1621.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
:m a
x
:m b
x
:check x
:check a::x
:check
17 changes: 17 additions & 0 deletions tests/issues/issue1621/issue1621.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
Loading module Cryptol
Loading module Cryptol
Loading module a
True
Loading module Cryptol
Loading module a
Loading module b

[error] at issue1621.icry:4:1--4:2
Value not in scope: x

[error] at issue1621.icry:5:8--5:9
Value not in scope: x

[error] at issue1621.icry:6:8--6:12
Value not in scope: a::x
There are no properties in scope.

0 comments on commit 5293c51

Please sign in to comment.