maybe.hs

module Test () where

import Language.Haskell.Liquid.Prelude (liquidAssert)

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

{-@ 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 

{-@ 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