-- | 'Contexted' patches.

{-# LANGUAGE ViewPatterns #-}
module Darcs.Patch.V3.Contexted
    ( -- * Contexted patches
      Contexted
      -- * Query
    , ctxId
    , ctxView
    , ctxNoConflict
    , ctxToFL
      -- * Construct
    , ctx
    , ctxAdd
    , ctxAddRL
    , ctxAddInvFL
    , ctxAddFL
    , commutePast
    , commutePastRL
      -- * 'PatchInspect' helpers
    , ctxTouches
    , ctxHunkMatches
      -- * 'ReadPatch' and 'ShowPatch' helpers
    , showCtx
    , readCtx
      -- * Properties
    , prop_ctxInvariants
    , prop_ctxEq
    , prop_ctxPositive
    ) where

import qualified Data.ByteString as B
import qualified Data.ByteString.Char8 as BC ( pack )
import Data.Maybe ( isNothing, isJust )

import Darcs.Prelude

import Darcs.Patch.Commute
import Darcs.Patch.Format ( PatchListFormat(..) )
import Darcs.Patch.Ident
import Darcs.Patch.Invert
import Darcs.Patch.Inspect
import Darcs.Patch.Merge ( CleanMerge(..) )
import Darcs.Patch.Read ( ReadPatch(..) )
import Darcs.Util.Parser ( Parser, lexString )
import Darcs.Patch.Show ( ShowPatchBasic(..), ShowPatchFor )
import Darcs.Patch.Viewing ()
import Darcs.Patch.Witnesses.Eq
import Darcs.Patch.Witnesses.Ordered
import Darcs.Patch.Witnesses.Sealed
import Darcs.Patch.Witnesses.Show

import Darcs.Util.Path ( AnchoredPath )
import Darcs.Util.Printer

{-
| (Definition 10.1) A 'Contexted' patch is a patch transferred to, or viewed
from, a different context.

More precisely we make the following definitions:

* A /context/ for a patch @p@ is a sequence of patches that @p@ depends on,
  and such that it never contains a patch and its inverse.

* A 'Contexted' patch is a patch @p@ together with a context for @p@, such
  that the end state of the patch and its context is hidden (existentially
  quantified).

The definition of context above is chosen so that this sequence is minimal.
-}
data Contexted p wX where
  Contexted :: FL p wX wY -> p wY wZ -> Contexted p wX

-- | Equality between 'Contexted' patches reduces to equality of the
-- identifiers of the patches referred to /if/ we look at them from the same
-- context. (This assumes witnesses aren't coerced in an unsafe manner.)
instance Ident p => Eq (Contexted p wX) where
  Contexted p wX
c1 == :: Contexted p wX -> Contexted p wX -> Bool
== Contexted p wX
c2 = Contexted p wX -> PatchId p
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
c1 PatchId p -> PatchId p -> Bool
forall a. Eq a => a -> a -> Bool
== Contexted p wX -> PatchId p
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
c2
{-
-- Comparing the contexts is inefficient and unnecessary
-- if the patches have identities, see 'prop_ctxEq'.
instance (Commute p, Eq2 p) => Eq (Contexted p wX) where
  Contexted cx x == Contexted cy y
    | IsEq <- cx =\/= cy
    , IsEq <- x =\/= y = True
    | otherwise = False
-}

instance Ident p => Ord (Contexted p wX) where
  Contexted p wX
cp compare :: Contexted p wX -> Contexted p wX -> Ordering
`compare` Contexted p wX
cq = Contexted p wX -> PatchId p
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
cp PatchId p -> PatchId p -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Contexted p wX -> PatchId p
forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
cq

instance Show2 p => Show (Contexted p wX) where
  showsPrec :: Int -> Contexted p wX -> ShowS
showsPrec Int
d (Contexted FL p wX wY
ps p wY wZ
p) =
    Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Contexted " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Int -> FL p 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) FL p wX wY
ps ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Int -> p wY wZ -> 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) p wY wZ
p

instance Show2 p => Show1 (Contexted p)

-- | This property states that no prefix of the context commutes with the rest
-- of the 'Contexted' patch and that the context never contains a patch
-- and its inverse.
prop_ctxInvariants :: (Commute p, Invert p, SignedIdent p) => Contexted p wX -> Bool
prop_ctxInvariants :: Contexted p wX -> Bool
prop_ctxInvariants (Contexted FL p wX wY
NilFL p wY wZ
_) = Bool
True
prop_ctxInvariants c :: Contexted p wX
c@(Contexted (p wX wY
_ :>: FL p wY wY
ps) p wY wZ
q) =
  Contexted p wY -> Bool
forall (p :: * -> * -> *) wX.
(Commute p, Invert p, SignedIdent p) =>
Contexted p wX -> Bool
prop_ctxInvariants (FL p wY wY -> p wY wZ -> Contexted p wY
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted FL p wY wY
ps p wY wZ
q) Bool -> Bool -> Bool
&& Contexted p wX -> Bool
forall (p :: * -> * -> *) wX. Commute p => Contexted p wX -> Bool
prop_ctxNotCom Contexted p wX
c Bool -> Bool -> Bool
&& Contexted p wX -> Bool
forall (p :: * -> * -> *) wX.
SignedIdent p =>
Contexted p wX -> Bool
prop_ctxNotInv Contexted p wX
c

-- | This property states that the first patch in the context must not
-- commute with the rest of the 'Contexted' patch.
prop_ctxNotCom :: Commute p => Contexted p wX -> Bool
prop_ctxNotCom :: Contexted p wX -> Bool
prop_ctxNotCom (Contexted FL p wX wY
NilFL p wY wZ
_) = Bool
True
prop_ctxNotCom (Contexted (p wX wY
p :>: FL p wY wY
ps) p wY wZ
q) =
  Maybe ((:>) (FL p) p wX wZ) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe ((:>) (FL p) p wX wZ) -> Bool)
