content: module ListMem where
  
  
  import Data.Set hiding (partition)
  
  
  {-@ member' :: Eq a 
             => x:a 
             -> xs:[a] 
             -> {v:([{vv:a|vv=x}], [{vv:a|vv!=x}]) | (PairEqElts xs v)}
    @-}
  member' :: Eq a => a -> [a] -> ([a], [a])
  member' x ls = partition (cmp x) ls 
  
  {-@ member :: Eq a 
             => x:a 
             -> xs:[a] 
             -> {v:Bool|((Prop v) <=> (ListElt x xs))}
    @-}
  member :: Eq a => a -> [a] -> Bool
  member x ls 
    = case partition (cmp x) ls of
       ([], _) -> False -- can not prove this!
       (_, _)  -> True
  
  {-@ predicate ListElt N LS =
         (Set_mem N (listElts LS)) 
    @-}
  
  {-@ predicate PairEqElts X P =
   ((listElts X) = (Set_cup (listElts (getFst P)) (listElts (getSnd P))))
    @-}
  
  {-@ predicate UnionElts X Y Z W =
         ((listElts X) = (Set_cup (listElts Y) (Set_cup (listElts Z) (listElts W)))) 
    @-}
  
  {-@ measure getFst :: (a, b) -> a
      getFst(a, b) = a 
    @-}
  
  {-@ measure getSnd :: (a, b) -> b
      getSnd(a, b) = b
    @-}
  
  
  {-@ cmp :: Eq a 
          => x:a 
          -> y:a 
          -> Either {v:a| ((v = y) && (v = x))} 
                    {v:a| ((v != x) && (v = y))} 
    @-}
  cmp :: Eq a => a -> a ->  Either a a
  cmp x y | x == y    = Left  y
          | otherwise = Right y
  
  
  {-@ partition :: forall <p :: a -> Prop, q :: a -> Prop>.
                   (x:a -> Either {v:a<p>|v = x} {v:a<q>|v=x})
                -> xs:[a] 
                -> {v:([a<p>], [a<q>]) | (PairEqElts xs v) }
    @-}
  partition :: (a -> Either a a) -> [a] -> ([a], [a])
  partition f xs = partition' f xs xs ([], [])
  
  {-@ partition' :: forall <p :: a -> Prop, q :: a -> Prop>.
                   (x:a -> Either {v:a<p>|v = x} {v:a<q>|v=x})
                -> init:[a] 
                -> xs:[a] 
                -> ack:{v:([a<p>], [a<q>]) | ((listElts init) = (Set_cup (listElts xs) (Set_cup (listElts (getFst v)) (listElts (getSnd v))))) }
                -> {v:([a<p>], [a<q>]) | (listElts init) = (Set_cup (listElts (getFst v)) (listElts (getSnd v)))}
    @-}
  partition' :: (a -> Either a a) -> [a] -> [a] -> ([a], [a]) -> ([a], [a])
  partition' _ a [] (x, y) = (x, y)
  partition' f a (x:xs) (pos, neg) 
    = case f x of
      Left _  -> partition' f a xs (x:pos, neg) 
      Right _ -> partition' f a xs (pos, x:neg) 
  
  