\begin{code}
{-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts -fallow-undecidable-instances #-}
#include "gadts.h"
module Darcs.Patch.QuickCheck ( WithStartState, RepoModel, Tree,
#ifndef GADT_WITNESSES
                                merge_examples, commute_examples, triple_examples,
#endif
                                prop_consistent_tree_flattenings, prop_fail,
                                prop_is_mergeable,
                                flattenOne, simpleCheck, simpleConditionalCheck, thoroughCheck,
                                commutePairFromTree, mergePairFromTree,
                                commuteTripleFromTree,
                                commutePairFromTWFP, mergePairFromTWFP, getPairs, getTriples,
                                patchFromTree,
                                quickCheck, real_patch_loop_examples, shrink
                              ) where

import Control.Arrow ( (***) )
import Control.Monad ( liftM, replicateM, mplus, mzero )
import FastPackedString
import Test.QuickCheck
import Darcs.Sealed
import Darcs.Patch ( Patch )
import Darcs.Patch.Ordered
import Darcs.Patch.Patchy (--showPatch,
                           Invert(..), Commute(..))
import Darcs.Patch.Prim (Prim(..), Effect(..), FilePatchType(..), FromPrim(..), is_identity )
import Darcs.Patch.Real ( RealPatch, prim2real )
--import Darcs.ColorPrinter ( errorDoc )
--import Darcs.ColorPrinter ( traceDoc )
import Darcs.Show
--import Printer ( greenText, ($$) )
import FileName

#include "impossible.h"


#ifndef GADT_WITNESSES
instance Eq (a C(x y)) => Eq (Sealed2 a) where
    (Sealed2 x) == (Sealed2 y) = x == y
#endif

instance Show2 Patch where
    show2 = show

#ifndef GADT_WITNESSES
triple_examples :: (FromPrim p, Commute p, Invert p) => [p :> p :> p]
triple_examples = [commuteTripleFromTree id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "g"]))
                     (SeqTree (FP (fp2fn "./file") (Hunk 1 [] [packString "j"]))
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "s"])) NilTree)))
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "e"])) NilTree))
                  ,commuteTripleFromTree id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file",
                                               rmFileContents = [packString "j"] })
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "s"]))
                     (ParTree
                      (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "j"] [])) NilTree)
                      (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "j"] [])) NilTree)))
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "j"] [])) NilTree))
                  ]


merge_examples :: (FromPrim p, Commute p, Invert p) => [p :\/: p]
merge_examples = map (mergePairFromCommutePair id) commute_examples

