@@ -0,0 +1,355 @@
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, ppr) 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+printerS = let ?ifDebug = True in tcPluginIO . debug . showSDocUnsafe . ppCts
86+printer = let ?ifDebug = True in tcPluginIO . debug
87+
88+pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
89+pluginSolve () given derived wanted =
90+ let ?ifDebug = True in
91+
92+ do tcPluginIO $ debug "*****************************"
93+ tcPluginIO $ debug "Running TySet equality plugin"
94+ --debug $ ppCts wanted
95+ tcPluginIO $ debug $ showSDocUnsafe $ ppCts wanted
96+ tcPluginIO $ debug "Givens"
97+ --debug $ ppCts given
98+ tcPluginIO $ debug $ showSDocUnsafe $ ppCts given
99+ tcPluginIO $ debug "Derived"
100+ -- debug $ ppCts derived
101+ tcPluginIO $ debug $ showSDocUnsafe $ ppCts derived
102+ -- debug $ ppr $ head $ wanted
103+
104+ --solved <- findEmptySetEquality wanted
105+ (solved, generated) <- findSetEquality wanted
106+ printer "Done - solved"
107+ printerS (map snd solved)
108+ printer "DOne - generated"
109+ printerS generated
110+
111+ return $ TcPluginOk solved generated
112+
113+pluginStop :: () -> TcPluginM ()
114+pluginStop _ = return ()
115+
116+-- Pretty print constraints
117+ppCts [] = text "(empty)"
118+ppCts cs = vcat (map ppr cs)
119+
120+{- Some debugging Show instances to help me understand what is coming in and out of GHC -}
121+deriving instance Show TyLit
122+deriving instance Show Type
123+instance Show Var where
124+ show v = showSDocUnsafe $ ppr v
125+instance Show TyCon where
126+ show tycon = showSDocUnsafe $ ppr tycon
127+instance Show Ct where
128+ show ct = showSDocUnsafe $ ppr ct
129+
130+{-
131+-- Prediacate one whether a type is = Set '[]
132+isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
133+ guard $ length tcs == 2
134+ guard $ getOccString (tyConName x) == "Set"
135+ case tcs of [TyVarTy k, TyConApp con [TyVarTy k']] ->
136+ do guard $ k == k'
137+ guard $ (getOccString . tyConName $ con) == "[]"
138+ _ -> Nothing
139+-}
140+
141+getNameStr = getOccString . tyConName
142+
143+liftTc :: Maybe a -> MaybeT TcPluginM a
144+liftTc = MaybeT . return
145+
146+liftMt :: TcPluginM a -> MaybeT TcPluginM a
147+liftMt x = MaybeT (fmap Just x)
148+
149+findSetEquality :: [Ct] -> TcPluginM ([(EvTerm, Ct)], [Ct])
150+findSetEquality [] = return ([], [])
151+findSetEquality (ct : xs) =
152+ do x <- runMaybeT $
153+ do (Nominal, t1, t2) <- liftTc $ getEqPredTys_maybe (ctPred ct)
154+ a <- liftTc $ listTypeToTerm t1
155+ b <- "sofar sogood" `trace` liftTc $ listTypeToTerm t2
156+ (show (t1, a, t2, b)) `trace`
157+ if (a == b) then
158+ "are equal" `trace` return $ Left (EvCoercion $ TcRefl Nominal t1, ct)
159+ else -- not equal, try to find an mgu and generate conditions on that
160+ let ?ctLoc = ctLoc ct in
161+ do unifiers <- "not equal" `trace` mgu a b
162+ case unifiers of
163+ Left unifiers -> ("L unifiers: \n" ++ show unifiers) `trace` return $ Right []
164+ Right (dataUnifiers, unsolvedExtra) -> ("data unifiers:" ++ (show $ dataUnifiers)) `trace` return $ Right $ (EvCoercion $ TcRefl Nominal t1, ct) : map (\c -> (EvCoercion $ TcRefl Nominal undefined, c)) dataUnifiers
165+
166+ (solved, generated) <- findSetEquality xs
167+ case x of
168+ Just y -> case y of
169+ Left (ev, ct) -> return $ ((ev, ct) : solved, generated)
170+ Right cts -> return $ (solved ++ cts, generated)
171+ Nothing -> return (solved, generated)
172+
173+listTypeToTerm :: Type -> Maybe (TermTree Type)
174+listTypeToTerm t = case (splitTyConApp_maybe t) of
175+ Just (tcon, args) ->
176+ case getNameStr tcon of
177+ "Union" -> do guard $ (length args) >= 3
178+ (_ : (t1 : (t2 : ts))) <- return args
179+ t1' <- listTypeToTerm t1
180+ t2' <- listTypeToTerm t2
181+ return $ Union t1' t2'
182+ -- this case is probably temporary [see SessionListE.hs]
183+ ":++" -> do guard $ (length args) >= 3
184+ (_ : (t1 : (t2 : ts))) <- return args
185+ t1' <- listTypeToTerm t1
186+ t2' <- listTypeToTerm t2
187+ return $ Union t1' t2'
188+ ":" -> do guard $ (length args >= 2)
189+ (t1 : (t2 : ts)) <- return args
190+ (kind, args) <- splitTyConApp_maybe $ t1
191+ ts' <- listTypeToTerm $ head ts -- possible bug here
192+ return $ Union (Data [t2]) ts'
193+ "[]" -> do guard $ (length args == 1)
194+ [t] <- return args
195+ (kind, args) <- splitTyConApp_maybe $ t
196+ return $ Empty
197+
198+ _ -> return $ Empty -- Data [t]
199+ _ -> case t of
200+ TyVarTy v -> return $ Var $ v
201+
202+-- Representation for solving equalities on terms comprising union, data, and variables
203+
204+data TermTree a = Union (TermTree a) (TermTree a) | Empty | Var Var | Data [a] deriving Show
205+
206+-- if the second argument is a prefix of the first argument, then return Just of the suffix, else Nothing
207+dropPrefix :: Eq a => [a] -> [a] -> Maybe [a]
208+dropPrefix [] xs = Just []
209+dropPrefix xs [] = Just xs
210+dropPrefix (x:xs) (y:ys) | x == y = dropPrefix xs ys
211+ | otherwise = Nothing
212+
213+mguDataVars :: [a] -> [Var] -> Maybe [(Var, TermTree a)]
214+mguDataVars suffix [] = Nothing -- No variables to unify with
215+mguDataVars suffix (v:vs) = Just $ [(v, Data suffix)] ++ map (\v' -> (v', Var v)) vs
216+
217+mgu :: (?ctLoc :: CtLoc) => TermTree Type -> TermTree Type -> MaybeT TcPluginM (Either [(Var, TermTree Type)] ([Ct], ([Type], [Type]))) -- last component should be some equalities
218+mgu t1 t2 = let (vs1, ds1) = normalisedRep t1
219+ (vs2, ds2) = normalisedRep t2
220+ in ("----> " ++ show (ds1, ds2)) `trace`
221+ (show $ dropPrefix ds1 ds2) `trace`
222+ case (dropPrefix ds1 ds2) of
223+ Nothing -> case (dropPrefix ds2 ds1) of
224+ Nothing -> "el zilcho primo" `trace` do x <- liftMt (zipMatch ds1 ds2)
225+ return $ Right x -- ([], ([], []))
226+ Just suffix_ds2 -> "suffix_ds2" `trace`
227+ do x <- liftTc $ mguDataVars suffix_ds2 vs1
228+ return $ Left x
229+ Just suffix_ds1 -> ("suffix_ds1 " ++ (show suffix_ds1))
230+ `trace`
231+ if (suffix_ds1 == []) then
232+ do x <- liftMt (zipMatch ds1 ds2)
233+ ("zipm: ds1 = " ++ (show ds1) ++ " ds2 = " ++ (show ds2) ++ ": " ++ (show x)) `trace` return $ Right x -- ([], ([], []))
234+ else
235+ do x <- liftTc $ mguDataVars suffix_ds1 vs2
236+ return $ Left x
237+
238+mkEqualities :: (?ctLoc :: CtLoc) => [(Type, Type)] -> TcPluginM [Ct]
239+mkEqualities xs = (mapM (\(x, y) -> mkCt x y) xs) -- >>= (return . concat)
240+
241+mkCt t t' = fmap mkNonCanonical (newDerived ?ctLoc (uncurry mkPrimEqPred (t,t')))
242+
243+mkEqualities' (AppTy t1 t2) (AppTy t1' t2') = do ct <- mkCt t1 t1'
244+ ct' <- mkCt t2 t2'
245+ return [ct, ct']
246+mkEqualities' (TyConApp con kt) (TyConApp con' kt') | con == con' = mapM (uncurry mkCt) (zip kt kt')
247+mkEqualities' (FunTy t1 t2) (FunTy t1' t2') = do ct <- mkCt t1 t1'
248+ ct' <- mkCt t2 t2'
249+ return [ct, ct']
250+mkEqualities' (ForAllTy v t) (ForAllTy v' t') | v == v' = do ct <- mkCt t t'
251+ return [ct]
252+mkEqualities' t t' = do ct <- mkCt t t'
253+ return [ct]
254+
255+
256+
257+
258+zipMatch :: (?ctLoc :: CtLoc) => [Type] -> [Type] -> TcPluginM ([Ct], ([Type], [Type]))
259+zipMatch xs ys = let (unifiers, restL, restR) = zipMatch' xs ys
260+ in do unifiers' <- mkEqualities unifiers
261+ return $ (unifiers', (restL, restR))
262+
263+zipMatch' :: [a] -> [a] -> ([(a, a)], [a], [a])
264+zipMatch' [] xs = ([], [], xs)
265+zipMatch' xs [] = ([], xs, [])
266+zipMatch' (x:xs) (y:ys) = let (zips, l, r) = zipMatch' xs ys
267+ in ((x, y) : zips, l, r)
268+
269+
270+
271+
272+
273+
274+subst :: TermTree a -> [(Var, TermTree a)] -> TermTree a
275+subst (Union s t) theta = Union (subst s theta) (subst t theta)
276+subst (Var a) theta = case (lookup a theta) of
277+ Just t -> t
278+ Nothing -> Var a
279+subst t theta = t
280+
281+instance Eq a => Eq (TermTree a) where
282+ t1 == t2 = let (vs1, ds1) = normalisedRep t1
283+ (vs2, ds2) = normalisedRep t2
284+ in ("vars = " ++ (show (vs1, vs2)) ++ " eq = " ++ (show (vs1 == vs2)))
285+ `trace` (vs1 == vs2) && (all (flip elem $ ds2) ds1) && (all (flip elem $ ds1) ds2)
286+
287+normalisedRep :: Eq a => TermTree a -> ([Var], [a])
288+normalisedRep t = let (vs, ds) = separate t
289+ in (nub . sort $ vs, nub ds)
290+
291+separate :: TermTree a -> ([Var], [a])
292+separate Empty = ([], [])
293+separate (Var s) = ([s], [])
294+separate (Data xs) = ([], xs)
295+separate (Union a b) = let (vs1, ds1) = separate a
296+ (vs2, ds2) = separate b
297+ in (vs1++vs2, ds1++ds2)
298+
299+{-- Unit testing of normaliser and set equality --}
300+testSetTermEquality :: IO ()
301+testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n == m)
302+
303+mkVar :: String -> Var
304+mkVar = undefined
305+
306+instance {-# OVERLAPS #-} Arbitrary (TermTree Int, TermTree Int) where
307+ arbitrary = sized $ \vars ->
308+ sized $ \datums ->
309+ do v0 <- (vector vars)::(Gen [String])
310+ v <- return $ map mkVar v0
311+ dat <- (vector datums)::(Gen [Int])
312+ v' <- shuffle v
313+ dat' <- shuffle dat
314+ g1 <- gen v dat
315+ g2 <- gen v' dat'
316+
317+ -- Soundness check on generated tree
318+ let (v0, dat0) = separate g1
319+ (v1, dat1) = separate g2
320+ norm :: (Ord a) => [a] -> [a]
321+ norm = nub . sort
322+
323+ if and [(norm v0) == (norm v), (norm v1) == (norm v),
324+ (norm dat) == (norm dat0), (norm dat) == (norm dat1)]
325+ then return ()
326+ else error $ "Generated trees failed soundness check: " ++ (show g1) ++ " " ++ (show g2)
327+ return (g1, g2)
328+
329+-- Arbitrarily permute a union of two generators
330+unionPerm x y = do x' <- x
331+ y' <- y
332+ elements [Union x' y', Union y' x']
333+
334+-- Generates arbitrary terms from a list of variables and list of Int adtums
335+gen :: [Var] -> [Int] -> Gen (TermTree Int)
336+gen [] [] = return $ Empty
337+gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
338+ choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)
339+ case choose::Int of
340+ -- Union with Empty
341+ 0 -> unionPerm (gen vs ds) (return $ Empty)
342+
343+ -- Pick some number of elements (maybe none) and create a data leaf
344+ 1 -> do i <- suchThat arbitrary (<= (length ds))
345+ unionPerm (gen vs (drop i ds)) (return $ Data (take i ds))
346+
347+ -- Case where vs is non-empty, create a variable node, and either remove that
348+ -- variable, or keep it around as a possibility again to test idempotency
349+ 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
350+ unionPerm (gen vs ds) (return $ Var (head vs))]
351+ _ -> error "unpossible"
352+
353+
354+
355+