-> Maybe ((:>) (FL p) p wX wZ) -> Bool
forall a b. (a -> b) -> a -> b
$ (:>) p (FL p) wX wZ -> Maybe ((:>) (FL p) p wX wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
p p wX wY -> FL p wY wZ -> (:>) p (FL p) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
ps FL p wY wY -> FL p wY wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
q p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)

-- | This property states that patches in the context of a 'Contexted' patch as
-- well as the patch itself are positive. It does /not/ necessarily hold for all
-- 'Contexted' patches.
prop_ctxPositive :: SignedIdent p => Contexted p wX -> Bool
prop_ctxPositive :: Contexted p wX -> Bool
prop_ctxPositive (Contexted FL p wX wY
ps p wY wZ
p) =
  (forall wX wY. p wX wY -> Bool) -> FL p wX wY -> Bool
forall (a :: * -> * -> *) wW wZ.
(forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool
allFL (PatchId p -> Bool
forall a. SignedId a => a -> Bool
positiveId (PatchId p -> Bool) -> (p wX wY -> PatchId p) -> p wX wY -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) FL p wX wY
ps Bool -> Bool -> Bool
&& PatchId p -> Bool
forall a. SignedId a => a -> Bool
positiveId (p wY wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p)

-- | This property states that the inverse of the first patch in the context
-- is not contained in the rest of the context.
prop_ctxNotInv :: SignedIdent p => Contexted p wX -> Bool
prop_ctxNotInv :: Contexted p wX -> Bool
prop_ctxNotInv (Contexted FL p wX wY
NilFL p wY wZ
_) = Bool
True
prop_ctxNotInv (Contexted (p wX wY
p :>: FL p wY wY
ps) p wY wZ
_) =
  PatchId p -> PatchId p
forall a. SignedId a => a -> a
invertId (p wX wY -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wY
p) PatchId p -> [PatchId p] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (forall wW wZ. p wW wZ -> PatchId p) -> FL p wY wY -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wY wY
ps

-- This property states that equal 'Contexted' patches have equal content.
prop_ctxEq :: (Commute p, Eq2 p, Ident p) => Contexted p wX -> Contexted p wX -> Bool
prop_ctxEq :: Contexted p wX -> Contexted p wX -> Bool
prop_ctxEq cp :: Contexted p wX
cp@(Contexted FL p wX wY
ps p wY wZ
p) cq :: Contexted p wX
cq@(Contexted FL p wX wY
qs p wY wZ
q)
  | Contexted p wX
cp Contexted p wX -> Contexted p wX -> Bool
forall a. Eq a => a -> a -> Bool
== Contexted p wX
cq =
      case FL p wX wY
ps FL p wX wY -> FL p wX wY -> EqCheck wY wY
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= FL p wX wY
qs of
        EqCheck wY wY
IsEq -> EqCheck wZ wZ -> Bool
forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wY wZ
p p wY wZ -> p wY wZ -> EqCheck wZ wZ
forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wY wZ
p wY wZ
q)
        EqCheck wY wY
