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

Cryptol.REPL.Command

Contents

Commands

Description

Synopsis

data Command
- = Command (Int -> Maybe FilePath -> REPL CommandResult)
- | 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 CommandResult)
- | FileExprArg (FilePath -> String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult)
- | DeclsArg (String -> REPL CommandResult)
- | ExprTypeArg (String -> REPL CommandResult)
- | ModNameArg (String -> REPL CommandResult)
- | FilenameArg (FilePath -> REPL CommandResult)
- | OptionArg (String -> REPL CommandResult)
- | ShellArg (String -> REPL CommandResult)
- | HelpArg (String -> REPL CommandResult)
- | NoArg (REPL CommandResult)
data CommandResult = CommandResult {
- crType :: Maybe String
- crValue :: Maybe String
- crSuccess :: Bool
}
parseCommand :: (String -> [CommandDescr]) -> String -> Maybe Command
runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandResult
splitCommand :: String -> Maybe (Int, String, String)
findCommand :: String -> [CommandDescr]
findCommandExact :: String -> [CommandDescr]
findNbCommand :: Bool -> String -> [CommandDescr]
commandList :: [CommandDescr]
emptyCommandResult :: CommandResult
moduleCmd :: String -> REPL CommandResult
loadCmd :: FilePath -> REPL CommandResult
loadPrelude :: REPL ()
setOptionCmd :: String -> REPL CommandResult
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 CommandResult
data QCMode
- = QCRandom
- | QCExhaust
satCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult
proveCmd :: String -> (Int, Int) -> Maybe FilePath -> REPL CommandResult
onlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL (Maybe String, ProverResult, ProverStats)
offlineProveSat :: String -> QueryType -> Expr -> Schema -> Maybe FilePath -> REPL Bool
checkDocStrings :: LoadedModule -> REPL [DocstringResult]
data SubcommandResult = SubcommandResult {
- srInput :: Text
- srResult :: CommandResult
- srLog :: String
}
data DocstringResult = DocstringResult {
- drName :: DocFor
- drFences :: [[SubcommandResult]]
}
handleCtrlC :: a -> REPL a
sanitize :: String -> String
withRWTempFile :: String -> (Handle -> IO a) -> IO a
printModuleWarnings :: [ModuleWarning] -> REPL ()
replParse :: (String -> Either ParseError a) -> String -> REPL a
liftModuleCmd :: ModuleCmd a -> REPL a
moduleCmdResult :: ModuleRes a -> REPL a
loadProjectREPL :: LoadProjectMode -> Config -> REPL CommandResult

Commands

data Command Source #

Commands.

Constructors

Command (Int -> Maybe FilePath -> REPL CommandResult)	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

Show CommandDescr Source #
Instance details Defined in Cryptol.REPL.Command Methods showsPrec :: Int -> CommandDescr -> ShowS # show :: CommandDescr -> String # showList :: [CommandDescr] -> ShowS #
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 #

data CommandBody Source #

Constructors

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

data CommandResult Source #

Constructors

CommandResult
Fields crType :: Maybe String type output for relevant commands crValue :: Maybe String value output for relevant commands crSuccess :: Bool indicator that command successfully performed its task

Instances

Instances details

Show CommandResult Source #
Instance details Defined in Cryptol.REPL.Command Methods showsPrec :: Int -> CommandResult -> ShowS # show :: CommandResult -> String # showList :: [CommandResult] -> ShowS #

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

Parse a line as a command.

runCommand :: Int -> Maybe FilePath -> Command -> REPL CommandResult 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 #

emptyCommandResult :: CommandResult Source #

moduleCmd :: String -> REPL CommandResult Source #

loadCmd :: FilePath -> REPL CommandResult Source #

loadPrelude :: REPL () Source #

setOptionCmd :: String -> REPL CommandResult 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 CommandResult 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

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

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

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

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

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

checkDocStrings :: LoadedModule -> REPL [DocstringResult] Source #

Check all of the docstrings in the given module.

The outer list elements correspond to the code blocks from the docstrings in file order. Each inner list corresponds to the REPL commands inside each of the docstrings.

data SubcommandResult Source #

Constructors

SubcommandResult
Fields srInput :: Text srResult :: CommandResult srLog :: String

data DocstringResult Source #

The result of running a docstring as attached to a definition

Constructors

DocstringResult
Fields drName :: DocFor The associated definition of the docstring drFences :: [[SubcommandResult]] list of fences in this definition's docstring

handleCtrlC :: a -> REPL a Source #

sanitize :: String -> String Source #

Strip leading space.

withRWTempFile :: String -> (Handle -> IO a) -> IO a Source #

printModuleWarnings :: [ModuleWarning] -> REPL () 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 #

loadProjectREPL :: LoadProjectMode -> Config -> REPL CommandResult Source #

Load a project. Note that this does not update the Cryptol environment, it only updates the project cache.