-- |
-- 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
  , try
  , 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(..), lName, getLoadedMod, setLoadedMod, clearLoadedMod
  , setEditPath, getEditPath, clearEditPath
  , setSearchPath, prependSearchPath
  , getPrompt
  , shouldContinue
  , unlessBatch
  , asBatch
  , validEvalContext
  , updateREPLTitle
  , isolated
  , setUpdateREPLTitle
  , withRandomGen
  , setRandomGen
  , getRandomGen
  , getModuleInput

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

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

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

  , RW(..)
  , defaultRW
  , mkUserEnv

  ) 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 qualified Data.ByteString as BS
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.Tuple (swap)
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 (ImpName Name)
lFocus :: Maybe (P.ImpName T.Name) -- ^ Working on this module.
  , LoadedModule -> ModulePath
lPath :: M.ModulePath -- ^ Working on this file.
  }

lName :: LoadedModule -> Maybe P.ModName
lName :: LoadedModule -> Maybe ModName
lName LoadedModule
lm = ImpName Name -> ModName
M.impNameTopModule (ImpName Name -> ModName) -> Maybe (ImpName Name) -> Maybe ModName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoadedModule -> Maybe (ImpName Name)
lFocus LoadedModule
lm

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

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

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

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

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

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

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

  , RW -> Bool
eCallStacks :: Bool

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

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

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

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

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

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


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

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

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

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

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



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance X.Exception REPLException

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

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


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

try :: REPL a -> REPL (Either REPLException a)
try :: forall a. REPL a -> REPL (Either REPLException a)
try REPL a
m = (IORef RW -> IO (Either REPLException a))
-> REPL (Either REPLException a)
forall a. (IORef RW -> IO a) -> REPL a
REPL (IO a -> IO (Either REPLException a)
forall e a. Exception e => IO a -> IO (Either e a)
X.try (IO a -> IO (Either REPLException a))
-> (IORef RW -> IO a) -> IORef RW -> IO (Either REPLException a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> IO a
forall a. IO a -> IO a
rethrowEvalError (IO a -> IO a) -> (IORef RW -> IO a) -> IORef RW -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPL a -> IORef RW -> IO a
forall a. REPL a -> IORef RW -> IO a
unREPL REPL a
m)

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


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

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

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

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


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


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

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

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

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

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

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

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


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

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

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

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

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

clearLoadedMod :: REPL ()
clearLoadedMod :: REPL ()
clearLoadedMod = do (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eLoadedMod = upd <$> eLoadedMod rw })
                    REPL ()
updateREPLTitle
  where upd :: LoadedModule -> LoadedModule
upd LoadedModule
x = LoadedModule
x { lFocus = 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 = Just n })
  REPL ()
updateREPLTitle

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



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

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

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

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

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

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

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

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

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

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

isolated :: REPL a -> REPL a
isolated :: forall a. REPL a -> REPL a
isolated REPL a
body = do
  RW
rw <- REPL RW
getRW
  REPL a
body REPL a -> REPL () -> REPL a
forall a b. REPL a -> REPL b -> REPL a
`finally` (RW -> RW) -> REPL ()
modifyRW_ (RW -> RW -> RW
forall a b. a -> b -> a
const RW
rw)

-- | Is evaluation enabled? If the currently focused module is parameterized,
-- then we cannot evaluate.
validEvalContext :: T.FreeVars a => a -> REPL ()
validEvalContext :: forall a. FreeVars a => a -> REPL ()
validEvalContext a
a =
  do ModuleEnv
me <- RW -> ModuleEnv
eModuleEnv (RW -> ModuleEnv) -> REPL RW -> REPL ModuleEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL RW
getRW
     let (Set TParam
badTs, Set Name
bad) = LoadedModules -> a -> (Set TParam, Set Name)
forall a.
FreeVars a =>
LoadedModules -> a -> (Set TParam, Set Name)
M.loadedParamModDeps (ModuleEnv -> LoadedModules
M.meLoadedModules ModuleEnv
me) a
a
     Bool -> REPL () -> REPL ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Name -> Bool
