cryptol-2.9.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.REPL.Monad

Contents

Description

 
Synopsis

REPL Monad

newtype REPL a Source #

REPL_ context with InputT handling.

Constructors

REPL 

Fields

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.

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

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. 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.

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)

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 #

Instances
Show EnvVal Source # 
Instance details

Defined in Cryptol.REPL.Monad

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