{-# Language DataKinds #-}

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

import Prelude hiding (Word, LT, GT)

import Control.Monad.Identity

import EVM.Types

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

-- | 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 forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr c
expr)
  where
    go :: forall a . Expr a -> b
    go :: forall (a :: EType). Expr a -> b
go = \case

      -- literals & variables

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

      -- bytes

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

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

      -- control flow

      e :: Expr a
e@(Revert [Prop]
a Expr 'Buf
b) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b)
      e :: Expr a
e@(Return [Prop]
a Expr 'Buf
b Expr 'Storage
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Buf
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'Storage
c)
      e :: Expr a
e@(ITE Expr 'EWord
a Expr 'End
b Expr 'End
c) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'EWord
a) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'End
b) forall a. Semigroup a => a -> a -> a
<> (forall (a :: EType). Expr a -> b
go Expr 'End
c)
      e :: Expr a
e@(Failure [Prop]
a Error
_) -> forall (a :: EType). Expr a -> b
f Expr a
e forall a. Semigroup a => a -> a -> a
<> (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall b.
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Prop -> b
foldProp forall (a :: EType). Expr a -> b
f) forall a. Monoid a => a
mempty [Prop]
a)

      -- integers

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

      -- booleans

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

      -- bits

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

      -- Hashes

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

      -- block context

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

      -- frame context

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

      -- code

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

      -- logs

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

      -- Contract Creation

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

      -- Calls

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

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

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

      -- storage

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

      -- buffers

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

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

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

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


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

  -- literals & variables

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

  -- bytes

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

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

  -- control flow

  Failure [Prop]
a Error
b -> do
    [Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Error -> Expr 'End
Failure [Prop]
a' Error
b)
  Revert [Prop]
a Expr 'Buf
b -> do
    [Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    Expr 'Buf
b' <- forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
    forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Expr 'Buf -> Expr 'End
Revert [Prop]
a' Expr 'Buf
b')
  Return [Prop]
a Expr 'Buf
b Expr 'Storage
c -> do
    [Prop]
a' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Prop -> m Prop
mapPropM forall (a :: EType). Expr a -> m (Expr a)
f) [Prop]
a
    Expr 'Buf
b' <- forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Buf
b
    Expr 'Storage
c' <- forall (m :: * -> *) (b :: EType).
Monad m =>
(forall (a :: EType). Expr a -> m (Expr a)) -> Expr b -> m (Expr b)
mapExprM forall (a :: EType). Expr a -> m (Expr a)
f Expr 'Storage
c
    forall (a :: EType). Expr a -> m (Expr a)
f ([Prop] -> Expr 'Buf -> Expr 'Storage -> Expr 'End
Return [Prop]
a' Expr 'Buf
b' Expr 'Storage
c')

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

  -- integers

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

  -- booleans

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

  -- bits

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


  -- Hashes

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

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

  -- block context

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

  -- frame context

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

  -- code

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

  -- logs

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

  -- Contract Creation

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

  -- Calls

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

  -- storage

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

  -- buffers

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

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

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


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


-- | 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 (b :: EType).
(forall (a :: EType). Expr a -> Expr a) -> Expr b -> Expr b
mapExpr
  foldTerm :: forall c.
Monoid c =>
(forall (b :: EType). Expr b -> c) -> c -> Expr a -> c
foldTerm = forall b (c :: EType).
Monoid b =>
(forall (a :: EType). Expr a -> b) -> b -> Expr c -> b
foldExpr

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