-- |
-- 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
  , whenDebug
  , getExprNames
  , getTypeNames
  , getPropertyNames
  , getModNames
  , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
  , setEditPath, getEditPath, clearEditPath
  , setSearchPath, prependSearchPath
  , getPrompt
  , shouldContinue
  , unlessBatch
  , asBatch
  , validEvalContext
  , updateREPLTitle
  , setUpdateREPLTitle

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

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

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

  ) where

import Cryptol.REPL.Trie

import Cryptol.Eval (EvalError, Unsupported)
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 (SatNum(..))
import Cryptol.Symbolic.SBV (SBVPortfolioException)
import Cryptol.Symbolic.What4 (W4Exception)
import Cryptol.Backend.Monad(PPFloatFormat(..),PPFloatExp(..))
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,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 (SBVException)

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

-- | Initial, empty environment.
defaultRW :: Bool -> Logger -> IO RW
defaultRW :: Bool -> Logger -> IO RW
defaultRW Bool
isBatch 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
-> REPL ()
-> Either SBVProverConfig W4ProverConfig
-> 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
    , eUpdateTitle :: REPL ()
eUpdateTitle = () -> REPL ()
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
    }

-- | Build up the prompt for the REPL.
mkPrompt :: RW -> String
mkPrompt :: RW -> FilePath
mkPrompt RW
rw
  | RW -> Bool
eIsBatch RW
rw = FilePath
""
  | Bool
detailedPrompt = FilePath
withEdit FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"> "
  | Bool
otherwise      = FilePath
modLn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"> "
  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
      Maybe ModName
Nothing -> Doc -> FilePath
forall a. Show a => a -> FilePath
show (ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
I.preludeName)
      Just 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]
++ FilePath
"(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
      Maybe LoadedModule
Nothing -> FilePath
modLn
      Just LoadedModule
m ->
        case (LoadedModule -> Maybe ModName
lName LoadedModule
m, LoadedModule -> ModulePath
lPath LoadedModule
m) of
          (Maybe ModName
Nothing, M.InFile FilePath
f) -> FilePath
":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]
++ FilePath
"\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
modLn
          (Maybe ModName, ModulePath)
_ -> FilePath
modLn

  withEdit :: FilePath
withEdit =
    case RW -> Maybe FilePath
eEditFile RW
rw of
      Maybe FilePath
Nothing -> FilePath
withFocus
      Just FilePath
