{- |
    Module: EVM.Traversals
    Description: Generic traversal functions for Expr datatypes
-}
module EVM.Traversals where

import Prelude hiding (LT, GT)

import Control.Monad.Identity

import EVM.Types

foldProp :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Prop -> b
foldProp :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f b
acc Prop
p = b
acc b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Prop -> b
go Prop
p)
  where
    go :: Prop -> b
    go :: Prop -> b
go = \case
      PBool Bool
_ -> b
forall a. Monoid a => a
mempty
      PEq Expr a
a Expr a
b -> ((forall (a :: EType). Expr a -> b) -> b -> Expr a -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr a
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((forall (a :: EType). Expr a -> b) -> b -> Expr a -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr a
b)
      PLT Expr 'EWord
a Expr 'EWord
b -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
b
      PGT Expr 'EWord
a Expr 'EWord
b -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
b
      PGEq Expr 'EWord
a Expr 'EWord
b -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
b
      PLEq Expr 'EWord
a Expr 'EWord
b -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
b
      PNeg Prop
a -> Prop -> b
go Prop
a
      PAnd Prop
a Prop
b -> Prop -> b
go Prop
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b
      POr Prop
a Prop
b -> Prop -> b
go Prop
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b
      PImpl Prop
a Prop
b -> Prop -> b
go Prop
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b

foldTrace :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Trace -> b
foldTrace :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Trace -> b
foldTrace forall (a :: EType). Expr a -> b
f b
acc Trace
t = b
acc b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Trace -> b
go Trace
t)
  where
    go :: Trace -> b
    go :: Trace -> b
go (Trace Int
_ Contract
_ TraceData
d) = case TraceData
d of
      EventTrace Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'Buf -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'Buf
b b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> Expr 'EWord -> b) -> b -> [Expr 'EWord] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f) b
forall a. Monoid a => a
mempty [Expr 'EWord]
c)
      FrameTrace FrameContext
a -> FrameContext -> b
go' FrameContext
a
      ErrorTrace EvmError
_ -> b
forall a. Monoid a => a
mempty
      EntryTrace Text
_ -> b
forall a. Monoid a => a
mempty
      ReturnTrace Expr 'Buf
a FrameContext
b -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'Buf -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'Buf
a b -> b -> b
forall a. Semigroup a => a -> a -> a
<> FrameContext -> b
go' FrameContext
b

    go' :: FrameContext -> b
    go' :: FrameContext -> b
go' = \case
      CreationContext Addr
_ Expr 'EWord
b Map Addr Contract
_ SubState
_ -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
b
      CallContext Addr
_ Addr
_ W256
_ W256
_ Expr 'EWord
e Maybe W256
_ Expr 'Buf
g (Map Addr Contract
_, Expr 'Storage
h) SubState
_ -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EWord -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'EWord
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'Buf -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'Buf
g b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Expr 'Storage -> b
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Expr 'Storage
h

foldTraces :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Traces -> b
foldTraces :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Traces -> b
foldTraces forall (a :: EType). Expr a -> b
f b
acc (Traces Forest Trace
a Map Addr Contract
_) = b
acc b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (b -> Tree Trace -> b) -> b -> Forest Trace -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((b -> Trace -> b) -> b -> Tree Trace -> b
forall b a. (b -> a -> b) -> b -> Tree a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (a :: EType). Expr a -> b) -> b -> Trace -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Trace -> b
foldTrace Expr a -> b
forall (a :: EType). Expr a -> b
f)) b
forall a. Monoid a => a
mempty Forest Trace
a



-- | Recursively folds a given function over a given expression
-- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle
foldExpr :: forall b c . Monoid b => (forall a . Expr a -> b) -> b -> Expr c -> b
foldExpr :: forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f b
acc Expr c
expr = b
acc b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr c -> b
forall (a :: EType). Expr a -> b
go Expr c
expr)
  where
    go :: forall a . Expr a -> b
    go :: forall (a :: EType). Expr a -> b
go = \case

      -- literals & variables

      e :: Expr a
