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

Cryptol.REPL.Command

Contents

Commands

Description

Synopsis

data Command
- = Command (Int -> Maybe FilePath -> REPL ())
- | Ambiguous String [String]
- | Unknown String
data CommandDescr = CommandDescr {
- cNames :: [String]
- cArgs :: [String]
- cBody :: CommandBody
- cHelp :: String
- cLongHelp :: String
}
data CommandBody
- = ExprArg (String -> (Int, Int) -> Maybe FilePath -> REPL ())
- | FileExprArg (FilePath -> String -> (Int, Int) -> Maybe FilePath -> REPL ())
- | DeclsArg (String -> REPL ())
- | ExprTypeArg (String -> REPL ())
- | ModNameArg (String -> REPL ())
- | FilenameArg (FilePath -> REPL ())
- | OptionArg (String -> REPL ())
- | ShellArg (String -> REPL ())
- | HelpArg (String -> REPL ())
- | NoArg (REPL ())
data CommandExitCode
- = CommandOk
- | CommandError
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode
splitCommand :: String -> Maybe (Int, String, String)
findCommand :: String -> [CommandDescr]
findCommandExact :: String -> [CommandDescr]
findNbCommand :: Bool -> String -> [CommandDescr]
commandList :: [CommandDescr]
moduleCmd :: String -> REPL ()
loadCmd :: FilePath -> REPL ()
loadPrelude :: REPL ()
setOptionCmd :: String -> REPL ()
interactiveConfig :: Config
replParseExpr :: String -> (Int, Int) -> Maybe FilePath -> REPL (Expr PName)
replEvalExpr :: Expr PName -> REPL (Value, Type)
replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema)
data TestReport = TestReport {
- reportExpr :: Doc
- reportResult :: TestResult
- reportTestsRun :: Integer
- reportTestsPossible :: Maybe Integer
}
qcExpr :: QCMode -> Doc -> Expr -> Schema -> REPL TestReport
qcCmd :: QCMode -> String -> (Int, Int) -> Maybe FilePath -> REPL ()
data QCMode
- = QCRandom
- | QCExhaust
satCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
proveCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL ()
onlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL (Maybe String, ProverResult, ProverStats)
offlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL ()
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

data Command Source #

Commands.

Constructors

Command (Int -> Maybe FilePath -> REPL ())	Successfully parsed command
Ambiguous String [String]	Ambiguous command, list of conflicting commands
Unknown String	The unknown command

data CommandDescr Source #

Command builder.

Constructors

CommandDescr
Fields cNames :: [String] cArgs :: [String] cBody :: CommandBody cHelp :: String cLongHelp :: String

Instances

Instances details

Eq CommandDescr Source #
Instance details Defined in Cryptol.REPL.Command Methods (==) :: CommandDescr -> CommandDescr -> Bool # (/=) :: CommandDescr -> CommandDescr -> Bool #
Ord CommandDescr Source #
Instance details Defined in Cryptol.REPL.Command Methods compare :: CommandDescr -> CommandDescr -> Ordering # (<) :: CommandDescr -> CommandDescr -> Bool # (<=) :: CommandDescr -> CommandDescr -> Bool # (>) :: CommandDescr -> CommandDescr -> Bool # (>=) :: CommandDescr -> CommandDescr -> Bool # max :: CommandDescr -> CommandDescr -> CommandDescr # min :: CommandDescr -> CommandDescr -> CommandDescr #
Show CommandDescr Source #
Instance details Defined in Cryptol.REPL.Command Methods showsPrec :: Int -> CommandDescr -> ShowS # show :: CommandDescr -> String # showList :: [CommandDescr] -> ShowS #

data CommandBody Source #

Constructors

ExprArg (String -> (Int, Int) -> Maybe FilePath -> REPL ())
FileExprArg (FilePath -> String -> (Int, Int) -> Maybe FilePath -> REPL ())
DeclsArg (String -> REPL ())
ExprTypeArg (String -> REPL ())
ModNameArg (String -> REPL ())
FilenameArg (FilePath -> REPL ())
OptionArg (String -> REPL ())
ShellArg (String -> REPL ())
HelpArg (String -> REPL ())
NoArg (REPL ())

data CommandExitCode Source #

Constructors

CommandOk
CommandError

parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command Source #

Parse a line as a command.

runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandExitCode Source #

Run a command.

splitCommand :: String -> Maybe (Int, String, String) Source #

Split at the first word boundary.

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.

commandList :: [CommandDescr] Source #

moduleCmd :: String -> REPL () Source #

loadCmd :: FilePath -> REPL () Source #

loadPrelude :: REPL () Source #

setOptionCmd :: String -> REPL () Source #

interactiveConfig :: Config Source #

replParseExpr :: String -> (Int, Int) -> Maybe FilePath -> REPL (Expr PName) Source #

replEvalExpr :: Expr PName -> REPL (Value, Type) Source #

replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema) Source #

data TestReport Source #

Constructors

TestReport
Fields reportExpr :: Doc reportResult :: TestResult reportTestsRun :: Integer reportTestsPossible :: Maybe Integer

qcExpr :: QCMode -> Doc -> Expr -> Schema -> REPL TestReport Source #

qcCmd :: QCMode -> String -> (Int, Int) -> Maybe FilePath -> REPL () 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.

data QCMode Source #

Constructors

QCRandom
QCExhaust

Instances

Instances details

Eq QCMode Source #
Instance details Defined in Cryptol.REPL.Command Methods (==) :: QCMode -> QCMode -> Bool # (/=) :: QCMode -> QCMode -> Bool #
Show QCMode Source #
Instance details Defined in Cryptol.REPL.Command Methods showsPrec :: Int -> QCMode -> ShowS # show :: QCMode -> String # showList :: [QCMode] -> ShowS #

satCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () Source #

proveCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL () Source #

onlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL (Maybe String, ProverResult, ProverStats) Source #

offlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL () Source #

handleCtrlC :: a -> REPL a Source #

sanitize :: String -> String Source #

Strip leading space.

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 #