module Darcs.Patch.CommuteFn
    ( CommuteFn,
      commuterIdFL, commuterFLId,
      commuterIdRL, commuterRLId,
      commuterRLFL,
      MergeFn,
      PartialMergeFn,
      mergerIdFL,
      TotalCommuteFn,
      totalCommuterIdFL, totalCommuterFLId, totalCommuterFLFL,
      invertCommuter
    ) where

import Darcs.Prelude

import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Witnesses.Ordered
    ( (:>)(..)
    , (:\/:)(..)
    , (:/\:)(..)
    , FL(..)
    , RL(..)
    )

-- |CommuteFn is the basis of a general framework for building up commutation
-- operations between different patch types in a generic manner. Unfortunately
-- type classes are not well suited to the problem because of the multiple possible
-- routes by which the commuter for (FL p1, FL p2) can be built out of the
-- commuter for (p1, p2) - and more complicated problems when we start building
-- multiple constructors on top of each other. The type class resolution machinery
-- really can't cope with selecting some route, because it doesn't know that all
-- possible routes should be equivalent.
--
-- Note that a CommuteFn cannot be lazy i.e. commute patches only when the
-- resulting sequences are demanded. This is because of the possibility of
-- failure ('Nothing'): all the commutes must be performed before we can know
-- whether the overall commute succeeds.
type CommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> Maybe ((p2 :> p1) wX wY)

type TotalCommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> (p2 :> p1) wX wY

type MergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> (p2 :/\: p1) wX wY

type PartialMergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> Maybe ((p2 :/\: p1) wX wY)

commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL CommuteFn p1 p2
_ (p1 wX wZ
x :> RL p2 wZ wY
NilRL) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdRL CommuteFn p1 p2
commuter (p1 wX wZ
x :> (RL p2 wZ wY
ys :<: p2 wY wY
y))
  = do RL p2 wX wZ
ys' :> p1 wZ wY
x' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL CommuteFn p1 p2
commuter (p1 wX wZ
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p2 wZ wY
ys)
       p2 wZ wZ
y' :> p1 wZ wY
x'' <- CommuteFn p1 p2
commuter (p1 wZ wY
x' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wY
y)
       forall (m :: * -> *) a. Monad m => a -> m a
