src/Darcs/Patch/Properties.lhs

   1 %  Copyright (C) 2007 David Roundy
   2 %
   3 %  This program is free software; you can redistribute it and/or modify
   4 %  it under the terms of the GNU General Public License as published by
   5 %  the Free Software Foundation; either version 2, or (at your option)
   6 %  any later version.
   7 %
   8 %  This program is distributed in the hope that it will be useful,
   9 %  but WITHOUT ANY WARRANTY; without even the implied warranty of
  10 %  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  11 %  GNU General Public License for more details.
  12 %
  13 %  You should have received a copy of the GNU General Public License
  14 %  along with this program; see the file COPYING.  If not, write to
  15 %  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  16 %  Boston, MA 02110-1301, USA.
  17
  18 \documentclass{article}
  19 %\usepackage{color}
  20
  21 \usepackage{verbatim}
  22 \usepackage{html}
  23 \usepackage{fancyvrb}
  24 \newenvironment{code}{\comment}{\endcomment}
  25 % \newenvironment{code}{\color{blue}\verbatim}{\endverbatim}
  26
  27 \newcommand{\commutes}{\longleftrightarrow}
  28
  29 \begin{document}
  30
  31 \begin{code}
  32 {-# LANGUAGE CPP #-}
  33 {-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts #-}
  34
  35 #include "gadts.h"
  36
  37 module Darcs.Patch.Properties ( recommute, commute_inverses, permutivity, partial_permutivity,
  38                                 identity_commutes, inverse_doesnt_commute,
  39                                 patch_and_inverse_commute, merge_either_way,
  40                                 show_read,
  41                                 merge_commute, merge_consistent, merge_arguments_consistent,
  42                                 join_inverses, join_commute ) where
  43
  44 import Control.Monad ( msum, mplus )
  45 import Darcs.Show ( Show2(..) )
  46 import Darcs.Patch.Patchy
  47 import Darcs.Patch.Prim
  48 import Darcs.Patch ()
  49 import Darcs.Patch.Read ( readPatch )
  50 import Darcs.Ordered
  51 import Darcs.Sealed ( Sealed(Sealed) )
  52 import Printer ( Doc, renderPS, redText, greenText, ($$) )
  53 --import Darcs.ColorPrinter ( traceDoc )
  54 \end{code}
  55
  56 \section{Patch properties}
  57
  58 Darcs is built on a hierarchy of patch types.  At the lowest level are
  59 ``primitive'' patches, and from these building blocks, a whole hierarchy of
  60 patch types are built.  Each of these patch types must support a number of
  61 functions, which must obey a number of laws.
  62
  63 \subsection{Properties of identity}
  64
  65 \newtheorem{prp}{Property}
  66
  67 \begin{prp}[Identity commutes trivially]
  68   The identity patch must commute with any patch without modifying said patch.
  69 \end{prp}
  70
  71 \begin{code}
  72 identity_commutes :: forall p C(x y). Patchy p => p C(x y) -> Maybe Doc
  73 identity_commutes p = case commute (p :> identity) of
  74                       Nothing -> Just $ redText "identity_commutes failed:" $$ showPatch p
  75                       Just (i :> p') | IsEq <- i =\/= identity,
  76                                        IsEq <- p' =\/= p ->
  77                               checkRightIdentity $ commute $ identity :> p
  78                       Just _ -> Just $ greenText "identity_commutes"
  79   where checkRightIdentity :: Maybe ((p :> p) C(x y)) -> Maybe Doc
  80         checkRightIdentity Nothing = Just $ redText "identity_commutes failed 2:" $$ showPatch p
  81         checkRightIdentity (Just (p2 :> i2)) | IsEq <- i2 =\/= identity,
  82                                                IsEq <- p2 =\/= p = Nothing
  83         checkRightIdentity (Just _) = Just $ greenText "identity_commutes 2"
  84 \end{code}
  85
  86 \begin{prp}[Inverse doesn't commute]
  87   A patch and its inverse will always commute, unless that patch is an
  88   identity patch (or an identity-like patch that has no effect).
  89 \end{prp}
  90
  91 \begin{code}
  92 inverse_doesnt_commute :: Patchy p => p C(a b) -> Maybe Doc
  93 inverse_doesnt_commute p | IsEq <- sloppyIdentity p = Nothing
  94                          | otherwise = do p' :> _ <- commute (invert p :> p)
  95                                           Just $ redText "inverse_doesnt_commute" $$ showPatch p'
  96 \end{code}
  97
  98 \subsection{Commute properties}
  99
 100 \begin{prp}[Recommute]
 101   $AB \commutes B'A'$ if and only if $B'A' \commutes AB$
 102 \end{prp}
 103
 104 \begin{code}
 105 recommute :: Patchy p => (FORALL(x y) ((p :> p) C(x y) -> Maybe ((p :> p) C(x y))))
 106           -> (p :> p) C(a b) -> Maybe Doc
 107 recommute c (x :> y) =
 108     case c (x :> y) of
 109     Nothing -> Nothing
 110     Just (y' :> x') ->
 111        case c (y' :> x') of
 112          Nothing -> Just (redText "failed" $$ showPatch y' $$ redText ":>" $$ showPatch x')
 113          Just (x'' :> y'') ->
 114              case y'' =/\= y of
 115              NotEq -> Just (redText "y'' =/\\= y failed, where x" $$ showPatch x $$
 116                             redText ":> y" $$ showPatch y $$
 117                             redText "y'" $$ showPatch y' $$
 118                             redText ":> x'" $$ showPatch x' $$
 119                             redText "x''" $$ showPatch x'' $$
 120                             redText ":> y''" $$ showPatch y'')
 121              IsEq -> case x'' =/\= x of
 122                      NotEq -> Just (redText "x'' /= x" $$ showPatch x'' $$ redText ":>" $$ showPatch y'')
 123                      IsEq -> Nothing
 124 \end{code}
 125
 126 \begin{prp}[Commute inverses]
 127   $AB \commutes B'A'$ if and only if $B^{-1}A^{-1} \commutes A'^{-1}B'^{-1}$
 128 \end{prp}
 129
 130 \begin{code}
 131 commute_inverses :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
 132                  -> (p :> p) C(a b) -> Maybe Doc
 133 commute_inverses c (x :> y) =
 134     case c (x :> y) of
 135     Nothing -> Nothing
 136     Just (y' :> x') ->
 137         case c (invert y :> invert x) of
 138         Nothing -> Just $ redText "second commute failed" $$
 139                    redText "x" $$ showPatch x $$ redText "y" $$ showPatch y $$
 140                    redText "y'" $$ showPatch y' $$ redText "x'" $$ showPatch x'
 141         Just (ix' :> iy') ->
 142             case invert ix' =/\= x' of
 143             NotEq -> Just $ redText "invert ix' /= x'" $$
 144                      redText "x" $$ showPatch x $$
 145                      redText "y" $$ showPatch y $$
 146                      redText "y'" $$ showPatch y' $$
 147                      redText "x'" $$ showPatch x' $$
 148                      redText "ix'" $$ showPatch ix' $$
 149                      redText "iy'" $$ showPatch iy' $$
 150                      redText "invert ix'" $$ showPatch (invert ix') $$
 151                      redText "invert iy'" $$ showPatch (invert iy')
 152             IsEq -> case y' =\/= invert iy' of
 153                     NotEq -> Just $ redText "y' /= invert iy'" $$ showPatch iy' $$ showPatch y'
 154                     IsEq -> Nothing
 155 \end{code}
 156
 157 \begin{prp}[Patch and inverse]
 158   If $AB \commutes B'A'$ then $A^{-1}B' \commutes BA'^{-1}$
 159 \end{prp}
 160
 161 This property is only true of primitive patches.
 162
 163 \begin{code}
 164 patch_and_inverse_commute :: Patchy p =>
 165                              (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
 166                           -> (p :> p) C(a b) -> Maybe Doc
 167 patch_and_inverse_commute c (x :> y) =
 168   do y' :> x' <- c (x :> y)
 169      case c (invert x :> y') of
 170        Nothing -> Just (redText "failure in patch_and_inverse_commute")
 171        Just (y'' :> ix') ->
 172            case y'' =\/= y of
 173            NotEq -> Just (redText "y'' /= y" $$
 174                           redText "x" $$ showPatch x $$
 175                           redText "y" $$ showPatch y $$
 176                           redText "x'" $$ showPatch x' $$
 177                           redText "y'" $$ showPatch y' $$
 178                           redText "y''" $$ showPatch y'' $$
 179                           redText ":> x'" $$ showPatch x')
 180            IsEq -> case x' =\/= invert ix' of
 181                    NotEq -> Just (redText "x' /= invert ix'" $$
 182                                   redText "y''" $$ showPatch y'' $$
 183                                   redText ":> x'" $$ showPatch x' $$
 184                                   redText "invert x" $$ showPatch (invert x) $$
 185                                   redText ":> y" $$ showPatch y $$
 186                                   redText "y'" $$ showPatch y' $$
 187                                   redText "ix'" $$ showPatch ix')
 188                    IsEq -> Nothing
 189 \end{code}
 190
 191 \begin{prp}[Permutivity]
 192   (to be added...)
 193 \end{prp}
 194
 195 \begin{code}
 196 permutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
 197             -> (p :> p :> p) C(a b) -> Maybe Doc
 198 permutivity c (x:>y:>z) =
 199   do y1 :> x1 <- c (x :> y)
 200      z2 :> y2 <- --traceDoc (greenText "first commuted") $
 201                  c (y :> z)
 202      z3 :> x3 <- --traceDoc (greenText "second commuted") $
 203                  c (x :> z2)
 204      case c (x1 :> z) of
 205        Nothing -> Just $ redText "permutivity1"
 206        Just (z4 :> x4) ->
 207          --traceDoc (greenText "third commuted" $$
 208          --          greenText "about to commute" $$
 209          --          greenText "y1" $$ showPatch y1 $$
 210          --          greenText "z4" $$ showPatch z4) $
 211          case c (y1 :> z4) of
 212          Nothing -> Just $ redText "permutivity2"
 213          Just (z3_ :> y4)
 214              | IsEq <- z3_ =\/= z3 ->
 215                   --traceDoc (greenText "passed z3") $ error "foobar test" $
 216                   case c (y4 :> x4) of
 217                   Nothing -> Just $ redText "permutivity5: input was" $$
 218                              redText "x" $$ showPatch x $$
 219                              redText "y" $$ showPatch y $$
 220                              redText "z" $$ showPatch z $$
 221                              redText "z3" $$ showPatch z3 $$
 222                              redText "failed commute of" $$
 223                              redText "y4" $$ showPatch y4 $$
 224                              redText "x4" $$ showPatch x4 $$
 225                              redText "whereas commute of x and y give" $$
 226                              redText "y1" $$ showPatch y1 $$
 227                              redText "x1" $$ showPatch x1
 228                   Just (x3_ :> y2_)
 229                        | NotEq <- x3_ =\/= x3 -> Just $ redText "permutivity6"
 230                        | NotEq <- y2_ =/\= y2 -> Just $ redText "permutivity7"
 231                        | otherwise -> Nothing
 232              | otherwise ->
 233                  Just $ redText "permutivity failed" $$
 234                         redText "z3" $$ showPatch z3 $$
 235                         redText "z3_" $$ showPatch z3_
 236
 237 partial_permutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y)))
 238                     -> (p :> p :> p) C(a b) -> Maybe Doc
 239 partial_permutivity c (xx:>yy:>zz) = pp (xx:>yy:>zz) `mplus` pp (invert zz:>invert yy:>invert xx)
 240     where pp (x:>y:>z) = do z1 :> y1 <- c (y :> z)
 241                             _ :> x1 <- c (x :> z1)
 242                             case c (x :> y) of
 243                               Just _ -> Nothing -- this is covered by full permutivity test above
 244                               Nothing ->
 245                                   case c (x1 :> y1) of
 246                                   Nothing -> Nothing
 247                                   Just _ -> Just $ greenText "partial_permutivity error" $$
 248                                             greenText "x" $$ showPatch x $$
 249                                             greenText "y" $$ showPatch y $$
 250                                             greenText "z" $$ showPatch z
 251
 252 \end{code}
 253
 254 \begin{code}
 255 merge_arguments_consistent :: Patchy p =>
 256                               (FORALL(x y) p C(x y) -> Maybe Doc)
 257                            -> (p :\/: p) C(a b) -> Maybe Doc
 258 merge_arguments_consistent is_consistent (x :\/: y) =
 259     msum [(\z -> redText "merge_arguments_consistent x" $$ showPatch x $$ z) `fmap` is_consistent x,
 260           (\z -> redText "merge_arguments_consistent y" $$ showPatch y $$ z) `fmap` is_consistent y]
 261
 262 merge_consistent :: Patchy p =>
 263                            (FORALL(x y) p C(x y) -> Maybe Doc)
 264                         -> (p :\/: p) C(a b) -> Maybe Doc
 265 merge_consistent is_consistent (x :\/: y) =
 266     case merge (x :\/: y) of
 267     y' :/\: x' ->
 268         msum [(\z -> redText "merge_consistent x" $$ showPatch x $$ z) `fmap` is_consistent x,
 269               (\z -> redText "merge_consistent y" $$ showPatch y $$ z) `fmap` is_consistent y,
 270               (\z -> redText "merge_consistent x'" $$ showPatch x' $$ z $$
 271                      redText "where x' comes from x" $$ showPatch x $$
 272                      redText "and y" $$ showPatch y) `fmap` is_consistent x',
 273               (\z -> redText "merge_consistent y'" $$ showPatch y' $$ z) `fmap` is_consistent y']
 274
 275 merge_either_way :: Patchy p => (p :\/: p) C(x y) -> Maybe Doc
 276 merge_either_way (x :\/: y) =
 277     case merge (x :\/: y) of
 278     y' :/\: x' -> case merge (y :\/: x) of
 279                   x'' :/\: y'' | IsEq <- x'' =\/= x',
 280                                  IsEq <- y'' =\/= y' -> Nothing
 281                                | otherwise -> Just $ redText "merge_either_way bug"
 282
 283 merge_commute :: Patchy p => (p :\/: p) C(x y) -> Maybe Doc
 284 merge_commute (x :\/: y) =
 285     case merge (x :\/: y) of
 286     y' :/\: x' ->
 287         case commute (x :> y') of
 288         Nothing -> Just $ redText "merge_commute 1" $$
 289                    redText "x" $$ showPatch x $$
 290                    redText "y" $$ showPatch y $$
 291                    redText "x'" $$ showPatch x' $$
 292                    redText "y'" $$ showPatch y'
 293         Just (y_ :> x'_)
 294             | IsEq <- y_ =\/= y,
 295               IsEq <- x'_ =\/= x' ->
 296                       case commute (y :> x') of
 297                       Nothing -> Just $ redText "merge_commute 2 failed" $$
 298                                  redText "x" $$ showPatch x $$
 299                                  redText "y" $$ showPatch y $$
 300                                  redText "x'" $$ showPatch x' $$
 301                                  redText "y'" $$ showPatch y'
 302                       Just (x_ :> y'_)
 303                            | IsEq <- x_ =\/= x,
 304                              IsEq <- y'_ =\/= y' -> Nothing
 305                            | otherwise -> Just $ redText "merge_commute 3" $$
 306                                           redText "x" $$ showPatch x $$
 307                                           redText "y" $$ showPatch y $$
 308                                           redText "x'" $$ showPatch x' $$
 309                                           redText "y'" $$ showPatch y' $$
 310                                           redText "x_" $$ showPatch x_ $$
 311                                           redText "y'_" $$ showPatch y'_
 312             | otherwise -> Just $ redText "merge_commute 4" $$
 313                            redText "x" $$ showPatch x $$
 314                            redText "y" $$ showPatch y $$
 315                            redText "x'" $$ showPatch x' $$
 316                            redText "y'" $$ showPatch y' $$
 317                            redText "x'_" $$ showPatch x'_ $$
 318                            redText "y_" $$ showPatch y_
 319
 320 \end{code}
 321
 322 \begin{code}
 323 join_inverses :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (Prim C(x y)))
 324               -> Prim C(a b) -> Maybe Doc
 325 join_inverses j p = case j (invert p :> p) of
 326                     Just Identity -> Nothing
 327                     Just p' -> Just $ redText "join_inverses gave just" $$ showPatch p'
 328                     Nothing -> Just $ redText "join_inverses failed"
 329
 330 join_commute :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (Prim C(x y)))
 331              -> (Prim :> Prim :> Prim) C(a b) -> Maybe Doc
 332 join_commute j (a :> b :> c) =
 333     do x <- j (b :> c)
 334        case commuteFL (a :> b :>: c :>: NilFL) of
 335         Right (b' :>: c' :>: NilFL :> a') ->
 336            case commute (a :> x) of
 337              Nothing -> Just $ greenText "join_commute 1"
 338              Just (x' :> a'') ->
 339                  case a'' =/\= a' of
 340                  NotEq -> Just $ greenText "join_commute 3"
 341                  IsEq -> case j (b' :> c') of
 342                          Nothing -> Just $ greenText "join_commute 4"
 343                          Just x'' -> case x' =\/= x'' of
 344                                      NotEq -> Just $ greenText "join_commute 5"
 345                                      IsEq -> Nothing
 346         _ -> Nothing
 347 \end{code}
 348
 349
 350 \begin{code}
 351 show_read :: (Show2 p, Patchy p) => p C(a b) -> Maybe Doc
 352 show_read p = let ps = renderPS (showPatch p)
 353               in case readPatch ps of
 354                  Nothing -> Just (redText "unable to read " $$ showPatch p)
 355                  Just (Sealed p',_) | IsEq <- p' =\/= p -> Nothing
 356                                     | otherwise -> Just $ redText "trouble reading patch p" $$
 357                                                           showPatch p $$
 358                                                           redText "reads as p'" $$
 359                                                           showPatch p' $$
 360                                                           redText "aka" $$
 361                                                           greenText (show2 p) $$
 362                                                           redText "and" $$
 363                                                           greenText (show2 p')
 364 \end{code}
 365
 366 \end{document}