-- Copyright (C) 2002-2003 David Roundy
-- Copyright (C) 2009 Ganesh Sittampalam
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2, or (at your option)
-- any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with this program; see the file COPYING.  If not, write to
-- the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
-- Boston, MA 02110-1301, USA.

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Darcs.Patch.Permutations
    ( removeFL
    , removeRL
    , removeCommon
    , commuteWhatWeCanFL
    , commuteWhatWeCanRL
    , genCommuteWhatWeCanRL
    , genCommuteWhatWeCanFL
    , partitionFL
    , partitionRL
    , partitionFL'
    , partitionRL'
    , simpleHeadPermutationsFL
    , headPermutationsRL
    , headPermutationsFL
    , permutationsRL
    , removeSubsequenceFL
    , removeSubsequenceRL
    , partitionConflictingFL
    , (=\~/=)
    , (=/~\=)
    , nubFL
    ) where

import Darcs.Prelude

import Data.List ( nubBy )
import Data.Maybe ( mapMaybe )
import Darcs.Patch.Commute ( Commute, commute, commuteFL, commuteRL )
import Darcs.Patch.CommuteFn ( CommuteFn )
import Darcs.Patch.Merge ( CleanMerge(..), cleanMergeFL )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..), isIsEq )
import Darcs.Patch.Witnesses.Ordered
    ( FL(..), RL(..), (:>)(..), (:\/:)(..), (:/\:)(..)
    , (+<+), (+>+)
    , lengthFL, lengthRL
    , reverseFL, reverseRL
    )
import Darcs.Patch.Witnesses.Sealed ( Sealed(..) )

-- | Split an 'FL' according to a predicate, using commutation as necessary,
-- into those that satisfy the predicate and can be commuted to the left, and
-- those that do not satisfy it and can be commuted to the right. Whatever
-- remains stays in the middle.
--
-- Note that the predicate @p@ should be invariant under commutation:
-- if @commute(x:>y)==Just(y':>x')@ then @p x == p x' && p y == p y'@.
partitionFL :: Commute p
            => (forall wU wV . p wU wV -> Bool)  -- ^predicate; if true we would like the patch in the "left" list
            -> FL p wX wY                        -- ^input 'FL'
            -> (FL p :> FL p :> FL p) wX wY      -- ^"left", "middle" and "right"
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 wU wV. p wU wV -> Bool)
-> RL p wX wX
-> RL p wX wX
-> FL p wX wY
-> (:>) (FL p) (RL p :> RL 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) (RL p :> RL p) wA wD
partitionFL' p wU wV -> Bool
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 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 FL p wX wZ
-> (:>) (FL p) (FL p) wZ wY -> (:>) (FL p) (FL p :> FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ -> FL p wZ wZ
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wZ
middle FL p wZ wZ -> FL p wZ wY -> (:>) (FL p) (FL p) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY -> FL p wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wZ wY
right

-- optimise by using an accumulating parameter to track all the "left"
-- patches that we've found so far; also do not reverse the result lists
partitionFL' :: Commute p
             => (forall wU wV . p wU wV -> Bool)
             -> RL p wA wB  -- the "middle" patches found so far
             -> RL p wB wC  -- the "right" patches found so far
             -> 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 = FL p wA wA
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wA wA
-> (:>) (RL p) (RL p) wA wD -> (:>) (FL p) (RL p :> RL p) wA wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wA wB
middle RL p wA wB -> RL p wB wD -> (:>) (RL p) (RL p) wA wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wB wC
RL p wB wD
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)
    | p wC wY -> Bool
