Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Cryptol.REPL.Monad

Contents

REPL Monad

Description

Synopsis

newtype REPL a = REPL {
- unREPL :: IORef RW -> IO a
}
runREPL :: Bool -> Bool -> Logger -> REPL a -> IO a
io :: IO a -> REPL a
raise :: REPLException -> REPL a
stop :: REPL ()
catch :: REPL a -> (REPLException -> REPL a) -> REPL a
try :: REPL a -> REPL (Either REPLException a)
finally :: REPL a -> REPL b -> REPL a
rPutStrLn :: String -> REPL ()
rPutStr :: String -> REPL ()
rPrint :: Show a => a -> REPL ()
data REPLException
- = ParseError ParseError
- | FileNotFound FilePath
- | DirectoryNotFound FilePath
- | NoPatError [Error]
- | NoIncludeError [IncludeError]
- | EvalError EvalErrorEx
- | TooWide WordTooWide
- | Unsupported Unsupported
- | ModuleSystemError NameDisp ModuleError
- | EvalPolyError Schema
- | InstantiationsNotFound Schema
- | TypeNotTestable Type
- | EvalInParamModule [TParam] [Name]
- | SBVError String
- | SBVException SBVException
- | SBVPortfolioException SBVPortfolioException
- | W4Exception W4Exception
rethrowEvalError :: IO a -> IO a
getFocusedEnv :: REPL ModContext
getModuleEnv :: REPL ModuleEnv
setModuleEnv :: ModuleEnv -> REPL ()
getDynEnv :: REPL DynamicEnv
setDynEnv :: DynamicEnv -> REPL ()
getCallStacks :: REPL Bool
getTCSolver :: REPL Solver
resetTCSolver :: REPL ()
uniqify :: Name -> REPL Name
freshName :: Ident -> NameSource -> REPL Name
whenDebug :: REPL () -> REPL ()
getEvalOptsAction :: REPL (IO EvalOpts)
getPPValOpts :: REPL PPOpts
getExprNames :: REPL [String]
getTypeNames :: REPL [String]
getPropertyNames :: REPL ([(Name, Decl)], NameDisp)
getModNames :: REPL [ModName]
data LoadedModule = LoadedModule {
- lFocus :: Maybe (ImpName Name)
- lPath :: ModulePath
}
lName :: LoadedModule -> Maybe ModName
getLoadedMod :: REPL (Maybe LoadedModule)
setLoadedMod :: LoadedModule -> REPL ()
clearLoadedMod :: REPL ()
setEditPath :: FilePath -> REPL ()
getEditPath :: REPL (Maybe FilePath)
clearEditPath :: REPL ()
setSearchPath :: [FilePath] -> REPL ()
prependSearchPath :: [FilePath] -> REPL ()
getPrompt :: REPL String
shouldContinue :: REPL Bool
unlessBatch :: REPL () -> REPL ()
asBatch :: REPL a -> REPL a
validEvalContext :: FreeVars a => a -> REPL ()
updateREPLTitle :: REPL ()
isolated :: REPL a -> REPL a
setUpdateREPLTitle :: REPL () -> REPL ()
withRandomGen :: (TFGen -> REPL (a, TFGen)) -> REPL a
setRandomGen :: TFGen -> REPL ()
getRandomGen :: REPL TFGen
getModuleInput :: REPL (ModuleInput IO)
data EnvVal
- = EnvString String
- | EnvProg String [String]
- | EnvNum !Int
- | EnvBool Bool
data OptionDescr = OptionDescr {
- optName :: String
- optAliases :: [String]
- optDefault :: EnvVal
- optCheck :: Checker
- optHelp :: String
- optEff :: EnvVal -> REPL ()
}
setUser :: String -> String -> REPL Bool
getUser :: String -> REPL EnvVal
getKnownUser :: IsEnvVal a => String -> REPL a
tryGetUser :: String -> REPL (Maybe EnvVal)
userOptions :: OptionMap
userOptionsWithAliases :: OptionMap
getUserSatNum :: REPL SatNum
getUserShowProverStats :: REPL Bool
getUserProverValidate :: REPL Bool
parsePPFloatFormat :: String -> Maybe PPFloatFormat
parseFieldOrder :: String -> Maybe FieldOrder
getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)
parseSearchPath :: String -> [String]
getPutStr :: REPL (String -> IO ())
getLogger :: REPL Logger
setLogger :: Logger -> REPL ()
setPutStr :: (String -> IO ()) -> REPL ()
smokeTest :: REPL [Smoke]
data Smoke = Z3NotFound
data RW = RW {
- eLoadedMod :: Maybe LoadedModule
- eEditFile :: Maybe FilePath
- eContinue :: Bool
- eIsBatch :: Bool
- eModuleEnv :: ModuleEnv
- eUserEnv :: UserEnv
- eLogger :: Logger
- eCallStacks :: Bool
- eUpdateTitle :: REPL ()
- eProverConfig :: Either SBVProverConfig W4ProverConfig
- eTCConfig :: SolverConfig
- eTCSolver :: Maybe Solver
- eTCSolverRestarts :: !Int
- eRandomGen :: TFGen
}
defaultRW :: Bool -> Bool -> Logger -> IO RW
mkUserEnv :: OptionMap -> UserEnv

