module EVM.Traversals where
import Prelude hiding (LT, GT)
import Control.Monad.Identity
import qualified Data.Map.Strict as Map
import Data.List (foldl')
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
foldEContract :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Expr EContract -> b
foldEContract :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr 'EContract -> b
foldEContract forall (a :: EType). Expr a -> b
f b
_ g :: Expr 'EContract
g@(GVar GVar 'EContract
_) = Expr 'EContract -> b
forall (a :: EType). Expr a -> b
f Expr 'EContract
g
foldEContract forall (a :: EType). Expr a -> b
f b
acc (C ContractCode
code Expr 'Storage
storage Expr 'EWord
balance Maybe W64
_)
= b
acc
b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> ContractCode -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> ContractCode -> b
foldCode Expr a -> b
forall (a :: EType). Expr a -> b
f ContractCode
code
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
storage
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
balance
foldContract :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Contract -> b
foldContract :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Contract -> b
foldContract forall (a :: EType). Expr a -> b
f b
acc Contract
c
= b
acc
b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b) -> ContractCode -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> ContractCode -> b
foldCode Expr a -> b
forall (a :: EType). Expr a -> b
f Contract
c.code
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 Contract
c.storage
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 Contract
c.origStorage
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 Contract
c.balance
foldCode :: forall b . Monoid b => (forall a . Expr a -> b) -> ContractCode -> b
foldCode :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> ContractCode -> b
foldCode forall (a :: EType). Expr a -> b
f = \case
RuntimeCode (ConcreteRuntimeCode ByteString
_) -> b
forall a. Monoid a => a
mempty
RuntimeCode (SymbolicRuntimeCode Vector (Expr 'Byte)
c) -> (b -> Expr 'Byte -> b) -> b -> Vector (Expr 'Byte) -> b
forall b a. (b -> a -> b) -> b -> Vector a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((forall (a :: EType). Expr a -> b) -> b -> Expr 'Byte -> 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 Vector (Expr 'Byte)
c
InitCode ByteString
_ Expr 'Buf
buf -> (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
buf
UnknownCode Expr 'EAddr
addr -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EAddr -> 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 'EAddr
addr
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
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
e :: Expr a
e@(C {}) -> (forall (a :: EType). Expr a -> b) -> b -> Expr 'EContract -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr 'EContract -> b
foldEContract Expr a -> b
forall (a :: EType). Expr a -> b
f b
acc Expr a
Expr 'EContract
e
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)
e :: Expr a
e@(Success [Prop]
a Traces
_ Expr 'Buf
c Map (Expr 'EAddr) (Expr 'EContract)
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
<> Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
c
b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (b -> Expr 'EAddr -> b) -> b -> [Expr 'EAddr] -> 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 'EAddr -> 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 (Map (Expr 'EAddr) (Expr 'EContract) -> [Expr 'EAddr]
forall k a. Map k a -> [k]
Map.keys Map (Expr 'EAddr) (Expr 'EContract)
d)
b -> b -> b
forall a. Semigroup a => a -> a -> a
<> (b -> Expr 'EContract -> b)
-> b -> Map (Expr 'EAddr) (Expr 'EContract) -> b
forall b a. (b -> a -> b) -> b -> Map (Expr 'EAddr) a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((forall (a :: EType). Expr a -> b) -> b -> Expr 'EContract -> b
forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr 'EContract -> b
foldEContract Expr a -> b
forall (a :: EType). Expr a -> b
f) b
forall a. Monoid a => a
mempty Map (Expr 'EAddr) (Expr 'EContract)
d
e :: Expr a
e@(Failure [Prop]
a Traces
_ (Revert 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
<> ((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
<> Expr 'Buf -> b
forall (a :: EType). Expr a -> b
go Expr 'Buf
c
e :: Expr a
e@(Failure [Prop]
a Traces
_ 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)
e :: Expr a
e@(Partial [Prop]
a Traces
_ 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)
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)
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)
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)
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)
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)
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)
e :: Expr a
e@(Expr a
TxValue) -> 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
e :: Expr a
e@(CodeSize Expr 'EAddr
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 'EAddr -> b
forall (a :: EType). Expr a -> b
go Expr 'EAddr
a)
e :: Expr a
e@(CodeHash Expr 'EAddr
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 'EAddr -> b
forall (a :: EType). Expr a -> b
go Expr 'EAddr
a)
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))
e :: Expr a
e@(LitAddr Addr
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(WAddr Expr 'EAddr
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 'EAddr -> b
forall (a :: EType). Expr a -> b
go Expr 'EAddr
a
e :: Expr a
e@(SymAddr Text
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(ConcreteStore Map W256 W256
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(AbstractStore Expr 'EAddr
_) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(SLoad Expr 'EWord
a Expr 'Storage
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 'Storage -> b
forall (a :: EType). Expr a -> b
go Expr 'Storage
b)
e :: Expr a
e@(SStore 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@(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)
mapProp' :: (Prop -> Prop) -> Prop -> Prop
mapProp' :: (Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f = \case
PBool Bool
b -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Bool -> Prop
PBool Bool
b
PEq Expr a
a Expr a
b -> Prop -> Prop
f (Prop -> Prop) -> Prop -> 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 -> Prop -> Prop
f (Prop -> Prop) -> Prop -> 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 -> Prop -> Prop
f (Prop -> Prop) -> Prop -> 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 -> Prop -> Prop
f (Prop -> Prop) -> Prop -> 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 -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Expr 'EWord -> Expr 'EWord -> Prop
PGEq Expr 'EWord
a Expr 'EWord
b
PNeg Prop
a -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
PNeg ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
a)
PAnd Prop
a Prop
b -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PAnd ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
a) ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
b)
POr Prop
a Prop
b -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
POr ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
a) ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
b)
PImpl Prop
a Prop
b -> Prop -> Prop
f (Prop -> Prop) -> Prop -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PImpl ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
a) ((Prop -> Prop) -> Prop -> Prop
mapProp' Prop -> Prop
f Prop
b)
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
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)
c :: Expr b
c@(C {}) -> (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EContract -> m (Expr 'EContract)
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EContract -> m (Expr 'EContract)
mapEContractM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EContract
c
LitAddr Addr
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Addr -> Expr 'EAddr
LitAddr Addr
a)
SymAddr Text
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Text -> Expr 'EAddr
SymAddr Text
a)
WAddr Expr 'EAddr
a -> do
Expr 'EAddr
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EAddr -> m (Expr 'EAddr)
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 'EAddr
a
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Expr 'EWord
WAddr Expr 'EAddr
a')
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')
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
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
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 Map (Expr 'EAddr) (Expr 'EContract)
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
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
Map (Expr 'EAddr) (Expr 'EContract)
d' <- do
let x :: [(Expr 'EAddr, Expr 'EContract)]
x = Map (Expr 'EAddr) (Expr 'EContract)
-> [(Expr 'EAddr, Expr 'EContract)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Expr 'EAddr) (Expr 'EContract)
d
[(Expr 'EAddr, Expr 'EContract)]
x' <- [(Expr 'EAddr, Expr 'EContract)]
-> ((Expr 'EAddr, Expr 'EContract)
-> m (Expr 'EAddr, Expr 'EContract))
-> m [(Expr 'EAddr, Expr 'EContract)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Expr 'EAddr, Expr 'EContract)]
x (((Expr 'EAddr, Expr 'EContract)
-> m (Expr 'EAddr, Expr 'EContract))
-> m [(Expr 'EAddr, Expr 'EContract)])
-> ((Expr 'EAddr, Expr 'EContract)
-> m (Expr 'EAddr, Expr 'EContract))
-> m [(Expr 'EAddr, Expr 'EContract)]
forall a b. (a -> b) -> a -> b
$ \(Expr 'EAddr
k,Expr 'EContract
v) -> do
Expr 'EAddr
k' <- Expr 'EAddr -> m (Expr 'EAddr)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EAddr
k
Expr 'EContract
v' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EContract -> m (Expr 'EContract)
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EContract -> m (Expr 'EContract)
mapEContractM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EContract
v
(Expr 'EAddr, Expr 'EContract) -> m (Expr 'EAddr, Expr 'EContract)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'EAddr
k',Expr 'EContract
v')
Map (Expr 'EAddr) (Expr 'EContract)
-> m (Map (Expr 'EAddr) (Expr 'EContract))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map (Expr 'EAddr) (Expr 'EContract)
-> m (Map (Expr 'EAddr) (Expr 'EContract)))
-> Map (Expr 'EAddr) (Expr 'EContract)
-> m (Map (Expr 'EAddr) (Expr 'EContract))
forall a b. (a -> b) -> a -> b
$ [(Expr 'EAddr, Expr 'EContract)]
-> Map (Expr 'EAddr) (Expr 'EContract)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Expr 'EAddr, Expr 'EContract)]
x'
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop]
-> Traces
-> Expr 'Buf
-> Map (Expr 'EAddr) (Expr 'EContract)
-> Expr 'End
Success [Prop]
a' Traces
b Expr 'Buf
c' Map (Expr 'EAddr) (Expr 'EContract)
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')
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')
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')
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')
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')
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')
Expr b
TxValue -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
TxValue
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 Expr 'EAddr
a -> do
Expr 'EAddr
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EAddr -> m (Expr 'EAddr)
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 'EAddr
a
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Expr 'EWord
Balance Expr 'EAddr
a')
CodeSize Expr 'EAddr
a -> do
Expr 'EAddr
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EAddr -> m (Expr 'EAddr)
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 'EAddr
a
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Expr 'EWord
CodeSize Expr 'EAddr
a')
CodeHash Expr 'EAddr
a -> do
Expr 'EAddr
a' <- (forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EAddr -> m (Expr 'EAddr)
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 'EAddr
a
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Expr 'EWord
CodeHash Expr 'EAddr
a')
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')
ConcreteStore Map W256 W256
b -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Map W256 W256 -> Expr 'Storage
ConcreteStore Map W256 W256
b)
AbstractStore Expr 'EAddr
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Expr 'Storage
AbstractStore Expr 'EAddr
a)
SLoad Expr 'EWord
a Expr 'Storage
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 'Storage
b' <- (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
b
Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
a' Expr 'Storage
b')
SStore 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 'Storage
SStore Expr 'EWord
a' Expr 'EWord
b' Expr 'Storage
c')
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'
mapEContractM :: Monad m => (forall a . Expr a -> m (Expr a)) -> Expr EContract -> m (Expr EContract)
mapEContractM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> Expr 'EContract -> m (Expr 'EContract)
mapEContractM forall (a :: EType). Expr a -> m (Expr a)
_ g :: Expr 'EContract
g@(GVar GVar 'EContract
_) = Expr 'EContract -> m (Expr 'EContract)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr 'EContract
g
mapEContractM forall (a :: EType). Expr a -> m (Expr a)
f (C ContractCode
code Expr 'Storage
storage Expr 'EWord
balance Maybe W64
nonce) = do
ContractCode
code' <- (forall (a :: EType). Expr a -> m (Expr a))
-> ContractCode -> m ContractCode
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> ContractCode -> m ContractCode
mapCodeM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f ContractCode
code
Expr 'Storage
storage' <- (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
storage
Expr 'EWord
balance' <- (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
balance
Expr 'EContract -> m (Expr 'EContract)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'EContract -> m (Expr 'EContract))
-> Expr 'EContract -> m (Expr 'EContract)
forall a b. (a -> b) -> a -> b
$ ContractCode
-> Expr 'Storage -> Expr 'EWord -> Maybe W64 -> Expr 'EContract
C ContractCode
code' Expr 'Storage
storage' Expr 'EWord
balance' Maybe W64
nonce
mapContractM :: Monad m => (forall a . Expr a -> m (Expr a)) -> Contract -> m (Contract)
mapContractM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> Contract -> m Contract
mapContractM forall (a :: EType). Expr a -> m (Expr a)
f Contract
c = do
ContractCode
code' <- (forall (a :: EType). Expr a -> m (Expr a))
-> ContractCode -> m ContractCode
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> ContractCode -> m ContractCode
mapCodeM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f Contract
c.code
Expr 'Storage
storage' <- (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 Contract
c.storage
Expr 'Storage
origStorage' <- (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 Contract
c.origStorage
Expr 'EWord
balance' <- (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 Contract
c.balance
Contract -> m Contract
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Contract -> m Contract) -> Contract -> m Contract
forall a b. (a -> b) -> a -> b
$ Contract
c { $sel:code:Contract :: ContractCode
code = ContractCode
code', $sel:storage:Contract :: Expr 'Storage
storage = Expr 'Storage
storage', $sel:origStorage:Contract :: Expr 'Storage
origStorage = Expr 'Storage
origStorage', $sel:balance:Contract :: Expr 'EWord
balance = Expr 'EWord
balance' }
mapCodeM :: Monad m => (forall a . Expr a -> m (Expr a)) -> ContractCode -> m (ContractCode)
mapCodeM :: forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a))
-> ContractCode -> m ContractCode
mapCodeM forall (a :: EType). Expr a -> m (Expr a)
f = \case
UnknownCode Expr 'EAddr
a -> (Expr 'EAddr -> ContractCode) -> m (Expr 'EAddr) -> m ContractCode
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr 'EAddr -> ContractCode
UnknownCode (Expr 'EAddr -> m (Expr 'EAddr)
forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EAddr
a)
c :: ContractCode
c@(RuntimeCode (ConcreteRuntimeCode ByteString
_)) -> ContractCode -> m ContractCode
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ContractCode
c
RuntimeCode (SymbolicRuntimeCode Vector (Expr 'Byte)
c) -> do
Vector (Expr 'Byte)
c' <- (Expr 'Byte -> m (Expr 'Byte))
-> Vector (Expr 'Byte) -> m (Vector (Expr 'Byte))
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) -> Vector a -> m (Vector b)
mapM ((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) Vector (Expr 'Byte)
c
ContractCode -> m ContractCode
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ContractCode -> m ContractCode)
-> (RuntimeCode -> ContractCode) -> RuntimeCode -> m ContractCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuntimeCode -> ContractCode
RuntimeCode (RuntimeCode -> m ContractCode) -> RuntimeCode -> m ContractCode
forall a b. (a -> b) -> a -> b
$ Vector (Expr 'Byte) -> RuntimeCode
SymbolicRuntimeCode Vector (Expr 'Byte)
c'
InitCode ByteString
bs Expr 'Buf
buf -> do
Expr 'Buf
buf' <- (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
buf
ContractCode -> m ContractCode
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ContractCode -> m ContractCode) -> ContractCode -> m ContractCode
forall a b. (a -> b) -> a -> b
$ ByteString -> Expr 'Buf -> ContractCode
InitCode ByteString
bs Expr 'Buf
buf'
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