-- BSD3
module Darcs.Patch.Unwind
  ( Unwind(..)
  , Unwound(..)
  , mkUnwound
  , squashUnwound
  ) where

import Darcs.Prelude

import Darcs.Patch.Commute
  ( Commute, commute, selfCommuter
  )
import Darcs.Patch.CommuteFn
  ( commuterIdFL, commuterFLId
  )
import Darcs.Patch.Format ( PatchListFormat )
import Darcs.Patch.FromPrim ( PrimOf )
import Darcs.Patch.Invert
  ( Invert(..), invertFL, invertRL
  )
import Darcs.Patch.Show ( ShowPatchBasic(..) )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Witnesses.Eq ( EqCheck(..), Eq2(..) )
import Darcs.Patch.Witnesses.Maybe ( Maybe2(..) )
import Darcs.Patch.Witnesses.Ordered
  ( FL(..), (:>)(..), (+>+), reverseFL
  , RL(..), (+<+), reverseRL
  )
import Darcs.Patch.Witnesses.Show ( Show1, Show2, show2 )

import Darcs.Util.Printer ( blueText, vcat )

-- | An 'Unwound' represents a primitive patch, together with any
-- other primitives that are required to place the primitive in a
-- different context. Typically, the presence of context patches
-- indicates that the underlying primitive would be in conflict in
-- the given context.
--
-- We have the following invariants:
--  - if a context contains a patch, that context does not also
--    contain the inverse of that patch (when commuted next to each other)
--  - if either context contains a patch that commutes with the underlying
--    patch, then neither context contains the inverse of that patch
--    (when commuted next to each other)
-- Another way of putting it is that all possible pairs of patch+inverse
-- that can be reached by commutation are removed.
data Unwound prim wX wY where
  Unwound
    :: FL prim wA wB        -- ^context before
    -> FL prim wB wC        -- ^underlying primitives
    -> RL prim wC wD        -- ^context after
    -> Unwound prim wA wD

deriving instance Show2 prim => Show (Unwound prim wX wY)
instance Show2 prim => Show1 (Unwound prim wX)
instance Show2 prim => Show2 (Unwound prim)

instance (PatchListFormat prim, ShowPatchBasic prim)
  => ShowPatchBasic (Unwound prim) where
  showPatch :: forall wX wY. ShowPatchFor -> Unwound prim wX wY -> Doc
showPatch ShowPatchFor
f (Unwound FL prim wX wB
before FL prim wB wC
prims RL prim wC wY
after) =
    [Doc] -> Doc
vcat [
      String -> Doc
blueText String
"before:",
      forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wX wB
before,
      String -> Doc
blueText String
"prims:",
      forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wB wC
prims,
      String -> Doc
blueText String
"after:",
      forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f RL prim wC wY
after
    ]

instance Invert prim => Invert (Unwound prim) where
  invert :: forall wX wY. Unwound prim wX wY -> Unwound prim wY wX
invert (Unwound FL prim wX wB
before FL prim wB wC
prim RL prim wC wY
after)
    = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL RL prim wC wY
after) (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert FL prim wB wC
prim) (forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL FL prim wX wB
before)

class Unwind p where
  -- | Get hold of the underlying primitives for a given patch, placed in
  -- the context of the patch. If there are conflicts then context patches
  -- will be needed.
  fullUnwind :: p wX wY -> Unwound (PrimOf p) wX wY

mkUnwound
  :: (Commute prim, Invert prim, Eq2 prim)
  => FL prim wA wB
  -> FL prim wB wC
  -> FL prim wC wD
  -> Unwound prim wA wD
mkUnwound :: forall (prim :: * -> * -> *) wA wB wC wD.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB
-> FL prim wB wC -> FL prim wC wD -> Unwound prim wA wD
mkUnwound FL prim wA wB
before FL prim wB wC
ps FL prim wC wD
after =
  forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
before forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters FL prim wC wD
after forall a b. (a -> b) -> a -> b
$
  forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wB wC
