darcs-2.18.5: src/Darcs/Patch/V3/Core.hs
{- | '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 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 ConflictorP r x cp <- Conflictor r x cp
-- * Effect
instance Effect (RepoPatchV3 name prim) where
effect (Prim p) = wnPatch p :>: NilFL
effect (Conflictor r _ _) = mapFL_FL wnPatch r
-- * Ident
type instance PatchId (RepoPatchV3 name prim) = name
instance SignedId name => Ident (RepoPatchV3 name prim) where
ident (Prim p) = ident p
ident (Conflictor _ _ cp) = ctxId 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 p = showPatch ForStorage p
instance (SignedId name, StorableId name, PrimPatch prim) =>
CleanMerge (RepoPatchV3 name prim) where
cleanMerge (p :\/: q)
| ident p == ident q = error "merging identical patches is undefined"
cleanMerge (Prim p :\/: Prim q) = do
q' :/\: p' <- cleanMerge (p :\/: q)
return $ Prim q' :/\: Prim p'
cleanMerge (Prim p :\/: Conflictor s y 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
s' :/\: p' <- cleanMergeFL (p :\/: s)
let ip' = invert p'
cq' <- commutePast ip' cq
y' <- S.fromList <$> mapM (commutePast ip') (S.toList y)
return $ Conflictor s' y' cq' :/\: Prim p'
cleanMerge pair@(Conflictor {} :\/: Prim {}) = swapCleanMerge pair
cleanMerge (Conflictor com_r x cp :\/: Conflictor com_s y cq) =
case findCommonFL com_r com_s of
Fork _ rev_r rev_s -> do
s' :/\: r' <- cleanMerge (rev_r :\/: 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' = ctxAddInvFL s' cp
let cq' = ctxAddInvFL r' cq
let x' = S.map (ctxAddInvFL s') x
let y' = S.map (ctxAddInvFL r') y
guard (ctxNoConflict cq' cp')
guard $ all (ctxNoConflict cq') (S.difference x' y')
guard $ all (ctxNoConflict cp') (S.difference y' x')
return $ Conflictor s' y' cq' :/\: Conflictor r' x' cp'
instance (SignedId name, StorableId name, PrimPatch prim) =>
Merge (RepoPatchV3 name prim) where
-- * no conflict
merge pq | Just r <- cleanMerge pq = 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 p :\/: Prim q) =
Conflictor (invert p :>: NilFL) (S.singleton (ctx p)) (ctx q)
:/\:
Conflictor (invert q :>: NilFL) (S.singleton (ctx q)) (ctx 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 p :\/: Conflictor r x cq) =
Conflictor (invert p :>: r) (ctxAddInvFL r (ctx p) +| x) cq
:/\:
Conflictor NilFL (S.singleton cq) (ctxAddInvFL r (ctx p))
-- same as previous case with both sides swapped
merge pair@(Conflictor {} :\/: Prim {}) = swapMerge 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@(Conflictor com_r x cp) :\/: rhs@(Conflictor com_s y cq)) =
case findCommonFL com_r com_s of
Fork _ r s ->
case cleanMerge (r :\/: s) of
Just (s' :/\: r') ->
let cp' = ctxAddInvFL s' cp
cq' = ctxAddInvFL r' cq
x' = cq' +| S.map (ctxAddInvFL s') x
y' = cp' +| S.map (ctxAddInvFL r') y
in Conflictor s' y' cq' :/\: Conflictor r' x' cp'
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
error $ renderString $ redText "uncommon effects can't be merged cleanly:"
$$ redText "lhs:" $$ displayPatch lhs
$$ redText "rhs:" $$ displayPatch rhs
$$ redText "r:" $$ displayPatch r
$$ redText "s:" $$ displayPatch 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 (Prim p :> Prim q) = do
q' :> p' <- commute (p :> q)
return $ Prim q' :> Prim p'
commuteNoConflicts (Conflictor r x cp :> Prim q) = do
q' :> r' <- commuteRL (reverseFL r :> q)
let iq = invert q
cp' <- commutePast iq cp
x' <- S.fromList <$> mapM (commutePast iq) (S.toList x)
return $ Prim q' :> Conflictor (reverseRL r') x' cp'
-- this case is completely symmetric to the previous one
commuteNoConflicts (Prim p :> Conflictor s y cq) = do
s' :> p' <- commuteFL (p :> s)
cq' <- commutePast p' cq
y' <- S.fromList <$> mapM (commutePast p') (S.toList y)
return $ Conflictor s' y' cq' :> Prim p'
commuteNoConflicts (Conflictor com_r x cp :> Conflictor s y cq) = do
-- com = prims in the effect of the lhs that the rhs also conflicts with;
-- these remain on the lhs
com :> rr <- commuteToPrefix (S.map (invertId . ctxId) y) com_r
s' :> rr' <- commuteRLFL (rr :> s)
let cp' = ctxAddInvFL s cp
cq' = ctxAddRL rr' cq
-- obviously p and q must not conflict, nor depend on each other
guard (ctxNoConflict cq cp')
let x' = S.map (ctxAddInvFL s) x
y' = S.map (ctxAddRL rr') y
-- somewhat less obviously, p must not conflict with the patches that only
-- q conflicts with, nor depend on them, and vice versa
guard $ all (ctxNoConflict cp') (S.difference y x')
guard $ all (ctxNoConflict cq) (S.difference x' y)
return $ Conflictor (com +>+ s') y' cq' :> Conflictor (reverseRL rr') x' 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 (Prim p :> Conflictor (ip:>:NilFL) ys cq@(ctxView -> Sealed (NilFL :> q)))
| [ctxView -> Sealed (NilFL :> p')] <- S.toList ys
, IsEq <- invert p =\/= ip
, IsEq <- p =\/= p' =
Just (Prim q :> Conflictor (invert q :>: NilFL) (S.singleton cq) (ctx 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 p :> Conflictor s y cq)
| ident p `S.member` S.map ctxId y =
case fastRemoveFL (invert p) s of
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
error $ renderString
$ redText "commuteConflicting: cannot remove (invert lhs):"
$$ displayPatch (invert p)
$$ redText "from effect of rhs:"
$$ displayPatch s
Just r ->
let cp = ctxAddInvFL r (ctx p)
in Just (Conflictor r (cp -| y) cq :> Conflictor NilFL (S.singleton cq) 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@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
| y == S.singleton cp =
case ctxView (ctxAddFL r cq) of
Sealed (NilFL :> q') ->
Just $ Prim q' :> Conflictor (invert q' :>: r) (cq +| x) cp
Sealed (c' :> _) ->
-- 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
error $ renderString $ redText "remaining context in commute:"
$$ displayPatch c'
$$ redText "lhs:" $$ displayPatch lhs
$$ redText "rhs:" $$ displayPatch 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 com_r x cp :> Conflictor s y cq)
| let cp' = ctxAddInvFL s cp
, cp' `S.member` y
, let y' = cp' -| y =
case commuteToPrefix (S.map (invertId . ctxId) y') com_r of
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
error "commuteConflicting: cannot commute common effects"
Just (com :> rr) ->
case commuteRLFL (rr :> s) of
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.
error "commuteConflicting: cannot commute uncommon effects"
Just (s' :> rr') ->
Just $
Conflictor (com +>+ s') (S.map (ctxAddRL rr') y') (ctxAddRL rr' cq)
:>
Conflictor (reverseRL rr') (cq +| S.map (ctxAddInvFL s) x) cp'
commuteConflicting _ = Nothing
instance (SignedId name, StorableId name, PrimPatch prim) =>
Commute (RepoPatchV3 name prim) where
commute pair = commuteConflicting pair <|> commuteNoConflicts 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 (Prim p) = listTouchedFiles p
listTouchedFiles (Conflictor r _ cp) =
nubSort $ concat (mapFL listTouchedFiles r) ++ ctxTouches cp
hunkMatches f (Prim p) = hunkMatches f p
hunkMatches f (Conflictor r _ cp) = hunkMatches f r || ctxHunkMatches f cp
-- * Boilerplate instances
instance (SignedId name, Eq2 prim, Commute prim) => Eq2 (RepoPatchV3 name prim) where
(Prim p) =\/= (Prim q) = p =\/= q
(Conflictor r x cp) =\/= (Conflictor s y cq)
| IsEq <- r =\^/= s -- more efficient than IsEq <- r =\/= s
, x == y
, cp == cq = IsEq
_ =\/= _ = NotEq
instance (Show name, Show2 prim) => Show (RepoPatchV3 name prim wX wY) where
showsPrec d rp = showParen (d > appPrec) $
case rp of
Prim prim ->
showString "Prim " . showsPrec2 (appPrec + 1) prim
Conflictor r x cp -> showString "Conflictor " . showContent r x cp
where
showContent r x cp =
showsPrec (appPrec + 1) r .
showString " " . showsPrec (appPrec + 1) x .
showString " " . showsPrec (appPrec + 1) 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 (Conflictor {}) = Nothing
toPrim (Prim p) = Just (wnPatch p)
instance PatchDebug prim => PatchDebug (RepoPatchV3 name prim)
instance PrimPatch prim => Apply (RepoPatchV3 name prim) where
type ApplyState (RepoPatchV3 name prim) = ApplyState prim
apply = applyPrimFL . effect
unapply = applyPrimFL . invert . effect
instance PatchListFormat (RepoPatchV3 name prim) where
patchListFormat = ListFormatV3
instance IsHunk prim => IsHunk (RepoPatchV3 name prim) where
isHunk rp = do
Prim p <- return rp
isHunk p
instance Summary (RepoPatchV3 name prim) where
conflictedEffect (Conflictor _ _ (ctxView -> Sealed (_ :> p))) = [IsC Conflicted (wnPatch p)]
conflictedEffect (Prim p) = [IsC Okay (wnPatch p)]
instance (Invert prim, Commute prim, Eq2 prim) => Unwind (RepoPatchV3 name prim) where
fullUnwind (Prim p)
= mkUnwound NilFL (wnPatch p :>: NilFL) NilFL
fullUnwind
(Conflictor
(mapFL_FL wnPatch -> es)
_
(ctxView -> Sealed ((mapFL_FL wnPatch -> cs) :> (wnPatch -> i)))
) =
mkUnwound
(es +>+ cs)
(i :>: NilFL)
(invert i :>: invert cs +>+ 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 = plainSummary
summaryFL = plainSummaryFL
thing _ = "change"
instance (SignedId name, StorableId name, PrimPatch prim)
=> ShowContextPatch (RepoPatchV3 name prim) where
showPatchWithContextAndApply f (Prim p) = showPatchWithContextAndApply f p
showPatchWithContextAndApply f p = apply p >> return (showPatch f p)
-- * Read and Write
instance (SignedId name, StorableId name, PrimPatch prim)
=> ReadPatch (RepoPatchV3 name prim) where
readPatch' = do
skipSpace
choice
[ do string (BC.pack "conflictor")
(Sealed r, x, p) <- readContent
return (Sealed (Conflictor r (S.map unsafeCoerceP1 x) (unsafeCoerceP1 p)))
, do mapSeal Prim <$> readPatch'
]
where
readContent = do
r <- bracketedFL readPatch' '[' ']'
x <- readCtxSet
p <- readCtx
return (r, x, p)
readCtxSet = (lexString (BC.pack "{{") >> go) <|> pure S.empty
where
go = (lexString (BC.pack "}}") >> pure S.empty) <|> S.insert <$> readCtx <*> go
instance (SignedId name, StorableId name, PrimPatch prim)
=> ShowPatchBasic (RepoPatchV3 name prim) where
showPatch fmt rp =
case rp of
Prim p -> showPatch fmt p
Conflictor r x cp ->
case fmt of
ForStorage -> blueText "conflictor" <+> showContent r x cp
ForDisplay ->
vcat
[ blueText "conflictor"
, vcat (mapFL displayPatch r)
, redText "v v v v v v v"
, vcat [ displayCtx p $$ redText "*************" | p <- S.toList x ]
, displayCtx cp
, redText "^ ^ ^ ^ ^ ^ ^"
]
where
showContent r x cp = showEffect r <+> showCtxSet x $$ showCtx fmt cp
showEffect NilFL = blueText "[]"
showEffect ps = blueText "[" $$ vcat (mapFL (showPatch fmt) ps) $$ blueText "]"
showCtxSet xs =
case S.minView xs of
Nothing -> mempty
Just _ ->
blueText "{{"
$$ vcat (map (showCtx fmt) (S.toAscList xs))
$$ blueText "}}"
displayCtx c =
-- need to use ForStorage to see the prim patch IDs
showId ForStorage (ctxId c) $$
unseal (showPatch ForDisplay . sortCoalesceFL . mapFL_FL wnPatch) (ctxToFL c)
-- * Local helper functions
infixr +|, -|
-- | A handy synonym for 'S.insert'.
(+|) :: Ord a => a -> S.Set a -> S.Set a
c +| cs = S.insert c cs
-- | A handy synonym for 'S.delete'.
(-|) :: Ord a => a -> S.Set a -> S.Set a
c -| cs = S.delete c cs