Bug-fixes from code-review on 12 March 2021

src/Cryptol/ModuleSystem/Base.hs

@@ -523,7 +523,7 @@ typecheck act i params env = do
 
 -- | Generate input for the typechecker.
 genInferInput :: Range -> PrimMap -> IfaceParams -> IfaceDecls -> ModuleM T.InferInput
-genInferInput r prims params env = do
+genInferInput r prims params env' = do
   seeds <- getNameSeeds
   monoBinds <- getMonoBinds
   cfg <- getSolverConfig
@@ -533,6 +533,8 @@ genInferInput r prims params env = do
   callStacks <- getCallStacks
 
   -- TODO: include the environment needed by the module
+  let env = flatPublicDecls env'
+            -- XXX: we should really just pass this directly
   return T.InferInput
     { T.inpRange     = r
     , T.inpVars      = Map.map ifDeclSig (ifDecls env)

src/Cryptol/ModuleSystem/Interface.hs

@@ -23,6 +23,9 @@ module Cryptol.ModuleSystem.Interface (
   , emptyIface
   , ifacePrimMap
   , noIfaceParams
+  , ifaceIsFunctor
+  , flatPublicIface
+  , flatPublicDecls
   ) where
 
 import qualified Data.Map as Map
@@ -52,6 +55,25 @@ data IfaceG mname = Iface
   , ifParams    :: IfaceParams  -- ^ Uninterpreted constants (aka module params)
   } deriving (Show, Generic, NFData)
 
+ifaceIsFunctor :: IfaceG mname -> Bool
+ifaceIsFunctor = not . isEmptyIfaceParams . ifParams
+
+-- | The public declarations in all modules, including nested
+-- The modules field contains public functors
+-- Assumes that we are not a functor.
+flatPublicIface :: IfaceG mname -> IfaceDecls
+flatPublicIface iface = flatPublicDecls (ifPublic iface)
+
+
+flatPublicDecls :: IfaceDecls -> IfaceDecls
+flatPublicDecls ifs = mconcat ( ifs { ifModules = fun }
+                              : map flatPublicIface (Map.elems nofun)
+                              )
+
+  where
+  (fun,nofun) = Map.partition ifaceIsFunctor (ifModules ifs)
+
+
 type Iface = IfaceG ModName
 
 emptyIface :: mname -> IfaceG mname
@@ -75,6 +97,10 @@ noIfaceParams = IfaceParams
   , ifParamFuns = Map.empty
   }
 
+isEmptyIfaceParams :: IfaceParams -> Bool
+isEmptyIfaceParams IfaceParams { .. } =
+  Map.null ifParamTypes && null ifParamConstraints && Map.null ifParamFuns
+
 data IfaceDecls = IfaceDecls
   { ifTySyns        :: Map.Map Name IfaceTySyn
   , ifNewtypes      :: Map.Map Name IfaceNewtype
@@ -83,6 +109,7 @@ data IfaceDecls = IfaceDecls
   , ifModules       :: !(Map.Map Name (IfaceG Name))
   } deriving (Show, Generic, NFData)
 
+
 instance Semigroup IfaceDecls where
   l <> r = IfaceDecls
     { ifTySyns   = Map.union (ifTySyns l)   (ifTySyns r)

src/Cryptol/ModuleSystem/Renamer/Monad.hs

@@ -293,8 +293,9 @@ addDep :: Name -> RenameM ()
 addDep x =
   do cur  <- getCurMod
      deps <- case nameInfo x of
-               Declared m _ | cur /= m && cur `containsModule` m ->
-                 do mb <- nestedModuleOrig m
+               -- XXX: this should be the outermost thing
+               Declared m _ | Just (c,i:_) <- cur `containsModule` m ->
+                 do mb <- nestedModuleOrig (Nested c i)
                     pure case mb of
                            Just y  -> Set.fromList [x,y]
                            Nothing -> Set.singleton x

src/Cryptol/REPL/Command.hs

@@ -1212,7 +1212,7 @@ browseMods isVisible prov M.IfaceDecls { .. } names =
             , secVisible = isVisible
             }
   where
-  ppM m = pp (M.ifModName m)
+  ppM m = "submodule" <+> pp (M.ifModName m)
   -- XXX: can print a lot more information about the moduels, but
   -- might be better to do that with a separate command
 

src/Cryptol/Utils/Ident.hs

@@ -64,8 +64,9 @@ module Cryptol.Utils.Ident
   ) where
 
 import           Control.DeepSeq (NFData)
+import           Control.Monad(guard)
 import           Data.Char (isSpace)
-import           Data.List (unfoldr,isPrefixOf)
+import           Data.List (unfoldr)
 import qualified Data.Text as T
 import           Data.String (IsString(..))
 import           GHC.Generics (Generic)
@@ -97,8 +98,10 @@ topModuleFor m =
     TopModule x -> x
     Nested p _ -> topModuleFor p
 
-containsModule :: ModPath -> ModPath -> Bool
-p1 `containsModule` p2 = m1 == m2 && reverse xs `isPrefixOf` reverse ys
+containsModule :: ModPath -> ModPath -> Maybe (ModPath,[Ident])
+p1 `containsModule` p2 =
+  do guard (m1 == m2)
+     check (TopModule m1) (reverse xs) (reverse ys)
   where
   (m1,xs) = toList p1
   (m2,ys) = toList p2
@@ -109,6 +112,12 @@ p1 `containsModule` p2 = m1 == m2 && reverse xs `isPrefixOf` reverse ys
       Nested b i  -> (a, i:bs)
         where (a,bs) = toList b
 
+  check m is js =
+    case (is,js) of
+      ([], _) -> pure (m, js)
+      (i : is', j : js') -> guard (i == j) >> check (Nested m i) is' js'
+      _ -> Nothing
+
 
 
 --------------------------------------------------------------------------------

tests/modsys/nested/T10.cry

@@ -0,0 +1,8 @@
+module T6 where
+
+import T4 as X
+
+import submodule X::A
+
+f = y
+

tests/modsys/nested/T10.icry

@@ -0,0 +1,2 @@
+:load T10.cry
+f

tests/modsys/nested/T10.icry.stdout

@@ -0,0 +1,5 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T4
+Loading module T6
+0x02

tests/modsys/nested/T5.icry.stdout

@@ -9,7 +9,7 @@ Modules
   From T4
   -------
 
-    A
+    submodule A
 
 Symbols
 =======

tests/modsys/nested/T6.icry.stdout

@@ -8,7 +8,7 @@ Modules
   From T4
   -------
 
-    X::A
+    submodule X::A
 
 Symbols
 =======

tests/modsys/nested/T8.cry

@@ -0,0 +1,10 @@
+module T9 where
+
+x = y
+
+submodule A where
+  submodule B where
+    y = x
+
+import submodule A
+import submodule B

tests/modsys/nested/T8.icry

@@ -0,0 +1 @@
+:load T8.cry

tests/modsys/nested/T8.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T9
+
+[error] Invalid recursive dependency:
+    • T9::x
+    • submodule T9::A

tests/modsys/nested/T9.cry

@@ -0,0 +1,10 @@
+module T9 where
+
+x = y
+
+submodule A where
+  submodule B where
+    y = 2
+
+import submodule A
+import submodule B

tests/modsys/nested/T9.icry

@@ -0,0 +1,2 @@
+:load T9.cry
+x

tests/modsys/nested/T9.icry.stdout

@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module T9
+Showing a specific instance of polymorphic result:
+  * Using 'Integer' for 1st type argument of 'T9::A::B::y'
+2