ps forall (a :: * -> * -> *) wX. RL a wX wX
NilRL

consBefores
  :: (Commute prim, Invert prim, Eq2 prim)
  => FL prim wA wB
  -> Unwound prim wB wC
  -> Unwound prim wA wC
consBefores :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
NilFL Unwound prim wB wC
u = Unwound prim wB wC
u
consBefores (prim wA wY
b :>: FL prim wY wB
bs) Unwound prim wB wC
u = forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wA wY
b (forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wY wB
bs Unwound prim wB wC
u)

consAfters
  :: (Commute prim, Invert prim, Eq2 prim)
  => Unwound prim wA wB
  -> FL prim wB wC
  -> Unwound prim wA wC
consAfters :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters Unwound prim wA wB
u FL prim wB wC
NilFL = Unwound prim wA wB
u
consAfters Unwound prim wA wB
u (prim wB wY
a :>: FL prim wY wC
as) = forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters (forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter Unwound prim wA wB
u prim wB wY
a) FL prim wY wC
as

consBefore
  :: (Commute prim, Invert prim, Eq2 prim)
  => prim wA wB
  -> Unwound prim wB wC
  -> Unwound prim wA wC
consBefore :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wA wB
b (Unwound FL prim wB wB
NilFL FL prim wB wC
ps RL prim wC wC
after) =
  case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (prim wA wB
b forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wB wC
ps) of
    Maybe ((:>) (FL prim) prim wA wC)
Nothing -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wB wC
ps RL prim wC wC
after
    -- It is possible for a context patch to commute with the
    -- underlying primitive. If that happens we want to see if we can eliminate it
    -- by propagating it through the other context ("after" in this case).
    -- "full unwind example 3" fails if this case is omitted, as (typically) do the standard
    -- 100 iteration QuickCheck tests
    Just (FL prim wA wZ
ps' :> prim wZ wC
b') -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wA wZ
ps' (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wC
b' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wC wC
after))
consBefore prim wA wB
b1 (Unwound (prim wB wY
b2 :>: FL prim wY wB
bs) FL prim wB wC
ps RL prim wC wC
after)
  | EqCheck wA wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wA wB
b1 forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wY
b2 = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
bs FL prim wB wC
ps RL prim wC wC
after
  | Just (prim wA wZ
b2' :> prim wZ wY
b1') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wA wB
b1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wY
b2)
     = case forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefore prim wZ wY
b1' (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
bs FL prim wB wC
ps RL prim wC wC
after) of
         Unwound FL prim wZ wB
bs' FL prim wB wC
ps' RL prim wC wC
after' -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wZ
b2' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
bs') FL prim wB wC
ps' RL prim wC wC
after'
consBefore prim wA wB
b (Unwound FL prim wB wB
bs FL prim wB wC
ps RL prim wC wC
after) = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wB wB
bs) FL prim wB wC
ps RL prim wC wC
after

consAfter
  :: (Commute prim, Invert prim, Eq2 prim)
  => Unwound prim wA wB
  -> prim wB wC
  -> Unwound prim wA wC
consAfter :: forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
NilRL) prim wB wC
a =
  case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (FL prim wB wC
ps forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
a) of
    Maybe ((:>) prim (FL prim) wB wC)
Nothing -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wB wC
a)
    -- as with consBefore, we need to see if we can eliminate a context patch
    -- that commutes with the underlying primitive, by propagating it through the
    -- "before" context
    -- "full unwind example 3" fails if this case is omitted, as (typically) do the standard
    -- 100 iteration QuickCheck tests
    Just (prim wB wZ
a' :> FL prim wZ wC
ps') -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wA wB
before forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wZ
a' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)) FL prim wZ wC
ps' forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps (RL prim wC wY
as :<: prim wY wB
a1)) prim wB wC
a2
  | EqCheck wY wC
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wB
a1 forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wC
a2 = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wY
as
  | Just (prim wY wZ
a2' :> prim wZ wC
a1') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wB
a1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
a2)
      = case forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wY
