SupGen + Fusion

supgen_fusion.txt

// Esse arquivo demonstra um caso onde fusão acelera exponencialmente o SupGen.
// Considere o tipo:
// 
//   data Tree a = Leaf a | Node (Tree a) (Tree a)
// 
// Considere a seguinte clase de funções lineares:
// 
//   F<0> : Tree a -> Tree a
//   F<0> x = x
// 
//   F<N> : Tree a -> Tree a
//   F<N> x = case F<N-1> x of
//     Leaf x   -> Leaf x
//     Node a b -> Node (F<N> &F<N>{a,b}) (F<N> &F<N>{b,a})
// 
// Por exemplo, esse é um dos programas desse espaço:
// 
//   F0 : Tree a -> Tree a
//   F0 x = x
//   
//   F1 : Tree a -> Tree a
//   F1 x = case F0 x of
//     Leaf x   -> Leaf x
//     Node a b -> Node (F1 b) (F1 a)
//   
//   F2 : Tree a -> Tree a
//   F2 x = case F1 x of
//     Leaf x   -> Leaf x
//     Node a b -> Node (F2 a) (F2 b)
// 
//   F3 : Tree a -> Tree a
//   F3 x = case F2 x of
//     Leaf x   -> Leaf x
//     Node a b -> Node (F3 b) (F3 a)
// 
// Repare que F<N> faz pattern-match em F<N-1>, analisa seu resultado, e faz
// recursão - ou seja, uma forma de composição. Cada F<N> faz recursão ou em
// (a,b), ou em (b,a), sendo o swap uma escolha sobreposta. Sendo assim, cada
// F<N> tem 2 possiveis formas diretas, e 2^N formas acumuladas (considerando
// as dependências). Semanticamente, essa família captura todas as possíveis
// funções que rotacionam uma árvore de profundidade N. Por exemplo:
// 
//   tree = (((a b) (c d)) ((e f) (g h)))
// 
//   &F1|&F2|&F3| F<3>(tree)
//   ---|---|---|------------------------------
//    0 | 0 | 0 | (((a b) (c d)) ((e f) (g h)))
//    0 | 0 | 1 | (((h g) (f e)) ((d c) (b a)))
//    0 | 1 | 0 | (((f e) (h g)) ((b a) (d c)))
//    0 | 1 | 1 | (((c d) (a b)) ((g h) (e f)))
//    1 | 0 | 0 | (((g h) (e f)) ((c d) (a b)))
//    1 | 0 | 1 | (((b a) (d c)) ((f e) (h g)))
//    1 | 1 | 0 | (((d c) (b a)) ((h g) (f e)))
//    1 | 1 | 1 | (((e f) (g h)) ((a b) (c d)))
// 
// O arquivo abaixo realiza busca de uma configuração de labels que encontre uma
// rotação específica, baseada em apenas um exemplo. O resultado é claro: com
// uma profundidade 6, enumerando a versão não-fusível (λ-encoded ou ctors), a
// busca completa em 442m interações; enumerando a versão fusível (λ-encoded), a
// busca completa em 1.9m interações.

@Y    = λ&f.f(@Y(f))
@when = λ{0:λx.&{};_:λk.λx.x}

@new = λ{
  0: λi. @L(i)
  _: λ&d. λ&i. @B(@new(d-1, i*2+0), @new(d-1, i*2+1))
}

@L = λx.λL.λB.L(x)
@B = λa.λb.λL.λB.B(a,b)

