content: module StackSet where
  
  import Data.Set (Set(..)) 
  
  data LL a = Nil | Cons { head :: a, tail :: LL a }
  
  {-@ data LL a = Nil | Cons { head :: a 
                             , tail :: {v: LL a | not (Set_mem head (LLElts v))  } } 
    @-}
  
  {-@ measure LLElts     :: LL a -> (Set a) 
      LLElts (Nil)       = {v | (Set_emp v)}
      LLElts (Cons x xs) = {v | v = (Set_cup (Set_sng x) (LLElts xs)) }
    @-}
  
  {-@ predicate Disjoint x y   = (Set_emp (Set_cap x y))            @-}  
  {-@ predicate NotIn    x y = not (Set_mem x (LLElts y))           @-} 
  
  
  ---------------------------------------------------------------------------------------------
  
  {-@ measure StackElts    :: Stack a -> (Set a) 
      StackElts (St f u d) = (Set_cup (Set_sng f) (Set_cup (LLElts u) (LLElts d)))
    @-}
  
  {-@ data Stack a = St { focus  :: a    
                        , up     :: {vu: LL a | (NotIn focus vu) } 
                        , down   :: {vd: LL a | ((NotIn focus vd) && (Disjoint (LLElts up) (LLElts vd))) } 
                        } 
    @-}
  
  data Stack a = St { focus  :: !a    
                    , up     :: !(LL a) 
                    , down   :: !(LL a)
                    } 
  
  ---------------------------------------------------------------------------------------------
  
  --| Super Vanilla Operations on Stacks
  
  {-@ 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 
  
  
  ---------------------------------------------------------------------------------------------
  
  {-@ measure MaybeStackElts :: Maybe (Stack a) -> (Set a) 
      MaybeStackElts Nothing  = {v | (? Set_emp(v))  }
      MaybeStackElts (Just s) = {v | v = StackElts s }
    @-}
  
  {-@ measure WorkspaceElts :: Workspace i l a -> (Set a) 
      WorkspaceElts (Workspace t l s) = (MaybeStackElts s) 
    @-}
  
  data Workspace i l a = Workspace  { tag :: !i, layout :: l, stack :: Maybe (Stack a) }
  
  ---------------------------------------------------------------------------------------------
  
  {-@ measure ScreenElts :: Screen i l a sid sd -> (Set a) 
      ScreenElts (ScreenElts w s d) = (WorkspaceElts w) 
    @-}
  
  data Screen i l a sid sd = Screen { workspace :: !(Workspace i l a)
                                    , screen :: !sid
                                    , screenDetail :: !sd }
  
  ---------------------------------------------------------------------------------------------
  
  {-@ measure ListScreenElts :: [Screen i l a sid sd] -> (Set a) 
      ListScreenElts ([])    =  {v | (Set_emp v)}
      ListScreenElts (x:xs)  =  {v | v = (Set_cup (ScreenElts x) (ListScreenElts xs)) }
    @-}
  
  
  {-@ measure ListWorkspaceElts :: [Workspace i l a] -> (Set a) 
      ListWorkspaceElts ([])    =  {v | (Set_emp v)}
      ListWorkspaceElts (x:xs)  =  {v | v = (Set_cup (WorkspaceElts x) (ListWorkspaceElts xs)) }
    @-}
  
  data StackSet i l a sid sd =
      StackSet { current  :: !(Screen i l a sid sd)    
               , visible  :: {v : [Screen i l a sid sd] | (Disjoint  (ScreenElts current)     (ListScreenElts v)) }
               , hidden   :: {v : [Workspace i l a]     | ((Disjoint (ScreenElts current)     (ListWorkspaceElts v)) && 
                                                           (Disjoint (ListScreenElts visible) (ListWorkspaceElts v))) }        
               , floating :: M.Map a RationalRect
               } 
  
  data RationalRect = RationalRect Rational Rational Rational Rational
  
  ----------------------------------------------------------------------------------------------------------------
  
  new :: (Integral s) => l -> [i] -> [sd] -> StackSet i l a s sd
  new l wids m 
    | not (null wids) && length m <= length wids && not (null m)
    = StackSet cur visi unseen M.empty
    where (seen,unseen) = L.splitAt (length m) $ map (\i -> Workspace i l Nothing) wids
          (cur:visi)    = [ Screen i s sd |  (i, s, sd) <- zip3 seen [0..] m ]
                  -- now zip up visibles with their screen id
  new _ _ _ = abort "non-positive argument to StackSet.new"
  
  
  abort :: {v: String | (0 = 1) } -> a
  abort x = error $ "xmonad: StackSet: " ++ x
  