{-# OPTIONS_GHC -fno-warn-orphans #-}
module Darcs.Patch.Permutations ( removeFL, removeRL, removeCommon,
commuteWhatWeCanFL, commuteWhatWeCanRL,
genCommuteWhatWeCanRL, genCommuteWhatWeCanFL,
partitionFL, partitionRL, partitionFL',
simpleHeadPermutationsFL, headPermutationsRL,
headPermutationsFL, permutationsRL,
removeSubsequenceFL, removeSubsequenceRL,
partitionConflictingFL
) where
import Darcs.Prelude
import Data.Maybe ( mapMaybe )
import Darcs.Patch.Commute ( Commute, commute, commuteFL, commuteRL )
import Darcs.Patch.Merge ( CleanMerge(..), cleanMergeFL )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
( FL(..), RL(..), (:>)(..), (:\/:)(..), (:/\:)(..)
, (+<+), (+>+)
, lengthFL, lengthRL
, reverseFL, reverseRL
)
partitionFL :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> FL p wX wY
-> (FL p :> FL p :> FL p) wX wY
partitionFL keepleft ps =
case partitionFL' keepleft NilRL NilRL ps of
left :> middle :> right -> left :> reverseRL middle :> reverseRL right
partitionFL' :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> (FL p :> RL p :> RL p) wA wD
partitionFL' _ middle right NilFL = NilFL :> middle :> right
partitionFL' keepleft middle right (p :>: ps)
| keepleft p = case commuteWhatWeCanRL (right :> p) of
(NilRL :> p' :> right') -> case commuteRL (middle :> p') of
Just (p'' :> middle') -> case partitionFL' keepleft middle' right' ps of
(a :> b :> c) -> p'' :>: a :> b :> c
Nothing -> partitionFL' keepleft (middle :<: p') right' ps
(tomiddle :> p' :> right') ->
partitionFL' keepleft (middle +<+ tomiddle :<: p') right' ps
| otherwise = partitionFL' keepleft middle (right :<: p) ps
partitionRL :: forall p wX wY. Commute p
=> (forall wU wV . p wU wV -> Bool)
-> RL p wX wY
-> (RL p :> RL p) wX wY
partitionRL keepright = go . (:> NilFL)
where
go :: (RL p :> FL p) wA wB -> (RL p :> RL p) wA wB
go (NilRL :> qs) = (reverseFL qs :> NilRL)
go (ps :<: p :> qs)
| keepright p
, Just (qs' :> p') <- commuteFL (p :> qs) =
case go (ps :> qs') of
a :> b -> a :> b :<: p'
| otherwise = go (ps :> p :>: qs)
commuteWhatWeCanFL :: Commute p => (p :> FL p) wX wY -> (FL p :> p :> FL p) wX wY
commuteWhatWeCanFL = genCommuteWhatWeCanFL commute
genCommuteWhatWeCanFL :: Commute q =>
(forall wA wB . ((p:>q) wA wB -> Maybe ((q:>p)wA wB)))
-> (p :> FL q) wX wY -> (FL q :> p :> FL q) wX wY
genCommuteWhatWeCanFL com (p :> x :>: xs) =
case com (p :> x) of
Nothing -> case commuteWhatWeCanFL (x :> xs) of
xs1 :> x' :> xs2 -> case genCommuteWhatWeCanFL com (p :> xs1) of
xs1' :> p' :> xs2' -> xs1' :> p' :> xs2' +>+ x' :>: xs2
Just (x' :> p') -> case genCommuteWhatWeCanFL com (p' :> xs) of
a :> p'' :> c -> x' :>: a :> p'' :> c
genCommuteWhatWeCanFL _ (y :> NilFL) = NilFL :> y :> NilFL
commuteWhatWeCanRL :: Commute p => (RL p :> p) wX wY -> (RL p :> p :> RL p) wX wY
commuteWhatWeCanRL = genCommuteWhatWeCanRL commute
genCommuteWhatWeCanRL :: Commute p =>
(forall wA wB . ((p :> q) wA wB -> Maybe ((q :> p) wA wB)))
-> (RL p :> q) wX wY -> (RL p :> q :> RL p) wX wY
genCommuteWhatWeCanRL com (xs :<: x :> p) =
case com (x :> p) of
Nothing -> case commuteWhatWeCanRL (xs :> x) of
xs1 :> x' :> xs2 -> case genCommuteWhatWeCanRL com (xs2 :> p) of
xs1' :> p' :> xs2' -> xs1 :<: x' +<+ xs1' :> p' :> xs2'
Just (p' :> x') -> case genCommuteWhatWeCanRL com (xs :> p') of
xs1 :> p'' :> xs2 -> xs1 :> p'' :> xs2 :<: x'
genCommuteWhatWeCanRL _ (NilRL :> y) = NilRL :> y :> NilRL
removeCommon :: (Eq2 p, Commute p) => (FL p :\/: FL p) wX wY -> (FL p :\/: FL p) wX wY
removeCommon (xs :\/: NilFL) = xs :\/: NilFL
removeCommon (NilFL :\/: xs) = NilFL :\/: xs
removeCommon (xs :\/: ys) = rc xs (headPermutationsFL ys)
where rc :: (Eq2 p, Commute p) => FL p wX wY -> [(p:>FL p) wX wZ] -> (FL p :\/: FL p) wY wZ
rc nms ((n:>ns):_) | Just ms <- removeFL n nms = removeCommon (ms :\/: ns)
rc ms [n:>ns] = ms :\/: n:>:ns
rc ms (_:nss) = rc ms nss
rc _ [] = error "impossible case"
removeFL :: (Eq2 p, Commute p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL x xs = r x $ headPermutationsFL xs
where r :: (Eq2 p, Commute p) => p wX wY -> [(p:>FL p) wX wZ] -> Maybe (FL p wY wZ)
r _ [] = Nothing
r z ((z':>zs):zss) | IsEq <- z =\/= z' = Just zs
| otherwise = r z zss
removeRL :: (Eq2 p, Commute p) => p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL x xs = r x $ headPermutationsRL xs
where r :: (Eq2 p, Commute p) => p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r z ((zs:<:z'):zss) | IsEq <- z =/\= z' = Just zs
| otherwise = r z zss
r _ _ = Nothing
removeSubsequenceFL :: (Eq2 p, Commute p) => FL p wA wB
-> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL a b | lengthFL a > lengthFL b = Nothing
| otherwise = rsFL a b
where rsFL :: (Eq2 p, Commute p) => FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
rsFL NilFL ys = Just ys
rsFL (x:>:xs) yys = removeFL x yys >>= removeSubsequenceFL xs
removeSubsequenceRL :: (Eq2 p, Commute p) => RL p wAb wAbc
-> RL p wA wAbc -> Maybe (RL p wA wAb)
removeSubsequenceRL a b | lengthRL a > lengthRL b = Nothing
| otherwise = rsRL a b
where rsRL :: (Eq2 p, Commute p) => RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
rsRL NilRL ys = Just ys
rsRL (xs:<:x) yys = removeRL x yys >>= removeSubsequenceRL xs
simpleHeadPermutationsFL :: Commute p => FL p wX wY -> [FL p wX wY]
simpleHeadPermutationsFL ps = map (\ (x:>xs) -> x:>:xs) $ headPermutationsFL ps
headPermutationsFL :: Commute p => FL p wX wY -> [(p :> FL p) wX wY]
headPermutationsFL NilFL = []
headPermutationsFL (p:>:ps) =
(p:>ps) : mapMaybe (swapfirstFL.(p:>)) (headPermutationsFL ps)
where swapfirstFL (p1:>p2:>xs) = do p2':>p1' <- commute (p1:>p2)
Just $ p2':>p1':>:xs
headPermutationsRL :: Commute p => RL p wX wY -> [RL p wX wY]
headPermutationsRL NilRL = []
headPermutationsRL (ps:<:p) =
(ps:<:p) : mapMaybe (swapfirstRL.(:<:p)) (headPermutationsRL ps)
where swapfirstRL (xs:<:p2:<:p1) = do p1':>p2' <- commute (p2:>p1)
Just $ xs:<:p1':<:p2'
swapfirstRL _ = Nothing
permutationsRL :: Commute p => RL p wX wY -> [RL p wX wY]
permutationsRL ps =
[qs' :<: q | qs :<: q <- headPermutationsRL ps, qs' <- permutationsRL qs]
instance (Eq2 p, Commute p) => Eq2 (FL p) where
a =\/= b | lengthFL a /= lengthFL b = NotEq
| otherwise = cmpSameLength a b
where cmpSameLength :: FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
cmpSameLength (x:>:xs) xys | Just ys <- removeFL x xys = cmpSameLength xs ys
cmpSameLength NilFL NilFL = IsEq
cmpSameLength _ _ = NotEq
xs =/\= ys = reverseFL xs =/\= reverseFL ys
instance (Eq2 p, Commute p) => Eq2 (RL p) where
unsafeCompare = error "Buggy use of unsafeCompare on RL"
a =/\= b | lengthRL a /= lengthRL b = NotEq
| otherwise = cmpSameLength a b
where cmpSameLength :: RL p wX wY -> RL p wW wY -> EqCheck wX wW
cmpSameLength (xs:<:x) xys | Just ys <- removeRL x xys = cmpSameLength xs ys
cmpSameLength NilRL NilRL = IsEq
cmpSameLength _ _ = NotEq
xs =\/= ys = reverseRL xs =\/= reverseRL ys
partitionConflictingFL :: (Commute p, CleanMerge p)
=> FL p wX wY -> FL p wX wZ -> (FL p :> FL p) wX wY
partitionConflictingFL NilFL _ = NilFL :> NilFL
partitionConflictingFL (x :>: xs) ys =
case cleanMergeFL (x :\/: ys) of
Nothing ->
case commuteWhatWeCanFL (x :> xs) of
xs_ok :> x' :> xs_deps ->
case partitionConflictingFL xs_ok ys of
xs_clean :> xs_conflicts ->
xs_clean :> (xs_conflicts +>+ (x' :>: xs_deps))
Just (ys' :/\: _) ->
case partitionConflictingFL xs ys' of
xs_clean :> xs_conflicts -> (x :>: xs_clean) :> xs_conflicts