e@(Lit W256
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(LitByte Word8
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Var Text
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(GVar GVar a
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e

      -- bytes

      e :: Expr a
e@(IndexWord Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(EqByte Expr 'Byte
a Expr 'Byte
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
b)

      e :: Expr a
e@(JoinBytes
        Expr 'Byte
zero Expr 'Byte
one Expr 'Byte
two Expr 'Byte
three Expr 'Byte
four Expr 'Byte
five Expr 'Byte
six Expr 'Byte
seven
        Expr 'Byte
eight Expr 'Byte
nine Expr 'Byte
ten Expr 'Byte
eleven Expr 'Byte
twelve Expr 'Byte
thirteen Expr 'Byte
fourteen Expr 'Byte
fifteen
        Expr 'Byte
sixteen Expr 'Byte
seventeen Expr 'Byte
eighteen Expr 'Byte
nineteen Expr 'Byte
twenty Expr 'Byte
twentyone Expr 'Byte
twentytwo Expr 'Byte
twentythree
        Expr 'Byte
twentyfour Expr 'Byte
twentyfive Expr 'Byte
twentysix Expr 'Byte
twentyseven Expr 'Byte
twentyeight Expr 'Byte
twentynine Expr 'Byte
thirty Expr 'Byte
thirtyone)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
zero) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
one) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
two) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
three)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
four) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
five) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
six) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
seven)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
eight) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
nine) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
ten) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
eleven)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twelve) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
thirteen) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
fourteen)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
fifteen) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
sixteen) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
seventeen)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
eighteen) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
nineteen) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twenty)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyone) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentytwo) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentythree)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyfour) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyfive) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentysix)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyseven) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyeight) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
twentynine)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
thirty) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
thirtyone)

      -- control flow

      e :: Expr a
e@(Success [Prop]
a Traces
b Expr 'Buf
c Expr 'Storage
d) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> Prop -> b) -> b -> [Prop] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (a :: EType). Expr a -> b) -> b -> Prop -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp Expr a -> b
forall (a :: EType). Expr a -> b
f) b
forall a. Monoid a => a
mempty [Prop]
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Traces -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Traces -> b
foldTraces Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Traces
b b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
c) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
d)
      e :: Expr a
e@(Failure [Prop]
a Traces
b EvmError
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> Prop -> b) -> b -> [Prop] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (a :: EType). Expr a -> b) -> b -> Prop -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp Expr a -> b
forall (a :: EType). Expr a -> b
f) b
forall a. Monoid a => a
mempty [Prop]
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Traces -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Traces -> b
foldTraces Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Traces
b
      e :: Expr a
e@(Partial [Prop]
a Traces
b PartialExec
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> Prop -> b) -> b -> [Prop] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((forall (a :: EType). Expr a -> b) -> b -> Prop -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp Expr a -> b
forall (a :: EType). Expr a -> b
f) b
forall a. Monoid a => a
mempty [Prop]
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> b -> Traces -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Traces -> b
foldTraces Expr a -> b
forall (a :: EType). Expr a -> b
f b
forall a. Monoid a => a
mempty Traces
b
      e :: Expr a
e@(ITE Expr 'EWord
a Expr 'End
b Expr 'End
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'End -> b
forall (a :: EType). Expr a -> b
go Expr 'End
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'End -> b
forall (a :: EType). Expr a -> b
go Expr 'End
c)

      -- integers

      e :: Expr a
e@(Add Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Sub Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Mul Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Div Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SDiv Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Mod Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SMod Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(AddMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
      e :: Expr a
e@(MulMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
      e :: Expr a
e@(Exp Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SEx Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Min Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Max Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)

      -- booleans

      e :: Expr a
e@(LT Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(GT Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(LEq Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(GEq Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SLT Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SGT Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Eq Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(IsZero Expr 'EWord
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)

      -- bits

      e :: Expr a
e@(And Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Or Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Xor Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(Not Expr 'EWord
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
      e :: Expr a
e@(SHL Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SHR Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
      e :: Expr a
e@(SAR Expr 'EWord
a Expr 'EWord
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)

      -- Hashes

      e :: Expr a
e@(Keccak Expr 'Buf
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
a)
      e :: Expr a
e@(SHA256 Expr 'Buf
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
a)

      -- block context

      e :: Expr a
e@(Expr a
Origin) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
Coinbase) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
Timestamp) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
BlockNumber) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
PrevRandao) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
GasLimit) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
ChainId) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
BaseFee) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(BlockHash Expr 'EWord
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)

      -- frame context

      e :: Expr a
e@(Caller Int
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(CallValue Int
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Address Int
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(SelfBalance Int
_ Int
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Gas Int
_ Int
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Balance {}) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e

      -- code

      e :: Expr a
e@(CodeSize Expr 'EWord
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
      e :: Expr a
e@(ExtCodeHash Expr 'EWord
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)

      -- logs

      e :: Expr a
e@(LogEntry Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'EWord -> b) -> [Expr 'EWord] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'EWord -> b
forall (a :: EType). Expr a -> b
f [Expr 'EWord]
c))

      -- Contract Creation

      e :: Expr a
e@(Create Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d [Expr 'Log]
g Expr 'Storage
h)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'Log -> b) -> [Expr 'Log] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Log -> b
forall (a :: EType). Expr a -> b
go [Expr 'Log]
g))
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
h)
      e :: Expr a
e@(Create2 Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'Buf
g [Expr 'Log]
h Expr 'Storage
i)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
g)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'Log -> b) -> [Expr 'Log] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Log -> b
forall (a :: EType). Expr a -> b
go [Expr 'Log]
h))
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
i)

      -- Calls

      e :: Expr a
