From f0bd0519b5bc99e26d14696b31c89d01da635044 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 6 Apr 2021 15:18:37 -0700 Subject: [PATCH] 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 | 14 ++++--------- src/Cryptol/REPL/Command.hs | 2 +- src/Cryptol/REPL/Monad.hs | 39 ++++++++++++++++++++++++++++++++++++- 3 files changed, 43 insertions(+), 12 deletions(-) diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 3832cfb92..13e001b71 100644 --- a/cryptol/Main.hs +++ b/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 () diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 141f3bfee..72754ea7a 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1245,7 +1245,7 @@ helpCmd cmd M.Parameter -> rPutStrLn "// No documentation is available." - showModHelp env disp x = + showModHelp _env disp x = rPrint $ runDoc disp $ vcat [ "`" <> pp x <> "` is a module." ] -- XXX: show doc. if any diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index cf4c102d0..76f3d193e 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -6,6 +6,7 @@ -- Stability : provisional -- Portability : portable +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -68,6 +69,7 @@ module Cryptol.REPL.Monad ( , getUserProverValidate , parsePPFloatFormat , getProverConfig + , parseSearchPath -- ** Configurable Output , getPutStr @@ -107,6 +109,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 @@ -120,6 +123,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 @@ -493,11 +497,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 @@ -662,6 +669,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. @@ -754,6 +779,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 @@ -850,6 +879,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