RepLib 0.4.0 → 0.5
raw patch · 11 files changed
+768/−349 lines, 11 filesdep +containersdep +type-equality
Dependencies added: containers, type-equality
Files
- Generics/RepLib.hs +4/−1
- Generics/RepLib/Derive.hs +562/−202
- Generics/RepLib/Lib.hs +29/−33
- Generics/RepLib/PreludeLib.hs +12/−11
- Generics/RepLib/PreludeReps.hs +1/−1
- Generics/RepLib/R.hs +16/−14
- Generics/RepLib/R1.hs +19/−7
- Generics/RepLib/RepAux.hs +106/−70
- Generics/RepLib/SYB/Aliases.hs +2/−0
- Generics/RepLib/Unify.hs +7/−6
- RepLib.cabal +10/−4
Generics/RepLib.hs view
@@ -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 -----------------------------------------------------------------------------
Generics/RepLib/Derive.hs view
@@ -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+
Generics/RepLib/Lib.hs view
@@ -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
Generics/RepLib/PreludeLib.hs view
@@ -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: " ++
Generics/RepLib/PreludeReps.hs view
@@ -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
Generics/RepLib/R.hs view
@@ -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
Generics/RepLib/R1.hs view
@@ -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
Generics/RepLib/RepAux.hs view
@@ -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
Generics/RepLib/SYB/Aliases.hs view
@@ -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 }
Generics/RepLib/Unify.hs view
@@ -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
RepLib.cabal view
@@ -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 <byorgey@cis.upenn.edu>- Chris Casinghino <ccasin@cis.upenn.edu>+ Chris Casinghino <ccasin@cis.upenn.edu> Stephanie Weirich <sweirich@cis.upenn.edu> 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,