commute_examples :: (FromPrim p, Commute p) => [p :> p]
commute_examples = [
                   commutePairFromTWFP id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                   (TWFP 3
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "h"])) NilTree)
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "b"]))
                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "f"]))
                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "v"]))
                           (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "f"] [])) NilTree)))))),
                   commutePairFromTWFP id $
                   WithStartState
                   (RepoModel { rmFileName = fp2fn "./file",
                                rmFileContents = [packString "f",packString "s",packString "d"] })
                   (TWFP 3
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 2 [packString "d"] [])) NilTree)
                     (ParTree
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "f"] [])) NilTree)
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "f"] []))
                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "s",packString "d"] []))
                          (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "v"])) NilTree)))))),
{-                   commutePairFromTWFP id $
                   WithStartState
                   (RepoModel { rmFileName = fp2fn "./file",
                                rmFileContents = [packString "f",packString "u",
                                                  packString "s",packString "d"] })
                   (TWFP 5
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 4 [] [packString "x"]))
                      (SeqTree (FP (fp2fn "./file") (Hunk 3 [packString "d"] [])) NilTree))
                     (ParTree
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "f",packString "u"] [])) NilTree)
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "f"] []))
                       (SeqTree (FP(fp2fn "./file") (Hunk 0 [packString "u",packString "s",packString "d"] []))
                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "a"]))
                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "a"] [])) NilTree))))))),-}
                   commutePairFromTree id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file",
                                          rmFileContents = [packString "n",packString "t",packString "h"] })
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "n",packString "t",packString "h"] []))
                     NilTree)
                    (SeqTree (FP (fp2fn "./file") (Hunk 2 [packString "h"] []))
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "n"] []))
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "t"] [])) NilTree)))),
                  commutePairFromTree id $
                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                  (ParTree
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "n"])) NilTree)
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "i"]))
                                (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "i"])) NilTree))),
                  commutePairFromTree id $
                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                  (ParTree
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "c"]))
                     (ParTree
                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "c"] [packString "r"])) NilTree)
                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "h"]))
                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "d"])) NilTree))))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "f"])) NilTree)),
                  commutePairFromTWFP id $
                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                  (TWFP 1
                  (ParTree
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "t"])) NilTree)
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "t"])) NilTree))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "f"])) NilTree))),
                   commutePairFromTWFP id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file",
                                               rmFileContents = [packString "f",packString " r",
                                                                 packString "c",packString "v"] })
                   (TWFP 4
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 2 [packString "c",packString "v"] []))
                        (ParTree
                         (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "r"] []))
                          (SeqTree (FP (fp2fn "fi le") (Hunk 0 [packString "f"] [])) NilTree))
                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "f",packString "r"] []))
                          (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "y"])) NilTree))))
                     (SeqTree (FP (fp2fn "./file") (Hunk 3 [packString "v"] [])) NilTree))),
                   commutePairFromTree id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "z"])) NilTree)
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "f"])) NilTree)
                     (ParTree
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "r"])) NilTree)
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "d"])) NilTree))))
                 , commutePairFromTree id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file",
                                               rmFileContents = [packString "t",packString "r",
                                                                 packString "h"] })
                   (ParTree
                    (ParTree
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "t",packString "r",packString "h"] []))
                              NilTree)
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "o"])) NilTree))
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "t"] []))
                     (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "h"] [])) NilTree)))
                 , commutePairFromTWFP id $
                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] }) $
                   TWFP 2
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "h"])) NilTree)
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "y"]))
                     (SeqTree (FP (fp2fn "./file") (Hunk 1 [] [packString "m"]))
                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "v"])) NilTree))))
                 , commutePairFromTree id $
                 WithStartState (RepoModel {rmFileName = fp2fn "./file",rmFileContents = [] })
                 (ParTree
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "p"]))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "p"] []))
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "c"])) NilTree)))
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "z"])) NilTree))
                 , commutePairFromTree id $
                 WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                 (ParTree
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "j" ]))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "j"] [])) NilTree))
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "v"])) NilTree))
                 , commutePairFromTree id $
                 WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                 (ParTree
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "v"])) NilTree)
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "j" ]))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [packString "j"] [])) NilTree)))
                 , commutePairFromTree id $
                 WithStartState (RepoModel { rmFileName = fp2fn "./file",
                                             rmFileContents = [packString "x",packString "c"] })
                 (ParTree
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "h"]))
                   (ParTree
                    (SeqTree (FP (fp2fn "./file") (Hunk 2 [packString "c"] [])) NilTree)
                    (SeqTree (FP (fp2fn "./file") (Hunk 1 [packString "x"] []))
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "j"])) NilTree))))
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [packString "l"])) NilTree))
                 , commutePairFromTree id $
                 WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
                 (ParTree
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "s"))) NilTree)
                  (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "k")))
                   (SeqTree (FP (fp2fn "./file") (Hunk 0 (packStringLetters "k") []))
                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "m")))
                     (SeqTree (FP (fp2fn "./file") (Hunk 0 (packStringLetters "m") [])) NilTree)))))
                 ]
#endif

simpleConditionalCheck :: (Arbitrary p, Show p, Show q) => (p -> Bool) -> (p -> Maybe q) -> IO Int
simpleConditionalCheck nottrivial t = do okay <- quickCheckWith maxSuccessTests maxTryTests maxSize t'
                                         return $ if okay then 0 else 1
    where t' p = nottrivial p ==> case t p of
                                  Nothing -> True
                                  Just q -> error $ show q
          maxSuccessTests = 100
          maxTryTests     = 50 * maxSuccessTests
          maxSize         = 100

simpleCheck :: (Arbitrary p, Show p, Show q) => (p -> Maybe q) -> IO Int
simpleCheck t = do okay <- quickCheck' t'
                   return $ if okay then 0 else 1
    where t' p = case t p of
                 Nothing -> True
                 Just q -> error $ show q

thoroughCheck :: (Arbitrary p, Show p, Show q) => Int -> (p -> Maybe q) -> IO Int
thoroughCheck num t = do let ntries = 20*num
                             maxsize = max 100 (num `div` 10)
                         okay <- quickCheckWith num ntries maxsize t'
                         return $ if okay then 0 else 1
    where t' p = case t p of
                 Nothing -> True
                 Just q -> error $ show q

data RepoModel C(x)
 = RepoModel {
     rmFileName :: !FileName,
     rmFileContents :: [PackedString]
   } deriving (Eq)

instance Show (RepoModel C(x)) where
  showsPrec d rm = showParen (d > app_prec) $
                   showString "RepoModel { rmFileName = " . showsPrec 0 (rmFileName rm) .
                   showString ", rmFileContents = " . showsPrec 0 (rmFileContents rm) .
                   showString " }"

instance Show1 RepoModel where
    showsPrec1 = showsPrec

#ifdef GADT_WITNESSES
data InitRepoModel -- this ought to be defined somewhere central as the unique starting state
#endif

