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(..)
)
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'')
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''
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')
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')
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)
{-# 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')