Skip to content
Browse files

Fixed #3. Parallel conjunction seems to work. See tests 14a and 14b.

  • Loading branch information...
1 parent b6bbce6 commit accb8f28f8f7055c7d2cbeffaab537adf726ffbe @jasonreich jasonreich committed
Showing with 58 additions and 16 deletions.
  1. +1 −2 README.md
  2. +1 −1 Test/LazySmallCheck2012.hs
  3. +22 −7 Test/LazySmallCheck2012/Core.lhs
  4. +34 −6 suite/Suite.hs
View
3 README.md
@@ -29,8 +29,7 @@ Boolean value can be expressed as a `foldr`.
``` haskell
prop_ReduceFold :: ([Bool] -> Bool) -> Property
-prop_ReduceFold r = existsDeeperBy (+2) $ \f z ->
- forAll $ \xs -> r xs == foldr f z xs
+prop_ReduceFold r = existsDeeperBy (+2) $ \f z -> forAll $ \xs -> r xs == foldr f z xs
```
When this property is tested using our advanced version of *Lazy
View
2 Test/LazySmallCheck2012.hs
@@ -4,7 +4,7 @@ module Test.LazySmallCheck2012(
depthCheck, test, Testable(),
-- ** Property language
Property(), PropertyLike(),
- tt, ff, inv, (*&&*), (*==>*), (==>),
+ tt, ff, inv, (*&&*), (*==>*), (==>), (|&&|),
forAll, exists, forAllDeeperBy, existsDeeperBy,
-- * Serial and Series definition
Serial(series), Series(),
View
29 Test/LazySmallCheck2012/Core.lhs
@@ -5,6 +5,7 @@
> import Control.Arrow
> import Control.DeepSeq
> import Control.Exception
+> import Control.Monad
> import Data.Data
> import Data.Maybe
> import Data.Monoid
@@ -13,7 +14,7 @@
>
> import Test.PartialValues
-> infixr 3 *&&*
+> infixr 3 *&&*, |&&|
> infixl 1 *==>*, ==>
Special Lazy SmallCheck exceptions
@@ -200,6 +201,7 @@ Properties
----------
> data Property = Lift Bool | Not Property | And Property Property
+> | PAnd Property Property
> | Implies Property Property
> | ForAll (Depth -> Depth) (Series Property)
> | Exists (Depth -> Depth) (Series Property)
@@ -246,6 +248,11 @@ Smart constructors for `Property`s.
> inv :: PropertyLike a => a -> Property
> inv = Not . mkProperty
>
+> -- | Boolean lazy implication.
+> (==>) :: Bool -> Bool -> Bool
+> False ==> _ = True
+> True ==> x = x
+>
> -- | 'Property' equivalent to '&&'.
> (*&&*) :: (PropertyLike a, PropertyLike b) => a -> b -> Property
> xs *&&* ys = mkProperty xs `And` mkProperty ys
@@ -253,6 +260,10 @@ Smart constructors for `Property`s.
> (*==>*) :: (PropertyLike a, PropertyLike b) => a -> b -> Property
> xs *==>* ys = mkProperty xs `Implies` mkProperty ys
>
+> -- | Parallel conjunction. If left is undefined, try right.
+> (|&&|) :: (PropertyLike a, PropertyLike b) => a -> b -> Property
+> xs |&&| ys = mkProperty xs `PAnd` mkProperty ys
+>
> -- | Universal quantification. Space searched is bounded by the
> -- global depth.
> forAll :: Testable a => a -> Property
@@ -305,17 +316,21 @@ through the `runPartial` function.
> prop (Not p) = not `fmap2` prop p
> prop (And p q) = (&&) `fmap2` prop p `appl2` prop q
> prop (Implies p q) = (==>) `fmap2` prop p `appl2` prop q
+> prop (PAnd p q) = parcomm (&&) (prop p) (prop q)
> prop (ForAll f xs) = isNothing `fmap2` refute (n + 1) (f d) xs
> prop (Exists f xs) = isJust `fmap2` refute (n + 1) (f d) (fmap Not xs)
> refineWith es (Sum m, Left (Expand (n', ps)))
> | n == n' = first (mappend $ Sum m) (terms (es ps))
> refineWith es x = x
-
-> -- | Boolean lazy implication.
-> (==>) :: Bool -> Bool -> Bool
-> False ==> _ = True
-> True ==> x = x
-
+>
+> -- | Parallel application of commutative binary Boolean functions.
+> parcomm :: (Bool -> Bool -> Bool) ->
+> Counter (Either LSC Bool) -> Counter (Either LSC Bool) ->
+> Counter (Either LSC Bool)
+> parcomm f p q = query (force $ snd p) (force $ snd q)
+> where force = join . fmap (peek . pure)
+> query (Left _) (Right _) = f `fmap2` q `appl2` p
+> query x _ = f `fmap2` p `appl2` q
> join2 :: Counter (Either a (Counter (Either a b))) -> Counter (Either a b)
> join2 (m, Left x) = (m, Left x)
View
40 suite/Suite.hs
@@ -28,7 +28,7 @@ data Test = forall a. (Data a, Typeable a, Testable a) =>
suite = [ test1, test2, test3, test4, test5, test6, test7, test8
, test9, test10, test11a, test11b, test11c
- , test12a, test12b, test12c ]
+ , test12a, test12b, test12c, test13, test14a, test14b ]
------------------------------------------------------------------------------------
@@ -43,19 +43,41 @@ isPrefix (x:xs) (y:ys) = x == y && isPrefix xs ys
test1 = Test "isPrefix" (\xs ys -> isPrefix xs (xs ++ ys)) True 5
test2 = Test "flip isPrefix" (\xs ys -> flip isPrefix xs (xs ++ ys)) False 5
--- Set insert
-type Set a = [a]
-
+-- Ordered List insert
insert :: Char -> [Char] -> [Char]
insert x [] = [x]
-insert x (y:ys) | x <= y = x:y:ys
+insert x (y:ys) | x <= y = x : y : ys
| otherwise = y : insert x ys
ordered :: Ord a => [a] -> Bool
ordered (x:y:zs) = x <= y && ordered (y:zs)
ordered _ = True
-test3 = Test "Set insert" (\c s -> ordered s ==> ordered (insert c s)) True 5
+test3 = Test "Ordered List insert"
+ (\c s -> ordered s ==> ordered (insert c s)) True 5
+
+-- Set insert
+
+allDiff [] = True
+allDiff (x:xs) = x `notElem` xs && allDiff xs
+
+isSet :: Ord a => Bool -> [a] -> Property
+isSet False xs = ordered xs *&&* allDiff xs
+isSet True xs = ordered xs |&&| allDiff xs
+
+setinsert :: Char -> [Char] -> [Char]
+setinsert x [] = [x]
+setinsert x (y:ys) | x == y = y : ys
+ | x <= y = x : y : ys
+ | otherwise = y : setinsert x ys
+
+test14a = Test "Set insert -- sequential conjunction"
+ (\c s -> isSet False s *==>* isSet False (setinsert c s))
+ True 5
+
+test14b = Test "Set insert -- parallel conjunction"
+ (\c s -> isSet True s *==>* isSet True (setinsert c s))
+ True 5
-- Associativity of Boolean
test4 = Test "Associativity of binary Boolean functions"
@@ -144,6 +166,12 @@ test10 = Test "Any fmap over the heap maintains the invariant."
invariant (fmap (f :: Peano -> Peano) h))
False 5
+-- Find a predicate on strings
+
+test13 = Test "Some large string"
+ (\p -> p "some long string" ==> p "some other string")
+ False 30
+
-- Clock/Emit is a monad
data ClockEmit a = Step (ClockEmit a)

0 comments on commit accb8f2

Please sign in to comment.
Something went wrong with that request. Please try again.