{-# Language GADTs #-}
{-# Language DataKinds #-}
module EVM.Stepper
( Action (..)
, Stepper
, exec
, execFully
, run
, runFully
, wait
, ask
, evm
, evmIO
, entering
, enter
, interpret
)
where
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
data Action a where
Exec :: Action VMResult
Run :: Action VM
Wait :: Query -> Action ()
Ask :: Choose -> Action ()
EVM :: EVM a -> Action a
IOAct :: StateT VM IO a -> Action a
type Stepper a = Program Action a
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
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)
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)