{-# LANGUAGE PatternGuards #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  XMonad.StackSet
-- Copyright   :  (c) Don Stewart 2007
-- License     :  BSD3-style (see LICENSE)
--
-- Maintainer  :  dons@galois.com
-- Stability   :  experimental
-- Portability :  portable, Haskell 98
--

module XMonad.StackSet (
        -- * Introduction
        -- $intro

        -- ** The Zipper
        -- $zipper

        -- ** Xinerama support
        -- $xinerama

        -- ** Master and Focus
        -- $focus

        StackSet(..), Workspace(..), Screen(..), Stack(..), RationalRect(..),
        -- *  Construction
        -- $construction
        new, view, greedyView,
        -- * Xinerama operations
        -- $xinerama
        lookupWorkspace,
        screens, workspaces, allWindows, currentTag,
        -- *  Operations on the current stack
        -- $stackOperations
        peek, index, integrate, integrate', differentiate,
        focusUp, focusDown, focusUp', focusDown', focusMaster, focusWindow,
        tagMember, renameTag, ensureTags, member, findTag, mapWorkspace, mapLayout,
        -- * Modifying the stackset
        -- $modifyStackset
        insertUp, delete, delete', filter,
        -- * Setting the master window
        -- $settingMW
        swapUp, swapDown, swapMaster, shiftMaster, modify, modify', float, sink, -- needed by users
        -- * Composite operations
        -- $composite
        shift, shiftWin,

        -- for testing
        abort
    ) where

import Prelude hiding (filter, reverse, (++), elem) -- LIQUID
import Data.Maybe   (listToMaybe,isJust,fromMaybe)
import qualified Data.List as L (deleteBy,find,splitAt,filter,nub)
import Data.List ( (\\) )
import qualified Data.Map  as M (Map,insert,delete,empty)
import qualified Data.Set -- LIQUID

-------------------------------------------------------------------------------
----------------------------- Refinements on  Lists ---------------------------
-------------------------------------------------------------------------------

-- measures

{-@
  measure head :: [a] -> a
  head([])   = {v | false}
  head(x:xs) = {v | v = x} 
  @-}

{-@
  measure listDup :: [a] -> (Data.Set.Set a)
  listDup([]) = {v | (? Set_emp (v))}
  listDup(x:xs) = {v | v = ((Set_mem x (listElts xs))?(Set_cup (Set_sng x) (listDup xs)):(listDup xs)) }
  @-}

-- predicates 

{-@ predicate EqElts X Y =
       ((listElts X) = (listElts Y)) @-}

{-@ predicate SubElts X Y =
       (Set_sub (listElts X) (listElts Y)) @-}

{-@ predicate UnionElts X Y Z =
       ((listElts X) = (Set_cup (listElts Y) (listElts Z))) @-}

{-@ predicate ListElt N LS =
       (Set_mem N (listElts LS)) @-}

{-@ predicate ListUnique LS =
       (Set_emp (listDup LS)) @-}

{-@ predicate ListUniqueDif LS X =
       ((ListUnique LS) && (not (ListElt X LS))) @-}


{-@ predicate ListDisjoint X Y =
       (Set_emp (Set_cap (listElts X) (listElts Y))) @-}


-- types

{-@ type UList a = {v:[a] | (ListUnique v)} @-}

{-@ type UListDif a N = {v:[a] | ((not (ListElt N v)) && (ListUnique v))} @-}



-------------------------------------------------------------------------------
----------------------------- Refinements on Stacks ---------------------------
-------------------------------------------------------------------------------

{-@
data Stack a = Stack { focus :: a   
                     , up    :: UListDif a focus
                     , down  :: UListDif a focus }
@-}

{-@ type UStack a = {v:(Stack a) | (ListDisjoint (getUp v) (getDown v))}@-}

{-@ measure getUp :: forall a. (Stack a) -> [a] 
    getUp (Stack focus up down) = up
  @-}

{-@ measure getDown :: forall a. (Stack a) -> [a] 
    getDown (Stack focus up down) = down
  @-}

{-@ measure getFocus :: forall a. (Stack a) -> a
    getFocus (Stack focus up down) = focus
  @-}

{-@ predicate StackElt N S =
       (((ListElt N (getUp S)) 
       || (Set_mem N (Set_sng (getFocus S))) 
       || (ListElt N (getDown S))))
  @-}

{-@ predicate StackSetVisibleElt N S = true @-}
{-@ predicate StackSetHiddenElt N S = true @-}


-------------------------------------------------------------------------------
-----------------------  Grap StackSet Elements -------------------------------
-------------------------------------------------------------------------------

{-@ measure stackSetElts :: (StackSet i l a sid sd) -> (Data.Set.Set a)
    stackSetElts(StackSet current visible hidden f) = (Set_cup (Set_cup (screenElts current) (screensElts visible)) (workspacesElts hidden))
   @-}

{-@ measure screensElts :: [(Screen i l a sid sd)] -> (Data.Set.Set a)
    screensElts([])   = {v|(? (Set_emp v))} 
    screensElts(x:xs) = (Set_cup (screenElt x) (screensElts xs))
  @-}

{-@ measure screenElts :: (Screen i l a sid sd) -> (Data.Set.Set a)
    screenElts(Screen w s sd) = (workspaceElts w) @-}

{-@ measure workspacesElts :: [(Workspace i l a)] -> (Data.Set.Set a)
    workspacesElts([])   = {v|(? (Set_emp v))} 
    workspacesElts(x:xs) = (Set_cup (workspaceElts x) (workspacesElts xs))
  @-}

{-@ measure workspaceElts :: (Workspace i l a) -> (Data.Set.Set a)
    workspaceElts(Workspace t l s) = {v| (if (isJust s) then (stackElts (fromJust s)) else (? (Set_emp v)))} @-}

{-@ measure stackElts :: (StackSet i l a sid sd) -> (Data.Set.Set a)
    stackElts(Stack f up down) = (Set_cup (Set_sng f) (Set_cup (listElts up) (listElts down))) @-}

{-@ predicate EmptyStackSet X = (? (Set_emp (stackSetElts X)))@-}


-------------------------------------------------------------------------------
-----------------------  Talking about Tags --- -------------------------------
-------------------------------------------------------------------------------

{-@ measure getTag :: (Workspace i l a) -> i
    getTag(Workspace t l s) = t
  @-}

{-@ predicate IsCurrentTag X Y = 
      (X = (getTag (getWorkspaceScreen (getCurrentScreen Y))))
  @-}

-- $intro
--
-- The 'StackSet' data type encodes a window manager abstraction. The
-- window manager is a set of virtual workspaces. On each workspace is a
-- stack of windows. A given workspace is always current, and a given
-- window on each workspace has focus. The focused window on the current
-- workspace is the one which will take user input. It can be visualised
-- as follows:
--
-- > Workspace  { 0*}   { 1 }   { 2 }   { 3 }   { 4 }
-- >
-- > Windows    [1      []      [3*     [6*]    []
-- >            ,2*]            ,4
-- >                            ,5]
--
-- Note that workspaces are indexed from 0, windows are numbered
-- uniquely. A '*' indicates the window on each workspace that has
-- focus, and which workspace is current.

-- $zipper
--
-- We encode all the focus tracking directly in the data structure, with a 'zipper':
--
--    A Zipper is essentially an `updateable' and yet pure functional
--    cursor into a data structure. Zipper is also a delimited
--    continuation reified as a data structure.
--
--    The Zipper lets us replace an item deep in a complex data
--    structure, e.g., a tree or a term, without an  mutation.  The
--    resulting data structure will share as much of its components with
--    the old structure as possible.
--
--      Oleg Kiselyov, 27 Apr 2005, haskell\@, "Zipper as a delimited continuation"
--
-- We use the zipper to keep track of the focused workspace and the
-- focused window on each workspace, allowing us to have correct focus
-- by construction. We closely follow Huet's original implementation:
--
--      G. Huet, /Functional Pearl: The Zipper/,
--      1997, J. Functional Programming 75(5):549-554.
-- and:
--      R. Hinze and J. Jeuring, /Functional Pearl: The Web/.
--
-- and Conor McBride's zipper differentiation paper.
-- Another good reference is:
--
--      The Zipper, Haskell wikibook

-- $xinerama
-- Xinerama in X11 lets us view multiple virtual workspaces
-- simultaneously. While only one will ever be in focus (i.e. will
-- receive keyboard events), other workspaces may be passively
-- viewable.  We thus need to track which virtual workspaces are
-- associated (viewed) on which physical screens.  To keep track of
-- this, 'StackSet' keeps separate lists of visible but non-focused
-- workspaces, and non-visible workspaces.

-- $focus
--
-- Each stack tracks a focused item, and for tiling purposes also tracks
-- a 'master' position. The connection between 'master' and 'focus'
-- needs to be well defined, particularly in relation to 'insert' and
-- 'delete'.
--

------------------------------------------------------------------------
-- |
-- A cursor into a non-empty list of workspaces.
--
-- We puncture the workspace list, producing a hole in the structure
-- used to track the currently focused workspace. The two other lists
-- that are produced are used to track those workspaces visible as
-- Xinerama screens, and those workspaces not visible anywhere.

data StackSet i l a sid sd =
    StackSet { current  :: !(Screen i l a sid sd)    -- ^ currently focused workspace
             , visible  :: [Screen i l a sid sd]     -- ^ non-focused workspaces, visible in xinerama
             , hidden   :: [Workspace i l a]         -- ^ workspaces not visible anywhere
             , floating :: M.Map a RationalRect      -- ^ floating windows
             } deriving (Show, Eq)
-- LIQUID             } deriving (Show, Read, Eq)

{-@ 
data StackSet i l a sid sd =
    StackSet { current  :: (Screen i l a sid sd)   
             , visible  :: [Screen i l a sid sd]   
             , hidden   :: [Workspace i l a]       
             , floating :: M.Map a RationalRect    
             }
@-}

{-@ invariant {v:(StackSet i l a sid sd) | 
     (((?(
       Set_emp (Set_cap (screenElts (getCurrentScreen v)) 
                        (screensElts (getVisible v))
      ))) && (?(
       Set_emp (Set_cap (screenElts (getCurrentScreen v)) 
                        (workspacesElts (getHidden v))
      )))) && (?(
       Set_emp (Set_cap (workspacesElts (getHidden v)) 
                        (screensElts (getVisible v))
      ))))} @-}

{-@ measure getCurrentScreen :: (StackSet i l a sid sd) -> (Screen i l a sid sd)
    getCurrentScreen(StackSet current v h f) = current @-}

{-@ measure getVisible :: (StackSet i l a sid sd) -> [(Screen i l a sid sd)]
    getVisible(StackSet current v h f) = v @-}

{-@ measure getHidden :: (StackSet i l a sid sd) -> [(Workspace i l a)]
    getHidden(StackSet current v h f) = h @-}

{-@ predicate StackSetCurrentElt N S = 
      (ScreenElt N (getCurrentScreen S))
  @-}

{-@ current :: s:(StackSet i l a sid sd) 
            -> {v:(Screen i l a sid sd) | v = (getCurrentScreen s)}
  @-}

{-@ stack :: w:(Workspace i l a) 
          -> {v:(Maybe (UStack a)) | v = (getStackWorkspace w)}
  @-}

{-@ workspace :: s:(Screen i l a sid sd) 
              -> {v:(Workspace i l a) | v = (getWorkspaceScreen s)}
  @-}

{-@ tag :: w:(Workspace i l a) -> {v:i|v = (getTag w)} @-}

-- | Visible workspaces, and their Xinerama screens.
data Screen i l a sid sd = Screen { workspace :: !(Workspace i l a)
                                  , screen :: !sid
                                  , screenDetail :: !sd }
    deriving (Show, Eq)
-- LIQUID    deriving (Show, Read, Eq)

{-@ 
data Screen i l a sid sd = Screen { workspace :: (Workspace i l a)
                                  , screen :: sid
                                  , screenDetail :: sd }
@-}

{-@ measure getWorkspaceScreen :: (Screen i l a sid sd) -> (Workspace i l a)
    getWorkspaceScreen(Screen w screen s) = w @-}


{-@ predicate ScreenElt N S = 
      (WorkspaceElt N (getWorkspaceScreen S))
  @-}


-- |
-- A workspace is just a tag, a layout, and a stack.
--
data Workspace i l a = Workspace  { tag :: !i, layout :: l, stack :: Maybe (Stack a) }
    deriving (Show, Eq)
--     deriving (Show, Read, Eq)

{-@
data Workspace i l a = Workspace  { tag :: i, layout :: l, stack :: Maybe (UStack a) }
  @-}

{-@ measure getStackWorkspace :: (Workspace i l a) -> (Maybe(Stack a))
    getStackWorkspace(Workspace t l stack) = stack @-}

{-@ predicate WorkspaceElt N W =
  ((isJust (getStackWorkspace W)) && (StackElt N (fromJust (getStackWorkspace W)))) @-}

-- | A structure for window geometries
data RationalRect = RationalRect Rational Rational Rational Rational
    deriving (Show, Read, Eq)

-- |
-- A stack is a cursor onto a window list.
-- The data structure tracks focus by construction, and
-- the master window is by convention the top-most item.
-- Focus operations will not reorder the list that results from
-- flattening the cursor. The structure can be envisaged as:
--
-- >    +-- master:  < '7' >
-- > up |            [ '2' ]
-- >    +---------   [ '3' ]
-- > focus:          < '4' >
-- > dn +----------- [ '8' ]
--
-- A 'Stack' can be viewed as a list with a hole punched in it to make
-- the focused position. Under the zipper\/calculus view of such
-- structures, it is the differentiation of a [a], and integrating it
-- back has a natural implementation used in 'index'.
--
data Stack a = Stack { focus  :: !a        -- focused thing in this set
                     , up     :: [a]       -- clowns to the left
                     , down   :: [a] }     -- jokers to the right
     deriving (Show, Eq)
-- LIQUID      deriving (Show, Read, Eq)


-- | this function indicates to catch that an error is expected
abort :: String -> a
abort x = error $ "xmonad: StackSet: " ++ x
  where [] ++ ys     = ys              -- LIQUID
        (x:xs) ++ ys = x: (xs ++ ys)   -- LIQUID


-- ---------------------------------------------------------------------
-- $construction

-- | /O(n)/. Create a new stackset, of empty stacks, with given tags,
-- with physical screens whose descriptions are given by 'm'. The
-- number of physical screens (@length 'm'@) should be less than or
-- equal to the number of workspace tags.  The first workspace in the
-- list will be current.
--
-- Xinerama: Virtual workspaces are assigned to physical screens, starting at 0.
--
{-@ new :: (Integral s) 
        => l 
        -> is:[i] 
        -> [sd] 
        -> {v:(StackSet i l a s sd) | ((EmptyStackSet v) && (IsCurrentTag (head is) v))} 
  @-}
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"

-- |
-- /O(w)/. Set focus to the workspace with index \'i\'.
-- If the index is out of range, return the original 'StackSet'.
--
-- Xinerama: If the workspace is not visible on any Xinerama screen, it
-- becomes the current screen. If it is in the visible list, it becomes
-- current.

{-@ view :: (Eq s, Eq i) 
         => t:i 
         -> StackSet i l a s sd 
         -> StackSet i l a s sd @-}
view :: (Eq s, Eq i) => i -> StackSet i l a s sd -> StackSet i l a s sd
view i s
    | i == currentTag s = s  -- current

    | Just x <- L.find ((i==).tag.workspace) (visible s)
    -- if it is visible, it is just raised
    = s { current = x, visible = current s : L.deleteBy (equating screen) x (visible s) }

    | Just x <- L.find ((i==).tag)           (hidden  s) -- must be hidden then
    -- if it was hidden, it is raised on the xine screen currently used
    = s { current = (current s) { workspace = x }
        , hidden = workspace (current s) : L.deleteBy (equating tag) x (hidden s) }

    | otherwise = s -- not a member of the stackset

  where equating f = \x y -> f x == f y

    -- 'Catch'ing this might be hard. Relies on monotonically increasing
    -- workspace tags defined in 'new'
    --
    -- and now tags are not monotonic, what happens here?

-- |
-- Set focus to the given workspace.  If that workspace does not exist
-- in the stackset, the original workspace is returned.  If that workspace is
-- 'hidden', then display that workspace on the current screen, and move the
-- current workspace to 'hidden'.  If that workspace is 'visible' on another
-- screen, the workspaces of the current screen and the other screen are
-- swapped.

{-@ greedyView :: (Eq s, Eq i) => i -> StackSet i l a s sd -> StackSet i l a s sd @-}
greedyView :: (Eq s, Eq i) => i -> StackSet i l a s sd -> StackSet i l a s sd
greedyView w ws
     | any wTag (hidden ws) = view w ws
     | (Just s) <- L.find (wTag . workspace) (visible ws)
                            = ws { current = (current ws) { workspace = workspace s }
                                 , visible = s { workspace = workspace (current ws) }
                                           : L.filter (not . wTag . workspace) (visible ws) }
     | otherwise = ws
   where wTag = (w == ) . tag

-- ---------------------------------------------------------------------
-- $xinerama

-- | Find the tag of the workspace visible on Xinerama screen 'sc'.
-- 'Nothing' if screen is out of bounds.
lookupWorkspace :: Eq s => s -> StackSet i l a s sd -> Maybe i
lookupWorkspace sc w = listToMaybe [ tag i | Screen i s _ <- current w : visible w, s == sc ]

-- ---------------------------------------------------------------------
-- $stackOperations

-- |
-- The 'with' function takes a default value, a function, and a
-- StackSet. If the current stack is Nothing, 'with' returns the
-- default value. Otherwise, it applies the function to the stack,
-- returning the result. It is like 'maybe' for the focused workspace.
--
with :: b -> (Stack a -> b) -> StackSet i l a s sd -> b
with dflt f = maybe dflt f . stack . workspace . current

-- |
-- Apply a function, and a default value for 'Nothing', to modify the current stack.
--
{-@ modify :: Maybe (UStack a) -> (UStack a -> Maybe (UStack a)) -> StackSet i l a s sd -> StackSet i l a s sd @-}
modify :: Maybe (Stack a) -> (Stack a -> Maybe (Stack a)) -> StackSet i l a s sd -> StackSet i l a s sd
modify d f s = s { current = (current s)
                        { workspace = (workspace (current s)) { stack = with d f s }}}

-- |
-- Apply a function to modify the current stack if it isn't empty, and we don't
--  want to empty it.
--
{-@ modify' :: (UStack a -> UStack a) -> StackSet i l a s sd -> StackSet i l a s sd @-}
modify' :: (Stack a -> Stack a) -> StackSet i l a s sd -> StackSet i l a s sd
modify' f = modify Nothing (Just . f)

-- |
-- /O(1)/. Extract the focused element of the current stack.
-- Return 'Just' that element, or 'Nothing' for an empty stack.
--
peek :: StackSet i l a s sd -> Maybe a
peek = with Nothing (return . focus)

-- |
-- /O(n)/. Flatten a 'Stack' into a list.
--
{-@ integrate :: UStack a -> UList a @-}
integrate :: Stack a -> [a]
integrate (Stack x l r) = reverse l ++ x : r

-- |
-- /O(n)/ Flatten a possibly empty stack into a list.
{-@ integrate' :: Maybe (UStack a) -> UList a @-}
integrate' :: Maybe (Stack a) -> [a]
integrate' = maybe [] integrate

-- |
-- /O(n)/. Turn a list into a possibly empty stack (i.e., a zipper):
-- the first element of the list is current, and the rest of the list
-- is down.
{-@ differentiate :: UList a -> Maybe (UStack a) @-}
differentiate :: [a] -> Maybe (Stack a)
differentiate []     = Nothing
differentiate (x:xs) = Just $ Stack x [] xs

-- |
-- /O(n)/. 'filter p s' returns the elements of 's' such that 'p' evaluates to
-- 'True'.  Order is preserved, and focus moves as described for 'delete'.
--
{-@ filter :: (a -> Bool) -> UStack a -> Maybe (UStack a) @-}
filter :: (a -> Bool) -> Stack a -> Maybe (Stack a)
filter p (Stack f ls rs) = case filterL p (f:rs) of
    f':rs' -> Just $ Stack f' (filterL p ls) rs'    -- maybe move focus down
    []     -> case filterL p ls of                  -- filter back up
                    f':ls' -> Just $ Stack f' ls' [] -- else up
                    []     -> Nothing

-- |
-- /O(s)/. Extract the stack on the current workspace, as a list.
-- The order of the stack is determined by the master window -- it will be
-- the head of the list. The implementation is given by the natural
-- integration of a one-hole list cursor, back to a list.
--
index :: StackSet i l a s sd -> [a]
index = with [] integrate

-- |
-- /O(1), O(w) on the wrapping case/.
--
-- focusUp, focusDown. Move the window focus up or down the stack,
-- wrapping if we reach the end. The wrapping should model a 'cycle'
-- on the current stack. The 'master' window, and window order,
-- are unaffected by movement of focus.
--
-- swapUp, swapDown, swap the neighbour in the stack ordering, wrapping
-- if we reach the end. Again the wrapping model should 'cycle' on
-- the current stack.
--
{-@ focusUp, focusDown, swapUp, swapDown :: StackSet i l a s sd -> StackSet i l a s sd @-}
focusUp, focusDown, swapUp, swapDown :: StackSet i l a s sd -> StackSet i l a s sd
focusUp   = modify' focusUp'
focusDown = modify' focusDown'

swapUp    = modify' swapUp'
swapDown  = modify' (reverseStack . swapUp' . reverseStack)

-- | Variants of 'focusUp' and 'focusDown' that work on a
-- 'Stack' rather than an entire 'StackSet'.
{-@ focusUp', focusDown' :: UStack a -> UStack a @-}
focusUp', focusDown' :: Stack a -> Stack a
focusUp' (Stack t (l:ls) rs) = Stack l ls (t:rs)
focusUp' (Stack t []     rs) = Stack x xs [] where (x:xs) = reverse (t:rs)
focusDown'                   = reverseStack . focusUp' . reverseStack

{-@ swapUp' :: UStack a -> UStack a @-}
swapUp' :: Stack a -> Stack a
swapUp'  (Stack t (l:ls) rs) = Stack t ls (l:rs)
swapUp'  (Stack t []     rs) = Stack t (reverse rs) []

-- | reverse a stack: up becomes down and down becomes up.
{-@ reverseStack :: UStack a -> UStack a @-}
reverseStack :: Stack a -> Stack a
reverseStack (Stack t ls rs) = Stack t rs ls

--
-- | /O(1) on current window, O(n) in general/. Focus the window 'w',
-- and set its workspace as current.
--
focusWindow :: (Eq s, Eq a, Eq i) => a -> StackSet i l a s sd -> StackSet i l a s sd
focusWindow w s | Just w == peek s = s
                | otherwise        = fromMaybe s $ do
                    n <- findTag w s
                    return $ until ((Just w ==) . peek) focusUp (view n s)

-- | Get a list of all screens in the 'StackSet'.
screens :: StackSet i l a s sd -> [Screen i l a s sd]
screens s = current s : visible s

-- | Get a list of all workspaces in the 'StackSet'.
{-@ workspaces :: StackSet i l a s sd -> [Workspace i l a] @-}
workspaces :: StackSet i l a s sd -> [Workspace i l a]
workspaces s = workspace (current s) : map workspace (visible s) ++ hidden s
  where [] ++ ys     = ys              -- LIQUID
        (x:xs) ++ ys = x: (xs ++ ys)   -- LIQUID


-- | Get a list of all windows in the 'StackSet' in no particular order
allWindows :: Eq a => StackSet i l a s sd -> [a]
allWindows = L.nub . concatMap (integrate' . stack) . workspaces

-- | Get the tag of the currently focused workspace.
{-@ currentTag :: s: StackSet i l a s sd 
               -> {v:i|(IsCurrentTag v s)} @-}
currentTag :: StackSet i l a s sd -> i
currentTag = tag . workspace . current

-- LIQUID : qualifier missing for currentTag
{-@ qcurrentTag :: s:(StackSet i l a s sd) 
                -> {v:(Workspace i l a) | v = (getWorkspaceScreen (getCurrentScreen s))} @-}
qcurrentTag :: StackSet i l a s sd -> Workspace i l a 
qcurrentTag = workspace . current

-- | Is the given tag present in the 'StackSet'?
tagMember :: Eq i => i -> StackSet i l a s sd -> Bool
tagMember t = elem t . map tag . workspaces

-- | Rename a given tag if present in the 'StackSet'.
renameTag :: Eq i => i -> i -> StackSet i l a s sd -> StackSet i l a s sd
renameTag o n = mapWorkspace rename
    where rename w = if tag w == o then w { tag = n } else w

-- | Ensure that a given set of workspace tags is present by renaming
-- existing workspaces and\/or creating new hidden workspaces as
-- necessary.
ensureTags :: Eq i => l -> [i] -> StackSet i l a s sd -> StackSet i l a s sd
ensureTags l allt st = et allt (map tag (workspaces st) \\ allt) st
    where et [] _ s = s
          et (i:is) rn s | i `tagMember` s = et is rn s
          et (i:is) [] s = et is [] (s { hidden = Workspace i l Nothing : hidden s })
          et (i:is) (r:rs) s = et is rs $ renameTag r i s

-- | Map a function on all the workspaces in the 'StackSet'.
mapWorkspace :: (Workspace i l a -> Workspace i l a) -> StackSet i l a s sd -> StackSet i l a s sd
mapWorkspace f s = s { current = updScr (current s)
                     , visible = map updScr (visible s)
                     , hidden  = map f (hidden s) }
    where updScr scr = scr { workspace = f (workspace scr) }

-- | Map a function on all the layouts in the 'StackSet'.
mapLayout :: (l -> l') -> StackSet i l a s sd -> StackSet i l' a s sd
mapLayout f (StackSet v vs hs m) = StackSet (fScreen v) (map fScreen vs) (map fWorkspace hs) m
 where
    fScreen (Screen ws s sd) = Screen (fWorkspace ws) s sd
    fWorkspace (Workspace t l s) = Workspace t (f l) s

-- | /O(n)/. Is a window in the 'StackSet'?
{-@ member :: Eq a 
           => x:a 
           -> st:(StackSet i l a s sd) 
           -> {v:Bool| ((~(Prop v)) => (~(StackSetCurrentElt x st)))}
  @-}
member :: Eq a => a -> StackSet i l a s sd -> Bool
member a s -- LIQUID isJust (findTag a s)
  = memberStack a (stack $ workspace $ current s) || isJust (findTag a s)

{-@ memberStack :: Eq a
                => x:a 
                -> st:(Maybe (UStack a))
                -> {v:Bool|((Prop v)<=>((isJust st) && (StackElt x (fromJust st))))}
  @-}
memberStack :: Eq a => a -> Maybe (Stack a) -> Bool
memberStack x (Just (Stack f up down)) = x `elem` (f : up ++ down)
memberStack _ Nothing                  = False

-- | /O(1) on current window, O(n) in general/.
-- Return 'Just' the workspace tag of the given window, or 'Nothing'
-- if the window is not in the 'StackSet'.
findTag :: Eq a => a -> StackSet i l a s sd -> Maybe i
findTag a s = listToMaybe
    [ tag w | w <- workspaces s, has a (stack w) ]
    where has _ Nothing         = False
          has x (Just (Stack t l r)) = x `elem` (t : l ++ r)

-- ---------------------------------------------------------------------
-- $modifyStackset

-- |
-- /O(n)/. (Complexity due to duplicate check). Insert a new element
-- into the stack, above the currently focused element. The new
-- element is given focus; the previously focused element is moved
-- down.
--
-- If the element is already in the stackset, the original stackset is
-- returned unmodified.
--
-- Semantics in Huet's paper is that insert doesn't move the cursor.
-- However, we choose to insert above, and move the focus.
--
{-@ insertUp :: Eq a => a -> StackSet i l a s sd -> StackSet i l a s sd @-}
insertUp :: Eq a => a -> StackSet i l a s sd -> StackSet i l a s sd
insertUp a s = if member a s then s else insertUp_ a (Just $ Stack a [] []) s
-- LIQUID insertUp a s = if member a s then s else insert
-- LIQUID   where insert = modify (Just $ Stack a [] []) (Just $ Stack a [] []) (\(Stack t l r) -> Just $ Stack a l (t:r)) s

{-@ insertUp_ :: x:a 
              -> (Maybe (UStack a))  
              -> {v:StackSet i l a s sd | (~ (StackSetCurrentElt x v))}
              -> (StackSet i l a s sd) @-}
insertUp_ :: a 
          -> Maybe (Stack a) 
          -> StackSet i l a s sd 
          -> StackSet i l a s sd
insertUp_ x _ (StackSet (Screen (Workspace i l (Just (Stack t ls rs))) a b ) v h c)
 = (StackSet (Screen (Workspace i l (Just (Stack x ls (t:rs)))) a b) v h c)
insertUp_ _ d (StackSet (Screen (Workspace i l Nothing) a b ) v h c)
 = (StackSet (Screen (Workspace i l d) a b ) v h c)

-- insertDown :: a -> StackSet i l a s sd -> StackSet i l a s sd
-- insertDown a = modify (Stack a [] []) $ \(Stack t l r) -> Stack a (t:l) r
-- Old semantics, from Huet.
-- >    w { down = a : down w }

-- |
-- /O(1) on current window, O(n) in general/. Delete window 'w' if it exists.
-- There are 4 cases to consider:
--
--   * delete on an 'Nothing' workspace leaves it Nothing
--
--   * otherwise, try to move focus to the down
--
--   * otherwise, try to move focus to the up
--
--   * otherwise, you've got an empty workspace, becomes 'Nothing'
--
-- Behaviour with respect to the master:
--
--   * deleting the master window resets it to the newly focused window
--
--   * otherwise, delete doesn't affect the master.
--
{-@ delete :: (Ord a, Eq s) => a -> StackSet i l a s sd -> StackSet i l a s sd @-}
delete :: (Ord a, Eq s) => a -> StackSet i l a s sd -> StackSet i l a s sd
delete w = sink w . delete' w

-- | Only temporarily remove the window from the stack, thereby not destroying special
-- information saved in the 'Stackset'
delete' :: (Eq a, Eq s) => a -> StackSet i l a s sd -> StackSet i l a s sd
delete' w s = s { current = removeFromScreen        (current s)
                , visible = map removeFromScreen    (visible s)
                , hidden  = map removeFromWorkspace (hidden  s) }
    where removeFromWorkspace ws = ws { stack = stack ws >>= filter (/=w) }
          removeFromScreen scr   = scr { workspace = removeFromWorkspace (workspace scr) }

------------------------------------------------------------------------

-- | Given a window, and its preferred rectangle, set it as floating
-- A floating window should already be managed by the 'StackSet'.
float :: Ord a => a -> RationalRect -> StackSet i l a s sd -> StackSet i l a s sd
float w r s = s { floating = M.insert w r (floating s) }

-- | Clear the floating status of a window
sink :: Ord a => a -> StackSet i l a s sd -> StackSet i l a s sd
sink w s = s { floating = M.delete w (floating s) }

------------------------------------------------------------------------
-- $settingMW

-- | /O(s)/. Set the master window to the focused window.
-- The old master window is swapped in the tiling order with the focused window.
-- Focus stays with the item moved.
{-@ swapMaster :: StackSet i l a s sd -> StackSet i l a s sd @-}
swapMaster :: StackSet i l a s sd -> StackSet i l a s sd
swapMaster = modify' swapMaster_ -- LIQUID $ \ccc -> case ccc of
-- LIQUID     Stack _ [] _  -> ccc    -- already master.
-- LIQUID     Stack t ls rs -> Stack t [] (xs ++ x : rs) where (x:xs) = reverse ls

-- LIQUID TODO this should be set to original code if we use invariants
{-@ swapMaster_ :: UStack a -> UStack a @-}
swapMaster_ :: Stack a -> Stack a
swapMaster_ =  \ccc -> case ccc of
    Stack _ [] _  -> ccc    -- already master.
    Stack t ls rs -> Stack t [] (xs ++ x : rs) where (x:xs) = reverse ls


-- natural! keep focus, move current to the top, move top to current.

-- | /O(s)/. Set the master window to the focused window.
-- The other windows are kept in order and shifted down on the stack, as if you
-- just hit mod-shift-k a bunch of times.
-- Focus stays with the item moved.
shiftMaster :: StackSet i l a s sd -> StackSet i l a s sd
shiftMaster = modify' $ \c -> case c of
    Stack _ [] _ -> c     -- already master.
    Stack t ls rs -> Stack t [] (reverse ls ++ rs)

-- | /O(s)/. Set focus to the master window.
{-@ focusMaster :: StackSet i l a s sd -> StackSet i l a s sd @-}
focusMaster :: StackSet i l a s sd -> StackSet i l a s sd
focusMaster = modify' focusMaster_ -- LIQUID $ \c -> case c of
-- LIQUID     Stack _ [] _  -> c
-- LIQUID     Stack t ls rs -> Stack x [] (xs ++ t : rs) where (x:xs) = reverse ls

{-@ focusMaster_ :: UStack a -> UStack a @-}
focusMaster_ :: Stack a -> Stack a
focusMaster_ = \c -> case c of
    Stack _ [] _  -> c
    Stack t ls rs -> Stack x [] (xs ++ t : rs) where (x:xs) = reverse ls

-- ---------------------------------------------------------------------
-- $composite

-- | /O(w)/. shift. Move the focused element of the current stack to stack
-- 'n', leaving it as the focused element on that stack. The item is
-- inserted above the currently focused element on that workspace.
-- The actual focused workspace doesn't change. If there is no
-- element on the current stack, the original stackSet is returned.
--
{-@ shift :: (Ord a, Eq s, Eq i) => i -> StackSet i l a s sd -> StackSet i l a s sd @-}
shift :: (Ord a, Eq s, Eq i) => i -> StackSet i l a s sd -> StackSet i l a s sd
shift n s = maybe s (\w -> shiftWin n w s) (peek s)

-- | /O(n)/. shiftWin. Searches for the specified window 'w' on all workspaces
-- of the stackSet and moves it to stack 'n', leaving it as the focused
-- element on that stack. The item is inserted above the currently
-- focused element on that workspace.
-- The actual focused workspace doesn't change. If the window is not
-- found in the stackSet, the original stackSet is returned.
{-@ shiftWin :: (Ord a, Eq a, Eq s, Eq i) => i -> a -> StackSet i l a s sd -> StackSet i l a s sd @-}
shiftWin :: (Ord a, Eq a, Eq s, Eq i) => i -> a -> StackSet i l a s sd -> StackSet i l a s sd
shiftWin n w s = case findTag w s of
                    Just from | n `tagMember` s && n /= from -> go from s
                    _                                        -> s
 where go from = onWorkspace n (insertUp w) . onWorkspace from (delete' w)

onWorkspace :: (Eq i, Eq s) => i -> (StackSet i l a s sd -> StackSet i l a s sd)
            -> (StackSet i l a s sd -> StackSet i l a s sd)
onWorkspace n f s = view (currentTag s) . f . view n $ s




-------------------------------------------------------------------------------
------------------------------- Functions on Lists ----------------------------
-------------------------------------------------------------------------------


infixr 5 ++
{-@ (++) :: xs:(UList a)
         -> ys:{v: UList a | (ListDisjoint v xs)}
         -> {v: UList a | (UnionElts v xs ys)}
  @-}
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x: (xs ++ ys)

{-@ reverse :: xs:(UList a)
            -> {v: UList a | (EqElts v xs)} 
  @-}
reverse :: [a] -> [a]
reverse = go []
  where go a []     = a
        go a (x:xs) = go (x:a) xs 

{-@ filterL :: (a -> Bool) -> xs:(UList a) -> {v:UList a | (SubElts v xs)} @-}
filterL :: (a -> Bool) -> [a] -> [a]
filterL p [] = []
filterL p (x:xs) | p x       = x : filterL p xs
                 | otherwise = filterL p xs

{-@ elem :: Eq a 
         => x:a 
         -> xs:[a] 
         -> {v:Bool|((Prop v)<=>(ListElt x xs))}
  @-}
elem :: Eq a => a -> [a] -> Bool
elem x []     = False
elem x (y:ys) | x == y    = True
              | otherwise = elem x ys

-- QUALIFIERS
{-@ q :: x:a -> {v:[a] |(not (Set_mem x (listElts v)))} @-}
q :: a -> [a]
q = undefined

{-@ q1 :: xs:[a] -> {v:a |(not (Set_mem v (listElts xs)))} @-}
q1 :: [a] -> a
q1 = undefined

