diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 8178e46cc..a19b14030 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -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 diff --git a/src/Cryptol/Prims/Syntax.hs b/src/Cryptol/Prims/Syntax.hs index 1bfb6c8ce..5b81b2af8 100644 --- a/src/Cryptol/Prims/Syntax.hs +++ b/src/Cryptol/Prims/Syntax.hs @@ -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." diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 7abe91fa9..4bd3a891d 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -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) $ diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 7468204b6..4598a5175 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -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