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,
    (:>)(..) )

{- | Class of patches that that can be commuted.

Instances should obey the following laws:

[commute-symmetry]

    prop> commute (p:>q) == Just (q':>p') <=> commute (q':>p') == Just (p':>q)

[invert-commute]

    If patches are invertible, then

    prop> commute (p:>q) == Just (q':>p') <=> commute (invert q:>invert p) == Just (invert p':>invert q')

The more general law

[square-commute]

    prop> commute (p:>q) == Just (q':>p') => commute (invert p:>q') == Just (q:>invert p')

is valid in general only provided we know (a priori) that @'commute' ('invert'
p':>'q')@ succeeds, in other words, that p and q are not in conflict with each
other. See "Darcs.Patch.CommuteNoConflicts" for an extended discussion.

-}
class Commute p where
    commute :: (p :> p) wX wY -> Maybe ((p :> p) wX wY)

instance Commute p => Commute (FL p) where
    {-# INLINE commute #-}
    commute :: forall wX wY.
(:>) (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) wX wY -> Maybe ((:>) (FL p) (FL p) wX wY)
forall a. a -> Maybe a
Just (FL p wX wY
FL p wZ wY
x FL p wX wY -> FL p wY wY -> (:>) (FL p) (FL p) wX 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 wY -> Maybe ((:>) (FL p) (FL p) wX wY)
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 wY -> (:>) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p 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 a. a -> Maybe a
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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (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 (:>) p p wX wY -> Maybe ((:>) p p wX wY)
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 :: forall wX wY.
(:>) (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 a. a -> Maybe a
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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (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 (:>) p p wX wY -> Maybe ((:>) p p wX wY)
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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) 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 (:>) p p wX wY -> Maybe ((:>) p p wX wY)
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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
selfCommuter = (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall wX wY. (:>) 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