cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Cryptol.REPL.Command

Contents

Description

 
Synopsis

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

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

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

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

Parse a line as 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.

loadCmd :: FilePath -> REPL () 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

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

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

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