Cryptol.REPL.Monad

REPL Monad

newtype REPL a

REPL_ context with InputT handling.

Constructors

REPL

Fields

• unREPL :: IORef RW -> IO a

Instances

Monad REPL

Defined in Cryptol.REPL.Monad

Methods

(>>=) :: REPL a -> (a -> REPL b) -> REPL b

(>>) :: REPL a -> REPL b -> REPL b

return :: a -> REPL a

Functor REPL

Defined in Cryptol.REPL.Monad

Methods

fmap :: (a -> b) -> REPL a -> REPL b

(<$) :: a -> REPL b -> REPL a

Applicative REPL

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

Defined in Cryptol.REPL.Monad

Methods

liftIO :: IO a -> REPL a

MonadThrow REPL

Defined in Cryptol.REPL.Monad

Methods

throwM :: Exception e => e -> REPL a

MonadCatch REPL

Defined in Cryptol.REPL.Monad

Methods

catch :: Exception e => REPL a -> (e -> REPL a) -> REPL a

MonadMask REPL

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

Defined in Cryptol.REPL.Monad

Methods

liftSupply :: (Supply -> (a, Supply)) -> REPL a

MonadBase IO REPL

Defined in Cryptol.REPL.Monad

Methods

liftBase :: IO α -> REPL α

MonadBaseControl IO REPL

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

type StM REPL a

Defined in Cryptol.REPL.Monad

type StM REPL a = a

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

Run a REPL action with a fresh environment.

io :: IO a -> REPL a

raise :: REPLException -> REPL a

Raise an exception.

stop :: REPL ()

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

finally :: REPL a -> REPL b -> REPL a

rPutStrLn :: String -> REPL ()

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

rPutStr :: String -> REPL ()

Use the configured output action to print a string

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

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

Errors

data REPLException

REPL exceptions.

Constructors

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

Instances

Show REPLException

Defined in Cryptol.REPL.Monad

Methods

showsPrec :: Int -> REPLException -> ShowS

show :: REPLException -> String

showList :: [REPLException] -> ShowS

Exception REPLException

Defined in Cryptol.REPL.Monad

Methods

toException :: REPLException -> SomeException

fromException :: SomeException -> Maybe REPLException

displayException :: REPLException -> String

PP REPLException

Defined in Cryptol.REPL.Monad

Methods

ppPrec :: Int -> REPLException -> Doc

rethrowEvalError :: IO a -> IO a

Environment

getFocusedEnv :: REPL ModContext

getModuleEnv :: REPL ModuleEnv

setModuleEnv :: ModuleEnv -> REPL ()

getDynEnv :: REPL DynamicEnv

setDynEnv :: DynamicEnv -> REPL ()

uniqify :: Name -> REPL Name

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

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

whenDebug :: REPL () -> REPL ()

getExprNames :: REPL [String]

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

getTypeNames :: REPL [String]

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

getPropertyNames :: REPL ([Name], NameDisp)

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

getModNames :: REPL [ModName]

data LoadedModule

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)

setLoadedMod :: LoadedModule -> REPL ()

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

clearLoadedMod :: REPL ()

setEditPath :: FilePath -> REPL ()

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)

clearEditPath :: REPL ()

setSearchPath :: [FilePath] -> REPL ()

prependSearchPath :: [FilePath] -> REPL ()

getPrompt :: REPL String

Construct the prompt for the current environment.

shouldContinue :: REPL Bool

unlessBatch :: REPL () -> REPL ()

asBatch :: REPL a -> REPL a

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

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

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

updateREPLTitle :: REPL ()

Update the title

setUpdateREPLTitle :: REPL () -> REPL ()

Set the function that will be called when updating the title

Config Options

data EnvVal

Constructors

EnvString String

EnvProg String [String]

EnvNum !Int

EnvBool Bool

Instances

Show EnvVal

Defined in Cryptol.REPL.Monad

Methods

showsPrec :: Int -> EnvVal -> ShowS

show :: EnvVal -> String

showList :: [EnvVal] -> ShowS

data OptionDescr

Constructors

OptionDescr

Fields

• optName :: String
• optDefault :: EnvVal
• optCheck :: Checker
• optHelp :: String
• optEff :: EnvVal -> REPL ()

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

Set a user option.

getUser :: String -> REPL EnvVal

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

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

tryGetUser :: String -> REPL (Maybe EnvVal)

Get a user option, using Maybe for failure.

userOptions :: OptionMap

getUserSatNum :: REPL SatNum

getUserShowProverStats :: REPL Bool

getUserProverValidate :: REPL Bool

parsePPFloatFormat :: String -> Maybe PPFloatFormat

getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)

Configurable Output

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

Get the REPL's string-printer

getLogger :: REPL Logger

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

Set the REPL's string-printer

Smoke Test

smokeTest :: REPL [Smoke]

data Smoke

Constructors

Z3NotFound

Instances

Eq Smoke

Defined in Cryptol.REPL.Monad

Methods

(==) :: Smoke -> Smoke -> Bool

(/=) :: Smoke -> Smoke -> Bool

Show Smoke

Defined in Cryptol.REPL.Monad

Methods

showsPrec :: Int -> Smoke -> ShowS

show :: Smoke -> String

showList :: [Smoke] -> ShowS

PP Smoke

Defined in Cryptol.REPL.Monad

Methods

ppPrec :: Int -> Smoke -> Doc