Find git executable at run time
[git-darcs-import.git] / src / Darcs / Patch / Commute.lhs
blob59db56ddf9558ccf44aa9b1896643b3bffcc441e
1 % Copyright (C) 2002-2003 David Roundy
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.
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.
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.
19 \begin{code}
20 {-# OPTIONS_GHC -cpp -fglasgow-exts -fno-warn-orphans #-}
21 {-# LANGUAGE CPP #-}
22 -- , TypeOperators #-}
24 #include "gadts.h"
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,
37 where
39 import Control.Monad ( MonadPlus, mplus, msum, mzero )
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
85 --import Darcs.ColorPrinter ( traceDoc )
86 --import Printer ( greenText )
87 \end{code}
89 \section{Commuting patches}
91 \subsection{Composite patches}
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.
97 \newcommand{\commutex}{\longleftrightarrow}
98 \newcommand{\commutes}{\longleftrightarrow}
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.}
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.
140 % There is another interesting property which is that a commutex's results
141 % can't be affected by commuting another thingamabopper.
143 \begin{code}
144 data Perhaps a = Unknown | Failed | Succeeded a
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
156 instance MonadPlus Perhaps where
157 mzero = Unknown
158 Unknown `mplus` ys = ys
159 Failed `mplus` _ = Failed
160 (Succeeded x) `mplus` _ = Succeeded x
162 toMaybe :: Perhaps a -> Maybe a
163 toMaybe (Succeeded x) = Just x
164 toMaybe _ = Nothing
166 toPerhaps :: Maybe a -> Perhaps a
167 toPerhaps (Just x) = Succeeded x
168 toPerhaps Nothing = Failed
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
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
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
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
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
234 Note that it must be true that
236 commutex (A^-1 A, P) = Just (P, A'^-1 A')
240 if commutex (A, B) == Just (B', A')
241 then commutex (B^-1, A^-1) == Just (A'^-1, B'^-1)
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
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
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
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
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 \end{code}
307 \begin{code}
308 #ifndef GADT_WITNESSES
309 commute_recursive_merger :: (Patch :< Patch) -> Perhaps (Patch :< Patch)
310 commute_recursive_merger (p@(Merger _ _ p1 p2) :< pA) = toPerhaps $
311 do (pA' :< _) <- commutex (undo :< pA)
312 commutex (invert undo :< pA')
313 (pAmid :< _) <- commutex (invert p1 :< pA)
314 (pAx :< p1') <- commutex (p1 :< pAmid)
315 assert (pAx `unsafeCompare` pA)
316 (_ :<p2') <- commutex (p2 :< pAmid)
317 (_ :< p2o) <- commutex (p2' :< invert pAmid)
318 assert (p2o `unsafeCompare` p2)
319 let p' = if unsafeCompare p1' p1 && unsafeCompare p2' p2
320 then p
321 else merger "0.0" p1' p2'
322 undo' = merger_undo p'
323 (_ :< pAo) <- commutex (pA' :< undo')
324 assert (pAo `unsafeCompare` pA)
325 return (pA' :< p')
326 where undo = merger_undo p
327 commute_recursive_merger _ = Unknown
329 other_commute_recursive_merger :: (Patch :< Patch) -> Perhaps (Patch :< Patch)
330 other_commute_recursive_merger (pA':< p_old@(Merger _ _ p1' p2')) =
331 toPerhaps $
332 do (_ :< pA) <- commutex (pA' :< merger_undo p_old)
333 (p1 :< pAmid) <- commutex (pA :< p1')
334 (pAmido :< _) <- commutex (invert p1 :< pA)
335 assert (pAmido `unsafeCompare` pAmid)
336 (_ :< p2) <- commutex (p2' :< invert pAmid)
337 (_ :< p2o') <- commutex (p2 :< pAmid)
338 assert (p2o' `unsafeCompare` p2')
339 let p = if p1 `unsafeCompare` p1' && p2 `unsafeCompare` p2'
340 then p_old
341 else merger "0.0" p1 p2
342 undo = merger_undo p
343 assert (not $ pA `unsafeCompare` p1) -- special case here...
344 (pAo' :< _) <- commutex (undo :<pA)
345 assert (pAo' `unsafeCompare` pA')
346 return (p :< pA)
347 other_commute_recursive_merger _ = Unknown
349 assert :: Bool -> Maybe ()
350 assert False = Nothing
351 assert True = Just ()
352 #endif
353 \end{code}
355 \begin{code}
356 type CommuteFunction = FORALL(x y) (Patch :< Patch) C(x y) -> Perhaps ((Patch :< Patch) C(x y))
357 type MaybeCommute = FORALL(x y) (Patch :< Patch) C(x y) -> Maybe ((Patch :< Patch) C(x y))
358 \end{code}
360 \paragraph{Merge}
361 \newcommand{\merge}{\Longrightarrow}
362 The second way one can change the context of a patch is by a {\bf merge}
363 operation. A merge is an operation that takes two parallel patches and
364 gives a pair of sequential patches. The merge operation is represented by
365 the arrow ``\( \merge \)''.
366 \begin{dfn}\label{merge_dfn}
367 The result of a merge of two patches, $P_1$ and $P_2$ is one of two patches,
368 $P_1'$ and $P_2'$, which satisfy the relationship:
369 \[ P_2 \parallel P_1 \merge {P_2}' P_1 \commutex {P_1}' P_2. \]
370 \end{dfn}
371 Note that the sequential patches resulting from a merge are \emph{required}
372 to commutex. This is an important consideration, as without it most of the
373 manipulations we would like to perform would not be possible. The other
374 important fact is that a merge \emph{cannot fail}. Naively, those two
375 requirements seem contradictory. In reality, what it means is that the
376 result of a merge may be a patch which is much more complex than any we
377 have yet considered\footnote{Alas, I don't know how to prove that the two
378 constraints even \emph{can} be satisfied. The best I have been able to do
379 is to believe that they can be satisfied, and to be unable to find an case
380 in which my implementation fails to satisfy them. These two requirements
381 are the foundation of the entire theory of patches (have you been counting
382 how many foundations it has?).}.
384 \subsection{How merges are actually performed}
386 The constraint that any two compatible patches (patches which can
387 successfully be applied to the same tree) can be merged is actually quite
388 difficult to apply. The above merge constraints also imply that the result
389 of a series of merges must be independent of the order of the merges. So
390 I'm putting a whole section here for the interested to see what algorithms
391 I use to actually perform the merges (as this is pretty close to being the
392 most difficult part of the code).
394 The first case is that in which the two merges don't actually conflict, but
395 don't trivially merge either (e.g.\ hunk patches on the same file, where the
396 line number has to be shifted as they are merged). This kind of merge can
397 actually be very elegantly dealt with using only commutation and inversion.
399 There is a handy little theorem which is immensely useful when trying to
400 merge two patches.
401 \begin{thm}\label{merge_thm}
402 $ P_2' P_1 \commutex P_1' P_2 $ if and only if $ P_1'^{ -1}
403 P_2' \commutex P_2 P_1^{ -1} $, provided both commutations succeed. If
404 either commutex fails, this theorem does not apply.
405 \end{thm}
406 This can easily be proven by multiplying both sides of the first
407 commutation by $P_1'^{ -1}$ on the left, and by $P_1^{ -1}$ on the right.
408 Besides being used in merging, this theorem is also useful in the recursive
409 commutations of mergers. From Theorem~\ref{merge_thm}, we see that the
410 merge of $P_1$ and $P_2'$ is simply the commutation of $P_2$ with $P_1^{
411 -1}$ (making sure to do the commutation the right way). Of course, if this
412 commutation fails, the patches conflict. Moreover, one must check that the
413 merged result actually commutes with $P_1$, as the theorem applies only
414 when \emph{both} commutations are successful.
416 \begin{code}
418 elegant_merge :: (Patch :\/: Patch) C(x y)
419 -> Maybe ((Patch :/\: Patch) C(x y))
420 elegant_merge (p1 :\/: p2) =
421 case commutex (p1 :< invert p2) of
422 Just (ip2':<p1') -> case commutex (p1' :< p2) of
423 Nothing -> Nothing -- should be a redundant check
424 Just (_:<p1o) -> if unsafeCompare p1o p1
425 then Just (invert ip2' :/\: p1')
426 else Nothing
427 Nothing -> Nothing
429 \end{code}
431 Of course, there are patches that actually conflict, meaning a merge where
432 the two patches truly cannot both be applied (e.g.\ trying to create a file
433 and a directory with the same name). We deal with this case by creating a
434 special kind of patch to support the merge, which we will call a
435 ``merger''. Basically, a merger is a patch that contains the two patches
436 that conflicted, and instructs darcs basically to resolve the conflict. By
437 construction a merger will satisfy the commutation property (see
438 Definition~\ref{merge_dfn}) that characterizes all merges. Moreover the
439 merger's properties are what makes the order of merges unimportant (which
440 is a rather critical property for darcs as a whole).
442 The job of a merger is basically to undo the two conflicting patches, and
443 then apply some sort of a ``resolution'' of the two instead. In the case
444 of two conflicting hunks, this will look much like what CVS does, where it
445 inserts both versions into the file. In general, of course, the two
446 conflicting patches may both be mergers themselves, in which case the
447 situation is considerably more complicated.
449 \begin{code}
450 #ifndef GADT_WITNESSES
451 actual_merge :: (Patch :\/: Patch) -> Patch
452 actual_merge (ComP the_p1s :\/: ComP the_p2s) =
453 join_patchesFL $ mc the_p1s the_p2s
454 where mc :: FL Patch -> FL Patch -> FL Patch
455 mc NilFL (_:>:_) = NilFL
456 mc p1s NilFL = p1s
457 mc p1s (p2:>:p2s) = mc (merge_patches_after_patch p1s p2) p2s
458 actual_merge (ComP p1s :\/: p2) = seq p2 $
459 join_patchesFL $ merge_patches_after_patch p1s p2
460 actual_merge (p1 :\/: ComP p2s) = seq p1 $ merge_patch_after_patches p1 p2s
462 actual_merge (p1 :\/: p2) = case elegant_merge (p1:\/:p2) of
463 Just (_ :/\: p1') -> p1'
464 Nothing -> merger "0.0" p2 p1
466 merge_patch_after_patches :: Patch -> FL Patch -> Patch
467 merge_patch_after_patches p (p1:>:p1s) =
468 merge_patch_after_patches (actual_merge (p:\/:p1)) p1s
469 merge_patch_after_patches p NilFL = p
471 merge_patches_after_patch :: FL Patch -> Patch -> FL Patch
472 merge_patches_after_patch p2s p =
473 case commutex (merge_patch_after_patches p p2s :< join_patchesFL p2s) of
474 Just (ComP p2s':< _) -> p2s'
475 _ -> impossible
476 #endif
477 \end{code}
479 Much of the merger code depends on a routine which recreates from a single
480 merger the entire sequence of patches which led up to that merger (this is,
481 of course, assuming that this is the complicated general case of a merger
482 of mergers of mergers). This ``unwind'' procedure is rather complicated,
483 but absolutely critical to the merger code, as without it we wouldn't even
484 be able to undo the effects of the patches involved in the merger, since we
485 wouldn't know what patches were all involved in it.
487 Basically, unwind takes a merger such as
488 \begin{verbatim}
489 M( M(A,B), M(A,M(C,D)))
490 \end{verbatim}
491 From which it recreates a merge history:
492 \begin{verbatim}
495 M(A,B)
496 M( M(A,B), M(A,M(C,D)))
497 \end{verbatim}
498 (For the curious, yes I can easily unwind this merger in my head [and on
499 paper can unwind insanely more complex mergers]---that's what comes of
500 working for a few months on an algorithm.) Let's start with a simple
501 unwinding. The merger \verb!M(A,B)! simply means that two patches
502 (\verb!A! and \verb!B!) conflicted, and of the two of them \verb!A! is
503 first in the history. The last two patches in the unwinding of any merger
504 are always just this easy. So this unwinds to:
505 \begin{verbatim}
507 M(A,B)
508 \end{verbatim}
509 What about a merger of mergers? How about \verb!M(A,M(C,D))!. In this case
510 we know the two most recent patches are:
511 \begin{verbatim}
513 M(A,M(C,D))
514 \end{verbatim}
515 But obviously the unwinding isn't complete, since we don't yet see where
516 \verb!C! and \verb!D! came from. In this case we take the unwinding of
517 \verb!M(C,D)! and drop its latest patch (which is \verb!M(C,D)! itself) and
518 place that at the beginning of our patch train:
519 \begin{verbatim}
522 M(A,M(C,D))
523 \end{verbatim}
524 As we look at \verb!M( M(A,B), M(A,M(C,D)))!, we consider the unwindings of
525 each of its subpatches:
526 \begin{verbatim}
529 M(A,B) M(A,M(C,D))
530 \end{verbatim}
531 As we did with \verb!M(A,M(C,D))!, we'll drop the first patch on the
532 right and insert the first patch on the left. That moves us up to the two
533 \verb!A!'s. Since these agree, we can use just one of them (they
534 ``should'' agree). That leaves us with the \verb!C! which goes first.
536 The catch is that things don't always turn out this easily. There is no
537 guarantee that the two \verb!A!'s would come out at the same time, and if
538 they didn't, we'd have to rearrange things until they did. Or if there was
539 no way to rearrange things so that they would agree, we have to go on to
540 plan B, which I will explain now.
542 Consider the case of \verb!M( M(A,B), M(C,D))!. We can easily unwind the
543 two subpatches
544 \begin{verbatim}
546 M(A,B) M(C,D)
547 \end{verbatim}
548 Now we need to reconcile the \verb!A! and \verb!C!. How do we do this?
549 Well, as usual, the solution is to use the most wonderful
550 Theorem~\ref{merge_thm}. In this case we have to use it in the reverse of
551 how we used it when merging, since we know that \verb!A! and \verb!C! could
552 either one be the \emph{last} patch applied before \verb!M(A,B)! or
553 \verb!M(C,D)!. So we can find \verb!C'! using
555 A^{ -1} C \commutex C' A'^{ -1}
557 Giving an unwinding of
558 \begin{verbatim}
561 M(A,B)
562 M( M(A,B), M(C,D) )
563 \end{verbatim}
564 There is a bit more complexity to the unwinding process (mostly having to
565 do with cases where you have deeper nesting), but I think the general
566 principles that are followed are pretty much included in the above
567 discussion.
569 \begin{code}
570 #ifndef GADT_WITNESSES
571 unwind :: Patch -> RL Patch -- Recreates a patch history in reverse.
572 unwind (Merger _ unwindings _ _) = unwindings
573 unwind p = p :<: NilRL;
575 true_unwind :: Patch -> RL Patch -- Recreates a patch history in reverse.
576 true_unwind p@(Merger _ _ p1 p2) =
577 case (unwind p1, unwind p2) of
578 (_:<:p1s,_:<:p2s) -> p :<: p1 :<: reconcile_unwindings p p1s p2s
579 _ -> impossible
580 true_unwind _ = impossible
582 reconcile_unwindings :: Patch -> RL Patch -> RL Patch -> RL Patch
583 reconcile_unwindings _ NilRL p2s = p2s
584 reconcile_unwindings _ p1s NilRL = p1s
585 reconcile_unwindings p (p1:<:p1s) p2s =
586 case [(p1s', p2s')|
587 p1s'@(hp1s':<:_) <- head_permutationsRL (p1:<:p1s),
588 p2s'@(hp2s':<:_) <- head_permutationsRL p2s,
589 hp1s' `unsafeCompare` hp2s'] of
590 ((p1':<:p1s', _:<:p2s'):_) ->
591 p1' :<: reconcile_unwindings p p1s' p2s'
592 [] -> case reverseFL `fmap` put_before p1 (reverseRL p2s) of
593 Just p2s' -> p1 :<: reconcile_unwindings p p1s p2s'
594 Nothing ->
595 case fmap reverseFL $ put_before (headRL p2s) $
596 reverseRL (p1:<:p1s) of
597 Just p1s' -> case p2s of
598 hp2s:<:tp2s -> hp2s :<:
599 reconcile_unwindings p p1s' tp2s
600 NilRL -> impossible
601 Nothing ->
602 bugDoc $ text "in function reconcile_unwindings"
603 $$ text "Original patch:"
604 $$ showPatch_ p
605 _ -> bug "in reconcile_unwindings"
607 put_before :: Patch -> FL Patch -> Maybe (FL Patch)
608 put_before p1 (p2:>:p2s) =
609 do p2':<p1' <- commutex (invert p1:<p2)
610 commutex (p1:<p2')
611 (p2' :>:) `fmap` put_before p1' p2s
612 put_before _ NilFL = Just NilFL
613 #endif
614 \end{code}
616 \section{Conflicts}
618 There are a couple of simple constraints on the routine which determines
619 how to resolve two conflicting patches (which is called `glump'). These
620 must be satisfied in order that the result of a series of merges is always
621 independent of their order. Firstly, the output of glump cannot change
622 when the order of the two conflicting patches is switched. If it did, then
623 commuting the merger could change the resulting patch, which would be bad.
624 Secondly, the result of the merge of three (or more) conflicting patches
625 cannot depend on the order in which the merges are performed.
627 The conflict resolution code (glump) begins by ``unravelling'' the merger
628 into a set of sequences of patches. Each sequence of patches corresponds
629 to one non-conflicted patch that got merged together with the others. The
630 result of the unravelling of a series of merges must obviously be
631 independent of the order in which those merges are performed. This
632 unravelling code (which uses the unwind code mentioned above) uses probably
633 the second most complicated algorithm. Fortunately, if we can successfully
634 unravel the merger, almost any function of the unravelled merger satisfies
635 the two constraints mentioned above that the conflict resolution code must
636 satisfy.
638 \begin{code}
639 instance Conflict Patch where
640 commute_no_conflicts (x:>y) = do x' :< y' <- commute_no_merger (y :< x)
641 return (y':>x')
642 #ifndef GADT_WITNESSES
643 resolve_conflicts patch = rcs NilFL $ reverseFL $ flattenFL patch
644 where rcs :: FL Patch C(w y) -> RL Patch C(x y) -> [[Sealed (FL Prim C(w))]]
645 rcs _ NilRL = []
646 rcs passedby (p@(Merger _ _ _ _):<:ps) =
647 case commute_no_merger (join_patchesFL passedby:<p) of
648 Just (p'@(Merger _ _ p1 p2):<_) ->
649 (map Sealed $ nubBy unsafeCompare $ effect (glump09 p1 p2) : unravel p')
650 : rcs (p :>: passedby) ps
651 Nothing -> rcs (p :>: passedby) ps
652 _ -> impossible
653 rcs passedby (p:<:ps) = seq passedby $
654 rcs (p :>: passedby) ps
655 #else
656 resolve_conflicts = bug "haven't defined resolve_conflicts with type witnesses."
657 #endif
659 public_unravel :: Patch C(x y) -> [Sealed (FL Prim C(y))]
660 #ifdef GADT_WITNESSES
661 public_unravel = bug "Haven't implemented public_unravel with type witnesses."
662 #else
663 public_unravel p = map Sealed $ unravel p
664 #endif
666 #ifndef GADT_WITNESSES
667 unravel :: Patch -> [FL Prim]
668 unravel p = nubBy unsafeCompare $
669 map (sort_coalesceFL . concatFL . mapFL_FL effect) $
670 get_supers $ map reverseRL $ new_ur p $ unwind p
672 get_supers :: [FL Patch] -> [FL Patch]
673 get_supers (x:xs) =
674 case filter (not.(x `is_superpatch_of`)) xs of
675 xs' -> if or $ map (`is_superpatch_of` x) xs'
676 then get_supers xs'
677 else x : get_supers xs'
678 get_supers [] = []
679 is_superpatch_of :: FL Patch -> FL Patch -> Bool
680 x `is_superpatch_of` y | lengthFL y > lengthFL x = False
681 x `is_superpatch_of` y = x `iso` y
682 where iso :: FL Patch -> FL Patch -> Bool
683 _ `iso` NilFL = True
684 NilFL `iso` _ = False
685 a `iso` (b:>:bs) =
686 case filter ((`unsafeCompare` b) . headFL) $
687 head_permutationsFL a of
688 ((_:>:as):_) -> as `iso` bs
689 [] -> False
690 _ -> bug "bug in is_superpatch_of"
692 headFL :: FL a -> a
693 headFL (x:>:_) = x
694 headFL NilFL = bug "bad headFL"
696 merger :: String -> Patch -> Patch -> Patch
697 merger "0.0" p1 p2 = Merger undoit unwindings p1 p2
698 where fake_p = Merger identity NilRL p1 p2
699 unwindings = true_unwind fake_p
700 p = Merger identity unwindings p1 p2
701 undoit =
702 case (is_merger p1, is_merger p2) of
703 (True ,True ) -> join_patchesFL $ invertRL $ tailRL $ unwind p
704 where tailRL (_:<:t) = t
705 tailRL _ = impossible
706 (False,False) -> invert p1
707 (True ,False) -> join_patchesFL NilFL
708 (False,True ) -> join_patchesFL (invert p1 :>: merger_undo p2 :>: NilFL)
709 merger g _ _ =
710 error $ "Cannot handle mergers other than version 0.0\n"++g
711 ++ "\nPlease use darcs optimize --modernize with an older darcs."
713 glump09 :: Patch -> Patch -> Patch
714 glump09 p1 p2 = fromPrims $ unsafeUnseal $ mangle_unravelled $ map Sealed $ unravel $ merger "0.0" p1 p2
716 #endif
718 mangle_unravelled :: [Sealed (FL Prim C(x))] -> Sealed (FL Prim C(x))
719 mangle_unravelled pss = if only_hunks pss
720 then (:>: NilFL) `mapSeal` mangle_unravelled_hunks pss
721 else head pss
723 only_hunks :: [Sealed (FL Prim C(x))] -> Bool
724 only_hunks [] = False
725 only_hunks pss = fn2fp f /= "" && all oh pss
726 where f = get_a_filename pss
727 oh :: Sealed (FL Prim C(x)) -> Bool
728 oh (Sealed (p:>:ps)) = is_hunk p &&
729 [fn2fp f] == list_touched_files p &&
730 oh (Sealed ps)
731 oh (Sealed NilFL) = True
733 apply_hunks :: [Maybe B.ByteString] -> FL Prim C(x y) -> [Maybe B.ByteString]
734 apply_hunks ms (FP _ (Hunk l o n):>:ps) = apply_hunks (rls l ms) ps
735 where rls 1 mls = map Just n ++ drop (length o) mls
736 rls i (ml:mls) = ml : rls (i-1) mls
737 rls _ [] = bug "rls in apply_hunks"
738 apply_hunks ms NilFL = ms
739 apply_hunks _ (_:>:_) = impossible
741 get_old :: [Maybe B.ByteString] -> [Sealed (FL Prim C(x))] -> [Maybe B.ByteString]
742 get_old mls (ps:pss) = get_old (get_hunks_old mls ps) pss
743 get_old mls [] = mls
745 get_a_filename :: [Sealed (FL Prim C(x))] -> FileName
746 get_a_filename ((Sealed (FP f _:>:_)):_) = f
747 get_a_filename _ = fp2fn ""
749 get_hunks_old :: [Maybe B.ByteString] -> Sealed (FL Prim C(x))
750 -> [Maybe B.ByteString]
751 get_hunks_old mls (Sealed ps) =
752 apply_hunks (apply_hunks mls ps) (invert ps)
754 get_hunks_new :: [Maybe B.ByteString] -> Sealed (FL Prim C(x))
755 -> [Maybe B.ByteString]
756 get_hunks_new mls (Sealed ps) = apply_hunks mls ps
758 get_hunkline :: [[Maybe B.ByteString]] -> Int
759 get_hunkline = ghl 1
760 where ghl :: Int -> [[Maybe B.ByteString]] -> Int
761 ghl n pps =
762 if any (isJust . head) pps
763 then n
764 else ghl (n+1) $ map tail pps
766 make_chunk :: Int -> [Maybe B.ByteString] -> [B.ByteString]
767 make_chunk n mls = pull_chunk $ drop (n-1) mls
768 where pull_chunk (Just l:mls') = l : pull_chunk mls'
769 pull_chunk (Nothing:_) = []
770 pull_chunk [] = bug "should this be [] in pull_chunk?"
772 mangle_unravelled_hunks :: [Sealed (FL Prim C(x))] -> Sealed (Prim C(x))
773 --mangle_unravelled_hunks [[h1],[h2]] = Deal with simple cases handily?
774 mangle_unravelled_hunks pss =
775 if null nchs then bug "mangle_unravelled_hunks"
776 else Sealed (FP filename (Hunk l old new))
777 where oldf = get_old (repeat Nothing) pss
778 newfs = map (get_hunks_new oldf) pss
779 l = get_hunkline $ oldf : newfs
780 nchs = sort $ map (make_chunk l) newfs
781 filename = get_a_filename pss
782 old = make_chunk l oldf
783 new = [top] ++ concat (intersperse [middle] nchs) ++ [bottom]
784 top = BC.pack $ "v v v v v v v" ++ eol_c
785 middle = BC.pack $ "*************" ++ eol_c
786 bottom = BC.pack $ "^ ^ ^ ^ ^ ^ ^" ++ eol_c
787 eol_c = if any (\ps -> not (B.null ps) && BC.last ps == '\r') old
788 then "\r"
789 else ""
790 \end{code}
792 \begin{code}
793 instance Effect Patch where
794 effect p@(Merger _ _ _ _) = sort_coalesceFL $ effect $ merger_undo p
795 effect p@(Regrem _ _ _ _) = invert $ effect $ invert p
796 effect (ComP ps) = concatFL $ mapFL_FL effect ps
797 effect (PP p) = effect p
798 isHunk p = do PP p' <- return p
799 isHunk p'
801 modernize_patch :: Patch C(x y) -> Patch C(x y)
802 modernize_patch p@(Merger _ _ _ _) = fromPrims $ effect p
803 modernize_patch p@(Regrem _ _ _ _) = fromPrims $ effect p
804 modernize_patch (ComP ps) = ComP $ filtermv $ mapFL_FL modernize_patch ps
805 where filtermv :: FL Patch C(x y) -> FL Patch C(x y)
806 #ifndef GADT_WITNESSES
807 filtermv (PP (Move _ b):>:xs) | hasadd xs = filtermv xs
808 where hasadd (PP (FP b' AddFile):>:_) | b' == b = True
809 hasadd (PP (DP b' AddDir):>:_) | b' == b = True
810 hasadd (PP (FP b' RmFile):>:_) | b' == b = False
811 hasadd (PP (DP b' RmDir):>:_) | b' == b = False
812 hasadd (_:>:z) = hasadd z
813 hasadd NilFL = False
814 #endif
815 filtermv (x:>:xs) = x :>: filtermv xs
816 filtermv NilFL = NilFL
818 modernize_patch (PP p) = fromPrims $ modernizePrim p
820 instance FromPrims Patch where
821 fromPrims (p :>: NilFL) = PP p
822 fromPrims ps = join_patchesFL $ mapFL_FL PP ps
823 joinPatches = join_patchesFL
824 \end{code}
826 \begin{code}
827 #ifndef GADT_WITNESSES
828 new_ur :: Patch -> RL Patch -> [RL Patch]
829 new_ur p (Merger _ _ p1 p2 :<: ps) =
830 case filter ((`unsafeCompare` p1) . headRL) $ head_permutationsRL ps of
831 ((_:<:ps'):_) -> new_ur p (p1:<:ps') ++ new_ur p (p2:<:ps')
832 _ -> bugDoc $ text "in function new_ur"
833 $$ text "Original patch:"
834 $$ showPatch_ p
835 $$ text "Unwound:"
836 $$ vcat (mapRL showPatch_ $ unwind p)
838 new_ur op ps =
839 case filter (is_merger.headRL) $ head_permutationsRL ps of
840 [] -> [ps]
841 (ps':_) -> new_ur op ps'
843 headRL :: RL a -> a
844 headRL (x:<:_) = x
845 headRL _ = bug "bad headRL"
846 #endif
847 \end{code}
849 \begin{code}
851 instance Invert p => Invert (Named p) where
852 invert (NamedP n d p) = NamedP (invert_name n) (map invert_name d) (invert p)
853 identity = NamedP idpatchinfo [] identity
855 instance Invert Patch where
856 invert (Merger undo unwindings p1 p2)
857 = Regrem undo unwindings p1 p2
858 invert (Regrem undo unwindings p1 p2)
859 = Merger undo unwindings p1 p2
860 invert (PP p) = PP (invert p)
861 invert (ComP ps) = ComP $ invert ps
862 identity = ComP NilFL
864 instance MyEq Patch where
865 unsafeCompare = eq_patches
866 instance MyEq p => MyEq (Named p) where
867 unsafeCompare (NamedP n1 d1 p1) (NamedP n2 d2 p2) =
868 n1 == n2 && d1 == d2 && unsafeCompare p1 p2
870 eq_patches :: Patch C(x y) -> Patch C(w z) -> Bool
871 eq_patches (PP p1) (PP p2) = unsafeCompare p1 p2
872 eq_patches (ComP ps1) (ComP ps2)
873 = eq_FL eq_patches ps1 ps2
874 eq_patches (ComP NilFL) (PP Identity) = True
875 eq_patches (PP Identity) (ComP NilFL) = True
876 eq_patches (Merger _ _ p1a p1b) (Merger _ _ p2a p2b)
877 = eq_patches p1a p2a &&
878 eq_patches p1b p2b
879 eq_patches (Regrem _ _ p1a p1b) (Regrem _ _ p2a p2b)
880 = eq_patches p1a p2a &&
881 eq_patches p1b p2b
882 eq_patches _ _ = False
884 eq_FL :: (FORALL(b c d e) a C(b c) -> a C(d e) -> Bool)
885 -> FL a C(x y) -> FL a C(w z) -> Bool
886 eq_FL _ NilFL NilFL = True
887 eq_FL f (x:>:xs) (y:>:ys) = f x y && eq_FL f xs ys
888 eq_FL _ _ _ = False
890 \end{code}