forall a. Set a -> Bool
Set.null Set Name
bad Bool -> Bool -> Bool
&& Set TParam -> Bool
forall a. Set a -> Bool
Set.null Set TParam
badTs) (REPL () -> REPL ()) -> REPL () -> REPL ()
forall a b. (a -> b) -> a -> b
$
       REPLException -> REPL ()
forall a. REPLException -> REPL a
raise ([TParam] -> [Name] -> REPLException
EvalInParamModule (Set TParam -> [TParam]
forall a. Set a -> [a]
Set.toList Set TParam
badTs) (Set Name -> [Name]
forall a. Set a -> [a]
Set.toList Set Name
bad))

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

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

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

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

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

setLogger :: Logger -> REPL ()
setLogger :: Logger -> REPL ()
setLogger Logger
logger = (RW -> RW) -> REPL ()
modifyRW_ ((RW -> RW) -> REPL ()) -> (RW -> RW) -> REPL ()
forall a b. (a -> b) -> a -> b
$ \RW
rw -> RW
rw { eLogger = logger }

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

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

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

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

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

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

-- | Return a list of property names, sorted by position in the file.
-- Only properties defined in the current module are returned, including
-- private properties in the current module. Imported properties are not
-- returned.
getPropertyNames :: REPL ([(M.Name, T.Decl)], NameDisp)
getPropertyNames :: REPL ([(Name, Decl)], NameDisp)
getPropertyNames =
 do ModContext
fe <- REPL ModContext
getFocusedEnv
    let nd :: NameDisp
nd = ModContext -> NameDisp
M.mctxNameDisp ModContext
fe
    Maybe ModName
mblm <- (Maybe LoadedModule -> Maybe ModName)
-> REPL (Maybe LoadedModule) -> REPL (Maybe ModName)
forall a b. (a -> b) -> REPL a -> REPL b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LoadedModule -> Maybe ModName
lName (LoadedModule -> Maybe ModName)
-> Maybe LoadedModule -> Maybe ModName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) REPL (Maybe LoadedModule)
getLoadedMod
    case Maybe ModName
mblm of
      Maybe ModName
Nothing -> ([(Name, Decl)], NameDisp) -> REPL ([(Name, Decl)], NameDisp)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], NameDisp
nd)
      Just ModName
mn ->
       do Maybe LoadedModule
mb <- ModName -> ModuleEnv -> Maybe LoadedModule
M.lookupModule ModName
mn (ModuleEnv -> Maybe LoadedModule)
-> REPL ModuleEnv -> REPL (Maybe LoadedModule)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPL ModuleEnv
getModuleEnv
          case Maybe LoadedModule
mb of
            Maybe LoadedModule
Nothing -> ([(Name, Decl)], NameDisp) -> REPL ([(Name, Decl)], NameDisp)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], NameDisp
nd)
            Just LoadedModule
lm -> ([(Name, Decl)], NameDisp) -> REPL ([(Name, Decl)], NameDisp)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Name, Decl)]
ps, NameDisp
nd)
              where
                ps :: [(Name, Decl)]
ps =
                  ((Name, Decl) -> (Name, Decl) -> Ordering)
-> [(Name, Decl)] -> [(Name, Decl)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Name, Decl) -> Position)
-> (Name, Decl) -> (Name, Decl) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Range -> Position
from (Range -> Position)
-> ((Name, Decl) -> Range) -> (Name, Decl) -> Position
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
M.nameLoc (Name -> Range) -> ((Name, Decl) -> Name) -> (Name, Decl) -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Decl) -> Name
forall a b. (a, b) -> a
fst))
                    [ (Decl -> Name
T.dName Decl
d,Decl
d)
                    | Decl
d <- DeclGroup -> [Decl]
T.groupDecls (DeclGroup -> [Decl]) -> [DeclGroup] -> [Decl]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleG ModName -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
T.mDecls (LoadedModuleData -> ModuleG ModName
M.lmdModule (LoadedModule -> LoadedModuleData
forall a. LoadedModuleG a -> a
M.lmData LoadedModule
lm))
                    , Pragma
T.PragmaProperty Pragma -> [Pragma] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Decl -> [Pragma]
T.dPragmas Decl
d
                    ]


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

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

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

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

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

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

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

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

