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
Errors.
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 : Module.name -> 'v env
An empty environment.
val module_name : 'v env -> Module.name
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 ->
Variable.name 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 -> Variable.name SurfaceSyntax.maybe_qualified -> Kind.kind
find_kind env x returns the kind of the possibly-qualified
variable x.
val find_nonlocal_variable : 'v env -> Variable.name -> '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 * Datacon.name * 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 -> (Variable.name * '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 -> Module.name -> '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 -> Variable.name * 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 -> Module.name -> '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 ->
Datacon.name -> 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 ->
Module.name -> Variable.name -> Kind.kind -> 'v -> 'v env
val bind_external_datacon : 'v env ->
Module.name ->
Datacon.name -> 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