git.iko.soy/type-level-sets
on master help sign in
some updates to the solver, trying to work with the plugin
618db42dominic
TySet.hs+19−8
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
1-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
2{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
2{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
3
3
4−module TySet(plugin, Set, Union, dropPrefix) where
4+module TySet(plugin, Set, Union, dropPrefix, ppr) where
5
5
6import TypeRep
6import TypeRep
7import Type
7import Type
@@ -82,17 +82,32 @@ instance Debug String IO where
82pluginInit :: [CommandLineOption] -> TcPluginM ()
82pluginInit :: [CommandLineOption] -> TcPluginM ()
83pluginInit _ = return ()
83pluginInit _ = return ()
84
84
85+printerS = let ?ifDebug = True in tcPluginIO . debug . showSDocUnsafe . ppCts
86+printer = let ?ifDebug = True in tcPluginIO . debug
87+
85pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
88pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
86pluginSolve () given derived wanted =
89pluginSolve () given derived wanted =
87 let ?ifDebug = True in
90 let ?ifDebug = True in
88
91
89− do
92+ do tcPluginIO $ debug "*****************************"
90 tcPluginIO $ debug "Running TySet equality plugin"
93 tcPluginIO $ debug "Running TySet equality plugin"
94+ --debug $ ppCts wanted
91− 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
92 -- debug $ ppr $ head $ wanted
102 -- debug $ ppr $ head $ wanted
93
103
94 --solved <- findEmptySetEquality wanted
104 --solved <- findEmptySetEquality wanted
95 (solved, generated) <- findSetEquality wanted
105 (solved, generated) <- findSetEquality wanted
106+ printer "Done - solved"
107+ printerS (map snd solved)
108+ printer "DOne - generated"
109+ printerS generated
110+
96 return $ TcPluginOk solved generated
111 return $ TcPluginOk solved generated
97
112
98pluginStop :: () -> TcPluginM ()
113pluginStop :: () -> TcPluginM ()
@@ -288,7 +303,7 @@ testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n
288mkVar :: String -> Var
303mkVar :: String -> Var
289mkVar = undefined
304mkVar = undefined
290
305
291−instance Arbitrary (TermTree Int, TermTree Int) where
306+instance {-# OVERLAPS #-} Arbitrary (TermTree Int, TermTree Int) where
292 arbitrary = sized $ \vars ->
307 arbitrary = sized $ \vars ->
293 sized $ \datums ->
308 sized $ \datums ->
294 do v0 <- (vector vars)::(Gen [String])
309 do v0 <- (vector vars)::(Gen [String])
@@ -334,10 +349,6 @@ gen vs ds = do -- Choose between 0 and 1 if 'vs' is empty, or 0-2 if 'vs'
334 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
349 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
335 unionPerm (gen vs ds) (return $ Var (head vs))]
350 unionPerm (gen vs ds) (return $ Var (head vs))]
336 _ -> error "unpossible"
351 _ -> error "unpossible"
337−
338−
339−
340−
341
352
342
353
343
354
example-new.hs−25
@@ -3,31 +3,6 @@
3{-# OPTIONS_GHC -fplugin=TyMap #-}
3{-# OPTIONS_GHC -fplugin=TyMap #-}
4import TyMap
4import TyMap
5
5
6−
7−
8−
9−
10−
11−
12−
13−
14−
15−
16−
17−
18−
19−
20−
21−
22−
23−
24−
25−
26−
27−
28−
29−
30−
31import GHC.TypeLits
6import GHC.TypeLits
32
7
33
8
example.hs+4
@@ -1,6 +1,7 @@
1{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
1{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
2
2
3import GHC.TypeLits
3import GHC.TypeLits
4+import Data.Type.Set (subset)
4import Data.Type.Map
5import Data.Type.Map
5
6
6-- Specify that key-value pairs on Ints combine to an Int
7-- Specify that key-value pairs on Ints combine to an Int
@@ -24,3 +25,6 @@ bar = Ext (Var :: (Var "y")) 3 $
24-- GHC can easily infer this type, so an explicit signature not necessary
25-- GHC can easily infer this type, so an explicit signature not necessary
25-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
26-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
26foobar = foo `union` bar
27foobar = foo `union` bar
28+
29+foobarToFoo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
30+foobarToFoo = subset foobar