{- |
    Module: EVM.Traversals
    Description: Generic traversal functions for Expr datatypes
-}
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

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

      -- literals & variables

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

      -- contracts

      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

      -- bytes

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

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

      -- control flow

      e :: Expr a
e@(Success [Prop]
a Traces
_ 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)

      -- integers

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

      -- booleans

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

      -- bits

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

      -- Hashes

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

      -- block context

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

      -- tx context

      e :: Expr a
e@(Expr a
TxValue) -> Expr a -> b
forall (a :: EType). Expr a -> b
f Expr a
e

      -- frame context

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

      -- code

      e :: Expr a
e@(CodeSize Expr '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)

      -- logs

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

      -- storage

      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

      -- storage

      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
_ Maybe W256
_) -> 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)

      -- buffers

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

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

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

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

  -- literals & variables

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

  -- addresses

  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

  -- addresses

  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')

  -- bytes

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

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

  -- control flow

  Failure [Prop]
a Traces
b EvmError
c -> do
    [Prop]
a' <- (Prop -> m Prop) -> [Prop] -> m [Prop]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM Expr a -> m (Expr a)
forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    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')

  -- integers

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

  -- booleans

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

  -- bits

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


  -- Hashes

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

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

  -- block context

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

  -- tx context

  Expr b
TxValue -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f Expr b
Expr 'EWord
TxValue

  -- frame context

  Gas Int
a -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Int -> Expr 'EWord
Gas Int
a)
  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')

  -- code

  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')

  -- logs

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

  -- storage

  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 Maybe W256
b -> Expr b -> m (Expr b)
forall (a :: EType). Expr a -> m (Expr a)
f (Expr 'EAddr -> Maybe W256 -> Expr 'Storage
AbstractStore Expr 'EAddr
a Maybe W256
b)
  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')

  -- buffers

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

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

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

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


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'

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

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

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