module Darcs.Patch.Rebase.PushFixup
( PushFixupFn, dropFixups
, pushFixupFLFL_FLFLFL
, pushFixupFLFL_FLFLFLFL
, pushFixupFLMB_FLFLMB
, pushFixupIdFL_FLFLFL
, pushFixupIdMB_FLFLMB
, pushFixupIdMB_FLIdFLFL
) where
import Darcs.Prelude
import Darcs.Patch.Witnesses.Maybe ( Maybe2(..) )
import Darcs.Patch.Witnesses.Ordered
( (:>)(..), FL(..), (+>+)
)
import Darcs.Patch.Witnesses.Sealed ( Sealed(..) )
type PushFixupFn fixupIn itemIn itemOut fixupOut
= forall wX wY
. (fixupIn :> itemIn ) wX wY
-> (itemOut :> fixupOut) wX wY
dropFixups :: (item :> fixup) wX wY -> Sealed (item wX)
dropFixups :: forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item fixup wX wY -> Sealed (item wX)
dropFixups (item wX wZ
item :> fixup wZ wY
_) = item wX wZ -> Sealed (item wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed item wX wZ
item
pushFixupFLFL_FLFLFL
:: PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL PushFixupFn fixup item (FL item) (FL fixup)
_pushOne (fixup wX wZ
fixup :> FL item wZ wY
NilFL)
= FL item wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL item wX wX -> FL fixup wX wY -> (:>) (FL item) (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (fixup wX wZ
fixup fixup wX wZ -> FL fixup wZ wY -> FL fixup wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL fixup wZ wY
FL fixup wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
pushFixupFLFL_FLFLFL PushFixupFn fixup item (FL item) (FL fixup)
pushOne (fixup wX wZ
fixup :> (item wZ wY
item1 :>: FL item wY wY
items2))
= case (:>) fixup item wX wY -> (:>) (FL item) (FL fixup) wX wY
PushFixupFn fixup item (FL item) (FL fixup)
pushOne (fixup wX wZ
fixup fixup wX wZ -> item wZ wY -> (:>) fixup item wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> item wZ wY
item1) of
FL item wX wZ
items1' :> FL fixup wZ wY
fixups' ->
case PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFLFL (:>) fixup item wX wY -> (:>) (FL item) (FL fixup) wX wY
PushFixupFn fixup item (FL item) (FL fixup)
pushOne (FL fixup wZ wY
fixups' FL fixup wZ wY -> FL item wY wY -> (:>) (FL fixup) (FL item) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL item wY wY
items2) of
FL item wZ wZ
items2' :> FL fixup wZ wY
fixups'' -> (FL item wX wZ
items1' FL item wX wZ -> FL item wZ wZ -> FL item wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wZ wZ
items2') FL item wX wZ -> FL fixup wZ wY -> (:>) (FL item) (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wZ wY
fixups''
pushFixupFLFL_FLFLFLFL
:: PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFLFL :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFLFL PushFixupFn fixup item (FL item) (FL fixup)
_pushOne (FL fixup wX wZ
NilFL :> FL item wZ wY
items)
= FL item wX wY
FL item wZ wY
items FL item wX wY -> FL fixup wY wY -> (:>) (FL item) (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
pushFixupFLFL_FLFLFLFL PushFixupFn fixup item (FL item) (FL fixup)
pushOne ((fixup wX wY
fixup1 :>: FL fixup wY wZ
fixups2) :> FL item wZ wY
items)
= case PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn (FL fixup) (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFLFL (:>) fixup item wX wY -> (:>) (FL item) (FL fixup) wX wY
PushFixupFn fixup item (FL item) (FL fixup)
pushOne (FL fixup wY wZ
fixups2 FL fixup wY wZ -> FL item wZ wY -> (:>) (FL fixup) (FL item) wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL item wZ wY
items) of
FL item wY wZ
items' :> FL fixup wZ wY
fixups2' ->
case PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL (:>) fixup item wX wY -> (:>) (FL item) (FL fixup) wX wY
PushFixupFn fixup item (FL item) (FL fixup)
pushOne (fixup wX wY
fixup1 fixup wX wY -> FL item wY wZ -> (:>) fixup (FL item) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL item wY wZ
items') of
FL item wX wZ
items'' :> FL fixup wZ wZ
fixups1' -> FL item wX wZ
items'' FL item wX wZ -> FL fixup wZ wY -> (:>) (FL item) (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL fixup wZ wZ
fixups1' FL fixup wZ wZ -> FL fixup wZ wY -> FL fixup wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL fixup wZ wY
fixups2')
pushFixupFLMB_FLFLMB
:: PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupFLMB_FLFLMB :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupFLMB_FLFLMB PushFixupFn fixup item (FL item) (Maybe2 fixup)
_pushOne (fixup wX wZ
fixup :> FL item wZ wY
NilFL)
= FL item wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL item wX wX
-> Maybe2 fixup wX wY -> (:>) (FL item) (Maybe2 fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> fixup wX wY -> Maybe2 fixup wX wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 fixup wX wY
fixup wX wZ
fixup
pushFixupFLMB_FLFLMB PushFixupFn fixup item (FL item) (Maybe2 fixup)
pushOne (fixup wX wZ
fixup :> (item wZ wY
item1 :>: FL item wY wY
items2))
= case (:>) fixup item wX wY -> (:>) (FL item) (Maybe2 fixup) wX wY
PushFixupFn fixup item (FL item) (Maybe2 fixup)
pushOne (fixup wX wZ
fixup fixup wX wZ -> item wZ wY -> (:>) fixup item wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> item wZ wY
item1) of
FL item wX wZ
items1' :> Maybe2 fixup wZ wY
Nothing2 -> FL item wX wZ
items1' FL item wX wZ -> FL item wZ wY -> FL item wX wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wY wY
FL item wZ wY
items2 FL item wX wY
-> Maybe2 fixup wY wY -> (:>) (FL item) (Maybe2 fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 fixup wY wY
forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
FL item wX wZ
items1' :> Just2 fixup wZ wY
fixup' ->
case PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupFLMB_FLFLMB (:>) fixup item wX wY -> (:>) (FL item) (Maybe2 fixup) wX wY
PushFixupFn fixup item (FL item) (Maybe2 fixup)
pushOne (fixup wZ wY
fixup' fixup wZ wY -> FL item wY wY -> (:>) fixup (FL item) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL item wY wY
items2) of
FL item wZ wZ
items2' :> Maybe2 fixup wZ wY
fixup'' -> FL item wX wZ
items1' FL item wX wZ -> FL item wZ wZ -> FL item wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wZ wZ
items2' FL item wX wZ
-> Maybe2 fixup wZ wY -> (:>) (FL item) (Maybe2 fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 fixup wZ wY
fixup''
pushFixupIdFL_FLFLFL
:: PushFixupFn fixup item item (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupIdFL_FLFLFL :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item item (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupIdFL_FLFLFL PushFixupFn fixup item item (FL fixup)
pushOne
= PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL ((:>) item (FL fixup) wX wY -> (:>) (FL item) (FL fixup) wX wY
forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (FL fixup) wX wY -> (:>) (FL item) (FL fixup) wX wY
mkList ((:>) item (FL fixup) wX wY -> (:>) (FL item) (FL fixup) wX wY)
-> ((:>) fixup item wX wY -> (:>) item (FL fixup) wX wY)
-> (:>) fixup item wX wY
-> (:>) (FL item) (FL fixup) wX wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:>) fixup item wX wY -> (:>) item (FL fixup) wX wY
PushFixupFn fixup item item (FL fixup)
pushOne)
where
mkList :: (item :> FL fixup) wX wY -> (FL item :> FL fixup) wX wY
mkList :: forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (FL fixup) wX wY -> (:>) (FL item) (FL fixup) wX wY
mkList (item wX wZ
item :> FL fixup wZ wY
fixups) = (item wX wZ
item item wX wZ -> FL item wZ wZ -> FL item wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL item wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL item wX wZ -> FL fixup wZ wY -> (:>) (FL item) (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wZ wY
fixups
pushFixupIdMB_FLFLMB
:: PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupIdMB_FLFLMB :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupIdMB_FLFLMB PushFixupFn fixup item item (Maybe2 fixup)
pushOne
= PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupFLMB_FLFLMB ((:>) item (Maybe2 fixup) wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY
forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (Maybe2 fixup) wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY
mkList ((:>) item (Maybe2 fixup) wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY)
-> ((:>) fixup item wX wY -> (:>) item (Maybe2 fixup) wX wY)
-> (:>) fixup item wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:>) fixup item wX wY -> (:>) item (Maybe2 fixup) wX wY
PushFixupFn fixup item item (Maybe2 fixup)
pushOne)
where
mkList :: (item :> Maybe2 fixup) wX wY -> (FL item :> Maybe2 fixup) wX wY
mkList :: forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (Maybe2 fixup) wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY
mkList (item wX wZ
item :> Maybe2 fixup wZ wY
fixups) = (item wX wZ
item item wX wZ -> FL item wZ wZ -> FL item wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL item wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL item wX wZ
-> Maybe2 fixup wZ wY -> (:>) (FL item) (Maybe2 fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 fixup wZ wY
fixups
pushFixupIdMB_FLIdFLFL
:: PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn (FL fixup) item item (FL fixup)
pushFixupIdMB_FLIdFLFL :: forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn (FL fixup) item item (FL fixup)
pushFixupIdMB_FLIdFLFL PushFixupFn fixup item item (Maybe2 fixup)
_pushOne (FL fixup wX wZ
NilFL :> item wZ wY
item)
= item wX wY
item wZ wY
item item wX wY -> FL fixup wY wY -> (:>) item (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
pushFixupIdMB_FLIdFLFL PushFixupFn fixup item item (Maybe2 fixup)
pushOne ((fixup wX wY
fixup :>: FL fixup wY wZ
fixups) :> item wZ wY
item)
= case PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn (FL fixup) item item (FL fixup)
forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item item (Maybe2 fixup)
-> PushFixupFn (FL fixup) item item (FL fixup)
pushFixupIdMB_FLIdFLFL (:>) fixup item wX wY -> (:>) item (Maybe2 fixup) wX wY
PushFixupFn fixup item item (Maybe2 fixup)
pushOne (FL fixup wY wZ
fixups FL fixup wY wZ -> item wZ wY -> (:>) (FL fixup) item wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> item wZ wY
item) of
item wY wZ
item' :> FL fixup wZ wY
fixups2' ->
case (:>) fixup item wX wZ -> (:>) item (Maybe2 fixup) wX wZ
PushFixupFn fixup item item (Maybe2 fixup)
pushOne (fixup wX wY
fixup fixup wX wY -> item wY wZ -> (:>) fixup item wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> item wY wZ
item') of
item wX wZ
item'' :> Maybe2 fixup wZ wZ
Nothing2 -> item wX wZ
item'' item wX wZ -> FL fixup wZ wY -> (:>) item (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wZ wY
FL fixup wZ wY
fixups2'
item wX wZ
item'' :> Just2 fixup wZ wZ
fixup1' -> item wX wZ
item'' item wX wZ -> FL fixup wZ wY -> (:>) item (FL fixup) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> fixup wZ wZ
fixup1' fixup wZ wZ -> FL fixup wZ wY -> FL fixup wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL fixup wZ wY
fixups2'