    -- |
    -- Module      :  Cryptol.REPL.Monad
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE ViewPatterns #-}
    {-# LANGUAGE FlexibleInstances #-}

    module Cryptol.REPL.Monad (
        -- * REPL Monad
        REPL(..), runREPL
      , io
      , raise
      , stop
      , catch
      , rPutStrLn
      , rPutStr
      , rPrint

        -- ** Errors
      , REPLException(..)
      , rethrowEvalError

        -- ** Environment
      , getFocusedEnv
      , getModuleEnv, setModuleEnv
      , getDynEnv, setDynEnv
      , uniqify, freshName
      , getTSyns, getNewtypes, getVars
      , whenDebug
      , getExprNames
      , getTypeNames
      , getPropertyNames
      , getModNames
      , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod, setEditPath
      , setSearchPath, prependSearchPath
      , getPrompt
      , shouldContinue
      , unlessBatch
      , asBatch
      , disableLet
      , enableLet
      , getLetEnabled
      , validEvalContext
      , updateREPLTitle
      , setUpdateREPLTitle

        -- ** Config Options
      , EnvVal(..)
      , OptionDescr(..)
      , setUser, getUser, getKnownUser, tryGetUser
      , userOptions
      , getUserSatNum
      , getUserShowProverStats

        -- ** Configurable Output
      , getPutStr
      , getLogger
      , setPutStr

        -- ** Smoke Test
      , smokeTest
      , Smoke(..)

      ) where

    import Cryptol.REPL.Trie

    import Cryptol.Eval (EvalError)
    import qualified Cryptol.ModuleSystem as M
    import qualified Cryptol.ModuleSystem.Env as M
    import qualified Cryptol.ModuleSystem.Name as M
    import qualified Cryptol.ModuleSystem.NamingEnv as M
    import Cryptol.Parser (ParseError,ppError)
    import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
    import Cryptol.Parser.NoPat (Error)
    import Cryptol.Parser.Position (emptyRange, Range(from))
    import qualified Cryptol.TypeCheck.AST as T
    import qualified Cryptol.TypeCheck as T
    import qualified Cryptol.IR.FreeVars as T
    import qualified Cryptol.Utils.Ident as I
    import Cryptol.Utils.PP
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
    import qualified Cryptol.Parser.AST as P
    import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))

    import Control.Monad (ap,unless,when,msum)
    import Control.Monad.Base
    import Control.Monad.IO.Class
    import Control.Monad.Trans.Control
    import Data.Char (isSpace)
    import Data.IORef
        (IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
    import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
    import Data.Maybe (catMaybes,mapMaybe)
    import Data.Ord (comparing)
    import Data.Typeable (Typeable)
    import System.Directory (findExecutable)
    import qualified Control.Exception as X
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Text.Read (readMaybe)

    import Data.SBV.Dynamic (sbvCheckSolverInstallation)

    import Prelude ()
    import Prelude.Compat

    -- REPL Environment ------------------------------------------------------------

    -- | This indicates what the user would like to work on.
    data LoadedModule = LoadedModule
      { lName :: Maybe P.ModName -- ^ Working on this module.
      , lPath :: FilePath        -- ^ Working on this file.
      }

    -- | REPL RW Environment.
    data RW = RW
      { eLoadedMod   :: Maybe LoadedModule
        -- ^ This is the name of the currently "focused" module.
        -- This is what we edit (:e) or reload (:r)

      , eContinue    :: Bool
        -- ^ Should we keep going when we encounter an error, or give up.

      , eIsBatch     :: Bool
        -- ^ Are we in batch mode.

      , eModuleEnv   :: M.ModuleEnv
        -- ^ The current environment of all things loaded.

      , eUserEnv     :: UserEnv
        -- ^ User settings

      , eLogger      :: Logger
        -- ^ Use this to send messages to the user

      , eLetEnabled  :: Bool
        -- ^ Should we allow `let` on the command line

      , eUpdateTitle :: REPL ()
        -- ^ Execute this every time we load a module.
        -- This is used to change the title of terminal when loading a module.
      }

    -- | Initial, empty environment.
    defaultRW :: Bool -> Logger -> IO RW
    defaultRW isBatch l = do
      env <- M.initialModuleEnv
      return RW
        { eLoadedMod   = Nothing
        , eContinue    = True
        , eIsBatch     = isBatch
        , eModuleEnv   = env
        , eUserEnv     = mkUserEnv userOptions
        , eLogger      = l
        , eLetEnabled  = True
        , eUpdateTitle = return ()
        }

    -- | Build up the prompt for the REPL.
    mkPrompt :: RW -> String
    mkPrompt rw
      | eIsBatch rw = ""
      | otherwise   = maybe "cryptol" pretty (lName =<< eLoadedMod rw) ++ "> "

    -- REPL Monad ------------------------------------------------------------------

    -- | REPL_ context with InputT handling.
    newtype REPL a = REPL { unREPL :: IORef RW -> IO a }

    -- | Run a REPL action with a fresh environment.
    runREPL :: Bool -> Logger -> REPL a -> IO a
    runREPL isBatch l m = do
      ref <- newIORef =<< defaultRW isBatch l
      unREPL m ref

    instance Functor REPL where
      {-# INLINE fmap #-}
      fmap f m = REPL (\ ref -> fmap f (unREPL m ref))

    instance Applicative REPL where
      {-# INLINE pure #-}
      pure = return
      {-# INLINE (<*>) #-}
      (<*>) = ap

    instance Monad REPL where
      {-# INLINE return #-}
      return x = REPL (\_ -> return x)

      {-# INLINE (>>=) #-}
      m >>= f = REPL $ \ref -> do
        x <- unREPL m ref
        unREPL (f x) ref

    instance MonadIO REPL where
      liftIO = io

    instance MonadBase IO REPL where
      liftBase = liftIO

    instance MonadBaseControl IO REPL where
      type StM REPL a = a
      liftBaseWith f = REPL $ \ref ->
        f $ \m -> unREPL m ref
      restoreM x = return x

    instance M.FreshM REPL where
      liftSupply f = modifyRW $ \ RW { .. } ->
        let (a,s') = f (M.meSupply eModuleEnv)
         in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)

    -- Exceptions ------------------------------------------------------------------

    -- | REPL exceptions.
    data REPLException
      = ParseError ParseError
      | FileNotFound FilePath
      | DirectoryNotFound FilePath
      | NoPatError [Error]
      | NoIncludeError [IncludeError]
      | EvalError EvalError
      | ModuleSystemError NameDisp M.ModuleError
      | EvalPolyError T.Schema
      | TypeNotTestable T.Type
      | EvalInParamModule P.ModName [M.Name]
      | SBVError String
        deriving (Show,Typeable)

    instance X.Exception REPLException

    instance PP REPLException where
      ppPrec _ re = case re of
        ParseError e         -> ppError e
        FileNotFound path    -> sep [ text "File"
                                    , text ("`" ++ path ++ "'")
                                    , text"not found"
                                    ]
        DirectoryNotFound path -> sep [ text "Directory"
                                      , text ("`" ++ path ++ "'")
                                      , text"not found or not a directory"
                                      ]
        NoPatError es        -> vcat (map pp es)
        NoIncludeError es    -> vcat (map ppIncludeError es)
        ModuleSystemError ns me -> fixNameDisp ns (pp me)
        EvalError e          -> pp e
        EvalPolyError s      -> text "Cannot evaluate polymorphic value."
                             $$ text "Type:" <+> pp s
        TypeNotTestable t    -> text "The expression is not of a testable type."
                             $$ text "Type:" <+> pp t
        EvalInParamModule _ xs ->
          text "Expression depends on a module parameter:" <+> hsep (map pp xs)
        SBVError s           -> text "SBV error:" $$ text s

    -- | Raise an exception.
    raise :: REPLException -> REPL a
    raise exn = io (X.throwIO exn)

    catch :: REPL a -> (REPLException -> REPL a) -> REPL a
    catch m k = REPL (\ ref -> rethrowEvalError (unREPL m ref) `X.catch` \ e -> unREPL (k e) ref)

    rethrowEvalError :: IO a -> IO a
    rethrowEvalError m = run `X.catch` rethrow
      where
      run = do
        a <- m
        return $! a

      rethrow :: EvalError -> IO a
      rethrow exn = X.throwIO (EvalError exn)

    -- Primitives ------------------------------------------------------------------

    io :: IO a -> REPL a
    io m = REPL (\ _ -> m)

    getRW :: REPL RW
    getRW  = REPL readIORef

    modifyRW :: (RW -> (RW,a)) -> REPL a
    modifyRW f = REPL (\ ref -> atomicModifyIORef ref f)

    modifyRW_ :: (RW -> RW) -> REPL ()
    modifyRW_ f = REPL (\ ref -> modifyIORef ref f)

    -- | Construct the prompt for the current environment.
    getPrompt :: REPL String
    getPrompt  = mkPrompt `fmap` getRW

    clearLoadedMod :: REPL ()
    clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw })
                        updateREPLTitle
      where upd x = x { lName = Nothing }

    -- | Set the name of the currently focused file, edited by @:e@ and loaded via
    -- @:r@.
    setLoadedMod :: LoadedModule -> REPL ()
    setLoadedMod n = do
      modifyRW_ (\ rw -> rw { eLoadedMod = Just n })
      updateREPLTitle

    setEditPath :: FilePath -> REPL ()
    setEditPath p = setLoadedMod LoadedModule { lName = Nothing, lPath = p }

    getLoadedMod :: REPL (Maybe LoadedModule)
    getLoadedMod  = eLoadedMod `fmap` getRW

    setSearchPath :: [FilePath] -> REPL ()
    setSearchPath path = do
      me <- getModuleEnv
      setModuleEnv $ me { M.meSearchPath = path }

    prependSearchPath :: [FilePath] -> REPL ()
    prependSearchPath path = do
      me <- getModuleEnv
      setModuleEnv $ me { M.meSearchPath = path ++ M.meSearchPath me }

    shouldContinue :: REPL Bool
    shouldContinue  = eContinue `fmap` getRW

    stop :: REPL ()
    stop  = modifyRW_ (\ rw -> rw { eContinue = False })

    unlessBatch :: REPL () -> REPL ()
    unlessBatch body = do
      rw <- getRW
      unless (eIsBatch rw) body

    -- | Run a computation in batch mode, restoring the previous isBatch
    -- flag afterwards
    asBatch :: REPL a -> REPL a
    asBatch body = do
      wasBatch <- eIsBatch `fmap` getRW
      modifyRW_ $ (\ rw -> rw { eIsBatch = True })
      a <- body
      modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch })
      return a

    disableLet :: REPL ()
    disableLet  = modifyRW_ (\ rw -> rw { eLetEnabled = False })

    enableLet :: REPL ()
    enableLet  = modifyRW_ (\ rw -> rw { eLetEnabled = True })

    -- | Are let-bindings enabled in this REPL?
    getLetEnabled :: REPL Bool
    getLetEnabled = fmap eLetEnabled getRW

    -- | Is evaluation enabled.  If the currently focused module is
    -- parameterized, then we cannot evalute.
    validEvalContext :: T.FreeVars a => a -> REPL ()
    validEvalContext a =
      do me <- eModuleEnv <$> getRW
         case M.meFocusedModule me of
           Nothing -> return ()
           Just fm ->
             case M.lookupModule fm me of
               Just lm
                 | Set.null tps && Set.null vps -> return ()
                 | Just xs <- check (T.freeVars a) ->
                                  raise $ EvalInParamModule fm xs
                 | otherwise -> return ()
                 where
                 m = M.lmModule lm

                 tps = Set.fromList $ map T.mtpParam $ Map.elems $ T.mParamTypes m
                 vps = Map.keysSet (T.mParamFuns m)

                 bad ds | not $ null badTP = Just $ mapMaybe T.tpName badTP
                        | not $ null badVP = Just badVP
                        | otherwise = Nothing
                   where
                   badTP = Set.toList $ Set.intersection tps (T.tyParams ds)
                   badVP = Set.toList $ Set.intersection vps (T.valDeps ds)

                 check ds   = msum (bad ds : map badSub (Set.toList (T.valDeps ds)))
                 badSub x   = maybe Nothing bad (Map.lookup x deps)
                 deps       = T.moduleDeps m

               Nothing ->
                 panic "getEvalEnabled" ["The focused module is not loaded."
                                        , show fm ]

    -- | Update the title
    updateREPLTitle :: REPL ()
    updateREPLTitle  = unlessBatch $ do
      rw <- getRW
      eUpdateTitle rw

    -- | Set the function that will be called when updating the title
    setUpdateREPLTitle :: REPL () -> REPL ()
    setUpdateREPLTitle m = modifyRW_ (\rw -> rw { eUpdateTitle = m })

    -- | Set the REPL's string-printer
    setPutStr :: (String -> IO ()) -> REPL ()
    setPutStr fn = modifyRW_ $ \rw -> rw { eLogger = funLogger fn }

    -- | Get the REPL's string-printer
    getPutStr :: REPL (String -> IO ())
    getPutStr =
      do rw <- getRW
         return (logPutStr (eLogger rw))

    getLogger :: REPL Logger
    getLogger = eLogger <$> getRW

    -- | Use the configured output action to print a string
    rPutStr :: String -> REPL ()
    rPutStr str = do
      f <- getPutStr
      io (f str)

    -- | Use the configured output action to print a string with a trailing newline
    rPutStrLn :: String -> REPL ()
    rPutStrLn str = rPutStr $ str ++ "\n"

    -- | Use the configured output action to print something using its Show instance
    rPrint :: Show a => a -> REPL ()
    rPrint x = rPutStrLn (show x)

    getFocusedEnv :: REPL (M.IfaceParams,M.IfaceDecls,M.NamingEnv,NameDisp)
    getFocusedEnv  = do
      me <- getModuleEnv
      -- dyNames is a NameEnv that removes the #Uniq prefix from interactively-bound
      -- variables.
      let (dyDecls,dyNames,dyDisp) = M.dynamicEnv me
      let (fParams,fDecls,fNames,fDisp) = M.focusedEnv me
      return ( fParams
             , dyDecls `mappend` fDecls
             , dyNames `M.shadowing` fNames
             , dyDisp `mappend` fDisp)

      -- -- the subtle part here is removing the #Uniq prefix from
      -- -- interactively-bound variables, and also excluding any that are
      -- -- shadowed and thus can no longer be referenced
      -- let (fDecls,fNames,fDisp) = M.focusedEnv me
      --     edecls = M.ifDecls dyDecls
      --     -- is this QName something the user might actually type?
      --     isShadowed (qn@(P.QName (Just (P.unModName -> ['#':_])) name), _) =
      --         case Map.lookup localName neExprs of
      --           Nothing -> False
      --           Just uniqueNames -> isNamed uniqueNames
      --       where localName = P.QName Nothing name
      --             isNamed us = any (== qn) (map M.qname us)
      --             neExprs = M.neExprs (M.deNames (M.meDynEnv me))
      --     isShadowed _ = False
      --     unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
      --     edecls' = Map.fromList
      --             . map unqual
      --             . filter isShadowed
      --             $ Map.toList edecls
      -- return (decls `mappend` mempty { M.ifDecls = edecls' }, names `mappend` dyNames)

    getVars :: REPL (Map.Map M.Name M.IfaceDecl)
    getVars  = do
      (_,decls,_,_) <- getFocusedEnv
      return (M.ifDecls decls)

    getTSyns :: REPL (Map.Map M.Name T.TySyn)
    getTSyns  = do
      (_,decls,_,_) <- getFocusedEnv
      return (M.ifTySyns decls)

    getNewtypes :: REPL (Map.Map M.Name T.Newtype)
    getNewtypes = do
      (_,decls,_,_) <- getFocusedEnv
      return (M.ifNewtypes decls)

    -- | Get visible variable names.
    getExprNames :: REPL [String]
    getExprNames =
      do (_,_, fNames, _) <- getFocusedEnv
         return (map (show . pp) (Map.keys (M.neExprs fNames)))

    -- | Get visible type signature names.
    getTypeNames :: REPL [String]
    getTypeNames  =
      do (_,_, fNames, _) <- getFocusedEnv
         return (map (show . pp) (Map.keys (M.neTypes fNames)))

    -- | Return a list of property names, sorted by position in the file.
    getPropertyNames :: REPL ([M.Name],NameDisp)
    getPropertyNames =
      do (_,decls,_,names) <- getFocusedEnv
         let xs = M.ifDecls decls
             ps = sortBy (comparing (from . M.nameLoc))
                $ [ x | (x,d) <- Map.toList xs, T.PragmaProperty `elem` M.ifDeclPragmas d ]

         return (ps, names)

    getModNames :: REPL [I.ModName]
    getModNames =
      do me <- getModuleEnv
         return (map T.mName (M.loadedModules me))

    getModuleEnv :: REPL M.ModuleEnv
    getModuleEnv  = eModuleEnv `fmap` getRW

    setModuleEnv :: M.ModuleEnv -> REPL ()
    setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })

    getDynEnv :: REPL M.DynamicEnv
    getDynEnv  = (M.meDynEnv . eModuleEnv) `fmap` getRW

    setDynEnv :: M.DynamicEnv -> REPL ()
    setDynEnv denv = do
      me <- getModuleEnv
      setModuleEnv (me { M.meDynEnv = denv })

    -- | Given an existing qualified name, prefix it with a
    -- relatively-unique string. We make it unique by prefixing with a
    -- character @#@ that is not lexically valid in a module name.
    uniqify :: M.Name -> REPL M.Name

    uniqify name =
      case M.nameInfo name of
        M.Declared ns s ->
          M.liftSupply (M.mkDeclared ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name))

        M.Parameter ->
          panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name]

    -- uniqify (P.QName Nothing name) = do
    --   i <- eNameSupply `fmap` getRW
    --   modifyRW_ (\rw -> rw { eNameSupply = i+1 })
    --   let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ]
    --   return (P.QName (Just modname') name)

    -- uniqify qn =
    --   panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn]

    -- | Generate a fresh name using the given index. The name will reside within
    -- the "<interactive>" namespace.
    freshName :: I.Ident -> M.NameSource -> REPL M.Name
    freshName i sys =
      M.liftSupply (M.mkDeclared I.interactiveName sys i Nothing emptyRange)

    -- User Environment Interaction ------------------------------------------------

    -- | User modifiable environment, for things like numeric base.
    type UserEnv = Map.Map String EnvVal

    data EnvVal
      = EnvString String
      | EnvProg   String [String]
      | EnvNum    !Int
      | EnvBool   Bool
        deriving (Show)

    -- | Generate a UserEnv from a description of the options map.
    mkUserEnv :: OptionMap -> UserEnv
    mkUserEnv opts = Map.fromList $ do
      opt <- leaves opts
      return (optName opt, optDefault opt)

    -- | Set a user option.
    setUser :: String -> String -> REPL ()
    setUser name val = case lookupTrieExact name userOptions of

      [opt] -> setUserOpt opt
      []    -> rPutStrLn ("Unknown env value `" ++ name ++ "`")
      _     -> rPutStrLn ("Ambiguous env value `" ++ name ++ "`")

      where
      setUserOpt opt = case optDefault opt of
        EnvString _ -> doCheck (EnvString val)

        EnvProg _ _ ->
          case splitOptArgs val of
            prog:args -> doCheck (EnvProg prog args)
            [] -> rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`")

        EnvNum _ -> case reads val of
          [(x,_)] -> doCheck (EnvNum x)
          _ -> rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`")

        EnvBool _
          | any (`isPrefixOf` val) ["enable", "on", "yes", "true"] ->
            writeEnv (EnvBool True)
          | any (`isPrefixOf` val) ["disable", "off", "no", "false"] ->
            writeEnv (EnvBool False)
          | otherwise ->
            rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`")
        where
        doCheck v = do (r,ws) <- io (optCheck opt v)
                       case r of
                         Just err -> rPutStrLn err
                         Nothing  -> do mapM_ rPutStrLn ws
                                        writeEnv v
        writeEnv ev =
          do optEff opt ev
             modifyRW_ (\rw -> rw { eUserEnv = Map.insert (optName opt) ev (eUserEnv rw) })

    splitOptArgs :: String -> [String]
    splitOptArgs  = unfoldr (parse "")
      where

      parse acc (c:cs) | isQuote c       = quoted (c:acc) cs
                       | not (isSpace c) = parse (c:acc) cs
                       | otherwise       = result acc cs
      parse acc []                       = result acc []

      quoted acc (c:cs) | isQuote c      = parse  (c:acc) cs
                        | otherwise      = quoted (c:acc) cs
      quoted acc []                      = result acc []

      result []  [] = Nothing
      result []  cs = parse [] (dropWhile isSpace cs)
      result acc cs = Just (reverse acc, dropWhile isSpace cs)

      isQuote :: Char -> Bool
      isQuote c = c `elem` ("'\"" :: String)

    -- | Get a user option, using Maybe for failure.
    tryGetUser :: String -> REPL (Maybe EnvVal)
    tryGetUser name = do
      rw <- getRW
      return (Map.lookup name (eUserEnv rw))

    -- | Get a user option, when it's known to exist.  Fail with panic when it
    -- doesn't.
    getUser :: String -> REPL EnvVal
    getUser name = do
      mb <- tryGetUser name
      case mb of
        Just ev -> return ev
        Nothing -> panic "[REPL] getUser" ["option `" ++ name ++ "` does not exist"]

    getKnownUser :: IsEnvVal a => String -> REPL a
    getKnownUser x = fromEnvVal <$> getUser x

    class IsEnvVal a where
      fromEnvVal :: EnvVal -> a

    instance IsEnvVal Bool where
      fromEnvVal x = case x of
                       EnvBool b -> b
                       _         -> badIsEnv "Bool"

    instance IsEnvVal Int where
      fromEnvVal x = case x of
                       EnvNum b -> b
                       _         -> badIsEnv "Num"

    instance IsEnvVal (String,[String]) where
      fromEnvVal x = case x of
                       EnvProg b bs -> (b,bs)
                       _            -> badIsEnv "Prog"

    instance IsEnvVal String where
      fromEnvVal x = case x of
                       EnvString b -> b
                       _           -> badIsEnv "String"

    badIsEnv :: String -> a
    badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ]

    getUserShowProverStats :: REPL Bool
    getUserShowProverStats = getKnownUser "prover-stats"

    -- Environment Options ---------------------------------------------------------

    type OptionMap = Trie OptionDescr

    mkOptionMap :: [OptionDescr] -> OptionMap
    mkOptionMap  = foldl insert emptyTrie
      where
      insert m d = insertTrie (optName d) d m

    -- | Returns maybe an error, and some warnings
    type Checker = EnvVal -> IO (Maybe String, [String])

    noCheck :: Checker
    noCheck _ = return (Nothing, [])

    noWarns :: Maybe String -> IO (Maybe String, [String])
    noWarns mb = return (mb, [])

    data OptionDescr = OptionDescr
      { optName    :: String
      , optDefault :: EnvVal
      , optCheck   :: Checker
      , optHelp    :: String
      , optEff     :: EnvVal -> REPL ()
      }

    simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
    simpleOpt optName optDefault optCheck optHelp =
      OptionDescr { optEff = \ _ -> return (), .. }

    userOptions :: OptionMap
    userOptions  = mkOptionMap
      [ simpleOpt "base" (EnvNum 16) checkBase
        "The base to display words at (2, 8, 10, or 16)."
      , simpleOpt "debug" (EnvBool False) noCheck
        "Enable debugging output."
      , simpleOpt "ascii" (EnvBool False) noCheck
        "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 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'\n(" ++ proverListString ++ ")."
      , simpleOpt "warnDefaulting" (EnvBool True) noCheck
        "Choose whether to display warnings when defaulting."
      , simpleOpt "warnShadowing" (EnvBool True) noCheck
        "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).\nUse \"-\" for stdout."
      , OptionDescr "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" ])
        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
                                      let cfg = M.meSolverConfig me
                                      setModuleEnv me { M.meSolverConfig =
                                                          cfg { T.solverPath = prog
                                                              , T.solverArgs = args } }
              _                 -> return ()

      , OptionDescr "tc-debug" (EnvNum 0)
        noCheck
        "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." $
          let setIt x = do me <- getModuleEnv
                           setModuleEnv me { M.meCoreLint = x }
          in \case EnvBool True  -> setIt M.CoreLint
                   EnvBool False -> setIt M.NoCoreLint
                   _             -> return ()

      , simpleOpt "prover-stats" (EnvBool True) noCheck
        "Enable prover timing statistics."
      ]

    -- | Check the value to the `base` option.
    checkBase :: Checker
    checkBase val = case val of
      EnvNum n
        | n `elem` [2,8,10,16] -> noWarns Nothing
        | otherwise            -> noWarns $ Just "base must be 2, 8, 10, or 16"
      _                     -> noWarns $ Just "unable to parse a value for base"

    checkInfLength :: Checker
    checkInfLength val = case val of
      EnvNum n
        | n >= 0    -> noWarns Nothing
        | otherwise -> noWarns $ Just "the number of elements should be positive"
      _ -> noWarns $ Just "unable to parse a value for infLength"

    checkProver :: Checker
    checkProver val = case val of
      EnvString s
        | s `notElem` proverNames ->
          noWarns $ Just $ "Prover must be " ++ proverListString
        | s `elem` ["offline", "any"] -> noWarns Nothing
        | otherwise ->
          do let prover = lookupProver s
             available <- sbvCheckSolverInstallation prover
             let ws = if available
                         then []
                         else ["Warning: " ++ s ++ " installation not found"]
             return (Nothing, ws)

      _ -> noWarns $ Just "unable to parse a value for prover"

    proverListString :: String
    proverListString = concatMap (++ ", ") (init proverNames) ++ "or " ++ last proverNames

    checkSatNum :: Checker
    checkSatNum val = case val of
      EnvString "all" -> noWarns Nothing
      EnvString s ->
        case readMaybe s :: Maybe Int of
          Just n | n >= 1 -> noWarns Nothing
          _               -> noWarns $ Just "must be an integer > 0 or \"all\""
      _ -> noWarns $ Just "unable to parse a value for satNum"

    getUserSatNum :: REPL SatNum
    getUserSatNum = do
      s <- getKnownUser "satNum"
      case s of
        "all"                     -> return AllSat
        _ | Just n <- readMaybe s -> return (SomeSat n)
        _                         -> panic "REPL.Monad.getUserSatNum"
                                       [ "invalid satNum option" ]

    -- Environment Utilities -------------------------------------------------------

    whenDebug :: REPL () -> REPL ()
    whenDebug m = do
      b <- getKnownUser "debug"
      when b m

    -- Smoke Testing ---------------------------------------------------------------

    smokeTest :: REPL [Smoke]
    smokeTest = catMaybes <$> sequence tests
      where
        tests = [ z3exists ]

    type SmokeTest = REPL (Maybe Smoke)

    data Smoke
      = Z3NotFound
      deriving (Show, Eq)

    instance PP Smoke where
      ppPrec _ smoke =
        case smoke of
          Z3NotFound -> text . intercalate " " $ [
              "[error] z3 is required to run Cryptol, but was not found in the"
            , "system path. See the Cryptol README for more on how to install z3."
            ]

    z3exists :: SmokeTest
    z3exists = do
      mPath <- io $ findExecutable "z3"
      case mPath of
        Nothing -> return (Just Z3NotFound)
        Just _  -> return Nothing