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

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

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

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

        -- ** Environment
      , getFocusedEnv
      , getModuleEnv, setModuleEnv
      , getDynEnv, setDynEnv
      , getCallStacks
      , getTCSolver
      , resetTCSolver
      , uniqify, freshName
      , whenDebug
      , getEvalOptsAction
      , getPPValOpts
      , getExprNames
      , getTypeNames
      , getPropertyNames
      , getModNames
      , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
      , setEditPath, getEditPath, clearEditPath
      , setSearchPath, prependSearchPath
      , getPrompt
      , shouldContinue
      , unlessBatch
      , asBatch
      , validEvalContext
      , updateREPLTitle
      , setUpdateREPLTitle
      , withRandomGen
      , setRandomGen
      , getRandomGen

        -- ** Config Options
      , EnvVal(..)
      , OptionDescr(..)
      , setUser, getUser, getKnownUser, tryGetUser
      , userOptions
      , userOptionsWithAliases
      , getUserSatNum
      , getUserShowProverStats
      , getUserProverValidate
      , parsePPFloatFormat
      , parseFieldOrder
      , getProverConfig
      , parseSearchPath

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

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

      ) where

    import Cryptol.REPL.Trie

    import Cryptol.Eval (EvalErrorEx, Unsupported, WordTooWide,EvalOpts(..))
    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.TypeCheck.Solver.SMT as SMT
    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 (SatNum(..))
    import Cryptol.Symbolic.SBV (SBVPortfolioException)
    import Cryptol.Symbolic.What4 (W4Exception)
    import qualified Cryptol.Symbolic.SBV as SBV (proverNames, setupProver, defaultProver, SBVProverConfig)
    import qualified Cryptol.Symbolic.What4 as W4 (proverNames, setupProver, W4ProverConfig)

    import Control.Monad (ap,unless,when)
    import Control.Monad.Base
    import qualified Control.Monad.Catch as Ex
    import Control.Monad.IO.Class
    import Control.Monad.Trans.Control
    import Data.Char (isSpace, toLower)
    import Data.IORef
        (IORef,newIORef,readIORef,atomicModifyIORef)
    import Data.List (intercalate, isPrefixOf, unfoldr, sortBy)
    import Data.Maybe (catMaybes)
    import Data.Ord (comparing)
    import Data.Typeable (Typeable)
    import System.Directory (findExecutable)
    import System.FilePath (splitSearchPath, searchPathSeparator)
    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 (SBVException)
    import qualified System.Random.TF as TF

    import Prelude ()
    import Prelude.Compat

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

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

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

      , RW -> Maybe [Char]
    eEditFile :: Maybe FilePath
        -- ^ This is what we edit (:e)

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

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

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

      , RW -> UserEnv
    eUserEnv     :: UserEnv
        -- ^ User settings

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

      , RW -> Bool
    eCallStacks :: Bool

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

      , RW -> Either SBVProverConfig W4ProverConfig
    eProverConfig :: Either SBV.SBVProverConfig W4.W4ProverConfig

      , RW -> SolverConfig
    eTCConfig :: T.SolverConfig
        -- ^ Solver configuration to be used for typechecking

      , RW -> Maybe Solver
    eTCSolver :: Maybe SMT.Solver
        -- ^ Solver instance to be used for typechecking

      , RW -> Int
    eTCSolverRestarts :: !Int
        -- ^ Counts how many times we've restarted the solver.
        -- Used as a kind of id for the current solver, which helps avoid
        -- a race condition where the callback of a dead solver runs after
        -- a new one has been started.

      , RW -> TFGen
    eRandomGen :: TF.TFGen
        -- ^ Random number generator for things like QC and dumpTests
      }

    -- | Initial, empty environment.
    defaultRW :: Bool -> Bool -> Logger -> IO RW
    defaultRW :: Bool -> Bool -> Logger -> IO RW
    defaultRW Bool
    isBatch Bool
    callStacks Logger
    l = do
      ModuleEnv
    env <- IO ModuleEnv
    M.initialModuleEnv
      TFGen
    rng <- IO TFGen
    TF.newTFGen
      let searchPath :: [[Char]]
    searchPath = ModuleEnv -> [[Char]]
    M.meSearchPath ModuleEnv
    env
      let solverConfig :: SolverConfig
    solverConfig = [[Char]] -> SolverConfig
    T.defaultSolverConfig [[Char]]
    searchPath
      RW -> IO RW
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return RW
        { eLoadedMod :: Maybe LoadedModule
    eLoadedMod   = Maybe LoadedModule
    forall a. Maybe a
    Nothing
        , eEditFile :: Maybe [Char]
    eEditFile    = Maybe [Char]
    forall a. Maybe a
    Nothing
        , eContinue :: Bool
    eContinue    = Bool
    True
        , eIsBatch :: Bool
    eIsBatch     = Bool
    isBatch
        , eModuleEnv :: ModuleEnv
    eModuleEnv   = ModuleEnv
    env
        , eUserEnv :: UserEnv
    eUserEnv     = OptionMap -> UserEnv
    mkUserEnv OptionMap
    userOptions
        , eLogger :: Logger
    eLogger      = Logger
    l
        , eCallStacks :: Bool
    eCallStacks  = Bool
    callStacks
        , eUpdateTitle :: REPL ()
    eUpdateTitle = () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        , eProverConfig :: Either SBVProverConfig W4ProverConfig
    eProverConfig = SBVProverConfig -> Either SBVProverConfig W4ProverConfig
    forall a b. a -> Either a b
    Left SBVProverConfig
    SBV.defaultProver
        , eTCConfig :: SolverConfig
    eTCConfig    = SolverConfig
    solverConfig
        , eTCSolver :: Maybe Solver
    eTCSolver    = Maybe Solver
    forall a. Maybe a
    Nothing
        , eTCSolverRestarts :: Int
    eTCSolverRestarts = Int
    0
        , eRandomGen :: TFGen
    eRandomGen = TFGen
    rng
        }

    -- | Build up the prompt for the REPL.
    mkPrompt :: RW -> String
    mkPrompt :: RW -> [Char]
    mkPrompt RW
    rw
      | RW -> Bool
    eIsBatch RW
    rw = [Char]
    ""
      | Bool
    detailedPrompt = [Char]
    withEdit [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "> "
      | Bool
    otherwise      = [Char]
    modLn [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "> "
      where
      detailedPrompt :: Bool
    detailedPrompt = Bool -> Bool
    forall a. a -> a
    id Bool
    False

      modLn :: [Char]
    modLn   =
        case LoadedModule -> Maybe ModName
    lName (LoadedModule -> Maybe ModName)
    -> Maybe LoadedModule -> Maybe ModName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< RW -> Maybe LoadedModule
    eLoadedMod RW
    rw of
          Maybe ModName
    Nothing -> Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    I.preludeName)
          Just ModName
    m
            | ModName -> LoadedModules -> Bool
    M.isLoadedParamMod ModName
    m LoadedModules
    loaded -> [Char]
    modName [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "(parameterized)"
            | ModName -> LoadedModules -> Bool
    M.isLoadedInterface ModName
    m LoadedModules
    loaded -> [Char]
    modName [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "(interface)"
            | Bool
    otherwise -> [Char]
    modName
            where modName :: [Char]
    modName = ModName -> [Char]
    forall a. PP a => a -> [Char]
    pretty ModName
    m
                  loaded :: LoadedModules
    loaded = ModuleEnv -> LoadedModules
    M.meLoadedModules (RW -> ModuleEnv
    eModuleEnv RW
    rw)

      withFocus :: [Char]
    withFocus =
        case RW -> Maybe LoadedModule
    eLoadedMod RW
    rw of
          Maybe LoadedModule
    Nothing -> [Char]
    modLn
          Just LoadedModule
    m ->
            case (LoadedModule -> Maybe ModName
    lName LoadedModule
    m, LoadedModule -> ModulePath
    lPath LoadedModule
    m) of
              (Maybe ModName
    Nothing, M.InFile [Char]
    f) -> [Char]
    ":r to reload " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    forall a. Show a => a -> [Char]
    show [Char]
    f [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    modLn
              (Maybe ModName, ModulePath)
    _ -> [Char]
    modLn

      withEdit :: [Char]
    withEdit =
        case RW -> Maybe [Char]
    eEditFile RW
    rw of
          Maybe [Char]
    Nothing -> [Char]
    withFocus
          Just [Char]
    e
            | Just (M.InFile [Char]
    f) <- LoadedModule -> ModulePath
    lPath (LoadedModule -> ModulePath)
    -> Maybe LoadedModule -> Maybe ModulePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RW -> Maybe LoadedModule
    eLoadedMod RW
    rw
            , [Char]
    f [Char] -> [Char] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Char]
    e -> [Char]
    withFocus
            | Bool
    otherwise -> [Char]
    ":e to edit " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    e [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\n" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    withFocus

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

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

    -- | Run a REPL action with a fresh environment.
    runREPL :: Bool -> Bool -> Logger -> REPL a -> IO a
    runREPL :: forall a. Bool -> Bool -> Logger -> REPL a -> IO a
    runREPL Bool
    isBatch Bool
    callStacks Logger
    l REPL a
    m = do
      IO (IORef RW) -> (IORef RW -> IO ()) -> (IORef RW -> IO a) -> IO a
    forall (m :: * -> *) a c b.
    MonadMask m =>
    m a -> (a -> m c) -> (a -> m b) -> m b
    Ex.bracket
        (RW -> IO (IORef RW)
    forall a. a -> IO (IORef a)
    newIORef (RW -> IO (IORef RW)) -> IO RW -> IO (IORef RW)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Bool -> Bool -> Logger -> IO RW
    defaultRW Bool
    isBatch Bool
    callStacks Logger
    l)
        (REPL () -> IORef RW -> IO ()
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL ()
    resetTCSolver)
        (REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m)

    instance Functor REPL where
      {-# INLINE fmap #-}
      fmap :: forall a b. (a -> b) -> REPL a -> REPL b
    fmap a -> b
    f REPL a
    m = (IORef RW -> IO b) -> REPL b
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ IORef RW
    ref -> (a -> b) -> IO a -> IO b
    forall a b. (a -> b) -> IO a -> IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f (REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m IORef RW
    ref))

    instance Applicative REPL where
      {-# INLINE pure #-}
      pure :: forall a. a -> REPL a
    pure a
    x = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\IORef RW
    _ -> a -> IO a
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x)
      {-# INLINE (<*>) #-}
      <*> :: forall a b. REPL (a -> b) -> REPL a -> REPL b
    (<*>) = REPL (a -> b) -> REPL a -> REPL b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad REPL where
      {-# INLINE return #-}
      return :: forall a. a -> REPL a
    return = a -> REPL a
    forall a. a -> REPL a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure

      {-# INLINE (>>=) #-}
      REPL a
    m >>= :: forall a b. REPL a -> (a -> REPL b) -> REPL b
    >>= a -> REPL b
    f = (IORef RW -> IO b) -> REPL b
    forall a. (IORef RW -> IO a) -> REPL a
    REPL ((IORef RW -> IO b) -> REPL b) -> (IORef RW -> IO b) -> REPL b
    forall a b. (a -> b) -> a -> b
    $ \IORef RW
    ref -> do
        a
    x <- REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m IORef RW
    ref
        REPL b -> IORef RW -> IO b
    forall a. REPL a -> IORef RW -> IO a
    unREPL (a -> REPL b
    f a
    x) IORef RW
    ref

    instance MonadIO REPL where
      liftIO :: forall a. IO a -> REPL a
    liftIO = IO a -> REPL a
    forall a. IO a -> REPL a
    io

    instance MonadBase IO REPL where
      liftBase :: forall a. IO a -> REPL a
    liftBase = IO α -> REPL α
    forall a. IO a -> REPL a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO

    instance MonadBaseControl IO REPL where
      type StM REPL a = a
      liftBaseWith :: forall a. (RunInBase REPL IO -> IO a) -> REPL a
    liftBaseWith RunInBase REPL IO -> IO a
    f = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL ((IORef RW -> IO a) -> REPL a) -> (IORef RW -> IO a) -> REPL a
    forall a b. (a -> b) -> a -> b
    $ \IORef RW
    ref ->
        RunInBase REPL IO -> IO a
    f (RunInBase REPL IO -> IO a) -> RunInBase REPL IO -> IO a
    forall a b. (a -> b) -> a -> b
    $ \REPL a
    m -> REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m IORef RW
    ref
      restoreM :: forall a. StM REPL a -> REPL a
    restoreM StM REPL a
    x = a -> REPL a
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    StM REPL a
    x

    instance M.FreshM REPL where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> REPL a
    liftSupply Supply -> (a, Supply)
    f = (RW -> (RW, a)) -> REPL a
    forall a. (RW -> (RW, a)) -> REPL a
    modifyRW ((RW -> (RW, a)) -> REPL a) -> (RW -> (RW, a)) -> REPL a
    forall a b. (a -> b) -> a -> b
    $ \ RW { Bool
    Int
    Maybe [Char]
    Maybe Solver
    Maybe LoadedModule
    Either SBVProverConfig W4ProverConfig
    UserEnv
    TFGen
    Logger
    SolverConfig
    ModuleEnv
    REPL ()
    eLoadedMod :: RW -> Maybe LoadedModule
    eEditFile :: RW -> Maybe [Char]
    eContinue :: RW -> Bool
    eIsBatch :: RW -> Bool
    eModuleEnv :: RW -> ModuleEnv
    eUserEnv :: RW -> UserEnv
    eLogger :: RW -> Logger
    eCallStacks :: RW -> Bool
    eUpdateTitle :: RW -> REPL ()
    eProverConfig :: RW -> Either SBVProverConfig W4ProverConfig
    eTCConfig :: RW -> SolverConfig
    eTCSolver :: RW -> Maybe Solver
    eTCSolverRestarts :: RW -> Int
    eRandomGen :: RW -> TFGen
    eLoadedMod :: Maybe LoadedModule
    eEditFile :: Maybe [Char]
    eContinue :: Bool
    eIsBatch :: Bool
    eModuleEnv :: ModuleEnv
    eUserEnv :: UserEnv
    eLogger :: Logger
    eCallStacks :: Bool
    eUpdateTitle :: REPL ()
    eProverConfig :: Either SBVProverConfig W4ProverConfig
    eTCConfig :: SolverConfig
    eTCSolver :: Maybe Solver
    eTCSolverRestarts :: Int
    eRandomGen :: TFGen
    .. } ->
        let (a
    a,Supply
    s') = Supply -> (a, Supply)
    f (ModuleEnv -> Supply
    M.meSupply ModuleEnv
    eModuleEnv)
         in (RW { eModuleEnv :: ModuleEnv
    eModuleEnv = ModuleEnv
    eModuleEnv { meSupply :: Supply
    M.meSupply = Supply
    s' }, Bool
    Int
    Maybe [Char]
    Maybe Solver
    Maybe LoadedModule
    Either SBVProverConfig W4ProverConfig
    UserEnv
    TFGen
    Logger
    SolverConfig
    REPL ()
    eLoadedMod :: Maybe LoadedModule
    eEditFile :: Maybe [Char]
    eContinue :: Bool
    eIsBatch :: Bool
    eUserEnv :: UserEnv
    eLogger :: Logger
    eCallStacks :: Bool
    eUpdateTitle :: REPL ()
    eProverConfig :: Either SBVProverConfig W4ProverConfig
    eTCConfig :: SolverConfig
    eTCSolver :: Maybe Solver
    eTCSolverRestarts :: Int
    eRandomGen :: TFGen
    eLoadedMod :: Maybe LoadedModule
    eEditFile :: Maybe [Char]
    eContinue :: Bool
    eIsBatch :: Bool
    eUserEnv :: UserEnv
    eLogger :: Logger
    eCallStacks :: Bool
    eUpdateTitle :: REPL ()
    eProverConfig :: Either SBVProverConfig W4ProverConfig
    eTCConfig :: SolverConfig
    eTCSolver :: Maybe Solver
    eTCSolverRestarts :: Int
    eRandomGen :: TFGen
    .. },a
    a)

    instance Ex.MonadThrow REPL where
      throwM :: forall e a. Exception e => e -> REPL a
    throwM e
    e = IO a -> REPL a
    forall a. IO a -> REPL a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> REPL a) -> IO a -> REPL a
    forall a b. (a -> b) -> a -> b
    $ e -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO e
    e

    instance Ex.MonadCatch REPL where
      catch :: forall e a. Exception e => REPL a -> (e -> REPL a) -> REPL a
    catch REPL a
    op e -> REPL a
    handler = (RunInBase REPL IO -> IO (StM REPL a)) -> REPL a
    forall (b :: * -> *) (m :: * -> *) a.
    MonadBaseControl b m =>
    (RunInBase m b -> b (StM m a)) -> m a
    control ((RunInBase REPL IO -> IO (StM REPL a)) -> REPL a)
    -> (RunInBase REPL IO -> IO (StM REPL a)) -> REPL a
    forall a b. (a -> b) -> a -> b
    $ \RunInBase REPL IO
    runInBase -> IO a -> (e -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    forall (m :: * -> *) e a.
    (MonadCatch m, Exception e) =>
    m a -> (e -> m a) -> m a
    Ex.catch (REPL a -> IO (StM REPL a)
    RunInBase REPL IO
    runInBase REPL a
    op) (REPL a -> IO a
    REPL a -> IO (StM REPL a)
    RunInBase REPL IO
    runInBase (REPL a -> IO a) -> (e -> REPL a) -> e -> IO a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . e -> REPL a
    handler)

    instance Ex.MonadMask REPL where
      mask :: forall b. ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b
    mask (forall a. REPL a -> REPL a) -> REPL b
    op = (IORef RW -> IO b) -> REPL b
    forall a. (IORef RW -> IO a) -> REPL a
    REPL ((IORef RW -> IO b) -> REPL b) -> (IORef RW -> IO b) -> REPL b
    forall a b. (a -> b) -> a -> b
    $ \IORef RW
    ref -> ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall (m :: * -> *) b.
    MonadMask m =>
    ((forall a. m a -> m a) -> m b) -> m b
    Ex.mask (((forall a. IO a -> IO a) -> IO b) -> IO b)
    -> ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall a b. (a -> b) -> a -> b
    $ \forall a. IO a -> IO a
    u -> REPL b -> IORef RW -> IO b
    forall a. REPL a -> IORef RW -> IO a
    unREPL ((forall a. REPL a -> REPL a) -> REPL b
    op ((IO a -> IO a) -> REPL a -> REPL a
    forall {a} {a}. (IO a -> IO a) -> REPL a -> REPL a
    q IO a -> IO a
    forall a. IO a -> IO a
    u)) IORef RW
    ref
        where q :: (IO a -> IO a) -> REPL a -> REPL a
    q IO a -> IO a
    u (REPL IORef RW -> IO a
    b) = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\IORef RW
    ref -> IO a -> IO a
    u (IORef RW -> IO a
    b IORef RW
    ref))

      uninterruptibleMask :: forall b. ((forall a. REPL a -> REPL a) -> REPL b) -> REPL b
    uninterruptibleMask (forall a. REPL a -> REPL a) -> REPL b
    op = (IORef RW -> IO b) -> REPL b
    forall a. (IORef RW -> IO a) -> REPL a
    REPL ((IORef RW -> IO b) -> REPL b) -> (IORef RW -> IO b) -> REPL b
    forall a b. (a -> b) -> a -> b
    $ \IORef RW
    ref ->
        ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall (m :: * -> *) b.
    MonadMask m =>
    ((forall a. m a -> m a) -> m b) -> m b
    Ex.uninterruptibleMask (((forall a. IO a -> IO a) -> IO b) -> IO b)
    -> ((forall a. IO a -> IO a) -> IO b) -> IO b
    forall a b. (a -> b) -> a -> b
    $ \forall a. IO a -> IO a
    u -> REPL b -> IORef RW -> IO b
    forall a. REPL a -> IORef RW -> IO a
    unREPL ((forall a. REPL a -> REPL a) -> REPL b
    op ((IO a -> IO a) -> REPL a -> REPL a
    forall {a} {a}. (IO a -> IO a) -> REPL a -> REPL a
    q IO a -> IO a
    forall a. IO a -> IO a
    u)) IORef RW
    ref
        where q :: (IO a -> IO a) -> REPL a -> REPL a
    q IO a -> IO a
    u (REPL IORef RW -> IO a
    b) = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\IORef RW
    ref -> IO a -> IO a
    u (IORef RW -> IO a
    b IORef RW
    ref))

      generalBracket :: forall a b c.
    REPL a
    -> (a -> ExitCase b -> REPL c) -> (a -> REPL b) -> REPL (b, c)
    generalBracket REPL a
    acq a -> ExitCase b -> REPL c
    rls a -> REPL b
    op = (RunInBase REPL IO -> IO (StM REPL (b, c))) -> REPL (b, c)
    forall (b :: * -> *) (m :: * -> *) a.
    MonadBaseControl b m =>
    (RunInBase m b -> b (StM m a)) -> m a
    control ((RunInBase REPL IO -> IO (StM REPL (b, c))) -> REPL (b, c))
    -> (RunInBase REPL IO -> IO (StM REPL (b, c))) -> REPL (b, c)
    forall a b. (a -> b) -> a -> b
    $ \RunInBase REPL IO
    runInBase ->
        IO a -> (a -> ExitCase b -> IO c) -> (a -> IO b) -> IO (b, c)
    forall a b c.
    IO a -> (a -> ExitCase b -> IO c) -> (a -> IO b) -> IO (b, c)
    forall (m :: * -> *) a b c.
    MonadMask m =>
    m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
    Ex.generalBracket (REPL a -> IO (StM REPL a)
    RunInBase REPL IO
    runInBase REPL a
    acq)
        (\a
    saved -> \ExitCase b
    e -> REPL c -> IO (StM REPL c)
    RunInBase REPL IO
    runInBase (StM REPL a -> REPL a
    forall a. StM REPL a -> REPL a
    forall (b :: * -> *) (m :: * -> *) a.
    MonadBaseControl b m =>
    StM m a -> m a
    restoreM a
    StM REPL a
    saved REPL a -> (a -> REPL c) -> REPL c
    forall a b. REPL a -> (a -> REPL b) -> REPL b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    a -> a -> ExitCase b -> REPL c
    rls a
    a ExitCase b
    e))
        (\a
    saved -> REPL b -> IO (StM REPL b)
    RunInBase REPL IO
    runInBase (StM REPL a -> REPL a
    forall a. StM REPL a -> REPL a
    forall (b :: * -> *) (m :: * -> *) a.
    MonadBaseControl b m =>
    StM m a -> m a
    restoreM a
    StM REPL a
    saved REPL a -> (a -> REPL b) -> REPL b
    forall a b. REPL a -> (a -> REPL b) -> REPL b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> REPL b
    op))

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

    -- | REPL exceptions.
    data REPLException
      = ParseError ParseError
      | FileNotFound FilePath
      | DirectoryNotFound FilePath
      | NoPatError [Error]
      | NoIncludeError [IncludeError]
      | EvalError EvalErrorEx
      | TooWide WordTooWide
      | Unsupported Unsupported
      | ModuleSystemError NameDisp M.ModuleError
      | EvalPolyError T.Schema
      | InstantiationsNotFound T.Schema
      | TypeNotTestable T.Type
      | EvalInParamModule [T.TParam] [M.Name]
      | SBVError String
      | SBVException SBVException
      | SBVPortfolioException SBVPortfolioException
      | W4Exception W4Exception
        deriving (Int -> REPLException -> [Char] -> [Char]
    [REPLException] -> [Char] -> [Char]
    REPLException -> [Char]
    (Int -> REPLException -> [Char] -> [Char])
    -> (REPLException -> [Char])
    -> ([REPLException] -> [Char] -> [Char])
    -> Show REPLException
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> REPLException -> [Char] -> [Char]
    showsPrec :: Int -> REPLException -> [Char] -> [Char]
    $cshow :: REPLException -> [Char]
    show :: REPLException -> [Char]
    $cshowList :: [REPLException] -> [Char] -> [Char]
    showList :: [REPLException] -> [Char] -> [Char]
    Show,Typeable)

    instance X.Exception REPLException

    instance PP REPLException where
      ppPrec :: Int -> REPLException -> Doc
    ppPrec Int
    _ REPLException
    re = case REPLException
    re of
        ParseError ParseError
    e         -> ParseError -> Doc
    ppError ParseError
    e
        FileNotFound [Char]
    path    -> [Doc] -> Doc
    sep [ [Char] -> Doc
    text [Char]
    "File"
                                    , [Char] -> Doc
    text ([Char]
    "`" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    path [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "'")
                                    , [Char] -> Doc
    text[Char]
    "not found"
                                    ]
        DirectoryNotFound [Char]
    path -> [Doc] -> Doc
    sep [ [Char] -> Doc
    text [Char]
    "Directory"
                                      , [Char] -> Doc
    text ([Char]
    "`" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    path [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "'")
                                      , [Char] -> Doc
    text[Char]
    "not found or not a directory"
                                      ]
        NoPatError [Error]
    es        -> [Doc] -> Doc
    vcat ((Error -> Doc) -> [Error] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Error -> Doc
    forall a. PP a => a -> Doc
    pp [Error]
    es)
        NoIncludeError [IncludeError]
    es    -> [Doc] -> Doc
    vcat ((IncludeError -> Doc) -> [IncludeError] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map IncludeError -> Doc
    ppIncludeError [IncludeError]
    es)
        ModuleSystemError NameDisp
    ns ModuleError
    me -> NameDisp -> Doc -> Doc
    fixNameDisp NameDisp
    ns (ModuleError -> Doc
    forall a. PP a => a -> Doc
    pp ModuleError
    me)
        EvalError EvalErrorEx
    e          -> EvalErrorEx -> Doc
    forall a. PP a => a -> Doc
    pp EvalErrorEx
    e
        Unsupported Unsupported
    e        -> Unsupported -> Doc
    forall a. PP a => a -> Doc
    pp Unsupported
    e
        TooWide WordTooWide
    e            -> WordTooWide -> Doc
    forall a. PP a => a -> Doc
    pp WordTooWide
    e
        EvalPolyError Schema
    s      -> [Char] -> Doc
    text [Char]
    "Cannot evaluate polymorphic value."
                             Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text [Char]
    "Type:" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    s
        InstantiationsNotFound Schema
    s -> [Char] -> Doc
    text [Char]
    "Cannot find instantiations for some type variables."
                                 Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text [Char]
    "Type:" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    s
        TypeNotTestable Type
    t    -> [Char] -> Doc
    text [Char]
    "The expression is not of a testable type."
                             Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text [Char]
    "Type:" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t
        EvalInParamModule [TParam]
    as [Name]
    xs -> Int -> Doc -> Doc
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    vsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          [ [Char] -> Doc
    text [Char]
    "Expression depends on definitions from a parameterized module:" ]
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (TParam -> Doc) -> [TParam] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map TParam -> Doc
    forall a. PP a => a -> Doc
    pp [TParam]
    as
          [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. PP a => a -> Doc
    pp [Name]
    xs
        SBVError [Char]
    s           -> [Char] -> Doc
    text [Char]
    "SBV error:" Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text [Char]
    s
        SBVException SBVException
    e       -> [Char] -> Doc
    text [Char]
    "SBV exception:" Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text (SBVException -> [Char]
    forall a. Show a => a -> [Char]
    show SBVException
    e)
        SBVPortfolioException SBVPortfolioException
    e -> [Char] -> Doc
    text [Char]
    "SBV exception:" Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text (SBVPortfolioException -> [Char]
    forall a. Show a => a -> [Char]
    show SBVPortfolioException
    e)
        W4Exception W4Exception
    e        -> [Char] -> Doc
    text [Char]
    "What4 exception:" Doc -> Doc -> Doc
    $$ [Char] -> Doc
    text (W4Exception -> [Char]
    forall a. Show a => a -> [Char]
    show W4Exception
    e)

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

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

    finally :: REPL a -> REPL b -> REPL a
    finally :: forall a b. REPL a -> REPL b -> REPL a
    finally REPL a
    m1 REPL b
    m2 = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\IORef RW
    ref -> REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m1 IORef RW
    ref IO a -> IO b -> IO a
    forall a b. IO a -> IO b -> IO a
    `X.finally` REPL b -> IORef RW -> IO b
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL b
    m2 IORef RW
    ref)

    rethrowEvalError :: IO a -> IO a
    rethrowEvalError :: forall a. IO a -> IO a
    rethrowEvalError IO a
    m =
        IO a
    run IO a -> (EvalErrorEx -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` EvalErrorEx -> IO a
    forall a. EvalErrorEx -> IO a
    rethrow
            IO a -> (WordTooWide -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` WordTooWide -> IO a
    forall a. WordTooWide -> IO a
    rethrowTooWide
            IO a -> (Unsupported -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` Unsupported -> IO a
    forall a. Unsupported -> IO a
    rethrowUnsupported
      where
      run :: IO a
    run = do
        a
    a <- IO a
    m
        a -> IO a
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> IO a) -> a -> IO a
    forall a b. (a -> b) -> a -> b
    $! a
    a

      rethrow :: EvalErrorEx -> IO a
      rethrow :: forall a. EvalErrorEx -> IO a
    rethrow EvalErrorEx
    exn = REPLException -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (EvalErrorEx -> REPLException
    EvalError EvalErrorEx
    exn)

      rethrowTooWide :: WordTooWide -> IO a
      rethrowTooWide :: forall a. WordTooWide -> IO a
    rethrowTooWide WordTooWide
    exn = REPLException -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (WordTooWide -> REPLException
    TooWide WordTooWide
    exn)

      rethrowUnsupported :: Unsupported -> IO a
      rethrowUnsupported :: forall a. Unsupported -> IO a
    rethrowUnsupported Unsupported
    exn = REPLException -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (Unsupported -> REPLException
    Unsupported Unsupported
    exn)

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

    io :: IO a -> REPL a
    io :: forall a. IO a -> REPL a
    io IO a
    m = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ IORef RW
    _ -> IO a
    m)

    getRW :: REPL RW
    getRW :: REPL RW
    getRW  = (IORef RW -> IO RW) -> REPL RW
    forall a. (IORef RW -> IO a) -> REPL a
    REPL IORef RW -> IO RW
    forall a. IORef a -> IO a
    readIORef

    modifyRW :: (RW -> (RW,a)) -> REPL a
    modifyRW :: forall a. (RW -> (RW, a)) -> REPL a
    modifyRW RW -> (RW, a)
    f = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ IORef RW
    ref -> IORef RW -> (RW -> (RW, a)) -> IO a
    forall a b. IORef a -> (a -> (a, b)) -> IO b
    atomicModifyIORef IORef RW
    ref RW -> (RW, a)
    f)

    modifyRW_ :: (RW -> RW) -> REPL ()
    modifyRW_ :: (RW -> RW) -> REPL ()
    modifyRW_ RW -> RW
    f = (IORef RW -> IO ()) -> REPL ()
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ IORef RW
    ref -> IORef RW -> (RW -> (RW, ())) -> IO ()
    forall a b. IORef a -> (a -> (a, b)) -> IO b
    atomicModifyIORef IORef RW
    ref (\RW
    x -> (RW -> RW
    f RW
    x, ())))

    -- | Construct the prompt for the current environment.
    getPrompt :: REPL String
    getPrompt :: REPL [Char]
    getPrompt  = RW -> [Char]
    mkPrompt (RW -> [Char]) -> REPL RW -> REPL [Char]
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

    getCallStacks :: REPL Bool
    getCallStacks :: REPL Bool
    getCallStacks = RW -> Bool
    eCallStacks (RW -> Bool) -> REPL RW -> REPL Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW

    -- This assumes that we are not starting solvers in parallel, otherwise
    -- there are a bunch of race conditions here.
    getTCSolver :: REPL SMT.Solver
    getTCSolver :: REPL Solver
    getTCSolver =
      do RW
    rw <- REPL RW
    getRW
         case RW -> Maybe Solver
    eTCSolver RW
    rw of
           Just Solver
    s -> Solver -> REPL Solver
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver
    s
           Maybe Solver
    Nothing ->
             do IORef RW
    ref <- (IORef RW -> IO (IORef RW)) -> REPL (IORef RW)
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\IORef RW
    ref -> IORef RW -> IO (IORef RW)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure IORef RW
    ref)
                let now :: Int
    now = RW -> Int
    eTCSolverRestarts RW
    rw Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1
                    upd :: RW -> RW
    upd RW
    new = if RW -> Int
    eTCSolverRestarts RW
    new Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    now
                                 then RW
    new { eTCSolver :: Maybe Solver
    eTCSolver = Maybe Solver
    forall a. Maybe a
    Nothing }
                                 else RW
    new
                    onExit :: IO ()
    onExit = IORef RW -> (RW -> (RW, ())) -> IO ()
    forall a b. IORef a -> (a -> (a, b)) -> IO b
    atomicModifyIORef IORef RW
    ref (\RW
    s -> (RW -> RW
    upd RW
    s, ()))
                Solver
    s <- IO Solver -> REPL Solver
    forall a. IO a -> REPL a
    io (IO () -> SolverConfig -> IO Solver
    SMT.startSolver IO ()
    onExit (RW -> SolverConfig
    eTCConfig RW
    rw))
                (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw' -> RW
    rw'{ eTCSolver :: Maybe Solver
    eTCSolver = Solver -> Maybe Solver
    forall a. a -> Maybe a
    Just Solver
    s
                                      , eTCSolverRestarts :: Int
    eTCSolverRestarts = Int
    now })
                Solver -> REPL Solver
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Solver
    s

    resetTCSolver :: REPL ()
    resetTCSolver :: REPL ()
    resetTCSolver =
      do Maybe Solver
    mtc <- RW -> Maybe Solver
    eTCSolver (RW -> Maybe Solver) -> REPL RW -> REPL (Maybe Solver)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW
         case Maybe Solver
    mtc of
           Maybe Solver
    Nothing -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
           Just Solver
    s  ->
             do IO () -> REPL ()
    forall a. IO a -> REPL a
    io (Solver -> IO ()
    SMT.stopSolver Solver
    s)
                (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw{ eTCSolver :: Maybe Solver
    eTCSolver = Maybe Solver
    forall a. Maybe a
    Nothing })

    -- Get the setting we should use for displaying values.
    getPPValOpts :: REPL PPOpts
    getPPValOpts :: REPL PPOpts
    getPPValOpts =
      do Int
    base       <- [Char] -> REPL Int
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "base"
         Bool
    ascii      <- [Char] -> REPL Bool
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "ascii"
         Int
    infLength  <- [Char] -> REPL Int
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "infLength"

         Int
    fpBase     <- [Char] -> REPL Int
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "fpBase"
         [Char]
    fpFmtTxt   <- [Char] -> REPL [Char]
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "fpFormat"
         FieldOrder
    fieldOrder <- [Char] -> REPL FieldOrder
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "fieldOrder"
         let fpFmt :: PPFloatFormat
    fpFmt = case [Char] -> Maybe PPFloatFormat
    parsePPFloatFormat [Char]
    fpFmtTxt of
                       Just PPFloatFormat
    f  -> PPFloatFormat
    f
                       Maybe PPFloatFormat
    Nothing -> [Char] -> [[Char]] -> PPFloatFormat
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "getPPOpts"
                                          [ [Char]
    "Failed to parse fp-format" ]

         PPOpts -> REPL PPOpts
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PPOpts { useBase :: Int
    useBase       = Int
    base
                       , useAscii :: Bool
    useAscii      = Bool
    ascii
                       , useInfLength :: Int
    useInfLength  = Int
    infLength
                       , useFPBase :: Int
    useFPBase     = Int
    fpBase
                       , useFPFormat :: PPFloatFormat
    useFPFormat   = PPFloatFormat
    fpFmt
                       , useFieldOrder :: FieldOrder
    useFieldOrder = FieldOrder
    fieldOrder
                       }

    getEvalOptsAction :: REPL (IO EvalOpts)
    getEvalOptsAction :: REPL (IO EvalOpts)
    getEvalOptsAction = (IORef RW -> IO (IO EvalOpts)) -> REPL (IO EvalOpts)
    forall a. (IORef RW -> IO a) -> REPL a
    REPL ((IORef RW -> IO (IO EvalOpts)) -> REPL (IO EvalOpts))
    -> (IORef RW -> IO (IO EvalOpts)) -> REPL (IO EvalOpts)
    forall a b. (a -> b) -> a -> b
    $ \IORef RW
    rwRef -> IO EvalOpts -> IO (IO EvalOpts)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (IO EvalOpts -> IO (IO EvalOpts))
    -> IO EvalOpts -> IO (IO EvalOpts)
    forall a b. (a -> b) -> a -> b
    $
      do PPOpts
    ppOpts <- REPL PPOpts -> IORef RW -> IO PPOpts
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL PPOpts
    getPPValOpts IORef RW
    rwRef
         Logger
    l      <- REPL Logger -> IORef RW -> IO Logger
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL Logger
    getLogger IORef RW
    rwRef
         EvalOpts -> IO EvalOpts
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return EvalOpts { evalPPOpts :: PPOpts
    evalPPOpts = PPOpts
    ppOpts, evalLogger :: Logger
    evalLogger = Logger
    l }

    clearLoadedMod :: REPL ()
    clearLoadedMod :: REPL ()
    clearLoadedMod = do (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw { eLoadedMod :: Maybe LoadedModule
    eLoadedMod = LoadedModule -> LoadedModule
    upd (LoadedModule -> LoadedModule)
    -> Maybe LoadedModule -> Maybe LoadedModule
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RW -> Maybe LoadedModule
    eLoadedMod RW
    rw })
                        REPL ()
    updateREPLTitle
      where upd :: LoadedModule -> LoadedModule
    upd LoadedModule
    x = LoadedModule
    x { lName :: Maybe ModName
    lName = Maybe ModName
    forall a. Maybe a
    Nothing }

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

    getLoadedMod :: REPL (Maybe LoadedModule)
    getLoadedMod :: REPL (Maybe LoadedModule)
    getLoadedMod  = RW -> Maybe LoadedModule
    eLoadedMod (RW -> Maybe LoadedModule) -> REPL RW -> REPL (Maybe LoadedModule)
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

    -- | Set the path for the ':e' command.
    -- Note that this does not change the focused module (i.e., what ":r" reloads)
    setEditPath :: FilePath -> REPL ()
    setEditPath :: [Char] -> REPL ()
    setEditPath [Char]
    p = (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    rw -> RW
    rw { eEditFile :: Maybe [Char]
    eEditFile = [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    p }

    getEditPath :: REPL (Maybe FilePath)
    getEditPath :: REPL (Maybe [Char])
    getEditPath = RW -> Maybe [Char]
    eEditFile (RW -> Maybe [Char]) -> REPL RW -> REPL (Maybe [Char])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW

    clearEditPath :: REPL ()
    clearEditPath :: REPL ()
    clearEditPath = (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    rw -> RW
    rw { eEditFile :: Maybe [Char]
    eEditFile = Maybe [Char]
    forall a. Maybe a
    Nothing }

    setSearchPath :: [FilePath] -> REPL ()
    setSearchPath :: [[Char]] -> REPL ()
    setSearchPath [[Char]]
    path = do
      ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
      ModuleEnv -> REPL ()
    setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ ModuleEnv
    me { meSearchPath :: [[Char]]
    M.meSearchPath = [[Char]]
    path }
      [Char] -> EnvVal -> REPL ()
    setUserDirect [Char]
    "path" ([Char] -> EnvVal
    EnvString ([[Char]] -> [Char]
    renderSearchPath [[Char]]
    path))

    prependSearchPath :: [FilePath] -> REPL ()
    prependSearchPath :: [[Char]] -> REPL ()
    prependSearchPath [[Char]]
    path = do
      ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
      let path' :: [[Char]]
    path' = [[Char]]
    path [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ ModuleEnv -> [[Char]]
    M.meSearchPath ModuleEnv
    me
      ModuleEnv -> REPL ()
    setModuleEnv (ModuleEnv -> REPL ()) -> ModuleEnv -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ ModuleEnv
    me { meSearchPath :: [[Char]]
    M.meSearchPath = [[Char]]
    path' }
      [Char] -> EnvVal -> REPL ()
    setUserDirect [Char]
    "path" ([Char] -> EnvVal
    EnvString ([[Char]] -> [Char]
    renderSearchPath [[Char]]
    path'))

    getProverConfig :: REPL (Either SBV.SBVProverConfig W4.W4ProverConfig)
    getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)
    getProverConfig = RW -> Either SBVProverConfig W4ProverConfig
    eProverConfig (RW -> Either SBVProverConfig W4ProverConfig)
    -> REPL RW -> REPL (Either SBVProverConfig W4ProverConfig)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW

    shouldContinue :: REPL Bool
    shouldContinue :: REPL Bool
    shouldContinue  = RW -> Bool
    eContinue (RW -> Bool) -> REPL RW -> REPL Bool
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

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

    unlessBatch :: REPL () -> REPL ()
    unlessBatch :: REPL () -> REPL ()
    unlessBatch REPL ()
    body = do
      RW
    rw <- REPL RW
    getRW
      Bool -> REPL () -> REPL ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (RW -> Bool
    eIsBatch RW
    rw) REPL ()
    body

    -- | Run a computation in batch mode, restoring the previous isBatch
    -- flag afterwards
    asBatch :: REPL a -> REPL a
    asBatch :: forall a. REPL a -> REPL a
    asBatch REPL a
    body = do
      Bool
    wasBatch <- RW -> Bool
    eIsBatch (RW -> Bool) -> REPL RW -> REPL Bool
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW
      (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ (\ RW
    rw -> RW
    rw { eIsBatch :: Bool
    eIsBatch = Bool
    True })
      a
    a <- REPL a
    body
      (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ (\ RW
    rw -> RW
    rw { eIsBatch :: Bool
    eIsBatch = Bool
    wasBatch })
      a -> REPL a
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | Is evaluation enabled.  If the currently focused module is
    -- parameterized, then we cannot evalute.
    validEvalContext :: T.FreeVars a => a -> REPL ()
    validEvalContext :: forall a. FreeVars a => a -> REPL ()
    validEvalContext a
    a =
      do ModuleEnv
    me <- RW -> ModuleEnv
    eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW
         let ds :: Deps
    ds      = a -> Deps
    forall e. FreeVars e => e -> Deps
    T.freeVars a
    a
             badVals :: Set Name
    badVals = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
    forall a b. (a -> b -> b) -> b -> Set a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Name -> Set Name -> Set Name
    badName Set Name
    forall a. Set a
    Set.empty (Deps -> Set Name
    T.valDeps Deps
    ds)
             bad :: Set Name
    bad     = (Name -> Set Name -> Set Name) -> Set Name -> Set Name -> Set Name
    forall a b. (a -> b -> b) -> b -> Set a -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Name -> Set Name -> Set Name
    badName Set Name
    badVals (Deps -> Set Name
    T.tyDeps Deps
    ds)
             badTs :: Set TParam
    badTs   = Deps -> Set TParam
    T.tyParams Deps
    ds

             badName :: Name -> Set Name -> Set Name
    badName Name
    nm Set Name
    bs =
               case Name -> NameInfo
    M.nameInfo Name
    nm of

                 -- XXX: Changes if focusing on nested modules
                 M.GlobalName NameSource
    _ I.OrigName { ogModule :: OrigName -> ModPath
    ogModule = I.TopModule ModName
    m }
                   | ModName -> LoadedModules -> Bool
    M.isLoadedParamMod ModName
    m (ModuleEnv -> LoadedModules
    M.meLoadedModules ModuleEnv
    me) -> Name -> Set Name -> Set Name
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Name
    nm Set Name
    bs
                   | ModName -> LoadedModules -> Bool
    M.isLoadedInterface ModName
    m (ModuleEnv -> LoadedModules
    M.meLoadedModules ModuleEnv
    me) -> Name -> Set Name -> Set Name
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Name
    nm Set Name
    bs

                 NameInfo
    _ -> Set Name
    bs

         Bool -> REPL () -> REPL ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    bad Bool -> Bool -> Bool
    && Set TParam -> Bool
    forall a. Set a -> Bool
    Set.null Set TParam
    badTs) (REPL () -> REPL ()) -> REPL () -> REPL ()
    forall a b. (a -> b) -> a -> b
    $
           REPLException -> REPL ()
    forall a. REPLException -> REPL a
    raise ([TParam] -> [Name] -> REPLException
    EvalInParamModule (Set TParam -> [TParam]
    forall a. Set a -> [a]
    Set.toList Set TParam
    badTs) (Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList Set Name
    bad))

    -- | Update the title
    updateREPLTitle :: REPL ()
    updateREPLTitle :: REPL ()
    updateREPLTitle  = REPL () -> REPL ()
    unlessBatch (REPL () -> REPL ()) -> REPL () -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ do
      RW
    rw <- REPL RW
    getRW
      RW -> REPL ()
    eUpdateTitle RW
    rw

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

    -- | Set the REPL's string-printer
    setPutStr :: (String -> IO ()) -> REPL ()
    setPutStr :: ([Char] -> IO ()) -> REPL ()
    setPutStr [Char] -> IO ()
    fn = (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ \RW
    rw -> RW
    rw { eLogger :: Logger
    eLogger = ([Char] -> IO ()) -> Logger
    funLogger [Char] -> IO ()
    fn }

    -- | Get the REPL's string-printer
    getPutStr :: REPL (String -> IO ())
    getPutStr :: REPL ([Char] -> IO ())
    getPutStr =
      do RW
    rw <- REPL RW
    getRW
         ([Char] -> IO ()) -> REPL ([Char] -> IO ())
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Logger -> [Char] -> IO ()
    logPutStr (RW -> Logger
    eLogger RW
    rw))

    getLogger :: REPL Logger
    getLogger :: REPL Logger
    getLogger = RW -> Logger
    eLogger (RW -> Logger) -> REPL RW -> REPL Logger
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW

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

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

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

    getFocusedEnv :: REPL M.ModContext
    getFocusedEnv :: REPL ModContext
    getFocusedEnv  = ModuleEnv -> ModContext
    M.focusedEnv (ModuleEnv -> ModContext) -> REPL ModuleEnv -> REPL ModContext
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL ModuleEnv
    getModuleEnv

    -- | Get visible variable names.
    -- This is used for command line completition.
    getExprNames :: REPL [String]
    getExprNames :: REPL [[Char]]
    getExprNames =
      do NamingEnv
    fNames <- ModContext -> NamingEnv
    M.mctxNames (ModContext -> NamingEnv) -> REPL ModContext -> REPL NamingEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL ModContext
    getFocusedEnv
         [[Char]] -> REPL [[Char]]
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((PName -> [Char]) -> [PName] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Doc -> [Char]) -> (PName -> Doc) -> PName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PName -> Doc
    forall a. PP a => a -> Doc
    pp) (Map PName Names -> [PName]
    forall k a. Map k a -> [k]
    Map.keys (Namespace -> NamingEnv -> Map PName Names
    M.namespaceMap Namespace
    M.NSValue NamingEnv
    fNames)))

    -- | Get visible type signature names.
    -- This is used for command line completition.
    getTypeNames :: REPL [String]
    getTypeNames :: REPL [[Char]]
    getTypeNames  =
      do NamingEnv
    fNames <- ModContext -> NamingEnv
    M.mctxNames (ModContext -> NamingEnv) -> REPL ModContext -> REPL NamingEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL ModContext
    getFocusedEnv
         [[Char]] -> REPL [[Char]]
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((PName -> [Char]) -> [PName] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> [Char]
    forall a. Show a => a -> [Char]
    show (Doc -> [Char]) -> (PName -> Doc) -> PName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PName -> Doc
    forall a. PP a => a -> Doc
    pp) (Map PName Names -> [PName]
    forall k a. Map k a -> [k]
    Map.keys (Namespace -> NamingEnv -> Map PName Names
    M.namespaceMap Namespace
    M.NSType NamingEnv
    fNames)))

    -- | Return a list of property names, sorted by position in the file.
    getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp)
    getPropertyNames :: REPL ([(Name, IfaceDecl)], NameDisp)
    getPropertyNames =
      do ModContext
    fe <- REPL ModContext
    getFocusedEnv
         let xs :: Map Name IfaceDecl
    xs = IfaceDecls -> Map Name IfaceDecl
    M.ifDecls (ModContext -> IfaceDecls
    M.mctxDecls ModContext
    fe)
             ps :: [(Name, IfaceDecl)]
    ps = ((Name, IfaceDecl) -> (Name, IfaceDecl) -> Ordering)
    -> [(Name, IfaceDecl)] -> [(Name, IfaceDecl)]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy (((Name, IfaceDecl) -> Position)
    -> (Name, IfaceDecl) -> (Name, IfaceDecl) -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Range -> Position
    from (Range -> Position)
    -> ((Name, IfaceDecl) -> Range) -> (Name, IfaceDecl) -> Position
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Range
    M.nameLoc (Name -> Range)
    -> ((Name, IfaceDecl) -> Name) -> (Name, IfaceDecl) -> Range
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, IfaceDecl) -> Name
    forall a b. (a, b) -> a
    fst))
                  [ (Name
    x,IfaceDecl
    d) | (Name
    x,IfaceDecl
    d) <- Map Name IfaceDecl -> [(Name, IfaceDecl)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name IfaceDecl
    xs,
                        Pragma
    T.PragmaProperty Pragma -> [Pragma] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` IfaceDecl -> [Pragma]
    M.ifDeclPragmas IfaceDecl
    d ]

         ([(Name, IfaceDecl)], NameDisp)
    -> REPL ([(Name, IfaceDecl)], NameDisp)
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Name, IfaceDecl)]
    ps, ModContext -> NameDisp
    M.mctxNameDisp ModContext
    fe)

    getModNames :: REPL [I.ModName]
    getModNames :: REPL [ModName]
    getModNames =
      do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
         [ModName] -> REPL [ModName]
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((ModuleG ModName -> ModName) -> [ModuleG ModName] -> [ModName]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleG ModName -> ModName
    forall mname. ModuleG mname -> mname
    T.mName (ModuleEnv -> [ModuleG ModName]
    M.loadedModules ModuleEnv
    me))

    getModuleEnv :: REPL M.ModuleEnv
    getModuleEnv :: REPL ModuleEnv
    getModuleEnv  = RW -> ModuleEnv
    eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

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

    getDynEnv :: REPL M.DynamicEnv
    getDynEnv :: REPL DynamicEnv
    getDynEnv  = (ModuleEnv -> DynamicEnv
    M.meDynEnv (ModuleEnv -> DynamicEnv) -> (RW -> ModuleEnv) -> RW -> DynamicEnv
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RW -> ModuleEnv
    eModuleEnv) (RW -> DynamicEnv) -> REPL RW -> REPL DynamicEnv
    forall a b. (a -> b) -> REPL a -> REPL b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

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

    getRandomGen :: REPL TF.TFGen
    getRandomGen :: REPL TFGen
    getRandomGen = RW -> TFGen
    eRandomGen (RW -> TFGen) -> REPL RW -> REPL TFGen
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> REPL RW
    getRW

    setRandomGen :: TF.TFGen -> REPL ()
    setRandomGen :: TFGen -> REPL ()
    setRandomGen TFGen
    rng = (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    s -> RW
    s { eRandomGen :: TFGen
    eRandomGen = TFGen
    rng })

    withRandomGen :: (TF.TFGen -> REPL (a, TF.TFGen)) -> REPL a
    withRandomGen :: forall a. (TFGen -> REPL (a, TFGen)) -> REPL a
    withRandomGen TFGen -> REPL (a, TFGen)
    repl =
      do  TFGen
    g <- REPL TFGen
    getRandomGen
          (a
    result, TFGen
    g') <- TFGen -> REPL (a, TFGen)
    repl TFGen
    g
          TFGen -> REPL ()
    setRandomGen TFGen
    g'
          a -> REPL a
    forall a. a -> REPL a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    result

    -- | 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 -> REPL Name
    uniqify Name
    name =
      case Name -> NameInfo
    M.nameInfo Name
    name of
        M.GlobalName NameSource
    s OrigName
    og ->
          (Supply -> (Name, Supply)) -> REPL Name
    forall a. (Supply -> (a, Supply)) -> REPL a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    M.liftSupply (Namespace
    -> ModPath
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    M.mkDeclared (Name -> Namespace
    M.nameNamespace Name
    name)
                      (OrigName -> ModPath
    I.ogModule OrigName
    og) NameSource
    s
                      (Name -> Ident
    M.nameIdent Name
    name) (Name -> Maybe Fixity
    M.nameFixity Name
    name) (Name -> Range
    M.nameLoc Name
    name))

        M.LocalName {} ->
          [Char] -> [[Char]] -> REPL Name
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "[REPL] uniqify" [[Char]
    "tried to uniqify a parameter: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Name -> [Char]
    forall a. PP a => a -> [Char]
    pretty Name
    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 :: Ident -> NameSource -> REPL Name
    freshName Ident
    i NameSource
    sys =
      (Supply -> (Name, Supply)) -> REPL Name
    forall a. (Supply -> (a, Supply)) -> REPL a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    M.liftSupply (Namespace
    -> ModPath
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    M.mkDeclared Namespace
    I.NSValue ModPath
    mpath NameSource
    sys Ident
    i Maybe Fixity
    forall a. Maybe a
    Nothing Range
    emptyRange)
      where mpath :: ModPath
    mpath = ModName -> ModPath
    M.TopModule ModName
    I.interactiveName

    parseSearchPath :: String -> [String]
    parseSearchPath :: [Char] -> [[Char]]
    parseSearchPath [Char]
    path = [[Char]]
    path'
    #if defined(mingw32_HOST_OS) || defined(__MINGW32__)
          -- Windows paths search from end to beginning
          where path' = reverse (splitSearchPath path)
    #else
          where path' :: [[Char]]
    path' = [Char] -> [[Char]]
    splitSearchPath [Char]
    path
    #endif

    renderSearchPath :: [String] -> String
    renderSearchPath :: [[Char]] -> [Char]
    renderSearchPath [[Char]]
    pathSegs = [Char]
    path
    #if defined(mingw32_HOST_OS) || defined(__MINGW32__)
          -- Windows paths search from end to beginning
          where path = intercalate [searchPathSeparator] (reverse pathSegs)
    #else
          where path :: [Char]
    path = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char
    searchPathSeparator] [[Char]]
    pathSegs
    #endif

    -- 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 (Int -> EnvVal -> [Char] -> [Char]
    [EnvVal] -> [Char] -> [Char]
    EnvVal -> [Char]
    (Int -> EnvVal -> [Char] -> [Char])
    -> (EnvVal -> [Char])
    -> ([EnvVal] -> [Char] -> [Char])
    -> Show EnvVal
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> EnvVal -> [Char] -> [Char]
    showsPrec :: Int -> EnvVal -> [Char] -> [Char]
    $cshow :: EnvVal -> [Char]
    show :: EnvVal -> [Char]
    $cshowList :: [EnvVal] -> [Char] -> [Char]
    showList :: [EnvVal] -> [Char] -> [Char]
    Show)

    -- | Generate a UserEnv from a description of the options map.
    mkUserEnv :: OptionMap -> UserEnv
    mkUserEnv :: OptionMap -> UserEnv
    mkUserEnv OptionMap
    opts = [([Char], EnvVal)] -> UserEnv
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([([Char], EnvVal)] -> UserEnv) -> [([Char], EnvVal)] -> UserEnv
    forall a b. (a -> b) -> a -> b
    $ do
      OptionDescr
    opt <- OptionMap -> [OptionDescr]
    forall a. Trie a -> [a]
    leaves OptionMap
    opts
      ([Char], EnvVal) -> [([Char], EnvVal)]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (OptionDescr -> [Char]
    optName OptionDescr
    opt, OptionDescr -> EnvVal
    optDefault OptionDescr
    opt)

    -- | Set a user option.
    setUser :: String -> String -> REPL ()
    setUser :: [Char] -> [Char] -> REPL ()
    setUser [Char]
    name [Char]
    val = case [Char] -> OptionMap -> [OptionDescr]
    forall a. [Char] -> Trie a -> [a]
    lookupTrieExact [Char]
    name OptionMap
    userOptionsWithAliases of

      [OptionDescr
    opt] -> OptionDescr -> REPL ()
    setUserOpt OptionDescr
    opt
      []    -> [Char] -> REPL ()
    rPutStrLn ([Char]
    "Unknown env value `" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "`")
      [OptionDescr]
    _     -> [Char] -> REPL ()
    rPutStrLn ([Char]
    "Ambiguous env value `" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "`")

      where
      setUserOpt :: OptionDescr -> REPL ()
    setUserOpt OptionDescr
    opt = case OptionDescr -> EnvVal
    optDefault OptionDescr
    opt of
        EnvString [Char]
    _ -> EnvVal -> REPL ()
    doCheck ([Char] -> EnvVal
    EnvString [Char]
    val)

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

        EnvNum Int
    _ -> case ReadS Int
    forall a. Read a => ReadS a
    reads [Char]
    val of
          [(Int
    x,[Char]
    _)] -> EnvVal -> REPL ()
    doCheck (Int -> EnvVal
    EnvNum Int
    x)
          [(Int, [Char])]
    _ -> [Char] -> REPL ()
    rPutStrLn ([Char]
    "Failed to parse number for field, `" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "`")

        EnvBool Bool
    _
          | ([Char] -> Bool) -> [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ([Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` [Char]
    val) [[Char]
    "enable", [Char]
    "on", [Char]
    "yes", [Char]
    "true"] ->
            EnvVal -> REPL ()
    writeEnv (Bool -> EnvVal
    EnvBool Bool
    True)
          | ([Char] -> Bool) -> [[Char]] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ([Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` [Char]
    val) [[Char]
    "disable", [Char]
    "off", [Char]
    "no", [Char]
    "false"] ->
            EnvVal -> REPL ()
    writeEnv (Bool -> EnvVal
    EnvBool Bool
    False)
          | Bool
    otherwise ->
            [Char] -> REPL ()
    rPutStrLn ([Char]
    "Failed to parse boolean for field, `" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    name [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "`")
        where
        doCheck :: EnvVal -> REPL ()
    doCheck EnvVal
    v = do (Maybe [Char]
    r,[[Char]]
    ws) <- OptionDescr -> Checker
    optCheck OptionDescr
    opt EnvVal
    v
                       case Maybe [Char]
    r of
                         Just [Char]
    err -> [Char] -> REPL ()
    rPutStrLn [Char]
    err
                         Maybe [Char]
    Nothing  -> do ([Char] -> REPL ()) -> [[Char]] -> REPL ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ [Char] -> REPL ()
    rPutStrLn [[Char]]
    ws
                                        EnvVal -> REPL ()
    writeEnv EnvVal
    v
        writeEnv :: EnvVal -> REPL ()
    writeEnv EnvVal
    ev =
          do OptionDescr -> EnvVal -> REPL ()
    optEff OptionDescr
    opt EnvVal
    ev
             (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw { eUserEnv :: UserEnv
    eUserEnv = [Char] -> EnvVal -> UserEnv -> UserEnv
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert (OptionDescr -> [Char]
    optName OptionDescr
    opt) EnvVal
    ev (RW -> UserEnv
    eUserEnv RW
    rw) })

    splitOptArgs :: String -> [String]
    splitOptArgs :: [Char] -> [[Char]]
    splitOptArgs  = ([Char] -> Maybe ([Char], [Char])) -> [Char] -> [[Char]]
    forall b a. (b -> Maybe (a, b)) -> b -> [a]
    unfoldr ([Char] -> [Char] -> Maybe ([Char], [Char])
    parse [Char]
    "")
      where

      parse :: [Char] -> [Char] -> Maybe ([Char], [Char])
    parse [Char]
    acc (Char
    c:[Char]
    cs) | Char -> Bool
    isQuote Char
    c       = [Char] -> [Char] -> Maybe ([Char], [Char])
    quoted (Char
    cChar -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[Char]
    acc) [Char]
    cs
                       | Bool -> Bool
    not (Char -> Bool
    isSpace Char
    c) = [Char] -> [Char] -> Maybe ([Char], [Char])
    parse (Char
    cChar -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[Char]
    acc) [Char]
    cs
                       | Bool
    otherwise       = [Char] -> [Char] -> Maybe ([Char], [Char])
    result [Char]
    acc [Char]
    cs
      parse [Char]
    acc []                       = [Char] -> [Char] -> Maybe ([Char], [Char])
    result [Char]
    acc []

      quoted :: [Char] -> [Char] -> Maybe ([Char], [Char])
    quoted [Char]
    acc (Char
    c:[Char]
    cs) | Char -> Bool
    isQuote Char
    c      = [Char] -> [Char] -> Maybe ([Char], [Char])
    parse  (Char
    cChar -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[Char]
    acc) [Char]
    cs
                        | Bool
    otherwise      = [Char] -> [Char] -> Maybe ([Char], [Char])
    quoted (Char
    cChar -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[Char]
    acc) [Char]
    cs
      quoted [Char]
    acc []                      = [Char] -> [Char] -> Maybe ([Char], [Char])
    result [Char]
    acc []

      result :: [Char] -> [Char] -> Maybe ([Char], [Char])
    result []  [] = Maybe ([Char], [Char])
    forall a. Maybe a
    Nothing
      result []  [Char]
    cs = [Char] -> [Char] -> Maybe ([Char], [Char])
    parse [] ((Char -> Bool) -> [Char] -> [Char]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    cs)
      result [Char]
    acc [Char]
    cs = ([Char], [Char]) -> Maybe ([Char], [Char])
    forall a. a -> Maybe a
    Just ([Char] -> [Char]
    forall a. [a] -> [a]
    reverse [Char]
    acc, (Char -> Bool) -> [Char] -> [Char]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace [Char]
    cs)

      isQuote :: Char -> Bool
      isQuote :: Char -> Bool
    isQuote Char
    c = Char
    c Char -> [Char] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ([Char]
    "'\"" :: String)

    -- | Get a user option, using Maybe for failure.
    tryGetUser :: String -> REPL (Maybe EnvVal)
    tryGetUser :: [Char] -> REPL (Maybe EnvVal)
    tryGetUser [Char]
    name = do
      RW
    rw <- REPL RW
    getRW
      Maybe EnvVal -> REPL (Maybe EnvVal)
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> UserEnv -> Maybe EnvVal
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup [Char]
    name (RW -> UserEnv
    eUserEnv RW
    rw))

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

    setUserDirect :: String -> EnvVal -> REPL ()
    setUserDirect :: [Char] -> EnvVal -> REPL ()
    setUserDirect [Char]
    optName EnvVal
    val = do
      (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw { eUserEnv :: UserEnv
    eUserEnv = [Char] -> EnvVal -> UserEnv -> UserEnv
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert [Char]
    optName EnvVal
    val (RW -> UserEnv
    eUserEnv RW
    rw) })

    getKnownUser :: IsEnvVal a => String -> REPL a
    getKnownUser :: forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    x = EnvVal -> a
    forall a. IsEnvVal a => EnvVal -> a
    fromEnvVal (EnvVal -> a) -> REPL EnvVal -> REPL a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> REPL EnvVal
    getUser [Char]
    x

    class IsEnvVal a where
      fromEnvVal :: EnvVal -> a

    instance IsEnvVal Bool where
      fromEnvVal :: EnvVal -> Bool
    fromEnvVal EnvVal
    x = case EnvVal
    x of
                       EnvBool Bool
    b -> Bool
    b
                       EnvVal
    _         -> [Char] -> Bool
    forall a. [Char] -> a
    badIsEnv [Char]
    "Bool"

    instance IsEnvVal Int where
      fromEnvVal :: EnvVal -> Int
    fromEnvVal EnvVal
    x = case EnvVal
    x of
                       EnvNum Int
    b -> Int
    b
                       EnvVal
    _         -> [Char] -> Int
    forall a. [Char] -> a
    badIsEnv [Char]
    "Num"

    instance IsEnvVal (String,[String]) where
      fromEnvVal :: EnvVal -> ([Char], [[Char]])
    fromEnvVal EnvVal
    x = case EnvVal
    x of
                       EnvProg [Char]
    b [[Char]]
    bs -> ([Char]
    b,[[Char]]
    bs)
                       EnvVal
    _            -> [Char] -> ([Char], [[Char]])
    forall a. [Char] -> a
    badIsEnv [Char]
    "Prog"

    instance IsEnvVal String where
      fromEnvVal :: EnvVal -> [Char]
    fromEnvVal EnvVal
    x = case EnvVal
    x of
                       EnvString [Char]
    b -> [Char]
    b
                       EnvVal
    _           -> [Char] -> [Char]
    forall a. [Char] -> a
    badIsEnv [Char]
    "String"

    instance IsEnvVal FieldOrder where
      fromEnvVal :: EnvVal -> FieldOrder
    fromEnvVal EnvVal
    x = case EnvVal
    x of
                       EnvString [Char]
    s | Just FieldOrder
    o <- [Char] -> Maybe FieldOrder
    parseFieldOrder [Char]
    s
                         -> FieldOrder
    o
                       EnvVal
    _ -> [Char] -> FieldOrder
    forall a. [Char] -> a
    badIsEnv [Char]
    "display` or `canonical"

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

    getUserShowProverStats :: REPL Bool
    getUserShowProverStats :: REPL Bool
    getUserShowProverStats = [Char] -> REPL Bool
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "proverStats"

    getUserProverValidate :: REPL Bool
    getUserProverValidate :: REPL Bool
    getUserProverValidate = [Char] -> REPL Bool
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "proverValidate"

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

    type OptionMap = Trie OptionDescr

    mkOptionMap :: [OptionDescr] -> OptionMap
    mkOptionMap :: [OptionDescr] -> OptionMap
    mkOptionMap  = (OptionMap -> OptionDescr -> OptionMap)
    -> OptionMap -> [OptionDescr] -> OptionMap
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl OptionMap -> OptionDescr -> OptionMap
    insert OptionMap
    forall a. Trie a
    emptyTrie
      where
      insert :: OptionMap -> OptionDescr -> OptionMap
    insert OptionMap
    m OptionDescr
    d = [Char] -> OptionDescr -> OptionMap -> OptionMap
    forall a. [Char] -> a -> Trie a -> Trie a
    insertTrie (OptionDescr -> [Char]
    optName OptionDescr
    d) OptionDescr
    d OptionMap
    m

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

    noCheck :: Checker
    noCheck :: Checker
    noCheck EnvVal
    _ = (Maybe [Char], [[Char]]) -> REPL (Maybe [Char], [[Char]])
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Char]
    forall a. Maybe a
    Nothing, [])

    noWarns :: Maybe String -> REPL (Maybe String, [String])
    noWarns :: Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    mb = (Maybe [Char], [[Char]]) -> REPL (Maybe [Char], [[Char]])
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Char]
    mb, [])

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

    simpleOpt :: String -> [String] -> EnvVal -> Checker -> String -> OptionDescr
    simpleOpt :: [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    optName [[Char]]
    optAliases EnvVal
    optDefault Checker
    optCheck [Char]
    optHelp =
      OptionDescr { optEff :: EnvVal -> REPL ()
    optEff = \ EnvVal
    _ -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (), [Char]
    [[Char]]
    EnvVal
    Checker
    optName :: [Char]
    optDefault :: EnvVal
    optCheck :: Checker
    optAliases :: [[Char]]
    optHelp :: [Char]
    optName :: [Char]
    optAliases :: [[Char]]
    optDefault :: EnvVal
    optCheck :: Checker
    optHelp :: [Char]
    .. }

    userOptionsWithAliases :: OptionMap
    userOptionsWithAliases :: OptionMap
    userOptionsWithAliases = (OptionMap -> OptionDescr -> OptionMap)
    -> OptionMap -> [OptionDescr] -> OptionMap
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl OptionMap -> OptionDescr -> OptionMap
    insert OptionMap
    userOptions (OptionMap -> [OptionDescr]
    forall a. Trie a -> [a]
    leaves OptionMap
    userOptions)
      where
      insert :: OptionMap -> OptionDescr -> OptionMap
    insert OptionMap
    m OptionDescr
    d = (OptionMap -> [Char] -> OptionMap)
    -> OptionMap -> [[Char]] -> OptionMap
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\OptionMap
    m' [Char]
    n -> [Char] -> OptionDescr -> OptionMap -> OptionMap
    forall a. [Char] -> a -> Trie a -> Trie a
    insertTrie [Char]
    n OptionDescr
    d OptionMap
    m') OptionMap
    m (OptionDescr -> [[Char]]
    optAliases OptionDescr
    d)

    userOptions :: OptionMap
    userOptions :: OptionMap
    userOptions  = [OptionDescr] -> OptionMap
    mkOptionMap
      [ [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "base" [] (Int -> EnvVal
    EnvNum Int
    16) Checker
    checkBase
        [Char]
    "The base to display words at (2, 8, 10, or 16)."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "debug" [] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Enable debugging output."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "ascii" [] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Whether to display 7- or 8-bit words using ASCII notation."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "infLength" [[Char]
    "inf-length"] (Int -> EnvVal
    EnvNum Int
    5) Checker
    checkInfLength
        [Char]
    "The number of elements to display for infinite sequences."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "tests" [] (Int -> EnvVal
    EnvNum Int
    100) Checker
    noCheck
        [Char]
    "The number of random tests to try with ':check'."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "satNum" [[Char]
    "sat-num"] ([Char] -> EnvVal
    EnvString [Char]
    "1") Checker
    checkSatNum
        [Char]
    "The maximum number of :sat solutions to display (\"all\" for no limit)."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "prover" [] ([Char] -> EnvVal
    EnvString [Char]
    "z3") Checker
    checkProver ([Char] -> OptionDescr) -> [Char] -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        [Char]
    "The external SMT solver for ':prove' and ':sat'\n(" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    proverListString [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ")."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "warnDefaulting" [[Char]
    "warn-defaulting"] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Choose whether to display warnings when defaulting."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "warnShadowing" [[Char]
    "warn-shadowing"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Choose whether to display warnings when shadowing symbols."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "warnPrefixAssoc" [[Char]
    "warn-prefix-assoc"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Choose whether to display warnings when expression association has changed due to new prefix operator fixities."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "warnUninterp" [[Char]
    "warn-uninterp"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "warnNonExhaustiveConstraintGuards" [[Char]
    "warn-nonexhaustive-constraintguards"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Choose whether to issue a warning when a use of constraint guards is not determined to be exhaustive."
      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "smtFile" [[Char]
    "smt-file"] ([Char] -> EnvVal
    EnvString [Char]
    "-") Checker
    noCheck
        [Char]
    "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
      , [Char]
    -> [[Char]]
    -> EnvVal
    -> Checker
    -> [Char]
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr [Char]
    "path" [] ([Char] -> EnvVal
    EnvString [Char]
    "") Checker
    noCheck
        [Char]
    "The search path for finding named Cryptol modules." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        \case EnvString [Char]
    path ->
                do let segs :: [[Char]]
    segs = [Char] -> [[Char]]
    parseSearchPath [Char]
    path
                   ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                   ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meSearchPath :: [[Char]]
    M.meSearchPath = [[Char]]
    segs }
              EnvVal
    _ -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , [Char]
    -> [[Char]]
    -> EnvVal
    -> Checker
    -> [Char]
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr [Char]
    "monoBinds" [[Char]
    "mono-binds"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Whether or not to generalize bindings in a 'where' clause." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        \case EnvBool Bool
    b -> do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                              ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meMonoBinds :: Bool
    M.meMonoBinds = Bool
    b }
              EnvVal
    _         -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , [Char]
    -> [[Char]]
    -> EnvVal
    -> Checker
    -> [Char]
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr [Char]
    "tcSolver" [[Char]
    "tc-solver"] ([Char] -> [[Char]] -> EnvVal
    EnvProg [Char]
    "z3" [ [Char]
    "-smt2", [Char]
    "-in" ])
        Checker
    noCheck  -- TODO: check for the program in the path
        [Char]
    "The solver that will be used by the type checker." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        \case EnvProg [Char]
    prog [[Char]]
    args -> do (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw { eTCConfig :: SolverConfig
    eTCConfig = (RW -> SolverConfig
    eTCConfig RW
    rw)
                                                                          { solverPath :: [Char]
    T.solverPath = [Char]
    prog
                                                                          , solverArgs :: [[Char]]
    T.solverArgs = [[Char]]
    args
                                                                          }})
                                      REPL ()
    resetTCSolver
              EnvVal
    _                 -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , [Char]
    -> [[Char]]
    -> EnvVal
    -> Checker
    -> [Char]
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr [Char]
    "tcDebug" [[Char]
    "tc-debug"] (Int -> EnvVal
    EnvNum Int
    0)
        Checker
    noCheck
        ([[Char]] -> [Char]
    unlines
          [ [Char]
    "Enable type-checker debugging output:"
          , [Char]
    "  *  0  no debug output"
          , [Char]
    "  *  1  show type-checker debug info"
          , [Char]
    "  * >1  show type-checker debug info and interactions with SMT solver"]) ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        \case EnvNum Int
    n -> do Bool
    changed <- (RW -> (RW, Bool)) -> REPL Bool
    forall a. (RW -> (RW, a)) -> REPL a
    modifyRW (\RW
    rw -> ( RW
    rw{ eTCConfig :: SolverConfig
    eTCConfig = (RW -> SolverConfig
    eTCConfig RW
    rw){ solverVerbose :: Int
    T.solverVerbose = Int
    n } }
                                                         , Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= SolverConfig -> Int
    T.solverVerbose (RW -> SolverConfig
    eTCConfig RW
    rw)
                                                         ))
                             Bool -> REPL () -> REPL ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    changed REPL ()
    resetTCSolver
              EnvVal
    _        -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , [Char]
    -> [[Char]]
    -> EnvVal
    -> Checker
    -> [Char]
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr [Char]
    "coreLint" [[Char]
    "core-lint"] (Bool -> EnvVal
    EnvBool Bool
    False)
        Checker
    noCheck
        [Char]
    "Enable sanity checking of type-checker." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
          let setIt :: CoreLint -> REPL ()
    setIt CoreLint
    x = do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                           ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meCoreLint :: CoreLint
    M.meCoreLint = CoreLint
    x }
          in \case EnvBool Bool
    True  -> CoreLint -> REPL ()
    setIt CoreLint
    M.CoreLint
                   EnvBool Bool
    False -> CoreLint -> REPL ()
    setIt CoreLint
    M.NoCoreLint
                   EnvVal
    _             -> () -> REPL ()
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "hashConsing" [[Char]
    "hash-consing"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Enable hash-consing in the What4 symbolic backends."

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "proverStats" [[Char]
    "prover-stats"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Enable prover timing statistics."

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "proverValidate" [[Char]
    "prover-validate"] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Validate :sat examples and :prove counter-examples for correctness."

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "showExamples" [[Char]
    "show-examples"] (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        [Char]
    "Print the (counter) example after :sat or :prove"

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "fpBase" [[Char]
    "fp-base"] (Int -> EnvVal
    EnvNum Int
    16) Checker
    checkBase
        [Char]
    "The base to display floating point numbers at (2, 8, 10, or 16)."

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "fpFormat" [[Char]
    "fp-format"] ([Char] -> EnvVal
    EnvString [Char]
    "free") Checker
    checkPPFloatFormat
        ([Char] -> OptionDescr) -> [Char] -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
        [ [Char]
    "Specifies the format to use when showing floating point numbers:"
        , [Char]
    "  * free      show using as many digits as needed"
        , [Char]
    "  * free+exp  like `free` but always show exponent"
        , [Char]
    "  * .NUM      show NUM (>=1) digits after floating point"
        , [Char]
    "  * NUM       show using NUM (>=1) significant digits"
        , [Char]
    "  * NUM+exp   like NUM but always show exponent"
        ]

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "ignoreSafety" [[Char]
    "ignore-safety"] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Ignore safety predicates when performing :sat or :prove checks"

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "fieldOrder" [[Char]
    "field-order"] ([Char] -> EnvVal
    EnvString [Char]
    "display") Checker
    checkFieldOrder
        ([Char] -> OptionDescr) -> [Char] -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
        [ [Char]
    "The order that record fields are displayed in."
        , [Char]
    "  * display      try to match the order they were written in the source code"
        , [Char]
    "  * canonical    use a predictable, canonical order"
        ]

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "timeMeasurementPeriod" [[Char]
    "time-measurement-period"] (Int -> EnvVal
    EnvNum Int
    10)
        Checker
    checkTimeMeasurementPeriod
        ([Char] -> OptionDescr) -> [Char] -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
        [ [Char]
    "The period of time in seconds to spend collecting measurements when"
        , [Char]
    "  running :time."
        , [Char]
    "This is a lower bound and the actual time taken might be higher if the"
        , [Char]
    "  evaluation takes a long time."
        ]

      , [Char] -> [[Char]] -> EnvVal -> Checker -> [Char] -> OptionDescr
    simpleOpt [Char]
    "timeQuiet" [[Char]
    "time-quiet"] (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        [Char]
    "Suppress output of :time command and only bind result to `it`."
      ]

    parsePPFloatFormat :: String -> Maybe PPFloatFormat
    parsePPFloatFormat :: [Char] -> Maybe PPFloatFormat
    parsePPFloatFormat [Char]
    s =
      case [Char]
    s of
        [Char]
    "free"     -> PPFloatFormat -> Maybe PPFloatFormat
    forall a. a -> Maybe a
    Just (PPFloatFormat -> Maybe PPFloatFormat)
    -> PPFloatFormat -> Maybe PPFloatFormat
    forall a b. (a -> b) -> a -> b
    $ PPFloatExp -> PPFloatFormat
    FloatFree PPFloatExp
    AutoExponent
        [Char]
    "free+exp" -> PPFloatFormat -> Maybe PPFloatFormat
    forall a. a -> Maybe a
    Just (PPFloatFormat -> Maybe PPFloatFormat)
    -> PPFloatFormat -> Maybe PPFloatFormat
    forall a b. (a -> b) -> a -> b
    $ PPFloatExp -> PPFloatFormat
    FloatFree PPFloatExp
    ForceExponent
        Char
    '.' : [Char]
    xs   -> Int -> PPFloatFormat
    FloatFrac (Int -> PPFloatFormat) -> Maybe Int -> Maybe PPFloatFormat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> Maybe Int
    forall a. Read a => [Char] -> Maybe a
    readMaybe [Char]
    xs
        [Char]
    _ | ([Char]
    as,[Char]
    res) <- (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '+') [Char]
    s
          , Just Int
    n   <- [Char] -> Maybe Int
    forall a. Read a => [Char] -> Maybe a
    readMaybe [Char]
    as
          , Just PPFloatExp
    e   <- case [Char]
    res of
                          [Char]
    "+exp" -> PPFloatExp -> Maybe PPFloatExp
    forall a. a -> Maybe a
    Just PPFloatExp
    ForceExponent
                          [Char]
    ""     -> PPFloatExp -> Maybe PPFloatExp
    forall a. a -> Maybe a
    Just PPFloatExp
    AutoExponent
                          [Char]
    _      -> Maybe PPFloatExp
    forall a. Maybe a
    Nothing
            -> PPFloatFormat -> Maybe PPFloatFormat
    forall a. a -> Maybe a
    Just (Int -> PPFloatExp -> PPFloatFormat
    FloatFixed Int
    n PPFloatExp
    e)
        [Char]
    _  -> Maybe PPFloatFormat
    forall a. Maybe a
    Nothing

    checkPPFloatFormat :: Checker
    checkPPFloatFormat :: Checker
    checkPPFloatFormat EnvVal
    val =
      case EnvVal
    val of
        EnvString [Char]
    s | Just PPFloatFormat
    _ <- [Char] -> Maybe PPFloatFormat
    parsePPFloatFormat [Char]
    s -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
        EnvVal
    _ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "Failed to parse `fp-format`"

    parseFieldOrder :: String -> Maybe FieldOrder
    parseFieldOrder :: [Char] -> Maybe FieldOrder
    parseFieldOrder [Char]
    "canonical" = FieldOrder -> Maybe FieldOrder
    forall a. a -> Maybe a
    Just FieldOrder
    CanonicalOrder
    parseFieldOrder [Char]
    "display" = FieldOrder -> Maybe FieldOrder
    forall a. a -> Maybe a
    Just FieldOrder
    DisplayOrder
    parseFieldOrder [Char]
    _ = Maybe FieldOrder
    forall a. Maybe a
    Nothing

    checkFieldOrder :: Checker
    checkFieldOrder :: Checker
    checkFieldOrder EnvVal
    val =
      case EnvVal
    val of
        EnvString [Char]
    s | Just FieldOrder
    _ <- [Char] -> Maybe FieldOrder
    parseFieldOrder [Char]
    s -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
        EnvVal
    _ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "Failed to parse field-order (expected one of \"canonical\" or \"display\")"

    -- | Check the value to the `base` option.
    checkBase :: Checker
    checkBase :: Checker
    checkBase EnvVal
    val = case EnvVal
    val of
      EnvNum Int
    n
        | Int
    n Int -> [Int] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Int
    2,Int
    8,Int
    10,Int
    16] -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
        | Bool
    otherwise            -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "base must be 2, 8, 10, or 16"
      EnvVal
    _                     -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "unable to parse a value for base"

    checkInfLength :: Checker
    checkInfLength :: Checker
    checkInfLength EnvVal
    val = case EnvVal
    val of
      EnvNum Int
    n
        | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
        | Bool
    otherwise -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "the number of elements should be positive"
      EnvVal
    _ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "unable to parse a value for infLength"

    checkProver :: Checker
    checkProver :: Checker
    checkProver EnvVal
    val = case EnvVal
    val of
      EnvString ((Char -> Char) -> [Char] -> [Char]
    forall a b. (a -> b) -> [a] -> [b]
    map Char -> Char
    toLower -> [Char]
    s)
        | [Char]
    s [Char] -> [[Char]] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [[Char]]
    W4.proverNames ->
          IO (Either [Char] ([[Char]], W4ProverConfig))
    -> REPL (Either [Char] ([[Char]], W4ProverConfig))
    forall a. IO a -> REPL a
    io ([Char] -> IO (Either [Char] ([[Char]], W4ProverConfig))
    W4.setupProver [Char]
    s) REPL (Either [Char] ([[Char]], W4ProverConfig))
    -> (Either [Char] ([[Char]], W4ProverConfig)
        -> REPL (Maybe [Char], [[Char]]))
    -> REPL (Maybe [Char], [[Char]])
    forall a b. REPL a -> (a -> REPL b) -> REPL b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Left [Char]
    msg -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    msg)
            Right ([[Char]]
    ws, W4ProverConfig
    cfg) ->
              do (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw{ eProverConfig :: Either SBVProverConfig W4ProverConfig
    eProverConfig = W4ProverConfig -> Either SBVProverConfig W4ProverConfig
    forall a b. b -> Either a b
    Right W4ProverConfig
    cfg })
                 (Maybe [Char], [[Char]]) -> REPL (Maybe [Char], [[Char]])
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Char]
    forall a. Maybe a
    Nothing, [[Char]]
    ws)
        | [Char]
    s [Char] -> [[Char]] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [[Char]]
    SBV.proverNames ->
          IO (Either [Char] ([[Char]], SBVProverConfig))
    -> REPL (Either [Char] ([[Char]], SBVProverConfig))
    forall a. IO a -> REPL a
    io ([Char] -> IO (Either [Char] ([[Char]], SBVProverConfig))
    SBV.setupProver [Char]
    s) REPL (Either [Char] ([[Char]], SBVProverConfig))
    -> (Either [Char] ([[Char]], SBVProverConfig)
        -> REPL (Maybe [Char], [[Char]]))
    -> REPL (Maybe [Char], [[Char]])
    forall a b. REPL a -> (a -> REPL b) -> REPL b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Left [Char]
    msg -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns ([Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    msg)
            Right ([[Char]]
    ws, SBVProverConfig
    cfg) ->
              do (RW -> RW) -> REPL ()
    modifyRW_ (\RW
    rw -> RW
    rw{ eProverConfig :: Either SBVProverConfig W4ProverConfig
    eProverConfig = SBVProverConfig -> Either SBVProverConfig W4ProverConfig
    forall a b. a -> Either a b
    Left SBVProverConfig
    cfg })
                 (Maybe [Char], [[Char]]) -> REPL (Maybe [Char], [[Char]])
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [Char]
    forall a. Maybe a
    Nothing, [[Char]]
    ws)

        | Bool
    otherwise ->
          Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Prover must be " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    proverListString

      EnvVal
    _ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "unable to parse a value for prover"

    allProvers :: [String]
    allProvers :: [[Char]]
    allProvers = [[Char]]
    SBV.proverNames [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    W4.proverNames

    proverListString :: String
    proverListString :: [Char]
    proverListString = ([Char] -> [Char]) -> [[Char]] -> [Char]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ([Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ", ") ([[Char]] -> [[Char]]
    forall a. HasCallStack => [a] -> [a]
    init [[Char]]
    allProvers) [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "or " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    forall a. HasCallStack => [a] -> a
    last [[Char]]
    allProvers

    checkSatNum :: Checker
    checkSatNum :: Checker
    checkSatNum EnvVal
    val = case EnvVal
    val of
      EnvString [Char]
    "all" -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
      EnvString [Char]
    s ->
        case [Char] -> Maybe Int
    forall a. Read a => [Char] -> Maybe a
    readMaybe [Char]
    s :: Maybe Int of
          Just Int
    n | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1 -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
          Maybe Int
    _               -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "must be an integer > 0 or \"all\""
      EnvVal
    _ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "unable to parse a value for satNum"

    getUserSatNum :: REPL SatNum
    getUserSatNum :: REPL SatNum
    getUserSatNum = do
      [Char]
    s <- [Char] -> REPL [Char]
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "satNum"
      case [Char]
    s of
        [Char]
    "all"                     -> SatNum -> REPL SatNum
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SatNum
    AllSat
        [Char]
    _ | Just Int
    n <- [Char] -> Maybe Int
    forall a. Read a => [Char] -> Maybe a
    readMaybe [Char]
    s -> SatNum -> REPL SatNum
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> SatNum
    SomeSat Int
    n)
        [Char]
    _                         -> [Char] -> [[Char]] -> REPL SatNum
    forall a. HasCallStack => [Char] -> [[Char]] -> a
    panic [Char]
    "REPL.Monad.getUserSatNum"
                                       [ [Char]
    "invalid satNum option" ]

    checkTimeMeasurementPeriod :: Checker
    checkTimeMeasurementPeriod :: Checker
    checkTimeMeasurementPeriod (EnvNum Int
    n)
      | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    1 = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns Maybe [Char]
    forall a. Maybe a
    Nothing
      | Bool
    otherwise = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $
        [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "timeMeasurementPeriod must be a positive integer"
    checkTimeMeasurementPeriod EnvVal
    _ = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
    -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
    forall a b. (a -> b) -> a -> b
    $
      [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    "unable to parse value for timeMeasurementPeriod"

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

    whenDebug :: REPL () -> REPL ()
    whenDebug :: REPL () -> REPL ()
    whenDebug REPL ()
    m = do
      Bool
    b <- [Char] -> REPL Bool
    forall a. IsEnvVal a => [Char] -> REPL a
    getKnownUser [Char]
    "debug"
      Bool -> REPL () -> REPL ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    b REPL ()
    m

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

    smokeTest :: REPL [Smoke]
    smokeTest :: REPL [Smoke]
    smokeTest = [Maybe Smoke] -> [Smoke]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe Smoke] -> [Smoke]) -> REPL [Maybe Smoke] -> REPL [Smoke]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [REPL (Maybe Smoke)] -> REPL [Maybe Smoke]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [REPL (Maybe Smoke)]
    tests
      where
        tests :: [REPL (Maybe Smoke)]
    tests = [ REPL (Maybe Smoke)
    z3exists ]

    type SmokeTest = REPL (Maybe Smoke)

    data Smoke
      = Z3NotFound
      deriving (Int -> Smoke -> [Char] -> [Char]
    [Smoke] -> [Char] -> [Char]
    Smoke -> [Char]
    (Int -> Smoke -> [Char] -> [Char])
    -> (Smoke -> [Char]) -> ([Smoke] -> [Char] -> [Char]) -> Show Smoke
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Int -> Smoke -> [Char] -> [Char]
    showsPrec :: Int -> Smoke -> [Char] -> [Char]
    $cshow :: Smoke -> [Char]
    show :: Smoke -> [Char]
    $cshowList :: [Smoke] -> [Char] -> [Char]
    showList :: [Smoke] -> [Char] -> [Char]
    Show, Smoke -> Smoke -> Bool
    (Smoke -> Smoke -> Bool) -> (Smoke -> Smoke -> Bool) -> Eq Smoke
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Smoke -> Smoke -> Bool
    == :: Smoke -> Smoke -> Bool
    $c/= :: Smoke -> Smoke -> Bool
    /= :: Smoke -> Smoke -> Bool
    Eq)

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

    z3exists :: SmokeTest
    z3exists :: REPL (Maybe Smoke)
    z3exists = do
      Maybe [Char]
    mPath <- IO (Maybe [Char]) -> REPL (Maybe [Char])
    forall a. IO a -> REPL a
    io (IO (Maybe [Char]) -> REPL (Maybe [Char]))
    -> IO (Maybe [Char]) -> REPL (Maybe [Char])
    forall a b. (a -> b) -> a -> b
    $ [Char] -> IO (Maybe [Char])
    findExecutable [Char]
    "z3"
      case Maybe [Char]
    mPath of
        Maybe [Char]
    Nothing -> Maybe Smoke -> REPL (Maybe Smoke)
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Smoke -> Maybe Smoke
    forall a. a -> Maybe a
    Just Smoke
    Z3NotFound)
        Just [Char]
    _  -> Maybe Smoke -> REPL (Maybe Smoke)
    forall a. a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Smoke
    forall a. Maybe a
    Nothing