module ListSets () where ------------------------------------------------------------------------- -- | Encoding Sets of Values With Liquid Types -------------------------- ------------------------------------------------------------------------- -- TODO: make this self-enclosed import Data.Set (Set(..)) -- | To start with, lets check that the `listElts` measure is sensible {-@ myid0 :: xs:[a] -> {v:[a]| (len v) = (len xs)} @-} myid0 [] = [] myid0 (x:xs) = x : myid0 xs {-@ myid :: xs:[a] -> {v:[a]| (listElts v) = (listElts xs)} @-} myid [] = [] myid (x:xs) = x : myid xs -- | The reverse function should also return the same set of values. -- Note that the reverse uses the tail-recursive helper @go@. -- Mouse over and see what type is inferred for it! {-@ decrease go 2 @-} {-@ myrev :: xs:[a] -> {v:[a]| listElts(v) = listElts(xs)} @-} myrev :: [a] -> [a] myrev = go [] where go acc [] = acc go acc (y:ys) = go (y:acc) ys -- | Next, here's good old List-append, but now with a specification about -- the sets of values in the input and output. {-@ myapp :: xs:[a] -> ys:[a] -> {v:[a] | listElts v = Set_cup (listElts xs) (listElts ys) } @-} myapp :: [a] -> [a] -> [a] myapp [] ys = ys myapp (x:xs) ys = x : myapp xs ys -- | Finally, to round off this little demo, here's @filter@, which returns a subset. {-@ myfilter :: (a -> Bool) -> xs:[a] -> {v:[a] | Set_sub (listElts v) (listElts xs) } @-} myfilter :: (a -> Bool) -> [a] -> [a] myfilter f [] = [] myfilter f (x:xs) = if f x then x : myfilter f xs else myfilter f xs