Converts an IR module to Gallina sentences.

Converts the given declarations of an IR module.

Converts the given data type or type synonym declarations.

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

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.

Converts the given function declarations.

Converts a strongly connected component of the function dependency graph.

Converts a non-recursive Haskell function declaration to a Coq Definition sentence.

Converts (mutually) recursive Haskell function declarations to Coq.

The function declarations are analyzed first. If they contain constant arguments (i.e. arguments that are passed unchanged between recursive calls), they are converted using a Section sentence (see convertRecFuncDeclsWithHelpers). Otherwise they are converted into helper and main functions (see convertRecFuncDeclsWithSection).

Converts a type from IR to Coq, lifting it into the Free monad.

\(\tau^\dagger = Free\,Shape\,Pos\,\tau^*\)

A type \(\tau\) is converted by lifting it into the Free monad and recursively converting the argument and return types of functions using convertType'.

Converts a type from IR to Coq.

In contrast to convertType, the type itself is not lifted into the Free monad. Only the argument and return types of the contained function type constructors are lifted recursively.

\(\alpha^* = \alpha'\)

A type variable \(\alpha\) is translated by looking up the corresponding Coq identifier \(\alpha'\).

\(T^* = T'\,Shape\,Pos\)

A type constructor \(T\) is translated by looking up the corresponding Coq identifier \(T'\) and adding the parameters \(Shape\) and \(Pos\).

\((\tau_1\,\tau_2)^* = \tau_1^*\,\tau_2^*\)

Type constructor applications are translated recursively but remain unchanged otherwise.

\((\tau_1 \rightarrow \tau_2)^* = \tau_1^\dagger \rightarrow \tau_2^\dagger\)

Type constructor applications are translated recursively but remain unchanged otherwise.

Converts a Haskell expression to Coq.