Merge pull request #1073 from GaloisInc/standardize-set

Rename the runtime-settable options to use a consistent style

cryptol-remote-api/docs/Cryptol.rst

@@ -23,7 +23,7 @@ zero or more of the following fields:
    + ``base``: What base to display numbers in (default ``10``).
    + ``prefix of infinite lengths``: How much of an infinite sequence to display (default ``5``.
    + ``floating point base``: What base to display floating point numbers in (default ``10``).
-   + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fp-format`` in the REPL).
+   + ``floating point format``: The output format used to display floating point numbers (accepts strings in the same format as the argument to ``:set fpFormat`` in the REPL).
 
 Module Management
 =================

cryptol/Main.hs

@@ -195,9 +195,15 @@ displayHelp errs = do
             , "addition to the default locations"
             ]
           )
+        , ( "EDITOR"
+          , [ "Sets the editor executable to use when opening an editor"
+            , "via the `:edit` command"
+            ]
+          )
         , ( "SBV_{ABC,BOOLECTOR,CVC4,MATHSAT,YICES,Z3}_OPTIONS"
           , [ "A string of command-line arguments to be passed to the"
             , "corresponding solver invoked for `:sat` and `:prove`"
+            , "when using a prover via SBV"
             ]
           )
         ]

docs/ProgrammingCryptol/technicalities/TechAppendix.tex

@@ -160,12 +160,12 @@ \section{Commands}
     \hline
      \texttt{ascii}           & \texttt{off}   & print sequences of bytes as a string \\
      \texttt{base}            & \texttt{16}    & numeric base for printing words  \\
-     \texttt{ignore-safety}   & \texttt{off}   & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
+     \texttt{ignoreSafety}   & \texttt{off}   & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
      \texttt{infLength}       & \texttt{5}     & number of elements to show from an infinite sequence \\
      \texttt{prover}          & \texttt{z3}    & which SMT solver to use for \texttt{:prove}  \\
      \texttt{satNum}          & \texttt{1}     & maximum number of solutions to show for \texttt{:sat} \\
-     \texttt{show-examples}   & \texttt{on}    & whether to print counterexamples and models \\
-     \texttt{smtfile}         & \texttt{-}     & file to write SMT problems when \texttt{prover = offline} \\
+     \texttt{showExamples}   & \texttt{on}    & whether to print counterexamples and models \\
+     \texttt{smtFile}         & \texttt{-}     & file to write SMT problems when \texttt{prover = offline} \\
      \texttt{tests}           & \texttt{100}   & number of tests to run for \texttt{:check} \\
     \hline
   \end{tabular*}

src/Cryptol/REPL/Command.hs

@@ -545,7 +545,7 @@ ppReport tys _ (TestReport exprDoc failure _testNum _testPossible) =
 
 ppFailure :: [E.TValue] -> Doc -> TestResult -> REPL ()
 ppFailure tys exprDoc failure = do
-    ~(EnvBool showEx) <- getUser "show-examples"
+    ~(EnvBool showEx) <- getUser "showExamples"
 
     vs <- case failure of
             FailFalse vs ->
@@ -641,7 +641,7 @@ rethrowErrorCall m = REPL (\r -> unREPL m r `X.catches` hs)
 safeCmd :: String -> (Int,Int) -> Maybe FilePath -> REPL ()
 safeCmd str pos fnm = do
   proverName <- getKnownUser "prover"
-  fileName   <- getKnownUser "smtfile"
+  fileName   <- getKnownUser "smtFile"
   let mfile = if fileName == "-" then Nothing else Just fileName
   pexpr <- replParseExpr str pos fnm
   nd <- M.mctxNameDisp <$> getFocusedEnv
@@ -669,7 +669,7 @@ safeCmd str pos fnm = do
 
             (t,e) <- mkSolverResult "counterexample" rng False (Right tes)
 
-            ~(EnvBool yes) <- getUser "show-examples"
+            ~(EnvBool yes) <- getUser "showExamples"
             when yes $ printCounterexample cexType exprDoc vs
             when yes $ printSafetyViolation texpr schema vs
 
@@ -723,7 +723,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
              | otherwise = "counterexample"
   qtype <- if isSat then SatQuery <$> getUserSatNum else pure ProveQuery
   proverName <- getKnownUser "prover"
-  fileName   <- getKnownUser "smtfile"
+  fileName   <- getKnownUser "smtFile"
   let mfile = if fileName == "-" then Nothing else Just fileName
 
   if proverName `elem` ["offline","sbv-offline","w4-offline"] then