NotEq -> Bool
False
prop_ctxEq Contexted p wX
_ Contexted p wX
_ = Bool
True

-- * Query

-- | Identity of a contexted patch.
{-# INLINE ctxId #-}
ctxId :: Ident p => Contexted p wX -> PatchId p
ctxId :: Contexted p wX -> PatchId p
ctxId (Contexted FL p wX wY
_ p wY wZ
p) = p wY wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p

-- | 'Contexted' patches conflict with each other if the identity of one is in
-- the context of the other or they cannot be merged cleanly.
ctxNoConflict :: (CleanMerge p, Commute p, Ident p)
              => Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict :: Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted p wX
cp Contexted p wX
cq | Contexted p wX
cp Contexted p wX -> Contexted p wX -> Bool
forall a. Eq a => a -> a -> Bool
== Contexted p wX
cq = Bool
True
ctxNoConflict (Contexted FL p wX wY
ps p wY wZ
p) (Contexted FL p wX wY
qs p wY wZ
q)
  | p wY wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p PatchId p -> [PatchId p] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall wW wZ. p wW wZ -> PatchId p) -> FL p wX wY -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wY
qs Bool -> Bool -> Bool
|| p wY wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
q PatchId p -> [PatchId p] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall wW wZ. p wW wZ -> PatchId p) -> FL p wX wY -> [PatchId p]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall wW wZ. p wW wZ -> PatchId p
forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wY
ps = Bool
False
  | Bool
otherwise =
      case FL p wX wY -> FL p wX wY -> Fork (FL p) (FL p) (FL p) wX wY 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 p wX wY
ps FL p wX wY
qs of
        Fork FL p wX wU
_ FL p wU wY
ps' FL p wU wY
qs' ->
          Maybe ((:/\:) (FL p) (FL p) wZ wZ) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ((:/\:) (FL p) (FL p) wZ wZ) -> Bool)
-> Maybe ((:/\:) (FL p) (FL p) wZ wZ) -> Bool
forall a b. (a -> b) -> a -> b
$ (:\/:) (FL p) (FL p) wZ wZ -> Maybe ((:/\:) (FL p) (FL p) wZ wZ)
forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL p wU wY
ps' FL p wU wY -> FL p wY wZ -> FL p wU wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
p p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wU wZ -> FL p wU wZ -> (:\/:) (FL p) (FL p) wZ wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wU wY
qs' FL p wU wY -> FL p wY wZ -> FL p wU wZ
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
q p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)

{-
-- This is (Definition 10.4) of the paper.
-- It misses a case for equal contexted patches and is also quite slow.
ctxNoConflict (Contexted cs p) cq =
  isJust $ commutePast (invert p) (ctxAddInvFL cs cq)
-}

-- | We sometimes want to pattern match on a 'Contexted' patch but still guard
-- against violation of teh invariants. So we export a view that is isomorphic
-- to the 'Contexted' type but doesn't allow to manipulate the internals.
ctxView :: Contexted p wX -> Sealed ((FL p :> p) wX)
ctxView :: Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView (Contexted FL p wX wY
cs p wY wZ
p) = (:>) (FL p) p wX wZ -> Sealed ((:>) (FL p) p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL p wX wY
cs FL p wX wY -> p wY wZ -> (:>) (FL p) p wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p)

