% Copyright (C) 2002-2003,2007 David Roundy % % This program is free software; you can redistribute it and/or modify % it under the terms of the GNU General Public License as published by % the Free Software Foundation; either version 2, or (at your option) % any later version. % % This program is distributed in the hope that it will be useful, % but WITHOUT ANY WARRANTY; without even the implied warranty of % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the % GNU General Public License for more details. % % You should have received a copy of the GNU General Public License % along with this program; see the file COPYING. If not, write to % the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, % Boston, MA 02110-1301, USA. \section{Patch relationships} \begin{code} {-# OPTIONS_GHC -cpp -fglasgow-exts #-} #include "gadts.h" module Darcs.Patch.Prim ( Prim(..), IsConflictedPrim(IsC), ConflictState(..), showPrim, DirPatchType(..), FilePatchType(..), CommuteFunction, Perhaps(..), null_patch, nullP, is_null_patch, is_identity, formatFileName, FileNameFormat(..), adddir, addfile, binary, changepref, hunk, move, rmdir, rmfile, tokreplace, is_addrmfile, is_addfile, is_hunk, is_binary, is_setpref, is_similar, is_adddir, is_addrmdir, is_filepatch, canonize, try_to_shrink, modernizePrim, subcommutes, sort_coalesceFL, join, applyBinary, try_tok_internal, try_shrinking_inverse, FromPrim(..), FromPrims(..), ToFromPrim(..), Conflict(..), Effect(..), commute_no_conflictsFL, commute_no_conflictsRL ) where import Prelude hiding ( pi ) import Control.Monad ( MonadPlus, msum, mzero, mplus ) import Data.Maybe ( isNothing ) #ifndef GADT_WITNESSES import Data.Map ( toList, fromListWith, mapWithKey ) import Data.List ( foldl' ) #endif import FastPackedString ( PackedString, lengthPS, dropPS, packString, unpackPS, substrPS, breakPS, concatPS, takePS, fromPS2Hex, nullPS ) import FileName ( FileName, fn2ps, fn2fp, fp2fn, norm_path, movedirfilename, encode_white ) import Darcs.Patch.Ordered import Darcs.Sealed ( Sealed, unseal ) import Darcs.Patch.Patchy ( Invert(..), Commute(..) ) import Darcs.Patch.Permutations () -- for Invert instance of FL import Darcs.SlurpDirectory ( FileContents ) import Darcs.Show import Darcs.Utils ( nubsort ) import Lcs ( getChanges ) import RegChars ( regChars ) import Printer ( Doc, vcat, packedString, Color(Cyan,Magenta), lineColor, text, userchunk, invisibleText, invisiblePS, blueText, ($$), (<+>), (<>), prefix, userchunkPS, ) import GHC.Base (unsafeCoerce#) #include "impossible.h" data Prim C(x y) where Move :: !FileName -> !FileName -> Prim C(x y) DP :: !FileName -> !(DirPatchType C(x y)) -> Prim C(x y) FP :: !FileName -> !(FilePatchType C(x y)) -> Prim C(x y) Split :: FL Prim C(x y) -> Prim C(x y) Identity :: Prim C(x x) ChangePref :: !String -> !String -> !String -> Prim C(x y) data FilePatchType C(x y) = RmFile | AddFile | Hunk !Int [PackedString] [PackedString] | TokReplace !String !String !String | Binary PackedString PackedString deriving (Eq,Ord) data DirPatchType C(x y) = RmDir | AddDir deriving (Eq,Ord) instance MyEq FilePatchType where unsafeCompare a b = a == unsafeCoerce# b instance MyEq DirPatchType where unsafeCompare a b = a == unsafeCoerce# b null_patch :: Prim C(x x) null_patch = Identity is_null_patch :: Prim C(x y) -> Bool is_null_patch (FP _ (Binary x y)) = nullPS x && nullPS y is_null_patch (FP _ (Hunk _ [] [])) = True is_null_patch Identity = True is_null_patch _ = False nullP :: Prim C(x y) -> EqCheck C(x y) nullP = sloppyIdentity is_identity :: Prim C(x y) -> EqCheck C(x y) is_identity (FP _ (Binary old new)) | old == new = unsafeCoerce# IsEq is_identity (FP _ (Hunk _ old new)) | old == new = unsafeCoerce# IsEq is_identity (FP _ (TokReplace _ old new)) | old == new = unsafeCoerce# IsEq is_identity (Move old new) | old == new = unsafeCoerce# IsEq is_identity Identity = IsEq is_identity _ = NotEq \end{code} %FIXME: The following code needs to be moved. It is a function %``is\_similar'' which tells you if two patches are in the same category %human-wise. Currently it just returns true if they are filepatches on the %same file. \begin{code} is_similar :: Prim C(x y) -> Prim C(a b) -> Bool is_similar (FP f _) (FP f' _) = f == f' is_similar (DP f _) (DP f' _) = f == f' is_similar _ _ = False is_addfile :: Prim C(x y) -> Bool is_addfile (FP _ AddFile) = True is_addfile _ = False is_adddir :: Prim C(x y) -> Bool is_adddir (DP _ AddDir) = True is_adddir _ = False is_addrmfile :: Prim C(x y) -> Bool is_addrmfile (FP _ AddFile) = True is_addrmfile (FP _ RmFile) = True is_addrmfile _ = False is_addrmdir :: Prim C(x y) -> Bool is_addrmdir (DP _ AddDir) = True is_addrmdir (DP _ RmDir) = True is_addrmdir _ = False is_hunk :: Prim C(x y) -> Bool is_hunk (FP _ (Hunk _ _ _)) = True is_hunk _ = False is_binary :: Prim C(x y) -> Bool is_binary (FP _ (Binary _ _)) = True is_binary _ = False is_setpref :: Prim C(x y) -> Bool is_setpref (ChangePref _ _ _) = True is_setpref _ = False \end{code} \begin{code} addfile :: FilePath -> Prim C(x y) rmfile :: FilePath -> Prim C(x y) adddir :: FilePath -> Prim C(x y) rmdir :: FilePath -> Prim C(x y) move :: FilePath -> FilePath -> Prim C(x y) changepref :: String -> String -> String -> Prim C(x y) hunk :: FilePath -> Int -> [PackedString] -> [PackedString] -> Prim C(x y) tokreplace :: FilePath -> String -> String -> String -> Prim C(x y) binary :: FilePath -> PackedString -> PackedString -> Prim C(x y) evalargs :: (a -> b -> c) -> a -> b -> c evalargs f x y = (f $! x) $! y addfile f = FP (fp2fn $ n_fn f) AddFile rmfile f = FP (fp2fn $ n_fn f) RmFile adddir d = DP (fp2fn $ n_fn d) AddDir rmdir d = DP (fp2fn $ n_fn d) RmDir move f f' = Move (fp2fn $ n_fn f) (fp2fn $ n_fn f') changepref p f t = ChangePref p f t hunk f line old new = evalargs FP (fp2fn $ n_fn f) (Hunk line old new) tokreplace f tokchars old new = evalargs FP (fp2fn $ n_fn f) (TokReplace tokchars old new) binary f old new = FP (fp2fn $! n_fn f) $ Binary old new \end{code} \begin{code} n_fn :: FilePath -> FilePath n_fn f = "./"++(fn2fp $ norm_path $ fp2fn f) \end{code} The simplest relationship between two patches is that of ``sequential'' patches, which means that the context of the second patch (the one on the left) consists of the first patch (on the right) plus the context of the first patch. The composition of two patches (which is also a patch) refers to the patch which is formed by first applying one and then the other. The composition of two patches, $P_1$ and $P_2$ is represented as $P_2P_1$, where $P_1$ is to be applied first, then $P_2$\footnote{This notation is inspired by the notation of matrix multiplication or the application of operators upon a Hilbert space. In the algebra of patches, there is multiplication (i.e.\ composition), which is associative but not commutative, but no addition or subtraction.} There is one other very useful relationship that two patches can have, which is to be parallel patches, which means that the two patches have an identical context (i.e.\ their representation applies to identical trees). This is represented by $P_1\parallel P_2$. Of course, two patches may also have no simple relationship to one another. In that case, if you want to do something with them, you'll have to manipulate them with respect to other patches until they are either in sequence or in parallel. The most fundamental and simple property of patches is that they must be invertible. The inverse of a patch is described by: $P^{ -1}$. In the darcs implementation, the inverse is required to be computable from knowledge of the patch only, without knowledge of its context, but that (although convenient) is not required by the theory of patches. \begin{dfn} The inverse of patch $P$ is $P^{ -1}$, which is the ``simplest'' patch for which the composition \( P^{ -1} P \) makes no changes to the tree. \end{dfn} Using this definition, it is trivial to prove the following theorem relating to the inverse of a composition of two patches. \begin{thm} The inverse of the composition of two patches is \[ (P_2 P_1)^{ -1} = P_1^{ -1} P_2^{ -1}. \] \end{thm} Moreover, it is possible to show that the right inverse of a patch is equal to its left inverse. In this respect, patches continue to be analogous to square matrices, and indeed the proofs relating to these properties of the inverse are entirely analogous to the proofs in the case of matrix multiplication. The compositions proofs can also readily be extended to the composition of more than two patches. \begin{code} instance Invert Prim where invert Identity = Identity invert (FP f RmFile) = FP f AddFile invert (FP f AddFile) = FP f RmFile invert (FP f (Hunk line old new)) = FP f $ Hunk line new old invert (FP f (TokReplace t o n)) = FP f $ TokReplace t n o invert (FP f (Binary o n)) = FP f $ Binary n o invert (DP d RmDir) = DP d AddDir invert (DP d AddDir) = DP d RmDir invert (Move f f') = Move f' f invert (ChangePref p f t) = ChangePref p t f invert (Split ps) = Split $ invert ps identity = Identity sloppyIdentity Identity = IsEq sloppyIdentity _ = NotEq \end{code} \begin{code} instance Show (Prim C(x y)) where showsPrec d (Move fn1 fn2) = showParen (d > app_prec) $ showString "Move " . showsPrec (app_prec + 1) fn1 . showString " " . showsPrec (app_prec + 1) fn2 showsPrec d (DP fn dp) = showParen (d > app_prec) $ showString "DP " . showsPrec (app_prec + 1) fn . showString " " . showsPrec (app_prec + 1) dp showsPrec d (FP fn fp) = showParen (d > app_prec) $ showString "FP " . showsPrec (app_prec + 1) fn . showString " " . showsPrec (app_prec + 1) fp showsPrec d (Split l) = showParen (d > app_prec) $ showString "Split " . showsPrec (app_prec + 1) l showsPrec _ Identity = showString "Identity" showsPrec d (ChangePref p f t) = showParen (d > app_prec) $ showString "ChangePref " . showsPrec (app_prec + 1) p . showString " " . showsPrec (app_prec + 1) f . showString " " . showsPrec (app_prec + 1) t instance Show2 Prim where showsPrec2 = showsPrec instance Show (FilePatchType C(x y)) where showsPrec _ RmFile = showString "RmFile" showsPrec _ AddFile = showString "AddFile" showsPrec d (Hunk line old new) | all ((==1) . length . unpackPS) old && all ((==1) . length . unpackPS) new = showParen (d > app_prec) $ showString "Hunk " . showsPrec (app_prec + 1) line . showString " " . showsPrecC old . showString " " . showsPrecC new where showsPrecC [] = showString "[]" showsPrecC ss = showParen True $ showString "packStringLetters " . showsPrec (app_prec + 1) (map (head . unpackPS) ss) showsPrec d (Hunk line old new) = showParen (d > app_prec) $ showString "Hunk " . showsPrec (app_prec + 1) line . showString " " . showsPrec (app_prec + 1) old . showString " " . showsPrec (app_prec + 1) new showsPrec d (TokReplace t old new) = showParen (d > app_prec) $ showString "TokReplace " . showsPrec (app_prec + 1) t . showString " " . showsPrec (app_prec + 1) old . showString " " . showsPrec (app_prec + 1) new -- this case may not work usefully showsPrec d (Binary old new) = showParen (d > app_prec) $ showString "Binary " . showsPrec (app_prec + 1) old . showString " " . showsPrec (app_prec + 1) new instance Show (DirPatchType C(x y)) where showsPrec _ RmDir = showString "RmDir" showsPrec _ AddDir = showString "AddDir" {- instance Show (Prim C(x y)) where show p = renderString (showPrim p) ++ "\n" -} data FileNameFormat = OldFormat | NewFormat formatFileName :: FileNameFormat -> FileName -> Doc formatFileName OldFormat = packedString . fn2ps formatFileName NewFormat = text . encode_white . fn2fp showPrim :: FileNameFormat -> Prim C(a b) -> Doc showPrim x (FP f AddFile) = showAddFile x f showPrim x (FP f RmFile) = showRmFile x f showPrim x (FP f (Hunk line old new)) = showHunk x f line old new showPrim x (FP f (TokReplace t old new)) = showTok x f t old new showPrim x (FP f (Binary old new)) = showBinary x f old new showPrim x (DP d AddDir) = showAddDir x d showPrim x (DP d RmDir) = showRmDir x d showPrim x (Move f f') = showMove x f f' showPrim _ (ChangePref p f t) = showChangePref p f t showPrim x (Split ps) = showSplit x ps showPrim _ Identity = blueText "{}" \end{code} \paragraph{Add file} Add an empty file to the tree. \verb!addfile filename! \begin{code} showAddFile :: FileNameFormat -> FileName -> Doc showAddFile x f = blueText "addfile" <+> formatFileName x f \end{code} \paragraph{Remove file} Delete a file from the tree. \verb!rmfile filename! \begin{code} showRmFile :: FileNameFormat -> FileName -> Doc showRmFile x f = blueText "rmfile" <+> formatFileName x f \end{code} \paragraph{Move} Rename a file or directory. \verb!move oldname newname! \begin{code} showMove :: FileNameFormat -> FileName -> FileName -> Doc showMove x d d' = blueText "move" <+> formatFileName x d <+> formatFileName x d' \end{code} \paragraph{Change Pref} Change one of the preference settings. Darcs stores a number of simple string settings. Among these are the name of the test script and the name of the script that must be called prior to packing in a make dist. \begin{verbatim} changepref prefname oldval newval \end{verbatim} \begin{code} showChangePref :: String -> String -> String -> Doc showChangePref p f t = blueText "changepref" <+> text p $$ userchunk f $$ userchunk t \end{code} \paragraph{Add dir} Add an empty directory to the tree. \verb!adddir filename! \begin{code} showAddDir :: FileNameFormat -> FileName -> Doc showAddDir x d = blueText "adddir" <+> formatFileName x d \end{code} \paragraph{Remove dir} Delete a directory from the tree. \verb!rmdir filename! \begin{code} showRmDir :: FileNameFormat -> FileName -> Doc showRmDir x d = blueText "rmdir" <+> formatFileName x d \end{code} \paragraph{Hunk} Replace a hunk (set of contiguous lines) of text with a new hunk. \begin{verbatim} hunk FILE LINE# -LINE ... +LINE ... \end{verbatim} \begin{code} showHunk :: FileNameFormat -> FileName -> Int -> [PackedString] -> [PackedString] -> Doc showHunk x f line old new = blueText "hunk" <+> formatFileName x f <+> text (show line) $$ lineColor Magenta (prefix "-" (vcat $ map userchunkPS old)) $$ lineColor Cyan (prefix "+" (vcat $ map userchunkPS new)) \end{code} \paragraph{Token replace} Replace a token with a new token. Note that this format means that whitespace must not be allowed within a token. If you know of a practical application of whitespace within a token, let me know and I may change this. \begin{verbatim} replace FILENAME [REGEX] OLD NEW \end{verbatim} \begin{code} showTok :: FileNameFormat -> FileName -> String -> String -> String -> Doc showTok x f t o n = blueText "replace" <+> formatFileName x f <+> text "[" <> userchunk t <> text "]" <+> userchunk o <+> userchunk n \end{code} \paragraph{Binary file modification} Modify a binary file \begin{verbatim} binary FILENAME oldhex *HEXHEXHEX ... newhex *HEXHEXHEX ... \end{verbatim} \begin{code} showBinary :: FileNameFormat -> FileName -> PackedString -> PackedString -> Doc showBinary x f o n = blueText "binary" <+> formatFileName x f $$ invisibleText "oldhex" $$ (vcat $ map makeprintable $ break_every 78 $ fromPS2Hex o) $$ invisibleText "newhex" $$ (vcat $ map makeprintable $ break_every 78 $ fromPS2Hex n) where makeprintable ps = invisibleText "*" <> invisiblePS ps break_every :: Int -> PackedString -> [PackedString] break_every n ps | lengthPS ps < n = [ps] | otherwise = takePS n ps : break_every n (dropPS n ps) \end{code} \paragraph{Split patch [OBSOLETE!]} A split patch is similar to a composite patch but rather than being composed of several patches grouped together, it is created from one patch that has been split apart, typically through a merge or commutation. \begin{verbatim} ( (indented two) ) \end{verbatim} \begin{code} showSplit :: FileNameFormat -> FL Prim C(x y) -> Doc showSplit x ps = blueText "(" $$ vcat (mapFL (showPrim x) ps) $$ blueText ")" \end{code} \section{Commuting patches} \subsection{Composite patches} Composite patches are made up of a series of patches intended to be applied sequentially. They are represented by a list of patches, with the first patch in the list being applied first. \begin{code} commute_split :: CommuteFunction commute_split (Split patches :< patch) = toPerhaps $ do (p1 :< ps) <- cs (patches :< patch) case sort_coalesceFL ps of p :>: NilFL -> return (p1 :< p) ps' -> return (p1 :< Split ps') where cs :: ((FL Prim) :< Prim) C(x y) -> Maybe ((Prim :< (FL Prim)) C(x y)) cs (NilFL :< p1) = return (p1 :< NilFL) cs (p:>:ps :< p1) = do p1' :< p' <- commutex (p :< p1) p1'' :< ps' <- cs (ps :< p1') return (p1'' :< p':>:ps') commute_split _ = Unknown \end{code} \begin{code} try_to_shrink :: FL Prim C(x y) -> FL Prim C(x y) try_to_shrink = mapPrimFL try_harder_to_shrink mapPrimFL :: (FORALL(x y) FL Prim C(x y) -> FL Prim C(x y)) -> FL Prim C(w z) -> FL Prim C(w z) mapPrimFL f x = #ifdef GADT_WITNESSES f x #else case mapM toSimple $ mapFL id x of Just sx -> foldl' (+>+) NilFL $ map snd $ toList $ fmap f $ mapWithKey fromSimples $ fromListWith (flip (+>+)) $ map (\ (a,b) -> (a,b:>:NilFL)) sx Nothing -> f x data Simple C(x y) = SFP !(FilePatchType C(x y)) | SDP !(DirPatchType C(x y)) deriving ( Show ) toSimple :: Prim C(x y) -> Maybe (FileName, Simple C(x y)) toSimple (FP a b) = Just (a, SFP b) toSimple (DP a AddDir) = Just (a, SDP AddDir) toSimple (DP _ RmDir) = Nothing -- ordering is trickier with rmdir present toSimple (Move _ _) = Nothing toSimple (Split _) = Nothing toSimple Identity = Nothing toSimple (ChangePref _ _ _) = Nothing fromSimple :: FileName -> Simple C(x y) -> Prim C(x y) fromSimple a (SFP b) = FP a b fromSimple a (SDP b) = DP a b fromSimples :: FileName -> FL Simple C(x y) -> FL Prim C(x y) fromSimples a bs = mapFL_FL (fromSimple a) bs #endif try_harder_to_shrink :: FL Prim C(x y) -> FL Prim C(x y) try_harder_to_shrink x = try_to_shrink2 $ maybe x id (try_shrinking_inverse x) try_to_shrink2 :: FL Prim C(x y) -> FL Prim C(x y) try_to_shrink2 psold = let ps = sort_coalesceFL psold ps_shrunk = shrink_a_bit ps in if lengthFL ps_shrunk < lengthFL ps then try_to_shrink2 ps_shrunk else ps_shrunk try_shrinking_inverse :: FL Prim C(x y) -> Maybe (FL Prim C(x y)) try_shrinking_inverse (x:>:y:>:z) | IsEq <- invert x =\/= y = Just z | otherwise = case try_shrinking_inverse (y:>:z) of Nothing -> Nothing Just yz' -> Just $ case try_shrinking_inverse (x:>:yz') of Nothing -> x:>:yz' Just xyz' -> xyz' try_shrinking_inverse _ = Nothing shrink_a_bit :: FL Prim C(x y) -> FL Prim C(x y) shrink_a_bit NilFL = NilFL shrink_a_bit (p:>:ps) = case try_one NilRL p ps of Nothing -> p :>: shrink_a_bit ps Just ps' -> ps' try_one :: RL Prim C(w x) -> Prim C(x y) -> FL Prim C(y z) -> Maybe (FL Prim C(w z)) try_one _ _ NilFL = Nothing try_one sofar p (p1:>:ps) = case coalesce (p1 :< p) of Just p' -> Just (reverseRL sofar +>+ p':>:NilFL +>+ ps) Nothing -> case commutex (p1 :< p) of Nothing -> Nothing Just (p' :< p1') -> try_one (p1':<:sofar) p' ps sort_coalesceFL :: FL Prim C(x y) -> FL Prim C(x y) sort_coalesceFL = mapPrimFL sort_coalesceFL2 sort_coalesceFL2 :: FL Prim C(x y) -> FL Prim C(x y) sort_coalesceFL2 NilFL = NilFL sort_coalesceFL2 (x:>:xs) | IsEq <- nullP x = sort_coalesceFL2 xs sort_coalesceFL2 (x:>:xs) | IsEq <- is_identity x = sort_coalesceFL2 xs sort_coalesceFL2 (x:>:xs) = push_coalesce_patch x $ sort_coalesceFL2 xs push_coalesce_patch :: Prim C(x y) -> FL Prim C(y z) -> FL Prim C(x z) push_coalesce_patch new NilFL = new :>: NilFL push_coalesce_patch new ps@(p:>:ps') = case coalesce (p :< new) of Just new' | IsEq <- nullP new' -> ps' | otherwise -> push_coalesce_patch new' ps' Nothing -> if comparePrim new p == LT then new:>:ps else case commutex (p :< new) of Just (new' :< p') -> case push_coalesce_patch new' ps' of r | lengthFL r < 1 + lengthFL ps' -> push_coalesce_patch p' r r -> p' :>: r Nothing -> new:>:ps \end{code} \newcommand{\commutex}{\longleftrightarrow} \newcommand{\commutes}{\longleftrightarrow} The first way (of only two) to change the context of a patch is by commutation, which is the process of changing the order of two sequential patches. \begin{dfn} The commutation of patches $P_1$ and $P_2$ is represented by \[ P_2 P_1 \commutes {P_1}' {P_2}'. \] Here $P_1'$ is intended to describe the same change as $P_1$, with the only difference being that $P_1'$ is applied after $P_2'$ rather than before $P_2$. \end{dfn} The above definition is obviously rather vague, the reason being that what is the ``same change'' has not been defined, and we simply assume (and hope) that the code's view of what is the ``same change'' will match those of its human users. The `$\commutes$' operator should be read as something like the $==$ operator in C, indicating that the right hand side performs identical changes to the left hand side, but the two patches are in reversed order. When read in this manner, it is clear that commutation must be a reversible process, and indeed this means that commutation \emph{can} fail, and must fail in certain cases. For example, the creation and deletion of the same file cannot be commuted. When two patches fail to commutex, it is said that the second patch depends on the first, meaning that it must have the first patch in its context (remembering that the context of a patch is a set of patches, which is how we represent a tree). \footnote{The fact that commutation can fail makes a huge difference in the whole patch formalism. It may be possible to create a formalism in which commutation always succeeds, with the result of what would otherwise be a commutation that fails being something like a virtual particle (which can violate conservation of energy), and it may be that such a formalism would allow strict mathematical proofs (whereas those used in the current formalism are mostly only hand waving ``physicist'' proofs). However, I'm not sure how you'd deal with a request to delete a file that has not yet been created, for example. Obviously you'd need to create some kind of antifile, which would annihilate with the file when that file finally got created, but I'm not entirely sure how I'd go about doing this. $\ddot\frown$ So I'm sticking with my hand waving formalism.} %I should add that one using the inversion relationship of sequential %patches, one can avoid having to provide redundant definitions of %commutation. % There is another interesting property which is that a commutex's results % can't be affected by commuting another thingamabopper. \begin{code} is_in_directory :: FileName -> FileName -> Bool is_in_directory d f = iid (fn2fp d) (fn2fp f) where iid (cd:cds) (cf:cfs) | cd /= cf = False | otherwise = iid cds cfs iid [] ('/':_) = True iid [] [] = True -- Count directory itself as being in directory... iid _ _ = False data Perhaps a = Unknown | Failed | Succeeded a instance Monad Perhaps where (Succeeded x) >>= k = k x Failed >>= _ = Failed Unknown >>= _ = Unknown Failed >> _ = Failed (Succeeded _) >> k = k Unknown >> k = k return = Succeeded fail _ = Unknown instance MonadPlus Perhaps where mzero = Unknown Unknown `mplus` ys = ys Failed `mplus` _ = Failed (Succeeded x) `mplus` _ = Succeeded x toMaybe :: Perhaps a -> Maybe a toMaybe (Succeeded x) = Just x toMaybe _ = Nothing toPerhaps :: Maybe a -> Perhaps a toPerhaps (Just x) = Succeeded x toPerhaps Nothing = Failed clever_commute :: CommuteFunction -> CommuteFunction clever_commute c (p1: Succeeded x Failed -> Failed Unknown -> case c (invert p2 :< invert p1) of Succeeded (p1' :< p2') -> Succeeded (invert p2' :< invert p1') Failed -> Failed Unknown -> Unknown --clever_commute c (p1,p2) = c (p1,p2) `mplus` -- (case c (invert p2,invert p1) of -- Succeeded (p1', p2') -> Succeeded (invert p2', invert p1') -- Failed -> Failed -- Unknown -> Unknown) speedy_commute :: CommuteFunction speedy_commute (p1 :< p2) -- Deal with common case quickly! | p1_modifies /= Nothing && p2_modifies /= Nothing && p1_modifies /= p2_modifies = Succeeded (unsafeCoerce# p2 :< unsafeCoerce# p1) | otherwise = Unknown where p1_modifies = is_filepatch p1 p2_modifies = is_filepatch p2 everything_else_commute :: CommuteFunction everything_else_commute x = eec x where eec :: CommuteFunction eec (ChangePref p f t : z' :/\: y' Nothing -> error "Commute Prim merge" commutex x = toMaybe $ msum [speedy_commute x, everything_else_commute x ] -- Recurse on everything, these are potentially spoofed patches list_touched_files (Move f1 f2) = map fn2fp [f1, f2] list_touched_files (Split ps) = nubsort $ concat $ mapFL list_touched_files ps list_touched_files (FP f _) = [fn2fp f] list_touched_files (DP d _) = [fn2fp d] list_touched_files (ChangePref _ _ _) = [] list_touched_files Identity = [] is_filepatch :: Prim C(x y) -> Maybe FileName is_filepatch (FP f _) = Just f is_filepatch _ = Nothing \end{code} \begin{code} is_superdir :: FileName -> FileName -> Bool is_superdir d1 d2 = isd (fn2fp d1) (fn2fp d2) where isd s1 s2 = length s2 >= length s1 + 1 && take (length s1 + 1) s2 == s1 ++ "/" commute_filedir :: CommuteFunction commute_filedir (FP f1 p1 :< FP f2 p2) = if f1 /= f2 then Succeeded ( FP f2 (unsafeCoerce# p2) :< FP f1 (unsafeCoerce# p1) ) else commuteFP f1 (p1 :< p2) commute_filedir (DP d1 p1 :< DP d2 p2) = if (not $ is_in_directory d1 d2) && (not $ is_in_directory d2 d1) && d1 /= d2 then Succeeded ( DP d2 (unsafeCoerce# p2) :< DP d1 (unsafeCoerce# p1) ) else Failed commute_filedir (DP d dp :< FP f fp) = if not $ is_in_directory d f then Succeeded (FP f (unsafeCoerce# fp) :< DP d (unsafeCoerce# dp)) else Failed commute_filedir (Move d d' :< FP f2 p2) | f2 == d' = Failed | (p2 == AddFile || p2 == RmFile) && d == f2 = Failed | otherwise = Succeeded (FP (movedirfilename d d' f2) (unsafeCoerce# p2) :< Move d d') commute_filedir (Move d d' :< DP d2 p2) | is_superdir d2 d' || is_superdir d2 d = Failed | (p2 == AddDir || p2 == RmDir) && d == d2 = Failed | d2 == d' = Failed | otherwise = Succeeded (DP (movedirfilename d d' d2) (unsafeCoerce# p2) :< Move d d') commute_filedir (Move d d' :< Move f f') | f == d' || f' == d = Failed | f == d || f' == d' = Failed | d `is_superdir` f && f' `is_superdir` d' = Failed | otherwise = Succeeded (Move (movedirfilename d d' f) (movedirfilename d d' f') :< Move (movedirfilename f' f d) (movedirfilename f' f d')) commute_filedir _ = Unknown \end{code} \begin{code} type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y)) subcommutes :: [(String, CommuteFunction)] subcommutes = [("speedy_commute", speedy_commute), ("commute_filedir", clever_commute commute_filedir), ("commute_filepatches", clever_commute commute_filepatches), ("commutex", toPerhaps . commutex) ] \end{code} \paragraph{Merge} \newcommand{\merge}{\Longrightarrow} The second way one can change the context of a patch is by a {\bf merge} operation. A merge is an operation that takes two parallel patches and gives a pair of sequential patches. The merge operation is represented by the arrow ``\( \merge \)''. \begin{dfn}\label{merge_dfn} The result of a merge of two patches, $P_1$ and $P_2$ is one of two patches, $P_1'$ and $P_2'$, which satisfy the relationship: \[ P_2 \parallel P_1 \merge {P_2}' P_1 \commutex {P_1}' P_2. \] \end{dfn} Note that the sequential patches resulting from a merge are \emph{required} to commutex. This is an important consideration, as without it most of the manipulations we would like to perform would not be possible. The other important fact is that a merge \emph{cannot fail}. Naively, those two requirements seem contradictory. In reality, what it means is that the result of a merge may be a patch which is much more complex than any we have yet considered\footnote{Alas, I don't know how to prove that the two constraints even \emph{can} be satisfied. The best I have been able to do is to believe that they can be satisfied, and to be unable to find an case in which my implementation fails to satisfy them. These two requirements are the foundation of the entire theory of patches (have you been counting how many foundations it has?).}. \subsection{How merges are actually performed} The constraint that any two compatible patches (patches which can successfully be applied to the same tree) can be merged is actually quite difficult to apply. The above merge constraints also imply that the result of a series of merges must be independent of the order of the merges. So I'm putting a whole section here for the interested to see what algorithms I use to actually perform the merges (as this is pretty close to being the most difficult part of the code). The first case is that in which the two merges don't actually conflict, but don't trivially merge either (e.g.\ hunk patches on the same file, where the line number has to be shifted as they are merged). This kind of merge can actually be very elegantly dealt with using only commutation and inversion. There is a handy little theorem which is immensely useful when trying to merge two patches. \begin{thm}\label{merge_thm} $ P_2' P_1 \commutex P_1' P_2 $ if and only if $ P_1'^{ -1} P_2' \commutex P_2 P_1^{ -1} $, provided both commutations succeed. If either commutex fails, this theorem does not apply. \end{thm} This can easily be proven by multiplying both sides of the first commutation by $P_1'^{ -1}$ on the left, and by $P_1^{ -1}$ on the right. \begin{code} elegant_merge :: (Prim :\/: Prim) C(x y) -> Maybe ((Prim :/\: Prim) C(x y)) elegant_merge (p1 :\/: p2) = do p1':>ip2' <- commute (invert p2 :> p1) -- The following should be a redundant check p1o:>_ <- commute (p2 :> p1') IsEq <- return $ p1o =\/= p1 return (invert ip2' :/\: p1') \end{code} It can sometimes be handy to have a canonical representation of a given patch. We achieve this by defining a canonical form for each patch type, and a function ``{\tt canonize}'' which takes a patch and puts it into canonical form. This routine is used by the diff function to create an optimal patch (based on an LCS algorithm) from a simple hunk describing the old and new version of a file. \begin{code} canonize :: Prim C(x y) -> FL Prim C(x y) canonize (Split ps) = sort_coalesceFL ps canonize p | IsEq <- is_identity p = NilFL canonize (FP f (Hunk line old new)) = canonizeHunk f line old new canonize p = p :>: NilFL \end{code} A simpler, faster (and more generally useful) cousin of canonize is the coalescing function. This takes two sequential patches, and tries to turn them into one patch. This function is used to deal with ``split'' patches, which are created when the commutation of a primitive patch can only be represented by a composite patch. In this case the resulting composite patch must return to the original primitive patch when the commutation is reversed, which a split patch accomplishes by trying to coalesce its contents each time it is commuted. \begin{code} coalesce :: (Prim :< Prim) C(x y) -> Maybe (Prim C(x y)) coalesce (FP f1 _ :< FP f2 _) | f1 /= f2 = Nothing coalesce (p2 :< p1) | IsEq <- p2 =\/= invert p1 = Just null_patch coalesce (FP f1 p1 :< FP _ p2) = coalesceFilePrim f1 (p1 :< p2) -- f1 = f2 coalesce (Identity :< p) = Just p coalesce (p :< Identity) = Just p coalesce (Split NilFL :< p) = Just p coalesce (p :< Split NilFL) = Just p coalesce (Move a b :< Move b' a') | a == a' = Just $ Move b' b coalesce (Move a b :< FP f AddFile) | f == a = Just $ FP b AddFile coalesce (FP f RmFile :< Move a b) | b == f = Just $ FP a RmFile coalesce (ChangePref p f1 t1 :< ChangePref p2 f2 t2) | p == p2 && t2 == f1 = Just $ ChangePref p f2 t1 coalesce _ = Nothing join :: (Prim :> Prim) C(x y) -> Maybe (Prim C(x y)) join (x :> y) = coalesce (y :< x) \end{code} \subsection{File patches} A file patch is a patch which only modifies a single file. There are some rules which can be made about file patches in general, which makes them a handy class. For example, commutation of two filepatches is trivial if they modify different files. If they happen to modify the same file, we'll have to check whether or not they commutex. \begin{code} commute_filepatches :: CommuteFunction commute_filepatches (FP f1 p1 :< FP f2 p2) | f1 == f2 = commuteFP f1 (p1 :< p2) commute_filepatches _ = Unknown commuteFP :: FileName -> (FilePatchType :< FilePatchType) C(x y) -> Perhaps ((Prim :< Prim) C(x y)) commuteFP f (Hunk line1 [] [] :< p2) = seq f $ Succeeded (FP f (unsafeCoerceP p2) :< FP f (Hunk line1 [] [])) commuteFP f (p2 :< Hunk line1 [] []) = seq f $ Succeeded (FP f (Hunk line1 [] []) :< FP f (unsafeCoerceP p2)) commuteFP f (Hunk line1 old1 new1 :< Hunk line2 old2 new2) = seq f $ toPerhaps $ commuteHunk f (Hunk line1 old1 new1 :< Hunk line2 old2 new2) commuteFP f (TokReplace t o n :< Hunk line2 old2 new2) = seq f $ case try_tok_replace t o n old2 of Nothing -> Failed Just old2' -> case try_tok_replace t o n new2 of Nothing -> Failed Just new2' -> Succeeded (FP f (Hunk line2 old2' new2') :< FP f (TokReplace t o n)) commuteFP f (TokReplace t o n :< TokReplace t2 o2 n2) | seq f $ t /= t2 = Failed | o == o2 = Failed | n == o2 = Failed | o == n2 = Failed | n == n2 = Failed | otherwise = Succeeded (FP f (TokReplace t2 o2 n2) :< FP f (TokReplace t o n)) commuteFP _ _ = Unknown \end{code} \begin{code} coalesceFilePrim :: FileName -> (FilePatchType :< FilePatchType) C(x y) -> Maybe (Prim C(x y)) coalesceFilePrim f (Hunk line1 old1 new1 :< Hunk line2 old2 new2) = coalesceHunk f line1 old1 new1 line2 old2 new2 -- Token replace patches operating right after (or before) AddFile (RmFile) -- is an identity patch, as far as coalescing is concerned. coalesceFilePrim f (TokReplace _ _ _ :< AddFile) = Just $ FP f AddFile coalesceFilePrim f (RmFile :< TokReplace _ _ _) = Just $ FP f RmFile coalesceFilePrim f (TokReplace t1 o1 n1 :< TokReplace t2 o2 n2) | t1 == t2 && n2 == o1 = Just $ FP f $ TokReplace t1 o2 n1 coalesceFilePrim f (Binary m n :< Binary o m') | m == m' = Just $ FP f $ Binary o n coalesceFilePrim _ _ = Nothing \end{code} \subsection{Hunks} The hunk is the simplest patch that has a commuting pattern in which the commuted patches differ from the originals (rather than simple success or failure). This makes commuting or merging two hunks a tad tedious. \begin{code} commuteHunk :: FileName -> (FilePatchType :< FilePatchType) C(x y) -> Maybe ((Prim :< Prim) C(x y)) commuteHunk f (Hunk line2 old2 new2 :< Hunk line1 old1 new1) | seq f $ line1 + lengthnew1 < line2 = Just (FP f (Hunk line1 old1 new1) :< FP f (Hunk (line2 - lengthnew1 + lengthold1) old2 new2)) | line2 + lengthold2 < line1 = Just (FP f (Hunk (line1+ lengthnew2 - lengthold2) old1 new1) :< FP f (Hunk line2 old2 new2)) | line1 + lengthnew1 == line2 && lengthold2 /= 0 && lengthold1 /= 0 && lengthnew2 /= 0 && lengthnew1 /= 0 = Just (FP f (Hunk line1 old1 new1) :< FP f (Hunk (line2 - lengthnew1 + lengthold1) old2 new2)) | line2 + lengthold2 == line1 && lengthold2 /= 0 && lengthold1 /= 0 && lengthnew2 /= 0 && lengthnew1 /= 0 = Just (FP f (Hunk (line1 + lengthnew2 - lengthold2) old1 new1) :< FP f (Hunk line2 old2 new2)) | otherwise = seq f Nothing where lengthnew1 = length new1 lengthnew2 = length new2 lengthold1 = length old1 lengthold2 = length old2 commuteHunk _ _ = impossible \end{code} Hunks, of course, can be coalesced if they have any overlap. Note that coalesce code doesn't check if the two patches are conflicting. If you are coalescing two conflicting hunks, you've already got a bug somewhere. \begin{code} coalesceHunk :: FileName -> Int -> [PackedString] -> [PackedString] -> Int -> [PackedString] -> [PackedString] -> Maybe (Prim C(x y)) coalesceHunk f line1 old1 new1 line2 old2 new2 | line1 == line2 && lengthold1 < lengthnew2 = if take lengthold1 new2 /= old1 then Nothing else case drop lengthold1 new2 of extranew -> Just (FP f (Hunk line1 old2 (new1 ++ extranew))) | line1 == line2 && lengthold1 > lengthnew2 = if take lengthnew2 old1 /= new2 then Nothing else case drop lengthnew2 old1 of extraold -> Just (FP f (Hunk line1 (old2 ++ extraold) new1)) | line1 == line2 = if new2 == old1 then Just (FP f (Hunk line1 old2 new1)) else Nothing | line1 < line2 && lengthold1 >= line2 - line1 = case take (line2 - line1) old1 of extra-> coalesceHunk f line1 old1 new1 line1 (extra ++ old2) (extra ++ new2) | line1 > line2 && lengthnew2 >= line1 - line2 = case take (line1 - line2) new2 of extra-> coalesceHunk f line2 (extra ++ old1) (extra ++ new1) line2 old2 new2 | otherwise = Nothing where lengthold1 = length old1 lengthnew2 = length new2 \end{code} One of the most important pieces of code is the canonization of a hunk, which is where the ``diff'' algorithm is performed. This algorithm begins with chopping off the identical beginnings and endings of the old and new hunks. This isn't strictly necessary, but is a good idea, since this process is $O(n)$, while the primary diff algorithm is something considerably more painful than that\ldots\ actually the head would be dealt with all right, but with more space complexity. I think it's more efficient to just chop the head and tail off first. \begin{code} canonizeHunk :: FileName -> Int -> [PackedString] -> [PackedString] -> FL Prim C(x y) canonizeHunk f line old new | null old || null new = FP f (Hunk line old new) :>: NilFL canonizeHunk f line old new = make_holey f line $ getChanges old new make_holey :: FileName -> Int -> [(Int,[PackedString], [PackedString])] -> FL Prim C(x y) make_holey f line changes = unsafeMap_l2f (\ (l,o,n) -> FP f (Hunk (l+line) o n)) changes applyBinary :: PackedString -> PackedString -> FileContents -> Maybe FileContents applyBinary o n c | c == o = Just n applyBinary _ _ _ = Nothing \end{code} \begin{code} try_tok_replace :: String -> String -> String -> [PackedString] -> Maybe [PackedString] try_tok_replace t o n mss = mapM (fmap concatPS . try_tok_internal t (packString o) (packString n)) mss try_tok_internal :: String -> PackedString -> PackedString -> PackedString -> Maybe [PackedString] try_tok_internal _ o n s | isNothing (substrPS o s) && isNothing (substrPS n s) = Just [s] try_tok_internal t o n s = case breakPS (regChars t) s of (before,s') -> case breakPS (not . regChars t) s' of (tok,after) -> case try_tok_internal t o n after of Nothing -> Nothing Just rest -> if tok == o then Just $ before : n : rest else if tok == n then Nothing else Just $ before : tok : rest \end{code} \begin{code} modernizePrim :: Prim C(x y) -> FL Prim C(x y) modernizePrim (Split ps) = concatFL $ mapFL_FL modernizePrim ps modernizePrim p = p :>: NilFL \end{code} \begin{code} instance MyEq Prim where unsafeCompare (Move a b) (Move c d) = a == c && b == d unsafeCompare (DP d1 p1) (DP d2 p2) = d1 == d2 && p1 `unsafeCompare` p2 unsafeCompare (FP f1 fp1) (FP f2 fp2) = f1 == f2 && fp1 `unsafeCompare` fp2 unsafeCompare (Split ps1) (Split ps2) = eq_FL unsafeCompare ps1 ps2 unsafeCompare (ChangePref a1 b1 c1) (ChangePref a2 b2 c2) = c1 == c2 && b1 == b2 && a1 == a2 unsafeCompare Identity Identity = True unsafeCompare _ _ = False merge_orders :: Ordering -> Ordering -> Ordering merge_orders EQ x = x merge_orders LT _ = LT merge_orders GT _ = GT comparePrim :: Prim C(x y) -> Prim C(w z) -> Ordering comparePrim (Move a b) (Move c d) = compare (a, b) (c, d) comparePrim (Move _ _) _ = LT comparePrim _ (Move _ _) = GT comparePrim (DP d1 p1) (DP d2 p2) = compare (d1, p1) $ unsafeCoerceP (d2, p2) comparePrim (DP _ _) _ = LT comparePrim _ (DP _ _) = GT comparePrim (FP f1 fp1) (FP f2 fp2) = compare (f1, fp1) $ unsafeCoerceP (f2, fp2) comparePrim (FP _ _) _ = LT comparePrim _ (FP _ _) = GT comparePrim (Split ps1) (Split ps2) = compare_FL comparePrim ps1 $ unsafeCoerceP ps2 comparePrim (Split _) _ = LT comparePrim _ (Split _) = GT comparePrim Identity Identity = EQ comparePrim Identity _ = LT comparePrim _ Identity = GT comparePrim (ChangePref a1 b1 c1) (ChangePref a2 b2 c2) = compare (c1, b1, a1) (c2, b2, a2) eq_FL :: (FORALL(b c d e) a C(b c) -> a C(d e) -> Bool) -> FL a C(x y) -> FL a C(w z) -> Bool eq_FL _ NilFL NilFL = True eq_FL f (x:>:xs) (y:>:ys) = f x y && eq_FL f xs ys eq_FL _ _ _ = False compare_FL :: (FORALL(b c d e) a C(b c) -> a C(d e) -> Ordering) -> FL a C(x y) -> FL a C(w z) -> Ordering compare_FL _ NilFL NilFL = EQ compare_FL _ NilFL _ = LT compare_FL _ _ NilFL = GT compare_FL f (x:>:xs) (y:>:ys) = f x y `merge_orders` compare_FL f xs ys \end{code} \begin{code} class FromPrim p where fromPrim :: Prim C(x y) -> p C(x y) class FromPrim p => ToFromPrim p where toPrim :: p C(x y) -> Maybe (Prim C(x y)) class FromPrims p where fromPrims :: FL Prim C(x y) -> p C(x y) joinPatches :: FL p C(x y) -> p C(x y) instance FromPrim Prim where fromPrim = id instance ToFromPrim Prim where toPrim = Just . id instance FromPrim p => FromPrims (FL p) where fromPrims = mapFL_FL fromPrim joinPatches = concatFL instance FromPrim p => FromPrims (RL p) where fromPrims = reverseFL . mapFL_FL fromPrim joinPatches = concatRL . reverseFL class (Invert p, Commute p, Effect p) => Conflict p where list_conflicted_files :: p C(x y) -> [FilePath] list_conflicted_files p = nubsort $ concatMap (unseal list_touched_files) $ concat $ resolve_conflicts p resolve_conflicts :: p C(x y) -> [[Sealed (FL Prim C(y))]] resolve_conflicts _ = [] commute_no_conflicts :: (p :> p) C(x y) -> Maybe ((p :> p) C(x y)) commute_no_conflicts (x:>y) = do y':>x' <- commute (x:>y) y'':>ix'' <- commute (invert x :> y') IsEq <- return $ y'' =\/= y IsEq <- return $ ix'' =\/= invert x' return (y':>x') conflictedEffect :: p C(x y) -> [IsConflictedPrim] conflictedEffect x = case list_conflicted_files x of [] -> mapFL (IsC Okay) $ effect x _ -> mapFL (IsC Conflicted) $ effect x instance Conflict p => Conflict (FL p) where list_conflicted_files = nubsort . concat . mapFL list_conflicted_files resolve_conflicts NilFL = [] resolve_conflicts x = resolve_conflicts $ reverseFL x commute_no_conflicts (NilFL :> x) = Just (x :> NilFL) commute_no_conflicts (x :> NilFL) = Just (NilFL :> x) commute_no_conflicts (xs :> ys) = do ys' :> rxs' <- commute_no_conflictsRLFL (reverseFL xs :> ys) return $ ys' :> reverseRL rxs' conflictedEffect = concat . mapFL conflictedEffect instance Conflict p => Conflict (RL p) where list_conflicted_files = nubsort . concat . mapRL list_conflicted_files resolve_conflicts x = rcs x NilFL where rcs :: RL p C(x y) -> FL p C(y w) -> [[Sealed (FL Prim C(w))]] rcs NilRL _ = [] rcs (p:<:ps) passedby | (_:_) <- resolve_conflicts p = case commute_no_conflictsFL (p:>passedby) of Just (_:> p') -> resolve_conflicts p' ++ rcs ps (p:>:passedby) Nothing -> rcs ps (p:>:passedby) rcs (p:<:ps) passedby = seq passedby $ rcs ps (p:>:passedby) commute_no_conflicts (NilRL :> x) = Just (x :> NilRL) commute_no_conflicts (x :> NilRL) = Just (NilRL :> x) commute_no_conflicts (xs :> ys) = do ys' :> rxs' <- commute_no_conflictsRLFL (xs :> reverseRL ys) return $ reverseFL ys' :> rxs' conflictedEffect = concat . reverse . mapRL conflictedEffect data IsConflictedPrim where IsC :: !ConflictState -> !(Prim C(x y)) -> IsConflictedPrim data ConflictState = Okay | Conflicted | Duplicated deriving ( Eq, Ord, Show, Read) class Effect p where effect :: p C(x y) -> FL Prim C(x y) effect = reverseRL . effectRL effectRL :: p C(x y) -> RL Prim C(x y) effectRL = reverseFL . effect isHunk :: p C(x y) -> Maybe (Prim C(x y)) isHunk _ = Nothing instance Effect Prim where effect p | IsEq <- sloppyIdentity p = NilFL | otherwise = p :>: NilFL effectRL p | IsEq <- sloppyIdentity p = NilRL | otherwise = p :<: NilRL isHunk p = if is_hunk p then Just p else Nothing instance Conflict Prim instance Effect p => Effect (FL p) where effect p = concatFL $ mapFL_FL effect p effectRL p = concatRL $ mapRL_RL effectRL $ reverseFL p instance Effect p => Effect (RL p) where effect p = concatFL $ mapFL_FL effect $ reverseRL p effectRL p = concatRL $ mapRL_RL effectRL p commute_no_conflictsFL :: Conflict p => (p :> FL p) C(x y) -> Maybe ((FL p :> p) C(x y)) commute_no_conflictsFL (p :> NilFL) = Just (NilFL :> p) commute_no_conflictsFL (q :> p :>: ps) = do p' :> q' <- commute_no_conflicts (q :> p) ps' :> q'' <- commute_no_conflictsFL (q' :> ps) return (p' :>: ps' :> q'') commute_no_conflictsRL :: Conflict p => (RL p :> p) C(x y) -> Maybe ((p :> RL p) C(x y)) commute_no_conflictsRL (NilRL :> p) = Just (p :> NilRL) commute_no_conflictsRL (p :<: ps :> q) = do q' :> p' <- commute_no_conflicts (p :> q) q'' :> ps' <- commute_no_conflictsRL (ps :> q') return (q'' :> p' :<: ps') commute_no_conflictsRLFL :: Conflict p => (RL p :> FL p) C(x y) -> Maybe ((FL p :> RL p) C(x y)) commute_no_conflictsRLFL (NilRL :> ys) = Just (ys :> NilRL) commute_no_conflictsRLFL (xs :> NilFL) = Just (NilFL :> xs) commute_no_conflictsRLFL (xs :> y :>: ys) = do y' :> xs' <- commute_no_conflictsRL (xs :> y) ys' :> xs'' <- commute_no_conflictsRLFL (xs' :> ys) return (y' :>: ys' :> xs'') \end{code}