getModuleInput :: REPL (M.ModuleInput IO)
getModuleInput :: REPL (ModuleInput IO)
getModuleInput = do
  IO EvalOpts
evo <- REPL (IO EvalOpts)
getEvalOptsAction
  ModuleEnv
env <- REPL ModuleEnv
getModuleEnv
  Bool
callStacks <- REPL Bool
getCallStacks
  Solver
tcSolver <- REPL Solver
getTCSolver
  ModuleInput IO -> REPL (ModuleInput IO)
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure M.ModuleInput
    { minpCallStacks :: Bool
minpCallStacks = Bool
callStacks
    , minpEvalOpts :: IO EvalOpts
minpEvalOpts   = IO EvalOpts
evo
    , minpByteReader :: [Char] -> IO ByteString
minpByteReader = [Char] -> IO ByteString
BS.readFile
    , minpModuleEnv :: ModuleEnv
minpModuleEnv  = ModuleEnv
env
    , minpTCSolver :: Solver
minpTCSolver   = Solver
tcSolver
    }

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

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

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


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

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


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


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

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

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

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

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

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

-- | Set a user option.
-- Returns 'True' on success
setUser :: String -> String -> REPL Bool
setUser :: [Char] -> [Char] -> REPL Bool
setUser [Char]
name [Char]
val = case [Char] -> OptionMap -> [OptionDescr]
forall a. [Char] -> Trie a -> [a]
lookupTrieExact [Char]
name OptionMap
userOptionsWithAliases of

  [OptionDescr
opt] -> OptionDescr -> REPL Bool
setUserOpt OptionDescr
opt
  []    -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Unknown env value `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"`")
  [OptionDescr]
_     -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Ambiguous env value `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"`")

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

    EnvProg [Char]
_ [[Char]]
_ ->
      case [Char] -> [[Char]]
splitOptArgs [Char]
val of
        [Char]
prog:[[Char]]
args -> EnvVal -> REPL Bool
doCheck ([Char] -> [[Char]] -> EnvVal
EnvProg [Char]
prog [[Char]]
args)
        [] -> Bool
