module ListSets () where
-------------------------------------------------------------------------
-- | Encoding Sets of Values With Liquid Types --------------------------
-------------------------------------------------------------------------
-- First, lets import the `Set` type from @Data.Set@
import Data.Set (Set (..))
-- Next, lets write a measure for the set of elements in a list.
{-@ measure elts :: [a] -> (Set a)
elts ([]) = {v | Set_emp v }
elts (x:xs) = {v | v = Set_cup (Set_sng x) (elts xs) }
@-}
-- Next, we tell the solver to interpret @Set@ natively in the refinement logic.
{-@ embed Set as Set_Set @-}
-- OK, now we can write some specifications!
-- | To start with, lets check that the `elts` measure is sensible
{-@ myid :: xs:[a] -> {v:[a]| (elts v) = (elts 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]| (elts v) = (elts xs)} @-}
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] | (elts v) = (Set_cup (elts xs) (elts ys))} @-}
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 (elts v) (elts xs) } @-}
myfilter f [] = []
myfilter f (x:xs)
| f x = x : myfilter f xs
| otherwise = myfilter f xs