| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Cryptol.REPL.Monad
Description
Synopsis
- newtype REPL a = REPL {}
- 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
- rPutStrLn :: String -> REPL ()
- rPutStr :: String -> REPL ()
- rPrint :: Show a => a -> REPL ()
- data REPLException
- 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 {}
- getLoadedMod :: REPL (Maybe LoadedModule)
- setLoadedMod :: LoadedModule -> REPL ()
- clearLoadedMod :: REPL ()
- setEditPath :: FilePath -> REPL ()
- getEditPath :: REPL (Maybe FilePath)
- 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
- data OptionDescr = OptionDescr {}
- 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
REPL_ context with InputT handling.
Instances
| Monad REPL Source # | |
| Functor REPL Source # | |
| Applicative REPL Source # | |
| MonadIO REPL Source # | |
Defined in Cryptol.REPL.Monad | |
| FreshM REPL Source # | |
Defined in Cryptol.REPL.Monad | |
| MonadBase IO REPL Source # | |
Defined in Cryptol.REPL.Monad | |
| MonadBaseControl IO REPL Source # | |
| type StM REPL a Source # | |
Defined in Cryptol.REPL.Monad | |
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.
Constructors
Instances
| Show REPLException Source # | |
Defined in Cryptol.REPL.Monad Methods showsPrec :: Int -> REPLException -> ShowS # show :: REPLException -> String # showList :: [REPLException] -> ShowS # | |
| Exception REPLException Source # | |
Defined in Cryptol.REPL.Monad Methods toException :: REPLException -> SomeException # fromException :: SomeException -> Maybe REPLException # displayException :: REPLException -> String # | |
| PP REPLException Source # | |
Defined in Cryptol.REPL.Monad | |
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 -> NameSource -> 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, sorted by position in the file.
getModNames :: REPL [ModName] Source #
data LoadedModule Source #
This indicates what the user would like to work on.
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)
setSearchPath :: [FilePath] -> REPL () Source #
prependSearchPath :: [FilePath] -> REPL () 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 #
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 OptionDescr Source #
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 #
userOptions :: OptionMap Source #