--
-- \"Scrap your boilerplate\" --- Generic programming in Haskell
-- See <http://www.cs.vu.nl/boilerplate/>. The present module provides
--- some preliminary support to compute on types.
+-- some preliminary support some sort of structural reflection. This
+-- module is presumably less common sense that most other boilerplate
+-- modules. Also, it is a bit less easy-going.
--
-----------------------------------------------------------------------------
TypeVal, -- view type "a" as "a -> ()"
typeVal, -- :: TypeVal a
sameType, -- two type values are the same
- typeValOf, -- :: a -> TypeVal a
- undefinedType, -- :: TypeVal a -> a
+ val2type, -- :: a -> TypeVal a
+ type2val, -- :: TypeVal a -> a
withType, -- :: a -> TypeVal a -> a
argType, -- :: (a -> b) -> TypeVal a
resType, -- :: (a -> b) -> TypeVal b
paraType, -- :: t a -> TypeVal a
TypeFun, -- functions on types
GTypeFun, -- polymorphic functions on types
+ extType, -- extend a function on types
-- * Generic operations to reify terms
glength,
gcount,
gnodecount,
gtypecount,
+ gfindtype,
-- * Generic operations to reify types
- constrArity,
- typeReachableFrom
+ gmapType, -- query all constructors of a type
+ gmapConstr, -- query all subterm types of a constructor
+ constrArity, -- compute arity of constructor
+ gmapSubtermTypes, -- query all subterm types of a type
+ gmapSubtermTypesConst, -- variation on gmapSubtermTypes
+ gcountSubtermTypes, -- count all types of immediate subterms
+ reachableType, -- test for reachability on types
+ depthOfType, -- compute minimum depth of type
+ depthOfConstr -- compute minimum depth of constructor
) where
-- | Test for type equivalence
sameType :: (Typeable a, Typeable b) => TypeVal a -> TypeVal b -> Bool
-sameType tva tvb = typeOf (undefinedType tva) ==
- typeOf (undefinedType tvb)
+sameType tva tvb = typeOf (type2val tva) ==
+ typeOf (type2val tvb)
-- | Map a value to its type
-typeValOf :: a -> TypeVal a
-typeValOf _ = typeVal
+val2type :: a -> TypeVal a
+val2type _ = typeVal
-- | Stipulate this idiom!
-undefinedType :: TypeVal a -> a
-undefinedType _ = undefined
+type2val :: TypeVal a -> a
+type2val _ = undefined
-- | Constrain a type
type GTypeFun r = forall a. Data a => TypeFun a r
+-- | Extend a type function
+extType :: (Data a, Typeable r) => GTypeFun r -> TypeFun a r -> GTypeFun r
+extType f = maybe f id . cast
+
+
------------------------------------------------------------------------------
--
gtypecount f = gcount (False `mkQ` (const True . f))
+-- | Find (unambiguously) an immediate subterm of a given type
+gfindtype :: (Data x, Data 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
+
+
------------------------------------------------------------------------------
--
--
------------------------------------------------------------------------------
--- | Compute arity of a constructor against a type argument
-constrArity :: Data a => (a -> ()) -> Constr -> Int
-constrArity ta c = glength $ withType (fromConstr c) ta
+-- | Query all constructors of a given type
---
--- Reachability relation on types:
--- Test if nodes of type "a" are reachable from nodes of type "b".
--- This is a naive, inefficient encoding.
--- As of writing, it does not even cope with recursive types.
---
-typeReachableFrom :: (Data a, Data b) => TypeVal a -> TypeVal b -> Bool
-typeReachableFrom (a::TypeVal a) (b::TypeVal b) =
- or ( sameType a b
- : map (recurse . fromConstr) (dataTypeCons $ dataTypeOf b)
- )
+gmapType :: ([(Constr,r')] -> r)
+ -> GTypeFun (Constr -> r')
+ -> GTypeFun r
+
+gmapType (o::[(Constr,r')] -> r) f (t::TypeVal a)
+ =
+ o $ zip cons query
+
+ where
+
+ -- All constructors of the given type
+ cons :: [Constr]
+ cons = dataTypeCons $ dataTypeOf $ type2val t
+
+ -- Query constructors
+ query :: [r']
+ query = map (f t) cons
+
+
+-- | Query all subterm types of a given constructor
+
+gmapConstr :: ([r] -> r')
+ -> GTypeFun r
+ -> GTypeFun (Constr -> r')
+
+gmapConstr (o::[r] -> r') f (t::TypeVal a) c
+ =
+ o $ query
+
+ where
+
+ -- Term for the given constructor
+ term :: a
+ term = fromConstr c
+
+ -- Query subterm types
+ query :: [r]
+ query = gmapQ (f . val2type) term
+
+
+-- | Compute arity of a given constructor
+constrArity :: GTypeFun (Constr -> Int)
+constrArity t c = glength $ withType (fromConstr c) t
+
+
+-- | Query all immediate subterm types of a given type
+gmapSubtermTypes :: (Data a, Typeable r)
+ => (r -> r -> r) -> r -> GTypeFun r -> TypeVal a -> r
+gmapSubtermTypes o (r::r) f (t::TypeVal a)
+ =
+ reduce (concat (map (gmapQ (query . val2type)) terms))
+ (GTypeFun' f)
+
+ where
+
+ -- All constructors of the given type
+ cons :: [Constr]
+ cons = dataTypeCons $ dataTypeOf $ type2val t
+
+ -- Terms for all constructors
+ terms :: [a]
+ terms = map fromConstr cons
+
+ -- Query a subterm type
+ query :: Data b => TypeVal b -> GTypeFun' r -> (r,GTypeFun' r)
+ query t f = (unGTypeFun' f t, GTypeFun' (disable t (unGTypeFun' f)))
+
+ -- Constant out given type
+ disable :: Data b => TypeVal b -> GTypeFun r -> GTypeFun r
+ disable (t::TypeVal b) f = f `extType` \(_::TypeVal b) -> r
+
+ -- Reduce all subterm types
+ reduce :: [GTypeFun' r -> (r,GTypeFun' r)] -> GTypeFun' r -> r
+ reduce [] _ = r
+ reduce (xy:z) g = fst (xy g) `o` reduce z (snd (xy g))
+
+
+-- First-class polymorphic variation on GTypeFun
+newtype GTypeFun' r = GTypeFun' (GTypeFun r)
+unGTypeFun' (GTypeFun' f) = f
+
+
+-- | Query all immediate subterm types.
+-- There is an extra argument to "constant out" the type at hand.
+-- This can be used to avoid cycles.
+
+gmapSubtermTypesConst :: (Data a, Typeable r)
+ => (r -> r -> r)
+ -> r
+ -> GTypeFun r
+ -> TypeVal a
+ -> r
+gmapSubtermTypesConst o (r::r) f (t::TypeVal a)
+ =
+ gmapSubtermTypes o r f' t
where
+ f' :: GTypeFun r
+ f' = f `extType` \(_::TypeVal a) -> r
+
+
+-- Count all distinct subterm types
+gcountSubtermTypes :: Data a => TypeVal a -> Int
+gcountSubtermTypes = gmapSubtermTypes (+) (0::Int) (const 1)
+
+
+-- | A simplied variation on gmapSubtermTypes.
+-- Weakness: no awareness of doubles.
+-- Strength: easy to comprehend as it uses gmapType and gmapConstr.
+
+_gmapSubtermTypes :: (Data a, Typeable r)
+ => (r -> r -> r) -> r -> GTypeFun r -> TypeVal a -> r
+_gmapSubtermTypes o (r::r) f
+ =
+ gmapType otype (gmapConstr oconstr f)
+
+ where
+
+ otype :: [(Constr,r)] -> r
+ otype = foldr (\x y -> snd x `o` y) r
+
+ oconstr :: [r] -> r
+ oconstr = foldr o r
+
+
+-- | Reachability relation on types, i.e.,
+-- test if nodes of type "a" are reachable from nodes of type "b".
+-- The relation is defined to be reflexive.
+
+reachableType :: (Data a, Data b) => TypeVal a -> TypeVal b -> Bool
+reachableType (a::TypeVal a) (b::TypeVal b)
+ =
+ or [ sameType a b
+ , gmapSubtermTypesConst (\x y -> or [x,y]) False (reachableType a) b
+ ]
+
+
+-- | Depth of a datatype as the constructor with the minimum depth.
+-- The outermost "Nothing" denotes a type without constructors.
+-- The innermost "Nothing" denotes potentially infinite.
+
+depthOfType :: GTypeFun Bool -> GTypeFun (Maybe (Constr, Maybe Int))
+depthOfType p (t::TypeVal a)
+ =
+ gmapType o f t
+
+ where
+
+ o :: [(Constr, Maybe Int)] -> Maybe (Constr, Maybe Int)
+ o l = if null l then Nothing else Just (foldr1 min' l)
+
+ f :: GTypeFun (Constr -> Maybe Int)
+ f = depthOfConstr p'
+
+ -- Specific minimum operator
+ min' :: (Constr, Maybe Int) -> (Constr, Maybe Int) -> (Constr, Maybe Int)
+ min' x (_, Nothing) = x
+ min' (_, Nothing) x = x
+ min' (c, Just i) (c', Just i') | i <= i' = (c, Just i)
+ min' (c, Just i) (c', Just i') = (c', Just i')
+
+ -- Updated predicate for unblocked types
+ p' :: GTypeFun Bool
+ p' = p `extType` \(_::TypeVal a) -> False
+
+
+-- | Depth of a constructor.
+-- Depth is viewed as the maximum depth of all subterm types + 1.
+-- "Nothing" denotes potentially infinite.
+
+depthOfConstr :: GTypeFun Bool -> GTypeFun (Constr -> Maybe Int)
+depthOfConstr p (t::TypeVal a) c
+ =
+ gmapConstr o f t c
+
+ where
+
+ o :: [Maybe Int] -> Maybe Int
+ o = inc' . foldr max' (Just 0)
+
+ f :: GTypeFun (Maybe Int)
+ f t' = if p t'
+ then
+ case depthOfType p t' of
+ Nothing -> Just 0
+ Just (_, x) -> x
+ else Nothing
+
+ -- Specific maximum operator
+ max' Nothing _ = Nothing
+ max' _ Nothing = Nothing
+ max' (Just i) (Just i') | i >= i' = Just i
+ max' (Just i) (Just i') = Just i'
- -- See if a is reachable from immediate subterms of a kind of b
- recurse :: b -> Bool
- recurse = or
- . gmapQ ( typeReachableFrom a
- . typeValOf
- )
+ -- Specific increment operator
+ inc' Nothing = Nothing
+ inc' (Just i) = Just (i+1)
projects / haskell-directory.git / blobdiff