{-# Language DataKinds #-}
module EVM.Traversals where
import Prelude hiding (Word, LT, GT)
import Control.Monad.Identity
import EVM.Types
foldProp :: forall b . Monoid b => (forall a . Expr a -> b) -> b -> Prop -> b
foldProp :: forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f b
acc Prop
p = b
acc forall a. Semigroup a => a -> a -> a
<> (Prop -> b
go Prop
p)
where
go :: Prop -> b
go :: Prop -> b
go = \case
PBool Bool
_ -> forall a. Monoid a => a
mempty
PEq Expr a
a Expr a
b -> (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr a
a) forall a. Semigroup a => a -> a -> a
<> (forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr a
b)
PLT Expr 'EWord
a Expr 'EWord
b -> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
b
PGT Expr 'EWord
a Expr 'EWord
b -> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
b
PGEq Expr 'EWord
a Expr 'EWord
b -> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
b
PLEq Expr 'EWord
a Expr 'EWord
b -> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f forall a. Monoid a => a
mempty Expr 'EWord
a forall a. Semigroup a => a -> a -> a
<> forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr forall (a :: EType). Expr a -> b
f 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 forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b
POr Prop
a Prop
b -> Prop -> b
go Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b
PImpl Prop
a Prop
b -> Prop -> b
go Prop
a forall a. Semigroup a => a -> a -> a
<> Prop -> b
go Prop
b
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 forall a. Semigroup a => a -> a -> a
<> (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
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(LitByte Word8
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Var Text
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(GVar GVar a
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(IndexWord Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(EqByte Expr 'Byte
a Expr 'Byte
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
a) forall a. Semigroup a => a -> a -> a
<> (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)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
zero) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
one) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
two) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
three)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
four) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
five) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
six) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
seven)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
eight) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
nine) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
ten) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
eleven)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twelve) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
thirteen) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
fourteen)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
fifteen) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
sixteen) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
seventeen)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
eighteen) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
nineteen) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twenty)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyone) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentytwo) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentythree)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyfour) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyfive) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentysix)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyseven) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentyeight) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
twentynine)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
thirty) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
thirtyone)
e :: Expr a
e@(Revert [Prop]
a Expr 'Buf
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
e :: Expr a
e@(Return [Prop]
a Expr 'Buf
b Expr 'Storage
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
c)
e :: Expr a
e@(ITE Expr 'EWord
a Expr 'End
b Expr 'End
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'End
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'End
c)
e :: Expr a
e@(Failure [Prop]
a Error
_) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a)
e :: Expr a
e@(Add Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Sub Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Mul Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Div Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SDiv Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Mod Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SMod Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(AddMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
e :: Expr a
e@(MulMod Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
e :: Expr a
e@(Exp Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SEx Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Min Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Max Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(LT Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(GT Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(LEq Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(GEq Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SLT Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SGT Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Eq Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(IsZero Expr 'EWord
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
e :: Expr a
e@(And Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Or Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Xor Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Not Expr 'EWord
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
e :: Expr a
e@(SHL Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SHR Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(SAR Expr 'EWord
a Expr 'EWord
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
e :: Expr a
e@(Keccak Expr 'Buf
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
a)
e :: Expr a
e@(SHA256 Expr 'Buf
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
a)
e :: Expr a
e@(Expr a
Origin) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
Coinbase) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
Timestamp) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
BlockNumber) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
PrevRandao) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
GasLimit) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
ChainId) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
BaseFee) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(BlockHash Expr 'EWord
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
e :: Expr a
e@(Caller Int
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(CallValue Int
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Address Int
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(SelfBalance Int
_ Int
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Gas Int
_ Int
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Balance {}) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(CodeSize Expr 'EWord
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
e :: Expr a
e@(ExtCodeHash Expr 'EWord
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
e :: Expr a
e@(LogEntry Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b) forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
f [Expr 'EWord]
c))
e :: Expr a
e@(Create Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d [Expr 'Log]
g Expr 'Storage
h)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
d)
forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
go [Expr 'Log]
g))
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
h)
e :: Expr a
e@(Create2 Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'Buf
g [Expr 'Log]
h Expr 'Storage
i)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
g)
forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
go [Expr 'Log]
h))
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
i)
e :: Expr a
e@(Call Expr 'EWord
a Maybe (Expr 'EWord)
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (forall (a :: EType). Expr a -> b
go) Maybe (Expr 'EWord)
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
k)
e :: Expr a
e@(CallCode Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
k)
e :: Expr a
e@(DelegeateCall Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
g Expr 'EWord
h Expr 'EWord
i [Expr 'Log]
j Expr 'Storage
k)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
d)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
g)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
h)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
i)
forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall a. Semigroup a => a -> a -> a
(<>) forall a. Monoid a => a
mempty (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (a :: EType). Expr a -> b
go [Expr 'Log]
j))
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
k)
e :: Expr a
e@(Expr a
EmptyStore) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(ConcreteStore Map W256 (Map W256 W256)
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(Expr a
AbstractStore) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(SLoad Expr 'EWord
a Expr 'EWord
b Expr 'Storage
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
c)
e :: Expr a
e@(SStore Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Storage
d) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
d)
e :: Expr a
e@(ConcreteBuf ByteString
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(AbstractBuf Text
_) -> forall (a :: EType). Expr a -> b
f Expr a
e
e :: Expr a
e@(ReadWord Expr 'EWord
a Expr 'Buf
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
e :: Expr a
e@(ReadByte Expr 'EWord
a Expr 'Buf
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
e :: Expr a
e@(WriteWord Expr 'EWord
a Expr 'EWord
b Expr 'Buf
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
c)
e :: Expr a
e@(WriteByte Expr 'EWord
a Expr 'Byte
b Expr 'Buf
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Byte
b) forall a. Semigroup a => a -> a -> a
<> (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)
-> forall (a :: EType). Expr a -> b
f Expr a
e
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
b)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
c)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
d)
forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
g)
e :: Expr a
e@(BufLength Expr 'Buf
a) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (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 -> forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
PEq (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (forall (a :: EType). Expr a -> Expr a
f Expr a
a)) (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (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 (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (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 (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (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 (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (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 (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (forall (a :: EType). Expr a -> Expr a
f Expr 'EWord
a)) (forall (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr forall (a :: EType). Expr a -> Expr a
f (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 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 forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp 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 forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp 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 forall (a :: EType). Expr a -> Expr a
f Prop
a) ((forall (a :: EType). Expr a -> Expr a) -> Prop -> Prop
mapProp forall (a :: EType). Expr a -> Expr a
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 = forall a. Identity a -> a
runIdentity (forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall (a :: EType). Expr a -> m (Expr a)
f (W256 -> Expr 'EWord
Lit W256
a)
LitByte Word8
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Word8 -> Expr 'Byte
LitByte Word8
a)
Var Text
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Text -> Expr 'EWord
Var Text
a)
GVar GVar b
s -> forall (a :: EType). Expr a -> m (Expr a)
f (forall (a :: EType). GVar a -> Expr a
GVar GVar b
s)
IndexWord Expr 'EWord
a Expr 'EWord
b -> do
Expr 'EWord
a' <- 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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'Byte
a
Expr 'Byte
b' <- 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 'Byte
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 (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 'Byte
zero
Expr 'Byte
one' <- 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 'Byte
one
Expr 'Byte
two' <- 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 'Byte
two
Expr 'Byte
three' <- 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 'Byte
three
Expr 'Byte
four' <- 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 'Byte
four
Expr 'Byte
five' <- 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 'Byte
five
Expr 'Byte
six' <- 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 'Byte
six
Expr 'Byte
seven' <- 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 'Byte
seven
Expr 'Byte
eight' <- 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 'Byte
eight
Expr 'Byte
nine' <- 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 'Byte
nine
Expr 'Byte
ten' <- 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 'Byte
ten
Expr 'Byte
eleven' <- 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 'Byte
eleven
Expr 'Byte
twelve' <- 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 'Byte
twelve
Expr 'Byte
thirteen' <- 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 'Byte
thirteen
Expr 'Byte
fourteen' <- 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 'Byte
fourteen
Expr 'Byte
fifteen' <- 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 'Byte
fifteen
Expr 'Byte
sixteen' <- 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 'Byte
sixteen
Expr 'Byte
seventeen' <- 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 'Byte
seventeen
Expr 'Byte
eighteen' <- 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 'Byte
eighteen
Expr 'Byte
nineteen' <- 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 'Byte
nineteen
Expr 'Byte
twenty' <- 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 'Byte
twenty
Expr 'Byte
twentyone' <- 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 'Byte
twentyone
Expr 'Byte
twentytwo' <- 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 'Byte
twentytwo
Expr 'Byte
twentythree' <- 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 'Byte
twentythree
Expr 'Byte
twentyfour' <- 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 'Byte
twentyfour
Expr 'Byte
twentyfive' <- 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 'Byte
twentyfive
Expr 'Byte
twentysix' <- 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 'Byte
twentysix
Expr 'Byte
twentyseven' <- 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 'Byte
twentyseven
Expr 'Byte
twentyeight' <- 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 'Byte
twentyeight
Expr 'Byte
twentynine' <- 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 'Byte
twentynine
Expr 'Byte
thirty' <- 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 'Byte
thirty
Expr 'Byte
thirtyone' <- 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 'Byte
thirtyone
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 Error
b -> do
[Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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) [Prop]
a
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Error -> Expr 'End
Failure [Prop]
a' Error
b)
Revert [Prop]
a Expr 'Buf
b -> do
[Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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) [Prop]
a
Expr 'Buf
b' <- 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 'Buf
b
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Expr 'Buf -> Expr 'End
Revert [Prop]
a' Expr 'Buf
b')
Return [Prop]
a Expr 'Buf
b Expr 'Storage
c -> do
[Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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) [Prop]
a
Expr 'Buf
b' <- 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 'Buf
b
Expr 'Storage
c' <- 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 'Storage
c
forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Return [Prop]
a' Expr 'Buf
b' Expr 'Storage
c')
ITE Expr 'EWord
a Expr 'End
b Expr 'End
c -> do
Expr 'EWord
a' <- 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 'EWord
a
Expr 'End
b' <- 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 'End
b
Expr 'End
c' <- 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 'End
c
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
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 (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 'Buf
a
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 (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 'Buf
a
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'Buf -> Expr 'EWord
SHA256 Expr 'Buf
a')
Expr b
Origin -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
Origin
Expr b
Coinbase -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
Coinbase
Expr b
Timestamp -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
Timestamp
Expr b
BlockNumber -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
BlockNumber
Expr b
PrevRandao -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
PrevRandao
Expr b
GasLimit -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
GasLimit
Expr b
ChainId -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
ChainId
Expr b
BaseFee -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'EWord
BaseFee
BlockHash Expr 'EWord
a -> do
Expr 'EWord
a' <- 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 'EWord
a
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
BlockHash Expr 'EWord
a')
Caller Int
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
Caller Int
a)
CallValue Int
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
CallValue Int
a)
Address Int
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
Address Int
a)
SelfBalance Int
a Int
b -> forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord
SelfBalance Int
a Int
b)
Gas Int
a Int
b -> forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord
Gas Int
a Int
b)
Balance Int
a Int
b Expr 'EWord
c -> do
Expr 'EWord
c' <- forall (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 'EWord
c
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Int -> Expr 'EWord -> Expr 'EWord
Balance Int
a Int
b Expr 'EWord
c')
CodeSize Expr 'EWord
a -> do
Expr 'EWord
a' <- 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 'EWord
a
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
CodeSize Expr 'EWord
a')
ExtCodeHash Expr 'EWord
a -> do
Expr 'EWord
a' <- forall (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 'EWord
a
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord
ExtCodeHash Expr 'EWord
a')
LogEntry Expr 'EWord
a Expr 'Buf
b [Expr 'EWord]
c -> do
Expr 'EWord
a' <- 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 'EWord
a
Expr 'Buf
b' <- 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 'Buf
b
[Expr 'EWord]
c' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'EWord]
c
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')
Create Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Buf
d [Expr 'Log]
e Expr 'Storage
g -> do
Expr 'EWord
a' <- 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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'Buf
d' <- 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 'Buf
d
[Expr 'Log]
e' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'Log]
e
Expr 'Storage
g' <- 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 'Storage
g
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Create Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'Buf
d' [Expr 'Log]
e' Expr 'Storage
g')
Create2 Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'Buf
e [Expr 'Log]
g Expr 'Storage
h -> do
Expr 'EWord
a' <- forall (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'EWord
d' <- 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 'EWord
d
Expr 'Buf
e' <- 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 'Buf
e
[Expr 'Log]
g' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'Log]
g
Expr 'Storage
h' <- 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 'Storage
h
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'Buf
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Create2 Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'Buf
e' [Expr 'Log]
g' Expr 'Storage
h')
Call Expr 'EWord
a Maybe (Expr 'EWord)
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
Expr 'EWord
a' <- forall (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 'EWord
a
Maybe (Expr 'EWord)
b' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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) Maybe (Expr 'EWord)
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'EWord
d' <- 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 'EWord
d
Expr 'EWord
e' <- 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 'EWord
e
Expr 'EWord
g' <- 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 'EWord
g
Expr 'EWord
h' <- 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 'EWord
h
[Expr 'Log]
i' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'Log]
i
Expr 'Storage
j' <- 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 'Storage
j
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Maybe (Expr 'EWord)
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
Call Expr 'EWord
a' Maybe (Expr 'EWord)
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')
CallCode Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
Expr 'EWord
a' <- forall (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'EWord
d' <- 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 'EWord
d
Expr 'EWord
e' <- 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 'EWord
e
Expr 'EWord
g' <- 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 'EWord
g
Expr 'EWord
h' <- 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 'EWord
h
[Expr 'Log]
i' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'Log]
i
Expr 'Storage
j' <- 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 'Storage
j
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
CallCode Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')
DelegeateCall Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'EWord
d Expr 'EWord
e Expr 'EWord
g Expr 'EWord
h [Expr 'Log]
i Expr 'Storage
j -> do
Expr 'EWord
a' <- forall (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'EWord
d' <- 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 'EWord
d
Expr 'EWord
e' <- 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 'EWord
e
Expr 'EWord
g' <- 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 'EWord
g
Expr 'EWord
h' <- 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 'EWord
h
[Expr 'Log]
i' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 'Log]
i
Expr 'Storage
j' <- 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 'Storage
j
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> Expr 'EWord
-> [Expr 'Log]
-> Expr 'Storage
-> Expr 'EWord
DelegeateCall Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'EWord
d' Expr 'EWord
e' Expr 'EWord
g' Expr 'EWord
h' [Expr 'Log]
i' Expr 'Storage
j')
Expr b
EmptyStore -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
EmptyStore
ConcreteStore Map W256 (Map W256 W256)
a -> forall (a :: EType). Expr a -> m (Expr a)
f (Map W256 (Map W256 W256) -> Expr 'Storage
ConcreteStore Map W256 (Map W256 W256)
a)
Expr b
AbstractStore -> forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
AbstractStore
SLoad Expr 'EWord
a Expr 'EWord
b Expr 'Storage
c -> do
Expr 'EWord
a' <- 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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'Storage
c' <- 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 'Storage
c
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'EWord
SLoad Expr 'EWord
a' Expr 'EWord
b' Expr 'Storage
c')
SStore Expr 'EWord
a Expr 'EWord
b Expr 'EWord
c Expr 'Storage
d -> do
Expr 'EWord
a' <- forall (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'Storage
d' <- 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 'Storage
d
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EWord
-> Expr 'EWord -> Expr 'EWord -> Expr 'Storage -> Expr 'Storage
SStore Expr 'EWord
a' Expr 'EWord
b' Expr 'EWord
c' Expr 'Storage
d')
ConcreteBuf ByteString
a -> do
forall (a :: EType). Expr a -> m (Expr a)
f (ByteString -> Expr 'Buf
ConcreteBuf ByteString
a)
AbstractBuf Text
a -> do
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 (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 'EWord
a
Expr 'Buf
b' <- 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 'Buf
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 (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 'EWord
a
Expr 'Buf
b' <- 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 'Buf
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'Buf
c' <- 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 'Buf
c
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 (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 'EWord
a
Expr 'Byte
b' <- 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 'Byte
b
Expr 'Buf
c' <- 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 'Buf
c
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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
Expr 'EWord
c' <- 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 'EWord
c
Expr 'Buf
d' <- 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 'Buf
d
Expr 'Buf
e' <- 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 'Buf
e
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 (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 'Buf
a
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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Prop
PBool Bool
b
PEq Expr a
a Expr a
b -> do
Expr a
a' <- 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 a
a
Expr a
b' <- 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 a
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (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 'EWord
a
Expr 'EWord
b' <- 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 'EWord
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> m (Expr a)
f Prop
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop
PNeg Prop
a'
PAnd Prop
a Prop
b -> do
Prop
a' <- 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 Prop
a
Prop
b' <- 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 Prop
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PAnd Prop
a' Prop
b'
POr Prop
a Prop
b -> do
Prop
a' <- 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 Prop
a
Prop
b' <- 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 Prop
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
POr Prop
a' Prop
b'
PImpl Prop
a Prop
b -> do
Prop
a' <- 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 Prop
a
Prop
b' <- 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 Prop
b
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop -> Prop
PImpl Prop
a' Prop
b'
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 (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 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 b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp