Module Exports

module Exports: sig .. end

Handling the names exported by interfaces and implementations.

From a very high-level perspective, the type-checker needs to maintain a map from names to TypeCore.vars.

We need to map _qualified_ names to vars (What is the var that stands for "int::int"?), and
we need to map _unqualified_ names to vars (This implementation contains "val x". Which var is "x"?)

Qualified names are added to this map when importing an interface. Unqualified names are added when type-checking an implementation.

What does this have to do with kind-check? Well, kind-check expects an environment where all required interfaces have been _imported_. This means that if there is an occurrence of module "m" in implementation "impl", then kind-checking expects "m::x" to be available in the environment. Opening a module is managed internally by KindCheck and TransSurface.

Rather than using a separate, high-level environment, which we would inject into the kind-checking environment, we cheat and reuse kind-checking environments as high-level environments. The invariant is that a high-level environment only contains NonLocal bindings, either qualified or unqualified.

type value_exports = (Variable.name * TypeCore.var) list

type datacon_exports = (TypeCore.var * Datacon.name * SurfaceSyntax.datacon_info) list

val bind_implementation_values : TypeCore.env -> value_exports -> TypeCore.env

Record exported values in an implementation. This creates non-local, unqualified bindings. One can reach these bindings using find_unqualified_var, for instance when printing a signature, or in the test-suite, when poking at a specific variable.

val bind_implementation_types : TypeCore.env ->
       TypeCore.data_type_group ->
       TypeCore.var list -> datacon_exports -> TypeCore.env

Record exported types and data constructors in an implementation.

val bind_interface_value : TypeCore.env -> Module.name -> Variable.name -> TypeCore.var -> TypeCore.env

Record exported values from an interface. This creates non-local, qualified bindings. One can reach these bindings using find_qualified_var at any time. Such bindings will be used by the kind-checking, translation and type-checking phases.

val bind_interface_types : TypeCore.env ->
       Module.name ->
       TypeCore.data_type_group ->
       TypeCore.var list -> datacon_exports -> TypeCore.env

Record exported types and data constructors from an interface.

val find_qualified_var : TypeCore.env -> Module.name -> Variable.name -> TypeCore.var

find_qualified_var env mname x finds name x as exported by module mname. Use this to reach values exported by _interfaces_ which the current program depends on.

val find_unqualified_var : TypeCore.env -> Variable.name -> TypeCore.var

find_unqualified_var env x finds the name x as exported by the current module. Use it after type-checking an _implementation_.