e
        | Just (M.InFile 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 -> FilePath
":e to edit " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
e FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\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 Bool
isBatch Logger
l 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 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 (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 a
x = (IORef RW -> IO a) -> REPL a
forall a. (IORef RW -> IO a) -> REPL a
REPL (\IORef RW
_ -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x)

  {-# INLINE (>>=) #-}
  REPL a
m >>= :: 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 :: 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 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 :: StM REPL a -> REPL a
restoreM 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 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
Maybe FilePath
Maybe LoadedModule
Either SBVProverConfig W4ProverConfig
UserEnv
Logger
ModuleEnv
REPL ()
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eLogger :: Logger
eUserEnv :: UserEnv
eModuleEnv :: ModuleEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe FilePath
eLoadedMod :: Maybe LoadedModule
eProverConfig :: RW -> Either SBVProverConfig W4ProverConfig
eUpdateTitle :: RW -> REPL ()
eLogger :: RW -> Logger
eUserEnv :: RW -> UserEnv
eModuleEnv :: RW -> ModuleEnv
eIsBatch :: RW -> Bool
eContinue :: RW -> Bool
eEditFile :: RW -> Maybe FilePath
eLoadedMod :: RW -> Maybe LoadedModule
.. } ->
    let (a
a,Supply
s') = Supply -> (a, Supply)
f (ModuleEnv -> Supply
M.meSupply ModuleEnv
eModuleEnv)
     in (RW :: Maybe LoadedModule
-> Maybe FilePath
-> Bool
-> Bool
-> ModuleEnv
-> UserEnv
-> Logger
-> REPL ()
-> Either SBVProverConfig W4ProverConfig
-> RW
RW { eModuleEnv :: ModuleEnv
eModuleEnv = ModuleEnv
eModuleEnv { meSupply :: Supply
M.meSupply = Supply
s' }, Bool
Maybe FilePath
Maybe LoadedModule
Either SBVProverConfig W4ProverConfig
UserEnv
Logger
REPL ()
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eLogger :: Logger
eUserEnv :: UserEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe FilePath
eLoadedMod :: Maybe LoadedModule
eProverConfig :: Either SBVProverConfig W4ProverConfig
eUpdateTitle :: REPL ()
eLogger :: Logger
eUserEnv :: UserEnv
eIsBatch :: Bool
eContinue :: Bool
eEditFile :: Maybe FilePath
eLoadedMod :: Maybe LoadedModule
.. },a
a)

instance Ex.MonadThrow REPL where
  throwM :: e -> REPL a
throwM e
e = 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 :: 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 (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
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 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 (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 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 (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 :: 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 (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 (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 (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 (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 (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 EvalError
  | Unsupported Unsupported
  | ModuleSystemError NameDisp M.ModuleError
  | EvalPolyError T.Schema
  | TypeNotTestable T.Type
  | EvalInParamModule [M.Name]
  | SBVError String
  | SBVException SBVException
  | SBVPortfolioException SBVPortfolioException
  | W4Exception W4Exception
    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 Int
_ REPLException
re = case REPLException
re of
    ParseError ParseError
e         -> ParseError -> Doc
ppError ParseError
e
    FileNotFound FilePath
path    -> [Doc] -> Doc
sep [ FilePath -> Doc
text FilePath
"File"
                                , FilePath -> Doc
text (FilePath
"`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'")
                                , FilePath -> Doc
textFilePath
"not found"
                                ]
    DirectoryNotFound FilePath
path -> [Doc] -> Doc
sep [ FilePath -> Doc
text FilePath
"Directory"
                                  , FilePath -> Doc
text (FilePath
"`" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
path FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"'")
                                  , FilePath -> Doc
textFilePath
"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 EvalError
e          -> EvalError -> Doc
forall a. PP a => a -> Doc
pp EvalError
e
    Unsupported Unsupported
e        -> Unsupported -> Doc
forall a. PP a => a -> Doc
pp Unsupported
e
    EvalPolyError Schema
s      -> FilePath -> Doc
text FilePath
"Cannot evaluate polymorphic value."
                         Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
"Type:" Doc -> Doc -> Doc
<+> Schema -> Doc
forall a. PP a => a -> Doc
pp Schema
s
    TypeNotTestable Type
t    -> FilePath -> Doc
text FilePath
"The expression is not of a testable type."
                         Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
"Type:" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PP a => a -> Doc
pp Type
t
    EvalInParamModule [Name]
xs ->
      FilePath -> Doc
text FilePath
"Expression depends on definitions from a parameterized module:"
        Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
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 FilePath
s           -> FilePath -> Doc
text FilePath
"SBV error:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
s
    SBVException SBVException
e       -> FilePath -> Doc
text FilePath
"SBV exception:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text (SBVException -> FilePath
forall a. Show a => a -> FilePath
show SBVException
e)
    SBVPortfolioException SBVPortfolioException
e -> FilePath -> Doc
text FilePath
"SBV exception:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text (SBVPortfolioException -> FilePath
forall a. Show a => a -> FilePath
show SBVPortfolioException
e)
    W4Exception W4Exception
e        -> FilePath -> Doc
text FilePath
"What4 exception:" Doc -> Doc -> Doc
$$ FilePath -> Doc
text (W4Exception -> FilePath
forall a. Show a => a -> FilePath
show W4Exception
e)

-- | Raise an exception.
raise :: REPLException -> REPL a
raise :: 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 :: 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 :: 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 :: IO a -> IO a
rethrowEvalError 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 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 (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 EvalError
exn = REPLException -> IO a
forall e a. Exception e => e -> IO a
X.throwIO (EvalError -> REPLException
EvalError EvalError
exn)

  rethrowUnsupported :: Unsupported -> IO a
  rethrowUnsupported :: 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 :: 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 :: (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. 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 { 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 (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 FilePath
p = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \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 { eEditFile :: Maybe FilePath
eEditFile = Maybe FilePath
forall a. Maybe a
Nothing }

setSearchPath :: [FilePath] -> REPL ()
setSearchPath :: [FilePath] -> REPL ()
setSearchPath [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 [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 }

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 (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 :: REPL a -> REPL a
asBatch 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 { 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 (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 :: 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 (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 Name
nm Set Name
bs =
           case Name -> NameInfo
M.nameInfo Name
nm of
             M.Declared ModName
m NameSource
_
               | 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
             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) (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 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 :: (FilePath -> IO ()) -> REPL ()
setPutStr FilePath -> 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 = (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 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 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]
++ FilePath
"\n"

-- | Use the configured output action to print something using its Show instance
rPrint :: Show a => a -> REPL ()
rPrint :: a -> REPL ()
rPrint a
x = FilePath -> REPL ()
rPutStrLn (a -> FilePath
forall a. Show a => a -> FilePath
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 [FilePath]
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
     [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.
-- This is used for command line completition.
getTypeNames :: REPL [String]
getTypeNames :: REPL [FilePath]
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
     [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 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]
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
x | (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 (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, ModContext -> NameDisp
M.mctxNameDisp ModContext
fe)

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 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 (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 })


-- | 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.Declared ModName
ns 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))

    NameInfo
M.Parameter ->
      FilePath -> [FilePath] -> REPL Name
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"[REPL] uniqify" [FilePath
"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 Ident
i 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 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 FilePath
name FilePath
val = case FilePath -> OptionMap -> [OptionDescr]
forall a. FilePath -> Trie a -> [a]
lookupTrieExact FilePath
name OptionMap
userOptions of

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

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

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

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

    EnvBool Bool
_
      | (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) [FilePath
"enable", FilePath
"on", FilePath
"yes", FilePath
"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) [FilePath
"disable", FilePath
"off", FilePath
"no", FilePath
"false"] ->
        EnvVal -> REPL ()
writeEnv (Bool -> EnvVal
EnvBool Bool
False)
      | Bool
otherwise ->
        FilePath -> REPL ()
rPutStrLn (FilePath
"Failed to parse boolean for field, `" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
name FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"`")
    where
    doCheck :: EnvVal -> REPL ()
doCheck EnvVal
v = do (Maybe FilePath
r,[FilePath]
ws) <- OptionDescr -> Checker
optCheck OptionDescr
opt EnvVal
v
                   case Maybe FilePath
r of
                     Just FilePath
err -> FilePath -> REPL ()
rPutStrLn FilePath
err
                     Maybe FilePath
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 EnvVal
ev =
      do OptionDescr -> EnvVal -> REPL ()
optEff OptionDescr
opt EnvVal
ev
         (RW -> RW) -> REPL ()
modifyRW_ (\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 FilePath
"")
  where

  parse :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
parse FilePath
acc (Char
c: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 FilePath
acc []                       = FilePath -> FilePath -> Maybe (FilePath, FilePath)
result FilePath
acc []

  quoted :: FilePath -> FilePath -> Maybe (FilePath, FilePath)
quoted FilePath
acc (Char
c: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 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 []  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 FilePath
acc 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 Char
c = Char
c Char -> FilePath -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (FilePath
"'\"" :: String)


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

getKnownUser :: IsEnvVal a => String -> REPL a
getKnownUser :: FilePath -> REPL a
getKnownUser 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 EnvVal
x = case EnvVal
x of
                   EnvBool Bool
b -> Bool
b
                   EnvVal
_         -> FilePath -> Bool
forall a. FilePath -> a
badIsEnv FilePath
"Bool"

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

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

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

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


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

getUserProverValidate :: REPL Bool
getUserProverValidate :: REPL Bool
getUserProverValidate = FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser FilePath
"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 OptionMap
m 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 -> REPL (Maybe String, [String])

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

noWarns :: Maybe String -> REPL (Maybe String, [String])
noWarns :: Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
mb = (Maybe FilePath, [FilePath]) -> REPL (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 FilePath
optName EnvVal
optDefault Checker
optCheck FilePath
optHelp =
  OptionDescr :: FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr { optEff :: EnvVal -> REPL ()
optEff = \ EnvVal
_ -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return (), FilePath
EnvVal
Checker
optHelp :: FilePath
optCheck :: Checker
optDefault :: EnvVal
optName :: FilePath
optHelp :: FilePath
optCheck :: Checker
optDefault :: EnvVal
optName :: FilePath
.. }

userOptions :: OptionMap
userOptions :: OptionMap
userOptions  = [OptionDescr] -> OptionMap
mkOptionMap
  [ FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"base" (Int -> EnvVal
EnvNum Int
16) Checker
checkBase
    FilePath
"The base to display words at (2, 8, 10, or 16)."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"debug" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    FilePath
"Enable debugging output."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"ascii" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    FilePath
"Whether to display 7- or 8-bit words using ASCII notation."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"infLength" (Int -> EnvVal
EnvNum Int
5) Checker
checkInfLength
    FilePath
"The number of elements to display for infinite sequences."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"tests" (Int -> EnvVal
EnvNum Int
100) Checker
noCheck
    FilePath
"The number of random tests to try with ':check'."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"satNum" (FilePath -> EnvVal
EnvString FilePath
"1") Checker
checkSatNum
    FilePath
"The maximum number of :sat solutions to display (\"all\" for no limit)."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"prover" (FilePath -> EnvVal
EnvString FilePath
"z3") Checker
checkProver (FilePath -> OptionDescr) -> FilePath -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    FilePath
"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
")."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"warnDefaulting" (Bool -> EnvVal
EnvBool Bool
False) Checker
noCheck
    FilePath
"Choose whether to display warnings when defaulting."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"warnShadowing" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    FilePath
"Choose whether to display warnings when shadowing symbols."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"warnUninterp" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    FilePath
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
  , FilePath -> EnvVal -> Checker -> FilePath -> OptionDescr
simpleOpt FilePath
"smtfile" (FilePath -> EnvVal
EnvString FilePath
"-") Checker
noCheck
    FilePath
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr FilePath
"mono-binds" (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    FilePath
"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 (m :: * -> *) a. Monad m => a -> m a
return ()

  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr FilePath
"tc-solver" (FilePath -> [FilePath] -> EnvVal
EnvProg FilePath
"z3" [ FilePath
"-smt2", FilePath
"-in" ])
    Checker
noCheck  -- TODO: check for the program in the path
    FilePath
"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 FilePath
prog [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 } }
          EnvVal
_                 -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr FilePath
"tc-debug" (Int -> EnvVal
EnvNum Int
0)
    Checker
noCheck
    ([FilePath] -> FilePath
unlines
      [ FilePath
"Enable type-checker debugging output:"
      , FilePath
"  *  0  no debug output"
      , FilePath
"  *  1  show type-checker debug info"
      , FilePath
"  * >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 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 } }
          EnvVal
_        -> () -> REPL ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , FilePath
-> EnvVal
-> Checker
-> FilePath
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr FilePath
"core-lint" (Bool -> EnvVal
EnvBool Bool
False)
    Checker
noCheck
    FilePath
"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 (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

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

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

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


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

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



-- | 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
2,Int
8,Int
10,Int
16] -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
    | Bool
otherwise            -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"base must be 2, 8, 10, or 16"
  EnvVal
_                     -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"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 FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
    | Bool
otherwise -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"the number of elements should be positive"
  EnvVal
_ -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"unable to parse a value for infLength"

checkProver :: Checker
checkProver :: Checker
checkProver EnvVal
val = case EnvVal
val of
  EnvString ((Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower -> FilePath
s)
    | FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
W4.proverNames ->
      IO (Either FilePath ([FilePath], W4ProverConfig))
-> REPL (Either FilePath ([FilePath], W4ProverConfig))
forall a. IO a -> REPL a
io (FilePath -> IO (Either FilePath ([FilePath], W4ProverConfig))
W4.setupProver FilePath
s) REPL (Either FilePath ([FilePath], W4ProverConfig))
-> (Either FilePath ([FilePath], W4ProverConfig)
    -> REPL (Maybe FilePath, [FilePath]))
-> REPL (Maybe FilePath, [FilePath])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left FilePath
msg -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
msg)
        Right ([FilePath]
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 FilePath, [FilePath]) -> REPL (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [FilePath]
ws)
    | FilePath
s FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
SBV.proverNames ->
      IO (Either FilePath ([FilePath], SBVProverConfig))
-> REPL (Either FilePath ([FilePath], SBVProverConfig))
forall a. IO a -> REPL a
io (FilePath -> IO (Either FilePath ([FilePath], SBVProverConfig))
SBV.setupProver FilePath
s) REPL (Either FilePath ([FilePath], SBVProverConfig))
-> (Either FilePath ([FilePath], SBVProverConfig)
    -> REPL (Maybe FilePath, [FilePath]))
-> REPL (Maybe FilePath, [FilePath])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left FilePath
msg -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
msg)
        Right ([FilePath]
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 FilePath, [FilePath]) -> REPL (Maybe FilePath, [FilePath])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath
forall a. Maybe a
Nothing, [FilePath]
ws)

    | Bool
otherwise ->
      Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (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
$ FilePath
"Prover must be " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
proverListString

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

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

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] -> [FilePath]
forall a. [a] -> [a]
init [FilePath]
allProvers) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"or " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. [a] -> a
last [FilePath]
allProvers

checkSatNum :: Checker
checkSatNum :: Checker
checkSatNum EnvVal
val = case EnvVal
val of
  EnvString FilePath
"all" -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
  EnvString FilePath
s ->
    case FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s :: Maybe Int of
      Just Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns Maybe FilePath
forall a. Maybe a
Nothing
      Maybe Int
_               -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"must be an integer > 0 or \"all\""
  EnvVal
_ -> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
noWarns (Maybe FilePath -> REPL (Maybe FilePath, [FilePath]))
-> Maybe FilePath -> REPL (Maybe FilePath, [FilePath])
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
"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 FilePath
"satNum"
  case FilePath
s of
    FilePath
"all"                     -> SatNum -> REPL SatNum
forall (m :: * -> *) a. Monad m => a -> m a
return SatNum
AllSat
    FilePath
_ | Just 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 -> [FilePath] -> REPL SatNum
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"REPL.Monad.getUserSatNum"
                                   [ FilePath
"invalid satNum option" ]

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

whenDebug :: REPL () -> REPL ()
whenDebug :: REPL () -> REPL ()
whenDebug REPL ()
m = do
  Bool
b <- FilePath -> REPL Bool
forall a. IsEnvVal a => FilePath -> REPL a
getKnownUser FilePath
"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 Int
_ Smoke
smoke =
    case Smoke
smoke of
      Smoke
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
" " ([FilePath] -> Doc) -> [FilePath] -> Doc
forall a b. (a -> b) -> a -> b
$ [
          FilePath
"[error] z3 is required to run Cryptol, but was not found in the"
        , FilePath
"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 FilePath
"z3"
  case Maybe FilePath
mPath of
    Maybe FilePath
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 FilePath
_  -> Maybe Smoke -> REPL (Maybe Smoke)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Smoke
forall a. Maybe a
Nothing