{-# LANGUAGE ViewPatterns #-}
module Darcs.Patch.V3.Contexted
(
Contexted
, ctxId
, ctxView
, ctxNoConflict
, ctxToFL
, ctx
, ctxAdd
, ctxAddRL
, ctxAddInvFL
, ctxAddFL
, commutePast
, commutePastRL
, ctxTouches
, ctxHunkMatches
, showCtx
, readCtx
, 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
data Contexted p wX where
Contexted :: FL p wX wY -> p wY wZ -> Contexted p wX
instance Ident p => Eq (Contexted p wX) where
Contexted p wX
c1 == :: Contexted p wX -> Contexted p wX -> Bool
== Contexted p wX
c2 = forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
c1 forall a. Eq a => a -> a -> Bool
== forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
c2
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 = forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId Contexted p wX
cp forall a. Ord a => a -> a -> Ordering
`compare` 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 forall a. Ord a => a -> a -> Bool
> Int
appPrec) forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Contexted " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec forall a. Num a => a -> a -> a
+ Int
1) FL p wX wY
ps forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS
showsPrec2 (Int
appPrec forall a. Num a => a -> a -> a
+ Int
1) p wY wZ
p
instance Show2 p => Show1 (Contexted p)
prop_ctxInvariants :: (Commute p, Invert p, SignedIdent p) => Contexted p wX -> Bool
prop_ctxInvariants :: forall (p :: * -> * -> *) wX.
(Commute p, Invert p, SignedIdent p) =>
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) =
forall (p :: * -> * -> *) wX.
(Commute p, Invert p, SignedIdent p) =>
Contexted p wX -> Bool
prop_ctxInvariants (forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX wZ -> Contexted p wX
Contexted FL p wY wY
ps p wY wZ
q) Bool -> Bool -> Bool
&& forall (p :: * -> * -> *) wX. Commute p => Contexted p wX -> Bool
prop_ctxNotCom Contexted p wX
c Bool -> Bool -> Bool
&& forall (p :: * -> * -> *) wX.
SignedIdent p =>
Contexted p wX -> Bool
prop_ctxNotInv Contexted p wX
c
prop_ctxNotCom :: Commute p => Contexted p wX -> Bool
prop_ctxNotCom :: forall (p :: * -> * -> *) wX. Commute p => 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) =
forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
p forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
ps forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
q forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
prop_ctxPositive :: SignedIdent p => Contexted p wX -> Bool
prop_ctxPositive :: forall (p :: * -> * -> *) wX.
SignedIdent p =>
Contexted p wX -> Bool
prop_ctxPositive (Contexted FL p wX wY
ps p wY wZ
p) =
forall (a :: * -> * -> *) wW wZ.
(forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool
allFL (forall a. SignedId a => a -> Bool
positiveId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident) FL p wX wY
ps Bool -> Bool -> Bool
&& forall a. SignedId a => a -> Bool
positiveId (forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p)
prop_ctxNotInv :: SignedIdent p => Contexted p wX -> Bool
prop_ctxNotInv :: forall (p :: * -> * -> *) wX.
SignedIdent p =>
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
_) =
forall a. SignedId a => a -> a
invertId (forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wX wY
p) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wY wY
ps
prop_ctxEq :: (Commute p, Eq2 p, Ident p) => Contexted p wX -> Contexted p wX -> Bool
prop_ctxEq :: forall (p :: * -> * -> *) wX.
(Commute p, Eq2 p, Ident p) =>
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 forall a. Eq a => a -> a -> Bool
== Contexted p wX
cq =
case FL p wX wY
ps 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 -> forall wA wB. EqCheck wA wB -> Bool
isIsEq (p wY wZ
p forall (p :: * -> * -> *) wA wB wC.
Eq2 p =>
p wA wB -> p wA wC -> EqCheck wB wC
=\/= p wY wZ
q)
EqCheck wY wY
NotEq -> Bool
False
prop_ctxEq Contexted p wX
_ Contexted p wX
_ = Bool
True
{-# INLINE ctxId #-}
ctxId :: Ident p => Contexted p wX -> PatchId p
ctxId :: forall (p :: * -> * -> *) wX.
Ident p =>
Contexted p wX -> PatchId p
ctxId (Contexted FL p wX wY
_ p wY wZ
p) = forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p
ctxNoConflict :: (CleanMerge p, Commute p, Ident p)
=> Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict :: forall (p :: * -> * -> *) wX.
(CleanMerge p, Commute p, Ident p) =>
Contexted p wX -> Contexted p wX -> Bool
ctxNoConflict Contexted p wX
cp Contexted p wX
cq | Contexted p wX
cp 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)
| forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wY
qs Bool -> Bool -> Bool
|| forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident p wY wZ
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL forall (p :: * -> * -> *) wX wY. Ident p => p wX wY -> PatchId p
ident FL p wX wY
ps = Bool
False
| Bool
otherwise =
case 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' ->
forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
CleanMerge p =>
(:\/:) p p wX wY -> Maybe ((:/\:) p p wX wY)
cleanMerge (FL p wU wY
ps' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
p forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wZ wX -> a2 wZ wY -> (:\/:) a1 a2 wX wY
:\/: FL p wU wY
qs' forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wY wZ
q forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
ctxView :: Contexted p wX -> Sealed ((FL p :> p) wX)
ctxView :: forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView (Contexted FL p wX wY
cs p wY wZ
p) = forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL p wX wY
cs forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p)
ctxToFL :: Contexted p wX -> Sealed (FL p wX)
ctxToFL :: forall (p :: * -> * -> *) wX. Contexted p wX -> Sealed (FL p wX)
ctxToFL (forall (p :: * -> * -> *) wX.
Contexted p wX -> Sealed ((:>) (FL p) p wX)
ctxView -> Sealed (FL p wX wZ
ps :> p wZ wX
p)) = forall (a :: * -> *) wX. a wX -> Sealed a
Sealed (FL p wX wZ
ps forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ p wZ wX
p forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: forall (a :: * -> * -> *) wX. FL a wX wX
NilFL)
ctx :: p wX wY -> Contexted p wX
ctx :: forall (p :: * -> * -> *) wX wY. p wX wY -> Contexted p wX
ctx p wX wY
p = forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX wZ -> Contexted p wX
Contexted forall (a :: * -> * -> *) wX. FL a wX wX
NilFL p wX wY
p
ctxAdd :: (Commute p, Invert p, Ident p)
=> p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd :: forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
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' <- forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Ident p) =>
p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)
fastRemoveFL (forall (p :: * -> * -> *) wX wY. Invert p => p wX wY -> p wY wX
invert p wX wY
p) FL p wY wY
ps = forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX 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 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 -> forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX wZ -> Contexted p wX
Contexted (p wX wY
p forall (a :: * -> * -> *) wX wX wZ.
a wX wX -> FL a wX wZ -> FL a wX wZ
:>: FL p wY wY
ps) p wY wZ
q
ctxAddRL :: (Commute p, Invert p, Ident p)
=> RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL :: 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
NilRL Contexted p wY
cp = Contexted p wY
cp
ctxAddRL (RL p wX wY
ps :<: p wY wY
p) Contexted p wY
cp = 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 (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)
ctxAddInvFL :: (Commute p, Invert p, Ident p)
=> FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL :: forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wX -> Contexted p wY
ctxAddInvFL = forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
RL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddRL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) wX wY.
Invert p =>
FL p wX wY -> RL p wY wX
invertFL
ctxAddFL :: (Commute p, Invert p, Ident p)
=> FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL :: forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
FL p wX wY -> Contexted p wY -> Contexted p wX
ctxAddFL FL p wX wY
NilFL Contexted p wY
t = Contexted p wY
t
ctxAddFL (p wX wY
p :>: FL p wY wY
ps) Contexted p wY
t = forall (p :: * -> * -> *) wX wY.
(Commute p, Invert p, Ident p) =>
p wX wY -> Contexted p wY -> Contexted p wX
ctxAdd p wX wY
p (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)
commutePast :: Commute p
=> p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast :: forall (p :: * -> * -> *) wX wY.
Commute p =>
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' <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wX wY
q 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
_ <- forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wY
q' forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
p)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX wZ -> Contexted p wX
Contexted FL p wX wZ
ps' p wZ wZ
p')
commutePastRL :: Commute p
=> RL p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePastRL :: forall (p :: * -> * -> *) wX wY.
Commute p =>
RL p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePastRL = 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 (p :: * -> * -> *) wX wY.
Commute p =>
p wX wY -> Contexted p wY -> Maybe (Contexted p wX)
commutePast
ctxTouches :: PatchInspect p => Contexted p wX -> [AnchoredPath]
ctxTouches :: forall (p :: * -> * -> *) wX.
PatchInspect p =>
Contexted p wX -> [AnchoredPath]
ctxTouches (Contexted FL p wX wY
ps p wY wZ
p) =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
p wX wY -> [AnchoredPath]
listTouchedFiles p wY wZ
p forall a. a -> [a] -> [a]
: forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL 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 :: forall (p :: * -> * -> *) wX.
PatchInspect p =>
(ByteString -> Bool) -> Contexted p wX -> Bool
ctxHunkMatches ByteString -> Bool
f (Contexted FL p wX wY
ps p wY wZ
p) = forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f FL p wX wY
ps Bool -> Bool -> Bool
|| forall (p :: * -> * -> *) wX wY.
PatchInspect p =>
(ByteString -> Bool) -> p wX wY -> Bool
hunkMatches ByteString -> Bool
f p wY wZ
p
showCtx :: (ShowPatchBasic p, PatchListFormat p)
=> ShowPatchFor -> Contexted p wX -> Doc
showCtx :: forall (p :: * -> * -> *) wX.
(ShowPatchBasic p, PatchListFormat p) =>
ShowPatchFor -> Contexted p wX -> Doc
showCtx ShowPatchFor
f (Contexted FL p wX wY
c p wY wZ
p) =
String -> Doc -> Doc
hiddenPrefix String
"|" (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
$$ 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 :: forall (p :: * -> * -> *) wX.
(ReadPatch p, PatchListFormat p) =>
Parser (Contexted p wX)
readCtx = do
Sealed FL p wX wX
ps <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
ByteString -> Parser ()
lexString (String -> ByteString
BC.pack String
":")
Sealed p wX wX
p <- forall (p :: * -> * -> *) wX. ReadPatch p => Parser (Sealed (p wX))
readPatch'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) wX wX wZ.
FL p wX wX -> p wX wZ -> Contexted p wX
Contexted FL p wX wX
ps p wX wX
p