Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module contains functions for expanding type synonyms in type expressions, type signatures as well as data type and other type synonym declarations.
The expansion of type synonyms is used to split the type of a function into the types of its arguments and the return type. It is also used during the conversion of mutually recursive data type and type synonym declarations to break the dependency of the data type declarations on the type synonyms (because they cannot be declared in the same sentence in Coq).
Synopsis
- expandAllTypeSynonymsInDecl :: TypeDecl -> Converter TypeDecl
- expandAllTypeSynonymsInDeclWhere :: (QName -> Bool) -> TypeDecl -> Converter TypeDecl
- expandAllTypeSynonymsInConDecl :: ConDecl -> Converter ConDecl
- expandAllTypeSynonymsInConDeclWhere :: (QName -> Bool) -> ConDecl -> Converter ConDecl
- expandTypeSynonym :: Type -> Converter Type
- expandAllTypeSynonyms :: Type -> Converter Type
- expandAllTypeSynonymsWhere :: (QName -> Bool) -> Type -> Converter Type
- expandTypeSynonyms :: Int -> Type -> Converter Type
- expandTypeSynonymsWhere :: Int -> (QName -> Bool) -> Type -> Converter Type
- expandTypeSynonymAt :: Pos -> Type -> Converter Type
Type Declarations
expandAllTypeSynonymsInDecl :: TypeDecl -> Converter TypeDecl Source #
Expands all type synonyms in all types in the given data type or type synonym declaration.
expandAllTypeSynonymsInDeclWhere :: (QName -> Bool) -> TypeDecl -> Converter TypeDecl Source #
Like expandAllTypeSynonymsInDecl
but expands only type synonyms whose
name matches the given predicate.
Constructor Declarations
expandAllTypeSynonymsInConDecl :: ConDecl -> Converter ConDecl Source #
Expands all type synonyms in all types in the given constructor declaration.
expandAllTypeSynonymsInConDeclWhere :: (QName -> Bool) -> ConDecl -> Converter ConDecl Source #
Like expandAllTypeSynonymsInConDecl
but expands only type synonyms whose
name matches the given predicate.
Type Expressions
expandTypeSynonym :: Type -> Converter Type Source #
Expands the outermost type synonym in the given type expression.
expandAllTypeSynonyms :: Type -> Converter Type Source #
Expands all type synonyms used in the given type expression by the type they are associated with in the current environment.
expandAllTypeSynonymsWhere :: (QName -> Bool) -> Type -> Converter Type Source #
Like expandAllTypeSynonyms
but expands only type synonyms whose name
matches the given predicate.
expandTypeSynonyms :: Int -> Type -> Converter Type Source #
Like expandAllTypeSynonyms
but accepts an additional argument for the
maximum depth.
If the maximum depth is 0
, the type will be returned unchanged.
If it is 1
, only the outermost type synonym will be expanded.
If it is negative, all type synonyms will be expanded (see also
expandAllTypeSynonyms
).
expandTypeSynonymsWhere :: Int -> (QName -> Bool) -> Type -> Converter Type Source #
Like expandTypeSynonyms
but expands only type synonyms whose name
matches the given predicate.
Subterms of Type Expressions
expandTypeSynonymAt :: Pos -> Type -> Converter Type Source #
Applies expandTypeSynonym
to the subterm at the given position.
If there are type constructor applications in parent positions, the type arguments from the parent positions are used to expand the type synonym as well.