1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
{-# 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
|
