-- | -- Module : Darcs.Patch.Merge -- Maintainer : darcs-devel@darcs.net -- Stability : experimental -- Portability : portable module Darcs.Patch.Merge ( -- * Classes CleanMerge(..) , Merge(..) -- * Functions , selfMerger , swapMerger , mergerIdFL , mergerFLId , mergerFLFL , cleanMergeFL , mergeFL , swapMerge , swapCleanMerge , mergeList -- * Properties , prop_mergeSymmetric , prop_mergeCommute ) where import Control.Monad ( foldM ) import Darcs.Prelude import Darcs.Patch.Commute ( Commute(..) ) import Darcs.Patch.CommuteFn ( MergeFn, PartialMergeFn ) import Darcs.Patch.Invert ( Invert(..) ) import Darcs.Patch.Witnesses.Eq ( Eq2(..), isIsEq ) import Darcs.Patch.Witnesses.Ordered ( (:\/:)(..) , (:/\:)(..) , FL(..) , (:>)(..) , (+>+) ) import Darcs.Patch.Witnesses.Sealed ( Sealed(..) ) {- | Class of patches that can, possibly, be merged cleanly, that is, without conflict. Every patch type can be made an instance of 'CleanMerge' in a trivial way by defining @'cleanMerge' _ = 'Nothing'@, which vacuously conforms to all required laws. Instances should obey the following laws: [/symmetry/] prop> cleanMerge (p :\/: q) == Just (q' :/\: p') <=> cleanMerge (q :\/: p) == Just (p' :/\: q') If an instance @'Commute' p@ exists, then we also require [/merge-commute/] prop> cleanMerge (p :\/: q) == Just (q' :/\: p') ==> commute (p :> q') == Just (q :> p') that is, the two branches of a clean merge commute to each other. If an instance @'Invert' p@ exists, then we also require [/square-merge/] prop> cleanMerge (p :\/: q) == Just (q' :/\: p') => cleanMerge (invert p :\/: q') == Just (q :/\: invert p') Here is a picture that explains why we call this /square-merge/: > A---p--->X A<--p^---X > | | | | > | | | | > q q' => q q' > | | | | > v v v v > Y---p'-->B Y<--p'^--B -} class CleanMerge p where cleanMerge :: (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY) instance CleanMerge p => CleanMerge (FL p) where cleanMerge :: (:\/:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY) cleanMerge (FL p wZ wX NilFL :\/: FL p wZ wY x) = (:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY)) -> (:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY) forall a b. (a -> b) -> a -> b $ FL p wZ wY x FL p wZ wY -> FL p wY wY -> (:/\:) (FL p) (FL p) wZ wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: FL p wY wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL cleanMerge (FL p wZ wX x :\/: FL p wZ wY NilFL) = (:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ)) -> (:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ) forall a b. (a -> b) -> a -> b $ FL p wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p wX wX -> FL p wZ wX -> (:/\:) (FL p) (FL p) wX wZ forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: FL p wZ wX x cleanMerge ((p wZ wY x :>: FL p wY wX xs) :\/: FL p wZ wY ys) = do FL p wY wZ ys' :/\: p wY wZ x' <- (:\/:) p (FL p) wY wY -> Maybe ((:/\:) (FL p) p wY wY) forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p) cleanMergeFL (p wZ wY x p wZ wY -> FL p wZ wY -> (:\/:) p (FL p) wY wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL p wZ wY ys) FL p wZ wZ xs' :/\: FL p wX wZ ys'' <- (:\/:) (FL p) (FL p) wZ wX -> Maybe ((:/\:) (FL p) (FL p) wZ wX) forall (p :: * -> * -> *) wX wY. CleanMerge p => (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) cleanMerge (FL p wY wZ ys' FL p wY wZ -> FL p wY wX -> (:\/:) (FL p) (FL p) wZ wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL p wY wX xs) (:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY)) -> (:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY) forall a b. (a -> b) -> a -> b $ FL p wX wZ ys'' FL p wX wZ -> FL p wY wZ -> (:/\:) (FL p) (FL p) wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: (p wY wZ x' p wY wZ -> FL p wZ wZ -> FL p wY wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p wZ wZ xs') -- | Cleanly merge a single patch with an 'FL' of patches. cleanMergeFL :: CleanMerge p => PartialMergeFn p (FL p) cleanMergeFL :: PartialMergeFn p (FL p) cleanMergeFL (p wZ wX p :\/: FL p wZ wY NilFL) = (:/\:) (FL p) p wX wZ -> Maybe ((:/\:) (FL p) p wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) (FL p) p wX wZ -> Maybe ((:/\:) (FL p) p wX wZ)) -> (:/\:) (FL p) p wX wZ -> Maybe ((:/\:) (FL p) p wX wZ) forall a b. (a -> b) -> a -> b $ FL p wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p wX wX -> p wZ wX -> (:/\:) (FL p) p wX wZ forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p wZ wX p cleanMergeFL (p wZ wX p :\/: (p wZ wY x :>: FL p wY wY xs)) = do p wX wZ x' :/\: p wY wZ p' <- (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) forall (p :: * -> * -> *) wX wY. CleanMerge p => (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) cleanMerge (p wZ wX p p wZ wX -> p wZ wY -> (:\/:) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wY x) FL p wZ wZ xs' :/\: p wY wZ p'' <- (:\/:) p (FL p) wZ wY -> Maybe ((:/\:) (FL p) p wZ wY) forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p) cleanMergeFL (p wY wZ p' p wY wZ -> FL p wY wY -> (:\/:) p (FL p) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL p wY wY xs) (:/\:) (FL p) p wX wY -> Maybe ((:/\:) (FL p) p wX wY) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) (FL p) p wX wY -> Maybe ((:/\:) (FL p) p wX wY)) -> (:/\:) (FL p) p wX wY -> Maybe ((:/\:) (FL p) p wX wY) forall a b. (a -> b) -> a -> b $ (p wX wZ x' p wX wZ -> FL p wZ wZ -> FL p wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p wZ wZ xs') FL p wX wZ -> p wY wZ -> (:/\:) (FL p) p wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p wY wZ p'' {- | Patches that can always be merged, even if they conflict. Instances should obey the following laws: [/symmetry/] prop> merge (p :\/: q) == q' :/\: p' <=> merge (q :\/: p) == p' :/\: q' [/merge-commute/] prop> merge (p :\/: q) == q' :/\: p' ==> commute (p :> q') == Just (q :> p') that is, the two branches of a merge commute to each other. [/extension/] prop> cleanMerge (p :\/: q) == Just (q' :/\: p') => merge (p :\/: q) == q' :/\: p' that is, 'merge' is an extension of 'cleanMerge'. -} class CleanMerge p => Merge p where merge :: (p :\/: p) wX wY -> (p :/\: p) wX wY -- | Synonym for 'merge'. selfMerger :: Merge p => MergeFn p p selfMerger :: MergeFn p p selfMerger = (:\/:) p p wX wY -> (:/\:) p p wX wY forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge instance Merge p => Merge (FL p) where merge :: (:\/:) (FL p) (FL p) wX wY -> (:/\:) (FL p) (FL p) wX wY merge = MergeFn p p -> forall wX wY. (:\/:) (FL p) (FL p) wX wY -> (:/\:) (FL p) (FL p) wX wY forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn (FL p) (FL q) mergerFLFL MergeFn p p forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge mergeFL :: Merge p => (p :\/: FL p) wX wY -> (FL p :/\: p) wX wY mergeFL :: (:\/:) p (FL p) wX wY -> (:/\:) (FL p) p wX wY mergeFL = MergeFn p p -> MergeFn p (FL p) forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn p (FL q) mergerIdFL MergeFn p p forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge -- | Lift a merge function over @p :\/: q@ -- to a merge function over @p :\/: FL q@ mergerIdFL :: MergeFn p q -> MergeFn p (FL q) mergerIdFL :: MergeFn p q -> MergeFn p (FL q) mergerIdFL MergeFn p q _mergeFn (p wZ wX p :\/: FL q wZ wY NilFL) = FL q wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL q wX wX -> p wZ wX -> (:/\:) (FL q) p wX wZ forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p wZ wX p mergerIdFL MergeFn p q mergeFn (p wZ wX p :\/: (q wZ wY x :>: FL q wY wY xs)) = case (:\/:) p q wX wY -> (:/\:) q p wX wY MergeFn p q mergeFn (p wZ wX p p wZ wX -> q wZ wY -> (:\/:) p q wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: q wZ wY x) of q wX wZ x' :/\: p wY wZ p' -> case MergeFn p q -> (:\/:) p (FL q) wZ wY -> (:/\:) (FL q) p wZ wY forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn p (FL q) mergerIdFL MergeFn p q mergeFn (p wY wZ p' p wY wZ -> FL q wY wY -> (:\/:) p (FL q) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL q wY wY xs) of FL q wZ wZ xs' :/\: p wY wZ p'' -> (q wX wZ x' q wX wZ -> FL q wZ wZ -> FL q wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL q wZ wZ xs') FL q wX wZ -> p wY wZ -> (:/\:) (FL q) p wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p wY wZ p'' -- | Lift a merge function over @p :\/: q@ -- to a merge function over @FL p :\/: q@ mergerFLId :: MergeFn p q -> MergeFn (FL p) q mergerFLId :: MergeFn p q -> MergeFn (FL p) q mergerFLId MergeFn p q mergeFn = MergeFn q (FL p) -> MergeFn (FL p) q forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn q p swapMerger (MergeFn q p -> MergeFn q (FL p) forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn p (FL q) mergerIdFL (MergeFn p q -> MergeFn q p forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn q p swapMerger MergeFn p q mergeFn)) -- | Lift a merge function over @p :\/: q@ -- to a merge function over @FL p :\/: FL q@ mergerFLFL :: MergeFn p q -> MergeFn (FL p) (FL q) mergerFLFL :: MergeFn p q -> MergeFn (FL p) (FL q) mergerFLFL MergeFn p q mergeFn = MergeFn (FL p) q -> MergeFn (FL p) (FL q) forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn p (FL q) mergerIdFL (MergeFn p q -> MergeFn (FL p) q forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn (FL p) q mergerFLId MergeFn p q mergeFn) -- | Swap the two patches, 'merge', then swap again. Used to exploit -- 'prop_mergeSymmetric' when defining 'merge'. swapMerge :: Merge p => (p :\/: p) wX wY -> (p :/\: p) wX wY swapMerge :: (:\/:) p p wX wY -> (:/\:) p p wX wY swapMerge = MergeFn p p -> MergeFn p p forall (p :: * -> * -> *) (q :: * -> * -> *). MergeFn p q -> MergeFn q p swapMerger MergeFn p p forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge -- | Swap the two patches, apply an arbitrary merge function, then swap again. swapMerger :: MergeFn p q -> MergeFn q p swapMerger :: MergeFn p q -> MergeFn q p swapMerger MergeFn p q mergeFn (q wZ wX x :\/: p wZ wY y) = case (:\/:) p q wY wX -> (:/\:) q p wY wX MergeFn p q mergeFn (p wZ wY y p wZ wY -> q wZ wX -> (:\/:) p q wY wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: q wZ wX x) of q wY wZ x' :/\: p wX wZ y' -> p wX wZ y' p wX wZ -> q wY wZ -> (:/\:) p q wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: q wY wZ x' -- | Swap the two patches, 'cleanMerge', then swap again. Used to exploit -- 'prop_cleanMergeSymmetric' when defining 'cleanMerge'. swapCleanMerge :: CleanMerge p => (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY) swapCleanMerge :: (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) swapCleanMerge (p wZ wX x :\/: p wZ wY y) = do p wY wZ x' :/\: p wX wZ y' <- (:\/:) p p wY wX -> Maybe ((:/\:) p p wY wX) forall (p :: * -> * -> *) wX wY. CleanMerge p => (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) cleanMerge (p wZ wY y p wZ wY -> p wZ wX -> (:\/:) p p wY wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wX x) (:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY) forall (m :: * -> *) a. Monad m => a -> m a return ((:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY)) -> (:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY) forall a b. (a -> b) -> a -> b $ p wX wZ y' p wX wZ -> p wY wZ -> (:/\:) p p wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p wY wZ x' -- | Combine a list of patch sequences, all starting at the same state, into a -- single sequence that also starts at the same state, using cleanMerge. -- If the merge fails, we return the two sequences that -- could not be merged so we can issue more detailed error messages. mergeList :: CleanMerge p => [Sealed (FL p wX)] -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX)) mergeList :: [Sealed (FL p wX)] -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX)) mergeList = (Sealed (FL p wX) -> Sealed (FL p wX) -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))) -> Sealed (FL p wX) -> [Sealed (FL p wX)] -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX)) forall (t :: * -> *) (m :: * -> *) b a. (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b foldM Sealed (FL p wX) -> Sealed (FL p wX) -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX)) forall (a :: * -> * -> *) wZ. CleanMerge a => Sealed (FL a wZ) -> Sealed (FL a wZ) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)) mergeTwo (FL p wX wX -> Sealed (FL p wX) forall (a :: * -> *) wX. a wX -> Sealed a Sealed FL p wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL) where mergeTwo :: Sealed (FL a wZ) -> Sealed (FL a wZ) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)) mergeTwo (Sealed FL a wZ wX ps) (Sealed qs) = case (:\/:) (FL a) (FL a) wX wX -> Maybe ((:/\:) (FL a) (FL a) wX wX) forall (p :: * -> * -> *) wX wY. CleanMerge p => (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY) cleanMerge (FL a wZ wX ps FL a wZ wX -> FL a wZ wX -> (:\/:) (FL a) (FL a) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL a wZ wX qs) of Just (FL a wX wZ qs' :/\: FL a wX wZ _) -> Sealed (FL a wZ) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)) forall a b. b -> Either a b Right (Sealed (FL a wZ) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))) -> Sealed (FL a wZ) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)) forall a b. (a -> b) -> a -> b $ FL a wZ wZ -> Sealed (FL a wZ) forall (a :: * -> *) wX. a wX -> Sealed a Sealed (FL a wZ wZ -> Sealed (FL a wZ)) -> FL a wZ wZ -> Sealed (FL a wZ) forall a b. (a -> b) -> a -> b $ FL a wZ wX ps FL a wZ wX -> FL a wX wZ -> FL a wZ wZ forall (a :: * -> * -> *) wX wY wZ. FL a wX wY -> FL a wY wZ -> FL a wX wZ +>+ FL a wX wZ qs' Maybe ((:/\:) (FL a) (FL a) wX wX) Nothing -> (Sealed (FL a wZ), Sealed (FL a wZ)) -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)) forall a b. a -> Either a b Left (FL a wZ wX -> Sealed (FL a wZ) forall (a :: * -> *) wX. a wX -> Sealed a Sealed FL a wZ wX ps, FL a wZ wX -> Sealed (FL a wZ) forall (a :: * -> *) wX. a wX -> Sealed a Sealed FL a wZ wX qs) -- | This function serves no purpose except to demonstrate how merge together -- with the square commute law allows us to commute any pair of adjacent -- patches. -- Note that using this function introduces inverse conflictors if the regular -- commute would fail. This is problematic because it invalidates another -- global invariant we rely on, namely that we can always drop (obliterate or -- amend) patches from the end of a repo. This is because inverse conflictors -- contain references to patches that come after it, so dropping them would -- make the inverse conflictor inconsistent. _forceCommute :: (Commute p, Merge p, Invert p) => (p :> p) wX wY -> (p :> p) wX wY _forceCommute :: (:>) p p wX wY -> (:>) p p wX wY _forceCommute (p wX wZ p :> p wZ wY q) = case (:>) p p wX wY -> Maybe ((:>) p p wX wY) forall (p :: * -> * -> *) wX wY. Commute p => (:>) p p wX wY -> Maybe ((:>) p p wX wY) commute (p wX wZ p p wX wZ -> p wZ wY -> (:>) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wZ wY q) of Just (p wX wZ q' :> p wZ wY p') -> p wX wZ q' p wX wZ -> p wZ wY -> (:>) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wZ wY p' Maybe ((:>) p p wX wY) Nothing -> case (:\/:) p p wX wY -> (:/\:) p p wX wY forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge (p wX wZ -> p wZ wX forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert p wX wZ p p wZ wX -> p wZ wY -> (:\/:) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wY q) of p wX wZ q' :/\: p wY wZ ip' -> p wX wZ q' p wX wZ -> p wZ wY -> (:>) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wY wZ -> p wZ wY forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert p wY wZ ip' -- | Whether the given pair of patches satisfies the /symmetry/ law. prop_mergeSymmetric :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool prop_mergeSymmetric :: (:\/:) p p wX wY -> Bool prop_mergeSymmetric (p wZ wX p :\/: p wZ wY q) = case (:\/:) p p wX wY -> (:/\:) p p wX wY forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge (p wZ wX p p wZ wX -> p wZ wY -> (:\/:) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wY q) of p wX wZ q' :/\: p wY wZ p' -> case (:\/:) p p wY wX -> (:/\:) p p wY wX forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge (p wZ wY q p wZ wY -> p wZ wX -> (:\/:) p p wY wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wX p) of p wY wZ p'' :/\: p wX wZ q'' -> EqCheck wZ wZ -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wX wZ q' p wX wZ -> p wX wZ -> EqCheck wZ wZ forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= p wX wZ q'') Bool -> Bool -> Bool && EqCheck wZ wZ -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wY wZ p' p wY wZ -> p wY wZ -> EqCheck wZ wZ forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= p wY wZ p'') -- | Whether the given pair of patches satisfies the /merge-commute/ law. prop_mergeCommute :: (Commute p, Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool prop_mergeCommute :: (:\/:) p p wX wY -> Bool prop_mergeCommute (p wZ wX p :\/: p wZ wY q) = case (:\/:) p p wX wY -> (:/\:) p p wX wY forall (p :: * -> * -> *) wX wY. Merge p => (:\/:) p p wX wY -> (:/\:) p p wX wY merge (p wZ wX p p wZ wX -> p wZ wY -> (:\/:) p p wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p wZ wY q) of p wX wZ q' :/\: p wY wZ p' -> case (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ) forall (p :: * -> * -> *) wX wY. Commute p => (:>) p p wX wY -> Maybe ((:>) p p wX wY) commute (p wZ wX p p wZ wX -> p wX wZ -> (:>) p p wZ wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wX wZ q') of Maybe ((:>) p p wZ wZ) Nothing -> Bool False Just (p wZ wZ q'' :> p wZ wZ p'') -> EqCheck wZ wY -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wZ wZ q'' p wZ wZ -> p wZ wY -> EqCheck wZ wY forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= p wZ wY q) Bool -> Bool -> Bool && EqCheck wZ wY -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wZ wZ p'' p wZ wZ -> p wY wZ -> EqCheck wZ wY forall (p :: * -> * -> *) wA wC wB. Eq2 p => p wA wC -> p wB wC -> EqCheck wA wB =/\= p wY wZ p') Bool -> Bool -> Bool && case (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ) forall (p :: * -> * -> *) wX wY. Commute p => (:>) p p wX wY -> Maybe ((:>) p p wX wY) commute (p wZ wY q p wZ wY -> p wY wZ -> (:>) p p wZ wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wY wZ p') of Maybe ((:>) p p wZ wZ) Nothing -> Bool False Just (p wZ wZ p'' :> p wZ wZ q'') -> EqCheck wZ wX -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wZ wZ p'' p wZ wZ -> p wZ wX -> EqCheck wZ wX forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= p wZ wX p) Bool -> Bool -> Bool && EqCheck wZ wX -> Bool forall wA wB. EqCheck wA wB -> Bool isIsEq (p wZ wZ q'' p wZ wZ -> p wX wZ -> EqCheck wZ wX forall (p :: * -> * -> *) wA wC wB. Eq2 p => p wA wC -> p wB wC -> EqCheck wA wB =/\= p wX wZ q')