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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes, TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.Equivalence.Monad_Test where
import Test.QuickCheck hiding ((===), classes)
import Data.Equivalence.Monad
import Control.Monad
import Data.Function (on)
import Data.Set (Set)
import qualified Data.Set as Set
import System.Exit
--------------------------------------------------------------------------------
-- Test Suits
--------------------------------------------------------------------------------
-- run :: (Ord a) => STT s Identity (Equiv s (Set a) a)
run :: (Ord v) => (forall s. EquivM s (Set v) v a) -> a
run = runEquivM Set.singleton Set.union
runInt :: (forall s. EquivM s (Set Int) Int a) -> a
runInt = run
allM f l = liftM and $ mapM f l
getClasses l1 = mapM getClass l1
infixr 9 <.>
-- | Composition: pure function after functorial (monadic) function.
(<.>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c
(f <.> g) a = f <$> g a
--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------
prop_singleton v = runInt $ do
d <- classDesc v
return (d == Set.singleton v)
prop_equateAll l' v = runInt $ do
let l = v:l'
equateAll l
d <- classDesc v
return (d == Set.fromList l)
prop_combineAll l' v = runInt $ do
let l = v:l'
cls <- getClasses l
cl <- getClass v
combineAll cls
d <- desc cl
return (d == Set.fromList l)
prop_equate x y = runInt $ do
equate x y
d <- classDesc x
return (d == Set.fromList [x,y])
prop_combine x y = runInt $ do
[cx,cy] <- getClasses [x,y]
combine cx cy
d <- desc cx
return (d == Set.fromList [x,y])
prop_equateOverlap x y z = runInt $ do
equate x y
equate y z
equivalent x z
prop_combineOverlap x y z = runInt $ do
[cx,cy,cz] <- getClasses [x,y,z]
combine cx cy
combine cy cz
cx === cz
prop_equateAllOverlap x y l1' l2' = runInt $ do
let l1 = x:l1'
l2 = y:l2'
equateAll l1
equateAll l2
if Set.null $ Set.fromList l1 `Set.intersection` Set.fromList l2
then liftM not $ equivalent x y
else equivalent x y
prop_combineAllOverlap x y l1' l2' = runInt $ do
let l1 = x:l1'
l2 = y:l2'
cls1 <- getClasses l1
cls2 <- getClasses l2
[cx,cy] <- getClasses [x,y]
combineAll cls1
combineAll cls2
if Set.null $ Set.fromList l1 `Set.intersection` Set.fromList l2
then liftM not (cx === cy)
else cx === cy
prop_removeClass x l' = runInt $ do
let l = x:l'
equateAll l
removeClass x
allM (\e -> liftM (== Set.singleton e) (classDesc e)) l
prop_remove x l' = runInt $ do
let l = x:l'
cls <- getClasses l
combineAll cls
cx <- getClass x
remove cx
allM check l
where check e = liftM (== Set.singleton e) $ getClass e >>= desc
prop_removeClass' x y l1' l2' = runInt $ do
let l1 = x:l1'
l2 = x:y:l2'
equateAll l1
removeClass x
equateAll l2
d <- classDesc y
return (Set.fromList l2 == d)
prop_remove' x y l1' l2' = runInt $ do
let l1 = x:l1'
l2 = x:y:l2'
cls1 <- getClasses l1
cls2 <- getClasses l2
cx <- getClass x
combineAll cls1
remove cx
combineAll cls2
cy <- getClass y
d <- desc cy
return (Set.fromList l2 == d)
prop_getClasses l1 l1' l2 x y =
putStrLn (show el ++ ";" ++ show cl) `whenFail` (el == cl)
where
l3 = concat (l2 : l1)
el = runInt $ do
mapM equateAll l1
mapM removeClass l2
mapM equateAll (l1' :: [[Int]])
res <- mapM classDesc l3
eq <- equivalent x y
return (res,eq)
cl = runInt $ do
cls1 <- mapM getClasses l1
mapM combineAll cls1
cls2 <- getClasses l2
mapM remove cls2
cls1' <- mapM getClasses l1'
mapM combineAll cls1'
cls3 <- getClasses l3
res <- mapM desc cls3
[cx,cy] <- getClasses [x,y]
eq <- cx === cy
return (res,eq)
prop_values l = runInt $ do
mapM (\x -> equate x x) l
sameSet l <$> values
where
sameSet = (==) `on` Set.fromList
prop_classes l = runInt $ do
mapM equateAll (l :: [[Int]])
classes1 <- uniqClass =<< mapM getClass =<< values
sameClasses classes1 =<< classes
where
uniqClass [] = return []
uniqClass (c:cs) = (c :) <$> do
uniqClass =<< filterM (not <.> (c ===)) cs
sameClasses [] cs2 = return $ null cs2
sameClasses (c:cs1') cs2 = sameClasses cs1' =<< filterM (not <.> (c ===)) cs2
return []
main :: IO ()
main = do
success <- $quickCheckAll
if success then exitSuccess else exitFailure
|
