-- |
-- 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 = merge

instance Merge p => Merge (FL p) where
    merge (NilFL :\/: x) = x :/\: NilFL
    merge (x :\/: NilFL) = NilFL :/\: x
    merge ((x:>:xs) :\/: ys) = case mergeFL (x :\/: ys) of
      ys' :/\: x' -> case merge (ys' :\/: xs) of
        xs' :/\: ys'' -> ys'' :/\: (x' :>: xs')

instance Merge p => Merge (RL p) where
    merge (x :\/: y) = case merge (reverseRL x :\/: reverseRL y) of
        (ry' :/\: rx') -> reverseFL ry' :/\: reverseFL rx'

mergeFL :: Merge p
        => (p :\/: FL p) wX wY
        -> (FL p :/\: p) wX wY
mergeFL (p :\/: NilFL) = NilFL :/\: p
mergeFL (p :\/: (x :>: xs)) = case merge (p :\/: x) of
    x' :/\: p' -> case mergeFL (p' :\/: xs) of
      xs' :/\: p'' -> (x' :>: xs') :/\: p''

-- | The natural, non-conflicting merge.
naturalMerge :: (Invert p, Commute p)
             => (p :\/: p) wX wY -> Maybe ((p :/\: p) wX wY)
naturalMerge (p :\/: q) = do
  q' :> ip' <- commute (invert p :> q)
  -- TODO: find a small convincing example that demonstrates why
  -- it is necessary to do this extra check here
  _ <- commute (p :> q')
  return (q' :/\: invert ip')

prop_mergeSymmetric :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeSymmetric (p :\/: q) =
  case merge (p :\/: q) of
    q' :/\: p' ->
      case merge (q :\/: p) of
        p'' :/\: q'' ->
          isIsEq (q' =\/= q'') && isIsEq (p' =\/= p'')

prop_mergeCommute :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> Bool
prop_mergeCommute (p :\/: q) =
  case merge (p :\/: q) of
    q' :/\: p' ->
      case commute (p :> q') of
        Nothing -> False
        Just (q'' :> p'') ->
          isIsEq (q'' =\/= q) && isIsEq (p'' =/\= p')
      &&
      case commute (q :> p') of
        Nothing -> False
        Just (p'' :> q'') ->
          isIsEq (p'' =\/= p) && isIsEq (q'' =/\= q')