{-# OPTIONS_GHC -cpp -fglasgow-exts #-} {-# LANGUAGE CPP #-} -- , GADTs, PatternGuards #-} #include "gadts.h" module Darcs.Patch.Core ( Patch(..), Named(..), join_patchesFL, concatFL, flattenFL, nullP, isNullPatch, infopatch, n_fn, adddeps, namepatch, anonymous, merger_undo, isMerger, getdeps, patch2patchinfo, patchname, patchcontents, ) where import Prelude hiding ( pi ) import Darcs.Patch.Info ( PatchInfo, patchinfo, make_filename ) import Darcs.Patch.Patchy ( Patchy ) import Darcs.Witnesses.Ordered import Darcs.Patch.Prim ( Prim(..), FromPrim(..), Effect(effect, effectRL), n_fn ) #include "impossible.h" data Patch C(x y) where PP :: Prim C(x y) -> Patch C(x y) ComP :: FL Patch C(x y) -> Patch C(x y) Merger :: Patch C(x y) -> RL Patch C(x b) -> Patch C(c b) -> Patch C(c d) -> Patch C(x y) Regrem :: Patch C(x y) -> RL Patch C(x b) -> Patch C(c b) -> Patch C(c a) -> Patch C(y x) instance FromPrim Patch where fromPrim = PP -- | The @Named@ type adds a patch info about a patch, that is a name. data Named p C(x y) where NamedP :: !PatchInfo -> ![PatchInfo] -> !(p C(x y)) -> Named p C(x y) -- ^ @NamedP info deps p@ represents patch @p@ with name -- @info@. @deps@ is a list of dependencies added at the named patch -- level, compared with the unnamed level (ie, dependencies added with -- @darcs record --ask-deps@). instance Effect p => Effect (Named p) where effect (NamedP _ _ p) = effect p effectRL (NamedP _ _ p) = effectRL p isNullPatch :: Patch C(x y) -> Bool isNullPatch (ComP ps) = and $ mapFL isNullPatch ps isNullPatch _ = False nullP :: Patch C(x y) -> EqCheck C(x y) nullP (ComP NilFL) = IsEq nullP (ComP (x:>:xs)) | IsEq <- nullP x = nullP (ComP xs) nullP _ = NotEq isMerger :: Patch C(a b) -> Bool isMerger (Merger _ _ _ _) = True isMerger (Regrem _ _ _ _) = True isMerger _ = False merger_undo :: Patch C(x y) -> Patch C(x y) merger_undo (Merger undo _ _ _) = undo merger_undo _ = impossible\end{code} %Another nice thing to be able to do with composite patches is to `flatten' %them, that is, turn them into a simple list of patches (appropriately %ordered, of course), with all nested compositeness unnested. \begin{code}

{- INLINE flattenFL -} flattenFL :: Patch C(x y) -> FL Patch C(x y) flattenFL (ComP ps) = concatFL (mapFL_FL flattenFL ps) flattenFL (PP Identity) = NilFL flattenFL p = p :>: NilFL join_patchesFL :: FL Patch C(x y) -> Patch C(x y) join_patchesFL ps = ComP $! ps infopatch :: Patchy p => PatchInfo -> p C(x y) -> Named p C(x y) adddeps :: Named p C(x y) -> [PatchInfo] -> Named p C(x y) getdeps :: Named p C(x y) -> [PatchInfo] namepatch :: Patchy p => String -> String -> String -> [String] -> p C(x y) -> IO (Named p C(x y)) namepatch date name author desc p | '\n' `elem` name = error "Patch names cannot contain newlines." | otherwise = do pinf <- patchinfo date name author desc return $ NamedP pinf [] p anonymous :: Patchy p => p C(x y) -> IO (Named p C(x y)) anonymous p = namepatch "today" "anonymous" "unknown" ["anonymous"] p infopatch pi p = NamedP pi [] p adddeps (NamedP pi _ p) ds = NamedP pi ds p getdeps (NamedP _ ds _) = ds patch2patchinfo :: Named p C(x y) -> PatchInfo patch2patchinfo (NamedP i _ _) = i patchname :: Named p C(x y) -> String patchname (NamedP i _ _) = make_filename i patchcontents :: Named p C(x y) -> p C(x y) patchcontents (NamedP _ _ p) = p\end{code} The simplest relationship between two patches is that of ``sequential'' patches, which means that the context of the second patch (the one on the left) consists of the first patch (on the right) plus the context of the first patch. The composition of two patches (which is also a patch) refers to the patch which is formed by first applying one and then the other. The composition of two patches, $P_1$ and $P_2$ is represented as $P_2P_1$, where $P_1$ is to be applied first, then $P_2$\footnote{This notation is inspired by the notation of matrix multiplication or the application of operators upon a Hilbert space. In the algebra of patches, there is multiplication (i.e.\ composition), which is associative but not commutative, but no addition or subtraction.} There is one other very useful relationship that two patches can have, which is to be parallel patches, which means that the two patches have an identical context (i.e.\ their representation applies to identical trees). This is represented by $P_1\parallel P_2$. Of course, two patches may also have no simple relationship to one another. In that case, if you want to do something with them, you'll have to manipulate them with respect to other patches until they are either in sequence or in parallel. The most fundamental and simple property of patches is that they must be invertible. The inverse of a patch is described by: $P^{ -1}$. In the darcs implementation, the inverse is required to be computable from knowledge of the patch only, without knowledge of its context, but that (although convenient) is not required by the theory of patches. \begin{dfn} The inverse of patch $P$ is $P^{ -1}$, which is the ``simplest'' patch for which the composition \( P^{ -1} P \) makes no changes to the tree. \end{dfn} Using this definition, it is trivial to prove the following theorem relating to the inverse of a composition of two patches. \begin{thm} The inverse of the composition of two patches is \[ (P_2 P_1)^{ -1} = P_1^{ -1} P_2^{ -1}. \] \end{thm} Moreover, it is possible to show that the right inverse of a patch is equal to its left inverse. In this respect, patches continue to be analogous to square matrices, and indeed the proofs relating to these properties of the inverse are entirely analogous to the proofs in the case of matrix multiplication. The compositions proofs can also readily be extended to the composition of more than two patches. \begin{code}

\end{code}