module Darcs.Patch.Choices
(
PatchChoices
, Slot(..)
, patchChoices
, mkPatchChoices
, patchSlot
, getChoices
, separateFirstMiddleFromLast
, separateFirstFromMiddleLast
, forceMatchingFirst
, forceFirsts
, forceFirst
, forceMatchingLast
, forceLasts
, forceLast
, forceMiddle
, makeEverythingSooner
, makeEverythingLater
, selectAllMiddles
, refineChoices
, substitute
, 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 )
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
data LabelledPatch p wX wY = LP Label (p wX wY)
data PatchChoice p wX wY = PC
{ forall (p :: * -> * -> *) wX wY.
PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch :: (LabelledPatch p wX wY)
, forall (p :: * -> * -> *) wX wY. PatchChoice p wX wY -> Bool
_pcIsLast :: Bool
}
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
data PatchChoices p wX wY where
PCs :: { ()
pcsFirsts :: FL (LabelledPatch p) wX wM
, ()
pcsMiddleLasts :: FL (PatchChoice p) wM wY}
-> PatchChoices p wX wY
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
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
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
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
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)
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
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'
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'
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)
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
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
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
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)
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)
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)
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
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 (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) )
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)
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)
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
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'
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 :: 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