
{-# LANGUAGE QuasiQuotes #-}


import LiquidHaskell


import Language.Haskell.Liquid.Prelude (liquidAssert)

[lq| type OList a = [a]<{\fld v -> (v >= fld)}> |]

[lq| filterGt :: (Ord a) => x:Maybe a -> OList a -> OList {v:a | ((isJust(x)) => (fromJust(x) <= v)) } |]

filterGt ::  Ord a => Maybe a -> [a] -> [a]
filterGt Nothing  xs = xs
filterGt (Just x) xs = foo x xs
  
foo y xs = foo' y xs

foo' :: (Ord a) => a -> [a] -> [a]
foo' y []     = []
foo' y (x:xs) 
 = case compare y x of 
     GT -> foo' y xs 
     LT -> x:xs 
     EQ -> xs 

[lq| bar :: (Ord a) => z:a -> OList a -> OList {v:a | z <= v} |]
bar y xs = bar' y xs

bar' y []     = []
bar' y (x:xs) 
  | y > x    = bar' y xs 
  | y < x    = x:xs 
  | y == x   = xs 


