Cryptol.REPL.Command

Commands

data Command

Commands.

Constructors

Command (REPL ())

Successfully parsed command

Ambiguous String [String]

Ambiguous command, list of conflicting commands

Unknown String

The unknown command

data CommandDescr

Command builder.

Constructors

CommandDescr

Fields

• cNames :: [String]
• cBody :: CommandBody
• cHelp :: String

Instances

Eq CommandDescr

Defined in Cryptol.REPL.Command

Methods

(==) :: CommandDescr -> CommandDescr -> Bool

(/=) :: CommandDescr -> CommandDescr -> Bool

Ord CommandDescr

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

Defined in Cryptol.REPL.Command

Methods

showsPrec :: Int -> CommandDescr -> ShowS

show :: CommandDescr -> String

showList :: [CommandDescr] -> ShowS

data CommandBody

Constructors

ExprArg (String -> REPL ())

FileExprArg (FilePath -> String -> 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

Constructors

CommandOk

CommandError

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

Parse a line as a command.

runCommand :: Command -> REPL CommandExitCode

Run a command.

splitCommand :: String -> Maybe (String, String)

Split at the first word boundary.

findCommand :: String -> [CommandDescr]

Lookup a string in the command list.

findCommandExact :: String -> [CommandDescr]

Lookup a string in the command list, returning an exact match even if it's the prefix of another command.

findNbCommand :: Bool -> String -> [CommandDescr]

Lookup a string in the notebook-safe command list.

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]

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

Constructors

QCRandom

QCExhaust

Instances

Eq QCMode

Defined in Cryptol.REPL.Command

Methods

(==) :: QCMode -> QCMode -> Bool

(/=) :: QCMode -> QCMode -> Bool

Show QCMode

Defined in Cryptol.REPL.Command

Methods

showsPrec :: Int -> QCMode -> ShowS

show :: QCMode -> String

showList :: [QCMode] -> ShowS

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

Strip leading space.

replParse :: (String -> Either ParseError a) -> String -> REPL a

Lift a parsing action into the REPL monad.

liftModuleCmd :: ModuleCmd a -> REPL a

moduleCmdResult :: ModuleRes a -> REPL a