// Non-fusible version
@K0 = λ&F.λx.x
@K1 = λF0.λ&F.λx.F0(x)(λx.@L(x), λa.λb.!&F1{ax,ay}=F(a);!&F1{bx,by}=F(b);@B(&F1{ax,by},&F1{bx,ay}))
@K2 = λF1.λ&F.λx.F1(x)(λx.@L(x), λa.λb.!&F2{ax,ay}=F(a);!&F2{bx,by}=F(b);@B(&F2{ax,by},&F2{bx,ay}))
@K3 = λF2.λ&F.λx.F2(x)(λx.@L(x), λa.λb.!&F3{ax,ay}=F(a);!&F3{bx,by}=F(b);@B(&F3{ax,by},&F3{bx,ay}))
@K4 = λF3.λ&F.λx.F3(x)(λx.@L(x), λa.λb.!&F4{ax,ay}=F(a);!&F4{bx,by}=F(b);@B(&F4{ax,by},&F4{bx,ay}))
@K5 = λF4.λ&F.λx.F4(x)(λx.@L(x), λa.λb.!&F5{ax,ay}=F(a);!&F5{bx,by}=F(b);@B(&F5{ax,by},&F5{bx,ay}))
@K6 = λF5.λ&F.λx.F5(x)(λx.@L(x), λa.λb.!&F6{ax,ay}=F(a);!&F6{bx,by}=F(b);@B(&F6{ax,by},&F6{bx,ay}))
@K7 = λF6.λ&F.λx.F6(x)(λx.@L(x), λa.λb.!&F7{ax,ay}=F(a);!&F7{bx,by}=F(b);@B(&F7{ax,by},&F7{bx,ay}))
@K8 = λF7.λ&F.λx.F7(x)(λx.@L(x), λa.λb.!&F8{ax,ay}=F(a);!&F8{bx,by}=F(b);@B(&F8{ax,by},&F8{bx,ay}))

// Fusible version
@K0 = λ&F.λx.x
@K1 = λF0.λ&F.λx.λL.λB.F0(x)(λx.L(x), λa.λb.!&F1{ax,ay}=F(a);!&F1{bx,by}=F(b);B(&F1{ax,by},&F1{bx,ay}))
@K2 = λF1.λ&F.λx.λL.λB.F1(x)(λx.L(x), λa.λb.!&F2{ax,ay}=F(a);!&F2{bx,by}=F(b);B(&F2{ax,by},&F2{bx,ay}))
@K3 = λF2.λ&F.λx.λL.λB.F2(x)(λx.L(x), λa.λb.!&F3{ax,ay}=F(a);!&F3{bx,by}=F(b);B(&F3{ax,by},&F3{bx,ay}))
@K4 = λF3.λ&F.λx.λL.λB.F3(x)(λx.L(x), λa.λb.!&F4{ax,ay}=F(a);!&F4{bx,by}=F(b);B(&F4{ax,by},&F4{bx,ay}))
@K5 = λF4.λ&F.λx.λL.λB.F4(x)(λx.L(x), λa.λb.!&F5{ax,ay}=F(a);!&F5{bx,by}=F(b);B(&F5{ax,by},&F5{bx,ay}))
@K6 = λF5.λ&F.λx.λL.λB.F5(x)(λx.L(x), λa.λb.!&F6{ax,ay}=F(a);!&F6{bx,by}=F(b);B(&F6{ax,by},&F6{bx,ay}))
@K7 = λF6.λ&F.λx.λL.λB.F6(x)(λx.L(x), λa.λb.!&F7{ax,ay}=F(a);!&F7{bx,by}=F(b);B(&F7{ax,by},&F7{bx,ay}))
@K8 = λF7.λ&F.λx.λL.λB.F7(x)(λx.L(x), λa.λb.!&F8{ax,ay}=F(a);!&F8{bx,by}=F(b);B(&F8{ax,by},&F8{bx,ay}))

