%  Copyright (C) 2002-2003 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 -fno-warn-deprecations #-}
module PatchTest
             ( 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_glump_order_independent,
               prop_glump_seq_merge, prop_glump_seq_merge_valid,
               prop_glump_three_merge, prop_glump_three_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,
             ) where

import Prelude hiding ( pi )
import Debug.QuickCheck
import Control.Monad ( liftM, liftM2, liftM3, liftM4, liftM5, replicateM )
import Data.Char ( ord )

import PatchInfo ( PatchInfo, patchinfo )
import PatchCheck ( 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, unpackPS, packString,
                          linesPS, nullPS, concatPS, breakPS,
                        )
import FileName ( fn2fp )

import Patch ( eq_patches, null_patch, addfile, adddir, move,
               hunk, tokreplace, join_patches, namepatch, binary,
               changepref, is_merger, invert, commute, merge,
               readPatch, flatten, resolve_conflicts,
               merger_equivalent, unravel, merger, glump, elegant_merge,
             )
import PatchCommute ( subcommutes, CommuteFunction, Perhaps(..) )
import PatchCore ( Patch(..), DirPatchType(..), FilePatchType(..) )

#include "impossible.h"

instance Eq Patch where
    (==) = eq_patches

instance Arbitrary Patch where
    arbitrary = sized arbpatch
    coarbitrary p = coarbitrary (show p)
\end{code}

\begin{code}
hunkgen :: Gen Patch
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 Patch
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 -> Patch) -> Gen Patch
twofilegen p = do
  n1 <- filepathgen
  n2 <- filepathgen
  if n1 /= n2 && (check_a_patch $ p n1 n2)
     then return $ p n1 n2
     else twofilegen p

chprefgen :: Gen Patch
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 Patch
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 Patch
onepatchgen = oneof [simplepatchgen, liftM invert simplepatchgen]

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

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

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

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
                             Nothing -> impossible
                             Just (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
          Just (p2',p1') ->
              if check_a_patch $ join_patches [p1',p2']
              then return $ join_patches [p1',p2']
              else return $ join_patches [addfile "Error_in_mergegen",
                                          addfile "Error_in_mergegen",
                                          p1,p2,p1',p2']
          Nothing -> impossible
     else mergegen n
  where len = if n < 15 then n`div`3 else 3

namedgen :: Int -> Gen Patch
namedgen n =
    liftM5 namepatch unempty unempty unempty arbitrary $ arbpatch (n-1)

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)

depgen :: Int -> Gen Patch
depgen n =
    liftM3 NamedP arbitrary arbitrary $ arbpatch (n-1)

