From e77b8bb293c0dec91d8cc461ee0ed56995bb5eb4 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/Monad.hs | 39 ++++++++++++++++++++++++++++++++++++++- 2 files changed, 42 insertions(+), 11 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/Monad.hs b/src/Cryptol/REPL/Monad.hs index 7e9062e4a..49892a764 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 #-} @@ -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