diff options
| -rw-r--r-- | Main.hs | 10 | ||||
| -rw-r--r-- | tests/Instances.hs | 135 | ||||
| -rw-r--r-- | tests/Properties.hs | 1320 | ||||
| -rw-r--r-- | tests/Properties/Delete.hs | 70 | ||||
| -rw-r--r-- | tests/Properties/Failure.hs | 26 | ||||
| -rw-r--r-- | tests/Properties/Floating.hs | 36 | ||||
| -rw-r--r-- | tests/Properties/Focus.hs | 74 | ||||
| -rw-r--r-- | tests/Properties/GreedyView.hs | 44 | ||||
| -rw-r--r-- | tests/Properties/Insert.hs | 52 | ||||
| -rw-r--r-- | tests/Properties/Layout/Full.hs | 34 | ||||
| -rw-r--r-- | tests/Properties/Layout/Tall.hs | 116 | ||||
| -rw-r--r-- | tests/Properties/Screen.hs | 40 | ||||
| -rw-r--r-- | tests/Properties/Shift.hs | 70 | ||||
| -rw-r--r-- | tests/Properties/Stack.hs | 51 | ||||
| -rw-r--r-- | tests/Properties/StackSet.hs | 135 | ||||
| -rw-r--r-- | tests/Properties/Swap.hs | 47 | ||||
| -rw-r--r-- | tests/Properties/View.hs | 47 | ||||
| -rw-r--r-- | tests/Properties/Workspace.hs | 65 | ||||
| -rw-r--r-- | tests/Utils.hs | 39 | ||||
| -rw-r--r-- | xmonad.cabal | 21 |
20 files changed, 1232 insertions, 1200 deletions
@@ -27,10 +27,6 @@ import Data.Version (showVersion) import Graphics.X11.Xinerama (compiledWithXinerama) -#ifdef TESTING -import qualified Properties -#endif - -- | The entry point into xmonad. Attempts to compile any custom main -- for xmonad, and if it doesn't find one, just launches the default. main :: IO () @@ -47,9 +43,6 @@ main = do ["--restart"] -> sendRestart >> return () ["--version"] -> putStrLn $ unwords shortVersion ["--verbose-version"] -> putStrLn . unwords $ shortVersion ++ longVersion -#ifdef TESTING - ("--run-tests":_) -> Properties.main -#endif _ -> fail "unrecognized flags" where shortVersion = ["xmonad", showVersion version] @@ -68,9 +61,6 @@ usage = do " --recompile Recompile your ~/.xmonad/xmonad.hs" : " --replace Replace the running window manager with xmonad" : " --restart Request a running xmonad process to restart" : -#ifdef TESTING - " --run-tests Run the test suite" : -#endif [] -- | Build "~\/.xmonad\/xmonad.hs" with ghc, then execute it. If there are no diff --git a/tests/Instances.hs b/tests/Instances.hs new file mode 100644 index 0000000..2f087f8 --- /dev/null +++ b/tests/Instances.hs @@ -0,0 +1,135 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Instances where + +import Test.QuickCheck + +import Utils + +import XMonad.StackSet +import Control.Monad +import Data.List (nub, genericLength) + +import Debug.Trace + +-- +-- The all important Arbitrary instance for StackSet. +-- +instance (Integral i, Integral s, Eq a, Arbitrary a, Arbitrary l, Arbitrary sd) + => Arbitrary (StackSet i l a s sd) where + arbitrary = do + -- TODO: Fix this to be a reasonable higher number, Possibly use PositiveSized + numWs <- choose (1, 20) -- number of workspaces, there must be at least 1. + numScreens <- choose (1, numWs) -- number of physical screens, there must be at least 1 + lay <- arbitrary -- pick any layout + + wsIdxInFocus <- choose (1, numWs) -- pick index of WS to be in focus + + -- The same screen id's will be present in the list, with high possibility. + screens <- replicateM numScreens arbitrary + + -- Generate a list of "windows" for each workspace. + wsWindows <- vector numWs :: Gen [[a]] + + -- Pick a random window "number" in each workspace, to give focus. + focus <- sequence [ if null windows + then return Nothing + else liftM Just $ choose (0, length windows - 1) + | windows <- wsWindows ] + + let tags = [1 .. fromIntegral numWs] + focusWsWindows = zip focus wsWindows + wss = zip tags focusWsWindows -- tmp representation of a workspace (tag, windows) + initSs = new lay tags screens + return $ + view (fromIntegral wsIdxInFocus) $ + foldr (\(tag, (focus, windows)) ss -> -- Fold through all generated (tags,windows). + -- set workspace active by tag and fold through all + -- windows while inserting them. Apply the given number + -- of `focusUp` on the resulting StackSet. + applyN focus focusUp $ foldr insertUp (view tag ss) windows + ) initSs wss + + +-- +-- Just generate StackSets with Char elements. +-- +type Tag = Int +type Window = Char +type T = StackSet Tag Int Window Int Int + + + +newtype EmptyStackSet = EmptyStackSet T + deriving Show + +instance Arbitrary EmptyStackSet where + arbitrary = do + (NonEmptyNubList ns) <- arbitrary + (NonEmptyNubList sds) <- arbitrary + l <- arbitrary + -- there cannot be more screens than workspaces: + return . EmptyStackSet . new l ns $ take (min (length ns) (length sds)) sds + + + +newtype NonEmptyWindowsStackSet = NonEmptyWindowsStackSet T + deriving Show + +instance Arbitrary NonEmptyWindowsStackSet where + arbitrary = + NonEmptyWindowsStackSet `fmap` (arbitrary `suchThat` (not . null . allWindows)) + + + +newtype SizedPositive = SizedPositive Int + deriving (Eq, Ord, Show, Read) + +instance Arbitrary SizedPositive where + arbitrary = sized $ \s -> do x <- choose (1, max 1 s) + return $ SizedPositive x + + + +newtype NonEmptyNubList a = NonEmptyNubList [a] + deriving ( Eq, Ord, Show, Read ) + +instance (Eq a, Arbitrary a) => Arbitrary (NonEmptyNubList a) where + arbitrary = NonEmptyNubList `fmap` ((liftM nub arbitrary) `suchThat` (not . null)) + + + +-- | Pull out an arbitrary tag from the StackSet. This removes the need for the +-- precondition "n `tagMember x` in many properties and thus reduces the number +-- of discarded tests. +-- +-- n <- arbitraryTag x +-- +-- We can do the reverse with a simple `suchThat`: +-- +-- n <- arbitrary `suchThat` \n' -> not $ n' `tagMember` x +arbitraryTag :: T -> Gen Tag +arbitraryTag x = do + let ts = tags x + -- There must be at least 1 workspace, thus at least 1 tag. + idx <- choose (0, (length ts) - 1) + return $ ts!!idx + +-- | Pull out an arbitrary window from a StackSet that is guaranteed to have a +-- non empty set of windows. This eliminates the precondition "i `member` x" in +-- a few properties. +-- +-- +-- foo (nex :: NonEmptyWindowsStackSet) = do +-- let NonEmptyWindowsStackSet x = nex +-- w <- arbitraryWindow nex +-- return $ ....... +-- +-- We can do the reverse with a simple `suchThat`: +-- +-- n <- arbitrary `suchThat` \n' -> not $ n `member` x +arbitraryWindow :: NonEmptyWindowsStackSet -> Gen Window +arbitraryWindow (NonEmptyWindowsStackSet x) = do + let ws = allWindows x + -- We know that there are at least 1 window in a NonEmptyWindowsStackSet. + idx <- choose(0, (length ws) - 1) + return $ ws!!idx diff --git a/tests/Properties.hs b/tests/Properties.hs index ae3f2e7..70d7e18 100644 --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -1,1191 +1,147 @@ -{-# OPTIONS -fglasgow-exts -w #-} -module Properties where +import Test.QuickCheck + +-- Our QC instances and properties. +import Instances +import Properties.Delete +import Properties.Failure +import Properties.Floating +import Properties.Focus +import Properties.GreedyView +import Properties.Insert +import Properties.Screen +import Properties.Shift +import Properties.Stack +import Properties.StackSet +import Properties.Swap +import Properties.View +import Properties.Workspace +import Properties.Layout.Full +import Properties.Layout.Tall -import XMonad.StackSet hiding (filter) -import XMonad.Layout -import XMonad.Core hiding (workspaces,trace) -import XMonad.Operations ( applyResizeIncHint, applyMaxSizeHint ) -import qualified XMonad.StackSet as S (filter) - -import Debug.Trace -import Data.Word -import Graphics.X11.Xlib.Types (Rectangle(..),Position,Dimension) -import Data.Ratio -import Data.Maybe import System.Environment -import Control.Exception (assert) -import qualified Control.Exception.Extensible as C -import Control.Monad -import Test.QuickCheck hiding (promote) -import System.IO.Unsafe -import System.IO -import System.Random hiding (next) import Text.Printf -import Data.List (nub,sort,sortBy,group,sort,intersperse,genericLength) -import qualified Data.List as L -import Data.Char (ord) -import Data.Map (keys,elems) -import qualified Data.Map as M - --- --------------------------------------------------------------------- --- 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. - --- --- The all important Arbitrary instance for StackSet. --- -instance (Integral i, Integral s, Eq a, Arbitrary a, Arbitrary l, Arbitrary sd) - => Arbitrary (StackSet i l a s sd) where - arbitrary = do - sz <- choose (1,10) -- number of workspaces - n <- choose (0,sz-1) -- pick one to be in focus - sc <- choose (1,sz) -- a number of physical screens - lay <- arbitrary -- pick any layout - sds <- replicateM sc arbitrary - ls <- vector sz -- a vector of sz workspaces - - -- pick a random item in each stack to focus - fs <- sequence [ if null s then return Nothing - else liftM Just (choose ((-1),length s-1)) - | s <- ls ] - - return $ fromList (fromIntegral n, sds,fs,ls,lay) - - --- | fromList. Build a new StackSet from a list of list of elements, --- keeping track of the currently focused workspace, and the total --- number of workspaces. If there are duplicates in the list, the last --- occurence wins. --- --- 'o' random workspace --- 'm' number of physical screens --- 'fs' random focused window on each workspace --- 'xs' list of list of windows --- -fromList :: (Integral i, Integral s, Eq a) => (i, [sd], [Maybe Int], [[a]], l) -> StackSet i l a s sd -fromList (_,_,_,[],_) = error "Cannot build a StackSet from an empty list" - -fromList (o,m,fs,xs,l) = - let s = view o $ - foldr (\(i,ys) s -> - foldr insertUp (view i s) ys) - (new l [0..genericLength xs-1] m) (zip [0..] xs) - in foldr (\f t -> case f of - Nothing -> t - Just i -> foldr (const focusUp) t [0..i] ) s fs - ------------------------------------------------------------------------- - --- --- Just generate StackSets with Char elements. --- -type T = StackSet (NonNegative Int) Int Char Int Int - --- Useful operation, the non-local workspaces -hidden_spaces x = map workspace (visible x) ++ hidden x - --- 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 - - -- 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 (n :: Positive Int) l = forAll (choose (1,fromIntegral n)) $ \m -> - forAll (vector m) $ \ms -> - invariant $ new l [0..fromIntegral n-1] ms - -prop_view_I (n :: NonNegative Int) (x :: T) = - invariant $ view (fromIntegral n) x - -prop_greedyView_I (n :: NonNegative Int) (x :: T) = - invariant $ greedyView (fromIntegral n) x - -prop_focusUp_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const focusUp) x [1..n] -prop_focusMaster_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const focusMaster) x [1..n] -prop_focusDown_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const focusDown) x [1..n] - -prop_focus_I (n :: NonNegative Int) (x :: T) = - case peek x of - Nothing -> True - Just _ -> let w = focus . fromJust . stack . workspace . current $ foldr (const focusUp) x [1..n] - 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 (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const swapUp ) x [1..n] -prop_swap_right_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const swapDown) x [1..n] - -prop_shift_I (n :: NonNegative Int) (x :: T) = - n `tagMember` x ==> invariant $ shift (fromIntegral n) x - -prop_shift_win_I (n :: NonNegative Int) (w :: Char) (x :: T) = - n `tagMember` x && w `member` x ==> invariant $ shiftWin (fromIntegral n) w x - - --- --------------------------------------------------------------------- --- 'new' - --- 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 (NonEmptyNubList ns) (NonEmptyNubList sds) l = - -- TODO, this is ugly - length sds <= length ns ==> - tag (workspace $ current x) == head ns - where x = new l ns sds :: T - --- no windows will be a member of an empty workspace -prop_member_empty i (EmptyStackSet x) - = member i x == False - --- --------------------------------------------------------------------- --- viewing workspaces - --- view sets the current workspace to 'n' -prop_view_current (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> - tag (workspace $ current (view i x)) == i - where - i = fromIntegral n - --- view *only* sets the current workspace, and touches Xinerama. --- no workspace contents will be changed. -prop_view_local (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> - workspaces x == workspaces (view i x) - where - workspaces a = sortBy (\s t -> tag s `compare` tag t) $ - workspace (current a) - : map workspace (visible a) ++ hidden a - i = fromIntegral n - --- view should result in a visible xinerama screen --- prop_view_xinerama (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> --- M.member i (screens (view i x)) --- where --- i = fromIntegral n - --- view is idempotent -prop_view_idem (x :: T) (i :: NonNegative Int) = i `tagMember` x ==> view i (view i x) == (view i x) - --- view is reversible, though shuffles the order of hidden/visible -prop_view_reversible (i :: NonNegative Int) (x :: T) = - i `tagMember` x ==> normal (view n (view i x)) == normal x - where n = tag (workspace $ current x) - --- --------------------------------------------------------------------- --- greedyViewing workspaces - --- greedyView sets the current workspace to 'n' -prop_greedyView_current (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> - tag (workspace $ current (greedyView i x)) == i - where - i = fromIntegral n - --- greedyView leaves things unchanged for invalid workspaces -prop_greedyView_current_id (x :: T) (n :: NonNegative Int) = not (i `tagMember` x) ==> - tag (workspace $ current (greedyView i x)) == j - where - i = fromIntegral n - j = tag (workspace (current x)) - --- greedyView *only* sets the current workspace, and touches Xinerama. --- no workspace contents will be changed. -prop_greedyView_local (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> - workspaces x == workspaces (greedyView i x) - where - workspaces a = sortBy (\s t -> tag s `compare` tag t) $ - workspace (current a) - : map workspace (visible a) ++ hidden a - i = fromIntegral n - --- greedyView is idempotent -prop_greedyView_idem (x :: T) (i :: NonNegative Int) = i `tagMember` x ==> greedyView i (greedyView i x) == (greedyView i x) - --- greedyView is reversible, though shuffles the order of hidden/visible -prop_greedyView_reversible (i :: NonNegative Int) (x :: T) = - i `tagMember` x ==> normal (greedyView n (greedyView i x)) == normal x - where n = tag (workspace $ current x) - --- normalise workspace list -normal s = s { hidden = sortBy g (hidden s), visible = sortBy f (visible s) } - where - f = \a b -> tag (workspace a) `compare` tag (workspace b) - g = \a b -> tag a `compare` tag b - --- --------------------------------------------------------------------- --- Xinerama - --- every screen should yield a valid workspace --- prop_lookupWorkspace (n :: NonNegative Int) (x :: T) = --- s < M.size (screens x) ==> --- fromJust (lookupWorkspace s x) `elem` (map tag $ current x : prev x ++ next x) --- where --- s = fromIntegral n - --- --------------------------------------------------------------------- --- peek/index - --- 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 - --- --------------------------------------------------------------------- --- index - --- the list returned by index should be the same length as the actual --- windows kept in the zipper -prop_index_length (x :: T) = - case stack . workspace . current $ x of - Nothing -> length (index x) == 0 - Just it -> length (index x) == length (focus it : up it ++ down it) - --- --------------------------------------------------------------------- --- rotating focus --- - --- master/focus --- --- The tiling order, and master window, of a stack is unaffected by focus changes. --- -prop_focus_left_master (n :: NonNegative Int) (x::T) = - index (foldr (const focusUp) x [1..n]) == index x -prop_focus_right_master (n :: NonNegative Int) (x::T) = - index (foldr (const focusDown) x [1..n]) == index x -prop_focus_master_master (n :: NonNegative Int) (x::T) = - index (foldr (const focusMaster) x [1..n]) == index x - -prop_focusWindow_master (n :: NonNegative Int) (x :: T) = - case peek x of - Nothing -> True - Just _ -> let s = index x - i = fromIntegral n `mod` length s - in index (focusWindow (s !! i) x) == index x - --- shifting focus is trivially reversible -prop_focus_left (x :: T) = (focusUp (focusDown x)) == x -prop_focus_right (x :: T) = (focusDown (focusUp x)) == x - --- focus master is idempotent -prop_focusMaster_idem (x :: T) = focusMaster x == focusMaster (focusMaster x) - --- focusWindow actually leaves the window focused... -prop_focusWindow_works (n :: NonNegative Int) (x :: T) = - case peek x of - Nothing -> True - Just _ -> let s = index x - i = fromIntegral n `mod` length s - in (focus . fromJust . stack . workspace . current) (focusWindow (s !! i) x) == (s !! i) - --- rotation through the height of a stack gets us back to the start -prop_focus_all_l (x :: T) = (foldr (const focusUp) x [1..n]) == x - where n = length (index x) -prop_focus_all_r (x :: T) = (foldr (const focusDown) x [1..n]) == x - where n = length (index x) - --- prop_rotate_all (x :: T) = f (f x) == f x --- f x' = foldr (\_ y -> rotate GT y) x' [1..n] - --- focus is local to the current workspace -prop_focus_down_local (x :: T) = hidden_spaces (focusDown x) == hidden_spaces x -prop_focus_up_local (x :: T) = hidden_spaces (focusUp x) == hidden_spaces x - -prop_focus_master_local (x :: T) = hidden_spaces (focusMaster x) == hidden_spaces x - -prop_focusWindow_local (n :: NonNegative Int) (x::T ) = - case peek x of - Nothing -> True - Just _ -> let s = index x - i = fromIntegral n `mod` length s - in hidden_spaces (focusWindow (s !! i) x) == hidden_spaces x - --- On an invalid window, the stackset is unmodified -prop_focusWindow_identity (n :: Char) (x::T ) = - not (n `member` x) ==> focusWindow n x == x - --- --------------------------------------------------------------------- --- member/findTag - --- --- For all windows in the stackSet, findTag should identify the --- correct workspace --- -prop_findIndex (x :: T) = - and [ tag w == fromJust (findTag i x) - | w <- workspace (current x) : map workspace (visible x) ++ hidden x - , t <- maybeToList (stack w) - , i <- focus t : up t ++ down t - ] - -prop_allWindowsMember w (x :: T) = (w `elem` allWindows x) ==> member w x - -prop_currentTag (x :: T) = - currentTag x == tag (workspace (current x)) - --- --------------------------------------------------------------------- --- 'insert' - --- inserting a item into an empty stackset means that item is now a member -prop_insert_empty i (EmptyStackSet x)= member i (insertUp i x) - --- insert should be idempotent -prop_insert_idem i (x :: T) = insertUp i x == insertUp i (insertUp i x) - --- insert when an item is a member should leave the stackset unchanged -prop_insert_duplicate i (x :: T) = member i x ==> insertUp i x == x - --- push shouldn't change anything but the current workspace -prop_insert_local (x :: T) i = not (member i x) ==> hidden_spaces x == hidden_spaces (insertUp i x) - --- Inserting a (unique) list of items into an empty stackset should --- result in the last inserted element having focus. -prop_insert_peek (EmptyStackSet x) (NonEmptyNubList is) = - peek (foldr insertUp x is) == Just (head is) - --- insert >> delete is the identity, when i `notElem` . --- Except for the 'master', which is reset on insert and delete. --- -prop_insert_delete n x = not (member n x) ==> delete n (insertUp n y) == (y :: T) - where - y = swapMaster x -- sets the master window to the current focus. - -- otherwise, we don't have a rule for where master goes. - --- inserting n elements increases current stack size by n -prop_size_insert is (EmptyStackSet x) = - size (foldr insertUp x ws ) == (length ws) - where - ws = nub is - size = length . index - - --- --------------------------------------------------------------------- --- 'delete' - --- deleting the current item removes it. -prop_delete x = - case peek x of - Nothing -> True - Just i -> not (member i (delete i x)) - where _ = x :: T - --- delete is reversible with 'insert'. --- It is the identiy, except for the 'master', which is reset on insert and delete. --- -prop_delete_insert (x :: T) = - case peek x of - Nothing -> True - Just n -> insertUp n (delete n y) == y - where - y = swapMaster x - --- delete should be local -prop_delete_local (x :: T) = - case peek x of - Nothing -> True - Just i -> hidden_spaces x == hidden_spaces (delete i x) - --- delete should not affect focus unless the focused element is what is being deleted -prop_delete_focus n (x :: T) = member n x && Just n /= peek x ==> peek (delete n x) == peek x - --- focus movement in the presence of delete: --- when the last window in the stack set is focused, focus moves `up'. --- usual case is that it moves 'down'. -prop_delete_focus_end (x :: T) = - length (index x) > 1 - ==> - peek (delete n y) == peek (focusUp y) - where - n = last (index x) - y = focusWindow n x -- focus last window in stack - --- focus movement in the presence of delete: --- when not in the last item in the stack, focus moves down -prop_delete_focus_not_end (x :: T) = - length (index x) > 1 && - n /= last (index x) - ==> - peek (delete n x) == peek (focusDown x) - where - Just n = peek x - --- --------------------------------------------------------------------- --- filter - --- preserve order -prop_filter_order (x :: T) = - case stack $ workspace $ current x of - Nothing -> True - Just s@(Stack i _ _) -> integrate' (S.filter (/= i) s) == filter (/= i) (integrate' (Just s)) - --- --------------------------------------------------------------------- --- swapUp, swapDown, swapMaster: reordiring windows - --- swap is trivially reversible -prop_swap_left (x :: T) = (swapUp (swapDown x)) == x -prop_swap_right (x :: T) = (swapDown (swapUp x)) == x --- TODO swap is reversible --- swap is reversible, but involves moving focus back the window with --- master on it. easy to do with a mouse... -{- -prop_promote_reversible x b = (not . null . fromMaybe [] . flip index x . current $ x) ==> - (raiseFocus y . promote . raiseFocus z . promote) x == x - where _ = x :: T - dir = if b then LT else GT - (Just y) = peek x - (Just (z:_)) = flip index x . current $ x --} - --- swap doesn't change focus -prop_swap_master_focus (x :: T) = peek x == (peek $ swapMaster x) --- = case peek x of --- Nothing -> True --- Just f -> focus (stack (workspace $ current (swap x))) == f -prop_swap_left_focus (x :: T) = peek x == (peek $ swapUp x) -prop_swap_right_focus (x :: T) = peek x == (peek $ swapDown x) - --- swap is local -prop_swap_master_local (x :: T) = hidden_spaces x == hidden_spaces (swapMaster x) -prop_swap_left_local (x :: T) = hidden_spaces x == hidden_spaces (swapUp x) -prop_swap_right_local (x :: T) = hidden_spaces x == hidden_spaces (swapDown x) - --- rotation through the height of a stack gets us back to the start -prop_swap_all_l (x :: T) = (foldr (const swapUp) x [1..n]) == x - where n = length (index x) -prop_swap_all_r (x :: T) = (foldr (const swapDown) x [1..n]) == x - where n = length (index x) - -prop_swap_master_idempotent (x :: T) = swapMaster (swapMaster x) == swapMaster x - --- --------------------------------------------------------------------- --- shift - --- shift is fully reversible on current window, when focus and master --- are the same. otherwise, master may move. -prop_shift_reversible i (x :: T) = - i `tagMember` x ==> case peek y of - Nothing -> True - Just _ -> normal ((view n . shift n . view i . shift i) y) == normal y - where - y = swapMaster x - n = tag (workspace $ current y) - ------------------------------------------------------------------------- --- shiftMaster - --- focus/local/idempotent same as swapMaster: -prop_shift_master_focus (x :: T) = peek x == (peek $ shiftMaster x) -prop_shift_master_local (x :: T) = hidden_spaces x == hidden_spaces (shiftMaster x) -prop_shift_master_idempotent (x :: T) = shiftMaster (shiftMaster x) == shiftMaster x --- ordering is constant modulo the focused window: -prop_shift_master_ordering (x :: T) = case peek x of - Nothing -> True - Just m -> L.delete m (index x) == L.delete m (index $ shiftMaster x) - --- --------------------------------------------------------------------- --- shiftWin - --- shiftWin on current window is the same as shift -prop_shift_win_focus i (x :: T) = - i `tagMember` x ==> case peek x of - Nothing -> True - Just w -> shiftWin i w x == shift i x - --- shiftWin on a non-existant window is identity -prop_shift_win_indentity i w (x :: T) = - i `tagMember` x && not (w `member` x) ==> shiftWin i w x == x - --- shiftWin leaves the current screen as it is, if neither i is the tag --- of the current workspace nor w on the current workspace -prop_shift_win_fix_current i w (x :: T) = - i `tagMember` x && w `member` x && i /= n && findTag w x /= Just n - ==> (current $ x) == (current $ shiftWin i w x) - where - n = tag (workspace $ current x) - ------------------------------------------------------------------------- --- properties for the floating layer: - -prop_float_reversible n (x :: T) = - n `member` x ==> sink n (float n geom x) == x - where - geom = RationalRect 100 100 100 100 - -prop_float_geometry n (x :: T) = - n `member` x ==> let s = float n geom x - in M.lookup n (floating s) == Just geom - where - geom = RationalRect 100 100 100 100 - -prop_float_delete n (x :: T) = - n `member` x ==> let s = float n geom x - t = delete n s - in not (n `member` t) - where - geom = RationalRect 100 100 100 100 - - ------------------------------------------------------------------------- - -prop_screens (x :: T) = n `elem` screens x - where - n = current x - -prop_differentiate xs = - if null xs then differentiate xs == Nothing - else (differentiate xs) == Just (Stack (head xs) [] (tail xs)) - where _ = xs :: [Int] - --- looking up the tag of the current workspace should always produce a tag. -prop_lookup_current (x :: T) = lookupWorkspace scr x == Just tg - where - (Screen (Workspace tg _ _) scr _) = current x - --- looking at a visible tag -prop_lookup_visible (x :: T) = - visible x /= [] ==> - fromJust (lookupWorkspace scr x) `elem` tags - where - tags = [ tag (workspace y) | y <- visible x ] - scr = last [ screen y | y <- visible x ] --- --------------------------------------------------------------------- --- testing for failure - --- and help out hpc -prop_abort x = unsafePerformIO $ C.catch (abort "fail") - (\(C.SomeException e) -> return $ show e == "xmonad: StackSet: fail" ) - where - _ = x :: Int - --- new should fail with an abort -prop_new_abort x = unsafePerformIO $ C.catch f - (\(C.SomeException e) -> return $ show e == "xmonad: StackSet: non-positive argument to StackSet.new" ) - where - f = new undefined{-layout-} [] [] `seq` return False - - _ = x :: Int - --- prop_view_should_fail = view {- with some bogus data -} - --- screens makes sense -prop_screens_works (x :: T) = screens x == current x : visible x - ------------------------------------------------------------------------- --- renaming tags - --- | Rename a given tag if present in the StackSet. --- 408 renameTag :: Eq i => i -> i -> StackSet i l a s sd -> StackSet i l a s sd - -prop_rename1 (x::T) o n = o `tagMember` x && not (n `tagMember` x) ==> - let y = renameTag o n x - in n `tagMember` y - --- | --- Ensure that a given set of workspace tags is present by renaming --- existing workspaces and\/or creating new hidden workspaces as --- necessary. --- -prop_ensure (x :: T) l xs = let y = ensureTags l xs x - in and [ n `tagMember` y | n <- xs ] - --- adding a tag should create a new hidden workspace -prop_ensure_append (x :: T) l n = - not (n `tagMember` x) - ==> - (hidden y /= hidden x -- doesn't append, renames - && - and [ isNothing (stack z) && layout z == l | z <- hidden y, tag z == n ] - ) - where - y = ensureTags l (n:ts) x - ts = [ tag z | z <- workspaces x ] - -prop_mapWorkspaceId (x::T) = x == mapWorkspace id x - -prop_mapWorkspaceInverse (x::T) = x == mapWorkspace predTag (mapWorkspace succTag x) - where predTag w = w { tag = pred $ tag w } - succTag w = w { tag = succ $ tag w } - -prop_mapLayoutId (x::T) = x == mapLayout id x - -prop_mapLayoutInverse (x::T) = x == mapLayout pred (mapLayout succ x) - ------------------------------------------------------------------------- --- The Tall layout - --- 1 window should always be tiled fullscreen -prop_tile_fullscreen rect = tile pct rect 1 1 == [rect] - where pct = 1/2 - --- multiple windows -prop_tile_non_overlap rect windows nmaster = noOverlaps (tile pct rect nmaster windows) - where _ = rect :: Rectangle - pct = 3 % 100 - --- splitting horizontally yields sensible results -prop_split_hoziontal (NonNegative n) x = -{- - trace (show (rect_x x - ,rect_width x - ,rect_x x + fromIntegral (rect_width x) - ,map rect_x xs)) - $ --} - - sum (map rect_width xs) == rect_width x - && - all (== rect_height x) (map rect_height xs) - && - (map rect_x xs) == (sort $ map rect_x xs) - - where - xs = splitHorizontally n x - --- splitting horizontally yields sensible results -prop_splitVertically (r :: Rational) x = - - rect_x x == rect_x a && rect_x x == rect_x b - && - rect_width x == rect_width a && rect_width x == rect_width b - -{- - trace (show (rect_x x - ,rect_width x - ,rect_x x + fromIntegral (rect_width x) - ,map rect_x xs)) - $ --} - - where - (a,b) = splitVerticallyBy r x - - --- pureLayout works. -prop_purelayout_tall n r1 r2 rect (t :: T) = - isJust (peek t) ==> - length ts == length (index t) - && - noOverlaps (map snd ts) - && - description layoot == "Tall" - where layoot = Tall n r1 r2 - st = fromJust . stack . workspace . current $ t - ts = pureLayout layoot rect st - --- Test message handling of Tall - --- what happens when we send a Shrink message to Tall -prop_shrink_tall (NonNegative n) (NonZero (NonNegative delta)) (NonNegative frac) = - n == n' && delta == delta' -- these state components are unchanged - && frac' <= frac && (if frac' < frac then frac' == 0 || frac' == frac - delta - else frac == 0 ) - -- remaining fraction should shrink - where - l1 = Tall n delta frac - Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage Shrink) - -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) - - --- what happens when we send a Shrink message to Tall -prop_expand_tall (NonNegative n) - (NonZero (NonNegative delta)) - (NonNegative n1) - (NonZero (NonNegative d1)) = - - n == n' - && delta == delta' -- these state components are unchanged - && frac' >= frac - && (if frac' > frac - then frac' == 1 || frac' == frac + delta - else frac == 1 ) - - -- remaining fraction should shrink - where - frac = min 1 (n1 % d1) - l1 = Tall n delta frac - Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage Expand) - -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) - --- what happens when we send an IncMaster message to Tall -prop_incmaster_tall (NonNegative n) (NonZero (NonNegative delta)) (NonNegative frac) - (NonNegative k) = - delta == delta' && frac == frac' && n' == n + k - where - l1 = Tall n delta frac - Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage (IncMasterN k)) - -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) - - - - -- toMessage LT = SomeMessage Shrink - -- toMessage EQ = SomeMessage Expand - -- toMessage GT = SomeMessage (IncMasterN 1) - - ------------------------------------------------------------------------- --- Full layout - --- pureLayout works for Full -prop_purelayout_full rect (t :: T) = - isJust (peek t) ==> - length ts == 1 -- only one window to view - && - snd (head ts) == rect -- and sets fullscreen - && - fst (head ts) == fromJust (peek t) -- and the focused window is shown - - where layoot = Full - st = fromJust . stack . workspace . current $ t - ts = pureLayout layoot rect st - --- what happens when we send an IncMaster message to Full --- Nothing -prop_sendmsg_full (NonNegative k) = - isNothing (Full `pureMessage` (SomeMessage (IncMasterN k))) - -prop_desc_full = description Full == show Full - ------------------------------------------------------------------------- - -prop_desc_mirror n r1 r2 = description (Mirror $! t) == "Mirror Tall" - where t = Tall n r1 r2 - ------------------------------------------------------------------------- - -noOverlaps [] = True -noOverlaps [_] = True -noOverlaps xs = and [ verts a `notOverlap` verts b - | a <- xs - , b <- filter (a /=) xs - ] - where - verts (Rectangle a b w h) = (a,b,a + fromIntegral w - 1, b + fromIntegral h - 1) - - notOverlap (left1,bottom1,right1,top1) - (left2,bottom2,right2,top2) - = (top1 < bottom2 || top2 < bottom1) - || (right1 < left2 || right2 < left1) - ------------------------------------------------------------------------- --- Aspect ratios - -prop_resize_inc (NonZero (NonNegative inc_w),NonZero (NonNegative inc_h)) b@(w,h) = - w' `mod` inc_w == 0 && h' `mod` inc_h == 0 - where (w',h') = applyResizeIncHint a b - a = (inc_w,inc_h) - -prop_resize_inc_extra ((NonNegative inc_w)) b@(w,h) = - (w,h) == (w',h') - where (w',h') = applyResizeIncHint a b - a = (-inc_w,0::Dimension)-- inc_h) - -prop_resize_max (NonZero (NonNegative inc_w),NonZero (NonNegative inc_h)) b@(w,h) = - w' <= inc_w && h' <= inc_h - where (w',h') = applyMaxSizeHint a b - a = (inc_w,inc_h) - -prop_resize_max_extra ((NonNegative inc_w)) b@(w,h) = - (w,h) == (w',h') - where (w',h') = applyMaxSizeHint a b - a = (-inc_w,0::Dimension)-- inc_h) - ------------------------------------------------------------------------- - main :: IO () main = do - args <- fmap (drop 1) getArgs - let n = if null args then 100 else read (head args) - (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-40s: " s >> a n) tests - printf "Passed %d tests!\n" (sum passed) - when (not . and $ results) $ fail "Not all tests passed!" - where - - tests = - [("StackSet invariants" , mytest prop_invariant) - - ,("empty: invariant" , mytest prop_empty_I) - ,("empty is empty" , mytest prop_empty) - ,("empty / current" , mytest prop_empty_current) - ,("empty / member" , mytest prop_member_empty) - - ,("view : invariant" , mytest prop_view_I) - ,("view sets current" , mytest prop_view_current) - ,("view idempotent" , mytest prop_view_idem) - ,("view reversible" , mytest prop_view_reversible) --- ,("view / xinerama" , mytest prop_view_xinerama) - ,("view is local" , mytest prop_view_local) - - ,("greedyView : invariant" , mytest prop_greedyView_I) - ,("greedyView sets current" , mytest prop_greedyView_current) - ,("greedyView is safe " , mytest prop_greedyView_current_id) - ,("greedyView idempotent" , mytest prop_greedyView_idem) - ,("greedyView reversible" , mytest prop_greedyView_reversible) - ,("greedyView is local" , mytest prop_greedyView_local) --- --- ,("valid workspace xinerama", mytest prop_lookupWorkspace) - - ,("peek/member " , mytest prop_member_peek) - - ,("index/length" , mytest prop_index_length) - - ,("focus left : invariant", mytest prop_focusUp_I) - ,("focus master : invariant", mytest prop_focusMaster_I) - ,("focus right: invariant", mytest prop_focusDown_I) - ,("focusWindow: invariant", mytest prop_focus_I) - ,("focus left/master" , mytest prop_focus_left_master) - ,("focus right/master" , mytest prop_focus_right_master) - ,("focus master/master" , mytest prop_focus_master_master) - ,("focusWindow master" , mytest prop_focusWindow_master) - ,("focus left/right" , mytest prop_focus_left) - ,("focus right/left" , mytest prop_focus_right) - ,("focus all left " , mytest prop_focus_all_l) - ,("focus all right " , mytest prop_focus_all_r) - ,("focus down is local" , mytest prop_focus_down_local) - ,("focus up is local" , mytest prop_focus_up_local) - ,("focus master is local" , mytest prop_focus_master_local) - ,("focus master idemp" , mytest prop_focusMaster_idem) - - ,("focusWindow is local", mytest prop_focusWindow_local) - ,("focusWindow works" , mytest prop_focusWindow_works) - ,("focusWindow identity", mytest prop_focusWindow_identity) - - ,("findTag" , mytest prop_findIndex) - ,("allWindows/member" , mytest prop_allWindowsMember) - ,("currentTag" , mytest prop_currentTag) - - ,("insert: invariant" , mytest prop_insertUp_I) - ,("insert/new" , mytest prop_insert_empty) - ,("insert is idempotent", mytest prop_insert_idem) - ,("insert is reversible", mytest prop_insert_delete) - ,("insert is local" , mytest prop_insert_local) - ,("insert duplicates" , mytest prop_insert_duplicate) - ,("insert/peek " , mytest prop_insert_peek) - ,("insert/size" , mytest prop_size_insert) - - ,("delete: invariant" , mytest prop_delete_I) - ,("delete/empty" , mytest prop_empty) - ,("delete/member" , mytest prop_delete) - ,("delete is reversible", mytest prop_delete_insert) - ,("delete is local" , mytest prop_delete_local) - ,("delete/focus" , mytest prop_delete_focus) - ,("delete last/focus up", mytest prop_delete_focus_end) - ,("delete ~last/focus down", mytest prop_delete_focus_not_end) - - ,("filter preserves order", mytest prop_filter_order) - - ,("swapMaster: invariant", mytest prop_swap_master_I) - ,("swapUp: invariant" , mytest prop_swap_left_I) - ,("swapDown: invariant", mytest prop_swap_right_I) - ,("swapMaster id on focus", mytest prop_swap_master_focus) - ,("swapUp id on focus", mytest prop_swap_left_focus) - ,("swapDown id on focus", mytest prop_swap_right_focus) - ,("swapMaster is idempotent", mytest prop_swap_master_idempotent) - ,("swap all left " , mytest prop_swap_all_l) - ,("swap all right " , mytest prop_swap_all_r) - ,("swapMaster is local" , mytest prop_swap_master_local) - ,("swapUp is local" , mytest prop_swap_left_local) - ,("swapDown is local" , mytest prop_swap_right_local) - - ,("shiftMaster id on focus", mytest prop_shift_master_focus) - ,("shiftMaster is local", mytest prop_shift_master_local) - ,("shiftMaster is idempotent", mytest prop_shift_master_idempotent) - ,("shiftMaster preserves ordering", mytest prop_shift_master_ordering) - - ,("shift: invariant" , mytest prop_shift_I) - ,("shift is reversible" , mytest prop_shift_reversible) - ,("shiftWin: invariant" , mytest prop_shift_win_I) - ,("shiftWin is shift on focus" , mytest prop_shift_win_focus) - ,("shiftWin fix current" , mytest prop_shift_win_fix_current) - - ,("floating is reversible" , mytest prop_float_reversible) - ,("floating sets geometry" , mytest prop_float_geometry) - ,("floats can be deleted", mytest prop_float_delete) - ,("screens includes current", mytest prop_screens) - - ,("differentiate works", mytest prop_differentiate) - ,("lookupTagOnScreen", mytest prop_lookup_current) - ,("lookupTagOnVisbleScreen", mytest prop_lookup_visible) - ,("screens works", mytest prop_screens_works) - ,("renaming works", mytest prop_rename1) - ,("ensure works", mytest prop_ensure) - ,("ensure hidden semantics", mytest prop_ensure_append) - - ,("mapWorkspace id", mytest prop_mapWorkspaceId) - ,("mapWorkspace inverse", mytest prop_mapWorkspaceInverse) - ,("mapLayout id", mytest prop_mapLayoutId) - ,("mapLayout inverse", mytest prop_mapLayoutInverse) - - -- testing for failure: - ,("abort fails", mytest prop_abort) - ,("new fails with abort", mytest prop_new_abort) - ,("shiftWin identity", mytest prop_shift_win_indentity) - - -- tall layout - - ,("tile 1 window fullsize", mytest prop_tile_fullscreen) - ,("tiles never overlap", mytest prop_tile_non_overlap) - ,("split hozizontally", mytest prop_split_hoziontal) - ,("split verticalBy", mytest prop_splitVertically) - - ,("pure layout tall", mytest prop_purelayout_tall) - ,("send shrink tall", mytest prop_shrink_tall) - ,("send expand tall", mytest prop_expand_tall) - ,("send incmaster tall", mytest prop_incmaster_tall) - - -- full layout - - ,("pure layout full", mytest prop_purelayout_full) - ,("send message full", mytest prop_sendmsg_full) - ,("describe full", mytest prop_desc_full) - - ,("describe mirror", mytest prop_desc_mirror) - - -- resize hints - ,("window hints: inc", mytest prop_resize_inc) - ,("window hints: inc all", mytest prop_resize_inc_extra) - ,("window hints: max", mytest prop_resize_max) - ,("window hints: max all ", mytest prop_resize_max_extra) - - ] - ------------------------------------------------------------------------- --- --- QC driver --- - -debug = False - -mytest :: Testable a => a -> Int -> IO (Bool, Int) -mytest a n = mycheck defaultConfig - { configMaxTest=n - , configEvery = \n args -> let s = show n in s ++ [ '\b' | _ <- s ] } a - -- , configEvery= \n args -> if debug then show n ++ ":\n" ++ unlines args else [] } a - -mycheck :: Testable a => Config -> a -> IO (Bool, Int) -mycheck config a = do - rnd <- newStdGen - mytests config (evaluate a) rnd 0 0 [] - -mytests :: Config -> Gen Result -> StdGen -> Int -> Int -> [[String]] -> IO (Bool, Int) -mytests config gen rnd0 ntest nfail stamps - | ntest == configMaxTest config = done "OK," ntest stamps >> return (True, ntest) - | nfail == configMaxFail config = done "Arguments exhausted after" ntest stamps >> return (True, ntest) - | otherwise = - do putStr (configEvery config ntest (arguments result)) >> hFlush stdout - case ok result of - Nothing -> - mytests config gen rnd1 ntest (nfail+1) stamps - Just True -> - mytests config gen rnd1 (ntest+1) nfail (stamp result:stamps) - Just False -> - putStr ( "Falsifiable after " - ++ show ntest - ++ " tests:\n" - ++ unlines (arguments result) - ) >> hFlush stdout >> return (False, ntest) - where - result = generate (configSize config ntest) rnd2 gen - (rnd1,rnd2) = split rnd0 - -done :: String -> Int -> [[String]] -> IO () -done mesg ntest stamps = putStr ( mesg ++ " " ++ show ntest ++ " tests" ++ table ) - where - table = display - . map entry - . reverse - . sort - . map pairLength - . group - . sort - . filter (not . null) - $ stamps - - display [] = ".\n" - display [x] = " (" ++ x ++ ").\n" - display xs = ".\n" ++ unlines (map (++ ".") xs) - - pairLength xss@(xs:_) = (length xss, xs) - entry (n, xs) = percentage n ntest - ++ " " - ++ concat (intersperse ", " xs) - - percentage n m = show ((100 * n) `div` m) ++ "%" - ------------------------------------------------------------------------- - -instance Arbitrary Char where - arbitrary = choose ('a','z') - coarbitrary n = coarbitrary (ord n) - -instance Random Word8 where - randomR = integralRandomR - random = randomR (minBound,maxBound) - -instance Arbitrary Word8 where - arbitrary = choose (minBound,maxBound) - coarbitrary n = variant (fromIntegral ((fromIntegral n) `rem` 4)) - -instance Random Word64 where - randomR = integralRandomR - random = randomR (minBound,maxBound) - -instance Arbitrary Word64 where - arbitrary = choose (minBound,maxBound) - coarbitrary n = variant (fromIntegral ((fromIntegral n) `rem` 4)) - -integralRandomR :: (Integral a, RandomGen g) => (a,a) -> g -> (a,g) -integralRandomR (a,b) g = case randomR (fromIntegral a :: Integer, - fromIntegral b :: Integer) g of - (x,g) -> (fromIntegral x, g) - -instance Arbitrary Position where - arbitrary = do n <- arbitrary :: Gen Word8 - return (fromIntegral n) - coarbitrary = undefined - -instance Arbitrary Dimension where - arbitrary = do n <- arbitrary :: Gen Word8 - return (fromIntegral n) - coarbitrary = undefined - -instance Arbitrary Rectangle where - arbitrary = do - sx <- arbitrary - sy <- arbitrary - sw <- arbitrary - sh <- arbitrary - return $ Rectangle sx sy sw sh - coarbitrary = undefined - -instance Arbitrary Rational where - arbitrary = do - n <- arbitrary - d' <- arbitrary - let d = if d' == 0 then 1 else d' - return (n % d) - coarbitrary = undefined - ------------------------------------------------------------------------- --- QC 2 - --- from QC2 --- | NonEmpty xs: guarantees that xs is non-empty. -newtype NonEmptyList a = NonEmpty [a] - deriving ( Eq, Ord, Show, Read ) - -instance Arbitrary a => Arbitrary (NonEmptyList a) where - arbitrary = NonEmpty `fmap` (arbitrary `suchThat` (not . null)) - coarbitrary = undefined - -newtype NonEmptyNubList a = NonEmptyNubList [a] - deriving ( Eq, Ord, Show, Read ) - -instance (Eq a, Arbitrary a) => Arbitrary (NonEmptyNubList a) where - arbitrary = NonEmptyNubList `fmap` ((liftM nub arbitrary) `suchThat` (not . null)) - coarbitrary = undefined - -type Positive a = NonZero (NonNegative a) - -newtype NonZero a = NonZero a - deriving ( Eq, Ord, Num, Integral, Real, Enum, Show, Read ) - -instance (Num a, Ord a, Arbitrary a) => Arbitrary (NonZero a) where - arbitrary = fmap NonZero $ arbitrary `suchThat` (/= 0) - coarbitrary = undefined - -newtype NonNegative a = NonNegative a - deriving ( Eq, Ord, Num, Integral, Real, Enum, Show, Read ) - -instance (Num a, Ord a, Arbitrary a) => Arbitrary (NonNegative a) where - arbitrary = - frequency - [ (5, (NonNegative . abs) `fmap` arbitrary) - , (1, return 0) - ] - coarbitrary = undefined - -newtype EmptyStackSet = EmptyStackSet T deriving Show - -instance Arbitrary EmptyStackSet where - arbitrary = do - (NonEmptyNubList ns) <- arbitrary - (NonEmptyNubList sds) <- arbitrary - l <- arbitrary - -- there cannot be more screens than workspaces: - return . EmptyStackSet . new l ns $ take (min (length ns) (length sds)) sds - coarbitrary = error "coarbitrary EmptyStackSet" + arg <- fmap (drop 1) getArgs + let n = if null arg then 100 else read $ head arg + args = stdArgs { maxSuccess = n, maxSize = 100 } + qc = quickCheckWithResult args + perform (s, t) = printf "%-35s: " s >> qc t + mapM_ perform tests + + +tests = + [("StackSet invariants", property prop_invariant) + ,("empty: invariant", property prop_empty_I) + ,("empty is empty", property prop_empty) + ,("empty / current", property prop_empty_current) + ,("empty / member", property prop_member_empty) + + + ,("view : invariant", property prop_view_I) + ,("view sets current", property prop_view_current) + ,("view idempotent", property prop_view_idem) + ,("view reversible", property prop_view_reversible) + + ,("view is local", property prop_view_local) + + ,("greedyView : invariant", property prop_greedyView_I) + ,("greedyView sets current", property prop_greedyView_current) + ,("greedyView is safe", property prop_greedyView_current_id) + ,("greedyView idempotent", property prop_greedyView_idem) + ,("greedyView reversible", property prop_greedyView_reversible) + ,("greedyView is local", property prop_greedyView_local) + + ,("peek/member", property prop_member_peek) + + ,("index/length", property prop_index_length) + + ,("focus left : invariant", property prop_focusUp_I) + ,("focus master : invariant", property prop_focusMaster_I) + ,("focus right: invariant", property prop_focusDown_I) + ,("focusWindow: invariant", property prop_focus_I) + ,("focus left/master", property prop_focus_left_master) + ,("focus right/master", property prop_focus_right_master) + ,("focus master/master", property prop_focus_master_master) + ,("focusWindow master", property prop_focusWindow_master) + ,("focus left/right", property prop_focus_left) + ,("focus right/left", property prop_focus_right) + ,("focus all left", property prop_focus_all_l) + ,("focus all right", property prop_focus_all_r) + ,("focus down is local", property prop_focus_down_local) + ,("focus up is local", property prop_focus_up_local) + ,("focus master is local", property prop_focus_master_local) + ,("focus master idemp", property prop_focusMaster_idem) + + ,("focusWindow is local", property prop_focusWindow_local) + ,("focusWindow works" , property prop_focusWindow_works) + ,("focusWindow identity", property prop_focusWindow_identity) + + ,("findTag", property prop_findIndex) + ,("allWindows/member", property prop_allWindowsMember) + ,("currentTag", property prop_currentTag) + + ,("insert: invariant", property prop_insertUp_I) + ,("insert/new", property prop_insert_empty) + ,("insert is idempotent", property prop_insert_idem) + ,("insert is reversible", property prop_insert_delete) + ,("insert is local", property prop_insert_local) + ,("insert duplicates", property prop_insert_duplicate) + ,("insert/peek", property prop_insert_peek) + ,("insert/size", property prop_size_insert) + + ,("delete: invariant", property prop_delete_I) + ,("delete/empty", property prop_empty) + ,("delete/member", property prop_delete) + ,("delete is reversible", property prop_delete_insert) + ,("delete is local", property prop_delete_local) + ,("delete/focus", property prop_delete_focus) + ,("delete last/focus up", property prop_delete_focus_end) + ,("delete ~last/focus down", property prop_delete_focus_not_end) + + ,("filter preserves order", property prop_filter_order) + + ,("swapMaster: invariant", property prop_swap_master_I) + ,("swapUp: invariant" , property prop_swap_left_I) + ,("swapDown: invariant", property prop_swap_right_I) + ,("swapMaster id on focus", property prop_swap_master_focus) + ,("swapUp id on focus", property prop_swap_left_focus) + ,("swapDown id on focus", property prop_swap_right_focus) + ,("swapMaster is idempotent", property prop_swap_master_idempotent) + ,("swap all left", property prop_swap_all_l) + ,("swap all right", property prop_swap_all_r) + ,("swapMaster is local", property prop_swap_master_local) + ,("swapUp is local", property prop_swap_left_local) + ,("swapDown is local", property prop_swap_right_local) + + ,("shiftMaster id on focus", property prop_shift_master_focus) + ,("shiftMaster is local", property prop_shift_master_local) + ,("shiftMaster is idempotent", property prop_shift_master_idempotent) + ,("shiftMaster preserves ordering", property prop_shift_master_ordering) + + ,("shift: invariant" , property prop_shift_I) + ,("shift is reversible" , property prop_shift_reversible) + ,("shiftWin: invariant" , property prop_shift_win_I) + ,("shiftWin is shift on focus", property prop_shift_win_focus) + ,("shiftWin fix current" , property prop_shift_win_fix_current) + + ,("floating is reversible" , property prop_float_reversible) + ,("floating sets geometry" , property prop_float_geometry) + ,("floats can be deleted", property prop_float_delete) + ,("screens includes current", property prop_screens) + + ,("differentiate works", property prop_differentiate) + ,("lookupTagOnScreen", property prop_lookup_current) + ,("lookupTagOnVisbleScreen", property prop_lookup_visible) + ,("screens works", property prop_screens_works) + ,("renaming works", property prop_rename1) + ,("ensure works", property prop_ensure) + ,("ensure hidden semantics", property prop_ensure_append) + + ,("mapWorkspace id", property prop_mapWorkspaceId) + ,("mapWorkspace inverse", property prop_mapWorkspaceInverse) + ] --- | Generates a value that satisfies a predicate. -suchThat :: Gen a -> (a -> Bool) -> Gen a -gen `suchThat` p = - do mx <- gen `suchThatMaybe` p - case mx of - Just x -> return x - Nothing -> sized (\n -> resize (n+1) (gen `suchThat` p)) --- | Tries to generate a value that satisfies a predicate. -suchThatMaybe :: Gen a -> (a -> Bool) -> Gen (Maybe a) -gen `suchThatMaybe` p = sized (try 0 . max 1) - where - try _ 0 = return Nothing - try k n = do x <- resize (2*k+n) gen - if p x then return (Just x) else try (k+1) (n-1) diff --git a/tests/Properties/Delete.hs b/tests/Properties/Delete.hs new file mode 100644 index 0000000..6fb7566 --- /dev/null +++ b/tests/Properties/Delete.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Delete where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +-- --------------------------------------------------------------------- +-- 'delete' + +-- deleting the current item removes it. +prop_delete x = + case peek x of + Nothing -> True + Just i -> not (member i (delete i x)) + where _ = x :: T + +-- delete is reversible with 'insert'. +-- It is the identiy, except for the 'master', which is reset on insert and delete. +-- +prop_delete_insert (x :: T) = + case peek x of + Nothing -> True + Just n -> insertUp n (delete n y) == y + where + y = swapMaster x + +-- delete should be local +prop_delete_local (x :: T) = + case peek x of + Nothing -> True + Just i -> hidden_spaces x == hidden_spaces (delete i x) + +-- delete should not affect focus unless the focused element is what is being deleted +prop_delete_focus = do + -- There should be at least two windows. One in focus, and some to try and + -- delete (doesn't have to be windows on the current workspace). We generate + -- our own, since we can't rely on NonEmptyWindowsStackSet returning one in + -- the argument with at least two windows. + x <- arbitrary `suchThat` \x' -> length (allWindows x') >= 2 + w <- arbitraryWindow (NonEmptyWindowsStackSet x) + -- Make sure we pick a window that is NOT the currently focused + `suchThat` \w' -> Just w' /= peek x + return $ peek (delete w x) == peek x + +-- focus movement in the presence of delete: +-- when the last window in the stack set is focused, focus moves `up'. +-- usual case is that it moves 'down'. +prop_delete_focus_end = do + -- Generate a StackSet with at least two windows on the current workspace. + x <- arbitrary `suchThat` \(x' :: T) -> length (index x') >= 2 + let w = last (index x) + y = focusWindow w x -- focus last window in stack + return $ peek (delete w y) == peek (focusUp y) + + +-- focus movement in the presence of delete: +-- when not in the last item in the stack, focus moves down +prop_delete_focus_not_end = do + x <- arbitrary + -- There must be at least two windows and the current focused is not the + -- last one in the stack. + `suchThat` \(x' :: T) -> + let currWins = index x' + in length (currWins) >= 2 && peek x' /= Just (last currWins) + -- This is safe, as we know there are >= 2 windows + let Just n = peek x + return $ peek (delete n x) == peek (focusDown x) diff --git a/tests/Properties/Failure.hs b/tests/Properties/Failure.hs new file mode 100644 index 0000000..fc7a359 --- /dev/null +++ b/tests/Properties/Failure.hs @@ -0,0 +1,26 @@ +module Properties.Failure where + +import XMonad.StackSet hiding (filter) + +import qualified Control.Exception.Extensible as C +import System.IO.Unsafe + +-- --------------------------------------------------------------------- +-- testing for failure + +-- and help out hpc +prop_abort x = unsafePerformIO $ C.catch (abort "fail") + (\(C.SomeException e) -> return $ show e == "xmonad: StackSet: fail" ) + where + _ = x :: Int + +-- new should fail with an abort +prop_new_abort x = unsafePerformIO $ C.catch f + (\(C.SomeException e) -> return $ show e == "xmonad: StackSet: non-positive argument to StackSet.new" ) + where + f = new undefined{-layout-} [] [] `seq` return False + + _ = x :: Int + +-- TODO: Fix this? +-- prop_view_should_fail = view {- with some bogus data -} diff --git a/tests/Properties/Floating.hs b/tests/Properties/Floating.hs new file mode 100644 index 0000000..a9afad7 --- /dev/null +++ b/tests/Properties/Floating.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Floating where + +import Test.QuickCheck +import Instances + +import XMonad.StackSet hiding (filter) + +import qualified Data.Map as M + +------------------------------------------------------------------------ +-- properties for the floating layer: + +prop_float_reversible (nex :: NonEmptyWindowsStackSet) = do + let NonEmptyWindowsStackSet x = nex + w <- arbitraryWindow nex + return $ sink w (float w geom x) == x + where + geom = RationalRect 100 100 100 100 + +prop_float_geometry (nex :: NonEmptyWindowsStackSet) = do + let NonEmptyWindowsStackSet x = nex + w <- arbitraryWindow nex + let s = float w geom x + return $ M.lookup w (floating s) == Just geom + where + geom = RationalRect 100 100 100 100 + +prop_float_delete (nex :: NonEmptyWindowsStackSet) = do + let NonEmptyWindowsStackSet x = nex + w <- arbitraryWindow nex + let s = float w geom x + t = delete w s + return $ not (w `member` t) + where + geom = RationalRect 100 100 100 100 diff --git a/tests/Properties/Focus.hs b/tests/Properties/Focus.hs new file mode 100644 index 0000000..865dc72 --- /dev/null +++ b/tests/Properties/Focus.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Focus where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import Data.Maybe (fromJust) + +-- --------------------------------------------------------------------- +-- rotating focus +-- + +-- master/focus +-- +-- The tiling order, and master window, of a stack is unaffected by focus changes. +-- +prop_focus_left_master (SizedPositive n) (x::T) = + index (applyN (Just n) focusUp x) == index x +prop_focus_right_master (SizedPositive n) (x::T) = + index (applyN (Just n) focusDown x) == index x +prop_focus_master_master (SizedPositive n) (x::T) = + index (applyN (Just n) focusMaster x) == index x + +prop_focusWindow_master (NonNegative n) (x :: T) = + case peek x of + Nothing -> True + Just _ -> let s = index x + i = n `mod` length s + in index (focusWindow (s !! i) x) == index x + +-- shifting focus is trivially reversible +prop_focus_left (x :: T) = (focusUp (focusDown x)) == x +prop_focus_right (x :: T) = (focusDown (focusUp x)) == x + +-- focus master is idempotent +prop_focusMaster_idem (x :: T) = focusMaster x == focusMaster (focusMaster x) + +-- focusWindow actually leaves the window focused... +prop_focusWindow_works (n :: NonNegative Int) (x :: T) = + case peek x of + Nothing -> True + Just _ -> let s = index x + i = fromIntegral n `mod` length s + in (focus . fromJust . stack . workspace . current) (focusWindow (s !! i) x) == (s !! i) + +-- rotation through the height of a stack gets us back to the start +prop_focus_all_l (x :: T) = (foldr (const focusUp) x [1..n]) == x + where n = length (index x) +prop_focus_all_r (x :: T) = (foldr (const focusDown) x [1..n]) == x + where n = length (index x) + +-- prop_rotate_all (x :: T) = f (f x) == f x +-- f x' = foldr (\_ y -> rotate GT y) x' [1..n] + +-- focus is local to the current workspace +prop_focus_down_local (x :: T) = hidden_spaces (focusDown x) == hidden_spaces x +prop_focus_up_local (x :: T) = hidden_spaces (focusUp x) == hidden_spaces x + +prop_focus_master_local (x :: T) = hidden_spaces (focusMaster x) == hidden_spaces x + +prop_focusWindow_local (n :: NonNegative Int) (x::T ) = + case peek x of + Nothing -> True + Just _ -> let s = index x + i = fromIntegral n `mod` length s + in hidden_spaces (focusWindow (s !! i) x) == hidden_spaces x + +-- On an invalid window, the stackset is unmodified +prop_focusWindow_identity (x::T ) = do + n <- arbitrary `suchThat` \n' -> not $ n' `member` x + return $ focusWindow n x == x diff --git a/tests/Properties/GreedyView.hs b/tests/Properties/GreedyView.hs new file mode 100644 index 0000000..3f2eb9b --- /dev/null +++ b/tests/Properties/GreedyView.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.GreedyView where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import Data.List (sortBy) + +-- --------------------------------------------------------------------- +-- greedyViewing workspaces + +-- greedyView sets the current workspace to 'n' +prop_greedyView_current (x :: T) = do + n <- arbitraryTag x + return $ currentTag (greedyView n x) == n + +-- greedyView leaves things unchanged for invalid workspaces +prop_greedyView_current_id (x :: T) = do + n <- arbitrary `suchThat` \n' -> not $ n' `tagMember` x + return $ currentTag (greedyView n x) == currentTag x + +-- greedyView *only* sets the current workspace, and touches Xinerama. +-- no workspace contents will be changed. +prop_greedyView_local (x :: T) = do + n <- arbitraryTag x + return $ workspaces x == workspaces (greedyView n x) + where + workspaces a = sortBy (\s t -> tag s `compare` tag t) $ + workspace (current a) + : map workspace (visible a) ++ hidden a + +-- greedyView is idempotent +prop_greedyView_idem (x :: T) = do + n <- arbitraryTag x + return $ greedyView n (greedyView n x) == (greedyView n x) + +-- greedyView is reversible, though shuffles the order of hidden/visible +prop_greedyView_reversible (x :: T) = do + n <- arbitraryTag x + return $ normal (greedyView n' (greedyView n x)) == normal x + where n' = currentTag x diff --git a/tests/Properties/Insert.hs b/tests/Properties/Insert.hs new file mode 100644 index 0000000..c277795 --- /dev/null +++ b/tests/Properties/Insert.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Insert where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import Data.List (nub) + +-- --------------------------------------------------------------------- +-- 'insert' + +-- inserting a item into an empty stackset means that item is now a member +prop_insert_empty i (EmptyStackSet x)= member i (insertUp i x) + +-- insert should be idempotent +prop_insert_idem i (x :: T) = insertUp i x == insertUp i (insertUp i x) + +-- insert when an item is a member should leave the stackset unchanged +prop_insert_duplicate (nex :: NonEmptyWindowsStackSet) = do + let NonEmptyWindowsStackSet x = nex + w <- arbitraryWindow nex + return $ insertUp w x == x + +-- push shouldn't change anything but the current workspace +prop_insert_local (x :: T) = do + i <- arbitrary `suchThat` \i' -> not $ i' `member` x + return $ hidden_spaces x == hidden_spaces (insertUp i x) + +-- Inserting a (unique) list of items into an empty stackset should +-- result in the last inserted element having focus. +prop_insert_peek (EmptyStackSet x) (NonEmptyNubList is) = + peek (foldr insertUp x is) == Just (head is) + +-- insert >> delete is the identity, when i `notElem` . +-- Except for the 'master', which is reset on insert and delete. +-- +prop_insert_delete x = do + n <- arbitrary `suchThat` \n -> not $ n `member` x + return $ delete n (insertUp n y) == (y :: T) + where + y = swapMaster x -- sets the master window to the current focus. + -- otherwise, we don't have a rule for where master goes. + +-- inserting n elements increases current stack size by n +prop_size_insert is (EmptyStackSet x) = + size (foldr insertUp x ws ) == (length ws) + where + ws = nub is + size = length . index diff --git a/tests/Properties/Layout/Full.hs b/tests/Properties/Layout/Full.hs new file mode 100644 index 0000000..eca6ec3 --- /dev/null +++ b/tests/Properties/Layout/Full.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Layout.Full where + +import Test.QuickCheck +import Instances + +import XMonad.StackSet hiding (filter) +import XMonad.Core +import XMonad.Layout + +import Data.Maybe + +------------------------------------------------------------------------ +-- Full layout + +-- pureLayout works for Full +prop_purelayout_full rect = do + x <- (arbitrary :: Gen T) `suchThat` (isJust . peek) + let layout = Full + st = fromJust . stack . workspace . current $ x + ts = pureLayout layout rect st + return $ + length ts == 1 -- only one window to view + && + snd (head ts) == rect -- and sets fullscreen + && + fst (head ts) == fromJust (peek x) -- and the focused window is shown + + +-- what happens when we send an IncMaster message to Full --- Nothing +prop_sendmsg_full (NonNegative k) = + isNothing (Full `pureMessage` (SomeMessage (IncMasterN k))) + +prop_desc_full = description Full == show Full diff --git a/tests/Properties/Layout/Tall.hs b/tests/Properties/Layout/Tall.hs new file mode 100644 index 0000000..7464184 --- /dev/null +++ b/tests/Properties/Layout/Tall.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Layout.Tall where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) +import XMonad.Core +import XMonad.Layout + +import Graphics.X11.Xlib.Types (Rectangle(..)) + +import Data.Maybe +import Data.List (sort) +import Data.Ratio + +------------------------------------------------------------------------ +-- The Tall layout + +-- 1 window should always be tiled fullscreen +prop_tile_fullscreen rect = tile pct rect 1 1 == [rect] + where pct = 1/2 + +-- multiple windows +prop_tile_non_overlap rect windows nmaster = noOverlaps (tile pct rect nmaster windows) + where _ = rect :: Rectangle + pct = 3 % 100 + +-- splitting horizontally yields sensible results +prop_split_hoziontal (NonNegative n) x = + sum (map rect_width xs) == rect_width x + && + all (== rect_height x) (map rect_height xs) + && + (map rect_x xs) == (sort $ map rect_x xs) + + where + xs = splitHorizontally n x + +-- splitting horizontally yields sensible results +prop_splitVertically (r :: Rational) x = + + rect_x x == rect_x a && rect_x x == rect_x b + && + rect_width x == rect_width a && rect_width x == rect_width b + where + (a,b) = splitVerticallyBy r x + + +-- pureLayout works. +prop_purelayout_tall n r1 r2 rect = do + x <- (arbitrary :: Gen T) `suchThat` (isJust . peek) + let layout = Tall n r1 r2 + st = fromJust . stack . workspace . current $ x + ts = pureLayout layout rect st + return $ + length ts == length (index x) + && + noOverlaps (map snd ts) + && + description layout == "Tall" + + +-- Test message handling of Tall + +-- what happens when we send a Shrink message to Tall +prop_shrink_tall (NonNegative n) (NonZero (NonNegative delta)) (NonNegative frac) = + n == n' && delta == delta' -- these state components are unchanged + && frac' <= frac && (if frac' < frac then frac' == 0 || frac' == frac - delta + else frac == 0 ) + -- remaining fraction should shrink + where + l1 = Tall n delta frac + Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage Shrink) + -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) + + +-- what happens when we send a Shrink message to Tall +prop_expand_tall (NonNegative n) + (NonZero (NonNegative delta)) + (NonNegative n1) + (NonZero (NonNegative d1)) = + + n == n' + && delta == delta' -- these state components are unchanged + && frac' >= frac + && (if frac' > frac + then frac' == 1 || frac' == frac + delta + else frac == 1 ) + + -- remaining fraction should shrink + where + frac = min 1 (n1 % d1) + l1 = Tall n delta frac + Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage Expand) + -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) + +-- what happens when we send an IncMaster message to Tall +prop_incmaster_tall (NonNegative n) (NonZero (NonNegative delta)) (NonNegative frac) + (NonNegative k) = + delta == delta' && frac == frac' && n' == n + k + where + l1 = Tall n delta frac + Just l2@(Tall n' delta' frac') = l1 `pureMessage` (SomeMessage (IncMasterN k)) + -- pureMessage :: layout a -> SomeMessage -> Maybe (layout a) + + + + -- toMessage LT = SomeMessage Shrink + -- toMessage EQ = SomeMessage Expand + -- toMessage GT = SomeMessage (IncMasterN 1) + + +prop_desc_mirror n r1 r2 = description (Mirror $! t) == "Mirror Tall" + where t = Tall n r1 r2 diff --git a/tests/Properties/Screen.hs b/tests/Properties/Screen.hs new file mode 100644 index 0000000..09a08af --- /dev/null +++ b/tests/Properties/Screen.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Screen where + +import Test.QuickCheck +import Instances + +import XMonad.StackSet hiding (filter) +import XMonad.Operations (applyResizeIncHint, applyMaxSizeHint ) +import Graphics.X11.Xlib.Types (Dimension) + +prop_screens (x :: T) = n `elem` screens x + where + n = current x + +-- screens makes sense +prop_screens_works (x :: T) = screens x == current x : visible x + + +------------------------------------------------------------------------ +-- Aspect ratios + +prop_resize_inc (NonZero (NonNegative inc_w),NonZero (NonNegative inc_h)) b@(w,h) = + w' `mod` inc_w == 0 && h' `mod` inc_h == 0 + where (w',h') = applyResizeIncHint a b + a = (inc_w,inc_h) + +prop_resize_inc_extra ((NonNegative inc_w)) b@(w,h) = + (w,h) == (w',h') + where (w',h') = applyResizeIncHint a b + a = (-inc_w,0::Dimension)-- inc_h) + +prop_resize_max (NonZero (NonNegative inc_w),NonZero (NonNegative inc_h)) b@(w,h) = + w' <= inc_w && h' <= inc_h + where (w',h') = applyMaxSizeHint a b + a = (inc_w,inc_h) + +prop_resize_max_extra ((NonNegative inc_w)) b@(w,h) = + (w,h) == (w',h') + where (w',h') = applyMaxSizeHint a b + a = (-inc_w,0::Dimension)-- inc_h) diff --git a/tests/Properties/Shift.hs b/tests/Properties/Shift.hs new file mode 100644 index 0000000..2150cbf --- /dev/null +++ b/tests/Properties/Shift.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Shift where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import qualified Data.List as L + +-- --------------------------------------------------------------------- +-- shift + +-- shift is fully reversible on current window, when focus and master +-- are the same. otherwise, master may move. +prop_shift_reversible (x :: T) = do + i <- arbitraryTag x + case peek y of + Nothing -> return True + Just _ -> return $ normal ((view n . shift n . view i . shift i) y) == normal y + where + y = swapMaster x + n = currentTag y + +------------------------------------------------------------------------ +-- shiftMaster + +-- focus/local/idempotent same as swapMaster: +prop_shift_master_focus (x :: T) = peek x == (peek $ shiftMaster x) +prop_shift_master_local (x :: T) = hidden_spaces x == hidden_spaces (shiftMaster x) +prop_shift_master_idempotent (x :: T) = shiftMaster (shiftMaster x) == shiftMaster x +-- ordering is constant modulo the focused window: +prop_shift_master_ordering (x :: T) = case peek x of + Nothing -> True + Just m -> L.delete m (index x) == L.delete m (index $ shiftMaster x) + +-- --------------------------------------------------------------------- +-- shiftWin + +-- shiftWin on current window is the same as shift +prop_shift_win_focus (x :: T) = do + n <- arbitraryTag x + case peek x of + Nothing -> return True + Just w -> return $ shiftWin n w x == shift n x + +-- shiftWin on a non-existant window is identity +prop_shift_win_indentity (x :: T) = do + n <- arbitraryTag x + w <- arbitrary `suchThat` \w' -> not (w' `member` x) + return $ shiftWin n w x == x + +-- shiftWin leaves the current screen as it is, if neither n is the tag +-- of the current workspace nor w on the current workspace +prop_shift_win_fix_current = do + x <- arbitrary `suchThat` \(x' :: T) -> + -- Invariant, otherWindows are NOT in the current workspace. + let otherWindows = allWindows x' L.\\ index x' + in length(tags x') >= 2 && length(otherWindows) >= 1 + -- Sadly we have to construct `otherWindows` again, for the actual StackSet + -- that got chosen. + let otherWindows = allWindows x L.\\ index x + -- We know such tag must exists, due to the precondition + n <- arbitraryTag x `suchThat` (/= currentTag x) + -- we know length is >= 1, from above precondition + idx <- choose(0, length(otherWindows) - 1) + let w = otherWindows !! idx + return $ (current $ x) == (current $ shiftWin n w x) + diff --git a/tests/Properties/Stack.hs b/tests/Properties/Stack.hs new file mode 100644 index 0000000..586df1d --- /dev/null +++ b/tests/Properties/Stack.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Stack where + +import Test.QuickCheck +import Instances + +import XMonad.StackSet hiding (filter) +import qualified XMonad.StackSet as S (filter) + +import Data.Maybe + + +-- The list returned by index should be the same length as the actual +-- windows kept in the zipper +prop_index_length (x :: T) = + case stack . workspace . current $ x of + Nothing -> length (index x) == 0 + Just it -> length (index x) == length (focus it : up it ++ down it) + + +-- For all windows in the stackSet, findTag should identify the +-- correct workspace +prop_findIndex (x :: T) = + and [ tag w == fromJust (findTag i x) + | w <- workspace (current x) : map workspace (visible x) ++ hidden x + , t <- maybeToList (stack w) + , i <- focus t : up t ++ down t + ] + +prop_allWindowsMember (NonEmptyWindowsStackSet x) = do + -- Reimplementation of arbitraryWindow, but to make sure that + -- implementation doesn't change in the future, and stop using allWindows, + -- which is a key component in this test (together with member). + let ws = allWindows x + -- We know that there are at least 1 window in a NonEmptyWindowsStackSet. + idx <- choose(0, (length ws) - 1) + return $ member (ws!!idx) x + + +-- preserve order +prop_filter_order (x :: T) = + case stack $ workspace $ current x of + Nothing -> True + Just s@(Stack i _ _) -> integrate' (S.filter (/= i) s) == filter (/= i) (integrate' (Just s)) + +-- differentiate should return Nothing if the list is empty or Just stack, with +-- the first element of the list is current, and the rest of the list is down. +prop_differentiate xs = + if null xs then differentiate xs == Nothing + else (differentiate xs) == Just (Stack (head xs) [] (tail xs)) + where _ = xs :: [Int] diff --git a/tests/Properties/StackSet.hs b/tests/Properties/StackSet.hs new file mode 100644 index 0000000..7fc5192 --- /dev/null +++ b/tests/Properties/StackSet.hs @@ -0,0 +1,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) = member i x == False + +-- 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 diff --git a/tests/Properties/Swap.hs b/tests/Properties/Swap.hs new file mode 100644 index 0000000..a516f2c --- /dev/null +++ b/tests/Properties/Swap.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Swap where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +-- --------------------------------------------------------------------- +-- swapUp, swapDown, swapMaster: reordiring windows + +-- swap is trivially reversible +prop_swap_left (x :: T) = (swapUp (swapDown x)) == x +prop_swap_right (x :: T) = (swapDown (swapUp x)) == x +-- TODO swap is reversible +-- swap is reversible, but involves moving focus back the window with +-- master on it. easy to do with a mouse... +{- +prop_promote_reversible x b = (not . null . fromMaybe [] . flip index x . current $ x) ==> + (raiseFocus y . promote . raiseFocus z . promote) x == x + where _ = x :: T + dir = if b then LT else GT + (Just y) = peek x + (Just (z:_)) = flip index x . current $ x +-} + +-- swap doesn't change focus +prop_swap_master_focus (x :: T) = peek x == (peek $ swapMaster x) +-- = case peek x of +-- Nothing -> True +-- Just f -> focus (stack (workspace $ current (swap x))) == f +prop_swap_left_focus (x :: T) = peek x == (peek $ swapUp x) +prop_swap_right_focus (x :: T) = peek x == (peek $ swapDown x) + +-- swap is local +prop_swap_master_local (x :: T) = hidden_spaces x == hidden_spaces (swapMaster x) +prop_swap_left_local (x :: T) = hidden_spaces x == hidden_spaces (swapUp x) +prop_swap_right_local (x :: T) = hidden_spaces x == hidden_spaces (swapDown x) + +-- rotation through the height of a stack gets us back to the start +prop_swap_all_l (x :: T) = (foldr (const swapUp) x [1..n]) == x + where n = length (index x) +prop_swap_all_r (x :: T) = (foldr (const swapDown) x [1..n]) == x + where n = length (index x) + +prop_swap_master_idempotent (x :: T) = swapMaster (swapMaster x) == swapMaster x diff --git a/tests/Properties/View.hs b/tests/Properties/View.hs new file mode 100644 index 0000000..ef9b58d --- /dev/null +++ b/tests/Properties/View.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.View where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import Data.List (sortBy) + +-- --------------------------------------------------------------------- +-- viewing workspaces + +-- view sets the current workspace to 'n' +prop_view_current (x :: T) = do + n <- arbitraryTag x + return $ (tag . workspace . current . view n) x == n + +-- view *only* sets the current workspace, and touches Xinerama. +-- no workspace contents will be changed. +prop_view_local (x :: T) = do + n <- arbitraryTag x + return $ workspaces x == workspaces (view n x) + where + workspaces a = sortBy (\s t -> tag s `compare` tag t) $ + workspace (current a) + : map workspace (visible a) ++ hidden a + +-- TODO: Fix this +-- view should result in a visible xinerama screen +-- prop_view_xinerama (x :: T) (n :: NonNegative Int) = i `tagMember` x ==> +-- M.member i (screens (view i x)) +-- where +-- i = fromIntegral n + +-- view is idempotent +prop_view_idem (x :: T) = do + n <- arbitraryTag x + return $ view n (view n x) == (view n x) + +-- view is reversible, though shuffles the order of hidden/visible +prop_view_reversible (x :: T) = do + n <- arbitraryTag x + return $ normal (view n' (view n x)) == normal x + where + n' = currentTag x diff --git a/tests/Properties/Workspace.hs b/tests/Properties/Workspace.hs new file mode 100644 index 0000000..612cba9 --- /dev/null +++ b/tests/Properties/Workspace.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE ScopedTypeVariables #-} +module Properties.Workspace where + +import Test.QuickCheck +import Instances +import Utils + +import XMonad.StackSet hiding (filter) + +import Data.Maybe + +-- looking up the tag of the current workspace should always produce a tag. +prop_lookup_current (x :: T) = lookupWorkspace scr x == Just tg + where + (Screen (Workspace tg _ _) scr _) = current x + +-- looking at a visible tag +prop_lookup_visible = do + -- make sure we have some xinerama screens. + x <- arbitrary `suchThat` \(x' :: T) -> visible x' /= [] + let tags = [ tag (workspace y) | y <- visible x ] + scr = last [ screen y | y <- visible x ] + return $ fromJust (lookupWorkspace scr x) `elem` tags + + +prop_currentTag (x :: T) = + currentTag x == tag (workspace (current x)) + +-- Rename a given tag if present in the StackSet. +prop_rename1 (x::T) = do + o <- arbitraryTag x + n <- arbitrary `suchThat` \n' -> not $ n' `tagMember` x + -- Rename o to n + let y = renameTag o n x + return $ n `tagMember` y + +-- Ensure that a given set of workspace tags is present by renaming +-- existing workspaces and\/or creating new hidden workspaces as +-- necessary. +-- +prop_ensure (x :: T) l xs = let y = ensureTags l xs x + in and [ n `tagMember` y | n <- xs ] + +-- adding a tag should create a new hidden workspace +prop_ensure_append (x :: T) l = do + n <- arbitrary `suchThat` \n' -> not $ n' `tagMember` x + let ts = tags x + y = ensureTags l (n:ts) x + return $ hidden y /= hidden x -- doesn't append, renames + && and [ isNothing (stack z) && layout z == l | z <- hidden y, tag z == n ] + + + + +prop_mapWorkspaceId (x::T) = x == mapWorkspace id x + +prop_mapWorkspaceInverse (x::T) = x == mapWorkspace predTag (mapWorkspace succTag x) + where predTag w = w { tag = pred $ tag w } + succTag w = w { tag = succ $ tag w } + +prop_mapLayoutId (x::T) = x == mapLayout id x + +prop_mapLayoutInverse (x::T) = x == mapLayout pred (mapLayout succ x) + + diff --git a/tests/Utils.hs b/tests/Utils.hs new file mode 100644 index 0000000..2d9df81 --- /dev/null +++ b/tests/Utils.hs @@ -0,0 +1,39 @@ +module Utils where + +import XMonad.StackSet hiding (filter) +import Graphics.X11.Xlib.Types (Rectangle(..)) +import Data.List (sortBy) + +-- Useful operation, the non-local workspaces +hidden_spaces x = map workspace (visible x) ++ hidden x + + +-- normalise workspace list +normal s = s { hidden = sortBy g (hidden s), visible = sortBy f (visible s) } + where + f = \a b -> tag (workspace a) `compare` tag (workspace b) + g = \a b -> tag a `compare` tag b + + +noOverlaps [] = True +noOverlaps [_] = True +noOverlaps xs = and [ verts a `notOverlap` verts b + | a <- xs + , b <- filter (a /=) xs + ] + where + verts (Rectangle a b w h) = (a,b,a + fromIntegral w - 1, b + fromIntegral h - 1) + + notOverlap (left1,bottom1,right1,top1) + (left2,bottom2,right2,top2) + = (top1 < bottom2 || top2 < bottom1) + || (right1 < left2 || right2 < left1) + + +applyN :: (Integral n) => Maybe n -> (a -> a) -> a -> a +applyN Nothing f v = v +applyN (Just 0) f v = v +applyN (Just n) f v = applyN (Just $ n-1) f (f v) + + +tags x = map tag $ workspaces x diff --git a/xmonad.cabal b/xmonad.cabal index 5b7dc7a..0265a91 100644 --- a/xmonad.cabal +++ b/xmonad.cabal @@ -17,7 +17,9 @@ license: BSD3 license-file: LICENSE author: Spencer Janssen maintainer: xmonad@haskell.org -extra-source-files: README TODO CONFIG STYLE tests/loc.hs tests/Properties.hs +extra-source-files: README TODO CONFIG STYLE tests/loc.hs + tests/Properties.hs tests/Properties/*.hs + tests/Properties/Layout*.hs man/xmonad.1.markdown man/xmonad.1 man/xmonad.1.html util/GenerateManpage.hs cabal-version: >= 1.8 @@ -88,10 +90,13 @@ executable xmonad ghc-prof-options: -prof -auto-all extensions: CPP - if flag(testing) - cpp-options: -DTESTING - hs-source-dirs: . tests/ - build-depends: QuickCheck < 2 - ghc-options: -Werror - if flag(testing) && flag(small_base) - build-depends: filepath, process, directory, mtl, unix, X11, base, containers, random, extensible-exceptions +test-suite properties + type: exitcode-stdio-1.0 + hs-source-dirs: tests + build-depends: base, + QuickCheck >= 2, + X11, + containers, + extensible-exceptions, + xmonad + main-is: Properties.hs |