diff --git a/Generics/RepLib.hs b/Generics/RepLib.hs --- a/Generics/RepLib.hs +++ b/Generics/RepLib.hs @@ -35,7 +35,9 @@ -- ** Library of generic operations module Generics.RepLib.Lib, -- ** Derivable type classes written as generic operations - module Generics.RepLib.PreludeLib + module Generics.RepLib.PreludeLib, + + (:=:)(..), EqT(..) ) where @@ -48,5 +50,6 @@ import Generics.RepLib.SYB.Schemes import Generics.RepLib.Lib import Generics.RepLib.PreludeLib +import Data.Type.Equality ----------------------------------------------------------------------------- diff --git a/Generics/RepLib/Derive.hs b/Generics/RepLib/Derive.hs --- a/Generics/RepLib/Derive.hs +++ b/Generics/RepLib/Derive.hs @@ -1,10 +1,15 @@ --- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -ddump-splices -- - -{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} +{-# LANGUAGE TemplateHaskell + , UndecidableInstances + , TypeOperators + , ScopedTypeVariables + , GADTs + , GeneralizedNewtypeDeriving + #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} ----------------------------------------------------------------------------- -- | --- Module : Derive +-- Module : Generics.RepLib.Derive -- License : TBD -- -- Maintainer : sweirich@cis.upenn.edu @@ -27,44 +32,24 @@ import Generics.RepLib.R import Generics.RepLib.R1 -import Language.Haskell.TH -import Data.List (nub) -import Data.Tuple - - --- | Given a type, produce its representation. +import Language.Haskell.TH hiding (Con) +import qualified Language.Haskell.TH as TH (Con) +import Language.Haskell.TH.Syntax (Quasi(..)) +import Data.List (foldl', nub) +import qualified Data.Set as S +import Data.Maybe (catMaybes) +import Data.Type.Equality --- Note, that the representation of a type variable "a" is (rep :: R a) so Rep a must be --- in the context -repty :: Type -> Q Exp -repty (ForallT _ _ _) = error "cannot rep" -repty (VarT n) = return (SigE (VarE (mkName "rep")) ((ConT ''R) `AppT` (VarT n))) -repty (AppT t1 t2) = (repty t1) -- `AppE` (repty t2) -repty (ConT n) = do - info <- reify n - case info of - TyConI (TySynD n' vars t) -> repty t - _ -> - return $ - case nameBase n of - "Int" -> (ConE 'Int) - "Char" -> (ConE 'Char) - "Float" -> (ConE 'Float) - "Double" -> (ConE 'Double) - "Rational"-> (ConE 'Rational) - "Integer" -> (ConE 'Integer) - "IOError" -> (ConE 'IOError) - "IO" -> (ConE 'IO) - "[]" -> (VarE 'rList) --- don't know why this isn't ListT - "String" -> (VarE 'rList) - c -> (VarE (rName n)) -repty (TupleT i) - | i <= 7 = return $ VarE (mkName $ "rTup" ++ show i) - | otherwise = error $ "Why on earth are you using " ++ (show i) ++ "-tuples??" +import Control.Monad (replicateM, zipWithM, liftM, liftM2, when) +import Control.Monad.Writer (WriterT, MonadWriter(..), runWriterT, lift) +import Control.Arrow ((***), second) +import Control.Applicative ((<$>)) -repty (ArrowT) = return (ConE 'Arrow) -repty (ListT) = return (VarE 'rList) +import Unsafe.Coerce +-- | Given a type, produce its representation. +repty :: Type -> Exp +repty ty = SigE (VarE (mkName "rep")) ((ConT ''R) `AppT` ty) rName :: Name -> Name rName n = @@ -88,67 +73,154 @@ "(,)" -> mkName ("rTup2_1") c -> mkName ("r" ++ c ++ "1") -------------------------------------------------------------------------------------------------------- --- represent a data constructor. +---------------------------------------------------------------------------------- + +-- Q-like monad which also remembers a Set of Int values. We use this +-- to keep track of which Res/destr definitions we end up needing +-- while generating constructor representations. + +newtype QN a = QN { unQN :: WriterT (S.Set Int) Q a } + deriving (Functor, Monad, MonadWriter (S.Set Int)) + +liftQN :: Q a -> QN a +liftQN = QN . lift + +runQN :: QN a -> Q (a, S.Set Int) +runQN = runWriterT . unQN + +instance Quasi QN where + qNewName s = liftQN $ qNewName s + qReport b s = liftQN $ qReport b s + qRecover = error "qRecover not implemented for QN" + qReify n = liftQN $ qReify n + qClassInstances n tys = liftQN $ qClassInstances n tys + qLocation = liftQN qLocation + qRunIO io = liftQN $ qRunIO io + +-- Generate the representation for a data constructor. -- As our representation of data constructors evolves, so must this definition. --- Currently, we don't handle data constructors with record components +-- Currently, we don't handle data constructors with record components. -repcon :: Bool -> -- Is this the ONLY constructor for the datatype - Type -> -- The type that this is a constructor for (applied to all of its parameters) - (Name, [(Maybe Name, Type)]) -> -- data constructor name * list of [record name * type] - Q Exp -repcon single d (name, sttys) = - let rargs = foldr (\ (_,t) tl -> - [| $(repty t) :+: $(tl) |]) [| MNil |] sttys in - [| Con $(remb single d (name,sttys)) $(rargs) |] +-- | Generate an R-type constructor representation. +repcon :: TypeInfo -> -- information about the type + ConstrInfo -> -- information about the constructor + QN Exp +repcon info constr + | null (constrCxt constr) = liftQN [| Just $con |] + | otherwise = gadtCase (typeParams info) constr con + where args = map (return . repty . fieldType) . constrFields $ constr + mtup = foldr (\ t tl -> [| $(t) :+: $(tl) |]) [| MNil |] args + con = [| Con $(remb constr) $(mtup) |] +gadtCase :: [TyVarBndr] -> ConstrInfo -> Q Exp -> QN Exp +gadtCase tyVars constr conQ = do + con <- liftQN [| Just $conQ |] + (m, pat) <- typeRefinements tyVars constr + n <- liftQN [| Nothing |] + return $ CaseE m + [ Match pat (NormalB con) [] + , Match WildP (NormalB n) [] + ] + +typeRefinements :: [TyVarBndr] -> ConstrInfo -> QN (Exp, Pat) +typeRefinements tyVars constr = + fmap ((TupE *** TupP) . unzip) + . sequence + . map genRefinement + . extractParamEqualities tyVars + $ constrCxt constr + +extractParamEqualities :: [TyVarBndr] -> Cxt -> [(Name, Type)] +extractParamEqualities tyVars = filterWith extractLHSVars + . filterWith extractEq + where extractEq :: Pred -> Maybe (Type, Type) + extractEq (EqualP ty1 ty2) = Just (ty1, ty2) + extractEq _ = Nothing + + extractLHSVars (VarT n, t2) | any ((==n) . tyVarBndrName) tyVars = Just (n,t2) + extractLHSVars _ = Nothing + -- Note, assuming here that equalities involving type parameters + -- will always have the type parameter on the LHS... + + filterWith :: (a -> Maybe b) -> [a] -> [b] + filterWith f = catMaybes . map f + +-- The third result is the arity of the type constructor, hence the N +-- of the required ResN/destrN declarations. +genRefinement :: (Name, Type) -> QN (Exp, Pat) +genRefinement (n, ty) = do + let (con, args) = decomposeTy ty + when (not (null args)) $ tell $ S.singleton (length args) + liftQN $ case args of + [] -> do e <- [| eqT (rep :: R $(varT n)) $(return $ repty ty) |] + p <- [p| Just Refl |] + return (e,p) + _ -> do e <- [| $(varE (mkName $ "destr" ++ show (length args))) + (rep :: R $(varT n)) + (rep :: R $(appUnits con (length args))) + |] + p <- conP (mkName $ "Result" ++ show (length args)) + [sigP [p| Refl |] [t| $(varT n) :=: $(return ty) |] ] + return (e,p) + +-- | Decompose a type into a constructor and a list of arguments. +decomposeTy :: Type -> (Type, [Type]) +decomposeTy (AppT t1 t2) = second (++[t2]) (decomposeTy t1) +decomposeTy t = (t, []) + +-- | Apply a type constructor to a certain number of copies of the +-- unit type. +appUnits :: Type -> Int -> Q Type +appUnits ty n = do + u <- [t| () |] + return $ foldl' AppT ty (replicate n u) + -- the "from" function that coerces from an "a" to the arguments -rfrom :: Bool -> -- does this datatype have only a single constructor - Type -> -- the datatype itself - (Name, [(Maybe Name, Type)]) -> -- data constructor name, list of parameters with record names - Q Exp -rfrom single d (name, sttys) = do - vars <- mapM (\_ -> newName "x") sttys - outvar <- newName "y" - let outpat :: Pat - outpat = ConP name (map VarP vars) - outbod :: Exp - outbod = foldr (\v tl -> (ConE (mkName (":*:"))) `AppE` (VarE v) `AppE` tl) - (ConE 'Nil) vars - success = Match outpat (NormalB ((ConE 'Just) `AppE` outbod)) [] - outcase x = if single then - CaseE x [success] - else - CaseE x - [success, Match WildP (NormalB (ConE 'Nothing)) [] ] - return (LamE [VarP outvar] (outcase (VarE outvar))) +rfrom :: ConstrInfo -> Q Exp +rfrom constr = do + vars <- mapM (const (newName "x")) (constrFields constr) + outvar <- newName "y" + let nm = (simpleName . constrName $ constr) + let outpat :: Pat + outpat = ConP nm (map VarP vars) + outbod :: Exp + outbod = foldr (\v tl -> (ConE (mkName (":*:"))) `AppE` (VarE v) `AppE` tl) + (ConE 'Nil) vars + success = Match outpat (NormalB ((ConE 'Just) `AppE` outbod)) [] + outcase x = if isOnlyConstr constr + then CaseE x [success] + else CaseE x + [success, Match WildP (NormalB (ConE 'Nothing)) [] ] + return (LamE [VarP outvar] (outcase (VarE outvar))) -- to component of th embedding -rto :: Type -> (Name, [(Maybe Name, Type)]) -> Q Exp -rto d (name,sttys) = - do vars <- mapM (\_ -> newName "x") sttys +rto :: ConstrInfo -> Q Exp +rto constr = + do vars <- mapM (const (newName "x")) (constrFields constr) let topat = foldr (\v tl -> InfixP (VarP v) (mkName ":*:") tl) (ConP 'Nil []) vars - tobod = foldl (\tl v -> tl `AppE` (VarE v)) (ConE name) vars + tobod = foldl' (\tl v -> tl `AppE` (VarE v)) + (ConE (simpleName . constrName $ constr)) + vars return (LamE [topat] tobod) -- the embedding record -remb :: Bool -> Type -> (Name, [(Maybe Name, Type)]) -> Q Exp -remb single d (name, sttys) = - [| Emb { name = $(stringName name), - to = $(rto d (name,sttys)), - from = $(rfrom single d (name,sttys)), +remb :: ConstrInfo -> Q Exp +remb constr = + [| Emb { name = $(stringName . simpleName . constrName $ constr), + to = $(rto constr), + from = $(rfrom constr), labels = Nothing, fixity = Nonfix } |] repDT :: Name -> [Name] -> Q Exp -repDT name param = - do str <- stringName name +repDT nm param = + do str <- stringName nm let reps = foldr (\p f -> - (ConE (mkName ":+:")) `AppE` - (SigE (VarE (mkName "rep")) - ((ConT ''R) `AppT` (VarT p))) `AppE` f) - (ConE 'MNil) param + (ConE (mkName ":+:")) `AppE` + repty (VarT p) `AppE` + f) + (ConE 'MNil) param [| DT $(return str) $(return reps) |] data Flag = Abs | Conc @@ -159,17 +231,24 @@ repr f n = do info' <- reify n case info' of TyConI d -> do - (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) - let paramNames = map tyVarBndrName param - baseT <- conT name + let dInfo = typeInfo d + paramNames = map tyVarBndrName (typeParams dInfo) + nm = typeName dInfo + constrs = typeConstrs dInfo + baseT <- conT nm -- the type that we are defining, applied to its parameters. - let ty = foldl (\x p -> x `AppT` (VarT p)) baseT paramNames + let ty = foldl' (\x p -> x `AppT` (VarT p)) baseT paramNames -- the representations of the paramters, as a list -- representations of the data constructors - rcons <- mapM (repcon (length terms == 1) ty) terms + (rcons, ks) <- runQN $ mapM (repcon dInfo) constrs + + ress <- case f of + Conc -> deriveRess ks + Abs -> return [] body <- case f of - Conc -> [| Data $(repDT name paramNames) $(return (ListE rcons)) |] - Abs -> [| Abstract $(repDT name paramNames) |] + Conc -> [| Data $(repDT nm paramNames) + (catMaybes $(return (ListE rcons))) |] + Abs -> [| Abstract $(repDT nm paramNames) |] let ctx = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames let rTypeName :: Name rTypeName = rName n @@ -181,115 +260,228 @@ rType = ValD (VarP rTypeName) (NormalB body) [] let inst = InstanceD ctx ((ConT (mkName "Rep")) `AppT` ty) [ValD (VarP (mkName "rep")) (NormalB (VarE rTypeName)) []] - return [rSig, rType, inst] + return $ ress ++ [rSig, rType, inst] + reprs :: Flag -> [Name] -> Q [Dec] -reprs f ns = foldl (\qd n -> do decs1 <- repr f n - decs2 <- qd - return (decs1 ++ decs2)) (return []) ns +reprs f ns = concat <$> mapM (repr f) ns -------------------------------------------------------------------------------------------- --- Generating the R1 representation --- The difficult part of repr1 is that we need to paramerize over recs for types that --- appear in the constructors, as well as the reps of parameters. +-- The difficult part of repr1 is that we need to paramerize over reps for types that +-- appear as arguments of constructors, as well as the reps of parameters. -ctx_params :: Type -> -- type we are defining - Name -> -- name of the type variable "ctx" - [(Name, [(Maybe Name, Type)])] -> -- list of constructor names - -- and the types of their arguments (plus record labels) - Q [(Name, Type, Type)] - -- name of termvariable "pt" - -- (ctx t) - -- t -ctx_params ty ctxName l = do - let tys = nub (map snd (foldr (++) [] (map snd l))) - mapM (\t -> do n <- newName "p" - let ctx_t = (VarT ctxName) `AppT` t - return (n, ctx_t, t)) tys +-- The constructor for the R1 representation takes one argument +-- corresponding to each constructor, providing contexts for the +-- arguments to that constructor. Some of them are just (tuples of) +-- applications of ctx to some type. However, for GADT constructors, +-- the argument is a polymorphic function which takes an equality +-- proof (in order to refine one or more type parameters) and then +-- returns some contexts. For example, for +-- +-- data Foo a where +-- Bar :: Int -> Foo Int +-- Bar2 :: Foo b -> Foo [b] +-- Bar3 :: Foo c -> Foo d -> Foo (c,d) +-- +-- we have +-- +-- rFoo1 :: +-- forall ctx a. Rep a => +-- ctx Int -> +-- (forall b. a :=: [b] -> ctx (Foo b)) -> +-- (forall c d. a :=: (c,d) -> (ctx (Foo c), ctx (Foo d))) -> +-- R1 ctx (Foo a) -lookupName :: Type -> [(Name, Type, Type)] -> [(Name, Type, Type)] -> Name -lookupName t l ((n, t1, t2):rest) = if t == t2 then n else lookupName t l rest -lookupName t l [] = error ("lookupName: Cannot find type " ++ show t ++ " in " ++ show l) +data CtxParam = CtxParam { cpName :: Name -- The argument name + , cpType :: Type -- The argument type + , cpEqs :: [(Name, Type)] -- Required equality proofs + , cpTyVars :: [Name] -- /All/ type variable arguments to the type + -- (not just ones requiring equality proofs); + -- needed when generating special Sat classes + , cpPayload :: Type -- What you get after supplying + -- the proofs + , cpPayloadElts :: [Type] -- individual elements in + -- the payload + , cpCtxName :: Name + , cpSat :: Maybe (Name, Name) + -- names of the special Sat-like class and + -- its dictionary method for this + -- constructor + } -repcon1 :: Type -- result type of the constructor - -> Bool - -> Exp -- recursive call (rList1 ra pa) - -> [(Name,Type,Type)] -- ctxParams - -> (Name, [(Maybe Name, Type)]) -- name of data constructor + args - -> Q Exp -repcon1 d single rd1 ctxParams (name, sttys) = - let rec = foldr (\ (_,t) tl -> - let expQ = (VarE (lookupName t ctxParams ctxParams)) - in [| $(return expQ) :+: $(tl) |]) [| MNil |] sttys in - [| Con $(remb single d (name,sttys)) $(rec) |] +-- | Generate the context parameters (see above) for a given type. +ctx_params :: TypeInfo -> -- information about the type we are defining + Name -> -- name of the type variable "ctx" + [ConstrInfo] -> -- information about the type's constructors + Q [CtxParam] +ctx_params tyInfo ctxName constrs = mapM (genCtxParam ctxName tyInfo) constrs --- Generate a parameterized representation of a type -repr1 :: Flag -> Name -> Q [Dec] -repr1 f n = do info' <- reify n - case info' of - TyConI d -> do - (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) - let paramNames = map tyVarBndrName param - -- the type that we are defining, applied to its parameters. - let ty = foldl (\x p -> x `AppT` (VarT p)) (ConT name) paramNames - let rTypeName = rName1 n +-- | Generate a context parameter for a single constructor. +genCtxParam :: Name -> TypeInfo -> ConstrInfo -> Q CtxParam +genCtxParam ctxName tyInfo constr + = newName "c" >>= \c -> return (CtxParam c pType eqs tvars payload payloadElts ctxName Nothing) + where allEqs = extractParamEqualities (typeParams tyInfo) (constrCxt constr) + eqs = filter (not . S.null . tyFV . snd) allEqs + tvars = map tyVarBndrName . typeParams $ tyInfo + pType | null eqs = payload + | otherwise = guarded + payloadElts = map ((VarT ctxName `AppT`) . fieldType) . constrFields $ constr + payload = mkTupleT payloadElts + guarded = ForallT vars [] (foldr (AppT . AppT ArrowT) payload proofs) + vars = map PlainTV $ concatMap (S.toList . tyFV . snd) eqs + proofs = map mkProof eqs + mkProof (n, ty) = AppT (AppT (ConT (mkName ":=:")) (VarT n)) ty - ctx <- newName "ctx" - ctxParams <- case f of - Conc -> ctx_params ty ctx terms - Abs -> return [] +mkTupleT :: [Type] -> Type +mkTupleT tys = foldl' AppT (TupleT (length tys)) tys - -- parameters to the rep function - -- let rparams = map (\p -> SigP (VarP p) ((ConT ''R) `AppT` (VarT p))) param - let cparams = map (\(n,t,_) -> SigP (VarP n) t) ctxParams +-- | Compute the free type variables of a type. +tyFV :: Type -> S.Set Name +tyFV (ForallT vs _ ty) = tyFV ty `S.difference` (S.fromList . map tyVarBndrName $ vs) +tyFV (VarT n) = S.singleton n +tyFV (ConT _) = S.empty +tyFV (TupleT _) = S.empty +tyFV ArrowT = S.empty +tyFV ListT = S.empty +tyFV (AppT ty1 ty2) = tyFV ty1 `S.union` tyFV ty2 +tyFV (SigT ty _) = tyFV ty - -- the recursive call of the rep function - let e1 = foldl (\a r -> a `AppE` (VarE r)) (VarE rTypeName) paramNames - let e2 = foldl (\a (n,_,_) -> a `AppE` (VarE n)) e1 ctxParams +repcon1 :: TypeInfo -- information about the type + -> CtxParam -- corresponding context parameter + -> ConstrInfo -- info about the constructor + -> Q Exp +repcon1 info ctxParam constr = do + cs <- replicateM (length . constrFields $ constr) (newName "c") + let conBody = caseE (applyPfs ctxParam) + [ match (tupP . map varP $ cs) (normalB con) [] ] + args = map varE cs + mtup = foldr (\ t tl -> [| $(t) :+: $(tl) |]) [| MNil |] args + con = [| Con $(remb constr) $(mtup) |] + case (null (constrCxt constr)) of + True -> [| Just $conBody |] + _ -> fst <$> (runQN $ gadtCase (typeParams info) constr conBody) - -- the representations of the parameters, as a list - -- representations of the data constructors - rcons <- mapM (repcon1 ty (length terms == 1) e2 ctxParams) terms - body <- case f of - Conc -> [| Data1 $(repDT name paramNames) - $(return (ListE rcons)) |] - Abs -> [| Abstract1 $(repDT name paramNames) |] +-- | Apply a context parameter to the right number of equality proofs +-- to get out the promised context. +applyPfs :: CtxParam -> Q Exp +applyPfs (CtxParam { cpName = n, cpEqs = eqs }) = + appsE (varE n : replicate (length eqs) [| Refl |]) - let rhs = LamE (cparams) body -{- rhs_type = ForallT (ctx:param) rparams - (foldr (\ (p,t) ret -> `ArrowT` `AppT` t `AppT` ret) ty params) -} - rTypeDecl = ValD (VarP rTypeName) (NormalB rhs) [] +genSatClass :: CtxParam -> Q (CtxParam, [Dec]) +genSatClass ctxParam | null (cpEqs ctxParam) = return (ctxParam, []) + | otherwise = do + satNm <- newName "Sat" + dictNm <- newName "dict" + let ctx = cpCtxName ctxParam + eqs = cpEqs ctxParam + tvs = cpTyVars ctxParam + satClass = ClassD [] satNm (PlainTV ctx : map PlainTV tvs) [] + [SigD dictNm (cpType ctxParam)] - let ctxRep = map (\p -> ClassP (mkName "Rep") [VarT p]) paramNames - ctxRec = map (\(_,t,_) -> ClassP ''Sat [t]) ctxParams + satInstHead = foldl' AppT (ConT satNm) (VarT ctx : map tvOrEqType tvs) + tvOrEqType a = case lookup a eqs of + Just t -> t + Nothing -> VarT a - -- appRep t = foldl (\a p -> a `AppE` (VarE 'rep)) t param - appRec t = foldl (\a p -> a `AppE` (VarE 'dict)) t ctxParams + satInst = InstanceD + (map (ClassP ''Sat . (:[])) (cpPayloadElts ctxParam)) + satInstHead + [ValD (VarP dictNm) + (NormalB (LamE (replicate (length eqs) (ConP 'Refl [])) + (TupE (replicate (length (cpPayloadElts ctxParam)) + (VarE 'dict) + ) + ) + ) + ) + [] + ] - let inst = InstanceD (ctxRep ++ ctxRec) - ((ConT ''Rep1) `AppT` (VarT ctx) `AppT` ty) - [ValD (VarP (mkName "rep1")) - (NormalB (appRec (VarE rTypeName))) []] + nms <- replicateM (length tvs) (newName "a") + err <- [| error "Impossible Sat instance!" |] - let rSig = SigD rTypeName (ForallT (map PlainTV (ctx : paramNames)) ctxRep - (foldr (\(_,p,_) f -> (ArrowT `AppT` p `AppT` f)) - ((ConT (mkName "R1")) `AppT` (VarT ctx) `AppT` ty) - ctxParams)) - decs <- repr f n - return (decs ++ [rSig, rTypeDecl, inst]) + let defSatInst = InstanceD [] (foldl' AppT (ConT satNm) (map VarT (ctx : nms))) + [ValD (VarP dictNm) + (NormalB (LamE (replicate (length eqs) (ConP 'Refl [])) err)) + [] + ] + return (ctxParam { cpSat = Just (satNm, dictNm) }, [satClass, satInst, defSatInst]) -repr1s :: Flag -> [Name] -> Q [Dec] +genSatClasses :: [CtxParam] -> Q ([CtxParam], [Dec]) +genSatClasses ps = (second concat . unzip) <$> mapM genSatClass ps +-- XXX look at Basics.hs -- tree example. The context for recursive +-- subtrees ends up getting duplicated. Need to nub out something so +-- that doesn't happen. -repr1s f ns = foldl (\qd n -> do decs1 <- repr1 f n - decs2 <- qd - return (decs1 ++ decs2)) (return []) ns +-- Generate a parameterized representation of a type +repr1 :: Flag -> Name -> Q [Dec] +repr1 f n = do + info' <- reify n + case info' of + TyConI d -> do + let dInfo = typeInfo d + paramNames = map tyVarBndrName (typeParams dInfo) + nm = typeName dInfo + constrs = typeConstrs dInfo + -- the type that we are defining, applied to its parameters. + let ty = foldl' (\x p -> x `AppT` (VarT p)) (ConT nm) paramNames + let rTypeName = rName1 n + ctx <- newName "ctx" + ctxParams <- case f of + Conc -> ctx_params dInfo ctx constrs + Abs -> return [] + + r1Ty <- [t| $(conT $ ''R1) $(varT ctx) $(return ty) |] + let ctxRep = map (\p -> ClassP (''Rep) [VarT p]) paramNames + rSig = SigD rTypeName + (ForallT + (map PlainTV (ctx : paramNames)) + ctxRep + (foldr (AppT . AppT ArrowT) r1Ty (map cpType ctxParams)) + ) + + rcons <- zipWithM (repcon1 dInfo) ctxParams constrs + body <- case f of + Conc -> [| Data1 $(repDT nm paramNames) + (catMaybes $(return (ListE rcons))) |] + Abs -> [| Abstract1 $(repDT nm paramNames) |] + + let rhs = LamE (map (VarP . cpName) ctxParams) body + + rDecl = ValD (VarP rTypeName) (NormalB rhs) [] + + -- generate a Sat-like class for each constructor requiring + -- equality proofs + (ctxParams', satClasses) <- genSatClasses ctxParams + let mkCtxRec c = case cpSat c of + Nothing -> map (ClassP ''Sat . (:[])) (cpPayloadElts c) + Just (s,_) -> [ClassP s (map VarT (cpCtxName c : paramNames))] + ctxRec = nub $ concatMap mkCtxRec ctxParams' + mkDictArg c = case cpSat c of + Just (_,dn) -> VarE dn + Nothing -> TupE (replicate (length (cpPayloadElts c)) (VarE 'dict)) + dicts = map mkDictArg ctxParams' + + inst <- instanceD (return $ ctxRep ++ ctxRec) + (conT ''Rep1 `appT` varT ctx `appT` (return ty)) + [valD (varP 'rep1) (normalB (appsE (varE rTypeName + : map return dicts))) []] + + -- generate the Rep instances as well + decs <- repr f n + return (decs ++ [rSig, rDecl] ++ satClasses ++ [inst]) + +repr1s :: Flag -> [Name] -> Q [Dec] +repr1s f ns = concat <$> mapM (repr1 f) ns + -- | Generate representations (both basic and parameterized) for a list of --- types. +-- types. derive :: [Name] -> Q [Dec] derive = repr1s Conc @@ -306,41 +498,74 @@ stringName :: Name -> Q Exp stringName n = return (LitE (StringL (nameBase n))) ---- from SYB III code.... +data TypeInfo = TypeInfo { typeName :: Name + , typeParams :: [TyVarBndr] + , typeConstrs :: [ConstrInfo] + } -typeInfo :: DecQ -> Q (Name, [TyVarBndr], [(Name, Int)], [(Name, [(Maybe Name, Type)])]) -typeInfo m = - do d <- m - case d of - d@(DataD _ _ _ _ _) -> - return $ (name d, paramsA d, consA d, termsA d) - d@(NewtypeD _ _ _ _ _) -> - return $ (name d, paramsA d, consA d, termsA d) - _ -> error ("derive: not a data type declaration: " ++ show d) +data ConstrInfo = ConstrInfo { constrName :: Name -- careful, this is NOT + -- simplified; may need to + -- call simpleName first + , constrBinders :: [TyVarBndr] + , constrCxt :: Cxt + , constrFields :: [FieldInfo] + , isOnlyConstr :: Bool -- is this the only + -- constructor of its type? + } - where - consA (DataD _ _ _ cs _) = map conA cs - consA (NewtypeD _ _ _ c _) = [ conA c ] +mkConstr :: Name -> ConstrInfo +mkConstr nm = ConstrInfo nm [] [] [] False - paramsA (DataD _ _ ps _ _) = ps - paramsA (NewtypeD _ _ ps _ _) = ps +data FieldInfo = FieldInfo { fieldName :: Maybe Name + , fieldType :: Type + } - termsA (DataD _ _ _ cs _) = map termA cs - termsA (NewtypeD _ _ _ c _) = [ termA c ] +typeInfo :: Dec -> TypeInfo +typeInfo d = case d of + (DataD _ _ _ _ _) -> + TypeInfo (getName d) (paramsA d) (consA d) + (NewtypeD _ _ _ _ _) -> + TypeInfo (getName d) (paramsA d) (consA d) + _ -> error ("derive: not a data type declaration: " ++ show d) - termA (NormalC c xs) = (c, map (\x -> (Nothing, snd x)) xs) - termA (RecC c xs) = (c, map (\(n, _, t) -> (Just $ simpleName n, t)) xs) - termA (InfixC t1 c t2) = (c, [(Nothing, snd t1), (Nothing, snd t2)]) - termA (ForallC _ _ n) = termA n + where + getName (DataD _ n _ _ _) = n + getName (NewtypeD _ n _ _ _) = n + getName x = error $ "Impossible! " ++ show x ++ " is neither data nor newtype" - conA (NormalC c xs) = (simpleName c, length xs) - conA (RecC c xs) = (simpleName c, length xs) - conA (InfixC _ c _) = (simpleName c, 2) + paramsA (DataD _ _ ps _ _) = ps + paramsA (NewtypeD _ _ ps _ _) = ps - name (DataD _ n _ _ _) = n - name (NewtypeD _ n _ _ _) = n - name d = error $ show d + consA (DataD _ _ _ cs _) = rememberOnly $ map conA cs + consA (NewtypeD _ _ _ c _) = rememberOnly $ [ conA c ] + conA (NormalC c xs) = (mkConstr c) + { constrFields = map normalField xs } + + conA (RecC c xs) = (mkConstr c) + { constrFields = map recField xs } + + conA (InfixC t1 c t2) = (mkConstr c) + { constrFields = map normalField [t1, t2] } + + conA (ForallC bdrs cx con) = let c' = conA con + in c' { constrBinders = bdrs ++ constrBinders c' + , constrCxt = cx ++ constrCxt c' + } + + normalField x = FieldInfo + { fieldName = Nothing + , fieldType = snd x + } + recField (n, _, t) = FieldInfo + { fieldName = Just $ simpleName n + , fieldType = t + } + +rememberOnly :: [ConstrInfo] -> [ConstrInfo] +rememberOnly [con] = [con { isOnlyConstr = True }] +rememberOnly cons = cons + simpleName :: Name -> Name simpleName nm = let s = nameBase nm @@ -349,7 +574,142 @@ _:[] -> mkName s _:t -> mkName t - tyVarBndrName :: TyVarBndr -> Name tyVarBndrName (PlainTV n) = n tyVarBndrName (KindedTV n _) = n + + +---------------------------------------------------------------- +-- Generating ResN types with associated destructor functions +---------------------------------------------------------------- + +{- Derive declarations of the form + +data Res2 c2 a where + Result2 :: (Rep d, Rep e) => a :=: (c2 d e) -> Res2 c2 a + NoResult2 :: Res2 c2 a + +destr2 :: R a -> R (c2 d e) -> Res2 c2 a +destr2 (Data (DT s1 ((rd :: R d) :+: (re :: R e) :+: MNil)) _) + (Data (DT s2 _) _) + | s1 == s2 = Result2 (unsafeCoerce Refl :: a :=: (c2 d e)) + | otherwise = NoResult2 +destr2 _ _ = NoResult2 + + for taking apart applications of type constructors of arity n. +-} + +deriveRess :: S.Set Int -> Q [Dec] +deriveRess = S.fold (liftM2 (++) . deriveResMaybe) (return []) + +deriveResMaybe :: Int -> Q [Dec] +deriveResMaybe n = recover + (deriveRes n) + (reify (mkName $ "Res" ++ show n) >> return []) + +deriveRes :: Int -> Q [Dec] +deriveRes n | n < 0 = error "deriveRes should only be called with positive arguments" +deriveRes n = do + c <- newName "c" + a <- newName "a" + bs <- replicateM n (newName "b") + liftM (deriveResData n c a bs:) (deriveResDestr n c a bs) + +deriveResData :: Int -> Name -> Name -> [Name] -> Dec +deriveResData n c a bs = + DataD [] (mkName $ "Res" ++ show n) (map PlainTV [c,a]) + [deriveResultCon n c a bs, deriveNoResultCon n] [] + +deriveResultCon :: Int -> Name -> Name -> [Name] -> TH.Con +deriveResultCon n c a bs = + ForallC + (map PlainTV bs) + (map (ClassP ''Rep . (:[]) . VarT) bs) + (NormalC (mkName $ "Result" ++ show n) + [(NotStrict, deriveResultEq c a bs)] + ) + +deriveResultEq :: Name -- Tyvar representing the type to be deconstructed + -> Name -- Constructor tyvar + -> [Name] -- Argument tyvars + -> Type +deriveResultEq c a bs = AppT (AppT (ConT (mkName ":=:")) (VarT a)) + (appsT (VarT c) bs) + +deriveNoResultCon :: Int -> TH.Con +deriveNoResultCon n = NormalC (mkName $ "NoResult" ++ show n) [] + +deriveResDestr :: Int -> Name -> Name -> [Name] -> Q [Dec] +deriveResDestr n c a bs = do + let sig = deriveResDestrSig n c a bs + decl <- deriveResDestrDecl n c a (length bs) + return [sig, decl] + +deriveResDestrSig :: Int -> Name -> Name -> [Name] -> Dec +deriveResDestrSig n c a bs = + SigD (mkName $ "destr" ++ show n) + (ForallT (map PlainTV $ [c,a] ++ bs) [] + ( (AppT (ConT ''R) (VarT a)) `arr` + (AppT (ConT ''R) (appsT (VarT c) bs)) `arr` + (AppT (AppT (ConT (mkName $ "Res" ++ show n)) (VarT c)) (VarT a)) + ) + ) + +deriveResDestrDecl :: Int -> Name -> Name -> Int -> Q Dec +deriveResDestrDecl n c a bNum = do + [s1, s2] <- replicateM 2 (newName "s") + bs <- replicateM bNum (newName "b") + return $ + FunD + (mkName $ "destr" ++ show n) + [ Clause + [ deriveResDestrLPat s1 bs + , deriveResDestrRPat s2 + ] + (GuardedB + [ ( NormalG (AppE (AppE (VarE '(==)) (VarE s1)) (VarE s2)) + , AppE (ConE (mkName $ "Result" ++ show n)) + (SigE (AppE (VarE 'unsafeCoerce) (ConE 'Refl)) + (deriveResultEq c a bs) + ) + ) + , ( NormalG (VarE 'otherwise) + , ConE (mkName $ "NoResult" ++ show n) + ) + ] + ) + [] + , Clause + [ WildP, WildP ] + (NormalB (ConE (mkName $ "NoResult" ++ show n))) + [] + ] + +-- (Data (DT s1 ((_ :: R b1') :+: (_ :: R b2') :+: MNil)) _) +deriveResDestrLPat :: Name -> [Name] -> Pat +deriveResDestrLPat s1 bs = + ConP 'Data + [ ConP 'DT + [ VarP s1 + , foldr (\p l -> InfixP p '(:+:) l) (ConP 'MNil []) + (map (SigP WildP . AppT (ConT ''R) . VarT) bs) + ] + , WildP + ] + +-- (Data (DT s2 _) _) +deriveResDestrRPat :: Name -> Pat +deriveResDestrRPat s2 = + ConP 'Data + [ ConP 'DT [ VarP s2, WildP ] + , WildP + ] + +infixr 5 `arr` +arr :: Type -> Type -> Type +arr t1 t2 = AppT (AppT ArrowT t1) t2 + +appsT :: Type -> [Name] -> Type +appsT t [] = t +appsT t (n:ns) = appsT (AppT t (VarT n)) ns + diff --git a/Generics/RepLib/Lib.hs b/Generics/RepLib/Lib.hs --- a/Generics/RepLib/Lib.hs +++ b/Generics/RepLib/Lib.hs @@ -80,21 +80,17 @@ rnfR :: R a -> a -> a -rnfR (Data dt cons) x = +rnfR (Data _ cons) x = case (findCon cons x) of Val emb reps args -> to emb (map_l rnfR reps args) rnfR _ x = x deepSeqR :: R a -> a -> b -> b -deepSeqR (Data dt cons) = \x -> +deepSeqR (Data _ cons) = \x -> case (findCon cons x) of Val _ reps args -> foldl_l (\ra bb a -> (deepSeqR ra a) . bb) id reps args deepSeqR _ = seq -deepSeq_l :: MTup R l -> l -> b -> b -deepSeq_l MNil Nil = id -deepSeq_l (rb :+: rs) (b :*: bs) = deepSeqR rb b . deepSeq_l rs bs - ------------------- Generic Sum ---------------------- -- | Add together all of the @Int@s in a datastructure -- For example: @@ -108,13 +104,13 @@ data GSumD a = GSumD { gsumD :: a -> Int } gsumR1 :: R1 GSumD a -> a -> Int -gsumR1 Int1 x = x -gsumR1 (Arrow1 r1 r2) f = error "urk" -gsumR1 (Data1 dt cons) x = +gsumR1 Int1 x = x +gsumR1 (Arrow1 _ _) _ = error "urk" +gsumR1 (Data1 _ cons) x = case (findCon cons x) of - Val emb rec kids -> + Val _ rec kids -> foldl_l (\ca a b -> (gsumD ca b) + a) 0 rec kids -gsumR1 _ x = 0 +gsumR1 _ _ = 0 instance GSum a => Sat (GSumD a) where dict = GSumD gsum @@ -147,11 +143,11 @@ zeroR1 :: R1 ZeroD a -> a zeroR1 Int1 = 0 zeroR1 Char1 = minBound -zeroR1 (Arrow1 z1 z2) = \x -> zeroD z2 +zeroR1 (Arrow1 _ z2) = const (zeroD z2) zeroR1 Integer1 = 0 zeroR1 Float1 = 0.0 zeroR1 Double1 = 0.0 -zeroR1 (Data1 dt (Con emb rec : rest)) = to emb (fromTup zeroD rec) +zeroR1 (Data1 _ (Con emb rec : _)) = to emb (fromTup zeroD rec) zeroR1 IOError1 = userError "Default Error" zeroR1 r1 = error ("No zero element of type: " ++ show r1) @@ -185,16 +181,16 @@ genEnum d = enumFromTo (toEnum 0) (toEnum d) generateR1 :: R1 GenerateD a -> Int -> [a] -generateR1 Int1 d = genEnum d -generateR1 Char1 d = genEnum d -generateR1 Integer1 d = genEnum d -generateR1 Float1 d = genEnum d -generateR1 Double1 d = genEnum d -generateR1 (Data1 dt cons) 0 = [] -generateR1 (Data1 dt cons) d = +generateR1 Int1 d = genEnum d +generateR1 Char1 d = genEnum d +generateR1 Integer1 d = genEnum d +generateR1 Float1 d = genEnum d +generateR1 Double1 d = genEnum d +generateR1 (Data1 _ _) 0 = [] +generateR1 (Data1 _ cons) d = [ to emb l | (Con emb rec) <- cons, l <- fromTupM (\x -> generateD x (d-1)) rec] -generateR1 r1 x = error ("No way to generate type: " ++ show r1) +generateR1 r1 _ = error ("No way to generate type: " ++ show r1) instance Generate Int instance Generate Char @@ -222,7 +218,7 @@ enumerateR1 :: R1 EnumerateD a -> [a] enumerateR1 Int1 = [minBound .. (maxBound::Int)] enumerateR1 Char1 = [minBound .. (maxBound::Char)] -enumerateR1 (Data1 dt cons) = enumerateCons cons +enumerateR1 (Data1 _ cons) = enumerateCons cons enumerateR1 r1 = error ("No way to enumerate type: " ++ show r1) enumerateCons :: [Con EnumerateD a] -> [a] @@ -241,10 +237,10 @@ class (Rep1 ShrinkD a) => Shrink a where shrink :: a -> [a] shrink a = subtrees a ++ shrinkStep a - where shrinkStep t = let M _ ts = gmapM1 m a - in ts - m :: forall a. ShrinkD a -> a -> M a - m dict x = M x ((shrinkD dict) x) + where shrinkStep _t = let M _ ts = gmapM1 m a + in ts + m :: forall b. ShrinkD b -> b -> M b + m d x = M x (shrinkD d x) data M a = M a [a] @@ -253,7 +249,7 @@ (M x xs) >>= k = M r (rs1 ++ rs2) where M r rs1 = k x - rs2 = [r | x <- xs, let M r _ = k x] + rs2 = [r' | x' <- xs, let M r' _ = k x'] instance Shrink Int instance Shrink a => Shrink [a] @@ -290,14 +286,14 @@ dict = LreduceD { lreduceD = lreduce } lreduceR1 :: R1 (LreduceD b) a -> b -> a -> b -lreduceR1 (Data1 dt cons) b a = case (findCon cons a) of - Val emb rec args -> foldl_l lreduceD b rec args -lreduceR1 _ b a = b +lreduceR1 (Data1 _ cons) b a = case (findCon cons a) of + Val _ rec args -> foldl_l lreduceD b rec args +lreduceR1 _ b _ = b rreduceR1 :: R1 (RreduceD b) a -> a -> b -> b -rreduceR1 (Data1 dt cons) a b = case (findCon cons a) of - Val emb rec args -> foldr_l rreduceD b rec args -rreduceR1 _ a b = b +rreduceR1 (Data1 _ cons) a b = case (findCon cons a) of + Val _ rec args -> foldr_l rreduceD b rec args +rreduceR1 _ _ b = b -- Instances for standard types instance Lreduce b Int diff --git a/Generics/RepLib/PreludeLib.hs b/Generics/RepLib/PreludeLib.hs --- a/Generics/RepLib/PreludeLib.hs +++ b/Generics/RepLib/PreludeLib.hs @@ -1,5 +1,6 @@ -- OPTIONS -fglasgow-exts -fallow-undecidable-instances {-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} ----------------------------------------------------------------------------- -- @@ -99,20 +100,20 @@ dict = OrdD { compareD = compare } lexord :: Ordering -> Ordering -> Ordering -lexord LT ord = LT +lexord LT _ = LT lexord EQ ord = ord -lexord GT ord = GT +lexord GT _ = GT -- | Minimal completion of the Ord class compareR1 :: R1 OrdD a -> a -> a -> Ordering compareR1 Int1 = compare compareR1 Char1 = compare -compareR1 (Data1 str cons) = \ x y -> +compareR1 (Data1 _ cons) = \ x y -> let loop (Con emb rec : rest) = case (from emb x, from emb y) of (Just t1, Just t2) -> compareTup rec t1 t2 - (Just t1, Nothing) -> LT - (Nothing, Just t2) -> GT + (Just _ , Nothing) -> LT + (Nothing, Just _ ) -> GT (Nothing, Nothing) -> loop rest in loop cons compareR1 r1 = error ("compareR1 not supported for " ++ show r1) @@ -133,14 +134,14 @@ minBoundR1 :: R1 BoundedD a -> a minBoundR1 Int1 = minBound minBoundR1 Char1 = minBound -minBoundR1 (Data1 dt (Con emb rec:rest)) = to emb (fromTup minBoundD rec) +minBoundR1 (Data1 _ (Con emb rec:_)) = to emb (fromTup minBoundD rec) minBoundR1 r1 = error ("minBoundR1 not supported for " ++ show r1) -- | To generate the Bounded class maxBoundR1 :: R1 BoundedD a -> a maxBoundR1 Int1 = maxBound maxBoundR1 Char1 = maxBound -maxBoundR1 (Data1 dt cons) = +maxBoundR1 (Data1 _ cons) = case last cons of (Con emb rec) -> to emb (fromTup maxBoundD rec) maxBoundR1 r1 = error ("maxBoundR1 not supported for " ++ show r1) @@ -165,8 +166,8 @@ Int -> -- precendence level a -> -- value to be shown ShowS -showsPrecR1 (Data1 (DT str _) cons) = \p a -> - case (findCon cons a) of +showsPrecR1 (Data1 (DT _ _) cons) = \p v -> + case (findCon cons v) of Val c rec kids -> case (labels c) of Just labs -> par $ showString (name c) . @@ -178,14 +179,14 @@ showKids rec kids where par = showParen (p > p' && conArity > 0) p' = getFixity c - maybespace = if conArity == 0 then id else (' ':) + maybespace = if conArity == (0::Int) then id else (' ':) conArity = foldr_l (\_ _ i -> 1 + i) 0 rec kids showKid :: ShowD a -> a -> ShowS showKid r x = showsPrecD r (p'+1) x showRecord :: MTup ShowD l -> l -> [String] -> ShowS - showRecord (r :+: MNil) (a :*: Nil) (l : ls) = showString l . ('=':) . showKid r a + showRecord (r :+: MNil) (a :*: Nil) (l : _) = showString l . ('=':) . showKid r a showRecord (r :+: rs) (a :*: aa) (l : ls) = showString l . ('=':) . showKid r a . showString (", ") . showRecord rs aa ls showRecord _ _ _ = error ("Incorrect representation: " ++ diff --git a/Generics/RepLib/PreludeReps.hs b/Generics/RepLib/PreludeReps.hs --- a/Generics/RepLib/PreludeReps.hs +++ b/Generics/RepLib/PreludeReps.hs @@ -1,6 +1,7 @@ {-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} ----------------------------------------------------------------------------- -- | -- Module : RepLib.PreludeReps @@ -17,7 +18,6 @@ module Generics.RepLib.PreludeReps where import Generics.RepLib.R -import Generics.RepLib.R1 import Generics.RepLib.Derive import Language.Haskell.TH diff --git a/Generics/RepLib/R.hs b/Generics/RepLib/R.hs --- a/Generics/RepLib/R.hs +++ b/Generics/RepLib/R.hs @@ -17,7 +17,7 @@ module Generics.RepLib.R where -import Data.List +import Data.Type.Equality -- | A value of type @R a@ is a representation of a type @a@. data R a where @@ -32,11 +32,13 @@ Arrow :: (Rep a, Rep b) => R a -> R b -> R (a -> b) Data :: DT -> [Con R a] -> R a Abstract :: DT -> R a + Equal :: (Rep a, Rep b) => R a -> R b -> R (a :=: b) -- | Representation of a data constructor includes an -- embedding between the datatype and a list of other types -- as well as the representation of that list of other types. -data Con r a = forall l. Con (Emb l a) (MTup r l) +data Con r a where + Con :: Emb l a -> MTup r l -> Con r a -- | An embedding between a list of types @l@ and -- a datatype @a@, based on a particular data constructor. @@ -65,19 +67,16 @@ -- | Cons for a list of types data a :*: l = a :*: l -data Ex f = forall a. Rep a => Ex (f a) - infixr 7 :*: -- | A heterogeneous list data MTup r l where MNil :: MTup r Nil (:+:) :: (Rep a) => r a -> MTup r l -> MTup r (a :*: l) - MEx :: (Rep a) => MTup r (f a) -> MTup r (Ex f) infixr 7 :+: --- | A Class of representatble types +-- | A class of representable types class Rep a where rep :: R a ------ Showing representations (rewrite this with showsPrec?) @@ -97,6 +96,8 @@ "(Data" ++ show dt ++ ")" show (Abstract dt) = "(Abstract" ++ show dt ++ ")" + show (Equal r1 r2) = + "(Equal" ++ show r1 ++ " " ++ show r2 ++ ")" instance Show DT where show (DT str reps) = str ++ show reps @@ -107,22 +108,23 @@ show (r :+: rs) = " " ++ show r ++ show rs instance Eq (R a) where - r1 == r2 = True + _ == _ = True instance Ord (R a) where - compare r1 r2 = EQ -- R a is a singleton + compare _ _ = EQ -- R a is a singleton --- Representations for (some) Haskell Prelude types instance Rep Int where rep = Int instance Rep Char where rep = Char +instance Rep Integer where rep = Integer +instance Rep Float where rep = Float instance Rep Double where rep = Double instance Rep Rational where rep = Rational -instance Rep Float where rep = Float -instance Rep Integer where rep = Integer -instance Rep a => Rep (IO a) where rep = IO rep instance Rep IOError where rep = IOError +instance Rep a => Rep (IO a) where rep = IO rep instance (Rep a, Rep b) => Rep (a -> b) where rep = Arrow rep rep +instance (Rep a, Rep b) => Rep (a :=: b) where rep = Equal rep rep -- Unit @@ -146,7 +148,7 @@ rTup2 :: forall a b. (Rep a, Rep b) => R (a,b) rTup2 = let args = ((rep :: R a) :+: (rep :: R b) :+: MNil) in - Data (DT "," args) [ Con rPairEmb args ] + Data (DT "(,)" args) [ Con rPairEmb args ] rPairEmb :: Emb (a :*: b :*: Nil) (a,b) rPairEmb = @@ -165,8 +167,8 @@ rNilEmb :: Emb Nil [a] rNilEmb = Emb { to = \Nil -> [], from = \x -> case x of - (x:xs) -> Nothing - [] -> Just Nil, + (_:_) -> Nothing + [] -> Just Nil, labels = Nothing, name = "[]", fixity = Nonfix diff --git a/Generics/RepLib/R1.hs b/Generics/RepLib/R1.hs --- a/Generics/RepLib/R1.hs +++ b/Generics/RepLib/R1.hs @@ -1,6 +1,13 @@ -{-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs, ScopedTypeVariables, - MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances +{-# LANGUAGE TemplateHaskell + , UndecidableInstances + , GADTs + , ScopedTypeVariables + , MultiParamTypeClasses + , FlexibleInstances + , TypeSynonymInstances + , TypeOperators #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} ----------------------------------------------------------------------------- -- | @@ -18,7 +25,7 @@ module Generics.RepLib.R1 where import Generics.RepLib.R -import Data.List +import Data.Type.Equality ---------- Basic infrastructure @@ -34,6 +41,7 @@ Arrow1 :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b) Data1 :: DT -> [Con ctx a] -> R1 ctx a Abstract1 :: DT -> R1 ctx a + Equal1 :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a :=: b) class Sat a where dict :: a class Rep a => Rep1 ctx a where rep1 :: R1 ctx a @@ -50,10 +58,11 @@ show (Arrow1 cb cc) = "(Arrow1 " ++ show (getRepC cb) ++ " " ++ show (getRepC cc) ++ ")" show (Data1 dt _) = "(Data1 " ++ show dt ++ ")" show (Abstract1 dt) = "(Abstract1 " ++ show dt ++ ")" + show (Equal1 ca cb) = "(Equal1 " ++ show (getRepC ca) ++ " " ++ show (getRepC cb) ++ ")" -- | Access a representation, given a proxy getRepC :: Rep b => c b -> R b -getRepC cb = rep +getRepC _ = rep -- | Transform a parameterized rep to a vanilla rep toR :: R1 c a -> R a @@ -72,6 +81,7 @@ toRs MNil = MNil toRs (c :+: l) = (getRepC c :+: toRs l) toR (Abstract1 dt) = Abstract dt +toR (Equal1 ca cb) = Equal (getRepC ca) (getRepC cb) --------------- Representations of Prelude types @@ -87,6 +97,8 @@ instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => Rep1 ctx (a -> b) where rep1 = Arrow1 dict dict +instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => + Rep1 ctx (a :=: b) where rep1 = Equal1 dict dict -- Data structures @@ -110,12 +122,12 @@ rList1 :: forall a ctx. Rep a => ctx a -> ctx [a] -> R1 ctx [a] rList1 ca cl = Data1 (DT "[]" ((rep :: R a) :+: MNil)) - [ rCons1 ca cl, rNil1 ] where + [ rCons1, rNil1 ] where rNil1 :: Con ctx [a] rNil1 = Con rNilEmb MNil - rCons1 :: ctx a -> ctx [a] -> Con ctx [a] - rCons1 ca cl = Con rConsEmb (ca :+: cl :+: MNil) + rCons1 :: Con ctx [a] + rCons1 = Con rConsEmb (ca :+: cl :+: MNil) instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a] where rep1 = rList1 dict dict diff --git a/Generics/RepLib/RepAux.hs b/Generics/RepLib/RepAux.hs --- a/Generics/RepLib/RepAux.hs +++ b/Generics/RepLib/RepAux.hs @@ -1,6 +1,12 @@ -{-# LANGUAGE TemplateHaskell, UndecidableInstances, MagicHash, - ScopedTypeVariables, GADTs, Rank2Types +{-# LANGUAGE TemplateHaskell + , UndecidableInstances + , MagicHash + , ScopedTypeVariables + , GADTs + , Rank2Types + , TypeOperators #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} ----------------------------------------------------------------------------- -- | -- Module : RepAux @@ -38,23 +44,30 @@ import Generics.RepLib.R import Generics.RepLib.R1 import GHC.Base (unsafeCoerce#) - +import Data.Type.Equality (EqT(..), (:=:)(..)) ------ Casting +instance EqT R where + -- eqT :: R a -> R b -> Maybe (a :=: b) + eqT ra rb = + if eqR ra rb then Just (unsafeCoerce# Refl) else Nothing + -- | Determine if two reps are for the same type eqR :: R a -> R b -> Bool -eqR Int Int = True -eqR Char Char = True -eqR Float Float = True -eqR Integer Integer = True -eqR Double Double = True -eqR (IO t1) (IO t2) = eqR t1 t2 -eqR IOError IOError = True -eqR (Arrow t1 t2) (Arrow s1 s2) = eqR t1 s1 && eqR t2 s2 -eqR (Data rc1 _) (Data rc2 _) = eqDT rc1 rc2 +eqR Int Int = True +eqR Char Char = True +eqR Integer Integer = True +eqR Float Float = True +eqR Double Double = True +eqR Rational Rational = True +eqR IOError IOError = True +eqR (IO t1) (IO t2) = eqR t1 t2 +eqR (Arrow t1 t2) (Arrow s1 s2) = eqR t1 s1 && eqR t2 s2 +eqR (Data rc1 _) (Data rc2 _) = eqDT rc1 rc2 eqR (Abstract rc1) (Abstract rc2) = eqDT rc1 rc2 -eqR _ _ = False +eqR (Equal t1 t2) (Equal s1 s2) = eqR t1 s1 && eqR t2 s2 +eqR _ _ = False eqDT :: DT -> DT -> Bool eqDT (DT str1 rt1) (DT str2 rt2) = str1 == str2 && eqRTup rt1 rt2 @@ -63,23 +76,27 @@ (==) = eqDT eqRTup :: MTup R t1 -> MTup R t2 -> Bool -eqRTup MNil MNil = True +eqRTup MNil MNil = True eqRTup (r1 :+: rt1) (r2 :+: rt2) = eqR r1 r2 && eqRTup rt1 rt2 +eqRTup _ _ = False -- | The type-safe cast operation, explicit arguments castR :: R a -> R b -> a -> Maybe b -castR (ra::R a) (rb::R b) = - if eqR ra rb then \(x::a) -> Just (unsafeCoerce# x::b) else \x -> Nothing +castR ra rb a = + case eqT ra rb of + Just Refl -> Just a + Nothing -> Nothing + -- | The type-safe cast operation, implicit arguments cast :: forall a b. (Rep a, Rep b) => a -> Maybe b -cast x = castR (rep :: R a) (rep :: R b) x +cast x = castR rep rep x -- | Leibniz equality between types, explicit representations gcastR :: forall a b c. R a -> R b -> c a -> Maybe (c b) -gcastR ra rb = if eqR ra rb - then \(x :: c a) -> Just (unsafeCoerce# x :: c b) - else \x -> Nothing +gcastR ra rb x = case eqT ra rb of + Just Refl -> Just x + Nothing -> Nothing -- | Leibniz equality between types, implicit representations gcast :: forall a b c. (Rep a, Rep b) => c a -> Maybe (c b) @@ -89,42 +106,59 @@ -- | Heterogeneous Ordering compareR :: R a -> R b -> Ordering -compareR Int Int = EQ -compareR Int _ = LT -compareR _ Int = GT -compareR Char Char = EQ -compareR Char _ = LT -compareR _ Char = GT -compareR Integer Integer = EQ -compareR Integer _ = LT -compareR _ Integer = GT -compareR Float Float = EQ -compareR Float _ = LT -compareR _ Float = GT + +compareR Int Int = EQ +compareR Int _ = LT +compareR _ Int = GT + +compareR Char Char = EQ +compareR Char _ = LT +compareR _ Char = GT + +compareR Integer Integer = EQ +compareR Integer _ = LT +compareR _ Integer = GT + +compareR Float Float = EQ +compareR Float _ = LT +compareR _ Float = GT + +compareR Double Double = EQ +compareR Double _ = LT +compareR _ Double = GT + compareR Rational Rational = EQ -compareR Rational _ = LT -compareR _ Rational = GT -compareR IOError IOError = EQ -compareR IOError _ = LT -compareR _ IOError = GT -compareR (IO r1) (IO r2) = compareR r1 r2 -compareR (IO _) _ = LT -compareR _ (IO _) = GT +compareR Rational _ = LT +compareR _ Rational = GT + +compareR IOError IOError = EQ +compareR IOError _ = LT +compareR _ IOError = GT + +compareR (IO r1) (IO r2) = compareR r1 r2 +compareR (IO _) _ = LT +compareR _ (IO _) = GT + compareR (Arrow r1 r2) (Arrow r3 r4) = case compareR r1 r3 of - EQ -> compareR r2 r4 + EQ -> compareR r2 r4 ord -> ord -compareR (Arrow _ _) _ = LT -compareR _ (Arrow _ _) = GT -compareR (Data dt1 _) (Data dt2 _) = - compare dt1 dt2 -compareR (Data _ _) _ = LT -compareR _ (Data _ _) = GT -compareR (Abstract dt1) (Abstract dt2) = - compare dt1 dt2 -compareR (Abstract _) _ = LT -compareR _ (Abstract _) = GT +compareR (Arrow _ _) _ = LT +compareR _ (Arrow _ _) = GT +compareR (Data dt1 _) (Data dt2 _) = compare dt1 dt2 +compareR (Data _ _) _ = LT +compareR _ (Data _ _) = GT + +compareR (Abstract dt1) (Abstract dt2) = compare dt1 dt2 +compareR (Abstract _) _ = LT +compareR _ (Abstract _) = GT + +compareR (Equal t1 t2) (Equal s1 s2) = + case compareR t1 s1 of + EQ -> compareR t2 s2 + ord -> ord + instance Ord DT where compare (DT str1 reps1) (DT str2 reps2) = case compare str1 str2 of @@ -145,42 +179,44 @@ --------- Basic instances and library operations for heterogeneous lists --------------- -- | A datastructure to store the results of findCon -data Val ctx a = forall l. Val (Emb l a) (MTup ctx l) l +data Val ctx a where + Val :: Emb l a -> MTup ctx l -> l -> Val ctx a -- | Given a list of constructor representations for a datatype, -- determine which constructor formed the datatype. findCon :: [Con ctx a] -> a -> Val ctx a findCon (Con rcd rec : rest) x = case (from rcd x) of - Just ys -> Val rcd rec ys - Nothing -> findCon rest x + Just ys -> Val rcd rec ys + Nothing -> findCon rest x +findCon [] _ = error "findCon: panic: exhausted constructor list without finding a match" -- | A fold right operation for heterogeneous lists, that folds a function -- expecting a type type representation across each element of the list. foldr_l :: (forall a. Rep a => ctx a -> a -> b -> b) -> b -> (MTup ctx l) -> l -> b -foldr_l f b MNil Nil = b +foldr_l _ b MNil Nil = b foldr_l f b (ca :+: cl) (a :*: l) = f ca a (foldr_l f b cl l ) -- | A fold left for heterogeneous lists foldl_l :: (forall a. Rep a => ctx a -> b -> a -> b) -> b -> (MTup ctx l) -> l -> b -foldl_l f b MNil Nil = b +foldl_l _ b MNil Nil = b foldl_l f b (ca :+: cl) (a :*: l) = foldl_l f (f ca b a) cl l -- | A map for heterogeneous lists map_l :: (forall a. Rep a => ctx a -> a -> a) -> (MTup ctx l) -> l -> l -map_l f MNil Nil = Nil +map_l _ MNil Nil = Nil map_l f (ca :+: cl) (a :*: l) = (f ca a) :*: (map_l f cl l) -- | Transform a heterogeneous list in to a standard list mapQ_l :: (forall a. Rep a => ctx a -> a -> r) -> MTup ctx l -> l -> [r] -mapQ_l q MNil Nil = [] +mapQ_l _ MNil Nil = [] mapQ_l q (r :+: rs) (a :*: l) = q r a : mapQ_l q rs l -- | mapM for heterogeneous lists mapM_l :: (Monad m) => (forall a. Rep a => ctx a -> a -> m a) -> MTup ctx l -> l -> m l -mapM_l f MNil Nil = return Nil +mapM_l _ MNil Nil = return Nil mapM_l f (ca :+: cl) (a :*: l) = do x1 <- f ca a x2 <- mapM_l f cl l @@ -188,19 +224,19 @@ -- | Generate a heterogeneous list from metadata fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l -fromTup f MNil = Nil +fromTup _ MNil = Nil fromTup f (b :+: l) = (f b) :*: (fromTup f l) -- | Generate a heterogeneous list from metadata, in a monad fromTupM :: (Monad m) => (forall a. Rep a => ctx a -> m a) -> MTup ctx l -> m l -fromTupM f MNil = return Nil +fromTupM _ MNil = return Nil fromTupM f (b :+: l) = do hd <- f b tl <- fromTupM f l return (hd :*: tl) -- | Generate a normal lists from metadata toList :: (forall a. Rep a => ctx a -> b) -> MTup ctx l -> [b] -toList f MNil = [] +toList _ MNil = [] toList f (b :+: l) = f b : toList f l --------------------- SYB style operations -------------------------- @@ -212,7 +248,7 @@ gmapT :: forall a. Rep a => Traversal -> a -> a gmapT t = case (rep :: R a) of - (Data dt cons) -> \x -> + (Data _ cons) -> \x -> case (findCon cons x) of Val emb reps ys -> to emb (map_l (const t) reps ys) _ -> id @@ -224,8 +260,8 @@ gmapQ :: forall a r. Rep a => Query r -> a -> [r] gmapQ q = case (rep :: R a) of - (Data dt cons) -> \x -> case (findCon cons x) of - Val emb reps ys -> mapQ_l (const q) reps ys + (Data _ cons) -> \x -> case (findCon cons x) of + Val _ reps ys -> mapQ_l (const q) reps ys _ -> const [] @@ -234,7 +270,7 @@ gmapM :: forall a m. (Rep a, Monad m) => MapM m -> a -> m a gmapM m = case (rep :: R a) of - (Data dt cons) -> \x -> case (findCon cons x) of + (Data _ cons) -> \x -> case (findCon cons x) of Val emb reps ys -> do l <- mapM_l (const m) reps ys return (to emb l) _ -> return @@ -246,7 +282,7 @@ gmapT1 :: forall a ctx. (Rep1 ctx a) => Traversal1 ctx -> a -> a gmapT1 t = case (rep1 :: R1 ctx a) of - (Data1 dt cons) -> \x -> + (Data1 _ cons) -> \x -> case (findCon cons x) of Val emb recs kids -> to emb (map_l t recs kids) _ -> id @@ -255,14 +291,14 @@ gmapQ1 :: forall a ctx r. (Rep1 ctx a) => Query1 ctx r -> a -> [r] gmapQ1 q = case (rep1 :: R1 ctx a) of - (Data1 dt cons) -> \x -> case (findCon cons x) of - Val emb recs kids -> mapQ_l q recs kids + (Data1 _ cons) -> \x -> case (findCon cons x) of + Val _ recs kids -> mapQ_l q recs kids _ -> const [] type MapM1 ctx m = forall a. Rep a => ctx a -> a -> m a gmapM1 :: forall a ctx m. (Rep1 ctx a, Monad m) => MapM1 ctx m -> a -> m a gmapM1 m = case (rep1 :: R1 ctx a) of - (Data1 dt cons) -> \x -> case (findCon cons x) of + (Data1 _ cons) -> \x -> case (findCon cons x) of Val emb rec ys -> do l <- mapM_l m rec ys return (to emb l) _ -> return diff --git a/Generics/RepLib/SYB/Aliases.hs b/Generics/RepLib/SYB/Aliases.hs --- a/Generics/RepLib/SYB/Aliases.hs +++ b/Generics/RepLib/SYB/Aliases.hs @@ -366,8 +366,10 @@ -- | The type constructor for transformations newtype M m x = M { unM :: x -> m x } +{- -- | The type constructor for queries newtype Q q x = Q { unQ :: x -> q } +-} -- | The type constructor for readers newtype R m x = R { unR :: m x } diff --git a/Generics/RepLib/Unify.hs b/Generics/RepLib/Unify.hs --- a/Generics/RepLib/Unify.hs +++ b/Generics/RepLib/Unify.hs @@ -2,6 +2,7 @@ ExistentialQuantification, ScopedTypeVariables, EmptyDataDecls, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} +{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} ----------------------------------------------------------------------------- -- @@ -88,7 +89,7 @@ (Nothing, Nothing) -> loop rest (_,_) -> throwError (strMsg $ "constructor mismatch when trying to match " ++ show x ++ " = " ++ show y) in loop cons -unifyStepR1 r1 _ = \_ _ -> throwError (strMsg ("unifyStepR1 unhandled generic type constructor")) +unifyStepR1 _ _ = \_ _ -> throwError (strMsg ("unifyStepR1 unhandled generic type constructor")) @@ -98,7 +99,7 @@ do queueConstraint $ UC r p1 p2 addConstraintsRL1 rl dum t1 t2 - +unifyStepEq :: (Eq b, Show b) => b -> b -> UM n a () unifyStepEq x y = if x == y then return () else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y) -- " show x ++ " /= " ++ show y) @@ -169,7 +170,7 @@ cs = [(UC dict a1 a2) | (a1, a2) <- eqs] rwConstraints :: UM n a () rwConstraints = do c <- dequeueConstraint - case c of Just (UC d a1 a2) -> do result <- unifyStepD d (undefined :: Proxy (n, a)) a1 a2 + case c of Just (UC d a1 a2) -> do _ <- unifyStepD d (undefined :: Proxy (n, a)) a1 a2 rwConstraints Nothing -> return () @@ -189,7 +190,7 @@ cs = [(UC dict a1 a2) | (a1, a2) <- eqs] rwConstraints :: UM n a () rwConstraints = do c <- dequeueConstraint - case c of Just (UC d a1 a2) -> do result <- unifyStepD d dum a1 a2 + case c of Just (UC d a1 a2) -> do _ <- unifyStepD d dum a1 a2 rwConstraints Nothing -> return () @@ -213,7 +214,7 @@ -- generic subst. substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t' -substR1 r (a::a) (t::t) t' = gmapT1 (\cb b -> substD cb a t b) t' +substR1 _ (a::a) (t::t) t' = gmapT1 (\cb b -> substD cb a t b) t' -- a a instance instance (Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t where @@ -232,7 +233,7 @@ -- generic subst. occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool -occursCheckR1 r (n::n) pa b = or $ gmapQ1 (\cb b -> occursCheckD cb n pa b) b +occursCheckR1 _ (n::n) pa b = or $ gmapQ1 (\cb b' -> occursCheckD cb n pa b') b -- a a instance. instance (Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a where diff --git a/RepLib.cabal b/RepLib.cabal --- a/RepLib.cabal +++ b/RepLib.cabal @@ -1,13 +1,13 @@ name: RepLib -version: 0.4.0 +version: 0.5 license: BSD3 license-file: LICENSE build-type: Simple cabal-version: >= 1.6 -tested-with: GHC == 7.0.1 +tested-with: GHC == 7.0.1, GHC == 7.0.3, GHC == 7.0.4 author: Stephanie Weirich maintainer: Brent Yorgey - Chris Casinghino + Chris Casinghino Stephanie Weirich homepage: http://code.google.com/p/replib/ category: Generics @@ -16,10 +16,16 @@ description: Generic programming library providing structural polymorphism and other features. +Source-repository head + type: svn + location: http://replib.googlecode.com/svn/trunk/ + Library build-depends: base >= 4.3 && < 5, template-haskell >= 2.4 && < 2.6, - mtl >= 2.0 && < 2.1 + mtl >= 2.0 && < 2.1, + type-equality >= 0.1.0.2 && < 0.2, + containers >= 0.4 && < 0.5 exposed-modules: Generics.RepLib, Generics.RepLib.R,