src/Darcs/Patch/Unit.lhs

   1 %  Copyright (C) 2007 David Roundy
   2 %
   3 %  This program is free software; you can redistribute it and/or modify
   4 %  it under the terms of the GNU General Public License as published by
   5 %  the Free Software Foundation; either version 2, or (at your option)
   6 %  any later version.
   7 %
   8 %  This program is distributed in the hope that it will be useful,
   9 %  but WITHOUT ANY WARRANTY; without even the implied warranty of
  10 %  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  11 %  GNU General Public License for more details.
  12 %
  13 %  You should have received a copy of the GNU General Public License
  14 %  along with this program; see the file COPYING.  If not, write to
  15 %  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  16 %  Boston, MA 02110-1301, USA.
  17
  18 \begin{code}
  19 {-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts #-}
  20 {-# LANGUAGE CPP #-}
  21
  22 #include "gadts.h"
  23
  24 module Darcs.Patch.Unit ( run_patch_unit_tests ) where
  25
  26 import Control.Monad ( unless )
  27 import Data.Maybe ( catMaybes )
  28 import qualified Data.ByteString.Char8 as BC ( pack )
  29 import Darcs.Sealed
  30 import Darcs.Patch
  31 import Darcs.Patch.Patchy ( mergeFL, Invert )
  32 import Darcs.Patch.Real ( RealPatch, prim2real, is_consistent, is_forward, is_duplicate )
  33 import Darcs.Patch.Test () -- for instance Eq Patch
  34 import Darcs.Ordered
  35 import Darcs.Patch.Properties ( recommute, commute_inverses, permutivity, partial_permutivity,
  36                                 inverse_doesnt_commute, patch_and_inverse_commute,
  37                                 merge_commute, merge_consistent, merge_arguments_consistent,
  38                                 merge_either_way, show_read,
  39                                 join_inverses, join_commute )
  40 import Darcs.Patch.Prim ( join )
  41 import Darcs.Patch.QuickCheck
  42 import Printer ( Doc, redText, ($$) )
  43 --import Printer ( greenText )
  44 --import Darcs.ColorPrinter ( traceDoc )
  45 --import Darcs.ColorPrinter ( errorDoc )
  46 import Darcs.ColorPrinter () -- for instance Show Doc
  47
  48 -- import Debug.Trace
  49 -- #include "impossible.h"
  50 \end{code}
  51
  52 \begin{code}
  53 run_patch_unit_tests :: IO Int
  54 run_patch_unit_tests =
  55     run_some_tests ""
  56     [--do putStr "Checking with quickcheck that real patches have consistent flattenings... "
  57      --   quickCheck (not . isBottomTimeOut (Just 10) . prop_consistent_tree_flattenings) >> return 0
  58      run_primitive_tests "prim join inverses"
  59                          (\(a:\/:_) -> join_inverses join a) mergeables
  60     ,do putStr "Checking prim join inverses using QuickCheck... "
  61         simpleCheck (join_inverses join)
  62     ,run_primitive_tests "prim inverse doesn't commute"
  63                          (\(a:\/:_) -> inverse_doesnt_commute a) mergeables
  64     -- The following fails because of setpref patches...
  65     --,do putStr "Checking prim inverse doesn't commute using QuickCheck... "
  66     --    simpleCheck (inverse_doesnt_commute :: Prim -> Maybe Doc)
  67     ,run_primitive_tests "join commute" (join_commute join) prim_permutables
  68     ,do putStr "Checking prim join commute using QuickCheck... "
  69         simpleCheck (unseal2 (join_commute join))
  70
  71     ,run_primitive_tests "prim recommute"
  72                          (recommute commute) $ map mergeable2commutable mergeables
  73     ,run_primitive_tests "prim patch and inverse commute"
  74                          (patch_and_inverse_commute commute) $ map mergeable2commutable mergeables
  75     ,run_primitive_tests "prim inverses commute"
  76                          (commute_inverses commute) $ map mergeable2commutable mergeables
  77
  78 --    ,do putStr "Checking prim recommute using QuickCheck... "
  79 --        simpleCheck (recommute
  80 --                     (commute :: Prim :> Prim
  81 --                              -> Maybe (Prim :> Prim)))
  82
  83     ,run_primitive_tests "FL prim recommute"
  84                          (recommute commute) $ map mergeable2commutable mergeablesFL
  85     ,run_primitive_tests "FL prim patch and inverse commute"
  86                          (patch_and_inverse_commute commute) $ map mergeable2commutable mergeablesFL
  87     ,run_primitive_tests "FL prim inverses commute"
  88                          (commute_inverses commute) $ map mergeable2commutable mergeablesFL
  89
  90     ,run_primitive_tests "fails" (commute_fails commute) ([] :: [Prim :> Prim])
  91
  92     ,run_primitive_tests "read and show work on Prim" show_read prim_patches
  93     ,run_primitive_tests "read and show work on RealPatch" show_read real_patches
  94     ,do putStr "Checking that readPatch and showPatch work on RealPatch... "
  95         simpleCheck (unseal $ patchFromTree $ (show_read :: RealPatch -> Maybe Doc))
  96     ,do putStr "Checking that readPatch and showPatch work on FL RealPatch... "
  97         simpleCheck (unseal2 $ (show_read :: FL RealPatch -> Maybe Doc))
  98
  99     ,run_primitive_tests "example flattenings work"
 100                              (\x -> if prop_consistent_tree_flattenings x
 101                                     then Nothing
 102                                     else Just $ redText "oops")
 103                              real_patch_loop_examples
 104     ,do putStr "Checking that tree flattenings are consistent... "
 105         simpleCheck ((\b -> if b then Nothing else Just False) . prop_consistent_tree_flattenings)
 106
 107     ,do putStr "Checking with quickcheck that real patches are consistent... "
 108         simpleCheck (unseal $ patchFromTree $ is_consistent)
 109     ,run_primitive_tests "real merge input consistent"
 110                              (merge_arguments_consistent is_consistent) real_mergeables
 111     ,run_primitive_tests "real merge input is forward"
 112                              (merge_arguments_consistent is_forward) real_mergeables
 113     ,run_primitive_tests "real merge output is forward"
 114                              (merge_consistent is_forward) real_mergeables
 115     ,run_primitive_tests "real merge output consistent"
 116                              (merge_consistent is_consistent) real_mergeables
 117     ,run_primitive_tests "real merge either way" merge_either_way real_mergeables
 118     ,run_primitive_tests "real merge and commute" merge_commute real_mergeables
 119
 120     ,run_primitive_tests "real recommute" (recommute commute) real_commutables
 121     ,run_primitive_tests "real inverses commute" (commute_inverses commute) real_commutables
 122
 123     ,run_primitive_tests "real permutivity" (permutivity commute) $
 124                          filter (not_duplicatestriple) real_triples
 125     ,run_primitive_tests "real partial permutivity" (partial_permutivity commute) $
 126                          filter (not_duplicatestriple) real_triples
 127
 128     ,do putStr "Checking we can do merges using QuickCheck... "
 129         simpleCheck (prop_is_mergeable ::
 130                          Sealed (WithStartState RepoModel (Tree Prim))
 131                              -> Maybe (Tree RealPatch C(x)))
 132     ,do putStr "Checking again we can do merges using QuickCheck... "
 133         thoroughCheck 1000 (prop_is_mergeable ::
 134                                 Sealed (WithStartState RepoModel (Tree Prim))
 135                                     -> Maybe (Tree RealPatch C(x)))
 136
 137     ,do putStr "Checking recommute using QuickCheck Tree generator... "
 138         simpleCheck (unseal $ commutePairFromTree $
 139                     (recommute
 140                      (commute :: RealPatch :> RealPatch
 141                               -> Maybe (RealPatch :> RealPatch))))
 142     ,do putStr "Checking recommute using QuickCheck TWFP generator... "
 143         simpleCheck (unseal $ commutePairFromTWFP $
 144                     (recommute
 145                      (commute :: RealPatch :> RealPatch
 146                               -> Maybe (RealPatch :> RealPatch))))
 147     ,do putStr "Checking nontrivial recommute... "
 148         simpleConditionalCheck (unseal $ commutePairFromTree $ nontrivial_reals)
 149                                    (unseal $ commutePairFromTree $
 150                                     (recommute
 151                                      (commute :: RealPatch :> RealPatch
 152                                               -> Maybe (RealPatch :> RealPatch))))
 153     ,do putStr "Checking nontrivial recommute using TWFP... "
 154         simpleConditionalCheck (unseal $ commutePairFromTWFP $ nontrivial_reals)
 155                                    (unseal $ commutePairFromTWFP $
 156                                     (recommute
 157                                      (commute :: RealPatch :> RealPatch
 158                                               -> Maybe (RealPatch :> RealPatch))))
 159
 160     ,do putStr "Checking inverses commute using QuickCheck Tree generator... "
 161         simpleCheck (unseal $ commutePairFromTree $
 162                     (commute_inverses
 163                      (commute :: RealPatch :> RealPatch
 164                               -> Maybe (RealPatch :> RealPatch))))
 165     ,do putStr "Checking inverses commute using QuickCheck TWFP generator... "
 166         simpleCheck (unseal $ commutePairFromTWFP $
 167                     (commute_inverses
 168                      (commute :: RealPatch :> RealPatch
 169                               -> Maybe (RealPatch :> RealPatch))))
 170     ,do putStr "Checking nontrivial inverses commute... "
 171         simpleConditionalCheck (unseal $ commutePairFromTree $ nontrivial_reals)
 172                                    (unseal $ commutePairFromTree $
 173                                     (commute_inverses
 174                                      (commute :: RealPatch :> RealPatch
 175                                               -> Maybe (RealPatch :> RealPatch))))
 176     ,do putStr "Checking nontrivial inverses commute using TWFP... "
 177         simpleConditionalCheck (unseal $ commutePairFromTWFP $ nontrivial_reals)
 178                                    (unseal $ commutePairFromTWFP $
 179                                     (commute_inverses
 180                                      (commute :: RealPatch :> RealPatch
 181                                               -> Maybe (RealPatch :> RealPatch))))
 182
 183     ,do putStr "Checking merge either way using QuickCheck TWFP generator... "
 184         simpleCheck (unseal $ mergePairFromTWFP $
 185                      (merge_either_way :: RealPatch :\/: RealPatch -> Maybe Doc))
 186     ,do putStr "Checking merge either way using QuickCheck Tree generator... "
 187         simpleCheck (unseal $ mergePairFromTree $
 188                      (merge_either_way :: RealPatch :\/: RealPatch -> Maybe Doc))
 189     ,do putStr "Checking nontrivial merge either way... "
 190         simpleConditionalCheck (unseal $ mergePairFromTree $ nontrivial_merge_reals)
 191                                    (unseal $ mergePairFromTree $
 192                                     (merge_either_way :: RealPatch :\/: RealPatch -> Maybe Doc))
 193     ,do putStr "Checking nontrivial merge either way using TWFP... "
 194         simpleConditionalCheck (unseal $ mergePairFromTWFP $ nontrivial_merge_reals)
 195                                    (unseal $ mergePairFromTWFP $
 196                                     (merge_either_way :: RealPatch :\/: RealPatch -> Maybe Doc))
 197
 198     ,do putStr "Checking permutivity... "
 199         simpleConditionalCheck (unseal $ commuteTripleFromTree not_duplicatestriple)
 200             (unseal $ commuteTripleFromTree $ permutivity
 201                     (commute :: RealPatch :> RealPatch -> Maybe (RealPatch :> RealPatch)))
 202     ,do putStr "Checking partial permutivity... "
 203         simpleConditionalCheck (unseal $ commuteTripleFromTree not_duplicatestriple)
 204             (unseal $ commuteTripleFromTree $ partial_permutivity
 205                     (commute :: RealPatch :> RealPatch -> Maybe (RealPatch :> RealPatch)))
 206     ,do putStr "Checking nontrivial permutivity... "
 207         simpleConditionalCheck (unseal $ commuteTripleFromTree
 208                                            (\t -> nontrivial_triple t && not_duplicatestriple t))
 209                   (unseal $ commuteTripleFromTree $
 210                     (permutivity
 211                      (commute :: RealPatch :> RealPatch
 212                               -> Maybe (RealPatch :> RealPatch))))
 213     ]
 214
 215 not_duplicatestriple :: RealPatch :> RealPatch :> RealPatch -> Bool
 216 not_duplicatestriple (a :> b :> c) = not $ any is_duplicate [a,b,c]
 217
 218 --not_duplicates_pair :: RealPatch :> RealPatch -> Bool
 219 --not_duplicates_pair (a :> b) = not $ any is_duplicate [a,b]
 220
 221 nontrivial_triple :: RealPatch :> RealPatch :> RealPatch -> Bool
 222 nontrivial_triple (a :> b :> c) =
 223     case commute (a :> b) of
 224     Nothing -> False
 225     Just (b' :> a') ->
 226       case commute (a' :> c) of
 227       Nothing -> False
 228       Just (c'' :> a'') ->
 229         case commute (b :> c) of
 230         Nothing -> False
 231         Just (c' :> b'') -> (not (a `unsafeCompare` a') || not (b `unsafeCompare` b')) &&
 232                             (not (c' `unsafeCompare` c) || not (b'' `unsafeCompare` b)) &&
 233                             (not (c'' `unsafeCompare` c) || not (a'' `unsafeCompare` a'))
 234
 235 nontrivial_reals :: RealPatch :> RealPatch -> Bool
 236 nontrivial_reals = nontrivial_commute
 237
 238 nontrivial_commute :: Patchy p => p :> p -> Bool
 239 nontrivial_commute (x :> y) = case commute (x :> y) of
 240                               Just (y' :> x') -> not (y' `unsafeCompare` y) ||
 241                                                  not (x' `unsafeCompare` x)
 242                               Nothing -> False
 243
 244 nontrivial_merge_reals :: RealPatch :\/: RealPatch -> Bool
 245 nontrivial_merge_reals = nontrivial_merge
 246
 247 nontrivial_merge :: Patchy p => p :\/: p -> Bool
 248 nontrivial_merge (x :\/: y) = case merge (x :\/: y) of
 249                               y' :/\: x' -> not (y' `unsafeCompare` y) ||
 250                                             not (x' `unsafeCompare` x)
 251
 252 run_some_tests :: String -> [IO Int] -> IO Int
 253 run_some_tests name ts = do unless (null name) $ putStr $ "Testing " ++ name ++ "... "
 254                             errs <- sum `fmap` sequence ts
 255                             unless (null name) $
 256                                    if errs < 1
 257                                    then putStrLn "passed."
 258                                    else putStrLn $ "failed " ++ name ++" in "++ show errs ++ " tests."
 259                             return errs
 260
 261 run_primitive_tests :: (Show a, Show b) => String -> (a -> Maybe b) -> [a] -> IO Int
 262 run_primitive_tests name test datas = run_some_tests name $ map test' datas
 263     where test' d = case test d of
 264                     Just e -> do putStrLn $ name ++ " failed!"
 265                                  putStrLn $ "Input: " ++ show d
 266                                  putStrLn $ "Output: " ++ show e
 267                                  return 1
 268                     Nothing -> return 0
 269
 270 \end{code}
 271
 272 \begin{code}
 273 quickhunk :: Int -> String -> String -> Prim
 274 quickhunk l o n = hunk "test" l (map (\c -> BC.pack [c]) o)
 275                                 (map (\c -> BC.pack [c]) n)
 276 \end{code}
 277
 278 \begin{code}
 279 prim_permutables :: [Prim :> Prim :> Prim]
 280 prim_permutables =
 281     [quickhunk 0 "e" "bo" :> quickhunk 3 "" "x" :> quickhunk 2 "f" "qljo"]
 282
 283 mergeables :: [Prim :\/: Prim]
 284 mergeables = [quickhunk 1 "a" "b" :\/: quickhunk 1 "a" "c",
 285               quickhunk 1 "a" "b" :\/: quickhunk 3 "z" "c",
 286               quickhunk 0 "" "a" :\/: quickhunk 1 "" "b",
 287               quickhunk 0 "a" "" :\/: quickhunk 1 "" "b",
 288               quickhunk 0 "a" "" :\/: quickhunk 1 "b" "",
 289               quickhunk 0 "" "a" :\/: quickhunk 1 "b" ""
 290              ]
 291
 292 mergeablesFL :: [FL Prim :\/: FL Prim]
 293 mergeablesFL = map (\ (x:\/:y) -> (x :>: NilFL) :\/: (y :>: NilFL)) mergeables ++
 294            [] --    [(quickhunk 1 "a" "b" :>: quickhunk 3 "z" "c" :>: NilFL)
 295               --  :\/: (quickhunk 1 "a" "z" :>: NilFL),
 296               --  (quickhunk 1 "a" "b" :>: quickhunk 1 "b" "c" :>: NilFL)
 297               --  :\/: (quickhunk 1 "a" "z" :>: NilFL)]
 298
 299 mergeable2commutable :: Invert p => p :\/: p -> p :> p
 300 mergeable2commutable (x :\/: y) = invert x :> y
 301
 302 prim_patches :: [Prim]
 303 prim_patches = concatMap mergeable2patches mergeables
 304     where mergeable2patches (x:\/:y) = [x,y]
 305
 306 real_patches :: [RealPatch]
 307 real_patches = concatMap commutable2patches real_commutables
 308     where commutable2patches (x:>y) = [x,y]
 309
 310 real_triples :: [RealPatch :> RealPatch :> RealPatch]
 311 real_triples = [ob' :> oa2 :> a2'',
 312                 oa' :> oa2 :> a2''] ++ triple_examples
 313                ++ map unsafeUnseal2 (concatMap getTriples realFLs)
 314     where oa = prim2real $ quickhunk 1 "o" "aa"
 315           oa2 = oa
 316           a2 = prim2real $ quickhunk 2 "a34" "2xx"
 317           ob = prim2real $ quickhunk 1 "o" "bb"
 318           ob' :/\: oa' = merge (oa :\/: ob)
 319           a2' :/\: _ = merge (ob' :\/: a2)
 320           a2'' :/\: _ = merge (oa2 :\/: a2')
 321
 322 realFLs :: [FL RealPatch]
 323 realFLs = [oa :>: invert oa :>: oa :>: invert oa :>: ps +>+ oa :>: invert oa :>: NilFL]
 324     where oa = prim2real $ quickhunk 1 "o" "a"
 325           ps :/\: _ = merge (oa :>: invert oa :>: NilFL :\/: oa :>: invert oa :>: NilFL)
 326
 327 real_commutables :: [RealPatch :> RealPatch]
 328 real_commutables = commute_examples ++ map mergeable2commutable real_mergeables++
 329                    [invert oa :> ob'] ++ map unsafeUnseal2 (concatMap getPairs realFLs)
 330     where oa = prim2real $ quickhunk 1 "o" "a"
 331           ob = prim2real $ quickhunk 1 "o" "b"
 332           _ :/\: ob' = mergeFL (ob :\/: oa :>: invert oa :>: NilFL)
 333
 334 real_mergeables :: [RealPatch :\/: RealPatch]
 335 real_mergeables = map (\ (x :\/: y) -> prim2real x :\/: prim2real y) mergeables
 336                         ++ real_igloo_mergeables
 337                         ++ real_quickcheck_mergeables
 338                         ++ merge_examples
 339                         ++ catMaybes (map pair2m (concatMap getPairs realFLs))
 340                         ++ [(oa :\/: od),
 341                             (oa :\/: a2'),
 342                             (ob' :\/: od''),
 343                             (oe :\/: od),
 344                             (of' :\/: oe'),
 345                             (ob' :\/: oe'),
 346                             (oa :\/: oe'),
 347                             (ob' :\/: oc'),
 348                             (b2' :\/: oc'''),
 349                             (ob' :\/: a2),
 350                             (b2' :\/: og'''),
 351                             (oc''' :\/: og'''),
 352                             (oc'' :\/: og''),
 353                             (ob'' :\/: og''),
 354                             (ob'' :\/: oc''),
 355                             (oc' :\/: od'')]
 356     where oa = prim2real $ quickhunk 1 "o" "aa"
 357           a2 = prim2real $ quickhunk 2 "a34" "2xx"
 358           og = prim2real $ quickhunk 3 "4" "g"
 359           ob = prim2real $ quickhunk 1 "o" "bb"
 360           b2 = prim2real $ quickhunk 2 "b" "2"
 361           oc = prim2real $ quickhunk 1 "o" "cc"
 362           od = prim2real $ quickhunk 7 "x" "d"
 363           oe = prim2real $ quickhunk 7 "x" "e"
 364           pf = prim2real $ quickhunk 7 "x" "f"
 365           od'' = prim2real $ quickhunk 8 "x" "d"
 366           ob' :>: b2' :>: NilFL :/\: _ = mergeFL (oa :\/: ob :>: b2 :>: NilFL)
 367           a2' :/\: _ = merge (ob' :\/: a2)
 368           ob'' :/\: _ = merge (a2 :\/: ob')
 369           og' :/\: _ = merge (oa :\/: og)
 370           og'' :/\: _ = merge (a2 :\/: og')
 371           og''' :/\: _ = merge (ob' :\/: og')
 372           oc' :/\: _ = merge (oa :\/: oc)
 373           oc'' :/\: _ = merge (a2 :\/: oc)
 374           oc''' :/\: _ = merge (ob' :\/: oc')
 375           oe' :/\: _ = merge (od :\/: oe)
 376           of' :/\: _ = merge (od :\/: pf)
 377           pair2m :: Sealed2 (RealPatch :> RealPatch)
 378                  -> Maybe (RealPatch :\/: RealPatch)
 379           pair2m (Sealed2 (xx :> y)) = do y' :> _ <- commute (xx :> y)
 380                                           return (xx :\/: y')
 381
 382 real_igloo_mergeables :: [RealPatch :\/: RealPatch]
 383 real_igloo_mergeables = [(a :\/: b),
 384                     (b :\/: c),
 385                     (a :\/: c),
 386                     (x :\/: a),
 387                     (y :\/: b),
 388                     (z :\/: c),
 389                     (x' :\/: y'),
 390                     (z' :\/: y'),
 391                     (x' :\/: z'),
 392                     (a :\/: a)]
 393     where a = prim2real $ quickhunk 1 "1" "A"
 394           b = prim2real $ quickhunk 2 "2" "B"
 395           c = prim2real $ quickhunk 3 "3" "C"
 396           x = prim2real $ quickhunk 1 "1BC" "xbc"
 397           y = prim2real $ quickhunk 1 "A2C" "ayc"
 398           z = prim2real $ quickhunk 1 "AB3" "abz"
 399           x' :/\: _ = merge (a :\/: x)
 400           y' :/\: _ = merge (b :\/: y)
 401           z' :/\: _ = merge (c :\/: z)
 402
 403 real_quickcheck_mergeables :: [RealPatch :\/: RealPatch]
 404 real_quickcheck_mergeables = [-- invert k1 :\/: n1
 405                              --, invert k2 :\/: n2
 406                                hb :\/: k
 407                              , b' :\/: b'
 408                              , n' :\/: n'
 409                              , b :\/: d
 410                              , k' :\/: k'
 411                              , k3 :\/: k3
 412                              ] ++ catMaybes (map pair2m pairs)
 413     where hb = prim2real $ quickhunk 0 "" "hb"
 414           k = prim2real $ quickhunk 0 "" "k"
 415           n = prim2real $ quickhunk 0 "" "n"
 416           b = prim2real $ quickhunk 1 "b" ""
 417           d = prim2real $ quickhunk 2 "" "d"
 418           d':/\:_ = merge (b :\/: d)
 419           --k1 :>: n1 :>: NilFL :/\: _ = mergeFL (hb :\/: k :>: n :>: NilFL)
 420           --k2 :>: n2 :>: NilFL :/\: _ =
 421           --    merge (hb :>: b :>: NilFL :\/: k :>: n :>: NilFL)
 422           k' :>: n' :>: NilFL :/\: _ :>: b' :>: _ = merge (hb :>: b :>: d' :>: NilFL :\/: k :>: n :>: NilFL)
 423           pairs = getPairs (hb :>: b :>: d' :>: k' :>: n' :>: NilFL)
 424           pair2m :: Sealed2 (RealPatch :> RealPatch)
 425                  -> Maybe (RealPatch :\/: RealPatch)
 426           pair2m (Sealed2 (xx :> y)) = do y' :> _ <- commute (xx :> y)
 427                                           return (xx :\/: y')
 428
 429           i = prim2real $ quickhunk 0 "" "i"
 430           x = prim2real $ quickhunk 0 "" "x"
 431           xi = prim2real $ quickhunk 0 "xi" ""
 432           d3 :/\: _ = merge (xi :\/: d)
 433           _ :/\: k3 = mergeFL (k :\/: i :>: x :>: xi :>: d3 :>: NilFL)
 434
 435 \end{code}
 436
 437 \begin{code}
 438 commute_fails :: (MyEq p, Patchy p) => (p :> p -> Maybe (p :> p)) -> p :> p
 439               -> Maybe Doc
 440 commute_fails c (x :> y) = do y' :> x' <- c (x :> y)
 441                               return $ redText "x" $$ showPatch x $$
 442                                        redText ":> y" $$ showPatch y $$
 443                                        redText "y'" $$ showPatch y' $$
 444                                        redText ":> x'" $$ showPatch x'
 445
 446 \end{code}