git.iko.soy/type-level-sets
on master help sign in
some updates to the solver, trying to work with the plugin
commit618db423afb62b43081324b819fbdf91757e45f2 authordominic <dom.orchard@gmail.com> dateTue 23 Feb 2016, 15:32 (11 years ago) parenta86bba9
3 files changed+23−33
compare with master
unifiedsplit
TySet.hs+19−8 example-new.hs−25 example.hs+4
TySet.hs+19−8
@@ -1,7 +1,7 @@
11-- {-# OPTIONS_GHC -package=ghc-7.10.1 #-}
22{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, StandaloneDeriving, TypeOperators, FlexibleInstances, ScopedTypeVariables, ImplicitParams, MultiParamTypeClasses #-}
33
4−module TySet(plugin, Set, Union, dropPrefix) where
4+module TySet(plugin, Set, Union, dropPrefix, ppr) where
55
66import TypeRep
77import Type
@@ -82,17 +82,32 @@ instance Debug String IO where
8282pluginInit :: [CommandLineOption] -> TcPluginM ()
8383pluginInit _ = return ()
8484
85+printerS = let ?ifDebug = True in tcPluginIO . debug . showSDocUnsafe . ppCts
86+printer = let ?ifDebug = True in tcPluginIO . debug
87+
8588pluginSolve :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
8689pluginSolve () given derived wanted =
8790 let ?ifDebug = True in
8891
89− do
92+ do tcPluginIO $ debug "*****************************"
9093 tcPluginIO $ debug "Running TySet equality plugin"
91− debug $ ppCts wanted
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
92102 -- debug $ ppr $ head $ wanted
93103
94104 --solved <- findEmptySetEquality wanted
95105 (solved, generated) <- findSetEquality wanted
106+ printer "Done - solved"
107+ printerS (map snd solved)
108+ printer "DOne - generated"
109+ printerS generated
110+
96111 return $ TcPluginOk solved generated
97112
98113pluginStop :: () -> TcPluginM ()
@@ -288,7 +303,7 @@ testSetTermEquality = quickCheck (\((n, m) :: (TermTree Int, TermTree Int)) -> n
288303mkVar :: String -> Var
289304mkVar = undefined
290305
291−instance Arbitrary (TermTree Int, TermTree Int) where
306+instance {-# OVERLAPS #-} Arbitrary (TermTree Int, TermTree Int) where
292307 arbitrary = sized $ \vars ->
293308 sized $ \datums ->
294309 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'
334349 2 -> oneof [unionPerm (gen (tail vs) ds) (return $ Var (head vs)),
335350 unionPerm (gen vs ds) (return $ Var (head vs))]
336351 _ -> error "unpossible"
337−
338−
339−
340−
341352
342353
343354
example-new.hs−25
@@ -3,31 +3,6 @@
33{-# OPTIONS_GHC -fplugin=TyMap #-}
44import TyMap
55
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−
316import GHC.TypeLits
327
338
example.hs+4
@@ -1,6 +1,7 @@
11{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies, MultiParamTypeClasses #-}
22
33import GHC.TypeLits
4+import Data.Type.Set (subset)
45import Data.Type.Map
56
67-- Specify that key-value pairs on Ints combine to an Int
@@ -24,3 +25,6 @@ bar = Ext (Var :: (Var "y")) 3 $
2425-- GHC can easily infer this type, so an explicit signature not necessary
2526-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
2627foobar = foo `union` bar
28+
29+foobarToFoo :: Map '["x" :-> Int, "z" :-> Int, "w" :-> Int]
30+foobarToFoo = subset foobar