{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.REPL.Monad (
REPL(..), runREPL
, io
, raise
, stop
, catch
, finally
, rPutStrLn
, rPutStr
, rPrint
, REPLException(..)
, rethrowEvalError
, getFocusedEnv
, getModuleEnv, setModuleEnv
, getDynEnv, setDynEnv
, getCallStacks
, getTCSolver
, resetTCSolver
, uniqify, freshName
, whenDebug
, getEvalOptsAction
, getPPValOpts
, getExprNames
, getTypeNames
, getPropertyNames
, getModNames
, LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
, setEditPath, getEditPath, clearEditPath
, setSearchPath, prependSearchPath
, getPrompt
, shouldContinue
, unlessBatch
, asBatch
, validEvalContext
, updateREPLTitle
, setUpdateREPLTitle
, withRandomGen
, setRandomGen
, getRandomGen
, EnvVal(..)
, OptionDescr(..)
, setUser, getUser, getKnownUser, tryGetUser
, userOptions
, userOptionsWithAliases
, getUserSatNum
, getUserShowProverStats
, getUserProverValidate
, parsePPFloatFormat
, parseFieldOrder
, getProverConfig
, parseSearchPath
, getPutStr
, getLogger
, setPutStr
, smokeTest
, Smoke(..)
) where
import Cryptol.REPL.Trie
import Cryptol.Eval (EvalErrorEx, Unsupported, WordTooWide,EvalOpts(..))
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import Cryptol.Parser (ParseError,ppError)
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
import Cryptol.Parser.NoPat (Error)
import Cryptol.Parser.Position (emptyRange, Range(from))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import qualified Cryptol.IR.FreeVars as T
import qualified Cryptol.Utils.Ident as I
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
import qualified Cryptol.Parser.AST as P
import Cryptol.Symbolic (SatNum(..))
import Cryptol.Symbolic.SBV (SBVPortfolioException)
import Cryptol.Symbolic.What4 (W4Exception)
import qualified Cryptol.Symbolic.SBV as SBV (proverNames, setupProver, defaultProver, SBVProverConfig)
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
import Control.Monad.IO.Class
import Control.Monad.Trans.Control
import Data.Char (isSpace, toLower)
import Data.IORef
(IORef,newIORef,readIORef,atomicModifyIORef)
import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
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
import Text.Read (readMaybe)
import Data.SBV (SBVException)
import qualified System.Random.TF as TF
import Prelude ()
import Prelude.Compat
data LoadedModule = LoadedModule
{ LoadedModule -> Maybe ModName
lName :: Maybe P.ModName
, LoadedModule -> ModulePath
lPath :: M.ModulePath
}
data RW = RW
{ RW -> Maybe LoadedModule
eLoadedMod :: Maybe LoadedModule
, RW -> Maybe [Char]
eEditFile :: Maybe FilePath
, RW -> Bool
eContinue :: Bool
, RW -> Bool
eIsBatch :: Bool
, RW -> ModuleEnv
eModuleEnv :: M.ModuleEnv
, RW -> UserEnv
eUserEnv :: UserEnv
, RW -> Logger
eLogger :: Logger
, RW -> Bool
eCallStacks :: Bool
, RW -> REPL ()
eUpdateTitle :: REPL ()
, RW -> Either SBVProverConfig W4ProverConfig
eProverConfig :: Either SBV.SBVProverConfig W4.W4ProverConfig
, RW -> SolverConfig
eTCConfig :: T.SolverConfig
, RW -> Maybe Solver
eTCSolver :: Maybe SMT.Solver
, RW -> Int
eTCSolverRestarts :: !Int
, RW -> TFGen
eRandomGen :: TF.TFGen
}
defaultRW :: Bool -> Bool -> Logger -> IO RW
defaultRW :: Bool -> Bool -> Logger -> IO RW
defaultRW Bool
isBatch Bool
callStacks Logger
l = do
ModuleEnv
env <- IO ModuleEnv
M.initialModuleEnv
TFGen
rng <- IO TFGen
TF.newTFGen
let searchPath :: [[Char]]
searchPath = ModuleEnv -> [[Char]]
M.meSearchPath ModuleEnv
env
let solverConfig :: SolverConfig
solverConfig = [[Char]] -> SolverConfig
T.defaultSolverConfig [[Char]]
searchPath
forall (m :: * -> *) a. Monad m => a -> m a
return RW
{ eLoadedMod :: Maybe LoadedModule
eLoadedMod = forall a. Maybe a
Nothing
, eEditFile :: Maybe [Char]
eEditFile = forall a. Maybe a
Nothing
, eContinue :: Bool
eContinue = Bool
True
, eIsBatch :: Bool
eIsBatch = Bool
isBatch
, eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
env
, eUserEnv :: UserEnv
eUserEnv = OptionMap -> UserEnv
mkUserEnv OptionMap
userOptions
, eLogger :: Logger
eLogger = Logger
l
, eCallStacks :: Bool
eCallStacks = Bool
callStacks
, eUpdateTitle :: REPL ()
eUpdateTitle = forall (m :: * -> *) a. Monad m => a -> m a
return ()
, eProverConfig :: Either SBVProverConfig W4ProverConfig
eProverConfig = forall a b. a -> Either a b
Left SBVProverConfig
SBV.defaultProver
, eTCConfig :: SolverConfig
eTCConfig = SolverConfig
solverConfig
, eTCSolver :: Maybe Solver
eTCSolver = forall a. Maybe a
Nothing
, eTCSolverRestarts :: Int
eTCSolverRestarts = Int
0
, eRandomGen :: TFGen
eRandomGen = TFGen
rng
}
mkPrompt :: RW -> String
mkPrompt :: RW -> [Char]
mkPrompt RW
rw
| RW -> Bool
eIsBatch RW
rw = [Char]
""
| Bool
detailedPrompt = [Char]
withEdit forall a. [a] -> [a] -> [a]
++ [Char]
"> "
| Bool
otherwise = [Char]
modLn forall a. [a] -> [a] -> [a]
++ [Char]
"> "
where
detailedPrompt :: Bool
detailedPrompt = forall a. a -> a
id Bool
False
modLn :: [Char]
modLn =
case LoadedModule -> Maybe ModName
lName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< RW -> Maybe LoadedModule
eLoadedMod RW
rw of
Maybe ModName
Nothing -> forall a. Show a => a -> [Char]
show (forall a. PP a => a -> Doc
pp ModName
I.preludeName)
Just ModName
m
| ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m LoadedModules
loaded -> [Char]
modName forall a. [a] -> [a] -> [a]
++ [Char]
"(parameterized)"
| ModName -> LoadedModules -> Bool
M.isLoadedInterface ModName
m LoadedModules
loaded -> [Char]
modName forall a. [a] -> [a] -> [a]
++ [Char]
"(interface)"
| Bool
otherwise -> [Char]
modName
where modName :: [Char]
modName = forall a. PP a => a -> [Char]
pretty ModName
m
loaded :: LoadedModules
loaded = ModuleEnv -> LoadedModules
M.meLoadedModules (RW -> ModuleEnv
eModuleEnv RW
rw)
withFocus :: [Char]
withFocus =
case RW -> Maybe LoadedModule
eLoadedMod RW
rw of
Maybe LoadedModule
Nothing -> [Char]
modLn
Just LoadedModule
m ->
case (LoadedModule -> Maybe ModName
lName LoadedModule
m, LoadedModule -> ModulePath
lPath LoadedModule
m) of
(Maybe ModName
Nothing, M.InFile [Char]
f) -> [Char]
":r to reload " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
f forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ [Char]
modLn
(Maybe ModName, ModulePath)
_ -> [Char]
modLn
withEdit :: [Char]
withEdit =
case RW -> Maybe [Char]
eEditFile RW
rw of
Maybe [Char]
Nothing -> [Char]
withFocus
Just [Char]
e
| Just (M.InFile [Char]
f) <- LoadedModule -> ModulePath
lPath forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RW -> Maybe LoadedModule
eLoadedMod RW
rw
, [Char]
f forall a. Eq a => a -> a -> Bool
== [Char]
e -> [Char]
withFocus
| Bool
otherwise -> [Char]
":e to edit " forall a. [a] -> [a] -> [a]
++ [Char]
e forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ [Char]
withFocus
newtype REPL a = REPL { forall a. REPL a -> IORef RW -> IO a
unREPL :: IORef RW -> IO a }
runREPL :: Bool -> Bool -> Logger -> REPL a -> IO a
runREPL :: forall a. Bool -> Bool -> Logger -> REPL a -> IO a
runREPL Bool
isBatch Bool
callStacks Logger
l REPL a
m = do
forall (m :: * -> *) a c b.
MonadMask m =>
m a -> (a -> m c) -> (a -> m b) -> m b
Ex.bracket
(forall a. a -> IO (IORef a)
newIORef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Bool -> Logger -> IO RW
defaultRW Bool
isBatch Bool
callStacks Logger
l)
(forall a. REPL a -> IORef RW -> IO a
unREPL REPL ()
resetTCSolver)
(forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m)
instance Functor REPL where
{-# INLINE fmap #-}
fmap :: forall a b. (a -> b) -> REPL a -> REPL b
fmap a -> b
f REPL a
m = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref))
instance Applicative REPL where
{-# INLINE pure #-}
pure :: forall a. a -> REPL a
pure a
x = forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
{-# INLINE (<*>) #-}
<*> :: forall a b. REPL (a -> b) -> REPL a -> REPL b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad REPL where
{-# INLINE return #-}
return :: forall a. a -> REPL a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE (>>=) #-}
REPL a
m >>= :: forall a b. REPL a -> (a -> REPL b) -> REPL b
>>= a -> REPL b
f = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a b. (a -> b) -> a -> b
$ \IORef RW
ref -> do
a
x <- forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
forall a. REPL a -> IORef RW -> IO a
unREPL (a -> REPL b
f a
x) IORef RW
ref
instance MonadIO REPL where
liftIO :: forall a. IO a -> REPL a
liftIO = forall a. IO a -> REPL a
io
instance MonadBase IO REPL where
liftBase :: forall a. IO a -> REPL a
liftBase = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
instance MonadBaseControl IO REPL where
type StM REPL a = a
liftBaseWith :: forall a. (RunInBase REPL IO -> IO a) -> REPL a
liftBaseWith RunInBase REPL IO -> IO a
f = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a b. (a -> b) -> a -> b
$ \IORef RW
ref ->
RunInBase REPL IO -> IO a
f forall a b. (a -> b) -> a -> b
$ \REPL a
m -> forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
restoreM :: forall a. StM REPL a -> REPL a
restoreM StM REPL a
x = forall (m :: * -> *) a. Monad m => a -> m a
return StM REPL a
x
instance M.FreshM REPL where
liftSupply :: forall a. (Supply -> (a, Supply)) -> REPL a
liftSupply Supply -> (a, Supply)
f = forall a. (RW -> (RW, a)) -> REPL a
modifyRW forall a b. (a -> b) -> a -> b
$ \ RW { Bool
Int
Maybe [Char]
Maybe Solver
Maybe LoadedModule
Either SBVProverConfig W4ProverConfig
UserEnv
TFGen
Logger
SolverConfig
ModuleEnv
REPL ()
eRandomGen :: TFGen
eTCSolverRestarts :: Int
eTCSolver :: Maybe Solver
eTCConfig :: SolverConfig
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eCallStacks :: Bool
eLogger :: Logger
eUserEnv :: UserEnv
eModuleEnv :: ModuleEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe [Char]
eLoadedMod :: Maybe LoadedModule
eRandomGen :: RW -> TFGen
eTCSolverRestarts :: RW -> Int
eTCSolver :: RW -> Maybe Solver
eTCConfig :: RW -> SolverConfig
eProverConfig :: RW -> Either SBVProverConfig W4ProverConfig
eUpdateTitle :: RW -> REPL ()
eCallStacks :: RW -> Bool
eLogger :: RW -> Logger
eUserEnv :: RW -> UserEnv
eModuleEnv :: RW -> ModuleEnv
eIsBatch :: RW -> Bool
eContinue :: RW -> Bool
eEditFile :: RW -> Maybe [Char]
eLoadedMod :: RW -> Maybe LoadedModule
.. } ->
let (a
a,Supply
s') = Supply -> (a, Supply)
f (ModuleEnv -> Supply
M.meSupply ModuleEnv
eModuleEnv)
in (RW { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
eModuleEnv { meSupply :: Supply
M.meSupply = Supply
s' }, Bool
Int
Maybe [Char]
Maybe Solver
Maybe LoadedModule
Either SBVProverConfig W4ProverConfig
UserEnv
TFGen
Logger
SolverConfig
REPL ()
eRandomGen :: TFGen
eTCSolverRestarts :: Int
eTCSolver :: Maybe Solver
eTCConfig :: SolverConfig
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eCallStacks :: Bool
eLogger :: Logger
eUserEnv :: UserEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe [Char]
eLoadedMod :: Maybe LoadedModule
eRandomGen :: TFGen
eTCSolverRestarts :: Int
eTCSolver :: Maybe Solver
eTCConfig :: SolverConfig
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eCallStacks :: Bool
eLogger :: Logger
eUserEnv :: UserEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe [Char]
eLoadedMod :: Maybe LoadedModule
.. },a
a)
instance Ex.MonadThrow REPL where
throwM :: forall e a. Exception e => e -> REPL a
throwM e
e = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => e -> IO a
X.throwIO e
e
instance Ex.MonadCatch REPL where
catch :: forall e a. Exception e => REPL a -> (e -> REPL a) -> REPL a
catch REPL a
op e -> REPL a
handler = forall (b :: * -> *) (m :: * -> *) a.
MonadBaseControl b m =>
(RunInBase m b -> b (StM m a)) -> m a
control forall a b. (a -> b) -> a -> b
$ \RunInBase REPL IO
runInBase -> forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
Ex.catch (RunInBase REPL IO
runInBase REPL a
op) (RunInBase REPL IO
runInBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> REPL a
handler)
instance Ex.MonadMask REPL where
mask :: forall b. ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b
mask (forall a. REPL a -> REPL a) -> REPL b
op = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a b. (a -> b) -> a -> b
$ \IORef RW
ref -> forall (m :: * -> *) b.
MonadMask m =>
((forall a. m a -> m a) -> m b) -> m b
Ex.mask forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
u -> forall a. REPL a -> IORef RW -> IO a
unREPL ((forall a. REPL a -> REPL a) -> REPL b
op (forall {a} {a}. (IO a -> IO a) -> REPL a -> REPL a
q forall a. IO a -> IO a
u)) IORef RW
ref
where q :: (IO a -> IO a) -> REPL a -> REPL a
q IO a -> IO a
u (REPL IORef RW -> IO a
b) = forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
ref -> IO a -> IO a
u (IORef RW -> IO a
b IORef RW
ref))
uninterruptibleMask :: forall b. ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b
uninterruptibleMask (forall a. REPL a -> REPL a) -> REPL b
op = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a b. (a -> b) -> a -> b
$ \IORef RW
ref ->
forall (m :: * -> *) b.
MonadMask m =>
((forall a. m a -> m a) -> m b) -> m b
Ex.uninterruptibleMask forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
u -> forall a. REPL a -> IORef RW -> IO a
unREPL ((forall a. REPL a -> REPL a) -> REPL b
op (forall {a} {a}. (IO a -> IO a) -> REPL a -> REPL a
q forall a. IO a -> IO a
u)) IORef RW
ref
where q :: (IO a -> IO a) -> REPL a -> REPL a
q IO a -> IO a
u (REPL IORef RW -> IO a
b) = forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
ref -> IO a -> IO a
u (IORef RW -> IO a
b IORef RW
ref))
generalBracket :: forall a b c.
REPL a
-> (a -> ExitCase b -> REPL c) -> (a -> REPL b) -> REPL (b, c)
generalBracket REPL a
acq a -> ExitCase b -> REPL c
rls a -> REPL b
op = forall (b :: * -> *) (m :: * -> *) a.
MonadBaseControl b m =>
(RunInBase m b -> b (StM m a)) -> m a
control forall a b. (a -> b) -> a -> b
$ \RunInBase REPL IO
runInBase ->
forall (m :: * -> *) a b c.
MonadMask m =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
Ex.generalBracket (RunInBase REPL IO
runInBase REPL a
acq)
(\a
saved -> \ExitCase b
e -> RunInBase REPL IO
runInBase (forall (b :: * -> *) (m :: * -> *) a.
MonadBaseControl b m =>
StM m a -> m a
restoreM a
saved forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> a -> ExitCase b -> REPL c
rls a
a ExitCase b
e))
(\a
saved -> RunInBase REPL IO
runInBase (forall (b :: * -> *) (m :: * -> *) a.
MonadBaseControl b m =>
StM m a -> m a
restoreM a
saved forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> REPL b
op))
data REPLException
= ParseError ParseError
| FileNotFound FilePath
| DirectoryNotFound FilePath
| NoPatError [Error]
| NoIncludeError [IncludeError]
| EvalError EvalErrorEx
| TooWide WordTooWide
| Unsupported Unsupported
| ModuleSystemError NameDisp M.ModuleError
| EvalPolyError T.Schema
| InstantiationsNotFound T.Schema
| TypeNotTestable T.Type
| EvalInParamModule [T.TParam] [M.Name]
| SBVError String
| SBVException SBVException
| SBVPortfolioException SBVPortfolioException
| W4Exception W4Exception
deriving (Int -> REPLException -> ShowS
[REPLException] -> ShowS
REPLException -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [REPLException] -> ShowS
$cshowList :: [REPLException] -> ShowS
show :: REPLException -> [Char]
$cshow :: REPLException -> [Char]
showsPrec :: Int -> REPLException -> ShowS
$cshowsPrec :: Int -> REPLException -> ShowS
Show,Typeable)
instance X.Exception REPLException
instance PP REPLException where
ppPrec :: Int -> REPLException -> Doc
ppPrec Int
_ REPLException
re = case REPLException
re of
ParseError ParseError
e -> ParseError -> Doc
ppError ParseError
e
FileNotFound [Char]
path -> [Doc] -> Doc
sep [ [Char] -> Doc
text [Char]
"File"
, [Char] -> Doc
text ([Char]
"`" forall a. [a] -> [a] -> [a]
++ [Char]
path forall a. [a] -> [a] -> [a]
++ [Char]
"'")
, [Char] -> Doc
text[Char]
"not found"
]
DirectoryNotFound [Char]
path -> [Doc] -> Doc
sep [ [Char] -> Doc
text [Char]
"Directory"
, [Char] -> Doc
text ([Char]
"`" forall a. [a] -> [a] -> [a]
++ [Char]
path forall a. [a] -> [a] -> [a]
++ [Char]
"'")
, [Char] -> Doc
text[Char]
"not found or not a directory"
]
NoPatError [Error]
es -> [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [Error]
es)
NoIncludeError [IncludeError]
es -> [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map IncludeError -> Doc
ppIncludeError [IncludeError]
es)
ModuleSystemError NameDisp
ns ModuleError
me -> NameDisp -> Doc -> Doc
fixNameDisp NameDisp
ns (forall a. PP a => a -> Doc
pp ModuleError
me)
EvalError EvalErrorEx
e -> forall a. PP a => a -> Doc
pp EvalErrorEx
e
Unsupported Unsupported
e -> forall a. PP a => a -> Doc
pp Unsupported
e
TooWide WordTooWide
e -> forall a. PP a => a -> Doc
pp WordTooWide
e
EvalPolyError Schema
s -> [Char] -> Doc
text [Char]
"Cannot evaluate polymorphic value."
Doc -> Doc -> Doc
$$ [Char] -> Doc
text [Char]
"Type:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Schema
s
InstantiationsNotFound Schema
s -> [Char] -> Doc
text [Char]
"Cannot find instantiations for some type variables."
Doc -> Doc -> Doc
$$ [Char] -> Doc
text [Char]
"Type:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Schema
s
TypeNotTestable Type
t -> [Char] -> Doc
text [Char]
"The expression is not of a testable type."
Doc -> Doc -> Doc
$$ [Char] -> Doc
text [Char]
"Type:" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Type
t
EvalInParamModule [TParam]
as [Name]
xs -> Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vsep forall a b. (a -> b) -> a -> b
$
[ [Char] -> Doc
text [Char]
"Expression depends on definitions from a parameterized module:" ]
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [TParam]
as
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => a -> Doc
pp [Name]
xs
SBVError [Char]
s -> [Char] -> Doc
text [Char]
"SBV error:" Doc -> Doc -> Doc
$$ [Char] -> Doc
text [Char]
s
SBVException SBVException
e -> [Char] -> Doc
text [Char]
"SBV exception:" Doc -> Doc -> Doc
$$ [Char] -> Doc
text (forall a. Show a => a -> [Char]
show SBVException
e)
SBVPortfolioException SBVPortfolioException
e -> [Char] -> Doc
text [Char]
"SBV exception:" Doc -> Doc -> Doc
$$ [Char] -> Doc
text (forall a. Show a => a -> [Char]
show SBVPortfolioException
e)
W4Exception W4Exception
e -> [Char] -> Doc
text [Char]
"What4 exception:" Doc -> Doc -> Doc
$$ [Char] -> Doc
text (forall a. Show a => a -> [Char]
show W4Exception
e)
raise :: REPLException -> REPL a
raise :: forall a. REPLException -> REPL a
raise REPLException
exn = forall a. IO a -> REPL a
io (forall e a. Exception e => e -> IO a
X.throwIO REPLException
exn)
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch :: forall a. REPL a -> (REPLException -> REPL a) -> REPL a
catch REPL a
m REPLException -> REPL a
k = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> forall a. IO a -> IO a
rethrowEvalError (forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` \ REPLException
e -> forall a. REPL a -> IORef RW -> IO a
unREPL (REPLException -> REPL a
k REPLException
e) IORef RW
ref)
finally :: REPL a -> REPL b -> REPL a
finally :: forall a b. REPL a -> REPL b -> REPL a
finally REPL a
m1 REPL b
m2 = forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
ref -> forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m1 IORef RW
ref forall a b. IO a -> IO b -> IO a
`X.finally` forall a. REPL a -> IORef RW -> IO a
unREPL REPL b
m2 IORef RW
ref)
rethrowEvalError :: IO a -> IO a
rethrowEvalError :: forall a. IO a -> IO a
rethrowEvalError IO a
m =
IO a
run forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` forall a. EvalErrorEx -> IO a
rethrow
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` forall a. WordTooWide -> IO a
rethrowTooWide
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` forall a. Unsupported -> IO a
rethrowUnsupported
where
run :: IO a
run = do
a
a <- IO a
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! a
a
rethrow :: EvalErrorEx -> IO a
rethrow :: forall a. EvalErrorEx -> IO a
rethrow EvalErrorEx
exn = forall e a. Exception e => e -> IO a
X.throwIO (EvalErrorEx -> REPLException
EvalError EvalErrorEx
exn)
rethrowTooWide :: WordTooWide -> IO a
rethrowTooWide :: forall a. WordTooWide -> IO a
rethrowTooWide WordTooWide
exn = forall e a. Exception e => e -> IO a
X.throwIO (WordTooWide -> REPLException
TooWide WordTooWide
exn)
rethrowUnsupported :: Unsupported -> IO a
rethrowUnsupported :: forall a. Unsupported -> IO a
rethrowUnsupported Unsupported
exn = forall e a. Exception e => e -> IO a
X.throwIO (Unsupported -> REPLException
Unsupported Unsupported
exn)
io :: IO a -> REPL a
io :: forall a. IO a -> REPL a
io IO a
m = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
_ -> IO a
m)
getRW :: REPL RW
getRW :: REPL RW
getRW = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a. IORef a -> IO a
readIORef
modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW :: forall a. (RW -> (RW, a)) -> REPL a
modifyRW RW -> (RW, a)
f = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef RW
ref RW -> (RW, a)
f)
modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ :: (RW -> RW) -> REPL ()
modifyRW_ RW -> RW
f = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef RW
ref (\RW
x -> (RW -> RW
f RW
x, ())))
getPrompt :: REPL String
getPrompt :: REPL [Char]
getPrompt = RW -> [Char]
mkPrompt forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
getCallStacks :: REPL Bool
getCallStacks :: REPL Bool
getCallStacks = RW -> Bool
eCallStacks forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
getTCSolver :: REPL SMT.Solver
getTCSolver :: REPL Solver
getTCSolver =
do RW
rw <- REPL RW
getRW
case RW -> Maybe Solver
eTCSolver RW
rw of
Just Solver
s -> forall (m :: * -> *) a. Monad m => a -> m a
return Solver
s
Maybe Solver
Nothing ->
do IORef RW
ref <- forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
ref -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IORef RW
ref)
let now :: Int
now = RW -> Int
eTCSolverRestarts RW
rw forall a. Num a => a -> a -> a
+ Int
1
upd :: RW -> RW
upd RW
new = if RW -> Int
eTCSolverRestarts RW
new forall a. Eq a => a -> a -> Bool
== Int
now
then RW
new { eTCSolver :: Maybe Solver
eTCSolver = forall a. Maybe a
Nothing }
else RW
new
onExit :: IO ()
onExit = forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef RW
ref (\RW
s -> (RW -> RW
upd RW
s, ()))
Solver
s <- forall a. IO a -> REPL a
io (IO () -> SolverConfig -> IO Solver
SMT.startSolver IO ()
onExit (RW -> SolverConfig
eTCConfig RW
rw))
(RW -> RW) -> REPL ()
modifyRW_ (\RW
rw' -> RW
rw'{ eTCSolver :: Maybe Solver
eTCSolver = forall a. a -> Maybe a
Just Solver
s
, eTCSolverRestarts :: Int
eTCSolverRestarts = Int
now })
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
s
resetTCSolver :: REPL ()
resetTCSolver :: REPL ()
resetTCSolver =
do Maybe Solver
mtc <- RW -> Maybe Solver
eTCSolver forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
case Maybe Solver
mtc of
Maybe Solver
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Solver
s ->
do forall a. IO a -> REPL a
io (Solver -> IO ()
SMT.stopSolver Solver
s)
(RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw{ eTCSolver :: Maybe Solver
eTCSolver = forall a. Maybe a
Nothing })
getPPValOpts :: REPL PPOpts
getPPValOpts :: REPL PPOpts
getPPValOpts =
do Int
base <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"base"
Bool
ascii <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"ascii"
Int
infLength <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"infLength"
Int
fpBase <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"fpBase"
[Char]
fpFmtTxt <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"fpFormat"
FieldOrder
fieldOrder <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"fieldOrder"
let fpFmt :: PPFloatFormat
fpFmt = case [Char] -> Maybe PPFloatFormat
parsePPFloatFormat [Char]
fpFmtTxt of
Just PPFloatFormat
f -> PPFloatFormat
f
Maybe PPFloatFormat
Nothing -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"getPPOpts"
[ [Char]
"Failed to parse fp-format" ]
forall (m :: * -> *) a. Monad m => a -> m a
return PPOpts { useBase :: Int
useBase = Int
base
, useAscii :: Bool
useAscii = Bool
ascii
, useInfLength :: Int
useInfLength = Int
infLength
, useFPBase :: Int
useFPBase = Int
fpBase
, useFPFormat :: PPFloatFormat
useFPFormat = PPFloatFormat
fpFmt
, useFieldOrder :: FieldOrder
useFieldOrder = FieldOrder
fieldOrder
}
getEvalOptsAction :: REPL (IO EvalOpts)
getEvalOptsAction :: REPL (IO EvalOpts)
getEvalOptsAction = forall a. (IORef RW -> IO a) -> REPL a
REPL forall a b. (a -> b) -> a -> b
$ \IORef RW
rwRef -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
do PPOpts
ppOpts <- forall a. REPL a -> IORef RW -> IO a
unREPL REPL PPOpts
getPPValOpts IORef RW
rwRef
Logger
l <- forall a. REPL a -> IORef RW -> IO a
unREPL REPL Logger
getLogger IORef RW
rwRef
forall (m :: * -> *) a. Monad m => a -> m a
return EvalOpts { evalPPOpts :: PPOpts
evalPPOpts = PPOpts
ppOpts, evalLogger :: Logger
evalLogger = Logger
l }
clearLoadedMod :: REPL ()
clearLoadedMod :: REPL ()
clearLoadedMod = do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> LoadedModule
upd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RW -> Maybe LoadedModule
eLoadedMod RW
rw })
REPL ()
updateREPLTitle
where upd :: LoadedModule -> LoadedModule
upd LoadedModule
x = LoadedModule
x { lName :: Maybe ModName
lName = forall a. Maybe a
Nothing }
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod LoadedModule
n = do
(RW -> RW) -> REPL ()
modifyRW_ (\ RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = forall a. a -> Maybe a
Just LoadedModule
n })
REPL ()
updateREPLTitle
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod = RW -> Maybe LoadedModule
eLoadedMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setEditPath :: FilePath -> REPL ()
setEditPath :: [Char] -> REPL ()
setEditPath [Char]
p = (RW -> RW) -> REPL ()
modifyRW_ forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { eEditFile :: Maybe [Char]
eEditFile = forall a. a -> Maybe a
Just [Char]
p }
getEditPath :: REPL (Maybe FilePath)
getEditPath :: REPL (Maybe [Char])
getEditPath = RW -> Maybe [Char]
eEditFile forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
clearEditPath :: REPL ()
clearEditPath :: REPL ()
clearEditPath = (RW -> RW) -> REPL ()
modifyRW_ forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { eEditFile :: Maybe [Char]
eEditFile = forall a. Maybe a
Nothing }
setSearchPath :: [FilePath] -> REPL ()
setSearchPath :: [[Char]] -> REPL ()
setSearchPath [[Char]]
path = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [[Char]]
M.meSearchPath = [[Char]]
path }
[Char] -> EnvVal -> REPL ()
setUserDirect [Char]
"path" ([Char] -> EnvVal
EnvString ([[Char]] -> [Char]
renderSearchPath [[Char]]
path))
prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [[Char]] -> REPL ()
prependSearchPath [[Char]]
path = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
let path' :: [[Char]]
path' = [[Char]]
path forall a. [a] -> [a] -> [a]
++ ModuleEnv -> [[Char]]
M.meSearchPath ModuleEnv
me
ModuleEnv -> REPL ()
setModuleEnv forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [[Char]]
M.meSearchPath = [[Char]]
path' }
[Char] -> EnvVal -> REPL ()
setUserDirect [Char]
"path" ([Char] -> EnvVal
EnvString ([[Char]] -> [Char]
renderSearchPath [[Char]]
path'))
getProverConfig :: REPL (Either SBV.SBVProverConfig W4.W4ProverConfig)
getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig = RW -> Either SBVProverConfig W4ProverConfig
eProverConfig forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
shouldContinue :: REPL Bool
shouldContinue :: REPL Bool
shouldContinue = RW -> Bool
eContinue forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
stop :: REPL ()
stop :: REPL ()
stop = (RW -> RW) -> REPL ()
modifyRW_ (\ RW
rw -> RW
rw { eContinue :: Bool
eContinue = Bool
False })
unlessBatch :: REPL () -> REPL ()
unlessBatch :: REPL () -> REPL ()
unlessBatch REPL ()
body = do
RW
rw <- REPL RW
getRW
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RW -> Bool
eIsBatch RW
rw) REPL ()
body
asBatch :: REPL a -> REPL a
asBatch :: forall a. REPL a -> REPL a
asBatch REPL a
body = do
Bool
wasBatch <- RW -> Bool
eIsBatch forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
(RW -> RW) -> REPL ()
modifyRW_ forall a b. (a -> b) -> a -> b
$ (\ RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
True })
a
a <- REPL a
body
(RW -> RW) -> REPL ()
modifyRW_ forall a b. (a -> b) -> a -> b
$ (\ RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
wasBatch })
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
validEvalContext :: T.FreeVars a => a -> REPL ()
validEvalContext :: forall a. FreeVars a => a -> REPL ()
validEvalContext a
a =
do ModuleEnv
me <- RW -> ModuleEnv
eModuleEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
let ds :: Deps
ds = forall e. FreeVars e => e -> Deps
T.freeVars a
a
badVals :: Set Name
badVals = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
badName forall a. Set a
Set.empty (Deps -> Set Name
T.valDeps Deps
ds)
bad :: Set Name
bad = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
badName Set Name
badVals (Deps -> Set Name
T.tyDeps Deps
ds)
badTs :: Set TParam
badTs = Deps -> Set TParam
T.tyParams Deps
ds
badName :: Name -> Set Name -> Set Name
badName Name
nm Set Name
bs =
case Name -> NameInfo
M.nameInfo Name
nm of
M.GlobalName NameSource
_ I.OrigName { ogModule :: OrigName -> ModPath
ogModule = I.TopModule ModName
m }
| ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules ModuleEnv
me) -> forall a. Ord a => a -> Set a -> Set a
Set.insert Name
nm Set Name
bs
| ModName -> LoadedModules -> Bool
M.isLoadedInterface ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules ModuleEnv
me) -> forall a. Ord a => a -> Set a -> Set a
Set.insert Name
nm Set Name
bs
NameInfo
_ -> Set Name
bs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
Set.null Set Name
bad Bool -> Bool -> Bool
&& forall a. Set a -> Bool
Set.null Set TParam
badTs) forall a b. (a -> b) -> a -> b
$
forall a. REPLException -> REPL a
raise ([TParam] -> [Name] -> REPLException
EvalInParamModule (forall a. Set a -> [a]
Set.toList Set TParam
badTs) (forall a. Set a -> [a]
Set.toList Set Name
bad))
updateREPLTitle :: REPL ()
updateREPLTitle :: REPL ()
updateREPLTitle = REPL () -> REPL ()
unlessBatch forall a b. (a -> b) -> a -> b
$ do
RW
rw <- REPL RW
getRW
RW -> REPL ()
eUpdateTitle RW
rw
setUpdateREPLTitle :: REPL () -> REPL ()
setUpdateREPLTitle :: REPL () -> REPL ()
setUpdateREPLTitle REPL ()
m = (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eUpdateTitle :: REPL ()
eUpdateTitle = REPL ()
m })
setPutStr :: (String -> IO ()) -> REPL ()
setPutStr :: ([Char] -> IO ()) -> REPL ()
setPutStr [Char] -> IO ()
fn = (RW -> RW) -> REPL ()
modifyRW_ forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { eLogger :: Logger
eLogger = ([Char] -> IO ()) -> Logger
funLogger [Char] -> IO ()
fn }
getPutStr :: REPL (String -> IO ())
getPutStr :: REPL ([Char] -> IO ())
getPutStr =
do RW
rw <- REPL RW
getRW
forall (m :: * -> *) a. Monad m => a -> m a
return (Logger -> [Char] -> IO ()
logPutStr (RW -> Logger
eLogger RW
rw))
getLogger :: REPL Logger
getLogger :: REPL Logger
getLogger = RW -> Logger
eLogger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
rPutStr :: String -> REPL ()
rPutStr :: [Char] -> REPL ()
rPutStr [Char]
str = do
[Char] -> IO ()
f <- REPL ([Char] -> IO ())
getPutStr
forall a. IO a -> REPL a
io ([Char] -> IO ()
f [Char]
str)
rPutStrLn :: String -> REPL ()
rPutStrLn :: [Char] -> REPL ()
rPutStrLn [Char]
str = [Char] -> REPL ()
rPutStr forall a b. (a -> b) -> a -> b
$ [Char]
str forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
rPrint :: Show a => a -> REPL ()
rPrint :: forall a. Show a => a -> REPL ()
rPrint a
x = [Char] -> REPL ()
rPutStrLn (forall a. Show a => a -> [Char]
show a
x)
getFocusedEnv :: REPL M.ModContext
getFocusedEnv :: REPL ModContext
getFocusedEnv = ModuleEnv -> ModContext
M.focusedEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModuleEnv
getModuleEnv
getExprNames :: REPL [String]
getExprNames :: REPL [[Char]]
getExprNames =
do NamingEnv
fNames <- ModContext -> NamingEnv
M.mctxNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
pp) (forall k a. Map k a -> [k]
Map.keys (Namespace -> NamingEnv -> Map PName Names
M.namespaceMap Namespace
M.NSValue NamingEnv
fNames)))
getTypeNames :: REPL [String]
getTypeNames :: REPL [[Char]]
getTypeNames =
do NamingEnv
fNames <- ModContext -> NamingEnv
M.mctxNames forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModContext
getFocusedEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> [Char]
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> Doc
pp) (forall k a. Map k a -> [k]
Map.keys (Namespace -> NamingEnv -> Map PName Names
M.namespaceMap Namespace
M.NSType NamingEnv
fNames)))
getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
getPropertyNames :: REPL ([(Name, IfaceDecl)], NameDisp)
getPropertyNames =
do ModContext
fe <- REPL ModContext
getFocusedEnv
let xs :: Map Name IfaceDecl
xs = IfaceDecls -> Map Name IfaceDecl
M.ifDecls (ModContext -> IfaceDecls
M.mctxDecls ModContext
fe)
ps :: [(Name, IfaceDecl)]
ps = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Range -> Position
from forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
M.nameLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst))
[ (Name
x,IfaceDecl
d) | (Name
x,IfaceDecl
d) <- forall k a. Map k a -> [(k, a)]
Map.toList Map Name IfaceDecl
xs,
Pragma
T.PragmaProperty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IfaceDecl -> [Pragma]
M.ifDeclPragmas IfaceDecl
d ]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, IfaceDecl)]
ps, ModContext -> NameDisp
M.mctxNameDisp ModContext
fe)
getModNames :: REPL [I.ModName]
getModNames :: REPL [ModName]
getModNames =
do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall mname. ModuleG mname -> mname
T.mName (ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me))
getModuleEnv :: REPL M.ModuleEnv
getModuleEnv :: REPL ModuleEnv
getModuleEnv = RW -> ModuleEnv
eModuleEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setModuleEnv :: M.ModuleEnv -> REPL ()
setModuleEnv :: ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me = (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
me })
getDynEnv :: REPL M.DynamicEnv
getDynEnv :: REPL DynamicEnv
getDynEnv = (ModuleEnv -> DynamicEnv
M.meDynEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> ModuleEnv
eModuleEnv) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setDynEnv :: M.DynamicEnv -> REPL ()
setDynEnv :: DynamicEnv -> REPL ()
setDynEnv DynamicEnv
denv = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv
me { meDynEnv :: DynamicEnv
M.meDynEnv = DynamicEnv
denv })
getRandomGen :: REPL TF.TFGen
getRandomGen :: REPL TFGen
getRandomGen = RW -> TFGen
eRandomGen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
setRandomGen :: TF.TFGen -> REPL ()
setRandomGen :: TFGen -> REPL ()
setRandomGen TFGen
rng = (RW -> RW) -> REPL ()
modifyRW_ (\RW
s -> RW
s { eRandomGen :: TFGen
eRandomGen = TFGen
rng })
withRandomGen :: (TF.TFGen -> REPL (a, TF.TFGen)) -> REPL a
withRandomGen :: forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
withRandomGen TFGen -> REPL (a, TFGen)
repl =
do TFGen
g <- REPL TFGen
getRandomGen
(a
result, TFGen
g') <- TFGen -> REPL (a, TFGen)
repl TFGen
g
TFGen -> REPL ()
setRandomGen TFGen
g'
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
result
uniqify :: M.Name -> REPL M.Name
uniqify :: Name -> REPL Name
uniqify Name
name =
case Name -> NameInfo
M.nameInfo Name
name of
M.GlobalName NameSource
s OrigName
og ->
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (Namespace
-> ModPath
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared (Name -> Namespace
M.nameNamespace Name
name)
(OrigName -> ModPath
I.ogModule OrigName
og) NameSource
s
(Name -> Ident
M.nameIdent Name
name) (Name -> Maybe Fixity
M.nameFixity Name
name) (Name -> Range
M.nameLoc Name
name))
M.LocalName {} ->
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"[REPL] uniqify" [[Char]
"tried to uniqify a parameter: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty Name
name]
freshName :: I.Ident -> M.NameSource -> REPL M.Name
freshName :: Ident -> NameSource -> REPL Name
freshName Ident
i NameSource
sys =
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (Namespace
-> ModPath
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared Namespace
I.NSValue ModPath
mpath NameSource
sys Ident
i forall a. Maybe a
Nothing Range
emptyRange)
where mpath :: ModPath
mpath = ModName -> ModPath
M.TopModule ModName
I.interactiveName
parseSearchPath :: String -> [String]
parseSearchPath :: [Char] -> [[Char]]
parseSearchPath [Char]
path = [[Char]]
path'
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
where path' = reverse (splitSearchPath path)
#else
where path' :: [[Char]]
path' = [Char] -> [[Char]]
splitSearchPath [Char]
path
#endif
renderSearchPath :: [String] -> String
renderSearchPath :: [[Char]] -> [Char]
renderSearchPath [[Char]]
pathSegs = [Char]
path
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
where path = intercalate [searchPathSeparator] (reverse pathSegs)
#else
where path :: [Char]
path = forall a. [a] -> [[a]] -> [a]
intercalate [Char
searchPathSeparator] [[Char]]
pathSegs
#endif
type UserEnv = Map.Map String EnvVal
data EnvVal
= EnvString String
| EnvProg String [String]
| EnvNum !Int
| EnvBool Bool
deriving (Int -> EnvVal -> ShowS
[EnvVal] -> ShowS
EnvVal -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [EnvVal] -> ShowS
$cshowList :: [EnvVal] -> ShowS
show :: EnvVal -> [Char]
$cshow :: EnvVal -> [Char]
showsPrec :: Int -> EnvVal -> ShowS
$cshowsPrec :: Int -> EnvVal -> ShowS
Show)
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv OptionMap
opts = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
OptionDescr
opt <- forall a. Trie a -> [a]
leaves OptionMap
opts
forall (m :: * -> *) a. Monad m => a -> m a
return (OptionDescr -> [Char]
optName OptionDescr
opt, OptionDescr -> EnvVal
optDefault OptionDescr
opt)
setUser :: String -> String -> REPL ()
setUser :: [Char] -> [Char] -> REPL ()
setUser [Char]
name [Char]
val = case forall a. [Char] -> Trie a -> [a]
lookupTrieExact [Char]
name OptionMap
userOptionsWithAliases of
[OptionDescr
opt] -> OptionDescr -> REPL ()
setUserOpt OptionDescr
opt
[] -> [Char] -> REPL ()
rPutStrLn ([Char]
"Unknown env value `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"`")
[OptionDescr]
_ -> [Char] -> REPL ()
rPutStrLn ([Char]
"Ambiguous env value `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"`")
where
setUserOpt :: OptionDescr -> REPL ()
setUserOpt OptionDescr
opt = case OptionDescr -> EnvVal
optDefault OptionDescr
opt of
EnvString [Char]
_ -> EnvVal -> REPL ()
doCheck ([Char] -> EnvVal
EnvString [Char]
val)
EnvProg [Char]
_ [[Char]]
_ ->
case [Char] -> [[Char]]
splitOptArgs [Char]
val of
[Char]
prog:[[Char]]
args -> EnvVal -> REPL ()
doCheck ([Char] -> [[Char]] -> EnvVal
EnvProg [Char]
prog [[Char]]
args)
[] -> [Char] -> REPL ()
rPutStrLn ([Char]
"Failed to parse command for field, `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"`")
EnvNum Int
_ -> case forall a. Read a => ReadS a
reads [Char]
val of
[(Int
x,[Char]
_)] -> EnvVal -> REPL ()
doCheck (Int -> EnvVal
EnvNum Int
x)
[(Int, [Char])]
_ -> [Char] -> REPL ()
rPutStrLn ([Char]
"Failed to parse number for field, `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"`")
EnvBool Bool
_
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
val) [[Char]
"enable", [Char]
"on", [Char]
"yes", [Char]
"true"] ->
EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
True)
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
val) [[Char]
"disable", [Char]
"off", [Char]
"no", [Char]
"false"] ->
EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
False)
| Bool
otherwise ->
[Char] -> REPL ()
rPutStrLn ([Char]
"Failed to parse boolean for field, `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"`")
where
doCheck :: EnvVal -> REPL ()
doCheck EnvVal
v = do (Maybe [Char]
r,[[Char]]
ws) <- OptionDescr -> Checker
optCheck OptionDescr
opt EnvVal
v
case Maybe [Char]
r of
Just [Char]
err -> [Char] -> REPL ()
rPutStrLn [Char]
err
Maybe [Char]
Nothing -> do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> REPL ()
rPutStrLn [[Char]]
ws
EnvVal -> REPL ()
writeEnv EnvVal
v
writeEnv :: EnvVal -> REPL ()
writeEnv EnvVal
ev =
do OptionDescr -> EnvVal -> REPL ()
optEff OptionDescr
opt EnvVal
ev
(RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eUserEnv :: UserEnv
eUserEnv = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OptionDescr -> [Char]
optName OptionDescr
opt) EnvVal
ev (RW -> UserEnv
eUserEnv RW
rw) })
splitOptArgs :: String -> [String]
splitOptArgs :: [Char] -> [[Char]]
splitOptArgs = forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr ([Char] -> [Char] -> Maybe ([Char], [Char])
parse [Char]
"")
where
parse :: [Char] -> [Char] -> Maybe ([Char], [Char])
parse [Char]
acc (Char
c:[Char]
cs) | Char -> Bool
isQuote Char
c = [Char] -> [Char] -> Maybe ([Char], [Char])
quoted (Char
cforall a. a -> [a] -> [a]
:[Char]
acc) [Char]
cs
| Bool -> Bool
not (Char -> Bool
isSpace Char
c) = [Char] -> [Char] -> Maybe ([Char], [Char])
parse (Char
cforall a. a -> [a] -> [a]
:[Char]
acc) [Char]
cs
| Bool
otherwise = [Char] -> [Char] -> Maybe ([Char], [Char])
result [Char]
acc [Char]
cs
parse [Char]
acc [] = [Char] -> [Char] -> Maybe ([Char], [Char])
result [Char]
acc []
quoted :: [Char] -> [Char] -> Maybe ([Char], [Char])
quoted [Char]
acc (Char
c:[Char]
cs) | Char -> Bool
isQuote Char
c = [Char] -> [Char] -> Maybe ([Char], [Char])
parse (Char
cforall a. a -> [a] -> [a]
:[Char]
acc) [Char]
cs
| Bool
otherwise = [Char] -> [Char] -> Maybe ([Char], [Char])
quoted (Char
cforall a. a -> [a] -> [a]
:[Char]
acc) [Char]
cs
quoted [Char]
acc [] = [Char] -> [Char] -> Maybe ([Char], [Char])
result [Char]
acc []
result :: [Char] -> [Char] -> Maybe ([Char], [Char])
result [] [] = forall a. Maybe a
Nothing
result [] [Char]
cs = [Char] -> [Char] -> Maybe ([Char], [Char])
parse [] (forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
cs)
result [Char]
acc [Char]
cs = forall a. a -> Maybe a
Just (forall a. [a] -> [a]
reverse [Char]
acc, forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
cs)
isQuote :: Char -> Bool
isQuote :: Char -> Bool
isQuote Char
c = Char
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
"'\"" :: String)
tryGetUser :: String -> REPL (Maybe EnvVal)
tryGetUser :: [Char] -> REPL (Maybe EnvVal)
tryGetUser [Char]
name = do
RW
rw <- REPL RW
getRW
forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [Char]
name (RW -> UserEnv
eUserEnv RW
rw))
getUser :: String -> REPL EnvVal
getUser :: [Char] -> REPL EnvVal
getUser [Char]
name = do
Maybe EnvVal
mb <- [Char] -> REPL (Maybe EnvVal)
tryGetUser [Char]
name
case Maybe EnvVal
mb of
Just EnvVal
ev -> forall (m :: * -> *) a. Monad m => a -> m a
return EnvVal
ev
Maybe EnvVal
Nothing -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"[REPL] getUser" [[Char]
"option `" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"` does not exist"]
setUserDirect :: String -> EnvVal -> REPL ()
setUserDirect :: [Char] -> EnvVal -> REPL ()
setUserDirect [Char]
optName EnvVal
val = do
(RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eUserEnv :: UserEnv
eUserEnv = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert [Char]
optName EnvVal
val (RW -> UserEnv
eUserEnv RW
rw) })
getKnownUser :: IsEnvVal a => String -> REPL a
getKnownUser :: forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
x = forall a. IsEnvVal a => EnvVal -> a
fromEnvVal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> REPL EnvVal
getUser [Char]
x
class IsEnvVal a where
fromEnvVal :: EnvVal -> a
instance IsEnvVal Bool where
fromEnvVal :: EnvVal -> Bool
fromEnvVal EnvVal
x = case EnvVal
x of
EnvBool Bool
b -> Bool
b
EnvVal
_ -> forall a. [Char] -> a
badIsEnv [Char]
"Bool"
instance IsEnvVal Int where
fromEnvVal :: EnvVal -> Int
fromEnvVal EnvVal
x = case EnvVal
x of
EnvNum Int
b -> Int
b
EnvVal
_ -> forall a. [Char] -> a
badIsEnv [Char]
"Num"
instance IsEnvVal (String,[String]) where
fromEnvVal :: EnvVal -> ([Char], [[Char]])
fromEnvVal EnvVal
x = case EnvVal
x of
EnvProg [Char]
b [[Char]]
bs -> ([Char]
b,[[Char]]
bs)
EnvVal
_ -> forall a. [Char] -> a
badIsEnv [Char]
"Prog"
instance IsEnvVal String where
fromEnvVal :: EnvVal -> [Char]
fromEnvVal EnvVal
x = case EnvVal
x of
EnvString [Char]
b -> [Char]
b
EnvVal
_ -> forall a. [Char] -> a
badIsEnv [Char]
"String"
instance IsEnvVal FieldOrder where
fromEnvVal :: EnvVal -> FieldOrder
fromEnvVal EnvVal
x = case EnvVal
x of
EnvString [Char]
s | Just FieldOrder
o <- [Char] -> Maybe FieldOrder
parseFieldOrder [Char]
s
-> FieldOrder
o
EnvVal
_ -> forall a. [Char] -> a
badIsEnv [Char]
"display` or `canonical"
badIsEnv :: String -> a
badIsEnv :: forall a. [Char] -> a
badIsEnv [Char]
x = forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"fromEnvVal" [ [Char]
"[REPL] Expected a `" forall a. [a] -> [a] -> [a]
++ [Char]
x forall a. [a] -> [a] -> [a]
++ [Char]
"` value." ]
getUserShowProverStats :: REPL Bool
getUserShowProverStats :: REPL Bool
getUserShowProverStats = forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"proverStats"
getUserProverValidate :: REPL Bool
getUserProverValidate :: REPL Bool
getUserProverValidate = forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"proverValidate"
type OptionMap = Trie OptionDescr
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OptionMap -> OptionDescr -> OptionMap
insert forall a. Trie a
emptyTrie
where
insert :: OptionMap -> OptionDescr -> OptionMap
insert OptionMap
m OptionDescr
d = forall a. [Char] -> a -> Trie a -> Trie a
insertTrie (OptionDescr -> [Char]
optName OptionDescr
d) OptionDescr
d OptionMap
m
type Checker = EnvVal -> REPL (Maybe String, [String])
noCheck :: Checker
noCheck :: Checker
noCheck EnvVal
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [])
noWarns :: Maybe String -> REPL (Maybe String, [String])
noWarns :: Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns Maybe [Char]
mb = forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char]
mb, [])
data OptionDescr = OptionDescr
{ OptionDescr -> [Char]
optName :: String
, OptionDescr -> [[Char]]
optAliases :: [String]
, OptionDescr -> EnvVal
optDefault :: EnvVal
, OptionDescr -> Checker
optCheck :: Checker
, OptionDescr -> [Char]
optHelp :: String
, OptionDescr -> EnvVal -> REPL ()
optEff :: EnvVal -> REPL ()
}
simpleOpt :: String -> [String] -> EnvVal -> Checker -> String -> OptionDescr
simpleOpt :: [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
optName [[Char]]
optAliases EnvVal
optDefault Checker
optCheck [Char]
optHelp =
OptionDescr { optEff :: EnvVal -> REPL ()
optEff = \ EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (), [Char]
[[Char]]
EnvVal
Checker
optHelp :: [Char]
optCheck :: Checker
optDefault :: EnvVal
optAliases :: [[Char]]
optName :: [Char]
optHelp :: [Char]
optAliases :: [[Char]]
optCheck :: Checker
optDefault :: EnvVal
optName :: [Char]
.. }
userOptionsWithAliases :: OptionMap
userOptionsWithAliases :: OptionMap
userOptionsWithAliases = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OptionMap -> OptionDescr -> OptionMap
insert OptionMap
userOptions (forall a. Trie a -> [a]
leaves OptionMap
userOptions)
where
insert :: OptionMap -> OptionDescr -> OptionMap
insert OptionMap
m OptionDescr
d = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\OptionMap
m' [Char]
n -> forall a. [Char] -> a -> Trie a -> Trie a
insertTrie [Char]
n OptionDescr
d OptionMap
m') OptionMap
m (OptionDescr -> [[Char]]
optAliases OptionDescr
d)
userOptions :: OptionMap
userOptions :: OptionMap
userOptions = [OptionDescr] -> OptionMap
mkOptionMap
[ [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"base" [] (Int -> EnvVal
EnvNum Int
16) Checker
checkBase
[Char]
"The base to display words at (2, 8, 10, or 16)."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"debug" [] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Enable debugging output."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"ascii" [] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Whether to display 7- or 8-bit words using ASCII notation."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"infLength" [[Char]
"inf-length"] (Int -> EnvVal
EnvNum Int
5) Checker
checkInfLength
[Char]
"The number of elements to display for infinite sequences."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"tests" [] (Int -> EnvVal
EnvNum Int
100) Checker
noCheck
[Char]
"The number of random tests to try with ':check'."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"satNum" [[Char]
"sat-num"] ([Char] -> EnvVal
EnvString [Char]
"1") Checker
checkSatNum
[Char]
"The maximum number of :sat solutions to display (\"all\" for no limit)."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"prover" [] ([Char] -> EnvVal
EnvString [Char]
"z3") Checker
checkProver forall a b. (a -> b) -> a -> b
$
[Char]
"The external SMT solver for ':prove' and ':sat'\n(" forall a. [a] -> [a] -> [a]
++ [Char]
proverListString forall a. [a] -> [a] -> [a]
++ [Char]
")."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"warnDefaulting" [[Char]
"warn-defaulting"] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Choose whether to display warnings when defaulting."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"warnShadowing" [[Char]
"warn-shadowing"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Choose whether to display warnings when shadowing symbols."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"warnPrefixAssoc" [[Char]
"warn-prefix-assoc"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Choose whether to display warnings when expression association has changed due to new prefix operator fixities."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"warnUninterp" [[Char]
"warn-uninterp"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"warnNonExhaustiveConstraintGuards" [[Char]
"warn-nonexhaustive-constraintguards"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Choose whether to issue a warning when a use of constraint guards is not determined to be exhaustive."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"smtFile" [[Char]
"smt-file"] ([Char] -> EnvVal
EnvString [Char]
"-") Checker
noCheck
[Char]
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
, [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"path" [] ([Char] -> EnvVal
EnvString [Char]
"") Checker
noCheck
[Char]
"The search path for finding named Cryptol modules." forall a b. (a -> b) -> a -> b
$
\case EnvString [Char]
path ->
do let segs :: [[Char]]
segs = [Char] -> [[Char]]
parseSearchPath [Char]
path
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meSearchPath :: [[Char]]
M.meSearchPath = [[Char]]
segs }
EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
, [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"monoBinds" [[Char]
"mono-binds"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Whether or not to generalize bindings in a 'where' clause." forall a b. (a -> b) -> a -> b
$
\case EnvBool Bool
b -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meMonoBinds :: Bool
M.meMonoBinds = Bool
b }
EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
, [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"tcSolver" [[Char]
"tc-solver"] ([Char] -> [[Char]] -> EnvVal
EnvProg [Char]
"z3" [ [Char]
"-smt2", [Char]
"-in" ])
Checker
noCheck
[Char]
"The solver that will be used by the type checker." forall a b. (a -> b) -> a -> b
$
\case EnvProg [Char]
prog [[Char]]
args -> do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eTCConfig :: SolverConfig
eTCConfig = (RW -> SolverConfig
eTCConfig RW
rw)
{ solverPath :: [Char]
T.solverPath = [Char]
prog
, solverArgs :: [[Char]]
T.solverArgs = [[Char]]
args
}})
REPL ()
resetTCSolver
EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
, [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"tcDebug" [[Char]
"tc-debug"] (Int -> EnvVal
EnvNum Int
0)
Checker
noCheck
([[Char]] -> [Char]
unlines
[ [Char]
"Enable type-checker debugging output:"
, [Char]
" * 0 no debug output"
, [Char]
" * 1 show type-checker debug info"
, [Char]
" * >1 show type-checker debug info and interactions with SMT solver"]) forall a b. (a -> b) -> a -> b
$
\case EnvNum Int
n -> do Bool
changed <- forall a. (RW -> (RW, a)) -> REPL a
modifyRW (\RW
rw -> ( RW
rw{ eTCConfig :: SolverConfig
eTCConfig = (RW -> SolverConfig
eTCConfig RW
rw){ solverVerbose :: Int
T.solverVerbose = Int
n } }
, Int
n forall a. Eq a => a -> a -> Bool
/= SolverConfig -> Int
T.solverVerbose (RW -> SolverConfig
eTCConfig RW
rw)
))
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
changed REPL ()
resetTCSolver
EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
, [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"coreLint" [[Char]
"core-lint"] (Bool -> EnvVal
EnvBool Bool
False)
Checker
noCheck
[Char]
"Enable sanity checking of type-checker." forall a b. (a -> b) -> a -> b
$
let setIt :: CoreLint -> REPL ()
setIt CoreLint
x = do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meCoreLint :: CoreLint
M.meCoreLint = CoreLint
x }
in \case EnvBool Bool
True -> CoreLint -> REPL ()
setIt CoreLint
M.CoreLint
EnvBool Bool
False -> CoreLint -> REPL ()
setIt CoreLint
M.NoCoreLint
EnvVal
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"hashConsing" [[Char]
"hash-consing"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Enable hash-consing in the What4 symbolic backends."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"proverStats" [[Char]
"prover-stats"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Enable prover timing statistics."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"proverValidate" [[Char]
"prover-validate"] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Validate :sat examples and :prove counter-examples for correctness."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"showExamples" [[Char]
"show-examples"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
[Char]
"Print the (counter) example after :sat or :prove"
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"fpBase" [[Char]
"fp-base"] (Int -> EnvVal
EnvNum Int
16) Checker
checkBase
[Char]
"The base to display floating point numbers at (2, 8, 10, or 16)."
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"fpFormat" [[Char]
"fp-format"] ([Char] -> EnvVal
EnvString [Char]
"free") Checker
checkPPFloatFormat
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"Specifies the format to use when showing floating point numbers:"
, [Char]
" * free show using as many digits as needed"
, [Char]
" * free+exp like `free` but always show exponent"
, [Char]
" * .NUM show NUM (>=1) digits after floating point"
, [Char]
" * NUM show using NUM (>=1) significant digits"
, [Char]
" * NUM+exp like NUM but always show exponent"
]
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"ignoreSafety" [[Char]
"ignore-safety"] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Ignore safety predicates when performing :sat or :prove checks"
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"fieldOrder" [[Char]
"field-order"] ([Char] -> EnvVal
EnvString [Char]
"display") Checker
checkFieldOrder
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"The order that record fields are displayed in."
, [Char]
" * display try to match the order they were written in the source code"
, [Char]
" * canonical use a predictable, canonical order"
]
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"timeMeasurementPeriod" [[Char]
"time-measurement-period"] (Int -> EnvVal
EnvNum Int
10)
Checker
checkTimeMeasurementPeriod
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"The period of time in seconds to spend collecting measurements when"
, [Char]
" running :time."
, [Char]
"This is a lower bound and the actual time taken might be higher if the"
, [Char]
" evaluation takes a long time."
]
, [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
simpleOpt [Char]
"timeQuiet" [[Char]
"time-quiet"] (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
[Char]
"Suppress output of :time command and only bind result to `it`."
]
parsePPFloatFormat :: String -> Maybe PPFloatFormat
parsePPFloatFormat :: [Char] -> Maybe PPFloatFormat
parsePPFloatFormat [Char]
s =
case [Char]
s of
[Char]
"free" -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ PPFloatExp -> PPFloatFormat
FloatFree PPFloatExp
AutoExponent
[Char]
"free+exp" -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ PPFloatExp -> PPFloatFormat
FloatFree PPFloatExp
ForceExponent
Char
'.' : [Char]
xs -> Int -> PPFloatFormat
FloatFrac forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
xs
[Char]
_ | ([Char]
as,[Char]
res) <- forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== Char
'+') [Char]
s
, Just Int
n <- forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
as
, Just PPFloatExp
e <- case [Char]
res of
[Char]
"+exp" -> forall a. a -> Maybe a
Just PPFloatExp
ForceExponent
[Char]
"" -> forall a. a -> Maybe a
Just PPFloatExp
AutoExponent
[Char]
_ -> forall a. Maybe a
Nothing
-> forall a. a -> Maybe a
Just (Int -> PPFloatExp -> PPFloatFormat
FloatFixed Int
n PPFloatExp
e)
[Char]
_ -> forall a. Maybe a
Nothing
checkPPFloatFormat :: Checker
checkPPFloatFormat :: Checker
checkPPFloatFormat EnvVal
val =
case EnvVal
val of
EnvString [Char]
s | Just PPFloatFormat
_ <- [Char] -> Maybe PPFloatFormat
parsePPFloatFormat [Char]
s -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"Failed to parse `fp-format`"
parseFieldOrder :: String -> Maybe FieldOrder
parseFieldOrder :: [Char] -> Maybe FieldOrder
parseFieldOrder [Char]
"canonical" = forall a. a -> Maybe a
Just FieldOrder
CanonicalOrder
parseFieldOrder [Char]
"display" = forall a. a -> Maybe a
Just FieldOrder
DisplayOrder
parseFieldOrder [Char]
_ = forall a. Maybe a
Nothing
checkFieldOrder :: Checker
checkFieldOrder :: Checker
checkFieldOrder EnvVal
val =
case EnvVal
val of
EnvString [Char]
s | Just FieldOrder
_ <- [Char] -> Maybe FieldOrder
parseFieldOrder [Char]
s -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"Failed to parse field-order (expected one of \"canonical\" or \"display\")"
checkBase :: Checker
checkBase :: Checker
checkBase EnvVal
val = case EnvVal
val of
EnvNum Int
n
| Int
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
2,Int
8,Int
10,Int
16] -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
| Bool
otherwise -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"base must be 2, 8, 10, or 16"
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"unable to parse a value for base"
checkInfLength :: Checker
checkInfLength :: Checker
checkInfLength EnvVal
val = case EnvVal
val of
EnvNum Int
n
| Int
n forall a. Ord a => a -> a -> Bool
>= Int
0 -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
| Bool
otherwise -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"the number of elements should be positive"
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"unable to parse a value for infLength"
checkProver :: Checker
checkProver :: Checker
checkProver EnvVal
val = case EnvVal
val of
EnvString (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower -> [Char]
s)
| [Char]
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
W4.proverNames ->
forall a. IO a -> REPL a
io ([Char] -> IO (Either [Char] ([[Char]], W4ProverConfig))
W4.setupProver [Char]
s) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left [Char]
msg -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns (forall a. a -> Maybe a
Just [Char]
msg)
Right ([[Char]]
ws, W4ProverConfig
cfg) ->
do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw{ eProverConfig :: Either SBVProverConfig W4ProverConfig
eProverConfig = forall a b. b -> Either a b
Right W4ProverConfig
cfg })
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [[Char]]
ws)
| [Char]
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
SBV.proverNames ->
forall a. IO a -> REPL a
io ([Char] -> IO (Either [Char] ([[Char]], SBVProverConfig))
SBV.setupProver [Char]
s) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left [Char]
msg -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns (forall a. a -> Maybe a
Just [Char]
msg)
Right ([[Char]]
ws, SBVProverConfig
cfg) ->
do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw{ eProverConfig :: Either SBVProverConfig W4ProverConfig
eProverConfig = forall a b. a -> Either a b
Left SBVProverConfig
cfg })
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [[Char]]
ws)
| Bool
otherwise ->
Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Char]
"Prover must be " forall a. [a] -> [a] -> [a]
++ [Char]
proverListString
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"unable to parse a value for prover"
allProvers :: [String]
allProvers :: [[Char]]
allProvers = [[Char]]
SBV.proverNames forall a. [a] -> [a] -> [a]
++ [[Char]]
W4.proverNames
proverListString :: String
proverListString :: [Char]
proverListString = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. [a] -> [a] -> [a]
++ [Char]
", ") (forall a. [a] -> [a]
init [[Char]]
allProvers) forall a. [a] -> [a] -> [a]
++ [Char]
"or " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> a
last [[Char]]
allProvers
checkSatNum :: Checker
checkSatNum :: Checker
checkSatNum EnvVal
val = case EnvVal
val of
EnvString [Char]
"all" -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
EnvString [Char]
s ->
case forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
s :: Maybe Int of
Just Int
n | Int
n forall a. Ord a => a -> a -> Bool
>= Int
1 -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
Maybe Int
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"must be an integer > 0 or \"all\""
EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [Char]
"unable to parse a value for satNum"
getUserSatNum :: REPL SatNum
getUserSatNum :: REPL SatNum
getUserSatNum = do
[Char]
s <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"satNum"
case [Char]
s of
[Char]
"all" -> forall (m :: * -> *) a. Monad m => a -> m a
return SatNum
AllSat
[Char]
_ | Just Int
n <- forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SatNum
SomeSat Int
n)
[Char]
_ -> forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"REPL.Monad.getUserSatNum"
[ [Char]
"invalid satNum option" ]
checkTimeMeasurementPeriod :: Checker
checkTimeMeasurementPeriod :: Checker
checkTimeMeasurementPeriod (EnvNum Int
n)
| Int
n forall a. Ord a => a -> a -> Bool
>= Int
1 = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a. Maybe a
Nothing
| Bool
otherwise = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$
forall a. a -> Maybe a
Just [Char]
"timeMeasurementPeriod must be a positive integer"
checkTimeMeasurementPeriod EnvVal
_ = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns forall a b. (a -> b) -> a -> b
$
forall a. a -> Maybe a
Just [Char]
"unable to parse value for timeMeasurementPeriod"
whenDebug :: REPL () -> REPL ()
whenDebug :: REPL () -> REPL ()
whenDebug REPL ()
m = do
Bool
b <- forall a. IsEnvVal a => [Char] -> REPL a
getKnownUser [Char]
"debug"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b REPL ()
m
smokeTest :: REPL [Smoke]
smokeTest :: REPL [Smoke]
smokeTest = forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SmokeTest]
tests
where
tests :: [SmokeTest]
tests = [ SmokeTest
z3exists ]
type SmokeTest = REPL (Maybe Smoke)
data Smoke
= Z3NotFound
deriving (Int -> Smoke -> ShowS
[Smoke] -> ShowS
Smoke -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Smoke] -> ShowS
$cshowList :: [Smoke] -> ShowS
show :: Smoke -> [Char]
$cshow :: Smoke -> [Char]
showsPrec :: Int -> Smoke -> ShowS
$cshowsPrec :: Int -> Smoke -> ShowS
Show, Smoke -> Smoke -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Smoke -> Smoke -> Bool
$c/= :: Smoke -> Smoke -> Bool
== :: Smoke -> Smoke -> Bool
$c== :: Smoke -> Smoke -> Bool
Eq)
instance PP Smoke where
ppPrec :: Int -> Smoke -> Doc
ppPrec Int
_ Smoke
smoke =
case Smoke
smoke of
Smoke
Z3NotFound -> [Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " forall a b. (a -> b) -> a -> b
$ [
[Char]
"[error] z3 is required to run Cryptol, but was not found in the"
, [Char]
"system path. See the Cryptol README for more on how to install z3."
]
z3exists :: SmokeTest
z3exists :: SmokeTest
z3exists = do
Maybe [Char]
mPath <- forall a. IO a -> REPL a
io forall a b. (a -> b) -> a -> b
$ [Char] -> IO (Maybe [Char])
findExecutable [Char]
"z3"
case Maybe [Char]
mPath of
Maybe [Char]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Smoke
Z3NotFound)
Just [Char]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing