content: {-@ LIQUID "--pruneunsorted" @-}
  module Elements where
  
  import Prelude hiding (elem)
  
  import Data.Set (Set (..))
  
  {-@ append  :: xs:_ -> ys:_ -> {v:_ | UnElts v xs ys} @-}
  append [] ys     = ys
  append (x:xs) ys = x : append xs ys
  
  
  {-@ reverse :: xs:_ -> {v:_ | EqElts v xs} @-}
  reverse xs           = revAcc xs []
    where
     revAcc []     acc = acc
     revAcc (x:xs) acc = revAcc xs (x:acc)
  
  
  
  {-@ nub :: (Eq a) => xs:_ -> {v:_ | nodups v && EqElts v xs} @-}
  nub xs             = go xs []
    where
      go (x:xs) l
        | x `elem` l = go xs l
        | otherwise  = go xs (x:l)
      go [] l        = l
  
  
  {-@ elem :: (Eq a) => x:_ -> ys:_ -> {v:Bool | v <=> Set_mem x (elems ys)} @-}
  elem x []     = False
  elem x (y:ys) = x == y || elem x ys
  
  
  
  {-@ find :: (Eq a) => key:_ -> {map:_ | ValidKey key map} -> b @-}
  find key ((k,v):kvs)
    | key == k  = v
    | otherwise = find key kvs
  find _ []     = die "Lookup failed!"
  
  
  {-@ die :: {v:String | false} -> b @-}
  die x = error x
  
  ----------------------------------------------------------------------------
  ----------------------------------------------------------------------------
  ----------------------------------------------------------------------------
  
  {-@ predicate ValidKey K M    = Set_mem K (keys M)                       @-}
  {-@ predicate EqElts Xs Ys    = elems Xs = elems Ys                      @-}
  {-@ predicate UnElts Xs Ys Zs = elems Xs = Set_cup (elems Ys) (elems Zs) @-}
  
  {-@ measure keys  :: [(a, b)] -> (Set a)
        keys []     = (Set_empty 0)
        keys (kv:kvs) = (Set_cup (Set_sng (fst kv)) (keys kvs))
    @-}
  
  {-@ measure elems :: [a] -> (Set a)
        elems []    = (Set_empty 0)
        elems (x:xs)  = (Set_cup (Set_sng x) (elems xs))
    @-}
  
  {-@ measure nodups :: [a] -> Bool
        nodups []   = true
        nodups (x:xs) = (not (Set_mem x (elems xs)) && nodups xs)
    @-}
  