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