Darcs.Patch.Ident

Documentation

class Ord (PatchId p) => Ident p where

Class of patches that have an identity/name.

Patches with an identity give rise to the notion of nominal equality, expressed by the operators =\^/= and =/^\=.

Laws:

ident-commute

Patch identity must be invariant under commutation:

'commute' (p :> _) == 'Just' (_ :> p') => 'ident' p == 'ident' p'

and thus (via symmetry of commute):

'commute' (_ :> q) == 'Just' (q' :> _) => 'ident' q == 'ident' q'

Conversely, patches with the same identity result from a series of commutes:

'ident' p == 'ident' p' => exists qs, qs' :: FL p. 'commuteFL' (p :> qs) == 'Just' (qs' :> p')

ident-compare

In general, comparing patches via their identity is weaker than (semantic) equality:

'unsafeCompare' p q => 'ident' p == 'ident' q

However, if the patches have a common context, then semantic and nominal equality should coincide, up to internal re-ordering:

p '=\~/=' q  <=> p '=\^/=' q

p '=/~\=' q  <=> p '=/^\=' q

(Technical note: equality up to internal re-ordering is currently only defined for FLs, but it should be obvious how to generalize it.)

Taken together, these laws express the assumption that recording a patch gives it a universally unique identity.

Note that violations of this universal property are currently not detected in a reliable way. Fixing this is possible but far from easy.

Methods

ident :: p wX wY -> PatchId p

Instances

Ident p => Ident (Invertible p)

Defined in Darcs.Patch.Invertible

Methods

ident :: Invertible p wX wY -> PatchId (Invertible p)

Ident (Named p)

Defined in Darcs.Patch.Named

Methods

ident :: Named p wX wY -> PatchId (Named p)

Ident (PatchInfoAndG p)

Defined in Darcs.Patch.PatchInfoAnd

Methods

ident :: PatchInfoAndG p wX wY -> PatchId (PatchInfoAndG p)

Ident (RebaseChange prim)

Defined in Darcs.Patch.Rebase.Change

Methods

ident :: RebaseChange prim wX wY -> PatchId (RebaseChange prim)

Ident (PatchSet p)

Defined in Darcs.Patch.Set

Methods

ident :: PatchSet p wX wY -> PatchId (PatchSet p)

Ident p => Ident (FL p)

Defined in Darcs.Patch.Ident

Methods

ident :: FL p wX wY -> PatchId (FL p)

Ident p => Ident (RL p)

Defined in Darcs.Patch.Ident

Methods

ident :: RL p wX wY -> PatchId (RL p)

SignedId name => Ident (PrimWithName name p)

Defined in Darcs.Patch.Prim.WithName

Methods

ident :: PrimWithName name p wX wY -> PatchId (PrimWithName name p)

SignedId name => Ident (RepoPatchV3 name prim)

Defined in Darcs.Patch.V3.Core

Methods

ident :: RepoPatchV3 name prim wX wY -> PatchId (RepoPatchV3 name prim)

Ident p => Ident (p :> p)

Defined in Darcs.Patch.Ident

Methods

ident :: (p :> p) wX wY -> PatchId (p :> p)

type SignedIdent p = (Ident p, SignedId (PatchId p))

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:

'ident' ('invert' p) = 'invertId' ('ident' p)

type family PatchId (p :: * -> * -> *)

The reason this is not associated to class Ident is that for technical reasons we want to be able to define type instances for patches that don't have an identity and therefore cannot be lawful members of class Ident.

Instances

type PatchId (Invertible p)

Defined in Darcs.Patch.Invertible

type PatchId (Invertible p)

type PatchId (Named p)

Defined in Darcs.Patch.Named

type PatchId (Named p) = PatchInfo

type PatchId (PatchInfoAndG p)

Defined in Darcs.Patch.PatchInfoAnd

type PatchId (PatchInfoAndG p) = PatchInfo

type PatchId (NamedPrim p)

Defined in Darcs.Patch.Prim.Named

type PatchId (NamedPrim p) = PrimPatchId

type PatchId (RebaseChange prim)

Defined in Darcs.Patch.Rebase.Change

type PatchId (RebaseChange prim) = PatchInfo

type PatchId (PatchSet p)

Defined in Darcs.Patch.Set

type PatchId (PatchSet p) = Set PatchInfo

type PatchId (RepoPatchV1 prim)

Defined in Darcs.Patch.V1.Core

type PatchId (RepoPatchV1 prim) = ()

type PatchId (RepoPatchV2 prim)

Defined in Darcs.Patch.V2.RepoPatch

type PatchId (RepoPatchV2 prim) = ()

type PatchId (FL p)

Defined in Darcs.Patch.Ident

type PatchId (FL p) = Set (PatchId p)

type PatchId (RL p)

Defined in Darcs.Patch.Ident

type PatchId (RL p) = Set (PatchId p)

type PatchId (PrimWithName name p)

Defined in Darcs.Patch.Prim.WithName

type PatchId (PrimWithName name p) = name

type PatchId (RepoPatchV3 name prim)

Defined in Darcs.Patch.V3.Core

type PatchId (RepoPatchV3 name prim) = name

type PatchId (p :> p)

Defined in Darcs.Patch.Ident

type PatchId (p :> p) = Set (PatchId p)

(=\^/=) :: Ident p => p wA wB -> p wA wC -> EqCheck wB wC

Nominal equality for patches with an identity in the same context. Usually quite a bit faster than structural equality.

(=/^\=) :: Ident p => p wA wC -> p wB wC -> EqCheck wA wB

class Ord a => SignedId a where

Signed identities.

Like for class Invert, we require that invertId is self-inverse:

'invertId' . 'invertId' = 'id'

We also require that inverting changes the sign:

'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.

Methods

positiveId :: a -> Bool

invertId :: a -> a

Instances

SignedId PrimPatchId

Defined in Darcs.Patch.Prim.Named

Methods

positiveId :: PrimPatchId -> Bool

invertId :: PrimPatchId -> PrimPatchId

class StorableId a where

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 x can be parsed by readId to produce x:

'parse' 'readId' . 'renderPS' . 'showId' 'ForStorage' == 'id'

Methods

readId :: Parser a

showId :: ShowPatchFor -> a -> Doc

Instances

StorableId PrimPatchId

Defined in Darcs.Patch.Prim.Named

Methods

readId :: Parser PrimPatchId

showId :: ShowPatchFor -> PrimPatchId -> Doc

fastRemoveFL :: forall p wX wY wZ. (Commute p, Ident p) => p wX wY -> FL p wX wZ -> Maybe (FL p wY wZ)

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.

For patch types that define semantic equality via nominal equality, this is only faster than removeFL if the patch does not occur in the sequence, otherwise we have to perform the same number of commutations.

fastRemoveRL :: forall p wX wY wZ. (Commute p, Ident p) => p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)

Same as fastRemoveFL only for RL.

fastRemoveSubsequenceRL :: (Commute p, Ident p) => RL p wY wZ -> RL p wX wZ -> Maybe (RL p wX wY)

findCommonFL :: (Commute p, Ident p) => FL p wX wY -> FL p wX wZ -> Fork (FL p) (FL p) (FL p) wX wY wZ

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.

findCommonRL :: (Commute p, Ident p) => RL p wX wY -> RL p wX wZ -> Fork (RL p) (RL p) (RL p) wX wY wZ

findCommonWithThemFL :: (Commute p, Ident p) => FL p wX wY -> FL p wX wZ -> (FL p :> FL p) wX wY

findCommonWithThemRL :: (Commute p, Ident p) => RL p wX wY -> RL p wX wZ -> (RL p :> RL p) wX wY

commuteToPrefix :: (Commute p, Ident p) => Set (PatchId p) -> FL p wX wY -> Maybe ((FL p :> RL p) wX wY)

Try to commute all patches matching any of the PatchIds in the set to the head of an FL, i.e. backwards in history.

Properties

prop_identInvariantUnderCommute :: (Commute p, Ident p) => (p :> p) wX wY -> Maybe Bool

prop_sameIdentityImpliesCommutable :: (Commute p, Eq2 p, Ident p) => (p :\/: (RL p :> p)) wX wY -> Maybe Bool

prop_equalImpliesSameIdentity :: (Eq2 p, Ident p) => p wA wB -> p wC wD -> Maybe Bool

prop_sameIdentityImpliesEqual :: (Eq2 p, Ident p) => (p :\/: p) wX wY -> Maybe Bool