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
_) = forall (a :: * -> *) wY. a wY -> 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)
= forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (fixup wX wZ
fixup forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX 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 PushFixupFn fixup item (FL item) (FL fixup)
pushOne (fixup wX wZ
fixup 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 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 wZ wY
fixups' 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' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wZ wZ
items2') 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 wZ wY
items forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX 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 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 wY wZ
fixups2 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 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 wY
fixup1 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'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (FL fixup wZ wZ
fixups1' 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)
= 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 (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 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 PushFixupFn fixup item (FL item) (Maybe2 fixup)
pushOne (fixup wX wZ
fixup 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' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wY wY
items2 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
FL item wX wZ
items1' :> Just2 fixup wZ wY
fixup' ->
case 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 wZ wY
fixup' 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' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL item wZ wZ
items2' 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
= forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (FL fixup)
-> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL (forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (FL fixup) wX wY -> (:>) (FL item) (FL fixup) wX wY
mkList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) 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
= forall (fixup :: * -> * -> *) (item :: * -> * -> *).
PushFixupFn fixup item (FL item) (Maybe2 fixup)
-> PushFixupFn fixup (FL item) (FL item) (Maybe2 fixup)
pushFixupFLMB_FLFLMB (forall (item :: * -> * -> *) (fixup :: * -> * -> *) wX wY.
(:>) item (Maybe2 fixup) wX wY
-> (:>) (FL item) (Maybe2 fixup) wX wY
mkList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) 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 wZ wY
item forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX 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 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 wY wZ
fixups 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 PushFixupFn fixup item item (Maybe2 fixup)
pushOne (fixup wX wY
fixup 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'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL fixup wZ wY
fixups2'
item wX wZ
item'' :> Just2 fixup wZ wZ
fixup1' -> item wX wZ
item'' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> fixup wZ wZ
fixup1' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL fixup wZ wY
fixups2'