{-|
Module      : Effects
Description : Domain specific effects

This module contains custom app specific mtl style effects for hevm
These are written in the style of the ReaderT over IO pattern [1].
Right now we only have a single `ReadConfig` effect, but over time hope to
migrate most usages of IO into custom effects here.

This framework would allow us to have multiple interpretations for effects
(e.g. a pure version for tests), but for now we interpret everything in IO
only.

[1]: https://www.fpcomplete.com/blog/readert-design-pattern/
-}

module EVM.Effects where

import Control.Monad.Reader
import Control.Monad.IO.Unlift
import Data.Text (Text)
import Data.Text.IO qualified as T
import System.IO (stderr)


-- Abstract Effects --------------------------------------------------------------------------------
-- Here we define the abstract interface for the effects that we wish to model


-- Read from global config
class Monad m => ReadConfig m where
  readConfig ::  m Config

data Config = Config
  { Config -> Bool
dumpQueries      :: Bool
  , Config -> Bool
dumpExprs        :: Bool
  , Config -> Bool
dumpEndStates    :: Bool
  , Config -> Bool
debug            :: Bool
  , Config -> Bool
dumpTrace        :: Bool
  , Config -> Integer
numCexFuzz       :: Integer
   -- Used to debug fuzzer in test.hs. It disables the SMT solver
   -- and uses the fuzzer ONLY to try to find a counterexample.
   -- Returns Unknown if the Cex cannot be found via fuzzing
  , Config -> Bool
onlyCexFuzz      :: Bool
  , Config -> Bool
decomposeStorage :: Bool
  }
  deriving (Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Config -> ShowS
showsPrec :: Int -> Config -> ShowS
$cshow :: Config -> String
show :: Config -> String
$cshowList :: [Config] -> ShowS
showList :: [Config] -> ShowS
Show, Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
/= :: Config -> Config -> Bool
Eq)

defaultConfig :: Config
defaultConfig :: Config
defaultConfig = Config
  { $sel:dumpQueries:Config :: Bool
dumpQueries = Bool
False
  , $sel:dumpExprs:Config :: Bool
dumpExprs = Bool
False
  , $sel:dumpEndStates:Config :: Bool
dumpEndStates = Bool
False
  , $sel:debug:Config :: Bool
debug = Bool
False
  , $sel:dumpTrace:Config :: Bool
dumpTrace = Bool
False
  , $sel:numCexFuzz:Config :: Integer
numCexFuzz = Integer
10
  , $sel:onlyCexFuzz:Config :: Bool
onlyCexFuzz  = Bool
False
  , $sel:decomposeStorage:Config :: Bool
decomposeStorage = Bool
True
  }

-- Write to the console
class Monad m => TTY m where
  writeOutput :: Text -> m ()
  writeErr :: Text -> m ()

-- IO Interpretation -------------------------------------------------------------------------------


newtype Env = Env
  { Env -> Config
config :: Config
  }

defaultEnv :: Env
defaultEnv :: Env
defaultEnv = Env { $sel:config:Env :: Config
config = Config
defaultConfig }

instance Monad m => ReadConfig (ReaderT Env m) where
  readConfig :: ReaderT Env m Config
readConfig = do
    Env
e <- ReaderT Env m Env
forall r (m :: * -> *). MonadReader r m => m r
ask
    Config -> ReaderT Env m Config
forall a. a -> ReaderT Env m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
e.config

instance (Monad m, MonadIO m) => TTY (ReaderT Env m) where
  writeOutput :: Text -> ReaderT Env m ()
writeOutput Text
txt = IO () -> ReaderT Env m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env m ()) -> IO () -> ReaderT Env m ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn Text
txt
  writeErr :: Text -> ReaderT Env m ()
writeErr Text
txt = IO () -> ReaderT Env m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env m ()) -> IO () -> ReaderT Env m ()
forall a b. (a -> b) -> a -> b
$ Handle -> Text -> IO ()
T.hPutStr Handle
stderr Text
txt

runEnv :: Env -> ReaderT Env m a -> m a
runEnv :: forall (m :: * -> *) a. Env -> ReaderT Env m a -> m a
runEnv Env
e ReaderT Env m a
a = ReaderT Env m a -> Env -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Env m a
a Env
e


-- Helpful Aliases ---------------------------------------------------------------------------------


type App m = (MonadUnliftIO m, ReadConfig m, TTY m)

runApp :: ReaderT Env m a -> m a
runApp :: forall (m :: * -> *) a. ReaderT Env m a -> m a
runApp = Env -> ReaderT Env m a -> m a
forall (m :: * -> *) a. Env -> ReaderT Env m a -> m a
runEnv Env
defaultEnv