-- 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.

{-# OPTIONS_GHC -cpp -fno-warn-deprecations -fglasgow-exts -fno-warn-orphans #-}
{-# LANGUAGE CPP #-}

#include "gadts.h"

module Darcs.Test.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 System.IO.Unsafe ( unsafePerformIO )
import Test.QuickCheck
import Control.Monad ( liftM, liftM2, liftM3, liftM4, replicateM )

import Darcs.Patch.Info ( PatchInfo, patchinfo )
import Darcs.Test.Patch.Check ( PatchCheck,
                                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, FileContents(..)
                              )
import Darcs.Patch.RegChars ( regChars )
import ByteStringUtils ( linesPS )
import qualified Data.ByteString as B ( ByteString, null, concat )
import qualified Data.ByteString.Char8 as BC ( break, pack )
import Darcs.Patch.FileName ( fn2fp )
import qualified Data.Map as M ( mapMaybe )

import Darcs.Patch.Patchy ( Commute )
import Darcs.Patch ( addfile, adddir, move, showPatch,
                     hunk, tokreplace, joinPatches, binary,
                     changepref, isMerger, invert, commute, merge,
                     readPatch, resolveConflicts,
                     effect, fromPrims,
                     unravel, merger, elegantMerge )
import Darcs.Patch.Core ( Patch(..) )
import Darcs.Patch.Prim ( Prim(..), DirPatchType(..), FilePatchType(..),
                          CommuteFunction, Perhaps(..),
                          subcommutes )
import Printer ( renderPS )
import Darcs.Witnesses.Ordered
import Darcs.Witnesses.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

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 = do n <- unempty
           a <- unempty
           l <- unempty
           d <- unempty
           return $ unsafePerformIO $ patchinfo n d a l

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

instance Arbitrary B.ByteString where
    arbitrary = liftM BC.pack 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

-- resize to size 25, that means we'll get line numbers no greater
-- than 1025 using QuickCheck 2.1
linenumgen :: Gen Int
linenumgen = frequency [(1,return 1), (1,return 2), (1,return 3),
                    (3,liftM (\n->1+abs n) (resize 25 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 B.ByteString
filelinegen = liftM BC.pack $
              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)

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 | isMerger 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

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]

prop_commute_twice :: Patch -> Patch -> Property
prop_commute_twice p1 p2 =
    (does_commute p1 p2) ==> (Just (p1:>p2) == (commute (p1:>p2) >>= commute))
does_commute :: Patch -> Patch -> Bool
does_commute p1 p2 =
    commute (p1:>p2) /= 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 (p1:>p2) of
    Just (p2':>p1') -> check_a_patch $ join_patches [p1,p2,invert p1',invert p2']
    _ -> impossible

prop_commute_either_way :: Patch -> Patch -> Property
prop_commute_either_way p1 p2 =
    does_commute p1 p2 ==> does_commute (invert p2) (invert p1)

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 (p1:>p2) of
    Nothing -> False
    Just (p2':>p1') ->
        case commute (p1':>p3) of
        Nothing -> False
        Just (p3':>_) ->
            case commute (p2':>p3') of
            Nothing -> False
            Just (p3'' :> _) ->
                case commute (p2:>p3) of
                Nothing -> False
                Just (p3'a:>_) ->
                    case commute (p1:>p3'a) of
                    Just (p3''a:>_) -> p3''a == p3''
                    Nothing -> False

prop_patch_and_inverse_is_identity :: Patch -> Patch -> Property
prop_patch_and_inverse_is_identity p1 p2 =
    (check_a_patch $ join_patches [p1,p2]) && (commute (p1:>p2) /= Nothing) ==>
    case commute (p1:>p2) of
    Just (p2':>_) -> case commute (invert p1:>p2') of
                    Nothing -> True -- This is a subtle distinction.
                    Just (p2'':>_) -> p2'' == p2
    Nothing -> impossible

quickmerge :: (Patch :\/: Patch) -> Patch
quickmerge (p1:\/:p2) = case merge (p1:\/:p2) of
                        _ :/\: p1' -> p1'

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 commute (p1:>p2') of
        Nothing -> False
        Just (p2'':>p1'') -> 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']

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) of
      Nothing -> Nothing
      Just (x:<y) ->
        case commute (y:>x) of
        Nothing -> Nothing
        Just (p2b :> p1'b) ->
          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 (invert p2 :> p1) of
  Just (p1':>_) ->
      case commute (p2:>p1') 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` elegantMerge (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 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

instance Show p => Show (p :> p) where
  show (x :> y) = show x ++ " :> " ++ show y

test_patch :: String
test_patch = test_str ++ test_note
tp1, tp2 :: Patch
tp1 = unsafeUnseal . fst . fromJust . readPatch $ BC.pack "\nmove ./test/test ./hello\n"
tp2 = unsafeUnseal . fst . fromJust . readPatch $ BC.pack "\nmove ./test ./hello\n"
tp1', tp2' :: Patch
tp2' = quickmerge (tp2:\/:tp1)
tp1' = quickmerge (tp1:\/:tp2)
test_note :: String
test_note = (if commute (tp1:>tp2') == Just (tp2:>tp1')
              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")
           ++"commute of tp2 and tp1' is "++show (commute (tp2:>tp1'))++"\n"
           ++"commute of tp1 and tp2' is "++show (commute (tp1:>tp2'))++"\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")-}

-- | 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.
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))

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)

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)

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]))
            $ resolveConflicts 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

try_tok_possibly :: String -> String -> String
                -> (Maybe FileContents) -> (Maybe FileContents)
try_tok_possibly t o n = liftM $ \contents ->
        let lines' = M.mapMaybe (liftM B.concat
                                  . try_tok_internal t (BC.pack o) (BC.pack n))
                                (fc_lines contents)
        in contents { fc_lines = lines' }

try_tok_internal :: String -> B.ByteString -> B.ByteString
                 -> B.ByteString -> Maybe [B.ByteString]
try_tok_internal _ _ _ s | B.null s = Just []
try_tok_internal t o n s =
    case BC.break (regChars t) s of
    (before,s') ->
        case BC.break (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

prop_read_show :: Patch -> Bool
prop_read_show p = case readPatch $ renderPS $ showPatch p of
                   Just (Sealed p',_) -> p' == p
                   Nothing -> False

-- |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.
prop_commute_inverse :: Patch -> Patch -> Property
prop_commute_inverse p1 p2 =
    does_commute p1 p2 ==> case commute (p1 :> p2) of
                           Nothing -> impossible
                           Just (_ :> p1') ->
                               case commute (p1' :> invert p2) of
                               Nothing -> False
                               Just (_ :> p1'') -> p1'' == p1

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