% Copyright (C) 2007 David Roundy
%
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2, or (at your option)
% any later version.
%
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU General Public License
% along with this program; see the file COPYING. If not, write to
% the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
% Boston, MA 02110-1301, USA.
\documentclass{article}
%\usepackage{color}
\usepackage{verbatim}
\usepackage{html}
\usepackage{fancyvrb}
\newenvironment{code}{\comment}{\endcomment}
% \newenvironment{code}{\color{blue}\verbatim}{\endverbatim}
\newcommand{\commutes}{\longleftrightarrow}
\begin{document}
\begin{code}
#include "gadts.h"
module Darcs.Patch.Properties ( recommute, commute_inverses, permutivity, partial_permutivity,
identity_commutes, inverse_doesnt_commute,
patch_and_inverse_commute, merge_either_way,
show_read,
merge_commute, merge_consistent, merge_arguments_consistent,
join_inverses, join_commute ) where
import Control.Monad ( msum, mplus )
import Darcs.Witnesses.Show ( Show2(..) )
import Darcs.Patch.Patchy
import Darcs.Patch.Prim
import Darcs.Patch ()
import Darcs.Patch.Read ( readPatch )
import Darcs.Witnesses.Ordered
import Darcs.Witnesses.Sealed ( Sealed(Sealed) )
import Printer ( Doc, renderPS, redText, greenText, ($$) )
\end{code}
\section{Patch properties}
Darcs is built on a hierarchy of patch types. At the lowest level are
``primitive'' patches, and from these building blocks, a whole hierarchy of
patch types are built. Each of these patch types must support a number of
functions, which must obey a number of laws.
\subsection{Properties of identity}
\newtheorem{prp}{Property}
\begin{prp}[Identity commutes trivially]
The identity patch must commute with any patch without modifying said patch.
\end{prp}
\begin{code}
identity_commutes :: forall p C(x y). Patchy p => p C(x y) -> Maybe Doc
identity_commutes p = case commute (p :> identity) of
Nothing -> Just $ redText "identity_commutes failed:" $$ showPatch p
Just (i :> p') | IsEq <- i =\/= identity,
IsEq <- p' =\/= p ->
checkRightIdentity $ commute $ identity :> p
Just _ -> Just $ greenText "identity_commutes"
where checkRightIdentity :: Maybe ((p :> p) C(x y)) -> Maybe Doc
checkRightIdentity Nothing = Just $ redText "identity_commutes failed 2:" $$ showPatch p
checkRightIdentity (Just (p2 :> i2)) | IsEq <- i2 =\/= identity,
IsEq <- p2 =\/= p = Nothing
checkRightIdentity (Just _) = Just $ greenText "identity_commutes 2"
\end{code}
\begin{prp}[Inverse doesn't commute]
A patch and its inverse will always commute, unless that patch is an
identity patch (or an identity-like patch that has no effect).
\end{prp}
\begin{code}
inverse_doesnt_commute :: Patchy p => p C(a b) -> Maybe Doc
inverse_doesnt_commute p | IsEq <- sloppyIdentity p = Nothing
| otherwise = do p' :> _ <- commute (invert p :> p)
Just $ redText "inverse_doesnt_commute" $$ showPatch p'
\end{code}
\subsection{Commute properties}
\begin{prp}[Recommute]
$AB \commutes B'A'$ if and only if $B'A' \commutes AB$
\end{prp}
\begin{code}
recommute :: Patchy p => (FORALL(x y) ((p :> p) C(x y) -> Maybe ((p :> p) C(x y))))
-> (p :> p) C(a b) -> Maybe Doc
recommute c (x :> y) =
case c (x :> y) of
Nothing -> Nothing
Just (y' :> x') ->
case c (y' :> x') of
Nothing -> Just (redText "failed" $$ showPatch y' $$ redText ":>" $$ showPatch x')
Just (x'' :> y'') ->
case y'' =/\= y of
NotEq -> Just (redText "y'' =/\\= y failed, where x" $$ showPatch x $$
redText ":> y" $$ showPatch y $$
redText "y'" $$ showPatch y' $$
redText ":> x'" $$ showPatch x' $$
redText "x''" $$ showPatch x'' $$
redText ":> y''" $$ showPatch y'')
IsEq -> case x'' =/\= x of
NotEq -> Just (redText "x'' /= x" $$ showPatch x'' $$ redText ":>" $$ showPatch y'')
IsEq -> Nothing
\end{code}
\begin{prp}[Commute inverses]
$AB \commutes B'A'$ if and only if $B^{-1}A^{-1} \commutes A'^{-1}B'^{-1}$
\end{prp}
\begin{code}
commute_inverses :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
-> (p :> p) C(a b) -> Maybe Doc
commute_inverses c (x :> y) =
case c (x :> y) of
Nothing -> Nothing
Just (y' :> x') ->
case c (invert y :> invert x) of
Nothing -> Just $ redText "second commute failed" $$
redText "x" $$ showPatch x $$ redText "y" $$ showPatch y $$
redText "y'" $$ showPatch y' $$ redText "x'" $$ showPatch x'
Just (ix' :> iy') ->
case invert ix' =/\= x' of
NotEq -> Just $ redText "invert ix' /= x'" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "y'" $$ showPatch y' $$
redText "x'" $$ showPatch x' $$
redText "ix'" $$ showPatch ix' $$
redText "iy'" $$ showPatch iy' $$
redText "invert ix'" $$ showPatch (invert ix') $$
redText "invert iy'" $$ showPatch (invert iy')
IsEq -> case y' =\/= invert iy' of
NotEq -> Just $ redText "y' /= invert iy'" $$ showPatch iy' $$ showPatch y'
IsEq -> Nothing
\end{code}
\begin{prp}[Patch and inverse]
If $AB \commutes B'A'$ then $A^{-1}B' \commutes BA'^{-1}$
\end{prp}
This property is only true of primitive patches.
\begin{code}
patch_and_inverse_commute :: Patchy p =>
(FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
-> (p :> p) C(a b) -> Maybe Doc
patch_and_inverse_commute c (x :> y) =
do y' :> x' <- c (x :> y)
case c (invert x :> y') of
Nothing -> Just (redText "failure in patch_and_inverse_commute")
Just (y'' :> ix') ->
case y'' =\/= y of
NotEq -> Just (redText "y'' /= y" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "x'" $$ showPatch x' $$
redText "y'" $$ showPatch y' $$
redText "y''" $$ showPatch y'' $$
redText ":> x'" $$ showPatch x')
IsEq -> case x' =\/= invert ix' of
NotEq -> Just (redText "x' /= invert ix'" $$
redText "y''" $$ showPatch y'' $$
redText ":> x'" $$ showPatch x' $$
redText "invert x" $$ showPatch (invert x) $$
redText ":> y" $$ showPatch y $$
redText "y'" $$ showPatch y' $$
redText "ix'" $$ showPatch ix')
IsEq -> Nothing
\end{code}
\begin{prp}[Permutivity]
(to be added...)
\end{prp}
\begin{code}
permutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
-> (p :> p :> p) C(a b) -> Maybe Doc
permutivity c (x:>y:>z) =
do y1 :> x1 <- c (x :> y)
z2 :> y2 <-
c (y :> z)
z3 :> x3 <-
c (x :> z2)
case c (x1 :> z) of
Nothing -> Just $ redText "permutivity1"
Just (z4 :> x4) ->
case c (y1 :> z4) of
Nothing -> Just $ redText "permutivity2"
Just (z3_ :> y4)
| IsEq <- z3_ =\/= z3 ->
case c (y4 :> x4) of
Nothing -> Just $ redText "permutivity5: input was" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "z" $$ showPatch z $$
redText "z3" $$ showPatch z3 $$
redText "failed commute of" $$
redText "y4" $$ showPatch y4 $$
redText "x4" $$ showPatch x4 $$
redText "whereas commute of x and y give" $$
redText "y1" $$ showPatch y1 $$
redText "x1" $$ showPatch x1
Just (x3_ :> y2_)
| NotEq <- x3_ =\/= x3 -> Just $ redText "permutivity6"
| NotEq <- y2_ =/\= y2 -> Just $ redText "permutivity7"
| otherwise -> Nothing
| otherwise ->
Just $ redText "permutivity failed" $$
redText "z3" $$ showPatch z3 $$
redText "z3_" $$ showPatch z3_
partial_permutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
-> (p :> p :> p) C(a b) -> Maybe Doc
partial_permutivity c (xx:>yy:>zz) = pp (xx:>yy:>zz) `mplus` pp (invert zz:>invert yy:>invert xx)
where pp (x:>y:>z) = do z1 :> y1 <- c (y :> z)
_ :> x1 <- c (x :> z1)
case c (x :> y) of
Just _ -> Nothing
Nothing ->
case c (x1 :> y1) of
Nothing -> Nothing
Just _ -> Just $ greenText "partial_permutivity error" $$
greenText "x" $$ showPatch x $$
greenText "y" $$ showPatch y $$
greenText "z" $$ showPatch z
merge_arguments_consistent :: Patchy p =>
(FORALL(x y) p C(x y) -> Maybe Doc)
-> (p :\/: p) C(a b) -> Maybe Doc
merge_arguments_consistent is_consistent (x :\/: y) =
msum [(\z -> redText "merge_arguments_consistent x" $$ showPatch x $$ z) `fmap` is_consistent x,
(\z -> redText "merge_arguments_consistent y" $$ showPatch y $$ z) `fmap` is_consistent y]
merge_consistent :: Patchy p =>
(FORALL(x y) p C(x y) -> Maybe Doc)
-> (p :\/: p) C(a b) -> Maybe Doc
merge_consistent is_consistent (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x' ->
msum [(\z -> redText "merge_consistent x" $$ showPatch x $$ z) `fmap` is_consistent x,
(\z -> redText "merge_consistent y" $$ showPatch y $$ z) `fmap` is_consistent y,
(\z -> redText "merge_consistent x'" $$ showPatch x' $$ z $$
redText "where x' comes from x" $$ showPatch x $$
redText "and y" $$ showPatch y) `fmap` is_consistent x',
(\z -> redText "merge_consistent y'" $$ showPatch y' $$ z) `fmap` is_consistent y']
merge_either_way :: Patchy p => (p :\/: p) C(x y) -> Maybe Doc
merge_either_way (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x' -> case merge (y :\/: x) of
x'' :/\: y'' | IsEq <- x'' =\/= x',
IsEq <- y'' =\/= y' -> Nothing
| otherwise -> Just $ redText "merge_either_way bug"
merge_commute :: Patchy p => (p :\/: p) C(x y) -> Maybe Doc
merge_commute (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x' ->
case commute (x :> y') of
Nothing -> Just $ redText "merge_commute 1" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "x'" $$ showPatch x' $$
redText "y'" $$ showPatch y'
Just (y_ :> x'_)
| IsEq <- y_ =\/= y,
IsEq <- x'_ =\/= x' ->
case commute (y :> x') of
Nothing -> Just $ redText "merge_commute 2 failed" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "x'" $$ showPatch x' $$
redText "y'" $$ showPatch y'
Just (x_ :> y'_)
| IsEq <- x_ =\/= x,
IsEq <- y'_ =\/= y' -> Nothing
| otherwise -> Just $ redText "merge_commute 3" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "x'" $$ showPatch x' $$
redText "y'" $$ showPatch y' $$
redText "x_" $$ showPatch x_ $$
redText "y'_" $$ showPatch y'_
| otherwise -> Just $ redText "merge_commute 4" $$
redText "x" $$ showPatch x $$
redText "y" $$ showPatch y $$
redText "x'" $$ showPatch x' $$
redText "y'" $$ showPatch y' $$
redText "x'_" $$ showPatch x'_ $$
redText "y_" $$ showPatch y_
join_inverses :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (Prim C(x y)))
-> Prim C(a b) -> Maybe Doc
join_inverses j p = case j (invert p :> p) of
Just Identity -> Nothing
Just p' -> Just $ redText "join_inverses gave just" $$ showPatch p'
Nothing -> Just $ redText "join_inverses failed"
join_commute :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (Prim C(x y)))
-> (Prim :> Prim :> Prim) C(a b) -> Maybe Doc
join_commute j (a :> b :> c) =
do x <- j (b :> c)
case commuteFL (a :> b :>: c :>: NilFL) of
Right (b' :>: c' :>: NilFL :> a') ->
case commute (a :> x) of
Nothing -> Just $ greenText "join_commute 1"
Just (x' :> a'') ->
case a'' =/\= a' of
NotEq -> Just $ greenText "join_commute 3"
IsEq -> case j (b' :> c') of
Nothing -> Just $ greenText "join_commute 4"
Just x'' -> case x' =\/= x'' of
NotEq -> Just $ greenText "join_commute 5"
IsEq -> Nothing
_ -> Nothing
show_read :: (Show2 p, Patchy p) => p C(a b) -> Maybe Doc
show_read p = let ps = renderPS (showPatch p)
in case readPatch ps of
Nothing -> Just (redText "unable to read " $$ showPatch p)
Just (Sealed p',_) | IsEq <- p' =\/= p -> Nothing
| otherwise -> Just $ redText "trouble reading patch p" $$
showPatch p $$
redText "reads as p'" $$
showPatch p' $$
redText "aka" $$
greenText (show2 p) $$
redText "and" $$
greenText (show2 p')
\end{code}
\end{document}