@@ -0,0 +1,199 @@
2+{-# LANGUAGE FlexibleInstances #-}
4+{-# LANGUAGE TemplateHaskell #-}
5+{-# LANGUAGE TypeOperators #-}
6+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
7+{-# LANGUAGE PolyKinds #-}
9+module Data.GADT.Compare.TH
12+ , GComparing, runGComparing, geq', compare'
15+import Control.Applicative
17+import Data.GADT.Compare
18+import Language.Haskell.TH
19+import Language.Haskell.TH.Extras
21+-- A type class purely for overloading purposes
22+class DeriveGEQ t where
23+ deriveGEq :: t -> Q [Dec]
25+instance DeriveGEQ Name where
26+ deriveGEq typeName = do
27+ typeInfo <- reify typeName
29+ TyConI dec -> deriveGEq dec
30+ _ -> fail "deriveGEq: the name of a type constructor is required"
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
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
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
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
55+instance DeriveGEQ t => DeriveGEQ [t] where
56+ deriveGEq [it] = deriveGEq it
57+ deriveGEq _ = fail "deriveGEq: [] instance only applies to single-element lists"
59+instance DeriveGEQ t => DeriveGEQ (Q t) where
60+ deriveGEq = (>>= deriveGEq)
62+geqFunction bndrs cons = funD 'geq
63+ ( map (geqClause bndrs) cons
64+ ++ [ clause [wildP, wildP] (normalB [| Nothing |]) []
69+geqClause bndrs con = do
70+ let argTypes = argTypesOfCon con
71+ needsGEq argType = any ((`occursInType` argType) . nameOfBinder) (bndrs ++ varsBoundInCon con)
73+ nArgs = length argTypes
74+ lArgNames <- replicateM nArgs (newName "x")
75+ rArgNames <- replicateM nArgs (newName "y")
77+ clause [ conP conName (map varP lArgNames)
78+ , conP conName (map varP rArgNames)
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
86+ ++ [ noBindS [| return Refl |] ]
89+ where conName = nameOfCon con
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)
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
103+geq' :: GCompare t => t a -> t b -> GComparing x y (a := b)
104+geq' x y = GComparing (case gcompare x y of
109+compare' x y = GComparing $ case compare x y of
114+runGComparing (GComparing x) = either id id x
116+class DeriveGCompare t where
117+ deriveGCompare :: t -> Q [Dec]
119+instance DeriveGCompare Name where
120+ deriveGCompare typeName = do
121+ typeInfo <- reify typeName
123+ TyConI dec -> deriveGCompare dec
124+ _ -> fail "deriveGCompare: the name of a type constructor is required"
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
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
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
149+instance DeriveGCompare t => DeriveGCompare [t] where
150+ deriveGCompare [it] = deriveGCompare it
151+ deriveGCompare _ = fail "deriveGCompare: [] instance only applies to single-element lists"
153+instance DeriveGCompare t => DeriveGCompare (Q t) where
154+ deriveGCompare = (>>= deriveGCompare)
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)
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 =
165+ , clause [recP conName [], wildP] (normalB [| GLT |]) []
166+ , clause [wildP, recP conName []] (normalB [| GGT |]) []
167+ ] where conName = nameOfCon con
169+ needsGCompare argType con = any ((`occursInType` argType) . nameOfBinder) (boundVars ++ varsBoundInCon con)
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
177+ let conName = nameOfCon con
178+ argTypes = argTypesOfCon con
179+ nArgs = length argTypes
181+ lArgNames <- replicateM nArgs (newName "x")
182+ rArgNames <- replicateM nArgs (newName "y")
184+ clause [ conP conName (map varP lArgNames)
185+ , conP conName (map varP rArgNames)
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
195+ ++ [ noBindS [| return GEQ |] ]