module Darcs.Patch.Ident ( Ident(..) , SignedIdent , PatchId , SignedId(..) , StorableId(..) , IdEq2(..) , merge2FL , fastRemoveFL , fastRemoveRL , fastRemoveSubsequenceRL , findCommonFL , commuteToPrefix , commuteToPostfix , commuteWhatWeCanToPostfix -- * Properties , prop_identInvariantUnderCommute , prop_sameIdentityImpliesCommutable , prop_equalImpliesSameIdentity ) where import qualified Data.Set as S import Darcs.Prelude import Darcs.Patch.Commute ( Commute, commute, commuteFL, commuteRL ) import Darcs.Patch.Merge ( Merge, mergeFL ) import Darcs.Patch.Permutations ( partitionFL', commuteWhatWeCanFL ) import Darcs.Patch.Show ( ShowPatchFor ) import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..), isIsEq ) import Darcs.Patch.Witnesses.Ordered ( (:/\:)(..) , (:>)(..) , (:\/:)(..) , FL(..) , RL(..) , Fork(..) , (+<<+) , (+>>+) , mapFL , mapRL , reverseRL ) import Darcs.Patch.Witnesses.Unsafe ( unsafeCoercePEnd, unsafeCoercePStart ) import Darcs.Util.Parser ( Parser ) import Darcs.Util.Printer ( Doc ) type family PatchId (p :: * -> * -> *) {- | Class of patches that have an identity. It generalizes named prim patches a la camp (see Darcs.Patch.Prim.Named) and Named patches i.e. those with a PatchInfo. Patch identity should be invariant under commutation: if there is also an @instance 'Commute' p@, then prop> commute (p :> q) == Just (q' :> p') => ident p == ident p' && ident q == ident q' The converse should also be true: patches with the same identity can be commuted (back) to the same context and then compare equal. Assuming @ p :: p wX wY, (ps :> q) :: (RL p :> p) wX wZ @ then prop> ident p == ident q => commuteRL (ps :> q) == Just (p :> _) As a special case we get that parallel patches with the same identity are equal: if @p :: p wX wY, q :: p wX wZ@, then prop> ident p == ident q => p =\/= q == IsEq In general, comparing patches via their identity is coarser than (structural) equality, so we only have prop> unsafeCompare p q => (ident p == ident q) -} class Ord (PatchId p) => Ident p where ident :: p wX wY -> PatchId p {- | Signed identities. Like for class 'Invert', we require that 'invertId' is self-inverse: prop> invertId . invertId = id We also require that inverting changes the sign: prop> positiveId . invertId = not . positiveId Side remark: in mathematical terms, these properties can be expressed by stating that 'invertId' is an involution and that 'positiveId' is a "homomorphism of sets with an involution" (there is no official term for this) from @a@ to the simplest non-trivial set with involution, namely 'Bool' with the involution 'not'. -} class Ord a => SignedId a where positiveId :: a -> Bool invertId :: a -> a {- | Constraint for patches that have an identity that is signed, i.e. can be positive (uninverted) or negative (inverted). Provided that an instance 'Invert' exists, inverting a patch inverts its identity: prop> ident (invert p) = invertId (ident p) -} type SignedIdent p = (Ident p, SignedId (PatchId p)) {- | Storable identities. The methods here can be used to help implement ReadPatch and ShowPatch for a patch type containing the identity. As with all Read/Show pairs, We expect that the output of @showId ForStorage a@ can be parsed by 'readId' to produce @a@. -} class StorableId a where readId :: Parser a showId :: ShowPatchFor -> a -> Doc -- | Faster equality tests for patches with an identity. class IdEq2 p where (=\^/=) :: p wA wB -> p wA wC -> EqCheck wB wC (=/^\=) :: p wA wC -> p wB wC -> EqCheck wA wB default (=\^/=) :: Ident p => p wA wB -> p wA wC -> EqCheck wB wC p =\^/= q = if ident p == ident q then unsafeCoercePEnd IsEq else NotEq default (=/^\=) :: Ident p => p wA wC -> p wB wC -> EqCheck wA wB p =/^\= q = if ident p == ident q then unsafeCoercePStart IsEq else NotEq -- | The 'Commute' requirement here is not technically needed but makes -- sense logically. instance (Commute p, Ident p) => IdEq2 (FL p) where ps =\^/= qs | S.fromList (mapFL ident ps) == S.fromList (mapFL ident qs) = unsafeCoercePEnd IsEq | otherwise = NotEq ps =/^\= qs | S.fromList (mapFL ident ps) == S.fromList (mapFL ident qs) = unsafeCoercePStart IsEq | otherwise = NotEq -- | This function is similar to 'merge', but with one important -- difference: 'merge' works on patches for which there is not necessarily a -- concept of identity (e.g. primitive patches, conflictors, etc). Thus it does -- not even try to recognize patches that are common to both sequences. Instead -- these are passed on to the Merge instance for single patches. This instance -- may handle duplicate patches by creating special patches (Duplicate, -- Conflictor). -- -- We do not want this to happen for named patches, or in general for patches -- with an identity. Instead, we want to -- /discard/ one of the two duplicates, retaining only one copy. This is done -- by the fastRemoveFL calls below. We call mergeFL only after we have ensured -- that the head of the left hand side does not occur in the right hand side. merge2FL :: (Commute p, Merge p, Ident p) => FL p wX wY -> FL p wX wZ -> (FL p :/\: FL p) wY wZ merge2FL xs NilFL = NilFL :/\: xs merge2FL NilFL ys = ys :/\: NilFL merge2FL xs (y :>: ys) | Just xs' <- fastRemoveFL y xs = merge2FL xs' ys merge2FL (x :>: xs) ys | Just ys' <- fastRemoveFL x ys = merge2FL xs ys' | otherwise = case mergeFL (x :\/: ys) of ys' :/\: x' -> case merge2FL xs ys' of ys'' :/\: xs' -> ys'' :/\: (x' :>: xs') {-# INLINABLE fastRemoveFL #-} -- | Remove a patch from an FL of patches with an identity. The result is -- 'Just' whenever the patch has been found and removed and 'Nothing' -- otherwise. If the patch is not found at the head of the sequence we must -- first commute it to the head before we can remove it. -- -- We assume that this commute always succeeds. This is justified because -- patches are created with a (universally) unique identity, implying that if -- two patches have the same identity, then they have originally been the same -- patch; thus being at a different position must be due to commutation, -- meaning we can commute it back. fastRemoveFL :: forall p wX wY wZ. (Commute p, Ident p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ) fastRemoveFL a bs | i `notElem` mapFL ident bs = Nothing | otherwise = do _ :> bs' <- pullout NilRL bs Just (unsafeCoercePStart bs') where i = ident a pullout :: RL p wA wB -> FL p wB wC -> Maybe ((p :> FL p) wA wC) pullout _ NilFL = Nothing pullout acc (x :>: xs) | ident x == i = do x' :> acc' <- commuteRL (acc :> x) Just (x' :> acc' +>>+ xs) | otherwise = pullout (acc :<: x) xs -- | Same as 'fastRemoveFL' only for 'RL'. fastRemoveRL :: forall p wX wY wZ. (Commute p, Ident p) => p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY) fastRemoveRL a bs | i `notElem` mapRL ident bs = Nothing | otherwise = do bs' :> _ <- pullout bs NilFL Just (unsafeCoercePEnd bs') where i = ident a pullout :: RL p wA wB -> FL p wB wC -> Maybe ((RL p :> p) wA wC) pullout NilRL _ = Nothing pullout (xs :<: x) acc | ident x == i = do acc' :> x' <- commuteFL (x :> acc) Just (xs +<<+ acc' :> x') | otherwise = pullout xs (x :>: acc) fastRemoveSubsequenceRL :: (Commute p, Ident p) => RL p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY) fastRemoveSubsequenceRL NilRL ys = Just ys fastRemoveSubsequenceRL (xs :<: x) ys = fastRemoveRL x ys >>= fastRemoveSubsequenceRL xs -- | Find the common and uncommon parts of two lists that start in a common -- context, using patch identity for comparison. Of the common patches, only -- one is retained, the other is discarded, similar to 'merge2FL'. findCommonFL :: (Commute p, Ident p) => FL p wX wY -> FL p wX wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ findCommonFL xs ys = case commuteToPrefix commonIds xs of Nothing -> error "failed to commute common patches (lhs)" Just (cxs :> xs') -> case commuteToPrefix commonIds ys of Nothing -> error "failed to commute common patches (rhs)" Just (cys :> ys') -> case cxs =\^/= cys of NotEq -> error "common patches aren't equal" IsEq -> Fork cxs (reverseRL xs') (reverseRL ys') where commonIds = S.fromList (mapFL ident xs) `S.intersection` S.fromList (mapFL ident ys) -- | Try to commute patches matching any of the 'PatchId's in the set to the -- head of an 'FL', i.e. backwards in history. It is not required that all the -- 'PatchId's are found in the sequence, but if they do then the traversal -- terminates as soon as the set is exhausted. commuteToPrefix :: (Commute p, Ident p) => S.Set (PatchId p) -> FL p wX wY -> Maybe ((FL p :> RL p) wX wY) commuteToPrefix is ps | prefix :> NilRL :> rest <- partitionFL' ((`S.member` is) . ident) NilRL NilRL ps = Just (prefix :> rest) | otherwise = Nothing -- | Try to commute patches matching any of the 'PatchId's in the set to the -- head of an 'RL', i.e. forwards in history. It is not required that all the -- 'PatchId's are found in the sequence, but if they do then the traversal -- terminates as soon as the set is exhausted. commuteToPostfix :: forall p wX wY. (Commute p, Ident p) => S.Set (PatchId p) -> RL p wX wY -> Maybe ((FL p :> RL p) wX wY) commuteToPostfix ids patches = push ids (patches :> NilFL) where push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> Maybe ((FL p :> RL p) wA wB) push _ (NilRL :> left) = return (left :> NilRL) -- input RL is ehausted push is (ps :> left) | S.null is = return (ps +>>+ left :> NilRL) -- set of IDs is exhausted push is (ps :<: p :> left) | let i = ident p , i `S.member` is = do left' :> p' <- commuteFL (p :> left) left'' :> right <- push (S.delete i is) (ps :> left') return (left'' :> right :<: p') | otherwise = push is (ps :> p :>: left) -- | Like 'commuteToPostfix' but drag dependencies with us. commuteWhatWeCanToPostfix :: forall p wX wY. (Commute p, Ident p) => S.Set (PatchId p) -> RL p wX wY -> (FL p :> RL p) wX wY commuteWhatWeCanToPostfix ids patches = push ids (patches :> NilFL) where push :: S.Set (PatchId p) -> (RL p :> FL p) wA wB -> (FL p :> RL p) wA wB push _ (NilRL :> left) = left :> NilRL -- input RL is ehausted push is (ps :> left) | S.null is = ps +>>+ left :> NilRL -- set of IDs is exhausted push is (ps :<: p :> left) | let i = ident p , i `S.member` is = case commuteWhatWeCanFL (p :> left) of left' :> p' :> deps -> case push (S.delete i is) (ps :> left') of left'' :> right -> left'' :> (right :<: p' +<<+ deps) | otherwise = push is (ps :> p :>: left) prop_identInvariantUnderCommute :: (Commute p, Ident p) => (p :> p) wX wY -> Maybe Bool prop_identInvariantUnderCommute (p :> q) = case commute (p :> q) of Just (q' :> p') -> Just $ ident p == ident p' && ident q == ident q' Nothing -> Nothing prop_sameIdentityImpliesCommutable :: (Commute p, Eq2 p, Ident p) => (p :\/: (RL p :> p)) wX wY -> Maybe Bool prop_sameIdentityImpliesCommutable (p :\/: (ps :> q)) | ident p == ident q = case commuteRL (ps :> q) of Just (p' :> _) -> Just $ isIsEq (p =\/= p') Nothing -> Just False | otherwise = Nothing prop_equalImpliesSameIdentity :: (Eq2 p, Ident p) => (p :\/: p) wX wY -> Maybe Bool prop_equalImpliesSameIdentity (p :\/: q) | IsEq <- p =\/= q = Just $ ident p == ident q | otherwise = Nothing