-- 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 Prelude ()
import Darcs.Prelude

import Darcs.Patch.Merge ( Merge, merge )
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 ( Eq2(..), 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 tg :: Label
tg _) = Label
tg

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

unLabel :: LabelledPatch p wX wY -> p wX wY
unLabel :: LabelledPatch p wX wY -> p wX wY
unLabel (LP _ p :: 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 l1 :: Label
l1 _) (LP l2 :: Label
l2 _) = 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 Eq2 p => Eq2 (LabelledPatch p) where
  unsafeCompare :: LabelledPatch p wA wB -> LabelledPatch p wC wD -> Bool
unsafeCompare (LP l1 :: Label
l1 p1 :: p wA wB
p1) (LP l2 :: Label
l2 p2 :: p wC wD
p2) = Label
l1 Label -> Label -> Bool
forall a. Eq a => a -> a -> Bool
== Label
l2 Bool -> Bool -> Bool
&& p wA wB -> p wC wD -> Bool
forall (p :: * -> * -> *) wA wB wC wD.
Eq2 p =>
p wA wB -> p wC wD -> Bool
unsafeCompare p wA wB
p1 p wC wD
p2

instance Invert p => Invert (LabelledPatch p) where
  invert :: LabelledPatch p wX wY -> LabelledPatch p wY wX
invert (LP t :: Label
t p :: 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 l1 :: Label
l1 p1 :: p wX wZ
p1 :> LP l2 :: Label
l2 p2 :: p wZ wY
p2) = do
    p2' :: p wX wZ
