This module contains a compiler pass that adds a module interface for the translated module to the environment.

The interface contains all top-level entries that are currently in the environment. Only entries that are defined in the translated module are listed as exported. All other entries are "hidden". Hidden entries are included such that module interfaces are self contained and type synonyms can be expanded properly. Additionally, all Coq identifiers of exported entries are qualified with their original module name in the module interface. This prevents name conflicts when several modules that use the same identifier are imported.

Examples

Example 1

The module interface for the following module

module A where

data Foo = Bar

contains interfaceEntries for all entries from the implicitly imported Prelude module and an entry for the type A.Foo and constructor A.Bar. However, only A.Foo and A.Bar are exported by the module and therefore listed in interfaceExports.

Example 2

When a module imports the module A from the example above,

module B where

import A

foo :: a -> Foo
foo x = Bar

its interface contains again all entries from the implicitly imported Prelude module, the entries from A's module interface and the entry for the top-level function B.foo. Entries for local variables such as x are not part of B's interface. Since interfaceEntries is a set, the Prelude entries which are both implicitly imported by B and part of the imported interface from A are not listed twice in B's interface.

Specification

Preconditions

The environment must contain all entries for declarations that should be exported.

Translation

No modifications are made to the AST. A module interface is added to the environment.

Postcondition

The environment contains a module interface for the translated module.