1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where
import Control.Exception (evaluate)
import Data.List (elemIndex)
import Data.Int (Int8)
import Test.QuickCheck
import Data.Universe.Class (Universe(..), Finite(..))
import Data.Universe.Helpers (interleave, choices)
import Data.Set (Set)
import Data.Ratio (Ratio, (%))
import Numeric.Natural (Natural)
import System.Timeout (timeout)
import qualified Data.Set as Set
data P a = P
-------------------------------------------------------------------------------
-- Universe laws
-------------------------------------------------------------------------------
universeLaw :: (Eq a, Show a, Arbitrary a, Universe a) => P a -> a -> Property
universeLaw _ x = counterexample (show x) (elem x universe)
universeProdLaw
:: forall a. (Ord a, Show a, Arbitrary a, Universe a)
=> P a -> NonNegative Int -> Property
universeProdLaw _ (NonNegative n) = label (show $ div n 10) $
let pfx = take n universe :: [a]
in length pfx === nubLength pfx
nubLength :: Ord a => [a] -> Int
nubLength = Set.size . Set.fromList
universeLaws :: (Ord a, Show a, Arbitrary a, Universe a) => P a -> Property
universeLaws p = universeLaw p .&&. universeProdLaw p
rationalLaw :: Gen Property
-- We have to keep the numbers fairly small here to avoid needing to
-- dig too deep.
rationalLaw = do
n <- choose (-19, 19 :: Integer)
d <- choose (1, 19)
return $ let nd = n % d in counterexample (show nd) (elem nd universe)
natRatioLaw :: Gen Property
natRatioLaw = do
n <- choose (0, 19 :: Int)
d <- choose (1, 19 :: Int)
return $ let nd = (fromIntegral n :: Natural) % fromIntegral d
in counterexample (show nd) (elem nd universe)
-------------------------------------------------------------------------------
-- Finite laws
-------------------------------------------------------------------------------
finiteLaw1 :: (Eq a, Show a, Arbitrary a, Finite a) => P a -> a -> Property
finiteLaw1 _ x = counterexample (show x) (elem x universeF)
finiteLaw2 :: (Eq a, Show a, Arbitrary a, Finite a) => P a -> a -> Property
finiteLaw2 _ x = length (filter (== x) universeF) === 1
finiteLaws :: (Ord a, Show a, Arbitrary a, Finite a) => P a -> Property
finiteLaws p = universeLaws p .&&. finiteLaw1 p .&&. finiteLaw2 p
-------------------------------------------------------------------------------
-- Special examples
-------------------------------------------------------------------------------
eitherExample :: Property
eitherExample = once $ u /= f
where
u = elemIndex (Left True :: Either Bool Bool) universe
f = elemIndex (Left True :: Either Bool Bool) universeF
choicesLazinessProperty :: IO ()
choicesLazinessProperty = do
v <- timeout oneSecond (evaluate (s !! 1))
case v of
Just _ -> putStrLn "OK"
Nothing -> putStrLn "ERROR: Timeout while evaluating a sneaky, self-referential collection of helpers"
where
-- generate strings from the grammar S -> x | S S
s = interleave [["x"], map concat $ choices [s, s]]
oneSecond = 1000000
-------------------------------------------------------------------------------
-- Main
-------------------------------------------------------------------------------
main :: IO ()
main = do
-- Note: checking on 'Int' is bad idea as it's definition is 'universeDef',
-- i.e. it takes lots of time to get to small numbers!
quickCheck eitherExample
quickCheck $ universeLaws (P :: P Integer)
quickCheck $ universeLaws (P :: P Natural')
quickCheck $ rationalLaw
quickCheck $ natRatioLaw
quickCheck $ universeProdLaw (P :: P Rational)
quickCheck $ universeProdLaw (P :: P (Ratio Natural))
quickCheck $ finiteLaws (P :: P Char)
quickCheck $ finiteLaws (P :: P (Maybe Int8))
quickCheck $ finiteLaws (P :: P (Either Int8 Int8))
-- Even this is a bad idea:
-- quickCheck $ universeLaw (P :: P [Bool])
quickCheck $ universeProdLaw (P :: P (Set Integer))
quickCheck $ finiteLaws (P :: P (Set ()))
quickCheck $ finiteLaws (P :: P (Set Bool))
quickCheck $ finiteLaws (P :: P (Set (Maybe Bool)))
quickCheck $ finiteLaws (P :: P (Set (Set (Maybe Bool))))
choicesLazinessProperty
-------------------------------------------------------------------------------
-- Natural'
-------------------------------------------------------------------------------
newtype Natural' = Natural' Natural deriving (Eq, Ord, Show)
instance Universe Natural' where universe = map Natural' universe
instance Arbitrary Natural' where
arbitrary = fmap (Natural' . fromInteger . abs) arbitrary
|