{-
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 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,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 [] = []

badfpgen :: Gen String
badfpgen =  frequency [(1,return "test"), (1,return "hello"), (1,return "world"),
                       (1,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 (NamedP _ _ p) = check_patch p
check_patch p | is_merger p = do
  check_patch $ merger_equivalent p
check_patch (Merger _ _ _ _ _ _) = impossible
check_patch (Conflictor False a [b]) =
    do check_patch $ invert $ join_patches a
       check_patch b
       check_patch $ invert b
check_patch (Conflictor True a [b]) =
    do check_patch b
       check_patch $ invert b
       check_patch $ join_patches a
check_patch (Conflictor _ a b) =
    do check_patch $ join_patches a
       check_patch $ invert $ join_patches a
       check_patch $ join_patches b
       check_patch $ invert $ join_patches b
check_patch (ComP []) = is_valid
check_patch (ComP (p:ps)) =
  check_patch p >> check_patch (ComP ps)
check_patch (Split []) = is_valid
check_patch (Split (p:ps)) =
  check_patch p >> check_patch (Split ps)

check_patch (FP f RmFile) = remove_file $ fn2fp f
check_patch (FP f AddFile) =  create_file $ fn2fp f
check_patch (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 (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 (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 (DP d AddDir) = create_dir $ fn2fp d
check_patch (DP d RmDir) = remove_dir $ fn2fp d

check_patch (Move f f') = check_move (fn2fp f) (fn2fp f')
check_patch (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) == (commute (p2,p1) >>= commute))
does_commute :: Patch -> Patch -> Bool
does_commute p1 p2 =
    commute (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 commute (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 commute (p2,p1) of
    Nothing -> False
    Just (p1',p2') ->
        case commute (p3,p1') of
        Nothing -> False
        Just (_,p3') ->
            case commute (p3',p2') of
            Nothing -> False
            Just (_, p3'') ->
                case commute (p3,p2) of
                Nothing -> False
                Just (_,p3'a) ->
                    case commute (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 $ ComP [p1,p2]) && (commute (p2,p1) /= Nothing) ==>
    case commute (p2,p1) of
    Just (_,p2') -> case commute (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 (p2,p1) = case merge (p2,p1) of
                     Just (p1',_) -> p1'
                     Nothing -> impossible
\end{code}

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

prop_merge_valid :: Patch -> Patch -> Property
prop_merge_valid p1 p2 =
    (check_a_patch $ ComP [invert p1,p2]) ==>
    case merge (p2,p1) of
    Nothing -> False
    Just (p2',p1') ->
        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 $ ComP [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) >>= commute 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 commute (p1, invert p2) of
  Just (_,p1') ->
      case commute (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 $ ComP [invert p1,p2]) ==>
    (fst `liftM` smart_merge (p2,p1)) == elegant_merge (p2,p1)
\end{code}

\begin{code}
prop_glump_order_independent :: String -> Patch -> Patch -> Property
prop_glump_order_independent g p1 p2 =
    (check_a_patch $ ComP [invert p1,p2]) ==>
    glump g p1 p2 == glump g p2 p1
\end{code}

\begin{code}
prop_glump_seq_merge :: String -> Patch -> Patch -> Patch -> Property
prop_glump_seq_merge g p1 p2 p3 =
    (check_a_patch $ ComP [invert p1,p2, p3]) ==>
    glump g p3 (merger g p2 p1) == glump g (merger g p2 p1) p3
prop_glump_seq_merge_valid :: String -> Patch -> Patch -> Patch -> Property
prop_glump_seq_merge_valid _ p1 p2 p3 =
    (check_a_patch $ ComP [invert p1,p2, p3]) ==>
    (check_a_patch $ join_patches [invert p1,p2,p3,invert p3,invert p2])
test_patch :: String
test_patch = test_str ++ test_note
tp1, tp2 :: Patch
tp1 = fst . fromJust . readPatch $ packString "\nmove ./test/test ./hello\n"
tp2 = 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 commute (tp2',tp1) == Just (tp1', tp2)
              then "At least they commute right.\n"
              else "Argh! they don't even commute 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")
           ++"commute of tp1' and tp2 is "++show (commute (tp1',tp2))++"\n"
           ++"commute of tp2' and tp1 is "++show (commute (tp2',tp1))++"\n"
           {-++ "\nSimply flattened, it is:\n"
                  ++ (show $ map (join_patches.flatten.merger_equivalent) $ flatten tp)
           ++ "\n\nUnravelled, it gives:\n" ++ (show $ map unravel $ flatten tp)
           ++ "\n\nUnwound, it gives:\n" ++ (show $ map unwind $ flatten 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}

\begin{code}
prop_glump_three_merge :: String -> Patch -> Patch -> Patch -> Property
prop_glump_three_merge g p1 p2 p3 =
    (check_a_patch $ ComP [invert p1,p2,invert p2, p3]) ==>
    glump g (merger g p2 p1) (merger g p2 p3) ==
          glump g (merger g p1 p2) (merger g p1 p3)
              &&
    glump g (merger g p2 p1) (merger g p2 p3) ==
          glump g (merger g p1 p3) (merger g p1 p2)
prop_glump_three_merge_valid :: String -> Patch -> Patch -> Patch -> Property
prop_glump_three_merge_valid g p1 p2 p3 =
    (check_a_patch $ ComP [invert p1,p2,invert p2, p3]) ==>
    (check_a_patch $
     join_patches [invert p1,p2,invert p2,p3,invert p3,
                   glump g (merger g p2 p1) (merger g p2 p3)])
\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 $ ComP [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 $ ComP [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 $ ComP [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 $ ComP [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
                  Just (p1',_) -> join_patches [p2,p1']
                  Nothing -> impossible
merge_list :: [Patch] -> Patch
merge_list ps = doml null_patch ps
doml :: Patch -> [Patch] -> Patch
doml mp (p:ps) = case merge (mp,p) of
                 Just (mp',_) -> doml (join_patches $ p : (flatten mp')) ps
                 Nothing -> impossible
doml mp [] = 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 $ packString $ show p of
                   Just (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 commute (p2, p1) of
                           Nothing -> impossible
                           Just (p1',_) ->
                               case commute (invert p2, p1') of
                               Nothing -> False
                               Just (p1'',_) -> p1'' == p1
\end{code}

\begin{code}
subcommutes_inverse :: [(String, Patch -> Patch -> 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, Patch -> Patch -> 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, Patch -> Patch -> 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 -> Patch -> Patch -> Bool
does_fail c p1 p2 =
    fails (c (p2,p1)) && (check_a_patch $ join_patches [p1,p2])
        where fails Failed = True
              fails _ = False

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

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