//// Fusible version (equal alternative)
//@K0 = λ&F.λx.x
//@K1 = λF0.λ&F.λx.λL.λ&B.F0(x)(λx.L(x), λa.λb.!&F1{Bx,By}=B;!&F1{ax,ay}=F(a);!&F1{bx,by}=F(b);&F1{Bx(ax,bx),By(by,ay)})
//@K2 = λF1.λ&F.λx.λL.λ&B.F1(x)(λx.L(x), λa.λb.!&F2{Bx,By}=B;!&F2{ax,ay}=F(a);!&F2{bx,by}=F(b);&F2{Bx(ax,bx),By(by,ay)})
//@K3 = λF2.λ&F.λx.λL.λ&B.F2(x)(λx.L(x), λa.λb.!&F3{Bx,By}=B;!&F3{ax,ay}=F(a);!&F3{bx,by}=F(b);&F3{Bx(ax,bx),By(by,ay)})
//@K4 = λF3.λ&F.λx.λL.λ&B.F3(x)(λx.L(x), λa.λb.!&F4{Bx,By}=B;!&F4{ax,ay}=F(a);!&F4{bx,by}=F(b);&F4{Bx(ax,bx),By(by,ay)})
//@K5 = λF4.λ&F.λx.λL.λ&B.F4(x)(λx.L(x), λa.λb.!&F5{Bx,By}=B;!&F5{ax,ay}=F(a);!&F5{bx,by}=F(b);&F5{Bx(ax,bx),By(by,ay)})
//@K6 = λF5.λ&F.λx.λL.λ&B.F5(x)(λx.L(x), λa.λb.!&F6{Bx,By}=B;!&F6{ax,ay}=F(a);!&F6{bx,by}=F(b);&F6{Bx(ax,bx),By(by,ay)})
//@K7 = λF6.λ&F.λx.λL.λ&B.F6(x)(λx.L(x), λa.λb.!&F7{Bx,By}=B;!&F7{ax,ay}=F(a);!&F7{bx,by}=F(b);&F7{Bx(ax,bx),By(by,ay)})
//@K8 = λF7.λ&F.λx.λL.λ&B.F7(x)(λx.L(x), λa.λb.!&F8{Bx,By}=B;!&F8{ax,ay}=F(a);!&F8{bx,by}=F(b);&F8{Bx(ax,bx),By(by,ay)})

//// Fusible version (slower alternative)
//@K0 = λ&F.λx.x
//@K1 = λF0.λ&F.λx.λL.λB.F0(x)(λx.L(x), λa.λb.!&F1{&fx,&fy}=F;!&F1{ax,ay}=a;!&F1{bx,by}=b;B(&F1{fx(ax),fy(by)},&F1{fx(bx),fy(ay)}))
//@K2 = λF1.λ&F.λx.λL.λB.F1(x)(λx.L(x), λa.λb.!&F2{&fx,&fy}=F;!&F2{ax,ay}=a;!&F2{bx,by}=b;B(&F2{fx(ax),fy(by)},&F2{fx(bx),fy(ay)}))
//@K3 = λF2.λ&F.λx.λL.λB.F2(x)(λx.L(x), λa.λb.!&F3{&fx,&fy}=F;!&F3{ax,ay}=a;!&F3{bx,by}=b;B(&F3{fx(ax),fy(by)},&F3{fx(bx),fy(ay)}))
//@K4 = λF3.λ&F.λx.λL.λB.F3(x)(λx.L(x), λa.λb.!&F4{&fx,&fy}=F;!&F4{ax,ay}=a;!&F4{bx,by}=b;B(&F4{fx(ax),fy(by)},&F4{fx(bx),fy(ay)}))
//@K5 = λF4.λ&F.λx.λL.λB.F4(x)(λx.L(x), λa.λb.!&F5{&fx,&fy}=F;!&F5{ax,ay}=a;!&F5{bx,by}=b;B(&F5{fx(ax),fy(by)},&F5{fx(bx),fy(ay)}))
//@K6 = λF5.λ&F.λx.λL.λB.F5(x)(λx.L(x), λa.λb.!&F6{&fx,&fy}=F;!&F6{ax,ay}=a;!&F6{bx,by}=b;B(&F6{fx(ax),fy(by)},&F6{fx(bx),fy(ay)}))
//@K7 = λF6.λ&F.λx.λL.λB.F6(x)(λx.L(x), λa.λb.!&F7{&fx,&fy}=F;!&F7{ax,ay}=a;!&F7{bx,by}=b;B(&F7{fx(ax),fy(by)},&F7{fx(bx),fy(ay)}))
//@K8 = λF7.λ&F.λx.λL.λB.F7(x)(λx.L(x), λa.λb.!&F8{&fx,&fy}=F;!&F8{ax,ay}=a;!&F8{bx,by}=b;B(&F8{fx(ax),fy(by)},&F8{fx(bx),fy(ay)}))

