Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell98 |
- data Command
- data CommandDescr = CommandDescr {}
- data CommandBody
- data CommandExitCode
- parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
- runCommand :: Command -> REPL CommandExitCode
- splitCommand :: String -> Maybe (String, String)
- findCommand :: String -> [CommandDescr]
- findCommandExact :: String -> [CommandDescr]
- findNbCommand :: Bool -> String -> [CommandDescr]
- moduleCmd :: String -> REPL ()
- loadCmd :: FilePath -> REPL ()
- loadPrelude :: REPL ()
- setOptionCmd :: String -> REPL ()
- interactiveConfig :: Config
- replParseExpr :: String -> REPL (Expr PName)
- replEvalExpr :: Expr PName -> REPL (Value, Type)
- replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)
- qcCmd :: QCMode -> String -> REPL [TestReport]
- data QCMode
- satCmd :: String -> REPL ()
- proveCmd :: String -> REPL ()
- onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats)
- offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String)
- handleCtrlC :: a -> REPL a
- sanitize :: String -> String
- replParse :: (String -> Either ParseError a) -> String -> REPL a
- liftModuleCmd :: ModuleCmd a -> REPL a
- moduleCmdResult :: ModuleRes a -> REPL a
Commands
Commands.
data CommandBody Source #
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command Source #
Parse a line as a command.
runCommand :: Command -> REPL CommandExitCode Source #
Run a command.
findCommand :: String -> [CommandDescr] Source #
Lookup a string in the command list.
findCommandExact :: String -> [CommandDescr] Source #
Lookup a string in the command list, returning an exact match even if it's the prefix of another command.
findNbCommand :: Bool -> String -> [CommandDescr] Source #
Lookup a string in the notebook-safe command list.
loadPrelude :: REPL () Source #
setOptionCmd :: String -> REPL () Source #
qcCmd :: QCMode -> String -> REPL [TestReport] Source #
Randomly test a property, or exhaustively check it if the number
of values in the type under test is smaller than the tests
environment variable, or we specify exhaustive testing.
onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats) Source #
handleCtrlC :: a -> REPL a Source #
replParse :: (String -> Either ParseError a) -> String -> REPL a Source #
Lift a parsing action into the REPL monad.
liftModuleCmd :: ModuleCmd a -> REPL a Source #
moduleCmdResult :: ModuleRes a -> REPL a Source #