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(..) )

-- | During a rebase, we use "fixup" patches to maintain the correct
-- context for the real "items" that are being stored in the rebase
-- that the user wants to keep. As the context of the rebase changes,
-- new fixups get added to the beginning that then need to be pushed
-- past as many items as possible.
--
-- There are multiple fixup types and multiple ways of representing
-- the items being stored in the rebase, so this is polymorphic in
-- both types. Also, the structure of the results varies - in some
-- cases it will be a single value, sometimes an FL, or sometimes
-- zero or one values (Maybe2), so the output types are separate
-- variables. A typical instantiation would be something like
-- PushFixupFn Fixup Item (FL Item) (FL Fixup).
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 :: (:>) 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

{-
The collection below of pushFixup combinators is quite annoying, but
there's no obvious generalisation, and inlining them at each use site
would be even worse.
-}

pushFixupFLFL_FLFLFL
  :: PushFixupFn fixup     item  (FL item) (FL fixup)
  -> PushFixupFn fixup (FL item) (FL item) (FL fixup)
pushFixupFLFL_FLFLFL :: 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 wZ -> (:>) (FL item) (FL fixup) wX wZ
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 wZ -> FL fixup wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: 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)
-> (:>) (FL fixup) (FL item) wZ wY
-> (:>) (FL item) (FL fixup) wZ wY
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' 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 :: 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 FL item wZ wY -> FL fixup wY wY -> (:>) (FL item) (FL fixup) wZ 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)
-> (:>) (FL fixup) (FL item) wY wY
-> (:>) (FL item) (FL fixup) wY wY
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 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)
-> (:>) fixup (FL item) wX wZ -> (:>) (FL item) (FL fixup) wX wZ
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 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 :: 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 wZ -> (:>) (FL item) (Maybe2 fixup) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> fixup wX wZ -> Maybe2 fixup wX wZ
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 (:>) 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)
-> (:>) fixup (FL item) wZ wY
-> (:>) (FL item) (Maybe2 fixup) wZ wY
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' 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 :: 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 :: (:>) 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 :: 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 :: (:>) 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 :: 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 item wZ wY -> FL fixup wY wY -> (:>) item (FL fixup) wZ 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)
-> (:>) (FL fixup) item wY wY -> (:>) item (FL fixup) wY wY
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 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'