Allow loading interfaces.

When loaded an interface is treated like an empty functor.
Adding this capability would also be useful if we generalize
interfaces to allow for definitions, as discussed in #1457

This also fixes #1456

src/Cryptol/ModuleSystem/Base.hs

@@ -51,7 +51,7 @@ import Cryptol.ModuleSystem.Env ( lookupModule
                                 , lookupTCEntity
                                 , LoadedModuleG(..), lmInterface
                                 , meCoreLint, CoreLint(..)
-                                , ModContext(..)
+                                , ModContext(..), ModContextParams(..)
                                 , ModulePath(..), modulePathLabel)
 import           Cryptol.Backend.FFI
 import qualified Cryptol.Eval                 as E
@@ -544,7 +544,7 @@ checkModule isrc m = do
                      , tcPrims  = prims }
 
 
-  tcm <- typecheck act (R.rmModule renMod) mempty (R.rmImported renMod)
+  tcm <- typecheck act (R.rmModule renMod) NoParams (R.rmImported renMod)
 
   rewMod <- case tcm of
               T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)
@@ -611,7 +611,7 @@ data TCAction i o = TCAction
 
 typecheck ::
   (Show i, Show o, HasLoc i) =>
-  TCAction i o -> i -> T.FunctorParams -> IfaceDecls -> ModuleM o
+  TCAction i o -> i -> ModContextParams -> IfaceDecls -> ModuleM o
 typecheck act i params env = do
 
   let range = fromMaybe emptyRange (getLoc i)
@@ -643,7 +643,7 @@ typecheck act i params env = do
          typeCheckingFailed nameMap errs
 
 -- | Generate input for the typechecker.
-genInferInput :: Range -> PrimMap -> T.FunctorParams -> IfaceDecls ->
+genInferInput :: Range -> PrimMap -> ModContextParams -> IfaceDecls ->
                                                           ModuleM T.InferInput
 genInferInput r prims params env = do
   seeds <- getNameSeeds
@@ -668,7 +668,10 @@ genInferInput r prims params env = do
     , T.inpCallStacks       = callStacks
     , T.inpSearchPath       = searchPath
     , T.inpSupply           = supply
-    , T.inpParams           = params
+    , T.inpParams           = case params of
+                                NoParams -> T.allParamNames mempty
+                                FunctorParams ps -> T.allParamNames ps
+                                InterfaceParams ps -> ps
     , T.inpPrimNames        = prims
     , T.inpSolver           = solver
     , T.inpTopModules       = topMods

src/Cryptol/ModuleSystem/Env.hs

@@ -193,10 +193,15 @@ hasParamModules = not . null . lmLoadedParamModules . meLoadedModules
 allDeclGroups :: ModuleEnv -> [T.DeclGroup]
 allDeclGroups = concatMap T.mDecls . loadedNonParamModules
 
+data ModContextParams =
+    InterfaceParams T.ModParamNames
+  | FunctorParams T.FunctorParams
+  | NoParams
+
 -- | Contains enough information to browse what's in scope,
 -- or type check new expressions.
 data ModContext = ModContext