initRepoModel :: RepoModel C(InitRepoModel)
initRepoModel = RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] }
rebuildRepoModel :: RepoModel C(x) -> RepoModel C(y)
rebuildRepoModel rm = RepoModel { rmFileName = rmFileName rm, rmFileContents = rmFileContents rm }

data WithEndState px s C(y) = WithEndState { wesPatch :: px C(y), _wesState :: s C(y) }

class ArbitraryState s p where
  arbitraryState :: s C(x) -> Gen (Sealed (WithEndState (p C(x)) s))
  -- does a coarbitrary make sense?

class ArbitraryStateIn s p where
  arbitraryStateIn :: s C(x) -> Gen (p C(x))

instance ArbitraryState RepoModel Prim where
  arbitraryState rm = oneof [arbitraryFP rm]

instance Arbitrary (Sealed2 (FL Prim)) where
  arbitrary = do Sealed2 ps1 <- liftM (unseal (seal2 . wesPatch)) $ arbitraryState initRepoModel
                 return $ Sealed2 $ mapFL_FL make_identity_identity ps1
                     where make_identity_identity :: Prim C(x y) -> Prim C(x y)
                           make_identity_identity p | IsEq <- is_identity p = identity
                                                    | otherwise = p

instance Arbitrary (Sealed2 (FL (WithState RepoModel Prim))) where
  arbitrary = liftM (unseal (seal2 . wesPatch)) $ arbitraryState initRepoModel

prop_consistent_tree_flattenings :: Sealed (WithStartState RepoModel (Tree Prim)) -> Bool
prop_consistent_tree_flattenings (Sealed (WithStartState start t))
  = fromJust $
    do Sealed (G2 flat) <- return $ flattenTree $ mapTree prim2real t
       rms <- return $ map (applyPatch start) flat
       return $ and $ zipWith assert_equal_fst (zip rms flat) (tail $ zip rms flat)

assert_equal_fst :: (Eq a, Show a, Show b, Show c) => (a, b) -> (a, c) -> Bool
assert_equal_fst (x,bx) (y,by)
    | x == y = True
    | otherwise = error ("Not really equal:\n" ++ show x ++ "\nand\n" ++ show y
                         ++ "\ncoming from\n" ++ show bx ++ "\nand\n" ++ show by)

-- WithState and prop_fail are handy for debugging arbitrary code
data WithState s p C(x y) = WithState (s C(x)) (p C(x y)) (s C(y))
  deriving Show

data WithStartState s p C(x) = WithStartState (s C(x)) (p C(x))

instance (Show1 s, Show1 p) => Show (WithStartState s p C(x)) where
   showsPrec d (WithStartState s p) = showParen (d > app_prec) $ showString "WithStartState " .
                                      showsPrec1 (app_prec + 1) s . showString " " .
                                      showsPrec1 (app_prec + 1) p

instance (Show1 s, Show1 p) => Show1 (WithStartState s p) where
   showsPrec1 = showsPrec

prop_fail :: Int -> Tree Prim C(x) -> Bool
prop_fail n xs = sizeTree xs < n

