@@ -1,5 +1,5 @@
11-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2−{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators #-}
2+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables #-}
33
44module TySet(plugin, Set, Union) where
55
@@ -42,7 +42,12 @@ import Outputable
4242import DynFlags
4343
4444import Control.Monad
45+import Control.Applicative
4546import qualified Data.Typeable as DT
47+import Data.List
48+
49+import Test.QuickCheck
50+import Test.QuickCheck.Property
4651
4752{- Set constructor -}
4853data Set (a :: [k])
@@ -130,7 +135,7 @@ splitList t = do (tcon, args) <- splitTyConApp_maybe t
130135 guard $ emptyArgs == []
131136 -- maybe be unnecessary and even restrictive
132137 guard $ getNameStr kind == "*"
133− ts' <- splitList ts
138+ ts' <- splitList $ head ts -- possible bug here
134139 return $ (t2 : ts')
135140 "[]" -> do guard $ (length args == 1)
136141 [t] <- return args
@@ -139,11 +144,11 @@ splitList t = do (tcon, args) <- splitTyConApp_maybe t
139144 guard $ getNameStr kind == "*"
140145 guard $ emptyArgs == []
141146 return $ []
142− _ -> Nothing
147+ _ -> return $ []
143148
144149unionSingle t = do (x, tcs) <- splitTyConApp_maybe t
145150 guard $ length tcs == 2
146− guard $ getName x == "Set"
151+ guard $ getNameStr x == "Set"
147152 return ()
148153
149154{- Experimenting, finds Set '[] ~ Set '[] and returns a refl coercion
@@ -171,3 +176,68 @@ findSetEquality (ct : xs) = let x = (do (Nominal,t1,t2) <- getEqPredTys_maybe (c
171176
172177pluginStop :: () -> TcPluginM ()
173178pluginStop _ = return ()
179+
180+data TermTree a = Union (TermTree a) (TermTree a) | Empty | Var String | Data [a] deriving Show
181+
182+equal :: Eq a => TermTree a -> TermTree a -> Bool
183+equal t1 t2 = let (vs1, ds1) = normalisedRep t1
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])
188+ normalisedRep t = let (vs, ds) = separate t
189+ in (sort vs, ds)
190+
191+separate :: TermTree a -> ([String], [a])
192+separate Empty = ([], [])
193+separate (Var s) = ([s], [])
194+separate (Data xs) = ([], xs)
195+separate (Union a b) = let (vs1, ds1) = separate a
196+ (vs2, ds2) = separate b
197+ in (vs1++vs2, ds1++ds2)
198+
199+{-- Unit testing of normaliser and set equality --}
200+equalUnitTest :: IO ()
201+equalUnitTest = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)
202+
203+instance 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)))
219+unionPerm x y = do x' <- x
220+ y' <- y
221+ choice <- arbitrary
222+ return $ if choice then (Union x' y') else (Union y' x')
223+
224+gen :: [String] -> [Int] -> Gen (TermTree Int)
225+gen [] [] = 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)
230+ case choose::Int of
231+ 0 -> unionPerm (gen vs ds) (return $ Var v)
232+ 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)
235+ _ -> error "unpossible"
236+
237+
238+
239+
240+
241+
242+
243+