
{-# LANGUAGE QuasiQuotes #-}


import LiquidHaskell


import Prelude hiding (reverse)

foo :: Int -> Int -> Int
[lq| foo :: n:Nat -> m:Nat -> Nat /[n+m] |]

foo n m 
  | cond 1 = 0
  | cond 2 && n > 1 = foo (n-1) m
  | cond 3 && m > 2 = foo (n+1) (m-2)
 
[lq| cond :: Int -> Bool |]
cond :: Int -> Bool
cond _ = undefined


data L a = N | C a (L a)

[lq| data L [llen] |]

[lq| measure llen :: (L a) -> Int
    llen(N)      = 0
    llen(C x xs) = 1 + (llen xs)
  |]

[lq| invariant {v: L a | (llen v) >= 0} |]

[lq| reverse :: xs: L a -> ys : L a -> L a / [(llen ys)] |]
reverse :: L a -> L a -> L a
reverse xs N = xs
reverse xs (C y ys) = reverse (C y xs) ys

merge :: Ord a => L a -> L a -> L a 
[lq| merge :: Ord a => xs:L a -> ys:L a -> L a /[(llen xs) + (llen ys)]|]
merge (C x xs) (C y ys) | x > y     = C x $ merge xs (C y ys) 
                        | otherwise = C y $ merge (C x xs) ys
