-- 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 :: 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:",
      ShowPatchFor -> FL prim wX wB -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wX wB
before,
      String -> Doc
blueText String
"prims:",
      ShowPatchFor -> FL prim wB wC -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL prim wB wC
prims,
      String -> Doc
blueText String
"after:",
      ShowPatchFor -> RL prim wC wY -> Doc
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 :: 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)
    = FL prim wY wC
-> FL prim wC wB -> RL prim wB wX -> Unwound prim wY wX
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (RL prim wC wY -> FL prim wY wC
forall (p :: * -> * -> *) wX wY.
Invert p =>
RL p wX wY -> FL p wY wX
invertRL RL prim wC wY
after) (FL prim wB wC -> FL prim wC wB
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert FL prim wB wC
prim) (FL prim wX wB -> RL prim wB wX
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 :: 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 =
  FL prim wA wB -> Unwound prim wB wD -> Unwound prim wA wD
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 (Unwound prim wB wD -> Unwound prim wA wD)
-> (Unwound prim wB wC -> Unwound prim wB wD)
-> Unwound prim wB wC
-> Unwound prim wA wD
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (Unwound prim wB wC -> FL prim wC wD -> Unwound prim wB wD)
-> FL prim wC wD -> Unwound prim wB wC -> Unwound prim wB wD
forall a b c. (a -> b -> c) -> b -> a -> c
flip Unwound prim wB wC -> FL prim wC wD -> Unwound prim wB wD
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 (Unwound prim wB wC -> Unwound prim wA wD)
-> Unwound prim wB wC -> Unwound prim wA wD
forall a b. (a -> b) -> a -> b
$
  FL prim wB wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wB wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wB wB
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wB wC
ps RL prim wC wC
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 :: 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 wA wC
Unwound prim wB wC
u
consBefores (prim wA wY
b :>: FL prim wY wB
bs) Unwound prim wB wC
u = prim wA wY -> Unwound prim wY wC -> Unwound prim wA wC
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 (FL prim wY wB -> Unwound prim wB wC -> Unwound prim wY wC
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 :: 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
Unwound prim wA wC
u
consAfters Unwound prim wA wB
u (prim wB wY
a :>: FL prim wY wC
as) = Unwound prim wA wY -> FL prim wY wC -> Unwound prim wA wC
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 -> prim wB wY -> Unwound prim wA wY
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 :: 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 CommuteFn prim prim
-> (:>) prim (FL prim) wA wC -> Maybe ((:>) (FL prim) prim wA wC)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL CommuteFn prim prim
forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (prim wA wB
b prim wA wB -> FL prim wB wC -> (:>) prim (FL prim) wA wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wB wC
FL prim wB wC
ps) of
    Maybe ((:>) (FL prim) prim wA wC)
Nothing -> FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b prim wA wB -> FL prim wB wB -> FL prim wA wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wB wB
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) FL prim wB wC
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') -> FL prim wA wA
-> FL prim wA wZ -> RL prim wZ wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wA
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wA wZ
ps' ((:>) (RL prim) (prim :> FL prim) wZ wC -> RL prim wZ wC
forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
propagateAfter (RL prim wZ wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL prim wZ wZ
-> (:>) prim (FL prim) wZ wC
-> (:>) (RL prim) (prim :> FL prim) wZ wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wC
b' prim wZ wC -> FL prim wC wC -> (:>) prim (FL prim) wZ wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL prim wC wC -> FL prim wC wC
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 <- prim wA wB -> prim wB wA
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wA wB
b1 prim wB wA -> prim wB wY -> EqCheck wA wY
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wY
b2 = FL prim wY wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wY wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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') <- (:>) prim prim wA wY -> Maybe ((:>) prim prim wA wY)
forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wA wB
b1 prim wA wB -> prim wB wY -> (:>) prim prim wA wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wY
b2)
     = case prim wZ wY -> Unwound prim wY wC -> Unwound prim wZ wC
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' (FL prim wY wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wY wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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' -> FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wZ
b2' prim wA wZ -> FL prim wZ wB -> FL prim wA wB
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) = FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound (prim wA wB
b prim wA wB -> FL prim wB wB -> FL prim wA wB
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 :: 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 CommuteFn prim prim
-> (:>) (FL prim) prim wB wC -> Maybe ((:>) prim (FL prim) wB wC)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn (FL p1) p2
commuterFLId CommuteFn prim prim
forall (p :: * -> * -> *). Commute p => CommuteFn p p
selfCommuter (FL prim wB wC
ps FL prim wB wC -> prim wC wC -> (:>) (FL prim) prim wB wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
prim wC wC
a) of
    Maybe ((:>) prim (FL prim) wB wC)
Nothing -> FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps (RL prim wB wB
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL prim wB wB -> prim wB wC -> RL prim wB wC
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') -> FL prim wA wZ
-> FL prim wZ wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound ((:>) (RL prim) (prim :> FL prim) wA wZ -> FL prim wA wZ
forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
(:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
propagateBefore (FL prim wA wB -> RL prim wA wB
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL prim wA wB
before RL prim wA wB
-> (:>) prim (FL prim) wB wZ
-> (:>) (RL prim) (prim :> FL prim) wA wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wZ
a' prim wB wZ -> FL prim wZ wZ -> (:>) prim (FL prim) wB wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL prim wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)) FL prim wZ wC
ps' RL prim wC wC
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 <- prim wY wB -> prim wB wY
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wB
a1 prim wB wY -> prim wB wC -> EqCheck wY wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wB wC
a2 = FL prim wA wB
-> FL prim wB wC -> RL prim wC wY -> Unwound prim wA wY
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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') <- (:>) prim prim wY wC -> Maybe ((:>) prim prim wY wC)
forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wB
a1 prim wY wB -> prim wB wC -> (:>) prim prim wY wC
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wB wC
a2)
      = case Unwound prim wA wY -> prim wY wZ -> Unwound prim wA wZ
forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> prim wB wC -> Unwound prim wA wC
consAfter (FL prim wA wB
-> FL prim wB wC -> RL prim wC wY -> Unwound prim wA wY
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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' -> FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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' RL prim wC wZ -> prim wZ wC -> RL prim wC wC
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 = FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB 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 RL prim wC wB -> prim wB wC -> RL prim wC wC
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 :: (:>) (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 prim wZ wZ -> FL prim wZ wB -> FL prim wZ wB
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 <- prim wY wZ -> prim wZ wY
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wY wZ
q prim wZ wY -> prim wZ wZ -> EqCheck wY wZ
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= prim wZ wZ
p = RL prim wA wY -> FL prim wA wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs FL prim wA wY -> FL prim wY wB -> FL prim wA wB
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wY wB
FL prim wZ wB
acc
  | Just (prim wY wZ
p' :> prim wZ wZ
q') <- (:>) prim prim wY wZ -> Maybe ((:>) prim prim wY wZ)
forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wY wZ
q prim wY wZ -> prim wZ wZ -> (:>) prim prim wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
p)
      = (:>) (RL prim) (prim :> FL prim) wA wB -> FL prim wA wB
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 RL prim wA wY
-> (:>) prim (FL prim) wY wB
-> (:>) (RL prim) (prim :> FL prim) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wY wZ
p' prim wY wZ -> FL prim wZ wB -> (:>) prim (FL prim) wY wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wZ
q' prim wZ wZ -> FL prim wZ wB -> FL prim wZ wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wZ wB
acc)
  | Bool
otherwise = RL prim wA wY -> FL prim wA wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wA wY
qs FL prim wA wY -> FL prim wY wB -> FL prim wA wB
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ prim wY wZ
q prim wY wZ -> FL prim wZ wB -> FL prim wY wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: prim wZ wZ
p prim wZ wZ -> FL prim wZ wB -> FL prim wZ wB
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 :: (:>) (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 RL prim wA wZ -> prim wZ wZ -> RL prim wA wZ
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 <- prim wZ wZ -> prim wZ wZ
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wZ wZ
p prim wZ wZ -> prim wZ wY -> EqCheck wZ wY
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 RL prim wA wZ -> RL prim wZ wB -> RL prim wA wB
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ FL prim wY wB -> RL prim wY wB
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') <- (:>) prim prim wZ wY -> Maybe ((:>) prim prim wZ wY)
forall (p :: * -> * -> *). Commute p => CommuteFn p p
commute (prim wZ wZ
p prim wZ wZ -> prim wZ wY -> (:>) prim prim wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
q)
      = (:>) (RL prim) (prim :> FL prim) wA wB -> RL prim wA wB
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 RL prim wA wZ -> prim wZ wZ -> RL prim wA wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
q' RL prim wA wZ
-> (:>) prim (FL prim) wZ wB
-> (:>) (RL prim) (prim :> FL prim) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> prim wZ wY
p' prim wZ wY -> FL prim wY wB -> (:>) prim (FL prim) wZ wB
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 RL prim wA wZ -> prim wZ wZ -> RL prim wA wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wZ
p RL prim wA wZ -> prim wZ wY -> RL prim wA wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: prim wZ wY
q RL prim wA wY -> RL prim wY wB -> RL prim wA wB
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ FL prim wY wB -> RL prim wY wB
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 :: FL (Unwound prim) wX wY -> Unwound prim wX wY
squashUnwound FL (Unwound prim) wX wY
NilFL = FL prim wX wX
-> FL prim wX wX -> RL prim wX wX -> Unwound prim wX wX
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL prim wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL RL prim wX wX
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)
  (:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
forall (prim :: * -> * -> *) wX wY.
(Show2 prim, Commute prim, Eq2 prim, Invert prim) =>
(:>) (Unwound prim) (Unwound prim) wX wY -> Unwound prim wX wY
squashPair (Unwound prim wX wY -> Unwound prim wX wY
forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToBefore Unwound prim wX wY
u Unwound prim wX wY
-> Unwound prim wY wY -> (:>) (Unwound prim) (Unwound prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> Unwound prim wY wY -> Unwound prim wY wY
forall (prim :: * -> * -> *) wA wB.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> Unwound prim wA wB
moveCommutingToAfter (FL (Unwound prim) wY wY -> Unwound prim wY wY
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 :: 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) =
  (Unwound prim wA wC -> FL prim wC wB -> Unwound prim wA wB)
-> FL prim wC wB -> Unwound prim wA wC -> Unwound prim wA wB
forall a b c. (a -> b -> c) -> b -> a -> c
flip Unwound prim wA wC -> FL prim wC wB -> Unwound prim wA wB
forall (prim :: * -> * -> *) wA wB wC.
(Commute prim, Invert prim, Eq2 prim) =>
Unwound prim wA wB -> FL prim wB wC -> Unwound prim wA wC
consAfters (RL prim wC wB -> FL prim wC wB
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL prim wC wB
after) (Unwound prim wA wC -> Unwound prim wA wB)
-> Unwound prim wA wC -> Unwound prim wA wB
forall a b. (a -> b) -> a -> b
$
  FL prim wA wB
-> FL prim wB wC -> RL prim wC wC -> Unwound prim wA wC
forall (prim :: * -> * -> *) wA wB wC wD.
FL prim wA wB
-> FL prim wB wC -> RL prim wC wD -> Unwound prim wA wD
Unwound FL prim wA wB
before FL prim wB wC
ps RL prim wC wC
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL

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