False Bool -> REPL () -> REPL Bool
forall a b. a -> REPL b -> REPL a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> REPL ()
rPutStrLn ([Char]
"Failed to parse command for field, `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"`")

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

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

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

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

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

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

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


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

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

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

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

class IsEnvVal a where
  fromEnvVal :: EnvVal -> a

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

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

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

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

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

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


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

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

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

type OptionMap = Trie OptionDescr

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

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

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

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

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

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

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

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

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

  , [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"tcSmtFile" [[Char]
"tc-smt-file"] ([Char] -> EnvVal
EnvString [Char]
"-") Checker
noCheck
    ([[Char]] -> [Char]
unlines
      [ [Char]
"The file to record SMT solver interactions in the type checker (for debugging or offline proving)."
      , [Char]
"Use \"-\" for stdout." ]) ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    \case EnvString [Char]
fileName -> do let mfile :: Maybe [Char]
mfile = if [Char]
fileName [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"-" then Maybe [Char]
forall a. Maybe a
Nothing else [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
fileName
                                   (RW -> RW) -> REPL ()
modifyRW_ (\RW
rw -> RW
rw { eTCConfig = (eTCConfig rw)
                                                                       { T.solverSmtFile = mfile
                                                                       }})
                                   REPL ()
resetTCSolver
          EnvVal
_                  -> () -> REPL ()
forall a. a -> REPL a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

  , [Char]
-> [[Char]]
-> EnvVal
-> Checker
-> [Char]
-> (EnvVal -> REPL ())
-> OptionDescr
OptionDescr [Char]
"evalForeign" [[Char]
"eval-foreign"] EnvVal
defaultEvalForeignOpt
    Checker
checkEvalForeign
    ([[Char]] -> [Char]
unlines
      [ [Char]
"How to evaluate 'foreign' bindings:"
      , [Char]
"  * always  Always call the foreign implementation with the FFI and"
      , [Char]
"            report an error on module load if it is unavailable."
      , [Char]
"  * prefer  Call the foreign implementation with the FFI by default,"
      , [Char]
"            and when unavailable, fall back to the cryptol"
      , [Char]
"            implementation if present and report runtime error"
      , [Char]
"            otherwise."
      , [Char]
"  * never   Never use the FFI. Always call the cryptol implementation"
      , [Char]
"            if present, and report runtime error otherwise."
      , [Char]
"Note: changes take effect on module reload."
      ]) ((EnvVal -> REPL ()) -> OptionDescr)
-> (EnvVal -> REPL ()) -> OptionDescr
forall a b. (a -> b) -> a -> b
$
    \case EnvString [Char]
s
            | Just EvalForeignPolicy
p <- [Char] -> [([Char], EvalForeignPolicy)] -> Maybe EvalForeignPolicy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
s [([Char], EvalForeignPolicy)]
evalForeignOptMap -> do
              ModuleEnv
me <- REPL ModuleEnv
getModuleEnv
              ModuleEnv -> REPL ()
setModuleEnv ModuleEnv
me { M.meEvalForeignPolicy = p }
          EnvVal
_ -> () -> REPL ()
forall a. a -> REPL a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  , [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]
"proverTimeout" [[Char]
"prover-timeout"] (Int -> EnvVal
EnvNum Int
0) Checker
checkTimeout
    [Char]
"Specify timeout in seconds for online prover processes."

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

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

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

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

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

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

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

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


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

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

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

checkTimeout :: Checker
checkTimeout :: Checker
checkTimeout EnvVal
val =
  case EnvVal
val of
    EnvNum Int
n
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"timeout should be non-negative")
      | Bool
otherwise -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns Maybe [Char]
forall a. Maybe a
Nothing
    EnvVal
_ -> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
"Failed to parse `prover-timeout`")

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

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

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

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

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

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

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

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

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

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

checkEvalForeign :: Checker
checkEvalForeign :: Checker
checkEvalForeign (EnvString [Char]
s)
  | Just EvalForeignPolicy
_ <- [Char] -> [([Char], EvalForeignPolicy)] -> Maybe EvalForeignPolicy
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Char]
s [([Char], EvalForeignPolicy)]
evalForeignOptMap = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns Maybe [Char]
forall a. Maybe a
Nothing
checkEvalForeign EnvVal
_ = Maybe [Char] -> REPL (Maybe [Char], [[Char]])
noWarns (Maybe [Char] -> REPL (Maybe [Char], [[Char]]))
-> Maybe [Char] -> REPL (Maybe [Char], [[Char]])
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"evalForeign must be one of: "
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ((([Char], EvalForeignPolicy) -> [Char])
-> [([Char], EvalForeignPolicy)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], EvalForeignPolicy) -> [Char]
forall a b. (a, b) -> a
fst [([Char], EvalForeignPolicy)]
evalForeignOptMap)

evalForeignOptMap :: [(String, M.EvalForeignPolicy)]
evalForeignOptMap :: [([Char], EvalForeignPolicy)]
evalForeignOptMap =
  [ ([Char]
"always", EvalForeignPolicy
M.AlwaysEvalForeign)
  , ([Char]
"prefer", EvalForeignPolicy
M.PreferEvalForeign)
  , ([Char]
"never", EvalForeignPolicy
M.NeverEvalForeign)
  ]

defaultEvalForeignOpt :: EnvVal
defaultEvalForeignOpt :: EnvVal
defaultEvalForeignOpt =
  case EvalForeignPolicy -> [(EvalForeignPolicy, [Char])] -> Maybe [Char]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup EvalForeignPolicy
M.defaultEvalForeignPolicy ((([Char], EvalForeignPolicy) -> (EvalForeignPolicy, [Char]))
-> [([Char], EvalForeignPolicy)] -> [(EvalForeignPolicy, [Char])]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], EvalForeignPolicy) -> (EvalForeignPolicy, [Char])
forall a b. (a, b) -> (b, a)
swap [([Char], EvalForeignPolicy)]
evalForeignOptMap) of
    Just [Char]
s -> [Char] -> EnvVal
EnvString [Char]
s
    Maybe [Char]
Nothing -> [Char] -> [[Char]] -> EnvVal
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"defaultEvalForeignOpt"
      [[Char]
"cannot find option value matching default EvalForeignPolicy"]

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

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

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

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

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

type SmokeTest = REPL (Maybe Smoke)

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

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

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