diff options
| -rw-r--r-- | Config.hs | 29 | ||||
| -rw-r--r-- | Operations.hs | 12 | ||||
| -rw-r--r-- | StackSet.hs | 91 | ||||
| -rw-r--r-- | tests/Properties.hs | 92 |
4 files changed, 117 insertions, 107 deletions
@@ -148,35 +148,40 @@ defaultLayouts = [ full -- keys :: M.Map (KeyMask, KeySym) (X ()) keys = M.fromList $ + -- launching and killing programs [ ((modMask .|. shiftMask, xK_Return), spawn "xterm") , ((modMask, xK_p ), spawn "exe=`dmenu_path | dmenu` && exec $exe") , ((modMask .|. shiftMask, xK_p ), spawn "gmrun") + , ((modMask .|. shiftMask, xK_c ), kill) + + -- rotate through the available layout algorithms , ((modMask, xK_space ), switchLayout) -- 'nudge': resize viewed windows to the correct size. , ((modMask, xK_n ), refresh) - , ((modMask, xK_Tab ), focusRight) - , ((modMask, xK_j ), focusRight) - , ((modMask, xK_k ), focusLeft) + -- move focus up or down the window stack + , ((modMask, xK_Tab ), focusDown) + , ((modMask, xK_j ), focusDown) + , ((modMask, xK_k ), focusUp) - , ((modMask, xK_Left ), swapLeft) - , ((modMask, xK_Right ), swapRight) + -- modifying the window order + , ((modMask, xK_Return), swapMaster) + , ((modMask .|. shiftMask, xK_j ), swapDown) + , ((modMask .|. shiftMask, xK_k ), swapUp) + -- resizing the master/slave ratio , ((modMask, xK_h ), sendMessage Shrink) , ((modMask, xK_l ), sendMessage Expand) - , ((modMask .|. shiftMask, xK_j ), sendMessage (IncMasterN 1)) - , ((modMask .|. shiftMask, xK_k ), sendMessage (IncMasterN (-1))) - - , ((modMask .|. shiftMask, xK_c ), kill) + -- increase or decrease number of windows in the master area + , ((modMask , xK_comma ), sendMessage (IncMasterN 1)) + , ((modMask , xK_period), sendMessage (IncMasterN (-1))) + -- quit, or restart , ((modMask .|. shiftMask, xK_q ), io $ exitWith ExitSuccess) , ((modMask .|. shiftMask .|. controlMask, xK_q ), restart Nothing True) - -- Cycle the current tiling order - , ((modMask, xK_Return), swapMaster) - ] ++ -- Keybindings to get to each workspace: [((m .|. modMask, k), f i) diff --git a/Operations.hs b/Operations.hs index 39a5a35..84994d6 100644 --- a/Operations.hs +++ b/Operations.hs @@ -43,7 +43,7 @@ manage w = do selectInput d w $ structureNotifyMask .|. enterWindowMask .|. propertyChangeMask mapWindow d w setWindowBorderWidth d w borderWidth - windows $ W.insertLeft w + windows $ W.insertUp w -- | unmanage. A window no longer exists, remove it from the window -- list, on whatever workspace it is. @@ -51,11 +51,11 @@ unmanage :: Window -> X () unmanage = windows . W.delete -- | focus. focus window to the left or right. -focusLeft, focusRight, swapLeft, swapRight :: X () -focusLeft = windows W.focusLeft -focusRight = windows W.focusRight -swapLeft = windows W.swapLeft -swapRight = windows W.swapRight +focusUp, focusDown, swapUp, swapDown :: X () +focusUp = windows W.focusUp +focusDown = windows W.focusDown +swapUp = windows W.swapUp +swapDown = windows W.swapDown -- | swapMaster. Move the currently focused window into the master frame swapMaster :: X () diff --git a/StackSet.hs b/StackSet.hs index f6af748..cae577c 100644 --- a/StackSet.hs +++ b/StackSet.hs @@ -76,9 +76,9 @@ -- module StackSet ( StackSet(..), Workspace(..), Screen(..), Stack(..), - new, view, lookupWorkspace, peek, index, focusLeft, focusRight, - focusWindow, member, findIndex, insertLeft, delete, shift, - swapMaster, swapLeft, swapRight, modify -- needed by users + new, view, lookupWorkspace, peek, index, focusUp, focusDown, + focusWindow, member, findIndex, insertUp, delete, shift, + swapMaster, swapUp, swapDown, modify -- needed by users ) where import Data.Maybe (listToMaybe) @@ -91,10 +91,10 @@ import qualified Data.List as L (delete,find,genericSplitAt) -- view, -- index, -- peek, -- was: peek/peekStack --- focusLeft, focusRight, -- was: rotate --- swapLeft, swapRight +-- focusUp, focusDown, -- was: rotate +-- swapUp, swapDown -- focus -- was: raiseFocus --- insertLeft, -- was: insert/push +-- insertUp, -- was: insert/push -- delete, -- swapMaster, -- was: promote/swap -- member, @@ -131,9 +131,15 @@ data Workspace i a = Workspace { tag :: !i, stack :: Stack a } -- -- A stack is a cursor onto a (possibly empty) window list. -- The data structure tracks focus by construction, and --- the master window is by convention the left most item. +-- the master window is by convention the top-most item. -- Focus operations will not reorder the list that results from --- flattening the cursor. +-- flattening the cursor. The structure can be envisaged as: +-- +-- +-- master: < '7' > +-- up | [ '2' ] +-- +--------- [ '3' ] +-- focus: < '4' > +-- dn +----------- [ '8' ] -- -- A 'Stack' can be viewed as a list with a hole punched in it to make -- the focused position. Under the zipper/calculus view of such @@ -142,8 +148,8 @@ data Workspace i a = Workspace { tag :: !i, stack :: Stack a } -- data Stack a = Empty | Node { focus :: !a -- focused thing in this set - , left :: [a] -- clowns to the left - , right :: [a] } -- jokers to the right + , up :: [a] -- clowns to the left + , down :: [a] } -- jokers to the right deriving (Show, Read, Eq) @@ -247,32 +253,32 @@ index = with [] $ \(Node t l r) -> reverse l ++ t : r -- -- /O(1), O(w) on the wrapping case/. -- --- focusLeft, focusRight. Move the window focus left or --- right, wrapping if we reach the end. The wrapping should model a --- 'cycle' on the current stack. The 'master' window, and window order, +-- focusUp, focusDown. Move the window focus up or down the stack, +-- wrapping if we reach the end. The wrapping should model a -- 'cycle' +-- on the current stack. The 'master' window, and window order, -- are unaffected by movement of focus. -- --- swapLeft, swapRight. Swap the focused window with its left or right --- neighbour in the stack ordering, wrapping if we reach the end. Again --- the wrapping model should 'cycle' on the current stack. +-- swapUp, swapDown, swap the neighbour in the stack ordering, wrapping +-- if we reach the end. Again the wrapping model should 'cycle' on +-- the current stack. -- -focusLeft, focusRight, swapLeft, swapRight :: StackSet i a s -> StackSet i a s -focusLeft = modify Empty $ \c -> case c of +focusUp, focusDown, swapUp, swapDown :: StackSet i a s -> StackSet i a s +focusUp = modify Empty $ \c -> case c of Node _ [] [] -> c Node t (l:ls) rs -> Node l ls (t:rs) Node t [] rs -> Node x (xs ++ [t]) [] where (x:xs) = reverse rs -focusRight = modify Empty $ \c -> case c of +focusDown = modify Empty $ \c -> case c of Node _ [] [] -> c Node t ls (r:rs) -> Node r (t:ls) rs Node t ls [] -> Node x [] (xs ++ [t]) where (x:xs) = reverse ls -swapLeft = modify Empty $ \c -> case c of +swapUp = modify Empty $ \c -> case c of Node _ [] [] -> c Node t (l:ls) rs -> Node t ls (l:rs) Node t [] rs -> Node t (reverse rs) [] -swapRight = modify Empty $ \c -> case c of +swapDown = modify Empty $ \c -> case c of Node _ [] [] -> c Node t ls (r:rs) -> Node t (r:ls) rs Node t ls [] -> Node t [] (reverse ls) @@ -285,7 +291,7 @@ focusWindow :: (Integral i, Eq s, Eq a) => a -> StackSet i a s -> StackSet i a s focusWindow w s | Just w == peek s = s | otherwise = maybe s id $ do n <- findIndex w s - return $ until ((Just w ==) . peek) focusLeft (view n s) + return $ until ((Just w ==) . peek) focusUp (view n s) -- -- Finding if a window is in the stackset is a little tedious. We could @@ -310,34 +316,34 @@ findIndex a s = listToMaybe -- -- /O(n)/. (Complexity due to duplicate check). Insert a new element into --- the stack, to the left of the currently focused element. +-- the stack, above the currently focused element. -- -- The new element is given focus, and is set as the master window. --- The previously focused element is moved to the right. The previously +-- The previously focused element is moved down. The previously -- 'master' element is forgotten. (Thus, 'insert' will cause a retiling). -- -- If the element is already in the stackset, the original stackset is -- returned unmodified. -- -- Semantics in Huet's paper is that insert doesn't move the cursor. --- However, we choose to insert to the left, and move the focus. +-- However, we choose to insert above, and move the focus. -- -insertLeft :: Eq a => a -> StackSet i a s -> StackSet i a s -insertLeft a s = if member a s then s else insert +insertUp :: Eq a => a -> StackSet i a s -> StackSet i a s +insertUp a s = if member a s then s else insert where insert = modify (Node a [] []) (\(Node t l r) -> Node a l (t:r)) s --- insertRight :: a -> StackSet i a s -> StackSet i a s --- insertRight a = modify (Node a [] []) $ \(Node t l r) -> Node a (t:l) r +-- insertDown :: a -> StackSet i a s -> StackSet i a s +-- insertDown a = modify (Node a [] []) $ \(Node t l r) -> Node a (t:l) r -- Old semantics, from Huet. --- > w { right = a : right w } +-- > w { down = a : down w } -- -- /O(1) on current window, O(n) in general/. Delete window 'w' if it exists. -- There are 4 cases to consider: -- -- * delete on an Empty workspace leaves it Empty --- * otherwise, try to move focus to the right --- * otherwise, try to move focus to the left +-- * otherwise, try to move focus to the down +-- * otherwise, try to move focus to the up -- * otherwise, you've got an empty workspace, becomes Empty -- -- Behaviour with respect to the master: @@ -353,13 +359,13 @@ delete w s | Just w == peek s = remove s -- common case. removeWindow o n = foldr ($) s [view o,remove,view n] -- actual removal logic, and focus/master logic: - remove = modify Empty $ \c -> - if focus c == w + remove = modify Empty $ \c -> + if focus c == w then case c of - Node _ ls (r:rs) -> Node r ls rs -- try right first - Node _ (l:ls) [] -> Node l ls [] -- else left. + Node _ ls (r:rs) -> Node r ls rs -- try down first + Node _ (l:ls) [] -> Node l ls [] -- else up Node _ [] [] -> Empty - else c { left = w `L.delete` left c, right = w `L.delete` right c } + else c { up = w `L.delete` up c, down = w `L.delete` down c } ------------------------------------------------------------------------ -- Setting the master window @@ -372,8 +378,7 @@ swapMaster = modify Empty $ \c -> case c of Node _ [] _ -> c -- already master. Node t ls rs -> Node t [] (ys ++ x : rs) where (x:ys) = reverse ls - -- natural! keep focus, move current to furthest left, move furthest --- left to current position. + -- natural! keep focus, move current to the top, move top to current. -- --------------------------------------------------------------------- -- Composite operations @@ -381,13 +386,13 @@ swapMaster = modify Empty $ \c -> case c of -- /O(w)/. shift. Move the focused element of the current stack to stack -- 'n', leaving it as the focused element on that stack. The item is --- inserted to the left of the currently focused element on that --- workspace. The actual focused workspace doesn't change. If there is --- no element on the current stack, the original stackSet is returned. +-- inserted above the currently focused element on that workspace. -- +-- The actual focused workspace doesn't change. If there is -- no +-- element on the current stack, the original stackSet is returned. -- shift :: (Eq a, Eq s, Integral i) => i -> StackSet i a s -> StackSet i a s shift n s = if and [n >= 0,n < size s,n /= tag (workspace (current s))] then maybe s go (peek s) else s - where go w = foldr ($) s [view (tag (workspace (current s))),insertLeft w,view n,delete w] + where go w = foldr ($) s [view (tag (workspace (current s))),insertUp w,view n,delete w] -- ^^ poor man's state monad :-) diff --git a/tests/Properties.hs b/tests/Properties.hs index 3013985..8a2d712 100644 --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -70,11 +70,11 @@ fromList (n,m,fs,xs) | n < 0 || n >= genericLength xs fromList (o,m,fs,xs) = let s = view o $ foldr (\(i,ys) s -> - foldr insertLeft (view i s) ys) + foldr insertUp (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 + Just i -> foldr (const focusUp) t [0..i] ) s fs ------------------------------------------------------------------------ @@ -112,7 +112,7 @@ invariant (s :: T) = and ] where - ws = concat [ focus t : left t ++ right t + ws = concat [ focus t : up t ++ down t | w <- workspace (current s) : map workspace (visible s) ++ hidden s , let t = stack w, t /= Empty ] :: [Char] noDuplicates = nub ws == ws @@ -140,18 +140,18 @@ prop_empty_I (n :: Positive Int) = forAll (choose (1,fromIntegral n)) $ \m -> prop_view_I (n :: NonNegative Int) (x :: T) = fromIntegral n < size x ==> invariant $ view (fromIntegral n) x -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_focusUp_I (n :: NonNegative Int) (x :: T) = + invariant $ foldr (const focusUp) 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 . stack . workspace . current $ foldr (const focusLeft) x [1..n] + Just _ -> let w = focus . stack . workspace . current $ foldr (const focusUp) x [1..n] in invariant $ focusWindow w x -prop_insertLeft_I n (x :: T) = invariant $ insertLeft n x +prop_insertUp_I n (x :: T) = invariant $ insertUp n x prop_delete_I (x :: T) = invariant $ case peek x of @@ -161,9 +161,9 @@ prop_delete_I (x :: T) = invariant $ prop_swap_master_I (x :: T) = invariant $ swapMaster x prop_swap_left_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const swapLeft ) x [1..n] + invariant $ foldr (const swapUp ) x [1..n] prop_swap_right_I (n :: NonNegative Int) (x :: T) = - invariant $ foldr (const swapRight) x [1..n] + invariant $ foldr (const swapDown) x [1..n] prop_shift_I (n :: NonNegative Int) (x :: T) = fromIntegral n < size x ==> invariant $ shift (fromIntegral n) x @@ -262,7 +262,7 @@ prop_index_length (x :: T) = Node {} -> length (index x) == length list where it = stack . workspace . current $ x - list = focus it : left it ++ right it + list = focus it : up it ++ down it -- --------------------------------------------------------------------- -- rotating focus @@ -273,9 +273,9 @@ prop_index_length (x :: T) = -- 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 + index (foldr (const focusUp) x [1..n]) == index x prop_focus_right_master (n :: NonNegative Int) (x::T) = - index (foldr (const focusRight) x [1..n]) == index x + index (foldr (const focusDown) x [1..n]) == index x prop_focusWindow_master (n :: NonNegative Int) (x :: T) = case peek x of Nothing -> True @@ -284,8 +284,8 @@ prop_focusWindow_master (n :: NonNegative Int) (x :: T) = in index (focusWindow (s !! i) x) == index x -- shifting focus is trivially reversible -prop_focus_left (x :: T) = (focusLeft (focusRight x)) == x -prop_focus_right (x :: T) = (focusRight (focusLeft x)) == x +prop_focus_left (x :: T) = (focusUp (focusDown x)) == x +prop_focus_right (x :: T) = (focusDown (focusUp x)) == x -- focusWindow actually leaves the window focused... prop_focusWindow_works (n :: NonNegative Int) (x :: T) = @@ -296,16 +296,16 @@ prop_focusWindow_works (n :: NonNegative Int) (x :: T) = in (focus . 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 focusLeft) x [1..n]) == x +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 focusRight) x [1..n]) == 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_local (x :: T) = hidden_spaces (focusRight x) == hidden_spaces x +prop_focus_local (x :: T) = hidden_spaces (focusDown x) == hidden_spaces x prop_focusWindow_local (n :: NonNegative Int) (x::T ) = case peek x of @@ -326,43 +326,43 @@ prop_findIndex (x :: T) = | w <- workspace (current x) : map workspace (visible x) ++ hidden x , let t = stack w , t /= Empty - , i <- focus (stack w) : left (stack w) ++ right (stack w) + , i <- focus (stack w) : up (stack w) ++ down (stack w) ] -- --------------------------------------------------------------------- -- '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) +prop_insert_empty i (n :: Positive Int) (m :: Positive Int) = member i (insertUp 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) +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 ==> insertLeft i x == x +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 (insertLeft i x) +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 (n :: Positive Int) (m :: Positive Int) (NonEmptyNubList is) = - peek (foldr insertLeft x is) == Just (head is) + peek (foldr insertUp 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) +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 (n :: Positive Int) (m :: Positive Int) = - size (foldr insertLeft x ws ) == (length ws) + size (foldr insertUp x ws ) == (length ws) where ws = nub is x = new (fromIntegral n) (fromIntegral m) :: T @@ -385,7 +385,7 @@ prop_delete x = prop_delete_insert (x :: T) = case peek x of Nothing -> True - Just n -> insertLeft n (delete n y) == y + Just n -> insertUp n (delete n y) == y where y = swapMaster x @@ -399,11 +399,11 @@ prop_delete_local (x :: T) = prop_delete_focus n (x :: T) = member n x && Just n /= peek x ==> peek (delete n x) == peek x -- --------------------------------------------------------------------- --- swapLeft, swapRight, swapMaster: reordiring windows +-- swapUp, swapDown, swapMaster: reordiring windows -- swap is trivially reversible -prop_swap_left (x :: T) = (swapLeft (swapRight x)) == x -prop_swap_right (x :: T) = (swapRight (swapLeft x)) == x +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... @@ -421,18 +421,18 @@ 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 $ swapLeft x) -prop_swap_right_focus (x :: T) = peek x == (peek $ swapRight x) +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 (swapLeft x) -prop_swap_right_local (x :: T) = hidden_spaces x == hidden_spaces (swapRight 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 swapLeft) x [1..n]) == x +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 swapRight) x [1..n]) == 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 @@ -513,8 +513,8 @@ main = do ,("index/length" , mytest prop_index_length) - ,("focus left : invariant", mytest prop_focusLeft_I) - ,("focus right: invariant", mytest prop_focusRight_I) + ,("focus left : invariant", mytest prop_focusUp_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) @@ -529,7 +529,7 @@ main = do ,("findIndex" , mytest prop_findIndex) - ,("insert: invariant" , mytest prop_insertLeft_I) + ,("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) @@ -546,17 +546,17 @@ main = do ,("delete/focus" , mytest prop_delete_focus) ,("swapMaster: invariant", mytest prop_swap_master_I) - ,("swapLeft: invariant" , mytest prop_swap_left_I) - ,("swapRight: invariant", mytest prop_swap_right_I) + ,("swapUp: invariant" , mytest prop_swap_left_I) + ,("swapDown: invariant", mytest prop_swap_right_I) ,("swapMaster id on focus", mytest prop_swap_master_focus) - ,("swapLeft id on focus", mytest prop_swap_left_focus) - ,("swapRight id on focus", mytest prop_swap_right_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) - ,("swapLeft is local" , mytest prop_swap_left_local) - ,("swapRight is local" , mytest prop_swap_right_local) + ,("swapUp is local" , mytest prop_swap_left_local) + ,("swapDown is local" , mytest prop_swap_right_local) ,("shift: invariant" , mytest prop_shift_I) ,("shift is reversible" , mytest prop_shift_reversible) |