@@ -1,355 +0,0 @@
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−