module Darcs.Patch.Merge
(
Merge(..)
, selfMerger
, mergeFL
, naturalMerge
, prop_mergeSymmetric
, prop_mergeCommute
) where
import Darcs.Patch.Commute ( Commute(..) )
import Darcs.Patch.CommuteFn ( MergeFn )
import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), isIsEq )
import Darcs.Patch.Witnesses.Ordered
( (:\/:)(..)
, (:/\:)(..)
, FL(..)
, RL
, (:>)(..)
, reverseFL
, reverseRL
)
class Commute p => Merge p where
merge :: (p :\/: p) wX wY
-> (p :/\: p) wX wY
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 (NilFL :\/: x :: FL p wZ wY
x) = 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
merge (x :: FL p wZ wX
x :\/: NilFL) = 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
merge ((x :: p wZ wY
x:>:xs :: FL p wY wX
xs) :\/: ys :: FL p wZ wY
ys) = case (:\/:) p (FL p) wY wY -> (:/\:) (FL p) p wY wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p (FL p) wX wY -> (:/\:) (FL p) p wX wY
mergeFL (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) of
ys' :: FL p wY wZ
ys' :/\: x' :: p wY wZ
x' -> case (:\/:) (FL p) (FL p) wZ wX -> (:/\:) (FL p) (FL p) wZ wX
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge (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) of
xs' :: FL p wZ wZ
xs' :/\: ys'' :: FL p wX wZ
ys'' -> 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')
instance Merge p => Merge (RL p) where
merge :: (:\/:) (RL p) (RL p) wX wY -> (:/\:) (RL p) (RL p) wX wY
merge (x :: RL p wZ wX
x :\/: y :: RL p wZ wY
y) = case (:\/:) (FL p) (FL p) wX wY -> (:/\:) (FL p) (FL p) wX wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge (RL p wZ wX -> FL p wZ wX
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wX
x FL p wZ wX -> FL p wZ wY -> (:\/:) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: RL p wZ wY -> FL p wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wY
y) of
(ry' :: FL p wX wZ
ry' :/\: rx' :: FL p wY wZ
rx') -> FL p wX wZ -> RL p wX wZ
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wX wZ
ry' RL p wX wZ -> RL p wY wZ -> (:/\:) (RL p) (RL p) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: FL p wY wZ -> RL p wY wZ
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wY wZ
rx'
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 (p :: p wZ wX
p :\/: NilFL) = 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
mergeFL (p :: p wZ wX
p :\/: (x :: p wZ wY
x :>: xs :: FL p wY wY
xs)) = 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
x) of
x' :: p wX wZ
x' :/\: p' :: p wY wZ
p' -> case (:\/:) p (FL p) wZ wY -> (:/\:) (FL p) p wZ wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p (FL p) wX wY -> (:/\:) (FL p) p wX wY
mergeFL (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) of
xs' :: FL p wZ wZ
xs' :/\: p'' :: p wY wZ
p'' -> (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''
naturalMerge :: (Invert p, Commute p)
=> (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY)
naturalMerge :: (:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
naturalMerge (p :: p wZ wX
p :\/: q :: p wZ wY
q) = do
q' :: p wX wZ
q' :> ip' :: p wZ wY
ip' <- (:>) 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 wZ wX -> p wX wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wX
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)
(:>) p p wZ wZ
_ <- (:>) 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')
(:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p wX wZ
q' 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 wZ wY -> p wY wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wY
ip')
prop_mergeSymmetric :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeSymmetric :: (:\/:) p p wX wY -> Bool
prop_mergeSymmetric (p :: p wZ wX
p :\/: q :: 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
q' :: p wX wZ
q' :/\: p' :: 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'' :: p wY wZ
p'' :/\: q'' :: 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'')
prop_mergeCommute :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeCommute :: (:\/:) p p wX wY -> Bool
prop_mergeCommute (p :: p wZ wX
p :\/: q :: 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
q' :: p wX wZ
q' :/\: p' :: 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
Nothing -> Bool
False
Just (q'' :: p wZ wZ
q'' :> p'' :: 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
Nothing -> Bool
False
Just (p'' :: p wZ wZ
p'' :> q'' :: 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')