@@ -1,344 +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) 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−