instance ArbitraryState s p => ArbitraryState s (WithState s p) where
  arbitraryState rm = do xandrm' <- arbitraryState rm
                         flip unseal xandrm' $ \(WithEndState x rm') ->
                           return $ seal $ WithEndState (WithState rm x rm') rm'

instance ArbitraryState s p => ArbitraryState s (FL p) where
  arbitraryState rm1 = sized $ \n -> do k <- choose (0, n)
                                        arbitraryList k rm1
      where arbitraryList :: FORALL(x) Int -> s C(x) -> Gen (Sealed (WithEndState (FL p C(x)) s))
            arbitraryList 0 rm = return $ seal $ WithEndState NilFL rm
            arbitraryList (n+1) rm = do Sealed (WithEndState x rm') <- arbitraryState rm
                                        Sealed (WithEndState xs rm'') <- arbitraryList n rm'
                                        return $ seal $ WithEndState (x :>: xs) rm''
            arbitraryList _ _ = impossible

data Tree p C(x) where
   NilTree :: Tree p C(x)
   SeqTree :: p C(x y) -> Tree p C(y) -> Tree p C(x)
   ParTree :: Tree p C(x) -> Tree p C(x) -> Tree p C(x)

mapTree :: (FORALL(y z) p C(y z) -> q C(y z)) -> Tree p C(x) -> Tree q C(x)
mapTree _ NilTree = NilTree
mapTree f (SeqTree p t) = SeqTree (f p) (mapTree f t)
mapTree f (ParTree t1 t2) = ParTree (mapTree f t1) (mapTree f t2)

instance Show2 p => Show (Tree p C(x)) where
   showsPrec _ NilTree = showString "NilTree"
   showsPrec d (SeqTree a t) = showParen (d > app_prec) $ showString "SeqTree " .
                               showsPrec2 (app_prec + 1) a . showString " " .
                               showsPrec (app_prec + 1) t
   showsPrec d (ParTree t1 t2) = showParen (d > app_prec) $ showString "ParTree " .
                                 showsPrec (app_prec + 1) t1 . showString " " .
                                 showsPrec (app_prec + 1) t2

instance Show2 p => Show1 (Tree p) where
    showsPrec1 = showsPrec

sizeTree :: Tree p C(x) -> Int
sizeTree NilTree = 0
sizeTree (SeqTree _ t) = 1 + sizeTree t
sizeTree (ParTree t1 t2) = 1 + sizeTree t1 + sizeTree t2

-- newtype G1 l p C(x) = G1 { _unG1 :: l (p C(x)) }
newtype G2 l p C(x y) = G2 { unG2 :: l (p C(x y)) }

flattenTree :: (Commute p) => Tree p C(z) -> Sealed (G2 [] (FL p) C(z))
flattenTree NilTree = seal $ G2 $ return NilFL
flattenTree (SeqTree p t) = mapSeal (G2 . map (p :>:) . unG2) $ flattenTree t
flattenTree (ParTree t1 t2) = flip unseal (flattenTree t1) $ \gpss1 ->
                              flip unseal (flattenTree t2) $ \gpss2 ->
                              seal $ G2 $
                              do ps1 <- unG2 gpss1
                                 ps2 <- unG2 gpss2
                                 ps2' :/\: ps1' <- return $ merge (ps1 :\/: ps2)
                                 -- We can't prove that the existential type in the result
                                 -- of merge will be the same for each pair of
                                 -- ps1 and ps2.
                                 map unsafeCoerceP [ps1 +>+ ps2', ps2 +>+ ps1']

instance ArbitraryState s p => ArbitraryStateIn s (Tree p) where
  arbitraryStateIn rm = frequency [(2, return NilTree)
                                  ,(2, do Sealed (WithEndState p rm') <- arbitraryState rm
                                          t <- arbitraryStateIn rm'
                                          return (SeqTree p t))
                                  ,(1, do t1 <- arbitraryStateIn rm
                                          t2 <- arbitraryStateIn rm
                                          return (ParTree t1 t2))]


shrinkWSSTree :: Sealed (WithStartState RepoModel (Tree Prim))
              -> [Sealed (WithStartState RepoModel (Tree Prim))]
shrinkWSSTree = unseal doShrinkWSSTree
 where
 doShrinkWSSTree wss@(WithStartState rm t)
  = shrinkWSSTree' wss -- shrink the tree
     `mplus`
    do -- shrink the starting context
      pos <- [0 .. length (rmFileContents rm) - 1]
      let rmFileContents' = take pos (rmFileContents rm) ++ drop (pos+1) (rmFileContents rm)
          t' = shrinkPosStart pos (canonizeTree t)
      return $ seal $ WithStartState (rm { rmFileContents = rmFileContents' }) (canonizeTree t')


-- If we had a more general repo model, then Int would need to be more general too

class ShrinkablePos p where
  shrinkPos :: Int -> p C(x y) -> (p C(x y), Maybe Int)
  shrinkPatch :: p C(x y) -> [(p C(x y), Maybe Int)]
  nullPatch :: p C(x y) -> EqCheck C(x y)

class ShrinkablePosStart p where
  shrinkPosStart :: Int -> p C(x) -> p C(x)

instance ShrinkablePos p => ShrinkablePosStart (Tree p) where
  shrinkPosStart _ NilTree = NilTree
  shrinkPosStart pos (SeqTree p t)
    = let (p', mpos') = shrinkPos pos p
      in case mpos' of
           Nothing -> SeqTree p' t
           Just pos' -> SeqTree p' (shrinkPosStart pos' t)
  shrinkPosStart pos (ParTree t1 t2) = ParTree (shrinkPosStart pos t1) (shrinkPosStart pos t2)

smartFP :: FileName -> FilePatchType C(x y) -> Prim C(x y)
smartFP _ (Hunk _ [] []) | avoidEmptyHunks = unsafeCoerceP Identity
smartFP fn filepatch = FP fn filepatch

instance ShrinkablePos Prim where
  shrinkPos pos (FP fn fp) = (smartFP fn *** id) (shrinkPos pos fp)
  shrinkPos pos Identity = (Identity, Just pos)
  shrinkPos _ _ = impossible
  shrinkPatch (FP fn fp) = map (smartFP fn *** id) (shrinkPatch fp)
  shrinkPatch Identity = []
  shrinkPatch _ = impossible
  nullPatch (FP _ fp) = nullPatch fp
  nullPatch Identity = IsEq
  nullPatch _ = impossible

avoidEmptyHunks :: Bool
avoidEmptyHunks = True

instance ShrinkablePos FilePatchType where
  shrinkPos pos (Hunk n old new)
    | pos < n = (Hunk (n-1) old new, Just pos)
    | pos >= n + length old = (Hunk n old new, Just (pos + length new - length old))
    | otherwise = (Hunk n (take pos' old ++ drop (pos'+1) old) new, Nothing)
        where pos' = pos - n
  shrinkPos _ _ = bug "foo1 in ShrinkablePos"
  shrinkPatch (Hunk (n+1) [] []) = [(Hunk n [] [], Nothing)]
  shrinkPatch (Hunk n old new)
   = do i <- [0 .. length new - 1]
        return (Hunk n old (take i new ++ drop (i+1) new), Just (n + i))
  shrinkPatch _ = bug "foo in ShrinkablePos"
  nullPatch (Hunk _ [] []) = unsafeCoerceP IsEq -- is this safe?
  nullPatch _ = NotEq

shrinkWSSTree'
 -- start a new line here because apparently ' confuses CPP..
   :: WithStartState RepoModel (Tree Prim) C(x)
   -> [Sealed (WithStartState RepoModel (Tree Prim))]
shrinkWSSTree' (WithStartState _ NilTree) = []
shrinkWSSTree' (WithStartState rm t@(SeqTree p t'))
  = return (seal (WithStartState (applyPatch rm p) (canonizeTree t')))
     `mplus`
    liftM (seal . WithStartState rm) (map canonizeTree $ shrinkTree t)
shrinkWSSTree' (WithStartState rm t@(ParTree _ _))
  = liftM (seal . WithStartState rm) (map canonizeTree $ shrinkTree t)

-- canonize a tree, removing any dead branches
canonizeTree :: ShrinkablePos p => Tree p C(x) -> Tree p C(x)
canonizeTree NilTree = NilTree
canonizeTree (ParTree t1 t2)
    | NilTree <- canonizeTree t1 = canonizeTree t2
    | NilTree <- canonizeTree t2 = canonizeTree t1
    | otherwise = ParTree (canonizeTree t1) (canonizeTree t2)
canonizeTree (SeqTree p t) | IsEq <- nullPatch p = canonizeTree t
                           | otherwise = SeqTree p (canonizeTree t)

-- shrink the tree without changing the starting context
shrinkTree :: ShrinkablePos p => Tree p C(x) -> [Tree p C(x)]
shrinkTree NilTree = []
shrinkTree (SeqTree p t) = do case nullPatch p of
                                 IsEq -> return t
                                 NotEq -> mzero
                             `mplus`
                           do (p', pos) <- shrinkPatch p
                              return (SeqTree p' (maybe id shrinkPosStart pos t))
                             `mplus`
                           do t' <- shrinkTree t
                              return (SeqTree p t')
shrinkTree (ParTree t1 t2) = [t1, t2]
                              `mplus`
                             do t1' <- shrinkTree t1
                                return (ParTree t1' t2)
                              `mplus`
                             do t2' <- shrinkTree t2
                                return (ParTree t1 t2')

instance Arbitrary (Sealed (WithStartState RepoModel (Tree Prim))) where
  arbitrary = do Sealed (WithStartState rm tree) <-
                     liftM (seal . WithStartState initRepoModel) (arbitraryStateIn initRepoModel)
                 return $ Sealed $ WithStartState rm (canonizeTree tree)
  shrink = shrinkWSSTree

prop_is_mergeable :: forall p C(x) . (FromPrim p, Commute p)
                  => Sealed (WithStartState RepoModel (Tree Prim))
                  -> Maybe (Tree p C(x))
prop_is_mergeable (Sealed (WithStartState _ t))
   = case flattenOne t of
        Sealed ps -> let _ = seal2 ps :: Sealed2 (FL p)
                     in case lengthFL ps of
                       _ -> Nothing

flattenOne :: (FromPrim p, Commute p) => Tree Prim C(x) -> Sealed (FL p C(x))
flattenOne NilTree = seal NilFL
flattenOne (SeqTree p t) = flip unseal (flattenOne t) $ \ps -> seal (fromPrim p :>: ps)
flattenOne (ParTree t1 t2) =
    flip unseal (flattenOne t1) $ \ps1 ->
    flip unseal (flattenOne t2) $ \ps2 ->
    --traceDoc (greenText "flattening two parallel series: ps1" $$ showPatch ps1 $$
    --          greenText "ps2" $$ showPatch ps2) $
    case merge (ps1 :\/: ps2) of
      ps2' :/\: _ -> seal (ps1 +>+ ps2')

instance Arbitrary (Sealed2 (FL RealPatch)) where
    arbitrary = do Sealed (WithStartState _ tree) <- arbitrary :: Gen (Sealed (WithStartState RepoModel (Tree Prim)))
                   return $ unseal seal2 (flattenOne tree)

instance Arbitrary (Sealed2 RealPatch) where
    arbitrary = do Sealed (WithStartState _ tree) <- arbitrary :: Gen (Sealed (WithStartState RepoModel (Tree Prim)))
                   case mapFL seal2 `unseal` flattenOne tree of
                     [] -> return $ seal2 $ fromPrim Identity
                     ps -> elements ps

instance (Arbitrary (Sealed2 (FL p)), Commute p) => Arbitrary (Sealed2 (p :\/: p)) where
    arbitrary = do Sealed2 (a :> b) <- arbitrary
                   case commute (a :> b) of
                     Just (b' :> _) -> return (seal2 (a :\/: b'))
                     Nothing -> arbitrary

instance Arbitrary (Sealed2 (FL p)) => Arbitrary (Sealed2 (p :> p)) where
    arbitrary = do Sealed2 ps <- arbitrary
                   let pairs = getPairs ps
                   case pairs of
                      [] -> arbitrary
                      _ -> elements pairs

instance (Invert p, Arbitrary (Sealed2 (FL p))) => Arbitrary (Sealed2 (p :> p :> p)) where
    arbitrary = do Sealed2 ps <- arbitrary
                   return $ last_triple ps
        where last_triple :: FL p C(x y) -> Sealed2 (p :> p :> p)
              last_triple NilFL = seal2 $ identity :> identity :> identity
              last_triple (a :>: NilFL) = seal2 $ a :> invert a :> identity
              last_triple (a :>: b :>: NilFL) = seal2 $ invert a :> a :> b
              last_triple (a :>: b :>: c :>: NilFL) = seal2 $ a :> b :> c
              last_triple (_ :>: xs) = last_triple xs

data TreeWithFlattenPos p C(x) = TWFP Int (Tree p C(x))

commutePairFromTWFP :: (FromPrim p, Commute p)
                    => (FORALL (y z) (p :> p) C(y z) -> t)
                    -> (WithStartState RepoModel (TreeWithFlattenPos Prim) C(x) -> t)
commutePairFromTWFP handlePair (WithStartState _ (TWFP n t))
    = unseal2 handlePair $
      let xs = unseal getPairs (flattenOne t)
      in if length xs > n && n >= 0 then xs!!n else seal2 (fromPrim Identity :> fromPrim Identity)

commutePairFromTree :: (FromPrim p, Commute p)
                    => (FORALL (y z) (p :> p) C(y z) -> t)
                    -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
commutePairFromTree handlePair (WithStartState _ t)
   = unseal2 handlePair $
     let Sealed ps = flattenOne t
         xs = --traceDoc (greenText "I'm flattening one to get:" $$ showPatch ps) $
              getPairs ps
     in if null xs then seal2 (fromPrim Identity :> fromPrim Identity) else last xs

commuteTripleFromTree :: (FromPrim p, Commute p)
                      => (FORALL (y z) (p :> p :> p) C(y z) -> t)
                      -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
commuteTripleFromTree handle (WithStartState _ t)
   = unseal2 handle $
     let Sealed ps = flattenOne t
         xs = --traceDoc (greenText "I'm flattening one to get:" $$ showPatch ps) $
              getTriples ps
     in if null xs
        then seal2 (fromPrim Identity :> fromPrim Identity :> fromPrim Identity)
        else last xs

mergePairFromCommutePair :: (Commute p, Invert p)
                         => (FORALL (y z) (p :\/: p) C(y z) -> t)
                         -> (FORALL (y z) (p :>   p) C(y z) -> t)
mergePairFromCommutePair handlePair (a :> b)
 = case commute (a :> b) of
     Just (b' :> _) -> handlePair (a :\/: b')
     Nothing -> handlePair (b :\/: b)

-- impredicativity problems mean we can't use (.) in the definitions below

mergePairFromTWFP :: (FromPrim p, Commute p, Invert p)
                  => (FORALL (y z) (p :\/: p) C(y z) -> t)
                  -> (WithStartState RepoModel (TreeWithFlattenPos Prim) C(x) -> t)
mergePairFromTWFP x = commutePairFromTWFP (mergePairFromCommutePair x)

mergePairFromTree :: (FromPrim p, Commute p, Invert p)
                  => (FORALL (y z) (p :\/: p) C(y z) -> t)
                  -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
mergePairFromTree x = commutePairFromTree (mergePairFromCommutePair x)

patchFromCommutePair :: (Commute p, Invert p)
                     => (FORALL (y z) p C(y z) -> t)
                     -> (FORALL (y z) (p :> p) C(y z) -> t)
patchFromCommutePair handle (_ :> b) = handle b

patchFromTree :: (FromPrim p, Commute p, Invert p)
              => (FORALL (y z) p C(y z) -> t)
              -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
patchFromTree x = commutePairFromTree (patchFromCommutePair x)


instance Show2 p => Show (TreeWithFlattenPos p C(x)) where
   showsPrec d (TWFP n t) = showParen (d > app_prec) $ showString "TWFP " .
                            showsPrec (app_prec + 1) n . showString " " .
                            showsPrec1 (app_prec + 1) t

instance Show1 (TreeWithFlattenPos Prim) where
   show1 = show

instance Arbitrary (Sealed (WithStartState RepoModel (TreeWithFlattenPos Prim))) where
   arbitrary = do Sealed (WithStartState rm t) <- arbitrary
                  let num = unseal (length . getPairs) (flattenOneRP t)
                  if num == 0 then return $ Sealed $ WithStartState rm $ TWFP 0 NilTree
                    else do n <- choose (0, num - 1)
                            return $ Sealed $ WithStartState rm $ TWFP n t
                    where -- just used to get the length. In principle this should be independent of the patch type.
                          flattenOneRP :: Tree Prim C(x) -> Sealed (FL RealPatch C(x))
                          flattenOneRP = flattenOne
   shrink (Sealed (WithStartState rm (TWFP n t))) =
      [Sealed (WithStartState rm' (TWFP n' t')) | Sealed (WithStartState rm' t') <- shrink (Sealed (WithStartState rm t)),
                                                  n' <- [0..n]]


getPairs :: FL p C(x y) -> [Sealed2 (p :> p)]
getPairs NilFL = []
getPairs (_:>:NilFL) = []
getPairs (a:>:b:>:c) = seal2 (a:>b) : getPairs (b:>:c)

getTriples :: FL p C(x y) -> [Sealed2 (p :> p :> p)]
getTriples NilFL = []
getTriples (_:>:NilFL) = []
getTriples (_:>:_:>:NilFL) = []
getTriples (a:>:b:>:c:>:d) = seal2 (a:>b:>c) : getTriples (b:>:c:>:d)

arbitraryFP :: RepoModel C(x) -> Gen (Sealed (WithEndState (Prim C(x)) RepoModel))
arbitraryFP rm
 = do (fp, newcontents) <- arbitraryFilePatchType (rmFileContents rm)
      return $ seal $ WithEndState (FP (rmFileName rm) fp) (rebuildRepoModel (rm { rmFileContents = newcontents }))

-- Really [PackedString] should be parametrised by x y, and the result tuple sealed on y
arbitraryFilePatchType :: [PackedString] -> Gen (FilePatchType C(x y), [PackedString])
arbitraryFilePatchType contents = oneof [arbitraryHunk contents]

arbitraryHunk :: [PackedString] -> Gen (FilePatchType C(x y), [PackedString])
arbitraryHunk contents
 = sized $ \n ->
   do start <- choose (0, min n (length contents))
      (removelen, _)
        <- frequency $ zip (if start == length contents then [1, 13, 0, 0] else [1, 3, 5, 3])
                [return (0, 0)
                ,do xa <- choose (0, n)
                    return (0, xa)
                ,do xr <- choose (1, min n (length contents - start))
                    return (xr, 0)
                ,do xr <- choose (1, min n (length contents - start))
                    xa <- choose (0, n)
                    return (xr, xa)
                ]
      addlen <- choose (0, n)
      additems <- replicateM addlen (do c <- choose ('a', 'z')
                                        return $ packString [c])
      let newcontents = take start contents ++ additems ++ drop (start + removelen) contents
      return (Hunk start (take removelen $ drop start $ contents) additems, newcontents)

class Applyable p where
  applyPatch :: RepoModel C(x) -> p C(x y) -> RepoModel C(y)

instance Applyable p => Applyable (FL p) where
  applyPatch rm NilFL = rm
  applyPatch rm (p :>: ps) = applyPatch (applyPatch rm p) ps

instance Applyable RealPatch where
  applyPatch rm p = applyPatch rm (effect p)

instance Applyable Prim where
  applyPatch (rm@RepoModel { rmFileName = filename, rmFileContents = oldcontents }) (FP filename' fp)
     | filename == filename' = rebuildRepoModel (rm { rmFileContents = applyFilePatchType oldcontents fp })
  applyPatch rm Identity = rm
  applyPatch _ _ = bug "We haven't defined applyPatch on Prim for all patch types."

applyFilePatchType :: [PackedString] -> FilePatchType C(x y) -> [PackedString]
applyFilePatchType oldcontents (Hunk n old new)
 = if take (length old) (drop n oldcontents) == old
   then take n oldcontents ++ new ++ drop (n + length old) oldcontents
   else error "Bad patch context"
applyFilePatchType _ _ = bug "We haven't defined applyFilePatchType for all patch types."

packStringLetters :: String -> [PackedString]
packStringLetters = map (packString . (:[]))

real_patch_loop_examples :: [Sealed (WithStartState RepoModel (Tree Prim))]
real_patch_loop_examples =
    [Sealed (WithStartState (RepoModel { rmFileName = fx, rmFileContents = [] })
     $ canonizeTree
     (ParTree
      (SeqTree (FP fx (Hunk 0 [] (packStringLetters "pkotufogbvdabnmbzajvolwviqebieonxvcvuvigkfgybmqhzuaaurjspd")))
       (ParTree
        (SeqTree (FP fx (Hunk 46 (packStringLetters "qhzu") (packStringLetters "zafybdcokyjskcgnvhkbzpysaafnjjhcstgrczplxsfwagmh")))
         (ParTree
          (ParTree
           NilTree
           (ParTree
            (ParTree
             (ParTree
              (SeqTree (FP fx (Hunk 14 (packStringLetters "mbzajvolwviqebieonxvcvuvigkfgyb") (packStringLetters "vujnxnhvybvpouyciaabszfmgssezlwwjgnethvrpnfrkubphzvdgymjjoacppqps")))
               (ParTree
                NilTree
                (ParTree
                 (SeqTree (FP fx (Hunk 39 (packStringLetters "ssezlwwjgnethvrpnfrkubphzvdgymjjoacppqpsmzafybdcokyjskcgnvhkbz") (packStringLetters "wnesidpccwoiqiichxaaejdsyrhrusqljlcoro")))
                  (ParTree
                   (ParTree
                    (SeqTree (FP fx (Hunk 11 (packStringLetters "abnvujnxnhvybvpouyciaabszfmgwnesidpccwoiqii") (packStringLetters "czfdhqkipdstfjycqaxwnbxrihrufdeyneqiiiafwzlmg"))) NilTree)
                    NilTree)
                   NilTree))
                 (SeqTree (FP fx (Hunk 24 [] (packStringLetters "dihgmsotezucqdgxczvcivijootyvhlwymbiueufnvpwpeukmskqllalfe"))) NilTree))))
              (SeqTree (FP fx (Hunk 55 (packStringLetters "yjskcgnvhkbzpysaafnjjhcstgrczplxsfwagmhaaurjsp") (packStringLetters "xldhrutyhcyaqeezwujiguawfyawjjqlirxshjddvq"))) NilTree))
             (SeqTree (FP fx (Hunk 19 [] (packStringLetters "ooygwiyogqrqnytixqtmvdxx")))
              (SeqTree (FP fx (Hunk 25 (packStringLetters "yogqrqnytixqtmvdxxvolwviqebieonxvcvuvigkfgybmzafybdcokyjskcgnvhkbz") (packStringLetters "akhsmlbkdxnvfoikmiatfbpzdrsyykkpoxvvddeaspzxe")))
               (SeqTree (FP fx (Hunk 38 [] (packStringLetters "ji")))
                (ParTree
                 NilTree
                 (ParTree
                  NilTree
                  (ParTree
                   (ParTree
                    NilTree
                    (SeqTree (FP fx (Hunk 25 (packStringLetters "akhsmlbkdxnvfjioikmiatfbpzdrsyykkpoxvvddeaspzxepysaafnjjhcstgrczplxs") (packStringLetters "onjbhddskcj")))
                     (SeqTree (FP fx (Hunk 38 [] (packStringLetters "fyscunxxxjjtyqpfxeznhtwvlphmp"))) NilTree)))
                   (ParTree
                    NilTree
                    (SeqTree (FP fx (Hunk 43 [] (packStringLetters "xcchzwmzoezxkmkhcmesplnjpqriypshgiqklgdnbmmkldnydiy")))
                     (ParTree
                      NilTree
                      (SeqTree (FP fx (Hunk 63 (packStringLetters "plnjpqriypshgiqklgdnbmmkldnydiymiatfbpzdrsyykkpoxvvddeaspzxepysaafn") (packStringLetters "anjlzfdqbjqbcplvqvkhwjtkigp"))) NilTree)))))))))))
            (ParTree
             NilTree
             NilTree)))
          NilTree))
        NilTree))
      (ParTree
       NilTree
       (SeqTree (FP fx (Hunk 0 [] (packStringLetters "ti")))
        (SeqTree (FP fx (Hunk 0 (packStringLetters "t") (packStringLetters "ybcop")))
         (SeqTree (FP fx (Hunk 1 [] (packStringLetters "dvlhgwqlpaeweerqrhnjtfolczbqbzoccnvdsyqiefqitrqneralf")))
          (SeqTree (FP fx (Hunk 14 [] (packStringLetters "yairbjphwtnaerccdlfewujvjvmjakbc")))
           (SeqTree (FP fx (Hunk 50 [] (packStringLetters "xayvfuwaiiogginufnhsrmktpmlbvxiakjwllddkiyofyfw")))
            (ParTree
             NilTree
             NilTree)))))))))]

fx :: FileName
fx = fp2fn "./F"

\end{code}