Merge pull request #1642 from GaloisInc/rem/iss-1621

Make it so only public IfaceDecls are loaded from other modules
GaloisInc · Mar 19, 2024 · 1e06a4b · 1e06a4b
2 parents c62c653 + 19ebc25
commit 1e06a4b
Show file tree

Hide file tree

Showing 5 changed files with 40 additions and 4 deletions.
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
@@ -278,23 +278,21 @@ 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
        }
   `mplus`
   do lm <- lookupSignature mname me
      let localNames  = lmNamingEnv lm
-         -- XXX: do we want only public ones here?
          loadedDecls = map (ifDefines . lmInterface)
                      $ getLoadedModules (meLoadedModules me)
      pure ModContext
@@ -304,6 +302,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
 
 
 

diff --git a/tests/issues/issue1621/a.cry b/tests/issues/issue1621/a.cry
@@ -0,0 +1,5 @@
+module a where
+
+private
+
+property x = True
diff --git a/tests/issues/issue1621/b.cry b/tests/issues/issue1621/b.cry
@@ -0,0 +1,3 @@
+module b where
+
+import a
diff --git a/tests/issues/issue1621/issue1621.icry b/tests/issues/issue1621/issue1621.icry
@@ -0,0 +1,7 @@
+:m a
+x
+:m b
+x
+:check x
+:check a::x
+:check
diff --git a/tests/issues/issue1621/issue1621.icry.stdout b/tests/issues/issue1621/issue1621.icry.stdout
@@ -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.