[Wrote tests for SemanticOrd.
Nils Anders Danielsson <nad@cs.chalmers.se>**20050531204733] {
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 1
--- | Tests for "Test.ChasingBottoms.SemanticOrd".
+{-# OPTIONS -fglasgow-exts -cpp #-}
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 3
+-- | Tests for "Test.ChasingBottoms.SemanticOrd". The functions using
+-- implicit arguments are currently not tested.
+
+-- This module contains _many_ generators. It is probably not too hard
+-- to implement them in a generic way. Then it would also be
+-- worthwhile exporting them.
+
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 12
-tests :: [Bool]
-tests =
-  [
+import Test.ChasingBottoms.IsBottom
+import Test.ChasingBottoms.SemanticOrd
+import Test.ChasingBottoms.TestUtilities
+#if __GLASGOW_HASKELL__ <= 602
+import Debug.QuickCheck
+import Debug.QuickCheck.Batch (run)
+#else
+import Test.QuickCheck
+import Test.QuickCheck.Batch (run)
+#endif
+import Data.Generics hiding (GT)
+import Control.Monad
+import Data.Maybe
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 26
-    -- We should check that ==! corresponds to an equivalence
-    -- relation, and so on for the other operators, plus test that
-    -- they really do what they are supposed to do.
+import Test.ChasingBottoms.ApproxShow
+import Test.ChasingBottoms.Nat
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 29
+------------------------------------------------------------------------
+-- Data types
+
+-- | Binary trees with information in the leaves.
+
+data Tree a
+   = Node (Tree a) (Tree a)
+   | Leaf a
+     deriving (Show, Typeable, Data)
+
+------------------------------------------------------------------------
+-- Basic generators
+
+integer :: Gen Integer
+integer = frequency [ (1, return bottom), (10, arbitrary) ]
+
+bool :: Gen Bool
+bool = elements [bottom, False, True]
+
+finiteListOf :: Gen a -> Gen [a]
+finiteListOf gen = sized finList
+  where
+  finList size | size == 0 = baseCase
+               | otherwise =
+                   frequency [ (1, baseCase)
+                             , (10, do elem <- gen
+                                       l <- finList (size - 1)
+                                       return (elem : l)
+                               )
+                             ]
+
+  baseCase = elements [bottom, []]
+
+finiteTreeOf :: Gen a -> Gen (Tree a)
+finiteTreeOf gen = sized finTree
+  where
+  finTree size | size == 0 = baseCase
+               | otherwise =
+                   frequency [ (1, baseCase)
+                             , (2, do left  <- finTree (size `div` 2)
+                                      right <- finTree (size `div` 2)
+                                      return (Node left right)
+                               )
+                             ]
+
+  baseCase = frequency [(1, bottom), (3, liftM Leaf gen)]
+
+-- | Definitely infinite lists.
+
+infiniteListOf :: Gen a -> Gen [a]
+infiniteListOf gen = liftM2 (:) gen (infiniteListOf gen)
+
+-- | Possibly infinite trees.
+
+infiniteTreeOf :: Gen a -> Gen (Tree a)
+infiniteTreeOf gen = infTree
+  where
+  infTree = frequency [ (1, return bottom)
+                      , (1, liftM Leaf gen)
+                      , (3, liftM2 Node infTree infTree)
+                      ]
+
+testGen :: (Show a, Data a) => Nat -> Gen a -> IO ()
+testGen depth gen = test $ forAll gen $ \n ->
+                      collect (approxShow depth n) $ True
+
+------------------------------------------------------------------------
+-- Cogenerators
+
+-- Note that the functions generated by these cogenerators are not
+-- necessarily monotone.
+
+type Cogen a = forall b. a -> Gen b -> Gen b
+
+coBool :: Cogen Bool
+coBool b | isBottom b = variant 0
+coBool False          = variant 1
+coBool True           = variant 2
+
+coInteger :: Cogen Integer
+coInteger i | isBottom i = variant 0
+            | otherwise  = variant 1 . coarbitrary i
+
+coListOf :: Cogen a -> Cogen [a]
+coListOf cog xs | isBottom xs = variant 0
+coListOf cog []               = variant 1
+coListOf cog (x:xs)           = variant 2 . cog x . coListOf cog xs
+
+coTreeOf :: Cogen a -> Cogen (Tree a)
+coTreeOf cog xs | isBottom xs = variant 0
+coTreeOf cog (Leaf x)         = variant 1 . cog x
+coTreeOf cog (Node l r)       = variant 2 . coTreeOf cog l . coTreeOf cog r
+
+-- Note that the functions generated by function are all non-bottom.
+-- That is not a problem, though, since the functions are only used
+-- applied to arguments when testing congruence.
+
+function :: Cogen a -> Gen b -> Gen (a -> b)
+function coGen gen = promote (\a -> coGen a gen)
+
+testFunction :: (Data a, Data b) => Nat -> Cogen a -> Gen b -> [a] -> IO ()
+testFunction depth coGen gen inputs =
+  test $ forAll (function coGen gen) $ \f ->
+    collect (map (\x -> approxShow depth (x, f x)) inputs) $ True
+
+------------------------------------------------------------------------
+-- Generators for element not equal to argument
+
+type NotEqualGen a = a -> Gen a
+
+neBool :: NotEqualGen Bool
+neBool b | isBottom b = elements [False, True]
+neBool False          = elements [bottom, True]
+neBool True           = elements [bottom, False]
+
+neInteger :: NotEqualGen Integer
+neInteger i | isBottom i = arbitrary
+            | otherwise  =
+                frequency [ (1, return bottom)
+                          , (10, do j <- arbitrary
+                                    let j' = if j >= 0 then j + 1 else j - 1
+                                    return (i + j')
+                            )
+                          ]
+
+neListOf :: Gen a -> NotEqualGen a -> (Gen a -> Gen [a]) -> NotEqualGen [a]
+neListOf gen neg listOf xs = neList xs
+  where
+  neList xs
+    | isBottom xs = frequency [ (1, return []), (10, nonEmpty gen) ]
+    | otherwise = case xs of
+        []     -> frequency [ (1, return bottom), (10, nonEmpty gen) ]
+        (y:ys) -> frequency [ (1, return bottom)
+                            , (1, return [])
+                            , (5, nonEmpty (neg y))
+                            , (5, do y' <- neg y
+                                     return (y':ys)
+                              )
+                            , (5, do ys' <- neList ys
+                                     return (y:ys')
+                              )
+                            ]
+
+  nonEmpty headGen = do x <- headGen
+                        xs <- listOf gen
+                        return (x:xs)
+
+neTreeOf :: Gen a
+         -> NotEqualGen a
+         -> (Gen a -> Gen (Tree a))
+         -> NotEqualGen (Tree a)
+neTreeOf gen neg treeOf t = neTree t
+  where
+  neTree t
+    | isBottom t = frequency [ (1, leaf gen), (10, node) ]
+    | otherwise = case t of
+        Leaf x   -> frequency [ (1, smallTreeNE x), (2, node) ]
+        Node l r -> frequency [ (1, return bottom)
+                              , (2, leaf gen)
+                              , (2, do l' <- neTree l
+                                       return (Node l' r)
+                                )
+                              , (2, do r' <- neTree r
+                                       return (Node l r')
+                                )
+                              , (2, do l' <- neTree l
+                                       r' <- node
+                                       return (Node l' r')
+                                )
+                              , (2, do l' <- node
+                                       r' <- neTree r
+                                       return (Node l' r')
+                                )
+                              ]
+
+  leaf g = liftM Leaf g
+  smallTreeNE x = frequency [(1, return bottom), (3, leaf (neg x))]
+
+  node = do l <- treeOf gen
+            r <- treeOf gen
+            return (Node l r)
+
+prop_notEqualGen element gen =
+  forAll (pair element gen) $ \(x, y) ->
+    x /=! y
+
+testGenPair :: (Show a, Data a) => Nat -> Gen a -> (a -> Gen a) -> IO ()
+testGenPair depth gen gen' = test $
+  forAll (pair gen gen') $ \(x, y) ->
+    collect (approxShow depth (x, y)) $ True
+
+------------------------------------------------------------------------
+-- Generators for element greater than or equal to argument
+
+type GreaterEqualGen a = a -> Gen a
+
+-- | 'GreaterEqualGen' for flat CPOs.
+
+flatGEGen :: Gen a -> GreaterEqualGen a
+flatGEGen gen x | isBottom x = gen
+                | otherwise  = return x
+
+geBool :: GreaterEqualGen Bool
+geBool = flatGEGen bool
+
+geInteger :: GreaterEqualGen Integer
+geInteger = flatGEGen integer
+
+geListOf :: Gen a
+         -> GreaterEqualGen a
+         -> (Gen a -> Gen [a])
+         -> GreaterEqualGen [a]
+geListOf gen geGen listOf xs
+  | isBottom xs = listOf gen
+  | otherwise   = case xs of
+      []   -> return []
+      y:ys -> do y'  <- geGen y
+                 ys' <- geListOf gen geGen listOf ys
+                 return (y':ys')
+
+geTreeOf :: Gen a
+         -> GreaterEqualGen a
+         -> (Gen a -> Gen (Tree a))
+         -> GreaterEqualGen (Tree a)
+geTreeOf gen geGen treeOf t
+  | isBottom t = treeOf gen
+  | otherwise  = case t of
+      Leaf x   -> liftM Leaf (geGen x)
+      Node l r -> do l' <- geTreeOf gen geGen treeOf l
+                     r' <- geTreeOf gen geGen treeOf r
+                     return (Node l' r')
+
+prop_greaterEqualGen element gen =
+  forAll (pair element gen) $ \(x, y) ->
+    x <=! y
+
+------------------------------------------------------------------------
+-- Generators for pairs whose components' join exists
+
+-- Note that the output pairs of these generators have components
+-- whose _meet_ is also likely to be "interesting".
+
+type JoinableGen a = a -> Gen a
+
+-- | 'JoinableGen' for flat CPOs.
+
+flatJoinGen :: Gen a -> JoinableGen a
+flatJoinGen gen x | isBottom x = gen
+                  | otherwise  = frequency [(1, return bottom), (4, return x)]
+
+joinBool :: JoinableGen Bool
+joinBool = flatJoinGen bool
+
+joinInteger :: JoinableGen Integer
+joinInteger = flatJoinGen integer
+
+joinListOf :: Gen a -> JoinableGen a -> (Gen a -> Gen [a]) -> JoinableGen [a]
+joinListOf gen joinGen listOf xs
+  | isBottom xs = listOf gen
+  | otherwise   = case xs of
+      []   -> frequency [(1, return bottom), (4, return [])]
+      y:ys -> frequency [ (1, return bottom)
+                        , (10, do y'  <- joinGen y
+                                  ys' <- joinListOf gen joinGen listOf ys
+                                  return (y':ys')
+                          )
+                        ]
+
+joinTreeOf :: Gen a
+           -> JoinableGen a
+           -> (Gen a -> Gen (Tree a))
+           -> JoinableGen (Tree a)
+joinTreeOf gen joinGen treeOf t
+  | isBottom t = treeOf gen
+  | otherwise   = case t of
+      Leaf x   -> frequency [(1, return bottom), (4, liftM Leaf (joinGen x))]
+      Node l r -> frequency [ (1, return bottom)
+                            , (5, do l' <- joinTreeOf gen joinGen treeOf l
+                                     r' <- joinTreeOf gen joinGen treeOf r
+                                     return (Node l' r')
+                              )
+                            ]
+
+prop_joinableGen element gen =
+  forAll (pair element gen) $ \(x, y) ->
+    isJust (x \/! y)
+
+------------------------------------------------------------------------
+-- The actual tests
+
+prop_SemanticEq_congruence :: (Data a, Show a)
+                           => Gen a
+                           -> NotEqualGen a
+                           -> Cogen a
+                           -> [Property]
+prop_SemanticEq_congruence element notEqualTo coGen =
+  isCongruence element return notEqualTo (==!) (/=!)
+               (function coGen integer) (==!)
+
+prop_SemanticOrd_partial_order :: (Data a, Show a)
+                               => Gen a
+                               -> NotEqualGen a
+                               -> GreaterEqualGen a
+                               -> JoinableGen a
+                               -> [Property]
+prop_SemanticOrd_partial_order element notEqualTo greaterThan joinable =
+  isPartialOrder element return notEqualTo greaterThan (==!) (<=!) ++
+  isPartialOrderOperators element greaterThan (==!) (<=!) (<!) (>=!) (>!) ++
+  [ compare
+  , meet_associative, meet_commutative, meet_idempotent, meet_lt
+  , join_associative, join_commutative, join_idempotent, join_lt
+  , join_meet_absorption, meet_join_absorption
hunk ./Test/ChasingBottoms/SemanticOrd/Tests.hs 342
+  where
+  twoElems = pair3 element greaterThan
+
+  compare =
+    forAll twoElems $ \(x, y) ->
+      case semanticCompare x y of
+        Nothing -> not (x <=! y) && not (x >=! y)
+        Just LT -> x <! y
+        Just EQ -> x ==! y
+        Just GT -> x >! y
+
+  meet_associative = isAssociative (oneof [ liftM3 (,,) element element element
+                                          , triple element joinable joinable
+                                          ]
+                                   )
+                                   (==!) (/\!)
+  meet_commutative = isCommutative (oneof [ liftM2 (,) element element
+                                          , pair element joinable
+                                          ]
+                                   )
+                                   (==!) (/\!)
+  meet_idempotent  = isIdempotent element (==!) (/\!)
+
+  join_associative =
+    forAll (triple element joinable joinable) $ \(x, y, z) ->
+      (x \/! y >>= (\/! z)) ==! ((x \/!) =<< y \/! z)
+  join_commutative = isCommutative (pair element joinable) (==!) (\/!)
+  join_idempotent  =
+    forAll element $ \x ->
+      x \/! x ==! Just x
+
+  join_meet_absorption =
+    forAll jmPair $ \(x, y) ->
+      x \/! (x /\! y) ==! Just x
+    where jmPair = oneof [ liftM2 (,) element element
+                         , pair element joinable
+                         ]
+  meet_join_absorption =
+    forAll (pair element joinable) $ \(x, y) ->
+      x /\! fromJust (x \/! y) ==! x
+
+  twoElems' = frequency [ (2, twoElems), (1, pair element joinable) ]
+
+  meet_lt =
+    forAll twoElems' $ \(x, y) ->
+      (x <=! y) == (x /\! y ==! x)
+  join_lt =
+    forAll twoElems' $ \(x, y) ->
+      (x <=! y) == (x \/! y ==! Just y)
+
+-- | All tests collected together.
+
+tests :: IO Bool
+tests = runQuickCheckTests $ map run $ concat theTests
+  where
+  theTests =
+      -- Testing the generators.
+    [ [ prop_notEqualGen bool neBool
+      , prop_notEqualGen integer neInteger
+      , prop_notEqualGen (finiteListOf bool)
+                         (neListOf bool neBool finiteListOf)
+      , prop_notEqualGen (finiteTreeOf integer)
+                         (neTreeOf integer neInteger finiteTreeOf)
+      ]
+    , [ prop_greaterEqualGen bool geBool
+      , prop_greaterEqualGen integer geInteger
+      , prop_greaterEqualGen (finiteListOf bool)
+                             (geListOf bool geBool finiteListOf)
+      , prop_greaterEqualGen (finiteTreeOf integer)
+                             (geTreeOf integer geInteger finiteTreeOf)
+      ]
+    , [ prop_joinableGen bool joinBool
+      , prop_joinableGen integer joinInteger
+      , prop_joinableGen (finiteListOf bool)
+                         (joinListOf bool joinBool finiteListOf)
+      , prop_joinableGen (finiteTreeOf integer)
+                         (joinTreeOf integer joinInteger finiteTreeOf)
+      ]
+      -- Testing the functions from SemanticOrd.
+    , prop_SemanticEq_congruence bool neBool coBool
+    , prop_SemanticEq_congruence integer neInteger coInteger
+    , prop_SemanticEq_congruence (finiteListOf bool)
+                                 (neListOf bool neBool finiteListOf)
+                                 (coListOf coBool)
+    , prop_SemanticEq_congruence (finiteTreeOf integer)
+                                 (neTreeOf integer neInteger finiteTreeOf)
+                                 (coTreeOf coInteger)
+    , prop_SemanticOrd_partial_order bool neBool geBool joinBool
+    , prop_SemanticOrd_partial_order integer neInteger geInteger joinInteger
+    , prop_SemanticOrd_partial_order (finiteListOf bool)
+                                     (neListOf bool neBool finiteListOf)
+                                     (geListOf bool geBool finiteListOf)
+                                     (joinListOf bool joinBool finiteListOf)
+    , prop_SemanticOrd_partial_order (finiteTreeOf integer)
+                                     (neTreeOf integer neInteger finiteTreeOf)
+                                     (geTreeOf integer geInteger finiteTreeOf)
+                                     (joinTreeOf integer joinInteger
+                                                 finiteTreeOf)
+    ]
hunk ./Test/ChasingBottoms/Tests.hs 3
--- | Tests of everything related to "Test.ChasingBottoms". Not finished
---   yet. (Missing: "Test.ChasingBottoms.SemanticOrd".)
+-- | Tests of almost everything related to "Test.ChasingBottoms".
hunk ./Test/ChasingBottoms/Tests.hs 12
--- import qualified Test.ChasingBottoms.SemanticOrd.Tests as SemanticOrd
+import qualified Test.ChasingBottoms.SemanticOrd.Tests as SemanticOrd
hunk ./Test/ChasingBottoms/Tests.hs 61
-                   -- , test "SemanticOrd:" SemanticOrd.tests
+                   , test "SemanticOrd:" SemanticOrd.tests
}