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

Cryptol.REPL.Monad

Contents

REPL Monad

Description

Synopsis

newtype REPL a = REPL {
- unREPL :: IORef RW -> IO a
}
runREPL :: 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
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 EvalError
- | Unsupported Unsupported
- | ModuleSystemError NameDisp ModuleError
- | EvalPolyError Schema
- | TypeNotTestable Type
- | EvalInParamModule [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 ()
uniqify :: Name -> REPL Name
freshName :: Ident -> NameSource -> REPL Name
whenDebug :: REPL () -> REPL ()
getExprNames :: REPL [String]
getTypeNames :: REPL [String]
getPropertyNames :: REPL ([Name], NameDisp)
getModNames :: REPL [ModName]
data LoadedModule = LoadedModule {
- lName :: Maybe ModName
- lPath :: ModulePath
}
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
disableLet :: REPL ()
enableLet :: REPL ()
getLetEnabled :: REPL Bool
validEvalContext :: FreeVars a => a -> REPL ()
updateREPLTitle :: REPL ()
setUpdateREPLTitle :: REPL () -> REPL ()
data EnvVal
- = EnvString String
- | EnvProg String [String]
- | EnvNum !Int
- | EnvBool Bool
data OptionDescr = OptionDescr {
- optName :: String
- optDefault :: EnvVal
- optCheck :: Checker
- optHelp :: String
- optEff :: EnvVal -> REPL ()
}
setUser :: String -> String -> REPL ()
getUser :: String -> REPL EnvVal
getKnownUser :: IsEnvVal a => String -> REPL a
tryGetUser :: String -> REPL (Maybe EnvVal)
userOptions :: OptionMap
getUserSatNum :: REPL SatNum
getUserShowProverStats :: REPL Bool
getUserProverValidate :: REPL Bool
parsePPFloatFormat :: String -> Maybe PPFloatFormat
getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)
getPutStr :: REPL (String -> IO ())
getLogger :: REPL Logger
setPutStr :: (String -> IO ()) -> REPL ()
smokeTest :: REPL [Smoke]
data Smoke = Z3NotFound

REPL Monad

newtype REPL a Source #

REPL_ context with InputT handling.

Constructors

REPL
Fields unREPL :: IORef RW -> IO a

Instances

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 # fail :: String -> 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 #
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 #
MonadIO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftIO :: IO a -> REPL a #
MonadThrow REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods throwM :: Exception e => e -> REPL a #
MonadCatch REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods catch :: Exception e => REPL a -> (e -> REPL a) -> REPL a #
MonadMask REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods mask :: ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b # uninterruptibleMask :: ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b # generalBracket :: REPL a -> (a -> ExitCase b -> REPL c) -> (a -> REPL b) -> REPL (b, c) #
FreshM REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> REPL a Source #
MonadBase IO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Methods liftBase :: IO α -> REPL α #
MonadBaseControl IO REPL Source #
Instance details Defined in Cryptol.REPL.Monad Associated Types type StM REPL a :: Type # Methods liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a # restoreM :: StM REPL a -> REPL a #
type StM REPL a Source #
Instance details Defined in Cryptol.REPL.Monad type StM REPL a = a

runREPL :: 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 #

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

Show REPLException Source #
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> REPLException -> ShowS # show :: REPLException -> String # showList :: [REPLException] -> ShowS #
Exception REPLException Source #
Instance details Defined in Cryptol.REPL.Monad Methods toException :: REPLException -> SomeException # fromException :: SomeException -> Maybe REPLException # displayException :: REPLException -> String #
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 #

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 #

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], NameDisp) Source #

Return a list of property names, sorted by position in the file.

getModNames :: REPL [ModName] Source #

data LoadedModule Source #

This indicates what the user would like to work on.

Constructors

LoadedModule
Fields lName :: Maybe ModName Working on this module. lPath :: ModulePath Working on this file.

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

disableLet :: REPL () Source #

enableLet :: REPL () Source #

getLetEnabled :: REPL Bool Source #

Are let-bindings enabled in this REPL?

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

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

updateREPLTitle :: REPL () Source #

Update the title

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

Set the function that will be called when updating the title

Config Options

data EnvVal Source #

Constructors

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

Instances

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 optDefault :: EnvVal optCheck :: Checker optHelp :: String optEff :: EnvVal -> REPL ()

setUser :: String -> String -> REPL () Source #

Set a user option.

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 #

getUserSatNum :: REPL SatNum Source #

getUserShowProverStats :: REPL Bool Source #

getUserProverValidate :: REPL Bool Source #

parsePPFloatFormat :: String -> Maybe PPFloatFormat Source #

getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig) Source #

Configurable Output

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

Get the REPL's string-printer

getLogger :: REPL Logger Source #

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

Set the REPL's string-printer

Smoke Test

smokeTest :: REPL [Smoke] Source #

data Smoke Source #

Constructors

Z3NotFound

Instances

Eq Smoke Source #
Instance details Defined in Cryptol.REPL.Monad Methods (==) :: Smoke -> Smoke -> Bool # (/=) :: Smoke -> Smoke -> Bool #
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 #

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