p2' :> p1' :: 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 -> [FilePath]
listTouchedFiles = p wX wY -> [FilePath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [FilePath]
listTouchedFiles (p wX wY -> [FilePath])
-> (LabelledPatch p wX wY -> p wX wY)
-> LabelledPatch p wX wY
-> [FilePath]
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 f :: 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 Merge p => Merge (LabelledPatch p) where
  merge :: (:\/:) (LabelledPatch p) (LabelledPatch p) wX wY
-> (:/\:) (LabelledPatch p) (LabelledPatch p) wX wY
merge (LP l1 :: Label
l1 p1 :: p wZ wX
p1 :\/: LP l2 :: Label
l2 p2 :: p wZ wY
p2) =
    case (:\/:) p p wX wY -> (:/\:) p p wX wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge (p wZ wX
p1 p wZ wX -> p wZ wY -> (:\/:) p p wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: p wZ wY
p2) of
      p2' :: p wX wZ
p2' :/\: p1' :: p wY wZ
p1' -> 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 wY wZ
-> (:/\:) (LabelledPatch p) (LabelledPatch p) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: Label -> p wY wZ -> LabelledPatch p wY wZ
forall (p :: * -> * -> *) wX wY.
Label -> p wX wY -> LabelledPatch p wX wY
LP Label
l1 p wY wZ
p1'

instance Commute p => Commute (PatchChoice p) where
  commute :: (:>) (PatchChoice p) (PatchChoice p) wX wY
-> Maybe ((:>) (PatchChoice p) (PatchChoice p) wX wY)
commute (PC p1 :: LabelledPatch p wX wZ
p1 c1 :: Bool
c1 :> PC p2 :: LabelledPatch p wZ wY
p2 c2 :: Bool
c2) = do
    p2' :: LabelledPatch p wX wZ
p2' :> p1' :: 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 -> [FilePath]
listTouchedFiles = LabelledPatch p wX wY -> [FilePath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [FilePath]
listTouchedFiles (LabelledPatch p wX wY -> [FilePath])
-> (PatchChoice p wX wY -> LabelledPatch p wX wY)
-> PatchChoice p wX wY
-> [FilePath]
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 f :: 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

instance Merge p => Merge (PatchChoice p) where
  merge :: (:\/:) (PatchChoice p) (PatchChoice p) wX wY
-> (:/\:) (PatchChoice p) (PatchChoice p) wX wY
merge (PC lp1 :: LabelledPatch p wZ wX
lp1 c1 :: Bool
c1 :\/: PC lp2 :: LabelledPatch p wZ wY
lp2 c2 :: Bool
c2) = case (:\/:) (LabelledPatch p) (LabelledPatch p) wX wY
-> (:/\:) (LabelledPatch p) (LabelledPatch p) wX wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
merge (LabelledPatch p wZ wX
lp1 LabelledPatch p wZ wX
-> LabelledPatch p wZ wY
-> (:\/:) (LabelledPatch p) (LabelledPatch p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: LabelledPatch p wZ wY
lp2) of
    lp2' :: LabelledPatch p wX wZ
lp2' :/\: lp1' :: LabelledPatch p wY wZ
lp1' -> 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
lp2' Bool
c2 PatchChoice p wX wZ
-> PatchChoice p wY wZ
-> (:/\:) (PatchChoice p) (PatchChoice p) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: LabelledPatch p wY wZ -> Bool -> PatchChoice p wY wZ
forall (p :: * -> * -> *) wX wY.
LabelledPatch p wX wY -> Bool -> PatchChoice p wX wY
PC LabelledPatch p wY wZ
lp1' Bool
c1

-- | 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 tg :: Maybe Label
tg ps :: 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) [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)

instance Eq2 p => Eq2 (PatchChoice p) where
  unsafeCompare :: PatchChoice p wA wB -> PatchChoice p wC wD -> Bool
unsafeCompare (PC lp1 :: LabelledPatch p wA wB
lp1 _) (PC lp2 :: LabelledPatch p wC wD
lp2 _) = LabelledPatch p wA wB -> LabelledPatch p wC wD -> Bool
forall (p :: * -> * -> *) wA wB wC wD.
Eq2 p =>
p wA wB -> p wC wD -> Bool
unsafeCompare LabelledPatch p wA wB
lp1 LabelledPatch p wC wD
lp2


-- | 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 f :: FL (LabelledPatch p) wX wM
f ml :: 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 f :: FL (LabelledPatch p) wX wM
f l :: 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
    (m :: FL (LabelledPatch p) wM wZ
m :> l' :: 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 f :: FL (LabelledPatch p) wX wM
f ml :: 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
    (m :: FL (LabelledPatch p) wM wZ
m :> l' :: 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 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 lp :: LabelledPatch p wX wY
lp False :>: pcs :: 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
       (m :: FL (LabelledPatch p) wY wZ
m :> l :: 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 lp :: LabelledPatch p wX wY
lp True :>: pcs :: 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
    (m :: FL (LabelledPatch p) wY wZ
m :> l :: 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
        (m' :: FL (LabelledPatch p) wX wZ
m' :> lp' :: LabelledPatch p wZ wZ
lp' :> deps :: 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 act :: forall wU wV.
FL (LabelledPatch p) wU wV
-> PatchChoices p wU wV -> m (PatchChoices p wU wV)
act ps :: 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
    (f :: FL (LabelledPatch p) wX wZ
f :> m :: FL (LabelledPatch p) wZ wZ
m :> l :: FL (LabelledPatch p) wZ wY
l) -> do
      (PCs f' :: FL (LabelledPatch p) wZ wM
f' l' :: 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 t :: Label
t _) pc :: PatchChoices p wX wY
pc@(PCs f :: FL (LabelledPatch p) wX wM
f ml :: 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 firsts :: FL (LabelledPatch p) wX wM
firsts middles :: RL (LabelledPatch p) wM wC
middles bubble :: RL (LabelledPatch p) wC wL
bubble (PC lp :: LabelledPatch p wL wY
lp True :>: ls :: 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
                      , $WPCs :: 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 firsts :: FL (LabelledPatch p) wX wM
firsts middles :: RL (LabelledPatch p) wM wC
middles bubble :: RL (LabelledPatch p) wC wL
bubble (PC lp :: LabelledPatch p wL wY
lp False :>: ls :: 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 (lp' :: LabelledPatch p wC wZ
lp' :> bubble' :: RL (LabelledPatch p) wZ wY
bubble') -> (Slot
InMiddle,
                                 $WPCs :: 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})
        Nothing -> (Slot
InLast,
                   $WPCs :: 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 firsts :: FL (LabelledPatch p) wX wM
firsts middles :: RL (LabelledPatch p) wM wC
middles bubble :: RL (LabelledPatch p) wC wL
bubble (PC lp :: LabelledPatch p wL wY
lp True :>: ls :: 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 firsts :: FL (LabelledPatch p) wX wM
firsts middles :: RL (LabelledPatch p) wM wC
middles bubble :: RL (LabelledPatch p) wC wL
bubble (PC lp :: LabelledPatch p wL wY
lp False :>: ls :: 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 (lp' :: LabelledPatch p wC wZ
lp' :> bubble' :: 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
        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 _ _ _ NilFL = (Slot, PatchChoices p wX wY)
forall a. a
impossible
    settleM :: RL (LabelledPatch p) wX wZ -> FL (PatchChoice p) wX wZ
settleM middles :: 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 (\lp :: 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 bubble :: 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 (\lp :: 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 pred :: forall wX wY. LabelledPatch p wX wY -> Bool
pred (PCs f0 :: FL (LabelledPatch p) wA wM
f0 ml :: 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 f :: FL (LabelledPatch p) wA wM
f l1 :: RL (PatchChoice p) wM wN
l1 (a :: PatchChoice p wN wY
a :>: l2 :: 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
              (deps :: RL (PatchChoice p) wM wZ
deps :> a' :: PatchChoice p wZ wZ
a' :> l1' :: 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 f :: FL (LabelledPatch p) wA wM
f l1 :: RL (PatchChoice p) wM wN
l1 (a :: PatchChoice p wN wY
a :>: l2 :: 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 f :: FL (LabelledPatch p) wA wM
f l1 :: RL (PatchChoice p) wM wN
l1 NilFL = $WPCs :: 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 lp :: LabelledPatch p wX wY
lp _) = 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 ps :: [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 p :: 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 True (PCs f :: FL (LabelledPatch p) wX wM
f l :: 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 lp :: LabelledPatch p wX wY
lp _) = 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 False (PCs f :: FL (LabelledPatch p) wX wM
f l :: 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 f1 :: FL (LabelledPatch p) wX wM1
f1 f2 :: RL (LabelledPatch p) wM1 wM2
f2 l1 :: RL (PatchChoice p) wM2 wM3
l1 (pc :: PatchChoice p wM3 wY
pc@(PC lp :: LabelledPatch p wM3 wY
lp False) :>: l2 :: 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
        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 lp' :: LabelledPatch p wM2 wZ
lp' _) :> l1' :: 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 f1 :: FL (LabelledPatch p) wX wM1
f1 f2 :: RL (LabelledPatch p) wM1 wM2
f2 l1 :: RL (PatchChoice p) wM2 wM3
l1 (PC lp :: LabelledPatch p wM3 wY
lp True :>: l2 :: 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 f1 :: FL (LabelledPatch p) wX wM1
f1 f2 :: RL (LabelledPatch p) wM1 wM2
f2 l1 :: RL (PatchChoice p) wM2 wM3
l1 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 pred :: forall wX wY. LabelledPatch p wX wY -> Bool
pred (PCs f :: FL (LabelledPatch p) wA wM
f ml :: 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 pred :: forall wX wY. LabelledPatch p wX wY -> Bool
pred b :: Bool
b f1 :: RL (LabelledPatch p) wA wM1
f1 (a :: LabelledPatch p wM1 wY
a :>: f2 :: FL (LabelledPatch p) wY wM2
f2) ml :: 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
      (f2' :: FL (LabelledPatch p) wM1 wZ
f2' :> a' :: LabelledPatch p wZ wZ
a' :> deps :: 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 pred :: forall wX wY. LabelledPatch p wX wY -> Bool
pred b :: Bool
b f1 :: RL (LabelledPatch p) wA wM1
f1 (a :: LabelledPatch p wM1 wY
a :>: f2 :: FL (LabelledPatch p) wY wM2
f2) ml :: 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 pred :: forall wX wY. LabelledPatch p wX wY -> Bool
pred b :: Bool
b f1 :: RL (LabelledPatch p) wA wM1
f1 NilFL ml :: FL (PatchChoice p) wM2 wB
ml =
  $WPCs :: 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 lp :: LabelledPatch p wX wY
lp c :: 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 ps :: [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 p :: 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 t :: Label
t (PCs f :: FL (LabelledPatch p) wA wM
f l :: 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 f :: FL (LabelledPatch p) wX wM
f ml :: 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 f :: FL (LabelledPatch p) wX wM
f ml :: 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 (m :: FL (LabelledPatch p) wM wZ
m :> ml' :: 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 middle :: RL (LabelledPatch p) wM1 wM2
middle bubble :: RL (LabelledPatch p) wM2 wM3
bubble (PC lp :: LabelledPatch p wM3 wY
lp True :>: mls :: 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 middle :: RL (LabelledPatch p) wM1 wM2
middle bubble :: RL (LabelledPatch p) wM2 wM3
bubble (PC lp :: LabelledPatch p wM3 wY
lp False :>: mls :: 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
          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 (lp' :: LabelledPatch p wM2 wZ
lp' :> bubble' :: 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 middle :: RL (LabelledPatch p) wM1 wM2
middle bubble :: RL (LabelledPatch p) wM2 wM3
bubble 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 (\lp :: 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 (lp :: LabelledPatch p wX wY
lp :||: new_lps :: FL (LabelledPatch p) wX wY
new_lps)) (PCs f :: FL (LabelledPatch p) wX wM
f l :: 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 lp' :: 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 lp' :: LabelledPatch p wA wB
lp' c :: 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