-- Copyright (C) 2002-2004 David Roundy
--
-- 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.

-- | The purpose of this module is to deal with many of the common
-- cases that come up when choosing a subset of a group of patches.
--
-- The idea is to divide a sequence of candidate patches into an initial
-- section named 'InFirst', a final section named 'InLast', and between them a
-- third section of not yet decided patches named 'InMiddle'. The reason for the
-- neutral terminology 'InFirst', 'InMiddle', and 'InLast', is that which of 'InFirst'
-- and 'InLast' counts as @selected@ or @deselected@ depends on
-- what we want to achive, that is, on the command and its options.
-- See "Darcs.UI.SelectChanges" for examples of how to use the functions from
-- this module.
--
-- Obviously if there are dependencies between the patches that will put a
-- constraint on how you can choose to divide them up. Unless stated otherwise,
-- functions that move patches from one section to another pull all dependent
-- patches with them.
--
-- Internally, we don't necessarily reorder patches immediately, but merely
-- tag them with the desired status, and thus postpone the actual commutation.
-- This saves a lot of unnecessary work, especially when choices are made
-- interactively, where the user can revise earlier decisions.
module Darcs.Patch.Choices
    ( -- * Choosing patches
      PatchChoices
    , Slot(..)
      -- ** Constructing
    , patchChoices
    , mkPatchChoices
      -- ** Querying
    , patchSlot
    , getChoices
    , separateFirstMiddleFromLast
    , separateFirstFromMiddleLast
      -- ** Forcing patches into a given 'Slot'
    , forceMatchingFirst
    , forceFirsts
    , forceFirst
    , forceMatchingLast
    , forceLasts
    , forceLast
    , forceMiddle
    , makeEverythingSooner
    , makeEverythingLater
      -- ** Operations on 'InMiddle' patches
    , selectAllMiddles
    , refineChoices
      -- ** Substitution
    , substitute
      -- * Labelling patches
    , LabelledPatch
    , Label
    , label
    , unLabel
    , labelPatches
    , getLabelInt
    ) where

import Darcs.Prelude

import Darcs.Patch.Invert ( Invert, invert )
import Darcs.Patch.Commute ( Commute, commute, commuteRL )
import Darcs.Patch.Inspect ( PatchInspect, listTouchedFiles, hunkMatches )
import Darcs.Patch.Permutations ( commuteWhatWeCanRL, commuteWhatWeCanFL )
import Darcs.Patch.Witnesses.Eq ( EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
    ( FL(..), RL(..)
    , (:>)(..), (:||:)(..)
    , zipWithFL, mapFL_FL, concatFL
    , (+>+), reverseRL, anyFL )
import Darcs.Patch.Witnesses.Sealed ( Sealed2(..) )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP )

-- | 'Label' @mp i@ acts as a temporary identifier to help us keep track of patches
--   during the selection process.  These are useful for finding patches that
--   may have moved around during patch selection (being pushed forwards or
--   backwards as dependencies arise).
--
--   The identifier is implemented as a tuple @Label mp i@. The @i@ is an
--   integer, expected to be unique within the patches being
--   scrutinised.  The @mp@ is motivated by patch splitting; it
--   provides a convenient way to generate a new identifier from the patch
--   being split.  For example, if we split a patch identified as @Label Nothing
--   5@, the resulting sub-patches could be identified as
--   @Label (Just (Label Nothing 5))1@, @Label (Just (Label Nothing 5)) 2@, etc.
--
--   IOW, 'Label' is a non-empty, reversed list of 'Int's.
data Label = Label (Maybe Label) Int deriving Label -> Label -> Bool
(Label -> Label -> Bool) -> (Label -> Label -> Bool) -> Eq Label
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c== :: Label -> Label -> Bool
Eq

-- | A patch with a 'Label' attached to it.
data LabelledPatch p wX wY = LP Label (p wX wY)

-- | This internal type tags a 'LabelledPatch' with a 'Bool', to distinguish
-- 'InMiddle' from 'InLast' patches.
data PatchChoice p wX wY = PC
  { PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch :: (LabelledPatch p wX wY) -- ^ the 'LabelledPatch' in question
  , PatchChoice p wX wY -> Bool
_pcIsLast :: Bool                  -- ^ 'False' = 'InMiddle', 'True' = 'InLast'
  }

-- | Internal function to tag a 'LabelledPatch' as 'InMiddle' or 'InLast'.
pcSetLast :: Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast :: Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast = (LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY)
-> Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
forall a b c. (a -> b -> c) -> b -> a -> c
flip LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC

-- TODO pcsFirsts should be an 'RL', not an 'FL'.
-- | A sequence of 'LabelledPatch'es where each patch is either
-- 'InFirst', 'InMiddle', or 'InLast'. The representation is
-- optimized for the case where we start chosing patches from the left
-- of the sequence: patches that are 'InFirst' are commuted to the head
-- immediately, but patches that are 'InMiddle' or 'InLast' are mixed
-- together; when a patch is marked 'InLast', its dependencies are
-- not updated until we retrieve the final result.
data PatchChoices p wX wY where
  PCs :: { ()
pcsFirsts :: FL (LabelledPatch p) wX wM
         , ()
pcsMiddleLasts :: FL (PatchChoice p) wM wY}
      -> PatchChoices p wX wY

-- | See module documentation for "Darcs.Patch.Choices".
data Slot = InFirst | InMiddle | InLast

label :: LabelledPatch p wX wY -> Label
label :: LabelledPatch p wX wY -> Label
label (LP Label
tg p wX wY
_) = Label
tg

getLabelInt :: Label -> Int
getLabelInt :: Label -> Int
getLabelInt (Label Maybe Label
_ Int
i) = Int
i

unLabel :: LabelledPatch p wX wY -> p wX wY
unLabel :: LabelledPatch p wX wY -> p wX wY
unLabel (LP Label
_ p wX wY
p) = p wX wY
p

-- This is dangerous if two patches from different labelled series are compared
-- ideally Label (and hence LabelledPatch/PatchChoices) would have a witness type
-- to represent the originally labelled sequence.
compareLabels :: LabelledPatch p wA wB -> LabelledPatch p wC wD -> EqCheck (wA, wB) (wC, wD)
compareLabels :: LabelledPatch p wA wB
-> LabelledPatch p wC wD -> EqCheck (wA, wB) (wC, wD)
compareLabels (LP Label
l1 p wA wB
_) (LP Label
l2 p wC wD
_) = if Label
l1 Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
l2 then EqCheck Any Any -> EqCheck (wA, wB) (wC, wD)
forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP EqCheck Any Any
forall wA. EqCheck wA wA
IsEq else EqCheck (wA, wB) (wC, wD)
forall wA wB. EqCheck wA wB
NotEq

instance Invert p => Invert (LabelledPatch p) where
  invert :: LabelledPatch p wX wY -> LabelledPatch p wY wX
invert (LP Label
t p wX wY
p) = Label -> p wY wX -> LabelledPatch p wY wX
forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
t (p wX wY -> p wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
p)

instance Commute p => Commute (LabelledPatch p) where
  commute :: (:>) (LabelledPatch p) (LabelledPatch p) wX wY
-> Maybe ((:>) (LabelledPatch p) (LabelledPatch p) wX wY)
commute (LP Label
l1 p wX wZ
p1 :> LP Label
l2 p wZ wY
p2) = do
    p wX wZ
p2' :> p wZ wY
p1' <- (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wX wZ
p1 p wX wZ -> p wZ wY -> (:>) p p wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
p2)
    (:>) (LabelledPatch p) (LabelledPatch p) wX wY
