cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.REPL.Monad

Description

 
Synopsis

REPL Monad

newtype REPL a Source #

REPL_ context with InputT handling.

Constructors

REPL 

Fields

Instances

Instances details
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 #

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

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 α Source #

MonadBaseControl IO REPL Source # 
Instance details

Defined in Cryptol.REPL.Monad

Associated Types

type StM REPL a Source #

Methods

liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a Source #

restoreM :: StM REPL a -> REPL a Source #

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.

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

Instances details
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

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.

getTypeNames :: REPL [String] Source #

Get visible type signature names.

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

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

data LoadedModule Source #

This indicates what the user would like to work on.

Constructors

LoadedModule 

Fields

setLoadedMod :: LoadedModule -> REPL () Source #

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

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 #

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

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

getPrompt :: REPL String Source #

Construct the prompt for the current environment.

asBatch :: REPL a -> REPL a Source #

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

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

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

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 #

Configurable Output

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

Get the REPL's string-printer

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

Set the REPL's string-printer

Smoke Test

data Smoke Source #

Constructors

Z3NotFound 

Instances

Instances details
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 #