Merge pull request #1698 from GaloisInc/issue_1691_2

Make fixes for 1691 work with more nested modules.
This commit is contained in:
Iavor S. Diatchki 2024-07-03 09:27:22 -07:00 committed by GitHub
commit 07bb442d7e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
4 changed files with 25 additions and 1 deletions

View File

@ -76,7 +76,13 @@ processModule dcl =
Private -> []
)
FunctorInstance {} -> ([dcl, mkImp loc [mname]], [])
FunctorInstance {} ->
let imps = [[mname]]
in ( dcl : map (mkImp loc) imps
, case tlExport m of
Public -> imps
Private -> []
)
InterfaceModule {} -> ([dcl], [])
_ -> panic "processModule" ["Not a module"]

View File

@ -0,0 +1,12 @@
submodule F where
parameter x: Integer
y = x + 1
submodule B = submodule F where x = 2
submodule M where
submodule A where
a = 2
submodule B = submodule F where x = 2

View File

@ -0,0 +1,2 @@
:load issue_1691_2.cry
:t M::B::y

View File

@ -0,0 +1,4 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
M::B::y : Integer