-- |
-- 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 (NilFL :\/: x) = return $ x :/\: NilFL
  cleanMerge (x :\/: NilFL) = return $ NilFL :/\: x
  cleanMerge ((x :>: xs) :\/: ys) = do
    ys' :/\: x' <- cleanMergeFL (x :\/: ys)
    xs' :/\: ys'' <- cleanMerge (ys' :\/: xs)
    return $ ys'' :/\: (x' :>: xs')

-- | Cleanly merge a single patch with an 'FL' of patches.
cleanMergeFL :: CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p :\/: NilFL) = return $ NilFL :/\: p
cleanMergeFL (p :\/: (x :>: xs)) = do
  x' :/\: p'  <- cleanMerge (p :\/: x)
  xs' :/\: p'' <- cleanMergeFL (p' :\/: xs)
  return $ (x' :>: xs') :/\: 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 = merge

instance Merge p => Merge (FL p) where
    merge = mergerFLFL merge

mergeFL :: Merge p
        => (p :\/: FL p) wX wY
        -> (FL p :/\: p) wX wY
mergeFL = mergerIdFL 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 :\/: NilFL) = NilFL :/\: p
mergerIdFL  mergeFn (p :\/: (x :>: xs)) =
  case mergeFn (p :\/: x) of
    x' :/\: p' -> case mergerIdFL mergeFn (p' :\/: xs) of
      xs' :/\: p'' -> (x' :>: xs') :/\: 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 = swapMerger (mergerIdFL (swapMerger 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 = mergerIdFL (mergerFLId 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 = swapMerger merge

-- | Swap the two patches, apply an arbitrary merge function, then swap again.
swapMerger :: MergeFn p q -> MergeFn q p
swapMerger mergeFn (x :\/: y) = case mergeFn (y :\/: x) of x' :/\: y' -> y' :/\: 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 (x :\/: y) = do
  x' :/\: y' <- cleanMerge (y :\/: x)
  return $ y' :/\: 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 = foldM mergeTwo (Sealed NilFL)
  where
    mergeTwo (Sealed ps) (Sealed qs) =
      case cleanMerge (ps :\/: qs) of
        Just (qs' :/\: _) -> Right $ Sealed $ ps +>+ qs'
        Nothing -> Left (Sealed ps, Sealed 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 :> q) =
  case commute (p :> q) of
    Just (q' :> p') -> q' :> p'
    Nothing ->
      case merge (invert p :\/: q) of
        q' :/\: ip' -> q' :> invert 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 :\/: q) =
  case merge (p :\/: q) of
    q' :/\: p' ->
      case merge (q :\/: p) of
        p'' :/\: q'' ->
          isIsEq (q' =\/= q'') && isIsEq (p' =\/= 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 :\/: 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')