Add implicit imports for locally defined modules

This also fixes the extra space in the "invlid dependency" error

src/Cryptol/ModuleSystem/Renamer.hs

@@ -29,7 +29,7 @@ import Prelude ()
 import Prelude.Compat
 
 import Data.Either(partitionEithers)
-import Data.Maybe(fromJust,mapMaybe)
+import Data.Maybe(fromJust)
 import Data.List(find,foldl')
 import Data.Foldable(toList)
 import Data.Map.Strict(Map)
@@ -48,7 +48,7 @@ import Cryptol.Parser.AST
 import Cryptol.Parser.Selector(selName)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.RecordMap
-import Cryptol.Utils.Ident(allNamespaces,textToModName)
+import Cryptol.Utils.Ident(allNamespaces,packModName)
 
 import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Renamer.Error
@@ -57,7 +57,7 @@ import Cryptol.ModuleSystem.Renamer.Monad
 
 renameModule :: Module PName -> RenameM (IfaceDecls,NamingEnv,Module Name)
 renameModule m0 =
-  do let m = m0 { mDecls = addImplicitNestedImports (mDecls m0) }
+  do let m = m0 { mDecls = snd (addImplicitNestedImports (mDecls m0)) }
      env      <- liftSupply (defsOf m)
      nested   <- liftSupply (collectNestedModules env m)
      setNestedModule (nestedModuleNames nested)
@@ -68,7 +68,7 @@ renameModule m0 =
 renameTopDecls ::
   ModName -> [TopDecl PName] -> RenameM (NamingEnv,[TopDecl Name])
 renameTopDecls m ds0 =
-  do let ds = addImplicitNestedImports ds0
+  do let ds = snd (addImplicitNestedImports ds0)
      let mpath = TopModule m
      env    <- liftSupply (defsOf (map (InModule (Just mpath)) ds))
      nested <- liftSupply (collectNestedModulesDecls env m ds)
@@ -79,30 +79,44 @@ renameTopDecls m ds0 =
           pure (env,ds1)
 
 
--- XXX: add implicit imports to the nested modules too
--- XXX: also add imports for exported nested modules
-addImplicitNestedImports :: [TopDecl PName] -> [TopDecl PName]
-addImplicitNestedImports decls = mapMaybe addImp mods ++ decls
+-- | Returns declarations with additional imports and the public module names
+-- of this module and its children
+addImplicitNestedImports ::
+  [TopDecl PName] -> ([[Ident]], [TopDecl PName])
+addImplicitNestedImports decls = (concat exportedMods, concat newDecls ++ other)
   where
-  (imps,mods) = foldr modsOrImp (Set.empty, []) decls
-  addImp m
-    | mname `Set.member` imps = Nothing
-    | otherwise = Just $ DImport m { thing = Import
-                                               { iModule = ImpNested mname
-                                               , iAs     = Just qualName
-                                               , iSpec   = Nothing
-                                               }
-                                    }
-    where
-    mname    = thing m
-    qualName = textToModName (identText (getIdent mname))
+  (mods,other)            = foldr classify ([], []) decls
+  (newDecls,exportedMods) = unzip (map processModule mods)
+  processModule m =
+    let NestedModule m1 = tlValue m
+        (childExs, ds1) = addImplicitNestedImports (mDecls m1)
+        mname           = getIdent (thing (mName m1))
+        imps            = map (mname :) ([] : childExs)
+        isToName is     = case is of
+                            [i] -> mkUnqual i
+                            _   -> mkQual (isToQual (init is)) (last is)
+        isToQual is     = packModName (map identText is)
+        mkImp xs        = DImport
+                          Located
+                            { srcRange = srcRange (mName m1)
+                            , thing = Import
+                                        { iModule = ImpNested (isToName xs)
+                                        , iAs     = Just (isToQual xs)
+                                        , iSpec   = Nothing
+                                        }
+                            }
+    in ( DModule m { tlValue = NestedModule m1 { mDecls = ds1 } }
+       : map mkImp imps
+       , case tlExport m of
+           Public  -> imps
+           Private -> []
+       )
 
-  modsOrImp d (is,ms) =
+
+  classify d (ms,ds) =
     case d of
-      DImport li | ImpNested i <- iModule (thing li) -> (Set.insert i is, ms)
-      DModule tl | NestedModule m <- tlValue tl -> (is, mName m : ms)
-      _  -> (is, ms)
-  
+      DModule tl -> (tl : ms, ds)
+      _          -> (ms, d : ds)
 
 
 nestedModuleNames :: NestedMods -> Map ModPath Name

src/Cryptol/ModuleSystem/Renamer/Error.hs

@@ -140,7 +140,7 @@ instance PP RenamerError where
 
     InvalidDependency ds ->
       "[error] Invalid recursive dependency:"
-      $$ nest 4 (vcat [ "•" <+> pp x <+> ", defined at" <+> ppR (depNameLoc x)
+      $$ nest 4 (vcat [ "•" <+> pp x <.> ", defined at" <+> ppR (depNameLoc x)
                       | x <- ds ])
       where ppR r = pp (from r) <.> "--" <.> pp (to r)
 

tests/issues/issue1040.icry.stdout

@@ -3,4 +3,4 @@ Loading module Cryptol
 Loading module binarytree
 
 [error] Invalid recursive dependency:
-    • type binarytree::Tree , defined at 3:9--3:13
+    • type binarytree::Tree, defined at 3:9--3:13

tests/modsys/nested/T14.cry

@@ -0,0 +1,20 @@
+module T14 where
+
+submodule A where
+  x = 0x1
+
+  submodule B where
+    y = 0x2
+
+    submodule C where
+      z = 0x3
+
+import submodule A::B
+import submodule C as D
+
+output = { ex1 = A::x
+         , ex2 = A::B::y
+         , ex3 = A::B::C::z
+         , ex4 = y
+         , ex5 = D::z
+         }

tests/modsys/nested/T14.icry

@@ -0,0 +1,2 @@
+:load T14.cry
+output

tests/modsys/nested/T14.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T14
+{ex1 = 0x1, ex2 = 0x2, ex3 = 0x3, ex4 = 0x2, ex5 = 0x3}

tests/modsys/nested/T15.cry

@@ -0,0 +1,12 @@
+module T15 where
+
+submodule A where
+  x = 1
+  submodule A where
+    y = 2
+    submodule A where
+      z = 3
+
+import submodule A::A
+
+out = y

tests/modsys/nested/T15.icry

@@ -0,0 +1,2 @@
+:load T15.cry
+out

tests/modsys/nested/T15.icry.stdout

@@ -0,0 +1,15 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T15
+[warning] at T15.cry:5:13--5:14
+    This binding for `A` shadows the existing binding at
+    T15.cry:3:11--3:12
+[warning] at T15.cry:7:15--7:16
+    This binding for `A` shadows the existing binding at
+    T15.cry:5:13--5:14
+[warning] at T15.cry:7:15--7:16
+    This binding for `A::A` shadows the existing binding at
+    T15.cry:5:13--5:14
+Showing a specific instance of polymorphic result:
+  * Using 'Integer' for 1st type argument of 'T15::A::A::y'
+2

tests/modsys/nested/T3.icry.stdout

@@ -3,5 +3,5 @@ Loading module Cryptol
 Loading module T3
 
 [error] Invalid recursive dependency:
-    • T3::x , defined at 4:1--4:2
-    • submodule T3::A , defined at 6:11--6:12
+    • submodule T3::A, defined at 6:11--6:12
+    • T3::x, defined at 4:1--4:2

tests/modsys/nested/T8.icry.stdout

@@ -3,5 +3,5 @@ Loading module Cryptol
 Loading module T9
 
 [error] Invalid recursive dependency:
-    • T9::x , defined at 3:1--3:2
-    • submodule T9::A , defined at 5:11--5:12
+    • submodule T9::A, defined at 5:11--5:12
+    • T9::x, defined at 3:1--3:2

tests/regression/tc-errors.icry.stdout

@@ -52,7 +52,7 @@ Loading module Cryptol
 Loading module Main
 
 [error] Invalid recursive dependency:
-    • type Main::T , defined at 1:6--1:7
+    • type Main::T, defined at 1:6--1:7
 Loading module Cryptol
 Loading module Main