e@(Call Expr 'EWord
a Maybe (Expr 'EWord)
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (b -> (Expr 'EWord -> b) -> Maybe (Expr 'EWord) -> b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe b
forall a. Monoid a => a
mempty (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go) Maybe (Expr 'EWord)
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'Log -> b) -> [Expr 'Log] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Log -> b
forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
k)

      e :: Expr a
e@(CallCode Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'Log -> b) -> [Expr 'Log] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Log -> b
forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
k)

      e :: Expr a
e@(DelegeateCall Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> ((b -> b -> b) -> b -> [b] -> b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> b -> b
forall a. Semigroup a => a -> a -> a
(<>) b
forall a. Monoid a => a
mempty ((Expr 'Log -> b) -> [Expr 'Log] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'Log -> b
forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
k)

      -- storage

      e :: Expr a
e@(Expr a
EmptyStore) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(ConcreteStore Map W256 (Map W256 W256)
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(Expr a
AbstractStore) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(SLoad Expr 'EWord
a Expr 'EWord
b Expr 'Storage
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
c)
      e :: Expr a
e@(SStore Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Storage
d) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
d)

      -- buffers

      e :: Expr a
e@(ConcreteBuf ByteString
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(AbstractBuf Text
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
      e :: Expr a
e@(ReadWord Expr 'EWord
a Expr 'Buf
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
      e :: Expr a
e@(ReadByte Expr 'EWord
a Expr 'Buf
b) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
      e :: Expr a
e@(WriteWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
c)
      e :: Expr a
e@(WriteByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Byte -> b
forall (a :: EType). Expr a -> b
go Expr 'Byte
b) b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
c)

      e :: Expr a
e@(CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
g)
        -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'EWord -> b
forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
d)
        b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
g)
      e :: Expr a
e@(BufLength Expr 'Buf
a) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
a)

mapProp :: (forall a . Expr a -> Expr a) -> Prop -> Prop
mapProp :: (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp forall (a :: EType). Expr a -> Expr a
f = \case
  PBool Bool
b -> Bool -> Prop
PBool Bool
b
  PEq Expr a
a Expr a
b -> Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq ((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Expr a
a)) ((forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Expr a
b))
  PLT Expr 'EWord
a Expr 'EWord
b -> Expr 'EWord -> Expr 'EWord -> Prop
PLT ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
b))
  PGT Expr 'EWord
a Expr 'EWord
b -> Expr 'EWord -> Expr 'EWord -> Prop
PGT ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
b))
  PLEq Expr 'EWord
a Expr 'EWord
b -> Expr 'EWord -> Expr 'EWord -> Prop
PLEq ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
b))
  PGEq Expr 'EWord
a Expr 'EWord
b -> Expr 'EWord -> Expr 'EWord -> Prop
PGEq ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
b))
  PNeg Prop
a -> Prop -> Prop
PNeg ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
a)
  PAnd Prop
a Prop
b -> Prop -> Prop -> Prop
PAnd ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
b)
  POr Prop
a Prop
b -> Prop -> Prop -> Prop
POr ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
b)
  PImpl Prop
a Prop
b -> Prop -> Prop -> Prop
PImpl ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f Prop
b)

mapTrace :: (forall a . Expr a -> Expr a) -> Trace -> Trace
mapTrace :: (forall (a :: EType). Expr a -> Expr a) -> Trace -> Trace
mapTrace forall (a :: EType). Expr a -> Expr a
f (Trace Int
x Contract
y TraceData
z) = Int -> Contract -> TraceData -> Trace
Trace Int
x Contract
y (TraceData -> TraceData
go TraceData
z)
  where
    go :: TraceData -> TraceData
    go :: TraceData -> TraceData
go = \case
      EventTrace Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c -> Expr 'EWord -> Expr 'Buf -> [Expr 'EWord] -> TraceData
EventTrace (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a) (Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
f Expr 'Buf
b) ((Expr 'EWord -> Expr 'EWord) -> [Expr 'EWord] -> [Expr 'EWord]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (a :: EType). Expr a -> Expr a)
-> Expr 'EWord -> Expr 'EWord
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f) [Expr 'EWord]
c)
      FrameTrace FrameContext
a -> FrameContext -> TraceData
FrameTrace (FrameContext -> FrameContext
go' FrameContext
a)
      ErrorTrace EvmError
a -> EvmError -> TraceData
ErrorTrace EvmError
a
      EntryTrace Text
a -> Text -> TraceData
EntryTrace Text
a
      ReturnTrace Expr 'Buf
a FrameContext
b -> Expr 'Buf -> FrameContext -> TraceData
ReturnTrace (Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
f Expr 'Buf
a) (FrameContext -> FrameContext
go' FrameContext
b)

    go' :: FrameContext -> FrameContext
    go' :: FrameContext -> FrameContext
