@@ -0,0 +1,344 @@
1+-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
3+
4+module TySet(plugin, Set, Union, dropPrefix) where
5+
6+import TypeRep
7+import Type
8+import Kind
9+import TcEvidence
10+import CoAxiom
11+import Name
12+import OccName
13+import Var
14+import TyCon
15+import BasicTypes
16+
17+-- friends:
18+import Var
19+import VarEnv
20+import VarSet
21+import Name
22+import BasicTypes
23+import TyCon
24+import Class
25+import CoAxiom
26+
27+-- others
28+import PrelNames
29+import Outputable
30+import FastString
31+import Util
32+import DynFlags
33+
34+import TcPluginM ( TcPluginM, tcPluginIO, tcPluginTrace )
35+import TcRnMonad ( TcPlugin(..), TcPluginResult(..)
36+ , Ct(..), CtEvidence(..), CtLoc, ctLoc, ctPred
37+ , mkNonCanonical, isTouchableTcM, unsafeTcPluginTcM)
38+import Plugins ( CommandLineOption, defaultPlugin, Plugin(..) )
39+import GHC.TcPluginM.Extra
40+
41+import Debug.Trace
42+import Outputable
43+import DynFlags
44+
45+import Control.Monad
46+import Control.Monad.Trans.Maybe
47+import Control.Applicative
48+import qualified Data.Typeable as DT
49+import Data.List
50+
51+import Test.QuickCheck
52+import Test.QuickCheck.Property
53+
54+{- Set constructor -}
55+data Set (a :: [k])
56+{- Union operation -}
57+type family Union (a :: [k]) (b :: [k]) :: [k]
58+
59+type family Member (a :: k) (b :: [k]) :: Bool where
60+ Member x '[] = False
61+ Member x (x ': xs) = True
62+ Member x (y ': xs) = Member x xs
63+
64+{- Plugin setup -}
65+plugin :: Plugin
66+plugin = defaultPlugin { tcPlugin = Just . thePlugin }
67+
68+thePlugin :: [CommandLineOption] -> TcPlugin
69+thePlugin opts = TcPlugin
70+ { tcPluginInit = pluginInit opts
71+ , tcPluginSolve = pluginSolve
72+ , tcPluginStop = pluginStop
73+ }
74+
75+class Debug t m where
76+ debug :: (?ifDebug :: Bool) => t -> m ()
77+instance Debug SDoc TcPluginM where
78+ debug x = tcPluginTrace "TySet" x
79+instance Debug String IO where
80+ debug x = putStrLn x
81+
82+pluginInit :: [CommandLineOption] -> TcPluginM ()
83+pluginInit _ = return ()
84+
85+pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
86+pluginSolve () given derived wanted =
87+ let ?ifDebug = True in
88+
89+ do
90+ tcPluginIO $ debug "Running TySet equality plugin"
91+ debug $ ppCts wanted
92+ -- debug $ ppr $ head $ wanted
93+
94+ --solved <- findEmptySetEquality wanted
95+ (solved, generated) <- findSetEquality wanted
96+ return $ TcPluginOk solved generated
97+
98+pluginStop :: () -> TcPluginM ()
99+pluginStop _ = return ()
100+
101+-- Pretty print constraints
102+ppCts [] = text "(empty)"
103+ppCts cs = vcat (map ppr cs)
104+
105+{- Some debugging Show instances to help me understand what is coming in and out of GHC -}
106+deriving instance Show TyLit
107+deriving instance Show Type
108+instance Show Var where
109+ show v = showSDocUnsafe $ ppr v
110+instance Show TyCon where
111+ show tycon = showSDocUnsafe $ ppr tycon
112+instance Show Ct where
113+ show ct = showSDocUnsafe $ ppr ct
114+
115+{-
116+-- Prediacate one whether a type is = Set '[]
117+isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
118+ guard $ length tcs == 2
119+ guard $ getOccString (tyConName x) == "Set"
120+ case tcs of [TyVarTy k, TyConApp con [TyVarTy k']] ->
121+ do guard $ k == k'
122+ guard $ (getOccString . tyConName $ con) == "[]"
123+ _ -> Nothing
124+-}
125+
126+getNameStr = getOccString . tyConName
127+
128+liftTc :: Maybe a -> MaybeT TcPluginM a
129+liftTc = MaybeT . return
130+
131+liftMt :: TcPluginM a -> MaybeT TcPluginM a
132+liftMt x = MaybeT (fmap Just x)
133+
134+findSetEquality :: [Ct] -> TcPluginM ([(EvTerm, Ct)], [Ct])
135+findSetEquality [] = return ([], [])
136+findSetEquality (ct : xs) =
137+ do x <- runMaybeT $
138+ do (Nominal, t1, t2) <- liftTc $ getEqPredTys_maybe (ctPred ct)
139+ a <- liftTc $ listTypeToTerm t1
140+ b <- "sofar sogood" `trace` liftTc $ listTypeToTerm t2
141+ (show (t1, a, t2, b)) `trace`
142+ if (a == b) then
143+ "are equal" `trace` return $ Left (EvCoercion $ TcRefl Nominal t1, ct)
144+ else -- not equal, try to find an mgu and generate conditions on that
145+ let ?ctLoc = ctLoc ct in
146+ do unifiers <- "not equal" `trace` mgu a b
147+ case unifiers of
148+ Left unifiers -> ("L unifiers: \n" ++ show unifiers) `trace` return $ Right []
149+ Right (dataUnifiers, unsolvedExtra) -> ("data unifiers:" ++ (show $ dataUnifiers)) `trace` return $ Right $ (EvCoercion $ TcRefl Nominal t1, ct) : map (\c -> (EvCoercion $ TcRefl Nominal undefined, c)) dataUnifiers
150+
151+ (solved, generated) <- findSetEquality xs
152+ case x of
153+ Just y -> case y of
154+ Left (ev, ct) -> return $ ((ev, ct) : solved, generated)
155+ Right cts -> return $ (solved ++ cts, generated)
156+ Nothing -> return (solved, generated)
157+
158+listTypeToTerm :: Type -> Maybe (TermTree Type)
159+listTypeToTerm t = case (splitTyConApp_maybe t) of
160+ Just (tcon, args) ->
161+ case getNameStr tcon of
162+ "Union" -> do guard $ (length args) >= 3
163+ (_ : (t1 : (t2 : ts))) <- return args
164+ t1' <- listTypeToTerm t1
165+ t2' <- listTypeToTerm t2
166+ return $ Union t1' t2'
167+ -- this case is probably temporary [see SessionListE.hs]
168+ ":++" -> do guard $ (length args) >= 3
169+ (_ : (t1 : (t2 : ts))) <- return args
170+ t1' <- listTypeToTerm t1
171+ t2' <- listTypeToTerm t2
172+ return $ Union t1' t2'
173+ ":" -> do guard $ (length args >= 2)
174+ (t1 : (t2 : ts)) <- return args
175+ (kind, args) <- splitTyConApp_maybe $ t1
176+ ts' <- listTypeToTerm $ head ts -- possible bug here
177+ return $ Union (Data [t2]) ts'
178+ "[]" -> do guard $ (length args == 1)
179+ [t] <- return args
180+ (kind, args) <- splitTyConApp_maybe $ t
181+ return $ Empty
182+
183+ _ -> return $ Empty -- Data [t]
184+ _ -> case t of
185+ TyVarTy v -> return $ Var $ v
186+
187+-- Representation for solving equalities on terms comprising union, data, and variables
188+
189+data TermTree a = Union (TermTree a) (TermTree a) | Empty | Var Var | Data [a] deriving Show
190+
191+-- if the second argument is a prefix of the first argument, then return Just of the suffix, else Nothing
192+dropPrefix :: Eq a => [a] -> [a] -> Maybe [a]
193+dropPrefix [] xs = Just []
194+dropPrefix xs [] = Just xs
195+dropPrefix (x:xs) (y:ys) | x == y = dropPrefix xs ys
196+ | otherwise = Nothing
197+
198+mguDataVars :: [a] -> [Var] -> Maybe [(Var, TermTree a)]
199+mguDataVars suffix [] = Nothing -- No variables to unify with
200+mguDataVars suffix (v:vs) = Just $ [(v, Data suffix)] ++ map (\v' -> (v', Var v)) vs
201+
202+mgu :: (?ctLoc :: CtLoc) => TermTree Type -> TermTree Type -> MaybeT TcPluginM (Either [(Var, TermTree Type)] ([Ct], ([Type], [Type]))) -- last component should be some equalities
203+mgu t1 t2 = let (vs1, ds1) = normalisedRep t1
204+ (vs2, ds2) = normalisedRep t2
205+ in ("----> " ++ show (ds1, ds2)) `trace`
206+ (show $ dropPrefix ds1 ds2) `trace`
207+ case (dropPrefix ds1 ds2) of
208+ Nothing -> case (dropPrefix ds2 ds1) of
209+ Nothing -> "el zilcho primo" `trace` do x <- liftMt (zipMatch ds1 ds2)
210+ return $ Right x -- ([], ([], []))
211+ Just suffix_ds2 -> "suffix_ds2" `trace`
212+ do x <- liftTc $ mguDataVars suffix_ds2 vs1
213+ return $ Left x
214+ Just suffix_ds1 -> ("suffix_ds1 " ++ (show suffix_ds1))
215+ `trace`
216+ if (suffix_ds1 == []) then
217+ do x <- liftMt (zipMatch ds1 ds2)
218+ ("zipm: ds1 = " ++ (show ds1) ++ " ds2 = " ++ (show ds2) ++ ": " ++ (show x)) `trace` return $ Right x -- ([], ([], []))
219+ else
220+ do x <- liftTc $ mguDataVars suffix_ds1 vs2
221+ return $ Left x
222+
223+mkEqualities :: (?ctLoc :: CtLoc) => [(Type, Type)] -> TcPluginM [Ct]
224+mkEqualities xs = (mapM (\(x, y) -> mkCt x y) xs) -- >>= (return . concat)
225+
226+mkCt t t' = fmap mkNonCanonical (newDerived ?ctLoc (uncurry mkPrimEqPred (t,t')))
227+
228+mkEqualities' (AppTy t1 t2) (AppTy t1' t2') = do ct <- mkCt t1 t1'
229+ ct' <- mkCt t2 t2'
230+ return [ct, ct']
231+mkEqualities' (TyConApp con kt) (TyConApp con' kt') | con == con' = mapM (uncurry mkCt) (zip kt kt')
232+mkEqualities' (FunTy t1 t2) (FunTy t1' t2') = do ct <- mkCt t1 t1'
233+ ct' <- mkCt t2 t2'
234+ return [ct, ct']
235+mkEqualities' (ForAllTy v t) (ForAllTy v' t') | v == v' = do ct <- mkCt t t'
236+ return [ct]
237+mkEqualities' t t' = do ct <- mkCt t t'
238+ return [ct]
239+
240+
241+
242+
243+zipMatch :: (?ctLoc :: CtLoc) => [Type] -> [Type] -> TcPluginM ([Ct], ([Type], [Type]))
244+zipMatch xs ys = let (unifiers, restL, restR) = zipMatch' xs ys
245+ in do unifiers' <- mkEqualities unifiers
246+ return $ (unifiers', (restL, restR))
247+
248+zipMatch' :: [a] -> [a] -> ([(a, a)], [a], [a])
249+zipMatch' [] xs = ([], [], xs)
250+zipMatch' xs [] = ([], xs, [])
251+zipMatch' (x:xs) (y:ys) = let (zips, l, r) = zipMatch' xs ys
252+ in ((x, y) : zips, l, r)
253+
254+
255+
256+
257+
258+
259+subst :: TermTree a -> [(Var, TermTree a)] -> TermTree a
260+subst (Union s t) theta = Union (subst s theta) (subst t theta)
261+subst (Var a) theta = case (lookup a theta) of
262+ Just t -> t
263+ Nothing -> Var a
264+subst t theta = t
265+
266+instance Eq a => Eq (TermTree a) where
267+ t1 == t2 = let (vs1, ds1) = normalisedRep t1
268+ (vs2, ds2) = normalisedRep t2
269+ in ("vars = " ++ (show (vs1, vs2)) ++ " eq = " ++ (show (vs1 == vs2)))
270+ `trace` (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)
271+
272+normalisedRep :: Eq a => TermTree a -> ([Var], [a])
273+normalisedRep t = let (vs, ds) = separate t
274+ in (nub . sort $ vs, nub ds)
275+
276+separate :: TermTree a -> ([Var], [a])
277+separate Empty = ([], [])
278+separate (Var s) = ([s], [])
279+separate (Data xs) = ([], xs)
280+separate (Union a b) = let (vs1, ds1) = separate a
281+ (vs2, ds2) = separate b
282+ in (vs1++vs2, ds1++ds2)
283+
284+{-- Unit testing of normaliser and set equality --}
285+testSetTermEquality :: IO ()
286+testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n == m)
287+
288+mkVar :: String -> Var
289+mkVar = undefined
290+
291+instance Arbitrary (TermTree Int, TermTree Int) where
292+ arbitrary = sized $ \vars ->
293+ sized $ \datums ->
294+ do v0 <- (vector vars)::(Gen [String])
295+ v <- return $ map mkVar v0
296+ dat <- (vector datums)::(Gen [Int])
297+ v' <- shuffle v
298+ dat' <- shuffle dat
299+ g1 <- gen v dat
300+ g2 <- gen v' dat'
301+
302+ -- Soundness check on generated tree
303+ let (v0, dat0) = separate g1
304+ (v1, dat1) = separate g2
305+ norm :: (Ord a) => [a] -> [a]
306+ norm = nub . sort
307+
308+ if and [(norm v0) == (norm v), (norm v1) == (norm v),
309+ (norm dat) == (norm dat0), (norm dat) == (norm dat1)]
310+ then return ()
311+ else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
312+ return (g1, g2)
313+
314+-- Arbitrarily permute a union of two generators
315+unionPerm x y = do x' <- x
316+ y' <- y
317+ elements [Union x' y', Union y' x']
318+
319+-- Generates arbitrary terms from a list of variables and list of Int adtums
320+gen :: [Var] -> [Int] -> Gen (TermTree Int)
321+gen [] [] = return $ Empty
322+gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
323+ choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)
324+ case choose::Int of
325+ -- Union with Empty
326+ 0 -> unionPerm (gen vs ds) (return $ Empty)
327+
328+ -- Pick some number of elements (maybe none) and create a data leaf
329+ 1 -> do i <- suchThat arbitrary (<= (length ds))
330+ unionPerm (gen vs (drop i ds)) (return $ Data (take i ds))
331+
332+ -- Case where vs is non-empty, create a variable node, and either remove that
333+ -- variable, or keep it around as a possibility again to test idempotency
334+ 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
335+ unionPerm (gen vs ds) (return $ Var (head vs))]
336+ _ -> error "unpossible"
337+
338+
339+
340+
341+
342+
343+
344+