update testsuite (mostly due Jesper Reenberg)

Ignore-this: a5e926aa4e397e70d56e3c9db7108d5b

* use quickcheck2
* run them using cabal's test-suite field
* split up Properties into separate files

darcs-hash:20140502180146-1499c-dc8c09c3ec76a42a0e146925adce960435dc81db.gz

20 files changed, 1232 insertions, 1200 deletions

diff --git a/Main.hs b/Main.hs
index 5fe83f9..2fcfe13 100644
--- a/Main.hs
+++ b/Main.hs
@@ -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