Tags: measures
I have been preparing an undergraduate course on Compilers in which we build a compiler that crunches an ML-like language to X86 assembly. One of my favorite steps in the compilation is the conversion to A-Normal Form (ANF) where, informally speaking, each call or primitive operation’s arguments are immediate values, i.e. constants or variable lookups whose values can be loaded with a single machine instruction. For example, the expression
25: ((2 + 3) * (12 - 4)) * (7 + 8)
has the A-Normal Form:
31: let anf0 = 2 + 3 32: anf1 = 12 - 4 33: anf2 = anf0 * anf1 34: anf3 = 7 + 8 35: in 36: anf2 * anf3
The usual presentation of ANF conversion is very elegant but relies upon a clever use of continuations. Lets look at another perhaps simpler approach, where we can use refinements to light the way.
49: {-@ LIQUID "--no-termination" @-} 50: {-@ LIQUID "--total" @-} 51: 52: module ANF (Op (..), Expr (..), isImm, isAnf, toAnf) where 53: 54: import Control.Monad.State.Lazy 55: 56: mkLet :: [(Var, AnfExpr)] -> AnfExpr -> AnfExpr 57: imm, immExpr :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr) 58: anf :: Expr -> AnfM AnfExpr 59: 60: -- data IExpr 61: -- = IInt Int 62: -- | IVar Var 63: -- 64: -- data AExpr 65: -- = AImm IExpr 66: -- | ABin Op IExpr IExpr 67: -- | ALet Var AExpr AExpr 68: -- | ALam Var AExpr 69: -- | AApp IExpr IExpr 70: 71: type AnfExpr = Expr 72: type ImmExpr = Expr
Source Language
Lets commence by defining the source language that we wish to work with:
82: data Expr 83: = EInt Int -- ^ Integers 84: | EVar Var -- ^ Variables 85: | EBin Op Expr Expr -- ^ Binary Operators 86: | ELet Var Expr Expr -- ^ Let-binders 87: | ELam Var Expr -- ^ Function definitions 88: | EApp Expr Expr -- ^ Function applications 89: deriving ((GHC.Show.Show ANF.Expr)Show)
The language, defined by Expr has integers, variables, binary operators,
let-binders and function definitions (lambdas) and calls (applications).
In the above, Var and Op are simply:
97: type Var = String 98: 99: data Op = Plus | Minus | Times 100: deriving ((GHC.Show.Show ANF.Op)Show)
For example, the source expression above corresponds to the value:
106: -- ((2 + 3) * (12 - 4)) * (7 + 8) 107: srcExpr :: Expr 108: {VV : ANF.Expr | VV /= ANF.e1 && VV /= ANF.e2 && VV /= ANF.e2' && VV /= ANF.e3 && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false)}srcExpr = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Times 109: ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Times 110: ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Plus ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 2) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 3)) 111: ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Minus ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 12) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 4))) 112: ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Plus ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 7) ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 8))
A-Normal Form
Before we can describe a conversion to A-Normal Form (ANF), we must pin down what ANF is. Our informal description was: ``each call or primitive operation’s arguments are immediate values, i.e. constants or variable lookups’’.
We could define a brand new datatypes, say IExpr and AExpr
whose values correspond to immediate and ANF terms.
(Try it, as an exercise.) Unfortunately, doing so leads to a
bunch of code duplication, e.g. duplicate printers for Expr
and AExpr. Instead, lets see how we can use refinements to
carve out suitable subsets.
Immediate Expressions
An Expr is immediate if it is a Number or a Var;
we can formalize this as a Haskell predicate:
136: {-@ measure isImm @-} 137: isImm :: Expr -> Bool 138: x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isImm x1)}isImm (EInt _) = True 139: isImm (EVar _) = True 140: isImm _ = False
and then we can use the predicate to define a refinement type for immediate expressions:
147: {-@ type ImmExpr = {v:Expr | isImm v} @-}
For example, e1 is immediate but e2 is not:
153: {-@ e1 :: ImmExpr @-} 154: {v : ANF.Expr | Prop (isImm v)}e1 = {v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt 7 155: 156: {-@ e2 :: ImmExpr @-} 157: {v : ANF.Expr | Prop (isImm v)}e2 = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e1 e1
ANF Expressions
Similiarly, an Expr is in ANF if all arguments for operators
and applications are immediate. Once again, we can formalize
this intuition as a Haskell predicate:
167: {-@ measure isAnf @-} 168: isAnf :: Expr -> Bool 169: x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf (EInt {}) = True 170: isAnf (EVar {}) = True 171: isAnf (EBin _ e1 e2) = {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1 && Prop x2} | v == GHC.Classes.&&}&& {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e2 -- args for operators 172: isAnf (EApp e1 e2) = {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1 && Prop x2} | v == GHC.Classes.&&}&& {v : x1:ANF.Expr -> {v : GHC.Types.Bool | Prop v <=> Prop (isImm x1)} | v == isImm}isImm e2 -- must be immediate, 173: isAnf (ELet _ e1 e2) = x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e1 {v : x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x1 && Prop x2} | v == GHC.Classes.&&}&& x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e2 -- and sub-expressions 174: isAnf (ELam _ e) = x1:ANF.Expr -> {VV : GHC.Types.Bool | Prop VV <=> Prop (isAnf x1)}isAnf e -- must be in ANF
and then use the predicate to define the subset of legal ANF expressions:
180: {-@ type AnfExpr = {v:Expr | isAnf v} @-}
For example, e2 above is in ANF but e3 is not:
186: {-@ e2' :: AnfExpr @-} 187: {v : ANF.Expr | Prop (isAnf v)}e2' = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e1 e1 188: 189: {-@ e3 :: AnfExpr @-} 190: {v : ANF.Expr | Prop (isAnf v)}e3 = {v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin Plus e2' e2'
ANF Conversion: Intuition
Now that we have clearly demarcated the territories belonging to plain Expr,
immediate ImmExpr and A-Normal AnfExpr, lets see how we can convert the
former to the latter.
Recall that our goal is to convert expressions like
203: ((2 + 3) * (12 - 4)) * (7 + 8)
into
209: let anf0 = 2 + 3 210: anf1 = 12 - 4 211: anf2 = anf0 * anf1 212: anf3 = 7 + 8 213: in 214: anf2 * anf3
Generalising a bit, we want to convert
220: e1 + e2
into
226: let x1 = a1 ... xn = an 227: x1' = a1' ... xm' = am' 228: in 229: v1 + v2
where, v1 and v2 are immediate, and ai are ANF.
Making Arguments Immediate
In other words, the key requirement is a way to crunch
arbitrary argument expressions like e1 into a pair
240: ([(x1, a1) ... (xn, an)], v1)
where
a1...anareAnfExpr, andv1is an immediateImmExpr
such that e1 is equivalent to let x1 = a1 ... xn = an in v1.
Thus, we need a function
252: imm :: Expr -> ([(Var, AnfExpr)], ImmExpr)
which we will use to make arguments immediate thereby yielding a top level conversion function
259: anf :: Expr -> AnfExpr
As we need to generate “temporary” intermediate
binders, it will be convenient to work within a
monad that generates fresh variables:
267: type AnfM a = State Int a 268: 269: fresh :: AnfM Var 270: (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {VV : [GHC.Types.Char] | (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) >= 0})fresh = do 271: GHC.Types.Intn <- (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity GHC.Types.Int)get 272: GHC.Types.Int -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ())put (GHC.Types.Intnx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+1) 273: [GHC.Types.Char] -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity [GHC.Types.Char])return ([GHC.Types.Char]"anf" ++ GHC.Types.Int -> [GHC.Types.Char]show n)
Thus, the conversion functions will have the types:
279: anf :: Expr -> AnfM AnfExpr 280: imm :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr)
ANF Conversion: Code
We can now define the top-level conversion thus:
289: -------------------------------------------------------------------------------- 290: {-@ anf :: Expr -> AnfM AnfExpr @-} 291: -------------------------------------------------------------------------------- 292: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf (EInt n) = 293: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt n) 294: 295: anf (EVar x) = 296: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar x) 297: 298: anf (ELet x e1 e2) = do 299: {v : ANF.Expr | Prop (isAnf v)}a1 <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e1 300: {v : ANF.Expr | Prop (isAnf v)}a2 <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e2 301: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isAnf x2) && Prop (isAnf x3))} | v == ANF.ELet}ELet x a1 a2) 302: 303: anf (EBin o e1 e2) = do 304: (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1 305: (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2 306: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet ({v : [([GHC.Types.Char], ANF.Expr)] | len v == len b1s + len b2s}b1s ++ b2s) ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin o v1 v2)) 307: 308: anf (ELam x e) = do 309: {v : ANF.Expr | Prop (isAnf v)}a <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e 310: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ({v : [GHC.Types.Char] -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isAnf x2))} | v == ANF.ELam}ELam x a) 311: 312: anf (EApp e1 e2) = do 313: (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1 314: (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2 315: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ANF.Expr)return ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet ({v : [([GHC.Types.Char], ANF.Expr)] | len v == len b1s + len b2s}b1s ++ b2s) ({v : x1:ANF.Expr -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x1) && Prop (isImm x2))} | v == ANF.EApp}EApp v1 v2))
In anf the real work happens inside imm which takes an arbitary
argument expression and makes it immediate by generating temporary
(ANF) bindings. The resulting bindings (and immediate values) are
composed by the helper mkLet that takes a list of binders and a body
AnfExpr and stitches them into a single AnfExpr:
325: {-@ mkLet :: [(Var, AnfExpr)] -> AnfExpr -> AnfExpr @-} 326: [([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet [] {v : ANF.Expr | Prop (isAnf v)}e' = e' 327: mkLet ((x,e):bs) e' = {v : [GHC.Types.Char] -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isAnf x2) && Prop (isAnf x3))} | v == ANF.ELet}ELet x e ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})] -> {v : ANF.Expr | Prop (isAnf v)} -> {v : ANF.Expr | Prop (isAnf v)}mkLet bs e')
The arguments are made immediate by imm defined as:
333: -------------------------------------------------------------------------------- 334: {-@ imm :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr) @-} 335: -------------------------------------------------------------------------------- 336: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm (EInt n) = ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([], {v : GHC.Types.Int -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EInt}EInt n) 337: imm (EVar x) = ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([], {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar x) 338: imm e@(ELet {}) = ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr e 339: imm e@(ELam {}) = ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr e 340: imm (EBin o e1 e2) = ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && VV /= x5 && VV /= ANF.e2 && VV /= x4 && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) >= 0 && (VV : @(43)) == ((fst : func(0, [(Tuple @(43) @(44)); @(43)])) (VV : (Tuple @(45) @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (VV : @(42)) == ((snd : func(0, [(Tuple @(45) @(42)); @(42)])) (VV : (Tuple @(45) @(44))) : @(42))}))imm2 e1 e2 ({v : ANF.Op -> x2:ANF.Expr -> x3:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x2) && Prop (isImm x3))} | v == ANF.EBin}EBin o) 341: imm (EApp e1 e2) = ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && VV /= x5 && VV /= ANF.e2 && VV /= x4 && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) >= 0 && (VV : @(43)) == ((fst : func(0, [(Tuple @(43) @(44)); @(43)])) (VV : (Tuple @(45) @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (VV : @(42)) == ((snd : func(0, [(Tuple @(45) @(42)); @(42)])) (VV : (Tuple @(45) @(44))) : @(42))}))imm2 e1 e2 {v : x1:ANF.Expr -> x2:ANF.Expr -> {v : ANF.Expr | (Prop (isImm v) <=> false) && (Prop (isAnf v) <=> Prop (isImm x1) && Prop (isImm x2))} | v == ANF.EApp}EApp
Numbers and variables are already immediate, and are returned directly.
Let-binders and lambdas are simply converted to ANF, and assigned to a fresh binder:
350: {-@ immExpr :: Expr -> AnfM ([(Var, AnfExpr)], ImmExpr) @-} 351: ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))immExpr ANF.Expre = do 352: {v : ANF.Expr | Prop (isAnf v)}a <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e 353: {v : [GHC.Types.Char] | (len : func(2, [(@(0) @(1)); int])) (v : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (v : [@(0)]) >= 0}t <- fresh 354: ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return ([(t, a)], {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar t)
- Finally, binary operators and applications are converted by
imm2that takes two arbitrary expressions and an expression constructor, yielding the anf-binders and immediate expression.
362: imm2 :: Expr -> Expr -> (ImmExpr -> ImmExpr -> AnfExpr) 363: -> AnfM ([(Var, AnfExpr)], ImmExpr) 364: ANF.Expr -> ANF.Expr -> (x4:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x5:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x5 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x4 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && VV /= x5 && VV /= ANF.e2 && VV /= x4 && VV /= ANF.e1}) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ({VV : [([GHC.Types.Char], {VV : ANF.Expr | ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)})] | (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (VV : [@(0)]) >= 0 && (VV : @(43)) == ((fst : func(0, [(Tuple @(43) @(44)); @(43)])) (VV : (Tuple @(45) @(44))) : @(43))}, {VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && (VV : @(42)) == ((snd : func(0, [(Tuple @(45) @(42)); @(42)])) (VV : (Tuple @(45) @(44))) : @(42))}))imm2 ANF.Expre1 ANF.Expre2 x1:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> x2:{VV : ANF.Expr | VV /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool)} -> {VV : ANF.Expr | (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> false) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (VV : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && VV /= x2 && VV /= ANF.e2 && VV /= x1 && VV /= ANF.e1}f = do 365: (b1s, v1) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e1 366: (b2s, v2) <- ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], {v : ANF.Expr | Prop (isAnf v)})], {v : ANF.Expr | Prop (isImm v)}))imm e2 367: {v : [GHC.Types.Char] | (len : func(2, [(@(0) @(1)); int])) (v : [@(0)]) > 0 && (len : func(2, [(@(0) @(1)); int])) (v : [@(0)]) >= 0}t <- fresh 368: let [([GHC.Types.Char], ANF.Expr)]bs' = [([GHC.Types.Char], ANF.Expr)]b1s ++ [([GHC.Types.Char], ANF.Expr)]b2s ++ [(t, {v : x1:{v : ANF.Expr | v /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool)} -> x2:{v : ANF.Expr | v /= ANF.srcExpr && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool)} -> {v : ANF.Expr | (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> false) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (x1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool) && (Prop : func(0, [GHC.Types.Bool; bool])) ((isImm : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e1 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> true) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e3 : ANF.Expr) : GHC.Types.Bool)) && ((Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (v : ANF.Expr) : GHC.Types.Bool) <=> (Prop : func(0, [GHC.Types.Bool; bool])) ((isAnf : func(0, [ANF.Expr; GHC.Types.Bool])) (ANF.e2' : ANF.Expr) : GHC.Types.Bool)) && v /= x2 && v /= ANF.e2 && v /= x1 && v /= ANF.e1} | v == f}f v1 v2)] 369: ([([GHC.Types.Char], ANF.Expr)], ANF.Expr) -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity ([([GHC.Types.Char], ANF.Expr)], ANF.Expr))return (bs', {v : [GHC.Types.Char] -> {v : ANF.Expr | (Prop (isImm v) <=> true) && (Prop (isAnf v) <=> true)} | v == ANF.EVar}EVar t)
You can run it thus:
376: toAnf :: Expr -> AnfExpr 377: ANF.Expr -> ANF.ExprtoAnf ANF.Expre = GHC.Types.Int -> ANF.ExprevalState (ANF.Expr -> (Control.Monad.Trans.State.Lazy.StateT GHC.Types.Int Data.Functor.Identity.Identity {v : ANF.Expr | Prop (isAnf v)})anf e) 0
381: ghci> toAnf srcExpr 382: ELet "anf0" (EBin Plus (EInt 2) (EInt 3)) 383: (ELet "anf1" (EBin Minus (EInt 12) (EInt 4)) 384: (ELet "anf2" (EBin Times (EVar "anf0") (EVar "anf1")) 385: (ELet "anf3" (EBin Plus (EInt 7) (EInt 8)) 386: (EBin Times (EVar "anf2") (EVar "anf3")))))
which, can be pretty-printed to yield exactly the outcome desired at the top:
392: let anf0 = 2 + 3 393: anf1 = 12 - 4 394: anf2 = anf0 * anf1 395: anf3 = 7 + 8 396: in 397: anf2 * anf3
There! The refinements make this tricky conversion quite straightforward and natural, without requiring us to duplicate types and code. As an exercise, can you use refinements to:
- Port the classic continuation-based conversion ?
- Check that the conversion yields well-scoped terms ?