content: {-# 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 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)
  {-@ predicate IsTagInStackSet T ST = 
      ((( (T = (getTag (getWorkspaceScreen (getCurrentScreen ST))))
       )) || ((
        (Set_mem T (getTagScreens (getVisible ST)))
      ) || (false)))
    @-}
  
  --       (Set_mem T (getTagScreens (getVisible ST)))
  {-@ view :: (Eq s, Eq i) 
           => t:i 
           -> st: {v:(StackSet i l a s sd) | true}
           -> {v:StackSet i l a s sd|((IsTagInStackSet t st) => (IsCurrentTag t v))} @-}
  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 <- findTagInScreen i (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 <- findTagInWorkspace i (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
  
  {-@ findTagInScreen :: (Eq i) 
           => t:i 
           -> s:([Screen i l a sid sd])
           -> {v:(Maybe (Screen i l a sid sd)) | ( ((isJust v) =>  (t = (getTag (getWorkspaceScreen (fromJust v))))))}
    @-}
  findTagInScreen :: (Eq i) => i -> [Screen i l a sid sd] -> Maybe (Screen i l a sid sd)
  findTagInScreen i []     = Nothing
  findTagInScreen i (x:xs) 
    | i == (tag (workspace x)) = Just x
    | otherwise                = findTagInScreen i xs
  
  {-@ findTagInWorkspace :: (Eq i) 
           => t:i 
           -> [Workspace i l a] 
           -> {v:(Maybe (Workspace i l a)) | ((isJust v) => (t = (getTag (fromJust v))))}
    @-}
  findTagInWorkspace :: (Eq i) => i -> [Workspace i l a] -> Maybe (Workspace i l a)
  findTagInWorkspace i []     = Nothing
  findTagInWorkspace i (x:xs) 
    | i == (tag x) = Just x
    | otherwise    = findTagInWorkspace i xs
  
  {-@ qview :: x:(Workspace i l a) -> {v:(Screen i l a sid sd)|(getWorkspaceScreen v) = x} @-}
  qview :: Workspace i l a -> Screen i l a sid sd 
  qview = undefined
  
  {-@ qview1 :: x:(Screen i l a sid sd) -> {v:(StackSet i l a sid sd)|(getCurrentScreen v) = x} @-}
  qview1 :: Screen i l a sid sd -> StackSet i l a sid sd 
  qview1 = undefined
  
  {-@ qview2 :: x:([Workspace i l a]) -> {v:(StackSet i l a sid sd)|(getHidden v) = x} @-}
  qview2 :: [Workspace i l a] -> StackSet i l a sid sd 
  qview2 = undefined
  
  {-@ qview3 :: x:([Screen i l a sid sd]) -> {v:(StackSet i l a sid sd)|(getVisible v) = x} @-}
  qview3 :: [Screen i l a sid sd] -> StackSet i l a sid sd 
  qview3 = undefined
  
  {-@ 
  qview4 :: x : (Screen i l a sid sd)
         -> y : ([Screen i l a sid sd])
         -> z : Workspace i l a
         -> {v:(StackSet i l a sid sd)|(stackSetElts v) = 
           (Set_cup (Set_cup (screenElts x) (screensElts y)) 
                     (workspaceElts z))}
  @-}
  qview4 :: (Screen i l a sid sd)
         -> [Screen i l a sid sd]
         -> Workspace i l a
         -> StackSet i l a sid sd
  qview4 = undefined
  
      -- '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.
  
  {-@ measure getTagWorkspace :: (Workspace i l a) -> (Data.Set.Set i)
      getTagWorkspace(Workspace t l s) = (Set_sng t)
    @-}
  
  {-@ measure getTagScreen :: (Screen i l a sid sd) -> (Data.Set.Set i)
      getTagScreen(Screen w s sd) = (getTagWorkspace w)
    @-}
  
  {-@ measure getTagScreens :: ([(Screen i l a sid sd)]) -> (Data.Set.Set i)
      getTagScreens([])   = {v | (?(Set_emp v))}
      getTagScreens(x:xs) = (Set_cap (getTagScreen x) (getTagScreens xs))
    @-}
  
  
  {-@ 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
  
  
  