{-# Language GADTs #-}
{-# Language DataKinds #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , evmIO
  , entering
  , enter
  , interpret
  )
where

-- This module is an abstract definition of EVM steppers.
-- Steppers can be run as TTY debuggers or as CLI test runners.
--
-- The implementation uses the operational monad pattern
-- as the framework for monadic interpretation.
--
-- Note: this is a sketch of a work in progress!

import Prelude hiding (fail)

import Control.Monad.Operational (Program, singleton, view, ProgramViewT(..), ProgramView)
import Control.Monad.State.Strict (runState, liftIO, StateT)
import qualified Control.Monad.State.Class as State
import qualified EVM.Exec
import Data.Text (Text)
import EVM.Types (Buffer)

import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose)
import qualified EVM

import qualified EVM.Fetch as Fetch

-- | The instruction type of the operational monad
data Action a where

  -- | Keep executing until an intermediate result is reached
  Exec ::           Action VMResult

  -- | Keep executing until an intermediate state is reached
  Run ::             Action VM

  -- | Wait for a query to be resolved
  Wait :: Query   -> Action ()

  -- | Multiple things can happen
  Ask :: Choose -> Action ()

  -- | Embed a VM state transformation
  EVM  :: EVM a   -> Action a

  -- | Perform an IO action
  IOAct :: StateT VM IO a -> Action a -- they should all just be this?

-- | Type alias for an operational monad of @Action@
type Stepper a = Program Action a

-- Singleton actions

exec :: Stepper VMResult
exec :: Stepper VMResult
exec = Action VMResult -> Stepper VMResult
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VMResult
Exec

run :: Stepper VM
run :: Stepper VM
run = Action VM -> Stepper VM
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VM
Run

wait :: Query -> Stepper ()
wait :: Query -> Stepper ()
wait = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Query -> Action ()) -> Query -> Stepper ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Query -> Action ()
Wait

ask :: Choose -> Stepper ()
ask :: Choose -> Stepper ()
ask = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Choose -> Action ()) -> Choose -> Stepper ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Choose -> Action ()
Ask

evm :: EVM a -> Stepper a
evm :: EVM a -> Stepper a
evm = Action a -> Stepper a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> Stepper a)
-> (EVM a -> Action a) -> EVM a -> Stepper a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EVM a -> Action a
forall a. EVM a -> Action a
EVM

evmIO :: StateT VM IO a -> Stepper a
evmIO :: StateT VM IO a -> Stepper a
evmIO = Action a -> Stepper a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> Stepper a)
-> (StateT VM IO a -> Action a) -> StateT VM IO a -> Stepper a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT VM IO a -> Action a
forall a. StateT VM IO a -> Action a
IOAct

-- | Run the VM until final result, resolving all queries
execFully :: Stepper (Either Error Buffer)
execFully :: Stepper (Either Error Buffer)
execFully =
  Stepper VMResult
exec Stepper VMResult
-> (VMResult -> Stepper (Either Error Buffer))
-> Stepper (Either Error Buffer)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    VMFailure (Query Query
q) ->
      Query -> Stepper ()
wait Query
q Stepper ()
-> Stepper (Either Error Buffer) -> Stepper (Either Error Buffer)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper (Either Error Buffer)
execFully
    VMFailure (Choose Choose
q) ->
      Choose -> Stepper ()
ask Choose
q Stepper ()
-> Stepper (Either Error Buffer) -> Stepper (Either Error Buffer)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper (Either Error Buffer)
execFully
    VMFailure Error
x ->
      Either Error Buffer -> Stepper (Either Error Buffer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Error -> Either Error Buffer
forall a b. a -> Either a b
Left Error
x)
    VMSuccess Buffer
x ->
      Either Error Buffer -> Stepper (Either Error Buffer)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Buffer -> Either Error Buffer
forall a b. b -> Either a b
Right Buffer
x)

-- | Run the VM until its final state
runFully :: Stepper EVM.VM
runFully :: Stepper VM
runFully = do
  VM
vm <- Stepper VM
run
  case VM -> Maybe VMResult
EVM._result VM
vm of
    Maybe VMResult
