syb-0.2: tests/Reify.hs
{-# OPTIONS -fglasgow-exts #-}
module Reify (tests) where
{-
The following examples illustrate the reification facilities for type
structure. Most notably, we generate shallow terms using the depth of
types and constructors as means to steer the generation.
-}
import Test.HUnit
import Data.Maybe
import Data.Generics
import Control.Monad.State
import CompanyDatatypes
------------------------------------------------------------------------------
--
-- Encoding types as values; some other way.
--
------------------------------------------------------------------------------
{-
This group provides a style of encoding types as values and using
them. This style is seen as an alternative to the pragmatic style used
in Data.Typeable.typeOf and elsewhere, i.e., simply use an "undefined"
to denote a type argument. This pragmatic style suffers from lack
of robustness: one feels tempted to pattern match on undefineds.
Maybe Data.Typeable.typeOf etc. should be rewritten accordingly.
-}
-- | Type as values to stipulate use of undefineds
type TypeVal a = a -> ()
-- | The value that denotes a type
typeVal :: TypeVal a
typeVal = const ()
-- | Test for type equivalence
sameType :: (Typeable a, Typeable b) => TypeVal a -> TypeVal b -> Bool
sameType tva tvb = typeOf (type2val tva) ==
typeOf (type2val tvb)
-- | Map a value to its type
val2type :: a -> TypeVal a
val2type _ = typeVal
-- | Stipulate this idiom!
type2val :: TypeVal a -> a
type2val _ = undefined
-- | Constrain a type
withType :: a -> TypeVal a -> a
withType x _ = x
-- | The argument type of a function
argType :: (a -> b) -> TypeVal a
argType _ = typeVal
-- | The result type of a function
resType :: (a -> b) -> TypeVal b
resType _ = typeVal
-- | The parameter type of type constructor
paraType :: t a -> TypeVal a
paraType _ = typeVal
-- Type functions,
-- i.e., functions mapping types to values
--
type TypeFun a r = TypeVal a -> r
-- Generic type functions,
-- i.e., functions mapping types to values
--
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 x = maybe f id (cast x)
------------------------------------------------------------------------------
--
-- Mapping operators to map over type structure
--
------------------------------------------------------------------------------
-- | Query all constructors of a given type
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 = if isAlgType $ dataTypeOf $ type2val t
then dataTypeConstrs $ dataTypeOf $ type2val t
else []
-- 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 = if isAlgType $ dataTypeOf $ type2val t
then dataTypeConstrs $ dataTypeOf $ type2val t
else []
-- 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
------------------------------------------------------------------------------
--
-- Some reifying relations on types
--
------------------------------------------------------------------------------
-- | 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'
-- Specific increment operator
inc' Nothing = Nothing
inc' (Just i) = Just (i+1)
------------------------------------------------------------------------------
--
-- Build a shallow term
--
------------------------------------------------------------------------------
shallowTerm :: (forall a. Data a => Maybe a) -> (forall b. Data b => b)
shallowTerm cust
= result
where
result :: forall b. Data b => b
-- Need a type signature here to bring 'b' into scope
result = maybe gdefault id cust
where
-- The worker, also used for type disambiguation
gdefault :: b
gdefault = case con of
Just (con, Just _) -> fromConstrB (shallowTerm cust) con
_ -> error "no shallow term!"
-- The type to be constructed
typeVal :: TypeVal b
typeVal = val2type gdefault
-- The most shallow constructor if any
con :: Maybe (Constr, Maybe Int)
con = depthOfType (const True) typeVal
-- For testing shallowTerm
shallowTermBase :: GenericR Maybe
shallowTermBase = Nothing
`extR` Just (1.23::Float)
`extR` Just ("foo"::String)
-- Sample datatypes
data T1 = T1a deriving (Typeable, Data) -- just a constant
data T2 = T2 T1 deriving (Typeable, Data) -- little detour
data T3 = T3a T3 | T3b T2 deriving (Typeable, Data) -- recursive case
data T4 = T4 T3 T3 deriving (Typeable, Data) -- sum matters
-- Sample type arguments
t0 = typeVal :: TypeVal Int
t1 = typeVal :: TypeVal T1
t2 = typeVal :: TypeVal T2
t3 = typeVal :: TypeVal T3
t4 = typeVal :: TypeVal T4
tCompany = typeVal :: TypeVal Company
tPerson = typeVal :: TypeVal Person
tEmployee = typeVal :: TypeVal Employee
tDept = typeVal :: TypeVal Dept
-- Test cases
test0 = t1 `reachableType` t1 -- True
test1 = t1 `reachableType` t2 -- True
test2 = t2 `reachableType` t1 -- False
test3 = t1 `reachableType` t3
test4 = tPerson `reachableType` tCompany
test5 = gcountSubtermTypes tPerson
test6 = gcountSubtermTypes tEmployee
test7 = gcountSubtermTypes tDept
test8 = shallowTerm shallowTermBase :: Person
test9 = shallowTerm shallowTermBase :: Employee
test10 = shallowTerm shallowTermBase :: Dept
tests = ( test0
, ( test1
, ( test2
, ( test3
, ( test4
, ( test5
, ( test6
, ( test7
, ( test8
, ( test9
, ( test10
))))))))))) ~=? output
output = (True,(True,(False,(True,(True,(1,(2,(3,(P "foo" "foo",
(E (P "foo" "foo") (S 1.23),
D "foo" (E (P "foo" "foo") (S 1.23)) []))))))))))