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 :: FL p wX wY -> RL p wY wX
invertFL FL p wX wY
NilFL = RL p wY wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
invertFL (p wX wY
x:>:FL p wY wY
xs) = FL p wY wY -> RL p wY wY
forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL FL p wY wY
xs RL p wY wY -> p wY wX -> RL p wY wX
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wX wY -> p wY wX
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 :: RL p wX wY -> FL p wY wX
invertRL RL p wX wY
NilRL = FL p wY wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
invertRL (RL p wX wY
xs:<:p wY wY
x) = p wY wY -> p wY wY
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wY wY
x p wY wY -> FL p wY wX -> FL p wY wX
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: RL p wX wY -> FL p wY wX
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 :: FL p wX wY -> FL p wY wX
invert = RL p wY wX -> FL p wY wX
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL (RL p wY wX -> FL p wY wX)
-> (FL p wX wY -> RL p wY wX) -> FL p wX wY -> FL p wY wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL p wX wY -> RL p wY wX
forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL

instance Invert p => Invert (RL p) where
    invert :: RL p wX wY -> RL p wY wX
invert = FL p wY wX -> RL p wY wX
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL (FL p wY wX -> RL p wY wX)
-> (RL p wX wY -> FL p wY wX) -> RL p wX wY -> RL p wY wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RL p wX wY -> FL p wY wX
forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL

instance Invert p => Invert (p :> p) where
  invert :: (:>) p p wX wY -> (:>) p p wY wX
invert (p wX wZ
a :> p wZ wY
b) = p wZ wY -> p wY wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wZ wY
b p wY wZ -> p wZ wX -> (:>) p p wY wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wX wZ -> p wZ wX
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 :: 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 <- p wX wY -> p wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
x p wY wX -> p wY wY -> EqCheck wX wY
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wY wY
y = FL p wY wY -> Maybe (FL p wY wY)
forall a. a -> Maybe a
Just FL p wY wY
z
  | Bool
otherwise = do
      FL p wY wY
yz <- FL p wY wY -> Maybe (FL p wY wY)
forall (p :: * -> * -> *) wX wY.
(Invert p, Eq2 p) =>
FL p wX wY -> Maybe (FL p wX wY)
dropInverses (p wY wY
y p wY wY -> FL p wY wY -> FL p wY wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wY
z)
      FL p wX wY -> Maybe (FL p wX wY)
forall (p :: * -> * -> *) wX wY.
(Invert p, Eq2 p) =>
FL p wX wY -> Maybe (FL p wX wY)
dropInverses (p wX wY
x p wX wY -> FL p wY wY -> FL p wX wY
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
_ = Maybe (FL p wX wY)
forall a. Maybe a
Nothing