@@ -748,7 +748,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
 
             (t,e) <- mkSolverResult cexStr rng isSat (Right tes)
 
-            ~(EnvBool yes) <- getUser "show-examples"
+            ~(EnvBool yes) <- getUser "showExamples"
             when yes $ printCounterexample cexType exprDoc vs
 
             -- if there's a safety violation, evalute the counterexample to
@@ -778,7 +778,7 @@ proveSatExpr isSat rng exprDoc texpr schema = do
                     [(t, e)] -> (t, [e])
                     _        -> collectTes resultRecs
 
-            ~(EnvBool yes) <- getUser "show-examples"
+            ~(EnvBool yes) <- getUser "showExamples"
             when yes $ forM_ vss (printSatisfyingModel exprDoc)
 
             case exprs of
@@ -812,7 +812,7 @@ onlineProveSat proverName qtype expr schema mfile = do
   validEvalContext schema
   decls <- fmap M.deDecls getDynEnv
   timing <- io (newIORef 0)
-  ~(EnvBool ignoreSafety) <- getUser "ignore-safety"
+  ~(EnvBool ignoreSafety) <- getUser "ignoreSafety"
   let cmd = ProverCommand {
           pcQueryType    = qtype
         , pcProverName   = proverName
@@ -828,7 +828,7 @@ onlineProveSat proverName qtype expr schema mfile = do
   (firstProver, res) <- getProverConfig >>= \case
        Left sbvCfg -> liftModuleCmd $ SBV.satProve sbvCfg cmd
        Right w4Cfg ->
-         do ~(EnvBool hashConsing) <- getUser "hash-consing"
+         do ~(EnvBool hashConsing) <- getUser "hashConsing"
             ~(EnvBool warnUninterp) <- getUser "warnUninterp"
             liftModuleCmd $ W4.satProve w4Cfg hashConsing warnUninterp cmd
 
@@ -842,7 +842,7 @@ offlineProveSat proverName qtype expr schema mfile = do
 
   decls <- fmap M.deDecls getDynEnv
   timing <- io (newIORef 0)
-  ~(EnvBool ignoreSafety) <- getUser "ignore-safety"
+  ~(EnvBool ignoreSafety) <- getUser "ignoreSafety"
   let cmd = ProverCommand {
           pcQueryType    = qtype
         , pcProverName   = proverName
@@ -882,7 +882,7 @@ offlineProveSat proverName qtype expr schema mfile = do
                Nothing -> rPutStr smtlib
 
     Right w4Cfg ->
-      do ~(EnvBool hashConsing) <- getUser "hash-consing"
+      do ~(EnvBool hashConsing) <- getUser "hashConsing"
          ~(EnvBool warnUninterp) <- getUser "warnUninterp"
          result <- liftModuleCmd $ W4.satProveOffline w4Cfg hashConsing warnUninterp cmd $ \f ->
                      do displayMsg

src/Cryptol/REPL/Monad.hs

@@ -60,6 +60,7 @@ module Cryptol.REPL.Monad (
   , OptionDescr(..)
   , setUser, getUser, getKnownUser, tryGetUser
   , userOptions
+  , userOptionsWithAliases
   , getUserSatNum
   , getUserShowProverStats
   , getUserProverValidate
@@ -399,8 +400,8 @@ getPPValOpts =
      ascii     <- getKnownUser "ascii"
      infLength <- getKnownUser "infLength"
 
-     fpBase    <- getKnownUser "fp-base"
-     fpFmtTxt  <- getKnownUser "fp-format"
+     fpBase    <- getKnownUser "fpBase"
+     fpFmtTxt  <- getKnownUser "fpFormat"
      let fpFmt = case parsePPFloatFormat fpFmtTxt of
                    Just f  -> f
                    Nothing -> panic "getPPOpts"
@@ -637,7 +638,7 @@ mkUserEnv opts = Map.fromList $ do
 
 -- | Set a user option.
 setUser :: String -> String -> REPL ()
-setUser name val = case lookupTrieExact name userOptions of
+setUser name val = case lookupTrieExact name userOptionsWithAliases of
 
   [opt] -> setUserOpt opt
   []    -> rPutStrLn ("Unknown env value `" ++ name ++ "`")
@@ -740,10 +741,10 @@ badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]
 
 
 getUserShowProverStats :: REPL Bool
-getUserShowProverStats = getKnownUser "prover-stats"
+getUserShowProverStats = getKnownUser "proverStats"
 
 getUserProverValidate :: REPL Bool
-getUserProverValidate = getKnownUser "prover-validate"
+getUserProverValidate = getKnownUser "proverValidate"
 
 -- Environment Options ---------------------------------------------------------
 
@@ -765,47 +766,53 @@ noWarns mb = return (mb, [])
 
 data OptionDescr = OptionDescr
   { optName    :: String
+  , optAliases :: [String]
   , optDefault :: EnvVal
   , optCheck   :: Checker
   , optHelp    :: String
   , optEff     :: EnvVal -> REPL ()
   }
 
-simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
-simpleOpt optName optDefault optCheck optHelp =
+simpleOpt :: String -> [String] -> EnvVal -> Checker -> String -> OptionDescr
+simpleOpt optName optAliases optDefault optCheck optHelp =
   OptionDescr { optEff = \ _ -> return (), .. }
 
+userOptionsWithAliases :: OptionMap
+userOptionsWithAliases = foldl insert userOptions (leaves userOptions)
+  where
+  insert m d = foldl (\m' n -> insertTrie n d m') m (optAliases d)
+
 userOptions :: OptionMap
 userOptions  = mkOptionMap
-  [ simpleOpt "base" (EnvNum 16) checkBase
+  [ simpleOpt "base" [] (EnvNum 16) checkBase
     "The base to display words at (2, 8, 10, or 16)."
-  , simpleOpt "debug" (EnvBool False) noCheck
+  , simpleOpt "debug" [] (EnvBool False) noCheck
     "Enable debugging output."
-  , simpleOpt "ascii" (EnvBool False) noCheck
+  , simpleOpt "ascii" [] (EnvBool False) noCheck
     "Whether to display 7- or 8-bit words using ASCII notation."
-  , simpleOpt "infLength" (EnvNum 5) checkInfLength
+  , simpleOpt "infLength" ["inf-length"] (EnvNum 5) checkInfLength
     "The number of elements to display for infinite sequences."
-  , simpleOpt "tests" (EnvNum 100) noCheck
+  , simpleOpt "tests" [] (EnvNum 100) noCheck
     "The number of random tests to try with ':check'."
-  , simpleOpt "satNum" (EnvString "1") checkSatNum
+  , simpleOpt "satNum" ["sat-num"] (EnvString "1") checkSatNum
     "The maximum number of :sat solutions to display (\"all\" for no limit)."
-  , simpleOpt "prover" (EnvString "z3") checkProver $
+  , simpleOpt "prover" [] (EnvString "z3") checkProver $
     "The external SMT solver for ':prove' and ':sat'\n(" ++ proverListString ++ ")."
-  , simpleOpt "warnDefaulting" (EnvBool False) noCheck
+  , simpleOpt "warnDefaulting" ["warn-defaulting"] (EnvBool False) noCheck
     "Choose whether to display warnings when defaulting."
-  , simpleOpt "warnShadowing" (EnvBool True) noCheck
+  , simpleOpt "warnShadowing" ["warn-shadowing"] (EnvBool True) noCheck
     "Choose whether to display warnings when shadowing symbols."
-  , simpleOpt "warnUninterp" (EnvBool True) noCheck
+  , simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck
     "Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
-  , simpleOpt "smtfile" (EnvString "-") noCheck
+  , simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
     "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
-  , OptionDescr "mono-binds" (EnvBool True) noCheck
+  , OptionDescr "monoBinds" ["mono-binds"] (EnvBool True) noCheck
     "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" ])
+  , OptionDescr "tcSolver" ["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." $
     \case EnvProg prog args -> do me <- getModuleEnv
@@ -815,7 +822,7 @@ userOptions  = mkOptionMap
                                                           , T.solverArgs = args } }
           _                 -> return ()
 
-  , OptionDescr "tc-debug" (EnvNum 0)
+  , OptionDescr "tcDebug" ["tc-debug"] (EnvNum 0)
     noCheck
     (unlines
       [ "Enable type-checker debugging output:"
@@ -826,7 +833,7 @@ userOptions  = mkOptionMap
                          let cfg = M.meSolverConfig me
                          setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = n } }
           _        -> return ()
-  , OptionDescr "core-lint" (EnvBool False)
+  , OptionDescr "coreLint" ["core-lint"] (EnvBool False)
     noCheck
     "Enable sanity checking of type-checker." $
       let setIt x = do me <- getModuleEnv
@@ -835,22 +842,22 @@ userOptions  = mkOptionMap
                EnvBool False -> setIt M.NoCoreLint
                _             -> return ()
 
-  , simpleOpt "hash-consing" (EnvBool True) noCheck
+  , simpleOpt "hashConsing" ["hash-consing"] (EnvBool True) noCheck
     "Enable hash-consing in the What4 symbolic backends."
 
-  , simpleOpt "prover-stats" (EnvBool True) noCheck
+  , simpleOpt "proverStats" ["prover-stats"] (EnvBool True) noCheck
     "Enable prover timing statistics."
 
-  , simpleOpt "prover-validate" (EnvBool False) noCheck
+  , simpleOpt "proverValidate" ["prover-validate"] (EnvBool False) noCheck
     "Validate :sat examples and :prove counter-examples for correctness."
 
-  , simpleOpt "show-examples" (EnvBool True) noCheck
+  , simpleOpt "showExamples" ["show-examples"] (EnvBool True) noCheck
     "Print the (counter) example after :sat or :prove"
 
-  , simpleOpt "fp-base" (EnvNum 16) checkBase
+  , simpleOpt "fpBase" ["fp-base"] (EnvNum 16) checkBase
     "The base to display floating point numbers at (2, 8, 10, or 16)."
 
-  , simpleOpt "fp-format" (EnvString "free") checkPPFloatFormat
+  , simpleOpt "fpFormat" ["fp-format"] (EnvString "free") checkPPFloatFormat
     $ unlines
     [ "Specifies the format to use when showing floating point numbers:"
     , "  * free      show using as many digits as needed"
@@ -860,7 +867,7 @@ userOptions  = mkOptionMap
     , "  * NUM+exp   like NUM but always show exponent"
     ]
 
-  , simpleOpt "ignore-safety" (EnvBool False) noCheck
+  , simpleOpt "ignoreSafety" ["ignore-safety"] (EnvBool False) noCheck
     "Ignore safety predicates when performing :sat or :prove checks"
   ]
 

