module Darcs.Patch.CommuteFn ( CommuteFn, commuterIdFL, commuterFLId, commuterIdRL, commuterRLId, commuterRLFL, MergeFn, PartialMergeFn, mergerIdFL, TotalCommuteFn, totalCommuterIdFL, totalCommuterFLId, totalCommuterFLFL, invertCommuter ) where import Darcs.Prelude import Darcs.Patch.Invert ( Invert(..) ) import Darcs.Patch.Witnesses.Ordered ( (:>)(..) , (:\/:)(..) , (:/\:)(..) , FL(..) , RL(..) ) -- |CommuteFn is the basis of a general framework for building up commutation -- operations between different patch types in a generic manner. Unfortunately -- type classes are not well suited to the problem because of the multiple possible -- routes by which the commuter for (FL p1, FL p2) can be built out of the -- commuter for (p1, p2) - and more complicated problems when we start building -- multiple constructors on top of each other. The type class resolution machinery -- really can't cope with selecting some route, because it doesn't know that all -- possible routes should be equivalent. -- -- Note that a CommuteFn cannot be lazy i.e. commute patches only when the -- resulting sequences are demanded. This is because of the possibility of -- failure ('Nothing'): all the commutes must be performed before we can know -- whether the overall commute succeeds. type CommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> Maybe ((p2 :> p1) wX wY) type TotalCommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> (p2 :> p1) wX wY type MergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> (p2 :/\: p1) wX wY type PartialMergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> Maybe ((p2 :/\: p1) wX wY) commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2) commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2) commuterIdRL CommuteFn p1 p2 _ (p1 wX wZ x :> RL p2 wZ wY NilRL) = (:>) (RL p2) p1 wX wZ -> Maybe ((:>) (RL p2) p1 wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return (RL p2 wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL RL p2 wX wX -> p1 wX wZ -> (:>) (RL p2) p1 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wX wZ x) commuterIdRL CommuteFn p1 p2 commuter (p1 wX wZ x :> (RL p2 wZ wY ys :<: p2 wY wY y)) = do RL p2 wX wZ ys' :> p1 wZ wY x' <- CommuteFn p1 p2 -> (:>) p1 (RL p2) wX wY -> Maybe ((:>) (RL p2) p1 wX wY) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn p1 (RL p2) commuterIdRL CommuteFn p1 p2 commuter (p1 wX wZ x p1 wX wZ -> RL p2 wZ wY -> (:>) p1 (RL p2) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p2 wZ wY ys) p2 wZ wZ y' :> p1 wZ wY x'' <- (:>) p1 p2 wZ wY -> Maybe ((:>) p2 p1 wZ wY) CommuteFn p1 p2 commuter (p1 wZ wY x' p1 wZ wY -> p2 wY wY -> (:>) p1 p2 wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wY wY y) (:>) (RL p2) p1 wX wY -> Maybe ((:>) (RL p2) p1 wX wY) forall (m :: * -> *) a. Monad m => a -> m a return ((RL p2 wX wZ ys' RL p2 wX wZ -> p2 wZ wZ -> RL p2 wX wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: p2 wZ wZ y') RL p2 wX wZ -> p1 wZ wY -> (:>) (RL p2) p1 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wZ wY x'') commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2) commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2) commuterIdFL CommuteFn p1 p2 _ (p1 wX wZ x :> FL p2 wZ wY NilFL) = (:>) (FL p2) p1 wX wZ -> Maybe ((:>) (FL p2) p1 wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return (FL p2 wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wX wZ x) commuterIdFL CommuteFn p1 p2 commuter (p1 wX wZ x :> (p2 wZ wY y :>: FL p2 wY wY ys)) = do p2 wX wZ y' :> p1 wZ wY x' <- (:>) p1 p2 wX wY -> Maybe ((:>) p2 p1 wX wY) CommuteFn p1 p2 commuter (p1 wX wZ x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wZ wY y) FL p2 wZ wZ ys' :> p1 wZ wY x'' <- CommuteFn p1 p2 -> (:>) p1 (FL p2) wZ wY -> Maybe ((:>) (FL p2) p1 wZ wY) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn p1 (FL p2) commuterIdFL CommuteFn p1 p2 commuter (p1 wZ wY x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p2 wY wY ys) (:>) (FL p2) p1 wX wY -> Maybe ((:>) (FL p2) p1 wX wY) forall (m :: * -> *) a. Monad m => a -> m a return ((p2 wX wZ y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p2 wZ wZ ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wZ wY x'') -- | TODO document laziness or lack thereof mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2) mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2) mergerIdFL MergeFn p1 p2 _ (p1 wZ wX x :\/: FL p2 wZ wY NilFL) = FL p2 wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p2 wX wX -> p1 wZ wX -> (:/\:) (FL p2) p1 wX wZ forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p1 wZ wX x mergerIdFL MergeFn p1 p2 merger (p1 wZ wX x :\/: (p2 wZ wY y :>: FL p2 wY wY ys)) = case (:\/:) p1 p2 wX wY -> (:/\:) p2 p1 wX wY MergeFn p1 p2 merger (p1 wZ wX x p1 wZ wX -> p2 wZ wY -> (:\/:) p1 p2 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: p2 wZ wY y) of p2 wX wZ y' :/\: p1 wY wZ x' -> case MergeFn p1 p2 -> (:\/:) p1 (FL p2) wZ wY -> (:/\:) (FL p2) p1 wZ wY forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). MergeFn p1 p2 -> MergeFn p1 (FL p2) mergerIdFL MergeFn p1 p2 merger (p1 wY wZ x' p1 wY wZ -> FL p2 wY wY -> (:\/:) p1 (FL p2) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY :\/: FL p2 wY wY ys) of FL p2 wZ wZ ys' :/\: p1 wY wZ x'' -> (p2 wX wZ y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p2 wZ wZ ys') FL p2 wX wZ -> p1 wY wZ -> (:/\:) (FL p2) p1 wX wY forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ. a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY :/\: p1 wY wZ x'' -- | TODO document laziness or lack thereof totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) totalCommuterIdFL TotalCommuteFn p1 p2 _ (p1 wX wZ x :> FL p2 wZ wY NilFL) = FL p2 wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p2 wX wX -> p1 wX wZ -> (:>) (FL p2) p1 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wX wZ x totalCommuterIdFL TotalCommuteFn p1 p2 commuter (p1 wX wZ x :> (p2 wZ wY y :>: FL p2 wY wY ys)) = case (:>) p1 p2 wX wY -> (:>) p2 p1 wX wY TotalCommuteFn p1 p2 commuter (p1 wX wZ x p1 wX wZ -> p2 wZ wY -> (:>) p1 p2 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wZ wY y) of p2 wX wZ y' :> p1 wZ wY x' -> case TotalCommuteFn p1 p2 -> (:>) p1 (FL p2) wZ wY -> (:>) (FL p2) p1 wZ wY forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) totalCommuterIdFL TotalCommuteFn p1 p2 commuter (p1 wZ wY x' p1 wZ wY -> FL p2 wY wY -> (:>) p1 (FL p2) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p2 wY wY ys) of FL p2 wZ wZ ys' :> p1 wZ wY x'' -> (p2 wX wZ y' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p2 wZ wZ ys') FL p2 wX wZ -> p1 wZ wY -> (:>) (FL p2) p1 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p1 wZ wY x'' commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2 commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2 commuterFLId CommuteFn p1 p2 _ (FL p1 wX wZ NilFL :> p2 wZ wY y) = (:>) p2 (FL p1) wZ wY -> Maybe ((:>) p2 (FL p1) wZ wY) forall (m :: * -> *) a. Monad m => a -> m a return (p2 wZ wY y p2 wZ wY -> FL p1 wY wY -> (:>) p2 (FL p1) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p1 wY wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL) commuterFLId CommuteFn p1 p2 commuter ((p1 wX wY x :>: FL p1 wY wZ xs) :> p2 wZ wY y) = do p2 wY wZ y' :> FL p1 wZ wY xs' <- CommuteFn p1 p2 -> (:>) (FL p1) p2 wY wY -> Maybe ((:>) p2 (FL p1) wY wY) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn (FL p1) p2 commuterFLId CommuteFn p1 p2 commuter (FL p1 wY wZ xs FL p1 wY wZ -> p2 wZ wY -> (:>) (FL p1) p2 wY wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wZ wY y) p2 wX wZ y'' :> p1 wZ wZ x' <- (:>) p1 p2 wX wZ -> Maybe ((:>) p2 p1 wX wZ) CommuteFn p1 p2 commuter (p1 wX wY x p1 wX wY -> p2 wY wZ -> (:>) p1 p2 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wY wZ y') (:>) p2 (FL p1) wX wY -> Maybe ((:>) p2 (FL p1) wX wY) forall (m :: * -> *) a. Monad m => a -> m a return (p2 wX wZ y'' p2 wX wZ -> FL p1 wZ wY -> (:>) p2 (FL p1) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> (p1 wZ wZ x' p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p1 wZ wY xs')) commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2 commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2 commuterRLId CommuteFn p1 p2 _ (RL p1 wX wZ NilRL :> p2 wZ wY y) = (:>) p2 (RL p1) wZ wY -> Maybe ((:>) p2 (RL p1) wZ wY) forall (m :: * -> *) a. Monad m => a -> m a return (p2 wZ wY y p2 wZ wY -> RL p1 wY wY -> (:>) p2 (RL p1) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p1 wY wY forall (a :: * -> * -> *) wX. RL a wX wX NilRL) commuterRLId CommuteFn p1 p2 commuter ((RL p1 wX wY xs :<: p1 wY wZ x) :> p2 wZ wY y) = do p2 wY wZ y' :> p1 wZ wY x' <- (:>) p1 p2 wY wY -> Maybe ((:>) p2 p1 wY wY) CommuteFn p1 p2 commuter (p1 wY wZ x p1 wY wZ -> p2 wZ wY -> (:>) p1 p2 wY wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wZ wY y) p2 wX wZ y'' :> RL p1 wZ wZ xs' <- CommuteFn p1 p2 -> (:>) (RL p1) p2 wX wZ -> Maybe ((:>) p2 (RL p1) wX wZ) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn (RL p1) p2 commuterRLId CommuteFn p1 p2 commuter (RL p1 wX wY xs RL p1 wX wY -> p2 wY wZ -> (:>) (RL p1) p2 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wY wZ y') (:>) p2 (RL p1) wX wY -> Maybe ((:>) p2 (RL p1) wX wY) forall (m :: * -> *) a. Monad m => a -> m a return (p2 wX wZ y'' p2 wX wZ -> RL p1 wZ wY -> (:>) p2 (RL p1) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> (RL p1 wZ wZ xs' RL p1 wZ wZ -> p1 wZ wY -> RL p1 wZ wY forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: p1 wZ wY x')) commuterRLFL :: forall p1 p2. CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2) commuterRLFL :: CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2) commuterRLFL CommuteFn p1 p2 commuter (RL p1 wX wZ xs :> FL p2 wZ wY ys) = RL p1 wX wZ -> FL p2 wZ wY -> Maybe ((:>) (FL p2) (RL p1) wX wY) forall wX wY wZ. RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) right RL p1 wX wZ xs FL p2 wZ wY ys where right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ) right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) right RL p1 wX wY as FL p2 wY wZ NilFL = (:>) (FL p2) (RL p1) wX wY -> Maybe ((:>) (FL p2) (RL p1) wX wY) forall a. a -> Maybe a Just (FL p2 wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL p2 wX wX -> RL p1 wX wY -> (:>) (FL p2) (RL p1) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p1 wX wY as) right RL p1 wX wY as (p2 wY wY b :>: FL p2 wY wZ bs) = do p2 wX wZ b' :> RL p1 wZ wY as' <- CommuteFn p1 p2 -> (:>) (RL p1) p2 wX wY -> Maybe ((:>) p2 (RL p1) wX wY) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn (RL p1) p2 commuterRLId CommuteFn p1 p2 commuter (RL p1 wX wY as RL p1 wX wY -> p2 wY wY -> (:>) (RL p1) p2 wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wY wY b) FL p2 wZ wZ bs' :> RL p1 wZ wZ as'' <- RL p1 wZ wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wZ wZ) forall wX wY wZ. RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) left RL p1 wZ wY as' FL p2 wY wZ bs (:>) (FL p2) (RL p1) wX wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return (p2 wX wZ b' p2 wX wZ -> FL p2 wZ wZ -> FL p2 wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p2 wZ wZ bs' FL p2 wX wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p1 wZ wZ as'') left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ) left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) left RL p1 wX wY NilRL FL p2 wY wZ bs = (:>) (FL p2) (RL p1) wY wZ -> Maybe ((:>) (FL p2) (RL p1) wY wZ) forall a. a -> Maybe a Just (FL p2 wY wZ bs FL p2 wY wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wY wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p1 wZ wZ forall (a :: * -> * -> *) wX. RL a wX wX NilRL) left (RL p1 wX wY as :<: p1 wY wY a) FL p2 wY wZ bs = do FL p2 wY wZ bs' :> p1 wZ wZ a' <- CommuteFn p1 p2 -> (:>) p1 (FL p2) wY wZ -> Maybe ((:>) (FL p2) p1 wY wZ) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). CommuteFn p1 p2 -> CommuteFn p1 (FL p2) commuterIdFL CommuteFn p1 p2 commuter (p1 wY wY a p1 wY wY -> FL p2 wY wZ -> (:>) p1 (FL p2) wY wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p2 wY wZ bs) FL p2 wX wZ bs'' :> RL p1 wZ wZ as' <- RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) forall wX wY wZ. RL p1 wX wY -> FL p2 wY wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) right RL p1 wX wY as FL p2 wY wZ bs' (:>) (FL p2) (RL p1) wX wZ -> Maybe ((:>) (FL p2) (RL p1) wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return (FL p2 wX wZ bs'' FL p2 wX wZ -> RL p1 wZ wZ -> (:>) (FL p2) (RL p1) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p1 wZ wZ as' RL p1 wZ wZ -> p1 wZ wZ -> RL p1 wZ wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: p1 wZ wZ a') -- | TODO document laziness or lack thereof totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2 totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2 totalCommuterFLId TotalCommuteFn p1 p2 _ (FL p1 wX wZ NilFL :> p2 wZ wY y) = p2 wZ wY y p2 wZ wY -> FL p1 wY wY -> (:>) p2 (FL p1) wZ wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p1 wY wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL totalCommuterFLId TotalCommuteFn p1 p2 commuter ((p1 wX wY x :>: FL p1 wY wZ xs) :> p2 wZ wY y) = case TotalCommuteFn p1 p2 -> (:>) (FL p1) p2 wY wY -> (:>) p2 (FL p1) wY wY forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2 totalCommuterFLId TotalCommuteFn p1 p2 commuter (FL p1 wY wZ xs FL p1 wY wZ -> p2 wZ wY -> (:>) (FL p1) p2 wY wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wZ wY y) of p2 wY wZ y' :> FL p1 wZ wY xs' -> case (:>) p1 p2 wX wZ -> (:>) p2 p1 wX wZ TotalCommuteFn p1 p2 commuter (p1 wX wY x p1 wX wY -> p2 wY wZ -> (:>) p1 p2 wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p2 wY wZ y') of p2 wX wZ y'' :> p1 wZ wZ x' -> p2 wX wZ y'' p2 wX wZ -> FL p1 wZ wY -> (:>) p2 (FL p1) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> (p1 wZ wZ x' p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p1 wZ wY xs') -- | TODO document laziness or lack thereof totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2) totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2) totalCommuterFLFL TotalCommuteFn p1 p2 commuter = TotalCommuteFn p1 (FL p2) -> TotalCommuteFn (FL p1) (FL p2) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2 totalCommuterFLId (TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) forall (p1 :: * -> * -> *) (p2 :: * -> * -> *). TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) totalCommuterIdFL TotalCommuteFn p1 p2 commuter) -- | Make use of the inverse-commute law to reduce the number of cases -- when defining commute for complicated patch types. {-# INLINE invertCommuter #-} invertCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p invertCommuter :: CommuteFn p q -> CommuteFn q p invertCommuter CommuteFn p q commuter (q wX wZ x :> p wZ wY y) = do q wY wZ ix' :> p wZ wX iy' <- (:>) p q wY wX -> Maybe ((:>) q p wY wX) CommuteFn p q commuter (p wZ wY -> p wY wZ forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert p wZ wY y p wY wZ -> q wZ wX -> (:>) p q wY wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> q wX wZ -> q wZ wX forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert q wX wZ x) (:>) p q wX wY -> Maybe ((:>) p q wX wY) forall (m :: * -> *) a. Monad m => a -> m a return (p wZ wX -> p wX wZ forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert p wZ wX iy' p wX wZ -> q wZ wY -> (:>) p q wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> q wY wZ -> q wZ wY forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX invert q wY wZ ix')