module Darcs.Patch.Invert
( Invert(..), invertFL, invertRL, dropInverses
)
where
import Darcs.Prelude
import Darcs.Patch.Witnesses.Ordered
( FL(..), RL(..), reverseFL, reverseRL, (:>)(..) )
import Darcs.Patch.Witnesses.Eq ( EqCheck(IsEq), Eq2((=\/=)) )
class Invert p where
invert :: p wX wY -> p wY wX
invertFL :: Invert p => FL p wX wY -> RL p wY wX
invertFL :: forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL FL p wX wY
NilFL = forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
invertFL (p wX wY
x:>:FL p wY wY
xs) = forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL FL p wY wY
xs forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
x
invertRL :: Invert p => RL p wX wY -> FL p wY wX
invertRL :: forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL RL p wX wY
NilRL = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
invertRL (RL p wX wY
xs:<:p wY wY
x) = forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wY wY
x forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL RL p wX wY
xs
instance Invert p => Invert (FL p) where
invert :: forall wX wY. FL p wX wY -> FL p wY wX
invert = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL
instance Invert p => Invert (RL p) where
invert :: forall wX wY. RL p wX wY -> RL p wY wX
invert = forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL
instance Invert p => Invert (p :> p) where
invert :: forall wX wY. (:>) p p wX wY -> (:>) p p wY wX
invert (p wX wZ
a :> p wZ wY
b) = forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wY
b 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 p wX wZ
a
dropInverses :: (Invert p, Eq2 p) => FL p wX wY -> Maybe (FL p wX wY)
dropInverses :: forall (p :: * -> * -> *) wX wY.
(Invert p, Eq2 p) =>
FL p wX wY -> Maybe (FL p wX wY)
dropInverses (p wX wY
x :>: p wY wY
y :>: FL p wY wY
z)
| EqCheck wX wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
x forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wY wY
y = forall a. a -> Maybe a
Just FL p wY wY
z
| Bool
otherwise = do
FL p wY wY
yz <- forall (p :: * -> * -> *) wX wY.
(Invert p, Eq2 p) =>
FL p wX wY -> Maybe (FL p wX wY)
dropInverses (p wY wY
y forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wY
z)
forall (p :: * -> * -> *) wX wY.
(Invert p, Eq2 p) =>
FL p wX wY -> Maybe (FL p wX wY)
dropInverses (p wX wY
x forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wY
yz)
dropInverses FL p wX wY
_ = forall a. Maybe a
Nothing