go' = \case
      CreationContext Addr
a Expr 'EWord
b Map Addr Contract
c SubState
d -> Addr
-> Expr 'EWord -> Map Addr Contract -> SubState -> FrameContext
CreationContext Addr
a (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
b) Map Addr Contract
c SubState
d
      CallContext Addr
a Addr
b W256
c W256
d Expr 'EWord
e Maybe W256
g Expr 'Buf
h (Map Addr Contract
i,Expr 'Storage
j) SubState
k -> Addr
-> Addr
-> W256
-> W256
-> Expr 'EWord
-> Maybe W256
-> Expr 'Buf
-> (Map Addr Contract, Expr 'Storage)
-> SubState
-> FrameContext
CallContext Addr
a Addr
b W256
c W256
d (Expr 'EWord -> Expr 'EWord
forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
e) Maybe W256
g (Expr 'Buf -> Expr 'Buf
forall (a :: EType). Expr a -> Expr a
f Expr 'Buf
h) (Map Addr Contract
i,Expr 'Storage -> Expr 'Storage
forall (a :: EType). Expr a -> Expr a
f Expr 'Storage
j) SubState
k

-- | Recursively applies a given function to every node in a given expr instance
-- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle
mapExpr :: (forall a . Expr a -> Expr a) -> Expr b -> Expr b
mapExpr :: forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f Expr b
expr = Identity (Expr b) -> Expr b
forall a. Identity a -> a
runIdentity ((forall (a :: EType). Expr a -> Identity (Expr a))
-> Expr b -> Identity (Expr b)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM (Expr a -> Identity (Expr a)
forall a. a -> Identity a
Identity (Expr a -> Identity (Expr a))
-> (Expr a -> Expr a) -> Expr a -> Identity (Expr a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr a -> Expr a
forall (a :: EType). Expr a -> Expr a
f) Expr b
expr)


mapExprM :: Monad m => (forall a . Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM :: forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM forall (a :: EType). Expr a -> m (Expr a)
f Expr b
expr = case Expr b
expr of

  -- literals & variables

  Lit W256
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (W256 -> Expr 'EWord
Lit W256
a)
  LitByte Word8
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Word8 -> Expr 'Byte
LitByte Word8
a)
  Var Text
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Text -> Expr 'EWord
Var Text
a)
  GVar GVar b
s -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (GVar b -> Expr b
forall (a :: EType). GVar a -> Expr a
GVar GVar b
s)

  -- bytes

  IndexWord Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'Byte
IndexWord Expr 'EWord
a' Expr 'EWord
b')
  EqByte Expr 'Byte
a Expr 'Byte
b -> do
    Expr 'Byte
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
a
    Expr 'Byte
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Byte -> Expr 'Byte -> Expr 'EWord
EqByte Expr 'Byte
a' Expr 'Byte
b')

  JoinBytes Expr 'Byte
zero Expr 'Byte
one Expr 'Byte
two Expr 'Byte
three Expr 'Byte
four Expr 'Byte
five Expr 'Byte
six Expr 'Byte
seven Expr 'Byte
eight Expr 'Byte
nine
    Expr 'Byte
ten Expr 'Byte
eleven Expr 'Byte
twelve Expr 'Byte
thirteen Expr 'Byte
fourteen Expr 'Byte
fifteen Expr 'Byte
sixteen Expr 'Byte
seventeen
    Expr 'Byte
eighteen Expr 'Byte
nineteen Expr 'Byte
twenty Expr 'Byte
twentyone Expr 'Byte
twentytwo Expr 'Byte
twentythree Expr 'Byte
twentyfour
    Expr 'Byte
twentyfive Expr 'Byte
twentysix Expr 'Byte
twentyseven Expr 'Byte
twentyeight Expr 'Byte
twentynine Expr 'Byte
thirty Expr 'Byte
thirtyone -> do
    Expr 'Byte
zero' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
zero
    Expr 'Byte
one' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
one
    Expr 'Byte
two' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
two
    Expr 'Byte
three' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
three
    Expr 'Byte
four' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
four
    Expr 'Byte
five' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
five
    Expr 'Byte
six' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
six
    Expr 'Byte
seven' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
seven
    Expr 'Byte
eight' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
eight
    Expr 'Byte
nine' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
nine
    Expr 'Byte
ten' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
ten
    Expr 'Byte
eleven' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
eleven
    Expr 'Byte
twelve' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twelve
    Expr 'Byte
thirteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
thirteen
    Expr 'Byte
fourteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
fourteen
    Expr 'Byte
fifteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
fifteen
    Expr 'Byte
sixteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
sixteen
    Expr 'Byte
seventeen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
seventeen
    Expr 'Byte
eighteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
eighteen
    Expr 'Byte
nineteen' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
nineteen
    Expr 'Byte
twenty' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twenty
    Expr 'Byte
twentyone' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentyone
    Expr 'Byte
twentytwo' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentytwo
    Expr 'Byte
twentythree' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentythree
    Expr 'Byte
twentyfour' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentyfour
    Expr 'Byte
twentyfive' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentyfive
    Expr 'Byte
twentysix' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentysix
    Expr 'Byte
twentyseven' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentyseven
    Expr 'Byte
twentyeight' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentyeight
    Expr 'Byte
twentynine' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
twentynine
    Expr 'Byte
thirty' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
thirty
    Expr 'Byte
thirtyone' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
thirtyone
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'Byte
-> Expr 'EWord
JoinBytes Expr 'Byte
zero' Expr 'Byte
one' Expr 'Byte
two' Expr 'Byte
three' Expr 'Byte
four' Expr 'Byte
five' Expr 'Byte
six' Expr 'Byte
seven' Expr 'Byte
eight' Expr 'Byte
nine'
         Expr 'Byte
ten' Expr 'Byte
eleven' Expr 'Byte
twelve' Expr 'Byte
thirteen' Expr 'Byte
fourteen' Expr 'Byte
fifteen' Expr 'Byte
sixteen' Expr 'Byte
seventeen'
         Expr 'Byte
eighteen' Expr 'Byte
nineteen' Expr 'Byte
twenty' Expr 'Byte
twentyone' Expr 'Byte
twentytwo' Expr 'Byte
twentythree' Expr 'Byte
twentyfour'
         Expr 'Byte
twentyfive' Expr 'Byte
twentysix' Expr 'Byte
twentyseven' Expr 'Byte
twentyeight' Expr 'Byte
twentynine' Expr 'Byte
thirty' Expr 'Byte
thirtyone')

  -- control flow

  Failure [Prop]
a Traces
b EvmError
c -> do
    [Prop]
a' <- (Prop -> m Prop) -> [Prop] -> m [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    Traces
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
mapTracesM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Traces
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Traces -> EvmError -> Expr 'End
Failure [Prop]
a' Traces
b' EvmError
c)
  Partial [Prop]
