1module Darcs.Patch.CommuteFn 2 ( CommuteFn, 3 commuterIdFL, commuterFLId, 4 commuterIdRL, commuterRLId, 5 commuterRLFL, 6 MergeFn, 7 PartialMergeFn, 8 mergerIdFL, 9 TotalCommuteFn, 10 totalCommuterIdFL, totalCommuterFLId, totalCommuterFLFL, 11 invertCommuter 12 ) where 13 14import Darcs.Prelude 15 16import Darcs.Patch.Invert ( Invert(..) ) 17import Darcs.Patch.Witnesses.Ordered 18 ( (:>)(..) 19 , (:\/:)(..) 20 , (:/\:)(..) 21 , FL(..) 22 , RL(..) 23 ) 24 25-- |CommuteFn is the basis of a general framework for building up commutation 26-- operations between different patch types in a generic manner. Unfortunately 27-- type classes are not well suited to the problem because of the multiple possible 28-- routes by which the commuter for (FL p1, FL p2) can be built out of the 29-- commuter for (p1, p2) - and more complicated problems when we start building 30-- multiple constructors on top of each other. The type class resolution machinery 31-- really can't cope with selecting some route, because it doesn't know that all 32-- possible routes should be equivalent. 33-- 34-- Note that a CommuteFn cannot be lazy i.e. commute patches only when the 35-- resulting sequences are demanded. This is because of the possibility of 36-- failure ('Nothing'): all the commutes must be performed before we can know 37-- whether the overall commute succeeds. 38type CommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> Maybe ((p2 :> p1) wX wY) 39 40type TotalCommuteFn p1 p2 = forall wX wY . (p1 :> p2) wX wY -> (p2 :> p1) wX wY 41 42type MergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> (p2 :/\: p1) wX wY 43 44type PartialMergeFn p1 p2 = forall wX wY . (p1 :\/: p2) wX wY -> Maybe ((p2 :/\: p1) wX wY) 45 46commuterIdRL :: CommuteFn p1 p2 -> CommuteFn p1 (RL p2) 47commuterIdRL _ (x :> NilRL) = return (NilRL :> x) 48commuterIdRL commuter (x :> (ys :<: y)) 49 = do ys' :> x' <- commuterIdRL commuter (x :> ys) 50 y' :> x'' <- commuter (x' :> y) 51 return ((ys' :<: y') :> x'') 52 53commuterIdFL :: CommuteFn p1 p2 -> CommuteFn p1 (FL p2) 54commuterIdFL _ (x :> NilFL) = return (NilFL :> x) 55commuterIdFL commuter (x :> (y :>: ys)) 56 = do y' :> x' <- commuter (x :> y) 57 ys' :> x'' <- commuterIdFL commuter (x' :> ys) 58 return ((y' :>: ys') :> x'') 59 60-- | TODO document laziness or lack thereof 61mergerIdFL :: MergeFn p1 p2 -> MergeFn p1 (FL p2) 62mergerIdFL _ (x :\/: NilFL) = NilFL :/\: x 63mergerIdFL merger (x :\/: (y :>: ys)) 64 = case merger (x :\/: y) of 65 y' :/\: x' -> case mergerIdFL merger (x' :\/: ys) of 66 ys' :/\: x'' -> (y' :>: ys') :/\: x'' 67 68-- | TODO document laziness or lack thereof 69totalCommuterIdFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2) 70totalCommuterIdFL _ (x :> NilFL) = NilFL :> x 71totalCommuterIdFL commuter (x :> (y :>: ys)) = 72 case commuter (x :> y) of 73 y' :> x' -> case totalCommuterIdFL commuter (x' :> ys) of 74 ys' :> x'' -> (y' :>: ys') :> x'' 75 76commuterFLId :: CommuteFn p1 p2 -> CommuteFn (FL p1) p2 77commuterFLId _ (NilFL :> y) = return (y :> NilFL) 78commuterFLId commuter ((x :>: xs) :> y) 79 = do y' :> xs' <- commuterFLId commuter (xs :> y) 80 y'' :> x' <- commuter (x :> y') 81 return (y'' :> (x' :>: xs')) 82 83commuterRLId :: CommuteFn p1 p2 -> CommuteFn (RL p1) p2 84commuterRLId _ (NilRL :> y) = return (y :> NilRL) 85commuterRLId commuter ((xs :<: x) :> y) 86 = do y' :> x' <- commuter (x :> y) 87 y'' :> xs' <- commuterRLId commuter (xs :> y') 88 return (y'' :> (xs' :<: x')) 89 90commuterRLFL :: forall p1 p2. CommuteFn p1 p2 -> CommuteFn (RL p1) (FL p2) 91commuterRLFL commuter (xs :> ys) = right xs ys 92 where 93 right :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ) 94 right as NilFL = Just (NilFL :> as) 95 right as (b :>: bs) = do 96 b' :> as' <- commuterRLId commuter (as :> b) 97 bs' :> as'' <- left as' bs 98 return (b' :>: bs' :> as'') 99 left :: RL p1 wX wY -> FL p2 wY wZ -> Maybe ((FL p2 :> RL p1) wX wZ) 100 left NilRL bs = Just (bs :> NilRL) 101 left (as :<: a) bs = do 102 bs' :> a' <- commuterIdFL commuter (a :> bs) 103 bs'' :> as' <- right as bs' 104 return (bs'' :> as' :<: a') 105 106-- | TODO document laziness or lack thereof 107totalCommuterFLId :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) p2 108totalCommuterFLId _ (NilFL :> y) = y :> NilFL 109totalCommuterFLId commuter ((x :>: xs) :> y) = 110 case totalCommuterFLId commuter (xs :> y) of 111 y' :> xs' -> case commuter (x :> y') of 112 y'' :> x' -> y'' :> (x' :>: xs') 113 114-- | TODO document laziness or lack thereof 115totalCommuterFLFL :: TotalCommuteFn p1 p2 -> TotalCommuteFn (FL p1) (FL p2) 116totalCommuterFLFL commuter = totalCommuterFLId (totalCommuterIdFL commuter) 117 118-- | Make use of the inverse-commute law to reduce the number of cases 119-- when defining commute for complicated patch types. 120{-# INLINE invertCommuter #-} 121invertCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p 122invertCommuter commuter (x :> y) = do 123 ix' :> iy' <- commuter (invert y :> invert x) 124 return (invert iy' :> invert ix') 125