content: module Stacks0 () where
  
  import qualified Data.Set as S -- (Set(..))
  
  data LL a = Nil | Cons { headC :: a
                         , tailC :: LL a
                         }
  
  {-@ data LL a = Nil | Cons { headC :: a
                             , tailC :: {v: LL a | not (Set_mem headC (elts v)) }
                             }
    @-}
  
  {-@ measure elts @-} 
  elts :: (Ord a) => LL a -> S.Set a
  elts (Nil)       = S.empty
  elts (Cons x xs) = S.union (S.singleton x) (elts xs)
  
  {-@ predicate Disjoint X Y = (Set_emp (Set_cap (elts X) (elts Y))) @-}
  {-@ predicate NotIn    X Y = not (Set_mem X (elts Y))              @-}
  
  ll2 = Cons x0 (Cons x1 (Cons x2 Nil))
    where x0 :: Int
          x0  = 0
          x1  = 1
          x2  = 2
  
  {-@ data Stack a = St { focus  :: a
                        , up     :: {vu: LL a | (NotIn focus vu) }
                        , down   :: {vd: LL a | ((NotIn focus vd) && (Disjoint up vd)) }
                        }
    @-}
  
  data Stack a = St { focus  :: !a
                    , up     :: !(LL a)
                    , down   :: !(LL a)
                    }
  
  {-@ fresh :: a -> Stack a @-}
  fresh x = St x Nil Nil
  
  {-@ moveUp :: Stack a -> Stack a @-}
  moveUp (St x (Cons y ys) zs) = St y ys (Cons x zs)
  moveUp s                     = s
  
  {-@ moveDn :: Stack a -> Stack a @-}
  moveDn (St x ys (Cons z zs)) = St z (Cons x ys) zs
  moveDn s                     = s
  