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 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 )
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
data LabelledPatch p wX wY = LP Label (p wX wY)
data PatchChoice p wX wY = PC
{ PatchChoice p wX wY -> LabelledPatch p wX wY
pcPatch :: (LabelledPatch p wX wY)
, PatchChoice p wX wY -> Bool
_pcIsLast :: Bool
}
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
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 :: 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
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
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
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
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
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
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'
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'
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)
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
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
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
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)
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)
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)
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
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)
-> 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) )
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)
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)
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
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'
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 :: 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