src/Cryptol/REPL/Trie.hs

@@ -9,6 +9,7 @@
 module Cryptol.REPL.Trie where
 
 import           Cryptol.Utils.Panic (panic)
+import           Data.Char (toLower)
 import qualified Data.Map as Map
 import           Data.Maybe (fromMaybe,maybeToList)
 
@@ -20,13 +21,13 @@ data Trie a = Node (Map.Map Char (Trie a)) (Maybe a)
 emptyTrie :: Trie a
 emptyTrie  = Node Map.empty Nothing
 
--- | Insert a value into the Trie.  Will call `panic` if a value already exists
--- with that key.
+-- | Insert a value into the Trie, forcing the key value to lower case.
+--   Will call `panic` if a value already exists with that key.
 insertTrie :: String -> a -> Trie a -> Trie a
 insertTrie k a = loop k
   where
   loop key (Node m mb) = case key of
-    c:cs -> Node (Map.alter (Just . loop cs . fromMaybe emptyTrie) c m) mb
+    c:cs -> Node (Map.alter (Just . loop cs . fromMaybe emptyTrie) (toLower c) m) mb
     []   -> case mb of
       Nothing -> Node m (Just a)
       Just _  -> panic "[REPL] Trie" ["key already exists:", "\t" ++ k]
@@ -35,7 +36,7 @@ insertTrie k a = loop k
 lookupTrie :: String -> Trie a -> [a]
 lookupTrie key t@(Node mp _) = case key of
 
