mirror of
https://github.com/GaloisInc/cryptol.git
synced 2025-01-05 23:17:42 +03:00
Polishing of :help output.
:help with primitive types now uses vertical whitespace to match
the :help output for other types.
Help text for REPL commands can now contain linebreaks.
For quoted Cryptol syntax in docstrings, consistently use singlequotes
(') instead of backquotes (`). Backquotes are sometimes used within
the quoted code, so it's probably best to avoid using them for quotes.
Consistently capitalize and put a period at the end of docstrings.
This commit is contained in:
Brian Huffman
parent
2e1dbad005
commit
9b97c74b48
@ -263,17 +263,17 @@ x \/ y = if x then True else y
|
||||
a ==> b = if a then b else True
|
||||
|
||||
/**
|
||||
* Logical `and' over bits. Extends element-wise over sequences, tuples.
|
||||
* Logical 'and' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (&&) : {a} (Logic a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* Logical `or' over bits. Extends element-wise over sequences, tuples.
|
||||
* Logical 'or' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (||) : {a} (Logic a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
|
||||
* Logical 'exclusive or' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (^) : {a} (Logic a) => a -> a -> a
|
||||
|
||||
@ -691,7 +691,7 @@ repeat : {n, a} a -> [n]a
|
||||
repeat x = [ x | _ <- zero : [n] ]
|
||||
|
||||
/**
|
||||
* `elem x xs` Returns true if x is equal to a value in xs.
|
||||
* 'elem x xs' returns true if x is equal to a value in xs.
|
||||
*/
|
||||
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
|
||||
elem a xs = any (\x -> x == a) xs
|
||||
|
||||
@ -42,7 +42,7 @@ primTyList =
|
||||
"The type of unbounded integers."
|
||||
|
||||
, tPrefix "Z" TC TCIntMod
|
||||
"`Z n` is the type of integers, modulo `n`."
|
||||
"'Z n' is the type of integers, modulo 'n'."
|
||||
|
||||
|
||||
-- Predicate constructors --------------------------------------------------
|
||||
@ -57,10 +57,10 @@ primTyList =
|
||||
"Assert that the first numeric type is larger than, or equal to the second."
|
||||
|
||||
, tPrefix "fin" PC PFin
|
||||
"Assert that a numeric type is a proper natural number (not `inf`)."
|
||||
"Assert that a numeric type is a proper natural number (not 'inf')."
|
||||
|
||||
, tPrefix "Zero" PC PZero
|
||||
"Value types that have a notion of `zero`."
|
||||
"Value types that have a notion of 'zero'."
|
||||
|
||||
, tPrefix "Logic" PC PLogic
|
||||
"Value types that support logical operations."
|
||||
@ -72,10 +72,10 @@ primTyList =
|
||||
"Value types that support unsigned comparisons."
|
||||
|
||||
, tPrefix "SignedCmp" PC PSignedCmp
|
||||
"Values types that support signed comparisons."
|
||||
"Value types that support signed comparisons."
|
||||
|
||||
, tPrefix "Literal" PC PLiteral
|
||||
"`Literal n a` asserts that type `a` contains the value `n`."
|
||||
"'Literal n a' asserts that type 'a' contains the number 'n'."
|
||||
|
||||
|
||||
|
||||
@ -85,16 +85,16 @@ primTyList =
|
||||
"Add numeric types."
|
||||
|
||||
, tInfix "-" TF TCSub (l 80)
|
||||
"Subtract numeric types"
|
||||
"Subtract numeric types."
|
||||
|
||||
, tInfix "*" TF TCMul (l 90)
|
||||
"Multiply numeric types"
|
||||
"Multiply numeric types."
|
||||
|
||||
, tInfix "/" TF TCDiv (l 90)
|
||||
"Divide numeric types, rounding down."
|
||||
|
||||
, tInfix "%" TF TCMod (l 90)
|
||||
"Reminder of numeric type division."
|
||||
"Remainder of numeric type division."
|
||||
|
||||
, tInfix "^^" TF TCExp (r 95)
|
||||
"Exponentiate numeric types."
|
||||
@ -103,10 +103,10 @@ primTyList =
|
||||
"The number of bits required to represent the value of a numeric type."
|
||||
|
||||
, tPrefix "min" TF TCMin
|
||||
"The smallest of two numeric types."
|
||||
"The smaller of two numeric types."
|
||||
|
||||
, tPrefix "max" TF TCMax
|
||||
"The largest of two numeric types."
|
||||
"The larger of two numeric types."
|
||||
|
||||
, tInfix "/^" TF TCCeilDiv (l 90)
|
||||
"Divide numeric types, rounding up."
|
||||
|
||||
@ -169,58 +169,59 @@ nbCommands = foldl insert emptyTrie nbCommandList
|
||||
nbCommandList :: [CommandDescr]
|
||||
nbCommandList =
|
||||
[ CommandDescr [ ":t", ":type" ] (ExprArg typeOfCmd)
|
||||
"check the type of an expression"
|
||||
"Check the type of an expression."
|
||||
, CommandDescr [ ":b", ":browse" ] (ModNameArg browseCmd)
|
||||
"display the current environment"
|
||||
"Display environment for all loaded modules, or for a specific module."
|
||||
, CommandDescr [ ":?", ":help" ] (HelpArg helpCmd)
|
||||
"display a brief description of a function or a type"
|
||||
"Display a brief description of a function, type, or command."
|
||||
, CommandDescr [ ":s", ":set" ] (OptionArg setOptionCmd)
|
||||
"set an environmental option (:set on its own displays current values)"
|
||||
"Set an environmental option (:set on its own displays current values)."
|
||||
, CommandDescr [ ":check" ] (ExprArg (void . qcCmd QCRandom))
|
||||
"use random testing to check that the argument always returns true (if no argument, check all properties)"
|
||||
"Use random testing to check that the argument always returns true.\n(If no argument, check all properties.)"
|
||||
, CommandDescr [ ":exhaust" ] (ExprArg (void . qcCmd QCExhaust))
|
||||
"use exhaustive testing to prove that the argument always returns true (if no argument, check all properties)"
|
||||
"Use exhaustive testing to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
|
||||
, CommandDescr [ ":prove" ] (ExprArg proveCmd)
|
||||
"use an external solver to prove that the argument always returns true (if no argument, check all properties)"
|
||||
"Use an external solver to prove that the argument always returns\ntrue. (If no argument, check all properties.)"
|
||||
, CommandDescr [ ":sat" ] (ExprArg satCmd)
|
||||
"use a solver to find a satisfying assignment for which the argument returns true (if no argument, find an assignment for all properties)"
|
||||
"Use a solver to find a satisfying assignment for which the argument\nreturns true. (If no argument, find an assignment for all properties.)"
|
||||
, CommandDescr [ ":debug_specialize" ] (ExprArg specializeCmd)
|
||||
"do type specialization on a closed expression"
|
||||
"Do type specialization on a closed expression."
|
||||
, CommandDescr [ ":eval" ] (ExprArg refEvalCmd)
|
||||
"evaluate an expression with the reference evaluator"
|
||||
"Evaluate an expression with the reference evaluator."
|
||||
, CommandDescr [ ":ast" ] (ExprArg astOfCmd)
|
||||
"print out the pre-typechecked AST of a given term"
|
||||
"Print out the pre-typechecked AST of a given term."
|
||||
, CommandDescr [ ":extract-coq" ] (NoArg allTerms)
|
||||
"print out the post-typechecked AST of all currently defined terms, in a Coq parseable format"
|
||||
"Print out the post-typechecked AST of all currently defined terms,\nin a Coq-parseable format."
|
||||
]
|
||||
|
||||
commandList :: [CommandDescr]
|
||||
commandList =
|
||||
nbCommandList ++
|
||||
[ CommandDescr [ ":q", ":quit" ] (NoArg quitCmd)
|
||||
"exit the REPL"
|
||||
"Exit the REPL."
|
||||
, CommandDescr [ ":l", ":load" ] (FilenameArg loadCmd)
|
||||
"load a module"
|
||||
"Load a module by filename."
|
||||
, CommandDescr [ ":r", ":reload" ] (NoArg reloadCmd)
|
||||
"reload the currently loaded module"
|
||||
"Reload the currently loaded module."
|
||||
, CommandDescr [ ":e", ":edit" ] (FilenameArg editCmd)
|
||||
"edit the currently loaded module"
|
||||
"Edit the currently loaded module."
|
||||
, CommandDescr [ ":!" ] (ShellArg runShellCmd)
|
||||
"execute a command in the shell"
|
||||
"Execute a command in the shell."
|
||||
, CommandDescr [ ":cd" ] (FilenameArg cdCmd)
|
||||
"set the current working directory"
|
||||
"Set the current working directory."
|
||||
, CommandDescr [ ":m", ":module" ] (FilenameArg moduleCmd)
|
||||
"load a module"
|
||||
"Load a module by its name."
|
||||
, CommandDescr [ ":w", ":writeByteArray" ] (FileExprArg writeFileCmd)
|
||||
"write data of type `fin n => [n][8]` to a file"
|
||||
"Write data of type 'fin n => [n][8]' to a file."
|
||||
, CommandDescr [ ":readByteArray" ] (FilenameArg readFileCmd)
|
||||
"read data from a file as type `fin n => [n][8]`, binding the value to variable `it`"
|
||||
"Read data from a file as type 'fin n => [n][8]', binding\nthe value to variable 'it'."
|
||||
]
|
||||
|
||||
genHelp :: [CommandDescr] -> [String]
|
||||
genHelp cs = map cmdHelp cs
|
||||
where
|
||||
cmdHelp cmd = concat [ " ", cmdNames cmd, pad (cmdNames cmd), cHelp cmd ]
|
||||
cmdHelp cmd = concat $ [ " ", cmdNames cmd, pad (cmdNames cmd),
|
||||
intercalate ("\n " ++ pad []) (lines (cHelp cmd)) ]
|
||||
cmdNames cmd = intercalate ", " (cNames cmd)
|
||||
padding = 2 + maximum (map (length . cmdNames) cs)
|
||||
pad n = replicate (max 0 (padding - length n)) ' '
|
||||
@ -937,14 +938,16 @@ helpCmd cmd
|
||||
M.Parameter -> rPutStrLn "// No documentation is available."
|
||||
|
||||
showPrimTyHelp nameEnv pt =
|
||||
do rPutStrLn "Primitive type:"
|
||||
do rPutStrLn ""
|
||||
let i = T.primTyIdent pt
|
||||
nm = pp (T.primTyIdent pt)
|
||||
pnam = if P.isInfixIdent i then parens nm else nm
|
||||
sig = pnam <+> ":" <+> pp (T.kindOf (T.primTyCon pt))
|
||||
sig = "primitive type" <+> pnam <+> ":" <+> pp (T.kindOf (T.primTyCon pt))
|
||||
rPrint $ runDoc nameEnv $ nest 4 sig
|
||||
doShowFix (T.primTyFixity pt)
|
||||
rPutStrLn ""
|
||||
rPutStrLn (T.primTyDoc pt)
|
||||
rPutStrLn ""
|
||||
|
||||
showTypeHelp params env nameEnv name =
|
||||
fromMaybe (noInfo nameEnv name) $
|
||||
|
||||
@ -688,34 +688,34 @@ simpleOpt optName optDefault optCheck optHelp =
|
||||
userOptions :: OptionMap
|
||||
userOptions = mkOptionMap
|
||||
[ simpleOpt "base" (EnvNum 16) checkBase
|
||||
"the base to display words at"
|
||||
"The base to display words at (2, 8, 10, or 16)."
|
||||
, simpleOpt "debug" (EnvBool False) noCheck
|
||||
"enable debugging output"
|
||||
"Enable debugging output."
|
||||
, simpleOpt "ascii" (EnvBool False) noCheck
|
||||
"display 7- or 8-bit words using ASCII notation."
|
||||
"Whether to display 7- or 8-bit words using ASCII notation."
|
||||
, simpleOpt "infLength" (EnvNum 5) checkInfLength
|
||||
"The number of elements to display for infinite sequences."
|
||||
, simpleOpt "tests" (EnvNum 100) noCheck
|
||||
"The number of random tests to try."
|
||||
"The number of random tests to try with ':check'."
|
||||
, simpleOpt "satNum" (EnvString "1") checkSatNum
|
||||
"The maximum number of :sat solutions to display (\"all\" for no limit)."
|
||||
, simpleOpt "prover" (EnvString "z3") checkProver $
|
||||
"The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
|
||||
"The external SMT solver for ':prove' and ':sat'\n(" ++ proverListString ++ ")."
|
||||
, simpleOpt "warnDefaulting" (EnvBool True) noCheck
|
||||
"Choose if we should display warnings when defaulting."
|
||||
"Choose whether to display warnings when defaulting."
|
||||
, simpleOpt "warnShadowing" (EnvBool True) noCheck
|
||||
"Choose if we should display warnings when shadowing symbols."
|
||||
"Choose whether to display warnings when shadowing symbols."
|
||||
, simpleOpt "smtfile" (EnvString "-") noCheck
|
||||
"The file to use for SMT-Lib scripts (for debugging or offline proving)"
|
||||
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
|
||||
, OptionDescr "mono-binds" (EnvBool True) noCheck
|
||||
"Whether or not to generalize bindings in a where-clause" $
|
||||
"Whether or not to generalize bindings in a 'where' clause." $
|
||||
\case EnvBool b -> do me <- getModuleEnv
|
||||
setModuleEnv me { M.meMonoBinds = b }
|
||||
_ -> return ()
|
||||
|
||||
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
|
||||
noCheck -- TODO: check for the program in the path
|
||||
"The solver that will be used by the type checker" $
|
||||
"The solver that will be used by the type checker." $
|
||||
\case EnvProg prog args -> do me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
setModuleEnv me { M.meSolverConfig =
|
||||
@ -725,14 +725,14 @@ userOptions = mkOptionMap
|
||||
|
||||
, OptionDescr "tc-debug" (EnvNum 0)
|
||||
noCheck
|
||||
"Enable type-checker debugging output" $
|
||||
"Enable type-checker debugging output." $
|
||||
\case EnvNum n -> do me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = fromIntegral n } }
|
||||
_ -> return ()
|
||||
, OptionDescr "core-lint" (EnvBool False)
|
||||
noCheck
|
||||
"Enable sanity checking of type-checker" $
|
||||
"Enable sanity checking of type-checker." $
|
||||
let setIt x = do me <- getModuleEnv
|
||||
setModuleEnv me { M.meCoreLint = x }
|
||||
in \case EnvBool True -> setIt M.CoreLint
|
||||
|
||||
Loading…
Reference in New Issue
Block a user