cryptol-2.6.0: Cryptol: The Language of Cryptography

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 (REPL ())
  - | Ambiguous String [String]
  - | Unknown String
- data CommandDescr = CommandDescr {
  - cNames :: [String]
  - cBody :: CommandBody
  - cHelp :: String
  }
- data CommandBody
  - = 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
  - = CommandOk
  - | CommandError
- 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
  - = QCRandom
  - | QCExhaust
- 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

data Command Source #

Commands.

Constructors

Command (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]
- cBody :: CommandBody
- cHelp :: String

Instances

Eq CommandDescr Source # |
Instance details Defined in Cryptol.REPL.Command Methods (==) :: CommandDescr -> CommandDescr -> Bool Source # (/=) :: CommandDescr -> CommandDescr -> Bool Source #
Ord CommandDescr Source # |

Instance details

Defined in Cryptol.REPL.Command

Methods

compare :: CommandDescr -> CommandDescr -> Ordering Source #

(<) :: CommandDescr -> CommandDescr -> Bool Source #

(<=) :: CommandDescr -> CommandDescr -> Bool Source #

(>) :: CommandDescr -> CommandDescr -> Bool Source #

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

max :: CommandDescr -> CommandDescr -> CommandDescr Source #

min :: CommandDescr -> CommandDescr -> CommandDescr Source #

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

data CommandBody Source #

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 Source #

Constructors

CommandOk |
CommandError |

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

Parse a line as a command.

runCommand :: Command -> REPL CommandExitCode Source #

Run a command.

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

moduleCmd :: String -> REPL () Source #

loadCmd :: FilePath -> REPL () Source #

loadPrelude :: REPL () Source #

setOptionCmd :: String -> REPL () Source #

interactiveConfig :: Config Source #

replParseExpr :: String -> REPL (Expr PName) Source #

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

replCheckExpr :: Expr PName -> REPL (Expr Name, Expr, Schema) 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.

data QCMode Source #

Constructors

QCRandom |
QCExhaust |

Instances

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

satCmd :: String -> REPL () Source #

proveCmd :: String -> REPL () Source #

onlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Maybe Solver, ProverResult, ProverStats) Source #

offlineProveSat :: Bool -> String -> Maybe FilePath -> REPL (Either String String) 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 #