return ((RL p2 wX wZ
ys' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p2 wZ wZ
y') forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x'')

commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
_ (p1 wX wZ
x :> FL p2 wZ wY
NilFL) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdFL CommuteFn p1 p2
commuter (p1 wX wZ
x :> (p2 wZ wY
y :>: FL p2 wY wY
ys))
  = do p2 wX wZ
y' :> p1 wZ wY
x' <- CommuteFn p1 p2
commuter (p1 wX wZ
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       FL p2 wZ wZ
ys' :> p1 wZ wY
x'' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
commuter (p1 wZ wY
x' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys)
       forall (m :: * -> *) a. Monad m => a -> m a
return ((p2 wX wZ
y' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x'')

-- | TODO document laziness or lack thereof
mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL MergeFn p1 p2
_ (p1 wZ wX
x :\/: FL p2 wZ wY
NilFL) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p1 wZ wX
x
mergerIdFL MergeFn p1 p2
merger (p1 wZ wX
x :\/: (p2 wZ wY
y :>: FL p2 wY wY
ys))
  = case MergeFn p1 p2
merger (p1 wZ wX
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p2 wZ wY
y) of
      p2 wX wZ
y' :/\: p1 wY wZ
x' -> case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
MergeFn p1 p2 -> MergeFn p1 (FL p2)
mergerIdFL MergeFn p1 p2
merger (p1 wY wZ
x' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p2 wY wY
ys) of
          FL p2 wZ wZ
ys' :/\: p1 wY wZ
x'' -> (p2 wX wZ
y' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: p1 wY wZ
x''

-- | TODO document laziness or lack thereof
totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
_ (p1 wX wZ
x :> FL p2 wZ wY
NilFL) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x
totalCommuterIdFL TotalCommuteFn p1 p2
commuter (p1 wX wZ
x :> (p2 wZ wY
y :>: FL p2 wY wY
ys)) =
   case TotalCommuteFn p1 p2
commuter (p1 wX wZ
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y) of
     p2 wX wZ
y' :> p1 wZ wY
x' -> case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter (p1 wZ wY
x' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys) of
                   FL p2 wZ wZ
ys' :> p1 wZ wY
x'' -> (p2 wX wZ
y' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x''

commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn p1 p2
_ (FL p1 wX wZ
NilFL :> p2 wZ wY
y) = forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
commuterFLId CommuteFn p1 p2
commuter ((p1 wX wY
x :>: FL p1 wY wZ
xs) :> p2 wZ wY
y)
  = do p2 wY wZ
y' :> FL p1 wZ wY
xs' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn p1 p2
commuter (FL p1 wY wZ
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       p2 wX wZ
y'' :> p1 wZ wZ
x' <- CommuteFn p1 p2
commuter (p1 wX wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (p1 wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p1 wZ wY
xs'))

commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
_ (RL p1 wX wZ
NilRL :> p2 wZ wY
y) = forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
commuterRLId CommuteFn p1 p2
commuter ((RL p1 wX wY
xs :<: p1 wY wZ
x) :> p2 wZ wY
y)
  = do p2 wY wZ
y' :> p1 wZ wY
x' <- CommuteFn p1 p2
commuter (p1 wY wZ
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       p2 wX wZ
y'' :> RL p1 wZ wZ
xs' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
commuter (RL p1 wX wY
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (RL p1 wZ wZ
xs' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p1 wZ wY
x'))

commuterRLFL :: forall p1 p2. CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2)
commuterRLFL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2)
commuterRLFL CommuteFn p1 p2
commuter (RL p1 wX wZ
xs :> FL p2 wZ wY
ys) = forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wZ
xs FL p2 wZ wY
ys
  where
    right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ)
    right :: forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wY
as FL p2 wY wZ
NilFL = forall a. a -> Maybe a
Just (forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wX wY
as)
    right RL p1 wX wY
as (p2 wY wY
b :>: FL p2 wY wZ
bs) = do
      p2 wX wZ
b' :> RL p1 wZ wY
as' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
commuter (RL p1 wX wY
as forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wY
b)
      FL p2 wZ wZ
bs' :> RL p1 wZ wZ
as'' <- forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
left RL p1 wZ wY
as' FL p2 wY wZ
bs
      forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
b' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
bs' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wZ wZ
as'')
    left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ)
    left :: forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
left RL p1 wX wY
NilRL FL p2 wY wZ
bs = forall a. a -> Maybe a
Just (FL p2 wY wZ
bs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
    left (RL p1 wX wY
as :<: p1 wY wY
a) FL p2 wY wZ
bs = do
      FL p2 wY wZ
bs' :> p1 wZ wZ
a' <- forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
commuter (p1 wY wY
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wZ
bs)
      FL p2 wX wZ
bs'' :> RL p1 wZ wZ
as' <- forall wX wY wZ.
RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ)
right RL p1 wX wY
as FL p2 wY wZ
bs'
      forall (m :: * -> *) a. Monad m => a -> m a
return (FL p2 wX wZ
bs'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wZ wZ
as' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p1 wZ wZ
a')

-- | TODO document laziness or lack thereof
totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId TotalCommuteFn p1 p2
_ (FL p1 wX wZ
NilFL :> p2 wZ wY
y) = p2 wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
totalCommuterFLId TotalCommuteFn p1 p2
commuter ((p1 wX wY
x :>: FL p1 wY wZ
xs) :> p2 wZ wY
y) =
   case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId TotalCommuteFn p1 p2
commuter (FL p1 wY wZ
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y) of
     p2 wY wZ
y' :> FL p1 wZ wY
xs' -> case TotalCommuteFn p1 p2
commuter (p1 wX wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y') of
                    p2 wX wZ
y'' :> p1 wZ wZ
x' -> p2 wX wZ
y'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (p1 wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p1 wZ wY
xs')

-- | TODO document laziness or lack thereof
totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL :: forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL TotalCommuteFn p1 p2
commuter = forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId (forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter)

-- | Make use of the inverse-commute law to reduce the number of cases
-- when defining commute for complicated patch types.
{-# INLINE invertCommuter #-}
invertCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p
invertCommuter :: forall (p :: * -> * -> *) (q :: * -> * -> *).
(Invert p, Invert q) =>
CommuteFn p q -> CommuteFn q p
invertCommuter CommuteFn p q
commuter (q wX wZ
x :> p wZ wY
y) = do
    q wY wZ
ix' :> p wZ wX
iy' <- CommuteFn p q
commuter (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert q wX wZ
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wX
iy' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert q wY wZ
ix')