Merge pull request #1650 from GaloisInc/iss-1649

#1649
This commit is contained in:
mccleeary-galois 2024-04-01 09:57:19 -06:00 committed by GitHub
commit a849b974ca
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
12 changed files with 37 additions and 41 deletions

View File

@ -278,7 +278,8 @@ modContextOf mname me =
let localIface = lmInterface lm
localNames = lmNamingEnv lm
loadedPublicDecls = map getPublicDecls
-- XXX: do we want only public ones here?
loadedDecls = map (ifDefines . lmInterface)
$ getLoadedModules (meLoadedModules me)
params = ifParams localIface
@ -286,13 +287,14 @@ modContextOf mname me =
{ mctxParams = if Map.null params then NoParams
else FunctorParams params
, mctxExported = ifsPublic (ifNames localIface)
, mctxDecls = mconcat (ifDefines localIface : loadedPublicDecls)
, mctxDecls = mconcat (ifDefines localIface : loadedDecls)
, 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
@ -302,12 +304,6 @@ 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

View File

@ -772,7 +772,7 @@ lookupVar x =
Just a -> pure (ExtVar a)
Nothing ->
do mp <- IM $ asks iVars
panic "lookupVar" $ [ "Undefined vairable"
panic "lookupVar" $ [ "Undefined variable"
, show x
, "IVARS"
] ++ map (show . debugShowUniques . pp) (Map.keys mp)

View File

@ -1,5 +0,0 @@
module a where
private
property x = True

View File

@ -1,3 +0,0 @@
module b where
import a

View File

@ -1,7 +0,0 @@
:m a
x
:m b
x
:check x
:check a::x
:check

View File

@ -1,17 +0,0 @@
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.

View File

@ -0,0 +1,5 @@
// A.cry
module A where
submodule B = BFunctor where
type BTy = ()

View File

@ -0,0 +1,9 @@
// BFunctor.cry
module BFunctor where
import interface BInterface as BI
type BTy = BI::BTy
b : BTy -> ()
b _ = ()

View File

@ -0,0 +1,4 @@
// BInterface.cry
interface module BInterface where
type BTy : *

View File

@ -0,0 +1,5 @@
// Test.cry
module Test where
import A as A
import submodule A::B as B

View File

@ -0,0 +1,2 @@
:l Test.cry
B::b ()

View File

@ -0,0 +1,7 @@
Loading module Cryptol
Loading module Cryptol
Loading interface module BInterface
Loading module BFunctor
Loading module A
Loading module Test
()