@@ -1,7 +1,7 @@
11-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2−{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables #-}
2+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
33
4−module TySet(plugin, Set, Union) where
4+module TySet(plugin, Set, Union, dropPrefix) where
55
66import TypeRep
77import Type
@@ -36,12 +36,14 @@ import TcRnMonad ( TcPlugin(..), TcPluginResult(..)
3636 , Ct(..), CtEvidence(..), CtLoc, ctLoc, ctPred
3737 , mkNonCanonical, isTouchableTcM, unsafeTcPluginTcM)
3838import Plugins ( CommandLineOption, defaultPlugin, Plugin(..) )
39+import GHC.TcPluginM.Extra
3940
4041import Debug.Trace
4142import Outputable
4243import DynFlags
4344
4445import Control.Monad
46+import Control.Monad.Trans.Maybe
4547import Control.Applicative
4648import qualified Data.Typeable as DT
4749import Data.List
@@ -70,30 +72,31 @@ thePlugin opts = TcPlugin
7072 , tcPluginStop = pluginStop
7173 }
7274
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+
7382pluginInit :: [CommandLineOption] -> TcPluginM ()
7483pluginInit _ = return ()
7584
7685pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
7786pluginSolve () given derived wanted =
78− do -- For debugging, show the constraints
79− tcPluginTrace "SET" $ ppCts wanted
80− tcPluginTrace "SET" $ ppr $ head $ wanted
81− solved <- findSetEquality wanted
82− -- For the sake of debugging
83− tcPluginIO $ putStrLn "Running Set equality plugin"
84− return $ TcPluginOk solved []
85−
86−-- Possible eqations for the solver
87−-- Union a b ~ a => b ~ '[]
88−-- Union a b ~ b => a ~ '[]
87+ let ?ifDebug = True in
8988
90−-- Union (Union a b) c ~ d => Union a (Union b c) ~ d
91−-- Union '[] a ~ b => a ~ b
92−-- Union a '[] ~ b => a ~ b
93−-- Union a a ~ b => a ~ b (can do in a reduce phases that looks through a tree of union terms..)
89+ do
90+ tcPluginIO $ debug "Running TySet equality plugin"
91+ debug $ ppCts wanted
92+ -- debug $ ppr $ head $ wanted
9493
95−-- Reqires an `ordering'
96−-- Union a b ~ c => Union b a ~ c [for the purpose of normalisation]
94+ --solved <- findEmptySetEquality wanted
95+ (solved, generated) <- findSetEquality wanted
96+ return $ TcPluginOk solved generated
97+
98+pluginStop :: () -> TcPluginM ()
99+pluginStop _ = return ()
97100
98101-- Pretty print constraints
99102ppCts [] = text "(empty)"
@@ -106,7 +109,10 @@ instance Show Var where
106109 show v = showSDocUnsafe $ ppr v
107110instance Show TyCon where
108111 show tycon = showSDocUnsafe $ ppr tycon
112+instance Show Ct where
113+ show ct = showSDocUnsafe $ ppr ct
109114
115+{-
110116-- Prediacate one whether a type is = Set '[]
111117isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
112118 guard $ length tcs == 2
@@ -115,80 +121,159 @@ isEmptySetType t = do (x, tcs) <- splitTyConApp_maybe t
115121 do guard $ k == k'
116122 guard $ (getOccString . tyConName $ con) == "[]"
117123 _ -> Nothing
124+-}
118125
119126getNameStr = getOccString . tyConName
120127
121−isUnion :: Type -> Bool
122−isUnion t = case splitTyConApp_maybe t of
123− Just (x, tcs) -> (getOccString . tyConName $ x) == "Union"
124− _ -> False
125−
126−-- splitUnion :: Type -> ([Type], [Type])
127−splitUnion t = do (x, tcs) <- splitTyConApp_maybe t
128− guard $ (getOccString . tyConName $ x) == "Union"
129−
130−splitList t = do (tcon, args) <- splitTyConApp_maybe t
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) ->
131161 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'
132173 ":" -> do guard $ (length args >= 2)
133174 (t1 : (t2 : ts)) <- return args
134− (kind, emptyArgs) <- splitTyConApp_maybe $ t1
135− guard $ emptyArgs == []
136− -- maybe be unnecessary and even restrictive
137− guard $ getNameStr kind == "*"
138− ts' <- splitList $ head ts -- possible bug here
139− return $ (t2 : ts')
175+ (kind, args) <- splitTyConApp_maybe $ t1
176+ ts' <- listTypeToTerm $ head ts -- possible bug here
177+ return $ Union (Data [t2]) ts'
140178 "[]" -> do guard $ (length args == 1)
141179 [t] <- return args
142− (kind, emptyArgs) <- splitTyConApp_maybe $ t
143− -- maybe be unnecessary and even restrictive
144− guard $ getNameStr kind == "*"
145− guard $ emptyArgs == []
146− return $ []
147− _ -> return $ []
148−
149−unionSingle t = do (x, tcs) <- splitTyConApp_maybe t
150− guard $ length tcs == 2
151− guard $ getNameStr x == "Set"
152− return ()
153−
154−{- Experimenting, finds Set '[] ~ Set '[] and returns a refl coercion
155− This was set up before when 'Set' was a type family, but is now redundant
156−-}
157−findSetEquality :: [Ct] -> TcPluginM [(EvTerm, Ct)]
158−findSetEquality [] = return []
159−findSetEquality (ct : xs) = let x = (do (Nominal,t1,t2) <- getEqPredTys_maybe (ctPred ct)
160− isEmptySetType t1
161− isEmptySetType t2
162− return ((EvCoercion $ TcRefl Nominal t1, ct), t1))
163− y = do (Nominal,t1,t2) <- getEqPredTys_maybe (ctPred ct)
164− return t1
165− in
166− case x of
167− Just (ct, tcsA) -> do xs' <- (findSetEquality xs)
168− tcPluginTrace "SET" $ ppr $ tcsA
169− tcPluginTrace "SET" $ text $ show tcsA
170− return $ ct : xs'
171− Nothing -> case y of
172− Just t -> do tcPluginTrace "SET" $ text $ show t
173− return []
174−
175− Nothing -> findSetEquality xs
176−
177−pluginStop :: () -> TcPluginM ()
178−pluginStop _ = 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 :: Eq a => TermTree a -> ([String], [a])
188− normalisedRep t = let (vs, ds) = separate t
189− in (nub . sort $ vs, nub ds)
190−
191−separate :: TermTree a -> ([String], [a])
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])
192277separate Empty = ([], [])
193278separate (Var s) = ([s], [])
194279separate (Data xs) = ([], xs)
@@ -198,12 +283,16 @@ separate (Union a b) = let (vs1, ds1) = separate a
198283
199284{-- Unit testing of normaliser and set equality --}
200285testSetTermEquality :: IO ()
201−testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> equal n m)
286+testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n == m)
287+
288+mkVar :: String -> Var
289+mkVar = undefined
202290
203291instance Arbitrary (TermTree Int, TermTree Int) where
204292 arbitrary = sized $ \vars ->
205293 sized $ \datums ->
206− do v <- (vector vars)::(Gen [String])
294+ do v0 <- (vector vars)::(Gen [String])
295+ v <- return $ map mkVar v0
207296 dat <- (vector datums)::(Gen [Int])
208297 v' <- shuffle v
209298 dat' <- shuffle dat
@@ -228,7 +317,7 @@ unionPerm x y = do x' <- x
228317 elements [Union x' y', Union y' x']
229318
230319-- Generates arbitrary terms from a list of variables and list of Int adtums
231−gen :: [String] -> [Int] -> Gen (TermTree Int)
320+gen :: [Var] -> [Int] -> Gen (TermTree Int)
232321gen [] [] = return $ Empty
233322gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs' has elements
234323 choose <- suchThat arbitrary (\x -> x<=(2 - if vs == [] then 1 else 0) && x>=0)