tests/pos/fixme.1.hs

Put mouse over identifiers to see inferred types
 1: module Ensure where
 2: 
 3: import Language.Haskell.Liquid.Prelude
 4: 
 5: {-@ qualif Diff(v:int,l:int,d:int): v = l-d @-}
 6: {-@ encodeUtf8 :: Nat -> Nat @-}
 7: 
 8: {-@ Decrease go    4 5 6 @-}
 9: {-@ Decrease start 4 5 6 @-}
10: encodeUtf8 :: Int -> Int
11: {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}encodeUtf8 {VV : (GHC.Types.Int) | (VV >= 0)}len = x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x3)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x3 - x2) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 1)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}start {VV : (GHC.Types.Int) | (VV == len) && (VV >= 0)}len {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == len) && (VV >= 0)}len {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
12: {-@ start :: len:Nat -> s:Nat -> n:{v:Nat|(len >= v)} 
13:           -> {v:Nat | v = (len - n)} -> {v:Int| v = ((n-s)+1)} 
14:           -> {v:Int | v = 1} -> Nat @-}
15: start :: Int -> Int -> Int -> Int -> Int -> Int -> Int
16: x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x3)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x3 - x2) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 1)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}start {VV : (GHC.Types.Int) | (VV >= 0)}len {VV : (GHC.Types.Int) | (VV >= 0)}size {VV : (GHC.Types.Int) | (VV >= 0) && (len >= VV)}n0 _ _ _ = x1:(GHC.Types.Int)
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x2)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x2 - x3) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}go {VV : (GHC.Types.Int) | (VV == len) && (VV >= 0)}len {VV : (GHC.Types.Int) | (VV == n0) && (VV >= 0) && (len >= VV)}n0 {VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}size ({VV : (GHC.Types.Int) | (VV == len) && (VV >= 0)}lenx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == n0) && (VV >= 0) && (len >= VV)}n0) ({VV : (GHC.Types.Int) | (VV == n0) && (VV >= 0) && (len >= VV)}n0 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}size x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) {VV : (GHC.Types.Int) | (VV == (0  :  int))}0
17:         {-@ go :: len:Int -> n:{v:Nat|len >= v} -> s:Nat -> {v:Nat|v = (len - n)} 
18:                -> {v:Int|(v = (n-s)+1)} 
19:                -> {v:Int | v = 0} -> Nat @-}
20: go :: Int -> Int -> Int -> Int -> Int -> Int -> Int
21: x1:(GHC.Types.Int)
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x2)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x2 - x3) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}go (GHC.Types.Int)len {VV : (GHC.Types.Int) | (VV >= 0) && (len >= VV)}n {VV : (GHC.Types.Int) | (VV >= 0)}size  _ _ _
22:   | {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n) && (len >= VV) && (VV <= len)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n) && (len >= VV) && (VV <= len)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {VV : (GHC.Types.Int) | (VV == len)}len  = {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n
23:   | otherwise = ({VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < size) && (VV <= len)}
 -> {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}ensure ({VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < len) && (VV < size)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}\{VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < len) && (VV < size)}n -> x1:(GHC.Types.Int)
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x2)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x2 - x3) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}go {VV : (GHC.Types.Int) | (VV == len)}len ({VV : (GHC.Types.Int) | (VV == n) && (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < len) && (VV < size)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) {VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}size ({VV : (GHC.Types.Int) | (VV == len)}len x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- ({VV : (GHC.Types.Int) | (VV == n) && (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < len) && (VV < size)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)) ({VV : (GHC.Types.Int) | (VV == n) && (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < len) && (VV < size)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}sizex1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (2  :  int))}2) {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 )
24:               where
25:                 ensure :: (Int -> Int) -> Int
26:                 ({VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < size) && (VV <= len)}
 -> {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}ensure {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < size) && (VV <= len)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}cont
27:                   | {VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}sizex1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 >= x2))}>= {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n = {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV) && (n >= VV) && (size >= VV) && (VV < size) && (VV <= len)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}cont {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n
28:                   | {VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}size x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x1:{VV : (GHC.Types.Int) | (len >= VV) && (n >= VV) && (VV <= len) && (VV <= n)}
-> x2:{VV : (GHC.Types.Int) | (len >= VV) && (n >= VV) && (VV <= len) && (VV <= n)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n = let (GHC.Types.Int)size' = {VV : (GHC.Types.Int) | (VV == (2  :  int))}2x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (((x1 > 1) && (x2 > 1)) => ((VV > x1) && (VV > x2))) && (((x1 >= 0) && (x2 >= 0)) => ((VV >= x1) && (VV >= x2)))}*{VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}size in 
29:                                   x1:(GHC.Types.Bool)
-> {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | ((Prop x1)) && (VV >= 0)}liquidAssume ({VV : (GHC.Types.Int) | (VV == size) && (VV >= 0)}sizex1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= size) && (size' >= VV) && (VV <= size')}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= size) && (size' >= VV) && (VV <= size')}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}<{VV : (GHC.Types.Int) | (VV == size')}size')    
30:                                      ({VV : (GHC.Types.Int) | (VV >= 0)}
 -> {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}$ x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0)}
-> x3:{VV : (GHC.Types.Int) | (VV >= 0) && (x1 >= VV)}
-> {VV : (GHC.Types.Int) | (VV == (x1 - x3)) && (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == ((x3 - x2) + 1))}
-> {VV : (GHC.Types.Int) | (VV == 1)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}start {VV : (GHC.Types.Int) | (VV == len)}len {VV : (GHC.Types.Int) | (VV == size')}size' {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n ({VV : (GHC.Types.Int) | (VV == len)}len x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}n) ({VV : (GHC.Types.Int) | (VV == n) && (VV >= 0) && (len >= VV)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == size')}size'x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
31: