module Darcs.Patch.Invert
       ( Invert(..), invertFL, invertRL
       )
       where

import Darcs.Prelude

import Darcs.Patch.Witnesses.Ordered
    ( FL(..), RL(..), reverseFL, reverseRL, (:>)(..) )

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