Copyright | (c) 2013-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell98 |
- newtype REPL a = REPL {}
- 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
- rethrowEvalError :: IO a -> IO a
- getFocusedEnv :: REPL (IfaceDecls, NamingEnv, NameDisp)
- getModuleEnv :: REPL ModuleEnv
- setModuleEnv :: ModuleEnv -> REPL ()
- getDynEnv :: REPL DynamicEnv
- setDynEnv :: DynamicEnv -> REPL ()
- uniqify :: Name -> REPL Name
- freshName :: Ident -> 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)
- data LoadedModule = LoadedModule {}
- getLoadedMod :: REPL (Maybe LoadedModule)
- setLoadedMod :: LoadedModule -> REPL ()
- setSearchPath :: [FilePath] -> REPL ()
- prependSearchPath :: [FilePath] -> REPL ()
- 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
- data OptionDescr = OptionDescr {}
- 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
REPL_ context with InputT handling.
raise :: REPLException -> REPL a Source
Raise an exception.
rPutStrLn :: String -> REPL () Source
Use the configured output action to print a string with a trailing newline
rPrint :: Show a => a -> REPL () Source
Use the configured output action to print something using its Show instance
Errors
data REPLException Source
REPL exceptions.
rethrowEvalError :: IO a -> IO a Source
Environment
setModuleEnv :: ModuleEnv -> REPL () 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 -> REPL Name Source
Generate a fresh name using the given index. The name will reside within the "interactive" namespace.
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.
NOTE: we sort by displayed name here, but it would be just as easy to sort by the position in the file, using nameLoc.
data 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
unlessBatch :: REPL () -> REPL () Source
asBatch :: REPL () -> REPL () Source
Run a computation in batch mode, restoring the previous isBatch flag afterwards
disableLet :: 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 OptionDescr Source
getUser :: String -> REPL EnvVal Source
Get a user option, when it's known to exist. Fail with panic when it doesn't.
userOptions :: OptionMap Source