{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
module Cryptol.REPL.Monad (
REPL(..), runREPL
, io
, raise
, stop
, catch
, finally
, rPutStrLn
, rPutStr
, rPrint
, REPLException(..)
, rethrowEvalError
, getFocusedEnv
, getModuleEnv, setModuleEnv
, getDynEnv, setDynEnv
, uniqify, freshName
, getTSyns, getNewtypes, getVars
, whenDebug
, getExprNames
, getTypeNames
, getPropertyNames
, getModNames
, LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
, setEditPath, getEditPath, clearEditPath
, setSearchPath, prependSearchPath
, getPrompt
, shouldContinue
, unlessBatch
, asBatch
, disableLet
, enableLet
, getLetEnabled
, validEvalContext
, updateREPLTitle
, setUpdateREPLTitle
, EnvVal(..)
, OptionDescr(..)
, setUser, getUser, getKnownUser, tryGetUser
, userOptions
, getUserSatNum
, getUserShowProverStats
, getUserProverValidate
, getPutStr
, getLogger
, setPutStr
, smokeTest
, Smoke(..)
) where
import Cryptol.REPL.Trie
import Cryptol.Eval (EvalError)
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.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 (proverNames, lookupProver, SatNum(..))
import Control.Monad (ap,unless,when)
import Control.Monad.Base
import Control.Monad.IO.Class
import Control.Monad.Trans.Control
import Data.Char (isSpace)
import Data.IORef
(IORef,newIORef,readIORef,modifyIORef,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 qualified Control.Exception as X
import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Read (readMaybe)
import Data.SBV.Dynamic (sbvCheckSolverInstallation)
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 FilePath
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
eLetEnabled :: Bool
, RW -> REPL ()
eUpdateTitle :: REPL ()
}
defaultRW :: Bool -> Logger -> IO RW
defaultRW :: Bool -> Logger -> IO RW
defaultRW isBatch :: Bool
isBatch l :: Logger
l = do
ModuleEnv
env <- IO ModuleEnv
M.initialModuleEnv
RW -> IO RW
forall (m :: * -> *) a. Monad m => a -> m a
return RW :: Maybe LoadedModule
-> Maybe FilePath
-> Bool
-> Bool
-> ModuleEnv
-> UserEnv
-> Logger
-> Bool
-> REPL ()
-> RW
RW
{ eLoadedMod :: Maybe LoadedModule
eLoadedMod = Maybe LoadedModule
forall a. Maybe a
Nothing
, eEditFile :: Maybe FilePath
eEditFile = Maybe FilePath
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
, eLetEnabled :: Bool
eLetEnabled = Bool
True
, eUpdateTitle :: REPL ()
eUpdateTitle = () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
mkPrompt :: RW -> String
mkPrompt :: RW -> FilePath
mkPrompt rw :: RW
rw
| RW -> Bool
eIsBatch RW
rw = ""
| Bool
detailedPrompt = FilePath
withEdit FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "> "
| Bool
otherwise = FilePath
modLn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "> "
where
detailedPrompt :: Bool
detailedPrompt = Bool
False
modLn :: FilePath
modLn =
case LoadedModule -> Maybe ModName
lName (LoadedModule -> Maybe ModName)
-> Maybe LoadedModule -> Maybe ModName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< RW -> Maybe LoadedModule
eLoadedMod RW
rw of
Nothing -> Doc -> FilePath
forall a. Show a => a -> FilePath
show (ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
I.preludeName)
Just m :: ModName
m
| ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules (RW -> ModuleEnv
eModuleEnv RW
rw)) ->
FilePath
modName FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "(parameterized)"
| Bool
otherwise -> FilePath
modName
where modName :: FilePath
modName = ModName -> FilePath
forall a. PP a => a -> FilePath
pretty ModName
m
withFocus :: FilePath
withFocus =
case RW -> Maybe LoadedModule
eLoadedMod RW
rw of
Nothing -> FilePath
modLn
Just m :: LoadedModule
m ->
case (LoadedModule -> Maybe ModName
lName LoadedModule
m, LoadedModule -> ModulePath
lPath LoadedModule
m) of
(Nothing, M.InFile f :: FilePath
f) -> ":r to reload " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
modLn
_ -> FilePath
modLn
withEdit :: FilePath
withEdit =
case RW -> Maybe FilePath
eEditFile RW
rw of
Nothing -> FilePath
withFocus
Just e :: FilePath
e
| Just (M.InFile f :: FilePath
f) <- LoadedModule -> ModulePath
lPath (LoadedModule -> ModulePath)
-> Maybe LoadedModule -> Maybe ModulePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RW -> Maybe LoadedModule
eLoadedMod RW
rw
, FilePath
f FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
e -> FilePath
withFocus
| Bool
otherwise -> ":e to edit " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
e FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
withFocus
newtype REPL a = REPL { REPL a -> IORef RW -> IO a
unREPL :: IORef RW -> IO a }
runREPL :: Bool -> Logger -> REPL a -> IO a
runREPL :: Bool -> Logger -> REPL a -> IO a
runREPL isBatch :: Bool
isBatch l :: Logger
l m :: REPL a
m = do
IORef RW
ref <- RW -> IO (IORef RW)
forall a. a -> IO (IORef a)
newIORef (RW -> IO (IORef RW)) -> IO RW -> IO (IORef RW)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Logger -> IO RW
defaultRW Bool
isBatch Logger
l
REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
instance Functor REPL where
{-# INLINE fmap #-}
fmap :: (a -> b) -> REPL a -> REPL b
fmap f :: a -> b
f m :: REPL a
m = (IORef RW -> IO b) -> REPL b
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref))
instance Applicative REPL where
{-# INLINE pure #-}
pure :: a -> REPL a
pure = a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return
{-# INLINE (<*>) #-}
<*> :: REPL (a -> b) -> REPL a -> REPL 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 :: a -> REPL a
return x :: a
x = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\_ -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)
{-# INLINE (>>=) #-}
m :: REPL a
m >>= :: REPL a -> (a -> REPL b) -> REPL b
>>= f :: a -> REPL b
f = (IORef RW -> IO b) -> REPL b
forall a. (IORef RW -> IO a) -> REPL a
REPL ((IORef RW -> IO b) -> REPL b) -> (IORef RW -> IO b) -> REPL b
forall a b. (a -> b) -> a -> b
$ \ref :: IORef RW
ref -> do
a
x <- REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
REPL b -> IORef RW -> IO b
forall a. REPL a -> IORef RW -> IO a
unREPL (a -> REPL b
f a
x) IORef RW
ref
instance MonadIO REPL where
liftIO :: IO a -> REPL a
liftIO = IO a -> REPL a
forall a. IO a -> REPL a
io
instance MonadBase IO REPL where
liftBase :: IO α -> REPL α
liftBase = IO α -> REPL α
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
instance MonadBaseControl IO REPL where
type StM REPL a = a
liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a
liftBaseWith f :: RunInBase REPL IO -> IO a
f = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL ((IORef RW -> IO a) -> REPL a) -> (IORef RW -> IO a) -> REPL a
forall a b. (a -> b) -> a -> b
$ \ref :: IORef RW
ref ->
RunInBase REPL IO -> IO a
f (RunInBase REPL IO -> IO a) -> RunInBase REPL IO -> IO a
forall a b. (a -> b) -> a -> b
$ \m :: REPL a
m -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref
restoreM :: StM REPL a -> REPL a
restoreM x :: StM REPL a
x = a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
StM REPL a
x
instance M.FreshM REPL where
liftSupply :: (Supply -> (a, Supply)) -> REPL a
liftSupply f :: Supply -> (a, Supply)
f = (RW -> (RW, a)) -> REPL a
forall a. (RW -> (RW, a)) -> REPL a
modifyRW ((RW -> (RW, a)) -> REPL a) -> (RW -> (RW, a)) -> REPL a
forall a b. (a -> b) -> a -> b
$ \ RW { .. } ->
let (a :: a
a,s' :: Supply
s') = Supply -> (a, Supply)
f (ModuleEnv -> Supply
M.meSupply ModuleEnv
eModuleEnv)
in (RW :: Maybe LoadedModule
-> Maybe FilePath
-> Bool
-> Bool
-> ModuleEnv
-> UserEnv
-> Logger
-> Bool
-> REPL ()
-> RW
RW { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
eModuleEnv { meSupply :: Supply
M.meSupply = Supply
s' }, .. },a
a)
data REPLException
= ParseError ParseError
| FileNotFound FilePath
| DirectoryNotFound FilePath
| NoPatError [Error]
| NoIncludeError [IncludeError]
| EvalError EvalError
| ModuleSystemError NameDisp M.ModuleError
| EvalPolyError T.Schema
| TypeNotTestable T.Type
| EvalInParamModule [M.Name]
| SBVError String
deriving (Int -> REPLException -> FilePath -> FilePath
[REPLException] -> FilePath -> FilePath
REPLException -> FilePath
(Int -> REPLException -> FilePath -> FilePath)
-> (REPLException -> FilePath)
-> ([REPLException] -> FilePath -> FilePath)
-> Show REPLException
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [REPLException] -> FilePath -> FilePath
$cshowList :: [REPLException] -> FilePath -> FilePath
show :: REPLException -> FilePath
$cshow :: REPLException -> FilePath
showsPrec :: Int -> REPLException -> FilePath -> FilePath
$cshowsPrec :: Int -> REPLException -> FilePath -> FilePath
Show,Typeable)
instance X.Exception REPLException
instance PP REPLException where
ppPrec :: Int -> REPLException -> Doc
ppPrec _ re :: REPLException
re = case REPLException
re of
ParseError e :: ParseError
e -> ParseError -> Doc
ppError ParseError
e
FileNotFound path :: FilePath
path -> [Doc] -> Doc
sep [ FilePath -> Doc
text "File"
, FilePath -> Doc
text ("`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'")
, FilePath -> Doc
text"not found"
]
DirectoryNotFound path :: FilePath
path -> [Doc] -> Doc
sep [ FilePath -> Doc
text "Directory"
, FilePath -> Doc
text ("`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'")
, FilePath -> Doc
text"not found or not a directory"
]
NoPatError es :: [Error]
es -> [Doc] -> Doc
vcat ((Error -> Doc) -> [Error] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Error -> Doc
forall a. PP a => a -> Doc
pp [Error]
es)
NoIncludeError es :: [IncludeError]
es -> [Doc] -> Doc
vcat ((IncludeError -> Doc) -> [IncludeError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IncludeError -> Doc
ppIncludeError [IncludeError]
es)
ModuleSystemError ns :: NameDisp
ns me :: ModuleError
me -> NameDisp -> Doc -> Doc
fixNameDisp NameDisp
ns (ModuleError -> Doc
forall a. PP a => a -> Doc
pp ModuleError
me)
EvalError e :: EvalError
e -> EvalError -> Doc
forall a. PP a => a -> Doc
pp EvalError
e
EvalPolyError s :: Schema
s -> FilePath -> Doc
text "Cannot evaluate polymorphic value."
Doc -> Doc -> Doc
$$ FilePath -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
s
TypeNotTestable t :: Type
t -> FilePath -> Doc
text "The expression is not of a testable type."
Doc -> Doc -> Doc
$$ FilePath -> Doc
text "Type:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
EvalInParamModule xs :: [Name]
xs ->
FilePath -> Doc
text "Expression depends on definitions from a parameterized module:"
Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 ([Doc] -> Doc
vcat ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. PP a => a -> Doc
pp [Name]
xs))
SBVError s :: FilePath
s -> FilePath -> Doc
text "SBV error:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
s
raise :: REPLException -> REPL a
raise :: REPLException -> REPL a
raise exn :: REPLException
exn = IO a -> REPL a
forall a. IO a -> REPL a
io (REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO REPLException
exn)
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
catch m :: REPL a
m k :: REPLException -> REPL a
k = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IO a -> IO a
forall a. IO a -> IO a
rethrowEvalError (REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m IORef RW
ref) IO a -> (REPLException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` \ e :: REPLException
e -> REPL a -> IORef RW -> IO a
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 :: REPL a -> REPL b -> REPL a
finally m1 :: REPL a
m1 m2 :: REPL b
m2 = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ref :: IORef RW
ref -> REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m1 IORef RW
ref IO a -> IO b -> IO a
forall a b. IO a -> IO b -> IO a
`X.finally` REPL b -> IORef RW -> IO b
forall a. REPL a -> IORef RW -> IO a
unREPL REPL b
m2 IORef RW
ref)
rethrowEvalError :: IO a -> IO a
rethrowEvalError :: IO a -> IO a
rethrowEvalError m :: IO a
m = IO a
run IO a -> (EvalError -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`X.catch` EvalError -> IO a
forall a. EvalError -> IO a
rethrow
where
run :: IO a
run = do
a
a <- IO a
m
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IO a) -> a -> IO a
forall a b. (a -> b) -> a -> b
$! a
a
rethrow :: EvalError -> IO a
rethrow :: EvalError -> IO a
rethrow exn :: EvalError
exn = REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (EvalError -> REPLException
EvalError EvalError
exn)
io :: IO a -> REPL a
io :: IO a -> REPL a
io m :: IO a
m = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ _ -> IO a
m)
getRW :: REPL RW
getRW :: REPL RW
getRW = (IORef RW -> IO RW) -> REPL RW
forall a. (IORef RW -> IO a) -> REPL a
REPL IORef RW -> IO RW
forall a. IORef a -> IO a
readIORef
modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW :: (RW -> (RW, a)) -> REPL a
modifyRW f :: RW -> (RW, a)
f = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IORef RW -> (RW -> (RW, a)) -> IO a
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_ f :: RW -> RW
f = (IORef RW -> IO ()) -> REPL ()
forall a. (IORef RW -> IO a) -> REPL a
REPL (\ ref :: IORef RW
ref -> IORef RW -> (RW -> RW) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef RW
ref RW -> RW
f)
getPrompt :: REPL String
getPrompt :: REPL FilePath
getPrompt = RW -> FilePath
mkPrompt (RW -> FilePath) -> REPL RW -> REPL FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
clearLoadedMod :: REPL ()
clearLoadedMod :: REPL ()
clearLoadedMod = do (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> LoadedModule
upd (LoadedModule -> LoadedModule)
-> Maybe LoadedModule -> Maybe LoadedModule
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 x :: LoadedModule
x = LoadedModule
x { lName :: Maybe ModName
lName = Maybe ModName
forall a. Maybe a
Nothing }
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod :: LoadedModule -> REPL ()
setLoadedMod n :: LoadedModule
n = do
(RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> Maybe LoadedModule
forall a. a -> Maybe a
Just LoadedModule
n })
REPL ()
updateREPLTitle
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod :: REPL (Maybe LoadedModule)
getLoadedMod = RW -> Maybe LoadedModule
eLoadedMod (RW -> Maybe LoadedModule) -> REPL RW -> REPL (Maybe LoadedModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setEditPath :: FilePath -> REPL ()
setEditPath :: FilePath -> REPL ()
setEditPath p :: FilePath
p = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eEditFile :: Maybe FilePath
eEditFile = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
p }
getEditPath :: REPL (Maybe FilePath)
getEditPath :: REPL (Maybe FilePath)
getEditPath = RW -> Maybe FilePath
eEditFile (RW -> Maybe FilePath) -> REPL RW -> REPL (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
clearEditPath :: REPL ()
clearEditPath :: REPL ()
clearEditPath = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eEditFile :: Maybe FilePath
eEditFile = Maybe FilePath
forall a. Maybe a
Nothing }
setSearchPath :: [FilePath] -> REPL ()
setSearchPath :: [FilePath] -> REPL ()
setSearchPath path :: [FilePath]
path = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [FilePath]
M.meSearchPath = [FilePath]
path }
prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [FilePath] -> REPL ()
prependSearchPath path :: [FilePath]
path = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
forall a b. (a -> b) -> a -> b
$ ModuleEnv
me { meSearchPath :: [FilePath]
M.meSearchPath = [FilePath]
path [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ ModuleEnv -> [FilePath]
M.meSearchPath ModuleEnv
me }
shouldContinue :: REPL Bool
shouldContinue :: REPL Bool
shouldContinue = RW -> Bool
eContinue (RW -> Bool) -> REPL RW -> REPL Bool
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
rw { eContinue :: Bool
eContinue = Bool
False })
unlessBatch :: REPL () -> REPL ()
unlessBatch :: REPL () -> REPL ()
unlessBatch body :: REPL ()
body = do
RW
rw <- REPL RW
getRW
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RW -> Bool
eIsBatch RW
rw) REPL ()
body
asBatch :: REPL a -> REPL a
asBatch :: REPL a -> REPL a
asBatch body :: REPL a
body = do
Bool
wasBatch <- RW -> Bool
eIsBatch (RW -> Bool) -> REPL RW -> REPL Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
(RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ (\ rw :: RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
True })
a
a <- REPL a
body
(RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ (\ rw :: RW
rw -> RW
rw { eIsBatch :: Bool
eIsBatch = Bool
wasBatch })
a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
disableLet :: REPL ()
disableLet :: REPL ()
disableLet = (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLetEnabled :: Bool
eLetEnabled = Bool
False })
enableLet :: REPL ()
enableLet :: REPL ()
enableLet = (RW -> RW) -> REPL ()
modifyRW_ (\ rw :: RW
rw -> RW
rw { eLetEnabled :: Bool
eLetEnabled = Bool
True })
getLetEnabled :: REPL Bool
getLetEnabled :: REPL Bool
getLetEnabled = (RW -> Bool) -> REPL RW -> REPL Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RW -> Bool
eLetEnabled REPL RW
getRW
validEvalContext :: T.FreeVars a => a -> REPL ()
validEvalContext :: a -> REPL ()
validEvalContext a :: a
a =
do ModuleEnv
me <- RW -> ModuleEnv
eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
let ds :: Deps
ds = a -> Deps
forall e. FreeVars e => e -> Deps
T.freeVars a
a
badVals :: Set Name
badVals = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Set Name -> Set Name
badName Set Name
forall a. Set a
Set.empty (Deps -> Set Name
T.valDeps Deps
ds)
bad :: Set Name
bad = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
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)
badName :: Name -> Set Name -> Set Name
badName nm :: Name
nm bs :: Set Name
bs =
case Name -> NameInfo
M.nameInfo Name
nm of
M.Declared m :: ModName
m _
| ModName -> LoadedModules -> Bool
M.isLoadedParamMod ModName
m (ModuleEnv -> LoadedModules
M.meLoadedModules ModuleEnv
me) -> Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.insert Name
nm Set Name
bs
_ -> Set Name
bs
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
bad) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
REPLException -> REPL ()
forall a. REPLException -> REPL a
raise ([Name] -> REPLException
EvalInParamModule (Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
bad))
updateREPLTitle :: REPL ()
updateREPLTitle :: REPL ()
updateREPLTitle = REPL () -> REPL ()
unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
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 m :: REPL ()
m = (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eUpdateTitle :: REPL ()
eUpdateTitle = REPL ()
m })
setPutStr :: (String -> IO ()) -> REPL ()
setPutStr :: (FilePath -> IO ()) -> REPL ()
setPutStr fn :: FilePath -> IO ()
fn = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \rw :: RW
rw -> RW
rw { eLogger :: Logger
eLogger = (FilePath -> IO ()) -> Logger
funLogger FilePath -> IO ()
fn }
getPutStr :: REPL (String -> IO ())
getPutStr :: REPL (FilePath -> IO ())
getPutStr =
do RW
rw <- REPL RW
getRW
(FilePath -> IO ()) -> REPL (FilePath -> IO ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Logger -> FilePath -> IO ()
logPutStr (RW -> Logger
eLogger RW
rw))
getLogger :: REPL Logger
getLogger :: REPL Logger
getLogger = RW -> Logger
eLogger (RW -> Logger) -> REPL RW -> REPL Logger
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
rPutStr :: String -> REPL ()
rPutStr :: FilePath -> REPL ()
rPutStr str :: FilePath
str = do
FilePath -> IO ()
f <- REPL (FilePath -> IO ())
getPutStr
IO () -> REPL ()
forall a. IO a -> REPL a
io (FilePath -> IO ()
f FilePath
str)
rPutStrLn :: String -> REPL ()
rPutStrLn :: FilePath -> REPL ()
rPutStrLn str :: FilePath
str = FilePath -> REPL ()
rPutStr (FilePath -> REPL ()) -> FilePath -> REPL ()
forall a b. (a -> b) -> a -> b
$ FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"
rPrint :: Show a => a -> REPL ()
rPrint :: a -> REPL ()
rPrint x :: a
x = FilePath -> REPL ()
rPutStrLn (a -> FilePath
forall a. Show a => a -> FilePath
show a
x)
getFocusedEnv :: REPL (M.IfaceParams,M.IfaceDecls,M.NamingEnv,NameDisp)
getFocusedEnv :: REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
let (dyDecls :: IfaceDecls
dyDecls,dyNames :: NamingEnv
dyNames,dyDisp :: NameDisp
dyDisp) = ModuleEnv -> (IfaceDecls, NamingEnv, NameDisp)
M.dynamicEnv ModuleEnv
me
let (fParams :: IfaceParams
fParams,fDecls :: IfaceDecls
fDecls,fNames :: NamingEnv
fNames,fDisp :: NameDisp
fDisp) = ModuleEnv -> (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
M.focusedEnv ModuleEnv
me
(IfaceParams, IfaceDecls, NamingEnv, NameDisp)
-> REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
forall (m :: * -> *) a. Monad m => a -> m a
return ( IfaceParams
fParams
, IfaceDecls
dyDecls IfaceDecls -> IfaceDecls -> IfaceDecls
forall a. Monoid a => a -> a -> a
`mappend` IfaceDecls
fDecls
, NamingEnv
dyNames NamingEnv -> NamingEnv -> NamingEnv
`M.shadowing` NamingEnv
fNames
, NameDisp
dyDisp NameDisp -> NameDisp -> NameDisp
forall a. Monoid a => a -> a -> a
`mappend` NameDisp
fDisp)
getVars :: REPL (Map.Map M.Name M.IfaceDecl)
getVars :: REPL (Map Name IfaceDecl)
getVars = do
(_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
Map Name IfaceDecl -> REPL (Map Name IfaceDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name IfaceDecl
M.ifDecls IfaceDecls
decls)
getTSyns :: REPL (Map.Map M.Name T.TySyn)
getTSyns :: REPL (Map Name TySyn)
getTSyns = do
(_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
Map Name TySyn -> REPL (Map Name TySyn)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name TySyn
M.ifTySyns IfaceDecls
decls)
getNewtypes :: REPL (Map.Map M.Name T.Newtype)
getNewtypes :: REPL (Map Name Newtype)
getNewtypes = do
(_,decls :: IfaceDecls
decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
Map Name Newtype -> REPL (Map Name Newtype)
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceDecls -> Map Name Newtype
M.ifNewtypes IfaceDecls
decls)
getExprNames :: REPL [String]
getExprNames :: REPL [FilePath]
getExprNames =
do (_,_, fNames :: NamingEnv
fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
[FilePath] -> REPL [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ((PName -> FilePath) -> [PName] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PName -> Doc
forall a. PP a => a -> Doc
pp) (Map PName [Name] -> [PName]
forall k a. Map k a -> [k]
Map.keys (NamingEnv -> Map PName [Name]
M.neExprs NamingEnv
fNames)))
getTypeNames :: REPL [String]
getTypeNames :: REPL [FilePath]
getTypeNames =
do (_,_, fNames :: NamingEnv
fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
[FilePath] -> REPL [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ((PName -> FilePath) -> [PName] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PName -> Doc
forall a. PP a => a -> Doc
pp) (Map PName [Name] -> [PName]
forall k a. Map k a -> [k]
Map.keys (NamingEnv -> Map PName [Name]
M.neTypes NamingEnv
fNames)))
getPropertyNames :: REPL ([M.Name],NameDisp)
getPropertyNames :: REPL ([Name], NameDisp)
getPropertyNames =
do (_,decls :: IfaceDecls
decls,_,names :: NameDisp
names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
getFocusedEnv
let xs :: Map Name IfaceDecl
xs = IfaceDecls -> Map Name IfaceDecl
M.ifDecls IfaceDecls
decls
ps :: [Name]
ps = (Name -> Name -> Ordering) -> [Name] -> [Name]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Name -> Position) -> Name -> Name -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Range -> Position
from (Range -> Position) -> (Name -> Range) -> Name -> Position
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
M.nameLoc))
([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [ Name
x | (x :: Name
x,d :: IfaceDecl
d) <- Map Name IfaceDecl -> [(Name, IfaceDecl)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name IfaceDecl
xs, Pragma
T.PragmaProperty Pragma -> [Pragma] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IfaceDecl -> [Pragma]
M.ifDeclPragmas IfaceDecl
d ]
([Name], NameDisp) -> REPL ([Name], NameDisp)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ps, NameDisp
names)
getModNames :: REPL [I.ModName]
getModNames :: REPL [ModName]
getModNames =
do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
[ModName] -> REPL [ModName]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Module -> ModName) -> [Module] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map Module -> ModName
T.mName (ModuleEnv -> [Module]
M.loadedModules ModuleEnv
me))
getModuleEnv :: REPL M.ModuleEnv
getModuleEnv :: REPL ModuleEnv
getModuleEnv = RW -> ModuleEnv
eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setModuleEnv :: M.ModuleEnv -> REPL ()
setModuleEnv :: ModuleEnv -> REPL ()
setModuleEnv me :: ModuleEnv
me = (RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
me })
getDynEnv :: REPL M.DynamicEnv
getDynEnv :: REPL DynamicEnv
getDynEnv = (ModuleEnv -> DynamicEnv
M.meDynEnv (ModuleEnv -> DynamicEnv) -> (RW -> ModuleEnv) -> RW -> DynamicEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> ModuleEnv
eModuleEnv) (RW -> DynamicEnv) -> REPL RW -> REPL DynamicEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW
setDynEnv :: M.DynamicEnv -> REPL ()
setDynEnv :: DynamicEnv -> REPL ()
setDynEnv denv :: DynamicEnv
denv = do
ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv (ModuleEnv
me { meDynEnv :: DynamicEnv
M.meDynEnv = DynamicEnv
denv })
uniqify :: M.Name -> REPL M.Name
uniqify :: Name -> REPL Name
uniqify name :: Name
name =
case Name -> NameInfo
M.nameInfo Name
name of
M.Declared ns :: ModName
ns s :: NameSource
s ->
(Supply -> (Name, Supply)) -> REPL Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared ModName
ns NameSource
s (Name -> Ident
M.nameIdent Name
name) (Name -> Maybe Fixity
M.nameFixity Name
name) (Name -> Range
M.nameLoc Name
name))
M.Parameter ->
FilePath -> [FilePath] -> REPL Name
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "[REPL] uniqify" ["tried to uniqify a parameter: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. PP a => a -> FilePath
pretty Name
name]
freshName :: I.Ident -> M.NameSource -> REPL M.Name
freshName :: Ident -> NameSource -> REPL Name
freshName i :: Ident
i sys :: NameSource
sys =
(Supply -> (Name, Supply)) -> REPL Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared ModName
I.interactiveName NameSource
sys Ident
i Maybe Fixity
forall a. Maybe a
Nothing Range
emptyRange)
type UserEnv = Map.Map String EnvVal
data EnvVal
= EnvString String
| EnvProg String [String]
| EnvNum !Int
| EnvBool Bool
deriving (Int -> EnvVal -> FilePath -> FilePath
[EnvVal] -> FilePath -> FilePath
EnvVal -> FilePath
(Int -> EnvVal -> FilePath -> FilePath)
-> (EnvVal -> FilePath)
-> ([EnvVal] -> FilePath -> FilePath)
-> Show EnvVal
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [EnvVal] -> FilePath -> FilePath
$cshowList :: [EnvVal] -> FilePath -> FilePath
show :: EnvVal -> FilePath
$cshow :: EnvVal -> FilePath
showsPrec :: Int -> EnvVal -> FilePath -> FilePath
$cshowsPrec :: Int -> EnvVal -> FilePath -> FilePath
Show)
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv :: OptionMap -> UserEnv
mkUserEnv opts :: OptionMap
opts = [(FilePath, EnvVal)] -> UserEnv
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(FilePath, EnvVal)] -> UserEnv)
-> [(FilePath, EnvVal)] -> UserEnv
forall a b. (a -> b) -> a -> b
$ do
OptionDescr
opt <- OptionMap -> [OptionDescr]
forall a. Trie a -> [a]
leaves OptionMap
opts
(FilePath, EnvVal) -> [(FilePath, EnvVal)]
forall (m :: * -> *) a. Monad m => a -> m a
return (OptionDescr -> FilePath
optName OptionDescr
opt, OptionDescr -> EnvVal
optDefault OptionDescr
opt)
setUser :: String -> String -> REPL ()
setUser :: FilePath -> FilePath -> REPL ()
setUser name :: FilePath
name val :: FilePath
val = case FilePath -> OptionMap -> [OptionDescr]
forall a. FilePath -> Trie a -> [a]
lookupTrieExact FilePath
name OptionMap
userOptions of
[opt :: OptionDescr
opt] -> OptionDescr -> REPL ()
setUserOpt OptionDescr
opt
[] -> FilePath -> REPL ()
rPutStrLn ("Unknown env value `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
_ -> FilePath -> REPL ()
rPutStrLn ("Ambiguous env value `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
where
setUserOpt :: OptionDescr -> REPL ()
setUserOpt opt :: OptionDescr
opt = case OptionDescr -> EnvVal
optDefault OptionDescr
opt of
EnvString _ -> EnvVal -> REPL ()
doCheck (FilePath -> EnvVal
EnvString FilePath
val)
EnvProg _ _ ->
case FilePath -> [FilePath]
splitOptArgs FilePath
val of
prog :: FilePath
prog:args :: [FilePath]
args -> EnvVal -> REPL ()
doCheck (FilePath -> [FilePath] -> EnvVal
EnvProg FilePath
prog [FilePath]
args)
[] -> FilePath -> REPL ()
rPutStrLn ("Failed to parse command for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
EnvNum _ -> case ReadS Int
forall a. Read a => ReadS a
reads FilePath
val of
[(x :: Int
x,_)] -> EnvVal -> REPL ()
doCheck (Int -> EnvVal
EnvNum Int
x)
_ -> FilePath -> REPL ()
rPutStrLn ("Failed to parse number for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
EnvBool _
| (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
val) ["enable", "on", "yes", "true"] ->
EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
True)
| (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
val) ["disable", "off", "no", "false"] ->
EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
False)
| Bool
otherwise ->
FilePath -> REPL ()
rPutStrLn ("Failed to parse boolean for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "`")
where
doCheck :: EnvVal -> REPL ()
doCheck v :: EnvVal
v = do (r :: Maybe FilePath
r,ws :: [FilePath]
ws) <- IO (Maybe FilePath, [FilePath])
-> REPL (Maybe FilePath, [FilePath])
forall a. IO a -> REPL a
io (OptionDescr -> Checker
optCheck OptionDescr
opt EnvVal
v)
case Maybe FilePath
r of
Just err :: FilePath
err -> FilePath -> REPL ()
rPutStrLn FilePath
err
Nothing -> do (FilePath -> REPL ()) -> [FilePath] -> REPL ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> REPL ()
rPutStrLn [FilePath]
ws
EnvVal -> REPL ()
writeEnv EnvVal
v
writeEnv :: EnvVal -> REPL ()
writeEnv ev :: EnvVal
ev =
do OptionDescr -> EnvVal -> REPL ()
optEff OptionDescr
opt EnvVal
ev
(RW -> RW) -> REPL ()
modifyRW_ (\rw :: RW
rw -> RW
rw { eUserEnv :: UserEnv
eUserEnv = FilePath -> EnvVal -> UserEnv -> UserEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OptionDescr -> FilePath
optName OptionDescr
opt) EnvVal
ev (RW -> UserEnv
eUserEnv RW
rw) })
splitOptArgs :: String -> [String]
splitOptArgs :: FilePath -> [FilePath]
splitOptArgs = (FilePath -> Maybe (FilePath, FilePath)) -> FilePath -> [FilePath]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse "")
where
parse :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse acc :: FilePath
acc (c :: Char
c:cs :: FilePath
cs) | Char -> Bool
isQuote Char
c = FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
| Bool -> Bool
not (Char -> Bool
isSpace Char
c) = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
| Bool
otherwise = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc FilePath
cs
parse acc :: FilePath
acc [] = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc []
quoted :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted acc :: FilePath
acc (c :: Char
c:cs :: FilePath
cs) | Char -> Bool
isQuote Char
c = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
| Bool
otherwise = FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted (Char
cChar -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
acc) FilePath
cs
quoted acc :: FilePath
acc [] = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc []
result :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
result [] [] = Maybe (FilePath, FilePath)
forall a. Maybe a
Nothing
result [] cs :: FilePath
cs = FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse [] ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
cs)
result acc :: FilePath
acc cs :: FilePath
cs = (FilePath, FilePath) -> Maybe (FilePath, FilePath)
forall a. a -> Maybe a
Just (FilePath -> FilePath
forall a. [a] -> [a]
reverse FilePath
acc, (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
cs)
isQuote :: Char -> Bool
isQuote :: Char -> Bool
isQuote c :: Char
c = Char
c Char -> FilePath -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ("'\"" :: String)
tryGetUser :: String -> REPL (Maybe EnvVal)
tryGetUser :: FilePath -> REPL (Maybe EnvVal)
tryGetUser name :: FilePath
name = do
RW
rw <- REPL RW
getRW
Maybe EnvVal -> REPL (Maybe EnvVal)
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> UserEnv -> Maybe EnvVal
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
name (RW -> UserEnv
eUserEnv RW
rw))
getUser :: String -> REPL EnvVal
getUser :: FilePath -> REPL EnvVal
getUser name :: FilePath
name = do
Maybe EnvVal
mb <- FilePath -> REPL (Maybe EnvVal)
tryGetUser FilePath
name
case Maybe EnvVal
mb of
Just ev :: EnvVal
ev -> EnvVal -> REPL EnvVal
forall (m :: * -> *) a. Monad m => a -> m a
return EnvVal
ev
Nothing -> FilePath -> [FilePath] -> REPL EnvVal
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "[REPL] getUser" ["option `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "` does not exist"]
getKnownUser :: IsEnvVal a => String -> REPL a
getKnownUser :: FilePath -> REPL a
getKnownUser x :: FilePath
x = EnvVal -> a
forall a. IsEnvVal a => EnvVal -> a
fromEnvVal (EnvVal -> a) -> REPL EnvVal -> REPL a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> REPL EnvVal
getUser FilePath
x
class IsEnvVal a where
fromEnvVal :: EnvVal -> a
instance IsEnvVal Bool where
fromEnvVal :: EnvVal -> Bool
fromEnvVal x :: EnvVal
x = case EnvVal
x of
EnvBool b :: Bool
b -> Bool
b
_ -> FilePath -> Bool
forall a. FilePath -> a
badIsEnv "Bool"
instance IsEnvVal Int where
fromEnvVal :: EnvVal -> Int
fromEnvVal x :: EnvVal
x = case EnvVal
x of
EnvNum b :: Int
b -> Int
b
_ -> FilePath -> Int
forall a. FilePath -> a
badIsEnv "Num"
instance IsEnvVal (String,[String]) where
fromEnvVal :: EnvVal -> (FilePath, [FilePath])
fromEnvVal x :: EnvVal
x = case EnvVal
x of
EnvProg b :: FilePath
b bs :: [FilePath]
bs -> (FilePath
b,[FilePath]
bs)
_ -> FilePath -> (FilePath, [FilePath])
forall a. FilePath -> a
badIsEnv "Prog"
instance IsEnvVal String where
fromEnvVal :: EnvVal -> FilePath
fromEnvVal x :: EnvVal
x = case EnvVal
x of
EnvString b :: FilePath
b -> FilePath
b
_ -> FilePath -> FilePath
forall a. FilePath -> a
badIsEnv "String"
badIsEnv :: String -> a
badIsEnv :: FilePath -> a
badIsEnv x :: FilePath
x = FilePath -> [FilePath] -> a
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "fromEnvVal" [ "[REPL] Expected a `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "` value." ]
getUserShowProverStats :: REPL Bool
getUserShowProverStats :: REPL Bool
getUserShowProverStats = FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "prover-stats"
getUserProverValidate :: REPL Bool
getUserProverValidate :: REPL Bool
getUserProverValidate = FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "prover-validate"
type OptionMap = Trie OptionDescr
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap :: [OptionDescr] -> OptionMap
mkOptionMap = (OptionMap -> OptionDescr -> OptionMap)
-> OptionMap -> [OptionDescr] -> OptionMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OptionMap -> OptionDescr -> OptionMap
insert OptionMap
forall a. Trie a
emptyTrie
where
insert :: OptionMap -> OptionDescr -> OptionMap
insert m :: OptionMap
m d :: OptionDescr
d = FilePath -> OptionDescr -> OptionMap -> OptionMap
forall a. FilePath -> a -> Trie a -> Trie a
insertTrie (OptionDescr -> FilePath
optName OptionDescr
d) OptionDescr
d OptionMap
m
type Checker = EnvVal -> IO (Maybe String, [String])
noCheck :: Checker
noCheck :: Checker
noCheck _ = (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [])
noWarns :: Maybe String -> IO (Maybe String, [String])
noWarns :: Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns mb :: Maybe FilePath
mb = (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
mb, [])
data OptionDescr = OptionDescr
{ OptionDescr -> FilePath
optName :: String
, OptionDescr -> EnvVal
optDefault :: EnvVal
, OptionDescr -> Checker
optCheck :: Checker
, OptionDescr -> FilePath
optHelp :: String
, OptionDescr -> EnvVal -> REPL ()
optEff :: EnvVal -> REPL ()
}
simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
simpleOpt :: FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt optName :: FilePath
optName optDefault :: EnvVal
optDefault optCheck :: Checker
optCheck optHelp :: FilePath
optHelp =
OptionDescr :: FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr { optEff :: EnvVal -> REPL ()
optEff = \ _ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return (), .. }
userOptions :: OptionMap
userOptions :: OptionMap
userOptions = [OptionDescr] -> OptionMap
mkOptionMap
[ FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "base" (Int -> EnvVal
EnvNum 16) Checker
checkBase
"The base to display words at (2, 8, 10, or 16)."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "debug" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
"Enable debugging output."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "ascii" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
"Whether to display 7- or 8-bit words using ASCII notation."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "infLength" (Int -> EnvVal
EnvNum 5) Checker
checkInfLength
"The number of elements to display for infinite sequences."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "tests" (Int -> EnvVal
EnvNum 100) Checker
noCheck
"The number of random tests to try with ':check'."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "satNum" (FilePath -> EnvVal
EnvString "1") Checker
checkSatNum
"The maximum number of :sat solutions to display (\"all\" for no limit)."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover" (FilePath -> EnvVal
EnvString "z3") Checker
checkProver (FilePath -> OptionDescr) -> FilePath -> OptionDescr
forall a b. (a -> b) -> a -> b
$
"The external SMT solver for ':prove' and ':sat'\n(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
proverListString FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "warnDefaulting" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
"Choose whether to display warnings when defaulting."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "warnShadowing" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
"Choose whether to display warnings when shadowing symbols."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "smtfile" (FilePath -> EnvVal
EnvString "-") Checker
noCheck
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
, FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "mono-binds" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
"Whether or not to generalize bindings in a 'where' clause." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
\case EnvBool b :: Bool
b -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meMonoBinds :: Bool
M.meMonoBinds = Bool
b }
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "tc-solver" (FilePath -> [FilePath] -> EnvVal
EnvProg "z3" [ "-smt2", "-in" ])
Checker
noCheck
"The solver that will be used by the type checker." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
\case EnvProg prog :: FilePath
prog args :: [FilePath]
args -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
let cfg :: SolverConfig
cfg = ModuleEnv -> SolverConfig
M.meSolverConfig ModuleEnv
me
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meSolverConfig :: SolverConfig
M.meSolverConfig =
SolverConfig
cfg { solverPath :: FilePath
T.solverPath = FilePath
prog
, solverArgs :: [FilePath]
T.solverArgs = [FilePath]
args } }
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "tc-debug" (Int -> EnvVal
EnvNum 0)
Checker
noCheck
"Enable type-checker debugging output." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
\case EnvNum n :: Int
n -> do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
let cfg :: SolverConfig
cfg = ModuleEnv -> SolverConfig
M.meSolverConfig ModuleEnv
me
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meSolverConfig :: SolverConfig
M.meSolverConfig = SolverConfig
cfg{ solverVerbose :: Int
T.solverVerbose = Int
n } }
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr "core-lint" (Bool -> EnvVal
EnvBool Bool
False)
Checker
noCheck
"Enable sanity checking of type-checker." ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
let setIt :: CoreLint -> REPL ()
setIt x :: CoreLint
x = do ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { meCoreLint :: CoreLint
M.meCoreLint = CoreLint
x }
in \case EnvBool True -> CoreLint -> REPL ()
setIt CoreLint
M.CoreLint
EnvBool False -> CoreLint -> REPL ()
setIt CoreLint
M.NoCoreLint
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover-stats" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
"Enable prover timing statistics."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "prover-validate" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
"Validate :sat examples and :prove counter-examples for correctness."
, FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt "show-examples" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
"Print the (counter) example after :sat or :prove"
]
checkBase :: Checker
checkBase :: Checker
checkBase val :: EnvVal
val = case EnvVal
val of
EnvNum n :: Int
n
| Int
n Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [2,8,10,16] -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
| Bool
otherwise -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "base must be 2, 8, 10, or 16"
_ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for base"
checkInfLength :: Checker
checkInfLength :: Checker
checkInfLength val :: EnvVal
val = case EnvVal
val of
EnvNum n :: Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
| Bool
otherwise -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "the number of elements should be positive"
_ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for infLength"
checkProver :: Checker
checkProver :: Checker
checkProver val :: EnvVal
val = case EnvVal
val of
EnvString s :: FilePath
s
| FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [FilePath]
proverNames ->
Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ "Prover must be " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
proverListString
| FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ["offline", "any"] -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
| Bool
otherwise ->
do let prover :: SMTConfig
prover = FilePath -> SMTConfig
lookupProver FilePath
s
Bool
available <- SMTConfig -> IO Bool
sbvCheckSolverInstallation SMTConfig
prover
let ws :: [FilePath]
ws = if Bool
available
then []
else ["Warning: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " installation not found"]
(Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [FilePath]
ws)
_ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for prover"
proverListString :: String
proverListString :: FilePath
proverListString = (FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ", ") ([FilePath] -> [FilePath]
forall a. [a] -> [a]
init [FilePath]
proverNames) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "or " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. [a] -> a
last [FilePath]
proverNames
checkSatNum :: Checker
checkSatNum :: Checker
checkSatNum val :: EnvVal
val = case EnvVal
val of
EnvString "all" -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
EnvString s :: FilePath
s ->
case FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s :: Maybe Int of
Just n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 1 -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
_ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "must be an integer > 0 or \"all\""
_ -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just "unable to parse a value for satNum"
getUserSatNum :: REPL SatNum
getUserSatNum :: REPL SatNum
getUserSatNum = do
FilePath
s <- FilePath -> REPL FilePath
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "satNum"
case FilePath
s of
"all" -> SatNum -> REPL SatNum
forall (m :: * -> *) a. Monad m => a -> m a
return SatNum
AllSat
_ | Just n :: Int
n <- FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s -> SatNum -> REPL SatNum
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SatNum
SomeSat Int
n)
_ -> FilePath -> [FilePath] -> REPL SatNum
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "REPL.Monad.getUserSatNum"
[ "invalid satNum option" ]
whenDebug :: REPL () -> REPL ()
whenDebug :: REPL () -> REPL ()
whenDebug m :: REPL ()
m = do
Bool
b <- FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser "debug"
Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b REPL ()
m
smokeTest :: REPL [Smoke]
smokeTest :: REPL [Smoke]
smokeTest = [Maybe Smoke] -> [Smoke]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Smoke] -> [Smoke]) -> REPL [Maybe Smoke] -> REPL [Smoke]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [REPL (Maybe Smoke)] -> REPL [Maybe Smoke]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [REPL (Maybe Smoke)]
tests
where
tests :: [REPL (Maybe Smoke)]
tests = [ REPL (Maybe Smoke)
z3exists ]
type SmokeTest = REPL (Maybe Smoke)
data Smoke
= Z3NotFound
deriving (Int -> Smoke -> FilePath -> FilePath
[Smoke] -> FilePath -> FilePath
Smoke -> FilePath
(Int -> Smoke -> FilePath -> FilePath)
-> (Smoke -> FilePath)
-> ([Smoke] -> FilePath -> FilePath)
-> Show Smoke
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [Smoke] -> FilePath -> FilePath
$cshowList :: [Smoke] -> FilePath -> FilePath
show :: Smoke -> FilePath
$cshow :: Smoke -> FilePath
showsPrec :: Int -> Smoke -> FilePath -> FilePath
$cshowsPrec :: Int -> Smoke -> FilePath -> FilePath
Show, Smoke -> Smoke -> Bool
(Smoke -> Smoke -> Bool) -> (Smoke -> Smoke -> Bool) -> Eq Smoke
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 _ smoke :: Smoke
smoke =
case Smoke
smoke of
Z3NotFound -> FilePath -> Doc
text (FilePath -> Doc) -> ([FilePath] -> FilePath) -> [FilePath] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate " " ([FilePath] -> Doc) -> [FilePath] -> Doc
forall a b. (a -> b) -> a -> b
$ [
"[error] z3 is required to run Cryptol, but was not found in the"
, "system path. See the Cryptol README for more on how to install z3."
]
z3exists :: SmokeTest
z3exists :: REPL (Maybe Smoke)
z3exists = do
Maybe FilePath
mPath <- IO (Maybe FilePath) -> REPL (Maybe FilePath)
forall a. IO a -> REPL a
io (IO (Maybe FilePath) -> REPL (Maybe FilePath))
-> IO (Maybe FilePath) -> REPL (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> IO (Maybe FilePath)
findExecutable "z3"
case Maybe FilePath
mPath of
Nothing -> Maybe Smoke -> REPL (Maybe Smoke)
forall (m :: * -> *) a. Monad m => a -> m a
return (Smoke -> Maybe Smoke
forall a. a -> Maybe a
Just Smoke
Z3NotFound)
Just _ -> Maybe Smoke -> REPL (Maybe Smoke)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Smoke
forall a. Maybe a
Nothing