{- | 'Conflictor's a la camp.

Similar to the camp paper, but with a few differences:

* no reverse conflictors and no Invert instance

* instead we directly implement cleanMerge

* minor details of merge and commute due to bug fixes

The proofs in this module assume that whenever we create a conflictor we
maintain the following invariants:

(1) A conflictor reverts a patch in its context iff it is the first patch
    that conflicts with it. This implies that any patch a conflictor reverts
    exists in its context as an unconflicted Prim.

(2) If v depends on u and p conflicts with u then it also conflicts with v.

-}

{-# LANGUAGE ViewPatterns, PatternSynonyms #-}
module Darcs.Patch.V3.Core
    ( RepoPatchV3(..)
    , pattern PrimP
    , pattern ConflictorP
    , (+|)
    , (-|)
    ) where

import Control.Applicative ( Alternative(..) )
import Control.Monad ( guard )
import qualified Data.ByteString.Char8 as BC
import Data.List.Ordered ( nubSort )
import qualified Data.Set as S

import Darcs.Prelude

import Darcs.Patch.Commute ( commuteFL, commuteRL, commuteRLFL )
import Darcs.Patch.CommuteFn ( CommuteFn )
import Darcs.Patch.CommuteNoConflicts ( CommuteNoConflicts(..) )
import Darcs.Patch.Debug ( PatchDebug(..) )
import Darcs.Patch.FileHunk ( IsHunk(..) )
import Darcs.Patch.Format ( ListFormat(ListFormatV3) )
import Darcs.Patch.FromPrim ( ToPrim(..) )
import Darcs.Patch.Ident
    ( Ident(..)
    , PatchId
    , SignedId(..)
    , StorableId(..)
    , commuteToPrefix
    , fastRemoveFL
    , findCommonFL
    , (=\^/=)
    )
import Darcs.Patch.Invert ( Invert, invert )
import Darcs.Patch.Merge
    ( CleanMerge(..)
    , Merge(..)
    , cleanMergeFL
    , swapCleanMerge
    , swapMerge
    )
import Darcs.Patch.Prim ( PrimPatch, applyPrimFL, sortCoalesceFL )
import Darcs.Patch.Prim.WithName ( PrimWithName, wnPatch )
import Darcs.Patch.Read ( bracketedFL )
import Darcs.Patch.Repair (RepairToFL(..), Check(..) )
import Darcs.Patch.RepoPatch
    ( Apply(..)
    , Commute(..)
    , Effect(..)
    , Eq2(..)
    , PatchInspect(..)
    , PatchListFormat(..)
    , PrimPatchBase(..)
    , ReadPatch(..)
    , Summary(..)
    )
import Darcs.Patch.Show hiding ( displayPatch )
import Darcs.Patch.Summary
    ( ConflictState(..)
    , IsConflictedPrim(..)
    , plainSummary
    , plainSummaryFL
    )
import Darcs.Patch.Unwind ( Unwind(..), mkUnwound )
import Darcs.Patch.V3.Contexted
    ( Contexted
    , ctxId
    , ctxView
    , ctxNoConflict
    , ctx
    , ctxAddRL
    , ctxAddInvFL
    , ctxAddFL
    , commutePast
    , ctxToFL
    , ctxTouches
    , ctxHunkMatches
    , showCtx
    , readCtx
    )
import Darcs.Patch.Witnesses.Eq ( EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
    ( (:/\:)(..)
    , (:>)(..)
    , (:\/:)(..)
    , FL(..)
    , Fork(..)
    , (+>+)
    , mapFL
    , mapFL_FL
    , reverseFL
    , reverseRL
    )
import Darcs.Patch.Witnesses.Sealed ( Sealed(..), mapSeal, unseal )
import Darcs.Patch.Witnesses.Show ( Show1, Show2, appPrec, showsPrec2 )
import Darcs.Patch.Witnesses.Unsafe ( unsafeCoerceP1 )

import Darcs.Test.TestOnly

import Darcs.Util.Parser ( string, lexString, choice, skipSpace )
import Darcs.Util.Printer
    ( Doc
    , ($$)
    , (<+>)
    , blueText
    , redText
    , renderString
    , vcat
    )

data RepoPatchV3 name prim wX wY where
  Prim :: PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
  Conflictor :: FL (PrimWithName name prim) wX wY             -- ^ effect
             -> S.Set (Contexted (PrimWithName name prim) wY) -- ^ conflicts
             -> Contexted (PrimWithName name prim) wY         -- ^ identity
             -> RepoPatchV3 name prim wX wY

{- Naming convention: If we don't examine the contents of a RepoPatchV3, we
use @p@ (on the lhs) and @q@ (on the rhs), otherwise these names refer to
the (uncontexted) prims they represent (regardless of whether they are
conflicted or not). The components of Conflictors are named as follows: On
the lhs we use @Conflictor r x cp@, on the rhs @Conflictor s y cq@, execpt
when we have two conflictors that may have common prims in their effects. In
that case we use @com_r@ and @com_s@ for the effects and use @r@ and @s@ for
the uncommon parts (and @com@ for the common part). Primed versions always
refer to things with the same ident/name i.e. they are commuted versions of
the un-primed ones. -}

-- TODO now that we export the constructors of RepoPatchV3 these
-- pattern synonyms could probably be removed
pattern PrimP :: TestOnly => PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
pattern $mPrimP :: forall {r} {name} {prim :: * -> * -> *} {wX} {wY}.
TestOnly =>
RepoPatchV3 name prim wX wY
-> (PrimWithName name prim wX wY -> r) -> ((# #) -> r) -> r
PrimP prim <- Prim prim

pattern ConflictorP
  :: TestOnly
  => FL (PrimWithName name prim) wX wY
  -> S.Set (Contexted (PrimWithName name prim) wY)
  -> Contexted (PrimWithName name prim) wY
  -> RepoPatchV3 name prim wX wY
pattern $mConflictorP :: forall {r} {name} {prim :: * -> * -> *} {wX} {wY}.
TestOnly =>
RepoPatchV3 name prim wX wY
-> (FL (PrimWithName name prim) wX wY
    -> Set (Contexted (PrimWithName name prim) wY)
    -> Contexted (PrimWithName name prim) wY
    -> r)
-> ((# #) -> r)
-> r
ConflictorP r x cp <- Conflictor r x cp

-- * Effect

instance Effect (RepoPatchV3 name prim) where
  effect :: forall wX wY.
RepoPatchV3 name prim wX wY
-> FL (PrimOf (RepoPatchV3 name prim)) wX wY
effect (Prim PrimWithName name prim wX wY
p) = PrimWithName name prim wX wY -> prim wX wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch PrimWithName name prim wX wY
p prim wX wY -> FL prim wY wY -> FL prim wX 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
  effect (Conflictor FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
_ Contexted (PrimWithName name prim) wY
_) = (forall wW wY. PrimWithName name prim wW wY -> prim wW wY)
-> FL (PrimWithName name prim) wX wY -> FL prim 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 PrimWithName name prim wW wY -> prim wW wY
forall wW wY. PrimWithName name prim wW wY -> prim wW wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch FL (PrimWithName name prim) wX wY
r

-- * Ident

type instance PatchId (RepoPatchV3 name prim) = name

instance SignedId name => Ident (RepoPatchV3 name prim) where
  ident :: forall wX wY.
RepoPatchV3 name prim wX wY -> PatchId (RepoPatchV3 name prim)
ident (Prim PrimWithName name prim wX wY
p) = PrimWithName name prim wX wY -> PatchId (PrimWithName name prim)
forall wX wY.
PrimWithName name prim wX wY -> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident PrimWithName name prim wX wY
p
  ident (Conflictor FL (PrimWithName name prim) wX wY
_ Set (Contexted (PrimWithName name prim) wY)
_ Contexted (PrimWithName name prim) wY
cp) = Contexted (PrimWithName name prim) wY
-> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted (PrimWithName name prim) wY
cp

-- * Merge

-- We only use displayPatch for error messages here, so it makes sense
-- to use the storage format that contains the patch names.
displayPatch :: ShowPatchBasic p => p wX wY -> Doc
displayPatch :: forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch p wX wY
p = ShowPatchFor -> p wX wY -> Doc
forall wX wY. ShowPatchFor -> p wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
ForStorage p wX wY
p

instance (SignedId name, StorableId name, PrimPatch prim) =>
         CleanMerge (RepoPatchV3 name prim) where
  cleanMerge :: forall wX wY.
(:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
cleanMerge (RepoPatchV3 name prim wZ wX
p :\/: RepoPatchV3 name prim wZ wY
q)
    | RepoPatchV3 name prim wZ wX -> PatchId (RepoPatchV3 name prim)
forall wX wY.
RepoPatchV3 name prim wX wY -> PatchId (RepoPatchV3 name prim)
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident RepoPatchV3 name prim wZ wX
p name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== RepoPatchV3 name prim wZ wY -> PatchId (RepoPatchV3 name prim)
forall wX wY.
RepoPatchV3 name prim wX wY -> PatchId (RepoPatchV3 name prim)
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident RepoPatchV3 name prim wZ wY
q = [Char]
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. HasCallStack => [Char] -> a
error [Char]
"merging identical patches is undefined"
  cleanMerge (Prim PrimWithName name prim wZ wX
p :\/: Prim PrimWithName name prim wZ wY
q) = do
    PrimWithName name prim wX wZ
q' :/\: PrimWithName name prim wY wZ
p' <- (:\/:) (PrimWithName name prim) (PrimWithName name prim) wX wY
-> Maybe
     ((:/\:) (PrimWithName name prim) (PrimWithName name prim) wX wY)
forall wX wY.
(:\/:) (PrimWithName name prim) (PrimWithName name prim) wX wY
-> Maybe
     ((:/\:) (PrimWithName name prim) (PrimWithName name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (PrimWithName name prim wZ wX
p PrimWithName name prim wZ wX
-> PrimWithName name prim wZ wY
-> (:\/:) (PrimWithName name prim) (PrimWithName name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: PrimWithName name prim wZ wY
q)
    (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ PrimWithName name prim wX wZ -> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wX wZ
q' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wY wZ
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: PrimWithName name prim wY wZ -> RepoPatchV3 name prim wY wZ
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wY wZ
p'
  cleanMerge (Prim PrimWithName name prim wZ wX
p :\/: Conflictor FL (PrimWithName name prim) wZ wY
s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq) = do
    -- note: p cannot occur in y, because every element of y already
    -- exists in the history /before/ the rhs, and PatchIds must be
    -- unique in a repo
    FL (PrimWithName name prim) wX wZ
s' :/\: PrimWithName name prim wY wZ
p' <- (:\/:) (PrimWithName name prim) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:/\:)
        (FL (PrimWithName name prim)) (PrimWithName name prim) wX wY)
PartialMergeFn
  (PrimWithName name prim) (FL (PrimWithName name prim))
forall (p :: * -> * -> *). CleanMerge p => PartialMergeFn p (FL p)
cleanMergeFL (PrimWithName name prim wZ wX
p PrimWithName name prim wZ wX
-> FL (PrimWithName name prim) wZ wY
-> (:\/:)
     (PrimWithName name prim) (FL (PrimWithName name prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL (PrimWithName name prim) wZ wY
s)
    let ip' :: PrimWithName name prim wZ wY
ip' = PrimWithName name prim wY wZ -> PrimWithName name prim wZ wY
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wY wZ
p'
    Contexted (PrimWithName name prim) wZ
cq' <- PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wY
-> Maybe (Contexted (PrimWithName name prim) wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wZ wY
ip' Contexted (PrimWithName name prim) wY
cq
    Set (Contexted (PrimWithName name prim) wZ)
y' <- [Contexted (PrimWithName name prim) wZ]
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => [a] -> Set a
S.fromList ([Contexted (PrimWithName name prim) wZ]
 -> Set (Contexted (PrimWithName name prim) wZ))
-> Maybe [Contexted (PrimWithName name prim) wZ]
-> Maybe (Set (Contexted (PrimWithName name prim) wZ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Contexted (PrimWithName name prim) wY
 -> Maybe (Contexted (PrimWithName name prim) wZ))
-> [Contexted (PrimWithName name prim) wY]
-> Maybe [Contexted (PrimWithName name prim) wZ]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wY
-> Maybe (Contexted (PrimWithName name prim) wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wZ wY
ip') (Set (Contexted (PrimWithName name prim) wY)
-> [Contexted (PrimWithName name prim) wY]
forall a. Set a -> [a]
S.toList Set (Contexted (PrimWithName name prim) wY)
y)
    (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wZ
s' Set (Contexted (PrimWithName name prim) wZ)
y' Contexted (PrimWithName name prim) wZ
cq' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wY wZ
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: PrimWithName name prim wY wZ -> RepoPatchV3 name prim wY wZ
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wY wZ
p'
  cleanMerge pair :: (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair@(Conflictor {} :\/: Prim {}) = (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
swapCleanMerge (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair
  cleanMerge (Conflictor FL (PrimWithName name prim) wZ wX
com_r Set (Contexted (PrimWithName name prim) wX)
x Contexted (PrimWithName name prim) wX
cp :\/: Conflictor FL (PrimWithName name prim) wZ wY
com_s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq) =
    case FL (PrimWithName name prim) wZ wX
-> FL (PrimWithName name prim) wZ wY
-> Fork
     (FL (PrimWithName name prim))
     (FL (PrimWithName name prim))
     (FL (PrimWithName name prim))
     wZ
     wX
     wY
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ
findCommonFL FL (PrimWithName name prim) wZ wX
com_r FL (PrimWithName name prim) wZ wY
com_s of
      Fork FL (PrimWithName name prim) wZ wU
_ FL (PrimWithName name prim) wU wX
rev_r FL (PrimWithName name prim) wU wY
rev_s -> do
        FL (PrimWithName name prim) wX wZ
s' :/\: FL (PrimWithName name prim) wY wZ
r' <- (:\/:)
  (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:/\:)
        (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY)
forall wX wY.
(:\/:)
  (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:/\:)
        (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL (PrimWithName name prim) wU wX
rev_r FL (PrimWithName name prim) wU wX
-> FL (PrimWithName name prim) wU wY
-> (:\/:)
     (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL (PrimWithName name prim) wU wY
rev_s)
        -- the paper uses commutePast to calculate cp' and cq', but this must
        -- succeed (and then give the same result as adding to the context)
        -- because of the ctxNoConflict guards below
        let cp' :: Contexted (PrimWithName name prim) wZ
cp' = FL (PrimWithName name prim) wX wZ
-> Contexted (PrimWithName name prim) wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wX wZ
s' Contexted (PrimWithName name prim) wX
cp
        let cq' :: Contexted (PrimWithName name prim) wZ
cq' = FL (PrimWithName name prim) wY wZ
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wY wZ
r' Contexted (PrimWithName name prim) wY
cq
        let x' :: Set (Contexted (PrimWithName name prim) wZ)
x' = (Contexted (PrimWithName name prim) wX
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wX)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wX wZ
-> Contexted (PrimWithName name prim) wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wX wZ
s') Set (Contexted (PrimWithName name prim) wX)
x
        let y' :: Set (Contexted (PrimWithName name prim) wZ)
y' = (Contexted (PrimWithName name prim) wY
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wY wZ
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wY wZ
r') Set (Contexted (PrimWithName name prim) wY)
y
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wZ -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wZ
cq' Contexted (PrimWithName name prim) wZ
cp')
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Contexted (PrimWithName name prim) wZ -> Bool)
-> Set (Contexted (PrimWithName name prim) wZ) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wZ -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wZ
cq') (Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (Contexted (PrimWithName name prim) wZ)
x' Set (Contexted (PrimWithName name prim) wZ)
y')
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Contexted (PrimWithName name prim) wZ -> Bool)
-> Set (Contexted (PrimWithName name prim) wZ) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wZ -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wZ
cp') (Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (Contexted (PrimWithName name prim) wZ)
y' Set (Contexted (PrimWithName name prim) wZ)
x')
        (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wZ
s' Set (Contexted (PrimWithName name prim) wZ)
y' Contexted (PrimWithName name prim) wZ
cq' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wY wZ
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: FL (PrimWithName name prim) wY wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wY wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wY wZ
r' Set (Contexted (PrimWithName name prim) wZ)
x' Contexted (PrimWithName name prim) wZ
cp'

instance (SignedId name, StorableId name, PrimPatch prim) =>
         Merge (RepoPatchV3 name prim) where
  -- * no conflict
  merge :: forall wX wY.
(:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
merge (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pq | Just (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
r <- (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall wX wY.
(:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pq = (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
r
  -- * conflicting prim patches:
  -- If we have p and pull conflicting q, we make a conflictor
  -- that inverts p, conflicts with p, and represents q.
  merge (Prim PrimWithName name prim wZ wX
p :\/: Prim PrimWithName name prim wZ wY
q) =
    FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (PrimWithName name prim wZ wX -> PrimWithName name prim wX wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wX
p PrimWithName name prim wX wZ
-> FL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PrimWithName name prim) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) (Contexted (PrimWithName name prim) wZ
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. a -> Set a
S.singleton (PrimWithName name prim wZ wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wX
p)) (PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wY
q)
    RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wY wZ
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\:
    FL (PrimWithName name prim) wY wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wY wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (PrimWithName name prim wZ wY -> PrimWithName name prim wY wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wY
q PrimWithName name prim wY wZ
-> FL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PrimWithName name prim) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) (Contexted (PrimWithName name prim) wZ
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. a -> Set a
S.singleton (PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wY
q)) (PrimWithName name prim wZ wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wX
p)
  -- * prim patch p conflicting with conflictor on the rhs:
  -- The rhs is the first to conflict with p, so we must add invert p
  -- to its effect, and to its conflicts (adding invert r as context for p).
  -- For the other branch, we add a new conflictor representing p. It
  -- conflicts with q and has no effect, since q is already conflicted.
  merge (Prim PrimWithName name prim wZ wX
p :\/: Conflictor FL (PrimWithName name prim) wZ wY
r Set (Contexted (PrimWithName name prim) wY)
x Contexted (PrimWithName name prim) wY
cq) =
    FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (PrimWithName name prim wZ wX -> PrimWithName name prim wX wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wX
p PrimWithName name prim wX wZ
-> FL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PrimWithName name prim) wZ wY
r) (FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
r (PrimWithName name prim wZ wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wX
p) Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => a -> Set a -> Set a
+| Set (Contexted (PrimWithName name prim) wY)
x) Contexted (PrimWithName name prim) wY
cq
    RepoPatchV3 name prim wX wY
-> RepoPatchV3 name prim wY wY
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\:
    FL (PrimWithName name prim) wY wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wY wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL (Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
forall a. a -> Set a
S.singleton Contexted (PrimWithName name prim) wY
cq) (FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
r (PrimWithName name prim wZ wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wZ wX
p))
  -- same as previous case with both sides swapped
  merge pair :: (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair@(Conflictor {} :\/: Prim {}) = (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (p :: * -> * -> *) wX wY.
Merge p =>
(:\/:) p p wX wY -> (:/\:) p p wX wY
swapMerge (:\/:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair
  -- * conflictor c1 conflicts with conflictor c2:
  -- If we pull c2 onto c1, we remove everything common to both effects
  -- from the effect of c2 (but still remember that we conflict with them).
  -- We also record that we now conflict with c1, too, and as before keep
  -- our identity unchanged. The rest consists of adapting contexts.
  merge (lhs :: RepoPatchV3 name prim wZ wX
lhs@(Conflictor FL (PrimWithName name prim) wZ wX
com_r Set (Contexted (PrimWithName name prim) wX)
x Contexted (PrimWithName name prim) wX
cp) :\/: rhs :: RepoPatchV3 name prim wZ wY
rhs@(Conflictor FL (PrimWithName name prim) wZ wY
com_s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq)) =
    case FL (PrimWithName name prim) wZ wX
-> FL (PrimWithName name prim) wZ wY
-> Fork
     (FL (PrimWithName name prim))
     (FL (PrimWithName name prim))
     (FL (PrimWithName name prim))
     wZ
     wX
     wY
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
FL p wX wY -> FL p wX wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ
findCommonFL FL (PrimWithName name prim) wZ wX
com_r FL (PrimWithName name prim) wZ wY
com_s of
      Fork FL (PrimWithName name prim) wZ wU
_ FL (PrimWithName name prim) wU wX
r FL (PrimWithName name prim) wU wY
s ->
        case (:\/:)
  (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:/\:)
        (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY)
forall wX wY.
(:\/:)
  (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:/\:)
        (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL (PrimWithName name prim) wU wX
r FL (PrimWithName name prim) wU wX
-> FL (PrimWithName name prim) wU wY
-> (:\/:)
     (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL (PrimWithName name prim) wU wY
s) of
          Just (FL (PrimWithName name prim) wX wZ
s' :/\: FL (PrimWithName name prim) wY wZ
r') ->
            let cp' :: Contexted (PrimWithName name prim) wZ
cp' = FL (PrimWithName name prim) wX wZ
-> Contexted (PrimWithName name prim) wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wX wZ
s' Contexted (PrimWithName name prim) wX
cp
                cq' :: Contexted (PrimWithName name prim) wZ
cq' = FL (PrimWithName name prim) wY wZ
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wY wZ
r' Contexted (PrimWithName name prim) wY
cq
                x' :: Set (Contexted (PrimWithName name prim) wZ)
x' = Contexted (PrimWithName name prim) wZ
cq' Contexted (PrimWithName name prim) wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => a -> Set a -> Set a
+| (Contexted (PrimWithName name prim) wX
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wX)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wX wZ
-> Contexted (PrimWithName name prim) wX
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wX wZ
s') Set (Contexted (PrimWithName name prim) wX)
x
                y' :: Set (Contexted (PrimWithName name prim) wZ)
y' = Contexted (PrimWithName name prim) wZ
cp' Contexted (PrimWithName name prim) wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => a -> Set a -> Set a
+| (Contexted (PrimWithName name prim) wY
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wY wZ
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wY wZ
r') Set (Contexted (PrimWithName name prim) wY)
y
            in FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wZ
s' Set (Contexted (PrimWithName name prim) wZ)
y' Contexted (PrimWithName name prim) wZ
cq' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wY wZ
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a3 :: * -> * -> *) (a4 :: * -> * -> *) wX wY wZ.
a3 wX wZ -> a4 wY wZ -> (:/\:) a3 a4 wX wY
:/\: FL (PrimWithName name prim) wY wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wY wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wY wZ
r' Set (Contexted (PrimWithName name prim) wZ)
x' Contexted (PrimWithName name prim) wZ
cp'
          Maybe
  ((:/\:)
     (FL (PrimWithName name prim)) (FL (PrimWithName name prim)) wX wY)
Nothing ->
            -- Proof that this is impossible:
            --
            -- A conflictor reverts another patch only if it is the first that
            -- conflicts with it. Thus every patch it reverts is contained in
            -- its context as an unconflicted Prim patch. This holds for both
            -- lhs and rhs, which share the same context. Thus there can be no
            -- conflict between the effects of lhs and rhs. QED
            [Char]
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall a. HasCallStack => [Char] -> a
error ([Char]
 -> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
-> [Char]
-> (:/\:) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
renderString (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
redText [Char]
"uncommon effects can't be merged cleanly:"
              Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"lhs:" Doc -> Doc -> Doc
$$ RepoPatchV3 name prim wZ wX -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch RepoPatchV3 name prim wZ wX
lhs
              Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"rhs:" Doc -> Doc -> Doc
$$ RepoPatchV3 name prim wZ wY -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch RepoPatchV3 name prim wZ wY
rhs
              Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"r:" Doc -> Doc -> Doc
$$ FL (PrimWithName name prim) wU wX -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch FL (PrimWithName name prim) wU wX
r
              Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"s:" Doc -> Doc -> Doc
$$ FL (PrimWithName name prim) wU wY -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch FL (PrimWithName name prim) wU wY
s

-- * CommuteNoConflicts

instance (SignedId name, StorableId name, PrimPatch prim)
  => CommuteNoConflicts (RepoPatchV3 name prim) where

  -- The various side-conditions here include checks that the two sides
  -- are not in conflict with each other (if the rhs is a Conflictor).
  commuteNoConflicts :: forall wX wY.
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
commuteNoConflicts (Prim PrimWithName name prim wX wZ
p :> Prim PrimWithName name prim wZ wY
q) = do
    PrimWithName name prim wX wZ
q' :> PrimWithName name prim wZ wY
p' <- (:>) (PrimWithName name prim) (PrimWithName name prim) wX wY
-> Maybe
     ((:>) (PrimWithName name prim) (PrimWithName name prim) wX wY)
forall wX wY.
(:>) (PrimWithName name prim) (PrimWithName name prim) wX wY
-> Maybe
     ((:>) (PrimWithName name prim) (PrimWithName name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (PrimWithName name prim wX wZ
p PrimWithName name prim wX wZ
-> PrimWithName name prim wZ wY
-> (:>) (PrimWithName name prim) (PrimWithName name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PrimWithName name prim wZ wY
q)
    (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ PrimWithName name prim wX wZ -> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wX wZ
q' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wZ wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PrimWithName name prim wZ wY -> RepoPatchV3 name prim wZ wY
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wZ wY
p'
  commuteNoConflicts (Conflictor FL (PrimWithName name prim) wX wZ
r Set (Contexted (PrimWithName name prim) wZ)
x Contexted (PrimWithName name prim) wZ
cp :> Prim PrimWithName name prim wZ wY
q) = do
    PrimWithName name prim wX wZ
q' :> RL (PrimWithName name prim) wZ wY
r' <- (:>) (RL (PrimWithName name prim)) (PrimWithName name prim) wX wY
-> Maybe
     ((:>) (PrimWithName name prim) (RL (PrimWithName name prim)) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (FL (PrimWithName name prim) wX wZ
-> RL (PrimWithName name prim) wX wZ
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL (PrimWithName name prim) wX wZ
r RL (PrimWithName name prim) wX wZ
-> PrimWithName name prim wZ wY
-> (:>)
     (RL (PrimWithName name prim)) (PrimWithName name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PrimWithName name prim wZ wY
q)
    let iq :: PrimWithName name prim wY wZ
iq = PrimWithName name prim wZ wY -> PrimWithName name prim wY wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wY
q
    Contexted (PrimWithName name prim) wY
cp' <- PrimWithName name prim wY wZ
-> Contexted (PrimWithName name prim) wZ
-> Maybe (Contexted (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wY wZ
iq Contexted (PrimWithName name prim) wZ
cp
    Set (Contexted (PrimWithName name prim) wY)
x' <- [Contexted (PrimWithName name prim) wY]
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => [a] -> Set a
S.fromList ([Contexted (PrimWithName name prim) wY]
 -> Set (Contexted (PrimWithName name prim) wY))
-> Maybe [Contexted (PrimWithName name prim) wY]
-> Maybe (Set (Contexted (PrimWithName name prim) wY))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Contexted (PrimWithName name prim) wZ
 -> Maybe (Contexted (PrimWithName name prim) wY))
-> [Contexted (PrimWithName name prim) wZ]
-> Maybe [Contexted (PrimWithName name prim) wY]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PrimWithName name prim wY wZ
-> Contexted (PrimWithName name prim) wZ
-> Maybe (Contexted (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wY wZ
iq) (Set (Contexted (PrimWithName name prim) wZ)
-> [Contexted (PrimWithName name prim) wZ]
forall a. Set a -> [a]
S.toList Set (Contexted (PrimWithName name prim) wZ)
x)
    (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ PrimWithName name prim wX wZ -> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wX wZ
q' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wZ wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wZ wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wZ wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (RL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PrimWithName name prim) wZ wY
r') Set (Contexted (PrimWithName name prim) wY)
x' Contexted (PrimWithName name prim) wY
cp'
  -- this case is completely symmetric to the previous one
  commuteNoConflicts (Prim PrimWithName name prim wX wZ
p :> Conflictor FL (PrimWithName name prim) wZ wY
s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq) = do
    FL (PrimWithName name prim) wX wZ
s' :> PrimWithName name prim wZ wY
p' <- (:>) (PrimWithName name prim) (FL (PrimWithName name prim)) wX wY
-> Maybe
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (PrimWithName name prim wX wZ
p PrimWithName name prim wX wZ
-> FL (PrimWithName name prim) wZ wY
-> (:>)
     (PrimWithName name prim) (FL (PrimWithName name prim)) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wZ wY
s)
    Contexted (PrimWithName name prim) wZ
cq' <- PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wY
-> Maybe (Contexted (PrimWithName name prim) wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wZ wY
p' Contexted (PrimWithName name prim) wY
cq
    Set (Contexted (PrimWithName name prim) wZ)
y' <- [Contexted (PrimWithName name prim) wZ]
-> Set (Contexted (PrimWithName name prim) wZ)
forall a. Ord a => [a] -> Set a
S.fromList ([Contexted (PrimWithName name prim) wZ]
 -> Set (Contexted (PrimWithName name prim) wZ))
-> Maybe [Contexted (PrimWithName name prim) wZ]
-> Maybe (Set (Contexted (PrimWithName name prim) wZ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Contexted (PrimWithName name prim) wY
 -> Maybe (Contexted (PrimWithName name prim) wZ))
-> [Contexted (PrimWithName name prim) wY]
-> Maybe [Contexted (PrimWithName name prim) wZ]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PrimWithName name prim wZ wY
-> Contexted (PrimWithName name prim) wY
-> Maybe (Contexted (PrimWithName name prim) wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast PrimWithName name prim wZ wY
p') (Set (Contexted (PrimWithName name prim) wY)
-> [Contexted (PrimWithName name prim) wY]
forall a. Set a -> [a]
S.toList Set (Contexted (PrimWithName name prim) wY)
y)
    (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wZ
s' Set (Contexted (PrimWithName name prim) wZ)
y' Contexted (PrimWithName name prim) wZ
cq' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wZ wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> PrimWithName name prim wZ wY -> RepoPatchV3 name prim wZ wY
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wZ wY
p'
  commuteNoConflicts (Conflictor FL (PrimWithName name prim) wX wZ
com_r Set (Contexted (PrimWithName name prim) wZ)
x Contexted (PrimWithName name prim) wZ
cp :> Conflictor FL (PrimWithName name prim) wZ wY
s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq) = do
    -- com = prims in the effect of the lhs that the rhs also conflicts with;
    -- these remain on the lhs
    FL (PrimWithName name prim) wX wZ
com :> RL (PrimWithName name prim) wZ wZ
rr <- Set (PatchId (PrimWithName name prim))
-> FL (PrimWithName name prim) wX wZ
-> Maybe
     ((:>)
        (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wX wZ)
forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> FL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPrefix ((Contexted (PrimWithName name prim) wY -> name)
-> Set (Contexted (PrimWithName name prim) wY) -> Set name
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (name -> name
forall a. SignedId a => a -> a
invertId (name -> name)
-> (Contexted (PrimWithName name prim) wY -> name)
-> Contexted (PrimWithName name prim) wY
-> name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Contexted (PrimWithName name prim) wY -> name
Contexted (PrimWithName name prim) wY
-> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId) Set (Contexted (PrimWithName name prim) wY)
y) FL (PrimWithName name prim) wX wZ
com_r
    FL (PrimWithName name prim) wZ wZ
s' :> RL (PrimWithName name prim) wZ wY
rr' <- (:>)
  (RL (PrimWithName name prim)) (FL (PrimWithName name prim)) wZ wY
-> Maybe
     ((:>)
        (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (RL (PrimWithName name prim) wZ wZ
rr RL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wZ wY
-> (:>)
     (RL (PrimWithName name prim)) (FL (PrimWithName name prim)) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wZ wY
s)
    let cp' :: Contexted (PrimWithName name prim) wY
cp' = FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
s Contexted (PrimWithName name prim) wZ
cp
        cq' :: Contexted (PrimWithName name prim) wZ
cq' = RL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL (PrimWithName name prim) wZ wY
rr' Contexted (PrimWithName name prim) wY
cq
    -- obviously p and q must not conflict, nor depend on each other
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wY -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wY
cq Contexted (PrimWithName name prim) wY
cp')
    let x' :: Set (Contexted (PrimWithName name prim) wY)
x' = (Contexted (PrimWithName name prim) wZ
 -> Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
s) Set (Contexted (PrimWithName name prim) wZ)
x
        y' :: Set (Contexted (PrimWithName name prim) wZ)
y' = (Contexted (PrimWithName name prim) wY
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (RL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL (PrimWithName name prim) wZ wY
rr') Set (Contexted (PrimWithName name prim) wY)
y
    -- somewhat less obviously, p must not conflict with the patches that only
    -- q conflicts with, nor depend on them, and vice versa
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Contexted (PrimWithName name prim) wY -> Bool)
-> Set (Contexted (PrimWithName name prim) wY) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wY -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wY
cp') (Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (Contexted (PrimWithName name prim) wY)
y Set (Contexted (PrimWithName name prim) wY)
x')
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Contexted (PrimWithName name prim) wY -> Bool)
-> Set (Contexted (PrimWithName name prim) wY) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wY -> Bool
forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted (PrimWithName name prim) wY
cq) (Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => Set a -> Set a -> Set a
S.difference Set (Contexted (PrimWithName name prim) wY)
x' Set (Contexted (PrimWithName name prim) wY)
y)
    (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (FL (PrimWithName name prim) wX wZ
com FL (PrimWithName name prim) wX wZ
-> FL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PrimWithName name prim) wZ wZ
s') Set (Contexted (PrimWithName name prim) wZ)
y' Contexted (PrimWithName name prim) wZ
cq' RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wZ wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wZ wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wZ wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (RL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PrimWithName name prim) wZ wY
rr') Set (Contexted (PrimWithName name prim) wY)
x' Contexted (PrimWithName name prim) wY
cp'

-- * Commute

-- | Commute conflicting patches. These cases follow directly from merge.
commuteConflicting
  :: (SignedId name, StorableId name, PrimPatch prim)
  => CommuteFn (RepoPatchV3 name prim) (RepoPatchV3 name prim)
-- if we have a prim and a conflictor that only conflicts with that prim,
-- they trade places
-- [p] :> [p^, {:p}, :q] <-> [q] :> [q^, {:q}, :p]
commuteConflicting :: forall name (prim :: * -> * -> *) wX wY.
(SignedId name, StorableId name, PrimPatch prim) =>
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
commuteConflicting (Prim PrimWithName name prim wX wZ
p :> Conflictor (PrimWithName name prim wZ wY
ip:>:FL (PrimWithName name prim) wY wY
NilFL) Set (Contexted (PrimWithName name prim) wY)
ys cq :: Contexted (PrimWithName name prim) wY
cq@(Contexted (PrimWithName name prim) wY
-> Sealed
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (FL (PrimWithName name prim) wY wZ
NilFL :> PrimWithName name prim wZ wX
q)))
  | [Contexted (PrimWithName name prim) wY
-> Sealed
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (FL (PrimWithName name prim) wY wZ
NilFL :> PrimWithName name prim wZ wX
p')] <- Set (Contexted (PrimWithName name prim) wY)
-> [Contexted (PrimWithName name prim) wY]
forall a. Set a -> [a]
S.toList Set (Contexted (PrimWithName name prim) wY)
ys
  , EqCheck wX wY
IsEq <- PrimWithName name prim wX wZ -> PrimWithName name prim wZ wX
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wX wZ
p PrimWithName name prim wZ wX
-> PrimWithName name prim wZ wY -> EqCheck wX wY
forall wA wB wC.
PrimWithName name prim wA wB
-> PrimWithName name prim wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= PrimWithName name prim wZ wY
ip
  , EqCheck wZ wX
IsEq <- PrimWithName name prim wX wZ
p PrimWithName name prim wX wZ
-> PrimWithName name prim wX wX -> EqCheck wZ wX
forall wA wB wC.
PrimWithName name prim wA wB
-> PrimWithName name prim wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= PrimWithName name prim wX wX
PrimWithName name prim wZ wX
p' =
      (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
Just (PrimWithName name prim wX wX -> RepoPatchV3 name prim wX wX
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wX wX
PrimWithName name prim wZ wX
q RepoPatchV3 name prim wX wX
-> RepoPatchV3 name prim wX wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (PrimWithName name prim wZ wX -> PrimWithName name prim wX wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wX
q PrimWithName name prim wX wZ
-> FL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PrimWithName name prim) wZ wY
FL (PrimWithName name prim) wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) (Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
forall a. a -> Set a
S.singleton Contexted (PrimWithName name prim) wY
cq) (PrimWithName name prim wY wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wX wZ
PrimWithName name prim wY wZ
p))
-- similar to above case: a prim and a conflictor that conflicts with the prim
-- but also conflicts with other patches
-- [p] :> [p^ s, {s^:p} U Y, cq] <-> [s, Y, cq] :> [, {cq}, s^:p]
commuteConflicting (Prim PrimWithName name prim wX wZ
p :> Conflictor FL (PrimWithName name prim) wZ wY
s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq)
  | PrimWithName name prim wX wZ -> PatchId (PrimWithName name prim)
forall wX wY.
PrimWithName name prim wX wY -> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident PrimWithName name prim wX wZ
p name -> Set name -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` (Contexted (PrimWithName name prim) wY -> name)
-> Set (Contexted (PrimWithName name prim) wY) -> Set name
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Contexted (PrimWithName name prim) wY -> name
Contexted (PrimWithName name prim) wY
-> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Set (Contexted (PrimWithName name prim) wY)
y =
      case PrimWithName name prim wZ wX
-> FL (PrimWithName name prim) wZ wY
-> Maybe (FL (PrimWithName name prim) wX wY)
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL (PrimWithName name prim wX wZ -> PrimWithName name prim wZ wX
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wX wZ
p) FL (PrimWithName name prim) wZ wY
s of
        Maybe (FL (PrimWithName name prim) wX wY)
Nothing ->
          -- Proof that this is impossible:
          --
          -- The case assumption (that p is in conflict with q) together
          -- with the fact that the rhs is obviously the first patch that
          -- conflicts with the lhs, imply that p^ is contained in s. It
          -- remains to be shown that p^ does not depend on any prim contained
          -- in s. Suppose there were such a prim, then p would be in conflict
          -- with it, which means p would have to be a conflictor. QED
          [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. HasCallStack => [Char] -> a
error ([Char]
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
renderString
            (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
redText [Char]
"commuteConflicting: cannot remove (invert lhs):"
            Doc -> Doc -> Doc
$$ PrimWithName name prim wZ wX -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch (PrimWithName name prim wX wZ -> PrimWithName name prim wZ wX
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wX wZ
p)
            Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"from effect of rhs:"
            Doc -> Doc -> Doc
$$ FL (PrimWithName name prim) wZ wY -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch FL (PrimWithName name prim) wZ wY
s
        Just FL (PrimWithName name prim) wX wY
r ->
          let cp :: Contexted (PrimWithName name prim) wY
cp = FL (PrimWithName name prim) wX wY
-> Contexted (PrimWithName name prim) wX
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wX wY
r (PrimWithName name prim wX wZ
-> Contexted (PrimWithName name prim) wX
forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx PrimWithName name prim wX wZ
p)
          in (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
Just (FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wY
r (Contexted (PrimWithName name prim) wY
cp Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => a -> Set a -> Set a
-| Set (Contexted (PrimWithName name prim) wY)
y) Contexted (PrimWithName name prim) wY
cq RepoPatchV3 name prim wX wY
-> RepoPatchV3 name prim wY wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wY wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wY wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL (Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
forall a. a -> Set a
S.singleton Contexted (PrimWithName name prim) wY
cq) Contexted (PrimWithName name prim) wY
cp)
-- if we have two conflictors where the rhs conflicts /only/ with the lhs,
-- the latter becomes a prim patch
-- [r, X, cp] [, {cp}, r^:q] <-> [q] [q^r, {r^:q} U X, cp]
commuteConflicting (lhs :: RepoPatchV3 name prim wX wZ
lhs@(Conflictor FL (PrimWithName name prim) wX wZ
r Set (Contexted (PrimWithName name prim) wZ)
x Contexted (PrimWithName name prim) wZ
cp) :> rhs :: RepoPatchV3 name prim wZ wY
rhs@(Conflictor FL (PrimWithName name prim) wZ wY
NilFL Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq))
  | Set (Contexted (PrimWithName name prim) wY)
y Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY) -> Bool
forall a. Eq a => a -> a -> Bool
== Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
forall a. a -> Set a
S.singleton Contexted (PrimWithName name prim) wY
Contexted (PrimWithName name prim) wZ
cp =
      case Contexted (PrimWithName name prim) wX
-> Sealed
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wX)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView (FL (PrimWithName name prim) wX wZ
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wX
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL FL (PrimWithName name prim) wX wZ
r Contexted (PrimWithName name prim) wY
Contexted (PrimWithName name prim) wZ
cq) of
        Sealed (FL (PrimWithName name prim) wX wZ
NilFL :> PrimWithName name prim wZ wX
q') ->
          (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
Just ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ PrimWithName name prim wX wX -> RepoPatchV3 name prim wX wX
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim PrimWithName name prim wX wX
PrimWithName name prim wZ wX
q' RepoPatchV3 name prim wX wX
-> RepoPatchV3 name prim wX wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (PrimWithName name prim wZ wX -> PrimWithName name prim wX wZ
forall wX wY.
PrimWithName name prim wX wY -> PrimWithName name prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert PrimWithName name prim wZ wX
q' PrimWithName name prim wX wZ
-> FL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL (PrimWithName name prim) wX wZ
FL (PrimWithName name prim) wZ wY
r) (Contexted (PrimWithName name prim) wY
cq Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => a -> Set a -> Set a
+| Set (Contexted (PrimWithName name prim) wY)
Set (Contexted (PrimWithName name prim) wZ)
x) Contexted (PrimWithName name prim) wY
Contexted (PrimWithName name prim) wZ
cp
        Sealed (FL (PrimWithName name prim) wX wZ
c' :> PrimWithName name prim wZ wX
_) ->
          -- Proof that this is impossible:
          --
          -- First, it must be true that commutePastFL r cq = Just cq'. For if
          -- not, then there would be a conflict between the rhs and one of the
          -- prims that the lhs reverts, in contradiction to our case
          -- assumption that the rhs conflicts only with the lhs.
          --
          -- Second, suppose that cq' has residual nonempty context. That means
          -- there is a patch x in the history that the rhs depends on, and
          -- which is in conflict with at least one other patch y in our
          -- history (the history being the patches that precede the lhs);
          -- because otherwise cq' appended to the history would be a sequence
          -- that contains x twice without an intermediate revert. But then the
          -- rhs would also have to conflict with the patch x, again in
          -- contradiction to our case assumption. QED
          [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. HasCallStack => [Char] -> a
error ([Char]
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
renderString (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
redText [Char]
"remaining context in commute:"
            Doc -> Doc -> Doc
$$ FL (PrimWithName name prim) wX wZ -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch FL (PrimWithName name prim) wX wZ
c'
            Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"lhs:" Doc -> Doc -> Doc
$$ RepoPatchV3 name prim wX wZ -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch RepoPatchV3 name prim wX wZ
lhs
            Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"rhs:" Doc -> Doc -> Doc
$$ RepoPatchV3 name prim wZ wY -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch RepoPatchV3 name prim wZ wY
rhs
-- conflicting conflictors where the rhs conflicts with lhs but
-- also conflicts with other patches
-- [com r, X, cp] [s, y=({s^cp} U Y'), cq] <-> [com s', r'Y', r'cq] [r', {cq} U s^X, s^cp]
commuteConflicting (Conflictor FL (PrimWithName name prim) wX wZ
com_r Set (Contexted (PrimWithName name prim) wZ)
x Contexted (PrimWithName name prim) wZ
cp :> Conflictor FL (PrimWithName name prim) wZ wY
s Set (Contexted (PrimWithName name prim) wY)
y Contexted (PrimWithName name prim) wY
cq)
  | let cp' :: Contexted (PrimWithName name prim) wY
cp' = FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
s Contexted (PrimWithName name prim) wZ
cp
  , Contexted (PrimWithName name prim) wY
cp' Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Contexted (PrimWithName name prim) wY)
y
  , let y' :: Set (Contexted (PrimWithName name prim) wY)
y' = Contexted (PrimWithName name prim) wY
cp' Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => a -> Set a -> Set a
-| Set (Contexted (PrimWithName name prim) wY)
y =
      case Set (PatchId (PrimWithName name prim))
-> FL (PrimWithName name prim) wX wZ
-> Maybe
     ((:>)
        (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wX wZ)
forall (p :: * -> * -> *) wX wY.
(Commute p, Ident p) =>
Set (PatchId p) -> FL p wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteToPrefix ((Contexted (PrimWithName name prim) wY -> name)
-> Set (Contexted (PrimWithName name prim) wY) -> Set name
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (name -> name
forall a. SignedId a => a -> a
invertId (name -> name)
-> (Contexted (PrimWithName name prim) wY -> name)
-> Contexted (PrimWithName name prim) wY
-> name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Contexted (PrimWithName name prim) wY -> name
Contexted (PrimWithName name prim) wY
-> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId) Set (Contexted (PrimWithName name prim) wY)
y') FL (PrimWithName name prim) wX wZ
com_r of
        Maybe
  ((:>)
     (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wX wZ)
Nothing ->
          -- Proof that the above commute must suceed:
          --
          -- Let u and v be prims that the lhs reverts, and suppose v also
          -- conflicts with the rhs. If v^ depends on u^, then u depends on v
          -- and thus u also conflicts with the rhs. Thus any v^ in com_r such
          -- that v conflicts with the rhs can depend only on other elements of
          -- com_r that also conflict with the rhs. QED
          [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. HasCallStack => [Char] -> a
error [Char]
"commuteConflicting: cannot commute common effects"
        Just (FL (PrimWithName name prim) wX wZ
com :> RL (PrimWithName name prim) wZ wZ
rr) ->
          case (:>)
  (RL (PrimWithName name prim)) (FL (PrimWithName name prim)) wZ wY
-> Maybe
     ((:>)
        (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) (FL p) wX wY -> Maybe ((:>) (FL p) (RL p) wX wY)
commuteRLFL (RL (PrimWithName name prim) wZ wZ
rr RL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wZ wY
-> (:>)
     (RL (PrimWithName name prim)) (FL (PrimWithName name prim)) wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL (PrimWithName name prim) wZ wY
s) of
            Maybe
  ((:>)
     (FL (PrimWithName name prim)) (RL (PrimWithName name prim)) wZ wY)
Nothing ->
              -- Proof that the above commute must succeed:
              --
              -- This is equivalent to the statement: a prim v that conflicts
              -- only with the lhs cannot depend on another prim u that
              -- conflicts only with the rhs. Again, this is a consequence of
              -- the fact that if v depends on u and u conflicts with q, then v
              -- must also conflict with q.
              [Char]
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. HasCallStack => [Char] -> a
error [Char]
"commuteConflicting: cannot commute uncommon effects"
            Just (FL (PrimWithName name prim) wZ wZ
s' :> RL (PrimWithName name prim) wZ wY
rr') ->
              (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. a -> Maybe a
Just ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
 -> Maybe
      ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY))
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a b. (a -> b) -> a -> b
$
                FL (PrimWithName name prim) wX wZ
-> Set (Contexted (PrimWithName name prim) wZ)
-> Contexted (PrimWithName name prim) wZ
-> RepoPatchV3 name prim wX wZ
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (FL (PrimWithName name prim) wX wZ
com FL (PrimWithName name prim) wX wZ
-> FL (PrimWithName name prim) wZ wZ
-> FL (PrimWithName name prim) wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL (PrimWithName name prim) wZ wZ
s') ((Contexted (PrimWithName name prim) wY
 -> Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (RL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL (PrimWithName name prim) wZ wY
rr') Set (Contexted (PrimWithName name prim) wY)
y') (RL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wY
-> Contexted (PrimWithName name prim) wZ
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL (PrimWithName name prim) wZ wY
rr' Contexted (PrimWithName name prim) wY
cq)
                RepoPatchV3 name prim wX wZ
-> RepoPatchV3 name prim wZ wY
-> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:>
                FL (PrimWithName name prim) wZ wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wZ wY
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor (RL (PrimWithName name prim) wZ wY
-> FL (PrimWithName name prim) wZ wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL (PrimWithName name prim) wZ wY
rr') (Contexted (PrimWithName name prim) wY
cq Contexted (PrimWithName name prim) wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wY)
forall a. Ord a => a -> Set a -> Set a
+| (Contexted (PrimWithName name prim) wZ
 -> Contexted (PrimWithName name prim) wY)
-> Set (Contexted (PrimWithName name prim) wZ)
-> Set (Contexted (PrimWithName name prim) wY)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (FL (PrimWithName name prim) wZ wY
-> Contexted (PrimWithName name prim) wZ
-> Contexted (PrimWithName name prim) wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL FL (PrimWithName name prim) wZ wY
s) Set (Contexted (PrimWithName name prim) wZ)
x) Contexted (PrimWithName name prim) wY
cp'
commuteConflicting (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
_ = Maybe ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. Maybe a
Nothing

instance (SignedId name, StorableId name, PrimPatch prim) =>
         Commute (RepoPatchV3 name prim) where
  commute :: forall wX wY.
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
commute (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair = (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall wX wY.
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall name (prim :: * -> * -> *) wX wY.
(SignedId name, StorableId name, PrimPatch prim) =>
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
commuteConflicting (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair Maybe ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall wX wY.
(:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
-> Maybe
     ((:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY)
forall (p :: * -> * -> *) wX wY.
CommuteNoConflicts p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commuteNoConflicts (:>) (RepoPatchV3 name prim) (RepoPatchV3 name prim) wX wY
pair

-- * PatchInspect

-- Note: in contrast to RepoPatchV2 we do not look at the list of conflicts
-- here. I see no reason why we should: the conflicts are only needed for the
-- instance Commute. We do however look at the patches that we undo.
instance PatchInspect prim => PatchInspect (RepoPatchV3 name prim) where
  listTouchedFiles :: forall wX wY. RepoPatchV3 name prim wX wY -> [AnchoredPath]
listTouchedFiles (Prim PrimWithName name prim wX wY
p) = PrimWithName name prim wX wY -> [AnchoredPath]
forall wX wY. PrimWithName name prim wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles PrimWithName name prim wX wY
p
  listTouchedFiles (Conflictor FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
_ Contexted (PrimWithName name prim) wY
cp) =
    [AnchoredPath] -> [AnchoredPath]
forall a. Ord a => [a] -> [a]
nubSort ([AnchoredPath] -> [AnchoredPath])
-> [AnchoredPath] -> [AnchoredPath]
forall a b. (a -> b) -> a -> b
$ [[AnchoredPath]] -> [AnchoredPath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((forall wX wY. PrimWithName name prim wX wY -> [AnchoredPath])
-> FL (PrimWithName name prim) wX wY -> [[AnchoredPath]]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL PrimWithName name prim wW wZ -> [AnchoredPath]
forall wX wY. PrimWithName name prim wX wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles FL (PrimWithName name prim) wX wY
r) [AnchoredPath] -> [AnchoredPath] -> [AnchoredPath]
forall a. [a] -> [a] -> [a]
++ Contexted (PrimWithName name prim) wY -> [AnchoredPath]
forall (p :: * -> * -> *) wX.
PatchInspect p =>
Contexted p wX -> [AnchoredPath]
ctxTouches Contexted (PrimWithName name prim) wY
cp
  hunkMatches :: forall wX wY.
(ByteString -> Bool) -> RepoPatchV3 name prim wX wY -> Bool
hunkMatches ByteString -> Bool
f (Prim PrimWithName name prim wX wY
p) = (ByteString -> Bool) -> PrimWithName name prim wX wY -> Bool
forall wX wY.
(ByteString -> Bool) -> PrimWithName name prim wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f PrimWithName name prim wX wY
p
  hunkMatches ByteString -> Bool
f (Conflictor FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
_ Contexted (PrimWithName name prim) wY
cp) = (ByteString -> Bool) -> FL (PrimWithName name prim) wX wY -> Bool
forall wX wY.
(ByteString -> Bool) -> FL (PrimWithName name prim) wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f FL (PrimWithName name prim) wX wY
r Bool -> Bool -> Bool
|| (ByteString -> Bool)
-> Contexted (PrimWithName name prim) wY -> Bool
forall (p :: * -> * -> *) wX.
PatchInspect p =>
(ByteString -> Bool) -> Contexted p wX -> Bool
ctxHunkMatches ByteString -> Bool
f Contexted (PrimWithName name prim) wY
cp

-- * Boilerplate instances

instance (SignedId name, Eq2 prim, Commute prim) => Eq2 (RepoPatchV3 name prim) where
    (Prim PrimWithName name prim wA wB
p) =\/= :: forall wA wB wC.
RepoPatchV3 name prim wA wB
-> RepoPatchV3 name prim wA wC -> EqCheck wB wC
=\/= (Prim PrimWithName name prim wA wC
q) = PrimWithName name prim wA wB
p PrimWithName name prim wA wB
-> PrimWithName name prim wA wC -> EqCheck wB wC
forall wA wB wC.
PrimWithName name prim wA wB
-> PrimWithName name prim wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= PrimWithName name prim wA wC
q
    (Conflictor FL (PrimWithName name prim) wA wB
r Set (Contexted (PrimWithName name prim) wB)
x Contexted (PrimWithName name prim) wB
cp) =\/= (Conflictor FL (PrimWithName name prim) wA wC
s Set (Contexted (PrimWithName name prim) wC)
y Contexted (PrimWithName name prim) wC
cq)
        | EqCheck wB wC
IsEq <- FL (PrimWithName name prim) wA wB
r FL (PrimWithName name prim) wA wB
-> FL (PrimWithName name prim) wA wC -> EqCheck wB wC
forall (p :: * -> * -> *) wA wB wC.
Ident p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\^/= FL (PrimWithName name prim) wA wC
s -- more efficient than IsEq <- r =\/= s
        , Set (Contexted (PrimWithName name prim) wB)
x Set (Contexted (PrimWithName name prim) wB)
-> Set (Contexted (PrimWithName name prim) wB) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (Contexted (PrimWithName name prim) wB)
Set (Contexted (PrimWithName name prim) wC)
y
        , Contexted (PrimWithName name prim) wB
cp Contexted (PrimWithName name prim) wB
-> Contexted (PrimWithName name prim) wB -> Bool
forall a. Eq a => a -> a -> Bool
== Contexted (PrimWithName name prim) wB
Contexted (PrimWithName name prim) wC
cq = EqCheck wB wB
EqCheck wB wC
forall wA. EqCheck wA wA
IsEq
    RepoPatchV3 name prim wA wB
_ =\/= RepoPatchV3 name prim wA wC
_ = EqCheck wB wC
forall wA wB. EqCheck wA wB
NotEq

instance (Show name, Show2 prim) => Show (RepoPatchV3 name prim wX wY) where
  showsPrec :: Int -> RepoPatchV3 name prim wX wY -> ShowS
showsPrec Int
d RepoPatchV3 name prim wX wY
rp = 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
$
    case RepoPatchV3 name prim wX wY
rp of
      Prim PrimWithName name prim wX wY
prim ->
        [Char] -> ShowS
showString [Char]
"Prim " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> PrimWithName name 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) PrimWithName name prim wX wY
prim
      Conflictor FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
x Contexted (PrimWithName name prim) wY
cp -> [Char] -> ShowS
showString [Char]
"Conflictor " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> ShowS
forall {a} {a} {a}.
(Show a, Show a, Show a) =>
a -> a -> a -> ShowS
showContent FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
x Contexted (PrimWithName name prim) wY
cp
    where
      showContent :: a -> a -> a -> ShowS
showContent a
r a
x a
cp =
        Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
r ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          [Char] -> ShowS
showString [Char]
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
          [Char] -> ShowS
showString [Char]
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
cp

instance (Show name, Show2 prim) => Show1 (RepoPatchV3 name prim wX)

instance (Show name, Show2 prim) => Show2 (RepoPatchV3 name prim)

instance PrimPatch prim => PrimPatchBase (RepoPatchV3 name prim) where
  type PrimOf (RepoPatchV3 name prim) = prim

instance ToPrim (RepoPatchV3 name prim) where
  toPrim :: forall wX wY.
RepoPatchV3 name prim wX wY
-> Maybe (PrimOf (RepoPatchV3 name prim) wX wY)
toPrim (Conflictor {}) = Maybe (prim wX wY)
Maybe (PrimOf (RepoPatchV3 name prim) wX wY)
forall a. Maybe a
Nothing
  toPrim (Prim PrimWithName name prim wX wY
p) = prim wX wY -> Maybe (prim wX wY)
forall a. a -> Maybe a
Just (PrimWithName name prim wX wY -> prim wX wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch PrimWithName name prim wX wY
p)

instance PatchDebug prim => PatchDebug (RepoPatchV3 name prim)

instance PrimPatch prim => Apply (RepoPatchV3 name prim) where
  type ApplyState (RepoPatchV3 name prim) = ApplyState prim
  apply :: forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState (RepoPatchV3 name prim)) m =>
RepoPatchV3 name prim wX wY -> m ()
apply = FL prim wX wY -> m ()
forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState prim) m =>
FL prim wX wY -> m ()
forall (prim :: * -> * -> *) (m :: * -> *) wX wY.
(PrimApply prim, ApplyMonad (ApplyState prim) m) =>
FL prim wX wY -> m ()
applyPrimFL (FL prim wX wY -> m ())
-> (RepoPatchV3 name prim wX wY -> FL prim wX wY)
-> RepoPatchV3 name prim wX wY
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RepoPatchV3 name prim wX wY -> FL prim wX wY
RepoPatchV3 name prim wX wY
-> FL (PrimOf (RepoPatchV3 name prim)) wX wY
forall wX wY.
RepoPatchV3 name prim wX wY
-> FL (PrimOf (RepoPatchV3 name prim)) wX wY
forall (p :: * -> * -> *) wX wY.
Effect p =>
p wX wY -> FL (PrimOf p) wX wY
effect
  unapply :: forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState (RepoPatchV3 name prim)) m =>
RepoPatchV3 name prim wX wY -> m ()
unapply = FL prim wY wX -> m ()
forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState prim) m =>
FL prim wX wY -> m ()
forall (prim :: * -> * -> *) (m :: * -> *) wX wY.
(PrimApply prim, ApplyMonad (ApplyState prim) m) =>
FL prim wX wY -> m ()
applyPrimFL (FL prim wY wX -> m ())
-> (RepoPatchV3 name prim wX wY -> FL prim wY wX)
-> RepoPatchV3 name prim wX wY
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL prim wX wY -> FL prim wY wX
forall wX wY. FL prim wX wY -> FL prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert (FL prim wX wY -> FL prim wY wX)
-> (RepoPatchV3 name prim wX wY -> FL prim wX wY)
-> RepoPatchV3 name prim wX wY
-> FL prim wY wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RepoPatchV3 name prim wX wY -> FL prim wX wY
RepoPatchV3 name prim wX wY
-> FL (PrimOf (RepoPatchV3 name prim)) wX wY
forall wX wY.
RepoPatchV3 name prim wX wY
-> FL (PrimOf (RepoPatchV3 name prim)) wX wY
forall (p :: * -> * -> *) wX wY.
Effect p =>
p wX wY -> FL (PrimOf p) wX wY
effect

instance PatchListFormat (RepoPatchV3 name prim) where
  patchListFormat :: ListFormat (RepoPatchV3 name prim)
patchListFormat = ListFormat (RepoPatchV3 name prim)
forall (p :: * -> * -> *). ListFormat p
ListFormatV3

instance IsHunk prim => IsHunk (RepoPatchV3 name prim) where
  isHunk :: forall wX wY.
RepoPatchV3 name prim wX wY
-> Maybe (FileHunk (ObjectIdOfPatch (RepoPatchV3 name prim)) wX wY)
isHunk RepoPatchV3 name prim wX wY
rp = do
    Prim PrimWithName name prim wX wY
p <- RepoPatchV3 name prim wX wY -> Maybe (RepoPatchV3 name prim wX wY)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return RepoPatchV3 name prim wX wY
rp
    PrimWithName name prim wX wY
-> Maybe
     (FileHunk (ObjectIdOfPatch (PrimWithName name prim)) wX wY)
forall wX wY.
PrimWithName name prim wX wY
-> Maybe
     (FileHunk (ObjectIdOfPatch (PrimWithName name prim)) wX wY)
forall (p :: * -> * -> *) wX wY.
IsHunk p =>
p wX wY -> Maybe (FileHunk (ObjectIdOfPatch p) wX wY)
isHunk PrimWithName name prim wX wY
p

instance Summary (RepoPatchV3 name prim) where
  conflictedEffect :: forall wX wY.
RepoPatchV3 name prim wX wY
-> [IsConflictedPrim (PrimOf (RepoPatchV3 name prim))]
conflictedEffect (Conflictor FL (PrimWithName name prim) wX wY
_ Set (Contexted (PrimWithName name prim) wY)
_ (Contexted (PrimWithName name prim) wY
-> Sealed
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (FL (PrimWithName name prim) wY wZ
_ :> PrimWithName name prim wZ wX
p))) = [ConflictState -> prim wZ wX -> IsConflictedPrim prim
forall (prim :: * -> * -> *) wX wY.
ConflictState -> prim wX wY -> IsConflictedPrim prim
IsC ConflictState
Conflicted (PrimWithName name prim wZ wX -> prim wZ wX
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch PrimWithName name prim wZ wX
p)]
  conflictedEffect (Prim PrimWithName name prim wX wY
p) = [ConflictState -> prim wX wY -> IsConflictedPrim prim
forall (prim :: * -> * -> *) wX wY.
ConflictState -> prim wX wY -> IsConflictedPrim prim
IsC ConflictState
Okay (PrimWithName name prim wX wY -> prim wX wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch PrimWithName name prim wX wY
p)]

instance (Invert prim, Commute prim, Eq2 prim) => Unwind (RepoPatchV3 name prim) where
  fullUnwind :: forall wX wY.
RepoPatchV3 name prim wX wY
-> Unwound (PrimOf (RepoPatchV3 name prim)) wX wY
fullUnwind (Prim PrimWithName name prim wX wY
p)
    = FL prim wX wX
-> FL prim wX wY -> FL prim wY wY -> Unwound prim wX wY
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 wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL (PrimWithName name prim wX wY -> prim wX wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch PrimWithName name prim wX wY
p prim wX wY -> FL prim wY wY -> FL prim wX 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 wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
  fullUnwind
    (Conflictor
      ((forall wW wY. PrimWithName name prim wW wY -> prim wW wY)
-> FL (PrimWithName name prim) wX wY -> FL prim 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 PrimWithName name prim wW wY -> prim wW wY
forall wW wY. PrimWithName name prim wW wY -> prim wW wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch -> FL prim wX wY
es)
      Set (Contexted (PrimWithName name prim) wY)
_
      (Contexted (PrimWithName name prim) wY
-> Sealed
     ((:>) (FL (PrimWithName name prim)) (PrimWithName name prim) wY)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (((forall wW wY. PrimWithName name prim wW wY -> prim wW wY)
-> FL (PrimWithName name prim) wY wZ -> FL prim wY 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 PrimWithName name prim wW wY -> prim wW wY
forall wW wY. PrimWithName name prim wW wY -> prim wW wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch -> FL prim wY wZ
cs) :> (PrimWithName name prim wZ wX -> prim wZ wX
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch -> prim wZ wX
i)))
    ) =
    FL prim wX wZ
-> FL prim wZ wX -> FL prim wX wY -> Unwound prim wX wY
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 wX wY
es FL prim wX wY -> FL prim wY wZ -> FL prim wX wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wY wZ
cs)
      (prim wZ wX
i prim wZ wX -> FL prim wX wX -> FL prim wZ wX
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL prim wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
      (prim wZ wX -> prim wX wZ
forall wX wY. prim wX wY -> prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert prim wZ wX
i 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
:>: FL prim wY wZ -> FL prim wZ wY
forall wX wY. FL prim wX wY -> FL prim wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert FL prim wY wZ
cs FL prim wZ wY -> FL prim wY wY -> FL prim wZ wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL prim wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)

-- * More boilerplate instances

instance PrimPatch prim => Check (RepoPatchV3 name prim)
  -- use the default implementation for method isInconsistent

instance PrimPatch prim => RepairToFL (RepoPatchV3 name prim)
  -- use the default implementation for method applyAndTryToFixFL

instance (SignedId name, StorableId name, PrimPatch prim)
  => ShowPatch (RepoPatchV3 name prim) where

  summary :: forall wX wY. RepoPatchV3 name prim wX wY -> Doc
summary = RepoPatchV3 name prim wX wY -> Doc
forall (e :: * -> * -> *) wX wY.
(Summary e, PrimDetails (PrimOf e)) =>
e wX wY -> Doc
plainSummary
  summaryFL :: forall wX wY. FL (RepoPatchV3 name prim) wX wY -> Doc
summaryFL = FL (RepoPatchV3 name prim) wX wY -> Doc
forall (e :: * -> * -> *) wX wY.
(Summary e, PrimDetails (PrimOf e)) =>
FL e wX wY -> Doc
plainSummaryFL
  thing :: forall wX wY. RepoPatchV3 name prim wX wY -> [Char]
thing RepoPatchV3 name prim wX wY
_ = [Char]
"change"

instance (SignedId name, StorableId name, PrimPatch prim)
  => ShowContextPatch (RepoPatchV3 name prim) where

  showPatchWithContextAndApply :: forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState (RepoPatchV3 name prim)) m =>
ShowPatchFor -> RepoPatchV3 name prim wX wY -> m Doc
showPatchWithContextAndApply ShowPatchFor
f (Prim PrimWithName name prim wX wY
p) = ShowPatchFor -> PrimWithName name prim wX wY -> m Doc
forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState (PrimWithName name prim)) m =>
ShowPatchFor -> PrimWithName name prim wX wY -> m Doc
forall (p :: * -> * -> *) (m :: * -> *) wX wY.
(ShowContextPatch p, ApplyMonad (ApplyState p) m) =>
ShowPatchFor -> p wX wY -> m Doc
showPatchWithContextAndApply ShowPatchFor
f PrimWithName name prim wX wY
p
  showPatchWithContextAndApply ShowPatchFor
f RepoPatchV3 name prim wX wY
p = RepoPatchV3 name prim wX wY -> m ()
forall (m :: * -> *) wX wY.
ApplyMonad (ApplyState (RepoPatchV3 name prim)) m =>
RepoPatchV3 name prim wX wY -> m ()
forall (p :: * -> * -> *) (m :: * -> *) wX wY.
(Apply p, ApplyMonad (ApplyState p) m) =>
p wX wY -> m ()
apply RepoPatchV3 name prim wX wY
p m () -> m Doc -> m Doc
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ShowPatchFor -> RepoPatchV3 name prim wX wY -> Doc
forall wX wY. ShowPatchFor -> RepoPatchV3 name prim wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f RepoPatchV3 name prim wX wY
p)

-- * Read and Write

instance (SignedId name, StorableId name, PrimPatch prim)
  => ReadPatch (RepoPatchV3 name prim) where

  readPatch' :: forall wX. Parser (Sealed (RepoPatchV3 name prim wX))
readPatch' = do
    Parser ()
skipSpace
    [Parser (Sealed (RepoPatchV3 name prim wX))]
-> Parser (Sealed (RepoPatchV3 name prim wX))
forall (f :: * -> *) a. Alternative f => [f a] -> f a
choice
      [ do ByteString -> Parser ()
string ([Char] -> ByteString
BC.pack [Char]
"conflictor")
           (Sealed FL (PrimWithName name prim) wX wX
r, Set (Contexted (PrimWithName name prim) Any)
x, Contexted (PrimWithName name prim) Any
p) <- Parser
  ByteString
  (Sealed (FL (PrimWithName name prim) wX),
   Set (Contexted (PrimWithName name prim) Any),
   Contexted (PrimWithName name prim) Any)
forall {wX} {wX} {wX}.
Parser
  ByteString
  (Sealed (FL (PrimWithName name prim) wX),
   Set (Contexted (PrimWithName name prim) wX),
   Contexted (PrimWithName name prim) wX)
readContent
           Sealed (RepoPatchV3 name prim wX)
-> Parser (Sealed (RepoPatchV3 name prim wX))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (RepoPatchV3 name prim wX wX -> Sealed (RepoPatchV3 name prim wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL (PrimWithName name prim) wX wX
-> Set (Contexted (PrimWithName name prim) wX)
-> Contexted (PrimWithName name prim) wX
-> RepoPatchV3 name prim wX wX
forall name (prim :: * -> * -> *) wX wY.
FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> RepoPatchV3 name prim wX wY
Conflictor FL (PrimWithName name prim) wX wX
r ((Contexted (PrimWithName name prim) Any
 -> Contexted (PrimWithName name prim) wX)
-> Set (Contexted (PrimWithName name prim) Any)
-> Set (Contexted (PrimWithName name prim) wX)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Contexted (PrimWithName name prim) Any
-> Contexted (PrimWithName name prim) wX
forall (a :: * -> *) wX wY. a wX -> a wY
unsafeCoerceP1 Set (Contexted (PrimWithName name prim) Any)
x) (Contexted (PrimWithName name prim) Any
-> Contexted (PrimWithName name prim) wX
forall (a :: * -> *) wX wY. a wX -> a wY
unsafeCoerceP1 Contexted (PrimWithName name prim) Any
p)))
      , do (forall wX.
 PrimWithName name prim wX wX -> RepoPatchV3 name prim wX wX)
-> Sealed (PrimWithName name prim wX)
-> Sealed (RepoPatchV3 name prim wX)
forall (a :: * -> *) (b :: * -> *).
(forall wX. a wX -> b wX) -> Sealed a -> Sealed b
mapSeal PrimWithName name prim wX wX -> RepoPatchV3 name prim wX wX
forall wX.
PrimWithName name prim wX wX -> RepoPatchV3 name prim wX wX
forall name (prim :: * -> * -> *) wX wY.
PrimWithName name prim wX wY -> RepoPatchV3 name prim wX wY
Prim (Sealed (PrimWithName name prim wX)
 -> Sealed (RepoPatchV3 name prim wX))
-> Parser ByteString (Sealed (PrimWithName name prim wX))
-> Parser (Sealed (RepoPatchV3 name prim wX))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ByteString (Sealed (PrimWithName name prim wX))
forall wX. Parser (Sealed (PrimWithName name prim wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
      ]
    where
      readContent :: Parser
  ByteString
  (Sealed (FL (PrimWithName name prim) wX),
   Set (Contexted (PrimWithName name prim) wX),
   Contexted (PrimWithName name prim) wX)
readContent = do
        Sealed (FL (PrimWithName name prim) wX)
r <- (forall wX. Parser (Sealed (PrimWithName name prim wX)))
-> Char -> Char -> Parser (Sealed (FL (PrimWithName name prim) wX))
forall (p :: * -> * -> *) wX.
(forall wY. Parser (Sealed (p wY)))
-> Char -> Char -> Parser (Sealed (FL p wX))
bracketedFL Parser (Sealed (PrimWithName name prim wY))
forall wX. Parser (Sealed (PrimWithName name prim wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch' Char
'[' Char
']'
        Set (Contexted (PrimWithName name prim) wX)
x <- Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall {wX}.
Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
readCtxSet
        Contexted (PrimWithName name prim) wX
p <- Parser (Contexted (PrimWithName name prim) wX)
forall (p :: * -> * -> *) wX.
(ReadPatch p, PatchListFormat p) =>
Parser (Contexted p wX)
readCtx
        (Sealed (FL (PrimWithName name prim) wX),
 Set (Contexted (PrimWithName name prim) wX),
 Contexted (PrimWithName name prim) wX)
-> Parser
     ByteString
     (Sealed (FL (PrimWithName name prim) wX),
      Set (Contexted (PrimWithName name prim) wX),
      Contexted (PrimWithName name prim) wX)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sealed (FL (PrimWithName name prim) wX)
r, Set (Contexted (PrimWithName name prim) wX)
x, Contexted (PrimWithName name prim) wX
p)
      readCtxSet :: Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
readCtxSet = (ByteString -> Parser ()
lexString ([Char] -> ByteString
BC.pack [Char]
"{{") Parser ()
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall {wX}.
Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
go) Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Set (Contexted (PrimWithName name prim) wX)
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (Contexted (PrimWithName name prim) wX)
forall a. Set a
S.empty
        where
          go :: Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
go = (ByteString -> Parser ()
lexString ([Char] -> ByteString
BC.pack [Char]
"}}") Parser ()
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Set (Contexted (PrimWithName name prim) wX)
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (Contexted (PrimWithName name prim) wX)
forall a. Set a
S.empty) Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Contexted (PrimWithName name prim) wX
-> Set (Contexted (PrimWithName name prim) wX)
-> Set (Contexted (PrimWithName name prim) wX)
forall a. Ord a => a -> Set a -> Set a
S.insert (Contexted (PrimWithName name prim) wX
 -> Set (Contexted (PrimWithName name prim) wX)
 -> Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Contexted (PrimWithName name prim) wX)
-> Parser
     ByteString
     (Set (Contexted (PrimWithName name prim) wX)
      -> Set (Contexted (PrimWithName name prim) wX))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ByteString (Contexted (PrimWithName name prim) wX)
forall (p :: * -> * -> *) wX.
(ReadPatch p, PatchListFormat p) =>
Parser (Contexted p wX)
readCtx Parser
  ByteString
  (Set (Contexted (PrimWithName name prim) wX)
   -> Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
-> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
forall a b.
Parser ByteString (a -> b)
-> Parser ByteString a -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser ByteString (Set (Contexted (PrimWithName name prim) wX))
go

instance (SignedId name, StorableId name, PrimPatch prim)
  => ShowPatchBasic (RepoPatchV3 name prim) where

  showPatch :: forall wX wY. ShowPatchFor -> RepoPatchV3 name prim wX wY -> Doc
showPatch ShowPatchFor
fmt RepoPatchV3 name prim wX wY
rp =
    case RepoPatchV3 name prim wX wY
rp of
      Prim PrimWithName name prim wX wY
p -> ShowPatchFor -> PrimWithName name prim wX wY -> Doc
forall wX wY. ShowPatchFor -> PrimWithName name prim wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
fmt PrimWithName name prim wX wY
p
      Conflictor FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
x Contexted (PrimWithName name prim) wY
cp ->
        case ShowPatchFor
fmt of
          ShowPatchFor
ForStorage -> [Char] -> Doc
blueText [Char]
"conflictor" Doc -> Doc -> Doc
<+> FL (PrimWithName name prim) wX wY
-> Set (Contexted (PrimWithName name prim) wY)
-> Contexted (PrimWithName name prim) wY
-> Doc
forall {a :: * -> * -> *} {p :: * -> * -> *} {p :: * -> * -> *}
       {wX} {wY} {wX} {wX}.
(ShowPatchBasic a, ShowPatchBasic p, ShowPatchBasic p,
 PatchListFormat p, PatchListFormat p) =>
FL a wX wY -> Set (Contexted p wX) -> Contexted p wX -> Doc
showContent FL (PrimWithName name prim) wX wY
r Set (Contexted (PrimWithName name prim) wY)
x Contexted (PrimWithName name prim) wY
cp
          ShowPatchFor
ForDisplay ->
            [Doc] -> Doc
vcat
            [ [Char] -> Doc
blueText [Char]
"conflictor"
            , [Doc] -> Doc
vcat ((forall wW wZ. PrimWithName name prim wW wZ -> Doc)
-> FL (PrimWithName name prim) wX wY -> [Doc]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL PrimWithName name prim wW wZ -> Doc
forall wW wZ. PrimWithName name prim wW wZ -> Doc
forall (p :: * -> * -> *) wX wY. ShowPatchBasic p => p wX wY -> Doc
displayPatch FL (PrimWithName name prim) wX wY
r)
            , [Char] -> Doc
redText [Char]
"v v v v v v v"
            , [Doc] -> Doc
vcat [ Contexted (PrimWithName name prim) wY -> Doc
forall {name} {prim :: * -> * -> *} {wX}.
(StorableId name, SignedId name, PatchListFormat prim,
 ShowPatchBasic prim, PrimCoalesce prim) =>
Contexted (PrimWithName name prim) wX -> Doc
displayCtx Contexted (PrimWithName name prim) wY
p Doc -> Doc -> Doc
$$ [Char] -> Doc
redText [Char]
"*************" | Contexted (PrimWithName name prim) wY
p <- Set (Contexted (PrimWithName name prim) wY)
-> [Contexted (PrimWithName name prim) wY]
forall a. Set a -> [a]
S.toList Set (Contexted (PrimWithName name prim) wY)
x ]
            , Contexted (PrimWithName name prim) wY -> Doc
forall {name} {prim :: * -> * -> *} {wX}.
(StorableId name, SignedId name, PatchListFormat prim,
 ShowPatchBasic prim, PrimCoalesce prim) =>
Contexted (PrimWithName name prim) wX -> Doc
displayCtx Contexted (PrimWithName name prim) wY
cp
            , [Char] -> Doc
redText [Char]
"^ ^ ^ ^ ^ ^ ^"
            ]
    where
      showContent :: FL a wX wY -> Set (Contexted p wX) -> Contexted p wX -> Doc
showContent FL a wX wY
r Set (Contexted p wX)
x Contexted p wX
cp = FL a wX wY -> Doc
forall {a :: * -> * -> *} {wX} {wY}.
ShowPatchBasic a =>
FL a wX wY -> Doc
showEffect FL a wX wY
r Doc -> Doc -> Doc
<+> Set (Contexted p wX) -> Doc
forall {p :: * -> * -> *} {wX}.
(ShowPatchBasic p, PatchListFormat p) =>
Set (Contexted p wX) -> Doc
showCtxSet Set (Contexted p wX)
x Doc -> Doc -> Doc
$$ ShowPatchFor -> Contexted p wX -> Doc
forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p) =>
ShowPatchFor -> Contexted p wX -> Doc
showCtx ShowPatchFor
fmt Contexted p wX
cp
      showEffect :: FL a wX wY -> Doc
showEffect FL a wX wY
NilFL = [Char] -> Doc
blueText [Char]
"[]"
      showEffect FL a wX wY
ps = [Char] -> Doc
blueText [Char]
"[" Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat ((forall wW wZ. a wW wZ -> Doc) -> FL a wX wY -> [Doc]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL (ShowPatchFor -> a wW wZ -> Doc
forall wX wY. ShowPatchFor -> a wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
fmt) FL a wX wY
ps) Doc -> Doc -> Doc
$$ [Char] -> Doc
blueText [Char]
"]"
      showCtxSet :: Set (Contexted p wX) -> Doc
showCtxSet Set (Contexted p wX)
xs =
        case Set (Contexted p wX)
-> Maybe (Contexted p wX, Set (Contexted p wX))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (Contexted p wX)
xs of
          Maybe (Contexted p wX, Set (Contexted p wX))
Nothing -> Doc
forall a. Monoid a => a
mempty
          Just (Contexted p wX, Set (Contexted p wX))
_ ->
            [Char] -> Doc
blueText [Char]
"{{"
              Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat ((Contexted p wX -> Doc) -> [Contexted p wX] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ShowPatchFor -> Contexted p wX -> Doc
forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p) =>
ShowPatchFor -> Contexted p wX -> Doc
showCtx ShowPatchFor
fmt) (Set (Contexted p wX) -> [Contexted p wX]
forall a. Set a -> [a]
S.toAscList Set (Contexted p wX)
xs))
              Doc -> Doc -> Doc
$$ [Char] -> Doc
blueText [Char]
"}}"
      displayCtx :: Contexted (PrimWithName name prim) wX -> Doc
displayCtx Contexted (PrimWithName name prim) wX
c =
        -- need to use ForStorage to see the prim patch IDs
        ShowPatchFor -> PatchId (PrimWithName name prim) -> Doc
forall a. StorableId a => ShowPatchFor -> a -> Doc
showId ShowPatchFor
ForStorage (Contexted (PrimWithName name prim) wX
-> PatchId (PrimWithName name prim)
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted (PrimWithName name prim) wX
c) Doc -> Doc -> Doc
$$
        (forall wX. FL (PrimWithName name prim) wX wX -> Doc)
-> Sealed (FL (PrimWithName name prim) wX) -> Doc
forall (a :: * -> *) b. (forall wX. a wX -> b) -> Sealed a -> b
unseal (ShowPatchFor -> FL prim wX wX -> Doc
forall wX wY. ShowPatchFor -> FL prim wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
ForDisplay (FL prim wX wX -> Doc)
-> (FL (PrimWithName name prim) wX wX -> FL prim wX wX)
-> FL (PrimWithName name prim) wX wX
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL prim wX wX -> FL prim wX wX
forall wX wY. FL prim wX wY -> FL prim wX wY
forall (prim :: * -> * -> *) wX wY.
PrimCoalesce prim =>
FL prim wX wY -> FL prim wX wY
sortCoalesceFL (FL prim wX wX -> FL prim wX wX)
-> (FL (PrimWithName name prim) wX wX -> FL prim wX wX)
-> FL (PrimWithName name prim) wX wX
-> FL prim wX wX
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall wW wY. PrimWithName name prim wW wY -> prim wW wY)
-> FL (PrimWithName name prim) wX wX -> FL prim wX wX
forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ.
(forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ
mapFL_FL PrimWithName name prim wW wY -> prim wW wY
forall wW wY. PrimWithName name prim wW wY -> prim wW wY
forall name (p :: * -> * -> *) wX wY.
PrimWithName name p wX wY -> p wX wY
wnPatch) (Contexted (PrimWithName name prim) wX
-> Sealed (FL (PrimWithName name prim) wX)
forall (p :: * -> * -> *) wX. Contexted p wX -> Sealed (FL p wX)
ctxToFL Contexted (PrimWithName name prim) wX
c)

-- * Local helper functions

infixr +|, -|

-- | A handy synonym for 'S.insert'.
(+|) :: Ord a => a -> S.Set a -> S.Set a
a
c +| :: forall a. Ord a => a -> Set a -> Set a
+| Set a
cs = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.insert a
c Set a
cs

-- | A handy synonym for 'S.delete'.
(-|) :: Ord a => a -> S.Set a -> S.Set a
a
c -| :: forall a. Ord a => a -> Set a -> Set a
-| Set a
cs = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
S.delete a
c Set a
cs