{-# 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> FL p wX wY -> (:>) (FL p) (FL p :> FL p) wX wY
partitionFL forall wU wV. p wU wV -> Bool
keepleft FL p wX wY
ps =
case forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
keepleft forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL p wX wY
ps of
FL p wX wZ
left :> RL p wZ wZ
middle :> RL p wZ wY
right -> FL p wX wZ
left forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wZ
middle forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wY
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' :: forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
_ RL p wA wB
middle RL p wB wC
right FL p wC wD
NilFL = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wA wB
middle forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wB wC
right
partitionFL' forall wU wV. p wU wV -> Bool
keepleft RL p wA wB
middle RL p wB wC
right (p wC wY
p :>: FL p wY wD
ps)
| forall wU wV. p wU wV -> Bool
keepleft p wC wY
p = case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL (RL p wB wC
right forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wC wY
p) of
(RL p wB wZ
NilRL :> p wZ wZ
p' :> RL p wZ wY
right') -> case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wA wB
middle forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p') of
Just (p wA wZ
p'' :> RL p wZ wZ
middle') -> case forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
keepleft RL p wZ wZ
middle' RL p wZ wY
right' FL p wY wD
ps of
(FL p wZ wZ
a :> RL p wZ wZ
b :> RL p wZ wD
c) -> p wA wZ
p'' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
b forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wD
c
Maybe ((:>) p (RL p) wA wZ)
Nothing -> forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
keepleft (RL p wA wB
middle forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
p') RL p wZ wY
right' FL p wY wD
ps
(RL p wB wZ
tomiddle :> p wZ wZ
p' :> RL p wZ wY
right') ->
forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
keepleft (RL p wA wB
middle forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL p wB wZ
tomiddle forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
p') RL p wZ wY
right' FL p wY wD
ps
| Bool
otherwise = forall (p :: * -> * -> *) wA wB wC wD.
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' forall wU wV. p wU wV -> Bool
keepleft RL p wA wB
middle (RL p wB wC
right forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wC wY
p) FL p wY wD
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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> (:>) (RL p) (RL p) wX wY
partitionRL forall wU wV. p wU wV -> Bool
keepright = forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
where
go :: (RL p :> FL p) wA wB -> (RL p :> RL p) wA wB
go :: forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go (RL p wA wZ
NilRL :> FL p wZ wB
qs) = (forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wZ wB
qs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
go (RL p wA wY
ps :<: p wY wZ
p :> FL p wZ wB
qs)
| forall wU wV. p wU wV -> Bool
keepright p wY wZ
p
, Just (FL p wY wZ
qs' :> p wZ wB
p') <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
qs) =
case forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wZ
qs') of
RL p wA wZ
a :> RL p wZ wZ
b -> RL p wA wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
b forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wB
p'
| Bool
otherwise = forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go (RL p wA wY
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wB
qs)
commuteWhatWeCanFL :: Commute p => (p :> FL p) wX wY -> (FL p :> p :> FL p) wX wY
commuteWhatWeCanFL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL = forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
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 :: forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wX wZ
p :> q wZ wY
x :>: FL q wY wY
xs) =
case forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wX wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
x) of
Maybe ((:>) q p wX wY)
Nothing -> case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (q wZ wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wY wY
xs) of
FL q wZ wZ
xs1 :> q wZ wZ
x' :> FL q wZ wY
xs2 -> case forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wX wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wZ
xs1) of
FL q wX wZ
xs1' :> p wZ wZ
p' :> FL q wZ wZ
xs2' -> FL q wX wZ
xs1' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wZ
xs2' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ q wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL q wZ wY
xs2
Just (q wX wZ
x' :> p wZ wY
p') -> case forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wZ wY
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wY wY
xs) of
FL q wZ wZ
a :> p wZ wZ
p'' :> FL q wZ wY
c -> q wX wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL q wZ wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wY
c
genCommuteWhatWeCanFL forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
_ (p wX wZ
y :> FL q wZ wY
NilFL) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wX wZ
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
commuteWhatWeCanRL :: Commute p => (RL p :> p) wX wY -> (RL p :> p :> RL p) wX wY
commuteWhatWeCanRL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL = forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
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 :: forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (RL p wX wY
xs :<: p wY wZ
x :> q wZ wY
p) =
case forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wY wZ
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
p) of
Maybe ((:>) q p wY wY)
Nothing -> case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL (RL p wX wY
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
x) of
RL p wX wZ
xs1 :> p wZ wZ
x' :> RL p wZ wZ
xs2 -> case forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (RL p wZ wZ
xs2 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
p) of
RL p wZ wZ
xs1' :> q wZ wZ
p' :> RL p wZ wY
xs2' -> RL p wX wZ
xs1 forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL p wZ wZ
xs1' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wZ
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
xs2'
Just (q wY wZ
p' :> p wZ wY
x') -> case forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
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 forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (RL p wX wY
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wY wZ
p') of
RL p wX wZ
xs1 :> q wZ wZ
p'' :> RL p wZ wZ
xs2 -> RL p wX wZ
xs1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wZ
p'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
xs2 forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wY
x'
genCommuteWhatWeCanRL forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
_ (RL p wX wZ
NilRL :> q wZ wY
y) = forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
y forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
removeCommon :: (Eq2 p, Commute p) => (FL p :\/: FL p) wX wY -> (FL p :\/: FL p) wX wY
removeCommon :: forall (p :: * -> * -> *) wX wY.
(Eq2 p, Commute p) =>
(:\/:) (FL p) (FL p) wX wY -> (:\/:) (FL p) (FL p) wX wY
removeCommon (FL p wZ wX
xs :\/: FL p wZ wY
NilFL) = FL p wZ wX
xs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
removeCommon (FL p wZ wX
NilFL :\/: FL p wZ wY
xs) = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wY
xs
removeCommon (FL p wZ wX
xs :\/: FL p wZ wY
ys) = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
FL p wX wY -> [(:>) p (FL p) wX wZ] -> (:\/:) (FL p) (FL p) wY wZ
rc FL p wZ wX
xs (forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL FL p wZ wY
ys)
where rc :: (Eq2 p, Commute p) => FL p wX wY -> [(p:>FL p) wX wZ] -> (FL p :\/: FL p) wY wZ
rc :: forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
FL p wX wY -> [(:>) p (FL p) wX wZ] -> (:\/:) (FL p) (FL p) wY wZ
rc FL p wX wY
nms ((p wX wZ
n:>FL p wZ wZ
ns):[(:>) p (FL p) wX wZ]
_) | Just FL p wZ wY
ms <- forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL p wX wZ
n FL p wX wY
nms = forall (p :: * -> * -> *) wX wY.
(Eq2 p, Commute p) =>
(:\/:) (FL p) (FL p) wX wY -> (:\/:) (FL p) (FL p) wX wY
removeCommon (FL p wZ wY
ms forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wZ
ns)
rc FL p wX wY
ms [p wX wZ
n:>FL p wZ wZ
ns] = FL p wX wY
ms forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p wX wZ
nforall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL p wZ wZ
ns
rc FL p wX wY
ms ((:>) p (FL p) wX wZ
_:[(:>) p (FL p) wX wZ]
nss) = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
FL p wX wY -> [(:>) p (FL p) wX wZ] -> (:\/:) (FL p) (FL p) wY wZ
rc FL p wX wY
ms [(:>) p (FL p) wX wZ]
nss
rc FL p wX wY
_ [] = forall a. HasCallStack => [Char] -> a
error [Char]
"impossible case"
removeFL :: (Eq2 p, Commute p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL :: forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL p wX wY
x FL p wX wZ
xs = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
r p wX wY
x forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL FL p wX wZ
xs
where r :: (Eq2 p, Commute p) => p wX wY -> [(p:>FL p) wX wZ] -> Maybe (FL p wY wZ)
r :: forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
r p wX wY
_ [] = forall a. Maybe a
Nothing
r p wX wY
z ((p wX wZ
z':>FL p wZ wZ
zs):[(:>) p (FL p) wX wZ]
zss) | EqCheck wY wZ
IsEq <- p wX wY
z forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wX wZ
z' = forall a. a -> Maybe a
Just FL p wZ wZ
zs
| Bool
otherwise = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
r p wX wY
z [(:>) p (FL p) wX wZ]
zss
removeRL :: (Eq2 p, Commute p) => p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL :: forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL p wY wZ
x RL p wX wZ
xs = forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r p wY wZ
x forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
headPermutationsRL RL p wX wZ
xs
where r :: (Eq2 p, Commute p) => p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r :: forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r p wY wZ
z ((RL p wX wY
zs:<:p wY wZ
z'):[RL p wX wZ]
zss) | EqCheck wY wY
IsEq <- p wY wZ
z forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= p wY wZ
z' = forall a. a -> Maybe a
Just RL p wX wY
zs
| Bool
otherwise = forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r p wY wZ
z [RL p wX wZ]
zss
r p wY wZ
_ [RL p wX wZ]
_ = forall a. Maybe a
Nothing
removeSubsequenceFL :: (Eq2 p, Commute p) => FL p wA wB
-> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL :: forall (p :: * -> * -> *) wA wB wC.
(Eq2 p, Commute p) =>
FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL FL p wA wB
a FL p wA wC
b | forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wB
a forall a. Ord a => a -> a -> Bool
> forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wC
b = forall a. Maybe a
Nothing
| Bool
otherwise = forall (p :: * -> * -> *) wA wB wC.
(Eq2 p, Commute p) =>
FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
rsFL FL p wA wB
a FL p wA wC
b
where rsFL :: (Eq2 p, Commute p) => FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
rsFL :: forall (p :: * -> * -> *) wA wB wC.
(Eq2 p, Commute p) =>
FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
rsFL FL p wA wB
NilFL FL p wA wC
ys = forall a. a -> Maybe a
Just FL p wA wC
ys
rsFL (p wA wY
x:>:FL p wY wB
xs) FL p wA wC
yys = forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL p wA wY
x FL p wA wC
yys forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: * -> * -> *) wA wB wC.
(Eq2 p, Commute p) =>
FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL FL p wY wB
xs
removeSubsequenceRL :: (Eq2 p, Commute p) => RL p wAb wAbc
-> RL p wA wAbc -> Maybe (RL p wA wAb)
removeSubsequenceRL :: forall (p :: * -> * -> *) wAb wAbc wA.
(Eq2 p, Commute p) =>
RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
removeSubsequenceRL RL p wAb wAbc
a RL p wA wAbc
b | forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wAb wAbc
a forall a. Ord a => a -> a -> Bool
> forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wA wAbc
b = forall a. Maybe a
Nothing
| Bool
otherwise = forall (p :: * -> * -> *) wAb wAbc wA.
(Eq2 p, Commute p) =>
RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
rsRL RL p wAb wAbc
a RL p wA wAbc
b
where rsRL :: (Eq2 p, Commute p) => RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
rsRL :: forall (p :: * -> * -> *) wAb wAbc wA.
(Eq2 p, Commute p) =>
RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
rsRL RL p wAb wAbc
NilRL RL p wA wAbc
ys = forall a. a -> Maybe a
Just RL p wA wAbc
ys
rsRL (RL p wAb wY
xs:<:p wY wAbc
x) RL p wA wAbc
yys = forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL p wY wAbc
x RL p wA wAbc
yys forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (p :: * -> * -> *) wAb wAbc wA.
(Eq2 p, Commute p) =>
RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
removeSubsequenceRL RL p wAb wY
xs
simpleHeadPermutationsFL :: Commute p => FL p wX wY -> [FL p wX wY]
simpleHeadPermutationsFL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [FL p wX wY]
simpleHeadPermutationsFL FL p wX wY
ps = forall a b. (a -> b) -> [a] -> [b]
map (\ (p wX wZ
x:>FL p wZ wY
xs) -> p wX wZ
xforall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL p wZ wY
xs) forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL FL p wX wY
ps
headPermutationsFL :: Commute p => FL p wX wY -> [(p :> FL p) wX wY]
headPermutationsFL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL FL p wX wY
NilFL = []
headPermutationsFL (p wX wY
p:>:FL p wY wY
ps) =
(p wX wY
pforall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>FL p wY wY
ps) forall a. a -> [a] -> [a]
: forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {a1 :: * -> * -> *} {wX} {wY}.
Commute a1 =>
(:>) a1 (a1 :> FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY)
swapfirstFLforall b c a. (b -> c) -> (a -> b) -> a -> c
.(p wX wY
pforall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>)) (forall (p :: * -> * -> *) wX wY.
Commute p =>
FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL FL p wY wY
ps)
where swapfirstFL :: (:>) a1 (a1 :> FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY)
swapfirstFL (a1 wX wZ
p1:>a1 wZ wZ
p2:>FL a1 wZ wY
xs) = do a1 wX wZ
p2':>a1 wZ wZ
p1' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (a1 wX wZ
p1forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a1 wZ wZ
p2)
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ a1 wX wZ
p2'forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a1 wZ wZ
p1'forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL a1 wZ wY
xs
headPermutationsRL :: Commute p => RL p wX wY -> [RL p wX wY]
headPermutationsRL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
headPermutationsRL RL p wX wY
NilRL = []
headPermutationsRL (RL p wX wY
ps:<:p wY wY
p) =
(RL p wX wY
psforall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:p wY wY
p) forall a. a -> [a] -> [a]
: forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall {a :: * -> * -> *} {wX} {wZ}.
Commute a =>
RL a wX wZ -> Maybe (RL a wX wZ)
swapfirstRLforall b c a. (b -> c) -> (a -> b) -> a -> c
.(forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:p wY wY
p)) (forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
headPermutationsRL RL p wX wY
ps)
where swapfirstRL :: RL a wX wZ -> Maybe (RL a wX wZ)
swapfirstRL (RL a wX wY
xs:<:a wY wY
p2:<:a wY wZ
p1) = do a wY wZ
p1':>a wZ wZ
p2' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (a wY wY
p2forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a wY wZ
p1)
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ RL a wX wY
xsforall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:a wY wZ
p1'forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:a wZ wZ
p2'
swapfirstRL RL a wX wZ
_ = forall a. Maybe a
Nothing
permutationsRL :: Commute p => RL p wX wY -> [RL p wX wY]
permutationsRL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
permutationsRL RL p wX wY
ps =
[RL p wX wY
qs' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wY wY
q | RL p wX wY
qs :<: p wY wY
q <- forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
headPermutationsRL RL p wX wY
ps, RL p wX wY
qs' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
permutationsRL RL p wX wY
qs]
instance (Eq2 p, Commute p) => Eq2 (FL p) where
FL p wA wB
a =\/= :: forall wA wB wC. FL p wA wB -> FL p wA wC -> EqCheck wB wC
=\/= FL p wA wC
b | forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wB
a forall a. Eq a => a -> a -> Bool
/= forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wC
b = forall wA wB. EqCheck wA wB
NotEq
| Bool
otherwise = forall wA wB wC. FL p wA wB -> FL p wA wC -> EqCheck wB wC
cmpSameLength FL p wA wB
a FL p wA wC
b
where cmpSameLength :: FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
cmpSameLength :: forall wA wB wC. FL p wA wB -> FL p wA wC -> EqCheck wB wC
cmpSameLength (p wX wY
x:>:FL p wY wY
xs) FL p wX wZ
xys | Just FL p wY wZ
ys <- forall (p :: * -> * -> *) wX wY wZ.
(Eq2 p, Commute p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL p wX wY
x FL p wX wZ
xys = forall wA wB wC. FL p wA wB -> FL p wA wC -> EqCheck wB wC
cmpSameLength FL p wY wY
xs FL p wY wZ
ys
cmpSameLength FL p wX wY
NilFL FL p wX wZ
NilFL = forall wA. EqCheck wA wA
IsEq
cmpSameLength FL p wX wY
_ FL p wX wZ
_ = forall wA wB. EqCheck wA wB
NotEq
FL p wA wC
xs =/\= :: forall wA wC wB. FL p wA wC -> FL p wB wC -> EqCheck wA wB
=/\= FL p wB wC
ys = forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wA wC
xs forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wB wC
ys
instance (Eq2 p, Commute p) => Eq2 (RL p) where
unsafeCompare :: forall wA wB wC wD. RL p wA wB -> RL p wC wD -> Bool
unsafeCompare = forall a. HasCallStack => [Char] -> a
error [Char]
"Buggy use of unsafeCompare on RL"
RL p wA wC
a =/\= :: forall wA wC wB. RL p wA wC -> RL p wB wC -> EqCheck wA wB
=/\= RL p wB wC
b | forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wA wC
a forall a. Eq a => a -> a -> Bool
/= forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wB wC
b = forall wA wB. EqCheck wA wB
NotEq
| Bool
otherwise = forall wA wC wB. RL p wA wC -> RL p wB wC -> EqCheck wA wB
cmpSameLength RL p wA wC
a RL p wB wC
b
where cmpSameLength :: RL p wX wY -> RL p wW wY -> EqCheck wX wW
cmpSameLength :: forall wA wC wB. RL p wA wC -> RL p wB wC -> EqCheck wA wB
cmpSameLength (RL p wX wY
xs:<:p wY wY
x) RL p wW wY
xys | Just RL p wW wY
ys <- forall (p :: * -> * -> *) wY wZ wX.
(Eq2 p, Commute p) =>
p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL p wY wY
x RL p wW wY
xys = forall wA wC wB. RL p wA wC -> RL p wB wC -> EqCheck wA wB
cmpSameLength RL p wX wY
xs RL p wW wY
ys
cmpSameLength RL p wX wY
NilRL RL p wW wY
NilRL = forall wA. EqCheck wA wA
IsEq
cmpSameLength RL p wX wY
_ RL p wW wY
_ = forall wA wB. EqCheck wA wB
NotEq
RL p wA wB
xs =\/= :: forall wA wB wC. RL p wA wB -> RL p wA wC -> EqCheck wB wC
=\/= RL p wA wC
ys = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wA wB
xs forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wA wC
ys
partitionConflictingFL :: (Commute p, CleanMerge p)
=> FL p wX wY -> FL p wX wZ -> (FL p :> FL p) wX wY
partitionConflictingFL :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, CleanMerge p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
partitionConflictingFL FL p wX wY
NilFL FL p wX wZ
_ = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
partitionConflictingFL (p wX wY
x :>: FL p wY wY
xs) FL p wX wZ
ys =
case forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p wX wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wX wZ
ys) of
Maybe ((:/\:) (FL p) p wY wZ)
Nothing ->
case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p wX wY
x forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
xs) of
FL p wX wZ
xs_ok :> p wZ wZ
x' :> FL p wZ wY
xs_deps ->
case forall (p :: * -> * -> *) wX wY wZ.
(Commute p, CleanMerge p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
partitionConflictingFL FL p wX wZ
xs_ok FL p wX wZ
ys of
FL p wX wZ
xs_clean :> FL p wZ wZ
xs_conflicts ->
FL p wX wZ
xs_clean forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL p wZ wZ
xs_conflicts forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (p wZ wZ
x' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wY
xs_deps))
Just (FL p wY wZ
ys' :/\: p wZ wZ
_) ->
case forall (p :: * -> * -> *) wX wY wZ.
(Commute p, CleanMerge p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
partitionConflictingFL FL p wY wY
xs FL p wY wZ
ys' of
FL p wY wZ
xs_clean :> FL p wZ wY
xs_conflicts -> (p wX wY
x forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wZ
xs_clean) forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wY
xs_conflicts