Implement module-name completion and validation for :browse.

Fixes #396.

cryptol.cabal

@@ -204,6 +204,7 @@ executable cryptol
                      , process
                      , random
                      , sbv >= 7.0
+                     , text
                      , tf-random
                      , transformers
   GHC-options:         -Wall -O2 -threaded -rtsopts "-with-rtsopts=-N1 -A64m"

cryptol/REPL/Haskeline.hs

@@ -26,6 +26,7 @@ import           Data.Char (isAlphaNum, isSpace)
 import           Data.Maybe(isJust)
 import           Data.Function (on)
 import           Data.List (isPrefixOf,nub,sortBy,sort)
+import qualified Data.Text as T (unpack)
 import           System.IO (stdout)
 import           System.Console.ANSI (setTitle, hSupportsANSI)
 import           System.Console.Haskeline
@@ -227,6 +228,7 @@ cmdArgument ct cursor@(l,_) = case ct of
   ExprArg     _ -> completeExpr cursor
   DeclsArg    _ -> (completeExpr +++ completeType) cursor
   ExprTypeArg _ -> (completeExpr +++ completeType) cursor
+  ModNameArg _  -> completeModName cursor
   FilenameArg _ -> completeFilename cursor
   ShellArg _    -> completeFilename cursor
   OptionArg _   -> completeOption cursor
@@ -260,6 +262,14 @@ completeType (l,_) = do
       vars = filter (n `isPrefixOf`) ns
   return (l,map (nameComp n) vars)
 
+-- | Complete a name from the list of loaded modules.
+completeModName :: CompletionFunc REPL
+completeModName (l, _) = do
+  ns <- map T.unpack <$> getModNames
+  let n    = reverse (takeIdent l)
+      vars = filter (n `isPrefixOf`) ns
+  return (l, map (nameComp n) vars)
+
 -- | Generate a completion from a prefix and a name.
 nameComp :: String -> String -> Completion
 nameComp prefix c = Completion

src/Cryptol/REPL/Command.hs

@@ -141,6 +141,7 @@ data CommandBody
   | FileExprArg (FilePath -> String -> REPL ())
   | DeclsArg    (String   -> REPL ())
   | ExprTypeArg (String   -> REPL ())
+  | ModNameArg  (String   -> REPL ())
   | FilenameArg (FilePath -> REPL ())
   | OptionArg   (String   -> REPL ())
   | ShellArg    (String   -> REPL ())
@@ -170,7 +171,7 @@ nbCommandList :: [CommandDescr]
 nbCommandList  =
   [ CommandDescr [ ":t", ":type" ] (ExprArg typeOfCmd)
     "check the type of an expression"
-  , CommandDescr [ ":b", ":browse" ] (ExprTypeArg browseCmd)
+  , CommandDescr [ ":b", ":browse" ] (ModNameArg browseCmd)
     "display the current environment"
   , CommandDescr [ ":?", ":help" ] (ExprArg helpCmd)
     "display a brief description of a function or a type"
@@ -776,18 +777,26 @@ quitCmd  = stop
 
 
 browseCmd :: String -> REPL ()
-browseCmd pfx = do
+browseCmd input = do
   (iface,names,disp) <- getFocusedEnv
+
+  let mnames = map ST.pack (words input)
+  validModNames <- getModNames
+  let checkModName m =
+        unless (m `elem` validModNames) $
+        rPutStrLn ("error: " ++ show m ++ " is not a loaded module.")
+  mapM_ checkModName mnames
+
   let (visibleTypes,visibleDecls) = M.visibleNames names
 
       (visibleType,visibleDecl)
-        | null pfx  =
+        | null mnames =
           ((`Set.member` visibleTypes)
           ,(`Set.member` visibleDecls))
 
         | otherwise =
-          (\n -> n `Set.member` visibleTypes && pfx `isNamePrefix` n
-          ,\n -> n `Set.member` visibleDecls && pfx `isNamePrefix` n)
+          (\n -> n `Set.member` visibleTypes && hasAnyModName mnames n
+          ,\n -> n `Set.member` visibleDecls && hasAnyModName mnames n)
 
   browseTSyns    visibleType iface disp
   browseNewtypes visibleType iface disp
@@ -967,12 +976,11 @@ handleCtrlC a = do rPutStrLn "Ctrl-C"
 
 -- Utilities -------------------------------------------------------------------
 
-isNamePrefix :: String -> M.Name -> Bool
-isNamePrefix pfx =
-  let pfx' = ST.pack pfx
-   in \n -> case M.nameInfo n of
-              M.Declared m -> pfx' `ST.isPrefixOf` m
-              M.Parameter  -> False
+hasAnyModName :: [M.ModName] -> M.Name -> Bool
+hasAnyModName mnames n =
+  case M.nameInfo n of
+    M.Declared m -> m `elem` mnames
+    M.Parameter  -> False
 
 
 -- | Lift a parsing action into the REPL monad.
@@ -1203,6 +1211,7 @@ parseCommand findCmd line = do
       ExprArg     body -> Just (Command (body args'))
       DeclsArg    body -> Just (Command (body args'))
       ExprTypeArg body -> Just (Command (body args'))
+      ModNameArg  body -> Just (Command (body args'))
       FilenameArg body -> Just (Command (body =<< expandHome args'))
       OptionArg   body -> Just (Command (body args'))
       ShellArg    body -> Just (Command (body args'))

src/Cryptol/REPL/Monad.hs

@@ -39,6 +39,7 @@ module Cryptol.REPL.Monad (
   , getExprNames
   , getTypeNames
   , getPropertyNames
+  , getModNames
   , LoadedModule(..), getLoadedMod, setLoadedMod
   , setSearchPath, prependSearchPath
   , getPrompt
@@ -433,6 +434,11 @@ getPropertyNames =
 
      return (ps, names)
 
+getModNames :: REPL [I.ModName]
+getModNames =
+  do me <- getModuleEnv
+     return $ map M.lmName $ M.getLoadedModules $ M.meLoadedModules me
+
 getModuleEnv :: REPL M.ModuleEnv
 getModuleEnv  = eModuleEnv `fmap` getRW