% 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}

    {-# LANGUAGE CPP #-}
    {-# OPTIONS_GHC -cpp -fno-warn-deprecations -fno-warn-orphans -fglasgow-exts #-}

    #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, ($$) )
    --import Darcs.ColorPrinter ( traceDoc )

\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 <- --traceDoc (greenText "first commuted") $
                     c (y :> z)
         z3 :> x3 <- --traceDoc (greenText "second commuted") $
                     c (x :> z2)
         case c (x1 :> z) of
           Nothing -> Just $ redText "permutivity1"
           Just (z4 :> x4) ->
             --traceDoc (greenText "third commuted" $$
             --          greenText "about to commute" $$
             --          greenText "y1" $$ showPatch y1 $$
             --          greenText "z4" $$ showPatch z4) $
             case c (y1 :> z4) of
             Nothing -> Just $ redText "permutivity2"
             Just (z3_ :> y4)
                 | IsEq <- z3_ =\/= z3 ->
                      --traceDoc (greenText "passed z3") $ error "foobar test" $
                      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 -- this is covered by full permutivity test above
                                  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}