+ 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'