//// Fusible version (slower alternative)
//@K0 = λ&F.λx.x
//@K1 = λF0.λ&F.λx.λL.λB.F0(x)(λx.L(x), λa.λb.!&F1{Bx,By}=B;!&F1{&fx,&fy}=F;!&F1{ax,ay}=a;!&F1{bx,by}=b;&F1{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K2 = λF1.λ&F.λx.λL.λB.F1(x)(λx.L(x), λa.λb.!&F2{Bx,By}=B;!&F2{&fx,&fy}=F;!&F2{ax,ay}=a;!&F2{bx,by}=b;&F2{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K3 = λF2.λ&F.λx.λL.λB.F2(x)(λx.L(x), λa.λb.!&F3{Bx,By}=B;!&F3{&fx,&fy}=F;!&F3{ax,ay}=a;!&F3{bx,by}=b;&F3{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K4 = λF3.λ&F.λx.λL.λB.F3(x)(λx.L(x), λa.λb.!&F4{Bx,By}=B;!&F4{&fx,&fy}=F;!&F4{ax,ay}=a;!&F4{bx,by}=b;&F4{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K5 = λF4.λ&F.λx.λL.λB.F4(x)(λx.L(x), λa.λb.!&F5{Bx,By}=B;!&F5{&fx,&fy}=F;!&F5{ax,ay}=a;!&F5{bx,by}=b;&F5{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K6 = λF5.λ&F.λx.λL.λB.F5(x)(λx.L(x), λa.λb.!&F6{Bx,By}=B;!&F6{&fx,&fy}=F;!&F6{ax,ay}=a;!&F6{bx,by}=b;&F6{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K7 = λF6.λ&F.λx.λL.λB.F6(x)(λx.L(x), λa.λb.!&F7{Bx,By}=B;!&F7{&fx,&fy}=F;!&F7{ax,ay}=a;!&F7{bx,by}=b;&F7{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})
//@K8 = λF7.λ&F.λx.λL.λB.F7(x)(λx.L(x), λa.λb.!&F8{Bx,By}=B;!&F8{&fx,&fy}=F;!&F8{ax,ay}=a;!&F8{bx,by}=b;&F8{Bx(fx(ax),fx(bx)),By(fy(by),fy(ay))})

@F0 = @Y(@K0)
@F1 = @Y(@K1(@F0))
@F2 = @Y(@K2(@F1))
@F3 = @Y(@K3(@F2))
@F4 = @Y(@K4(@F3))
@F5 = @Y(@K5(@F4))
@F6 = @Y(@K6(@F5))
@F7 = @Y(@K7(@F6))
@F8 = @Y(@K8(@F7))