-> Maybe ((:>) (LabelledPatch p) (LabelledPatch p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (Label -> p wX wZ -> LabelledPatch p wX wZ
forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
l2 p wX wZ
p2' LabelledPatch p wX wZ
-> LabelledPatch p wZ wY
-> (:>) (LabelledPatch p) (LabelledPatch p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Label -> p wZ wY -> LabelledPatch p wZ wY
forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
l1 p wZ wY
p1')

instance PatchInspect p => PatchInspect (LabelledPatch p) where
  listTouchedFiles :: LabelledPatch p wX wY -> [AnchoredPath]
listTouchedFiles = p wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles (p wX wY -> [AnchoredPath])
-> (LabelledPatch p wX wY -> p wX wY)
-> LabelledPatch p wX wY
-> [AnchoredPath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> p wX wY
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> p wX wY
unLabel
  hunkMatches :: (ByteString -> Bool) -> LabelledPatch p wX wY -> Bool
hunkMatches ByteString -> Bool
f = (ByteString -> Bool) -> p wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f (p wX wY -> Bool)
-> (LabelledPatch p wX wY -> p wX wY)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> p wX wY
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> p wX wY
unLabel

instance Commute p => Commute (PatchChoice p) where
  commute :: (:>) (PatchChoice p) (PatchChoice p) wX wY
-> Maybe ((:>) (PatchChoice p) (PatchChoice p) wX wY)
commute (PC LabelledPatch p wX wZ
p1 Bool
c1 :> PC LabelledPatch p wZ wY
p2 Bool
c2) = do
    LabelledPatch p wX wZ
p2' :> LabelledPatch p wZ wY
p1' <- (:>) (LabelledPatch p) (LabelledPatch p) wX wY
-> Maybe ((:>) (LabelledPatch p) (LabelledPatch p) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (LabelledPatch p wX wZ
p1 LabelledPatch p wX wZ
-> LabelledPatch p wZ wY
-> (:>) (LabelledPatch p) (LabelledPatch p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wZ wY
p2)
    (:>) (PatchChoice p) (PatchChoice p) wX wY
-> Maybe ((:>) (PatchChoice p) (PatchChoice p) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (LabelledPatch p wX wZ -> Bool -> PatchChoice p wX wZ
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wX wZ
p2' Bool
c2 PatchChoice p wX wZ
-> PatchChoice p wZ wY
-> (:>) (PatchChoice p) (PatchChoice p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wZ wY -> Bool -> PatchChoice p wZ wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wZ wY
p1' Bool
c1)

instance PatchInspect p => PatchInspect (PatchChoice p) where
  listTouchedFiles :: PatchChoice p wX wY -> [AnchoredPath]
listTouchedFiles = LabelledPatch p wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles (LabelledPatch p wX wY -> [AnchoredPath])
-> (PatchChoice p wX wY -> LabelledPatch p wX wY)
-> PatchChoice p wX wY
-> [AnchoredPath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatchChoice p wX wY -> LabelledPatch p wX wY
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch
  hunkMatches :: (ByteString -> Bool) -> PatchChoice p wX wY -> Bool
hunkMatches ByteString -> Bool
f = (ByteString -> Bool) -> LabelledPatch p wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f (LabelledPatch p wX wY -> Bool)
-> (PatchChoice p wX wY -> LabelledPatch p wX wY)
-> PatchChoice p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatchChoice p wX wY -> LabelledPatch p wX wY
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch

-- | Create a 'PatchChoices' from a sequence of patches, so that
-- all patches are initially 'InMiddle'.
patchChoices :: FL p wX wY -> PatchChoices p wX wY
patchChoices :: FL p wX wY -> PatchChoices p wX wY
patchChoices = FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wY.
FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices (FL (LabelledPatch p) wX wY -> PatchChoices p wX wY)
-> (FL p wX wY -> FL (LabelledPatch p) wX wY)
-> FL p wX wY
-> PatchChoices p wX wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
forall (p :: * -> * -> *) wX wY.
Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
labelPatches Maybe Label
forall a. Maybe a
Nothing

-- | Label a sequence of patches, maybe using the given parent label.
labelPatches :: Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
labelPatches :: Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
labelPatches Maybe Label
tg FL p wX wY
ps = (forall wX wY. Label -> p wX wY -> LabelledPatch p wX wY)
-> [Label] -> FL p wX wY -> FL (LabelledPatch p) wX wY
forall a (p :: * -> * -> *) (q :: * -> * -> *) wW wZ.
(forall wX wY. a -> p wX wY -> q wX wY)
-> [a] -> FL p wW wZ -> FL q wW wZ
zipWithFL forall wX wY. Label -> p wX wY -> LabelledPatch p wX wY
forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP ((Int -> Label) -> [Int] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Label -> Int -> Label
Label Maybe Label
tg) [Int
1..]) FL p wX wY
ps

-- | Create a 'PatchChoices' from an already labelled sequence of patches,
-- so that all patches are initially 'InMiddle'.
mkPatchChoices :: FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices :: FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices = FL (LabelledPatch p) wX wX
-> FL (PatchChoice p) wX wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs FL (LabelledPatch p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL (FL (PatchChoice p) wX wY -> PatchChoices p wX wY)
-> (FL (LabelledPatch p) wX wY -> FL (PatchChoice p) wX wY)
-> FL (LabelledPatch p) wX wY
-> PatchChoices p wX wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wX wY -> FL (PatchChoice p) wX wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (Bool -> LabelledPatch p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
False)


-- | Like 'getChoices' but lumps together 'InMiddle' and 'InLast' patches.
-- This is more efficient than using 'getChoices' and then catenating 'InMiddle'
-- and 'InLast' sections because we have to commute less.
-- (This is what 'PatchChoices' are optimized for.)
--
-- prop> separateFirstFromMiddleLast c == case getChoices c of f:>m:>l -> f:>m+>+l
separateFirstFromMiddleLast :: PatchChoices p wX wZ
                            -> (FL (LabelledPatch p) :> FL (LabelledPatch p)) wX wZ
separateFirstFromMiddleLast :: PatchChoices p wX wZ
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wZ
separateFirstFromMiddleLast (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wZ
ml) = FL (LabelledPatch p) wX wM
f FL (LabelledPatch p) wX wM
-> FL (LabelledPatch p) wM wZ
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (forall wW wY. PatchChoice p wW wY -> LabelledPatch p wW wY)
-> FL (PatchChoice p) wM wZ -> FL (LabelledPatch p) wM wZ
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. PatchChoice p wW wY -> LabelledPatch p wW wY
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch FL (PatchChoice p) wM wZ
ml

-- | Like 'getChoices' but lumps together 'InFirst' and 'InMiddle' patches.
--
-- prop> separateFirstMiddleFromLast c == case getChoices c of f:>m:>l -> f+>+m:>l
separateFirstMiddleFromLast :: Commute p
                            => PatchChoices p wX wZ
                            -> (FL (LabelledPatch p) :> FL (LabelledPatch p)) wX wZ
separateFirstMiddleFromLast :: PatchChoices p wX wZ
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wZ
separateFirstMiddleFromLast (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wZ
l) =
  case FL (PatchChoice p) wM wZ
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wM wZ
forall (p :: * -> * -> *) wX wY.
Commute p =>
FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wM wZ
l of
    (FL (LabelledPatch p) wM wZ
m :> FL (LabelledPatch p) wZ wZ
l') -> FL (LabelledPatch p) wX wM
f FL (LabelledPatch p) wX wM
-> FL (LabelledPatch p) wM wZ -> FL (LabelledPatch p) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wM wZ
m FL (LabelledPatch p) wX wZ
-> FL (LabelledPatch p) wZ wZ
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wZ wZ
l'

-- | Retrieve the resulting sections from a 'PatchChoice'.  The result is a
-- triple @first:>middle:>last@, such that all patches in @first@ are
-- 'InFirst', all patches in @middle@ are 'InMiddle', and all patches in @last@
-- are 'InLast'.
getChoices :: Commute p
           => PatchChoices p wX wY
           -> (FL (LabelledPatch p) :> FL (LabelledPatch p) :> FL (LabelledPatch p)) wX wY
getChoices :: PatchChoices p wX wY
-> (:>)
     (FL (LabelledPatch p))
     (FL (LabelledPatch p) :> FL (LabelledPatch p))
     wX
     wY
getChoices (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
ml) =
  case FL (PatchChoice p) wM wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wM wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wM wY
ml of
    (FL (LabelledPatch p) wM wZ
m :> FL (LabelledPatch p) wZ wY
l') -> FL (LabelledPatch p) wX wM
f FL (LabelledPatch p) wX wM
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wM wY
-> (:>)
     (FL (LabelledPatch p))
     (FL (LabelledPatch p) :> FL (LabelledPatch p))
     wX
     wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wM wZ
m FL (LabelledPatch p) wM wZ
-> FL (LabelledPatch p) wZ wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wM wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wZ wY
l'

-- | Internal function to commute patches in the common 'pcsMiddleLasts' segment
-- so that all 'InLast' patches are behind 'InMiddle' ones. Patches 'InMiddle'
-- that depend on any 'InLast' are promoted to 'InLast'.
pushLasts :: Commute p
          => FL (PatchChoice p) wX wY
          -> (FL (LabelledPatch p) :> FL (LabelledPatch p)) wX wY
pushLasts :: FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wX wY
NilFL = FL (LabelledPatch p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL (LabelledPatch p) wX wX
-> FL (LabelledPatch p) wX wX
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
pushLasts (PC LabelledPatch p wX wY
lp Bool
False :>: FL (PatchChoice p) wY wY
pcs) =
  case FL (PatchChoice p) wY wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wY wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wY wY
pcs of
       (FL (LabelledPatch p) wY wZ
m :> FL (LabelledPatch p) wZ wY
l) -> (LabelledPatch p wX wY
lp LabelledPatch p wX wY
-> FL (LabelledPatch p) wY wZ -> FL (LabelledPatch p) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wY wZ
m) FL (LabelledPatch p) wX wZ
-> FL (LabelledPatch p) wZ wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wZ wY
l
pushLasts (PC LabelledPatch p wX wY
lp Bool
True :>: FL (PatchChoice p) wY wY
pcs) =
  case FL (PatchChoice p) wY wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wY wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wY wY
pcs of
    (FL (LabelledPatch p) wY wZ
m :> FL (LabelledPatch p) wZ wY
l) ->
      case (:>) (LabelledPatch p) (FL (LabelledPatch p)) wX wZ
-> (:>)
     (FL (LabelledPatch p))
     (LabelledPatch p :> FL (LabelledPatch p))
     wX
     wZ
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (LabelledPatch p wX wY
lp LabelledPatch p wX wY
-> FL (LabelledPatch p) wY wZ
-> (:>) (LabelledPatch p) (FL (LabelledPatch p)) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wY wZ
m) of
        (FL (LabelledPatch p) wX wZ
m' :> LabelledPatch p wZ wZ
lp' :> FL (LabelledPatch p) wZ wZ
deps) -> FL (LabelledPatch p) wX wZ
m' FL (LabelledPatch p) wX wZ
-> FL (LabelledPatch p) wZ wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (LabelledPatch p wZ wZ
lp' LabelledPatch p wZ wZ
-> FL (LabelledPatch p) wZ wY -> FL (LabelledPatch p) wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wZ wZ
deps FL (LabelledPatch p) wZ wZ
-> FL (LabelledPatch p) wZ wY -> FL (LabelledPatch p) wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wZ wY
l)

-- TODO for the way we use this function it is too restrictive IMO: it does not
-- allow the user to select anything that doesn't match the pre-filters.
-- | Use the given monadic 'PatchChoices' transformer on the 'InMiddle' section
-- of a 'PatchChoices', then fold the result back into the original 'PatchChoices'.
refineChoices :: (Commute p, Monad m)
              => (forall wU wV . FL (LabelledPatch p) wU wV ->
                  PatchChoices p wU wV -> m (PatchChoices p wU wV))
              -> PatchChoices p wX wY -> m (PatchChoices p wX wY)
refineChoices :: (forall wU wV.
 FL (LabelledPatch p) wU wV
 -> PatchChoices p wU wV -> m (PatchChoices p wU wV))
-> PatchChoices p wX wY -> m (PatchChoices p wX wY)
refineChoices forall wU wV.
FL (LabelledPatch p) wU wV
-> PatchChoices p wU wV -> m (PatchChoices p wU wV)
act PatchChoices p wX wY
ps =
  case PatchChoices p wX wY
-> (:>)
     (FL (LabelledPatch p))
     (FL (LabelledPatch p) :> FL (LabelledPatch p))
     wX
     wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
PatchChoices p wX wY
-> (:>)
     (FL (LabelledPatch p))
     (FL (LabelledPatch p) :> FL (LabelledPatch p))
     wX
     wY
getChoices PatchChoices p wX wY
ps of
    (FL (LabelledPatch p) wX wZ
f :> FL (LabelledPatch p) wZ wZ
m :> FL (LabelledPatch p) wZ wY
l) -> do
      (PCs FL (LabelledPatch p) wZ wM
f' FL (PatchChoice p) wM wZ
l') <- FL (LabelledPatch p) wZ wZ
-> PatchChoices p wZ wZ -> m (PatchChoices p wZ wZ)
forall wU wV.
FL (LabelledPatch p) wU wV
-> PatchChoices p wU wV -> m (PatchChoices p wU wV)
act FL (LabelledPatch p) wZ wZ
m (FL (LabelledPatch p) wZ wZ -> PatchChoices p wZ wZ
forall (p :: * -> * -> *) wX wY.
FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices FL (LabelledPatch p) wZ wZ
m)
      PatchChoices p wX wY -> m (PatchChoices p wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (PatchChoices p wX wY -> m (PatchChoices p wX wY))
-> (FL (PatchChoice p) wM wY -> PatchChoices p wX wY)
-> FL (PatchChoice p) wM wY
-> m (PatchChoices p wX wY)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wZ
f FL (LabelledPatch p) wX wZ
-> FL (LabelledPatch p) wZ wM -> FL (LabelledPatch p) wX wM
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wZ wM
f') (FL (PatchChoice p) wM wY -> m (PatchChoices p wX wY))
-> FL (PatchChoice p) wM wY -> m (PatchChoices p wX wY)
forall a b. (a -> b) -> a -> b
$ FL (PatchChoice p) wM wZ
l' FL (PatchChoice p) wM wZ
-> FL (PatchChoice p) wZ wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wZ wY -> FL (PatchChoice p) wZ wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (Bool -> LabelledPatch p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
True) FL (LabelledPatch p) wZ wY
l

-- | Given a 'LabelledPatch' determine to which section of the given
-- 'PatchChoices' it belongs. This is not trivial to compute, since a patch
-- tagged as 'InMiddle' may be forced to actually be 'InLast' by dependencies. We
-- return a possibly re-ordered 'PatchChoices' so as not to waste the
-- commutation effort.
patchSlot :: forall p wA wB wX wY. Commute p
          => LabelledPatch p wA wB
          -> PatchChoices p wX wY
          -> (Slot, PatchChoices p wX wY)
patchSlot :: LabelledPatch p wA wB
-> PatchChoices p wX wY -> (Slot, PatchChoices p wX wY)
patchSlot (LP Label
t p wA wB
_) pc :: PatchChoices p wX wY
pc@(PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
ml)
  | FL (LabelledPatch p) wX wM -> Bool
forall (p :: * -> * -> *) wW wZ. FL (LabelledPatch p) wW wZ -> Bool
foundIn FL (LabelledPatch p) wX wM
f = (Slot
InFirst, PatchChoices p wX wY
pc)
  | Bool
otherwise = FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wM
-> RL (LabelledPatch p) wM wM
-> FL (PatchChoice p) wM wY
-> (Slot, PatchChoices p wX wY)
forall wM wC wL.
FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wL
-> FL (PatchChoice p) wL wY
-> (Slot, PatchChoices p wX wY)
psLast FL (LabelledPatch p) wX wM
f RL (LabelledPatch p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (LabelledPatch p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (PatchChoice p) wM wY
ml
  where
    foundIn :: FL (LabelledPatch p) wW wZ -> Bool
foundIn = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> FL (LabelledPatch p) wW wZ -> Bool
forall (a :: * -> * -> *) wW wZ.
(forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool
anyFL ((Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
t) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label)
    psLast :: forall wM wC wL .
             FL (LabelledPatch p) wX wM ->
             RL (LabelledPatch p) wM wC ->
             RL (LabelledPatch p) wC wL ->
             FL (PatchChoice p) wL wY ->
             (Slot, PatchChoices p wX wY)
    psLast :: FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wL
-> FL (PatchChoice p) wL wY
-> (Slot, PatchChoices p wX wY)
psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles RL (LabelledPatch p) wC wL
bubble (PC LabelledPatch p wL wY
lp Bool
True :>: FL (PatchChoice p) wY wY
ls)
      | LabelledPatch p wL wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label LabelledPatch p wL wY
lp Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
t = (Slot
InLast
                      , PCs :: forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                            , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = RL (LabelledPatch p) wM wC -> FL (PatchChoice p) wM wC
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                         FL (PatchChoice p) wM wC
-> FL (PatchChoice p) wC wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ RL (LabelledPatch p) wC wL -> FL (PatchChoice p) wC wL
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wC wL
bubble
                                         FL (PatchChoice p) wC wL
-> FL (PatchChoice p) wL wY -> FL (PatchChoice p) wC wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ LabelledPatch p wL wY -> Bool -> PatchChoice p wL wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wL wY
lp Bool
True PatchChoice p wL wY
-> FL (PatchChoice p) wY wY -> FL (PatchChoice p) wL wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PatchChoice p) wY wY
ls})
    psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles RL (LabelledPatch p) wC wL
bubble (PC LabelledPatch p wL wY
lp Bool
False :>: FL (PatchChoice p) wY wY
ls)
      | LabelledPatch p wL wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label LabelledPatch p wL wY
lp Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
t =
        case (:>) (RL (LabelledPatch p)) (LabelledPatch p) wC wY
-> Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wC wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wC wL
bubble RL (LabelledPatch p) wC wL
-> LabelledPatch p wL wY
-> (:>) (RL (LabelledPatch p)) (LabelledPatch p) wC wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wL wY
lp) of
        Just (LabelledPatch p wC wZ
lp' :> RL (LabelledPatch p) wZ wY
bubble') -> (Slot
InMiddle,
                                 PCs :: forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                                     , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = RL (LabelledPatch p) wM wC -> FL (PatchChoice p) wM wC
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                                  FL (PatchChoice p) wM wC
-> FL (PatchChoice p) wC wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ LabelledPatch p wC wZ -> Bool -> PatchChoice p wC wZ
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wC wZ
lp' Bool
False
                                                  PatchChoice p wC wZ
-> FL (PatchChoice p) wZ wY -> FL (PatchChoice p) wC wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: RL (LabelledPatch p) wZ wY -> FL (PatchChoice p) wZ wY
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wZ wY
bubble'
                                                  FL (PatchChoice p) wZ wY
-> FL (PatchChoice p) wY wY -> FL (PatchChoice p) wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PatchChoice p) wY wY
ls})
        Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wC wY)
Nothing -> (Slot
InLast,
                   PCs :: forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                       , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = RL (LabelledPatch p) wM wC -> FL (PatchChoice p) wM wC
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                    FL (PatchChoice p) wM wC
-> FL (PatchChoice p) wC wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ RL (LabelledPatch p) wC wL -> FL (PatchChoice p) wC wL
forall (p :: * -> * -> *) wX wZ.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wC wL
bubble
                                    FL (PatchChoice p) wC wL
-> FL (PatchChoice p) wL wY -> FL (PatchChoice p) wC wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ LabelledPatch p wL wY -> Bool -> PatchChoice p wL wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wL wY
lp Bool
True
                                    PatchChoice p wL wY
-> FL (PatchChoice p) wY wY -> FL (PatchChoice p) wL wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PatchChoice p) wY wY
ls})
    psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles RL (LabelledPatch p) wC wL
bubble (PC LabelledPatch p wL wY
lp Bool
True :>: FL (PatchChoice p) wY wY
ls) =
      FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wY
-> FL (PatchChoice p) wY wY
-> (Slot, PatchChoices p wX wY)
forall wM wC wL.
FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wL
-> FL (PatchChoice p) wL wY
-> (Slot, PatchChoices p wX wY)
psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles (RL (LabelledPatch p) wC wL
bubble RL (LabelledPatch p) wC wL
-> LabelledPatch p wL wY -> RL (LabelledPatch p) wC wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wL wY
lp) FL (PatchChoice p) wY wY
ls
    psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles RL (LabelledPatch p) wC wL
bubble (PC LabelledPatch p wL wY
lp Bool
False :>: FL (PatchChoice p) wY wY
ls) =
      case (:>) (RL (LabelledPatch p)) (LabelledPatch p) wC wY
-> Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wC wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wC wL
bubble RL (LabelledPatch p) wC wL
-> LabelledPatch p wL wY
-> (:>) (RL (LabelledPatch p)) (LabelledPatch p) wC wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wL wY
lp) of
        Just (LabelledPatch p wC wZ
lp' :> RL (LabelledPatch p) wZ wY
bubble') -> FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wZ
-> RL (LabelledPatch p) wZ wY
-> FL (PatchChoice p) wY wY
-> (Slot, PatchChoices p wX wY)
forall wM wC wL.
FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wL
-> FL (PatchChoice p) wL wY
-> (Slot, PatchChoices p wX wY)
psLast FL (LabelledPatch p) wX wM
firsts (RL (LabelledPatch p) wM wC
middles RL (LabelledPatch p) wM wC
-> LabelledPatch p wC wZ -> RL (LabelledPatch p) wM wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wC wZ
lp') RL (LabelledPatch p) wZ wY
bubble' FL (PatchChoice p) wY wY
ls
        Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wC wY)
Nothing -> FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wY
-> FL (PatchChoice p) wY wY
-> (Slot, PatchChoices p wX wY)
forall wM wC wL.
FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wC
-> RL (LabelledPatch p) wC wL
-> FL (PatchChoice p) wL wY
-> (Slot, PatchChoices p wX wY)
psLast FL (LabelledPatch p) wX wM
firsts RL (LabelledPatch p) wM wC
middles (RL (LabelledPatch p) wC wL
bubble RL (LabelledPatch p) wC wL
-> LabelledPatch p wL wY -> RL (LabelledPatch p) wC wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wL wY
lp) FL (PatchChoice p) wY wY
ls
    psLast FL (LabelledPatch p) wX wM
_ RL (LabelledPatch p) wM wC
_ RL (LabelledPatch p) wC wL
_ FL (PatchChoice p) wL wY
NilFL = [Char] -> (Slot, PatchChoices p wX wY)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible case"
    settleM :: RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wX wZ
middles = (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (\LabelledPatch p wW wY
lp -> LabelledPatch p wW wY -> Bool -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
False) (FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ)
-> FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
forall a b. (a -> b) -> a -> b
$ RL (LabelledPatch p) wX wZ -> FL (LabelledPatch p) wX wZ
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wX wZ
middles
    settleB :: RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wX wZ
bubble = (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (\LabelledPatch p wW wY
lp -> LabelledPatch p wW wY -> Bool -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
True) (FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ)
-> FL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
forall a b. (a -> b) -> a -> b
$ RL (LabelledPatch p) wX wZ -> FL (LabelledPatch p) wX wZ
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wX wZ
bubble

-- | Force all patches matching the given predicate to be 'InFirst',
-- pulling any dependencies with them. This even forces any patches
-- that were already tagged 'InLast'.
forceMatchingFirst :: forall p wA wB. Commute p
                   => ( forall wX wY . LabelledPatch p wX wY -> Bool)
                   -> PatchChoices p wA wB
                   -> PatchChoices p wA wB
forceMatchingFirst :: (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingFirst forall wX wY. LabelledPatch p wX wY -> Bool
pred (PCs FL (LabelledPatch p) wA wM
f0 FL (PatchChoice p) wM wB
ml) = FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wM
-> FL (PatchChoice p) wM wB
-> PatchChoices p wA wB
forall wM wN.
FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wN
-> FL (PatchChoice p) wN wB
-> PatchChoices p wA wB
fmfLasts FL (LabelledPatch p) wA wM
f0 RL (PatchChoice p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (PatchChoice p) wM wB
ml
    where
      fmfLasts :: FL (LabelledPatch p) wA wM
                 -> RL (PatchChoice p) wM wN
                 -> FL (PatchChoice p) wN wB
                 -> PatchChoices p wA wB
      fmfLasts :: FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wN
-> FL (PatchChoice p) wN wB
-> PatchChoices p wA wB
fmfLasts FL (LabelledPatch p) wA wM
f RL (PatchChoice p) wM wN
l1 (PatchChoice p wN wY
a :>: FL (PatchChoice p) wY wB
l2)
          | PatchChoice p wN wY -> Bool
forall wX wY. PatchChoice p wX wY -> Bool
pred_pc PatchChoice p wN wY
a =
            case (:>) (RL (PatchChoice p)) (PatchChoice p) wM wY
-> (:>)
     (RL (PatchChoice p)) (PatchChoice p :> RL (PatchChoice p)) wM wY
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> (:>) (RL p) (p :> RL p) wX wY
commuteWhatWeCanRL (RL (PatchChoice p) wM wN
l1 RL (PatchChoice p) wM wN
-> PatchChoice p wN wY
-> (:>) (RL (PatchChoice p)) (PatchChoice p) wM wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchChoice p wN wY
a) of
              (RL (PatchChoice p) wM wZ
deps :> PatchChoice p wZ wZ
a' :> RL (PatchChoice p) wZ wY
l1') ->
                let
                  f' :: FL (LabelledPatch p) wA wZ
f' = FL (LabelledPatch p) wA wM
f FL (LabelledPatch p) wA wM
-> FL (LabelledPatch p) wM wZ -> FL (LabelledPatch p) wA wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (forall wW wY. PatchChoice p wW wY -> LabelledPatch p wW wY)
-> FL (PatchChoice p) wM wZ -> FL (LabelledPatch p) wM wZ
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. PatchChoice p wW wY -> LabelledPatch p wW wY
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch (RL (PatchChoice p) wM wZ -> FL (PatchChoice p) wM wZ
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PatchChoice p) wM wZ
deps) FL (LabelledPatch p) wM wZ
-> FL (LabelledPatch p) wZ wZ -> FL (LabelledPatch p) wM wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (PatchChoice p wZ wZ -> LabelledPatch p wZ wZ
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch PatchChoice p wZ wZ
a' LabelledPatch p wZ wZ
-> FL (LabelledPatch p) wZ wZ -> FL (LabelledPatch p) wZ wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
                in FL (LabelledPatch p) wA wZ
-> RL (PatchChoice p) wZ wY
-> FL (PatchChoice p) wY wB
-> PatchChoices p wA wB
forall wM wN.
FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wN
-> FL (PatchChoice p) wN wB
-> PatchChoices p wA wB
fmfLasts FL (LabelledPatch p) wA wZ
f' RL (PatchChoice p) wZ wY
l1' FL (PatchChoice p) wY wB
l2
      fmfLasts FL (LabelledPatch p) wA wM
f RL (PatchChoice p) wM wN
l1 (PatchChoice p wN wY
a :>: FL (PatchChoice p) wY wB
l2) = FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wY
-> FL (PatchChoice p) wY wB
-> PatchChoices p wA wB
forall wM wN.
FL (LabelledPatch p) wA wM
-> RL (PatchChoice p) wM wN
-> FL (PatchChoice p) wN wB
-> PatchChoices p wA wB
fmfLasts FL (LabelledPatch p) wA wM
f (RL (PatchChoice p) wM wN
l1 RL (PatchChoice p) wM wN
-> PatchChoice p wN wY -> RL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: PatchChoice p wN wY
a) FL (PatchChoice p) wY wB
l2
      fmfLasts FL (LabelledPatch p) wA wM
f RL (PatchChoice p) wM wN
l1 FL (PatchChoice p) wN wB
NilFL = PCs :: forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs { pcsFirsts :: FL (LabelledPatch p) wA wM
pcsFirsts = FL (LabelledPatch p) wA wM
f
                                , pcsMiddleLasts :: FL (PatchChoice p) wM wB
pcsMiddleLasts = RL (PatchChoice p) wM wN -> FL (PatchChoice p) wM wN
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PatchChoice p) wM wN
l1 }
      pred_pc :: forall wX wY . PatchChoice p wX wY -> Bool
      pred_pc :: PatchChoice p wX wY -> Bool
pred_pc (PC LabelledPatch p wX wY
lp Bool
_) = LabelledPatch p wX wY -> Bool
forall wX wY. LabelledPatch p wX wY -> Bool
pred LabelledPatch p wX wY
lp

-- | Force all patches labelled with one of the given labels to be 'InFirst',
-- pulling any dependencies with them. This even forces any patches
-- that were already tagged 'InLast'.
forceFirsts :: Commute p
            => [Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirsts :: [Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirsts [Label]
ps = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingFirst ((Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Label]
ps) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label)

-- | Force a single patch labelled with the given label to be 'InFirst',
-- pulling any dependencies with them. This even forces any patches
-- that were already tagged 'InLast'.
forceFirst :: Commute p
           => Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirst :: Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirst Label
p = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingFirst ((Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
p) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label)
--TODO: stop after having seen the patch we want to force first

-- | Make all 'InMiddle' patches either 'InFirst' or 'InLast'. This does *not*
-- modify any patches that are already determined to be 'InLast' by
-- dependencies.
selectAllMiddles :: forall p wX wY. Commute p
                 => Bool -> PatchChoices p wX wY -> PatchChoices p wX wY
selectAllMiddles :: Bool -> PatchChoices p wX wY -> PatchChoices p wX wY
selectAllMiddles Bool
True (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
l) = FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs FL (LabelledPatch p) wX wM
f ((forall wW wY. PatchChoice p wW wY -> PatchChoice p wW wY)
-> FL (PatchChoice p) wM wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. PatchChoice p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> PatchChoice p wX wY
g FL (PatchChoice p) wM wY
l)
    where g :: PatchChoice p wX wY -> PatchChoice p wX wY
g (PC LabelledPatch p wX wY
lp Bool
_) = LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wX wY
lp Bool
True
selectAllMiddles Bool
False (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
l) = FL (LabelledPatch p) wX wM
-> RL (LabelledPatch p) wM wM
-> RL (PatchChoice p) wM wM
-> FL (PatchChoice p) wM wY
-> PatchChoices p wX wY
forall wM1 wM2 wM3.
FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> PatchChoices p wX wY
samf FL (LabelledPatch p) wX wM
f RL (LabelledPatch p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (PatchChoice p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (PatchChoice p) wM wY
l
  where
    samf :: forall wM1 wM2 wM3 .
           FL (LabelledPatch p) wX wM1 ->
           RL (LabelledPatch p) wM1 wM2 ->
           RL (PatchChoice p) wM2 wM3 ->
           FL (PatchChoice p) wM3 wY ->
           PatchChoices p wX wY
    samf :: FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> PatchChoices p wX wY
samf FL (LabelledPatch p) wX wM1
f1 RL (LabelledPatch p) wM1 wM2
f2 RL (PatchChoice p) wM2 wM3
l1 (pc :: PatchChoice p wM3 wY
pc@(PC LabelledPatch p wM3 wY
lp Bool
False) :>: FL (PatchChoice p) wY wY
l2) =
      case (:>) (RL (PatchChoice p)) (PatchChoice p) wM2 wY
-> Maybe ((:>) (PatchChoice p) (RL (PatchChoice p)) wM2 wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (PatchChoice p) wM2 wM3
l1 RL (PatchChoice p) wM2 wM3
-> PatchChoice p wM3 wY
-> (:>) (RL (PatchChoice p)) (PatchChoice p) wM2 wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PatchChoice p wM3 wY
pc) of
        Maybe ((:>) (PatchChoice p) (RL (PatchChoice p)) wM2 wY)
Nothing -> FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wY
-> FL (PatchChoice p) wY wY
-> PatchChoices p wX wY
forall wM1 wM2 wM3.
FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> PatchChoices p wX wY
samf FL (LabelledPatch p) wX wM1
f1 RL (LabelledPatch p) wM1 wM2
f2 (RL (PatchChoice p) wM2 wM3
l1 RL (PatchChoice p) wM2 wM3
-> PatchChoice p wM3 wY -> RL (PatchChoice p) wM2 wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM3 wY -> Bool -> PatchChoice p wM3 wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wM3 wY
lp Bool
True) FL (PatchChoice p) wY wY
l2
        Just ((PC LabelledPatch p wM2 wZ
lp' Bool
_) :> RL (PatchChoice p) wZ wY
l1') -> FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wZ
-> RL (PatchChoice p) wZ wY
-> FL (PatchChoice p) wY wY
-> PatchChoices p wX wY
forall wM1 wM2 wM3.
FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> PatchChoices p wX wY
samf FL (LabelledPatch p) wX wM1
f1 (RL (LabelledPatch p) wM1 wM2
f2 RL (LabelledPatch p) wM1 wM2
-> LabelledPatch p wM2 wZ -> RL (LabelledPatch p) wM1 wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM2 wZ
lp') RL (PatchChoice p) wZ wY
l1' FL (PatchChoice p) wY wY
l2
    samf FL (LabelledPatch p) wX wM1
f1 RL (LabelledPatch p) wM1 wM2
f2 RL (PatchChoice p) wM2 wM3
l1 (PC LabelledPatch p wM3 wY
lp Bool
True :>: FL (PatchChoice p) wY wY
l2) = FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wY
-> FL (PatchChoice p) wY wY
-> PatchChoices p wX wY
forall wM1 wM2 wM3.
FL (LabelledPatch p) wX wM1
-> RL (LabelledPatch p) wM1 wM2
-> RL (PatchChoice p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> PatchChoices p wX wY
samf FL (LabelledPatch p) wX wM1
f1 RL (LabelledPatch p) wM1 wM2
f2 (RL (PatchChoice p) wM2 wM3
l1 RL (PatchChoice p) wM2 wM3
-> PatchChoice p wM3 wY -> RL (PatchChoice p) wM2 wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM3 wY -> Bool -> PatchChoice p wM3 wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wM3 wY
lp Bool
True) FL (PatchChoice p) wY wY
l2
    samf FL (LabelledPatch p) wX wM1
f1 RL (LabelledPatch p) wM1 wM2
f2 RL (PatchChoice p) wM2 wM3
l1 FL (PatchChoice p) wM3 wY
NilFL = FL (LabelledPatch p) wX wM2
-> FL (PatchChoice p) wM2 wM3 -> PatchChoices p wX wM3
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wM1
f1 FL (LabelledPatch p) wX wM1
-> FL (LabelledPatch p) wM1 wM2 -> FL (LabelledPatch p) wX wM2
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ RL (LabelledPatch p) wM1 wM2 -> FL (LabelledPatch p) wM1 wM2
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wM1 wM2
f2) (RL (PatchChoice p) wM2 wM3 -> FL (PatchChoice p) wM2 wM3
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PatchChoice p) wM2 wM3
l1)

-- | Similar to 'forceMatchingFirst' only that patches are forced to be
-- 'InLast' regardless of their previous status.
forceMatchingLast :: Commute p => (forall wX wY . LabelledPatch p wX wY -> Bool)
                  -> PatchChoices p wA wB
                  -> PatchChoices p wA wB
forceMatchingLast :: (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingLast forall wX wY. LabelledPatch p wX wY -> Bool
pred (PCs FL (LabelledPatch p) wA wM
f FL (PatchChoice p) wM wB
ml) =
  (forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wA
-> FL (LabelledPatch p) wA wM
-> FL (PatchChoice p) wM wB
-> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB wM1 wM2.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
True RL (LabelledPatch p) wA wA
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (LabelledPatch p) wA wM
f FL (PatchChoice p) wM wB
ml

-- | Internal function working directly on the constituent parts of a
-- 'PatchChoices' and taking an accumulating 'RL' to build up a new 'InFirst'
-- section.  It forces patches to be 'InMiddle' or 'InLast', depending
-- on the 'Bool' parameter ('True' means 'InLast', 'False' means 'InMiddle').
-- It does this regardless of the previous status of patches and also pulls
-- any dependent patches with it.
forceMatchingMiddleOrLast
  :: forall p wA wB wM1 wM2 . Commute p
  => (forall wX wY . LabelledPatch p wX wY -> Bool)
  -> Bool
  -> RL (LabelledPatch p) wA wM1  -- ^ accumulator for 'InFirst' patches
  -> FL (LabelledPatch p) wM1 wM2 -- ^ original 'InFirst' section
  -> FL (PatchChoice p) wM2 wB    -- ^ original 'InMiddle' and 'InLast' section
  -> PatchChoices p wA wB
forceMatchingMiddleOrLast :: (forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
b RL (LabelledPatch p) wA wM1
f1 (LabelledPatch p wM1 wY
a :>: FL (LabelledPatch p) wY wM2
f2) FL (PatchChoice p) wM2 wB
ml
  | LabelledPatch p wM1 wY -> Bool
forall wX wY. LabelledPatch p wX wY -> Bool
pred LabelledPatch p wM1 wY
a =
    case (:>) (LabelledPatch p) (FL (LabelledPatch p)) wM1 wM2
-> (:>)
     (FL (LabelledPatch p))
     (LabelledPatch p :> FL (LabelledPatch p))
     wM1
     wM2
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (LabelledPatch p wM1 wY
a LabelledPatch p wM1 wY
-> FL (LabelledPatch p) wY wM2
-> (:>) (LabelledPatch p) (FL (LabelledPatch p)) wM1 wM2
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wY wM2
f2) of
      (FL (LabelledPatch p) wM1 wZ
f2' :> LabelledPatch p wZ wZ
a' :> FL (LabelledPatch p) wZ wM2
deps) ->
        let
          ml' :: FL (PatchChoice p) wZ wB
ml' = (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wZ wM2 -> FL (PatchChoice p) wZ wM2
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (Bool -> LabelledPatch p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
b) (LabelledPatch p wZ wZ
a' LabelledPatch p wZ wZ
-> FL (LabelledPatch p) wZ wM2 -> FL (LabelledPatch p) wZ wM2
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wZ wM2
deps) FL (PatchChoice p) wZ wM2
-> FL (PatchChoice p) wM2 wB -> FL (PatchChoice p) wZ wB
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PatchChoice p) wM2 wB
ml
        in
        (forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wZ
-> FL (PatchChoice p) wZ wB
-> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB wM1 wM2.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
b RL (LabelledPatch p) wA wM1
f1 FL (LabelledPatch p) wM1 wZ
f2' FL (PatchChoice p) wZ wB
ml'
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
b RL (LabelledPatch p) wA wM1
f1 (LabelledPatch p wM1 wY
a :>: FL (LabelledPatch p) wY wM2
f2) FL (PatchChoice p) wM2 wB
ml =
  (forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wY
-> FL (LabelledPatch p) wY wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB wM1 wM2.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
b (RL (LabelledPatch p) wA wM1
f1 RL (LabelledPatch p) wA wM1
-> LabelledPatch p wM1 wY -> RL (LabelledPatch p) wA wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM1 wY
a) FL (LabelledPatch p) wY wM2
f2 FL (PatchChoice p) wM2 wB
ml
forceMatchingMiddleOrLast forall wX wY. LabelledPatch p wX wY -> Bool
pred Bool
b RL (LabelledPatch p) wA wM1
f1 FL (LabelledPatch p) wM1 wM2
NilFL FL (PatchChoice p) wM2 wB
ml =
  PCs :: forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs { pcsFirsts :: FL (LabelledPatch p) wA wM1
pcsFirsts = RL (LabelledPatch p) wA wM1 -> FL (LabelledPatch p) wA wM1
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wA wM1
f1
      , pcsMiddleLasts :: FL (PatchChoice p) wM1 wB
pcsMiddleLasts = (forall wW wY. PatchChoice p wW wY -> PatchChoice p wW wY)
-> FL (PatchChoice p) wM2 wB -> FL (PatchChoice p) wM2 wB
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. PatchChoice p wW wY -> PatchChoice p wW wY
choose FL (PatchChoice p) wM2 wB
ml
      }
  where
    choose :: PatchChoice p wX wY -> PatchChoice p wX wY
choose (PC LabelledPatch p wX wY
lp Bool
c) = (LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wX wY
lp (if LabelledPatch p wX wY -> Bool
forall wX wY. LabelledPatch p wX wY -> Bool
pred LabelledPatch p wX wY
lp then Bool
b else Bool
c) )

-- | Force all patches labelled with one of the given labels to be 'InLast',
-- pulling any dependencies with them. This even forces any patches
-- that were previously tagged 'InFirst'.
forceLasts :: Commute p
           => [Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLasts :: [Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLasts [Label]
ps = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingLast ((Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Label]
ps) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label)

-- | Force a single patch labelled with the given label to be 'InLast',
-- pulling any dependencies with them, regardless of their previous status.
forceLast :: Commute p
          => Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLast :: Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLast Label
p = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingLast ((Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
p) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label)

-- | Force a patch with the given 'Label' to be 'InMiddle',
-- pulling any dependencies with it, regardless of their previous status.
forceMiddle :: Commute p => Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceMiddle :: Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceMiddle Label
t (PCs FL (LabelledPatch p) wA wM
f FL (PatchChoice p) wM wB
l) = (forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wA
-> FL (LabelledPatch p) wA wM
-> FL (PatchChoice p) wM wB
-> PatchChoices p wA wB
forall (p :: * -> * -> *) wA wB wM1 wM2.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> Bool
-> RL (LabelledPatch p) wA wM1
-> FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wB
-> PatchChoices p wA wB
forceMatchingMiddleOrLast ((Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
t) (Label -> Bool)
-> (LabelledPatch p wX wY -> Label)
-> LabelledPatch p wX wY
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LabelledPatch p wX wY -> Label
forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label) Bool
False RL (LabelledPatch p) wA wA
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (LabelledPatch p) wA wM
f FL (PatchChoice p) wM wB
l

-- | Turn 'InFirst' patches into 'InMiddle' ones and 'InMiddle' into 'InLast' ones.
makeEverythingLater :: PatchChoices p wX wY -> PatchChoices p wX wY
makeEverythingLater :: PatchChoices p wX wY -> PatchChoices p wX wY
makeEverythingLater (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
ml) =
  let m :: FL (PatchChoice p) wX wM
m = (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wX wM -> FL (PatchChoice p) wX wM
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (Bool -> LabelledPatch p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
False) FL (LabelledPatch p) wX wM
f
      ml' :: FL (PatchChoice p) wM wY
ml' = (forall wW wY. PatchChoice p wW wY -> PatchChoice p wW wY)
-> FL (PatchChoice p) wM wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (\(PC lp _) -> LabelledPatch p wW wY -> Bool -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
True) FL (PatchChoice p) wM wY
ml
  in FL (LabelledPatch p) wX wX
-> FL (PatchChoice p) wX wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs FL (LabelledPatch p) wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL (FL (PatchChoice p) wX wY -> PatchChoices p wX wY)
-> FL (PatchChoice p) wX wY -> PatchChoices p wX wY
forall a b. (a -> b) -> a -> b
$ FL (PatchChoice p) wX wM
m FL (PatchChoice p) wX wM
-> FL (PatchChoice p) wM wY -> FL (PatchChoice p) wX wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PatchChoice p) wM wY
ml'

-- | Turn 'InMiddle' patches into 'InFirst' and 'InLast' patches into 'InMiddle'.
-- Does *not* pull dependencies into 'InFirst', instead patches that
-- cannot be commuted past 'InLast' patches stay 'InMiddle'.
makeEverythingSooner :: forall p wX wY. Commute p
                     => PatchChoices p wX wY -> PatchChoices p wX wY
makeEverythingSooner :: PatchChoices p wX wY -> PatchChoices p wX wY
makeEverythingSooner (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
ml) =
  case RL (LabelledPatch p) wM wM
-> RL (LabelledPatch p) wM wM
-> FL (PatchChoice p) wM wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM wY
forall wM1 wM2 wM3.
RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
mes RL (LabelledPatch p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL (LabelledPatch p) wM wM
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (PatchChoice p) wM wY
ml
       of (FL (LabelledPatch p) wM wZ
m :> FL (PatchChoice p) wZ wY
ml') ->
            FL (LabelledPatch p) wX wZ
-> FL (PatchChoice p) wZ wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wM
f FL (LabelledPatch p) wX wM
-> FL (LabelledPatch p) wM wZ -> FL (LabelledPatch p) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wM wZ
m) FL (PatchChoice p) wZ wY
ml'
    where
      mes :: forall wM1 wM2 wM3 .
            RL (LabelledPatch p) wM1 wM2 ->
            RL (LabelledPatch p) wM2 wM3 ->
            FL (PatchChoice p) wM3 wY ->
            (FL (LabelledPatch p) :> FL (PatchChoice p)) wM1 wY
      mes :: RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
mes RL (LabelledPatch p) wM1 wM2
middle RL (LabelledPatch p) wM2 wM3
bubble (PC LabelledPatch p wM3 wY
lp Bool
True :>: FL (PatchChoice p) wY wY
mls) = RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wY
-> FL (PatchChoice p) wY wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
forall wM1 wM2 wM3.
RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
mes RL (LabelledPatch p) wM1 wM2
middle (RL (LabelledPatch p) wM2 wM3
bubble RL (LabelledPatch p) wM2 wM3
-> LabelledPatch p wM3 wY -> RL (LabelledPatch p) wM2 wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM3 wY
lp) FL (PatchChoice p) wY wY
mls
      mes RL (LabelledPatch p) wM1 wM2
middle RL (LabelledPatch p) wM2 wM3
bubble (PC LabelledPatch p wM3 wY
lp Bool
False :>: FL (PatchChoice p) wY wY
mls) =
        case (:>) (RL (LabelledPatch p)) (LabelledPatch p) wM2 wY
-> Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wM2 wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wM2 wM3
bubble RL (LabelledPatch p) wM2 wM3
-> LabelledPatch p wM3 wY
-> (:>) (RL (LabelledPatch p)) (LabelledPatch p) wM2 wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wM3 wY
lp) of
          Maybe ((:>) (LabelledPatch p) (RL (LabelledPatch p)) wM2 wY)
Nothing -> RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wY
-> FL (PatchChoice p) wY wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
forall wM1 wM2 wM3.
RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
mes RL (LabelledPatch p) wM1 wM2
middle (RL (LabelledPatch p) wM2 wM3
bubble RL (LabelledPatch p) wM2 wM3
-> LabelledPatch p wM3 wY -> RL (LabelledPatch p) wM2 wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM3 wY
lp) FL (PatchChoice p) wY wY
mls
          Just (LabelledPatch p wM2 wZ
lp' :> RL (LabelledPatch p) wZ wY
bubble') -> RL (LabelledPatch p) wM1 wZ
-> RL (LabelledPatch p) wZ wY
-> FL (PatchChoice p) wY wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
forall wM1 wM2 wM3.
RL (LabelledPatch p) wM1 wM2
-> RL (LabelledPatch p) wM2 wM3
-> FL (PatchChoice p) wM3 wY
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wY
mes (RL (LabelledPatch p) wM1 wM2
middle RL (LabelledPatch p) wM1 wM2
-> LabelledPatch p wM2 wZ -> RL (LabelledPatch p) wM1 wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: LabelledPatch p wM2 wZ
lp') RL (LabelledPatch p) wZ wY
bubble' FL (PatchChoice p) wY wY
mls
      mes RL (LabelledPatch p) wM1 wM2
middle RL (LabelledPatch p) wM2 wM3
bubble FL (PatchChoice p) wM3 wY
NilFL =
        (RL (LabelledPatch p) wM1 wM2 -> FL (LabelledPatch p) wM1 wM2
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wM1 wM2
middle) FL (LabelledPatch p) wM1 wM2
-> FL (PatchChoice p) wM2 wM3
-> (:>) (FL (LabelledPatch p)) (FL (PatchChoice p)) wM1 wM3
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wM2 wM3 -> FL (PatchChoice p) wM2 wM3
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (\LabelledPatch p wW wY
lp -> LabelledPatch p wW wY -> Bool -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
False) (RL (LabelledPatch p) wM2 wM3 -> FL (LabelledPatch p) wM2 wM3
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wM2 wM3
bubble)

-- | Substitute a single 'LabelledPatch' with an equivalent list of patches,
-- preserving its status as 'InFirst', 'InMiddle' or 'InLast').
-- The patch is looked up using equality of 'Label's.
substitute :: forall p wX wY .
              Sealed2 (LabelledPatch p :||: FL (LabelledPatch p))
           -> PatchChoices p wX wY
           -> PatchChoices p wX wY
substitute :: Sealed2 (LabelledPatch p :||: FL (LabelledPatch p))
-> PatchChoices p wX wY -> PatchChoices p wX wY
substitute (Sealed2 (LabelledPatch p wX wY
lp :||: FL (LabelledPatch p) wX wY
new_lps)) (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
l) =
  FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
forall (p :: * -> * -> *) wX wM wY.
FL (LabelledPatch p) wX wM
-> FL (PatchChoice p) wM wY -> PatchChoices p wX wY
PCs (FL (FL (LabelledPatch p)) wX wM -> FL (LabelledPatch p) wX wM
forall (a :: * -> * -> *) wX wZ. FL (FL a) wX wZ -> FL a wX wZ
concatFL (FL (FL (LabelledPatch p)) wX wM -> FL (LabelledPatch p) wX wM)
-> FL (FL (LabelledPatch p)) wX wM -> FL (LabelledPatch p) wX wM
forall a b. (a -> b) -> a -> b
$ (forall wW wY. LabelledPatch p wW wY -> FL (LabelledPatch p) wW wY)
-> FL (LabelledPatch p) wX wM -> FL (FL (LabelledPatch p)) wX wM
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. LabelledPatch p wW wY -> FL (LabelledPatch p) wW wY
substLp FL (LabelledPatch p) wX wM
f) (FL (FL (PatchChoice p)) wM wY -> FL (PatchChoice p) wM wY
forall (a :: * -> * -> *) wX wZ. FL (FL a) wX wZ -> FL a wX wZ
concatFL (FL (FL (PatchChoice p)) wM wY -> FL (PatchChoice p) wM wY)
-> FL (FL (PatchChoice p)) wM wY -> FL (PatchChoice p) wM wY
forall a b. (a -> b) -> a -> b
$ (forall wW wY. PatchChoice p wW wY -> FL (PatchChoice p) wW wY)
-> FL (PatchChoice p) wM wY -> FL (FL (PatchChoice p)) wM wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall wW wY. PatchChoice p wW wY -> FL (PatchChoice p) wW wY
substPc FL (PatchChoice p) wM wY
l)
   where
     substLp :: LabelledPatch p wA wB -> FL (LabelledPatch p) wA wB
     substLp :: LabelledPatch p wA wB -> FL (LabelledPatch p) wA wB
substLp LabelledPatch p wA wB
lp'
       | EqCheck (wX, wY) (wA, wB)
IsEq <- LabelledPatch p wX wY
-> LabelledPatch p wA wB -> EqCheck (wX, wY) (wA, wB)
forall (p :: * -> * -> *) wA wB wC wD.
LabelledPatch p wA wB
-> LabelledPatch p wC wD -> EqCheck (wA, wB) (wC, wD)
compareLabels LabelledPatch p wX wY
lp LabelledPatch p wA wB
lp' = FL (LabelledPatch p) wX wY
FL (LabelledPatch p) wA wB
new_lps
       | Bool
otherwise = LabelledPatch p wA wB
lp' LabelledPatch p wA wB
-> FL (LabelledPatch p) wB wB -> FL (LabelledPatch p) wA wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wB wB
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
     substPc :: PatchChoice p wA wB -> FL (PatchChoice p) wA wB
     substPc :: PatchChoice p wA wB -> FL (PatchChoice p) wA wB
substPc (PC LabelledPatch p wA wB
lp' Bool
c)
       | EqCheck (wX, wY) (wA, wB)
IsEq <- LabelledPatch p wX wY
-> LabelledPatch p wA wB -> EqCheck (wX, wY) (wA, wB)
forall (p :: * -> * -> *) wA wB wC wD.
LabelledPatch p wA wB
-> LabelledPatch p wC wD -> EqCheck (wA, wB) (wC, wD)
compareLabels LabelledPatch p wX wY
lp LabelledPatch p wA wB
lp' = (forall wW wY. LabelledPatch p wW wY -> PatchChoice p wW wY)
-> FL (LabelledPatch p) wX wY -> FL (PatchChoice p) wX wY
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (Bool -> LabelledPatch p wW wY -> PatchChoice p wW wY
forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
c) FL (LabelledPatch p) wX wY
new_lps
       | Bool
otherwise = LabelledPatch p wA wB -> Bool -> PatchChoice p wA wB
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wA wB
lp' Bool
c PatchChoice p wA wB
-> FL (PatchChoice p) wB wB -> FL (PatchChoice p) wA wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PatchChoice p) wB wB
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL