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

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , 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

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

-- | 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 q :: 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 q :: 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 x :: 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 x :: 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
    Nothing -> [Char] -> Stepper VM
forall a. HasCallStack => [Char] -> a
error "should not occur"
    Just (VMFailure (Query q :: 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 q :: 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 _ ->
      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 t :: Text
t stepper :: 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 t :: 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
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 x :: a
x) =
      a -> StateT VM IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x

    eval (action :: Action b
action :>>= k :: b -> ProgramT Action Identity a
k) =
      case Action b
action of
        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
        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 q :: 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 _ ->
          [Char] -> StateT VM IO a
forall a. HasCallStack => [Char] -> a
error "cannot make choices with this interpreter"
        EVM m :: 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)