%  Copyright (C) 2002-2003,2007 David Roundy
%
%  This program is free software; you can redistribute it and/or modify
%  it under the terms of the GNU General Public License as published by
%  the Free Software Foundation; either version 2, or (at your option)
%  any later version.
%
%  This program is distributed in the hope that it will be useful,
%  but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%  GNU General Public License for more details.
%
%  You should have received a copy of the GNU General Public License
%  along with this program; see the file COPYING.  If not, write to
%  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
%  Boston, MA 02110-1301, USA.


\begin{code}
{-# OPTIONS_GHC -cpp -fno-warn-deprecations -fglasgow-exts #-}
#include "gadts.h"
module Darcs.Patch.Test
             ( prop_read_show,
               prop_inverse_composition, prop_commute_twice,
               prop_inverse_valid, prop_other_inverse_valid,
               prop_commute_equivalency, prop_commute_either_order,
               prop_commute_either_way, prop_merge_is_commutable_and_correct,
               prop_merge_is_swapable, prop_merge_valid,
               prop_unravel_three_merge, prop_unravel_seq_merge,
               prop_unravel_order_independent,
               prop_simple_smart_merge_good_enough,
               prop_elegant_merge_good_enough,
               prop_patch_and_inverse_is_identity,
               quickmerge, check_patch, check_a_patch, verbose_check_a_patch,
               prop_resolve_conflicts_valid,
               test_patch, prop_commute_inverse,
               subcommutes_inverse, subcommutes_nontrivial_inverse,
               subcommutes_failure,
               join_patches
             ) where

import Prelude hiding ( pi )
import Test.QuickCheck
import Control.Monad ( liftM, liftM2, liftM3, liftM4, replicateM )

import Darcs.Patch.Info ( PatchInfo, patchinfo )
import Darcs.Patch.Check ( PatchCheck, Possibly(..),
                    check_move, remove_dir, create_dir,
                    is_valid, insert_line, file_empty, file_exists,
                    delete_line, modify_file, create_file, remove_file,
                    do_check, do_verbose_check,
                  )
import RegChars ( regChars )
import FastPackedString ( PackedString, packString,
                          linesPS, nullPS, concatPS, breakPS,
                        )
import FileName ( fn2fp )

import Darcs.Patch.Patchy ( Commute )
import Darcs.Patch ( addfile, adddir, move, showPatch,
                     hunk, tokreplace, joinPatches, binary,
                     changepref, is_merger, invert, commute, commutex, merge,
                     readPatch, resolve_conflicts,
                     effect, fromPrims,
                     unravel, merger, elegant_merge )
import Darcs.Patch.Core ( Patch(..) )
import Darcs.Patch.Prim ( Prim(..), DirPatchType(..), FilePatchType(..),
                          CommuteFunction, Perhaps(..),
                          subcommutes )
import Printer ( renderPS )
import Darcs.Patch.Ordered
import Darcs.Sealed ( Sealed(Sealed), unsafeUnseal, unseal )

#include "impossible.h"

instance Eq Patch where
   x == y = IsEq == (x =\/= y)

instance Eq Prim where
   x == y = IsEq == (x =\/= y)

instance (Commute a, MyEq a) => Eq (FL a) where
   x == y = IsEq == (x =\/= y)

instance Arbitrary Patch where
    arbitrary = sized arbpatch
--    coarbitrary p = coarbitrary (show p)

instance Arbitrary Prim where
    arbitrary = onepatchgen
--    coarbitrary = impossible
\end{code}

\begin{code}
hunkgen :: Gen Prim
hunkgen = do
  i <- frequency [(1,choose (0,5)),(1,choose (0,35)),
                  (2,return 0),(3,return 1),(2,return 2),(1,return 3)]
  j <- frequency [(1,choose (0,5)),(1,choose (0,35)),
                  (2,return 0),(3,return 1),(2,return 2),(1,return 3)]
  if i == 0 && j == 0 then hunkgen
    else liftM4 hunk filepathgen linenumgen
                (replicateM i filelinegen)
                (replicateM j filelinegen)

tokreplacegen :: Gen Prim
tokreplacegen = do
  f <- filepathgen
  o <- tokengen
  n <- tokengen
  if o == n
     then return $ tokreplace f "A-Za-z" "old" "new"
     else return $ tokreplace f "A-Za-z_" o n

twofilegen :: (FilePath -> FilePath -> Prim) -> Gen Prim
twofilegen p = do
  n1 <- filepathgen
  n2 <- filepathgen
  if n1 /= n2 && (check_a_patch $ fromPrims $ (p n1 n2 :>: NilFL))
     then return $ p n1 n2
     else twofilegen p

chprefgen :: Gen Prim
chprefgen = do
  f <- oneof [return "color", return "movie"]
  o <- tokengen
  n <- tokengen
  if o == n then return $ changepref f "old" "new"
            else return $ changepref f o n

simplepatchgen :: Gen Prim
simplepatchgen = frequency [(1,liftM addfile filepathgen),
                            (1,liftM adddir filepathgen),
                            (1,liftM3 binary filepathgen arbitrary arbitrary),
                            (1,twofilegen move),
                            (1,tokreplacegen),
                            (1,chprefgen),
                            (7,hunkgen)
                           ]

onepatchgen :: Gen Prim
onepatchgen = oneof [simplepatchgen, (invert) `fmap` simplepatchgen]

norecursgen :: Int -> Gen Patch
norecursgen 0 = PP `fmap` onepatchgen
norecursgen n = oneof [PP `fmap` onepatchgen,flatcompgen n]

arbpatch :: Int -> Gen Patch
arbpatch 0 = PP `fmap` onepatchgen
arbpatch n = frequency [(3,PP `fmap` onepatchgen),
                       -- (1,compgen n),
                        (2,flatcompgen n),
                        (0,raw_merge_gen n),
                        (0,mergegen n),
                        (1,PP `fmap` onepatchgen)
                       ]

unempty :: Arbitrary a => Gen [a]
unempty = do
  as <- arbitrary
  case as of
    [] -> unempty
    _ -> return as

join_patches :: [Patch] -> Patch
join_patches = joinPatches . unsafeFL

raw_merge_gen :: Int -> Gen Patch
raw_merge_gen n = do p1 <- arbpatch len
                     p2 <- arbpatch len
                     if (check_a_patch $ join_patches [invert p1,p2]) &&
                        (check_a_patch $ join_patches [invert p2,p1])
                        then case merge (p2 :\/: p1) of
                             _ :/\: p2' -> return p2'
                        else raw_merge_gen n
    where len = if n < 15 then n`div`3 else 3

mergegen :: Int -> Gen Patch
mergegen n = do
  p1 <- norecursgen len
  p2 <- norecursgen len
  if (check_a_patch $ join_patches [invert p1,p2]) &&
         (check_a_patch $ join_patches [invert p2,p1])
     then case merge (p2:\/:p1) of
          p1' :/\: p2' ->
              if check_a_patch $ join_patches [p1,p2']
              then return $ join_patches [p1,p2']
              else return $ join_patches [PP $ addfile "Error_in_mergegen",
                                          PP $ addfile "Error_in_mergegen",
                                          p1,p2,p1',p2']
     else mergegen n
  where len = if n < 15 then n`div`3 else 3

arbpi :: Gen PatchInfo
arbpi = liftM4 patchinfo unempty unempty unempty unempty

instance Arbitrary PatchInfo where
    arbitrary = arbpi
--    coarbitrary pi = coarbitrary (show pi)

instance Arbitrary PackedString where
    arbitrary = liftM packString arbitrary
--    coarbitrary ps = coarbitrary (unpackPS ps)

{-
plistgen :: Int -> Int -> Gen [Patch]
plistgen s n
    | n <= 0 = return []
    | otherwise = do
                  next <- arbpatch s
                  rest <- plistgen s (n-1)
                  return $ next : rest

compgen :: Int -> Gen Patch
compgen n = do
    size <- choose (0,n)
    myp <- liftM join_patches $ plistgen size ((n+1) `div` (size+1))
-- here I assume we only want to consider valid patches...
    if check_a_patch myp
       then return myp
       else compgen n
-}

flatlistgen :: Int -> Gen [Patch]
flatlistgen n = replicateM n (PP `fmap` onepatchgen)

flatcompgen :: Int -> Gen Patch
flatcompgen n = do
  myp <- liftM (join_patches . regularize_patches) $ flatlistgen n
  if check_a_patch myp
     then return myp
     else flatcompgen n

linenumgen :: Gen Int
linenumgen = frequency [(1,return 1), (1,return 2), (1,return 3),
                    (3,liftM (\n->1+abs n) arbitrary) ]

tokengen :: Gen String
tokengen = oneof [return "hello", return "world", return "this",
                  return "is", return "a", return "silly",
                  return "token", return "test"]

toklinegen :: Gen String
toklinegen = liftM unwords $ replicateM 3 tokengen

filelinegen :: Gen PackedString
filelinegen = liftM packString $
              frequency [(1,map fromSafeChar `fmap` arbitrary),(5,toklinegen),
                         (1,return ""), (1,return "{"), (1,return "}") ]

filepathgen :: Gen String
filepathgen = liftM fixpath badfpgen

fixpath :: String -> String
fixpath "" = "test"
fixpath p = fpth p

fpth :: String -> String
fpth ('/':'/':cs) = fpth ('/':cs)
fpth (c:cs) = c : fpth cs
fpth [] = []

newtype SafeChar = SS Char
instance Arbitrary SafeChar where
    arbitrary = oneof $ map (return . SS) (['a'..'z']++['A'..'Z']++['1'..'9']++"0")

fromSafeChar :: SafeChar -> Char
fromSafeChar (SS s) = s

badfpgen :: Gen String
badfpgen =  frequency [(1,return "test"), (1,return "hello"), (1,return "world"),
                       (1,map fromSafeChar `fmap` arbitrary),
                       (1,liftM2 (\a b-> a++"/"++b) filepathgen filepathgen) ]

{-
instance Arbitrary Char where
    arbitrary = oneof $ map return
                (['a'..'z']++['A'..'Z']++['1'..'9']++['0','~','.',',','-','/'])
-}
--    coarbitrary c = coarbitrary (ord c)
\end{code}

\begin{code}
check_patch :: Patch -> PatchCheck Bool
check_a_patch :: Patch -> Bool
check_a_patch p = do_check $ do check_patch p
                                check_patch $ invert p
verbose_check_a_patch :: Patch -> Bool
verbose_check_a_patch p = do_verbose_check $ do check_patch p
                                                check_patch $ invert p

check_patch p | is_merger p = do
  check_patch $ fromPrims $ effect p
check_patch (Merger _ _ _ _) = impossible
check_patch (Regrem _ _ _ _) = impossible
check_patch (ComP NilFL) = is_valid
check_patch (ComP (p:>:ps)) =
  check_patch p >> check_patch (ComP ps)
check_patch (PP Identity) = is_valid
check_patch (PP (Split NilFL)) = is_valid
check_patch (PP (Split (p:>:ps))) =
  check_patch (PP p) >> check_patch (PP (Split ps))

check_patch (PP (FP f RmFile)) = remove_file $ fn2fp f
check_patch (PP (FP f AddFile)) =  create_file $ fn2fp f
check_patch (PP (FP f (Hunk line old new))) = do
    file_exists $ fn2fp f
    mapM (delete_line (fn2fp f) line) old
    mapM (insert_line (fn2fp f) line) (reverse new)
    is_valid
check_patch (PP (FP f (TokReplace t old new))) =
    modify_file (fn2fp f) (try_tok_possibly t old new)
-- note that the above isn't really a sure check, as it leaves PSomethings
-- and PNothings which may have contained new...
check_patch (PP (FP f (Binary o n))) = do
    file_exists $ fn2fp f
    mapM (delete_line (fn2fp f) 1) (linesPS o)
    file_empty $ fn2fp f
    mapM (insert_line (fn2fp f) 1) (reverse $ linesPS n)
    is_valid

check_patch (PP (DP d AddDir)) = create_dir $ fn2fp d
check_patch (PP (DP d RmDir)) = remove_dir $ fn2fp d

check_patch (PP (Move f f')) = check_move (fn2fp f) (fn2fp f')
check_patch (PP (ChangePref _ _ _)) = return True

regularize_patches :: [Patch] -> [Patch]
regularize_patches patches = rpint [] patches
    where rpint ok_ps [] = ok_ps
          rpint ok_ps (p:ps) =
            if check_a_patch (join_patches $ p:ok_ps)
            then rpint (p:ok_ps) ps
            else rpint ok_ps ps
\end{code}

\begin{code}
prop_inverse_composition :: Patch -> Patch -> Bool
prop_inverse_composition p1 p2 =
    invert (join_patches [p1,p2]) == join_patches [invert p2, invert p1]
prop_inverse_valid :: Patch -> Bool
prop_inverse_valid p1 = check_a_patch $ join_patches [invert p1,p1]
prop_other_inverse_valid :: Patch -> Bool
prop_other_inverse_valid p1 = check_a_patch $ join_patches [p1,invert p1]
\end{code}

\begin{code}
prop_commute_twice :: Patch -> Patch -> Property
prop_commute_twice p1 p2 =
    (does_commute p1 p2) ==> (Just (p2:<p1) == (commutex (p2:<p1) >>= commutex))
does_commute :: Patch -> Patch -> Bool
does_commute p1 p2 =
    commutex (p2:<p1) /= Nothing && (check_a_patch $ join_patches [p1,p2])
prop_commute_equivalency :: Patch -> Patch -> Property
prop_commute_equivalency p1 p2 =
    (does_commute p1 p2) ==>
    case commutex (p2:<p1) of
    Just (p1':<p2') -> check_a_patch $ join_patches [p1,p2,invert p1',invert p2']
    _ -> impossible
\end{code}

\begin{code}
prop_commute_either_way :: Patch -> Patch -> Property
prop_commute_either_way p1 p2 =
    does_commute p1 p2 ==> does_commute (invert p2) (invert p1)
\end{code}

\begin{code}
prop_commute_either_order :: Patch -> Patch -> Patch -> Property
prop_commute_either_order p1 p2 p3 =
    check_a_patch (join_patches [p1,p2,p3]) &&
    does_commute p1 (join_patches [p2,p3]) &&
    does_commute p2 p3 ==>
    case commutex (p2:<p1) of
    Nothing -> False
    Just (p1':<p2') ->
        case commutex (p3:<p1') of
        Nothing -> False
        Just (_:<p3') ->
            case commutex (p3':<p2') of
            Nothing -> False
            Just (_:< p3'') ->
                case commutex (p3:<p2) of
                Nothing -> False
                Just (_:<p3'a) ->
                    case commutex (p3'a:<p1) of
                    Just (_:<p3''a) -> p3''a == p3''
                    Nothing -> False
\end{code}

\begin{code}
prop_patch_and_inverse_is_identity :: Patch -> Patch -> Property
prop_patch_and_inverse_is_identity p1 p2 =
    (check_a_patch $ join_patches [p1,p2]) && (commutex (p2:<p1) /= Nothing) ==>
    case commutex (p2:<p1) of
    Just (_:<p2') -> case commutex (p2':<invert p1) of
                    Nothing -> True -- This is a subtle distinction.
                    Just (_:<p2'') -> p2'' == p2
    Nothing -> impossible
\end{code}

\begin{code}
quickmerge :: (Patch :\/: Patch) -> Patch
quickmerge (p1:\/:p2) = case merge (p1:\/:p2) of
                        _ :/\: p1' -> p1'
\end{code}

\begin{code}
prop_merge_is_commutable_and_correct :: Patch -> Patch -> Property
prop_merge_is_commutable_and_correct p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    case merge (p2:\/:p1) of
    p1' :/\: p2' ->
        case commutex (p2':<p1) of
        Nothing -> False
        Just (p1'':<p2'') -> p2'' == p2 && p1' == p1''
prop_merge_is_swapable :: Patch -> Patch -> Property
prop_merge_is_swapable p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    case merge (p2:\/:p1) of
    p1' :/\: p2' ->
           case merge (p1:\/:p2) of
           p2''' :/\: p1''' -> p1' == p1''' && p2' == p2'''

prop_merge_valid :: Patch -> Patch -> Property
prop_merge_valid p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    case merge (p2:\/:p1) of
    _ :/\: p2' ->
        check_a_patch $ join_patches [invert p1,p2,invert p2,p1,p2']
\end{code}

\begin{code}
prop_simple_smart_merge_good_enough :: Patch -> Patch -> Property
prop_simple_smart_merge_good_enough p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    smart_merge (p2:\/:p1) == simple_smart_merge (p2:\/:p1)

smart_merge :: (Patch :\/: Patch) -> Maybe (Patch :< Patch)
smart_merge (p1 :\/: p2) =
  case simple_smart_merge (p1:\/:p2) of
  Nothing -> Nothing
  Just (p1'a:<p2a) ->
      case simple_smart_merge (p2 :\/: p1) >>= commutex of
      Nothing -> Nothing
      Just (p1'b :< p2b) ->
          if p1'a == p1'b && p2a == p2b && p2a == p2
          then Just (p1'a :< p2)
          else Nothing
simple_smart_merge :: (Patch :\/:  Patch) -> Maybe (Patch :< Patch)
simple_smart_merge (p1 :\/: p2) =
  case commutex (p1 :< invert p2) of
  Just (_:<p1') ->
      case commutex (p1':< p2) of
      Just (_:< p1o) ->
          if p1o == p1 then Just (p1' :< p2)
          else Nothing
      Nothing -> Nothing
  Nothing -> Nothing

prop_elegant_merge_good_enough :: Patch -> Patch -> Property
prop_elegant_merge_good_enough p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    (fst' `fmap` smart_merge (p2:\/:p1)) ==
       (snd'' `fmap` elegant_merge (p2:\/:p1))

fst' :: p :< p -> p
fst' (x:<_) = x

snd'' :: q :/\: p -> p
snd'' (_:/\:x) = x

instance Eq p => Eq (p :< p) where
   (x:<y) == (x':<y') = x == x' && y == y'

instance Show p => Show (p :< p) where
  show (x :< y) = show x ++ " :< " ++ show y
\end{code}

\begin{code}
test_patch :: String
test_patch = test_str ++ test_note
tp1, tp2 :: Patch
tp1 = unsafeUnseal . fst . fromJust . readPatch $ packString "\nmove ./test/test ./hello\n"
tp2 = unsafeUnseal . fst . fromJust . readPatch $ packString "\nmove ./test ./hello\n"
tp1', tp2' :: Patch
tp2' = quickmerge (tp2:\/:tp1)
tp1' = quickmerge (tp1:\/:tp2)
test_note :: String
test_note = (if commutex (tp2':<tp1) == Just (tp1':<tp2)
              then "At least they commutex right.\n"
              else "Argh! they don't even commutex right.\n")
         ++(if check_a_patch $ tp2
              then "tp2 itself is valid!\n"
              else "Oh my! tp2 isn't even valid!\n")
         ++(if check_a_patch $ tp2'
              then "tp2' itself is valid!\n"
              else "Aaack! tp2' itself is invalid!\n")
         ++(if check_a_patch $ join_patches [tp1, tp2']
              then "Valid merge tp2'!\n"
              else "Bad merge tp2'!\n")
         ++ (if check_a_patch $ join_patches [tp2, tp1']
              then "Valid merge tp1'!\n"
              else "Bad merge tp1'!\n")
         ++ (if check_a_patch $ join_patches [tp2,tp1',invert tp2',invert tp1]
              then "Both agree!\n"
              else "The two merges don't agree!\n")
         ++ (if check_a_patch $ join_patches [invert tp2, tp1]
              then "They should be mergable!\n"
              else "Wait a minute, these guys can't be merged!\n")
tp :: Patch
tp = tp1'

test_str :: String
test_str = "Patches are:\n"++(show tp)
           ++(if check_a_patch tp
              then "At least the patch itself is valid.\n"
              else "The patch itself is bad!\n")
           ++"commutex of tp1' and tp2 is "++show (commutex (tp1':<tp2))++"\n"
           ++"commutex of tp2' and tp1 is "++show (commutex (tp2':<tp1))++"\n"
           {-++ "\nSimply flattened, it is:\n"
                  ++ (show $ mapFL (joinPatches.flattenFL.merger_equivalent) $ flattenFL tp)
           ++ "\n\nUnravelled, it gives:\n" ++ (show $ map unravel $ flatten tp)
           ++ "\n\nUnwound, it gives:\n" ++ (show $ mapFL unwind $ flattenFL tp)
           ++(if check_a_patch (join_patches$ reverse $ unwind tp)
              then "Unwinding is valid.\n"
              else "Bad unwinding!\n")
           ++(if check_a_patch $ join_patches [tp,invert tp]
              then "Inverse is valid.\n"
              else "Bad inverse!\n")
           ++(if check_a_patch $ join_patches [invert tp, tp]
              then "Other inverse is valid.\n"
              else "Bad other inverse!\n")-}
\end{code}

The conflict resolution code (glump) begins by ``unravelling'' the merger
into a set of sequences of patches.  Each sequence of patches corresponds
to one non-conflicted patch that got merged together with the others.  The
result of the unravelling of a series of merges must obviously be
independent of the order in which those merges are performed.  This
unravelling code (which uses the unwind code mentioned above) uses probably
the second most complicated algorithm.  Fortunately, if we can successfully
unravel the merger, almost any function of the unravelled merger satisfies
the two constraints mentioned above that the conflict resolution code must
satisfy.

\begin{code}
prop_unravel_three_merge :: Patch -> Patch -> Patch -> Property
prop_unravel_three_merge p1 p2 p3 =
    (check_a_patch $ join_patches [invert p1,p2,invert p2,p3]) ==>
    (unravel $ merger "0.0" (merger "0.0" p2 p3) (merger "0.0" p2 p1)) ==
    (unravel $ merger "0.0" (merger "0.0" p1 p3) (merger "0.0" p1 p2))
\end{code}
\begin{code}
prop_unravel_seq_merge :: Patch -> Patch -> Patch -> Property
prop_unravel_seq_merge p1 p2 p3 =
    (check_a_patch $ join_patches [invert p1,p2,p3]) ==>
    (unravel $ merger "0.0" p3 $ merger "0.0" p2 p1) ==
    (unravel $ merger "0.0" (merger "0.0" p2 p1) p3)
\end{code}
\begin{code}
prop_unravel_order_independent :: Patch -> Patch -> Property
prop_unravel_order_independent p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    (unravel $ merger "0.0" p2 p1) == (unravel $ merger "0.0" p1 p2)
\end{code}

\begin{code}
prop_resolve_conflicts_valid :: Patch -> Patch -> Property
prop_resolve_conflicts_valid p1 p2 =
    (check_a_patch $ join_patches [invert p1,p2]) ==>
    and $ map (check_a_patch.(\l-> join_patches [p,merge_list l]))
            $ resolve_conflicts p
        where p = case merge (p1:\/:p2) of
                  _ :/\: p1' -> join_patches [p2,p1']

merge_list :: [Sealed (FL Prim C(x))] -> Patch
merge_list patches = fromPrims `unseal` doml NilFL patches
    where doml mp (Sealed p:ps) =
              case commute (invert p :> mp) of
              Just (mp' :> _) -> doml (effect p +>+ effect mp') ps
              Nothing -> doml mp ps -- This shouldn't happen for "good" resolutions.
          doml mp [] = Sealed mp
\end{code}

\begin{code}
try_tok_possibly :: String -> String -> String
                -> [Possibly PackedString] -> Maybe [Possibly PackedString]
try_tok_possibly t o n mss =
    mapM (silly_maybe_possibly $ liftM concatPS .
                    try_tok_internal t (packString o) (packString n))
                 $ take 1000 mss

silly_maybe_possibly :: (PackedString -> Maybe PackedString) ->
                        (Possibly PackedString -> Maybe (Possibly PackedString))
silly_maybe_possibly f =
    \px -> case px of
           PNothing -> Just PNothing
           PSomething -> Just PSomething
           PJust x -> case f x of
                      Nothing -> Nothing
                      Just x' -> Just $ PJust x'

try_tok_internal :: String -> PackedString -> PackedString
                 -> PackedString -> Maybe [PackedString]
try_tok_internal _ _ _ s | nullPS s = Just []
try_tok_internal t o n s =
    case breakPS (regChars t) s of
    (before,s') ->
        case breakPS (not . regChars t) s' of
        (tok,after) ->
            case try_tok_internal t o n after of
            Nothing -> Nothing
            Just rest ->
                if tok == o
                then Just $ before : n : rest
                else if tok == n
                     then Nothing
                     else Just $ before : tok : rest
\end{code}

\begin{code}
prop_read_show :: Patch -> Bool
prop_read_show p = case readPatch $ renderPS $ showPatch p of
                   Just (Sealed p',_) -> p' == p
                   Nothing -> False
\end{code}

%In order for merges to work right with commuted patches, inverting a patch
%past a patch and its inverse had golly well better give you the same patch
%back again.
\begin{code}
prop_commute_inverse :: Patch -> Patch -> Property
prop_commute_inverse p1 p2 =
    does_commute p1 p2 ==> case commutex (p2:< p1) of
                           Nothing -> impossible
                           Just (p1':<_) ->
                               case commutex (invert p2:< p1') of
                               Nothing -> False
                               Just (p1'':<_) -> p1'' == p1
\end{code}

\begin{code}
subcommutes_inverse :: [(String, Prim -> Prim -> Property)]
subcommutes_inverse = zip names (map prop_subcommute cs)
    where (names, cs) = unzip subcommutes
          prop_subcommute c p1 p2 =
              does c p1 p2 ==>
              case c (p2:< p1) of
              Succeeded (p1':<p2') ->
                  case c (invert p2:< p1') of
                  Succeeded (p1'':<ip2x') -> p1'' == p1 &&
                      case c (invert p1:< invert p2) of
                      Succeeded (ip2':< ip1') ->
                          case c (p2':< invert p1) of
                          Succeeded (ip1o':< p2o) ->
                              invert ip1' == p1' && invert ip2' == p2' &&
                              ip1o' == ip1' && p2o == p2 &&
                              p1'' == p1 && ip2x' == ip2'
                          _ -> False
                      _ -> False
                  _ -> False
              _ -> False

subcommutes_nontrivial_inverse :: [(String, Prim -> Prim -> Property)]
subcommutes_nontrivial_inverse = zip names (map prop_subcommute cs)
    where (names, cs) = unzip subcommutes
          prop_subcommute c p1 p2 =
              nontrivial c p1 p2 ==>
              case c (p2:< p1) of
              Succeeded (p1':<p2') ->
                  case c (invert p2:< p1') of
                  Succeeded (p1'':<ip2x') -> p1'' == p1 &&
                      case c (invert p1:< invert p2) of
                      Succeeded (ip2':< ip1') ->
                          case c (p2':< invert p1) of
                          Succeeded (ip1o':< p2o) ->
                              invert ip1' == p1' && invert ip2' == p2' &&
                              ip1o' == ip1' && p2o == p2 &&
                              p1'' == p1 && ip2x' == ip2'
                          _ -> False
                      _ -> False
                  _ -> False
              _ -> False

subcommutes_failure :: [(String, Prim -> Prim -> Property)]
subcommutes_failure = zip names (map prop cs)
    where (names, cs) = unzip subcommutes
          prop c p1 p2 =
              does_fail c p1 p2 ==> case c (invert p1 :< invert p2) of
                                    Failed -> True
                                    _ -> False

does_fail :: CommuteFunction -> Prim -> Prim -> Bool
does_fail c p1 p2 =
    fails (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
        where fails Failed = True
              fails _ = False

does :: CommuteFunction -> Prim -> Prim -> Bool
does c p1 p2 =
    succeeds (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
        where succeeds (Succeeded _) = True
              succeeds _ = False

nontrivial :: CommuteFunction -> Prim -> Prim -> Bool
nontrivial c p1 p2 =
    succeeds (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
        where succeeds (Succeeded (p1' :< p2')) = p1' /= p1 || p2' /= p2
              succeeds _ = False
\end{code}