-- |
-- Module      : Darcs.Patch.Merge
-- Maintainer  : darcs-devel@darcs.net
-- Stability   : experimental
-- Portability : portable

module Darcs.Patch.Merge
    ( -- * Definitions
      Merge(..)
    , selfMerger
    , mergeFL
    , naturalMerge
      -- * Properties
    , 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
    )

-- | Things that can always be merged.
--
-- Instances should obey the following laws:
--
-- * Symmetry
--
--   prop> merge (p :\/: q) == q' :/\: p' <=> merge (q :\/: p) == p' :/\: q'
--
-- * MergesCommute
--
--   prop> merge (p :\/: q) == q' :/\: p' ==> commute (p :> q') == Just (q :> p')
--
--   that is, the two branches of a merge commute to each other
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''

-- | The natural, non-conflicting merge.
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)
  -- TODO: find a small convincing example that demonstrates why
  -- it is necessary to do this extra check here
  (:>) 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')