REPL Monad

newtype REPL a Source #

REPL_ context with InputT handling.

Constructors

REPL
Fields unREPL :: IORef RW -> IO a

Instances

Instances details

MonadIO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftIO :: IO a -> REPL a #
Applicative REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods pure :: a -> REPL a # (<>) :: REPL (a -> b) -> REPL a -> REPL b # liftA2 :: (a -> b -> c) -> REPL a -> REPL b -> REPL c # (>) :: REPL a -> REPL b -> REPL b # (<*) :: REPL a -> REPL b -> REPL a #
Functor REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods fmap :: (a -> b) -> REPL a -> REPL b # (<$) :: a -> REPL b -> REPL a #
Monad REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods (>>=) :: REPL a -> (a -> REPL b) -> REPL b # (>>) :: REPL a -> REPL b -> REPL b # return :: a -> REPL a #
FreshM REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> REPL a Source #
MonadCatch REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods catch :: (HasCallStack, Exception e) => REPL a -> (e -> REPL a) -> REPL a #
MonadMask REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods mask :: HasCallStack => ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b # uninterruptibleMask :: HasCallStack => ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b # generalBracket :: HasCallStack => REPL a -> (a -> ExitCase b -> REPL c) -> (a -> REPL b) -> REPL (b, c) #
MonadThrow REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods throwM :: (HasCallStack, Exception e) => e -> REPL a #
MonadBaseControl IO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Associated Types type StM REPL a # Methods liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a # restoreM :: StM REPL a -> REPL a #
MonadBase IO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftBase :: IO α -> REPL α #
type StM REPL a Source #
Instance details Defined in Cryptol.REPL.Monad type StM REPL a = a

runREPL :: Bool -> Bool -> Logger -> REPL a -> IO a Source #

Run a REPL action with a fresh environment.

io :: IO a -> REPL a Source #

raise :: REPLException -> REPL a Source #

Raise an exception.

stop :: REPL () Source #

catch :: REPL a -> (REPLException -> REPL a) -> REPL a Source #

try :: REPL a -> REPL (Either REPLException a) Source #

finally :: REPL a -> REPL b -> REPL a Source #

rPutStrLn :: String -> REPL () Source #

Use the configured output action to print a string with a trailing newline

rPutStr :: String -> REPL () Source #

Use the configured output action to print a string

rPrint :: Show a => a -> REPL () Source #

Use the configured output action to print something using its Show instance

Errors

data REPLException Source #

REPL exceptions.

Instances

Instances details

