module Darcs.Patch.Merge
(
CleanMerge(..)
, Merge(..)
, selfMerger
, swapMerger
, mergerIdFL
, mergerFLId
, mergerFLFL
, cleanMergeFL
, mergeFL
, swapMerge
, swapCleanMerge
, mergeList
, 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 CleanMerge p where
cleanMerge :: (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY)
instance CleanMerge p => CleanMerge (FL p) where
cleanMerge :: forall wX wY.
(:\/:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY)
cleanMerge (FL p wZ wX
NilFL :\/: FL p wZ wY
x) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FL p wZ wY
x forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
cleanMerge (FL p wZ wX
x :\/: FL p wZ wY
NilFL) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) wX. FL a wX wX
NilFL 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' <- forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p wZ wY
x 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'' <- forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL p wY wZ
ys' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wY wX
xs)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FL p wX wZ
ys'' forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: (p wY wZ
x' forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: FL p wZ wZ
xs')
cleanMergeFL :: CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL :: forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p wZ wX
p :\/: FL p wZ wY
NilFL) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) wX. FL a wX wX
NilFL 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' <- forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (p wZ wX
p 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'' <- forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p wY wZ
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wY wY
xs)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (p wX wZ
x' forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: FL p wZ wZ
xs') forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p wY wZ
p''
class CleanMerge p => Merge p where
merge :: (p :\/: p) wX wY -> (p :/\: p) wX wY
selfMerger :: Merge p => MergeFn p p
selfMerger :: forall (p :: * -> * -> *). Merge p => MergeFn p p
selfMerger = forall (p :: * -> * -> *). Merge p => MergeFn p p
merge
instance Merge p => Merge (FL p) where
merge :: forall wX wY.
(:\/:) (FL p) (FL p) wX wY -> (:/\:) (FL p) (FL p) wX wY
merge = forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) (FL q)
mergerFLFL forall (p :: * -> * -> *). Merge p => MergeFn p p
merge
mergeFL :: Merge p
=> (p :\/: FL p) wX wY
-> (FL p :/\: p) wX wY
mergeFL :: forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p (FL p) wX wY -> (:/\:) (FL p) p wX wY
mergeFL = forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL forall (p :: * -> * -> *). Merge p => MergeFn p p
merge
mergerIdFL :: MergeFn p q -> MergeFn p (FL q)
mergerIdFL :: forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL MergeFn p q
_mergeFn (p wZ wX
p :\/: FL q wZ wY
NilFL) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL 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 MergeFn p q
mergeFn (p wZ wX
p 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 forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL MergeFn p q
mergeFn (p wY wZ
p' 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' forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: FL q wZ wZ
xs') forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p wY wZ
p''
mergerFLId :: MergeFn p q -> MergeFn (FL p) q
mergerFLId :: forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) q
mergerFLId MergeFn p q
mergeFn = forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger (forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL (forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger MergeFn p q
mergeFn))
mergerFLFL :: MergeFn p q -> MergeFn (FL p) (FL q)
mergerFLFL :: forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) (FL q)
mergerFLFL MergeFn p q
mergeFn = forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL (forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) q
mergerFLId MergeFn p q
mergeFn)
swapMerge :: Merge p => (p :\/: p) wX wY -> (p :/\: p) wX wY
swapMerge :: forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
swapMerge = forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger forall (p :: * -> * -> *). Merge p => MergeFn p p
merge
swapMerger :: MergeFn p q -> MergeFn q p
swapMerger :: forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger MergeFn p q
mergeFn (q wZ wX
x :\/: p wZ wY
y) = case MergeFn p q
mergeFn (p wZ wY
y 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' forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: q wY wZ
x'
swapCleanMerge :: CleanMerge p => (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY)
swapCleanMerge :: forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) 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' <- forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (p wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p wZ wX
x)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ p wX wZ
y' forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p wY wZ
x'
mergeList :: CleanMerge p
=> [Sealed (FL p wX)]
-> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))
mergeList :: forall (p :: * -> * -> *) wX.
CleanMerge p =>
[Sealed (FL p wX)]
-> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))
mergeList = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {a :: * -> * -> *} {wX}.
CleanMerge a =>
Sealed (FL a wX)
-> Sealed (FL a wX)
-> Either (Sealed (FL a wX), Sealed (FL a wX)) (Sealed (FL a wX))
mergeTwo (forall (a :: * -> *) wX. a wX -> Sealed a
Sealed forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
where
mergeTwo :: Sealed (FL a wX)
-> Sealed (FL a wX)
-> Either (Sealed (FL a wX), Sealed (FL a wX)) (Sealed (FL a wX))
mergeTwo (Sealed FL a wX wX
ps) (Sealed FL a wX wX
qs) =
case forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL a wX wX
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL a wX wX
qs) of
Just (FL a wX wZ
qs' :/\: FL a wX wZ
_) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) wX. a wX -> Sealed a
Sealed forall a b. (a -> b) -> a -> b
$ FL a wX wX
ps 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 -> forall a b. a -> Either a b
Left (forall (a :: * -> *) wX. a wX -> Sealed a
Sealed FL a wX wX
ps, forall (a :: * -> *) wX. a wX -> Sealed a
Sealed FL a wX wX
qs)
_forceCommute :: (Commute p, Merge p, Invert p) => (p :> p) wX wY -> (p :> p) wX wY
_forceCommute :: forall (p :: * -> * -> *) wX wY.
(Commute p, Merge p, Invert p) =>
(:>) p p wX wY -> (:>) p p wX wY
_forceCommute (p wX wZ
p :> p wZ wY
q) =
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wX wZ
p 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' 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 forall (p :: * -> * -> *). Merge p => MergeFn p p
merge (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wZ
p 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' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wY wZ
ip'
prop_mergeSymmetric :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeSymmetric :: forall (p :: * -> * -> *) wX wY.
(Eq2 p, Merge p) =>
(:\/:) p p wX wY -> Bool
prop_mergeSymmetric (p wZ wX
p :\/: p wZ wY
q) =
case forall (p :: * -> * -> *). Merge p => MergeFn p p
merge (p wZ wX
p 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 forall (p :: * -> * -> *). Merge p => MergeFn p p
merge (p wZ wY
q 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'' ->
forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wX wZ
q' forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wX wZ
q'') Bool -> Bool -> Bool
&& forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wY wZ
p' forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wY wZ
p'')
prop_mergeCommute :: (Commute p, Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeCommute :: forall (p :: * -> * -> *) wX wY.
(Commute p, Eq2 p, Merge p) =>
(:\/:) p p wX wY -> Bool
prop_mergeCommute (p wZ wX
p :\/: p wZ wY
q) =
case forall (p :: * -> * -> *). Merge p => MergeFn p p
merge (p wZ wX
p 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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wX
p 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'') ->
forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wZ
q'' forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wZ wY
q) Bool -> Bool -> Bool
&& forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wZ
p'' forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= p wY wZ
p')
Bool -> Bool -> Bool
&&
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wY
q 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'') ->
forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wZ
p'' forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wZ wX
p) Bool -> Bool -> Bool
&& forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wZ wZ
q'' forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= p wX wZ
q')