-- |
-- 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 :: (:\/:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY)
cleanMerge (FL p wZ wX
NilFL :\/: FL p wZ wY
x) = (:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY))
-> (:/\:) (FL p) (FL p) wZ wY -> Maybe ((:/\:) (FL p) (FL p) wZ wY)
forall a b. (a -> b) -> a -> b
$ 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
  cleanMerge (FL p wZ wX
x :\/: FL p wZ wY
NilFL) = (:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ))
-> (:/\:) (FL p) (FL p) wX wZ -> Maybe ((:/\:) (FL p) (FL p) wX wZ)
forall a b. (a -> b) -> a -> b
$ 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
  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' <- (:\/:) p (FL p) wY wY -> Maybe ((:/\:) (FL p) p wY wY)
forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (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)
    FL p wZ wZ
xs' :/\: FL p wX wZ
ys'' <- (:\/:) (FL p) (FL p) wZ wX -> Maybe ((:/\:) (FL p) (FL p) wZ wX)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (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)
    (:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY))
-> (:/\:) (FL p) (FL p) wX wY -> Maybe ((:/\:) (FL p) (FL p) wX wY)
forall a b. (a -> b) -> a -> b
$ 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')

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

{- | 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 :: 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 = MergeFn p p
-> forall wX wY.
   (:\/:) (FL p) (FL p) wX wY -> (:/\:) (FL p) (FL p) wX wY
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) (FL q)
mergerFLFL MergeFn p p
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge

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 = MergeFn p p -> MergeFn p (FL p)
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL MergeFn p p
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
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 q -> MergeFn p (FL q)
mergerIdFL MergeFn p q
_mergeFn (p wZ wX
p :\/: FL q wZ wY
NilFL) = FL q wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL q wX wX -> p wZ wX -> (:/\:) (FL q) p wX wZ
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 (:\/:) p q wX wY -> (:/\:) q p wX wY
MergeFn p q
mergeFn (p wZ wX
p p wZ wX -> q wZ wY -> (:\/:) p q wX wY
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 MergeFn p q -> (:\/:) p (FL q) wZ wY -> (:/\:) (FL q) p wZ wY
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL MergeFn p q
mergeFn (p wY wZ
p' p wY wZ -> FL q wY wY -> (:\/:) p (FL q) wZ wY
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' q wX wZ -> FL q wZ wZ -> FL q wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL q wZ wZ
xs') FL q wX wZ -> p wY wZ -> (:/\:) (FL q) p wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p wY wZ
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 p q -> MergeFn (FL p) q
mergerFLId MergeFn p q
mergeFn = MergeFn q (FL p) -> MergeFn (FL p) q
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger (MergeFn q p -> MergeFn q (FL p)
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL (MergeFn p q -> MergeFn q p
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger MergeFn p q
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 p q -> MergeFn (FL p) (FL q)
mergerFLFL MergeFn p q
mergeFn = MergeFn (FL p) q -> MergeFn (FL p) (FL q)
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn p (FL q)
mergerIdFL (MergeFn p q -> MergeFn (FL p) q
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn (FL p) q
mergerFLId MergeFn p q
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 :: (:\/:) p p wX wY -> (:/\:) p p wX wY
swapMerge = MergeFn p p -> MergeFn p p
forall (p :: * -> * -> *) (q :: * -> * -> *).
MergeFn p q -> MergeFn q p
swapMerger MergeFn p p
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge

-- | Swap the two patches, apply an arbitrary merge function, then swap again.
swapMerger :: MergeFn p q -> MergeFn q p
swapMerger :: MergeFn p q -> MergeFn q p
swapMerger MergeFn p q
mergeFn (q wZ wX
x :\/: p wZ wY
y) = case (:\/:) p q wY wX -> (:/\:) q p wY wX
MergeFn p q
mergeFn (p wZ wY
y p wZ wY -> q wZ wX -> (:\/:) p q wY wX
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' p wX wZ -> q wY wZ -> (:/\:) p q wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: q wY wZ
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 :: (:\/:) 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' <- (:\/:) p p wY wX -> Maybe ((:/\:) p p wY wX)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (p wZ wY
y 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
x)
  (:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY))
-> (:/\:) p p wX wY -> Maybe ((:/\:) p p wX wY)
forall a b. (a -> b) -> a -> b
$ p wX wZ
y' 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 wY wZ
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 :: [Sealed (FL p wX)]
-> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))
mergeList = (Sealed (FL p wX)
 -> Sealed (FL p wX)
 -> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX)))
-> Sealed (FL p wX)
-> [Sealed (FL p wX)]
-> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Sealed (FL p wX)
-> Sealed (FL p wX)
-> Either (Sealed (FL p wX), Sealed (FL p wX)) (Sealed (FL p wX))
forall (a :: * -> * -> *) wZ.
CleanMerge a =>
Sealed (FL a wZ)
-> Sealed (FL a wZ)
-> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))
mergeTwo (FL p wX wX -> Sealed (FL p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
  where
    mergeTwo :: Sealed (FL a wZ)
-> Sealed (FL a wZ)
-> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))
mergeTwo (Sealed FL a wZ wX
ps) (Sealed qs) =
      case (:\/:) (FL a) (FL a) wX wX -> Maybe ((:/\:) (FL a) (FL a) wX wX)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL a wZ wX
ps FL a wZ wX -> FL a wZ wX -> (:\/:) (FL a) (FL a) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL a wZ wX
qs) of
        Just (FL a wX wZ
qs' :/\: FL a wX wZ
_) -> Sealed (FL a wZ)
-> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))
forall a b. b -> Either a b
Right (Sealed (FL a wZ)
 -> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ)))
-> Sealed (FL a wZ)
-> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))
forall a b. (a -> b) -> a -> b
$ FL a wZ wZ -> Sealed (FL a wZ)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL a wZ wZ -> Sealed (FL a wZ)) -> FL a wZ wZ -> Sealed (FL a wZ)
forall a b. (a -> b) -> a -> b
$ FL a wZ wX
ps FL a wZ wX -> FL a wX wZ -> FL a wZ wZ
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 -> (Sealed (FL a wZ), Sealed (FL a wZ))
-> Either (Sealed (FL a wZ), Sealed (FL a wZ)) (Sealed (FL a wZ))
forall a b. a -> Either a b
Left (FL a wZ wX -> Sealed (FL a wZ)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed FL a wZ wX
ps, FL a wZ wX -> Sealed (FL a wZ)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed FL a wZ wX
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 p wX wY -> (:>) p p wX wY
_forceCommute (p wX wZ
p :> p wZ wY
q) =
  case (:>) 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 wX wZ
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) of
    Just (p wX wZ
q' :> p wZ wY
p') -> p wX wZ
q' 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
p'
    Maybe ((:>) p p wX wY)
Nothing ->
      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 wX wZ -> p wZ wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wZ
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
        p wX wZ
q' :/\: p wY wZ
ip' -> p wX wZ
q' 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 wY wZ -> p wZ wY
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wY wZ
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 p wX wY -> Bool
prop_mergeSymmetric (p wZ wX
p :\/: 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
    p wX wZ
q' :/\: 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 wY wZ
p'' :/\: 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'')

-- | 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 p wX wY -> Bool
prop_mergeCommute (p wZ wX
p :\/: 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
    p wX wZ
q' :/\: 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
        Maybe ((:>) p p wZ wZ)
Nothing -> Bool
False
        Just (p wZ wZ
q'' :> 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
        Maybe ((:>) p p wZ wZ)
Nothing -> Bool
False
        Just (p wZ wZ
p'' :> 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')