-- 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. {-# LANGUAGE CPP #-} {-# OPTIONS_GHC -fno-warn-deprecations -fno-warn-orphans #-} #include "gadts.h" module Darcs.Test.Patch.Properties ( invertSymmetry, invertRollback, recommute, commuteInverses, effectPreserving, permutivity, partialPermutivity, patchAndInverseCommute, mergeEitherWay, show_read, mergeCommute, mergeConsistent, mergeArgumentsConsistent, joinEffectPreserving, joinCommute ) where import Darcs.Test.Util.TestResult ( TestResult, succeeded, failed, rejected, (<&&>), fromMaybe ) import Darcs.Test.Patch.RepoModel ( RepoModel, applyPatch ) import Darcs.Test.Patch.WithState ( WithState(..) ) import Control.Monad ( msum ) import Darcs.Witnesses.Show ( Show2(..), show2 ) import Darcs.Patch.Patchy ( Patchy, showPatch, commute, invert ) import Darcs.Patch.Prim.V1 ( Prim ) import Darcs.Patch () import Darcs.Patch.Commute ( commuteFLorComplain ) import Darcs.Patch.Merge ( Merge(merge) ) import Darcs.Patch.Read ( readPatch ) import Darcs.Witnesses.Eq ( MyEq(..), EqCheck(..) ) import Darcs.Witnesses.Ordered ( FL(..), (:>)(..), (:\/:)(..), (:/\:)(..) ) import Darcs.Witnesses.Sealed ( Sealed(Sealed) ) import Printer ( Doc, renderPS, redText, greenText, ($$) ) --import Darcs.ColorPrinter ( traceDoc ) -- | invert symmetry inv(inv(p)) = p invertSymmetry :: Patchy p => p C(a b) -> TestResult invertSymmetry p = case invert (invert p) =\/= p of IsEq -> succeeded NotEq -> failed $ redText "p /= inv(inv(p))" -- | invert rollback if b = A(a) then a = A'(b) invertRollback :: Patchy p => WithState RepoModel p C(a b) -> TestResult invertRollback (WithState a x b) = case applyPatch (invert x) b of Nothing -> failed $ redText "x' not applicable to b." Just a1 -> if a1 == a then succeeded else failed $ redText "a1 is not equals to a." -- | recommute AB <--> B'A' iff B'A' <--> AB recommute :: Patchy p => (FORALL(x y) ((p :> p) C(x y) -> Maybe ((p :> p) C(x y)))) -> (p :> p) C(a b) -> TestResult recommute c (x :> y) = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case c (y' :> x') of Nothing -> failed (redText "failed" $$ showPatch y' $$ redText ":>" $$ showPatch x') Just (x'' :> y'') -> case y'' =/\= y of NotEq -> failed (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 -> failed (redText "x'' /= x" $$ showPatch x'' $$ redText ":>" $$ showPatch y'') IsEq -> succeeded -- | commuteInverses AB <--> B'A' iff inv(B)inv(A) <--> inv(A')inv(B') commuteInverses :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y))) -> (p :> p) C(a b) -> TestResult commuteInverses c (x :> y) = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case c (invert y :> invert x) of Nothing -> failed $ 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 -> failed $ 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 -> failed $ redText "y' /= invert iy'" $$ showPatch iy' $$ showPatch y' IsEq -> succeeded -- | effect preserving AB <--> B'A' then effect(AB) = effect(B'A') effectPreserving :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y))) -> WithState RepoModel (p :> p) C(a b) -> TestResult effectPreserving c (WithState r (x :> y) r') = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case applyPatch y' r of Nothing -> failed $ redText "y' is not applicable to r." Just r_y' -> case applyPatch x' r_y' of Nothing -> failed $ redText "x' is not applicable to r_y'." Just r_y'x' -> if r_y'x' == r' then succeeded else failed $ redText "r_y'x' is not equal to r'." -- | patchAndInverseCommute if AB <--> B'A' then inv(A)B' <---> Binv(A') patchAndInverseCommute :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y))) -> (p :> p) C(a b) -> TestResult patchAndInverseCommute c (x :> y) = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case c (invert x :> y') of Nothing -> failed (redText "failure in patchAndInverseCommute") Just (y'' :> ix') -> case y'' =\/= y of NotEq -> failed (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 -> failed (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 -> succeeded permutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y))) -> (p :> p :> p) C(a b) -> TestResult permutivity c (x:>y:>z) = case c (x :> y) of Nothing -> rejected Just (y1 :> x1) -> case c (y :> z) of Nothing -> rejected Just (z2 :> y2) -> case c (x :> z2) of Nothing -> rejected Just (z3 :> x3) -> case c (x1 :> z) of Nothing -> failed $ 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 -> failed $ redText "permutivity2" Just (z3_ :> y4) | IsEq <- z3_ =\/= z3 -> --traceDoc (greenText "passed z3") $ error "foobar test" $ case c (y4 :> x4) of Nothing -> failed $ 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 -> failed $ redText "permutivity6" | NotEq <- y2_ =/\= y2 -> failed $ redText "permutivity7" | otherwise -> succeeded | otherwise -> failed $ redText "permutivity failed" $$ redText "z3" $$ showPatch z3 $$ redText "z3_" $$ showPatch z3_ partialPermutivity :: Patchy p => (FORALL(x y) (p :> p) C(x y) -> Maybe ((p :> p) C(x y))) -> (p :> p :> p) C(a b) -> TestResult partialPermutivity c (xx:>yy:>zz) = pp (xx:>yy:>zz) <&&> pp (invert zz:>invert yy:>invert xx) where pp (x:>y:>z) = case c (y :> z) of Nothing -> rejected Just (z1 :> y1) -> case c (x :> z1) of Nothing -> rejected Just (_ :> x1) -> case c (x :> y) of Just _ -> rejected -- this is covered by full permutivity test above Nothing -> case c (x1 :> y1) of Nothing -> succeeded Just _ -> failed $ greenText "partialPermutivity error" $$ greenText "x" $$ showPatch x $$ greenText "y" $$ showPatch y $$ greenText "z" $$ showPatch z mergeArgumentsConsistent :: Patchy p => (FORALL(x y) p C(x y) -> Maybe Doc) -> (p :\/: p) C(a b) -> TestResult mergeArgumentsConsistent isConsistent (x :\/: y) = fromMaybe $ msum [(\z -> redText "mergeArgumentsConsistent x" $$ showPatch x $$ z) `fmap` isConsistent x, (\z -> redText "mergeArgumentsConsistent y" $$ showPatch y $$ z) `fmap` isConsistent y] mergeConsistent :: (Patchy p, Merge p) => (FORALL(x y) p C(x y) -> Maybe Doc) -> (p :\/: p) C(a b) -> TestResult mergeConsistent isConsistent (x :\/: y) = case merge (x :\/: y) of y' :/\: x' -> fromMaybe $ msum [(\z -> redText "mergeConsistent x" $$ showPatch x $$ z) `fmap` isConsistent x, (\z -> redText "mergeConsistent y" $$ showPatch y $$ z) `fmap` isConsistent y, (\z -> redText "mergeConsistent x'" $$ showPatch x' $$ z $$ redText "where x' comes from x" $$ showPatch x $$ redText "and y" $$ showPatch y) `fmap` isConsistent x', (\z -> redText "mergeConsistent y'" $$ showPatch y' $$ z) `fmap` isConsistent y'] mergeEitherWay :: (Patchy p, Merge p) => (p :\/: p) C(x y) -> TestResult mergeEitherWay (x :\/: y) = case merge (x :\/: y) of y' :/\: x' -> case merge (y :\/: x) of x'' :/\: y'' | IsEq <- x'' =\/= x', IsEq <- y'' =\/= y' -> succeeded | otherwise -> failed $ redText "mergeEitherWay bug" mergeCommute :: (Patchy p, Merge p) => (p :\/: p) C(x y) -> TestResult mergeCommute (x :\/: y) = case merge (x :\/: y) of y' :/\: x' -> case commute (x :> y') of Nothing -> failed $ redText "mergeCommute 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 -> failed $ redText "mergeCommute 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' -> succeeded | otherwise -> failed $ redText "mergeCommute 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 -> failed $ redText "mergeCommute 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 effect preserving joinEffectPreserving :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (FL Prim C(x y))) -> WithState RepoModel (Prim :> Prim) C(a b) -> TestResult joinEffectPreserving j (WithState r (a :> b) r') = case j (a :> b) of Nothing -> rejected Just x -> case applyPatch x r of Nothing -> failed $ redText "x is not applicable to r." Just r_x -> if r_x == r' then succeeded else failed $ redText "r_x /= r'" joinCommute :: (FORALL(x y) (Prim :> Prim) C(x y) -> Maybe (FL Prim C(x y))) -> (Prim :> Prim :> Prim) C(a b) -> TestResult joinCommute j (a :> b :> c) = case j (b :> c) of Nothing -> rejected Just x -> case commuteFLorComplain (a :> b :>: c :>: NilFL) of Right (b' :>: c' :>: NilFL :> a') -> case commute (a:>:NilFL :> x) of Just (x' :> a'':>:NilFL) -> case a'' =/\= a' of NotEq -> failed $ greenText "joinCommute 3" IsEq -> case j (b' :> c') of Nothing -> failed $ greenText "joinCommute 4" Just x'' -> case x' =\/= x'' of NotEq -> failed $ greenText "joinCommute 5" IsEq -> succeeded _ -> failed $ greenText "joinCommute 1" _ -> rejected show_read :: (Show2 p, Patchy p) => p C(a b) -> TestResult show_read p = let ps = renderPS (showPatch p) in case readPatch ps of Nothing -> failed (redText "unable to read " $$ showPatch p) Just (Sealed p' ) | IsEq <- p' =\/= p -> succeeded | otherwise -> failed $ redText "trouble reading patch p" $$ showPatch p $$ redText "reads as p'" $$ showPatch p' $$ redText "aka" $$ greenText (show2 p) $$ redText "and" $$ greenText (show2 p')