Add a new 'path' option to the REPL.

This lets the user reset the module search path. It is a bit of a
blunt instrument as it resets the entire path.  Perhaps we should also
add the ability to add new paths to the front of the search order,
e.g. with a new `:prependpath` command?

Fixes #631

cryptol/Main.hs

@@ -15,7 +15,7 @@ import OptParser
 
 import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandExitCode(..))
 import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
-                   io,prependSearchPath,setSearchPath)
+                   io,prependSearchPath,setSearchPath,parseSearchPath)
 import qualified Cryptol.REPL.Monad as REPL
 import Cryptol.ModuleSystem.Env(ModulePath(..))
 
@@ -32,7 +32,7 @@ import System.Console.GetOpt
 import System.Directory (getTemporaryDirectory, removeFile)
 import System.Environment (getArgs, getProgName, lookupEnv)
 import System.Exit (exitFailure,exitSuccess)
-import System.FilePath (searchPathSeparator, splitSearchPath, takeDirectory)
+import System.FilePath (searchPathSeparator, takeDirectory)
 import System.IO (hClose, hPutStr, openTempFile)
 
 
@@ -256,14 +256,8 @@ setupREPL opts = do
   mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
   case mCryptolPath of
     Nothing -> return ()
-    Just path | optCryptolPathOnly opts -> setSearchPath path'
-              | otherwise               -> prependSearchPath path'
-#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-      -- Windows paths search from end to beginning
-      where path' = reverse (splitSearchPath path)
-#else
-      where path' = splitSearchPath path
-#endif
+    Just path | optCryptolPathOnly opts -> setSearchPath (parseSearchPath path)
+              | otherwise               -> prependSearchPath (parseSearchPath path)
   smoke <- REPL.smokeTest
   case smoke of
     [] -> return ()

src/Cryptol/REPL/Monad.hs

@@ -6,6 +6,7 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -69,6 +70,7 @@ module Cryptol.REPL.Monad (
   , parsePPFloatFormat
   , parseFieldOrder
   , getProverConfig
+  , parseSearchPath
 
     -- ** Configurable Output
   , getPutStr
@@ -108,6 +110,7 @@ import qualified Cryptol.Symbolic.SBV as SBV (proverNames, setupProver, defaultP
 import qualified Cryptol.Symbolic.What4 as W4 (proverNames, setupProver, W4ProverConfig)
 
 
+
 import Control.Monad (ap,unless,when)
 import Control.Monad.Base
 import qualified Control.Monad.Catch as Ex
@@ -121,6 +124,7 @@ import Data.Maybe (catMaybes)
 import Data.Ord (comparing)
 import Data.Typeable (Typeable)
 import System.Directory (findExecutable)
+import System.FilePath (splitSearchPath, searchPathSeparator)
 import qualified Control.Exception as X
 import qualified Data.Map as Map
 import qualified Data.Set as Set
@@ -490,11 +494,14 @@ setSearchPath :: [FilePath] -> REPL ()
 setSearchPath path = do
   me <- getModuleEnv
   setModuleEnv $ me { M.meSearchPath = path }
+  setUserDirect "path" (EnvString (renderSearchPath path))
 
 prependSearchPath :: [FilePath] -> REPL ()
 prependSearchPath path = do
   me <- getModuleEnv
-  setModuleEnv $ me { M.meSearchPath = path ++ M.meSearchPath me }
+  let path' = path ++ M.meSearchPath me
+  setModuleEnv $ me { M.meSearchPath = path' }
+  setUserDirect "path" (EnvString (renderSearchPath path'))
 
 getProverConfig :: REPL (Either SBV.SBVProverConfig W4.W4ProverConfig)
 getProverConfig = eProverConfig <$> getRW
@@ -659,6 +666,24 @@ freshName i sys =
   where mpath = M.TopModule I.interactiveName
 
 
+parseSearchPath :: String -> [String]
+parseSearchPath path = path'
+#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
+      -- Windows paths search from end to beginning
+      where path' = reverse (splitSearchPath path)
+#else
+      where path' = splitSearchPath path
+#endif
+
+renderSearchPath :: [String] -> String
+renderSearchPath pathSegs = path
+#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
+      -- Windows paths search from end to beginning
+      where path = intercalate [searchPathSeparator] (reverse pathSegs)
+#else
+      where path = intercalate [searchPathSeparator] pathSegs
+#endif
+
 -- User Environment Interaction ------------------------------------------------
 
 -- | User modifiable environment, for things like numeric base.
@@ -751,6 +776,10 @@ getUser name = do
     Just ev -> return ev
     Nothing -> panic "[REPL] getUser" ["option `" ++ name ++ "` does not exist"]
 
+setUserDirect :: String -> EnvVal -> REPL ()
+setUserDirect optName val = do
+  modifyRW_ (\rw -> rw { eUserEnv = Map.insert optName val (eUserEnv rw) })
+
 getKnownUser :: IsEnvVal a => String -> REPL a
 getKnownUser x = fromEnvVal <$> getUser x
 
@@ -853,6 +882,14 @@ userOptions  = mkOptionMap
     "Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
   , simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
     "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
+  , OptionDescr "path" [] (EnvString "") noCheck
+    "The search path for finding named Cryptol modules." $
+    \case EnvString path ->
+            do let segs = parseSearchPath path
+               me <- getModuleEnv
+               setModuleEnv me { M.meSearchPath = segs }
+          _ -> return ()
+
   , OptionDescr "monoBinds" ["mono-binds"] (EnvBool True) noCheck
     "Whether or not to generalize bindings in a 'where' clause." $
     \case EnvBool b -> do me <- getModuleEnv