| Copyright | (c) Galois Inc 2013-2014 | 
|---|---|
| Maintainer | Joe Hendrix <jhendrix@galois.com> | 
| Safe Haskell | None | 
| Language | Haskell98 | 
Data.Parameterized.TH.GADT
Description
This module declares template Haskell primitives so that it is easier to work with GADTs that have many constructors.
Synopsis
- structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
 - structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
 - structuralTypeOrd :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
 - structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ
 - structuralShowsPrec :: TypeQ -> ExpQ
 - structuralHash :: TypeQ -> ExpQ
 - class PolyEq u v where
 - type DataD = DatatypeInfo
 - lookupDataType' :: Name -> Q DatatypeInfo
 - asTypeCon :: Monad m => String -> Type -> m Name
 - conPat :: ConstructorInfo -> String -> Q (Pat, [Name])
 - data TypePat
 - dataParamTypes :: DatatypeInfo -> [Type]
 - assocTypePats :: [Type] -> [(TypePat, v)] -> Type -> Q (Maybe v)
 
Instance generators
The Template Haskell instance generators structuralEquality,
 structuralTypeEquality, structuralTypeOrd, and structuralTraversal
 employ heuristics to generate valid instances in the majority of cases.  Most
 failures in the heuristics occur on sub-terms that are type indexed.  To
 handle cases where these functions fail to produce a valid instance, they
 take a list of exceptions in the form of their second parameter, which has
 type [(.  Each TypePat, ExpQ)]TypePat is a matcher that tells the
 TH generator to use the ExpQ to process the matched sub-term.  Consider the
 following example:
data T a b where
  C1 :: NatRepr n -> T () n
instance TestEquality (T a) where
  testEquality = $(structuralTypeEquality [t|T|]
                   [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
                   ])The exception list says that structuralTypeEquality should use
 testEquality to compare any sub-terms of type  in a value of
 type NatRepr nT.
AnyTypemeans that the type parameter in that position can be instantiated as any typemeans that the type parameter in that position is theDataArgnn-th type parameter of the GADT being traversed (Tin the example)TypeAppis type applicationConTypespecifies a base type
The exception list could have equivalently (and more precisely) have been specified as:
[(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]
The use of DataArg says that the type parameter of the NatRepr must
 be the same as the second type parameter of T.
structuralEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralEquality declares a structural equality predicate.
structuralTypeEquality :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralTypeEquality f returns a function with the type:
   forall x y . f x -> f y -> Maybe (x :~: y)
structuralTypeOrd f returns a function with the type:
   forall x y . f x -> f y -> OrderingF x y
This implementation avoids matching on both the first and second parameters in a simple case expression in order to avoid stressing GHC's coverage checker. In the case that the first and second parameters have unique constructors, a simple numeric comparison is done to compute the result.
structuralTraversal :: TypeQ -> [(TypePat, ExpQ)] -> ExpQ Source #
structuralTraversal tp generates a function that applies
 a traversal f to the subterms with free variables in tp.
structuralShowsPrec :: TypeQ -> ExpQ Source #
structuralShow tp generates a function with the type
 tp -> ShowS that shows the constructor.
structuralHash :: TypeQ -> ExpQ Source #
structuralHash tp generates a function with the type
 Int -> tp -> Int that hashes type.
class PolyEq u v where Source #
A polymorphic equality operator that generalizes TestEquality.
Minimal complete definition
Instances
| PolyEq (NatRepr m) (NatRepr n) Source # | |
| TestEquality f => PolyEq (Assignment f x) (Assignment f y) Source # | |
Defined in Data.Parameterized.Context.Safe Methods polyEqF :: Assignment f x -> Assignment f y -> Maybe (Assignment f x :~: Assignment f y) Source # polyEq :: Assignment f x -> Assignment f y -> Bool Source #  | |
Template haskell utilities that may be useful in other contexts.
type DataD = DatatypeInfo Source #
lookupDataType' :: Name -> Q DatatypeInfo Source #
Arguments
| :: ConstructorInfo | constructor information  | 
| -> String | generated name prefix  | 
| -> Q (Pat, [Name]) | pattern and bound names  | 
Given a constructor and string, this generates a pattern for matching the expression, and the names of variables bound by pattern in order they appear in constructor.
A type used to describe (and match) types appearing in generated pattern
 matches inside of the TH generators in this module (structuralEquality,
 structuralTypeEquality, structuralTypeOrd, and structuralTraversal)
dataParamTypes :: DatatypeInfo -> [Type] Source #