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((=\/=)) )

-- | The 'invert' operation must be self-inverse, i.e. an involution:
--
-- prop> invert . invert = id
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

-- | Delete the first subsequence of patches that is followed by
-- an inverse subsequence, if one exists. If not return 'Nothing'.
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