diff --git a/Data/RepLib.hs b/Data/RepLib.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib.hs @@ -0,0 +1,45 @@ +-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances +{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.RepLib +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- +-- +----------------------------------------------------------------------------- + +-- Toplevel module to import all others. + +module Data.RepLib ( + + module Data.RepLib.R, + module Data.RepLib.R1, + module Data.RepLib.Lib, + module Data.RepLib.PreludeReps, + module Data.RepLib.PreludeLib, + module Data.RepLib.RepAux, + module Data.RepLib.Derive, + module Data.RepLib.SYB.Aliases, + module Data.RepLib.SYB.Schemes + +) where + +import Data.RepLib.R +import Data.RepLib.R1 +import Data.RepLib.PreludeReps +import Data.RepLib.Lib +import Data.RepLib.PreludeLib +import Data.RepLib.RepAux +import Data.RepLib.Derive +import Data.RepLib.SYB.Aliases +import Data.RepLib.SYB.Schemes + +----------------------------------------------------------------------------- + diff --git a/Data/RepLib/Derive.hs b/Data/RepLib/Derive.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/Derive.hs @@ -0,0 +1,320 @@ +-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances -ddump-splices -- + +{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Derive +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : TBD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- code to automatically derive representations and instance declarations +-- for user defined datatypes. +-- +-- +----------------------------------------------------------------------------- + + +module Data.RepLib.Derive ( + repr, reprs, repr1, repr1s, derive +) where + +import Data.RepLib.R +import Data.RepLib.R1 +import Language.Haskell.TH +import Data.List (nub) +import Data.Tuple + + +-- Given a type, produce its representation. +-- Note, that the representation of a type variable "a" is (rep :: R a) so Rep a must be +-- in the context +repty :: Type -> Exp +repty (ForallT _ _ _) = error "cannot rep" +repty (VarT n) = (SigE (VarE (mkName "rep")) ((ConT ''R) `AppT` (VarT n))) +repty (AppT t1 t2) = (repty t1) -- `AppE` (repty t2) +repty (ConT n) = + 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 2) = (VarE (mkName "rTup2")) +repty (TupleT i) = error "urk" +repty (ArrowT) = (ConE 'Arrow) +repty (ListT) = (VarE 'rList) + + +rName :: Name -> Name +rName n = + case nameBase n of + "(,,,,,,)" -> mkName ("rTup7") + "(,,,,,)" -> mkName ("rTup6") + "(,,,,)" -> mkName ("rTup5") + "(,,,)" -> mkName ("rTup4") + "(,,)" -> mkName ("rTup3") + "(,)" -> mkName ("rTup2") + c -> mkName ("r" ++ c) + +rName1 :: Name -> Name +rName1 n = + case nameBase n of + "(,,,,,,)" -> mkName ("rTup7_1") + "(,,,,,)" -> mkName ("rTup6_1") + "(,,,,)" -> mkName ("rTup5_1") + "(,,,)" -> mkName ("rTup4_1") + "(,,)" -> mkName ("rTup3_1") + "(,)" -> mkName ("rTup2_1") + c -> mkName ("r" ++ c ++ "1") + +------------------------------------------------------------------------------------------------------- +-- represent a data constructor. +-- As our representation of data constructors evolves, so must this definition. +-- 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 -> + [| $(return (repty t)) :+: $(tl) |]) [| MNil |] sttys in + [| Con $(remb single d (name,sttys)) $(rargs) |] + +-- 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))) + +-- to component of th embedding +rto :: Type -> (Name, [(Maybe Name, Type)]) -> Q Exp +rto d (name,sttys) = + do vars <- mapM (\_ -> newName "x") sttys + let topat = foldr (\v tl -> InfixP (VarP v) (mkName ":*:") tl) + (ConP 'Nil []) vars + tobod = foldl (\tl v -> tl `AppE` (VarE v)) (ConE name) 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)), + labels = Nothing, + fixity = Nonfix } |] + +repDT :: Name -> [Name] -> Q Exp +repDT name param = + do str <- stringName name + let reps = foldr (\p f -> + (ConE (mkName ":+:")) `AppE` + (SigE (VarE (mkName "rep")) + ((ConT ''R) `AppT` (VarT p))) `AppE` f) + (ConE 'MNil) param + [| DT $(return str) $(return reps) |] + +-- Create an "R" representation for a given type constructor +repr :: Name -> Q [Dec] +repr n = do info' <- reify n + case info' of + TyConI d -> do + (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) + baseT <- conT name + -- the type that we are defining, applied to its parameters. + let ty = foldl (\x p -> x `AppT` (VarT p)) baseT param + -- the representations of the paramters, as a list + -- representations of the data constructors + rcons <- mapM (repcon (length terms == 1) ty) terms + body <- [| Data $(repDT name param) $(return (ListE rcons)) |] + let ctx = map (\p -> (ConT (mkName "Rep")) `AppT` (VarT p)) param + let rTypeName :: Name + rTypeName = rName n + rSig :: Dec + rSig = SigD rTypeName (ForallT param ctx ((ConT (mkName "R")) + `AppT` ty)) + rType :: Dec + 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] + +reprs :: [Name] -> Q [Dec] +reprs ns = foldl (\qd n -> do decs1 <- repr n + decs2 <- qd + return (decs1 ++ decs2)) (return []) 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. + +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 + +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) + +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) |] + +repr1 :: Name -> Q [Dec] +repr1 n = do info' <- reify n + case info' of + TyConI d -> do + (name, param, ca, terms) <- typeInfo ((return d) :: Q Dec) + -- the type that we are defining, applied to its parameters. + let ty = foldl (\x p -> x `AppT` (VarT p)) (ConT name) param + let rTypeName = rName1 n + + ctx <- newName "ctx" + ctxParams <- ctx_params ty ctx terms + + -- 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 + + -- the recursive call of the rep function + let e1 = foldl (\a r -> a `AppE` (VarE r)) (VarE rTypeName) param + let e2 = foldl (\a (n,_,_) -> a `AppE` (VarE n)) e1 ctxParams + + -- the representations of the parameters, as a list + -- representations of the data constructors + rcons <- mapM (repcon1 ty (length terms == 1) e2 ctxParams) terms + body <- [| Data1 $(repDT name param) + $(return (ListE rcons)) |] + + 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) [] + + + let ctxRep = map (\p -> (ConT (mkName "Rep")) `AppT` (VarT p)) param + ctxRec = map (\(_,t,_) -> (ConT ''Sat) `AppT` t) ctxParams + + -- appRep t = foldl (\a p -> a `AppE` (VarE 'rep)) t param + appRec t = foldl (\a p -> a `AppE` (VarE 'dict)) t ctxParams + + let inst = InstanceD (ctxRep ++ ctxRec) + ((ConT ''Rep1) `AppT` (VarT ctx) `AppT` ty) + [ValD (VarP (mkName "rep1")) + (NormalB (appRec (VarE rTypeName))) []] + + let rSig = SigD rTypeName (ForallT (ctx : param) ctxRep + (foldr (\(_,p,_) f -> (ArrowT `AppT` p `AppT` f)) + ((ConT (mkName "R1")) `AppT` (VarT ctx) `AppT` ty) + ctxParams)) + decs <- repr n + return (decs ++ [rSig, rTypeDecl, inst]) + + +repr1s :: [Name] -> Q [Dec] + + +repr1s ns = foldl (\qd n -> do decs1 <- repr1 n + decs2 <- qd + return (decs1 ++ decs2)) (return []) ns +derive = repr1s + +-------------------------------------------------------------------------------------- + + + +--- Helper functions + +stringName :: Name -> Q Exp +stringName n = return (LitE (StringL (nameBase n))) + +--- from SYB III code.... + +typeInfo :: DecQ -> Q (Name, [Name], [(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) + + where + consA (DataD _ _ _ cs _) = map conA cs + consA (NewtypeD _ _ _ c _) = [ conA c ] + + paramsA (DataD _ _ ps _ _) = ps + paramsA (NewtypeD _ _ ps _ _) = ps + + termsA (DataD _ _ _ cs _) = map termA cs + termsA (NewtypeD _ _ _ c _) = [ termA c ] + + 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)]) + + conA (NormalC c xs) = (simpleName c, length xs) + conA (RecC c xs) = (simpleName c, length xs) + conA (InfixC _ c _) = (simpleName c, 2) + + name (DataD _ n _ _ _) = n + name (NewtypeD _ n _ _ _) = n + name d = error $ show d + +simpleName :: Name -> Name +simpleName nm = + let s = nameBase nm + in case dropWhile (/=':') s of + [] -> mkName s + _:[] -> mkName s + _:t -> mkName t + + diff --git a/Data/RepLib/Lib.hs b/Data/RepLib/Lib.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/Lib.hs @@ -0,0 +1,331 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, + MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, + TypeSynonymInstances + #-} + + +----------------------------------------------------------------------------- +-- | +-- Module : RepLib.Lib +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- A library of specializable, type-indexed functions +-- +----------------------------------------------------------------------------- +module Data.RepLib.Lib ( + -- * Available for all representable types + subtrees, deepSeq, rnf, + -- * Derivable classes + GSum(..), + Zero(..), + Generate(..), + Enumerate(..), + Shrink(..), + Lreduce(..), + Rreduce(..), + + -- * Generic operations based on Fold + Fold(..), + crush, gproduct, gand, gor, flatten, count, comp, gconcat, gall, gany, gelem, + + -- * Types and generators for derivable classes + GSumD(..), ZeroD(..), GenerateD(..), EnumerateD(..), ShrinkD(..), LreduceD(..), RreduceD(..), + rnfR, deepSeqR, gsumR1, zeroR1, generateR1, enumerateR1, lreduceR1, rreduceR1 + +) where + +import Data.RepLib.R +import Data.RepLib.R1 +import Data.RepLib.RepAux +import Data.RepLib.PreludeReps + +------------------- Subtrees -------------------------- +-- there is no point in using R1 for subtrees +-- From Mark P. Jones, Functional programming with +-- overloading and higher-order polymorphism +-- Also the same function as "children" from SYB III + +-- | Produce all children of a datastructure with the same type +-- Note that subtrees is available for all representable types. For those that +-- are not recursive datatypes, subtrees will always return the +-- empty list. But, these trivial instances are convenient to have +-- for the Shrink operation below. + +subtrees :: forall a. Rep a => a -> [a] +subtrees x = [y | Just y <- gmapQ (cast :: Query (Maybe a)) x] + +-------------------- DeepSeq ----------------------- + + +-- | deepSeq recursively forces the evaluation of its entire +-- argument. +deepSeq :: Rep a => a -> b -> b +deepSeq = deepSeqR rep + +-- | rnf forces the evaluation of *datatypes* to their normal +-- forms. However, other types are left alone and not forced. +rnf :: Rep a => a -> a +rnf = rnfR rep + + +rnfR :: R a -> a -> a +rnfR (Data dt 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 -> + 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 +class Rep1 GSumD a => GSum a where + gsum :: a -> Int + gsum = gsumR1 rep1 + +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 = + case (findCon cons x) of + Val emb rec kids -> + foldl_l (\ca a b -> (gsumD ca b) + a) 0 rec kids +gsumR1 _ x = 0 + +instance GSum a => Sat (GSumD a) where + dict = GSumD gsum + +instance GSum Float +instance GSum Int +instance GSum Bool +instance GSum () +instance GSum Integer +instance GSum Char +instance GSum Double +instance (GSum a, GSum b) => GSum (a,b) +instance (GSum a) => GSum [a] + +-------------------- Zero ------------------------------ +-- | Create a zero element of a type +class (Rep1 ZeroD a) => Zero a where + zero :: a + zero = zeroR1 rep1 + +data ZeroD a = ZD { zeroD :: a } + +instance Zero a => Sat (ZeroD a) where + dict = ZD zero + +zeroR1 :: R1 ZeroD a -> a +zeroR1 Int1 = minBound +zeroR1 Char1 = minBound +zeroR1 (Arrow1 z1 z2) = \x -> 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 IOError1 = userError "Default Error" +zeroR1 r1 = error ("No zero element of type: " ++ show r1) + +instance Zero Int +instance Zero Char +instance (Zero a, Zero b) => Zero (a -> b) +instance Zero Integer +instance Zero Float +instance Zero Double +instance Zero IOError + +instance Zero () +instance Zero Bool +instance (Zero a, Zero b) => Zero (a,b) +instance Zero a => Zero [a] + +---------- Generate ------------------------------ + +data GenerateD a = GenerateD { generateD :: Int -> [a] } + +-- | Generate elements of a type up to a certain depth +class Rep1 GenerateD a => Generate a where + generate :: Int -> [a] + generate = generateR1 rep1 + +instance Generate a => Sat (GenerateD a) where + dict = GenerateD generate + +genEnum :: (Enum a) => Int -> [a] +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 = + [ to emb l | (Con emb rec) <- cons, + l <- fromTupM (\x -> generateD x (d-1)) rec] + +instance Generate Int +instance Generate Char +instance Generate Integer +instance Generate Float +instance Generate Double + +instance Generate () +instance (Generate a, Generate b) => Generate (a,b) +instance Generate a => Generate [a] + +------------ Enumerate ------------------------------- +-- note that this is not the same as the Enum class in the standard prelude + +data EnumerateD a = EnumerateD { enumerateD :: [a] } + +instance Enumerate a => Sat (EnumerateD a) where + dict = EnumerateD { enumerateD = enumerate } + +-- | enumerate the elements of a type, in DFS order. +class Rep1 EnumerateD a => Enumerate a where + enumerate :: [a] + enumerate = enumerateR1 rep1 + +enumerateR1 :: R1 EnumerateD a -> [a] +enumerateR1 Int1 = [minBound .. (maxBound::Int)] +enumerateR1 Char1 = [minBound .. (maxBound::Char)] +enumerateR1 (Data1 dt cons) = enumerateCons cons + +enumerateCons :: [Con EnumerateD a] -> [a] +enumerateCons (Con emb rec:rest) = (map (to emb) (fromTupM enumerateD rec)) ++ (enumerateCons rest) +enumerateCons [] = [] + +----------------- Shrink (from SYB III) ------------------------------- + +data ShrinkD a = ShrinkD { shrinkD :: a -> [a] } + +instance Shrink a => Sat (ShrinkD a) where + dict = ShrinkD { shrinkD = shrink } + +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 dict x = M x ((shrinkD dict) x) + +data M a = M a [a] + +instance Monad M where + return x = M x [] + (M x xs) >>= k = M r (rs1 ++ rs2) + where + M r rs1 = k x + rs2 = [r | x <- xs, let M r _ = k x] + +instance Shrink Int +instance Shrink a => Shrink [a] +instance Shrink Char +instance Shrink () +instance (Shrink a, Shrink b) => Shrink (a,b) + +------------ Reduce ------------------------------- + +data RreduceD b a = RreduceD { rreduceD :: a -> b -> b } +data LreduceD b a = LreduceD { lreduceD :: b -> a -> b } + +class Rep1 (RreduceD b) a => Rreduce b a where + rreduce :: a -> b -> b + rreduce = rreduceR1 rep1 + +class Rep1 (LreduceD b) a => Lreduce b a where + lreduce :: b -> a -> b + lreduce = lreduceR1 rep1 + +instance Rreduce b a => Sat (RreduceD b a) where + dict = RreduceD { rreduceD = rreduce } +instance Lreduce b a => Sat (LreduceD b a) where + 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 + +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 + +-- Instances for standard types +instance Lreduce b Int +instance Lreduce b () +instance Lreduce b Char +instance Lreduce b Bool +instance (Lreduce c a, Lreduce c b) => Lreduce c (a,b) +instance Lreduce c a => Lreduce c[a] + +instance Rreduce b Int +instance Rreduce b () +instance Rreduce b Char +instance Rreduce b Bool +instance (Rreduce c a, Rreduce c b) => Rreduce c (a,b) +instance Rreduce c a => Rreduce c[a] + +-------------------- Fold ------------------------------- +class Fold f where + foldRight :: Rep a => (a -> b -> b) -> f a -> b -> b + foldLeft :: Rep a => (b -> a -> b) -> b -> f a -> b + +crush :: (Rep a, Fold t) => (a -> a -> a) -> a -> t a -> a +crush op = foldLeft op + +gproduct :: (Rep a, Num a, Fold t) => t a -> a +gproduct t = foldLeft (*) 1 t + +gand :: (Fold t) => t Bool -> Bool +gand t = foldLeft (&&) True t + +gor :: (Fold t) => t Bool -> Bool +gor t = foldLeft (||) False t + +flatten :: (Rep a, Fold t) => t a -> [a] +flatten t = foldRight (:) t [] + +count :: (Rep a, Fold t) => t a -> Int +count t = foldRight (const (+1)) t 0 + +comp :: (Rep a, Fold t) => t (a -> a) -> a -> a +comp t = foldLeft (.) id t + +gconcat :: (Rep a, Fold t) => t [a] -> [a] +gconcat t = foldLeft (++) [] t + +gall :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool +gall p t = foldLeft (\a b -> a && p b) True t + +gany :: (Rep a, Fold t) => (a -> Bool) -> t a -> Bool +gany p t = foldLeft (\a b -> a || p b) False t + +gelem :: (Rep a, Eq a, Fold t) => a -> t a -> Bool +gelem x t = foldRight (\a b -> a == x || b) t False + + +instance Fold [] where + foldRight op = rreduceR1 (rList1 (RreduceD { rreduceD = op }) + (RreduceD { rreduceD = foldRight op })) + foldLeft op = lreduceR1 (rList1 (LreduceD { lreduceD = op }) + (LreduceD { lreduceD = foldLeft op })) + diff --git a/Data/RepLib/PreludeLib.hs b/Data/RepLib/PreludeLib.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/PreludeLib.hs @@ -0,0 +1,205 @@ +-- OPTIONS -fglasgow-exts -fallow-undecidable-instances +{-# LANGUAGE TemplateHaskell, UndecidableInstances #-} + +----------------------------------------------------------------------------- +-- +-- Module : RepLib.PreludeLib +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- +----------------------------------------------------------------------------- + + +-- | The module PreludeLib contains generic operations to derive members of the standard +-- prelude classess: Eq, Bounded, Compare, Show (TODO: add Enum and Read) +-- +-- Although these classes may already be automatically derived via the +-- "deriving" mechanism, this module is included for two reasons: +-- +-- * Deriving only works when datatypes are defined. This library +-- allows instances of these classes to be generated anywhere. For +-- example, suppose some other module contains the definition of the +-- datatype T and exposes all of its constructors, but, frustratingly, +-- does not derive an instance of the Show class. +-- +-- You could define a Show instance of 'T' in your own module with the +-- following code: +-- +-- > import RepLib +-- > +-- > (repr1 ''T) -- make the Rep1 instance of T available +-- > +-- > instance Show T where +-- > showsPrec = showsPrecR1 rep1 -- showsPrecR1 is defined in this module + -- +-- * This library also serves as a model for generic functions that are +-- slight modifications to these prelude operations. For example, if you +-- wanted to define reverse lexicographic ordering or an XML pretty +-- printer for datatypes, you might start here. This library is also a +-- good place to start learning how to define your own generic +-- operations, because the behavior of these operations should match the +-- deriving mechanism specified by Haskell 98. +-- +module Data.RepLib.PreludeLib ( + EqD, + eqR1, + OrdD, + compareR1, + BoundedD, + minBoundR1, + maxBoundR1, + ShowD, + showsPrecR1 +)where + +import Data.RepLib.R +import Data.RepLib.R1 +import Data.RepLib.RepAux + +--- Polymorphic equality ------------------------- + +data EqD a = EqD { eqD :: a -> a -> Bool } +instance Eq a => Sat (EqD a) where + dict = EqD (==) + +-- | Polymorphic equality, given an R1 representation +eqR1 :: R1 EqD a -> a -> a -> Bool +eqR1 Int1 = (==) +eqR1 Char1 = (==) +eqR1 Integer1 = (==) +eqR1 Float1 = (==) +eqR1 Double1 = (==) +eqR1 (Data1 _ cons) = \x y -> + let loop (Con rcd rec : rest) = + case (from rcd x, from rcd y) of + (Just p1, Just p2) -> eqRL1 rec p1 p2 + (Nothing, Nothing) -> loop rest + (_,_) -> False + in loop cons +eqR1 r1 = error ("eqR1 undefined for " ++ show r1) + +eqRL1 :: MTup EqD l -> l -> l -> Bool +eqRL1 MNil Nil Nil = True +eqRL1 (r :+: rl) (p1 :*: t1) (p2 :*: t2) = + eqD r p1 p2 && eqRL1 rl t1 t2 + +------------ Ord ------------------------------- + +-- compare :: a -> a -> Ordering is a minimal instance +-- of the Ord class + +data OrdD a = OrdD { compareD :: a -> a -> Ordering } + +instance Ord a => Sat (OrdD a) where + dict = OrdD { compareD = compare } + +lexord :: Ordering -> Ordering -> Ordering +lexord LT ord = LT +lexord EQ ord = ord +lexord GT ord = 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 -> + 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 + (Nothing, Nothing) -> loop rest + in loop cons +compareR1 r1 = error ("compareR1 not supported for " ++ show r1) + +compareTup :: MTup OrdD l -> l -> l -> Ordering +compareTup MNil Nil Nil = EQ +compareTup (x :+: xs) (y :*: ys) (z :*: zs) = + lexord (compareD x y z) (compareTup xs ys zs) + +------------ Bounded ------------------------------ + +data BoundedD a = BoundedD { minBoundD :: a, maxBoundD :: a } + +instance Bounded a => Sat (BoundedD a) where + dict = BoundedD { minBoundD = minBound, maxBoundD = maxBound } + +-- | To generate the Bounded class +minBoundR1 :: R1 BoundedD a -> a +minBoundR1 Int1 = minBound +minBoundR1 Char1 = minBound +minBoundR1 (Data1 dt (Con emb rec:rest)) = 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) = + case last cons of (Con emb rec) -> to emb (fromTup maxBoundD rec) +maxBoundR1 r1 = error ("maxBoundR1 not supported for " ++ show r1) + +-------------------- Show ------------------------------------- +-- Inspired by the Generic Haskell implementation +-- Current version doesn't correctly handle fixity + +data ShowD a = ShowD { showsPrecD :: Int -> a -> ShowS } + +instance Show a => Sat (ShowD a) where + dict = ShowD { showsPrecD = showsPrec } + +getFixity :: Emb a b -> Int +getFixity c = case fixity c of + Nonfix -> 0 + Infix i -> i + Infixl i -> i + Infixr i -> i + +-- | Minimal completion of the show class +showsPrecR1 :: R1 ShowD a -> + Int -> -- precendence level + a -> -- value to be shown + ShowS +showsPrecR1 (Data1 (DT str _) cons) = \p a -> + case (findCon cons a) of + Val c rec kids -> + case (labels c) of + Just labs -> par $ showString (name c) . + showString "{" . + showRecord rec kids labs . + showString "}" + Nothing -> par $ showString (name c) . + maybespace . + showKids rec kids + where par = showParen (p > p' && conArity > 0) + p' = getFixity c + maybespace = if conArity == 0 then id else (' ':) + conArity = foldr_l (\_ _ i -> 1 + i) 0 rec kids + + 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 :+: rs) (a :*: aa) (l : ls) = + showString l . ('=':) . showKid r a . showString (", ") . showRecord rs aa ls + showRecord _ _ _ = error ("Incorrect representation: " ++ + "wrong number of labels in record type") + + showKids :: MTup ShowD l -> l -> ShowS + showKids MNil Nil = id + showKids (r :+: MNil) (x :*: Nil) = showsPrecD r (p'+1) x + showKids (r :+: cl) (x :*: l) = showsPrecD r (p'+1) x . (' ':) . (showKids cl l) + +showsPrecR1 Int1 = showsPrec +showsPrecR1 Char1 = showsPrec +showsPrecR1 Integer1 = showsPrec +showsPrecR1 Float1 = showsPrec +showsPrecR1 Double1 = showsPrec +showsPrecR1 r1 = error ("showsPrecR1 not supported for " ++ show r1) + + diff --git a/Data/RepLib/PreludeReps.hs b/Data/RepLib/PreludeReps.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/PreludeReps.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, + FlexibleInstances, MultiParamTypeClasses + #-} +----------------------------------------------------------------------------- +-- | +-- Module : RepLib.PreludeReps +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- +-- Automatically derive representations for prelude types +-- +----------------------------------------------------------------------------- +module Data.RepLib.PreludeReps where + +import Data.RepLib.R +import Data.RepLib.R1 +import Data.RepLib.Derive +import Language.Haskell.TH + +$(derive [''Bool, + ''Maybe, + ''Either, + ''Ordering, + tupleTypeName 3, + tupleTypeName 4, + tupleTypeName 5, + tupleTypeName 6, + tupleTypeName 7]) + + diff --git a/Data/RepLib/R.hs b/Data/RepLib/R.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/R.hs @@ -0,0 +1,231 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification, + TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances, + ScopedTypeVariables + #-} +----------------------------------------------------------------------------- +-- | +-- Module : Data.RepLib.R +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- +-- +----------------------------------------------------------------------------- + +module Data.RepLib.R where + +import Data.List + + +data R a where + Int :: R Int + Char :: R Char + Integer :: R Integer + Float :: R Float + Double :: R Double + Rational:: R Rational + IOError :: R IOError + IO :: (Rep a) => R a -> R (IO a) + Arrow :: (Rep a, Rep b) => R a -> R b -> R (a -> b) + Data :: DT -> [Con R a] -> R a + +data Emb l a = Emb { to :: l -> a, + from :: a -> Maybe l, + labels :: Maybe [String], + name :: String, + fixity :: Fixity + } + +data Fixity = Nonfix + | Infix { prec :: Int } + | Infixl { prec :: Int } + | Infixr { prec :: Int } + + +data DT = forall l. DT String (MTup R l) +data Con r a = forall l. Con (Emb l a) (MTup r l) + + +data Nil = Nil +data a :*: l = a :*: l +infixr 7 :*: + +data MTup r l where + MNil :: MTup ctx Nil + (:+:) :: (Rep a) => r a -> MTup r l -> MTup r (a :*: l) + +infixr 7 :+: + +class Rep a where rep :: R a + +------ Showing representations (rewrite this with showsPrec?) + +instance Show (R a) where + show Int = "Int" + show Char = "Char" + show Integer = "Integer" + show Float = "Float" + show Double = "Double" + show Rational= "Rational" + show (IO t) = "(IO " ++ show t ++ ")" + show IOError = "IOError" + show (Arrow r1 r2) = + "(" ++ (show r1) ++ " -> " ++ (show r2) ++ ")" + show (Data dt _) = + "(Data" ++ show dt ++ ")" + +instance Show DT where + show (DT str reps) = str ++ show reps + +instance Show (MTup R l) where + show MNil = "" + show (r :+: MNil) = show r + show (r :+: rs) = " " ++ show r ++ show rs + +instance Eq (R a) where + r1 == r2 = True + + +--- Representations for Haskell Prelude types + +instance Rep Int where rep = Int +instance Rep Char where rep = Char +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 b) => Rep (a -> b) where rep = Arrow rep rep + +-- Booleans +{- +rTrueEmb :: Emb Nil Bool +rTrueEmb = Emb { to = \Nil -> True, + from = \x -> if x then Just Nil else Nothing, + labels = Nothing, + name = "True", + fixity = Nonfix + } + +rFalseEmb :: Emb Nil Bool +rFalseEmb = Emb { to = \Nil -> False, + from = \x -> if x then Nothing else Just Nil, + labels = Nothing, + name = "False", + fixity = Nonfix + } + +rBool :: R Bool +rBool = Data (DT "Bool" MNil) [Con rTrueEmb, Con rFalseEmb] + +instance Rep Bool where rep = rBool + -} + +-- Unit + +rUnitEmb :: Emb Nil () +rUnitEmb = Emb { to = \Nil -> (), + from = \() -> Just Nil, + labels = Nothing, + name = "()", + fixity = Nonfix } + +rUnit :: R () +rUnit = Data (DT "()" MNil) + [Con rUnitEmb MNil] + +instance Rep () where rep = rUnit + +-- Tuples + +instance (Rep a, Rep b) => Rep (a,b) where + rep = rTup2 + +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 ] + +rPairEmb :: Emb (a :*: b :*: Nil) (a,b) +rPairEmb = + Emb { to = \( t1 :*: t2 :*: Nil) -> (t1,t2), + from = \(a,b) -> Just (a :*: b :*: Nil), + labels = Nothing, + name = "(,)", + fixity = Nonfix -- ??? + } + +-- Lists +rList :: forall a. Rep a => R [a] +rList = Data (DT "[]" ((rep :: R a) :+: MNil)) + [ Con rNilEmb MNil, Con rConsEmb ((rep :: R a) :+: rList :+: MNil) ] + +rNilEmb :: Emb Nil [a] +rNilEmb = Emb { to = \Nil -> [], + from = \x -> case x of + (x:xs) -> Nothing + [] -> Just Nil, + labels = Nothing, + name = "[]", + fixity = Nonfix + + } + +rConsEmb :: Emb (a :*: [a] :*: Nil) [a] +rConsEmb = + Emb { + to = (\ (hd :*: tl :*: Nil) -> (hd : tl)), + from = \x -> case x of + (hd : tl) -> Just (hd :*: tl :*: Nil) + [] -> Nothing, + labels = Nothing, + name = ":", + fixity = Nonfix -- ??? + } + +instance Rep a => Rep [a] where + rep = rList + +{- +-- Maybe representation + +rJust :: Rep a => Con (Maybe a) +rJust = Con (rJustEmb) + +rJustEmb :: Emb (a :*: Nil) (Maybe a) +rJustEmb = Emb + { to = (\(x :*: Nil) -> Just x), + from = \x -> case x of + (Just y) -> Just (y :*: Nil) + Nothing -> Nothing, + labels = Nothing, + name = "Just" + } + +rNothing :: Con (Maybe a) +rNothing = Con rNothingEmb + +rNothingEmb :: Emb Nil (Maybe a) +rNothingEmb = Emb + { to = \Nil -> Nothing, + from = \x -> case x of + Nothing -> Just Nil + _ -> Nothing, + labels = Nothing, + name = "Nothing" + } + +rMaybe :: forall a. Rep a => R (Maybe a) +rMaybe = Data (DT "Maybe" ((rep :: R a) :+: MNil)) + [rJust, rNothing] + +instance Rep a => Rep (Maybe a) where + rep = rMaybe +-} +-- Ordering +-- Either + diff --git a/Data/RepLib/R1.hs b/Data/RepLib/R1.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/R1.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, GADTs, ScopedTypeVariables, + MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances + #-} + +----------------------------------------------------------------------------- +-- | +-- Module : RepLib.R1 +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- +-- +----------------------------------------------------------------------------- + +module Data.RepLib.R1 where + +import Data.RepLib.R +import Data.List + +---------- Basic infrastructure + +data R1 ctx a where + Int1 :: R1 ctx Int + Char1 :: R1 ctx Char + Integer1 :: R1 ctx Integer + Float1 :: R1 ctx Float + Double1 :: R1 ctx Double + Rational1 :: R1 ctx Rational + IOError1 :: R1 ctx IOError + IO1 :: (Rep a) => ctx a -> R1 ctx (IO a) + Arrow1 :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b) + Data1 :: DT -> [Con ctx a] -> R1 ctx a + +class Sat a where dict :: a + +class Rep a => Rep1 ctx a where rep1 :: R1 ctx a + +instance Show (R1 c a) where + show Int1 = "Int1" + show Char1 = "Char1" + show Integer1 = "Integer1" + show Float1 = "Float1" + show Double1 = "Double1" + show Rational1 = "Rational1" + show IOError1 = "IOError1" + show (IO1 cb) = "(IO1 " ++ show (getRep cb) ++ ")" + show (Arrow1 cb cc) = "(Arrow1 " ++ show (getRep cb) ++ " " ++ show (getRep cc) ++ ")" + show (Data1 dt _) = "(Data1 " ++ show dt ++ ")" + +-- | Access a representation, given a proxy +getRep :: Rep b => c b -> R b +getRep cb = rep + +-- | Transform a parameterized rep to a vanilla rep +toR :: R1 c a -> R a +toR Int1 = Int +toR Char1 = Char +toR Integer1 = Integer +toR Float1 = Float +toR Double1 = Double +toR Rational1 = Rational +toR IOError1 = IOError +toR (Arrow1 t1 t2) = Arrow (getRep t1) (getRep t2) +toR (IO1 t1) = IO (getRep t1) +toR (Data1 dt cons) = (Data dt (map toCon cons)) + where toCon (Con emb rec) = Con emb (toRs rec) + toRs :: MTup c a -> MTup R a + toRs MNil = MNil + toRs (c :+: l) = (getRep c :+: toRs l) + +--------------- Representations of Prelude types + +instance Rep1 ctx Int where rep1 = Int1 +instance Rep1 ctx Char where rep1 = Char1 +instance Rep1 ctx Integer where rep1 = Integer1 +instance Rep1 ctx Float where rep1 = Float1 +instance Rep1 ctx Double where rep1 = Double1 +instance Rep1 ctx IOError where rep1 = IOError1 +instance Rep1 ctx Rational where rep1 = Rational1 +instance (Rep a, Sat (ctx a)) => + Rep1 ctx (IO a) where rep1 = IO1 dict +instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => + Rep1 ctx (a -> b) where rep1 = Arrow1 dict dict + + +-- Data structures + +-- unit +instance Rep1 ctx () where + rep1 = Data1 (DT "()" MNil) + [Con rUnitEmb MNil] + +-- pairs +rTup2_1 :: forall a b ctx. (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a,b) +rTup2_1 ca cb = + case (rep :: R (a,b)) of + Data rdt _ -> Data1 rdt + [Con rPairEmb (ca :+: cb :+: MNil)] + +instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a,b) where + rep1 = rTup2_1 dict dict + + +-- Lists +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 ] + +rNil1 :: Con ctx [a] +rNil1 = Con rNilEmb MNil + +rCons1 :: Rep a => ctx a -> ctx [a] -> Con ctx [a] +rCons1 ca cl = 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/Data/RepLib/RepAux.hs b/Data/RepLib/RepAux.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/RepAux.hs @@ -0,0 +1,234 @@ +{-# LANGUAGE TemplateHaskell, UndecidableInstances, MagicHash, + ScopedTypeVariables, GADTs, Rank2Types + #-} +----------------------------------------------------------------------------- +-- | +-- Module : RepAux +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- Auxiliary operations to aid in the definition of type-indexed functions +-- +----------------------------------------------------------------------------- +module Data.RepLib.RepAux ( + -- ** Casting operations + compR, cast, castR, gcast, gcastR, + + -- ** Operations for heterogeneous lists + findCon, Val(..), foldl_l, foldr_l, map_l, mapQ_l, mapM_l, fromTup, fromTupM, toList, + + -- ** SYB style operations (Rep) + Traversal, Query, MapM, + gmapT, gmapQ, gmapM, + + -- ** SYB style operations (Rep1) + Traversal1, Query1, MapM1, + gmapT1, gmapQ1, gmapM1, + + -- ** SYB Reloaded + Typed(..),Spine(..), toSpine, fromSpine +) where + +import Data.RepLib.R +import Data.RepLib.R1 +import GHC.Base (unsafeCoerce#) + + +------ Casting + +-- | Determine if two reps are for the same type +compR :: R a -> R b -> Bool +compR Int Int = True +compR Char Char = True +compR Float Float = True +compR Integer Integer = True +compR Double Double = True +compR (IO t1) (IO t2) = compR t1 t2 +compR IOError IOError = True +compR (Arrow t1 t2) (Arrow s1 s2) = compR t1 s1 && compR t2 s2 +compR (Data rc1 _) (Data rc2 _) = compDT rc1 rc2 +compR _ _ = False + +compDT :: DT -> DT -> Bool +compDT (DT str1 rt1) (DT str2 rt2) = str1 == str2 && compRTup rt1 rt2 + +compRTup :: MTup R t1 -> MTup R t2 -> Bool +compRTup MNil MNil = True +compRTup (r1 :+: rt1) (r2 :+: rt2) = compR r1 r2 && compRTup rt1 rt2 + +-- | The type-safe cast operation, explicit arguments +castR :: R a -> R b -> a -> Maybe b +castR (ra::R a) (rb::R b) = + if compR ra rb then \(x::a) -> Just (unsafeCoerce# x::b) else \x -> 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 + +-- | Leibniz equality between types, explicit representations +gcastR :: forall a b c. R a -> R b -> c a -> Maybe (c b) +gcastR ra rb = if compR ra rb + then \(x :: c a) -> Just (unsafeCoerce# x :: c b) + else \x -> Nothing + +-- | Leibniz equality between types, implicity representations +gcast :: forall a b c. (Rep a, Rep b) => c a -> Maybe (c b) +gcast = gcastR (rep :: R a) (rep :: R b) + +--------- 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 + +-- | 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 + +-- | 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 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 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 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 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 f (ca :+: cl) (a :*: l) = do + x1 <- f ca a + x2 <- mapM_l f cl l + return (x1 :*: x2) + +-- | Generate a heterogeneous list from metadata +fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l +fromTup f 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 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 f (b :+: l) = f b : toList f l + +--------------------- SYB style operations -------------------------- + +-- | A SYB style traversal +type Traversal = forall a. Rep a => a -> a + +-- | Map a traversal across the kids of a data structure +gmapT :: forall a. Rep a => Traversal -> a -> a +gmapT t = + case (rep :: R a) of + (Data dt cons) -> \x -> + case (findCon cons x) of + Val emb reps ys -> to emb (map_l (const t) reps ys) + _ -> id + + +-- | SYB style query type +type Query r = forall a. Rep a => a -> r + +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 + _ -> const [] + + +-- | SYB style monadic map type +type MapM m = forall a. Rep a => a -> m a + +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 + Val emb reps ys -> do l <- mapM_l (const m) reps ys + return (to emb l) + _ -> return + + +-------------- Generalized SYB ops --------------------------- + +type Traversal1 ctx = forall a. Rep a => ctx a -> a -> a +gmapT1 :: forall a ctx. (Rep1 ctx a) => Traversal1 ctx -> a -> a +gmapT1 t = + case (rep1 :: R1 ctx a) of + (Data1 dt cons) -> \x -> + case (findCon cons x) of + Val emb recs kids -> to emb (map_l t recs kids) + _ -> id + +type Query1 ctx r = forall a. Rep a => ctx a -> a -> r +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 + _ -> 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 + Val emb rec ys -> do l <- mapM_l m rec ys + return (to emb l) + _ -> return + +-------------- Spine from SYB Reloaded --------------------------- + +data Typed a = a ::: R a +infixr 7 ::: + +data Spine a where + Constr :: a -> Spine a + (:<>) :: Spine (a -> b) -> Typed a -> Spine b + +toSpineR :: R a -> a -> Spine a +toSpineR (Data _ cons) a = + case (findCon cons a) of + Val emb reps kids -> toSpineRl reps kids (to emb) +toSpineR _ a = Constr a + +toSpineRl :: MTup R l -> l -> (l -> a) -> Spine a +toSpineRl MNil Nil into = Constr (into Nil) +toSpineRl (ra :+: rs) (a :*: l) into = + (toSpineRl rs l into') :<> (a ::: ra) + where into' tl1 x1 = into (x1 :*: tl1) + +toSpine :: Rep a => a -> Spine a +toSpine = toSpineR rep + +fromSpine :: Spine a -> a +fromSpine (Constr x) = x +fromSpine (x :<> (y:::_)) = fromSpine x y + diff --git a/Data/RepLib/SYB/Aliases.hs b/Data/RepLib/SYB/Aliases.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/SYB/Aliases.hs @@ -0,0 +1,374 @@ +{-# OPTIONS -fglasgow-exts #-} + +----------------------------------------------------------------------------- +-- | +-- Module : RAliases +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- + +-- This module is derived from Data.Generics.Aliases +-- +-- The present module provides a number of declarations for typical +-- generic function types, corresponding type case, and others. +-- +-- +----------------------------------------------------------------------------- +module Data.RepLib.SYB.Aliases ( + + -- * Combinators to \"make\" generic functions via cast + mkT, mkQ, mkM, mkMp, mkR, + ext0, extT, extQ, extM, extMp, extB, extR, + + -- * Type synonyms for generic function types + GenericT, + GenericQ, + GenericM, + GenericB, + GenericR, + Generic, + Generic'(..), + GenericT'(..), + GenericQ'(..), + GenericM'(..), + + -- * Inredients of generic functions + orElse, + + -- * Function combinators on generic functions + recoverMp, + recoverQ, + choiceMp, + choiceQ + + -- * Type extension for unary type constructors +-- ext1T, +-- ext1M, +-- ext1Q, +-- ext1R + + ) where + +import Control.Monad +import Data.RepLib.R +import Data.RepLib.RepAux + +-- Derived from Data.Generics.Aliases +-- Only modification: "Data" and "Typeable" classes become "Rep" class +-- otherwise import our version of the libraries + +------------------------------------------------------------------------------ +-- +-- Combinators to "make" generic functions +-- We use type-safe cast in a number of ways to make generic functions. +-- +------------------------------------------------------------------------------ + +-- | Make a generic transformation; +-- start from a type-specific case; +-- preserve the term otherwise +-- +mkT :: ( Rep a + , Rep b + ) + => (b -> b) + -> a + -> a +mkT = extT id + + +-- | Make a generic query; +-- start from a type-specific case; +-- return a constant otherwise +-- +mkQ :: ( Rep a + , Rep b + ) + => r + -> (b -> r) + -> a + -> r +(r `mkQ` br) a = case cast a of + Just b -> br b + Nothing -> r + + +-- | Make a generic monadic transformation; +-- start from a type-specific case; +-- resort to return otherwise +-- +mkM :: ( Monad m + , Rep a + , Rep b + ) + => (b -> m b) + -> a + -> m a +mkM = extM return + + +{- + +For the remaining definitions, we stick to a more concise style, i.e., +we fold maybies with "maybe" instead of case ... of ..., and we also +use a point-free style whenever possible. + +-} + + +-- | Make a generic monadic transformation for MonadPlus; +-- use \"const mzero\" (i.e., failure) instead of return as default. +-- +mkMp :: ( MonadPlus m + , Rep a + , Rep b + ) + => (b -> m b) + -> a + -> m a +mkMp = extM (const mzero) + + +-- | Make a generic builder; +-- start from a type-specific ase; +-- resort to no build (i.e., mzero) otherwise +-- +mkR :: ( MonadPlus m + , Rep a + , Rep b + ) + => m b -> m a +mkR f = mzero `extR` f + + +-- | Flexible type extension +ext0 :: (Rep a, Rep b) => c a -> c b -> c a +ext0 def ext = maybe def id (gcast ext) + + +-- | Extend a generic transformation by a type-specific case +extT :: ( Rep a + , Rep b + ) + => (a -> a) + -> (b -> b) + -> a + -> a +extT def ext = unT ((T def) `ext0` (T ext)) + + +-- | Extend a generic query by a type-specific case +extQ :: ( Rep a + , Rep b + ) + => (a -> q) + -> (b -> q) + -> a + -> q +extQ f g a = maybe (f a) g (cast a) + + +-- | Extend a generic monadic transformation by a type-specific case +extM :: ( Monad m + , Rep a + , Rep b + ) + => (a -> m a) -> (b -> m b) -> a -> m a +extM def ext = unM ((M def) `ext0` (M ext)) + + +-- | Extend a generic MonadPlus transformation by a type-specific case +extMp :: ( MonadPlus m + , Rep a + , Rep b + ) + => (a -> m a) -> (b -> m b) -> a -> m a +extMp = extM + + +-- | Extend a generic builder +extB :: ( Rep a + , Rep b + ) + => a -> b -> a +extB a = maybe a id . cast + + +-- | Extend a generic reader +extR :: ( Monad m + , Rep a + , Rep b + ) + => m a -> m b -> m a +extR def ext = unR ((R def) `ext0` (R ext)) + + + +------------------------------------------------------------------------------ +-- +-- Type synonyms for generic function types +-- +------------------------------------------------------------------------------ + + +-- | Generic transformations, +-- i.e., take an \"a\" and return an \"a\" +-- +type GenericT = forall a. Rep a => a -> a + + +-- | Generic queries of type \"r\", +-- i.e., take any \"a\" and return an \"r\" +-- +type GenericQ r = forall a. Rep a => a -> r + + +-- | Generic monadic transformations, +-- i.e., take an \"a\" and compute an \"a\" +-- +type GenericM m = forall a. Rep a => a -> m a + + +-- | Generic builders +-- i.e., produce an \"a\". +-- +type GenericB = forall a. Rep a => a + + +-- | Generic readers, say monadic builders, +-- i.e., produce an \"a\" with the help of a monad \"m\". +-- +type GenericR m = forall a. Rep a => m a + + +-- | The general scheme underlying generic functions +-- assumed by gfoldl; there are isomorphisms such as +-- GenericT = Generic T. +-- +type Generic c = forall a. Rep a => a -> c a + + +-- | Wrapped generic functions; +-- recall: [Generic c] would be legal but [Generic' c] not. +-- +data Generic' c = Generic' { unGeneric' :: Generic c } + + +-- | Other first-class polymorphic wrappers +newtype GenericT' = GT { unGT :: Rep a => a -> a } +newtype GenericQ' r = GQ { unGQ :: GenericQ r } +newtype GenericM' m = GM { unGM :: Rep a => a -> m a } + + +-- | Left-biased choice on maybies +orElse :: Maybe a -> Maybe a -> Maybe a +x `orElse` y = case x of + Just _ -> x + Nothing -> y + + +{- + +The following variations take "orElse" to the function +level. Furthermore, we generalise from "Maybe" to any +"MonadPlus". This makes sense for monadic transformations and +queries. We say that the resulting combinators modell choice. We also +provide a prime example of choice, that is, recovery from failure. In +the case of transformations, we recover via return whereas for +queries a given constant is returned. + +-} + +-- | Choice for monadic transformations +choiceMp :: MonadPlus m => GenericM m -> GenericM m -> GenericM m +choiceMp f g x = f x `mplus` g x + + +-- | Choice for monadic queries +choiceQ :: MonadPlus m => GenericQ (m r) -> GenericQ (m r) -> GenericQ (m r) +choiceQ f g x = f x `mplus` g x + + +-- | Recover from the failure of monadic transformation by identity +recoverMp :: MonadPlus m => GenericM m -> GenericM m +recoverMp f = f `choiceMp` return + + +-- | Recover from the failure of monadic query by a constant +recoverQ :: MonadPlus m => r -> GenericQ (m r) -> GenericQ (m r) +recoverQ r f = f `choiceQ` const (return r) + + + +------------------------------------------------------------------------------ +-- +-- Type extension for unary type constructors +-- +------------------------------------------------------------------------------ + +{- + + +-- | Flexible type extension +ext1 :: (Rep a, Typeable1 t) + => c a + -> (forall a. Rep a => c (t a)) + -> c a +ext1 def ext = maybe def id (dataCast1 ext) + + +-- | Type extension of transformations for unary type constructors +ext1T :: (Rep d, Typeable1 t) + => (forall d. Rep d => d -> d) + -> (forall d. Rep d => t d -> t d) + -> d -> d +ext1T def ext = unT ((T def) `ext1` (T ext)) + + +-- | Type extension of monadic transformations for type constructors +ext1M :: (Monad m, Rep d, Typeable1 t) + => (forall d. Rep d => d -> m d) + -> (forall d. Rep d => t d -> m (t d)) + -> d -> m d +ext1M def ext = unM ((M def) `ext1` (M ext)) + + +-- | Type extension of queries for type constructors +ext1Q :: (Rep d, Typeable1 t) + => (d -> q) + -> (forall d. Rep d => t d -> q) + -> d -> q +ext1Q def ext = unQ ((Q def) `ext1` (Q ext)) + + +-- | Type extension of readers for type constructors +ext1R :: (Monad m, Rep d, Typeable1 t) + => m d + -> (forall d. Rep d => m (t d)) + -> m d +ext1R def ext = unR ((R def) `ext1` (R ext)) + +-} + +------------------------------------------------------------------------------ +-- +-- Type constructors for type-level lambdas +-- +------------------------------------------------------------------------------ + + +-- | The type constructor for transformations +newtype T x = T { unT :: x -> x } + +-- | 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/Data/RepLib/SYB/Schemes.hs b/Data/RepLib/SYB/Schemes.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/SYB/Schemes.hs @@ -0,0 +1,170 @@ +{-# OPTIONS -fglasgow-exts #-} + +----------------------------------------------------------------------------- +-- | +-- Module : RSchemes +-- Copyright : (c) The University of Pennsylvania 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- Derived from Data.Generics.Schemes +-- Only modification: "Data" class becomes "Rep" class +-- otherwise import our version of the libraries +-- For now, missing "somewhere" (lacking mapMp) +-- +----------------------------------------------------------------------------- + +module Data.RepLib.SYB.Schemes ( + + everywhere, + everywhere', + everywhereBut, + everywhereM, +-- somewhere, + everything, + listify, + something, + synthesize, + gsize, + glength, + gdepth, + gcount, + gnodecount, + gtypecount, + gfindtype + + ) where + +------------------------------------------------------------------------------ + + +import Data.RepLib.R +import Data.RepLib.RepAux +import Data.RepLib.SYB.Aliases +import Control.Monad + + +-- | Apply a transformation everywhere in bottom-up manner +everywhere :: (forall a. Rep a => a -> a) + -> (forall a. Rep a => a -> a) + +-- Use gmapT to recurse into immediate subterms; +-- recall: gmapT preserves the outermost constructor; +-- post-process recursively transformed result via f +-- +everywhere f = f . gmapT (everywhere f) + + +-- | Apply a transformation everywhere in top-down manner +everywhere' :: (forall a. Rep a => a -> a) + -> (forall a. Rep a => a -> a) + +-- Arguments of (.) are flipped compared to everywhere +everywhere' f = gmapT (everywhere' f) . f + + +-- | Variation on everywhere with an extra stop condition +everywhereBut :: GenericQ Bool -> GenericT -> GenericT + +-- Guarded to let traversal cease if predicate q holds for x +everywhereBut q f x + | q x = x + | otherwise = f (gmapT (everywhereBut q f) x) + + +-- | Monadic variation on everywhere +everywhereM :: Monad m => GenericM m -> GenericM m + +-- Bottom-up order is also reflected in order of do-actions +everywhereM f x = do x' <- gmapM (everywhereM f) x + f x' + + +-- | Apply a monadic transformation at least somewhere +-- somewhere :: MonadPlus m => GenericM m -> GenericM m + +-- We try "f" in top-down manner, but descent into "x" when we fail +-- at the root of the term. The transformation fails if "f" fails +-- everywhere, say succeeds nowhere. +-- +-- somewhere f x = f x `mplus` gmapMp (somewhere f) x + + +-- | Summarise all nodes in top-down, left-to-right order +everything :: (r -> r -> r) -> GenericQ r -> GenericQ r + +-- Apply f to x to summarise top-level node; +-- use gmapQ to recurse into immediate subterms; +-- use ordinary foldl to reduce list of intermediate results +-- +everything k f x + = foldl k (f x) (gmapQ (everything k f) x) + + +-- | Get a list of all entities that meet a predicate +listify :: Rep r => (r -> Bool) -> GenericQ [r] +listify p + = everything (++) ([] `mkQ` (\x -> if p x then [x] else [])) + + +-- | Look up a subterm by means of a maybe-typed filter +something :: GenericQ (Maybe u) -> GenericQ (Maybe u) + +-- "something" can be defined in terms of "everything" +-- when a suitable "choice" operator is used for reduction +-- +something = everything orElse + + +-- | Bottom-up synthesis of a data structure; +-- 1st argument z is the initial element for the synthesis; +-- 2nd argument o is for reduction of results from subterms; +-- 3rd argument f updates the synthesised data according to the given term +-- +synthesize :: s -> (s -> s -> s) -> GenericQ (s -> s) -> GenericQ s +synthesize z o f x = f x (foldr o z (gmapQ (synthesize z o f) x)) + + +-- | Compute size of an arbitrary data structure +gsize :: Rep a => a -> Int +gsize t = 1 + sum (gmapQ gsize t) + + +-- | Count the number of immediate subterms of the given term +glength :: GenericQ Int +glength = length . gmapQ (const ()) + + +-- | Determine depth of the given term +gdepth :: GenericQ Int +gdepth = (+) 1 . foldr max 0 . gmapQ gdepth + + +-- | Determine the number of all suitable nodes in a given term +gcount :: GenericQ Bool -> GenericQ Int +gcount p = everything (+) (\x -> if p x then 1 else 0) + + +-- | Determine the number of all nodes in a given term +gnodecount :: GenericQ Int +gnodecount = gcount (const True) + + +-- | Determine the number of nodes of a given type in a given term +gtypecount :: Rep a => a -> GenericQ Int +gtypecount (_::a) = gcount (False `mkQ` (\(_::a) -> True)) + + +-- | Find (unambiguously) an immediate subterm of a given type +gfindtype :: (Rep x, Rep y) => x -> Maybe y +gfindtype = singleton + . foldl unJust [] + . gmapQ (Nothing `mkQ` Just) + where + unJust l (Just x) = x:l + unJust l Nothing = l + singleton [s] = Just s + singleton _ = Nothing diff --git a/Data/RepLib/Unify.hs b/Data/RepLib/Unify.hs new file mode 100644 --- /dev/null +++ b/Data/RepLib/Unify.hs @@ -0,0 +1,244 @@ +{-# LANGUAGE UndecidableInstances, OverlappingInstances, IncoherentInstances, + ExistentialQuantification, ScopedTypeVariables, EmptyDataDecls, + MultiParamTypeClasses, FlexibleInstances, FlexibleContexts + #-} + +----------------------------------------------------------------------------- +-- +-- Module : Data.RepLib.Unify +-- Copyright : (c) Ben Kavanagh 2008 +-- License : BSD +-- +-- Maintainer : Ben Kavanagh (ben.kavanagh@gmail.com) +-- Stability : experimental +-- Portability : non-portable +-- +-- Generic unification with Replib +-- +----------------------------------------------------------------------------- + + +module Data.RepLib.Unify +where + +import Data.RepLib.R +import Data.RepLib.R1 +import Data.RepLib.RepAux +import Data.RepLib.PreludeReps +import Control.Monad +import Control.Monad.State +import Control.Monad.Error + +data Proxy a + + +----------------- Unification ------------------------- + +-- unify takes an equality constraint (from a pool of constraints) and processes it. +-- if there is a variable we do an occurs check and if passes add the assignment and apply +-- to the current substitution/constraints. otherwise it either matches leafs w/equality or decomposes +-- function terms (constructors) to produce additional constraints. So it takes a substitution +-- and a set of constraints and returns a new substitution, and a new set of constraints, +-- with the possibility of failure. + + +-- just use string errors for now. +type UnifyError = String + + +-- Error/State monad for unification. This version does not abstract the monad. +type UM n a b = ErrorT UnifyError (State (UnificationState n a)) b + + +data UnifySubD n a b = UnifySubD { unifyStepD :: Proxy (n, a) -> b -> b -> UM n a (), + substD:: n -> a -> b -> b, + occursCheckD :: n -> Proxy a -> b -> Bool} + +instance (Unify n a b, Subst n a b, Occurs n a b) => Sat (UnifySubD n a b) where + dict = UnifySubD {unifyStepD = unifyStep, substD = subst, occursCheckD = occursCheck} + + +data UConstraint n a = forall b. UC (UnifySubD n a b) b b +data UnificationState n a = UState {uConstraints :: [UConstraint n a], + uSubst :: [(n, a)]} + + + +-- Unification Step + +class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b where + unifyStep :: Proxy (n, a) -> b -> b -> UM n a () + +-- Generic unify instance +instance (Eq n, Show n, Show a, Show b, HasVar n a, Rep1 (UnifySubD n a) b) => Unify n a b where + unifyStep = unifyStepR1 rep1 + + +-- | Generic unifyStep. almost identical to polymorphic equality +unifyStepR1 :: (Eq n, Show n, Show a, Show b, HasVar n a) => R1 (UnifySubD n a) b -> Proxy (n, a) -> b -> b -> UM n a () +unifyStepR1 Int1 _ = unifyStepEq +unifyStepR1 Char1 _ = unifyStepEq +unifyStepR1 Integer1 _ = unifyStepEq +unifyStepR1 Float1 _ = unifyStepEq +unifyStepR1 Double1 _ = unifyStepEq +unifyStepR1 (Data1 _ cons) dum = + \ x y -> + let loop (Con rcd rec : rest) = + case (from rcd x, from rcd y) of + (Just p1, Just p2) -> addConstraintsRL1 rec dum p1 p2 + (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")) + + + +addConstraintsRL1 :: MTup (UnifySubD n a) l -> Proxy (n, a) -> l -> l -> UM n a () +addConstraintsRL1 MNil _ Nil Nil = return () +addConstraintsRL1 (r :+: rl) (dum :: Proxy (n, a)) (p1 :*: t1) (p2 :*: t2) = + do queueConstraint $ UC r p1 p2 + addConstraintsRL1 rl dum t1 t2 + + +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) + + +-- a a instance +instance (Eq n, Show n, Show a, HasVar n a, Rep1 (UnifySubD n a) a) => Unify n a a where + unifyStep (dum :: Proxy (n, a)) (a1::a) a2 = + case ((is_var a1) :: Maybe n, (is_var a2) :: Maybe n) of + (Just n1, Just n2) -> if n1 == n2 + then return () + else addSub n1 ((var n2) :: a); + (Just n1, _) -> addSub n1 a2 + (_, Just n2) -> addSub n2 a1 + (_, _) -> unifyStepR1 rep1 dum a1 a2 + where + addSub n t = extendSubstitution (n, t) + + +dequeueConstraint :: UM n a (Maybe (UConstraint n a)) +dequeueConstraint = do s <- get + case s of (UState [] _) -> return Nothing + (UState (x : xs) sub) -> do put $ UState xs sub + return $ Just x + +queueConstraint :: UConstraint n a -> UM n a () +queueConstraint eq = modify (\ (UState xs sub) -> (UState (eq : xs) sub)) + + +-- +-- I know of three ways to extend subst. +-- 1. Just extend the list. +-- this does not remove instances of the variable assigned from the remaining +-- substitution. This means that when doing occurs checks will +-- need to unfold the substitution as you step down the tree. This is done lazily +-- but repeat unfoldings will very often be necessary. +-- 2. Apply the sub everywhere in the current sub/constraints and then extend the list. This +-- Does unnecessary work by unfolding nodes that may never be examined but does not repeat +-- work. +-- 3. Just extend the list but construct the terms from references (graph datatype) so +-- that when unfolding substitution lazily during occurs check, no further unfolding will +-- be necessary once completed. This is more efficient but not as straightforward to +-- analyse. +-- +-- I use (2) + +extendSubstitution :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => (n, a) -> UM n a () -- (could fail with occurs check) +extendSubstitution asgn@((n :: n), (a :: a)) = + if (occursCheck n (undefined :: Proxy a) a) + then throwError $ "occurs check failed when extending sub with " ++ (show n) ++ " = " ++ (show a) + else do (UState xs sub) <- get + let sub' = [(n', subst n a a') | (n', a') <- sub] -- these might have side effects if we want to handle binding via freshmonad. + let xs' = [UC d (substD d n a b1) (substD d n a b2) | (UC d b1 b2) <- xs] + put (UState xs' (asgn : sub')) + + + + + + +-- Solving unification = 1) initialise problem, 2) run rewrites until no constraints or error. +solveUnification :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => [(a, a)] -> Maybe [(n, a)] +solveUnification (eqs :: [(a, a)]) = + case r of Left e -> error e + Right _ -> Just $ uSubst final + where + (r, final) = runState (runErrorT rwConstraints) (UState cs []) + 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 + rwConstraints + Nothing -> return () + + + +-- To offer this I have to turn on -fallow-overlapping-instances. This rejects the a a instance of the dictionary, +-- choosing the more general a b instance instead. Thus this can only be used when a /= b, for example Term, OuterTerm +-- in the example testcase. because the instances chosen for dict here are different than above I cannot reduce +-- solveUnification to a call to solveUnification'. Please forgive the code duplication. ugh. + +solveUnification' :: (HasVar n a, Eq n, Show n, Show a, Show b, Rep1 (UnifySubD n a) b) => Proxy (n, a) -> [(b, b)] -> Maybe [(n, a)] +solveUnification' (dum :: Proxy (n, a)) (eqs :: [(b, b)]) = + case r of Left e -> error e + Right _ -> Just $ uSubst final + where + (r, final) = runState (runErrorT rwConstraints) (UState cs []) + 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 + rwConstraints + Nothing -> return () + + + + +class HasVar a b where + is_var :: b -> Maybe a -- retrieve the name of a variable + var :: a -> b -- inject name as a variable + + + +-- Generic substitution without binding. (No freshness monad required) +-- substitute [a -> t] t'. +class Subst a t t' where + subst :: a -> t -> t' -> t' + +-- generic instance +instance Rep1 (UnifySubD a t) t' => Subst a t t' where + subst = substR1 rep1 + +-- 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' + +-- a a instance +instance (Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t where + subst a t t' = if is_var t' == Just a + then t + else gmapT1 (\cb b -> substD cb a t b) t' + + +-- Generic Occurs checking +class Occurs n a b where + occursCheck :: n -> Proxy a -> b -> Bool + +-- generic instance +instance Rep1 (UnifySubD n a) b => Occurs n a b where + occursCheck = occursCheckR1 rep1 + +-- 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 + +-- a a instance. +instance (Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a where + occursCheck n pa a = if is_var a == Just n + then True + else or $ gmapQ1 (\cb b -> occursCheckD cb n pa b) a + + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,31 @@ +Copyright (c) 2006, Stephanie Weirich +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of the University of Pennsylvania nor the names + of its contributors may be used to endorse or promote products + derived from this software without specific prior written + permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,44 @@ +----------------------------------------------------------------------------- +-- | +-- +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu, byorgey@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- RepLib +-- a library of derivable type classes based on representation types +-- +-- See http://www.cis.upenn.edu/~sweirich/RepLib for more information. +----------------------------------------------------------------------------- + +RepLib has been tested with GHC 6.8.3 and 6.10.3. + +This library contains the following modules: + +RepLib.R - Basic type representations +RepLib.R1 - Parameterized type representations +RepLib.Derive - Template Haskell code to automatically derive + representations of datatypes. +RepLIb.PreludeReps - Reps of Prelude types +RepLib.RepAux - Helper functions to define type-indexed functions + +RepLib.Lib - Examples of specializable type-indexed functions +RepLib.PreludeLib - Examples type-indexed functions from prelude + +RepLib.SYB.Aliases - SYB: Port of Data.Generics.Aliases +RepLib.SYB.Schemes - SYB: Port of Data.Generics.Schemes + +RepLib - Toplevel module that imports all of the above + +To use this library, import RepLib and derive representations of your +datatypes. The "Lib" module contains a number of type-indexed +operations that have been predefined. To see an example of +automatically deriving the representation of a datatype, see the file +Main.hs. + +Currently, the representations of datatypes with record components, +GADTs and nested datatypes cannot be automatically derived. + diff --git a/RepLib.cabal b/RepLib.cabal new file mode 100644 --- /dev/null +++ b/RepLib.cabal @@ -0,0 +1,34 @@ +name: RepLib +version: 0.2.1 +license: LGPL +license-file: LICENSE +build-type: Simple +cabal-version: >= 1.2.3 +tested-with: GHC == 6.10.3, GHC == 6.8.3 +author: Stephanie Weirich +maintainer: Brent Yorgey + Stephanie Weirich +homepage: http://www.cis.upenn.edu/~sweirich/RepLib +category: Data +extra-source-files: README, examples/Main.hs, examples/UnifyExp.hs +synopsis: Generic programming library with representation types +description: Generic programming library providing structural + polymorphism and other features. + +Library + build-depends: base >= 3.0 && < 4.2, haskell98 >= 1.0 && < 1.1, + template-haskell >= 2.2 && < 2.4, mtl >= 1.1 && < 1.2 + exposed-modules: + Data.RepLib, + Data.RepLib.R, + Data.RepLib.R1, + Data.RepLib.Lib, + Data.RepLib.PreludeReps, + Data.RepLib.PreludeLib, + Data.RepLib.RepAux, + Data.RepLib.Derive, + Data.RepLib.SYB.Aliases, + Data.RepLib.SYB.Schemes, + Data.RepLib.Unify + if impl(ghc < 6.10) + extensions: PatternSignatures diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Main.hs b/examples/Main.hs new file mode 100644 --- /dev/null +++ b/examples/Main.hs @@ -0,0 +1,175 @@ +-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses #-} +----------------------------------------------------------------------------- +-- | +-- Module : Main +-- Copyright : (c) The University of Pennsylvania, 2006 +-- License : BSD +-- +-- Maintainer : sweirich@cis.upenn.edu +-- Stability : experimental +-- Portability : non-portable +-- +-- A file demonstrating the use of RepLib +-- +----------------------------------------------------------------------------- + +module Main where + +import Data.RepLib +import Language.Haskell.TH + + +-- For each datatype that we define, we need to also create its representation. +-- The template Haskell function derive does this automatically for +-- each type. + +data Tree a = Leaf a | Node (Tree a) (Tree a) +$(derive [''Tree]) + +data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday +$(derive [''Day]) + +-- Note, for mutually recursive datatypes, use "derive" and give list +-- of type names. + +-- Note also that the functions of RepLib can cooperate with the +-- traditional 'deriving' mechanism +data Company = C [Dept] deriving (Eq, Ord, Show) +data Dept = D String Manager [CUnit] deriving (Eq, Ord, Show) +data Manager = M Employee deriving (Eq, Ord, Show) +data CUnit = PU Employee | DU Dept deriving (Eq, Ord, Show) +data Employee = E Person Salary deriving (Eq, Ord, Show) +data Person = P String deriving (Eq, Ord, Show) +data Salary = S Float deriving (Eq, Ord, Show) + +$(derive + [''Company, + ''Dept, + ''CUnit, + ''Employee, + ''Manager, + ''Person, + ''Salary]) + + +-- +-- Some sample data for these types +-- +t1 :: Tree Int +t1 = Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6)) + +t2 :: Tree Int +t2 = Node (Node (Leaf 0) (Leaf 7)) (Leaf 20) + +s1 :: Company +s1 = C [D "Types" (M (E (P "Stephanie") (S 1000.0))) + [PU (E (P "Michael") (S 50)), + PU (E (P "Samuel") (S 50)), + PU (E (P "Theodore") (S 50))], + D "Terms" (M (E (P "Stephanie") (S 200))) + [DU (D "Shipping" (M (E (P "Alice") (S 3000))) + [])]] + + +-- +-- Prelude operations. +-- +-- Note that we didn't derive Eq, Ord, Bounded or Show for "Day" and "Tree". We can +-- do that now with operations from RepLib.PreludeLib. + +-- for Day +instance Eq Day where + (==) = eqR1 rep1 +instance Ord Day where + compare = compareR1 rep1 +instance Bounded Day where + minBound = minBoundR1 rep1 + maxBound = maxBoundR1 rep1 +instance Show Day where + showsPrec = showsPrecR1 rep1 + +-- for Tree +instance (Rep a, Eq a) => Eq (Tree a) where (==) = eqR1 rep1 +instance (Rep a, Show a) => Show (Tree a) where showsPrec = showsPrecR1 rep1 +instance (Rep a, Ord a) => Ord (Tree a) where compare = compareR1 rep1 + +-- Besides the prelude operations, RepLib provides a number of other +-- type-indexed operations. + +-- +-- Instances for RepLib.Lib operations +-- + +-- Generate creates arbitrary elements of a type, up to a certain depth. +instance Generate Day +instance Generate a => Generate (Tree a) +instance Generate Company +instance Generate Dept +instance Generate Manager +instance Generate CUnit +instance Generate Employee +instance Generate Person +instance Generate Salary + + +-- Sum adds together all of the Ints in a datastructure +instance GSum a => GSum (Tree a) +instance GSum Company +instance GSum Dept +instance GSum Manager +instance GSum CUnit +instance GSum Employee +instance GSum Person +instance GSum Salary + +-- Shrink creates smaller versions of a data structure. +instance Shrink a => Shrink (Tree a) + +-- +-- SYB Style operations +-- +-- RepLib also supports many of the combinators from the SYB library. For example, +-- we can include the following code from the "Paradise" benchmark that gives everyone +-- in the company a raise. + +-- Increase salary by percentage +increase :: Float -> Company -> Company +increase k = everywhere (mkT (incS k)) + +-- "interesting" code for increase +incS :: Float -> Salary -> Salary +incS k (S s) = S (s * (1+k)) + + +-- +-- Generalized folds +-- +-- finally, we define generalized versions of fold left and +-- fold right for the Tree type constructor. +instance Fold Tree where + foldRight op = rreduceR1 (rTree1 (RreduceD { rreduceD = op }) + (RreduceD { rreduceD = foldRight op})) + foldLeft op = lreduceR1 (rTree1 (LreduceD { lreduceD = op }) + (LreduceD { lreduceD = foldLeft op })) + +main = do print (minBound :: Day) + print (maxBound :: Day) + print t1 + print s1 + print (Monday < Tuesday) + print (t1 < t2) +-- + print (generate 7 :: [Day]) + print (generate 3 :: [Tree Int]) + print (generate 7 :: [Company]) +-- + print (subtrees t1) + print (gsum t1) + print (gsum t2) +-- + print (increase 0.1 s1) + print (s1 < (increase 0.2 s1)) +-- + print (gproduct t1) + print (count t1) diff --git a/examples/UnifyExp.hs b/examples/UnifyExp.hs new file mode 100644 --- /dev/null +++ b/examples/UnifyExp.hs @@ -0,0 +1,161 @@ +{-# OPTIONS -fglasgow-exts #-} +{-# OPTIONS -fallow-undecidable-instances #-} +{-# OPTIONS -fallow-overlapping-instances #-} +{-# OPTIONS -fth #-} + +----------------------------------------------------------------------------- +-- | +-- Module : UnifyExp +-- Copyright : (c) Ben Kavanagh 2008 +-- License : BSD +-- +-- Maintainer : ben.kavanagh@gmail.com +-- Stability : experimental +-- Portability : non-portable +-- +-- A file demonstrating the use of Data.Replib.Unify +-- +----------------------------------------------------------------------------- + +module UnifyExp +where + +import Data.RepLib +import Data.RepLib.Unify +import Test.HUnit +import Control.Monad.Error + + + +data Exp = Var Int + | Plus Exp Exp + | K String + deriving (Show, Eq) +$(derive [''Exp]) + +instance HasVar Int Exp where + is_var (Var i) = Just i + is_var _ = Nothing + var = Var + +-- A = "f" ==> [(A, "f")] +test1 :: Maybe [(Int, Exp)] +test1 = solveUnification [(Var 1, K "f")] + + +-- A = "f" + A ==> fails occurs check +test2 :: Maybe [(Int, Exp)] +test2 = solveUnification [(Var 1, Plus (K "f") (Var 1))] + + +-- A + B = B + B ==> A = B +test3 :: Maybe [(Int, Exp)] +test3 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 2))] + +-- A + B = B + C ==> [(A, C), (B, C)] +test4 :: Maybe [(Int, Exp)] +test4 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 3))] + + + + +data Term = TVar Int + | K2 String + | App Term Term + deriving (Show, Eq) +$(derive [''Term]) + +instance HasVar Int Term where + is_var (TVar i) = Just i + is_var _ = Nothing + var = TVar + +-- There are two ways to override the unify [Char] [Char] problem. the first is to implement +-- unify and only offer the case for K2, defaulting to generic unify in other cases. The other +-- is to implement unify for String using equality, overriding the default Cons/Nil case handling + + +-- special instance of unify for String +-- Writing an instance for String which leaves 'special' term 'a' abstract has a problem with case a = String, +-- which leads to overlap with a a case.. So we can only specialise String for a known 'special' term (here Term) +instance (Eq n, Show n, HasVar n Term) => Unify n Term String where + unifyStep _ x y = if x == y + then return () + else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y) + + + + +-- f(g(A)) = f(B) ==> [(B, g(A))] +test5 :: Maybe [(Int, Term)] +test5 = solveUnification [(App (K2 "f") (App (K2 "g") (TVar 1)), App (K2 "f") (TVar 2))] + + +-- f(g(A), A) = f(B, xyz) ==> [(A, xyz), (B, g(xyz))] +test6 :: Maybe [(Int, Term)] +test6 = solveUnification [(App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1), App (App (K2 "f") (TVar 2)) (K2 "xyz"))] + +-- f(A) = f(B, C) ==> fail. constructor mismatch. App vs K2. This is in essence an 'arity' failure. +-- in a term datatype that had Application as an arity plus list, the arity would not be equal and would call failure. +-- I'm not sure the error message would be adequate. Perhaps I could use a typeclass/newtype to get better error messages +-- on equality failures. +test7 :: Maybe [(Int, Term)] +test7 = solveUnification [(App (K2 "f") (TVar 1), App (App (K2 "f") (TVar 2)) (TVar 3))] + +-- f(A) = f(B) ==> [(A, B)] +test8 :: Maybe [(Int, Term)] +test8 = solveUnification [(App (K2 "f") (TVar 1), App (K2 "f") (TVar 2))] + +-- A = B, B = abc ==> [(B, abc), (A, abc)] +test9 :: Maybe [(Int, Term)] +test9 = solveUnification [(TVar 1, TVar 2), (TVar 2, K2 "abc")] + +-- A = abc, xyz = X, A = X ==> fails with built in equality since we effectively ask abc = xyz +test10 :: Maybe [(Int, Term)] +test10 = solveUnification [(TVar 1, K2 "abc"), (K2 "xyz", TVar 2), (TVar 1, TVar 2)] + + + +-- Test that unification works with surrounding term structure (other datatypes) which are closed, i.e. they have no free variables. +data OuterTerm = K3 String + | Inner Term + | App3 OuterTerm OuterTerm + deriving (Show, Eq) +$(derive [''OuterTerm]) + + +-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))] where H is outer +test11 :: Maybe [(Int, Term)] +test11 = solveUnification' + (undefined :: Proxy (Int, Term)) + [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)), + App3 (K3 "H") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))] + + +-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))] where H is outer +test12 :: Maybe [(Int, Term)] +test12 = solveUnification' + (undefined :: Proxy (Int, Term)) + [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)), + App3 (K3 "I") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))] + + + + +-- todo. fix tests so that errors are tested properly. +tests = test [ test1 ~?= Just [(1,K "f")], + test2 ~?= error "***Exception: occurs check failed", + test3 ~?= Just [(1,Var 2)], + test4 ~?= Just [(1,Var 3),(2,Var 3)], + test5 ~?= Just [(2,App (K2 "g") (TVar 1))], + test6 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")], + test7 ~?= error "*** Exception: constructor mismatch", + test8 ~?= Just [(1,TVar 2)], + test9 ~?= Just [(2,K2 "abc"),(1,K2 "abc")], + test10 ~?= error "*** Exception: unify failed in built in equality", + test11 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")], + test12 ~?= error "*** Exception: unify failed when testing equality for \"H\" = \"I\""] + + +main = runTestTT tests +