module Darcs.Patch.Invert ( Invert(..), invertFL, invertRL ) where import Prelude () import Darcs.Prelude import Darcs.Patch.Witnesses.Ordered ( FL(..), RL(..), reverseFL, reverseRL, (:>)(..) ) 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 NilFL = RL p wY wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL invertFL (x :: p wX wY x:>:xs :: 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 NilRL = FL p wY wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL invertRL (xs :: RL p wX wY xs:<:x :: 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 (a :: p wX wZ a :> b :: 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