mirror of
https://github.com/xmonad/xmonad.git
synced 2025-05-19 08:30:21 -07:00
136 lines
4.4 KiB
Haskell
136 lines
4.4 KiB
Haskell
{-# LANGUAGE ScopedTypeVariables #-}
|
|
module Properties.StackSet where
|
|
|
|
import Test.QuickCheck
|
|
import Instances
|
|
import Utils
|
|
|
|
import XMonad.StackSet hiding (filter)
|
|
|
|
import Data.Maybe
|
|
|
|
import Data.List (nub)
|
|
-- ---------------------------------------------------------------------
|
|
-- QuickCheck properties for the StackSet
|
|
|
|
-- Some general hints for creating StackSet properties:
|
|
--
|
|
-- * ops that mutate the StackSet are usually local
|
|
-- * most ops on StackSet should either be trivially reversible, or
|
|
-- idempotent, or both.
|
|
------------------------------------------------------------------------
|
|
|
|
-- Basic data invariants of the StackSet
|
|
--
|
|
-- With the new zipper-based StackSet, tracking focus is no longer an
|
|
-- issue: the data structure enforces focus by construction.
|
|
--
|
|
-- But we still need to ensure there are no duplicates, and master/and
|
|
-- the xinerama mapping aren't checked by the data structure at all.
|
|
--
|
|
-- * no element should ever appear more than once in a StackSet
|
|
-- * the xinerama screen map should be:
|
|
-- -- keys should always index valid workspaces
|
|
-- -- monotonically ascending in the elements
|
|
-- * the current workspace should be a member of the xinerama screens
|
|
--
|
|
invariant (s :: T) = and
|
|
-- no duplicates
|
|
[ noDuplicates
|
|
|
|
-- TODO: Fix this.
|
|
-- all this xinerama stuff says we don't have the right structure
|
|
-- , validScreens
|
|
-- , validWorkspaces
|
|
-- , inBounds
|
|
]
|
|
where
|
|
ws = concat [ focus t : up t ++ down t
|
|
| w <- workspace (current s) : map workspace (visible s) ++ hidden s
|
|
, t <- maybeToList (stack w)] :: [Char]
|
|
noDuplicates = nub ws == ws
|
|
|
|
-- validScreens = monotonic . sort . M. . (W.current s : W.visible : W$ s
|
|
|
|
-- validWorkspaces = and [ w `elem` allworkspaces | w <- (M.keys . screens) s ]
|
|
-- where allworkspaces = map tag $ current s : prev s ++ next s
|
|
|
|
-- inBounds = and [ w >=0 && w < size s | (w,sc) <- M.assocs (screens s) ]
|
|
|
|
monotonic [] = True
|
|
monotonic [x] = True
|
|
monotonic (x:y:zs) | x == y-1 = monotonic (y:zs)
|
|
| otherwise = False
|
|
|
|
prop_invariant = invariant
|
|
|
|
-- and check other ops preserve invariants
|
|
prop_empty_I (SizedPositive n) l = forAll (choose (1, fromIntegral n)) $ \m ->
|
|
forAll (vector m) $ \ms ->
|
|
invariant $ new l [0..fromIntegral n-1] ms
|
|
|
|
prop_view_I n (x :: T) =
|
|
invariant $ view n x
|
|
|
|
prop_greedyView_I n (x :: T) =
|
|
invariant $ greedyView n x
|
|
|
|
prop_focusUp_I (SizedPositive n) (x :: T) =
|
|
invariant $ applyN (Just n) focusUp x
|
|
prop_focusMaster_I (SizedPositive n) (x :: T) =
|
|
invariant $ applyN (Just n) focusMaster x
|
|
prop_focusDown_I (SizedPositive n) (x :: T) =
|
|
invariant $ applyN (Just n) focusDown x
|
|
|
|
prop_focus_I (SizedPositive n) (x :: T) =
|
|
case peek x of
|
|
Nothing -> True
|
|
Just _ -> let w = focus . fromJust . stack . workspace . current $
|
|
applyN (Just n) focusUp x
|
|
in invariant $ focusWindow w x
|
|
|
|
prop_insertUp_I n (x :: T) = invariant $ insertUp n x
|
|
|
|
prop_delete_I (x :: T) = invariant $
|
|
case peek x of
|
|
Nothing -> x
|
|
Just i -> delete i x
|
|
|
|
prop_swap_master_I (x :: T) = invariant $ swapMaster x
|
|
|
|
prop_swap_left_I (SizedPositive n) (x :: T) =
|
|
invariant $ applyN (Just n) swapUp x
|
|
prop_swap_right_I (SizedPositive n) (x :: T) =
|
|
invariant $ applyN (Just n) swapDown x
|
|
|
|
prop_shift_I (x :: T) = do
|
|
n <- arbitraryTag x
|
|
return $ invariant $ shift (fromIntegral n) x
|
|
|
|
prop_shift_win_I (nex :: NonEmptyWindowsStackSet) = do
|
|
let NonEmptyWindowsStackSet x = nex
|
|
w <- arbitraryWindow nex
|
|
n <- arbitraryTag x
|
|
return $ invariant $ shiftWin n w x
|
|
|
|
|
|
-- ---------------------------------------------------------------------
|
|
|
|
|
|
-- empty StackSets have no windows in them
|
|
prop_empty (EmptyStackSet x) =
|
|
all (== Nothing) [ stack w | w <- workspace (current x)
|
|
: map workspace (visible x) ++ hidden x ]
|
|
|
|
-- empty StackSets always have focus on first workspace
|
|
prop_empty_current (EmptyStackSet x) = currentTag x == head (tags x)
|
|
|
|
-- no windows will be a member of an empty workspace
|
|
prop_member_empty i (EmptyStackSet x) = not (member i x)
|
|
|
|
-- peek either yields nothing on the Empty workspace, or Just a valid window
|
|
prop_member_peek (x :: T) =
|
|
case peek x of
|
|
Nothing -> True {- then we don't know anything -}
|
|
Just i -> member i x
|