darcs-beta-2.7.98.1: src/Darcs/Test/Patch/Properties.hs
-- 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')