a Traces
b PartialExec
c -> do
    [Prop]
a' <- (Prop -> m Prop) -> [Prop] -> m [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    Traces
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
mapTracesM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Traces
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Traces -> PartialExec -> Expr 'End
Partial [Prop]
a' Traces
b' PartialExec
c)
  Success [Prop]
a Traces
b Expr 'Buf
c Expr 'Storage
d -> do
    [Prop]
a' <- (Prop -> m Prop) -> [Prop] -> m [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    Traces
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
mapTracesM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Traces
b
    Expr 'Buf
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
c
    Expr 'Storage
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
d
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Traces -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Success [Prop]
a' Traces
b' Expr 'Buf
c' Expr 'Storage
d')

  ITE Expr 'EWord
a Expr 'End
b Expr 'End
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'End
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'End -> m (Expr 'End)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'End
b
    Expr 'End
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'End -> m (Expr 'End)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'End
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'End -> Expr 'End -> Expr 'End
ITE Expr 'EWord
a' Expr 'End
b' Expr 'End
c')

  -- integers

  Add Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Add Expr 'EWord
a' Expr 'EWord
b')
  Sub Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Sub Expr 'EWord
a' Expr 'EWord
b')
  Mul Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mul Expr 'EWord
a' Expr 'EWord
b')
  Div Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Div Expr 'EWord
a' Expr 'EWord
b')
  SDiv Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SDiv Expr 'EWord
a' Expr 'EWord
b')
  Mod Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Mod Expr 'EWord
a' Expr 'EWord
b')
  SMod Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SMod Expr 'EWord
a' Expr 'EWord
b')
  AddMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
AddMod Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c')
  MulMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord -> Expr 'EWord
MulMod Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c')
  Exp Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Exp Expr 'EWord
a' Expr 'EWord
b')
  SEx Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SEx Expr 'EWord
a' Expr 'EWord
b')
  Min Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Min Expr 'EWord
a' Expr 'EWord
b')
  Max Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Max Expr 'EWord
a' Expr 'EWord
b')

  -- booleans

  LT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
LT Expr 'EWord
a' Expr 'EWord
b')
  GT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GT Expr 'EWord
a' Expr 'EWord
b')
  LEq Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
LEq Expr 'EWord
a' Expr 'EWord
b')
  GEq Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
GEq Expr 'EWord
a' Expr 'EWord
b')
  SLT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SLT Expr 'EWord
a' Expr 'EWord
b')
  SGT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SGT Expr 'EWord
a' Expr 'EWord
b')
  Eq Expr 'EWord