Exception REPLException Source #
Instance details Defined in Cryptol.REPL.Monad Methods toException :: REPLException -> SomeException # fromException :: SomeException -> Maybe REPLException # displayException :: REPLException -> String #
Show REPLException Source #
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> REPLException -> ShowS # show :: REPLException -> String # showList :: [REPLException] -> ShowS #
PP REPLException Source #
Instance details Defined in Cryptol.REPL.Monad Methods ppPrec :: Int -> REPLException -> Doc Source #

rethrowEvalError :: IO a -> IO a Source #

Environment

getFocusedEnv :: REPL ModContext Source #

getModuleEnv :: REPL ModuleEnv Source #

setModuleEnv :: ModuleEnv -> REPL () Source #

getDynEnv :: REPL DynamicEnv Source #

setDynEnv :: DynamicEnv -> REPL () Source #

getCallStacks :: REPL Bool Source #

getTCSolver :: REPL Solver Source #

resetTCSolver :: REPL () Source #

uniqify :: Name -> REPL Name Source #

Given an existing qualified name, prefix it with a relatively-unique string. We make it unique by prefixing with a character # that is not lexically valid in a module name.

freshName :: Ident -> NameSource -> REPL Name Source #

Generate a fresh name using the given index. The name will reside within the "interactive" namespace.

whenDebug :: REPL () -> REPL () Source #

getEvalOptsAction :: REPL (IO EvalOpts) Source #

getPPValOpts :: REPL PPOpts Source #

getExprNames :: REPL [String] Source #

Get visible variable names. This is used for command line completition.

getTypeNames :: REPL [String] Source #

Get visible type signature names. This is used for command line completition.

getPropertyNames :: REPL ([(Name, Decl)], NameDisp) Source #

Return a list of property names, sorted by position in the file. Only properties defined in the current module are returned, including private properties in the current module. Imported properties are not returned.

getModNames :: REPL [ModName] Source #

data LoadedModule Source #

This indicates what the user would like to work on.

Constructors

LoadedModule
Fields lFocus :: Maybe (ImpName Name) Working on this module. lPath :: ModulePath Working on this file.

lName :: LoadedModule -> Maybe ModName Source #

getLoadedMod :: REPL (Maybe LoadedModule) Source #

setLoadedMod :: LoadedModule -> REPL () Source #

Set the name of the currently focused file, loaded via :r.

clearLoadedMod :: REPL () Source #

setEditPath :: FilePath -> REPL () Source #

Set the path for the ':e' command. Note that this does not change the focused module (i.e., what ":r" reloads)

getEditPath :: REPL (Maybe FilePath) Source #

clearEditPath :: REPL () Source #

setSearchPath :: [FilePath] -> REPL () Source #

prependSearchPath :: [FilePath] -> REPL () Source #

getPrompt :: REPL String Source #

Construct the prompt for the current environment.

shouldContinue :: REPL Bool Source #

unlessBatch :: REPL () -> REPL () Source #

asBatch :: REPL a -> REPL a Source #

Run a computation in batch mode, restoring the previous isBatch flag afterwards

validEvalContext :: FreeVars a => a -> REPL () Source #

Is evaluation enabled? If the currently focused module is parameterized, then we cannot evaluate.

updateREPLTitle :: REPL () Source #

Update the title

isolated :: REPL a -> REPL a Source #

setUpdateREPLTitle :: REPL () -> REPL () Source #

Set the function that will be called when updating the title

withRandomGen :: (TFGen -> REPL (a, TFGen)) -> REPL a Source #

setRandomGen :: TFGen -> REPL () Source #

getRandomGen :: REPL TFGen Source #

getModuleInput :: REPL (ModuleInput IO) Source #

Config Options

data EnvVal Source #

Constructors

EnvString String
EnvProg String [String]
EnvNum !Int
EnvBool Bool

Instances

Instances details

Show EnvVal Source #
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> EnvVal -> ShowS # show :: EnvVal -> String # showList :: [EnvVal] -> ShowS #

