9fbdaa3 · type-level-sets

184 (vs2, ds2) = normalisedRep t2

185 in (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)

186 where

187− normalisedRep :: TermTree a -> ([String], [a])

187+ normalisedRep :: Eq a => TermTree a -> ([String], [a])

188 normalisedRep t = let (vs, ds) = separate t

189− in (sort vs, ds)

189+ in (nub . sort $ vs, nub ds)

190

191separate :: TermTree a -> ([String], [a])

192separate Empty = ([], [])

197 in (vs1++vs2, ds1++ds2)

198

199{-- Unit testing of normaliser and set equality --}

200−equalUnitTest :: IO ()

200+testSetTermEquality :: IO ()

201−equalUnitTest = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)

201+testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)

202

203instance Arbitrary (TermTree Int, TermTree Int) where

204− arbitrary = sized (\vars ->

204+ arbitrary = sized $ \vars ->

205+ sized $ \datums ->

205− sized (\datums -> do v <- (vector vars)::(Gen [String])

206+ do v <- (vector vars)::(Gen [String])

206− dat <- (vector datums)::(Gen [Int])

207+ dat <- (vector datums)::(Gen [Int])

207− choose <- arbitrary::(Gen Int)

208− v' <- shuffle v

208+ v' <- shuffle v

209− dat' <- shuffle dat

209+ dat' <- shuffle dat

210− g1 <- gen v dat

210+ g1 <- gen v dat

211− g2 <- gen v' dat'

211+ g2 <- gen v' dat'

212− -- soundness of generation test

212+

213+ -- Soundness check on generated tree

213− let (v0, dat0) = separate g1

214+ let (v0, dat0) = separate g1

214− (v1, dat1) = separate g2

215+ (v1, dat1) = separate g2

215− if not( (sort v0 == sort v) && (sort v1 == sort v)

216+ norm :: (Ord a) => [a] -> [a]

217+ norm = nub . sort

218+

219+ if and [(norm v0) == (norm v), (norm v1) == (norm v),

216− && (sort dat == sort dat0) && (sort dat == sort dat1)) then return ()

220+ (norm dat) == (norm dat0), (norm dat) == (norm dat1)]

221+ then return ()

217− else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)

222+ else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)

218− return (g1, g2)))

223+ return (g1, g2)

224+

225+-- Arbitrarily permute a union of two generators

219unionPerm x y = do x' <- x

226unionPerm x y = do x' <- x

220 y' <- y

227 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']

223

229

230+-- Generates arbitrary terms from a list of variables and list of Int adtums

224gen :: [String] -> [Int] -> Gen (TermTree Int)

231gen :: [String] -> [Int] -> Gen (TermTree Int)

225gen [] [] = return $ Empty

232gen [] [] = return $ Empty

226−gen (v:vs) [] = unionPerm (gen vs []) (return $ Var v)

233+gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements

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)

234+ choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)

230 case choose::Int of

235 case choose::Int of

236+ -- Union with Empty

231− 0 -> unionPerm (gen vs ds) (return $ Var v)

237+ 0 -> unionPerm (gen vs ds) (return $ Empty)

238+

239+ -- Pick some number of elements (maybe none) and create a data leaf

232 1 -> do i <- suchThat arbitrary (<= (length ds))

240 1 -> do i <- suchThat arbitrary (<= (length ds))

233− unionPerm (gen (v:vs) (drop i ds)) (return $ Data (take i ds))

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

234− 2 -> unionPerm (gen (v:vs) ds) (return $ Empty)

245+ 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),

246+ unionPerm (gen vs ds) (return $ Var (head vs))]

235 _ -> error "unpossible"

247 _ -> error "unpossible"

236

248

237

249