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 :: 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

{-
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 :: 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'