-- | Convert a 'Contexted' patch into a plain 'FL' with the patch at the end.
ctxToFL :: Contexted p wX -> Sealed (FL p wX)
ctxToFL :: Contexted p wX -> Sealed (FL p wX)
ctxToFL (Contexted p wX -> Sealed ((:>) (FL p) p wX)
forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (FL p wX wZ
ps :> p wZ wX
p)) = FL p wX wX -> Sealed (FL p wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL p wX wZ
ps FL p wX wZ -> FL p wZ wX -> FL p wX wX
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wZ wX
p p wZ wX -> FL p wX wX -> FL p wZ wX
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)

-- * Construct

-- | A 'Contexted' patch with empty context.
ctx :: p wX wY -> Contexted p wX
ctx :: p wX wY -> Contexted p wX
ctx p wX wY
p = FL p wX wX -> p wX wY -> Contexted p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted FL p wX wX
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL p wX wY
p

-- | Add a patch to the context of a 'Contexted' patch. This is
-- the place where we take care of the invariants.
ctxAdd :: (Commute p, Invert p, Ident p)
       => p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd :: p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd p wX wY
p (Contexted FL p wY wY
ps p wY wZ
q)
  | Just FL p wX wY
ps' <- p wY wX -> FL p wY wY -> Maybe (FL p wX wY)
forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL (p wX wY -> p wY wX
forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
p) FL p wY wY
ps = FL p wX wY -> p wY wZ -> Contexted p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted FL p wX wY
ps' p wY wZ
q
ctxAdd p wX wY
p c :: Contexted p wY
c@(Contexted FL p wY wY
ps p wY wZ
q) =
  case p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast p wX wY
p Contexted p wY
c of
    Just Contexted p wX
c' -> Contexted p wX
c'
    Maybe (Contexted p wX)
Nothing -> FL p wX wY -> p wY wZ -> Contexted p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted (p wX wY
p p wX wY -> FL p wY wY -> FL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wY
ps) p wY wZ
q

-- | Add an 'RL' of patches to the context.
ctxAddRL :: (Commute p, Invert p, Ident p)
         => RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL :: RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL p wX wY
NilRL Contexted p wY
cp = Contexted p wX
Contexted p wY
cp
ctxAddRL (RL p wX wY
ps :<: p wY wY
p) Contexted p wY
cp = RL p wX wY -> Contexted p wY -> Contexted p wX
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL RL p wX wY
ps (p wY wY -> Contexted p wY -> Contexted p wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd p wY wY
p Contexted p wY
cp)

-- | Add an 'FL' of patches to the context but invert it first.
ctxAddInvFL :: (Commute p, Invert p, Ident p)
            => FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL :: FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL = RL p wY wX -> Contexted p wX -> Contexted p wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL (RL p wY wX -> Contexted p wX -> Contexted p wY)
-> (FL p wX wY -> RL p wY wX)
-> FL p wX wY
-> Contexted p wX
-> Contexted p wY
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FL p wX wY -> RL p wY wX
forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL

-- | Add an 'FL' of patches to the context.
ctxAddFL :: (Commute p, Invert p, Ident p)
         => FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL :: FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL FL p wX wY
NilFL Contexted p wY
t = Contexted p wX
Contexted p wY
t
ctxAddFL (p wX wY
p :>: FL p wY wY
ps) Contexted p wY
t = p wX wY -> Contexted p wY -> Contexted p wX
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd p wX wY
p (FL p wY wY -> Contexted p wY -> Contexted p wY
forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL FL p wY wY
ps Contexted p wY
t)

-- | (Definition 10.2) Commute a patch past a 'Contexted' patch. This
-- commutes it past the context and then past the patch itself. If it
-- succeeds, the patch that we commuted past gets dropped.
-- Note that this does /not/ succeed if the inverted patch is in the
-- 'Contexted' patch.
commutePast :: Commute p
            => p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast :: p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast p wX wY
q (Contexted FL p wY wY
ps p wY wZ
p) = do
  FL p wX wZ
ps' :> p wZ wY
q' <- (:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
q p wX wY -> FL p wY wY -> (:>) p (FL p) wX wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
ps)
  p wZ wZ
