@@ -184,9 +184,9 @@ equal t1 t2 = let (vs1, ds1) = normalisedRep t1
184184 (vs2, ds2) = normalisedRep t2
185185 in (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)
186186 where
187− normalisedRep :: TermTree a -> ([String], [a])
187+ normalisedRep :: Eq a => TermTree a -> ([String], [a])
188188 normalisedRep t = let (vs, ds) = separate t
189− in (sort vs, ds)
189+ in (nub . sort $ vs, nub ds)
190190
191191separate :: TermTree a -> ([String], [a])
192192separate Empty = ([], [])
@@ -197,41 +197,53 @@ separate (Union a b) = let (vs1, ds1) = separate a
197197 in (vs1++vs2, ds1++ds2)
198198
199199{-- Unit testing of normaliser and set equality --}
200−equalUnitTest :: IO ()
201−equalUnitTest = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)
200+testSetTermEquality :: IO ()
201+testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)
202202
203203instance Arbitrary (TermTree Int, TermTree Int) where
204− arbitrary = sized (\vars ->
205− sized (\datums -> do v <- (vector vars)::(Gen [String])
206− dat <- (vector datums)::(Gen [Int])
207− choose <- arbitrary::(Gen Int)
208− v' <- shuffle v
209− dat' <- shuffle dat
210− g1 <- gen v dat
211− g2 <- gen v' dat'
212− -- soundness of generation test
213− let (v0, dat0) = separate g1
214− (v1, dat1) = separate g2
215− if not( (sort v0 == sort v) && (sort v1 == sort v)
216− && (sort dat == sort dat0) && (sort dat == sort dat1)) then return ()
217− else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
218− return (g1, g2)))
204+ arbitrary = sized $ \vars ->
205+ sized $ \datums ->
206+ do v <- (vector vars)::(Gen [String])
207+ dat <- (vector datums)::(Gen [Int])
208+ v' <- shuffle v
209+ dat' <- shuffle dat
210+ g1 <- gen v dat
211+ g2 <- gen v' dat'
212+
213+ -- Soundness check on generated tree
214+ let (v0, dat0) = separate g1
215+ (v1, dat1) = separate g2
216+ norm :: (Ord a) => [a] -> [a]
217+ norm = nub . sort
218+
219+ if and [(norm v0) == (norm v), (norm v1) == (norm v),
220+ (norm dat) == (norm dat0), (norm dat) == (norm dat1)]
221+ then return ()
222+ else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
223+ return (g1, g2)
224+
225+-- Arbitrarily permute a union of two generators
219226unionPerm x y = do x' <- x
220227 y' <- y
221− choice <- arbitrary
222− return $ if choice then (Union x' y') else (Union y' x')
228+ elements [Union x' y', Union y' x']
223229
230+-- Generates arbitrary terms from a list of variables and list of Int adtums
224231gen :: [String] -> [Int] -> Gen (TermTree Int)
225232gen [] [] = return $ Empty
226−gen (v:vs) [] = unionPerm (gen vs []) (return $ Var v)
227−gen [] ds = do i <- suchThat arbitrary (<= (length ds))
228− unionPerm (gen [] (drop i ds)) (return $ Data (take i ds))
229−gen (v:vs) ds = do choose <- suchThat arbitrary (\x -> x<=2 && x>=0)
233+gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
234+ choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)
230235 case choose::Int of
231− 0 -> unionPerm (gen vs ds) (return $ Var v)
236+ -- Union with Empty
237+ 0 -> unionPerm (gen vs ds) (return $ Empty)
238+
239+ -- Pick some number of elements (maybe none) and create a data leaf
232240 1 -> do i <- suchThat arbitrary (<= (length ds))
233− unionPerm (gen (v:vs) (drop i ds)) (return $ Data (take i ds))
234− 2 -> unionPerm (gen (v:vs) ds) (return $ Empty)
241+ unionPerm (gen vs (drop i ds)) (return $ Data (take i ds))
242+
243+ -- Case where vs is non-empty, create a variable node, and either remove that
244+ -- variable, or keep it around as a possibility again to test idempotency
245+ 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
246+ unionPerm (gen vs ds) (return $ Var (head vs))]
235247 _ -> error "unpossible"
236248
237249