{-# OPTIONS_GHC -fno-warn-orphans #-}
module Darcs.Patch.Permutations ( removeFL, removeRL, removeCommon,
commuteWhatWeCanFL, commuteWhatWeCanRL,
genCommuteWhatWeCanRL, genCommuteWhatWeCanFL,
partitionFL, partitionRL,
simpleHeadPermutationsFL, headPermutationsRL,
headPermutationsFL,
removeSubsequenceFL, removeSubsequenceRL,
partitionConflictingFL,
inverseCommuter
) where
import Prelude ()
import Darcs.Prelude
import Data.Maybe ( mapMaybe )
import Darcs.Patch.Commute ( Commute, commute, commuteFLorComplain, commuteRL )
import Darcs.Patch.CommuteFn ( CommuteFn )
import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
( FL(..), RL(..), (:>)(..), (+<+)
, reverseFL, (+>+), (:\/:)(..), lengthFL
, lengthRL, reverseRL )
partitionFL :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> FL p wX wY
-> (FL p :> FL p :> FL p) wX wY
partitionFL' :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> (FL p :> FL p :> FL p) wA wD
partitionFL :: (forall wU wV. p wU wV -> Bool)
-> FL p wX wY -> (:>) (FL p) (FL p :> FL p) wX wY
partitionFL keepleft :: forall wU wV. p wU wV -> Bool
keepleft = (forall wU wV. p wU wV -> Bool)
-> RL p wX wX
-> RL p wX wX
-> FL p wX wY
-> (:>) (FL p) (FL p :> FL p) wX wY
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) (FL p :> FL p) wA wD
partitionFL' forall wU wV. p wU wV -> Bool
keepleft RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
partitionFL' :: (forall wU wV. p wU wV -> Bool)
-> RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> (:>) (FL p) (FL p :> FL p) wA wD
partitionFL' _ middle :: RL p wA wB
middle right :: RL p wB wC
right NilFL = FL p wA wA
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wA wA
-> (:>) (FL p) (FL p) wA wC -> (:>) (FL p) (FL p :> FL p) wA wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wA wB -> FL p wA wB
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wA wB
middle FL p wA wB -> FL p wB wC -> (:>) (FL p) (FL p) wA wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wB wC -> FL p wB wC
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wB wC
right
partitionFL' keepleft :: forall wU wV. p wU wV -> Bool
keepleft middle :: RL p wA wB
middle right :: RL p wB wC
right (p :: p wC wY
p :>: ps :: FL p wY wD
ps)
| p wC wY -> Bool
forall wU wV. p wU wV -> Bool
keepleft p wC wY
p = case (:>) (RL p) p wB wY -> Maybe ((:>) p (RL p) wB wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wB wC
right RL p wB wC -> p wC wY -> (:>) (RL p) p wB wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wC wY
p) of
Just (p' :: p wB wZ
p' :> right' :: RL p wZ wY
right') -> case (:>) (RL p) p wA wZ -> Maybe ((:>) p (RL p) wA wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wA wB
middle RL p wA wB -> p wB wZ -> (:>) (RL p) p wA wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wB wZ
p') of
Just (p'' :: p wA wZ
p'' :> middle' :: RL p wZ wZ
middle') -> case (forall wU wV. p wU wV -> Bool)
-> RL p wZ wZ
-> RL p wZ wY
-> FL p wY wD
-> (:>) (FL p) (FL p :> FL p) wZ wD
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) (FL p :> FL 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
(a :: FL p wZ wZ
a :> b :: FL p wZ wZ
b :> c :: FL p wZ wD
c) -> p wA wZ
p'' p wA wZ -> FL p wZ wZ -> FL p wA wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
a FL p wA wZ
-> (:>) (FL p) (FL p) wZ wD -> (:>) (FL p) (FL p :> FL p) wA wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wZ
b FL p wZ wZ -> FL p wZ wD -> (:>) (FL p) (FL p) wZ wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wD
c
Nothing -> (forall wU wV. p wU wV -> Bool)
-> RL p wA wZ
-> RL p wZ wY
-> FL p wY wD
-> (:>) (FL p) (FL p :> FL p) wA wD
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) (FL p :> FL p) wA wD
partitionFL' forall wU wV. p wU wV -> Bool
keepleft (RL p wA wB
middle RL p wA wB -> p wB wZ -> RL p wA wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wB wZ
p') RL p wZ wY
right' FL p wY wD
ps
Nothing -> case (:>) (RL p) p wB wY -> (:>) (RL p) (p :> RL p) wB wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL (RL p wB wC
right RL p wB wC -> p wC wY -> (:>) (RL p) p wB wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wC wY
p) of
(tomiddle :: RL p wB wZ
tomiddle :> p' :: p wZ wZ
p' :> right' :: RL p wZ wY
right') -> (forall wU wV. p wU wV -> Bool)
-> RL p wA wZ
-> RL p wZ wY
-> FL p wY wD
-> (:>) (FL p) (FL p :> FL p) wA wD
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) (FL p :> FL p) wA wD
partitionFL' forall wU wV. p wU wV -> Bool
keepleft (RL p wA wB
middle RL p wA wB -> RL p wB wZ -> RL p wA wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL p wB wZ
tomiddle RL p wA wZ -> p wZ wZ -> RL p wA wZ
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 wU wV. p wU wV -> Bool)
-> RL p wA wB
-> RL p wB wY
-> FL p wY wD
-> (:>) (FL p) (FL p :> FL p) wA wD
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) (FL p :> FL p) wA wD
partitionFL' forall wU wV. p wU wV -> Bool
keepleft RL p wA wB
middle (RL p wB wC
right RL p wB wC -> p wC wY -> RL p wB wY
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 :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> RL p wX wY
-> (RL p :> RL p) wX wY
partitionRL' :: Commute p
=> (forall wU wV . p wU wV -> Bool)
-> RL p wX wZ
-> FL p wZ wY
-> (RL p :> RL p) wX wY
partitionRL :: (forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> (:>) (RL p) (RL p) wX wY
partitionRL keepright :: forall wU wV. p wU wV -> Bool
keepright ps :: RL p wX wY
ps = (forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> FL p wY wY -> (:>) (RL p) (RL p) wX wY
forall (p :: * -> * -> *) wX wZ wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (RL p) wX wY
partitionRL' forall wU wV. p wU wV -> Bool
keepright RL p wX wY
ps FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
partitionRL' :: (forall wU wV. p wU wV -> Bool)
-> RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (RL p) wX wY
partitionRL' _ NilRL qs :: FL p wZ wY
qs = FL p wZ wY -> RL p wZ wY
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wZ wY
qs RL p wZ wY -> RL p wY wY -> (:>) (RL p) (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wY wY
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
partitionRL' keepright :: forall wU wV. p wU wV -> Bool
keepright (ps :: RL p wX wY
ps :<: p :: p wY wZ
p) qs :: FL p wZ wY
qs
| p wY wZ -> Bool
forall wU wV. p wU wV -> Bool
keepright p wY wZ
p,
Right (qs' :: FL p wY wZ
qs' :> p' :: p wZ wY
p') <- (:>) p (FL p) wY wY -> Either (Sealed2 p) ((:>) (FL p) p wY wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Either (Sealed2 p) ((:>) (FL p) p wX wY)
commuteFLorComplain (p wY wZ
p p wY wZ -> FL p wZ wY -> (:>) p (FL p) wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wY
qs)
= case (forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> FL p wY wZ -> (:>) (RL p) (RL p) wX wZ
forall (p :: * -> * -> *) wX wZ wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (RL p) wX wY
partitionRL' forall wU wV. p wU wV -> Bool
keepright RL p wX wY
ps FL p wY wZ
qs' of
a :: RL p wX wZ
a :> b :: RL p wZ wZ
b -> RL p wX wZ
a RL p wX wZ -> RL p wZ wY -> (:>) (RL p) (RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
b RL p wZ wZ -> p wZ wY -> RL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wY
p'
| Bool
otherwise = (forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> FL p wY wY -> (:>) (RL p) (RL p) wX wY
forall (p :: * -> * -> *) wX wZ wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wZ -> FL p wZ wY -> (:>) (RL p) (RL p) wX wY
partitionRL' forall wU wV. p wU wV -> Bool
keepright RL p wX wY
ps (p wY wZ
p p wY wZ -> FL p wZ wY -> FL p wY wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wY
qs)
commuteWhatWeCanFL :: Commute p => (p :> FL p) wX wY -> (FL p :> p :> FL p) wX wY
commuteWhatWeCanFL :: (:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL = (forall wA wB. (:>) p p wA wB -> Maybe ((:>) p p wA wB))
-> (:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
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 p wA wB -> Maybe ((:>) p p wA wB)
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 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 :: forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p :: p wX wZ
p :> x :: q wZ wY
x :>: xs :: FL q wY wY
xs) =
case (:>) p q wX wY -> Maybe ((:>) q p wX wY)
forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wX wZ
p 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 wZ wY
x) of
Nothing -> case (:>) q (FL q) wZ wY -> (:>) (FL q) (q :> FL q) wZ wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (q wZ wY
x q wZ wY -> FL q wY wY -> (:>) q (FL q) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wY wY
xs) of
xs1 :: FL q wZ wZ
xs1 :> x' :: q wZ wZ
x' :> xs2 :: FL q wZ wY
xs2 -> case (forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB))
-> (:>) p (FL q) wX wZ -> (:>) (FL q) (p :> FL q) wX wZ
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 p wX wZ -> FL q wZ wZ -> (:>) p (FL q) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wZ
xs1) of
xs1' :: FL q wX wZ
xs1' :> p' :: p wZ wZ
p' :> xs2' :: FL q wZ wZ
xs2' -> FL q wX wZ
xs1' FL q wX wZ -> (:>) p (FL q) wZ wY -> (:>) (FL q) (p :> FL q) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p' p wZ wZ -> FL q wZ wY -> (:>) p (FL q) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wZ
xs2' FL q wZ wZ -> FL q wZ wY -> FL q wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ q wZ wZ
x' q wZ wZ -> FL q wZ wY -> FL q wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL q wZ wY
xs2
Just (x' :: q wX wZ
x' :> p' :: p wZ wY
p') -> case (forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB))
-> (:>) p (FL q) wZ wY -> (:>) (FL q) (p :> FL q) wZ wY
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' p wZ wY -> FL q wY wY -> (:>) p (FL q) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wY wY
xs) of
a :: FL q wZ wZ
a :> p'' :: p wZ wZ
p'' :> c :: FL q wZ wY
c -> q wX wZ
x' q wX wZ -> FL q wZ wZ -> FL q wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL q wZ wZ
a FL q wX wZ -> (:>) p (FL q) wZ wY -> (:>) (FL q) (p :> FL q) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p'' p wZ wZ -> FL q wZ wY -> (:>) p (FL q) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wY
c
genCommuteWhatWeCanFL _ (y :: p wX wZ
y :> NilFL) = FL q wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL q wX wX -> (:>) p (FL q) wX wZ -> (:>) (FL q) (p :> FL q) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wX wZ
y p wX wZ -> FL q wZ wZ -> (:>) p (FL q) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
commuteWhatWeCanRL :: Commute p => (RL p :> p) wX wY -> (RL p :> p :> RL p) wX wY
commuteWhatWeCanRL :: (:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL = (forall wA wB. (:>) p p wA wB -> Maybe ((:>) p p wA wB))
-> (:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
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 p wA wB -> Maybe ((:>) p p wA wB)
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 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 :: forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (xs :: RL p wX wY
xs :<: x :: p wY wZ
x :> p :: q wZ wY
p) =
case (:>) p q wY wY -> Maybe ((:>) q p wY wY)
forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB)
com (p wY wZ
x p wY wZ -> q wZ wY -> (:>) p q wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
p) of
Nothing -> case (:>) (RL p) p wX wZ -> (:>) (RL p) (p :> RL p) wX wZ
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL (RL p wX wY
xs RL p wX wY -> p wY wZ -> (:>) (RL p) p wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
x) of
xs1 :: RL p wX wZ
xs1 :> x' :: p wZ wZ
x' :> xs2 :: RL p wZ wZ
xs2 -> case (forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB))
-> (:>) (RL p) q wZ wY -> (:>) (RL p) (q :> RL p) wZ wY
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 RL p wZ wZ -> q wZ wY -> (:>) (RL p) q wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
p) of
xs1' :: RL p wZ wZ
xs1' :> p' :: q wZ wZ
p' :> xs2' :: RL p wZ wY
xs2' -> RL p wX wZ
xs1 RL p wX wZ -> p wZ wZ -> RL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
x' RL p wX wZ -> RL p wZ wZ -> RL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL p wZ wZ
xs1' RL p wX wZ -> (:>) q (RL p) wZ wY -> (:>) (RL p) (q :> RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wZ
p' q wZ wZ -> RL p wZ wY -> (:>) q (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
xs2'
Just (p' :: q wY wZ
p' :> x' :: p wZ wY
x') -> case (forall wA wB. (:>) p q wA wB -> Maybe ((:>) q p wA wB))
-> (:>) (RL p) q wX wZ -> (:>) (RL p) (q :> RL p) wX wZ
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 RL p wX wY -> q wY wZ -> (:>) (RL p) q wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wY wZ
p') of
xs1 :: RL p wX wZ
xs1 :> p'' :: q wZ wZ
p'' :> xs2 :: RL p wZ wZ
xs2 -> RL p wX wZ
xs1 RL p wX wZ -> (:>) q (RL p) wZ wY -> (:>) (RL p) (q :> RL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wZ
p'' q wZ wZ -> RL p wZ wY -> (:>) q (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
xs2 RL p wZ wZ -> p wZ wY -> RL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wY
x'
genCommuteWhatWeCanRL _ (NilRL :> y :: q wZ wY
y) = RL p wZ wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wZ wZ -> (:>) q (RL p) wZ wY -> (:>) (RL p) (q :> RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> q wZ wY
y q wZ wY -> RL p wY wY -> (:>) q (RL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wY 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 :: (:\/:) (FL p) (FL p) wX wY -> (:\/:) (FL p) (FL p) wX wY
removeCommon (xs :: FL p wZ wX
xs :\/: NilFL) = FL p wZ wX
xs FL p wZ wX -> FL p wZ wZ -> (:\/:) (FL p) (FL p) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
removeCommon (NilFL :\/: xs :: FL p wZ wY
xs) = FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wZ wZ -> FL p wZ wY -> (:\/:) (FL p) (FL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wY
xs
removeCommon (xs :: FL p wZ wX
xs :\/: ys :: FL p wZ wY
ys) = FL p wZ wX -> [(:>) p (FL p) wZ wY] -> (:\/:) (FL p) (FL p) wX wY
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 (FL p wZ wY -> [(:>) p (FL p) wZ wY]
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 :: FL p wX wY -> [(:>) p (FL p) wX wZ] -> (:\/:) (FL p) (FL p) wY wZ
rc nms :: FL p wX wY
nms ((n :: p wX wZ
n:>ns :: FL p wZ wZ
ns):_) | Just ms :: FL p wZ wY
ms <- p wX wZ -> FL p wX wY -> Maybe (FL p wZ wY)
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 = (:\/:) (FL p) (FL p) wY wZ -> (:\/:) (FL p) (FL p) wY wZ
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 FL p wZ wY -> FL p wZ wZ -> (:\/:) (FL p) (FL p) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wZ
ns)
rc ms :: FL p wX wY
ms [n :: p wX wZ
n:>ns :: FL p wZ wZ
ns] = FL p wX wY
ms FL p wX wY -> FL p wX wZ -> (:\/:) (FL p) (FL p) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p wX wZ
np wX wZ -> FL p wZ wZ -> FL p wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL p wZ wZ
ns
rc ms :: FL p wX wY
ms (_:nss :: [(:>) p (FL p) wX wZ]
nss) = FL p wX wY -> [(:>) p (FL p) wX wZ] -> (:\/:) (FL p) (FL p) wY wZ
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) (FL p) wY wZ
forall a. a
impossible
removeFL :: (Eq2 p, Commute p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL :: p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
removeFL x :: p wX wY
x xs :: FL p wX wZ
xs = p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
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 ([(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ))
-> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
forall a b. (a -> b) -> a -> b
$ FL p wX wZ -> [(:>) p (FL p) wX wZ]
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 :: p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
r _ [] = Maybe (FL p wY wZ)
forall a. Maybe a
Nothing
r z :: p wX wY
z ((z' :: p wX wZ
z':>zs :: FL p wZ wZ
zs):zss :: [(:>) p (FL p) wX wZ]
zss) | EqCheck wY wZ
IsEq <- p wX wY
z p wX wY -> p wX wZ -> EqCheck wY wZ
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wX wZ
z' = FL p wZ wZ -> Maybe (FL p wZ wZ)
forall a. a -> Maybe a
Just FL p wZ wZ
zs
| Bool
otherwise = p wX wY -> [(:>) p (FL p) wX wZ] -> Maybe (FL p wY wZ)
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 :: p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)
removeRL x :: p wY wZ
x xs :: RL p wX wZ
xs = p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
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 ([RL p wX wZ] -> Maybe (RL p wX wY))
-> [RL p wX wZ] -> Maybe (RL p wX wY)
forall a b. (a -> b) -> a -> b
$ RL p wX wZ -> [RL p wX wZ]
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 :: p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
r z :: p wY wZ
z ((zs :: RL p wX wY
zs:<:z' :: p wY wZ
z'):zss :: [RL p wX wZ]
zss) | EqCheck wY wY
IsEq <- p wY wZ
z p wY wZ -> p wY wZ -> EqCheck wY wY
forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= p wY wZ
z' = RL p wX wY -> Maybe (RL p wX wY)
forall a. a -> Maybe a
Just RL p wX wY
zs
| Bool
otherwise = p wY wZ -> [RL p wX wZ] -> Maybe (RL p wX wY)
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 _ _ = Maybe (RL p wX wY)
forall a. Maybe a
Nothing
removeSubsequenceFL :: (Eq2 p, Commute p) => FL p wA wB
-> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL :: FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
removeSubsequenceFL a :: FL p wA wB
a b :: FL p wA wC
b | FL p wA wB -> Int
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wB
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> FL p wA wC -> Int
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wC
b = Maybe (FL p wB wC)
forall a. Maybe a
Nothing
| Bool
otherwise = FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
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 :: FL p wA wB -> FL p wA wC -> Maybe (FL p wB wC)
rsFL NilFL ys :: FL p wA wC
ys = FL p wA wC -> Maybe (FL p wA wC)
forall a. a -> Maybe a
Just FL p wA wC
ys
rsFL (x :: p wA wY
x:>:xs :: FL p wY wB
xs) yys :: FL p wA wC
yys = p wA wY -> FL p wA wC -> Maybe (FL p wY wC)
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 Maybe (FL p wY wC)
-> (FL p wY wC -> Maybe (FL p wB wC)) -> Maybe (FL p wB wC)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FL p wY wB -> FL p wY wC -> Maybe (FL p wB wC)
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 :: RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
removeSubsequenceRL a :: RL p wAb wAbc
a b :: RL p wA wAbc
b | RL p wAb wAbc -> Int
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wAb wAbc
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> RL p wA wAbc -> Int
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wA wAbc
b = Maybe (RL p wA wAb)
forall a. Maybe a
Nothing
| Bool
otherwise = RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
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 :: RL p wAb wAbc -> RL p wA wAbc -> Maybe (RL p wA wAb)
rsRL NilRL ys :: RL p wA wAbc
ys = RL p wA wAbc -> Maybe (RL p wA wAbc)
forall a. a -> Maybe a
Just RL p wA wAbc
ys
rsRL (xs :: RL p wAb wY
xs:<:x :: p wY wAbc
x) yys :: RL p wA wAbc
yys = p wY wAbc -> RL p wA wAbc -> Maybe (RL p wA wY)
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 Maybe (RL p wA wY)
-> (RL p wA wY -> Maybe (RL p wA wAb)) -> Maybe (RL p wA wAb)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RL p wAb wY -> RL p wA wY -> Maybe (RL p wA wAb)
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 :: FL p wX wY -> [FL p wX wY]
simpleHeadPermutationsFL ps :: FL p wX wY
ps = ((:>) p (FL p) wX wY -> FL p wX wY)
-> [(:>) p (FL p) wX wY] -> [FL p wX wY]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: p wX wZ
x:>xs :: FL p wZ wY
xs) -> p wX wZ
xp wX wZ -> FL p wZ wY -> FL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>:FL p wZ wY
xs) ([(:>) p (FL p) wX wY] -> [FL p wX wY])
-> [(:>) p (FL p) wX wY] -> [FL p wX wY]
forall a b. (a -> b) -> a -> b
$ FL p wX wY -> [(:>) p (FL p) wX wY]
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 :: FL p wX wY -> [(:>) p (FL p) wX wY]
headPermutationsFL NilFL = []
headPermutationsFL (p :: p wX wY
p:>:ps :: FL p wY wY
ps) =
(p wX wY
pp wX wY -> FL p wY wY -> (:>) p (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>FL p wY wY
ps) (:>) p (FL p) wX wY
-> [(:>) p (FL p) wX wY] -> [(:>) p (FL p) wX wY]
forall a. a -> [a] -> [a]
: ((:>) p (FL p) wY wY -> Maybe ((:>) p (FL p) wX wY))
-> [(:>) p (FL p) wY wY] -> [(:>) p (FL p) wX wY]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((:>) p (p :> FL p) wX wY -> Maybe ((:>) p (FL p) wX wY)
forall (a1 :: * -> * -> *) wX wY.
Commute a1 =>
(:>) a1 (a1 :> FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY)
swapfirstFL((:>) p (p :> FL p) wX wY -> Maybe ((:>) p (FL p) wX wY))
-> ((:>) p (FL p) wY wY -> (:>) p (p :> FL p) wX wY)
-> (:>) p (FL p) wY wY
-> Maybe ((:>) p (FL p) wX wY)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(p wX wY
pp wX wY -> (:>) p (FL p) wY wY -> (:>) p (p :> FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>)) (FL p wY wY -> [(:>) p (FL p) wY 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 (p1 :: a1 wX wZ
p1:>p2:>xs) = do p2' :: a1 wX wZ
p2':>p1' :: a1 wZ wZ
p1' <- (:>) a1 a1 wX wZ -> Maybe ((:>) a1 a1 wX wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (a1 wX wZ
p1a1 wX wZ -> a1 wZ wZ -> (:>) a1 a1 wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a1 wZ wZ
p2)
(:>) a1 (FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY)
forall a. a -> Maybe a
Just ((:>) a1 (FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY))
-> (:>) a1 (FL a1) wX wY -> Maybe ((:>) a1 (FL a1) wX wY)
forall a b. (a -> b) -> a -> b
$ a1 wX wZ
p2'a1 wX wZ -> FL a1 wZ wY -> (:>) a1 (FL a1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a1 wZ wZ
p1'a1 wZ wZ -> FL a1 wZ wY -> FL a1 wZ wY
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 :: RL p wX wY -> [RL p wX wY]
headPermutationsRL NilRL = []
headPermutationsRL (ps :: RL p wX wY
ps:<:p :: p wY wY
p) =
(RL p wX wY
psRL p wX wY -> p wY wY -> RL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:p wY wY
p) RL p wX wY -> [RL p wX wY] -> [RL p wX wY]
forall a. a -> [a] -> [a]
: (RL p wX wY -> Maybe (RL p wX wY)) -> [RL p wX wY] -> [RL p wX wY]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (RL p wX wY -> Maybe (RL p wX wY)
forall (a :: * -> * -> *) wX wZ.
Commute a =>
RL a wX wZ -> Maybe (RL a wX wZ)
swapfirstRL(RL p wX wY -> Maybe (RL p wX wY))
-> (RL p wX wY -> RL p wX wY) -> RL p wX wY -> Maybe (RL p wX wY)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RL p wX wY -> p wY wY -> RL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:p wY wY
p)) (RL p wX wY -> [RL p wX wY]
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 (xs :: RL a wX wY
xs:<:p2 :: a wY wY
p2:<:p1 :: a wY wZ
p1) = do p1' :: a wY wZ
p1':>p2' :: a wZ wZ
p2' <- (:>) a a wY wZ -> Maybe ((:>) a a wY wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (a wY wY
p2a wY wY -> a wY wZ -> (:>) a a wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>a wY wZ
p1)
RL a wX wZ -> Maybe (RL a wX wZ)
forall a. a -> Maybe a
Just (RL a wX wZ -> Maybe (RL a wX wZ))
-> RL a wX wZ -> Maybe (RL a wX wZ)
forall a b. (a -> b) -> a -> b
$ RL a wX wY
xsRL a wX wY -> a wY wZ -> RL a wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:a wY wZ
p1'RL a wX wZ -> a wZ wZ -> RL a wX wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<:a wZ wZ
p2'
swapfirstRL _ = Maybe (RL a wX wZ)
forall a. Maybe a
Nothing
instance (Eq2 p, Commute p) => Eq2 (FL p) where
a :: FL p wA wB
a =\/= :: FL p wA wB -> FL p wA wC -> EqCheck wB wC
=\/= b :: FL p wA wC
b | FL p wA wB -> Int
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wB
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= FL p wA wC -> Int
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL p wA wC
b = EqCheck wB wC
forall wA wB. EqCheck wA wB
NotEq
| Bool
otherwise = FL p wA wB -> FL p wA wC -> EqCheck wB wC
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 :: FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
cmpSameLength (x :: p wX wY
x:>:xs :: FL p wY wY
xs) xys :: FL p wX wZ
xys | Just ys :: FL p wY wZ
ys <- p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
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 = FL p wY wY -> FL p wY wZ -> EqCheck wY wZ
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 NilFL NilFL = EqCheck wY wZ
forall wA. EqCheck wA wA
IsEq
cmpSameLength _ _ = EqCheck wY wZ
forall wA wB. EqCheck wA wB
NotEq
xs :: FL p wA wC
xs =/\= :: FL p wA wC -> FL p wB wC -> EqCheck wA wB
=/\= ys :: FL p wB wC
ys = FL p wA wC -> RL p wA wC
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wA wC
xs RL p wA wC -> RL p wB wC -> EqCheck wA wB
forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= FL p wB wC -> RL p wB wC
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 :: RL p wA wB -> RL p wC wD -> Bool
unsafeCompare = String -> RL p wA wB -> RL p wC wD -> Bool
forall a. String -> a
bug "Buggy use of unsafeCompare on RL"
a :: RL p wA wC
a =/\= :: RL p wA wC -> RL p wB wC -> EqCheck wA wB
=/\= b :: RL p wB wC
b | RL p wA wC -> Int
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wA wC
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= RL p wB wC -> Int
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL p wB wC
b = EqCheck wA wB
forall wA wB. EqCheck wA wB
NotEq
| Bool
otherwise = RL p wA wC -> RL p wB wC -> EqCheck wA wB
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 :: RL p wX wY -> RL p wW wY -> EqCheck wX wW
cmpSameLength (xs :: RL p wX wY
xs:<:x :: p wY wY
x) xys :: RL p wW wY
xys | Just ys :: RL p wW wY
ys <- p wY wY -> RL p wW wY -> Maybe (RL p wW wY)
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 = RL p wX wY -> RL p wW wY -> EqCheck wX wW
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 NilRL NilRL = EqCheck wX wW
forall wA. EqCheck wA wA
IsEq
cmpSameLength _ _ = EqCheck wX wW
forall wA wB. EqCheck wA wB
NotEq
xs :: RL p wA wB
xs =\/= :: RL p wA wB -> RL p wA wC -> EqCheck wB wC
=\/= ys :: RL p wA wC
ys = RL p wA wB -> FL p wA wB
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wA wB
xs FL p wA wB -> FL p wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= RL p wA wC -> FL p wA wC
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wA wC
ys
partitionConflictingFL :: (Commute p1, Invert p1) => CommuteFn p1 p2 -> FL p1 wX wY -> p2 wX wZ -> (FL p1 :> FL p1) wX wY
partitionConflictingFL :: CommuteFn p1 p2
-> FL p1 wX wY -> p2 wX wZ -> (:>) (FL p1) (FL p1) wX wY
partitionConflictingFL _ NilFL _ = FL p1 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p1 wX wX -> FL p1 wX wX -> (:>) (FL p1) (FL p1) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
partitionConflictingFL commuter :: CommuteFn p1 p2
commuter (x :: p1 wX wY
x :>: xs :: FL p1 wY wY
xs) y :: p2 wX wZ
y =
case (:>) p1 p2 wY wZ -> Maybe ((:>) p2 p1 wY wZ)
CommuteFn p1 p2
commuter (p1 wX wY -> p1 wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p1 wX wY
x p1 wY wX -> p2 wX wZ -> (:>) p1 p2 wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p2 wX wZ
y) of
Nothing -> case (:>) p1 (FL p1) wX wY -> (:>) (FL p1) (p1 :> FL p1) wX wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p1 wX wY
x p1 wX wY -> FL p1 wY wY -> (:>) p1 (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wY wY
xs) of
xs_ok :: FL p1 wX wZ
xs_ok :> x' :: p1 wZ wZ
x' :> xs_deps :: FL p1 wZ wY
xs_deps ->
case CommuteFn p1 p2
-> FL p1 wX wZ -> p2 wX wZ -> (:>) (FL p1) (FL p1) wX wZ
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *) wX wY wZ.
(Commute p1, Invert p1) =>
CommuteFn p1 p2
-> FL p1 wX wY -> p2 wX wZ -> (:>) (FL p1) (FL p1) wX wY
partitionConflictingFL CommuteFn p1 p2
commuter FL p1 wX wZ
xs_ok p2 wX wZ
y of
xs_clean :: FL p1 wX wZ
xs_clean :> xs_conflicts :: FL p1 wZ wZ
xs_conflicts -> FL p1 wX wZ
xs_clean FL p1 wX wZ -> FL p1 wZ wY -> (:>) (FL p1) (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL p1 wZ wZ
xs_conflicts FL p1 wZ wZ -> FL p1 wZ wY -> FL p1 wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (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_deps))
Just (y' :: p2 wY wZ
y' :> _) ->
case CommuteFn p1 p2
-> FL p1 wY wY -> p2 wY wZ -> (:>) (FL p1) (FL p1) wY wY
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *) wX wY wZ.
(Commute p1, Invert p1) =>
CommuteFn p1 p2
-> FL p1 wX wY -> p2 wX wZ -> (:>) (FL p1) (FL p1) wX wY
partitionConflictingFL CommuteFn p1 p2
commuter FL p1 wY wY
xs p2 wY wZ
y' of
xs_clean :: FL p1 wY wZ
xs_clean :> xs_conflicts :: FL p1 wZ wY
xs_conflicts -> (p1 wX wY
x p1 wX wY -> FL p1 wY wZ -> FL p1 wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p1 wY wZ
xs_clean) FL p1 wX wZ -> FL p1 wZ wY -> (:>) (FL p1) (FL p1) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p1 wZ wY
xs_conflicts
inverseCommuter :: (Invert p, Invert q) => CommuteFn p q -> CommuteFn q p
inverseCommuter :: CommuteFn p q -> CommuteFn q p
inverseCommuter commuter :: CommuteFn p q
commuter (p :: q wX wZ
p :> q :: p wZ wY
q) =
do invp' :: q wY wZ
invp' :> invq' :: p wZ wX
invq' <- (:>) 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
q 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
p)
(:>) 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
invq' 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
invp')