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.
GaloisInc · Jul 31, 2018 · 9b97c74 · 9b97c74
1 parent 2e1dbad
commit 9b97c74
Show file tree

Hide file tree

Showing 4 changed files with 53 additions and 50 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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