RepLib (empty) → 0.2.1
raw patch · 17 files changed
+2758/−0 lines, 17 filesdep +basedep +haskell98dep +mtlsetup-changed
Dependencies added: base, haskell98, mtl, template-haskell
Files
- Data/RepLib.hs +45/−0
- Data/RepLib/Derive.hs +320/−0
- Data/RepLib/Lib.hs +331/−0
- Data/RepLib/PreludeLib.hs +205/−0
- Data/RepLib/PreludeReps.hs +35/−0
- Data/RepLib/R.hs +231/−0
- Data/RepLib/R1.hs +122/−0
- Data/RepLib/RepAux.hs +234/−0
- Data/RepLib/SYB/Aliases.hs +374/−0
- Data/RepLib/SYB/Schemes.hs +170/−0
- Data/RepLib/Unify.hs +244/−0
- LICENSE +31/−0
- README +44/−0
- RepLib.cabal +34/−0
- Setup.hs +2/−0
- examples/Main.hs +175/−0
- examples/UnifyExp.hs +161/−0
+ Data/RepLib.hs view
@@ -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++-----------------------------------------------------------------------------+
+ Data/RepLib/Derive.hs view
@@ -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++
+ Data/RepLib/Lib.hs view
@@ -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 }))+
+ Data/RepLib/PreludeLib.hs view
@@ -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)+ +
+ Data/RepLib/PreludeReps.hs view
@@ -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]) ++
+ Data/RepLib/R.hs view
@@ -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+
+ Data/RepLib/R1.hs view
@@ -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+
+ Data/RepLib/RepAux.hs view
@@ -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+
+ Data/RepLib/SYB/Aliases.hs view
@@ -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 }
+ Data/RepLib/SYB/Schemes.hs view
@@ -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
+ Data/RepLib/Unify.hs view
@@ -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++
+ LICENSE view
@@ -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.
+ README view
@@ -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.+
+ RepLib.cabal view
@@ -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 <byorgey@cis.upenn.edu>+ Stephanie Weirich <sweirich@cis.upenn.edu>+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
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/Main.hs view
@@ -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)
+ examples/UnifyExp.hs view
@@ -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+