module Darcs.Patch.Commute
( Commute(..)
, commuteFL
, commuteFLorComplain
, commuteRL
, commuteRLFL
, selfCommuter
) where
import Prelude ()
import Darcs.Prelude
import Darcs.Patch.CommuteFn ( CommuteFn )
import Darcs.Patch.Witnesses.Ordered
( FL(..), RL(..), reverseFL, reverseRL,
(:>)(..) )
import Darcs.Patch.Witnesses.Sealed ( Sealed2, seal2 )
class Commute p where
commute :: (p :> p) wX wY -> Maybe ((p :> p) wX wY)
instance Commute p => Commute (FL p) where
commute :: (:>) (FL p) (FL p) wX wY -> Maybe ((:>) (FL p) (FL p) wX wY)
commute (NilFL :> x :: FL p wZ wY
x) = (:>) (FL p) (FL p) wZ wY -> Maybe ((:>) (FL p) (FL p) wZ wY)
forall a. a -> Maybe a
Just (FL p wZ wY
x FL p wZ wY -> FL p wY wY -> (:>) (FL p) (FL p) wZ 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 (x :: FL p wX wZ
x :> NilFL) = (:>) (FL p) (FL p) wX wZ -> Maybe ((:>) (FL p) (FL p) wX wZ)
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 wZ -> (:>) (FL p) (FL p) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wX wZ
x)
commute (xs :: FL p wX wZ
xs :> ys :: FL p wZ wY
ys) = do
ys' :: FL p wX wZ
ys' :> rxs' :: 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 (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 :: Commute p => (RL p :> FL p) wX wY
-> Maybe ((FL p :> RL p) wX wY)
commuteRLFL :: (:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (NilRL :> ys :: FL p wZ wY
ys) = (:>) (FL p) (RL p) wZ wY -> Maybe ((:>) (FL p) (RL p) wZ wY)
forall a. a -> Maybe a
Just (FL p wZ wY
ys FL p wZ wY -> RL p wY wY -> (:>) (FL p) (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
commuteRLFL (xs :: RL p wX wZ
xs :> NilFL) = (:>) (FL p) (RL p) wX wZ -> Maybe ((:>) (FL p) (RL p) wX wZ)
forall a. a -> Maybe a
Just (FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wX wX -> RL p wX wZ -> (:>) (FL p) (RL p) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wX wZ
xs)
commuteRLFL (xs :: RL p wX wZ
xs :> y :: p wZ wY
y :>: ys :: FL p wY wY
ys) = do
y' :: p wX wZ
y' :> xs' :: RL p wZ wY
xs' <- (:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wX wZ
xs RL p wX wZ -> p wZ wY -> (:>) (RL p) p wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
y)
ys' :: FL p wZ wZ
ys' :> xs'' :: RL p wZ wY
xs'' <- (:>) (RL p) (FL p) wZ wY -> Maybe ((:>) (FL p) (RL p) wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (RL p wZ wY
xs' RL p wZ wY -> FL p wY wY -> (:>) (RL p) (FL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
ys)
(:>) (FL p) (RL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p wX wZ
y' p wX wZ -> FL p wZ wZ -> FL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
ys' FL p wX wZ -> RL p wZ wY -> (:>) (FL 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'')
instance Commute p => Commute (RL p) where
commute :: (:>) (RL p) (RL p) wX wY -> Maybe ((:>) (RL p) (RL p) wX wY)
commute (xs :: RL p wX wZ
xs :> ys :: RL p wZ wY
ys) = do
fys' :: FL p wX wZ
fys' :> xs' :: 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 (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 :: Commute p => (RL p :> p) wX wY -> Maybe ((p :> RL p) wX wY)
commuteRL :: (:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (zs :: RL p wX wY
zs :<: z :: p wY wZ
z :> w :: p wZ wY
w) = do
w' :: p wY wZ
w' :> z' :: p wZ wY
z' <- (:>) p p wY wY -> Maybe ((:>) p p wY wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wY wZ
z p wY wZ -> p wZ wY -> (:>) p p wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
w)
w'' :: p wX wZ
w'' :> zs' :: RL p wZ wZ
zs' <- (:>) (RL p) p wX wZ -> Maybe ((:>) p (RL p) wX wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wX wY
zs RL p wX wY -> p wY wZ -> (:>) (RL p) p wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
w')
(:>) p (RL p) wX wY -> Maybe ((:>) p (RL p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (p wX wZ
w'' p wX wZ -> RL p wZ wY -> (:>) p (RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
zs' RL p wZ wZ -> p wZ wY -> RL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wY
z')
commuteRL (NilRL :> w :: p wZ wY
w) = (:>) p (RL p) wZ wY -> Maybe ((:>) p (RL p) wZ wY)
forall a. a -> Maybe a
Just (p wZ wY
w p wZ wY -> RL p wY wY -> (:>) p (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
commuteFL :: Commute p => (p :> FL p) wX wY -> Maybe ((FL p :> p) wX wY)
commuteFL :: (:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL = (Sealed2 p -> Maybe ((:>) (FL p) p wX wY))
-> ((:>) (FL p) p wX wY -> Maybe ((:>) (FL p) p wX wY))
-> Either (Sealed2 p) ((:>) (FL p) p wX wY)
-> Maybe ((:>) (FL p) p wX wY)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe ((:>) (FL p) p wX wY)
-> Sealed2 p -> Maybe ((:>) (FL p) p wX wY)
forall a b. a -> b -> a
const Maybe ((:>) (FL p) p wX wY)
forall a. Maybe a
Nothing) (:>) (FL p) p wX wY -> Maybe ((:>) (FL p) p wX wY)
forall a. a -> Maybe a
Just (Either (Sealed2 p) ((:>) (FL p) p wX wY)
-> Maybe ((:>) (FL p) p wX wY))
-> ((:>) p (FL p) wX wY
-> Either (Sealed2 p) ((:>) (FL p) p wX wY))
-> (:>) p (FL p) wX wY
-> Maybe ((:>) (FL p) p wX wY)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:>) p (FL p) wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
commuteFLorComplain
commuteFLorComplain :: Commute p => (p :> FL p) wX wY
-> Either (Sealed2 p) ((FL p :> p) wX wY)
commuteFLorComplain :: (:>) p (FL p) wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
commuteFLorComplain (p :: p wX wZ
p :> NilFL) = (:>) (FL p) p wX wZ -> Either (Sealed2 p) ((:>) (FL p) p wX wZ)
forall a b. b -> Either a b
Right (FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wX wX -> p wX wZ -> (:>) (FL p) p wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wX wZ
p)
commuteFLorComplain (q :: p wX wZ
q :> p :: p wZ wY
p :>: ps :: FL p wY wY
ps) =
case (:>) 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 (p wX wZ
q p wX wZ -> p wZ wY -> (:>) p p wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
p) of
Just (p' :: p wX wZ
p' :> q' :: p wZ wY
q') ->
case (:>) p (FL p) wZ wY -> Either (Sealed2 p) ((:>) (FL p) p wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
commuteFLorComplain (p wZ wY
q' p wZ wY -> FL p wY wY -> (:>) p (FL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
ps) of
Right (ps' :: FL p wZ wZ
ps' :> q'' :: p wZ wY
q'') -> (:>) (FL p) p wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
forall a b. b -> Either a b
Right (p wX wZ
p' p wX wZ -> FL p wZ wZ -> FL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
ps' FL p wX wZ -> p wZ wY -> (:>) (FL p) p wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
q'')
Left l :: Sealed2 p
l -> Sealed2 p -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
forall a b. a -> Either a b
Left Sealed2 p
l
Nothing -> Sealed2 p -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
forall a b. a -> Either a b
Left (Sealed2 p -> Either (Sealed2 p) ((:>) (FL p) p wX wY))
-> Sealed2 p -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
forall a b. (a -> b) -> a -> b
$ p wZ wY -> Sealed2 p
forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a
seal2 p wZ wY
p
selfCommuter :: Commute p => CommuteFn p p
selfCommuter :: CommuteFn p p
selfCommuter = (:>) 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