a Expr 'EWord
b ->  do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Eq Expr 'EWord
a' Expr 'EWord
b')
  IsZero Expr 'EWord
a -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
IsZero Expr 'EWord
a')

  -- bits

  And Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
And Expr 'EWord
a' Expr 'EWord
b')
  Or Expr 'EWord
a Expr 'EWord
b ->  do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Or Expr 'EWord
a' Expr 'EWord
b')
  Xor Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
Xor Expr 'EWord
a' Expr 'EWord
b')
  Not Expr 'EWord
a -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
Not Expr 'EWord
a')
  SHL Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHL Expr 'EWord
a' Expr 'EWord
b')
  SHR Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SHR Expr 'EWord
a' Expr 'EWord
b')
  SAR Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'EWord
SAR Expr 'EWord
a' Expr 'EWord
b')


  -- Hashes

  Keccak Expr 'Buf
a -> do
    Expr 'Buf
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Buf -> Expr 'EWord
Keccak Expr 'Buf
a')

  SHA256 Expr 'Buf
a -> do
    Expr 'Buf
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Buf -> Expr 'EWord
SHA256 Expr 'Buf
a')

  -- block context

  Expr b
Origin -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
Origin
  Expr b
Coinbase -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
Coinbase
  Expr b
Timestamp -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
Timestamp
  Expr b
BlockNumber -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
BlockNumber
  Expr b
PrevRandao -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
PrevRandao
  Expr b
GasLimit -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
GasLimit
  Expr b
ChainId -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
ChainId
  Expr b
BaseFee -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
BaseFee
  BlockHash Expr 'EWord
a -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
BlockHash Expr 'EWord
a')

  -- frame context

  Caller Int
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
Caller Int
a)
  CallValue Int
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
CallValue Int
a)
  Address Int
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
Address Int
a)
  SelfBalance Int
a Int
b -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord
SelfBalance Int
a Int
b)
  Gas Int
a Int
b -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord
Gas Int
a Int
b)
  Balance Int
a Int
b Expr 'EWord
c -> do
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord -> Expr 'EWord
Balance Int
a Int
b Expr 'EWord
c')

  -- code

  CodeSize Expr 'EWord
a -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
CodeSize Expr 'EWord
a')
  ExtCodeHash Expr 'EWord
