src/Darcs/Patch/QuickCheck.lhs

   1 \begin{code}
   2
   3 {-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts -fallow-undecidable-instances #-}
   4 {-# LANGUAGE CPP, UndecidableInstances, ScopedTypeVariables #-}
   5
   6 #include "gadts.h"
   7 module Darcs.Patch.QuickCheck ( WithStartState, RepoModel, Tree,
   8 #ifndef GADT_WITNESSES
   9                                 merge_examples, commute_examples, triple_examples,
  10 #endif
  11                                 prop_consistent_tree_flattenings, prop_fail,
  12                                 prop_is_mergeable,
  13                                 flattenOne, simpleCheck, simpleConditionalCheck, thoroughCheck,
  14                                 commutePairFromTree, mergePairFromTree,
  15                                 commuteTripleFromTree,
  16                                 commutePairFromTWFP, mergePairFromTWFP, getPairs, getTriples,
  17                                 patchFromTree,
  18                                 quickCheck, real_patch_loop_examples, shrink
  19                               ) where
  20
  21 import Control.Arrow ( (***) )
  22 import Control.Monad ( liftM, replicateM, mplus, mzero )
  23 import qualified Data.ByteString.Char8 as BC (pack)
  24 import qualified Data.ByteString       as B  (ByteString)
  25 import Test.QuickCheck
  26 import Darcs.Sealed
  27 import Darcs.Patch ( Patch )
  28 import Darcs.Ordered
  29 import Darcs.Patch.Patchy (--showPatch,
  30                            Invert(..), Commute(..))
  31 import Darcs.Patch.Prim (Prim(..), Effect(..), FilePatchType(..), FromPrim(..), is_identity )
  32 import Darcs.Patch.Real ( RealPatch, prim2real )
  33 --import Darcs.ColorPrinter ( errorDoc )
  34 --import Darcs.ColorPrinter ( traceDoc )
  35 import Darcs.Show
  36 --import Printer ( greenText, ($$) )
  37 import Darcs.Patch.FileName ( FileName, fp2fn )
  38
  39 #include "impossible.h"
  40
  41
  42 #ifndef GADT_WITNESSES
  43 instance Eq (a C(x y)) => Eq (Sealed2 a) where
  44     (Sealed2 x) == (Sealed2 y) = x == y
  45 #endif
  46
  47 instance Show2 Patch where
  48     show2 = show
  49
  50 #ifndef GADT_WITNESSES
  51 triple_examples :: (FromPrim p, Commute p, Invert p) => [p :> p :> p]
  52 triple_examples = [commuteTripleFromTree id $
  53                    WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
  54                    (ParTree
  55                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "g"]))
  56                      (SeqTree (FP (fp2fn "./file") (Hunk 1 [] [BC.pack "j"]))
  57                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "s"])) NilTree)))
  58                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "e"])) NilTree))
  59                   ,commuteTripleFromTree id $
  60                    WithStartState (RepoModel { rmFileName = fp2fn "./file",
  61                                                rmFileContents = [BC.pack "j"] })
  62                    (ParTree
  63                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "s"]))
  64                      (ParTree
  65                       (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "j"] [])) NilTree)
  66                       (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "j"] [])) NilTree)))
  67                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "j"] [])) NilTree))
  68                   ]
  69
  70
  71 merge_examples :: (FromPrim p, Commute p, Invert p) => [p :\/: p]
  72 merge_examples = map (mergePairFromCommutePair id) commute_examples
  73
  74 commute_examples :: (FromPrim p, Commute p) => [p :> p]
  75 commute_examples = [
  76                    commutePairFromTWFP id $
  77                    WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
  78                    (TWFP 3
  79                     (ParTree
  80                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "h"])) NilTree)
  81                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "b"]))
  82                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "f"]))
  83                          (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "v"]))
  84                            (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "f"] [])) NilTree)))))),
  85                    commutePairFromTWFP id $
  86                    WithStartState
  87                    (RepoModel { rmFileName = fp2fn "./file",
  88                                 rmFileContents = [BC.pack "f",BC.pack "s",BC.pack "d"] })
  89                    (TWFP 3
  90                     (ParTree
  91                      (SeqTree (FP (fp2fn "./file") (Hunk 2 [BC.pack "d"] [])) NilTree)
  92                      (ParTree
  93                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "f"] [])) NilTree)
  94                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "f"] []))
  95                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "s",BC.pack "d"] []))
  96                           (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "v"])) NilTree)))))),
  97 {-                   commutePairFromTWFP id $
  98                    WithStartState
  99                    (RepoModel { rmFileName = fp2fn "./file",
 100                                 rmFileContents = [BC.pack "f",BC.pack "u",
 101                                                   BC.pack "s",BC.pack "d"] })
 102                    (TWFP 5
 103                     (ParTree
 104                      (SeqTree (FP (fp2fn "./file") (Hunk 4 [] [BC.pack "x"]))
 105                       (SeqTree (FP (fp2fn "./file") (Hunk 3 [BC.pack "d"] [])) NilTree))
 106                      (ParTree
 107                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "f",BC.pack "u"] [])) NilTree)
 108                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "f"] []))
 109                        (SeqTree (FP(fp2fn "./file") (Hunk 0 [BC.pack "u",BC.pack "s",BC.pack "d"] []))
 110                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "a"]))
 111                          (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "a"] [])) NilTree))))))),-}
 112                    commutePairFromTree id $
 113                    WithStartState (RepoModel { rmFileName = fp2fn "./file",
 114                                           rmFileContents = [BC.pack "n",BC.pack "t",BC.pack "h"] })
 115                    (ParTree
 116                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "n",BC.pack "t",BC.pack "h"] []))
 117                      NilTree)
 118                     (SeqTree (FP (fp2fn "./file") (Hunk 2 [BC.pack "h"] []))
 119                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "n"] []))
 120                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "t"] [])) NilTree)))),
 121                   commutePairFromTree id $
 122                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 123                   (ParTree
 124                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "n"])) NilTree)
 125                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "i"]))
 126                                 (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "i"])) NilTree))),
 127                   commutePairFromTree id $
 128                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 129                   (ParTree
 130                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "c"]))
 131                      (ParTree
 132                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "c"] [BC.pack "r"])) NilTree)
 133                        (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "h"]))
 134                         (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "d"])) NilTree))))
 135                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "f"])) NilTree)),
 136                   commutePairFromTWFP id $
 137                   WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 138                   (TWFP 1
 139                   (ParTree
 140                    (ParTree
 141                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "t"])) NilTree)
 142                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "t"])) NilTree))
 143                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "f"])) NilTree))),
 144                    commutePairFromTWFP id $
 145                    WithStartState (RepoModel { rmFileName = fp2fn "./file",
 146                                                rmFileContents = [BC.pack "f",BC.pack " r",
 147                                                                  BC.pack "c",BC.pack "v"] })
 148                    (TWFP 4
 149                     (ParTree
 150                      (SeqTree (FP (fp2fn "./file") (Hunk 2 [BC.pack "c",BC.pack "v"] []))
 151                         (ParTree
 152                          (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "r"] []))
 153                           (SeqTree (FP (fp2fn "fi le") (Hunk 0 [BC.pack "f"] [])) NilTree))
 154                          (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "f",BC.pack "r"] []))
 155                           (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "y"])) NilTree))))
 156                      (SeqTree (FP (fp2fn "./file") (Hunk 3 [BC.pack "v"] [])) NilTree))),
 157                    commutePairFromTree id $
 158                    WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 159                    (ParTree
 160                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "z"])) NilTree)
 161                     (ParTree
 162                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "f"])) NilTree)
 163                      (ParTree
 164                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "r"])) NilTree)
 165                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "d"])) NilTree))))
 166                  , commutePairFromTree id $
 167                    WithStartState (RepoModel { rmFileName = fp2fn "./file",
 168                                                rmFileContents = [BC.pack "t",BC.pack "r",
 169                                                                  BC.pack "h"] })
 170                    (ParTree
 171                     (ParTree
 172                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "t",BC.pack "r",BC.pack "h"] []))
 173                               NilTree)
 174                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "o"])) NilTree))
 175                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "t"] []))
 176                      (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "h"] [])) NilTree)))
 177                  , commutePairFromTWFP id $
 178                    WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] }) $
 179                    TWFP 2
 180                    (ParTree
 181                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "h"])) NilTree)
 182                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "y"]))
 183                      (SeqTree (FP (fp2fn "./file") (Hunk 1 [] [BC.pack "m"]))
 184                       (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "v"])) NilTree))))
 185                  , commutePairFromTree id $
 186                  WithStartState (RepoModel {rmFileName = fp2fn "./file",rmFileContents = [] })
 187                  (ParTree
 188                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "p"]))
 189                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "p"] []))
 190                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "c"])) NilTree)))
 191                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "z"])) NilTree))
 192                  , commutePairFromTree id $
 193                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 194                  (ParTree
 195                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "j" ]))
 196                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "j"] [])) NilTree))
 197                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "v"])) NilTree))
 198                  , commutePairFromTree id $
 199                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 200                  (ParTree
 201                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "v"])) NilTree)
 202                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "j" ]))
 203                    (SeqTree (FP (fp2fn "./file") (Hunk 0 [BC.pack "j"] [])) NilTree)))
 204                  , commutePairFromTree id $
 205                  WithStartState (RepoModel { rmFileName = fp2fn "./file",
 206                                              rmFileContents = [BC.pack "x",BC.pack "c"] })
 207                  (ParTree
 208                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "h"]))
 209                    (ParTree
 210                     (SeqTree (FP (fp2fn "./file") (Hunk 2 [BC.pack "c"] [])) NilTree)
 211                     (SeqTree (FP (fp2fn "./file") (Hunk 1 [BC.pack "x"] []))
 212                      (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "j"])) NilTree))))
 213                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] [BC.pack "l"])) NilTree))
 214                  , commutePairFromTree id $
 215                  WithStartState (RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] })
 216                  (ParTree
 217                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "s"))) NilTree)
 218                   (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "k")))
 219                    (SeqTree (FP (fp2fn "./file") (Hunk 0 (packStringLetters "k") []))
 220                     (SeqTree (FP (fp2fn "./file") (Hunk 0 [] (packStringLetters "m")))
 221                      (SeqTree (FP (fp2fn "./file") (Hunk 0 (packStringLetters "m") [])) NilTree)))))
 222                  ]
 223 #endif
 224
 225 simpleConditionalCheck :: (Arbitrary p, Show p, Show q) => (p -> Bool) -> (p -> Maybe q) -> IO Int
 226 simpleConditionalCheck nottrivial t = do okay <- quickCheckWith maxSuccessTests maxTryTests maxSize t'
 227                                          return $ if okay then 0 else 1
 228     where t' p = nottrivial p ==> case t p of
 229                                   Nothing -> True
 230                                   Just q -> error $ show q
 231           maxSuccessTests = 100
 232           maxTryTests     = 50 * maxSuccessTests
 233           maxSize         = 100
 234
 235 simpleCheck :: (Arbitrary p, Show p, Show q) => (p -> Maybe q) -> IO Int
 236 simpleCheck t = do okay <- quickCheck' t'
 237                    return $ if okay then 0 else 1
 238     where t' p = case t p of
 239                  Nothing -> True
 240                  Just q -> error $ show q
 241
 242 thoroughCheck :: (Arbitrary p, Show p, Show q) => Int -> (p -> Maybe q) -> IO Int
 243 thoroughCheck num t = do let ntries = 20*num
 244                              maxsize = max 100 (num `div` 10)
 245                          okay <- quickCheckWith num ntries maxsize t'
 246                          return $ if okay then 0 else 1
 247     where t' p = case t p of
 248                  Nothing -> True
 249                  Just q -> error $ show q
 250
 251 data RepoModel C(x)
 252  = RepoModel {
 253      rmFileName :: !FileName,
 254      rmFileContents :: [B.ByteString]
 255    } deriving (Eq)
 256
 257 instance Show (RepoModel C(x)) where
 258   showsPrec d rm = showParen (d > app_prec) $
 259                    showString "RepoModel { rmFileName = " . showsPrec 0 (rmFileName rm) .
 260                    showString ", rmFileContents = " . showsPrec 0 (rmFileContents rm) .
 261                    showString " }"
 262
 263 instance Show1 RepoModel where
 264     showsPrec1 = showsPrec
 265
 266 #ifdef GADT_WITNESSES
 267 data InitRepoModel -- this ought to be defined somewhere central as the unique starting state
 268 #endif
 269
 270 initRepoModel :: RepoModel C(InitRepoModel)
 271 initRepoModel = RepoModel { rmFileName = fp2fn "./file", rmFileContents = [] }
 272 rebuildRepoModel :: RepoModel C(x) -> RepoModel C(y)
 273 rebuildRepoModel rm = RepoModel { rmFileName = rmFileName rm, rmFileContents = rmFileContents rm }
 274
 275 data WithEndState px s C(y) = WithEndState { wesPatch :: px C(y), _wesState :: s C(y) }
 276
 277 class ArbitraryState s p where
 278   arbitraryState :: s C(x) -> Gen (Sealed (WithEndState (p C(x)) s))
 279   -- does a coarbitrary make sense?
 280
 281 class ArbitraryStateIn s p where
 282   arbitraryStateIn :: s C(x) -> Gen (p C(x))
 283
 284 instance ArbitraryState RepoModel Prim where
 285   arbitraryState rm = oneof [arbitraryFP rm]
 286
 287 instance Arbitrary (Sealed2 (FL Prim)) where
 288   arbitrary = do Sealed2 ps1 <- liftM (unseal (seal2 . wesPatch)) $ arbitraryState initRepoModel
 289                  return $ Sealed2 $ mapFL_FL make_identity_identity ps1
 290                      where make_identity_identity :: Prim C(x y) -> Prim C(x y)
 291                            make_identity_identity p | IsEq <- is_identity p = identity
 292                                                     | otherwise = p
 293
 294 instance Arbitrary (Sealed2 (FL (WithState RepoModel Prim))) where
 295   arbitrary = liftM (unseal (seal2 . wesPatch)) $ arbitraryState initRepoModel
 296
 297 prop_consistent_tree_flattenings :: Sealed (WithStartState RepoModel (Tree Prim)) -> Bool
 298 prop_consistent_tree_flattenings (Sealed (WithStartState start t))
 299   = fromJust $
 300     do Sealed (G2 flat) <- return $ flattenTree $ mapTree prim2real t
 301        rms <- return $ map (applyPatch start) flat
 302        return $ and $ zipWith assert_equal_fst (zip rms flat) (tail $ zip rms flat)
 303
 304 assert_equal_fst :: (Eq a, Show a, Show b, Show c) => (a, b) -> (a, c) -> Bool
 305 assert_equal_fst (x,bx) (y,by)
 306     | x == y = True
 307     | otherwise = error ("Not really equal:\n" ++ show x ++ "\nand\n" ++ show y
 308                          ++ "\ncoming from\n" ++ show bx ++ "\nand\n" ++ show by)
 309
 310 -- WithState and prop_fail are handy for debugging arbitrary code
 311 data WithState s p C(x y) = WithState (s C(x)) (p C(x y)) (s C(y))
 312   deriving Show
 313
 314 data WithStartState s p C(x) = WithStartState (s C(x)) (p C(x))
 315
 316 instance (Show1 s, Show1 p) => Show (WithStartState s p C(x)) where
 317    showsPrec d (WithStartState s p) = showParen (d > app_prec) $ showString "WithStartState " .
 318                                       showsPrec1 (app_prec + 1) s . showString " " .
 319                                       showsPrec1 (app_prec + 1) p
 320
 321 instance (Show1 s, Show1 p) => Show1 (WithStartState s p) where
 322    showsPrec1 = showsPrec
 323
 324 prop_fail :: Int -> Tree Prim C(x) -> Bool
 325 prop_fail n xs = sizeTree xs < n
 326
 327 instance ArbitraryState s p => ArbitraryState s (WithState s p) where
 328   arbitraryState rm = do xandrm' <- arbitraryState rm
 329                          flip unseal xandrm' $ \(WithEndState x rm') ->
 330                            return $ seal $ WithEndState (WithState rm x rm') rm'
 331
 332 instance ArbitraryState s p => ArbitraryState s (FL p) where
 333   arbitraryState rm1 = sized $ \n -> do k <- choose (0, n)
 334                                         arbitraryList k rm1
 335       where arbitraryList :: FORALL(x) Int -> s C(x) -> Gen (Sealed (WithEndState (FL p C(x)) s))
 336             arbitraryList 0 rm = return $ seal $ WithEndState NilFL rm
 337             arbitraryList (n+1) rm = do Sealed (WithEndState x rm') <- arbitraryState rm
 338                                         Sealed (WithEndState xs rm'') <- arbitraryList n rm'
 339                                         return $ seal $ WithEndState (x :>: xs) rm''
 340             arbitraryList _ _ = impossible
 341
 342 data Tree p C(x) where
 343    NilTree :: Tree p C(x)
 344    SeqTree :: p C(x y) -> Tree p C(y) -> Tree p C(x)
 345    ParTree :: Tree p C(x) -> Tree p C(x) -> Tree p C(x)
 346
 347 mapTree :: (FORALL(y z) p C(y z) -> q C(y z)) -> Tree p C(x) -> Tree q C(x)
 348 mapTree _ NilTree = NilTree
 349 mapTree f (SeqTree p t) = SeqTree (f p) (mapTree f t)
 350 mapTree f (ParTree t1 t2) = ParTree (mapTree f t1) (mapTree f t2)
 351
 352 instance Show2 p => Show (Tree p C(x)) where
 353    showsPrec _ NilTree = showString "NilTree"
 354    showsPrec d (SeqTree a t) = showParen (d > app_prec) $ showString "SeqTree " .
 355                                showsPrec2 (app_prec + 1) a . showString " " .
 356                                showsPrec (app_prec + 1) t
 357    showsPrec d (ParTree t1 t2) = showParen (d > app_prec) $ showString "ParTree " .
 358                                  showsPrec (app_prec + 1) t1 . showString " " .
 359                                  showsPrec (app_prec + 1) t2
 360
 361 instance Show2 p => Show1 (Tree p) where
 362     showsPrec1 = showsPrec
 363
 364 sizeTree :: Tree p C(x) -> Int
 365 sizeTree NilTree = 0
 366 sizeTree (SeqTree _ t) = 1 + sizeTree t
 367 sizeTree (ParTree t1 t2) = 1 + sizeTree t1 + sizeTree t2
 368
 369 -- newtype G1 l p C(x) = G1 { _unG1 :: l (p C(x)) }
 370 newtype G2 l p C(x y) = G2 { unG2 :: l (p C(x y)) }
 371
 372 flattenTree :: (Commute p) => Tree p C(z) -> Sealed (G2 [] (FL p) C(z))
 373 flattenTree NilTree = seal $ G2 $ return NilFL
 374 flattenTree (SeqTree p t) = mapSeal (G2 . map (p :>:) . unG2) $ flattenTree t
 375 flattenTree (ParTree t1 t2) = flip unseal (flattenTree t1) $ \gpss1 ->
 376                               flip unseal (flattenTree t2) $ \gpss2 ->
 377                               seal $ G2 $
 378                               do ps1 <- unG2 gpss1
 379                                  ps2 <- unG2 gpss2
 380                                  ps2' :/\: ps1' <- return $ merge (ps1 :\/: ps2)
 381                                  -- We can't prove that the existential type in the result
 382                                  -- of merge will be the same for each pair of
 383                                  -- ps1 and ps2.
 384                                  map unsafeCoerceP [ps1 +>+ ps2', ps2 +>+ ps1']
 385
 386 instance ArbitraryState s p => ArbitraryStateIn s (Tree p) where
 387   arbitraryStateIn rm = frequency [(2, return NilTree)
 388                                   ,(2, do Sealed (WithEndState p rm') <- arbitraryState rm
 389                                           t <- arbitraryStateIn rm'
 390                                           return (SeqTree p t))
 391                                   ,(1, do t1 <- arbitraryStateIn rm
 392                                           t2 <- arbitraryStateIn rm
 393                                           return (ParTree t1 t2))]
 394
 395
 396 shrinkWSSTree :: Sealed (WithStartState RepoModel (Tree Prim))
 397               -> [Sealed (WithStartState RepoModel (Tree Prim))]
 398 shrinkWSSTree = unseal doShrinkWSSTree
 399  where
 400  doShrinkWSSTree wss@(WithStartState rm t)
 401   = shrinkWSSTree' wss -- shrink the tree
 402      `mplus`
 403     do -- shrink the starting context
 404       pos <- [0 .. length (rmFileContents rm) - 1]
 405       let rmFileContents' = take pos (rmFileContents rm) ++ drop (pos+1) (rmFileContents rm)
 406           t' = shrinkPosStart pos (canonizeTree t)
 407       return $ seal $ WithStartState (rm { rmFileContents = rmFileContents' }) (canonizeTree t')
 408
 409
 410 -- If we had a more general repo model, then Int would need to be more general too
 411
 412 class ShrinkablePos p where
 413   shrinkPos :: Int -> p C(x y) -> (p C(x y), Maybe Int)
 414   shrinkPatch :: p C(x y) -> [(p C(x y), Maybe Int)]
 415   nullPatch :: p C(x y) -> EqCheck C(x y)
 416
 417 class ShrinkablePosStart p where
 418   shrinkPosStart :: Int -> p C(x) -> p C(x)
 419
 420 instance ShrinkablePos p => ShrinkablePosStart (Tree p) where
 421   shrinkPosStart _ NilTree = NilTree
 422   shrinkPosStart pos (SeqTree p t)
 423     = let (p', mpos') = shrinkPos pos p
 424       in case mpos' of
 425            Nothing -> SeqTree p' t
 426            Just pos' -> SeqTree p' (shrinkPosStart pos' t)
 427   shrinkPosStart pos (ParTree t1 t2) = ParTree (shrinkPosStart pos t1) (shrinkPosStart pos t2)
 428
 429 smartFP :: FileName -> FilePatchType C(x y) -> Prim C(x y)
 430 smartFP _ (Hunk _ [] []) | avoidEmptyHunks = unsafeCoerceP Identity
 431 smartFP fn filepatch = FP fn filepatch
 432
 433 instance ShrinkablePos Prim where
 434   shrinkPos pos (FP fn fp) = (smartFP fn *** id) (shrinkPos pos fp)
 435   shrinkPos pos Identity = (Identity, Just pos)
 436   shrinkPos _ _ = impossible
 437   shrinkPatch (FP fn fp) = map (smartFP fn *** id) (shrinkPatch fp)
 438   shrinkPatch Identity = []
 439   shrinkPatch _ = impossible
 440   nullPatch (FP _ fp) = nullPatch fp
 441   nullPatch Identity = IsEq
 442   nullPatch _ = impossible
 443
 444 avoidEmptyHunks :: Bool
 445 avoidEmptyHunks = True
 446
 447 instance ShrinkablePos FilePatchType where
 448   shrinkPos pos (Hunk n old new)
 449     | pos < n = (Hunk (n-1) old new, Just pos)
 450     | pos >= n + length old = (Hunk n old new, Just (pos + length new - length old))
 451     | otherwise = (Hunk n (take pos' old ++ drop (pos'+1) old) new, Nothing)
 452         where pos' = pos - n
 453   shrinkPos _ _ = bug "foo1 in ShrinkablePos"
 454   shrinkPatch (Hunk (n+1) [] []) = [(Hunk n [] [], Nothing)]
 455   shrinkPatch (Hunk n old new)
 456    = do i <- [0 .. length new - 1]
 457         return (Hunk n old (take i new ++ drop (i+1) new), Just (n + i))
 458   shrinkPatch _ = bug "foo in ShrinkablePos"
 459   nullPatch (Hunk _ [] []) = unsafeCoerceP IsEq -- is this safe?
 460   nullPatch _ = NotEq
 461
 462 shrinkWSSTree'
 463  -- start a new line here because apparently ' confuses CPP..
 464    :: WithStartState RepoModel (Tree Prim) C(x)
 465    -> [Sealed (WithStartState RepoModel (Tree Prim))]
 466 shrinkWSSTree' (WithStartState _ NilTree) = []
 467 shrinkWSSTree' (WithStartState rm t@(SeqTree p t'))
 468   = return (seal (WithStartState (applyPatch rm p) (canonizeTree t')))
 469      `mplus`
 470     liftM (seal . WithStartState rm) (map canonizeTree $ shrinkTree t)
 471 shrinkWSSTree' (WithStartState rm t@(ParTree _ _))
 472   = liftM (seal . WithStartState rm) (map canonizeTree $ shrinkTree t)
 473
 474 -- canonize a tree, removing any dead branches
 475 canonizeTree :: ShrinkablePos p => Tree p C(x) -> Tree p C(x)
 476 canonizeTree NilTree = NilTree
 477 canonizeTree (ParTree t1 t2)
 478     | NilTree <- canonizeTree t1 = canonizeTree t2
 479     | NilTree <- canonizeTree t2 = canonizeTree t1
 480     | otherwise = ParTree (canonizeTree t1) (canonizeTree t2)
 481 canonizeTree (SeqTree p t) | IsEq <- nullPatch p = canonizeTree t
 482                            | otherwise = SeqTree p (canonizeTree t)
 483
 484 -- shrink the tree without changing the starting context
 485 shrinkTree :: ShrinkablePos p => Tree p C(x) -> [Tree p C(x)]
 486 shrinkTree NilTree = []
 487 shrinkTree (SeqTree p t) = do case nullPatch p of
 488                                  IsEq -> return t
 489                                  NotEq -> mzero
 490                              `mplus`
 491                            do (p', pos) <- shrinkPatch p
 492                               return (SeqTree p' (maybe id shrinkPosStart pos t))
 493                              `mplus`
 494                            do t' <- shrinkTree t
 495                               return (SeqTree p t')
 496 shrinkTree (ParTree t1 t2) = [t1, t2]
 497                               `mplus`
 498                              do t1' <- shrinkTree t1
 499                                 return (ParTree t1' t2)
 500                               `mplus`
 501                              do t2' <- shrinkTree t2
 502                                 return (ParTree t1 t2')
 503
 504 instance Arbitrary (Sealed (WithStartState RepoModel (Tree Prim))) where
 505   arbitrary = do Sealed (WithStartState rm tree) <-
 506                      liftM (seal . WithStartState initRepoModel) (arbitraryStateIn initRepoModel)
 507                  return $ Sealed $ WithStartState rm (canonizeTree tree)
 508   shrink = shrinkWSSTree
 509
 510 prop_is_mergeable :: forall p C(x) . (FromPrim p, Commute p)
 511                   => Sealed (WithStartState RepoModel (Tree Prim))
 512                   -> Maybe (Tree p C(x))
 513 prop_is_mergeable (Sealed (WithStartState _ t))
 514    = case flattenOne t of
 515         Sealed ps -> let _ = seal2 ps :: Sealed2 (FL p)
 516                      in case lengthFL ps of
 517                        _ -> Nothing
 518
 519 flattenOne :: (FromPrim p, Commute p) => Tree Prim C(x) -> Sealed (FL p C(x))
 520 flattenOne NilTree = seal NilFL
 521 flattenOne (SeqTree p t) = flip unseal (flattenOne t) $ \ps -> seal (fromPrim p :>: ps)
 522 flattenOne (ParTree t1 t2) =
 523     flip unseal (flattenOne t1) $ \ps1 ->
 524     flip unseal (flattenOne t2) $ \ps2 ->
 525     --traceDoc (greenText "flattening two parallel series: ps1" $$ showPatch ps1 $$
 526     --          greenText "ps2" $$ showPatch ps2) $
 527     case merge (ps1 :\/: ps2) of
 528       ps2' :/\: _ -> seal (ps1 +>+ ps2')
 529
 530 instance Arbitrary (Sealed2 (FL RealPatch)) where
 531     arbitrary = do Sealed (WithStartState _ tree) <- arbitrary :: Gen (Sealed (WithStartState RepoModel (Tree Prim)))
 532                    return $ unseal seal2 (flattenOne tree)
 533
 534 instance Arbitrary (Sealed2 RealPatch) where
 535     arbitrary = do Sealed (WithStartState _ tree) <- arbitrary :: Gen (Sealed (WithStartState RepoModel (Tree Prim)))
 536                    case mapFL seal2 `unseal` flattenOne tree of
 537                      [] -> return $ seal2 $ fromPrim Identity
 538                      ps -> elements ps
 539
 540 instance (Arbitrary (Sealed2 (FL p)), Commute p) => Arbitrary (Sealed2 (p :\/: p)) where
 541     arbitrary = do Sealed2 (a :> b) <- arbitrary
 542                    case commute (a :> b) of
 543                      Just (b' :> _) -> return (seal2 (a :\/: b'))
 544                      Nothing -> arbitrary
 545
 546 instance Arbitrary (Sealed2 (FL p)) => Arbitrary (Sealed2 (p :> p)) where
 547     arbitrary = do Sealed2 ps <- arbitrary
 548                    let pairs = getPairs ps
 549                    case pairs of
 550                       [] -> arbitrary
 551                       _ -> elements pairs
 552
 553 instance (Invert p, Arbitrary (Sealed2 (FL p))) => Arbitrary (Sealed2 (p :> p :> p)) where
 554     arbitrary = do Sealed2 ps <- arbitrary
 555                    return $ last_triple ps
 556         where last_triple :: FL p C(x y) -> Sealed2 (p :> p :> p)
 557               last_triple NilFL = seal2 $ identity :> identity :> identity
 558               last_triple (a :>: NilFL) = seal2 $ a :> invert a :> identity
 559               last_triple (a :>: b :>: NilFL) = seal2 $ invert a :> a :> b
 560               last_triple (a :>: b :>: c :>: NilFL) = seal2 $ a :> b :> c
 561               last_triple (_ :>: xs) = last_triple xs
 562
 563 data TreeWithFlattenPos p C(x) = TWFP Int (Tree p C(x))
 564
 565 commutePairFromTWFP :: (FromPrim p, Commute p)
 566                     => (FORALL (y z) (p :> p) C(y z) -> t)
 567                     -> (WithStartState RepoModel (TreeWithFlattenPos Prim) C(x) -> t)
 568 commutePairFromTWFP handlePair (WithStartState _ (TWFP n t))
 569     = unseal2 handlePair $
 570       let xs = unseal getPairs (flattenOne t)
 571       in if length xs > n && n >= 0 then xs!!n else seal2 (fromPrim Identity :> fromPrim Identity)
 572
 573 commutePairFromTree :: (FromPrim p, Commute p)
 574                     => (FORALL (y z) (p :> p) C(y z) -> t)
 575                     -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
 576 commutePairFromTree handlePair (WithStartState _ t)
 577    = unseal2 handlePair $
 578      let Sealed ps = flattenOne t
 579          xs = --traceDoc (greenText "I'm flattening one to get:" $$ showPatch ps) $
 580               getPairs ps
 581      in if null xs then seal2 (fromPrim Identity :> fromPrim Identity) else last xs
 582
 583 commuteTripleFromTree :: (FromPrim p, Commute p)
 584                       => (FORALL (y z) (p :> p :> p) C(y z) -> t)
 585                       -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
 586 commuteTripleFromTree handle (WithStartState _ t)
 587    = unseal2 handle $
 588      let Sealed ps = flattenOne t
 589          xs = --traceDoc (greenText "I'm flattening one to get:" $$ showPatch ps) $
 590               getTriples ps
 591      in if null xs
 592         then seal2 (fromPrim Identity :> fromPrim Identity :> fromPrim Identity)
 593         else last xs
 594
 595 mergePairFromCommutePair :: (Commute p, Invert p)
 596                          => (FORALL (y z) (p :\/: p) C(y z) -> t)
 597                          -> (FORALL (y z) (p :>   p) C(y z) -> t)
 598 mergePairFromCommutePair handlePair (a :> b)
 599  = case commute (a :> b) of
 600      Just (b' :> _) -> handlePair (a :\/: b')
 601      Nothing -> handlePair (b :\/: b)
 602
 603 -- impredicativity problems mean we can't use (.) in the definitions below
 604
 605 mergePairFromTWFP :: (FromPrim p, Commute p, Invert p)
 606                   => (FORALL (y z) (p :\/: p) C(y z) -> t)
 607                   -> (WithStartState RepoModel (TreeWithFlattenPos Prim) C(x) -> t)
 608 mergePairFromTWFP x = commutePairFromTWFP (mergePairFromCommutePair x)
 609
 610 mergePairFromTree :: (FromPrim p, Commute p, Invert p)
 611                   => (FORALL (y z) (p :\/: p) C(y z) -> t)
 612                   -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
 613 mergePairFromTree x = commutePairFromTree (mergePairFromCommutePair x)
 614
 615 patchFromCommutePair :: (Commute p, Invert p)
 616                      => (FORALL (y z) p C(y z) -> t)
 617                      -> (FORALL (y z) (p :> p) C(y z) -> t)
 618 patchFromCommutePair handle (_ :> b) = handle b
 619
 620 patchFromTree :: (FromPrim p, Commute p, Invert p)
 621               => (FORALL (y z) p C(y z) -> t)
 622               -> (WithStartState RepoModel (Tree Prim) C(x) -> t)
 623 patchFromTree x = commutePairFromTree (patchFromCommutePair x)
 624
 625
 626 instance Show2 p => Show (TreeWithFlattenPos p C(x)) where
 627    showsPrec d (TWFP n t) = showParen (d > app_prec) $ showString "TWFP " .
 628                             showsPrec (app_prec + 1) n . showString " " .
 629                             showsPrec1 (app_prec + 1) t
 630
 631 instance Show1 (TreeWithFlattenPos Prim) where
 632    show1 = show
 633
 634 instance Arbitrary (Sealed (WithStartState RepoModel (TreeWithFlattenPos Prim))) where
 635    arbitrary = do Sealed (WithStartState rm t) <- arbitrary
 636                   let num = unseal (length . getPairs) (flattenOneRP t)
 637                   if num == 0 then return $ Sealed $ WithStartState rm $ TWFP 0 NilTree
 638                     else do n <- choose (0, num - 1)
 639                             return $ Sealed $ WithStartState rm $ TWFP n t
 640                     where -- just used to get the length. In principle this should be independent of the patch type.
 641                           flattenOneRP :: Tree Prim C(x) -> Sealed (FL RealPatch C(x))
 642                           flattenOneRP = flattenOne
 643    shrink (Sealed (WithStartState rm (TWFP n t))) =
 644       [Sealed (WithStartState rm' (TWFP n' t')) | Sealed (WithStartState rm' t') <- shrink (Sealed (WithStartState rm t)),
 645                                                   n' <- [0..n]]
 646
 647
 648 getPairs :: FL p C(x y) -> [Sealed2 (p :> p)]
 649 getPairs NilFL = []
 650 getPairs (_:>:NilFL) = []
 651 getPairs (a:>:b:>:c) = seal2 (a:>b) : getPairs (b:>:c)
 652
 653 getTriples :: FL p C(x y) -> [Sealed2 (p :> p :> p)]
 654 getTriples NilFL = []
 655 getTriples (_:>:NilFL) = []
 656 getTriples (_:>:_:>:NilFL) = []
 657 getTriples (a:>:b:>:c:>:d) = seal2 (a:>b:>c) : getTriples (b:>:c:>:d)
 658
 659 arbitraryFP :: RepoModel C(x) -> Gen (Sealed (WithEndState (Prim C(x)) RepoModel))
 660 arbitraryFP rm
 661  = do (fp, newcontents) <- arbitraryFilePatchType (rmFileContents rm)
 662       return $ seal $ WithEndState (FP (rmFileName rm) fp) (rebuildRepoModel (rm { rmFileContents = newcontents }))
 663
 664 -- Really [B.ByteString] should be parametrised by x y, and the result tuple sealed on y
 665 arbitraryFilePatchType :: [B.ByteString] -> Gen (FilePatchType C(x y), [B.ByteString])
 666 arbitraryFilePatchType contents = oneof [arbitraryHunk contents]
 667
 668 arbitraryHunk :: [B.ByteString] -> Gen (FilePatchType C(x y), [B.ByteString])
 669 arbitraryHunk contents
 670  = sized $ \n ->
 671    do start <- choose (0, min n (length contents))
 672       (removelen, _)
 673         <- frequency $ zip (if start == length contents then [1, 13, 0, 0] else [1, 3, 5, 3])
 674                 [return (0, 0)
 675                 ,do xa <- choose (0, n)
 676                     return (0, xa)
 677                 ,do xr <- choose (1, min n (length contents - start))
 678                     return (xr, 0)
 679                 ,do xr <- choose (1, min n (length contents - start))
 680                     xa <- choose (0, n)
 681                     return (xr, xa)
 682                 ]
 683       addlen <- choose (0, n)
 684       additems <- replicateM addlen (do c <- choose ('a', 'z')
 685                                         return $ BC.pack [c])
 686       let newcontents = take start contents ++ additems ++ drop (start + removelen) contents
 687       return (Hunk start (take removelen $ drop start $ contents) additems, newcontents)
 688
 689 class Applyable p where
 690   applyPatch :: RepoModel C(x) -> p C(x y) -> RepoModel C(y)
 691
 692 instance Applyable p => Applyable (FL p) where
 693   applyPatch rm NilFL = rm
 694   applyPatch rm (p :>: ps) = applyPatch (applyPatch rm p) ps
 695
 696 instance Applyable RealPatch where
 697   applyPatch rm p = applyPatch rm (effect p)
 698
 699 instance Applyable Prim where
 700   applyPatch (rm@RepoModel { rmFileName = filename, rmFileContents = oldcontents }) (FP filename' fp)
 701      | filename == filename' = rebuildRepoModel (rm { rmFileContents = applyFilePatchType oldcontents fp })
 702   applyPatch rm Identity = rm
 703   applyPatch _ _ = bug "We haven't defined applyPatch on Prim for all patch types."
 704
 705 applyFilePatchType :: [B.ByteString] -> FilePatchType C(x y) -> [B.ByteString]
 706 applyFilePatchType oldcontents (Hunk n old new)
 707  = if take (length old) (drop n oldcontents) == old
 708    then take n oldcontents ++ new ++ drop (n + length old) oldcontents
 709    else error "Bad patch context"
 710 applyFilePatchType _ _ = bug "We haven't defined applyFilePatchType for all patch types."
 711
 712 packStringLetters :: String -> [B.ByteString]
 713 packStringLetters = map (BC.pack . (:[]))
 714
 715 real_patch_loop_examples :: [Sealed (WithStartState RepoModel (Tree Prim))]
 716 real_patch_loop_examples =
 717     [Sealed (WithStartState (RepoModel { rmFileName = fx, rmFileContents = [] })
 718      $ canonizeTree
 719      (ParTree
 720       (SeqTree (FP fx (Hunk 0 [] (packStringLetters "pkotufogbvdabnmbzajvolwviqebieonxvcvuvigkfgybmqhzuaaurjspd")))
 721        (ParTree
 722         (SeqTree (FP fx (Hunk 46 (packStringLetters "qhzu") (packStringLetters "zafybdcokyjskcgnvhkbzpysaafnjjhcstgrczplxsfwagmh")))
 723          (ParTree
 724           (ParTree
 725            NilTree
 726            (ParTree
 727             (ParTree
 728              (ParTree
 729               (SeqTree (FP fx (Hunk 14 (packStringLetters "mbzajvolwviqebieonxvcvuvigkfgyb") (packStringLetters "vujnxnhvybvpouyciaabszfmgssezlwwjgnethvrpnfrkubphzvdgymjjoacppqps")))
 730                (ParTree
 731                 NilTree
 732                 (ParTree
 733                  (SeqTree (FP fx (Hunk 39 (packStringLetters "ssezlwwjgnethvrpnfrkubphzvdgymjjoacppqpsmzafybdcokyjskcgnvhkbz") (packStringLetters "wnesidpccwoiqiichxaaejdsyrhrusqljlcoro")))
 734                   (ParTree
 735                    (ParTree
 736                     (SeqTree (FP fx (Hunk 11 (packStringLetters "abnvujnxnhvybvpouyciaabszfmgwnesidpccwoiqii") (packStringLetters "czfdhqkipdstfjycqaxwnbxrihrufdeyneqiiiafwzlmg"))) NilTree)
 737                     NilTree)
 738                    NilTree))
 739                  (SeqTree (FP fx (Hunk 24 [] (packStringLetters "dihgmsotezucqdgxczvcivijootyvhlwymbiueufnvpwpeukmskqllalfe"))) NilTree))))
 740               (SeqTree (FP fx (Hunk 55 (packStringLetters "yjskcgnvhkbzpysaafnjjhcstgrczplxsfwagmhaaurjsp") (packStringLetters "xldhrutyhcyaqeezwujiguawfyawjjqlirxshjddvq"))) NilTree))
 741              (SeqTree (FP fx (Hunk 19 [] (packStringLetters "ooygwiyogqrqnytixqtmvdxx")))
 742               (SeqTree (FP fx (Hunk 25 (packStringLetters "yogqrqnytixqtmvdxxvolwviqebieonxvcvuvigkfgybmzafybdcokyjskcgnvhkbz") (packStringLetters "akhsmlbkdxnvfoikmiatfbpzdrsyykkpoxvvddeaspzxe")))
 743                (SeqTree (FP fx (Hunk 38 [] (packStringLetters "ji")))
 744                 (ParTree
 745                  NilTree
 746                  (ParTree
 747                   NilTree
 748                   (ParTree
 749                    (ParTree
 750                     NilTree
 751                     (SeqTree (FP fx (Hunk 25 (packStringLetters "akhsmlbkdxnvfjioikmiatfbpzdrsyykkpoxvvddeaspzxepysaafnjjhcstgrczplxs") (packStringLetters "onjbhddskcj")))
 752                      (SeqTree (FP fx (Hunk 38 [] (packStringLetters "fyscunxxxjjtyqpfxeznhtwvlphmp"))) NilTree)))
 753                    (ParTree
 754                     NilTree
 755                     (SeqTree (FP fx (Hunk 43 [] (packStringLetters "xcchzwmzoezxkmkhcmesplnjpqriypshgiqklgdnbmmkldnydiy")))
 756                      (ParTree
 757                       NilTree
 758                       (SeqTree (FP fx (Hunk 63 (packStringLetters "plnjpqriypshgiqklgdnbmmkldnydiymiatfbpzdrsyykkpoxvvddeaspzxepysaafn") (packStringLetters "anjlzfdqbjqbcplvqvkhwjtkigp"))) NilTree)))))))))))
 759             (ParTree
 760              NilTree
 761              NilTree)))
 762           NilTree))
 763         NilTree))
 764       (ParTree
 765        NilTree
 766        (SeqTree (FP fx (Hunk 0 [] (packStringLetters "ti")))
 767         (SeqTree (FP fx (Hunk 0 (packStringLetters "t") (packStringLetters "ybcop")))
 768          (SeqTree (FP fx (Hunk 1 [] (packStringLetters "dvlhgwqlpaeweerqrhnjtfolczbqbzoccnvdsyqiefqitrqneralf")))
 769           (SeqTree (FP fx (Hunk 14 [] (packStringLetters "yairbjphwtnaerccdlfewujvjvmjakbc")))
 770            (SeqTree (FP fx (Hunk 50 [] (packStringLetters "xayvfuwaiiogginufnhsrmktpmlbvxiakjwllddkiyofyfw")))
 771             (ParTree
 772              NilTree
 773              NilTree)))))))))]
 774
 775 fx :: FileName
 776 fx = fp2fn "./F"
 777
 778 \end{code}