-- 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
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
  { forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch :: (LabelledPatch p wX wY) -- ^ the 'LabelledPatch' in question
  , forall (p :: * -> * -> *) wX wY. 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 :: forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 :: forall (p :: * -> * -> *) wX wY. 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 :: forall (p :: * -> * -> *) wX wY. 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 :: forall (p :: * -> * -> *) wA wB wC wD.
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 forall a. Eq a => a -> a -> Bool
== Label
l2 then forall (a :: * -> * -> *) wX wY wB wC. a wX wY -> a wB wC
unsafeCoerceP forall wA. EqCheck wA wA
IsEq else forall wA wB. EqCheck wA wB
NotEq

instance Invert p => Invert (LabelledPatch p) where
  invert :: forall wX wY. LabelledPatch p wX wY -> LabelledPatch p wY wX
invert (LP Label
t p wX wY
p) = forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
t (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 :: forall wX wY.
(:>) (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' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wX wZ
p1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
p2)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
l2 p wX wZ
p2' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX 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 :: forall wX wY. LabelledPatch p wX wY -> [AnchoredPath]
listTouchedFiles = forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> p wX wY
unLabel
  hunkMatches :: forall wX wY. (ByteString -> Bool) -> LabelledPatch p wX wY -> Bool
hunkMatches ByteString -> Bool
f = forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> p wX wY
unLabel

instance Commute p => Commute (PatchChoice p) where
  commute :: forall wX wY.
(:>) (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' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (LabelledPatch p wX wZ
p1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> LabelledPatch p wZ wY
p2)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wX wZ
p2' Bool
c2 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX 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 :: forall wX wY. PatchChoice p wX wY -> [AnchoredPath]
listTouchedFiles = forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch
  hunkMatches :: forall wX wY. (ByteString -> Bool) -> PatchChoice p wX wY -> Bool
hunkMatches ByteString -> Bool
f = forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (p :: * -> * -> *) wX wY. FL p wX wY -> PatchChoices p wX wY
patchChoices = forall (p :: * -> * -> *) wX wY.
FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
labelPatches 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 :: forall (p :: * -> * -> *) wX wY.
Maybe Label -> FL p wX wY -> FL (LabelledPatch p) wX wY
labelPatches Maybe Label
tg FL p wX wY
ps = 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 (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP (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 :: forall (p :: * -> * -> *) wX wY.
FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices = forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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 :: forall (p :: * -> * -> *) wX wZ.
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 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 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 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 :: forall (p :: * -> * -> *) wX wZ.
Commute p =>
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 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 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wM wZ
m 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
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 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 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (LabelledPatch p) wM wZ
m 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
FL (PatchChoice p) wX wY
-> (:>) (FL (LabelledPatch p)) (FL (LabelledPatch p)) wX wY
pushLasts FL (PatchChoice p) wX wY
NilFL = forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
pushLasts (PC LabelledPatch p wX wY
lp Bool
False :>: FL (PatchChoice p) wY wY
pcs) =
  case 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 forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wY wZ
m) 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 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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (LabelledPatch p wX wY
lp 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' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (LabelledPatch p wZ wZ
lp' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wZ wZ
deps 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 (p :: * -> * -> *) (m :: * -> *) wX wY.
(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)
act PatchChoices p wX wY
ps =
  case 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') <- forall wU wV.
FL (LabelledPatch p) wU wV
-> PatchChoices p wU wV -> m (PatchChoices p wU wV)
act FL (LabelledPatch p) wZ wZ
m (forall (p :: * -> * -> *) wX wY.
FL (LabelledPatch p) wX wY -> PatchChoices p wX wY
mkPatchChoices FL (LabelledPatch p) wZ wZ
m)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wZ
f forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (LabelledPatch p) wZ wM
f') forall a b. (a -> b) -> a -> b
$ FL (PatchChoice p) wM wZ
l' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a 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 (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 :: forall (p :: * -> * -> *) wA wB wX wY.
Commute p =>
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)
  | 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 = 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 forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX. RL a wX wX
NilRL FL (PatchChoice p) wM wY
ml
  where
    foundIn :: FL (LabelledPatch p) wW wZ -> Bool
foundIn = forall (a :: * -> * -> *) wW wZ.
(forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool
anyFL ((forall a. Eq a => a -> a -> Bool
== Label
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: 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 (PC LabelledPatch p wL wY
lp Bool
True :>: FL (PatchChoice p) wY wY
ls)
      | forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label LabelledPatch p wL wY
lp forall a. Eq a => a -> a -> Bool
== Label
t = (Slot
InLast
                      , PCs { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                            , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                         forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wC wL
bubble
                                         forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wL wY
lp Bool
True 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)
      | forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label LabelledPatch p wL wY
lp forall a. Eq a => a -> a -> Bool
== Label
t =
        case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wC wL
bubble 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 { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                                     , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                                  forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wC wZ
lp' Bool
False
                                                  forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wZ wY
bubble'
                                                  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 { pcsFirsts :: FL (LabelledPatch p) wX wM
pcsFirsts = FL (LabelledPatch p) wX wM
firsts
                       , pcsMiddleLasts :: FL (PatchChoice p) wM wY
pcsMiddleLasts = forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM RL (LabelledPatch p) wM wC
middles
                                    forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall {p :: * -> * -> *} {wX} {wZ}.
RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleB RL (LabelledPatch p) wC wL
bubble
                                    forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wL wY
lp Bool
True
                                    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) =
      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 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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wC wL
bubble 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') -> 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 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 -> 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 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 = 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 (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 -> forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
False) forall a b. (a -> b) -> a -> b
$ 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 (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 -> forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
True) forall a b. (a -> b) -> a -> b
$ 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 (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
pred (PCs FL (LabelledPatch p) wA wM
f0 FL (PatchChoice p) wM wB
ml) = 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 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 :: 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 (PatchChoice p wN wY
a :>: FL (PatchChoice p) wY wB
l2)
          | forall wX wY. PatchChoice p wX wY -> Bool
pred_pc PatchChoice p wN wY
a =
            case 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 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 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a 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 forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PatchChoice p) wM wZ
deps) forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ (forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch PatchChoice p wZ wZ
a' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
                in 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) = 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 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 { pcsFirsts :: FL (LabelledPatch p) wA wM
pcsFirsts = FL (LabelledPatch p) wA wM
f
                                , pcsMiddleLasts :: FL (PatchChoice p) wM wN
pcsMiddleLasts = 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 :: forall wX wY. PatchChoice p wX wY -> Bool
pred_pc (PC LabelledPatch p wX wY
lp 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 :: forall (p :: * -> * -> *) wA wB.
Commute p =>
[Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirsts [Label]
ps = forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingFirst ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Label]
ps) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (p :: * -> * -> *) wA wB.
Commute p =>
Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceFirst Label
p = forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingFirst ((forall a. Eq a => a -> a -> Bool
== Label
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
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) = forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs FL (LabelledPatch p) wX wM
f (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 {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
_) = 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) = 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 forall (a :: * -> * -> *) wX. RL a wX wX
NilRL 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 :: 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 (pc :: PatchChoice p wM3 wY
pc@(PC LabelledPatch p wM3 wY
lp Bool
False) :>: FL (PatchChoice p) wY wY
l2) =
      case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (PatchChoice p) wM2 wM3
l1 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 -> 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 forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: 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') -> 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 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) = 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 forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: 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 = forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wM1
f1 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wM1 wM2
f2) (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 (p :: * -> * -> *) wA wB.
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
pred (PCs FL (LabelledPatch p) wA wM
f FL (PatchChoice p) wM wB
ml) =
  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 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 (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 (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
pred LabelledPatch p wM1 wY
a =
    case forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> (:>) (FL p) (p :> FL p) wX wY
commuteWhatWeCanFL (LabelledPatch p wM1 wY
a 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 (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (forall (p :: * -> * -> *) wX wY.
Bool -> LabelledPatch p wX wY -> PatchChoice p wX wY
pcSetLast Bool
b) (LabelledPatch p wZ wZ
a' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (LabelledPatch p) wZ wM2
deps) 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 (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 (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 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 { pcsFirsts :: FL (LabelledPatch p) wA wM1
pcsFirsts = 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 (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL forall {wX} {wY}. PatchChoice p wX wY -> PatchChoice p wX 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) = (forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wX wY
lp (if 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 :: forall (p :: * -> * -> *) wA wB.
Commute p =>
[Label] -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLasts [Label]
ps = forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingLast ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Label]
ps) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (p :: * -> * -> *) wA wB.
Commute p =>
Label -> PatchChoices p wA wB -> PatchChoices p wA wB
forceLast Label
p = forall (p :: * -> * -> *) wA wB.
Commute p =>
(forall wX wY. LabelledPatch p wX wY -> Bool)
-> PatchChoices p wA wB -> PatchChoices p wA wB
forceMatchingLast ((forall a. Eq a => a -> a -> Bool
== Label
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (p :: * -> * -> *) wA wB.
Commute p =>
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 (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 a. Eq a => a -> a -> Bool
== Label
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY. LabelledPatch p wX wY -> Label
label) Bool
False 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 :: forall (p :: * -> * -> *) wX wY.
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 (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (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 (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (\(PC LabelledPatch p wW wY
lp Bool
_) -> 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 forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall a b. (a -> b) -> a -> b
$ FL (PatchChoice p) wX wM
m 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 :: forall (p :: * -> * -> *) wX wY.
Commute p =>
PatchChoices p wX wY -> PatchChoices p wX wY
makeEverythingSooner (PCs FL (LabelledPatch p) wX wM
f FL (PatchChoice p) wM wY
ml) =
  case 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 forall (a :: * -> * -> *) wX. RL a wX wX
NilRL 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') ->
            forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs (FL (LabelledPatch p) wX wM
f 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 :: 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 (PC LabelledPatch p wM3 wY
lp Bool
True :>: FL (PatchChoice p) wY wY
mls) = 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 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 forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL (LabelledPatch p) wM2 wM3
bubble 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 -> 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 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') -> 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 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 =
        (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (LabelledPatch p) wM1 wM2
middle) forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 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 (\LabelledPatch p wW wY
lp -> forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wW wY
lp Bool
False) (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 :: forall (p :: * -> * -> *) wX wY.
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) =
  forall (p :: * -> * -> *) wX wY wY.
FL (LabelledPatch p) wX wY
-> FL (PatchChoice p) wY wY -> PatchChoices p wX wY
PCs (forall (a :: * -> * -> *) wX wZ. FL (FL a) wX wZ -> FL a wX wZ
concatFL forall a b. (a -> b) -> a -> b
$ 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 wA wB. LabelledPatch p wA wB -> FL (LabelledPatch p) wA wB
substLp FL (LabelledPatch p) wX wM
f) (forall (a :: * -> * -> *) wX wZ. FL (FL a) wX wZ -> FL a wX wZ
concatFL forall a b. (a -> b) -> a -> b
$ 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 wA wB. PatchChoice p wA wB -> FL (PatchChoice p) wA wB
substPc FL (PatchChoice p) wM wY
l)
   where
     substLp :: LabelledPatch p wA wB -> FL (LabelledPatch p) wA wB
     substLp :: forall wA wB. LabelledPatch p wA wB -> FL (LabelledPatch p) wA wB
substLp LabelledPatch p wA wB
lp'
       | EqCheck (wX, wY) (wA, wB)
IsEq <- 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
new_lps
       | Bool
otherwise = LabelledPatch p wA wB
lp' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
     substPc :: PatchChoice p wA wB -> FL (PatchChoice p) wA wB
     substPc :: forall wA wB. PatchChoice p wA wB -> FL (PatchChoice p) wA wB
substPc (PC LabelledPatch p wA wB
lp' Bool
c)
       | EqCheck (wX, wY) (wA, wB)
IsEq <- 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 (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL (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 = forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wA wB
lp' Bool
c forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL