-- 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. module Darcs.Test.Patch.Properties.Generic ( invertSymmetry, inverseComposition, invertRollback, recommute, commuteInverses, effectPreserving, permutivity, partialPermutivity, patchAndInverseCommute, mergeEitherWay, show_read, mergeCommute, mergeConsistent, mergeArgumentsConsistent, coalesceEffectPreserving, coalesceCommute, propIsMergeable ) where import Darcs.Test.Util.TestResult ( TestResult, succeeded, failed, rejected, (<&&>), fromMaybe ) import Darcs.Test.Patch.RepoModel ( RepoModel, RepoState, repoApply, eqModel, showModel , maybeFail ) import Darcs.Test.Patch.WithState ( WithState(..), WithStartState(..) ) import Darcs.Test.Patch.Arbitrary.Generic ( Tree, flattenOne, MightBeEmptyHunk(..), MightHaveDuplicate(..) ) import Control.Monad ( msum ) import Darcs.Patch.Witnesses.Show ( Show2(..), show2 ) import Darcs.Patch.Read ( ReadPatch ) import Darcs.Patch.Show ( ShowPatchBasic, displayPatch, showPatch, ShowPatchFor(ForStorage) ) import Darcs.Patch.Prim.Class ( PrimPatch, PrimOf, FromPrim ) import Darcs.Patch () import Darcs.Patch.Apply ( Apply, ApplyState ) import Darcs.Patch.Commute ( commute, commuteFL ) import Darcs.Patch.Merge ( Merge(merge) ) import Darcs.Patch.Read ( readPatch ) import Darcs.Patch.Invert ( Invert, invert, invertFL ) import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) ) import Darcs.Patch.Witnesses.Ordered ( FL(..), (:>)(..), (:\/:)(..), (:/\:)(..), lengthFL, eqFL, reverseRL ) import Darcs.Patch.Witnesses.Sealed ( Sealed(Sealed), seal2, Sealed2 ) import Darcs.Util.Printer ( Doc, renderPS, redText, greenText, ($$), text ) --import Darcs.ColorPrinter ( traceDoc ) propIsMergeable :: forall model p wX . (FromPrim p, Merge p, RepoModel model) => Sealed (WithStartState model (Tree (PrimOf p))) -> Maybe (Tree p wX) propIsMergeable (Sealed (WithStartState _ t)) = case flattenOne t of Sealed ps -> let _ = seal2 ps :: Sealed2 (FL p) in case lengthFL ps of _ -> Nothing -- | invert symmetry inv(inv(p)) = p invertSymmetry :: (Invert p, Eq2 p) => p wA wB -> TestResult invertSymmetry p = case invert (invert p) =\/= p of IsEq -> succeeded NotEq -> failed $ redText "p /= inv(inv(p))" inverseComposition :: (Invert p, Eq2 p) => (p :> p) wX wY -> TestResult inverseComposition (a :> b) = case eqFL (reverseRL (invertFL (a:>:b:>:NilFL))) (invert b:>:invert a:>:NilFL) of IsEq -> succeeded NotEq -> failed $ redText "inv(a :>: b :>: NilFL) /= inv(b) :>: inv(a) :>: NilFL" -- | invert rollback if b = A(a) then a = A'(b) invertRollback :: (Invert p, Apply p, ApplyState p ~ RepoState model, ShowPatchBasic p, RepoModel model) => WithState model p wA wB -> TestResult invertRollback (WithState a x b) = case maybeFail $ repoApply b (invert x) of Nothing -> failed $ redText "x' not applicable to b." Just a1 -> if a1 `eqModel` a then succeeded else failed $ redText "a1: " $$ text (showModel a1) $$ redText " ---- is not equals to a:" $$ text (showModel a) $$ redText "where a was" $$ text (showModel b) $$ redText "with (invert x) on top:" $$ displayPatch (invert x) -- | recommute AB ↔ B′A′ if and only if B′A′ ↔ AB recommute :: (ShowPatchBasic p, Eq2 p, MightHaveDuplicate p) => (forall wX wY . ((p :> p) wX wY -> Maybe ((p :> p) wX wY))) -> (p :> p) wA wB -> TestResult recommute c (x :> y) = case c (x :> y) of Nothing -> rejected Just (y' :> x') -- this test unfortunately fails on some V2 patches that contain duplicates -- after the commute. While in theory the underlying bug should be fixed, -- we don't know how to and even if we did, it would probably involve a repository -- migration to a new patch type. | hasDuplicate y' || hasDuplicate x' -> rejected | otherwise -> case c (y' :> x') of Nothing -> failed (redText "failed, where x" $$ displayPatch x $$ redText ":> y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText ":> x'" $$ displayPatch x') Just (x'' :> y'') -> case y'' =/\= y of NotEq -> failed (redText "y'' =/\\= y failed, where x" $$ displayPatch x $$ redText ":> y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText ":> x'" $$ displayPatch x' $$ redText "x''" $$ displayPatch x'' $$ redText ":> y''" $$ displayPatch y'') IsEq -> case x'' =/\= x of NotEq -> failed ( redText "x'' /= x, where x" $$ displayPatch x $$ redText ":> y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText ":> x'" $$ displayPatch x' $$ redText "x''" $$ displayPatch x'' $$ redText ":> y''" $$ displayPatch y'') IsEq -> succeeded -- | commuteInverses AB ↔ B′A′ if and only if B⁻¹A⁻¹ ↔ A′⁻¹B′⁻¹ commuteInverses :: (Invert p, ShowPatchBasic p, Eq2 p) => (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY)) -> (p :> p) wA wB -> 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" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText "x'" $$ displayPatch x' Just (ix' :> iy') -> case invert ix' =/\= x' of NotEq -> failed $ redText "invert ix' /= x'" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText "x'" $$ displayPatch x' $$ redText "ix'" $$ displayPatch ix' $$ redText "iy'" $$ displayPatch iy' $$ redText "invert ix'" $$ displayPatch (invert ix') $$ redText "invert iy'" $$ displayPatch (invert iy') IsEq -> case y' =\/= invert iy' of NotEq -> failed $ redText "y' /= invert iy'" $$ displayPatch iy' $$ displayPatch y' IsEq -> succeeded -- | effect preserving AB <--> B'A' then effect(AB) = effect(B'A') effectPreserving :: ( Apply p , MightBeEmptyHunk p , RepoModel model , ApplyState p ~ RepoState model , ShowPatchBasic p ) => (forall wX wY. (p :> p) wX wY -> Maybe ((p :> p) wX wY)) -> WithState model (p :> p) wA wB -> TestResult effectPreserving _ (WithState _ (x :> _) _) | isEmptyHunk x = rejected effectPreserving c (WithState r (x :> y) r') = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case maybeFail $ repoApply r y' of Nothing -> failed $ redText "##x" $$ displayPatch x $$ redText "##y" $$ displayPatch y $$ redText "##y'" $$ displayPatch y' $$ redText "##x'" $$ displayPatch x' $$ redText "##y' is not applicable to r" $$ displayModel r Just r_y' -> case maybeFail $ repoApply r_y' x' of Nothing -> failed $ redText "##x" $$ displayPatch x $$ redText "##y" $$ displayPatch y $$ redText "##y'" $$ displayPatch y' $$ redText "##x'" $$ displayPatch x' $$ redText "##x' is not applicable to r_y'" $$ displayModel r_y' Just r_y'x' -> if r_y'x' `eqModel` r' then succeeded else failed $ redText "##x" $$ displayPatch x $$ redText "##y" $$ displayPatch y $$ redText "##y'" $$ displayPatch y' $$ redText "##x'" $$ displayPatch x' $$ redText "##r_y'x'" $$ displayModel r_y'x' $$ redText "##is not equal to r'" $$ displayModel r' where displayModel = text . showModel -- | patchAndInverseCommute If AB ↔ B′A′ then A⁻¹B′ ↔ BA′⁻¹ patchAndInverseCommute :: (Invert p, ShowPatchBasic p, Eq2 p) => (forall wX wY. (p :> p) wX wY -> Maybe ((p :> p) wX wY)) -> (p :> p) wA wB -> TestResult patchAndInverseCommute c (x :> y) = case c (x :> y) of Nothing -> rejected Just (y' :> x') -> case c (invert x :> y') of Nothing -> failed $ redText "-------- original (x :> y)" $$ displayPatch x $$ redText ":>" $$ displayPatch y $$ redText "-------- result (y' :> x')" $$ displayPatch y' $$ redText ":>" $$ displayPatch x' $$ redText "-------- failed commute (invert x :> y')" $$ displayPatch (invert x) $$ redText ":>" $$ displayPatch y' Just (y'' :> ix') -> case y'' =\/= y of NotEq -> failed $ redText "y'' /= y" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText "x'" $$ displayPatch x' $$ redText "y''" $$ displayPatch y'' $$ redText "ix'" $$ displayPatch ix' IsEq -> case x' =\/= invert ix' of NotEq -> failed $ redText "x' /= invert ix'" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "y'" $$ displayPatch y' $$ redText "x'" $$ displayPatch x' $$ redText "invert x" $$ displayPatch (invert x) $$ redText "y'" $$ displayPatch y' $$ redText "invert ix'" $$ displayPatch (invert ix') IsEq -> succeeded permutivity :: (ShowPatchBasic p, Eq2 p) => (forall wX wY . (p :> p) wX wY -> Maybe ((p :> p) wX wY)) -> (p :> p :> p) wA wB -> 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" $$ displayPatch y1 $$ -- greenText "z4" $$ displayPatch 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" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "z" $$ displayPatch z $$ redText "z3" $$ displayPatch z3 $$ redText "failed commute of" $$ redText "y4" $$ displayPatch y4 $$ redText "x4" $$ displayPatch x4 $$ redText "whereas commute of x and y give" $$ redText "y1" $$ displayPatch y1 $$ redText "x1" $$ displayPatch 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" $$ displayPatch z3 $$ redText "z3_" $$ displayPatch z3_ partialPermutivity :: (Invert p, ShowPatchBasic p) => (forall wX wY. (p :> p) wX wY -> Maybe ((p :> p) wX wY)) -> (p :> p :> p) wA wB -> 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" $$ displayPatch x $$ greenText "y" $$ displayPatch y $$ greenText "z" $$ displayPatch z mergeArgumentsConsistent :: (ShowPatchBasic p) => (forall wX wY . p wX wY -> Maybe Doc) -> (p :\/: p) wA wB -> TestResult mergeArgumentsConsistent isConsistent (x :\/: y) = fromMaybe $ msum [(\z -> redText "mergeArgumentsConsistent x" $$ displayPatch x $$ z) `fmap` isConsistent x, (\z -> redText "mergeArgumentsConsistent y" $$ displayPatch y $$ z) `fmap` isConsistent y] mergeConsistent :: (ShowPatchBasic p, Merge p) => (forall wX wY . p wX wY -> Maybe Doc) -> (p :\/: p) wA wB -> TestResult mergeConsistent isConsistent (x :\/: y) = case merge (x :\/: y) of y' :/\: x' -> fromMaybe $ msum [(\z -> redText "mergeConsistent x" $$ displayPatch x $$ z) `fmap` isConsistent x, (\z -> redText "mergeConsistent y" $$ displayPatch y $$ z) `fmap` isConsistent y, (\z -> redText "mergeConsistent x'" $$ displayPatch x' $$ z $$ redText "where x' comes from x" $$ displayPatch x $$ redText "and y" $$ displayPatch y) `fmap` isConsistent x', (\z -> redText "mergeConsistent y'" $$ displayPatch y' $$ z) `fmap` isConsistent y'] mergeEitherWay :: (Eq2 p, Merge p) => (p :\/: p) wX wY -> 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 :: (Eq2 p, ShowPatchBasic p, Merge p, MightHaveDuplicate p) => (p :\/: p) wX wY -> TestResult mergeCommute (x :\/: y) = case merge (x :\/: y) of y' :/\: x' -- this test unfortunately fails on some V2 patches that contain duplicates -- after the merge. While in theory the underlying bug should be fixed, -- we don't know how to and even if we did, it would probably involve a repository -- migration to a new patch type. | hasDuplicate x' || hasDuplicate y' -> rejected | otherwise -> case commute (x :> y') of Nothing -> failed $ redText "mergeCommute 1" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "x'" $$ displayPatch x' $$ redText "y'" $$ displayPatch y' Just (y_ :> x'_) | IsEq <- y_ =\/= y, IsEq <- x'_ =\/= x' -> case commute (y :> x') of Nothing -> failed $ redText "mergeCommute 2 failed" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "x'" $$ displayPatch x' $$ redText "y'" $$ displayPatch y' Just (x_ :> y'_) | IsEq <- x_ =\/= x, IsEq <- y'_ =\/= y' -> succeeded | otherwise -> failed $ redText "mergeCommute 3" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "x'" $$ displayPatch x' $$ redText "y'" $$ displayPatch y' $$ redText "x_" $$ displayPatch x_ $$ redText "y'_" $$ displayPatch y'_ | otherwise -> failed $ redText "mergeCommute 4" $$ redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$ redText "x'" $$ displayPatch x' $$ redText "y'" $$ displayPatch y' $$ redText "x'_" $$ displayPatch x'_ $$ redText "y_" $$ displayPatch y_ -- | coalesce effect preserving coalesceEffectPreserving :: (PrimPatch prim, RepoModel model, ApplyState prim ~ RepoState model ) => (forall wX wY . (prim :> prim) wX wY -> Maybe (FL prim wX wY)) -> WithState model (prim :> prim) wA wB -> TestResult coalesceEffectPreserving j (WithState r (a :> b) r') = case j (a :> b) of Nothing -> rejected Just x -> case maybeFail $ repoApply r x of Nothing -> failed $ redText "x is not applicable to r." $$ text (showModel r) $$ displayPatch x $$ redText "a:>b" $$ displayPatch a $$ displayPatch b $$ redText "r'=" $$ text (showModel r') Just r_x -> if r_x `eqModel` r' then succeeded else failed $ redText "r_x /= r', r=" $$ text (showModel r) $$ redText "a:>b=" $$ displayPatch a $$ displayPatch b $$ redText "x=" $$ displayPatch x $$ redText "r'=" $$ text (showModel r') $$ redText "r_x=" $$ text (showModel r_x) coalesceCommute :: (PrimPatch prim, MightBeEmptyHunk prim) => (forall wX wY . (prim :> prim) wX wY -> Maybe (FL prim wX wY)) -> (prim :> prim :> prim) wA wB -> TestResult coalesceCommute _ (a :> _ :> _) | isEmptyHunk a = rejected coalesceCommute j (a :> b :> c) = case j (b :> c) of Nothing -> rejected Just x -> case commuteFL (a :> b :>: c :>: NilFL) of Just (b' :>: c' :>: NilFL :> a') -> case commuteFL (a :> x) of Just (x' :> a'') -> case a'' =/\= a' of NotEq -> failed $ greenText "a'' =/\\= a' failed" $$ display1 $$ display2 IsEq -> case j (b' :> c') of Nothing -> failed $ greenText "coalesce (b':>c') failed" $$ display1 $$ display2 Just x'' -> case x' =\/= x'' of NotEq -> failed $ greenText "x' =\\/= x'' failed" $$ display1 $$ display2 $$ display3 IsEq -> succeeded where display3 = redText "## coalesce (b':>c') => x''" $$ displayPatch x'' where display2 = redText "## commute (a:>x) => x'" $$ displayPatch x' $$ redText "## :> a''" $$ displayPatch a'' _ -> failed $ greenText "commute a x failed" $$ display1 where display1 = redText "## a" $$ displayPatch a $$ redText "## b" $$ displayPatch b $$ redText "## c" $$ displayPatch c $$ redText "## coalesce (b:>c) => x" $$ displayPatch x $$ redText "## commute (a:>b:>c) => a'" $$ displayPatch a' $$ redText "## b'" $$ displayPatch b' $$ redText "## c'" $$ displayPatch c' _ -> rejected -- note: we would normally use displayPatch in the failure message -- but that would be very misleading here show_read :: (Show2 p, Eq2 p, ReadPatch p, ShowPatchBasic p) => p wA wB -> TestResult show_read p = let ps = renderPS (showPatch ForStorage p) in case readPatch ps of Nothing -> failed (redText "unable to read " $$ showPatch ForStorage p) Just (Sealed p' ) | IsEq <- p' =\/= p -> succeeded | otherwise -> failed $ redText "trouble reading patch p" $$ showPatch ForStorage p $$ redText "reads as p'" $$ showPatch ForStorage p' $$ redText "aka" $$ greenText (show2 p) $$ redText "and" $$ greenText (show2 p') -- vim: fileencoding=utf-8 :