-  { mctxParams          :: T.FunctorParams
+  { mctxParams          :: ModContextParams -- T.FunctorParams
   , mctxExported        :: Set Name
   , mctxDecls           :: IfaceDecls
     -- ^ Should contain at least names in NamingEnv, but may have more
@@ -208,7 +213,7 @@ data ModContext = ModContext
 -- This instance is a bit bogus.  It is mostly used to add the dynamic
 -- environemnt to an existing module, and it makes sense for that use case.
 instance Semigroup ModContext where
-  x <> y = ModContext { mctxParams   = mctxParams x <> mctxParams y
+  x <> y = ModContext { mctxParams   = jnPs (mctxParams x) (mctxParams y)
                       , mctxExported = mctxExported x <> mctxExported y
                       , mctxDecls    = mctxDecls x  <> mctxDecls  y
                       , mctxNames    = names
@@ -217,9 +222,15 @@ instance Semigroup ModContext where
 
       where
       names = mctxNames x `R.shadowing` mctxNames y
+      jnPs as bs =
+        case (as,bs) of
+          (NoParams,_) -> bs
+          (_,NoParams) -> as
+          (FunctorParams xs, FunctorParams ys) -> FunctorParams (xs <> ys)
+          _ -> panic "(<>) @ ModContext" ["Can't combine parameters"]
 
 instance Monoid ModContext where
-  mempty = ModContext { mctxParams   = mempty
+  mempty = ModContext { mctxParams   = NoParams
                       , mctxDecls    = mempty
                       , mctxExported = mempty
                       , mctxNames    = mempty
@@ -237,13 +248,31 @@ modContextOf mname me =
          -- XXX: do we want only public ones here?
          loadedDecls = map (ifDefines . lmInterface)
                      $ getLoadedModules (meLoadedModules me)
+
+         params = ifParams localIface
      pure ModContext
-       { mctxParams   = ifParams localIface
+       { mctxParams   = if Map.null params then NoParams
+                                           else FunctorParams params
        , mctxExported = ifsPublic (ifNames localIface)
        , 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
+       { mctxParams   = InterfaceParams (lmData lm)
+       , mctxExported = Set.empty
+       , mctxDecls    = mconcat loadedDecls
+       , mctxNames    = localNames
+       , mctxNameDisp = R.toNameDisp localNames
+       }
+
+
 
 dynModContext :: ModuleEnv -> ModContext
 dynModContext me = mempty { mctxNames    = dynNames
@@ -396,6 +425,10 @@ isLoaded mn lm = mn `Set.member` getLoadedNames lm
 isLoadedParamMod :: ModName -> LoadedModules -> Bool
 isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln)
 
+-- | Is this a loaded interface module.
+isLoadedInterface :: ModName -> LoadedModules -> Bool
+isLoadedInterface mn ln = any ((mn ==) . lmName) (lmLoadedSignatures ln)
+
 
 
 lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG T.TCTopEntity)

src/Cryptol/REPL/Browse.hs

@@ -15,7 +15,7 @@ import qualified Cryptol.TypeCheck.Type as T
 import Cryptol.Utils.PP
 import Cryptol.Utils.Ident (OrigName(..), modPathIsNormal, identIsNormal)
 
-import Cryptol.ModuleSystem.Env(ModContext(..))
+import Cryptol.ModuleSystem.Env(ModContext(..),ModContextParams(..))
 import Cryptol.ModuleSystem.NamingEnv(namingEnvNames)
 import Cryptol.ModuleSystem.Name
 import Cryptol.ModuleSystem.Interface
@@ -54,10 +54,11 @@ data DispInfo = DispInfo { dispHow :: BrowseHow, env :: NameDisp }
 --------------------------------------------------------------------------------
 
 
-browseMParams :: NameDisp -> T.FunctorParams -> [Doc]
-browseMParams disp params
-  | Map.null params = []
-  | otherwise =
+browseMParams :: NameDisp -> ModContextParams -> [Doc]
+browseMParams disp pars =
+  case pars of
+    NoParams -> []
+    FunctorParams params ->
       ppSectionHeading "Module Parameters"
       $ [ "parameter" <+> pp (T.mpName p) <+> ":" <+>
           "interface" <+> pp (T.mpSignature p) $$
@@ -69,6 +70,7 @@ browseMParams disp params
         , let names = T.mpParameters p
         ] ++
         ["   "]
+    InterfaceParams ps -> [pp ps] -- XXX
   where
   ppParamTy p = nest 2 (sep ["type", pp (T.mtpName p) <+> ":", pp (T.mtpKind p)])
   ppParamFu p = nest 2 (sep [pp (T.mvpName p) <+> ":", pp (T.mvpType p)])

src/Cryptol/REPL/Command.hs

@@ -1214,13 +1214,10 @@ loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL ()
 loadHelper how =
   do clearLoadedMod
      (path,ent) <- liftModuleCmd how
-     m <- case ent of
-            T.TCTopModule mo -> pure mo
-            T.TCTopSignature {} -> raise CannotLoadASignature
 
-     whenDebug (rPutStrLn (dump m))
+     whenDebug (rPutStrLn (dump ent))
      setLoadedMod LoadedModule
-        { lName = Just (T.mName m)
+        { lName = Just (T.tcTopEntitytName ent)
         , lPath = path
         }
      -- after a successful load, the current module becomes the edit target

src/Cryptol/REPL/Help.hs

@@ -226,8 +226,9 @@ showSummary k name doc info =
 
 
 
-showTypeHelp :: T.FunctorParams -> M.IfaceDecls -> NameDisp -> T.Name -> REPL ()
-showTypeHelp fparams env nameEnv name =
+showTypeHelp ::
+  M.ModContextParams -> M.IfaceDecls -> NameDisp -> T.Name -> REPL ()
+showTypeHelp ctxparams env nameEnv name =
   fromMaybe (noInfo nameEnv name) $
   msum [ fromTySyn, fromPrimType, fromNewtype, fromTyParam ]
 
@@ -263,15 +264,21 @@ showTypeHelp fparams env nameEnv name =
                  doShowDocString (T.atDoc a)
 
   allParamNames =
-    Map.unions
-      [ (\x -> (p,x)) <$> T.mpnTypes (T.mpParameters ps)
-      | (p, ps) <- Map.toList fparams
-      ]
+    case ctxparams of
+      M.NoParams -> mempty
+      M.FunctorParams fparams ->
+        Map.unions
+          [ (\x -> (Just p,x)) <$> T.mpnTypes (T.mpParameters ps)
+          | (p, ps) <- Map.toList fparams
+          ]
+      M.InterfaceParams ps -> (\x -> (Nothing ,x)) <$> T.mpnTypes ps
 
   fromTyParam =
     do (x,p) <- Map.lookup name allParamNames
        pure do rPutStrLn ""
-               doShowParameterSource x
+               case x of
+                  Just src -> doShowParameterSource src
+                  Nothing  -> pure ()
                let ty = "type" <+> pp name <+> ":" <+> pp (T.mtpKind p)
                rPrint (runDoc nameEnv (indent 4 ty))
                doShowDocString (T.mtpDoc p)
@@ -286,9 +293,9 @@ doShowTyHelp nameEnv decl doc =
 
 
 showValHelp ::
-  T.FunctorParams -> M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL ()
+  M.ModContextParams -> M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL ()
 
-showValHelp fparams env nameEnv qname name =
+showValHelp ctxparams env nameEnv qname name =
   fromMaybe (noInfo nameEnv name)
             (msum [ fromDecl, fromNewtype, fromParameter ])
   where
@@ -316,15 +323,21 @@ showValHelp fparams env nameEnv qname name =
        return $ return ()
 
   allParamNames =
-    Map.unions
-      [ (\x -> (p,x)) <$> T.mpnFuns (T.mpParameters ps)
-      | (p, ps) <- Map.toList fparams
-      ]
+    case ctxparams of
+      M.NoParams -> mempty
+      M.FunctorParams fparams ->
+        Map.unions
+          [ (\x -> (Just p,x)) <$> T.mpnFuns (T.mpParameters ps)
+          | (p, ps) <- Map.toList fparams
+          ]
+      M.InterfaceParams ps -> (\x -> (Nothing,x)) <$> T.mpnFuns ps
 
   fromParameter =
     do (x,p) <- Map.lookup name allParamNames
        pure do rPutStrLn ""
-               doShowParameterSource x
+               case x of
+                 Just src -> doShowParameterSource src
+                 Nothing -> pure ()
                let ty = pp name <+> ":" <+> pp (T.mvpType p)
                rPrint (runDoc nameEnv (indent 4 ty))
                doShowFix (T.mvpFixity p)

src/Cryptol/REPL/Monad.hs

@@ -225,10 +225,11 @@ mkPrompt rw
     case lName =<< eLoadedMod rw of
       Nothing -> show (pp I.preludeName)
       Just m
-        | M.isLoadedParamMod m (M.meLoadedModules (eModuleEnv rw)) ->
-                 modName ++ "(parameterized)"
+        | M.isLoadedParamMod m loaded -> modName ++ "(parameterized)"
+        | M.isLoadedInterface m loaded -> modName ++ "(interface)"
         | otherwise -> modName
         where modName = pretty m
+              loaded = M.meLoadedModules (eModuleEnv rw)
 
   withFocus =
     case eLoadedMod rw of
@@ -329,7 +330,6 @@ data REPLException
   | TooWide WordTooWide
   | Unsupported Unsupported
   | ModuleSystemError NameDisp M.ModuleError
-  | CannotLoadASignature
   | EvalPolyError T.Schema
   | InstantiationsNotFound T.Schema
   | TypeNotTestable T.Type
@@ -372,7 +372,6 @@ instance PP REPLException where
     SBVException e       -> text "SBV exception:" $$ text (show e)
     SBVPortfolioException e -> text "SBV exception:" $$ text (show e)
     W4Exception e        -> text "What4 exception:" $$ text (show e)
-    CannotLoadASignature -> "Cannot load interfaces"
 
 -- | Raise an exception.
 raise :: REPLException -> REPL a
@@ -565,6 +564,7 @@ validEvalContext a =
              -- XXX: Changes if focusing on nested modules
              M.GlobalName _ I.OrigName { ogModule = I.TopModule m }
                | M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs
+               | M.isLoadedInterface m (M.meLoadedModules me) -> Set.insert nm bs
 
              _ -> bs
 

src/Cryptol/TypeCheck/AST.hs

@@ -459,4 +459,4 @@ instance PP (WithNames TCTopEntity) where
     case ent of
      TCTopModule m -> ppWithNames nm m
      TCTopSignature n ps ->
-        hang ("interface module" <+> pp n <+> "where") 2 (ppWithNames nm ps)
+        hang ("interface module" <+> pp n <+> "where") 2 (pp ps)

src/Cryptol/TypeCheck/Monad.hs

@@ -75,7 +75,7 @@ data InferInput = InferInput
     -- When typechecking a module these start off empty.
     -- We need them when type-checking an expression at the command
     -- line, for example.
-  , inpParams :: !(FunctorParams)
+  , inpParams :: !ModParamNames
 
   , inpNameSeeds :: NameSeeds         -- ^ Private state of type-checker
   , inpMonoBinds :: Bool              -- ^ Should local bindings without
@@ -126,7 +126,7 @@ runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
 runInferM info m0 =
   do let IM m = selectorScope m0
      counter <- newIORef 0
-     let allPs = allParamNames (inpParams info)
+     let allPs = inpParams info
 
      let env = Map.map ExtVar (inpVars info)
             <> Map.map (ExtVar . newtypeConType) (inpNewtypes info)

src/Cryptol/TypeCheck/Sanity.hs

@@ -560,7 +560,7 @@ runTcM env (TcM m) =
     (Left err, _) -> Left err
     (Right a, s)  -> Right (a, woProofObligations s)
   where
-  allPs = allParamNames (inpParams env)
+  allPs = inpParams env
 
   ro = RO { roTVars = Map.fromList [ (tpUnique x, x)
                                       | tp <- Map.elems (mpnTypes allPs)

src/Cryptol/TypeCheck/Type.hs

@@ -1286,24 +1286,22 @@ instance PP TypeSource where
       FunApp                -> "function call"
       TypeErrorPlaceHolder  -> "type error place-holder"
 
-instance PP (WithNames ModParamNames) where
-  ppPrec _ (WithNames ps ns) =
+instance PP ModParamNames where
+  ppPrec _ ps =
     let tps = Map.elems (mpnTypes ps)
     in
     vcat $ map pp tps ++
           if null (mpnConstraints ps) then [] else
             [ "type constraint" <+>
-                parens (commaSep (map (ppWithNames ns . thing)
-                                      (mpnConstraints ps)))
+                parens (commaSep (map (pp . thing) (mpnConstraints ps)))
             ] ++
-           map (ppWithNames ns) (Map.elems (mpnFuns ps))
+           map pp (Map.elems (mpnFuns ps))
 
 instance PP ModTParam where
   ppPrec _ p =
     "type" <+> pp (mtpName p) <+> ":" <+> pp (mtpKind p)
 
-instance PP (WithNames ModVParam) where
-  ppPrec _ (WithNames p ns) =
-    pp (mvpName p) <+> ":" <+> ppWithNames ns (mvpType p)
+instance PP ModVParam where
+  ppPrec _ p = pp (mvpName p) <+> ":" <+> pp (mvpType p)