-  c:cs -> case Map.lookup c mp of
+  c:cs -> case Map.lookup (toLower c) mp of
     Just m' -> lookupTrie cs m'
     Nothing -> []
 
@@ -47,7 +48,7 @@ lookupTrieExact :: String -> Trie a -> [a]
 lookupTrieExact []     (Node _ (Just x)) = return x
 lookupTrieExact []     t                 = leaves t
 lookupTrieExact (c:cs) (Node mp _)       =
-  case Map.lookup c mp of
+  case Map.lookup (toLower c) mp of
     Just m' -> lookupTrieExact cs m'
     Nothing -> []
 

tests/regression/float.icry

@@ -2,8 +2,8 @@
 :set ascii=on
 
 section "Float Formatting"
-:help :set fp-base
-:help :set fp-format
+:help :set fpBase
+:help :set fpFormat
 
 :set fp-base=2
 10.25 : Medium

tests/regression/float.icry.stdout

@@ -4,14 +4,14 @@ Loading module Float
 Loading module FloatTests
 "-- Float Formatting-----------------------------------------------------------"
 
-    fp-base = 16
+    fpBase = 16
 
 Default value: 16
 
 The base to display floating point numbers at (2, 8, 10, or 16).
 
 
-    fp-format = free
+    fpFormat = free
 
 Default value: free