liquid-fixpoint-0.9.6.3.4: tests/pos/LogicCurry1.hs.fq
fixpoint "--allowho"
qualif Fst(v : @(1), y : @(0)) { (v = (fst y)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.spec" (line 28, column 8)
qualif Snd(v : @(1), y : @(0)) { (v = (snd y)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.spec" (line 29, column 8)
qualif Auto(v##1 : int, n : int, x : int) { (v##1 = (ack n x)) } // "/Users/rjhala/research/stack/liquidhaskell/tests/pos/LogicCurry1.hs" (line 10, column 1)
qualif IsEmp(v : GHC.Types.Bool, xs : [@(0)]) { (v <=> ((len xs) > 0)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 13, column 8)
qualif IsEmp(v : GHC.Types.Bool, xs : [@(0)]) { (v <=> ((len xs) = 0)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 14, column 8)
qualif ListZ(v : [@(0)]) { ((len v) = 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 16, column 8)
qualif ListZ(v : [@(0)]) { ((len v) >= 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 17, column 8)
qualif ListZ(v : [@(0)]) { ((len v) > 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 18, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]) { ((len v) = (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 20, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]) { ((len v) >= (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 21, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]) { ((len v) > (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 22, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]) { ((len v) <= (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 23, column 8)
qualif CmpLen(v : [@(1)], xs : [@(0)]) { ((len v) < (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 24, column 8)
qualif EqLen(v : int, xs : [@(0)]) { (v = (len xs)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 26, column 8)
qualif LenEq(v : [@(0)], x : int) { (x = (len v)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 27, column 8)
qualif LenDiff(v : [@(0)], x : int) { ((len v) = (x + 1)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 28, column 8)
qualif LenDiff(v : [@(0)], x : int) { ((len v) = (x - 1)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 29, column 8)
qualif LenAcc(v : int, xs : [@(0)], n : int) { (v = ((len xs) + n)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/GHC/Base.hquals" (line 30, column 8)
qualif Bot(v : @(0)) { (0 = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 3, column 8)
qualif Bot(v : @(0)) { (0 = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 4, column 8)
qualif Bot(v : @(0)) { (0 = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 5, column 8)
qualif Bot(v : bool) { (0 = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 6, column 8)
qualif Bot(v : int) { (0 = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 7, column 8)
qualif CmpZ(v : @(0)) { (v < 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 9, column 8)
qualif CmpZ(v : @(0)) { (v <= 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 10, column 8)
qualif CmpZ(v : @(0)) { (v > 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 11, column 8)
qualif CmpZ(v : @(0)) { (v >= 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 12, column 8)
qualif CmpZ(v : @(0)) { (v = 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 13, column 8)
qualif CmpZ(v : @(0)) { (v != 0) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 14, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v < x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 16, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v <= x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 17, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v > x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 18, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v >= x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 19, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v = x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 20, column 8)
qualif Cmp(v : @(0), x : @(0)) { (v != x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 21, column 8)
qualif One(v : int) { (v = 1) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 28, column 8)
qualif True1(v : GHC.Types.Bool) { v } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 29, column 8)
qualif False1(v : GHC.Types.Bool) { (~ (v)) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 30, column 8)
qualif Papp(v : @(0), p : (Pred @(0))) { (papp1 p v) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 34, column 8)
qualif Papp2(v : @(1), x : @(0), p : (Pred @(1) @(0))) { (papp2 p v x) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 37, column 8)
qualif Papp3(v : @(2), x : @(0), y : @(1), p : (Pred @(2) @(0) @(1))) { (papp3 p v x y) } // "/Users/rjhala/research/stack/liquidhaskell/.stack-work/install/x86_64-osx/nightly-2016-05-21/7.10.3/share/x86_64-osx-ghc-7.10.3/liquidhaskell-0.6.0.0/include/Prelude.hquals" (line 39, column 8)
constant runFun : (func(2, [(Arrow @(0) @(1)); @(0); @(1)]))
constant addrLen : (func(0, [Str; int]))
constant papp5 : (func(10, [(Pred @(0) @(1) @(2) @(3) @(4));
@(5);
@(6);
@(7);
@(8);
@(9);
bool]))
constant x_Tuple21 : (func(2, [(Tuple @(0) @(1)); @(0)]))
constant GHC.Types.False##68 : (bool)
constant x_Tuple65 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(4)]))
constant x_Tuple55 : (func(5, [(Tuple @(0) @(1) @(2) @(3) @(4));
@(4)]))
constant x_Tuple33 : (func(3, [(Tuple @(0) @(1) @(2)); @(2)]))
constant x_Tuple77 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(6)]))
constant papp3 : (func(6, [(Pred @(0) @(1) @(2));
@(3);
@(4);
@(5);
bool]))
constant GHC.Types.True##6u : (bool)
constant x_Tuple63 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(2)]))
constant x_Tuple41 : (func(4, [(Tuple @(0) @(1) @(2) @(3));
@(0)]))
constant GHC.Types.LT##6S : (GHC.Types.Ordering)
constant papp4 : (func(8, [(Pred @(0) @(1) @(2) @(3));
@(4);
@(5);
@(6);
@(7);
bool]))
constant x_Tuple64 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(3)]))
constant GHC.Types.GT##6W : (GHC.Types.Ordering)
constant autolen : (func(1, [@(0); int]))
constant x_Tuple52 : (func(5, [(Tuple @(0) @(1) @(2) @(3) @(4));
@(1)]))
constant head : (func(1, [[@(0)]; @(0)]))
constant null : (func(1, [[@(0)]; bool]))
constant papp2 : (func(4, [(Pred @(0) @(1)); @(2); @(3); bool]))
constant x_Tuple62 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(1)]))
constant fromJust : (func(1, [(GHC.Base.Maybe @(0)); @(0)]))
constant papp7 : (func(14, [(Pred @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(7);
@(8);
@(9);
@(10);
@(11);
@(12);
@(13);
bool]))
constant x_Tuple53 : (func(5, [(Tuple @(0) @(1) @(2) @(3) @(4));
@(2)]))
constant x_Tuple71 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(0)]))
constant ack : (func(0, [int; int; int]))
constant x_Tuple74 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(3)]))
constant len : (func(2, [(@(0) @(1)); int]))
constant papp6 : (func(12, [(Pred @(0) @(1) @(2) @(3) @(4) @(5));
@(6);
@(7);
@(8);
@(9);
@(10);
@(11);
bool]))
constant x_Tuple22 : (func(2, [(Tuple @(0) @(1)); @(1)]))
constant x_Tuple66 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(5)]))
constant x_Tuple44 : (func(4, [(Tuple @(0) @(1) @(2) @(3));
@(3)]))
constant GHC.Err.undefined##02v : (func(1, [@(0)]))
constant strLen : (func(0, [[Char]; int]))
constant x_Tuple72 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(1)]))
constant isJust : (func(1, [(GHC.Base.Maybe @(0)); bool]))
constant x_Tuple31 : (func(3, [(Tuple @(0) @(1) @(2)); @(0)]))
constant x_Tuple75 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(4)]))
constant papp1 : (func(2, [(Pred @(0)); @(1); bool]))
constant x_Tuple61 : (func(6, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5));
@(0)]))
constant x_Tuple43 : (func(4, [(Tuple @(0) @(1) @(2) @(3));
@(2)]))
constant tail : (func(1, [[@(0)]; [@(0)]]))
constant GHC.Types.EQ##6U : (GHC.Types.Ordering)
constant x_Tuple51 : (func(5, [(Tuple @(0) @(1) @(2) @(3) @(4));
@(0)]))
constant x_Tuple73 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(2)]))
constant Main.ack##rjG : (func(0, [int; int; int]))
constant x_Tuple54 : (func(5, [(Tuple @(0) @(1) @(2) @(3) @(4));
@(3)]))
constant cmp : (func(0, [GHC.Types.Ordering; GHC.Types.Ordering]))
constant x_Tuple32 : (func(3, [(Tuple @(0) @(1) @(2)); @(1)]))
constant x_Tuple76 : (func(7, [(Tuple @(0) @(1) @(2) @(3) @(4) @(5) @(6));
@(5)]))
constant snd : (func(2, [(Tuple @(0) @(1)); @(1)]))
constant fst : (func(2, [(Tuple @(0) @(1)); @(0)]))
constant x_Tuple42 : (func(4, [(Tuple @(0) @(1) @(2) @(3));
@(1)]))
distinct GHC.Types.False##68 : (bool)
distinct GHC.Types.True##6u : (bool)
distinct GHC.Types.LT##6S : (GHC.Types.Ordering)
distinct GHC.Types.GT##6W : (GHC.Types.Ordering)
distinct GHC.Types.EQ##6U : (GHC.Types.Ordering)
bind 0 GHC.Err.undefined##02v : {VV : func(1, [@(0)]) | []}
bind 1 GHC.Types.True##6u : {VV##9 : bool | [(VV##9 = GHC.Types.True##6u)]}
bind 2 GHC.Types.False##68 : {VV##10 : bool | [(VV##10 = GHC.Types.False##68)]}
bind 3 GHC.Types.EQ##6U : {VV##11 : GHC.Types.Ordering | [(VV##11 = GHC.Types.EQ##6U)]}
bind 4 GHC.Types.LT##6S : {VV##12 : GHC.Types.Ordering | [(VV##12 = GHC.Types.LT##6S)]}
bind 5 GHC.Types.GT##6W : {VV##13 : GHC.Types.Ordering | [(VV##13 = GHC.Types.GT##6W)]}
bind 6 Main.ack##rjG : {VV : func(0, [int; int; int]) | []}
bind 7 Main.ack##rjG : {VV : func(0, [int; int; int]) | []}
bind 8 m##alH : {VV##41 : int | []}
bind 9 Main.bar##rlx : {VV : func(0, [int; int; int]) | []}
bind 10 VV##55 : {VV##55 : int | []}
bind 11 m##alH : {VV##57 : int | []}
bind 12 VV##58 : {VV##58 : int | []}
bind 13 lq_tmp$x##51 : {v : int | []}
bind 14 VV##61 : {VV##61 : int | []}
bind 15 VV##63 : {VV##63 : int | []}
bind 16 lq_tmp$x##40 : {v : int | []}
bind 17 VV##66 : {VV##66 : int | [(VV##66 = (ack m##alH lq_tmp$x##40))]}
bind 18 VV##68 : {VV##68 : int | [(VV##68 = m##alH)]}
bind 19 VV##70 : {VV##70 : int | []}
bind 20 lq_tmp$x##17 : {VV##72 : int | []}
bind 21 VV##73 : {VV##73 : int | []}
bind 22 lq_tmp$x##19 : {VV##75 : int | []}
bind 23 VV##76 : {VV##76 : int | [$k_##31[lq_tmp$x##22:=lq_tmp$x##17][VV##30:=VV##76][lq_tmp$x##26:=lq_tmp$x##19][lq_tmp$x##35:=VV##76]]}
bind 24 VV##23 : {VV##23 : int | [$k_##24]}
bind 25 lq_tmp$x##22 : {VV##23 : int | [$k_##24]}
bind 26 VV##27 : {VV##27 : int | [$k_##28]}
bind 27 lq_tmp$x##26 : {VV##27 : int | [$k_##28]}
bind 28 VV##30 : {VV##30 : int | [$k_##31]}
constraint:
env [0; 1; 2; 3; 4; 5; 6; 7; 8]
lhs {VV##F##1 : func(0, [int; int]) | [(VV##F##1 = (ack m##alH))]}
rhs {VV##F##1 : func(0, [int; int]) | [(VV##F##1 = (ack m##alH))]}
id 1 tag [2]
// META constraint id 1 : ()
constraint:
env [0; 1; 2; 3; 4; 5; 6]
lhs {VV##F##2 : int | []}
rhs {VV##F##2 : int | [$k_##24[VV##70:=VV##F##2][VV##23:=VV##F##2][VV##F:=VV##F##2][lq_tmp$x##33:=VV##F##2]]}
id 2 tag [1]
// META constraint id 2 : ()
constraint:
env [0; 1; 2; 3; 4; 5; 6; 20]
lhs {VV##F##3 : int | []}
rhs {VV##F##3 : int | [$k_##28[lq_tmp$x##22:=lq_tmp$x##17][lq_tmp$x##34:=VV##F##3][VV##27:=VV##F##3][VV##73:=VV##F##3][VV##F:=VV##F##3]]}
id 3 tag [1]
// META constraint id 3 : ()
wf:
env [0; 1; 2; 3; 4; 5; 6; 25]
reft {VV##27 : int | [$k_##28]}
// META wf : ()
wf:
env [0; 1; 2; 3; 4; 5; 6; 25; 27]
reft {VV##30 : int | [$k_##31]}
// META wf : ()
wf:
env [0; 1; 2; 3; 4; 5; 6]
reft {VV##23 : int | [$k_##24]}
// META wf : ()