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

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

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

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

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

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

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

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

      ) where

    import Cryptol.REPL.Trie

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

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

    import Data.SBV.Dynamic (sbvCheckSolverInstallation)

    import Prelude ()
    import Prelude.Compat

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

    -- | This indicates what the user would like to work on.
    data LoadedModule = LoadedModule
      { 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 FilePath
    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
    eLetEnabled  :: Bool
        -- ^ Should we allow `let` on the command line

      , 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.
      }

    -- | Initial, empty environment.
    defaultRW :: Bool -> Logger -> IO RW
    defaultRW :: Bool -> Logger -> IO RW
    defaultRW isBatch :: Bool
    isBatch l :: Logger
    l = do
      ModuleEnv
    env <- IO ModuleEnv
    M.initialModuleEnv
      RW -> IO RW
    forall (m :: * -> *) a. Monad m => a -> m a
    return RW :: Maybe LoadedModule
    -> Maybe FilePath
    -> Bool
    -> Bool
    -> ModuleEnv
    -> UserEnv
    -> Logger
    -> Bool
    -> REPL ()
    -> RW
    RW
        { eLoadedMod :: Maybe LoadedModule
    eLoadedMod   = Maybe LoadedModule
    forall a. Maybe a
    Nothing
        , eEditFile :: Maybe FilePath
    eEditFile    = Maybe FilePath
    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
        , eLetEnabled :: Bool
    eLetEnabled  = Bool
    True
        , eUpdateTitle :: REPL ()
    eUpdateTitle = () -> REPL ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        }

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

      modLn :: FilePath
    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
          Nothing -> Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    I.preludeName)
          Just m :: ModName
    m
            | ModName -> LoadedModules -> Bool
    M.isLoadedParamMod ModName
    m (ModuleEnv -> LoadedModules
    M.meLoadedModules (RW -> ModuleEnv
    eModuleEnv RW
    rw)) ->
                     FilePath
    modName FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "(parameterized)"
            | Bool
    otherwise -> FilePath
    modName
            where modName :: FilePath
    modName = ModName -> FilePath
    forall a. PP a => a -> FilePath
    pretty ModName
    m

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

      withEdit :: FilePath
    withEdit =
        case RW -> Maybe FilePath
    eEditFile RW
    rw of
          Nothing -> FilePath
    withFocus
          Just e :: FilePath
    e
            | Just (M.InFile f :: FilePath
    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
            , FilePath
    f FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == FilePath
    e -> FilePath
    withFocus
            | Bool
    otherwise -> ":e to edit " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    e FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "\n" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    withFocus

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

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

    -- | Run a REPL action with a fresh environment.
    runREPL :: Bool -> Logger -> REPL a -> IO a
    runREPL :: Bool -> Logger -> REPL a -> IO a
    runREPL isBatch :: Bool
    isBatch l :: Logger
    l m :: REPL a
    m = do
      IORef RW
    ref <- 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 -> Logger -> IO RW
    defaultRW Bool
    isBatch Logger
    l
      REPL a -> IORef RW -> IO a
    forall a. REPL a -> IORef RW -> IO a
    unREPL REPL a
    m IORef RW
    ref

    instance Functor REPL where
      {-# INLINE fmap #-}
      fmap :: (a -> b) -> REPL a -> REPL b
    fmap f :: a -> b
    f m :: REPL a
    m = (IORef RW -> IO b) -> REPL b
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ ref :: IORef RW
    ref -> (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 :: a -> REPL a
    pure = a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      {-# INLINE (<*>) #-}
      <*> :: 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 :: a -> REPL a
    return x :: a
    x = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\_ -> a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x)

      {-# INLINE (>>=) #-}
      m :: REPL a
    m >>= :: REPL a -> (a -> REPL b) -> REPL b
    >>= f :: 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
    $ \ref :: 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 :: IO a -> REPL a
    liftIO = IO a -> REPL a
    forall a. IO a -> REPL a
    io

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

    instance MonadBaseControl IO REPL where
      type StM REPL a = a
      liftBaseWith :: (RunInBase REPL IO -> IO a) -> REPL a
    liftBaseWith f :: 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
    $ \ref :: 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
    $ \m :: 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 :: StM REPL a -> REPL a
    restoreM x :: StM REPL a
    x = a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    StM REPL a
    x

    instance M.FreshM REPL where
      liftSupply :: (Supply -> (a, Supply)) -> REPL a
    liftSupply f :: 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 { .. } ->
        let (a :: a
    a,s' :: Supply
    s') = Supply -> (a, Supply)
    f (ModuleEnv -> Supply
    M.meSupply ModuleEnv
    eModuleEnv)
         in (RW :: Maybe LoadedModule
    -> Maybe FilePath
    -> Bool
    -> Bool
    -> ModuleEnv
    -> UserEnv
    -> Logger
    -> Bool
    -> REPL ()
    -> RW
    RW { eModuleEnv :: ModuleEnv
    eModuleEnv = ModuleEnv
    eModuleEnv { meSupply :: Supply
    M.meSupply = Supply
    s' }, .. },a
    a)

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

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

    instance X.Exception REPLException

    instance PP REPLException where
      ppPrec :: Int -> REPLException -> Doc
    ppPrec _ re :: REPLException
    re = case REPLException
    re of
        ParseError e :: ParseError
    e         -> ParseError -> Doc
    ppError ParseError
    e
        FileNotFound path :: FilePath
    path    -> [Doc] -> Doc
    sep [ FilePath -> Doc
    text "File"
                                    , FilePath -> Doc
    text ("`" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    path FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "'")
                                    , FilePath -> Doc
    text"not found"
                                    ]
        DirectoryNotFound path :: FilePath
    path -> [Doc] -> Doc
    sep [ FilePath -> Doc
    text "Directory"
                                      , FilePath -> Doc
    text ("`" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    path FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "'")
                                      , FilePath -> Doc
    text"not found or not a directory"
                                      ]
        NoPatError es :: [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 es :: [IncludeError]
    es    -> [Doc] -> Doc
    vcat ((IncludeError -> Doc) -> [IncludeError] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map IncludeError -> Doc
    ppIncludeError [IncludeError]
    es)
        ModuleSystemError ns :: NameDisp
    ns me :: ModuleError
    me -> NameDisp -> Doc -> Doc
    fixNameDisp NameDisp
    ns (ModuleError -> Doc
    forall a. PP a => a -> Doc
    pp ModuleError
    me)
        EvalError e :: EvalError
    e          -> EvalError -> Doc
    forall a. PP a => a -> Doc
    pp EvalError
    e
        EvalPolyError s :: Schema
    s      -> FilePath -> Doc
    text "Cannot evaluate polymorphic value."
                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "Type:" Doc -> Doc -> Doc
    <+> Schema -> Doc
    forall a. PP a => a -> Doc
    pp Schema
    s
        TypeNotTestable t :: Type
    t    -> FilePath -> Doc
    text "The expression is not of a testable type."
                             Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text "Type:" Doc -> Doc -> Doc
    <+> Type -> Doc
    forall a. PP a => a -> Doc
    pp Type
    t
        EvalInParamModule xs :: [Name]
    xs ->
          FilePath -> Doc
    text "Expression depends on definitions from a parameterized module:"
            Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((Name -> Doc) -> [Name] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc
    forall a. PP a => a -> Doc
    pp [Name]
    xs))
        SBVError s :: FilePath
    s           -> FilePath -> Doc
    text "SBV error:" Doc -> Doc -> Doc
    $$ FilePath -> Doc
    text FilePath
    s

    -- | Raise an exception.
    raise :: REPLException -> REPL a
    raise :: REPLException -> REPL a
    raise exn :: 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 :: REPL a -> (REPLException -> REPL a) -> REPL a
    catch m :: REPL a
    m k :: REPLException -> REPL a
    k = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ ref :: 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` \ e :: 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 :: REPL a -> REPL b -> REPL a
    finally m1 :: REPL a
    m1 m2 :: REPL b
    m2 = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ref :: 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 :: IO a -> IO a
    rethrowEvalError m :: IO a
    m = IO a
    run IO a -> (EvalError -> IO a) -> IO a
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `X.catch` EvalError -> IO a
    forall a. EvalError -> IO a
    rethrow
      where
      run :: IO a
    run = do
        a
    a <- IO a
    m
        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 :: EvalError -> IO a
      rethrow :: EvalError -> IO a
    rethrow exn :: EvalError
    exn = REPLException -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (EvalError -> REPLException
    EvalError EvalError
    exn)

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

    io :: IO a -> REPL a
    io :: IO a -> REPL a
    io m :: IO a
    m = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ _ -> 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 :: (RW -> (RW, a)) -> REPL a
    modifyRW f :: RW -> (RW, a)
    f = (IORef RW -> IO a) -> REPL a
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ ref :: 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_ f :: RW -> RW
    f = (IORef RW -> IO ()) -> REPL ()
    forall a. (IORef RW -> IO a) -> REPL a
    REPL (\ ref :: IORef RW
    ref -> IORef RW -> (RW -> RW) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    modifyIORef IORef RW
    ref RW -> RW
    f)

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

    clearLoadedMod :: REPL ()
    clearLoadedMod :: REPL ()
    clearLoadedMod = do (RW -> RW) -> REPL ()
    modifyRW_ (\rw :: 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 x :: 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 n :: LoadedModule
    n = do
      (RW -> RW) -> REPL ()
    modifyRW_ (\ rw :: 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 (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 :: FilePath -> REPL ()
    setEditPath p :: FilePath
    p = (RW -> RW) -> REPL ()
    modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
    forall a b. (a -> b) -> a -> b
    $ \rw :: RW
    rw -> RW
    rw { eEditFile :: Maybe FilePath
    eEditFile = FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just FilePath
    p }

    getEditPath :: REPL (Maybe FilePath)
    getEditPath :: REPL (Maybe FilePath)
    getEditPath = RW -> Maybe FilePath
    eEditFile (RW -> Maybe FilePath) -> REPL RW -> REPL (Maybe FilePath)
    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
    rw { eEditFile :: Maybe FilePath
    eEditFile = Maybe FilePath
    forall a. Maybe a
    Nothing }

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

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

    shouldContinue :: REPL Bool
    shouldContinue :: REPL Bool
    shouldContinue  = RW -> Bool
    eContinue (RW -> Bool) -> REPL RW -> REPL Bool
    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
    rw { eContinue :: Bool
    eContinue = Bool
    False })

    unlessBatch :: REPL () -> REPL ()
    unlessBatch :: REPL () -> REPL ()
    unlessBatch body :: 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 :: REPL a -> REPL a
    asBatch body :: REPL a
    body = do
      Bool
    wasBatch <- RW -> Bool
    eIsBatch (RW -> Bool) -> REPL RW -> REPL Bool
    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
    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
    rw { eIsBatch :: Bool
    eIsBatch = Bool
    wasBatch })
      a -> REPL a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

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

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

    -- | Are let-bindings enabled in this REPL?
    getLetEnabled :: REPL Bool
    getLetEnabled :: REPL Bool
    getLetEnabled = (RW -> Bool) -> REPL RW -> REPL Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap RW -> Bool
    eLetEnabled REPL RW
    getRW

    -- | Is evaluation enabled.  If the currently focused module is
    -- parameterized, then we cannot evalute.
    validEvalContext :: T.FreeVars a => a -> REPL ()
    validEvalContext :: a -> REPL ()
    validEvalContext a :: 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 (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 (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)

             badName :: Name -> Set Name -> Set Name
    badName nm :: Name
    nm bs :: Set Name
    bs =
               case Name -> NameInfo
    M.nameInfo Name
    nm of
                 M.Declared m :: 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
                 _ -> 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) (REPL () -> REPL ()) -> REPL () -> REPL ()
    forall a b. (a -> b) -> a -> b
    $
           REPLException -> REPL ()
    forall a. REPLException -> REPL a
    raise ([Name] -> REPLException
    EvalInParamModule (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 m :: REPL ()
    m = (RW -> RW) -> REPL ()
    modifyRW_ (\rw :: RW
    rw -> RW
    rw { eUpdateTitle :: REPL ()
    eUpdateTitle = REPL ()
    m })

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

    -- | Get the REPL's string-printer
    getPutStr :: REPL (String -> IO ())
    getPutStr :: REPL (FilePath -> IO ())
    getPutStr =
      do RW
    rw <- REPL RW
    getRW
         (FilePath -> IO ()) -> REPL (FilePath -> IO ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Logger -> FilePath -> 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 :: FilePath -> REPL ()
    rPutStr str :: FilePath
    str = do
      FilePath -> IO ()
    f <- REPL (FilePath -> IO ())
    getPutStr
      IO () -> REPL ()
    forall a. IO a -> REPL a
    io (FilePath -> IO ()
    f FilePath
    str)

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

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

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

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

    getVars :: REPL (Map.Map M.Name M.IfaceDecl)
    getVars :: REPL (Map Name IfaceDecl)
    getVars  = do
      (_,decls :: IfaceDecls
    decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
      Map Name IfaceDecl -> REPL (Map Name IfaceDecl)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceDecls -> Map Name IfaceDecl
    M.ifDecls IfaceDecls
    decls)

    getTSyns :: REPL (Map.Map M.Name T.TySyn)
    getTSyns :: REPL (Map Name TySyn)
    getTSyns  = do
      (_,decls :: IfaceDecls
    decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
      Map Name TySyn -> REPL (Map Name TySyn)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceDecls -> Map Name TySyn
    M.ifTySyns IfaceDecls
    decls)

    getNewtypes :: REPL (Map.Map M.Name T.Newtype)
    getNewtypes :: REPL (Map Name Newtype)
    getNewtypes = do
      (_,decls :: IfaceDecls
    decls,_,_) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
      Map Name Newtype -> REPL (Map Name Newtype)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IfaceDecls -> Map Name Newtype
    M.ifNewtypes IfaceDecls
    decls)

    -- | Get visible variable names.
    getExprNames :: REPL [String]
    getExprNames :: REPL [FilePath]
    getExprNames =
      do (_,_, fNames :: NamingEnv
    fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
         [FilePath] -> REPL [FilePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((PName -> FilePath) -> [PName] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PName -> Doc
    forall a. PP a => a -> Doc
    pp) (Map PName [Name] -> [PName]
    forall k a. Map k a -> [k]
    Map.keys (NamingEnv -> Map PName [Name]
    M.neExprs NamingEnv
    fNames)))

    -- | Get visible type signature names.
    getTypeNames :: REPL [String]
    getTypeNames :: REPL [FilePath]
    getTypeNames  =
      do (_,_, fNames :: NamingEnv
    fNames, _) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
         [FilePath] -> REPL [FilePath]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((PName -> FilePath) -> [PName] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map (Doc -> FilePath
    forall a. Show a => a -> FilePath
    show (Doc -> FilePath) -> (PName -> Doc) -> PName -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PName -> Doc
    forall a. PP a => a -> Doc
    pp) (Map PName [Name] -> [PName]
    forall k a. Map k a -> [k]
    Map.keys (NamingEnv -> Map PName [Name]
    M.neTypes NamingEnv
    fNames)))

    -- | Return a list of property names, sorted by position in the file.
    getPropertyNames :: REPL ([M.Name],NameDisp)
    getPropertyNames :: REPL ([Name], NameDisp)
    getPropertyNames =
      do (_,decls :: IfaceDecls
    decls,_,names :: NameDisp
    names) <- REPL (IfaceParams, IfaceDecls, NamingEnv, NameDisp)
    getFocusedEnv
         let xs :: Map Name IfaceDecl
    xs = IfaceDecls -> Map Name IfaceDecl
    M.ifDecls IfaceDecls
    decls
             ps :: [Name]
    ps = (Name -> Name -> Ordering) -> [Name] -> [Name]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy ((Name -> Position) -> Name -> Name -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing (Range -> Position
    from (Range -> Position) -> (Name -> Range) -> Name -> Position
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Range
    M.nameLoc))
                ([Name] -> [Name]) -> [Name] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ [ Name
    x | (x :: Name
    x,d :: 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` IfaceDecl -> [Pragma]
    M.ifDeclPragmas IfaceDecl
    d ]

         ([Name], NameDisp) -> REPL ([Name], NameDisp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Name]
    ps, NameDisp
    names)

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

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

    setModuleEnv :: M.ModuleEnv -> REPL ()
    setModuleEnv :: ModuleEnv -> REPL ()
    setModuleEnv me :: ModuleEnv
    me = (RW -> RW) -> REPL ()
    modifyRW_ (\rw :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` REPL RW
    getRW

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

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

    uniqify :: Name -> REPL Name
    uniqify name :: Name
    name =
      case Name -> NameInfo
    M.nameInfo Name
    name of
        M.Declared ns :: ModName
    ns s :: NameSource
    s ->
          (Supply -> (Name, Supply)) -> REPL Name
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    M.liftSupply (ModName
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    M.mkDeclared ModName
    ns NameSource
    s (Name -> Ident
    M.nameIdent Name
    name) (Name -> Maybe Fixity
    M.nameFixity Name
    name) (Name -> Range
    M.nameLoc Name
    name))

        M.Parameter ->
          FilePath -> [FilePath] -> REPL Name
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "[REPL] uniqify" ["tried to uniqify a parameter: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Name -> FilePath
    forall a. PP a => a -> FilePath
    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 i :: Ident
    i sys :: NameSource
    sys =
      (Supply -> (Name, Supply)) -> REPL Name
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    M.liftSupply (ModName
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    M.mkDeclared ModName
    I.interactiveName NameSource
    sys Ident
    i Maybe Fixity
    forall a. Maybe a
    Nothing Range
    emptyRange)

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

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

    data EnvVal
      = EnvString String
      | EnvProg   String [String]
      | EnvNum    !Int
      | EnvBool   Bool
        deriving (Int -> EnvVal -> FilePath -> FilePath
    [EnvVal] -> FilePath -> FilePath
    EnvVal -> FilePath
    (Int -> EnvVal -> FilePath -> FilePath)
    -> (EnvVal -> FilePath)
    -> ([EnvVal] -> FilePath -> FilePath)
    -> Show EnvVal
    forall a.
    (Int -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    showList :: [EnvVal] -> FilePath -> FilePath
    $cshowList :: [EnvVal] -> FilePath -> FilePath
    show :: EnvVal -> FilePath
    $cshow :: EnvVal -> FilePath
    showsPrec :: Int -> EnvVal -> FilePath -> FilePath
    $cshowsPrec :: Int -> EnvVal -> FilePath -> FilePath
    Show)

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

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

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

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

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

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

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

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

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

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

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

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

    -- | Get a user option, using Maybe for failure.
    tryGetUser :: String -> REPL (Maybe EnvVal)
    tryGetUser :: FilePath -> REPL (Maybe EnvVal)
    tryGetUser name :: FilePath
    name = do
      RW
    rw <- REPL RW
    getRW
      Maybe EnvVal -> REPL (Maybe EnvVal)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath -> UserEnv -> Maybe EnvVal
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup FilePath
    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 :: FilePath -> REPL EnvVal
    getUser name :: FilePath
    name = do
      Maybe EnvVal
    mb <- FilePath -> REPL (Maybe EnvVal)
    tryGetUser FilePath
    name
      case Maybe EnvVal
    mb of
        Just ev :: EnvVal
    ev -> EnvVal -> REPL EnvVal
    forall (m :: * -> *) a. Monad m => a -> m a
    return EnvVal
    ev
        Nothing -> FilePath -> [FilePath] -> REPL EnvVal
    forall a. HasCallStack => FilePath -> [FilePath] -> a
    panic "[REPL] getUser" ["option `" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    name FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ "` does not exist"]

    getKnownUser :: IsEnvVal a => String -> REPL a
    getKnownUser :: FilePath -> REPL a
    getKnownUser x :: FilePath
    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
    <$> FilePath -> REPL EnvVal
    getUser FilePath
    x

    class IsEnvVal a where
      fromEnvVal :: EnvVal -> a

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

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

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

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

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

    getUserShowProverStats :: REPL Bool
    getUserShowProverStats :: REPL Bool
    getUserShowProverStats = FilePath -> REPL Bool
    forall a. IsEnvVal a => FilePath -> REPL a
    getKnownUser "prover-stats"

    getUserProverValidate :: REPL Bool
    getUserProverValidate :: REPL Bool
    getUserProverValidate = FilePath -> REPL Bool
    forall a. IsEnvVal a => FilePath -> REPL a
    getKnownUser "prover-validate"

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

    type OptionMap = Trie OptionDescr

    mkOptionMap :: [OptionDescr] -> OptionMap
    mkOptionMap :: [OptionDescr] -> OptionMap
    mkOptionMap  = (OptionMap -> OptionDescr -> OptionMap)
    -> OptionMap -> [OptionDescr] -> OptionMap
    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 m :: OptionMap
    m d :: OptionDescr
    d = FilePath -> OptionDescr -> OptionMap -> OptionMap
    forall a. FilePath -> a -> Trie a -> Trie a
    insertTrie (OptionDescr -> FilePath
    optName OptionDescr
    d) OptionDescr
    d OptionMap
    m

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

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

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

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

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

    userOptions :: OptionMap
    userOptions :: OptionMap
    userOptions  = [OptionDescr] -> OptionMap
    mkOptionMap
      [ FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "base" (Int -> EnvVal
    EnvNum 16) Checker
    checkBase
        "The base to display words at (2, 8, 10, or 16)."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "debug" (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        "Enable debugging output."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "ascii" (Bool -> EnvVal
    EnvBool Bool
    False) Checker
    noCheck
        "Whether to display 7- or 8-bit words using ASCII notation."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "infLength" (Int -> EnvVal
    EnvNum 5) Checker
    checkInfLength
        "The number of elements to display for infinite sequences."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "tests" (Int -> EnvVal
    EnvNum 100) Checker
    noCheck
        "The number of random tests to try with ':check'."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "satNum" (FilePath -> EnvVal
    EnvString "1") Checker
    checkSatNum
        "The maximum number of :sat solutions to display (\"all\" for no limit)."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "prover" (FilePath -> EnvVal
    EnvString "z3") Checker
    checkProver (FilePath -> OptionDescr) -> FilePath -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        "The external SMT solver for ':prove' and ':sat'\n(" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    proverListString FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ ")."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "warnDefaulting" (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        "Choose whether to display warnings when defaulting."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "warnShadowing" (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        "Choose whether to display warnings when shadowing symbols."
      , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
    simpleOpt "smtfile" (FilePath -> EnvVal
    EnvString "-") Checker
    noCheck
        "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
      , FilePath
    -> EnvVal
    -> Checker
    -> FilePath
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr "mono-binds" (Bool -> EnvVal
    EnvBool Bool
    True) Checker
    noCheck
        "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 b :: Bool
    b -> do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                              ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meMonoBinds :: Bool
    M.meMonoBinds = Bool
    b }
              _         -> () -> REPL ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , FilePath
    -> EnvVal
    -> Checker
    -> FilePath
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr "tc-solver" (FilePath -> [FilePath] -> EnvVal
    EnvProg "z3" [ "-smt2", "-in" ])
        Checker
    noCheck  -- TODO: check for the program in the path
        "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 prog :: FilePath
    prog args :: [FilePath]
    args -> do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                                      let cfg :: SolverConfig
    cfg = ModuleEnv -> SolverConfig
    M.meSolverConfig ModuleEnv
    me
                                      ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meSolverConfig :: SolverConfig
    M.meSolverConfig =
                                                          SolverConfig
    cfg { solverPath :: FilePath
    T.solverPath = FilePath
    prog
                                                              , solverArgs :: [FilePath]
    T.solverArgs = [FilePath]
    args } }
              _                 -> () -> REPL ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

      , FilePath
    -> EnvVal
    -> Checker
    -> FilePath
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr "tc-debug" (Int -> EnvVal
    EnvNum 0)
        Checker
    noCheck
        "Enable type-checker debugging output." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
        \case EnvNum n :: Int
    n -> do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                             let cfg :: SolverConfig
    cfg = ModuleEnv -> SolverConfig
    M.meSolverConfig ModuleEnv
    me
                             ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meSolverConfig :: SolverConfig
    M.meSolverConfig = SolverConfig
    cfg{ solverVerbose :: Int
    T.solverVerbose = Int
    n } }
              _        -> () -> REPL ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      , FilePath
    -> EnvVal
    -> Checker
    -> FilePath
    -> (EnvVal -> REPL ())
    -> OptionDescr
    OptionDescr "core-lint" (Bool -> EnvVal
    EnvBool Bool
    False)
        Checker
    noCheck
        "Enable sanity checking of type-checker." ((EnvVal -> REPL ()) -> OptionDescr)
    -> (EnvVal -> REPL ()) -> OptionDescr
    forall a b. (a -> b) -> a -> b
    $
          let setIt :: CoreLint -> REPL ()
    setIt x :: CoreLint
    x = do ModuleEnv
    me <- REPL ModuleEnv
    getModuleEnv
                           ModuleEnv -> REPL ()
    setModuleEnv ModuleEnv
    me { meCoreLint :: CoreLint
    M.meCoreLint = CoreLint
    x }
          in \case EnvBool True  -> CoreLint -> REPL ()
    setIt CoreLint
    M.CoreLint
                   EnvBool False -> CoreLint -> REPL ()
    setIt CoreLint
    M.NoCoreLint
                   _             -> () -> REPL ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()

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

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

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

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

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

    checkProver :: Checker
    checkProver :: Checker
    checkProver val :: EnvVal
    val = case EnvVal
    val of
      EnvString s :: FilePath
    s
        | FilePath
    s FilePath -> [FilePath] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [FilePath]
    proverNames ->
          Maybe FilePath -> IO (Maybe FilePath, [FilePath])
    noWarns (Maybe FilePath -> IO (Maybe FilePath, [FilePath]))
    -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just (FilePath -> Maybe FilePath) -> FilePath -> Maybe FilePath
    forall a b. (a -> b) -> a -> b
    $ "Prover must be " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    proverListString
        | FilePath
    s FilePath -> [FilePath] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ["offline", "any"] -> Maybe FilePath -> IO (Maybe FilePath, [FilePath])
    noWarns Maybe FilePath
    forall a. Maybe a
    Nothing
        | Bool
    otherwise ->
          do let prover :: SMTConfig
    prover = FilePath -> SMTConfig
    lookupProver FilePath
    s
             Bool
    available <- SMTConfig -> IO Bool
    sbvCheckSolverInstallation SMTConfig
    prover
             let ws :: [FilePath]
    ws = if Bool
    available
                         then []
                         else ["Warning: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ " installation not found"]
             (Maybe FilePath, [FilePath]) -> IO (Maybe FilePath, [FilePath])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe FilePath
    forall a. Maybe a
    Nothing, [FilePath]
    ws)

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

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

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

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

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

    whenDebug :: REPL () -> REPL ()
    whenDebug :: REPL () -> REPL ()
    whenDebug m :: REPL ()
    m = do
      Bool
    b <- FilePath -> REPL Bool
    forall a. IsEnvVal a => FilePath -> REPL a
    getKnownUser "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)
    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 -> FilePath -> FilePath
    [Smoke] -> FilePath -> FilePath
    Smoke -> FilePath
    (Int -> Smoke -> FilePath -> FilePath)
    -> (Smoke -> FilePath)
    -> ([Smoke] -> FilePath -> FilePath)
    -> Show Smoke
    forall a.
    (Int -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    showList :: [Smoke] -> FilePath -> FilePath
    $cshowList :: [Smoke] -> FilePath -> FilePath
    show :: Smoke -> FilePath
    $cshow :: Smoke -> FilePath
    showsPrec :: Int -> Smoke -> FilePath -> FilePath
    $cshowsPrec :: Int -> Smoke -> FilePath -> FilePath
    Show, Smoke -> Smoke -> Bool
    (Smoke -> Smoke -> Bool) -> (Smoke -> Smoke -> Bool) -> Eq Smoke
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Smoke -> Smoke -> Bool
    $c/= :: Smoke -> Smoke -> Bool
    == :: Smoke -> Smoke -> Bool
    $c== :: Smoke -> Smoke -> Bool
    Eq)

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

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