module Generics.MultiRec.TH
( deriveAll,
deriveConstructors,
deriveFamily, deriveSystem,
derivePF,
deriveEl,
deriveFam,
deriveEqS
) where
import Generics.MultiRec.Base
import Language.Haskell.TH hiding (Fixity())
import Control.Applicative
import Control.Monad
deriveAll :: Name -> Q [Dec]
deriveAll n =
do
info <- reify n
let ns = map remakeName (extractConstructorNames info)
cs <- deriveConstructors ns
pf <- derivePFInstance n ns
el <- deriveEl n ns
fam <- deriveFam n ns
eq <- deriveEqS n ns
return $ cs ++ pf ++ el ++ fam ++ eq
deriveConstructors :: [Name] -> Q [Dec]
deriveConstructors =
liftM concat . mapM constrInstance
deriveFamily :: Name -> [Name] -> String -> Q [Dec]
deriveFamily n ns pfn =
do
pf <- derivePF pfn ns
el <- deriveEl n ns
fam <- deriveFam n ns
eq <- deriveEqS n (map remakeName ns)
return $ pf ++ el ++ fam ++ eq
deriveSystem :: Name -> [Name] -> String -> Q [Dec]
deriveSystem = deriveFamily
derivePF :: String -> [Name] -> Q [Dec]
derivePF pfn ns =
return <$>
tySynD (mkName pfn) [] (foldr1 sum (map (pfType ns) ns))
where
sum :: Q Type -> Q Type -> Q Type
sum a b = conT ''(:+:) `appT` a `appT` b
derivePFInstance :: Name -> [Name] -> Q [Dec]
derivePFInstance n ns =
return <$>
tySynInstD ''PF [conT n] (foldr1 sum (map (pfType ns) ns))
where
sum :: Q Type -> Q Type -> Q Type
sum a b = conT ''(:+:) `appT` a `appT` b
deriveEl :: Name -> [Name] -> Q [Dec]
deriveEl s ns =
mapM (elInstance s) ns
deriveFam :: Name -> [Name] -> Q [Dec]
deriveFam s ns =
do
fcs <- liftM concat $ zipWithM (mkFrom ns (length ns)) [0..] ns
tcs <- liftM concat $ zipWithM (mkTo ns (length ns)) [0..] ns
return <$>
instanceD (cxt []) (conT ''Fam `appT` conT s)
[funD 'from fcs, funD 'to tcs]
deriveEqS :: Name -> [Name] -> Q [Dec]
deriveEqS s ns =
return <$>
instanceD (cxt []) (conT ''EqS `appT` conT s)
[funD 'eqS (trues ++ falses)]
where
trueClause n = clause [conP n [], conP n []] (normalB (conE 'Just `appE` conE 'Refl)) []
falseClause = clause [wildP, wildP] (normalB (conE 'Nothing)) []
trues = map trueClause ns
falses = if length trues == 1 then [] else [falseClause]
extractConstructorNames :: Info -> [Name]
extractConstructorNames (TyConI (DataD _ _ _ cs _)) = concatMap extractFrom cs
where
extractFrom :: Con -> [Name]
extractFrom (ForallC _ _ c) = extractFrom c
extractFrom (InfixC _ n _) = [n]
extractFrom (RecC n _) = [n]
extractFrom (NormalC n []) = [n]
extractFrom _ = []
extractConstructorNames _ = []
stripRecordNames :: Con -> Con
stripRecordNames (RecC n f) =
NormalC n (map (\(_, s, t) -> (s, t)) f)
stripRecordNames c = c
constrInstance :: Name -> Q [Dec]
constrInstance n =
do
i <- reify n
let cs = case i of
TyConI (DataD _ _ _ cs _) -> cs
_ -> []
ds <- mapM mkData cs
is <- mapM mkInstance cs
return $ ds ++ is
mkData :: Con -> Q Dec
mkData (NormalC n _) =
dataD (cxt []) (remakeName n) [] [] []
mkData r@(RecC _ _) =
mkData (stripRecordNames r)
mkData (InfixC t1 n t2) =
mkData (NormalC n [t1,t2])
mkData (ForallC _ _ c) =
mkData c
fixity :: Fixity -> ExpQ
fixity Prefix = conE 'Prefix
fixity (Infix a n) = conE 'Infix `appE` assoc a `appE` [| n |]
assoc :: Associativity -> ExpQ
assoc LeftAssociative = conE 'LeftAssociative
assoc RightAssociative = conE 'RightAssociative
assoc NotAssociative = conE 'NotAssociative
mkInstance :: Con -> Q Dec
mkInstance (NormalC n _) =
instanceD (cxt []) (appT (conT ''Constructor) (conT $ remakeName n))
[funD 'conName [clause [wildP] (normalB (stringE (nameBase n))) []]]
mkInstance r@(RecC _ _) =
mkInstance (stripRecordNames r)
mkInstance (ForallC _ _ c) =
mkInstance c
mkInstance (InfixC t1 n t2) =
do
i <- reify n
let fi = case i of
DataConI _ _ _ f -> convertFixity f
_ -> Prefix
instanceD (cxt []) (appT (conT ''Constructor) (conT $ remakeName n))
[funD 'conName [clause [wildP] (normalB (stringE (nameBase n))) []],
funD 'conFixity [clause [wildP] (normalB (fixity fi)) []]]
where
convertFixity (Fixity n d) = Infix (convertDirection d) n
convertDirection InfixL = LeftAssociative
convertDirection InfixR = RightAssociative
convertDirection InfixN = NotAssociative
pfType :: [Name] -> Name -> Q Type
pfType ns n =
do
i <- reify n
let b = case i of
TyConI (DataD _ _ _ cs _) ->
foldr1 sum (map (pfCon ns) cs)
TyConI (TySynD t _ _) ->
conT ''K `appT` conT t
_ -> error "unknown construct"
appT (appT (conT ''(:>:)) b) (conT $ remakeName n)
where
sum :: Q Type -> Q Type -> Q Type
sum a b = conT ''(:+:) `appT` a `appT` b
pfCon :: [Name] -> Con -> Q Type
pfCon ns r@(RecC _ _) =
pfCon ns (stripRecordNames r)
pfCon ns (InfixC t1 n t2) =
pfCon ns (NormalC n [t1,t2])
pfCon ns (ForallC _ _ c) =
pfCon ns c
pfCon ns (NormalC n []) =
appT (appT (conT ''C) (conT $ remakeName n)) (conT ''U)
pfCon ns (NormalC n fs) =
appT (appT (conT ''C) (conT $ remakeName n))
(foldr1 prod (map (pfField ns . snd) fs))
where
prod :: Q Type -> Q Type -> Q Type
prod a b = conT ''(:*:) `appT` a `appT` b
pfField :: [Name] -> Type -> Q Type
pfField ns t@(ConT n)
| remakeName n `elem` ns = conT ''I `appT` return t
pfField ns t@(AppT f a) = conT ''(:.:) `appT` return f `appT` pfField ns a
pfField ns t = conT ''K `appT` return t
elInstance :: Name -> Name -> Q Dec
elInstance s n =
instanceD (cxt []) (conT ''El `appT` conT s `appT` conT n)
[mkProof n]
mkFrom :: [Name] -> Int -> Int -> Name -> Q [Q Clause]
mkFrom ns m i n =
do
let wrapE e = lrE m i (conE 'Tag `appE` e)
i <- reify n
let dn = remakeName n
let b = case i of
TyConI (DataD _ _ _ cs _) ->
zipWith (fromCon wrapE ns dn (length cs)) [0..] cs
TyConI (TySynD t _ _) ->
[clause [conP dn [], varP (field 0)] (normalB (wrapE $ conE 'K `appE` varE (field 0))) []]
_ -> error "unknown construct"
return b
mkTo :: [Name] -> Int -> Int -> Name -> Q [Q Clause]
mkTo ns m i n =
do
let wrapP p = lrP m i (conP 'Tag [p])
i <- reify n
let dn = remakeName n
let b = case i of
TyConI (DataD _ _ _ cs _) ->
zipWith (toCon wrapP ns dn (length cs)) [0..] cs
TyConI (TySynD t _ _) ->
[clause [conP dn [], wrapP $ conP 'K [varP (field 0)]] (normalB $ varE (field 0)) []]
_ -> error "unknown construct"
return b
mkProof :: Name -> Q Dec
mkProof n =
funD 'proof [clause [] (normalB (conE (remakeName n))) []]
fromCon :: (Q Exp -> Q Exp) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
fromCon wrap ns n m i (NormalC cn []) =
clause
[conP n [], conP cn []]
(normalB $ wrap $ lrE m i $ conE 'C `appE` (conE 'U)) []
fromCon wrap ns n m i (NormalC cn fs) =
clause
[conP n [], conP cn (map (varP . field) [0..length fs 1])]
(normalB $ wrap $ lrE m i $ conE 'C `appE` foldr1 prod (zipWith (fromField ns) [0..] (map snd fs))) []
where
prod x y = conE '(:*:) `appE` x `appE` y
fromCon wrap ns n m i r@(RecC _ _) =
fromCon wrap ns n m i (stripRecordNames r)
fromCon wrap ns n m i (InfixC t1 cn t2) =
fromCon wrap ns n m i (NormalC cn [t1,t2])
fromCon wrap ns n m i (ForallC _ _ c) =
fromCon wrap ns n m i c
toCon :: (Q Pat -> Q Pat) -> [Name] -> Name -> Int -> Int -> Con -> Q Clause
toCon wrap ns n m i (NormalC cn []) =
clause
[conP n [], wrap $ lrP m i $ conP 'C [conP 'U []]]
(normalB $ conE cn) []
toCon wrap ns n m i (NormalC cn fs) =
clause
[conP n [], wrap $ lrP m i $ conP 'C [foldr1 prod (map (varP . field) [0..length fs 1])]]
(normalB $ foldl appE (conE cn) (zipWith (toField ns) [0..] (map snd fs))) []
where
prod x y = conP '(:*:) [x,y]
toCon wrap ns n m i r@(RecC _ _) =
toCon wrap ns n m i (stripRecordNames r)
toCon wrap ns n m i (InfixC t1 cn t2) =
toCon wrap ns n m i (NormalC cn [t1,t2])
toCon wrap ns n m i (ForallC _ _ c) =
toCon wrap ns n m i c
fromField :: [Name] -> Int -> Type -> Q Exp
fromField ns nr t = [| $(fromFieldFun ns t) $(varE (field nr)) |]
fromFieldFun :: [Name] -> Type -> Q Exp
fromFieldFun ns t@(ConT n)
| remakeName n `elem` ns = [| I . I0 |]
fromFieldFun ns t@(AppT f a) = [| D . fmap $(fromFieldFun ns a) |]
fromFieldFun ns t = [| K |]
toField :: [Name] -> Int -> Type -> Q Exp
toField ns nr t = [| $(toFieldFun ns t) $(varE (field nr)) |]
toFieldFun :: [Name] -> Type -> Q Exp
toFieldFun ns t@(ConT n)
| remakeName n `elem` ns = [| unI0 . unI |]
toFieldFun ns t@(AppT f a) = [| fmap $(toFieldFun ns a) . unD |]
toFieldFun ns t = [| unK |]
field :: Int -> Name
field n = mkName $ "f" ++ show n
lrP :: Int -> Int -> (Q Pat -> Q Pat)
lrP 1 0 p = p
lrP m 0 p = conP 'L [p]
lrP m i p = conP 'R [lrP (m1) (i1) p]
lrE :: Int -> Int -> (Q Exp -> Q Exp)
lrE 1 0 e = e
lrE m 0 e = conE 'L `appE` e
lrE m i e = conE 'R `appE` lrE (m1) (i1) e
remakeName :: Name -> Name
remakeName n = mkName (nameBase n)