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

fail :: String -> 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

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

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

ModuleSystemError NameDisp ModuleError

EvalPolyError Schema

TypeNotTestable Type

EvalInParamModule ModName [Name]

SBVError String

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 (IfaceParams, IfaceDecls, NamingEnv, NameDisp)

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.

getTSyns :: REPL (Map Name TySyn)

getNewtypes :: REPL (Map Name Newtype)

getVars :: REPL (Map Name IfaceDecl)

whenDebug :: REPL () -> REPL ()

getExprNames :: REPL [String]

Get visible variable names.

getTypeNames :: REPL [String]

Get visible type signature names.

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 :: FilePath

  Working on this file.

getLoadedMod :: REPL (Maybe LoadedModule)

setLoadedMod :: LoadedModule -> REPL ()

Set the name of the currently focused file, edited by :e and loaded via :r.

clearLoadedMod :: REPL ()

setEditPath :: FilePath -> 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

disableLet :: REPL ()

enableLet :: REPL ()

getLetEnabled :: REPL Bool

Are let-bindings enabled in this REPL?

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.

tryGetUser :: String -> REPL (Maybe EnvVal)

Get a user option, using Maybe for failure.

userOptions :: OptionMap

getUserSatNum :: REPL SatNum

getUserShowProverStats :: REPL Bool

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