free-compiler-0.3.0.0: A Haskell to Coq compiler.

Safe HaskellNone
LanguageHaskell2010

FreeC.IR.TypeSynExpansion

Contents

Description

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

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.