cryptol-2.8.0: Cryptol: The Language of Cryptography

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
  - Errors
  - Environment
  - Config Options
  - Configurable Output
  - Smoke Test

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
  - | ModuleSystemError NameDisp ModuleError
  - | EvalPolyError Schema
  - | TypeNotTestable Type
  - | EvalInParamModule [Name]
  - | SBVError String
- rethrowEvalError :: IO a -> IO a
- getFocusedEnv :: REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
- getModuleEnv :: REPL ModuleEnv
- setModuleEnv :: ModuleEnv -> REPL ()
- getDynEnv :: REPL DynamicEnv
- setDynEnv :: DynamicEnv -> REPL ()
- uniqify :: Name -> REPL Name
- freshName :: Ident -> NameSource -> REPL Name
- getTSyns :: REPL (Map Name TySyn)
- getNewtypes :: REPL (Map Name Newtype)
- getVars :: REPL (Map Name IfaceDecl)
- 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
- 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

Instances details

Monad REPL Source # |
Instance details Defined in Cryptol.REPL.Monad Methods (>>=) :: REPL a -> (a -> REPL b) -> REPL b Source # (>>) :: REPL a -> REPL b -> REPL b Source # return :: a -> REPL a Source #
Functor REPL Source # |
Instance details Defined in Cryptol.REPL.Monad Methods fmap :: (a -> b) -> REPL a -> REPL b Source # (<$) :: a -> REPL b -> REPL a Source #
Applicative REPL Source # |
Instance details Defined in Cryptol.REPL.Monad Methods pure :: a -> REPL a Source # (<*>) :: REPL (a -> b) -> REPL a -> REPL b Source # liftA2 :: (a -> b -> c) -> REPL a -> REPL b -> REPL c Source # (*>) :: REPL a -> REPL b -> REPL b Source # (<*) :: REPL a -> REPL b -> REPL a Source #
MonadIO REPL Source # |
Instance details Defined in Cryptol.REPL.Monad Methods liftIO :: IO a -> REPL a Source #
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.

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.

Constructors

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

#### Instances

Instances details

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

getTSyns :: REPL (Map Name TySyn) Source #

getNewtypes :: REPL (Map Name Newtype) Source #

getVars :: REPL (Map Name IfaceDecl) Source #

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.

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

Instances details

Show EnvVal Source # |
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> EnvVal -> ShowS Source # show :: EnvVal -> String Source # showList :: [EnvVal] -> ShowS Source #

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 #

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

Instances details

Eq Smoke Source # |
Instance details Defined in Cryptol.REPL.Monad Methods (==) :: Smoke -> Smoke -> Bool Source # (/=) :: Smoke -> Smoke -> Bool Source #
Show Smoke Source # |
Instance details Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> Smoke -> ShowS Source # show :: Smoke -> String Source # showList :: [Smoke] -> ShowS Source #
PP Smoke Source # |
Instance details Defined in Cryptol.REPL.Monad Methods ppPrec :: Int -> Smoke -> Doc Source #