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

import Prelude ()
import Darcs.Prelude

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.
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

commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL _ (x :: p1 wX wZ
x :> NilRL) = (:>) (RL p2) p1 wX wZ -> Maybe ((:>) (RL p2) p1 wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (RL p2 wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p2 wX wX -> p1 wX wZ -> (:>) (RL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdRL commuter :: CommuteFn p1 p2
commuter (x :: p1 wX wZ
x :> (ys :: RL p2 wZ wY
ys :<: y :: p2 wY wY
y))
  = do ys' :: RL p2 wX wZ
ys' :> x' :: p1 wZ wY
x' <- CommuteFn p1 p2
-> (:>) p1 (RL p2) wX wY -> Maybe ((:>) (RL p2) p1 wX wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (RL p2)
commuterIdRL CommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> RL p2 wZ wY -> (:>) p1 (RL p2) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p2 wZ wY
ys)
       y' :: p2 wZ wZ
y' :> x'' :: p1 wZ wY
x'' <- (:>) p1 p2 wZ wY -> Maybe ((:>) p2 p1 wZ wY)
CommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> p2 wY wY -> (:>) p1 p2 wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wY
y)
       (:>) (RL p2) p1 wX wY -> Maybe ((:>) (RL p2) p1 wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((RL p2 wX wZ
ys' RL p2 wX wZ -> p2 wZ wZ -> RL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p2 wZ wZ
y') RL p2 wX wZ -> p1 wZ wY -> (:>) (RL p2) p1 wX wY
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 :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL _ (x :: p1 wX wZ
x :> NilFL) = (:>) (FL p2) p1 wX wZ -> Maybe ((:>) (FL p2) p1 wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x)
commuterIdFL commuter :: CommuteFn p1 p2
commuter (x :: p1 wX wZ
x :> (y :: p2 wZ wY
y :>: ys :: FL p2 wY wY
ys))
  = do y' :: p2 wX wZ
y' :> x' :: p1 wZ wY
x' <- (:>) p1 p2 wX wY -> Maybe ((:>) p2 p1 wX wY)
CommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       ys' :: FL p2 wZ wZ
ys' :> x'' :: p1 wZ wY
x'' <- CommuteFn p1 p2
-> (:>) p1 (FL p2) wZ wY -> Maybe ((:>) (FL p2) p1 wZ wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys)
       (:>) (FL p2) p1 wX wY -> Maybe ((:>) (FL p2) p1 wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((p2 wX wZ
y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wZ wY
x'')

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

totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL _ (x :: p1 wX wZ
x :> NilFL) = FL p2 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p1 wX wZ
x
totalCommuterIdFL commuter :: TotalCommuteFn p1 p2
commuter (x :: p1 wX wZ
x :> (y :: p2 wZ wY
y :>: ys :: FL p2 wY wY
ys)) =
   case (:>) p1 p2 wX wY -> (:>) p2 p1 wX wY
TotalCommuteFn p1 p2
commuter (p1 wX wZ
x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y) of
     y' :: p2 wX wZ
y' :> x' :: p1 wZ wY
x' -> case TotalCommuteFn p1 p2
-> (:>) p1 (FL p2) wZ wY -> (:>) (FL p2) p1 wZ wY
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter (p1 wZ wY
x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p2 wY wY
ys) of
                   ys' :: FL p2 wZ wZ
ys' :> x'' :: p1 wZ wY
x'' -> (p2 wX wZ
y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p2 wZ wZ
ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY
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 :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId _ (NilFL :> y :: p2 wZ wY
y) = (:>) p2 (FL p1) wZ wY -> Maybe ((:>) p2 (FL p1) wZ wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y p2 wZ wY -> FL p1 wY wY -> (:>) p2 (FL p1) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
commuterFLId commuter :: CommuteFn p1 p2
commuter ((x :: p1 wX wY
x :>: xs :: FL p1 wY wZ
xs) :> y :: p2 wZ wY
y)
  = do y' :: p2 wY wZ
y' :> xs' :: FL p1 wZ wY
xs' <- CommuteFn p1 p2
-> (:>) (FL p1) p2 wY wY -> Maybe ((:>) p2 (FL p1) wY wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn p1 p2
commuter (FL p1 wY wZ
xs FL p1 wY wZ -> p2 wZ wY -> (:>) (FL p1) p2 wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       y'' :: p2 wX wZ
y'' :> x' :: p1 wZ wZ
x' <- (:>) p1 p2 wX wZ -> Maybe ((:>) p2 p1 wX wZ)
CommuteFn p1 p2
commuter (p1 wX wY
x p1 wX wY -> p2 wY wZ -> (:>) p1 p2 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       (:>) p2 (FL p1) wX wY -> Maybe ((:>) p2 (FL p1) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' p2 wX wZ -> FL p1 wZ wY -> (:>) p2 (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (p1 wZ wZ
x' p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY
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 :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId _ (NilRL :> y :: p2 wZ wY
y) = (:>) p2 (RL p1) wZ wY -> Maybe ((:>) p2 (RL p1) wZ wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wZ wY
y p2 wZ wY -> RL p1 wY wY -> (:>) p2 (RL p1) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p1 wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
commuterRLId commuter :: CommuteFn p1 p2
commuter ((xs :: RL p1 wX wY
xs :<: x :: p1 wY wZ
x) :> y :: p2 wZ wY
y)
  = do y' :: p2 wY wZ
y' :> x' :: p1 wZ wY
x' <- (:>) p1 p2 wY wY -> Maybe ((:>) p2 p1 wY wY)
CommuteFn p1 p2
commuter (p1 wY wZ
x p1 wY wZ -> p2 wZ wY -> (:>) p1 p2 wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wZ wY
y)
       y'' :: p2 wX wZ
y'' :> xs' :: RL p1 wZ wZ
xs' <- CommuteFn p1 p2
-> (:>) (RL p1) p2 wX wZ -> Maybe ((:>) p2 (RL p1) wX wZ)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (RL p1) p2
commuterRLId CommuteFn p1 p2
commuter (RL p1 wX wY
xs RL p1 wX wY -> p2 wY wZ -> (:>) (RL p1) p2 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wY wZ
y')
       (:>) p2 (RL p1) wX wY -> Maybe ((:>) p2 (RL p1) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p2 wX wZ
y'' p2 wX wZ -> RL p1 wZ wY -> (:>) p2 (RL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (RL p1 wZ wZ
xs' RL p1 wZ wZ -> p1 wZ wY -> RL p1 wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p1 wZ wY
x'))

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

totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2)
totalCommuterFLFL commuter :: TotalCommuteFn p1 p2
commuter = TotalCommuteFn p1 (FL p2) -> TotalCommuteFn (FL p1) (FL p2)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2
totalCommuterFLId (TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn p1 p2
commuter)