1 % Copyright (C) 2002-2003 David Roundy 2 % 3 % This program is free software; you can redistribute it and/or modify 4 % it under the terms of the GNU General Public License as published by 5 % the Free Software Foundation; either version 2, or (at your option) 6 % any later version. 7 % 8 % This program is distributed in the hope that it will be useful, 9 % but WITHOUT ANY WARRANTY; without even the implied warranty of 10 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 11 % GNU General Public License for more details. 12 % 13 % You should have received a copy of the GNU General Public License 14 % along with this program; see the file COPYING. If not, write to 15 % the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, 16 % Boston, MA 02110-1301, USA. 17 18 19 \begin{code} 20 {-# OPTIONS_GHC -cpp -fglasgow-exts -fno-warn-orphans #-} 21 {-# LANGUAGE CPP #-} 22 -- , TypeOperators #-} 23 24 #include "gadts.h" 25 26 module Darcs.Patch.Commute ( fromPrims, 27 modernize_patch, 28 #ifndef GADT_WITNESSES 29 merge, elegant_merge, 30 merger, unravel, 31 #endif 32 public_unravel, mangle_unravelled, 33 CommuteFunction, Perhaps(..), 34 -- for other commutes: 35 toMaybe, 36 ) 37 where 38 39 import Control.Monad ( MonadPlus, mplus, msum, mzero ) 40 41 import Darcs.Patch.FileName ( FileName, fn2fp, fp2fn ) 42 import Darcs.Patch.Info ( invert_name, idpatchinfo ) 43 import Darcs.Patch.Patchy ( Commute(..), Invert(..) ) 44 import Darcs.Patch.Core ( Patch(..), Named(..), 45 #ifndef GADT_WITNESSES 46 flattenFL, 47 is_merger, 48 #endif 49 merger_undo, 50 join_patchesFL ) 51 import Darcs.Patch.Prim ( Prim(..), FromPrims(..), 52 Conflict(..), Effect(..), 53 is_filepatch, sort_coalesceFL, 54 #ifndef GADT_WITNESSES 55 FilePatchType(..), DirPatchType(..), 56 #else 57 FilePatchType(Hunk), 58 #endif 59 is_hunk, modernizePrim ) 60 import qualified Data.ByteString.Char8 as BC (pack, last) 61 import qualified Data.ByteString as B (null, ByteString) 62 import Data.Maybe ( isJust ) 63 import Data.List ( intersperse, sort ) 64 #ifndef GADT_WITNESSES 65 import Darcs.Patch.Permutations ( head_permutationsRL, head_permutationsFL ) 66 import Printer ( text, vcat, ($$) ) 67 import Darcs.Patch.Patchy ( invertRL ) 68 import Darcs.Patch.Show ( showPatch_ ) 69 import Data.List ( nubBy ) 70 import Darcs.Sealed ( unsafeUnseal ) 71 #endif 72 import Darcs.Utils ( nubsort ) 73 #include "impossible.h" 74 import Darcs.Sealed ( Sealed(..), mapSeal ) 75 import Darcs.Ordered ( mapFL, mapFL_FL, unsafeCoerceP, 76 FL(..), RL(..), 77 (:/\:)(..), (:<)(..), (:\/:)(..), (:>)(..), 78 #ifndef GADT_WITNESSES 79 lengthFL, mapRL, 80 #endif 81 reverseFL, reverseRL, concatFL, 82 MyEq, unsafeCompare 83 ) 84 85 --import Darcs.ColorPrinter ( traceDoc ) 86 --import Printer ( greenText ) 87 \end{code} 88 89 \section{Commuting patches} 90 91 \subsection{Composite patches} 92 93 Composite patches are made up of a series of patches intended to be applied 94 sequentially. They are represented by a list of patches, with the first 95 patch in the list being applied first. 96 97 \newcommand{\commutex}{\longleftrightarrow} 98 \newcommand{\commutes}{\longleftrightarrow} 99 100 The first way (of only two) to change the context of a patch is by 101 commutation, which is the process of changing the order of two sequential 102 patches. 103 \begin{dfn} 104 The commutation of patches $P_1$ and $P_2$ is represented by 105 \[ P_2 P_1 \commutes {P_1}' {P_2}'. \] 106 Here $P_1'$ is intended to describe the same change as $P_1$, with the 107 only difference being that $P_1'$ is applied after $P_2'$ rather than 108 before $P_2$. 109 \end{dfn} 110 The above definition is obviously rather vague, the reason being that what 111 is the ``same change'' has not been defined, and we simply assume (and 112 hope) that the code's view of what is the ``same change'' will match those 113 of its human users. The `$\commutes$' operator should be read as something 114 like the $==$ operator in C, indicating that the right hand side performs 115 identical changes to the left hand side, but the two patches are in 116 reversed order. When read in this manner, it is clear that commutation 117 must be a reversible process, and indeed this means that commutation 118 \emph{can} fail, and must fail in certain cases. For example, the creation 119 and deletion of the same file cannot be commuted. When two patches fail to 120 commutex, it is said that the second patch depends on the first, meaning 121 that it must have the first patch in its context (remembering that the 122 context of a patch is a set of patches, which is how we represent a tree). 123 \footnote{The fact that commutation can fail makes a huge difference in the 124 whole patch formalism. It may be possible to create a formalism in which 125 commutation always succeeds, with the result of what would otherwise be a 126 commutation that fails being something like a virtual particle (which can 127 violate conservation of energy), and it may be that such a formalism would 128 allow strict mathematical proofs (whereas those used in the current 129 formalism are mostly only hand waving ``physicist'' proofs). However, I'm 130 not sure how you'd deal with a request to delete a file that has not yet 131 been created, for example. Obviously you'd need to create some kind of 132 antifile, which would annihilate with the file when that file finally got 133 created, but I'm not entirely sure how I'd go about doing this. 134 $\ddot\frown$ So I'm sticking with my hand waving formalism.} 135 136 %I should add that one using the inversion relationship of sequential 137 %patches, one can avoid having to provide redundant definitions of 138 %commutation. 139 140 % There is another interesting property which is that a commutex's results 141 % can't be affected by commuting another thingamabopper. 142 143 \begin{code} 144 data Perhaps a = Unknown | Failed | Succeeded a 145 146 instance Monad Perhaps where 147 (Succeeded x) >>= k = k x 148 Failed >>= _ = Failed 149 Unknown >>= _ = Unknown 150 Failed >> _ = Failed 151 (Succeeded _) >> k = k 152 Unknown >> k = k 153 return = Succeeded 154 fail _ = Unknown 155 156 instance MonadPlus Perhaps where 157 mzero = Unknown 158 Unknown `mplus` ys = ys 159 Failed `mplus` _ = Failed 160 (Succeeded x) `mplus` _ = Succeeded x 161 162 toMaybe :: Perhaps a -> Maybe a 163 toMaybe (Succeeded x) = Just x 164 toMaybe _ = Nothing 165 166 toPerhaps :: Maybe a -> Perhaps a 167 toPerhaps (Just x) = Succeeded x 168 toPerhaps Nothing = Failed 169 170 #ifndef GADT_WITNESSES 171 clever_commute :: CommuteFunction -> CommuteFunction 172 clever_commute c (p1:<p2) = 173 case c (p1 :< p2) of 174 Succeeded x -> Succeeded x 175 Failed -> Failed 176 Unknown -> case c (invert p2 :< invert p1) of 177 Succeeded (p1' :< p2') -> Succeeded (invert p2' :< invert p1') 178 Failed -> Failed 179 Unknown -> Unknown 180 #endif 181 182 speedy_commute :: CommuteFunction 183 speedy_commute (p1 :< p2) -- Deal with common case quickly! 184 | p1_modifies /= Nothing && p2_modifies /= Nothing && 185 p1_modifies /= p2_modifies = Succeeded (unsafeCoerceP p2 :< unsafeCoerceP p1) 186 | otherwise = Unknown 187 where p1_modifies = is_filepatch_merger p1 188 p2_modifies = is_filepatch_merger p2 189 190 instance Commute p => Commute (Named p) where 191 commute (NamedP n1 d1 p1 :> NamedP n2 d2 p2) = 192 if n2 `elem` d1 || n1 `elem` d2 193 then Nothing 194 else do (p2' :> p1') <- commute (p1 :> p2) 195 return (NamedP n2 d2 p2' :> NamedP n1 d1 p1') 196 merge (NamedP n1 d1 p1 :\/: NamedP n2 d2 p2) 197 = case merge (p1 :\/: p2) of 198 (p2' :/\: p1') -> NamedP n2 d2 p2' :/\: NamedP n1 d1 p1' 199 list_touched_files (NamedP _ _ p) = list_touched_files p 200 201 instance Conflict p => Conflict (Named p) where 202 list_conflicted_files (NamedP _ _ p) = list_conflicted_files p 203 resolve_conflicts (NamedP _ _ p) = resolve_conflicts p 204 205 everything_else_commute :: MaybeCommute -> CommuteFunction 206 everything_else_commute c x = eec x 207 where 208 eec :: CommuteFunction 209 eec (PP px :< PP py) = toPerhaps $ do y' :< x' <- commutex (px :< py) 210 return (PP y' :< PP x') 211 eec (ComP NilFL :< p1) = Succeeded (unsafeCoerceP p1 :< (ComP NilFL)) 212 eec (p2 :< ComP NilFL) = Succeeded (ComP NilFL :< unsafeCoerceP p2) 213 eec (ComP (p:>:ps) :< p1) = toPerhaps $ do 214 (p1' :< p') <- c (p :< p1) 215 (p1'' :< ComP ps') <- c (ComP ps :< p1') 216 return (p1'' :< ComP (p':>:ps')) 217 eec (patch2 :< ComP patches) = 218 toPerhaps $ do (patches' :< patch2') <- ccr (patch2 :< reverseFL patches) 219 return (ComP (reverseRL patches') :< patch2') 220 where ccr :: FORALL(x y) (Patch :< RL Patch) C(x y) -> Maybe ((RL Patch :< Patch) C(x y)) 221 ccr (p2 :< NilRL) = seq p2 $ return (NilRL :< p2) 222 ccr (p2 :< p:<:ps) = do (p' :< p2') <- c (p2 :< p) 223 (ps' :< p2'') <- ccr (p2' :< ps) 224 return (p':<:ps' :< p2'') 225 eec _xx = 226 msum [ 227 #ifndef GADT_WITNESSES 228 clever_commute commute_recursive_merger _xx 229 ,clever_commute other_commute_recursive_merger _xx 230 #endif 231 ] 232 233 {- 234 Note that it must be true that 235 236 commutex (A^-1 A, P) = Just (P, A'^-1 A') 237 238 and 239 240 if commutex (A, B) == Just (B', A') 241 then commutex (B^-1, A^-1) == Just (A'^-1, B'^-1) 242 -} 243 244 #ifndef GADT_WITNESSES 245 merger_commute :: (Patch :< Patch) -> Perhaps (Patch :< Patch) 246 merger_commute (Merger _ _ p1 p2 :< pA) 247 | unsafeCompare pA p1 = Succeeded (merger "0.0" p2 p1 :< p2) 248 | unsafeCompare pA (invert (merger "0.0" p2 p1)) = Failed 249 merger_commute (Merger _ _ 250 (Merger _ _ c b) 251 (Merger _ _ c' a) :< 252 Merger _ _ b' c'') 253 | unsafeCompare b' b && unsafeCompare c c' && unsafeCompare c c'' = 254 Succeeded (merger "0.0" (merger "0.0" b a) (merger "0.0" b c) :< 255 merger "0.0" b a) 256 merger_commute _ = Unknown 257 #endif 258 259 instance Commute Patch where 260 merge (y :\/: z) = 261 #ifndef GADT_WITNESSES 262 case actual_merge (y:\/:z) of 263 y' -> case commutex (y' :< z) of 264 Nothing -> bugDoc $ text "merge_patches bug" 265 $$ showPatch_ y 266 $$ showPatch_ z 267 $$ showPatch_ y' 268 Just (z' :< _) -> z' :/\: y' 269 #else 270 case elegant_merge (y:\/:z) of 271 Just (z' :/\: y') -> z' :/\: y' 272 Nothing -> undefined 273 #endif 274 commutex x = toMaybe $ msum [speedy_commute x, 275 #ifndef GADT_WITNESSES 276 clever_commute merger_commute x, 277 #endif 278 everything_else_commute commutex x 279 ] 280 -- Recurse on everything, these are potentially spoofed patches 281 list_touched_files (ComP ps) = nubsort $ concat $ mapFL list_touched_files ps 282 list_touched_files (Merger _ _ p1 p2) = nubsort $ list_touched_files p1 283 ++ list_touched_files p2 284 list_touched_files c@(Regrem _ _ _ _) = list_touched_files $ invert c 285 list_touched_files (PP p) = list_touched_files p 286 287 commute_no_merger :: MaybeCommute 288 commute_no_merger x = 289 #ifndef GADT_WITNESSES 290 toMaybe $ msum [speedy_commute x, 291 everything_else_commute commute_no_merger x] 292 #else 293 bug "commute_no_merger undefined when compiled with GADTs" x 294 #endif 295 296 is_filepatch_merger :: Patch C(x y) -> Maybe FileName 297 is_filepatch_merger (PP p) = is_filepatch p 298 is_filepatch_merger (Merger _ _ p1 p2) = do 299 f1 <- is_filepatch_merger p1 300 f2 <- is_filepatch_merger p2 301 if f1 == f2 then return f1 else Nothing 302 is_filepatch_merger (Regrem und unw p1 p2) 303 = is_filepatch_merger (Merger und unw p1 p2) 304 is_filepatch_merger (ComP _) = Nothing 305 306 #ifndef GADT_WITNESSES 307 commute_recursive_merger :: (Patch :< Patch) -> Perhaps (Patch :< Patch) 308 commute_recursive_merger (p@(Merger _ _ p1 p2) :< pA) = toPerhaps $ 309 do (pA' :< _) <- commutex (undo :< pA) 310 commutex (invert undo :< pA') 311 (pAmid :< _) <- commutex (invert p1 :< pA) 312 (pAx :< p1') <- commutex (p1 :< pAmid) 313 assert (pAx `unsafeCompare` pA) 314 (_ :<p2') <- commutex (p2 :< pAmid) 315 (_ :< p2o) <- commutex (p2' :< invert pAmid) 316 assert (p2o `unsafeCompare` p2) 317 let p' = if unsafeCompare p1' p1 && unsafeCompare p2' p2 318 then p 319 else merger "0.0" p1' p2' 320 undo' = merger_undo p' 321 (_ :< pAo) <- commutex (pA' :< undo') 322 assert (pAo `unsafeCompare` pA) 323 return (pA' :< p') 324 where undo = merger_undo p 325 commute_recursive_merger _ = Unknown 326 327 other_commute_recursive_merger :: (Patch :< Patch) -> Perhaps (Patch :< Patch) 328 other_commute_recursive_merger (pA':< p_old@(Merger _ _ p1' p2')) = 329 toPerhaps $ 330 do (_ :< pA) <- commutex (pA' :< merger_undo p_old) 331 (p1 :< pAmid) <- commutex (pA :< p1') 332 (pAmido :< _) <- commutex (invert p1 :< pA) 333 assert (pAmido `unsafeCompare` pAmid) 334 (_ :< p2) <- commutex (p2' :< invert pAmid) 335 (_ :< p2o') <- commutex (p2 :< pAmid) 336 assert (p2o' `unsafeCompare` p2') 337 let p = if p1 `unsafeCompare` p1' && p2 `unsafeCompare` p2' 338 then p_old 339 else merger "0.0" p1 p2 340 undo = merger_undo p 341 assert (not $ pA `unsafeCompare` p1) -- special case here... 342 (pAo' :< _) <- commutex (undo :<pA) 343 assert (pAo' `unsafeCompare` pA') 344 return (p :< pA) 345 other_commute_recursive_merger _ = Unknown 346 347 assert :: Bool -> Maybe () 348 assert False = Nothing 349 assert True = Just () 350 #endif 351 352 type CommuteFunction = FORALL(x y) (Patch :< Patch) C(x y) -> Perhaps ((Patch :< Patch) C(x y)) 353 type MaybeCommute = FORALL(x y) (Patch :< Patch) C(x y) -> Maybe ((Patch :< Patch) C(x y)) 354 \end{code} 355 356 \paragraph{Merge} 357 \newcommand{\merge}{\Longrightarrow} 358 The second way one can change the context of a patch is by a {\bf merge} 359 operation. A merge is an operation that takes two parallel patches and 360 gives a pair of sequential patches. The merge operation is represented by 361 the arrow ``\( \merge \)''. 362 \begin{dfn}\label{merge_dfn} 363 The result of a merge of two patches, $P_1$ and $P_2$ is one of two patches, 364 $P_1'$ and $P_2'$, which satisfy the relationship: 365 \[ P_2 \parallel P_1 \merge {P_2}' P_1 \commutex {P_1}' P_2. \] 366 \end{dfn} 367 Note that the sequential patches resulting from a merge are \emph{required} 368 to commutex. This is an important consideration, as without it most of the 369 manipulations we would like to perform would not be possible. The other 370 important fact is that a merge \emph{cannot fail}. Naively, those two 371 requirements seem contradictory. In reality, what it means is that the 372 result of a merge may be a patch which is much more complex than any we 373 have yet considered\footnote{Alas, I don't know how to prove that the two 374 constraints even \emph{can} be satisfied. The best I have been able to do 375 is to believe that they can be satisfied, and to be unable to find an case 376 in which my implementation fails to satisfy them. These two requirements 377 are the foundation of the entire theory of patches (have you been counting 378 how many foundations it has?).}. 379 380 \subsection{How merges are actually performed} 381 382 The constraint that any two compatible patches (patches which can 383 successfully be applied to the same tree) can be merged is actually quite 384 difficult to apply. The above merge constraints also imply that the result 385 of a series of merges must be independent of the order of the merges. So 386 I'm putting a whole section here for the interested to see what algorithms 387 I use to actually perform the merges (as this is pretty close to being the 388 most difficult part of the code). 389 390 The first case is that in which the two merges don't actually conflict, but 391 don't trivially merge either (e.g.\ hunk patches on the same file, where the 392 line number has to be shifted as they are merged). This kind of merge can 393 actually be very elegantly dealt with using only commutation and inversion. 394 395 There is a handy little theorem which is immensely useful when trying to 396 merge two patches. 397 \begin{thm}\label{merge_thm} 398 $ P_2' P_1 \commutex P_1' P_2 $ if and only if $ P_1'^{ -1} 399 P_2' \commutex P_2 P_1^{ -1} $, provided both commutations succeed. If 400 either commutex fails, this theorem does not apply. 401 \end{thm} 402 This can easily be proven by multiplying both sides of the first 403 commutation by $P_1'^{ -1}$ on the left, and by $P_1^{ -1}$ on the right. 404 Besides being used in merging, this theorem is also useful in the recursive 405 commutations of mergers. From Theorem~\ref{merge_thm}, we see that the 406 merge of $P_1$ and $P_2'$ is simply the commutation of $P_2$ with $P_1^{ 407 -1}$ (making sure to do the commutation the right way). Of course, if this 408 commutation fails, the patches conflict. Moreover, one must check that the 409 merged result actually commutes with $P_1$, as the theorem applies only 410 when \emph{both} commutations are successful. 411 412 \begin{code} 413 414 elegant_merge :: (Patch :\/: Patch) C(x y) 415 -> Maybe ((Patch :/\: Patch) C(x y)) 416 elegant_merge (p1 :\/: p2) = 417 case commutex (p1 :< invert p2) of 418 Just (ip2':<p1') -> case commutex (p1' :< p2) of 419 Nothing -> Nothing -- should be a redundant check 420 Just (_:<p1o) -> if unsafeCompare p1o p1 421 then Just (invert ip2' :/\: p1') 422 else Nothing 423 Nothing -> Nothing 424 425 \end{code} 426 427 Of course, there are patches that actually conflict, meaning a merge where 428 the two patches truly cannot both be applied (e.g.\ trying to create a file 429 and a directory with the same name). We deal with this case by creating a 430 special kind of patch to support the merge, which we will call a 431 ``merger''. Basically, a merger is a patch that contains the two patches 432 that conflicted, and instructs darcs basically to resolve the conflict. By 433 construction a merger will satisfy the commutation property (see 434 Definition~\ref{merge_dfn}) that characterizes all merges. Moreover the 435 merger's properties are what makes the order of merges unimportant (which 436 is a rather critical property for darcs as a whole). 437 438 The job of a merger is basically to undo the two conflicting patches, and 439 then apply some sort of a ``resolution'' of the two instead. In the case 440 of two conflicting hunks, this will look much like what CVS does, where it 441 inserts both versions into the file. In general, of course, the two 442 conflicting patches may both be mergers themselves, in which case the 443 situation is considerably more complicated. 444 445 \begin{code} 446 #ifndef GADT_WITNESSES 447 actual_merge :: (Patch :\/: Patch) -> Patch 448 actual_merge (ComP the_p1s :\/: ComP the_p2s) = 449 join_patchesFL $ mc the_p1s the_p2s 450 where mc :: FL Patch -> FL Patch -> FL Patch 451 mc NilFL (_:>:_) = NilFL 452 mc p1s NilFL = p1s 453 mc p1s (p2:>:p2s) = mc (merge_patches_after_patch p1s p2) p2s 454 actual_merge (ComP p1s :\/: p2) = seq p2 $ 455 join_patchesFL $ merge_patches_after_patch p1s p2 456 actual_merge (p1 :\/: ComP p2s) = seq p1 $ merge_patch_after_patches p1 p2s 457 458 actual_merge (p1 :\/: p2) = case elegant_merge (p1:\/:p2) of 459 Just (_ :/\: p1') -> p1' 460 Nothing -> merger "0.0" p2 p1 461 462 merge_patch_after_patches :: Patch -> FL Patch -> Patch 463 merge_patch_after_patches p (p1:>:p1s) = 464 merge_patch_after_patches (actual_merge (p:\/:p1)) p1s 465 merge_patch_after_patches p NilFL = p 466 467 merge_patches_after_patch :: FL Patch -> Patch -> FL Patch 468 merge_patches_after_patch p2s p = 469 case commutex (merge_patch_after_patches p p2s :< join_patchesFL p2s) of 470 Just (ComP p2s':< _) -> p2s' 471 _ -> impossible 472 #endif 473 \end{code} 474 475 Much of the merger code depends on a routine which recreates from a single 476 merger the entire sequence of patches which led up to that merger (this is, 477 of course, assuming that this is the complicated general case of a merger 478 of mergers of mergers). This ``unwind'' procedure is rather complicated, 479 but absolutely critical to the merger code, as without it we wouldn't even 480 be able to undo the effects of the patches involved in the merger, since we 481 wouldn't know what patches were all involved in it. 482 483 Basically, unwind takes a merger such as 484 \begin{verbatim} 485 M( M(A,B), M(A,M(C,D))) 486 \end{verbatim} 487 From which it recreates a merge history: 488 \begin{verbatim} 489 C 490 A 491 M(A,B) 492 M( M(A,B), M(A,M(C,D))) 493 \end{verbatim} 494 (For the curious, yes I can easily unwind this merger in my head [and on 495 paper can unwind insanely more complex mergers]---that's what comes of 496 working for a few months on an algorithm.) Let's start with a simple 497 unwinding. The merger \verb!M(A,B)! simply means that two patches 498 (\verb!A! and \verb!B!) conflicted, and of the two of them \verb!A! is 499 first in the history. The last two patches in the unwinding of any merger 500 are always just this easy. So this unwinds to: 501 \begin{verbatim} 502 A 503 M(A,B) 504 \end{verbatim} 505 What about a merger of mergers? How about \verb!M(A,M(C,D))!. In this case 506 we know the two most recent patches are: 507 \begin{verbatim} 508 A 509 M(A,M(C,D)) 510 \end{verbatim} 511 But obviously the unwinding isn't complete, since we don't yet see where 512 \verb!C! and \verb!D! came from. In this case we take the unwinding of 513 \verb!M(C,D)! and drop its latest patch (which is \verb!M(C,D)! itself) and 514 place that at the beginning of our patch train: 515 \begin{verbatim} 516 C 517 A 518 M(A,M(C,D)) 519 \end{verbatim} 520 As we look at \verb!M( M(A,B), M(A,M(C,D)))!, we consider the unwindings of 521 each of its subpatches: 522 \begin{verbatim} 523 C 524 A A 525 M(A,B) M(A,M(C,D)) 526 \end{verbatim} 527 As we did with \verb!M(A,M(C,D))!, we'll drop the first patch on the 528 right and insert the first patch on the left. That moves us up to the two 529 \verb!A!'s. Since these agree, we can use just one of them (they 530 ``should'' agree). That leaves us with the \verb!C! which goes first. 531 532 The catch is that things don't always turn out this easily. There is no 533 guarantee that the two \verb!A!'s would come out at the same time, and if 534 they didn't, we'd have to rearrange things until they did. Or if there was 535 no way to rearrange things so that they would agree, we have to go on to 536 plan B, which I will explain now. 537 538 Consider the case of \verb!M( M(A,B), M(C,D))!. We can easily unwind the 539 two subpatches 540 \begin{verbatim} 541 A C 542 M(A,B) M(C,D) 543 \end{verbatim} 544 Now we need to reconcile the \verb!A! and \verb!C!. How do we do this? 545 Well, as usual, the solution is to use the most wonderful 546 Theorem~\ref{merge_thm}. In this case we have to use it in the reverse of 547 how we used it when merging, since we know that \verb!A! and \verb!C! could 548 either one be the \emph{last} patch applied before \verb!M(A,B)! or 549 \verb!M(C,D)!. So we can find \verb!C'! using 550 \[ 551 A^{ -1} C \commutex C' A'^{ -1} 552 \] 553 Giving an unwinding of 554 \begin{verbatim} 555 C' 556 A 557 M(A,B) 558 M( M(A,B), M(C,D) ) 559 \end{verbatim} 560 There is a bit more complexity to the unwinding process (mostly having to 561 do with cases where you have deeper nesting), but I think the general 562 principles that are followed are pretty much included in the above 563 discussion. 564 565 \begin{code} 566 #ifndef GADT_WITNESSES 567 unwind :: Patch -> RL Patch -- Recreates a patch history in reverse. 568 unwind (Merger _ unwindings _ _) = unwindings 569 unwind p = p :<: NilRL; 570 571 true_unwind :: Patch -> RL Patch -- Recreates a patch history in reverse. 572 true_unwind p@(Merger _ _ p1 p2) = 573 case (unwind p1, unwind p2) of 574 (_:<:p1s,_:<:p2s) -> p :<: p1 :<: reconcile_unwindings p p1s p2s 575 _ -> impossible 576 true_unwind _ = impossible 577 578 reconcile_unwindings :: Patch -> RL Patch -> RL Patch -> RL Patch 579 reconcile_unwindings _ NilRL p2s = p2s 580 reconcile_unwindings _ p1s NilRL = p1s 581 reconcile_unwindings p (p1:<:p1s) p2s = 582 case [(p1s', p2s')| 583 p1s'@(hp1s':<:_) <- head_permutationsRL (p1:<:p1s), 584 p2s'@(hp2s':<:_) <- head_permutationsRL p2s, 585 hp1s' `unsafeCompare` hp2s'] of 586 ((p1':<:p1s', _:<:p2s'):_) -> 587 p1' :<: reconcile_unwindings p p1s' p2s' 588 [] -> case reverseFL `fmap` put_before p1 (reverseRL p2s) of 589 Just p2s' -> p1 :<: reconcile_unwindings p p1s p2s' 590 Nothing -> 591 case fmap reverseFL $ put_before (headRL p2s) $ 592 reverseRL (p1:<:p1s) of 593 Just p1s' -> case p2s of 594 hp2s:<:tp2s -> hp2s :<: 595 reconcile_unwindings p p1s' tp2s 596 NilRL -> impossible 597 Nothing -> 598 bugDoc $ text "in function reconcile_unwindings" 599 $$ text "Original patch:" 600 $$ showPatch_ p 601 _ -> bug "in reconcile_unwindings" 602 603 put_before :: Patch -> FL Patch -> Maybe (FL Patch) 604 put_before p1 (p2:>:p2s) = 605 do p2':<p1' <- commutex (invert p1:<p2) 606 commutex (p1:<p2') 607 (p2' :>:) `fmap` put_before p1' p2s 608 put_before _ NilFL = Just NilFL 609 #endif 610 \end{code} 611 612 \section{Conflicts} 613 614 There are a couple of simple constraints on the routine which determines 615 how to resolve two conflicting patches (which is called `glump'). These 616 must be satisfied in order that the result of a series of merges is always 617 independent of their order. Firstly, the output of glump cannot change 618 when the order of the two conflicting patches is switched. If it did, then 619 commuting the merger could change the resulting patch, which would be bad. 620 Secondly, the result of the merge of three (or more) conflicting patches 621 cannot depend on the order in which the merges are performed. 622 623 The conflict resolution code (glump) begins by ``unravelling'' the merger 624 into a set of sequences of patches. Each sequence of patches corresponds 625 to one non-conflicted patch that got merged together with the others. The 626 result of the unravelling of a series of merges must obviously be 627 independent of the order in which those merges are performed. This 628 unravelling code (which uses the unwind code mentioned above) uses probably 629 the second most complicated algorithm. Fortunately, if we can successfully 630 unravel the merger, almost any function of the unravelled merger satisfies 631 the two constraints mentioned above that the conflict resolution code must 632 satisfy. 633 634 \begin{code} 635 instance Conflict Patch where 636 commute_no_conflicts (x:>y) = do x' :< y' <- commute_no_merger (y :< x) 637 return (y':>x') 638 #ifndef GADT_WITNESSES 639 resolve_conflicts patch = rcs NilFL $ reverseFL $ flattenFL patch 640 where rcs :: FL Patch C(w y) -> RL Patch C(x y) -> [[Sealed (FL Prim C(w))]] 641 rcs _ NilRL = [] 642 rcs passedby (p@(Merger _ _ _ _):<:ps) = 643 case commute_no_merger (join_patchesFL passedby:<p) of 644 Just (p'@(Merger _ _ p1 p2):<_) -> 645 (map Sealed $ nubBy unsafeCompare $ effect (glump09 p1 p2) : unravel p') 646 : rcs (p :>: passedby) ps 647 Nothing -> rcs (p :>: passedby) ps 648 _ -> impossible 649 rcs passedby (p:<:ps) = seq passedby $ 650 rcs (p :>: passedby) ps 651 #else 652 resolve_conflicts = bug "haven't defined resolve_conflicts with type witnesses." 653 #endif 654 655 public_unravel :: Patch C(x y) -> [Sealed (FL Prim C(y))] 656 #ifdef GADT_WITNESSES 657 public_unravel = bug "Haven't implemented public_unravel with type witnesses." 658 #else 659 public_unravel p = map Sealed $ unravel p 660 #endif 661 662 #ifndef GADT_WITNESSES 663 unravel :: Patch -> [FL Prim] 664 unravel p = nubBy unsafeCompare $ 665 map (sort_coalesceFL . concatFL . mapFL_FL effect) $ 666 get_supers $ map reverseRL $ new_ur p $ unwind p 667 668 get_supers :: [FL Patch] -> [FL Patch] 669 get_supers (x:xs) = 670 case filter (not.(x `is_superpatch_of`)) xs of 671 xs' -> if or $ map (`is_superpatch_of` x) xs' 672 then get_supers xs' 673 else x : get_supers xs' 674 get_supers [] = [] 675 is_superpatch_of :: FL Patch -> FL Patch -> Bool 676 x `is_superpatch_of` y | lengthFL y > lengthFL x = False 677 x `is_superpatch_of` y = x `iso` y 678 where iso :: FL Patch -> FL Patch -> Bool 679 _ `iso` NilFL = True 680 NilFL `iso` _ = False 681 a `iso` (b:>:bs) = 682 case filter ((`unsafeCompare` b) . headFL) $ 683 head_permutationsFL a of 684 ((_:>:as):_) -> as `iso` bs 685 [] -> False 686 _ -> bug "bug in is_superpatch_of" 687 688 headFL :: FL a -> a 689 headFL (x:>:_) = x 690 headFL NilFL = bug "bad headFL" 691 692 merger :: String -> Patch -> Patch -> Patch 693 merger "0.0" p1 p2 = Merger undoit unwindings p1 p2 694 where fake_p = Merger identity NilRL p1 p2 695 unwindings = true_unwind fake_p 696 p = Merger identity unwindings p1 p2 697 undoit = 698 case (is_merger p1, is_merger p2) of 699 (True ,True ) -> join_patchesFL $ invertRL $ tailRL $ unwind p 700 where tailRL (_:<:t) = t 701 tailRL _ = impossible 702 (False,False) -> invert p1 703 (True ,False) -> join_patchesFL NilFL 704 (False,True ) -> join_patchesFL (invert p1 :>: merger_undo p2 :>: NilFL) 705 merger g _ _ = 706 error $ "Cannot handle mergers other than version 0.0\n"++g 707 ++ "\nPlease use darcs optimize --modernize with an older darcs." 708 709 glump09 :: Patch -> Patch -> Patch 710 glump09 p1 p2 = fromPrims $ unsafeUnseal $ mangle_unravelled $ map Sealed $ unravel $ merger "0.0" p1 p2 711 712 #endif 713 714 mangle_unravelled :: [Sealed (FL Prim C(x))] -> Sealed (FL Prim C(x)) 715 mangle_unravelled pss = if only_hunks pss 716 then (:>: NilFL) `mapSeal` mangle_unravelled_hunks pss 717 else head pss 718 719 only_hunks :: [Sealed (FL Prim C(x))] -> Bool 720 only_hunks [] = False 721 only_hunks pss = fn2fp f /= "" && all oh pss 722 where f = get_a_filename pss 723 oh :: Sealed (FL Prim C(x)) -> Bool 724 oh (Sealed (p:>:ps)) = is_hunk p && 725 [fn2fp f] == list_touched_files p && 726 oh (Sealed ps) 727 oh (Sealed NilFL) = True 728 729 apply_hunks :: [Maybe B.ByteString] -> FL Prim C(x y) -> [Maybe B.ByteString] 730 apply_hunks ms (FP _ (Hunk l o n):>:ps) = apply_hunks (rls l ms) ps 731 where rls 1 mls = map Just n ++ drop (length o) mls 732 rls i (ml:mls) = ml : rls (i-1) mls 733 rls _ [] = bug "rls in apply_hunks" 734 apply_hunks ms NilFL = ms 735 apply_hunks _ (_:>:_) = impossible 736 737 get_old :: [Maybe B.ByteString] -> [Sealed (FL Prim C(x))] -> [Maybe B.ByteString] 738 get_old mls (ps:pss) = get_old (get_hunks_old mls ps) pss 739 get_old mls [] = mls 740 741 get_a_filename :: [Sealed (FL Prim C(x))] -> FileName 742 get_a_filename ((Sealed (FP f _:>:_)):_) = f 743 get_a_filename _ = fp2fn "" 744 745 get_hunks_old :: [Maybe B.ByteString] -> Sealed (FL Prim C(x)) 746 -> [Maybe B.ByteString] 747 get_hunks_old mls (Sealed ps) = 748 apply_hunks (apply_hunks mls ps) (invert ps) 749 750 get_hunks_new :: [Maybe B.ByteString] -> Sealed (FL Prim C(x)) 751 -> [Maybe B.ByteString] 752 get_hunks_new mls (Sealed ps) = apply_hunks mls ps 753 754 get_hunkline :: [[Maybe B.ByteString]] -> Int 755 get_hunkline = ghl 1 756 where ghl :: Int -> [[Maybe B.ByteString]] -> Int 757 ghl n pps = 758 if any (isJust . head) pps 759 then n 760 else ghl (n+1) $ map tail pps 761 762 make_chunk :: Int -> [Maybe B.ByteString] -> [B.ByteString] 763 make_chunk n mls = pull_chunk $ drop (n-1) mls 764 where pull_chunk (Just l:mls') = l : pull_chunk mls' 765 pull_chunk (Nothing:_) = [] 766 pull_chunk [] = bug "should this be [] in pull_chunk?" 767 768 mangle_unravelled_hunks :: [Sealed (FL Prim C(x))] -> Sealed (Prim C(x)) 769 --mangle_unravelled_hunks [[h1],[h2]] = Deal with simple cases handily? 770 mangle_unravelled_hunks pss = 771 if null nchs then bug "mangle_unravelled_hunks" 772 else Sealed (FP filename (Hunk l old new)) 773 where oldf = get_old (repeat Nothing) pss 774 newfs = map (get_hunks_new oldf) pss 775 l = get_hunkline $ oldf : newfs 776 nchs = sort $ map (make_chunk l) newfs 777 filename = get_a_filename pss 778 old = make_chunk l oldf 779 new = [top] ++ concat (intersperse [middle] nchs) ++ [bottom] 780 top = BC.pack $ "v v v v v v v" ++ eol_c 781 middle = BC.pack $ "*************" ++ eol_c 782 bottom = BC.pack $ "^ ^ ^ ^ ^ ^ ^" ++ eol_c 783 eol_c = if any (\ps -> not (B.null ps) && BC.last ps == '\r') old 784 then "\r" 785 else "" 786 787 instance Effect Patch where 788 effect p@(Merger _ _ _ _) = sort_coalesceFL $ effect $ merger_undo p 789 effect p@(Regrem _ _ _ _) = invert $ effect $ invert p 790 effect (ComP ps) = concatFL $ mapFL_FL effect ps 791 effect (PP p) = effect p 792 isHunk p = do PP p' <- return p 793 isHunk p' 794 795 modernize_patch :: Patch C(x y) -> Patch C(x y) 796 modernize_patch p@(Merger _ _ _ _) = fromPrims $ effect p 797 modernize_patch p@(Regrem _ _ _ _) = fromPrims $ effect p 798 modernize_patch (ComP ps) = ComP $ filtermv $ mapFL_FL modernize_patch ps 799 where filtermv :: FL Patch C(x y) -> FL Patch C(x y) 800 #ifndef GADT_WITNESSES 801 filtermv (PP (Move _ b):>:xs) | hasadd xs = filtermv xs 802 where hasadd (PP (FP b' AddFile):>:_) | b' == b = True 803 hasadd (PP (DP b' AddDir):>:_) | b' == b = True 804 hasadd (PP (FP b' RmFile):>:_) | b' == b = False 805 hasadd (PP (DP b' RmDir):>:_) | b' == b = False 806 hasadd (_:>:z) = hasadd z 807 hasadd NilFL = False 808 #endif 809 filtermv (x:>:xs) = x :>: filtermv xs 810 filtermv NilFL = NilFL 811 812 modernize_patch (PP p) = fromPrims $ modernizePrim p 813 814 instance FromPrims Patch where 815 fromPrims (p :>: NilFL) = PP p 816 fromPrims ps = join_patchesFL $ mapFL_FL PP ps 817 joinPatches = join_patchesFL 818 819 #ifndef GADT_WITNESSES 820 new_ur :: Patch -> RL Patch -> [RL Patch] 821 new_ur p (Merger _ _ p1 p2 :<: ps) = 822 case filter ((`unsafeCompare` p1) . headRL) $ head_permutationsRL ps of 823 ((_:<:ps'):_) -> new_ur p (p1:<:ps') ++ new_ur p (p2:<:ps') 824 _ -> bugDoc $ text "in function new_ur" 825 $$ text "Original patch:" 826 $$ showPatch_ p 827 $$ text "Unwound:" 828 $$ vcat (mapRL showPatch_ $ unwind p) 829 830 new_ur op ps = 831 case filter (is_merger.headRL) $ head_permutationsRL ps of 832 [] -> [ps] 833 (ps':_) -> new_ur op ps' 834 835 headRL :: RL a -> a 836 headRL (x:<:_) = x 837 headRL _ = bug "bad headRL" 838 #endif 839 840 instance Invert p => Invert (Named p) where 841 invert (NamedP n d p) = NamedP (invert_name n) (map invert_name d) (invert p) 842 identity = NamedP idpatchinfo [] identity 843 844 instance Invert Patch where 845 invert (Merger undo unwindings p1 p2) 846 = Regrem undo unwindings p1 p2 847 invert (Regrem undo unwindings p1 p2) 848 = Merger undo unwindings p1 p2 849 invert (PP p) = PP (invert p) 850 invert (ComP ps) = ComP $ invert ps 851 identity = ComP NilFL 852 853 instance MyEq Patch where 854 unsafeCompare = eq_patches 855 instance MyEq p => MyEq (Named p) where 856 unsafeCompare (NamedP n1 d1 p1) (NamedP n2 d2 p2) = 857 n1 == n2 && d1 == d2 && unsafeCompare p1 p2 858 859 eq_patches :: Patch C(x y) -> Patch C(w z) -> Bool 860 eq_patches (PP p1) (PP p2) = unsafeCompare p1 p2 861 eq_patches (ComP ps1) (ComP ps2) 862 = eq_FL eq_patches ps1 ps2 863 eq_patches (ComP NilFL) (PP Identity) = True 864 eq_patches (PP Identity) (ComP NilFL) = True 865 eq_patches (Merger _ _ p1a p1b) (Merger _ _ p2a p2b) 866 = eq_patches p1a p2a && 867 eq_patches p1b p2b 868 eq_patches (Regrem _ _ p1a p1b) (Regrem _ _ p2a p2b) 869 = eq_patches p1a p2a && 870 eq_patches p1b p2b 871 eq_patches _ _ = False 872 873 eq_FL :: (FORALL(b c d e) a C(b c) -> a C(d e) -> Bool) 874 -> FL a C(x y) -> FL a C(w z) -> Bool 875 eq_FL _ NilFL NilFL = True 876 eq_FL f (x:>:xs) (y:>:ys) = f x y && eq_FL f xs ys 877 eq_FL _ _ _ = False 878 879 \end{code}