{-# 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.

import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view)
import Control.Monad.State.Strict (StateT, execState, runState, runStateT)
import Data.Text (Text)

import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose)
import EVM qualified
import EVM.Exec qualified
import EVM.Fetch qualified as Fetch
import EVM.Types (Expr, EType(..))

-- | 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 = forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VMResult
Exec

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

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

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

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

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

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

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

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

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

interpret :: Fetch.Fetcher -> VM -> Stepper a -> IO a
interpret :: forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm = forall a. ProgramView Action a -> IO a
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view
  where
  eval :: ProgramView Action a -> IO a
  eval :: forall a. ProgramView Action a -> IO a
eval (Return a
x) = 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 ->
        let (VMResult
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState State VM VMResult
EVM.Exec.exec VM
vm
        in forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k VMResult
r)
      Action b
Run ->
        let vm' :: VM
vm' = forall s a. State s a -> s -> s
execState State VM VM
EVM.Exec.run VM
vm
        in forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k VM
vm')
      Wait Query
q -> do
        EVM ()
m <- Fetcher
fetcher Query
q
        let vm' :: VM
vm' = forall s a. State s a -> s -> s
execState EVM ()
m VM
vm
        forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k ())
      Ask Choose
_ ->
        forall a. HasCallStack => [Char] -> a
error [Char]
"cannot make choices with this interpreter"
      IOAct StateT VM IO b
m -> do
        (b
r, VM
vm') <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT VM IO b
m VM
vm
        forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
r)
      EVM EVM b
m ->
        let (b
r, VM
vm') = forall s a. State s a -> s -> (a, s)
runState EVM b
m VM
vm
        in forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
r)