cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell98

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 -> REPL a -> IO a
- io :: IO a -> REPL a
- raise :: REPLException -> REPL a
- stop :: REPL ()
- catch :: REPL a -> (REPLException -> REPL a) -> 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 ModuleError
  - | EvalPolyError Schema
  - | TypeNotTestable Type
- rethrowEvalError :: IO a -> IO a
- getModuleEnv :: REPL ModuleEnv
- setModuleEnv :: ModuleEnv -> REPL ()
- getDynEnv :: REPL DynamicEnv
- setDynEnv :: DynamicEnv -> REPL ()
- uniqify :: QName -> REPL QName
- getTSyns :: REPL (Map QName TySyn)
- getNewtypes :: REPL (Map QName Newtype)
- getVars :: REPL (Map QName IfaceDecl)
- whenDebug :: REPL () -> REPL ()
- getExprNames :: REPL [String]
- getTypeNames :: REPL [String]
- getPropertyNames :: REPL [String]
- data LoadedModule = LoadedModule {
  - lName :: Maybe ModName
  - lPath :: FilePath
  }
- getLoadedMod :: REPL (Maybe LoadedModule)
- setLoadedMod :: LoadedModule -> REPL ()
- setSearchPath :: [FilePath] -> REPL ()
- prependSearchPath :: [FilePath] -> REPL ()
- builtIns :: [(String, (ECon, Schema))]
- getPrompt :: REPL String
- shouldContinue :: REPL Bool
- unlessBatch :: REPL () -> REPL ()
- asBatch :: REPL () -> REPL ()
- disableLet :: REPL ()
- enableLet :: REPL ()
- getLetEnabled :: REPL Bool
- updateREPLTitle :: REPL ()
- setUpdateREPLTitle :: REPL () -> REPL ()
- data EnvVal
  - = EnvString String
  - | EnvNum !Int
  - | EnvBool Bool
- data OptionDescr = OptionDescr {
  - optName :: String
  - optDefault :: EnvVal
  - optCheck :: EnvVal -> IO (Maybe String)
  - optHelp :: String
  - optEff :: EnvVal -> REPL ()
  }
- setUser :: String -> String -> REPL ()
- getUser :: String -> REPL EnvVal
- tryGetUser :: String -> REPL (Maybe EnvVal)
- userOptions :: OptionMap
- getUserSatNum :: REPL SatNum
- getPutStr :: REPL (String -> IO ())
- 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

Monad REPL Source |
Functor REPL Source |
Applicative REPL Source |

runREPL :: Bool -> 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

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 ModuleError |
EvalPolyError Schema |
TypeNotTestable Type |

Instances

Show REPLException Source |
Exception REPLException Source |
PP REPLException Source |

rethrowEvalError :: IO a -> IO a Source

## Environment

getModuleEnv :: REPL ModuleEnv Source

setModuleEnv :: ModuleEnv -> REPL () Source

getDynEnv :: REPL DynamicEnv Source

setDynEnv :: DynamicEnv -> REPL () Source

uniqify :: QName -> REPL QName 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.

getTSyns :: REPL (Map QName TySyn) Source

getNewtypes :: REPL (Map QName Newtype) Source

getVars :: REPL (Map QName 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 [String] Source

data LoadedModule Source

Constructors

LoadedModule |

Fields

lName :: Maybe ModName

  Focused module

lPath :: FilePath

  Focused file

getLoadedMod :: REPL (Maybe LoadedModule) Source

setLoadedMod :: LoadedModule -> REPL () Source

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

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

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

builtIns :: [(String, (ECon, Schema))] Source

getPrompt :: REPL String Source

Construct the prompt for the current environment.

shouldContinue :: REPL Bool Source

unlessBatch :: REPL () -> REPL () Source

asBatch :: REPL () -> REPL () 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?

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 |
EnvNum !Int |
EnvBool Bool |

Instances

Show EnvVal Source |

data OptionDescr Source

Constructors

OptionDescr |

Fields

optName :: String
optDefault :: EnvVal
optCheck :: EnvVal -> IO (Maybe String)
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.

tryGetUser :: String -> REPL (Maybe EnvVal) Source

Get a user option, using Maybe for failure.

userOptions :: OptionMap Source

getUserSatNum :: REPL SatNum 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

smokeTest :: REPL [Smoke] Source

data Smoke Source

Constructors

Z3NotFound |

Instances

Eq Smoke Source |
Show Smoke Source |
PP Smoke Source |