module Darcs.Patch.Commute
    ( Commute(..)
    , commuteFL
    , commuteRL
    , commuteRLFL
    , selfCommuter
    ) where

import Darcs.Prelude

import Darcs.Patch.CommuteFn
    ( CommuteFn
    , commuterIdFL
    , commuterRLId
    , commuterRLFL
    )
import Darcs.Patch.Witnesses.Ordered
    ( FL(..), RL(..), reverseFL, reverseRL,
    (:>)(..) )

-- | Commute represents things that can be (possibly) commuted.
--
-- Instances should obey the following laws:
--
-- * Symmetry
--
--   prop> commute (p:>q) == Just (q':>p') <=> commute (q':>p') == Just (p':>q)
--
-- * If an instance @'Invert' p@ exists, then
--
--   prop> commute (p:>q) == Just (q':>p') <=> commute (invert q:>invert p) == Just (invert p':>invert q')
--
-- * The more general Square-Commute law
--
--   prop> commute (p:>q) == Just (q':>p') => commute (invert p:>q') == Just (q:>invert p')
--
--   is required to hold only for primitive patches, i.e. if there is /no/
--   instance @'Merge' p@, because together with 'merge' it implies that
--   any two patches commute.
class Commute p where
    commute :: (p :> p) wX wY -> Maybe ((p :> p) wX wY)

instance Commute p => Commute (FL p) where
    {-# INLINE commute #-}
    commute :: (:>) (FL p) (FL p) wX wY -> Maybe ((:>) (FL p) (FL p) wX wY)
commute (FL p wX wZ
NilFL :> FL p wZ wY
x) = (:>) (FL p) (FL p) wZ wY -> Maybe ((:>) (FL p) (FL p) wZ wY)
forall a. a -> Maybe a
Just (FL p wZ wY
x FL p wZ wY -> FL p wY wY -> (:>) (FL p) (FL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
    commute (FL p wX wZ
x :> FL p wZ wY
NilFL) = (:>) (FL p) (FL p) wX wZ -> Maybe ((:>) (FL p) (FL p) wX wZ)
forall a. a -> Maybe a
Just (FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wX wX -> FL p wX wZ -> (:>) (FL p) (FL p) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wX wZ
x)
    commute (FL p wX wZ
xs :> FL p wZ wY
ys) = do
        FL p wX wZ
ys' :> RL p wZ wY
rxs' <- (:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (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
xs RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wY
ys)
        (:>) (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 wZ wY -> (:>) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> 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
rxs'

-- |'commuteRLFL' commutes an 'RL' past an 'FL'.
{-# INLINE commuteRLFL #-}
commuteRLFL :: Commute p => (RL p :> FL p) wX wY
            -> Maybe ((FL p :> RL p) wX wY)
commuteRLFL :: (:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL = CommuteFn p p -> CommuteFn (RL p) (FL p)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2)
commuterRLFL CommuteFn p p
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute

instance Commute p => Commute (RL p) where
    {-# INLINE commute #-}
    commute :: (:>) (RL p) (RL p) wX wY -> Maybe ((:>) (RL p) (RL p) wX wY)
commute (RL p wX wZ
xs :> RL p wZ wY
ys) = do
        FL p wX wZ
fys' :> RL p wZ wY
xs' <- (:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (RL p wX wZ
xs RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> 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
ys)
        (:>) (RL p) (RL p) wX wY -> Maybe ((:>) (RL p) (RL p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (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
fys' RL p wX wZ -> RL p wZ wY -> (:>) (RL p) (RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
xs')

-- |'commuteRL' commutes a RL past a single element.
{-# INLINE commuteRL #-}
commuteRL :: Commute p => (RL p :> p) wX wY -> Maybe ((p :> RL p) wX wY)
commuteRL :: (:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL = CommuteFn p p -> CommuteFn (RL p) p
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p p
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute

-- |'commuteFL' commutes a single element past a FL.
{-# INLINE commuteFL #-}
commuteFL :: Commute p => (p :> FL p) wX wY -> Maybe ((FL p :> p) wX wY)
commuteFL :: (:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL = CommuteFn p p -> CommuteFn p (FL p)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p p
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute

-- |Build a commuter between a patch and itself using the operation from the type class.
selfCommuter :: Commute p => CommuteFn p p
selfCommuter :: CommuteFn p p
selfCommuter = (:>) 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