as) prim wY wZ
a2' of
          Unwound FL prim wA wB
before' FL prim wB wC
ps' RL prim wC wZ
as' -> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before' FL prim wB wC
ps' (RL prim wC wZ
as' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wC
a1')
consAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
as) prim wB wC
a = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps (RL prim wC wB
as forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wB wC
a)

propagateBefore
  :: (Commute prim, Invert prim, Eq2 prim)
  => (RL prim :> prim :> FL prim) wA wB
  -> FL prim wA wB
propagateBefore :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (RL prim wA wZ
NilRL :> prim wZ wZ
p :> FL prim wZ wB
acc) = prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc
propagateBefore (RL prim wA wY
qs :<: prim wY wZ
q :> prim wZ wZ
p :> FL prim wZ wB
acc)
  | EqCheck wY wZ
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wZ
q forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wZ
p = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wZ wB
acc
  | Just (prim wY wZ
p' :> prim wZ wZ
q') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wZ
q forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
p)
      = forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (RL prim wA wY
qs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wY wZ
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
q' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc)
  | Bool
otherwise = forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ prim wY wZ
q forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc

propagateAfter
  :: (Commute prim, Invert prim, Eq2 prim)
  => (RL prim :> prim :> FL prim) wA wB
  -> RL prim wA wB
propagateAfter :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (RL prim wA wZ
acc :> prim wZ wZ
p :> FL prim wZ wB
NilFL) = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
p
propagateAfter (RL prim wA wZ
acc :> prim wZ wZ
p :> prim wZ wY
q :>: FL prim wY wB
qs)
  | EqCheck wZ wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wZ wZ
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wY
q = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wY wB
qs
  | Just (prim wZ wZ
q' :> prim wZ wY
p') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wZ wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
      = forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
q' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wY wB
qs)
  | Bool
otherwise = RL prim wA wZ
acc forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
p forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wY
q forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wY wB
qs


-- | Given a list of unwound patches, use commutation and cancellation of
-- inverses to remove intermediate contexts. This is not guaranteed to be
-- possible in general, but should be possible if the patches that were
-- unwound were all originally recorded (unconflicted) in the same context,
-- e.g. as part of the same 'Darcs.Patch.Named.Named'.
squashUnwound
  :: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
  => FL (Unwound prim) wX wY
  -> Unwound prim wX wY
squashUnwound :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
FL (Unwound prim) wX wY -> Unwound prim wX wY
squashUnwound FL (Unwound prim) wX wY
NilFL = forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
squashUnwound (Unwound prim wX wY
u :>: FL (Unwound prim) wY wY
us) =
  -- As described in consBefore/consAfter, it's possible for some of the elements
  -- in a context to commute with the underlying prim that context is attached to,
  -- so consBefore/consAfter try to cancel them by propagating through the other
  -- context.
  -- Sometimes they also won't cancel or commute with patches in the other context
  -- so when squashing we need to move them out of the way of the patches that really
  -- need to be squashed first.
  -- The unit test "full unwind example 3" fails if we remove the moveCommuting calls,
  -- as do QuickCheck tests with a lot of iterations (e.g. 100K)
  forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToBefore Unwound prim wX wY
u forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToAfter (forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
FL (Unwound prim) wX wY -> Unwound prim wX wY
squashUnwound FL (Unwound prim) wY wY
us))

moveCommutingToBefore
  :: (Commute prim, Invert prim, Eq2 prim)
  => Unwound prim wA wB
  -> Unwound prim wA wB
moveCommutingToBefore :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToBefore (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
after) =
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters (forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wC wB
after) forall a b. (a -> b) -> a -> b
$
  forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps forall (a :: * -> * -> *) wX. RL a wX wX
NilRL

moveCommutingToAfter
  :: (Commute prim, Invert prim, Eq2 prim)
  => Unwound prim wA wB
  -> Unwound prim wA wB
moveCommutingToAfter :: forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToAfter (Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wB
after) =
  forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
