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

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 (Expr, EType(..))

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 = 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 -> Stepper a -> StateT VM IO a
interpret :: forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher =
  forall a. ProgramView Action a -> StateT VM 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
      -> StateT VM IO a

    eval :: forall a. ProgramView Action a -> StateT VM 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 ->
          (forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. State s a -> s -> (a, s)
runState) State VM VMResult
EVM.Exec.exec forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Action b
Run ->
          (forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. State s a -> s -> (a, s)
runState) State VM VM
EVM.Exec.run forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        Wait Query
q ->
          do EVM ()
m <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Fetcher
fetcher Query
q)
             forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (forall s a. State s a -> s -> (a, s)
runState EVM ()
m) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (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 StateT VM IO b
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> ProgramT Action Identity a
k
        EVM EVM b
m -> do
          b
r <- forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state (forall s a. State s a -> s -> (a, s)
runState EVM b
m)
          forall a. Fetcher -> Stepper a -> StateT VM IO a
interpret Fetcher
fetcher (b -> ProgramT Action Identity a
k b
r)