diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/Properties.hs | 813 |
1 files changed, 537 insertions, 276 deletions
diff --git a/tests/Properties.hs b/tests/Properties.hs index 01adc7d..170bc36 100644 --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -13,9 +13,10 @@ import Control.Exception (assert) import Control.Monad import Test.QuickCheck hiding (promote) import System.IO -import System.Random +import System.Random hiding (next) import Text.Printf -import Data.List (nub,sort,group,sort,intersperse,genericLength) +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 @@ -23,12 +24,42 @@ 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 (StackSet i a s) 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 + 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, fromIntegral sc,fs,ls) + coarbitrary = error "no coarbitrary for StackSet" + -- | 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. -fromList :: (Integral i, Integral j, Ord a) => (i, Int, [Maybe a], [[a]]) -> StackSet i j a +-- +-- '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, s, [Maybe Int], [[a]]) -> StackSet i a s fromList (_,_,_,[]) = error "Cannot build a StackSet from an empty list" fromList (n,m,fs,xs) | n < 0 || n >= genericLength xs @@ -36,235 +67,392 @@ fromList (n,m,fs,xs) | n < 0 || n >= genericLength xs | m < 1 || m > genericLength xs = error $ "Can't have more screens than workspaces: " ++ show (m, length xs) --- 'o' random workspace --- 'fs' random focused window on each workspace --- fromList (o,m,fs,xs) = let s = view o $ foldr (\(i,ys) s -> - foldr (\a t -> insert a i t) s ys) - (empty (length xs) m) (zip [0..] xs) - - in foldr (\f s -> case f of - Nothing -> s - Just w -> raiseFocus w s) s fs - --- --------------------------------------------------------------------- + foldr insertLeft (view i s) ys) + (new (genericLength xs) m) (zip [0..] xs) + in foldr (\f t -> case f of + Nothing -> t + Just i -> foldr (const focusLeft) t [0..i] ) s fs --- | /O(n)/. Number of stacks -size :: T -> Int -size = M.size . stacks - --- | Height of stack 'n' -height :: Int -> T -> Int -height i w = maybe 0 length (index i w) +------------------------------------------------------------------------ --- build (non-empty) StackSets with between 1 and 100 stacks -- --- StackSet --- { current :: i --- , screen2ws:: !(M.Map j i) -- ^ screen -> workspace --- , ws2screen:: !(M.Map i j) -- ^ workspace -> screen map --- , stacks :: !(M.Map i ([a], [a])) -- ^ screen -> (floating, normal) --- , cache :: !(M.Map a i) -- ^ a cache of windows back to their stacks --- } +-- Just generate StackSets with Char elements. -- --- Use 'raiseFocus' to bring focus to the front' --- -instance (Integral i, Integral j, Ord a, Arbitrary a) => Arbitrary (StackSet i j a) where - arbitrary = do - sz <- choose (1,20) - n <- choose (0,sz-1) - sc <- choose (1,sz) - ls <- vector sz +type T = StackSet Int Char Int - -- pick a random element of each stack to focus. - fs <- sequence [ if null s then return Nothing - else liftM Just (elements s) - | s <- ls ] - - return $ fromList (fromIntegral n,sc,fs,ls) - coarbitrary = error "no coarbitrary for StackSet" +-- Useful operation, the non-local workspaces +hidden x = [ w | w <- prev x ++ next x ] -- the hidden workspaces --- Invariants: +-- Basic data invariants of the StackSet -- --- * no element should ever appear more than once in a StackSet --- * the current index should always be valid +-- With the new zipper-based StackSet, tracking focus is no longer an +-- issue: the data structure enforces focus by construction. -- --- All operations must preserve this. +-- 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. -- -invariant (w :: T) = inBounds w && noDuplicates allWindows - where - allWindows = concatMap (uncurry (++)) . M.elems . stacks $ w - noDuplicates ws = nub ws == ws - inBounds x = current x >= 0 && current x < sz where sz = M.size (stacks x) +-- * 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 --- test generator -prop_invariant = invariant + -- all this xinerama stuff says we don't have the right structure + , currentIsVisible + , validScreens + , validWorkspaces + , inBounds + ] + where + ws = [ focus t : left t ++ right t + | w <- current s : prev s ++ next s, let t = stack w, t /= Empty ] + noDuplicates = nub ws == ws --- empty StackSets have no windows in them -prop_empty n m = n > 0 && m > 0 ==> all (null . uncurry (++)) (M.elems (stacks x)) - where x = empty n m :: T + -- xinerama invariants: --- empty StackSets always have focus on workspace 0 -prop_empty_current n m = n > 0 && m > 0 ==> current x == 0 - where x = empty n m :: T + currentIsVisible = M.member (tag (current s)) (screens s) -prop_member1 i n m = n > 0 && m > 0 ==> member i (push i x) - where x = empty n m :: T + validScreens = monotonic . sort . M.elems . screens $ s -prop_member2 i x = not (member i (delete i x)) - where _ = x :: T + validWorkspaces = and [ w `elem` allworkspaces | w <- (M.keys . screens) s ] + where allworkspaces = map tag $ current s : prev s ++ next s -prop_member3 i n m = member i (empty n m :: T) == False + inBounds = and [ w >=0 && w < size s | (w,sc) <- M.assocs (screens s) ] -prop_sizepush is n m = n > 0 ==> size (foldr push x is ) == n - where x = empty n m :: T +monotonic [] = True +monotonic (x:[]) = True +monotonic (x:y:zs) | x == y-1 = monotonic (y:zs) + | otherwise = False -prop_currentpush is n m = n > 0 ==> - height (current x) (foldr push x js) == length js - where - js = nub is - x = empty n m :: T +prop_invariant = invariant -prop_push_idem i (x :: T) = push i x == push i (push i x) +-- and check other ops preserve invariants +prop_empty_I (n :: Positive Int) = forAll (choose (1,fromIntegral n)) $ \m -> + invariant $ new (fromIntegral n) m -prop_pushpeek x is = not (null is) ==> fromJust (peek (foldr push x is)) == head is - where _ = x :: T +prop_view_I (n :: NonNegative Int) (x :: T) = + fromIntegral n < size x ==> invariant $ view (fromIntegral n) x -prop_peekmember x = case peek x of - Just w -> member w x - Nothing -> True {- then we don't know anything -} - where _ = x :: T +prop_focusLeft_I (n :: NonNegative Int) (x :: T) = + invariant $ foldr (const focusLeft) x [1..n] +prop_focusRight_I (n :: NonNegative Int) (x :: T) = + invariant $ foldr (const focusRight) x [1..n] -prop_peek_peekStack n x = - if current x == n then peekStack n x == peek x - else True -- so we don't exhaust - where _ = x :: T +prop_focus_I (n :: NonNegative Int) (x :: T) = + case peek x of + Nothing -> True + Just _ -> let w = focus . stack . current $ foldr (const focusLeft) x [1..n] + in invariant $ focusWindow w x -prop_notpeek_peekStack n x = current x /= n && isJust (peek x) ==> peekStack n x /= peek x - where _ = x :: T +prop_insertLeft_I n (x :: T) = invariant $ insertLeft n x ------------------------------------------------------------------------- +prop_delete_I (x :: T) = invariant $ + case peek x of + Nothing -> x + Just i -> delete i x -type T = StackSet Int Int Char +prop_swap_I (x :: T) = invariant $ swap x -prop_delete_uniq i x = not (member i x) ==> delete i x == x - where _ = x :: T +prop_shift_I (n :: NonNegative Int) (x :: T) = + fromIntegral n < size x ==> invariant $ shift (fromIntegral n) x -{- -TODO: enable this property when we have a better story about focus. -prop_delete_push i x = not (member i x) ==> delete i (push i x) == x - where _ = x :: T --} +-- --------------------------------------------------------------------- +-- 'new' -prop_delete_push i x = not (member i x) ==> delete i (push i x) == x - where _ = x :: T +-- empty StackSets have no windows in them +prop_empty (n :: Positive Int) + (m :: Positive Int) = + all (== Empty) [ stack w | w <- current x : prev x ++ next x ] -prop_delete2 i x = - delete i x == delete i (delete i x) - where _ = x :: T + where x = new (fromIntegral n) (fromIntegral m) :: T -prop_focus1 i x = member i x ==> peek (raiseFocus i x) == Just i - where _ = x :: T +-- empty StackSets always have focus on workspace 0 +prop_empty_current (n :: Positive Int) + (m :: Positive Int) = tag (current x) == 0 + where x = new (fromIntegral n) (fromIntegral m) :: T --- rotation is reversible in two directions -prop_rotaterotate1 (x :: T) = rotate LT (rotate GT x') == x' - where x' = rotate LT x -prop_rotaterotate2 (x :: T) = rotate GT (rotate LT x') == x' - where x' = rotate GT x +-- no windows will be a member of an empty workspace +prop_member_empty i (n :: Positive Int) (m :: Positive Int) + = member i (new (fromIntegral n) (fromIntegral m) :: T) == False --- rotation through the height of a stack gets us back to the start -prop_rotate_all (x :: T) = f (f x) == f x - where - n = height (current x) x - f x' = foldr (\_ y -> rotate GT y) x' [1..n] +-- --------------------------------------------------------------------- +-- viewing workspaces +-- view sets the current workspace to 'n' +prop_view_current (x :: T) (n :: NonNegative Int) = i < size x ==> + tag (current (view i x)) == i + where + i = fromIntegral n -prop_viewview r x = - let n = current x - sz = size x - i = r `mod` sz - in view n (view (fromIntegral i) x) == x +-- view *only* sets the current workspace, and touches Xinerama. +-- no workspace contents will be changed. +prop_view_local (x :: T) (n :: NonNegative Int) = i < size x ==> + workspaces x == workspaces (view i x) + where + workspaces a = sortBy (\s t -> tag s `compare` tag t) $ + current a : prev a ++ next a + i = fromIntegral n - where _ = x :: T +-- view should result in a visible xinerama screen +prop_view_xinerama (x :: T) (n :: NonNegative Int) = i < size x ==> + M.member i (screens (view i x)) + where + i = fromIntegral n +-- view is idempotent prop_view_idem (x :: T) r = let i = fromIntegral $ r `mod` sz sz = size x in view i (view i x) == (view i x) -{- -TODO: enable this property when we have a better story for focus. +-- view is reversible +prop_view_reversible r (x :: T) = view n (view i x) == x + where n = tag (current x) + sz = size x + i = fromIntegral $ r `mod` sz -prop_shift_reversible r (x :: T) = - let i = fromIntegral $ r `mod` sz - sz = size x - n = current x - in height n x > 0 ==> (view n . shift n . view i . shift i) x == x --} +-- --------------------------------------------------------------------- +-- 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 -prop_fullcache x = cached == allvals where - cached = sort . keys $ cache x - allvals = sort . concat . map (uncurry (++)) . elems $ stacks x - _ = x :: T +-- --------------------------------------------------------------------- +-- peek/index -prop_currentwsvisible x = (current x) `elem` (visibleWorkspaces x) - where _ = x :: T +-- 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 -prop_ws2screen_screen2ws x = (ws == ws') && (sc == sc') - where ws = sort . keys $ ws2screen x - ws' = sort . elems $ screen2ws x - sc = sort . keys $ screen2ws x - sc' = sort . elems $ ws2screen x - _ = x :: T +-- --------------------------------------------------------------------- +-- 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 it of + Empty -> length (index x) == 0 + Node {} -> length (index x) == length list + where + it = stack . current $ x + list = focus it : left it ++ right it -prop_screenworkspace x = all test [0..((fromIntegral $ size x)-1)] - where test ws = case screen ws x of - Nothing -> True - Just sc -> workspace sc x == Just ws - _ = x :: T +-- --------------------------------------------------------------------- +-- rotating focus +-- +-- Unfortunately, in the presence of wrapping of focus, we don't have a +-- simple identity where focusLeft . focusRight == id, as the focus +-- operations repartition the structure on wrapping. +-- +-- Note the issue with equality on Stacks given the wrapping semantics. +-- +-- [1,2,3] ++ [4] ++ [5] +-- +-- should be equivalent to: +-- +-- [] ++ [4] ++ [5,1,2,3] +-- +-- However, we can simply normalise the list, taking focus as the head, +-- and the items should be the same. + +-- So we normalise the stack on the current workspace. +-- We normalise by moving everything to the 'left' of the focused item, +-- to the right. +-- normal (x :: T) = modify Empty (\c -> case c of +-- Node t ls rs -> Node t [] (rs ++ reverse ls)) x +normal = id + +-- 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 focusLeft) x [1..n]) == index x +prop_focus_right_master (n :: NonNegative Int) (x::T) = + index (foldr (const focusRight) 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) = normal (focusLeft (focusRight x)) == normal x +prop_focus_right (x :: T) = normal (focusRight (focusLeft x)) == normal 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 . stack . current) (focusWindow (s !! i) x) == (s !! i) -prop_swap a b xs = swap a b (swap a b ys) == ys - where ys = nub xs :: [Int] +-- rotation through the height of a stack gets us back to the start +prop_focus_all_l (x :: T) = normal (foldr (const focusLeft) x [1..n]) == normal x + where n = length (index x) +prop_focus_all_r (x :: T) = normal (foldr (const focusRight) x [1..n]) == normal 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] --- promote is idempotent -prop_promote2 x = promote (promote x) == (promote x) - where _ = x :: T +-- focus is local to the current workspace +prop_focus_local (x :: T) = hidden (focusRight x) == hidden x --- focus doesn't change -prop_promotefocus x = focus (promote x) == focus x - where _ = x :: T +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 (focusWindow (s !! i) x) == hidden x --- screen certainly should't change -prop_promotecurrent x = current (promote x) == current x - where _ = x :: T +-- --------------------------------------------------------------------- +-- member/findIndex --- the physical screen doesn't change -prop_promotescreen n x = screen n (promote x) == screen n x - where _ = x :: T +-- +-- For all windows in the stackSet, findIndex should identify the +-- correct workspace +-- +prop_findIndex (x :: T) = + and [ tag w == fromJust (findIndex i x) + | w <- current x : prev x ++ next x + , let t = stack w + , t /= Empty + , i <- focus (stack w) : left (stack w) ++ right (stack w) + ] --- promote doesn't mess with other windows -prop_promote_raise_id x = (not . null . fromMaybe [] . flip index x . current $ x) ==> - (promote . promote . promote) x == promote x - where _ = x :: T +-- --------------------------------------------------------------------- +-- 'insert' + +-- inserting a item into an empty stackset means that item is now a member +prop_insert_empty i (n :: Positive Int) (m :: Positive Int) = member i (insertLeft i x) + where x = new (fromIntegral n) (fromIntegral m) :: T + +-- insert should be idempotent +prop_insert_idem i (x :: T) = insertLeft i x == insertLeft i (insertLeft i x) + +-- insert when an item is a member should leave the stackset unchanged +prop_insert_duplicate i (x :: T) = member i x ==> insertLeft i x == x -- push shouldn't change anything but the current workspace -prop_push_local (x :: T) i = not (member i x) ==> hidden x == hidden (push i x) +prop_insert_local (x :: T) i = not (member i x) ==> hidden x == hidden (insertLeft i x) + +-- Inserting a (unique) list of items into an empty stackset should +-- result in the last inserted element having focus. +prop_insert_peek (n :: Positive Int) (m :: Positive Int) (NonEmptyNubList is) = + peek (foldr insertLeft x is) == Just (head is) + where + x = new (fromIntegral n) (fromIntegral m) :: T + +-- 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 (insertLeft n y) == (y :: T) + where + y = swap 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 (n :: Positive Int) (m :: Positive Int) = + size (foldr insertLeft x ws ) == (length ws) where - hidden w = [ index n w | n <- [0 ..sz-1], n /= current w ] - sz = M.size (stacks x) + ws = nub is + x = new (fromIntegral n) (fromIntegral m) :: T + 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 -> insertLeft n (delete n y) == y + where + y = swap x + +-- delete should be local +prop_delete_local (x :: T) = + case peek x of + Nothing -> True + Just i -> hidden x == hidden (delete i x) + +-- --------------------------------------------------------------------- +-- swap: setting the master window +-- prop_swap_reversible a b xs = swap a b (swap a b ys) == ys +-- where ys = nub xs :: [Int] + +-- swap doesn't change focus +prop_swap_focus (x :: T) + = case peek x of + Nothing -> True + Just f -> focus (stack (current (swap x))) == f + +-- swap is local +prop_swap_local (x :: T) = hidden x == hidden (swap 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 +-} + +prop_swap_idempotent (x :: T) = swap (swap x) == swap x + +-- --------------------------------------------------------------------- +-- shift + +-- shift is fully reversible on current window, when focus and master +-- are the same. otherwise, master may move. +prop_shift_reversible (r :: Int) (x :: T) = + let i = fromIntegral $ r `mod` sz + sz = size y + n = tag (current y) + in case peek y of + Nothing -> True + Just _ -> (view n . shift n . view i . shift i) y == y + where + y = swap x ------------------------------------------------------------------------ -- some properties for layouts: -- 1 window should always be tiled fullscreen +{- prop_tile_fullscreen rect = tile pct rect 1 1 == [rect] -- multiple windows @@ -287,61 +475,7 @@ noOverlaps xs = and [ verts a `notOverlap` verts b = (top1 < bottom2 || top2 < bottom1) || (right1 < left2 || right2 < left1) - ------------------------------------------------------------------------- - -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 +-} ------------------------------------------------------------------------ @@ -349,81 +483,100 @@ main :: IO () main = do args <- getArgs let n = if null args then 100 else read (head args) - results <- mapM (\(s,a) -> printf "%-25s: " s >> a n) tests + (results, passed) <- liftM unzip $ mapM (\(s,a) -> printf "%-25s: " s >> a n) tests + printf "Passed %d tests!\n" (sum passed) when (not . and $ results) $ fail "Not all tests passed!" where - n = 100 tests = - [("StackSet invariants", mytest prop_invariant) - ,("empty is empty" , mytest prop_empty) - ,("empty / current" , mytest prop_empty_current) - - ,("member/push ", mytest prop_member1) - ,("member/peek ", mytest prop_peekmember) - ,("member/delete ", mytest prop_member2) - ,("member/empty ", mytest prop_member3) - - ,("size/push ", mytest prop_sizepush) - ,("height/push ", mytest prop_currentpush) - ,("push/peek ", mytest prop_pushpeek) - ,("push is local" , mytest prop_push_local) - ,("idempotent push" , mytest prop_push_idem) - - ,("peek/peekStack" , mytest prop_peek_peekStack) - ,("not . peek/peekStack", mytest prop_notpeek_peekStack) - - ,("delete/not.member", mytest prop_delete_uniq) - ,("delete idempotent", mytest prop_delete2) - ,("delete.push identity" , mytest prop_delete_push) - - ,("focus", mytest prop_focus1) - - ,("rotate l >> rotate r", mytest prop_rotaterotate1) - ,("rotate r >> rotate l", mytest prop_rotaterotate2) - ,("rotate all", mytest prop_rotate_all) - - ,("view/view ", mytest prop_viewview) - ,("view idem ", mytest prop_view_idem) - - -- disabled, for now ,("shift reversible ", mytest prop_shift_reversible) - - ,("fullcache ", mytest prop_fullcache) - ,("currentwsvisible ", mytest prop_currentwsvisible) - ,("ws screen mapping", mytest prop_ws2screen_screen2ws) - ,("screen/workspace ", mytest prop_screenworkspace) - - ,("promote idempotent", mytest prop_promote2) - ,("promote focus", mytest prop_promotefocus) - ,("promote current", mytest prop_promotecurrent) - ,("promote only swaps", mytest prop_promote_raise_id) - ,("promote/screen" , mytest prop_promotescreen) - - ,("swap", mytest prop_swap) - ------------------------------------------------------------------------- + [("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 reviersible" , mytest prop_view_reversible) + ,("view / xinerama" , mytest prop_view_xinerama) + ,("view is local" , mytest prop_view_local) + + ,("valid workspace xinerama", mytest prop_lookupWorkspace) + + ,("peek/member " , mytest prop_member_peek) + + ,("index/length" , mytest prop_index_length) + + ,("focus left : invariant", mytest prop_focusLeft_I) + ,("focus right: invariant", mytest prop_focusRight_I) + ,("focusWindow: invariant", mytest prop_focus_I) + ,("focus left/master" , mytest prop_focus_left_master) + ,("focus right/master" , mytest prop_focus_right_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 is local" , mytest prop_focus_local) + ,("focusWindow is local", mytest prop_focusWindow_local) + ,("focusWindow works" , mytest prop_focusWindow_works) + + ,("findIndex" , mytest prop_findIndex) + + ,("insert: invariant" , mytest prop_insertLeft_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) + + ,("swap: invariant " , mytest prop_swap_I) + ,("swap id on focus" , mytest prop_swap_focus) + ,("swap is idempotent" , mytest prop_swap_idempotent) + ,("swap is local" , mytest prop_swap_local) + + ,("shift: invariant" , mytest prop_shift_I) + ,("shift is reversible" , mytest prop_shift_reversible) +{- ,("tile 1 window fullsize", mytest prop_tile_fullscreen) ,("tiles never overlap", mytest prop_tile_non_overlap) +-} ] +------------------------------------------------------------------------ +-- +-- QC driver +-- + debug = False -mytest :: Testable a => a -> Int -> IO Bool +mytest :: Testable a => a -> Int -> IO (Bool, Int) mytest a n = mycheck defaultConfig { configMaxTest=n - , configEvery= \n args -> if debug then show n ++ ":\n" ++ unlines args else [] } a + , 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 +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 +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 - | nfail == configMaxFail config = done "Arguments exhausted after" ntest stamps >> return True + | 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 @@ -436,7 +589,7 @@ mytests config gen rnd0 ntest nfail stamps ++ show ntest ++ " tests:\n" ++ unlines (arguments result) - ) >> hFlush stdout >> return False + ) >> hFlush stdout >> return (False, ntest) where result = generate (configSize config ntest) rnd2 gen (rnd1,rnd2) = split rnd0 @@ -466,3 +619,111 @@ done mesg ntest stamps = putStr ( mesg ++ " " ++ show ntest ++ " tests" ++ table 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 + +-- | 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) |