--  Copyright (C) 2011-2 Ganesh Sittampalam 
--
--  BSD3

{-# LANGUAGE UndecidableInstances #-}
module Darcs.Patch.Rebase.Fixup
    ( RebaseFixup(..)
    , commuteNamedFixup, commuteFixupNamed
    , pushFixupFixup
    , flToNamesPrims, namedToFixups
    ) where

import Darcs.Prelude

import Darcs.Patch.Apply ( Apply(..) )
import Darcs.Patch.Commute ( Commute(..), selfCommuter )
import Darcs.Patch.CommuteFn ( totalCommuterIdFL )
import Darcs.Patch.Effect ( Effect(..) )
import Darcs.Patch.Inspect ( PatchInspect(..) )
import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Named ( Named(..) )
import Darcs.Patch.Format ( PatchListFormat )
import Darcs.Patch.FromPrim ( PrimPatchBase(..) )
import Darcs.Patch.Prim ( PrimPatch, canonizeFL )
import Darcs.Patch.Read ( ReadPatch(..) )
import Darcs.Patch.Rebase.Name
    ( RebaseName(..)
    , commuteNamedName, commuteNameNamed
    , commuterNamedId, commuterIdNamed
    , commutePrimName, commuteNamePrim
    , pushFixupName
    )
import Darcs.Patch.Rebase.PushFixup ( PushFixupFn )
import Darcs.Patch.Show ( ShowPatchBasic(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Maybe ( Maybe2(..), mapMB_MB )
import Darcs.Patch.Witnesses.Ordered
    ( FL(..), mapFL_FL, (:>)(..) )
import Darcs.Patch.Witnesses.Sealed ( Sealed, mapSeal )
import Darcs.Patch.Witnesses.Show ( Show1, Show2, showsPrec2, appPrec )

import qualified Darcs.Util.Diff as D ( DiffAlgorithm )
import Darcs.Util.Parser ( Parser, lexString )
import Darcs.Util.Printer ( ($$), (<+>), blueText )

import Control.Applicative ( (<|>) )
import qualified Data.ByteString as B ( ByteString )
import qualified Data.ByteString.Char8 as BC ( pack )

-- |A single rebase fixup, needed to ensure that the actual patches
-- being stored in the rebase state have the correct context.
data RebaseFixup prim wX wY where
  PrimFixup :: prim wX wY -> RebaseFixup prim wX wY
  NameFixup :: RebaseName wX wY -> RebaseFixup prim wX wY

namedToFixups :: (PrimPatch (PrimOf p), Effect p) => Named p wX wY -> FL (RebaseFixup (PrimOf p)) wX wY
namedToFixups :: Named p wX wY -> FL (RebaseFixup (PrimOf p)) wX wY
namedToFixups (NamedP PatchInfo
p [PatchInfo]
_ FL p wX wY
contents) = RebaseName wX wX -> RebaseFixup (PrimOf p) wX wX
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup (PatchInfo -> RebaseName wX wX
forall wX wY. PatchInfo -> RebaseName wX wY
AddName PatchInfo
p) RebaseFixup (PrimOf p) wX wX
-> FL (RebaseFixup (PrimOf p)) wX wY
-> FL (RebaseFixup (PrimOf p)) wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: (forall wW wY. PrimOf p wW wY -> RebaseFixup (PrimOf p) wW wY)
-> FL (PrimOf p) wX wY -> FL (RebaseFixup (PrimOf 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 forall wW wY. PrimOf p wW wY -> RebaseFixup (PrimOf p) wW wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup (FL p wX wY -> FL (PrimOf (FL p)) wX wY
forall (p :: * -> * -> *) wX wY.
Effect p =>
p wX wY -> FL (PrimOf p) wX wY
effect FL p wX wY
contents)

instance Show2 prim => Show (RebaseFixup prim wX wY) where
    showsPrec :: Int -> RebaseFixup prim wX wY -> ShowS
showsPrec Int
d (PrimFixup prim wX wY
p) =
        Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"PrimFixup " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> prim wX wY -> ShowS
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) prim wX wY
p
    showsPrec Int
d (NameFixup RebaseName wX wY
p) =
        Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"NameFixup " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> RebaseName wX wY -> ShowS
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) RebaseName wX wY
p

instance Show2 prim => Show1 (RebaseFixup prim wX)

instance Show2 prim => Show2 (RebaseFixup prim)

instance PrimPatch prim => PrimPatchBase (RebaseFixup prim) where
    type PrimOf (RebaseFixup prim) = prim

instance Apply prim => Apply (RebaseFixup prim) where
    type ApplyState (RebaseFixup prim) = ApplyState prim
    apply :: RebaseFixup prim wX wY -> m ()
apply (PrimFixup prim wX wY
p) = prim wX wY -> m ()
forall (p :: * -> * -> *) (m :: * -> *) wX wY.
(Apply p, ApplyMonad (ApplyState p) m) =>
p wX wY -> m ()
apply prim wX wY
p
    apply (NameFixup RebaseName wX wY
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    unapply :: RebaseFixup prim wX wY -> m ()
unapply (PrimFixup prim wX wY
p) = prim wX wY -> m ()
forall (p :: * -> * -> *) (m :: * -> *) wX wY.
(Apply p, ApplyMonad (ApplyState p) m) =>
p wX wY -> m ()
unapply prim wX wY
p
    unapply (NameFixup RebaseName wX wY
_) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance Invert prim => Invert (RebaseFixup prim) where
    invert :: RebaseFixup prim wX wY -> RebaseFixup prim wY wX
invert (PrimFixup prim wX wY
p) = prim wY wX -> RebaseFixup prim wY wX
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup (prim wX wY -> prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wX wY
p)
    invert (NameFixup RebaseName wX wY
n) = RebaseName wY wX -> RebaseFixup prim wY wX
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup (RebaseName wX wY -> RebaseName wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert RebaseName wX wY
n)

instance PatchInspect prim => PatchInspect (RebaseFixup prim) where
    listTouchedFiles :: RebaseFixup prim wX wY -> [AnchoredPath]
listTouchedFiles (PrimFixup prim wX wY
p) = prim wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles prim wX wY
p
    listTouchedFiles (NameFixup RebaseName wX wY
n) = RebaseName wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles RebaseName wX wY
n

    hunkMatches :: (ByteString -> Bool) -> RebaseFixup prim wX wY -> Bool
hunkMatches ByteString -> Bool
f (PrimFixup prim wX wY
p) = (ByteString -> Bool) -> prim wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f prim wX wY
p
    hunkMatches ByteString -> Bool
f (NameFixup RebaseName wX wY
n) = (ByteString -> Bool) -> RebaseName wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f RebaseName wX wY
n

instance PatchListFormat (RebaseFixup prim)

instance ShowPatchBasic prim => ShowPatchBasic (RebaseFixup prim) where
  showPatch :: ShowPatchFor -> RebaseFixup prim wX wY -> Doc
showPatch ShowPatchFor
f (PrimFixup prim wX wY
p) =
    String -> Doc
blueText String
"rebase-fixup" Doc -> Doc -> Doc
<+> String -> Doc
blueText String
"(" Doc -> Doc -> Doc
$$ ShowPatchFor -> prim wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f prim wX wY
p Doc -> Doc -> Doc
$$ String -> Doc
blueText String
")"
  showPatch ShowPatchFor
f (NameFixup RebaseName wX wY
p) =
    String -> Doc
blueText String
"rebase-name" Doc -> Doc -> Doc
<+> String -> Doc
blueText String
"(" Doc -> Doc -> Doc
$$ ShowPatchFor -> RebaseName wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f RebaseName wX wY
p Doc -> Doc -> Doc
$$ String -> Doc
blueText String
")"

instance ReadPatch prim => ReadPatch (RebaseFixup prim) where
 readPatch' :: Parser (Sealed (RebaseFixup prim wX))
readPatch' =
   (forall wX. prim wX wX -> RebaseFixup prim wX wX)
-> Sealed (prim wX) -> Sealed (RebaseFixup prim wX)
forall (a :: * -> *) (b :: * -> *).
(forall wX. a wX -> b wX) -> Sealed a -> Sealed b
mapSeal forall wX. prim wX wX -> RebaseFixup prim wX wX
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup (Sealed (prim wX) -> Sealed (RebaseFixup prim wX))
-> Parser ByteString (Sealed (prim wX))
-> Parser (Sealed (RebaseFixup prim wX))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> Parser ByteString (Sealed (prim wX))
forall (q :: * -> * -> *) wX.
ReadPatch q =>
ByteString -> Parser (Sealed (q wX))
readWith (String -> ByteString
BC.pack String
"rebase-fixup" ) Parser (Sealed (RebaseFixup prim wX))
-> Parser (Sealed (RebaseFixup prim wX))
-> Parser (Sealed (RebaseFixup prim wX))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
   (forall wX. RebaseName wX wX -> RebaseFixup prim wX wX)
-> Sealed (RebaseName wX) -> Sealed (RebaseFixup prim wX)
forall (a :: * -> *) (b :: * -> *).
(forall wX. a wX -> b wX) -> Sealed a -> Sealed b
mapSeal forall wX. RebaseName wX wX -> RebaseFixup prim wX wX
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup (Sealed (RebaseName wX) -> Sealed (RebaseFixup prim wX))
-> Parser ByteString (Sealed (RebaseName wX))
-> Parser (Sealed (RebaseFixup prim wX))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ByteString -> Parser ByteString (Sealed (RebaseName wX))
forall (q :: * -> * -> *) wX.
ReadPatch q =>
ByteString -> Parser (Sealed (q wX))
readWith (String -> ByteString
BC.pack String
"rebase-name"  )
   where
     readWith :: forall q wX . ReadPatch q => B.ByteString -> Parser (Sealed (q wX))
     readWith :: ByteString -> Parser (Sealed (q wX))
readWith ByteString
str = do
       ByteString -> Parser ()
lexString ByteString
str
       ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
"(")
       Sealed (q wX)
res <- Parser (Sealed (q wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
       ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
")")
       Sealed (q wX) -> Parser (Sealed (q wX))
forall (m :: * -> *) a. Monad m => a -> m a
return Sealed (q wX)
res


instance Commute prim => Commute (RebaseFixup prim) where
    commute :: (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (RebaseFixup prim) wX wY)
commute (PrimFixup prim wX wZ
p :> PrimFixup prim wZ wY
q) = do
        prim wX wZ
q' :> prim wZ wY
p' <- (:>) prim prim wX wY -> Maybe ((:>) prim prim wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (prim wX wZ
p prim wX wZ -> prim wZ wY -> (:>) prim prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
        (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (prim wX wZ -> RebaseFixup prim wX wZ
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wX wZ
q' RebaseFixup prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY -> RebaseFixup prim wZ wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wZ wY
p')

    commute (NameFixup RebaseName wX wZ
p :> NameFixup RebaseName wZ wY
q) = do
        RebaseName wX wZ
q' :> RebaseName wZ wY
p' <- (:>) RebaseName RebaseName wX wY
-> Maybe ((:>) RebaseName RebaseName wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (RebaseName wX wZ
p RebaseName wX wZ
-> RebaseName wZ wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
q)
        (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX wZ -> RebaseFixup prim wX wZ
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wX wZ
q' RebaseFixup prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY -> RebaseFixup prim wZ wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wZ wY
p')

    commute (PrimFixup prim wX wZ
p :> NameFixup RebaseName wZ wY
q) = do
        RebaseName wX wZ
q' :> prim wZ wY
p' <- (:>) RebaseName prim wX wY -> Maybe ((:>) RebaseName prim wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) RebaseName prim wX wY -> Maybe ((:>) RebaseName prim wX wY))
-> (:>) RebaseName prim wX wY -> Maybe ((:>) RebaseName prim wX wY)
forall a b. (a -> b) -> a -> b
$ (:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
forall (prim :: * -> * -> *) wX wY.
(:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
commutePrimName (prim wX wZ
p prim wX wZ -> RebaseName wZ wY -> (:>) prim RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
q)
        (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX wZ -> RebaseFixup prim wX wZ
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wX wZ
q' RebaseFixup prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY -> RebaseFixup prim wZ wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wZ wY
p')

    commute (NameFixup RebaseName wX wZ
p :> PrimFixup prim wZ wY
q) = do
        prim wX wZ
q' :> RebaseName wZ wY
p' <- (:>) prim RebaseName wX wY -> Maybe ((:>) prim RebaseName wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) prim RebaseName wX wY -> Maybe ((:>) prim RebaseName wX wY))
-> (:>) prim RebaseName wX wY -> Maybe ((:>) prim RebaseName wX wY)
forall a b. (a -> b) -> a -> b
$ (:>) RebaseName prim wX wY -> (:>) prim RebaseName wX wY
forall (prim :: * -> * -> *) wX wY.
(:>) RebaseName prim wX wY -> (:>) prim RebaseName wX wY
commuteNamePrim (RebaseName wX wZ
p RebaseName wX wZ -> prim wZ wY -> (:>) RebaseName prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
        (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (prim wX wZ -> RebaseFixup prim wX wZ
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wX wZ
q' RebaseFixup prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (RebaseFixup prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY -> RebaseFixup prim wZ wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wZ wY
p')

pushFixupPrim
  :: PrimPatch prim
  => D.DiffAlgorithm
  -> PushFixupFn prim prim (FL prim) (Maybe2 prim)
pushFixupPrim :: DiffAlgorithm -> PushFixupFn prim prim (FL prim) (Maybe2 prim)
pushFixupPrim DiffAlgorithm
da (prim wX wZ
f1 :> prim wZ wY
f2)
 | EqCheck wX wY
IsEq <- EqCheck wX wY
isInverse = FL prim wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wX wX
-> Maybe2 prim wX wX -> (:>) (FL prim) (Maybe2 prim) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 prim wX wX
forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
 | Bool
otherwise
   = case (:>) prim prim wX wY -> Maybe ((:>) prim prim wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (prim wX wZ
f1 prim wX wZ -> prim wZ wY -> (:>) prim prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
f2) of
       Maybe ((:>) prim prim wX wY)
Nothing -> DiffAlgorithm -> FL prim wX wY -> FL prim wX wY
forall (prim :: * -> * -> *) wX wY.
PrimCanonize prim =>
DiffAlgorithm -> FL prim wX wY -> FL prim wX wY
canonizeFL DiffAlgorithm
da (prim wX wZ
f1 prim wX wZ -> FL prim wZ wY -> FL prim wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: prim wZ wY
f2 prim wZ wY -> FL prim wY wY -> FL prim wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wX wY
-> Maybe2 prim wY wY -> (:>) (FL prim) (Maybe2 prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 prim wY wY
forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
       Just (prim wX wZ
f2' :> prim wZ wY
f1') -> (prim wX wZ
f2' prim wX wZ -> FL prim wZ wZ -> FL prim wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wX wZ
-> Maybe2 prim wZ wY -> (:>) (FL prim) (Maybe2 prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY -> Maybe2 prim wZ wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 prim wZ wY
f1'
  where isInverse :: EqCheck wX wY
isInverse = prim wX wZ -> prim wZ wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wX wZ
f1 prim wZ wX -> prim wZ wY -> EqCheck wX wY
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wY
f2

pushFixupFixup
  :: PrimPatch prim
  => D.DiffAlgorithm
  -> PushFixupFn
       (RebaseFixup prim) (RebaseFixup prim)
       (FL (RebaseFixup prim)) (Maybe2 (RebaseFixup prim))

pushFixupFixup :: DiffAlgorithm
-> PushFixupFn
     (RebaseFixup prim)
     (RebaseFixup prim)
     (FL (RebaseFixup prim))
     (Maybe2 (RebaseFixup prim))
pushFixupFixup DiffAlgorithm
da (PrimFixup prim wX wZ
f1 :> PrimFixup prim wZ wY
f2)
  = case DiffAlgorithm
-> (:>) prim prim wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
forall (prim :: * -> * -> *).
PrimPatch prim =>
DiffAlgorithm -> PushFixupFn prim prim (FL prim) (Maybe2 prim)
pushFixupPrim DiffAlgorithm
da (prim wX wZ
f1 prim wX wZ -> prim wZ wY -> (:>) prim prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
f2) of
      FL prim wX wZ
fs2' :> Maybe2 prim wZ wY
f1' -> (forall wW wY. prim wW wY -> RebaseFixup prim wW wY)
-> FL prim wX wZ -> FL (RebaseFixup prim) 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 forall wW wY. prim wW wY -> RebaseFixup prim wW wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup FL prim wX wZ
fs2' FL (RebaseFixup prim) wX wZ
-> Maybe2 (RebaseFixup prim) wZ wY
-> (:>) (FL (RebaseFixup prim)) (Maybe2 (RebaseFixup prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (prim wZ wY -> RebaseFixup prim wZ wY)
-> Maybe2 prim wZ wY -> Maybe2 (RebaseFixup prim) wZ wY
forall (p :: * -> * -> *) wX wY (q :: * -> * -> *).
(p wX wY -> q wX wY) -> Maybe2 p wX wY -> Maybe2 q wX wY
mapMB_MB prim wZ wY -> RebaseFixup prim wZ wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup Maybe2 prim wZ wY
f1'

pushFixupFixup DiffAlgorithm
_da (PrimFixup prim wX wZ
f :> NameFixup RebaseName wZ wY
n)
  = case (:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
forall (prim :: * -> * -> *) wX wY.
(:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
commutePrimName (prim wX wZ
f prim wX wZ -> RebaseName wZ wY -> (:>) prim RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
n) of
      RebaseName wX wZ
n' :> prim wZ wY
f' -> (RebaseName wX wZ -> RebaseFixup prim wX wZ
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wX wZ
n' RebaseFixup prim wX wZ
-> FL (RebaseFixup prim) wZ wZ -> FL (RebaseFixup prim) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (RebaseFixup prim) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL (RebaseFixup prim) wX wZ
-> Maybe2 (RebaseFixup prim) wZ wY
-> (:>) (FL (RebaseFixup prim)) (Maybe2 (RebaseFixup prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseFixup prim wZ wY -> Maybe2 (RebaseFixup prim) wZ wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 (prim wZ wY -> RebaseFixup prim wZ wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wZ wY
f')

pushFixupFixup DiffAlgorithm
_da (NameFixup RebaseName wX wZ
n1 :> NameFixup RebaseName wZ wY
n2)
  = case (:>) RebaseName RebaseName wX wY
-> (:>) (FL RebaseName) (Maybe2 RebaseName) wX wY
PushFixupFn
  RebaseName RebaseName (FL RebaseName) (Maybe2 RebaseName)
pushFixupName (RebaseName wX wZ
n1 RebaseName wX wZ
-> RebaseName wZ wY -> (:>) RebaseName RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
n2) of
      FL RebaseName wX wZ
ns2' :> Maybe2 RebaseName wZ wY
n1' -> (forall wW wY. RebaseName wW wY -> RebaseFixup prim wW wY)
-> FL RebaseName wX wZ -> FL (RebaseFixup prim) 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 forall wW wY. RebaseName wW wY -> RebaseFixup prim wW wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup FL RebaseName wX wZ
ns2' FL (RebaseFixup prim) wX wZ
-> Maybe2 (RebaseFixup prim) wZ wY
-> (:>) (FL (RebaseFixup prim)) (Maybe2 (RebaseFixup prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (RebaseName wZ wY -> RebaseFixup prim wZ wY)
-> Maybe2 RebaseName wZ wY -> Maybe2 (RebaseFixup prim) wZ wY
forall (p :: * -> * -> *) wX wY (q :: * -> * -> *).
(p wX wY -> q wX wY) -> Maybe2 p wX wY -> Maybe2 q wX wY
mapMB_MB RebaseName wZ wY -> RebaseFixup prim wZ wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup Maybe2 RebaseName wZ wY
n1'

pushFixupFixup DiffAlgorithm
_da (NameFixup RebaseName wX wZ
n :> PrimFixup prim wZ wY
f)
  = case (:>) RebaseName prim wX wY -> (:>) prim RebaseName wX wY
forall (prim :: * -> * -> *) wX wY.
(:>) RebaseName prim wX wY -> (:>) prim RebaseName wX wY
commuteNamePrim (RebaseName wX wZ
n RebaseName wX wZ -> prim wZ wY -> (:>) RebaseName prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
f) of
      prim wX wZ
f' :> RebaseName wZ wY
n' -> (prim wX wZ -> RebaseFixup prim wX wZ
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wX wZ
f' RebaseFixup prim wX wZ
-> FL (RebaseFixup prim) wZ wZ -> FL (RebaseFixup prim) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (RebaseFixup prim) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL (RebaseFixup prim) wX wZ
-> Maybe2 (RebaseFixup prim) wZ wY
-> (:>) (FL (RebaseFixup prim)) (Maybe2 (RebaseFixup prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseFixup prim wZ wY -> Maybe2 (RebaseFixup prim) wZ wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Maybe2 p wX wY
Just2 (RebaseName wZ wY -> RebaseFixup prim wZ wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wZ wY
n')


-- |Split a sequence of fixups into names and prims
flToNamesPrims :: FL (RebaseFixup prim) wX wY
               -> (FL RebaseName :> FL prim) wX wY
flToNamesPrims :: FL (RebaseFixup prim) wX wY -> (:>) (FL RebaseName) (FL prim) wX wY
flToNamesPrims FL (RebaseFixup prim) wX wY
NilFL = FL RebaseName wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL RebaseName wX wX
-> FL prim wX wX -> (:>) (FL RebaseName) (FL prim) wX wX
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
flToNamesPrims (NameFixup RebaseName wX wY
n :>: FL (RebaseFixup prim) wY wY
fs) =
    case FL (RebaseFixup prim) wY wY -> (:>) (FL RebaseName) (FL prim) wY wY
forall (prim :: * -> * -> *) wX wY.
FL (RebaseFixup prim) wX wY -> (:>) (FL RebaseName) (FL prim) wX wY
flToNamesPrims FL (RebaseFixup prim) wY wY
fs of
        FL RebaseName wY wZ
names :> FL prim wZ wY
prims -> (RebaseName wX wY
n RebaseName wX wY -> FL RebaseName wY wZ -> FL RebaseName wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL RebaseName wY wZ
names) FL RebaseName wX wZ
-> FL prim wZ wY -> (:>) (FL RebaseName) (FL prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wZ wY
prims
flToNamesPrims (PrimFixup prim wX wY
p :>: FL (RebaseFixup prim) wY wY
fs) =
    case FL (RebaseFixup prim) wY wY -> (:>) (FL RebaseName) (FL prim) wY wY
forall (prim :: * -> * -> *) wX wY.
FL (RebaseFixup prim) wX wY -> (:>) (FL RebaseName) (FL prim) wX wY
flToNamesPrims FL (RebaseFixup prim) wY wY
fs of
        FL RebaseName wY wZ
names :> FL prim wZ wY
prims ->
            case TotalCommuteFn prim RebaseName
-> (:>) prim (FL RebaseName) wX wZ
-> (:>) (FL RebaseName) prim wX wZ
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
TotalCommuteFn p1 p2 -> TotalCommuteFn p1 (FL p2)
totalCommuterIdFL TotalCommuteFn prim RebaseName
forall (prim :: * -> * -> *) wX wY.
(:>) prim RebaseName wX wY -> (:>) RebaseName prim wX wY
commutePrimName (prim wX wY
p prim wX wY
-> FL RebaseName wY wZ -> (:>) prim (FL RebaseName) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL RebaseName wY wZ
names) of
                FL RebaseName wX wZ
names' :> prim wZ wZ
p' -> FL RebaseName wX wZ
names' FL RebaseName wX wZ
-> FL prim wZ wY -> (:>) (FL RebaseName) (FL prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> (prim wZ wZ
p' prim wZ wZ -> FL prim wZ wY -> FL prim wZ wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wY
prims)

commuteNamedFixup
  :: Commute prim
  => (Named prim :> RebaseFixup prim) wX wY
  -> Maybe ((RebaseFixup prim :> Named prim) wX wY)
commuteNamedFixup :: (:>) (Named prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (Named prim) wX wY)
commuteNamedFixup (Named prim wX wZ
p :> PrimFixup prim wZ wY
q) = do
    prim wX wZ
q' :> Named prim wZ wY
p' <- CommuteFn prim prim
-> (:>) (Named prim) prim wX wY
-> Maybe ((:>) prim (Named prim) wX wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (Named p1) p2
commuterNamedId CommuteFn prim prim
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
selfCommuter (Named prim wX wZ
p Named prim wX wZ -> prim wZ wY -> (:>) (Named prim) prim wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
    (:>) (RebaseFixup prim) (Named prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (Named prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (prim wX wZ -> RebaseFixup prim wX wZ
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wX wZ
q' RebaseFixup prim wX wZ
-> Named prim wZ wY -> (:>) (RebaseFixup prim) (Named prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named prim wZ wY
p')
commuteNamedFixup (Named prim wX wZ
p :> NameFixup RebaseName wZ wY
n) = do
    RebaseName wX wZ
n' :> Named prim wZ wY
p' <- (:>) (Named prim) RebaseName wX wY
-> Maybe ((:>) RebaseName (Named prim) wX wY)
forall (p :: * -> * -> *). CommuteFn (Named p) RebaseName
commuteNamedName (Named prim wX wZ
p Named prim wX wZ
-> RebaseName wZ wY -> (:>) (Named prim) RebaseName wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY
n)
    (:>) (RebaseFixup prim) (Named prim) wX wY
-> Maybe ((:>) (RebaseFixup prim) (Named prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (RebaseName wX wZ -> RebaseFixup prim wX wZ
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wX wZ
n' RebaseFixup prim wX wZ
-> Named prim wZ wY -> (:>) (RebaseFixup prim) (Named prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named prim wZ wY
p')

commuteFixupNamed
  :: Commute prim
  => (RebaseFixup prim :> Named prim) wX wY
  -> Maybe ((Named prim :> RebaseFixup prim) wX wY)
commuteFixupNamed :: (:>) (RebaseFixup prim) (Named prim) wX wY
-> Maybe ((:>) (Named prim) (RebaseFixup prim) wX wY)
commuteFixupNamed (PrimFixup prim wX wZ
p :> Named prim wZ wY
q) = do
    Named prim wX wZ
q' :> prim wZ wY
p' <- CommuteFn prim prim
-> (:>) prim (Named prim) wX wY
-> Maybe ((:>) (Named prim) prim wX wY)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (Named p2)
commuterIdNamed CommuteFn prim prim
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
selfCommuter (prim wX wZ
p prim wX wZ -> Named prim wZ wY -> (:>) prim (Named prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named prim wZ wY
q)
    (:>) (Named prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (Named prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named prim wX wZ
q' Named prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (Named prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY -> RebaseFixup prim wZ wY
forall (prim :: * -> * -> *) wX wY.
prim wX wY -> RebaseFixup prim wX wY
PrimFixup prim wZ wY
p')
commuteFixupNamed (NameFixup RebaseName wX wZ
n :> Named prim wZ wY
q) = do
    Named prim wX wZ
q' :> RebaseName wZ wY
n' <- (:>) RebaseName (Named prim) wX wY
-> Maybe ((:>) (Named prim) RebaseName wX wY)
forall (p :: * -> * -> *). CommuteFn RebaseName (Named p)
commuteNameNamed (RebaseName wX wZ
n RebaseName wX wZ
-> Named prim wZ wY -> (:>) RebaseName (Named prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Named prim wZ wY
q)
    (:>) (Named prim) (RebaseFixup prim) wX wY
-> Maybe ((:>) (Named prim) (RebaseFixup prim) wX wY)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named prim wX wZ
q' Named prim wX wZ
-> RebaseFixup prim wZ wY
-> (:>) (Named prim) (RebaseFixup prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RebaseName wZ wY -> RebaseFixup prim wZ wY
forall wX wY (prim :: * -> * -> *).
RebaseName wX wY -> RebaseFixup prim wX wY
NameFixup RebaseName wZ wY
n')