forall wU wV. p wU wV -> Bool
keepleft p wC wY
p = 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
        (RL p wB wZ
NilRL :> p wZ wZ
p' :> 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 wZ wZ
p') of
            Just (p wA wZ
p'' :> 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) (RL p :> RL 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) (RL p :> RL p) wA wD
partitionFL' p wU wV -> Bool
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'' 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
-> (:>) (RL p) (RL p) wZ wD -> (:>) (FL p) (RL p :> RL p) wA wD
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 -> RL p wZ wD -> (:>) (RL p) (RL p) wZ wD
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 wU wV. p wU wV -> Bool)
-> RL p wA wZ
-> RL p wZ wY
-> FL p wY wD
-> (:>) (FL p) (RL p :> RL 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) (RL p :> RL p) wA wD
partitionFL' p wU wV -> Bool
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 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 wU wV. p wU wV -> Bool)
-> RL p wA wZ
-> RL p wZ wY
-> FL p wY wD
-> (:>) (FL p) (RL p :> RL 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) (RL p :> RL p) wA wD
partitionFL' p wU wV -> Bool
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) (RL p :> RL 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) (RL p :> RL p) wA wD
partitionFL' p wU wV -> Bool
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

-- | Split an 'RL' according to a predicate, using commutation as necessary,
-- into those that satisfy the predicate and can be commuted to the right, and
-- those that do not satisfy it and can be commuted to the left. Whatever
-- remains stays in the middle.
--
-- Note that the predicate @p@ should be invariant under commutation:
-- if @commute(x:>y)==Just(y':>x')@ then @p x == p x' && p y == p y'@.
partitionRL' :: forall p wX wY. Commute p
             => (forall wU wV . p wU wV -> Bool)
             -> RL p wX wY
             -> (FL p :> FL p :> RL p) wX wY
partitionRL' :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(forall wU wV. p wU wV -> Bool)
-> RL p wX wY -> (:>) (FL p) (FL p :> RL p) wX wY
partitionRL' forall wU wV. p wU wV -> Bool
predicate RL p wX wY
input = RL p wX wY
-> FL p wY wY -> FL p wY wY -> (:>) (FL p) (FL p :> RL p) wX wY
forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wX wY
input FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL where
  go :: RL p wA wB  -- input RL
     -> FL p wB wC  -- the "left" patches found so far
     -> FL p wC wD  -- the "middle" patches found so far
     -> (FL p :> FL p :> RL p) wA wD
  go :: forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wA wB
NilRL FL p wB wC
left FL p wC wD
middle = FL p wA wC
FL p wB wC
left FL p wA wC
-> (:>) (FL p) (RL p) wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wC wD
middle FL p wC wD -> RL p wD wD -> (:>) (FL p) (RL p) wC wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wD wD
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
  go (RL p wA wY
ps :<: p wY wB
p) FL p wB wC
left FL p wC wD
middle
    | p wY wB -> Bool
forall wU wV. p wU wV -> Bool
predicate p wY wB
p = case (:>) p (FL p) wY wC -> (:>) (FL p) (p :> FL p) wY wC
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (p wY wB
p p wY wB -> FL p wB wC -> (:>) p (FL p) wY wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wB wC
left) of
        (FL p wY wZ
left' :> p wZ wZ
p' :> FL p wZ wC
NilFL) -> case (:>) p (FL p) wZ wD -> Maybe ((:>) (FL p) p wZ wD)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wZ wZ
p' p wZ wZ -> FL p wZ wD -> (:>) p (FL p) wZ wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wC wD
FL p wZ wD
middle) of
            Just (FL p wZ wZ
middle' :> p wZ wD
p'') -> case RL p wA wY
-> FL p wY wZ -> FL p wZ wZ -> (:>) (FL p) (FL p :> RL p) wA wZ
forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wA wY
ps FL p wY wZ
left' FL p wZ wZ
middle' of
                (FL p wA wZ
a :> FL p wZ wZ
b :> RL p wZ wZ
c) -> FL p wA wZ
a FL p wA wZ
-> (:>) (FL p) (RL p) wZ wD -> (:>) (FL p) (FL p :> RL 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 -> RL p wZ wD -> (:>) (FL p) (RL p) wZ wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
c RL p wZ wZ -> p wZ wD -> RL p wZ wD
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wD
p''
            Maybe ((:>) (FL p) p wZ wD)
Nothing -> RL p wA wY
-> FL p wY wZ -> FL p wZ wD -> (:>) (FL p) (FL p :> RL p) wA wD
forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wA wY
ps FL p wY wZ
left' (p wZ wZ
p' p wZ wZ -> FL p wZ wD -> FL p wZ wD
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wC wD
FL p wZ wD
middle)
        (FL p wY wZ
left' :> p wZ wZ
p' :> FL p wZ wC
tomiddle) ->
            RL p wA wY
