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