@@ -0,0 +1,199 @@
1+{-# LANGUAGE CPP #-}
2+{-# LANGUAGE FlexibleInstances #-}
3+{-# LANGUAGE GADTs #-}
4+{-# LANGUAGE TemplateHaskell #-}
5+{-# LANGUAGE TypeOperators #-}
6+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
7+{-# LANGUAGE PolyKinds #-}
8+#endif
9+module Data.GADT.Compare.TH
10+ ( DeriveGEQ(..)
11+ , DeriveGCompare(..)
12+ , GComparing, runGComparing, geq', compare'
13+ ) where
14+
15+import Control.Applicative
16+import Control.Monad
17+import Data.GADT.Compare
18+import Language.Haskell.TH
19+import Language.Haskell.TH.Extras
20+
21+-- A type class purely for overloading purposes
22+class DeriveGEQ t where
23+ deriveGEq :: t -> Q [Dec]
24+
25+instance DeriveGEQ Name where
26+ deriveGEq typeName = do
27+ typeInfo <- reify typeName
28+ case typeInfo of
29+ TyConI dec -> deriveGEq dec
30+ _ -> fail "deriveGEq: the name of a type constructor is required"
31+
32+instance DeriveGEQ Dec where
33+ deriveGEq (InstanceD cxt (AppT instType dataType) decs)
34+ | headOfType instType == ''GEq = do
35+ let dataTypeName = headOfType dataType
36+ dataTypeInfo <- reify dataTypeName
37+ case dataTypeInfo of
38+ TyConI (DataD dataCxt name bndrs cons _) -> do
39+ geqDec <- geqFunction bndrs cons
40+ return [InstanceD cxt (AppT instType dataType) [geqDec]]
41+ _ -> fail "deriveGEq: the name of an algebraic data type constructor is required"
42+ deriveGEq (DataD dataCxt name bndrs cons _) = return <$> inst
43+ where
44+ inst = instanceD (cxt (map return dataCxt)) (appT (conT ''GEq) (conT name)) [geqDec]
45+ geqDec = geqFunction bndrs cons
46+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 612
47+ deriveGEq (DataInstD dataCxt name tyArgs cons _) = return <$> inst
48+ where
49+ inst = instanceD (cxt (map return dataCxt)) (appT (conT ''GEq) (foldl1 appT (map return $ (ConT name : init tyArgs)))) [geqDec]
50+ -- TODO: figure out proper number of family parameters vs instance parameters
51+ bndrs = [PlainTV v | VarT v <- tail tyArgs ]
52+ geqDec = geqFunction bndrs cons
53+#endif
54+
55+instance DeriveGEQ t => DeriveGEQ [t] where
56+ deriveGEq [it] = deriveGEq it
57+ deriveGEq _ = fail "deriveGEq: [] instance only applies to single-element lists"
58+
59+instance DeriveGEQ t => DeriveGEQ (Q t) where
60+ deriveGEq = (>>= deriveGEq)
61+
62+geqFunction bndrs cons = funD 'geq
63+ ( map (geqClause bndrs) cons
64+ ++ [ clause [wildP, wildP] (normalB [| Nothing |]) []
65+ | length cons /= 1
66+ ]
67+ )
68+
69+geqClause bndrs con = do
70+ let argTypes = argTypesOfCon con
71+ needsGEq argType = any ((`occursInType` argType) . nameOfBinder) (bndrs ++ varsBoundInCon con)
72+
73+ nArgs = length argTypes
74+ lArgNames <- replicateM nArgs (newName "x")
75+ rArgNames <- replicateM nArgs (newName "y")
76+
77+ clause [ conP conName (map varP lArgNames)
78+ , conP conName (map varP rArgNames)
79+ ]
80+ ( normalB $ doE
81+ ( [ if needsGEq argType
82+ then bindS (conP 'Refl []) [| geq $(varE lArg) $(varE rArg) |]
83+ else noBindS [| guard ($(varE lArg) == $(varE rArg)) |]
84+ | (lArg, rArg, argType) <- zip3 lArgNames rArgNames argTypes
85+ ]
86+ ++ [ noBindS [| return Refl |] ]
87+ )
88+ ) []
89+ where conName = nameOfCon con
90+
91+-- A monad allowing gcompare to be defined in the same style as geq
92+newtype GComparing a b t = GComparing (Either (GOrdering a b) t)
93+
94+instance Functor (GComparing a b) where fmap f (GComparing x) = GComparing (either Left (Right . f) x)
95+instance Monad (GComparing a b) where
96+ return = GComparing . Right
97+ GComparing (Left x) >>= f = GComparing (Left x)
98+ GComparing (Right x) >>= f = f x
99+instance Applicative (GComparing a b) where
100+ pure = return
101+ (<*>) = ap
102+
103+geq' :: GCompare t => t a -> t b -> GComparing x y (a := b)
104+geq' x y = GComparing (case gcompare x y of
105+ GLT -> Left GLT
106+ GEQ -> Right Refl
107+ GGT -> Left GGT)
108+
109+compare' x y = GComparing $ case compare x y of
110+ LT -> Left GLT
111+ EQ -> Right ()
112+ GT -> Left GGT
113+
114+runGComparing (GComparing x) = either id id x
115+
116+class DeriveGCompare t where
117+ deriveGCompare :: t -> Q [Dec]
118+
119+instance DeriveGCompare Name where
120+ deriveGCompare typeName = do
121+ typeInfo <- reify typeName
122+ case typeInfo of
123+ TyConI dec -> deriveGCompare dec
124+ _ -> fail "deriveGCompare: the name of a type constructor is required"
125+
126+instance DeriveGCompare Dec where
127+ deriveGCompare (InstanceD cxt (AppT instType dataType) decs)
128+ | headOfType instType == ''GCompare = do
129+ let dataTypeName = headOfType dataType
130+ dataTypeInfo <- reify dataTypeName
131+ case dataTypeInfo of
132+ TyConI (DataD dataCxt name bndrs cons _) -> do
133+ gcompareDec <- gcompareFunction bndrs cons
134+ return [InstanceD cxt (AppT instType dataType) [gcompareDec]]
135+ _ -> fail "deriveGCompare: the name of an algebraic data type constructor is required"
136+ deriveGCompare (DataD dataCxt name bndrs cons _) = return <$> inst
137+ where
138+ inst = instanceD (cxt (map return dataCxt)) (appT (conT ''GCompare) (conT name)) [gcompareDec]
139+ gcompareDec = gcompareFunction bndrs cons
140+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 612
141+ deriveGCompare (DataInstD dataCxt name tyArgs cons _) = return <$> inst
142+ where
143+ inst = instanceD (cxt (map return dataCxt)) (appT (conT ''GCompare) (foldl1 appT (map return $ (ConT name : init tyArgs)))) [gcompareDec]
144+ -- TODO: figure out proper number of family parameters vs instance parameters
145+ bndrs = [PlainTV v | VarT v <- tail tyArgs ]
146+ gcompareDec = gcompareFunction bndrs cons
147+#endif
148+
149+instance DeriveGCompare t => DeriveGCompare [t] where
150+ deriveGCompare [it] = deriveGCompare it
151+ deriveGCompare _ = fail "deriveGCompare: [] instance only applies to single-element lists"
152+
153+instance DeriveGCompare t => DeriveGCompare (Q t) where
154+ deriveGCompare = (>>= deriveGCompare)
155+
156+gcompareFunction boundVars cons
157+ | null cons = funD 'gcompare [clause [] (normalB [| \x y -> seq x (seq y undefined) |]) []]
158+ | otherwise = funD 'gcompare (concatMap gcompareClauses cons)
159+ where
160+ -- for every constructor, first check for equality (recursively comparing
161+ -- arguments) then add catch-all cases; all not-yet-matched patterns are
162+ -- "greater than" the constructor under consideration.
163+ gcompareClauses con =
164+ [ mainClause con
165+ , clause [recP conName [], wildP] (normalB [| GLT |]) []
166+ , clause [wildP, recP conName []] (normalB [| GGT |]) []
167+ ] where conName = nameOfCon con
168+
169+ needsGCompare argType con = any ((`occursInType` argType) . nameOfBinder) (boundVars ++ varsBoundInCon con)
170+
171+ -- main clause; using the 'GComparing' monad, compare all arguments to the
172+ -- constructor recursively, attempting to unify type variables by recursive
173+ -- calls to gcompare whenever needed (that is, whenever a constructor argument's
174+ -- type contains a variable bound in the data declaration or in the constructor's
175+ -- type signature)
176+ mainClause con = do
177+ let conName = nameOfCon con
178+ argTypes = argTypesOfCon con
179+ nArgs = length argTypes
180+
181+ lArgNames <- replicateM nArgs (newName "x")
182+ rArgNames <- replicateM nArgs (newName "y")
183+
184+ clause [ conP conName (map varP lArgNames)
185+ , conP conName (map varP rArgNames)
186+ ]
187+ ( normalB
188+ [| runGComparing $
189+ $(doE
190+ ( [ if needsGCompare argType con
191+ then bindS (conP 'Refl []) [| geq' $(varE lArg) $(varE rArg) |]
192+ else noBindS [| compare' $(varE lArg) $(varE rArg) |]
193+ | (lArg, rArg, argType) <- zip3 lArgNames rArgNames argTypes
194+ ]
195+ ++ [ noBindS [| return GEQ |] ]
196+ )
197+ )
198+ |]
199+ ) []