Converts a strongly connected component of the type dependency graph and creates a separate lit of qualified smart constructor notations.

Sorts type synonym declarations topologically.

After filtering type synonym declarations from the a strongly connected component, they are not mutually dependent on each other anymore (expect if they form a cycle). However, type synonyms may still depend on other type synonyms from the same strongly connected component. Therefore we have to sort the declarations in reverse topological order.

Extracts the single type synonym declaration from a strongly connected component of the type dependency graph.

Reports a fatal error if the component contains mutually recursive declarations (i.e. type synonyms form a cycle).

Tests whether the given declaration is a type synonym declaration.

Converts a Haskell type synonym declaration to Coq.

Converts multiple (mutually recursive) Haskell data type declaration declarations.

Before the declarations are actually translated, their identifiers are inserted into the current environment. Otherwise the data types would not be able to depend on each other. The identifiers for the constructors are inserted into the current environment as well. This makes the constructors more likely to keep their original name if there is a type variable with the same (lowercase) name.

After the Inductive sentences for the data type declarations there is one Arguments sentence and several smart constructor Notation declarations for each constructor declaration of the given data types. Qualified smart constructor notations are packed into a separate list.

Converts a Haskell data type declaration to the body of a Coq Inductive sentence, the Arguments sentences for it's constructors and the smart constructor notations and creates an induction scheme. Qualified smart constructor notations are packed into a separate list.

Type variables declared by the data type or the smart constructors are not visible outside of this function.