p' :> p wZ wZ
_ <- (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wY
q' p wZ wY -> p wY wZ -> (:>) p p wZ wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p)
  Contexted p wX -> Maybe (Contexted p wX)
forall (m :: * -> *) a. Monad m => a -> m a
return (FL p wX wZ -> p wZ wZ -> Contexted p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted FL p wX wZ
ps' p wZ wZ
p')

-- | Not defined in the paper but used in the commute algorithm.
commutePastRL :: Commute p
              => RL p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePastRL :: RL p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePastRL = (forall wA wB. p wA wB -> Contexted p wB -> Maybe (Contexted p wA))
-> RL p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
forall (m :: * -> *) (p :: * -> * -> *) (r :: * -> *) wX wY.
Monad m =>
(forall wA wB. p wA wB -> r wB -> m (r wA))
-> RL p wX wY -> r wY -> m (r wX)
foldRL_M forall wA wB. p wA wB -> Contexted p wB -> Maybe (Contexted p wA)
forall (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast

-- * 'PatchInspect' helpers

ctxTouches :: PatchInspect p => Contexted p wX -> [AnchoredPath]
ctxTouches :: Contexted p wX -> [AnchoredPath]
ctxTouches (Contexted FL p wX wY
ps p wY wZ
p) =
  [[AnchoredPath]] -> [AnchoredPath]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AnchoredPath]] -> [AnchoredPath])
-> [[AnchoredPath]] -> [AnchoredPath]
forall a b. (a -> b) -> a -> b
$ p wY wZ -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles p wY wZ
p [AnchoredPath] -> [[AnchoredPath]] -> [[AnchoredPath]]
forall a. a -> [a] -> [a]
: (forall wW wZ. p wW wZ -> [AnchoredPath])
-> FL p wX wY -> [[AnchoredPath]]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall wW wZ. p wW wZ -> [AnchoredPath]
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles FL p wX wY
ps

ctxHunkMatches :: PatchInspect p => (B.ByteString -> Bool)
               -> Contexted p wX -> Bool
ctxHunkMatches :: (ByteString -> Bool) -> Contexted p wX -> Bool
ctxHunkMatches ByteString -> Bool
f (Contexted FL p wX wY
ps p wY wZ
p) = (ByteString -> Bool) -> FL p wX wY -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f FL p wX wY
ps Bool -> Bool -> Bool
|| (ByteString -> Bool) -> p wY wZ -> Bool
forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f p wY wZ
p

-- * 'ReadPatch' and 'ShowPatch' helpers

-- For storage it would be enough to read/write the patch identifiers in the
-- context. But this means that we need access to the patches preceding us.
-- So these functions would no longer be independent of context.

showCtx :: (ShowPatchBasic p, PatchListFormat p)
        => ShowPatchFor -> Contexted p wX -> Doc
showCtx :: ShowPatchFor -> Contexted p wX -> Doc
showCtx ShowPatchFor
f (Contexted FL p wX wY
c p wY wZ
p) =
  String -> Doc -> Doc
hiddenPrefix String
"|" (ShowPatchFor -> FL p wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f FL p wX wY
c) Doc -> Doc -> Doc
$$ String -> Doc -> Doc
hiddenPrefix String
"|" (String -> Doc
blueText String
":") Doc -> Doc -> Doc
$$ ShowPatchFor -> p wY wZ -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
f p wY wZ
p

readCtx :: (ReadPatch p, PatchListFormat p)
        => Parser (Contexted p wX)
readCtx :: Parser (Contexted p wX)
readCtx = do
  Sealed FL p wX wX
ps <- Parser (Sealed (FL p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
  ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
":")
  Sealed p wX wX
p <- Parser (Sealed (p wX))
forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
  Contexted p wX -> Parser (Contexted p wX)
forall (m :: * -> *) a. Monad m => a -> m a
return (Contexted p wX -> Parser (Contexted p wX))
-> Contexted p wX -> Parser (Contexted p wX)
forall a b. (a -> b) -> a -> b
$ FL p wX wX -> p wX wX -> Contexted p wX
forall (p :: * -> * -> *) wX wY wZ.
FL p wX wY -> p wY wZ -> Contexted p wX
Contexted FL p wX wX
ps p wX wX
p