-> FL p wY wZ -> FL p wZ wD -> (:>) (FL p) (FL p :> RL p) wA wD
forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wA wY
ps FL p wY wZ
left' (p wZ wZ
p' p wZ wZ -> FL p wZ wD -> FL p wZ wD
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wC
tomiddle FL p wZ wC -> FL p wC wD -> FL p wZ wD
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL p wC wD
middle)
    | Bool
otherwise = RL p wA wY
-> FL p wY wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
forall wA wB wC wD.
RL p wA wB
-> FL p wB wC -> FL p wC wD -> (:>) (FL p) (FL p :> RL p) wA wD
go RL p wA wY
ps (p wY wB
p p wY wB -> FL p wB wC -> FL p wY wC
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wB wC
left) FL p wC wD
middle

-- | Split an 'RL' according to a predicate, using commutation as necessary,
-- into those that satisfy the predicate and can be commuted to the right, and
-- those that don't, i.e. either do not satisfy the predicate or cannot be
-- commuted to the right.
--
-- Note that the predicate @p@ should be invariant under commutation:
-- if @commute(x:>y)==Just(y':>x')@ then @p x == p x' && p y == p y'@.
partitionRL :: forall p wX wY. Commute p
            => (forall wU wV . p wU wV -> Bool) -- ^predicate; if true we would like the patch in the "right" list
            -> RL p wX wY                       -- ^input 'RL'
            -> (RL p :> RL p) wX wY             -- ^"left" and "right" results
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 = (:>) (RL p) (FL p) wX wY -> (:>) (RL p) (RL p) wX wY
forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go ((:>) (RL p) (FL p) wX wY -> (:>) (RL p) (RL p) wX wY)
-> (RL p wX wY -> (:>) (RL p) (FL p) wX wY)
-> RL p wX wY
-> (:>) (RL p) (RL p) wX wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RL p wX wY -> FL p wY wY -> (:>) (RL 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
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) = (FL p wA wB -> RL p wA wB
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wA wB
FL p wZ wB
qs RL p wA wB -> RL p wB wB -> (:>) (RL p) (RL p) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wB wB
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL)
    go (RL p wA wY
ps :<: p wY wZ
p :> FL p wZ wB
qs)
      | p wY wZ -> Bool
forall wU wV. p wU wV -> Bool
keepright p wY wZ
p
      , Just (FL p wY wZ
qs' :> p wZ wB
p') <- (:>) p (FL p) wY wB -> Maybe ((:>) (FL p) p wY wB)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wZ
p p wY wZ -> FL p wZ wB -> (:>) p (FL p) wY wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
qs) =
          case (:>) (RL p) (FL p) wA wZ -> (:>) (RL p) (RL p) wA wZ
forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go (RL p wA wY
ps RL p wA wY -> FL p wY wZ -> (:>) (RL p) (FL p) wA wZ
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 RL p wA wZ -> RL p wZ wB -> (:>) (RL p) (RL p) wA wB
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 wB -> RL p wZ wB
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wB
p'
      | Bool
otherwise = (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
forall wA wB. (:>) (RL p) (FL p) wA wB -> (:>) (RL p) (RL p) wA wB
go (RL p wA wY
ps RL p wA wY -> FL p wY wB -> (:>) (RL p) (FL p) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p p wY wZ -> FL p wZ wB -> FL p wY wB
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 = CommuteFn p p
-> (:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
Commute q =>
CommuteFn p q
-> (:>) p (FL q) wX wY -> (:>) (FL q) (p :> FL q) wX wY
genCommuteWhatWeCanFL (:>) p p wX wY -> Maybe ((:>) p p wX wY)
CommuteFn p p
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute

genCommuteWhatWeCanFL :: Commute q
                      => CommuteFn p q
                      -> (p :> FL q) wX wY
                      -> (FL q :> p :> FL q) wX wY
genCommuteWhatWeCanFL :: forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
Commute q =>
CommuteFn p q
-> (:>) p (FL q) wX wY -> (:>) (FL q) (p :> FL q) wX wY
genCommuteWhatWeCanFL CommuteFn p q
com (p wX wZ
p :> q wZ wY
x :>: FL q wY wY
xs) =
  case (:>) p q wX wY -> Maybe ((:>) q p wX wY)
CommuteFn p q
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
    Maybe ((:>) q p wX wY)
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
        FL q wZ wZ
xs1 :> q wZ wZ
x' :> FL q wZ wY
xs2 ->
          case CommuteFn p q
-> (:>) p (FL q) wX wZ -> (:>) (FL q) (p :> FL q) wX wZ
forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
Commute q =>
CommuteFn p q
-> (:>) p (FL q) wX wY -> (:>) (FL q) (p :> FL q) wX wY
genCommuteWhatWeCanFL (:>) p q wX wY -> Maybe ((:>) q p wX wY)
CommuteFn p q
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
            FL q wX wZ
xs1' :> p wZ wZ
p' :> 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 (q wX wZ
x' :> p wZ wY
p') ->
      case CommuteFn p q
-> (:>) p (FL q) wZ wY -> (:>) (FL q) (p :> FL q) wZ wY
forall (q :: * -> * -> *) (p :: * -> * -> *) wX wY.
Commute q =>
CommuteFn p q
-> (:>) p (FL q) wX wY -> (:>) (FL q) (p :> FL q) wX wY
genCommuteWhatWeCanFL (:>) p q wX wY -> Maybe ((:>) q p wX wY)
CommuteFn p q
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
        FL q wZ wZ
a :> p wZ wZ
p'' :> 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 CommuteFn p q
_ (p wX wZ
y :> FL q wZ wY
NilFL) = FL q wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL q wX wX -> (:>) p (FL q) wX 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 wX wZ
y p wX wZ -> FL q wZ wY -> (:>) p (FL q) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL q wZ 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL = CommuteFn p p
-> (:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
Commute p =>
CommuteFn p q
-> (:>) (RL p) q wX wY -> (:>) (RL p) (q :> RL p) wX wY
genCommuteWhatWeCanRL (:>) p p wX wY -> Maybe ((:>) p p wX wY)
CommuteFn p p
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute

genCommuteWhatWeCanRL :: Commute p
                      => CommuteFn p q
                      -> (RL p :> q) wX wY
                      -> (RL p :> q :> RL p) wX wY
genCommuteWhatWeCanRL :: forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
Commute p =>
CommuteFn p q
-> (:>) (RL p) q wX wY -> (:>) (RL p) (q :> RL p) wX wY
genCommuteWhatWeCanRL CommuteFn p q
com (RL p wX wY
xs :<: p wY wZ
x :> q wZ wY
p) =
  case (:>) p q wY wY -> Maybe ((:>) q p wY wY)
CommuteFn p q
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
    Maybe ((:>) q p wY wY)
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
        RL p wX wZ
xs1 :> p wZ wZ
x' :> RL p wZ wZ
xs2 ->
          case CommuteFn p q
-> (:>) (RL p) q wZ wY -> (:>) (RL p) (q :> RL p) wZ wY
forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
Commute p =>
CommuteFn p q
-> (:>) (RL p) q wX wY -> (:>) (RL p) (q :> RL p) wX wY
genCommuteWhatWeCanRL (:>) p q wX wY -> Maybe ((:>) q p wX wY)
CommuteFn p q
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
            RL p wZ wZ
xs1' :> q wZ wZ
p' :> 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 (q wY wZ
p' :> p wZ wY
x') ->
      case CommuteFn p q
-> (:>) (RL p) q wX wZ -> (:>) (RL p) (q :> RL p) wX wZ
forall (p :: * -> * -> *) (q :: * -> * -> *) wX wY.
Commute p =>
CommuteFn p q
-> (:>) (RL p) q wX wY -> (:>) (RL p) (q :> RL p) wX wY
genCommuteWhatWeCanRL (:>) p q wX wY -> Maybe ((:>) q p wX wY)
CommuteFn p q
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
        RL p wX wZ
xs1 :> q wZ wZ
p'' :> 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 CommuteFn p q
_ (RL p wX wZ
NilRL :> q wZ wY
y) = RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wX wX -> (:>) q (RL p) wX 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 wX wY
q wZ wY
y q wX wY -> RL p wY wY -> (:>) q (RL p) wX 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 :: 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 FL p wZ wX -> FL p wZ wY -> (:\/:) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wZ wY
FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
removeCommon (FL p wZ wX
NilFL :\/: FL p wZ wY
xs) = FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wX wX -> FL p wX wY -> (:\/:) (FL p) (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wX wY
FL p wZ wY
xs
removeCommon (FL p wZ wX
xs :\/: 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 :: 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 <- 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 FL p wX wY
ms [p wX wZ
n:>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 FL p wX wY
ms ((:>) p (FL p) wX wZ
_:[(:>) 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 wX wY
_ [] = [Char] -> (:\/:) (FL p) (FL p) wY wZ
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible case" -- because we already checked for NilFL case

-- | 'removeFL' @x xs@ removes @x@ from @xs@ if @x@ can be commuted to its head.
--   Otherwise it returns 'Nothing'
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 = 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 :: 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
_ [] = Maybe (FL p wY wZ)
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 p wX wY -> p wX wZ -> EqCheck wY wZ
forall wA wB wC. p wA wB -> p wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wX wZ
z' = FL p wY wZ -> Maybe (FL p wY wZ)
forall a. a -> Maybe a
Just FL p wY wZ
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' is like 'removeFL' except with 'RL'
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 = 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 :: 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 p wY wZ -> p wY wZ -> EqCheck wY wY
forall wA wC wB. p wA wC -> p wB wC -> EqCheck wA wB
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
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 p wY wZ
_ [RL p wX wZ]
_ = Maybe (RL p wX wY)
forall a. Maybe a
Nothing

-- | 'removeSubsequenceFL' @ab abc@ returns @Just c'@ where all the patches in
--   @ab@ have been commuted out of it, if possible.  If this is not possible
--   for any reason (the set of patches @ab@ is not actually a subset of @abc@,
--   or they can't be commuted out) we return '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 | 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 :: 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 = FL p wB wC -> Maybe (FL p wB wC)
forall a. a -> Maybe a
Just FL p wA wC
FL p wB wC
ys
          rsFL (p wA wY
x:>:FL p wY wB
xs) 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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
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' is like @removeSubsequenceFL@ except that it works
--   on 'RL'
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 | 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 :: 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 = RL p wA wAb -> Maybe (RL p wA wAb)
forall a. a -> Maybe a
Just RL p wA wAb
RL p wA wAbc
ys
          rsRL (RL p wAb wY
xs:<:p wY wAbc
x) 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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
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

-- | This is a minor variant of 'headPermutationsFL' with each permutation
--   is simply returned as a 'FL'
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 = ((:>) 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 (\ (p wX wZ
x:>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' @p:>:ps@ returns all the permutations of the list
--   in which one element of @ps@ is commuted past @p@
--
--   Suppose we have a sequence of patches
--
--   >  X h a y s-t-c k
--
--   Suppose furthermore that the patch @c@ depends on @t@, which in turn
--   depends on @s@.  This function will return
--
--   > X :> h a y s t c k
--   > h :> X a y s t c k
--   > a :> X h y s t c k
--   > y :> X h a s t c k
--   > s :> X h a y t c k
--   > k :> X h a y s t c
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
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 (a1 wX wZ
p1:>a1 wZ wZ
p2:>FL a1 wZ wY
xs) = do a1 wX wZ
p2':>a1 wZ wZ
p1' <- (:>) a1 a1 wX wZ -> Maybe ((:>) a1 a1 wX wZ)
forall wX wY. (:>) a1 a1 wX wY -> Maybe ((:>) a1 a1 wX wY)
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' is like 'headPermutationsFL', except that we
--   operate on an 'RL' (in other words, we are pushing things to the end of a
--   patch sequence instead of to the beginning).
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
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 (RL a wX wY
xs:<:a wY wY
p2:<:a wY wZ
p1) = do a wY wZ
p1':>a wZ wZ
p2' <- (:>) a a wY wZ -> Maybe ((:>) a a wY wZ)
forall wX wY. (:>) a a wX wY -> Maybe ((:>) a a wX wY)
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 RL a wX wZ
_ = Maybe (RL a wX wZ)
forall a. Maybe a
Nothing

-- | All permutations of an 'RL'.
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
ps RL p wX wY -> [RL p wX wY] -> [RL p wX wY]
forall a. a -> [a] -> [a]
: [RL p wX wY
qs' 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
q | RL p wX wY
qs :<: p wY wY
q <- 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, RL p wX wY
qs' <- RL p wX wY -> [RL p wX wY]
forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> [RL p wX wY]
permutationsRL RL p wX wY
qs]

-- | This commutes patches in the RHS to bring them into the same
-- order as the LHS.
(=\~/=)
  :: forall p wA wB wC
   . (Commute p, Eq2 p)
  => FL p wA wB
  -> FL p wA wC
  -> EqCheck wB wC
FL p wA wB
a =\~/= :: forall (p :: * -> * -> *) wA wB wC.
(Commute p, Eq2 p) =>
FL p wA wB -> FL p wA wC -> EqCheck wB wC
=\~/= 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 wX wY wZ. FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
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 wX wY wZ. FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
cmpSameLength (p wX wY
x :>: FL p wY wY
xs) FL p wX wZ
x_ys
      | Just 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
x_ys = FL p wY wY -> FL p wY wZ -> EqCheck wY wZ
forall wX wY wZ. FL p wX wY -> FL p wX wZ -> EqCheck wY wZ
cmpSameLength FL p wY wY
xs FL p wY wZ
ys
    cmpSameLength FL p wX wY
NilFL FL p wX wZ
NilFL = EqCheck wY wY
EqCheck wY wZ
forall wA. EqCheck wA wA
IsEq
    cmpSameLength FL p wX wY
_ FL p wX wZ
_ = EqCheck wY wZ
forall wA wB. EqCheck wA wB
NotEq

-- | This commutes patches in the RHS to bring them into the same
-- order as the LHS.
(=/~\=)
  :: forall p wA wB wC
   . (Commute p, Eq2 p)
  => RL p wA wC
  -> RL p wB wC
  -> EqCheck wA wB
RL p wA wC
a =/~\= :: forall (p :: * -> * -> *) wA wB wC.
(Commute p, Eq2 p) =>
RL p wA wC -> RL p wB wC -> EqCheck wA wB
=/~\= 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 wX wZ wY. RL p wX wZ -> RL p wY wZ -> EqCheck wX wY
cmpSameLength RL p wA wC
a RL p wB wC
b
  where
    cmpSameLength :: RL p wX wZ -> RL p wY wZ -> EqCheck wX wY
    cmpSameLength :: forall wX wZ wY. RL p wX wZ -> RL p wY wZ -> EqCheck wX wY
cmpSameLength (RL p wX wY
xs :<: p wY wZ
x) RL p wY wZ
ys_x
      | Just RL p wY wY
ys <- p wY wZ -> RL p wY wZ -> Maybe (RL p wY 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 wZ
x RL p wY wZ
ys_x = RL p wX wY -> RL p wY wY -> EqCheck wX wY
forall wX wZ wY. RL p wX wZ -> RL p wY wZ -> EqCheck wX wY
cmpSameLength RL p wX wY
xs RL p wY wY
ys
    cmpSameLength RL p wX wZ
NilRL RL p wY wZ
NilRL = EqCheck wX wX
EqCheck wX wY
forall wA. EqCheck wA wA
IsEq
    cmpSameLength RL p wX wZ
_ RL p wY wZ
_ = EqCheck wX wY
forall wA wB. EqCheck wA wB
NotEq

-- | A variant of 'nub' that is based on '=\~/= i.e. ignores (internal) ordering.
nubFL :: (Commute p, Eq2 p) => [Sealed (FL p wX)] -> [Sealed (FL p wX)]
nubFL :: forall (p :: * -> * -> *) wX.
(Commute p, Eq2 p) =>
[Sealed (FL p wX)] -> [Sealed (FL p wX)]
nubFL = (Sealed (FL p wX) -> Sealed (FL p wX) -> Bool)
-> [Sealed (FL p wX)] -> [Sealed (FL p wX)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Sealed (FL p wX) -> Sealed (FL p wX) -> Bool
forall {p :: * -> * -> *} {wA}.
(Commute p, Eq2 p) =>
Sealed (FL p wA) -> Sealed (FL p wA) -> Bool
eqSealedFL where
  eqSealedFL :: Sealed (FL p wA) -> Sealed (FL p wA) -> Bool
eqSealedFL (Sealed FL p wA wX
ps) (Sealed FL p wA wX
qs) = EqCheck wX wX -> Bool
forall wA wB. EqCheck wA wB -> Bool
isIsEq (FL p wA wX
ps FL p wA wX -> FL p wA wX -> EqCheck wX wX
forall (p :: * -> * -> *) wA wB wC.
(Commute p, Eq2 p) =>
FL p wA wB -> FL p wA wC -> EqCheck wB wC
=\~/= FL p wA wX
qs)

-- | Partition a list into the patches that merge cleanly with the given
-- patch and those that don't (including dependencies)
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 :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, CleanMerge p) =>
FL p wX wY -> FL p wX wZ -> (:>) (FL p) (FL p) wX wY
partitionConflictingFL = RL p wX wX
-> RL p wX wX
-> FL p wX wY
-> FL p wX wZ
-> (:>) (FL p) (FL p) wX wY
forall wA wB wC wD w.
RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> FL p wB w
-> (:>) (FL p) (FL p) wA wD
go RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
  where
    go :: RL p wA wB -> RL p wB wC -> FL p wC wD -> FL p wB w -> (FL p :> FL p) wA wD
    go :: forall wA wB wC wD w.
RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> FL p wB w
-> (:>) (FL p) (FL p) wA wD
go RL p wA wB
clean RL p wB wC
dirty FL p wC wD
NilFL FL p wB w
_ = 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
clean FL p wA wB -> FL p wB wD -> (:>) (FL p) (FL p) wA wD
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wB wD -> FL p wB wD
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wB wC
RL p wB wD
dirty
    go RL p wA wB
clean RL p wB wC
dirty (p wC wY
x:>:FL p wY wD
xs) FL p wB w
ys
      | Just (p wB wZ
x' :> RL p wZ wY
dirty') <- (:>) (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
dirty 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
x)
      , Just (FL p wZ wZ
ys' :/\: p w wZ
_) <- (:\/:) p (FL p) wZ w -> Maybe ((:/\:) (FL p) p wZ w)
PartialMergeFn p (FL p)
forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (p wB wZ
x' p wB wZ -> FL p wB w -> (:\/:) p (FL p) wZ w
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wB w
ys) =
        RL p wA wZ
-> RL p wZ wY
-> FL p wY wD
-> FL p wZ wZ
-> (:>) (FL p) (FL p) wA wD
forall wA wB wC wD w.
RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> FL p wB w
-> (:>) (FL p) (FL p) wA wD
go (RL p wA wB
clean 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
x') RL p wZ wY
dirty' FL p wY wD
xs FL p wZ wZ
ys'
      | Bool
otherwise = RL p wA wB
-> RL p wB wY
-> FL p wY wD
-> FL p wB w
-> (:>) (FL p) (FL p) wA wD
forall wA wB wC wD w.
RL p wA wB
-> RL p wB wC
-> FL p wC wD
-> FL p wB w
-> (:>) (FL p) (FL p) wA wD
go RL p wA wB
clean (RL p wB wC
dirty 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
x) FL p wY wD
xs FL p wB w
ys