Module KindCheck

module KindCheck: sig .. end
This module implements a well-kindedness check for the types of the surface language. It also offers the necessary building blocks for resolving names (i.e. determining which definition each variable and data constructor refers to) and translating types and expressions down to the internal syntax.

type 'v var = 
| Local of int
| NonLocal of 'v
An environment maintains a mapping of external variable names to internal objects, represented by the type var. A var is either a local name, represented as de Bruijn index, or a non-local name, represented in some other way. Typically, when checking a compilation unit, the names defined within this compilation unit are translated to local names, whereas the names defined in other units that this unit depends on are translated to non-local names.
type 'v env 


exception KindError of (Buffer.t -> unit -> unit)
A KindError exception carries a function that displays an error message.
val implication_only_on_arrow : 'v env -> 'a
This error is detected during the translation towards the internal syntax.

Building environments.

val empty : -> 'v env
An empty environment.

Extracting information out of an environment.

val module_name : 'v env ->
module_name env is the name of the current module.
val location : 'v env -> SurfaceSyntax.location
location env is the current location in the source code.
val find_variable : 'v env -> SurfaceSyntax.maybe_qualified -> 'v var
find_variable env x looks up the possibly-qualified variable x in the environment env.
val find_kind : 'v env -> SurfaceSyntax.maybe_qualified -> Kind.kind
find_kind env x returns the kind of the possibly-qualified variable x.
val find_nonlocal_variable : 'v env -> -> 'v
find_nonlocal_variable env x looks up the unqualified variable x in the environment env. The result is expected to be a NonLocal variable, and this injection is stripped off. If the variable is not found, the error message indicates that x is not defined in an implementation file, whereas its existence is advertised in the corresponding interface file.
val resolve_datacon : 'v env ->
SurfaceSyntax.datacon_reference ->
'v var * * DataTypeFlavor.flavor
resolve_datacon env dref looks up the possibly-qualified data constructor dref.datacon_unresolved in the environment env. It updates dref in place with a datacon_info component. It returns a triple of the type with which this data constructor is associated, the unqualified name of this data constructor, and its flavor.
val get_exports : 'v env -> ( * 'v) list
get_exports env returns the list of names that are exported by env. Calling this function only makes sense after type-checking took place.

Extending an environment.

val locate : 'v env -> SurfaceSyntax.location -> 'v env
locate env loc updates env with the location loc.
val enter_module : 'v env -> -> 'v env
enter_module env m resets env so that it is ready to translate another unit (interface or implementation) named m.
val extend : 'v env -> SurfaceSyntax.type_binding list -> 'v env
extend env bindings iterates over the list bindings, from left to right, and for each binding of the form (x, kind, loc), it extends the environment by binding the unqualified variable x to a new local name whose kind is kind.
val bind_nonlocal : 'v env -> * Kind.kind * 'v -> 'v env
bind_nonlocal env (x, kind, v) binds the unqualified variable x to the non-local name v, whose kind is kind.
val dissolve : 'v env -> -> 'v env
dissolve env m has the effect of introducing a new binding of x for every existing binding of m::x. This concerns both variables and data constructors.
val bindings_data_group_types : SurfaceSyntax.data_type_def list -> SurfaceSyntax.type_binding list
bindings_data_group_types group returns a list of bindings for the types of the data group.
val bind_data_group_datacons : 'v env -> SurfaceSyntax.data_type_def list -> 'v env
bind_data_group_datacons env group extends the environment with bindings for the data constructors of the data group. It must be called after the environment has been extended with bindings for the types.
val bind_nonlocal_datacon : 'v env -> -> SurfaceSyntax.datacon_info -> 'v -> 'v env

Extending an environment with external names.

These functions are used when constructing an interface. We need to add additional bindings in the Kind-Checking environment.
val bind_external_name : 'v env -> -> -> Kind.kind -> 'v -> 'v env
val bind_external_datacon : 'v env -> -> -> SurfaceSyntax.datacon_info -> 'v -> 'v env

Functions for obtaining the bindings introduced by a pattern or by a type (interpreted as a pattern).

val bv : SurfaceSyntax.pattern -> SurfaceSyntax.type_binding list
bv p returns the names bound by the pattern p, in left-to-right order. The order matters -- the de Bruijn numbering convention relies on it.
val names : SurfaceSyntax.typ -> SurfaceSyntax.type_binding list
names ty returns a list of the names introduced by the type ty, via TyNameIntro forms. The list is returned in left-to-right order, as above. names is in fact implemented via a call to bv.

Kind-checking functions.

val infer_reset : 'v env -> SurfaceSyntax.typ -> Kind.kind
infer_reset env ty returns the kind of the type ty.
val check_implementation : 'v env -> SurfaceSyntax.implementation -> unit
check_implementation env i checks that the implementation file i is well-formed, i.e. all names are properly bound and all types are well-kinded.
val check_interface : 'v env -> SurfaceSyntax.interface -> unit
check_implementation env i checks that the interface file i is well-formed, i.e. all names are properly bound and all types are well-kinded.

Debugging functions.

val p : Buffer.t -> 'a env -> unit