a -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
ExtCodeHash Expr 'EWord
a')

  -- logs

  LogEntry Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'Buf
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
    [Expr 'EWord]
c' <- (Expr 'EWord -> m (Expr 'EWord))
-> [Expr 'EWord] -> m [Expr 'EWord]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'EWord]
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'Buf -> [Expr 'EWord] -> Expr 'Log
LogEntry Expr 'EWord
a' Expr 'Buf
b' [Expr 'EWord]
c')

  -- Contract Creation

  Create Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d [Expr 'Log]
e Expr 'Storage
g -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'Buf
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
d
    [Expr 'Log]
e' <- (Expr 'Log -> m (Expr 'Log)) -> [Expr 'Log] -> m [Expr 'Log]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Log -> m (Expr 'Log)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'Log]
e
    Expr 'Storage
g' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
g
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Create Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'Buf
d' [Expr 'Log]
e' Expr 'Storage
g')
  Create2 Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'Buf
e [Expr 'Log]
g Expr 'Storage
h -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'EWord
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
d
    Expr 'Buf
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
e
    [Expr 'Log]
g' <- (Expr 'Log -> m (Expr 'Log)) -> [Expr 'Log] -> m [Expr 'Log]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Log -> m (Expr 'Log)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'Log]
g
    Expr 'Storage
h' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
h
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Create2 Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'Buf
e' [Expr 'Log]
g' Expr 'Storage
h')

  -- Calls

  Call Expr 'EWord
a Maybe (Expr 'EWord)
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Maybe (Expr 'EWord)
b' <- (Expr 'EWord -> m (Expr 'EWord))
-> Maybe (Expr 'EWord) -> m (Maybe (Expr 'EWord))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) Maybe (Expr 'EWord)
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'EWord
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
d
    Expr 'EWord
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
e
    Expr 'EWord
g' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
g
    Expr 'EWord
h' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
h
    [Expr 'Log]
i' <- (Expr 'Log -> m (Expr 'Log)) -> [Expr 'Log] -> m [Expr 'Log]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Log -> m (Expr 'Log)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'Log]
i
    Expr 'Storage
j' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
j
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Maybe (Expr 'EWord)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Call Expr 'EWord
a' Maybe (Expr 'EWord)
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')
  CallCode Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'EWord
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
d
    Expr 'EWord
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
e
    Expr 'EWord
g' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
g
    Expr 'EWord
h' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
h
    [Expr 'Log]
i' <- (Expr 'Log -> m (Expr 'Log)) -> [Expr 'Log] -> m [Expr 'Log]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Log -> m (Expr 'Log)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'Log]
i
    Expr 'Storage
j' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
j
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
CallCode Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')
  DelegeateCall Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'EWord
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
d
    Expr 'EWord
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
e
    Expr 'EWord
g' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
g
    Expr 'EWord
h' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
h
    [Expr 'Log]
i' <- (Expr 'Log -> m (Expr 'Log)) -> [Expr 'Log] -> m [Expr 'Log]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Log -> m (Expr 'Log)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'Log]
i
    Expr 'Storage
j' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
j
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
DelegeateCall Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')

  -- storage

  Expr b
EmptyStore -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'Storage
EmptyStore
  ConcreteStore Map W256 (Map W256 W256)
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore Map W256 (Map W256 W256)
a)
  Expr b
AbstractStore -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'Storage
AbstractStore
  SLoad Expr 'EWord
a Expr 'EWord
b Expr 'Storage
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'Storage
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
a' Expr 'EWord
b' Expr 'Storage
c')
  SStore Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Storage
d -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'Storage
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
d
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'Storage
d')

  -- buffers

  ConcreteBuf ByteString
a -> do
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (ByteString -> Expr 'Buf
ConcreteBuf ByteString
a)
  AbstractBuf Text
a -> do
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Text -> Expr 'Buf
AbstractBuf Text
a)
  ReadWord Expr 'EWord
a Expr 'Buf
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'Buf
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'Buf -> Expr 'EWord
ReadWord Expr 'EWord
a' Expr 'Buf
b')
  ReadByte Expr 'EWord
a Expr 'Buf
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'Buf
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'Buf -> Expr 'Byte
ReadByte Expr 'EWord
a' Expr 'Buf
b')
  WriteWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'Buf
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'Buf -> Expr 'Buf
WriteWord Expr 'EWord
a' Expr 'EWord
b' Expr 'Buf
c')
  WriteByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'Byte
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Byte -> m (Expr 'Byte)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Byte
b
    Expr 'Buf
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
c
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'Byte -> Expr 'Buf -> Expr 'Buf
WriteByte Expr 'EWord
a' Expr 'Byte
b' Expr 'Buf
c')

  CopySlice Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d Expr 'Buf
e -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Expr 'EWord
c' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
c
    Expr 'Buf
d' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
d
    Expr 'Buf
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
e
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> Expr 'Buf
-> Expr 'Buf
CopySlice Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'Buf
d' Expr 'Buf
e')

  BufLength Expr 'Buf
a -> do
    Expr 'Buf
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
a
    Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Buf -> Expr 'EWord
BufLength Expr 'Buf
a')


mapPropM :: Monad m => (forall a . Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> m (Expr a)
f = \case
  PBool Bool
b -> Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Bool -> Prop
PBool Bool
b
  PEq Expr a
a Expr a
b -> do
    Expr a
a' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr a
a
    Expr a
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr a
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Expr a -> Expr a -> Prop
forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq Expr a
a' Expr a
b'
  PLT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Prop
PLT Expr 'EWord
a' Expr 'EWord
b'
  PGT Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Prop
PGT Expr 'EWord
a' Expr 'EWord
b'
  PLEq Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Prop
PLEq Expr 'EWord
a' Expr 'EWord
b'
  PGEq Expr 'EWord
a Expr 'EWord
b -> do
    Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
    Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
a' Expr 'EWord
b'
  PNeg Prop
a -> do
    Prop
a' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
a
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
PNeg Prop
a'
  PAnd Prop
a Prop
b -> do
    Prop
a' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
a
    Prop
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PAnd Prop
a' Prop
b'
  POr Prop
a Prop
b -> do
    Prop
a' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
a
    Prop
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
POr Prop
a' Prop
b'
  PImpl Prop
a Prop
b -> do
    Prop
a' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
a
    Prop
b' <- (forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Prop
b
    Prop -> m Prop
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> m Prop) -> Prop -> m Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PImpl Prop
a' Prop
b'

mapTracesM :: forall m . Monad m => (forall a . Expr a -> m (Expr a)) -> Traces -> m Traces
mapTracesM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Traces -> m Traces
mapTracesM forall (a :: EType). Expr a -> m (Expr a)
f (Traces Forest Trace
a Map Addr Contract
b) = do
  Forest Trace
a' <- (Tree Trace -> m (Tree Trace)) -> Forest Trace -> m (Forest Trace)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Trace -> m Trace) -> Tree Trace -> m (Tree Trace)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Tree a -> m (Tree b)
mapM ((forall (a :: EType). Expr a -> m (Expr a)) -> Trace -> m Trace
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Trace -> m Trace
mapTraceM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f)) Forest Trace
a
  Traces -> m Traces
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Traces -> m Traces) -> Traces -> m Traces
forall a b. (a -> b) -> a -> b
$ Forest Trace -> Map Addr Contract -> Traces
Traces Forest Trace
a' Map Addr Contract
b

mapTraceM :: forall m . Monad m => (forall a . Expr a -> m (Expr a)) -> Trace -> m Trace
mapTraceM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Trace -> m Trace
mapTraceM forall (a :: EType). Expr a -> m (Expr a)
f (Trace Int
x Contract
y TraceData
z) = do
  TraceData
z' <- TraceData -> m TraceData
go TraceData
z
  Trace -> m Trace
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Trace -> m Trace) -> Trace -> m Trace
forall a b. (a -> b) -> a -> b
$ Int -> Contract -> TraceData -> Trace
Trace Int
x Contract
y TraceData
z'
  where
    go :: TraceData -> m TraceData
    go :: TraceData -> m TraceData
go = \case
      EventTrace Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c -> do
        Expr 'EWord
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
a
        Expr 'Buf
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
        [Expr 'EWord]
c' <- (Expr 'EWord -> m (Expr 'EWord))
-> [Expr 'EWord] -> m [Expr 'EWord]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Expr 'EWord]
c
        TraceData -> m TraceData
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TraceData -> m TraceData) -> TraceData -> m TraceData
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'Buf -> [Expr 'EWord] -> TraceData
EventTrace Expr 'EWord
a' Expr 'Buf
b' [Expr 'EWord]
c'
      FrameTrace FrameContext
a -> do
        FrameContext
a' <- FrameContext -> m FrameContext
go' FrameContext
a
        TraceData -> m TraceData
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TraceData -> m TraceData) -> TraceData -> m TraceData
forall a b. (a -> b) -> a -> b
$ FrameContext -> TraceData
FrameTrace FrameContext
a'
      ReturnTrace Expr 'Buf
a FrameContext
b -> do
        Expr 'Buf
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
a
        FrameContext
b' <- FrameContext -> m FrameContext
go' FrameContext
b
        TraceData -> m TraceData
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TraceData -> m TraceData) -> TraceData -> m TraceData
forall a b. (a -> b) -> a -> b
$ Expr 'Buf -> FrameContext -> TraceData
ReturnTrace Expr 'Buf
a' FrameContext
b'
      TraceData