// Target term
//@targ = λa.λb.b(λc.λd.d(λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(97),λq.λr.q(96)),λo.λp.p(λq.λr.q(99),λq.λr.q(98))),λm.λn.n(λo.λp.p(λq.λr.q(101),λq.λr.q(100)),λo.λp.p(λq.λr.q(103),λq.λr.q(102)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(105),λq.λr.q(104)),λo.λp.p(λq.λr.q(107),λq.λr.q(106))),λm.λn.n(λo.λp.p(λq.λr.q(109),λq.λr.q(108)),λo.λp.p(λq.λr.q(111),λq.λr.q(110))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(113),λq.λr.q(112)),λo.λp.p(λq.λr.q(115),λq.λr.q(114))),λm.λn.n(λo.λp.p(λq.λr.q(117),λq.λr.q(116)),λo.λp.p(λq.λr.q(119),λq.λr.q(118)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(121),λq.λr.q(120)),λo.λp.p(λq.λr.q(123),λq.λr.q(122))),λm.λn.n(λo.λp.p(λq.λr.q(125),λq.λr.q(124)),λo.λp.p(λq.λr.q(127),λq.λr.q(126)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(65),λq.λr.q(64)),λo.λp.p(λq.λr.q(67),λq.λr.q(66))),λm.λn.n(λo.λp.p(λq.λr.q(69),λq.λr.q(68)),λo.λp.p(λq.λr.q(71),λq.λr.q(70)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(73),λq.λr.q(72)),λo.λp.p(λq.λr.q(75),λq.λr.q(74))),λm.λn.n(λo.λp.p(λq.λr.q(77),λq.λr.q(76)),λo.λp.p(λq.λr.q(79),λq.λr.q(78))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(81),λq.λr.q(80)),λo.λp.p(λq.λr.q(83),λq.λr.q(82))),λm.λn.n(λo.λp.p(λq.λr.q(85),λq.λr.q(84)),λo.λp.p(λq.λr.q(87),λq.λr.q(86)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(89),λq.λr.q(88)),λo.λp.p(λq.λr.q(91),λq.λr.q(90))),λm.λn.n(λo.λp.p(λq.λr.q(93),λq.λr.q(92)),λo.λp.p(λq.λr.q(95),λq.λr.q(94))))))),λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(33),λq.λr.q(32)),λo.λp.p(λq.λr.q(35),λq.λr.q(34))),λm.λn.n(λo.λp.p(λq.λr.q(37),λq.λr.q(36)),λo.λp.p(λq.λr.q(39),λq.λr.q(38)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(41),λq.λr.q(40)),λo.λp.p(λq.λr.q(43),λq.λr.q(42))),λm.λn.n(λo.λp.p(λq.λr.q(45),λq.λr.q(44)),λo.λp.p(λq.λr.q(47),λq.λr.q(46))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(49),λq.λr.q(48)),λo.λp.p(λq.λr.q(51),λq.λr.q(50))),λm.λn.n(λo.λp.p(λq.λr.q(53),λq.λr.q(52)),λo.λp.p(λq.λr.q(55),λq.λr.q(54)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(57),λq.λr.q(56)),λo.λp.p(λq.λr.q(59),λq.λr.q(58))),λm.λn.n(λo.λp.p(λq.λr.q(61),λq.λr.q(60)),λo.λp.p(λq.λr.q(63),λq.λr.q(62)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(1),λq.λr.q(0)),λo.λp.p(λq.λr.q(3),λq.λr.q(2))),λm.λn.n(λo.λp.p(λq.λr.q(5),λq.λr.q(4)),λo.λp.p(λq.λr.q(7),λq.λr.q(6)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(9),λq.λr.q(8)),λo.λp.p(λq.λr.q(11),λq.λr.q(10))),λm.λn.n(λo.λp.p(λq.λr.q(13),λq.λr.q(12)),λo.λp.p(λq.λr.q(15),λq.λr.q(14))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(17),λq.λr.q(16)),λo.λp.p(λq.λr.q(19),λq.λr.q(18))),λm.λn.n(λo.λp.p(λq.λr.q(21),λq.λr.q(20)),λo.λp.p(λq.λr.q(23),λq.λr.q(22)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(25),λq.λr.q(24)),λo.λp.p(λq.λr.q(27),λq.λr.q(26))),λm.λn.n(λo.λp.p(λq.λr.q(29),λq.λr.q(28)),λo.λp.p(λq.λr.q(31),λq.λr.q(30)))))))),λc.λd.d(λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(225),λq.λr.q(224)),λo.λp.p(λq.λr.q(227),λq.λr.q(226))),λm.λn.n(λo.λp.p(λq.λr.q(229),λq.λr.q(228)),λo.λp.p(λq.λr.q(231),λq.λr.q(230)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(233),λq.λr.q(232)),λo.λp.p(λq.λr.q(235),λq.λr.q(234))),λm.λn.n(λo.λp.p(λq.λr.q(237),λq.λr.q(236)),λo.λp.p(λq.λr.q(239),λq.λr.q(238))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(241),λq.λr.q(240)),λo.λp.p(λq.λr.q(243),λq.λr.q(242))),λm.λn.n(λo.λp.p(λq.λr.q(245),λq.λr.q(244)),λo.λp.p(λq.λr.q(247),λq.λr.q(246)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(249),λq.λr.q(248)),λo.λp.p(λq.λr.q(251),λq.λr.q(250))),λm.λn.n(λo.λp.p(λq.λr.q(253),λq.λr.q(252)),λo.λp.p(λq.λr.q(255),λq.λr.q(254)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(193),λq.λr.q(192)),λo.λp.p(λq.λr.q(195),λq.λr.q(194))),λm.λn.n(λo.λp.p(λq.λr.q(197),λq.λr.q(196)),λo.λp.p(λq.λr.q(199),λq.λr.q(198)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(201),λq.λr.q(200)),λo.λp.p(λq.λr.q(203),λq.λr.q(202))),λm.λn.n(λo.λp.p(λq.λr.q(205),λq.λr.q(204)),λo.λp.p(λq.λr.q(207),λq.λr.q(206))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(209),λq.λr.q(208)),λo.λp.p(λq.λr.q(211),λq.λr.q(210))),λm.λn.n(λo.λp.p(λq.λr.q(213),λq.λr.q(212)),λo.λp.p(λq.λr.q(215),λq.λr.q(214)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(217),λq.λr.q(216)),λo.λp.p(λq.λr.q(219),λq.λr.q(218))),λm.λn.n(λo.λp.p(λq.λr.q(221),λq.λr.q(220)),λo.λp.p(λq.λr.q(223),λq.λr.q(222))))))),λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(161),λq.λr.q(160)),λo.λp.p(λq.λr.q(163),λq.λr.q(162))),λm.λn.n(λo.λp.p(λq.λr.q(165),λq.λr.q(164)),λo.λp.p(λq.λr.q(167),λq.λr.q(166)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(169),λq.λr.q(168)),λo.λp.p(λq.λr.q(171),λq.λr.q(170))),λm.λn.n(λo.λp.p(λq.λr.q(173),λq.λr.q(172)),λo.λp.p(λq.λr.q(175),λq.λr.q(174))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(177),λq.λr.q(176)),λo.λp.p(λq.λr.q(179),λq.λr.q(178))),λm.λn.n(λo.λp.p(λq.λr.q(181),λq.λr.q(180)),λo.λp.p(λq.λr.q(183),λq.λr.q(182)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(185),λq.λr.q(184)),λo.λp.p(λq.λr.q(187),λq.λr.q(186))),λm.λn.n(λo.λp.p(λq.λr.q(189),λq.λr.q(188)),λo.λp.p(λq.λr.q(191),λq.λr.q(190)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(129),λq.λr.q(128)),λo.λp.p(λq.λr.q(131),λq.λr.q(130))),λm.λn.n(λo.λp.p(λq.λr.q(133),λq.λr.q(132)),λo.λp.p(λq.λr.q(135),λq.λr.q(134)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(137),λq.λr.q(136)),λo.λp.p(λq.λr.q(139),λq.λr.q(138))),λm.λn.n(λo.λp.p(λq.λr.q(141),λq.λr.q(140)),λo.λp.p(λq.λr.q(143),λq.λr.q(142))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(145),λq.λr.q(144)),λo.λp.p(λq.λr.q(147),λq.λr.q(146))),λm.λn.n(λo.λp.p(λq.λr.q(149),λq.λr.q(148)),λo.λp.p(λq.λr.q(151),λq.λr.q(150)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(153),λq.λr.q(152)),λo.λp.p(λq.λr.q(155),λq.λr.q(154))),λm.λn.n(λo.λp.p(λq.λr.q(157),λq.λr.q(156)),λo.λp.p(λq.λr.q(159),λq.λr.q(158)))))))))
@targ = λa.λb.b(λc.λd.d(λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(82),λq.λr.q(83)),λo.λp.p(λq.λr.q(80),λq.λr.q(81))),λm.λn.n(λo.λp.p(λq.λr.q(86),λq.λr.q(87)),λo.λp.p(λq.λr.q(84),λq.λr.q(85)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(90),λq.λr.q(91)),λo.λp.p(λq.λr.q(88),λq.λr.q(89))),λm.λn.n(λo.λp.p(λq.λr.q(94),λq.λr.q(95)),λo.λp.p(λq.λr.q(92),λq.λr.q(93))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(66),λq.λr.q(67)),λo.λp.p(λq.λr.q(64),λq.λr.q(65))),λm.λn.n(λo.λp.p(λq.λr.q(70),λq.λr.q(71)),λo.λp.p(λq.λr.q(68),λq.λr.q(69)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(74),λq.λr.q(75)),λo.λp.p(λq.λr.q(72),λq.λr.q(73))),λm.λn.n(λo.λp.p(λq.λr.q(78),λq.λr.q(79)),λo.λp.p(λq.λr.q(76),λq.λr.q(77)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(114),λq.λr.q(115)),λo.λp.p(λq.λr.q(112),λq.λr.q(113))),λm.λn.n(λo.λp.p(λq.λr.q(118),λq.λr.q(119)),λo.λp.p(λq.λr.q(116),λq.λr.q(117)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(122),λq.λr.q(123)),λo.λp.p(λq.λr.q(120),λq.λr.q(121))),λm.λn.n(λo.λp.p(λq.λr.q(126),λq.λr.q(127)),λo.λp.p(λq.λr.q(124),λq.λr.q(125))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(98),λq.λr.q(99)),λo.λp.p(λq.λr.q(96),λq.λr.q(97))),λm.λn.n(λo.λp.p(λq.λr.q(102),λq.λr.q(103)),λo.λp.p(λq.λr.q(100),λq.λr.q(101)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(106),λq.λr.q(107)),λo.λp.p(λq.λr.q(104),λq.λr.q(105))),λm.λn.n(λo.λp.p(λq.λr.q(110),λq.λr.q(111)),λo.λp.p(λq.λr.q(108),λq.λr.q(109))))))),λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(18),λq.λr.q(19)),λo.λp.p(λq.λr.q(16),λq.λr.q(17))),λm.λn.n(λo.λp.p(λq.λr.q(22),λq.λr.q(23)),λo.λp.p(λq.λr.q(20),λq.λr.q(21)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(26),λq.λr.q(27)),λo.λp.p(λq.λr.q(24),λq.λr.q(25))),λm.λn.n(λo.λp.p(λq.λr.q(30),λq.λr.q(31)),λo.λp.p(λq.λr.q(28),λq.λr.q(29))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(2),λq.λr.q(3)),λo.λp.p(λq.λr.q(0),λq.λr.q(1))),λm.λn.n(λo.λp.p(λq.λr.q(6),λq.λr.q(7)),λo.λp.p(λq.λr.q(4),λq.λr.q(5)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(10),λq.λr.q(11)),λo.λp.p(λq.λr.q(8),λq.λr.q(9))),λm.λn.n(λo.λp.p(λq.λr.q(14),λq.λr.q(15)),λo.λp.p(λq.λr.q(12),λq.λr.q(13)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(50),λq.λr.q(51)),λo.λp.p(λq.λr.q(48),λq.λr.q(49))),λm.λn.n(λo.λp.p(λq.λr.q(54),λq.λr.q(55)),λo.λp.p(λq.λr.q(52),λq.λr.q(53)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(58),λq.λr.q(59)),λo.λp.p(λq.λr.q(56),λq.λr.q(57))),λm.λn.n(λo.λp.p(λq.λr.q(62),λq.λr.q(63)),λo.λp.p(λq.λr.q(60),λq.λr.q(61))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(34),λq.λr.q(35)),λo.λp.p(λq.λr.q(32),λq.λr.q(33))),λm.λn.n(λo.λp.p(λq.λr.q(38),λq.λr.q(39)),λo.λp.p(λq.λr.q(36),λq.λr.q(37)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(42),λq.λr.q(43)),λo.λp.p(λq.λr.q(40),λq.λr.q(41))),λm.λn.n(λo.λp.p(λq.λr.q(46),λq.λr.q(47)),λo.λp.p(λq.λr.q(44),λq.λr.q(45)))))))),λc.λd.d(λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(210),λq.λr.q(211)),λo.λp.p(λq.λr.q(208),λq.λr.q(209))),λm.λn.n(λo.λp.p(λq.λr.q(214),λq.λr.q(215)),λo.λp.p(λq.λr.q(212),λq.λr.q(213)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(218),λq.λr.q(219)),λo.λp.p(λq.λr.q(216),λq.λr.q(217))),λm.λn.n(λo.λp.p(λq.λr.q(222),λq.λr.q(223)),λo.λp.p(λq.λr.q(220),λq.λr.q(221))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(194),λq.λr.q(195)),λo.λp.p(λq.λr.q(192),λq.λr.q(193))),λm.λn.n(λo.λp.p(λq.λr.q(198),λq.λr.q(199)),λo.λp.p(λq.λr.q(196),λq.λr.q(197)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(202),λq.λr.q(203)),λo.λp.p(λq.λr.q(200),λq.λr.q(201))),λm.λn.n(λo.λp.p(λq.λr.q(206),λq.λr.q(207)),λo.λp.p(λq.λr.q(204),λq.λr.q(205)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(242),λq.λr.q(243)),λo.λp.p(λq.λr.q(240),λq.λr.q(241))),λm.λn.n(λo.λp.p(λq.λr.q(246),λq.λr.q(247)),λo.λp.p(λq.λr.q(244),λq.λr.q(245)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(250),λq.λr.q(251)),λo.λp.p(λq.λr.q(248),λq.λr.q(249))),λm.λn.n(λo.λp.p(λq.λr.q(254),λq.λr.q(255)),λo.λp.p(λq.λr.q(252),λq.λr.q(253))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(226),λq.λr.q(227)),λo.λp.p(λq.λr.q(224),λq.λr.q(225))),λm.λn.n(λo.λp.p(λq.λr.q(230),λq.λr.q(231)),λo.λp.p(λq.λr.q(228),λq.λr.q(229)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(234),λq.λr.q(235)),λo.λp.p(λq.λr.q(232),λq.λr.q(233))),λm.λn.n(λo.λp.p(λq.λr.q(238),λq.λr.q(239)),λo.λp.p(λq.λr.q(236),λq.λr.q(237))))))),λe.λf.f(λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(146),λq.λr.q(147)),λo.λp.p(λq.λr.q(144),λq.λr.q(145))),λm.λn.n(λo.λp.p(λq.λr.q(150),λq.λr.q(151)),λo.λp.p(λq.λr.q(148),λq.λr.q(149)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(154),λq.λr.q(155)),λo.λp.p(λq.λr.q(152),λq.λr.q(153))),λm.λn.n(λo.λp.p(λq.λr.q(158),λq.λr.q(159)),λo.λp.p(λq.λr.q(156),λq.λr.q(157))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(130),λq.λr.q(131)),λo.λp.p(λq.λr.q(128),λq.λr.q(129))),λm.λn.n(λo.λp.p(λq.λr.q(134),λq.λr.q(135)),λo.λp.p(λq.λr.q(132),λq.λr.q(133)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(138),λq.λr.q(139)),λo.λp.p(λq.λr.q(136),λq.λr.q(137))),λm.λn.n(λo.λp.p(λq.λr.q(142),λq.λr.q(143)),λo.λp.p(λq.λr.q(140),λq.λr.q(141)))))),λg.λh.h(λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(178),λq.λr.q(179)),λo.λp.p(λq.λr.q(176),λq.λr.q(177))),λm.λn.n(λo.λp.p(λq.λr.q(182),λq.λr.q(183)),λo.λp.p(λq.λr.q(180),λq.λr.q(181)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(186),λq.λr.q(187)),λo.λp.p(λq.λr.q(184),λq.λr.q(185))),λm.λn.n(λo.λp.p(λq.λr.q(190),λq.λr.q(191)),λo.λp.p(λq.λr.q(188),λq.λr.q(189))))),λi.λj.j(λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(162),λq.λr.q(163)),λo.λp.p(λq.λr.q(160),λq.λr.q(161))),λm.λn.n(λo.λp.p(λq.λr.q(166),λq.λr.q(167)),λo.λp.p(λq.λr.q(164),λq.λr.q(165)))),λk.λl.l(λm.λn.n(λo.λp.p(λq.λr.q(170),λq.λr.q(171)),λo.λp.p(λq.λr.q(168),λq.λr.q(169))),λm.λn.n(λo.λp.p(λq.λr.q(174),λq.λr.q(175)),λo.λp.p(λq.λr.q(172),λq.λr.q(173)))))))))

// Synth and output labels
@main =
  ! ok = @F8(@new(8, 0)) === @targ
  ! ls = [&F1{0,1}, &F2{0,1}, &F3{0,1}, &F4{0,1}, &F5{0,1}, &F6{0,1}]
  @when(ok, ls)

//@main = @F8(@new(8, 0))