FL prim wA wB -> Unwound prim wB wC -> Unwound prim wA wC
consBefores FL prim wA wB
before forall a b. (a -> b) -> a -> b
$
  forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wB wC
ps RL prim wC wB
after

squashPair
  :: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
  => (Unwound prim :> Unwound prim) wX wY
  -> Unwound prim wX wY
squashPair :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (Unwound FL prim wX wB
before FL prim wB wC
ps1 RL prim wC wZ
NilRL :> Unwound FL prim wZ wB
NilFL FL prim wB wC
ps2 RL prim wC wY
after) =
  forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before (FL prim wB wC
ps1 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wB wC
ps2) RL prim wC wY
after
squashPair (Unwound FL prim wX wB
before1 FL prim wB wC
ps1 (RL prim wC wY
after1 :<: prim wY wZ
a) :> Unwound FL prim wZ wB
before2 FL prim wB wC
ps2 RL prim wC wY
after2) =
  case forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wY wZ
a forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wZ wB
before2) of
    FL prim wY wZ
before2' :> Maybe2 prim wZ wB
Nothing2 ->
      forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wY
after1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wZ
before2' FL prim wB wC
ps2 RL prim wC wY
after2)
    FL prim wY wZ
before2' :> Just2 prim wZ wB
a' ->
      case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (prim wZ wB
a' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wB wC
ps2) of
        Maybe ((:>) (FL prim) prim wZ wC)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"stuck patch: squashPair 1:\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wZ wB
a' forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 FL prim wB wC
ps2
        Just (FL prim wZ wZ
ps2' :> prim wZ wC
a'') ->
          forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wY
after1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wZ
before2' FL prim wZ wZ
ps2' (forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wC
a'' forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ RL prim wC wY
after2))
squashPair (Unwound FL prim wX wB
before1 FL prim wB wC
ps1 RL prim wC wZ
NilRL :> Unwound (prim wZ wY
b :>: FL prim wY wB
before2) FL prim wB wC
ps2 RL prim wC wY
after2) =
  case forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (FL prim wB wC
ps1 forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
b) of
    Maybe ((:>) prim (FL prim) wB wY)
Nothing -> forall a. HasCallStack => String -> a
error String
"stuck patch: squashPair 2"
    Just (prim wB wZ
b' :> FL prim wZ wY
ps1') -> forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (FL prim wX wB
before1 forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ prim wB wZ
b' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wZ wY
ps1' forall (a :: * -> * -> *) wX. RL a wX wX
NilRL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (prim :: * -> * -> *) wA wY wC wD.
FL prim wA wY
-> FL prim wY wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wY wB
before2 FL prim wB wC
ps2 RL prim wC wY
after2)

pushPastForward
  :: (Show2 prim, Commute prim, Eq2 prim, Invert prim)
  => (prim :> FL prim) wX wY
  -> (FL prim :> Maybe2 prim) wX wY
pushPastForward :: forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wX wZ
p :> FL prim 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 prim wX wZ
p
pushPastForward (prim wX wZ
p :> (prim wZ wY
q :>: FL prim wY wY
qs))
  | EqCheck wX wY
IsEq <- forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wX wZ
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wY
q = FL prim wY wY
qs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> forall (p :: * -> * -> *) wX. Maybe2 p wX wX
Nothing2
  | Just (prim wX wZ
q' :> prim wZ wY
p') <- forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wX wZ
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
      = case forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) prim (FL prim) wX wY -> (:>) (FL prim) (Maybe2 prim) wX wY
pushPastForward (prim wZ wY
p' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wY wY
qs) of
          FL prim wZ wZ
qs' :> Maybe2 prim wZ wY
p'' -> (prim wX wZ
q' forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wZ
qs') forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Maybe2 prim wZ wY
p''
  | Bool
otherwise = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"stuck patch: pushPastForward:\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wX wZ
p forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall (a :: * -> * -> *) wX wY. Show2 a => a wX wY -> String
show2 prim wZ wY
q