Merge pull request #1692 from GaloisInc/issue_1691

Fixes #1691 (and removes partial match warning)

CHANGES.md

@@ -1,10 +1,15 @@
 # next -- TBA
 
+## Language changes
+
+* Add implicit imports for non-anonymous modules defined by functor
+  instantiation.   For details, see #1691.
+
+
 ## Bug fixes
 
 * Fix #1685, which caused Cryptol to panic when given a local definition without
   a type signature that uses numeric constraint guards.
-
 # 3.1.0 -- 2024-02-05
 
 ## Language changes

src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs

@@ -33,8 +33,9 @@ module Cryptol.ModuleSystem.Renamer.ImplicitImports
 
 import Data.List(partition)
 
+import Cryptol.Utils.Ident(identIsNormal, packModName)
+import Cryptol.Utils.Panic(panic)
 import Cryptol.Parser.Position(Range)
-import Cryptol.Utils.Ident(packModName)
 import Cryptol.Parser.AST
 
 {- | Add additional imports for modules nested withing this one -}
@@ -56,25 +57,28 @@ addImplicitNestedImports' decls =
 
 
 processModule :: TopDecl PName -> ([TopDecl PName], [[Ident]])
-processModule ~dcl@(DModule m) =
-  let NestedModule m1 = tlValue m
-  in
-  case mDef m1 of
-    NormalModule ds ->
-      let (childExs, ds1) = addImplicitNestedImports' ds
+processModule dcl =
+  case dcl of
+    DModule m ->
+      let NestedModule m1 = tlValue m
           mname           = getIdent (thing (mName m1))
-          imps            = map (mname :) ([] : childExs) -- this & nested
           loc             = srcRange (mName m1)
-      in ( DModule m { tlValue = NestedModule m1 { mDef = NormalModule ds1 } }
-         : map (mkImp loc) imps
-         , case tlExport m of
-             Public  -> imps
-             Private -> []
-         )
-
-    FunctorInstance {} -> ([dcl], [])
-    InterfaceModule {} -> ([dcl], [])
+      in
+      case mDef m1 of
+        _ | not (identIsNormal mname) -> ([dcl],[])
+        NormalModule ds ->
+          let (childExs, ds1) = addImplicitNestedImports' ds
+              imps            = map (mname :) ([] : childExs) -- this & nested
+          in ( DModule m { tlValue = NestedModule m1 { mDef = NormalModule ds1 } }
+             : map (mkImp loc) imps
+             , case tlExport m of
+                 Public  -> imps
+                 Private -> []
+             )
 
+        FunctorInstance {} -> ([dcl, mkImp loc [mname]], [])
+        InterfaceModule {} -> ([dcl], [])
+    _ -> panic "processModule" ["Not a module"]
 
 
 
@@ -112,4 +116,3 @@ mkImp loc xs =
       }
 
 
-

src/Cryptol/Parser/ParserUtils.hs

@@ -1487,6 +1487,7 @@ desugarInstImport i inst =
   where
   imp = thing i
   iname = mkUnqual
+        $ identAnonIfaceMod
         $ mkIdent
         $ "import of " <> nm <> " at " <> Text.pack (show (pp (srcRange i)))
     where

src/Cryptol/Utils/Ident.hs

@@ -56,6 +56,7 @@ module Cryptol.Utils.Ident
   , modParamIdent
   , identAnonArg
   , identAnonIfaceMod
+  , identAnontInstImport
   , identIsNormal
 
     -- * Namespaces
@@ -169,18 +170,17 @@ instance NFData ModName
 modNameArg :: ModName -> ModName
 modNameArg (ModName m fl) =
   case fl of
-    NormalName        -> ModName m AnonModArgName
-    AnonModArgName    -> panic "modNameArg" ["Name is not normal"]
-    AnonIfaceModName  -> panic "modNameArg" ["Name is not normal"]
+    NormalName  -> ModName m AnonModArgName
+    _           -> panic "modNameArg" ["Name is not normal"]
+
 
 -- | Change a normal module name to a module name to be used for an
 -- anonnymous interface.
 modNameIfaceMod :: ModName -> ModName
 modNameIfaceMod (ModName m fl) =
   case fl of
     NormalName        -> ModName m AnonIfaceModName
-    AnonModArgName    -> panic "modNameIfaceMod" ["Name is not normal"]
-    AnonIfaceModName  -> panic "modNameIfaceMod" ["Name is not normal"]
+    _                 -> panic "modNameIfaceMod" ["Name is not normal"]
 
 -- | This is used when we check that the name of a module matches the
 -- file where it is defined.
@@ -351,6 +351,10 @@ identAnonArg (Ident b _ txt) = Ident b AnonModArgName txt
 identAnonIfaceMod :: Ident -> Ident
 identAnonIfaceMod (Ident b _ txt) = Ident b AnonIfaceModName txt
 
+-- | Make an anonymous identifier for an instantiation in an import.
+identAnontInstImport :: Ident -> Ident
+identAnontInstImport (Ident b _ txt) = Ident b AnonInstImport txt
+
 identIsNormal :: Ident -> Bool
 identIsNormal (Ident _ mb _) = isNormal mb
 
@@ -360,6 +364,7 @@ identIsNormal (Ident _ mb _) = isNormal mb
 data MaybeAnon = NormalName       -- ^ Not an anonymous name.
                | AnonModArgName   -- ^ Anonymous module (from `where`)
                | AnonIfaceModName -- ^ Anonymous interface (from `parameter`)
+               | AnonInstImport   -- ^ Anonymous instance import
   deriving (Eq,Ord,Show,Generic)
 
 instance NFData MaybeAnon
@@ -371,6 +376,7 @@ maybeAnonText mb txt =
     NormalName       -> txt
     AnonModArgName   -> "`where` argument of " <> txt
     AnonIfaceModName -> "`parameter` interface of " <> txt
+    AnonInstImport   -> txt
 
 isNormal :: MaybeAnon -> Bool
 isNormal mb =

tests/issues/issue1455_3.icry.stdout

@@ -18,14 +18,6 @@ a : [4]
 b : [8]
 c : [m]
 0x0d
-Submodules
-==========
-
-  From Inst3
-  ----------
-
-    import of F at issue1455/G.cry:5:1--5:9
-
 Type Synonyms
 =============
 
@@ -276,9 +268,3 @@ Symbols
     x : [4]
     y : [8]
 
-  From Inst3::import of F at issue1455/G.cry:5:1--5:9
-  ---------------------------------------------------
-
-    a : [4]
-    b : [8]
-

tests/issues/issue1455_3.icry.stdout.mingw32

@@ -18,14 +18,6 @@ a : [4]
 b : [8]
 c : [m]
 0x0d
-Submodules
-==========
-
-  From Inst3
-  ----------
-
-    import of F at issue1455\G.cry:5:1--5:9
-
 Type Synonyms
 =============
 
@@ -276,9 +268,3 @@ Symbols
     x : [4]
     y : [8]
 
-  From Inst3::import of F at issue1455\G.cry:5:1--5:9
-  ---------------------------------------------------
-
-    a : [4]
-    b : [8]
-

tests/issues/issue_1691.cry

@@ -0,0 +1,11 @@
+
+submodule A where
+  x = 2
+
+submodule F where
+  parameter
+    a: Integer
+
+  z = a + 2
+
+submodule B = submodule F where a = 3

tests/issues/issue_1691.icry

@@ -0,0 +1,2 @@
+:load issue_1691.cry
+:t B::z

tests/issues/issue_1691.icry.stdout

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