data OptionDescr Source #

Constructors

OptionDescr
Fields optName :: String optAliases :: [String] optDefault :: EnvVal optCheck :: Checker optHelp :: String optEff :: EnvVal -> REPL ()

setUser :: String -> String -> REPL Bool Source #

Set a user option. Returns True on success

getUser :: String -> REPL EnvVal Source #

Get a user option, when it's known to exist. Fail with panic when it doesn't.

getKnownUser :: IsEnvVal a => String -> REPL a Source #

tryGetUser :: String -> REPL (Maybe EnvVal) Source #

Get a user option, using Maybe for failure.

userOptions :: OptionMap Source #

userOptionsWithAliases :: OptionMap Source #

getUserSatNum :: REPL SatNum Source #

getUserShowProverStats :: REPL Bool Source #

getUserProverValidate :: REPL Bool Source #

parsePPFloatFormat :: String -> Maybe PPFloatFormat Source #

parseFieldOrder :: String -> Maybe FieldOrder Source #

getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig) Source #

parseSearchPath :: String -> [String] Source #

Configurable Output

getPutStr :: REPL (String -> IO ()) Source #

Get the REPL's string-printer

getLogger :: REPL Logger Source #

setLogger :: Logger -> REPL () Source #

setPutStr :: (String -> IO ()) -> REPL () Source #

Set the REPL's string-printer

Smoke Test

smokeTest :: REPL [Smoke] Source #

data Smoke Source #

Constructors

Z3NotFound

Instances

Instances details

Show Smoke Source #
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> Smoke -> ShowS # show :: Smoke -> String # showList :: [Smoke] -> ShowS #
PP Smoke Source #
Instance details Defined in Cryptol.REPL.Monad Methods ppPrec :: Int -> Smoke -> Doc Source #
Eq Smoke Source #
Instance details Defined in Cryptol.REPL.Monad Methods (==) :: Smoke -> Smoke -> Bool # (/=) :: Smoke -> Smoke -> Bool #

data RW Source #

REPL RW Environment.

Constructors

RW

Fields

eLoadedMod :: Maybe LoadedModule
This is the name of the currently "focused" module. This is what we reload (:r)
eEditFile :: Maybe FilePath
This is what we edit (:e)
eContinue :: Bool
Should we keep going when we encounter an error, or give up.
eIsBatch :: Bool
Are we in batch mode.
eModuleEnv :: ModuleEnv
The current environment of all things loaded.
eUserEnv :: UserEnv
User settings
eLogger :: Logger
Use this to send messages to the user
eCallStacks :: Bool
eUpdateTitle :: REPL ()
Execute this every time we load a module. This is used to change the title of terminal when loading a module.
eProverConfig :: Either SBVProverConfig W4ProverConfig
eTCConfig :: SolverConfig
Solver configuration to be used for typechecking
eTCSolver :: Maybe Solver
Solver instance to be used for typechecking
eTCSolverRestarts :: !Int
Counts how many times we've restarted the solver. Used as a kind of id for the current solver, which helps avoid a race condition where the callback of a dead solver runs after a new one has been started.
eRandomGen :: TFGen
Random number generator for things like QC and dumpTests

defaultRW :: Bool -> Bool -> Logger -> IO RW Source #

Initial, empty environment.

mkUserEnv :: OptionMap -> UserEnv Source #

Generate a UserEnv from a description of the options map.

ParseError ParseError
FileNotFound FilePath
DirectoryNotFound FilePath
NoPatError [Error]
NoIncludeError [IncludeError]
EvalError EvalErrorEx
TooWide WordTooWide
Unsupported Unsupported
ModuleSystemError NameDisp ModuleError
EvalPolyError Schema
InstantiationsNotFound Schema
TypeNotTestable Type
EvalInParamModule [TParam] [Name]
SBVError String
SBVException SBVException
SBVPortfolioException SBVPortfolioException
W4Exception W4Exception