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

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

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

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

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

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

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

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

  ) where

import Cryptol.REPL.Trie

import Cryptol.Eval (EvalErrorEx, Unsupported, WordTooWide,EvalOpts(..))
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import Cryptol.Parser (ParseError,ppError)
import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
import Cryptol.Parser.NoPat (Error)
import Cryptol.Parser.Position (emptyRange, Range(from))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
import qualified Cryptol.IR.FreeVars as T
import qualified Cryptol.Utils.Ident as I
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
import qualified Cryptol.Parser.AST as P
import Cryptol.Symbolic (SatNum(..))
import Cryptol.Symbolic.SBV (SBVPortfolioException)
import Cryptol.Symbolic.What4 (W4Exception)
import qualified Cryptol.Symbolic.SBV as SBV (proverNames, setupProver, defaultProver, SBVProverConfig)
import qualified Cryptol.Symbolic.What4 as W4 (proverNames, setupProver, W4ProverConfig)



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

import Data.SBV (SBVException)
import qualified System.Random.TF as TF

import Prelude ()
import Prelude.Compat

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

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

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

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

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

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

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

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

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

  , RW -> Bool
eCallStacks :: Bool

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

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

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

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

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

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


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

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

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

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

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



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance X.Exception REPLException

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

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


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

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


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

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

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

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


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


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

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

modifyRW :: (RW -> (RW,a)) -> REPL a
modifyRW :: forall a. (RW -> (RW, a)) -> REPL a
modifyRW RW -> (RW, a)
f = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> 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 = forall a. (IORef RW -> IO a) -> REPL a
REPL (\ IORef RW
ref -> forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef RW
ref (\RW
x -> (RW -> RW
f RW
x, ())))

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

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

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


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

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

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

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

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

clearLoadedMod :: REPL ()
clearLoadedMod :: REPL ()
clearLoadedMod = do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eLoadedMod :: Maybe LoadedModule
eLoadedMod = LoadedModule -> LoadedModule
upd 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 = 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 = forall a. a -> Maybe a
Just LoadedModule
n })
  REPL ()
updateREPLTitle

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



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

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

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

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

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

getProverConfig :: REPL (Either SBV.SBVProverConfig W4.W4ProverConfig)
getProverConfig :: REPL (Either SBVProverConfig W4ProverConfig)
getProverConfig = RW -> Either SBVProverConfig W4ProverConfig
eProverConfig 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 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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (RW -> Bool
eIsBatch RW
rw) REPL ()
body

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

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

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

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

             NameInfo
_ -> Set Name
bs

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

getModuleEnv :: REPL M.ModuleEnv
getModuleEnv :: REPL ModuleEnv
getModuleEnv  = RW -> ModuleEnv
eModuleEnv 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. RW -> ModuleEnv
eModuleEnv) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` REPL RW
getRW

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

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

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

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

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

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

    M.LocalName {} ->
      forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"[REPL] uniqify" [[Char]
"tried to uniqify a parameter: " forall a. [a] -> [a] -> [a]
++ forall a. PP a => a -> [Char]
pretty Name
name]


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

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


-- | Generate a fresh name using the given index. The name will reside within
-- the "<interactive>" namespace.
freshName :: I.Ident -> M.NameSource -> REPL M.Name
freshName :: Ident -> NameSource -> REPL Name
freshName Ident
i NameSource
sys =
  forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
M.liftSupply (Namespace
-> ModPath
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
M.mkDeclared Namespace
I.NSValue ModPath
mpath NameSource
sys Ident
i forall a. Maybe a
Nothing Range
emptyRange)
  where mpath :: ModPath
mpath = ModName -> ModPath
M.TopModule ModName
I.interactiveName


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

class IsEnvVal a where
  fromEnvVal :: EnvVal -> a

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

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

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

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

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

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


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

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

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

type OptionMap = Trie OptionDescr

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

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

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

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

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

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

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

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

  , [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"monoBinds" [[Char]
"mono-binds"] (Bool -> EnvVal
EnvBool Bool
True) Checker
noCheck
    [Char]
"Whether or not to generalize bindings in a 'where' clause." 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
_         -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type SmokeTest = REPL (Maybe Smoke)

data Smoke
  = Z3NotFound
  deriving (Int -> Smoke -> ShowS
[Smoke] -> ShowS
Smoke -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Smoke] -> ShowS
$cshowList :: [Smoke] -> ShowS
show :: Smoke -> [Char]
$cshow :: Smoke -> [Char]
showsPrec :: Int -> Smoke -> ShowS
$cshowsPrec :: Int -> Smoke -> ShowS
Show, Smoke -> Smoke -> Bool
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 -> [Char] -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" " forall a b. (a -> b) -> a -> b
$ [
          [Char]
"[error] z3 is required to run Cryptol, but was not found in the"
        , [Char]
"system path. See the Cryptol README for more on how to install z3."
        ]

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