Cryptol.REPL.Command

Commands

data Command

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

Command builder.

Constructors

CommandDescr

Fields

• cNames :: [String]
• cArgs :: [String]
• cBody :: CommandBody
• cHelp :: String
• cLongHelp :: 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 -> (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

Constructors

CommandOk

CommandError

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

Parse a line as a command.

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

Run a command.

splitCommand :: String -> Maybe (Int, 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.

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

Constructors

TestReport

Fields

• reportExpr :: Doc
• reportResult :: TestResult
• reportTestsRun :: Integer
• reportTestsPossible :: Maybe Integer

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

qcCmd :: QCMode -> String -> (Int, Int) -> Maybe FilePath -> REPL ()

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 -> (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

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