Nothing -> [Char] -> Stepper VM
forall a. HasCallStack => [Char] -> a
error [Char]
"should not occur"
    Just (VMFailure (Query Query
q)) ->
      Query -> Stepper ()
wait Query
q Stepper () -> Stepper VM -> Stepper VM
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper VM
runFully
    Just (VMFailure (Choose Choose
q)) ->
      Choose -> Stepper ()
ask Choose
q Stepper () -> Stepper VM -> Stepper VM
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper VM
runFully
    Just VMResult
_ ->
      VM -> Stepper VM
forall (f :: * -> *) a. Applicative f => a -> f a
pure VM
vm

entering :: Text -> Stepper a -> Stepper a
entering :: Text -> Stepper a -> Stepper a
entering Text
t Stepper a
stepper = do
  EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm (TraceData -> EVM ()
EVM.pushTrace (Text -> TraceData
EVM.EntryTrace Text
t))
  a
x <- Stepper a
stepper
  EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm EVM ()
EVM.popTrace
  a -> Stepper a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

enter :: Text -> Stepper ()
enter :: Text -> Stepper ()
enter Text
t = EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm (TraceData -> EVM ()
EVM.pushTrace (Text -> TraceData
EVM.EntryTrace Text
t))

interpret :: Fetch.Fetcher -> Stepper a -> StateT VM IO a
interpret :: Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher =
  ProgramView Action a -> StateT VM IO a
forall a. ProgramView Action a -> StateT VM IO a
eval (ProgramView Action a -> StateT VM IO a)
-> (Stepper a -> ProgramView Action a)
-> Stepper a
-> StateT VM IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper a -> ProgramView Action a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view

  where
    eval
      :: ProgramView Action a
      -> StateT VM IO a

    eval :: ProgramView Action a -> StateT VM IO a
eval (Return a
x) =
      a -> StateT VM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

    eval (Action b
action :>>= b -> ProgramT Action Identity a
k) =
      case Action b
action of
        Action b
Exec ->
          StateT VM IO VMResult
forall (m :: * -> *). MonadState VM m => m VMResult
EVM.Exec.exec StateT VM IO VMResult
-> (VMResult -> StateT VM IO a) -> StateT VM IO a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher -> ProgramT Action Identity a -> StateT VM IO a
forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (ProgramT Action Identity a -> StateT VM IO a)
-> (b -> ProgramT Action Identity a) -> b -> StateT VM IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Action b
Run ->
          StateT VM IO VM
forall (m :: * -> *). MonadState VM m => m VM
EVM.Exec.run StateT VM IO VM -> (VM -> StateT VM IO a) -> StateT VM IO a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher -> ProgramT Action Identity a -> StateT VM IO a
forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (ProgramT Action Identity a -> StateT VM IO a)
-> (b -> ProgramT Action Identity a) -> b -> StateT VM IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Wait Query
q ->
          do EVM ()
m <- IO (EVM ()) -> StateT VM IO (EVM ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
             (VM -> ((), VM)) -> StateT VM IO ()
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState EVM ()
m) StateT VM IO () -> StateT VM IO a -> StateT VM IO a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fetcher -> ProgramT Action Identity a -> StateT VM IO a
forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (b -> ProgramT Action Identity a
k ())
        Ask Choose
_ ->
          [Char] -> StateT VM IO a
forall a. HasCallStack => [Char] -> a
error [Char]
"cannot make choices with this interpreter"
        IOAct StateT VM IO b
m ->
          do StateT VM IO b
m StateT VM IO b -> (b -> StateT VM IO a) -> StateT VM IO a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fetcher -> ProgramT Action Identity a -> StateT VM IO a
forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (ProgramT Action Identity a -> StateT VM IO a)
-> (b -> ProgramT Action Identity a) -> b -> StateT VM IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        EVM EVM b
m -> do
          b
r <- (VM -> (b, VM)) -> StateT VM IO b
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (EVM b -> VM -> (b, VM)
forall s a. State s a -> s -> (a, s)
runState EVM b
m)
          Fetcher -> ProgramT Action Identity a -> StateT VM IO a
forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (b -> ProgramT Action Identity a
k b
r)