a -> TraceData -> m TraceData
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TraceData
a

    go' :: FrameContext -> m FrameContext
    go' :: FrameContext -> m FrameContext
go' = \case
      CreationContext Addr
a Expr 'EWord
b Map Addr Contract
c SubState
d -> do
        Expr 'EWord
b' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
b
        FrameContext -> m FrameContext
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FrameContext -> m FrameContext) -> FrameContext -> m FrameContext
forall a b. (a -> b) -> a -> b
$ Addr
-> Expr 'EWord -> Map Addr Contract -> SubState -> FrameContext
CreationContext Addr
a Expr 'EWord
b' Map Addr Contract
c SubState
d
      CallContext Addr
a Addr
b W256
c W256
d Expr 'EWord
e Maybe W256
g Expr 'Buf
h (Map Addr Contract
i,Expr 'Storage
j) SubState
k -> do
        Expr 'EWord
e' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EWord -> m (Expr 'EWord)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
e
        Expr 'Buf
h' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Buf -> m (Expr 'Buf)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
h
        Expr 'Storage
j' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'Storage -> m (Expr 'Storage)
forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
j
        FrameContext -> m FrameContext
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FrameContext -> m FrameContext) -> FrameContext -> m FrameContext
forall a b. (a -> b) -> a -> b
$ Addr
-> Addr
-> W256
-> W256
-> Expr 'EWord
-> Maybe W256
-> Expr 'Buf
-> (Map Addr Contract, Expr 'Storage)
-> SubState
-> FrameContext
CallContext Addr
a Addr
b W256
c W256
d Expr 'EWord
e' Maybe W256
g Expr 'Buf
h' (Map Addr Contract
i,Expr 'Storage
j') SubState
k

-- | Generic operations over AST terms
class TraversableTerm a where
  mapTerm  :: (forall b. Expr b -> Expr b) -> a -> a
  foldTerm :: forall c. Monoid c => (forall b. Expr b -> c) -> c -> a -> c


instance TraversableTerm (Expr a) where
  mapTerm :: (forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
mapTerm = (forall (a :: EType). Expr a -> Expr a) -> Expr a -> Expr a
forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr
  foldTerm :: forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> Expr a -> c
foldTerm = (forall (a :: EType). Expr a -> c) -> c -> Expr a -> c
forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr

instance TraversableTerm Prop where
  mapTerm :: (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapTerm = (forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp
  foldTerm :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldTerm = (forall (a :: EType). Expr a -> c) -> c -> Prop -> c
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp