194 lines
9.0 KiB
OCaml
194 lines
9.0 KiB
OCaml
(******************************************************************************)
|
||
(* *)
|
||
(* Inferno *)
|
||
(* *)
|
||
(* François Pottier, Inria Paris *)
|
||
(* *)
|
||
(* Copyright Inria. All rights reserved. This file is distributed under the *)
|
||
(* terms of the MIT License, as described in the file LICENSE. *)
|
||
(* *)
|
||
(******************************************************************************)
|
||
|
||
open Signatures
|
||
|
||
(**This module provides machinery to deal with Hindley-Milner polymorphism.
|
||
It takes care of creating and instantiating schemes, and does so in an
|
||
efficient way. It is parameterized with the structure [S]. On top of it,
|
||
it adds its own structure, because it needs every unification variable to
|
||
carry extra information related to generalization. Thus, it wraps the
|
||
user-specified structure [S] in a richer structure [Data], and sets up a
|
||
unifier [U] that works with this data. It provides an abstract
|
||
representation of Hindley-Milner {i schemes}, together with several
|
||
operations that allow constructing, inspecting, and instantiating
|
||
schemes. *)
|
||
module Make
|
||
(S : sig (** @inline *) include GSTRUCTURE_OPT end)
|
||
: sig
|
||
|
||
(** {2 Unification} *)
|
||
|
||
(**This submodule defines the data attached with a unification variable. *)
|
||
module Data : sig
|
||
|
||
(** @inline *)
|
||
include DSTRUCTURE
|
||
|
||
(**The type ['a structure] is richer (carries more information) than the
|
||
type ['a S.structure]. The function [project] witnesses this fact. It
|
||
drops the extra information and extracts the underlying user-defined
|
||
structure. *)
|
||
val project : 'a structure -> 'a S.structure
|
||
|
||
end
|
||
|
||
(**This unifier operates with the structure specified by the submodule
|
||
{!Data}. *)
|
||
module U : sig
|
||
(** @inline *)
|
||
include GUNIFIER with type 'a structure = 'a Data.structure
|
||
end
|
||
|
||
(**The variables manipulated by this module are unifier variables. *)
|
||
type variable =
|
||
U.variable
|
||
|
||
(** {2 Schemes} *)
|
||
|
||
(**A {i scheme} is usually described in the literature under the form [∀V.T],
|
||
where [V] is a list of type variables (the {i quantifiers}) and [T] is a
|
||
type (the {i body}).
|
||
|
||
Here, a scheme is represented as an abstract data structure. The functions
|
||
{!quantifiers} and {!body} give a view of a scheme that matches the
|
||
description in the literature.
|
||
|
||
Two key operations on schemes are {i generalization} and {i instantiation}.
|
||
Generalization turns a fragment of the unification graph into a scheme.
|
||
Instantiation operates in the reverse direction and creates a fresh copy of
|
||
a scheme, which it turns into a graph fragment. *)
|
||
type scheme
|
||
|
||
(**[quantifiers σ] returns the quantifiers of the scheme [σ], in an arbitrary
|
||
fixed order. The quantifiers are {i generic} unifier variables. They carry
|
||
no structure. *)
|
||
val quantifiers: scheme -> variable list
|
||
|
||
(**[body σ] returns the body of the scheme [σ]. It is represented as a
|
||
variable, that is, a vertex in the unification graph. *)
|
||
val body: scheme -> variable
|
||
|
||
(**[trivial v] creates a trivial scheme, whose list of quantifiers is empty,
|
||
and whose body is [v]. A trivial scheme is also known as a monomorphic
|
||
scheme. Nontrivial schemes are created by the functions {!enter} and
|
||
{!exit} below. *)
|
||
val trivial: variable -> scheme
|
||
|
||
(** {2 Generalization and Instantiation} *)
|
||
|
||
(**This module maintains a mutable internal state, which is created and
|
||
initialized when {!Make} is applied. This state is updated by the
|
||
functions that follow: {!flexible}, {!rigid}, {!enter}, {!exit},
|
||
{!instantiate}.
|
||
|
||
This internal state keeps track of a {i constraint context}, which can be
|
||
thought of as a stack of {i frames}. The function {!enter} pushes a new
|
||
frame onto this stack; the function {!exit} pops a frame off this stack
|
||
(and performs generalization). {!enter} is invoked when the {i left-hand
|
||
side} of a [let] constraint is entered; {!exit} is invoked when it is
|
||
exited. Thus, each stack frame corresponds to a surrounding [let]
|
||
constraint. Every stack frame records the set of unifier variables that
|
||
are bound there.
|
||
|
||
As unification makes progress, the site where a unifier variable is bound
|
||
can change. Indeed, when two variables bound at two distinct stack frames
|
||
are merged, the merged variable is thereafter considered bound at the
|
||
most ancient of these stack frames. *)
|
||
|
||
(**[flexible s] creates a fresh unifier variable with structure [s]. This
|
||
variable is flexible: this means that it can be unified with other
|
||
variables without restrictions. This variable is initially bound at the
|
||
most recent stack frame. If is unified with more ancient variables, then
|
||
its binding site is implicitly hoisted up.
|
||
|
||
Invoking {!flexible} is permitted only if the stack is currently
|
||
nonempty, that is, if the current balance of calls to {!enter} versus
|
||
calls to {!exit} is at least one. *)
|
||
val flexible: variable S.structure -> variable
|
||
|
||
(**[rigid()] creates a fresh unifier variable [v] with structure [S.leaf].
|
||
This variable is rigid: this means that it can be unified with a flexible
|
||
variable that is as recent as [v] or more recent than [v], and with
|
||
nothing else. It cannot be unified with a more ancient flexible variable,
|
||
with another rigid variable, or with a variable that carries nonleaf
|
||
structure. This variable is bound at the most recent stack frame, and its
|
||
binding site is never hoisted up.
|
||
|
||
By convention, at each stack frame, the rigid variables are bound in
|
||
front of the flexible variables. Thus, a call to {!flexible} and a call
|
||
to {!rigid} commute.
|
||
|
||
Invoking {!rigid} is permitted only if the stack is currently nonempty,
|
||
that is, if the current balance of calls to {!enter} versus calls to
|
||
{!exit} is at least one. *)
|
||
val rigid: unit -> variable
|
||
|
||
(**[enter()] updates the current state by pushing a new frame onto the
|
||
current constraint context. It is invoked when the left-hand side of a
|
||
[CLet] constraint is entered. *)
|
||
val enter: unit -> unit
|
||
|
||
(**This exception is raised by {!exit}. *)
|
||
exception Cycle of variable
|
||
|
||
(**This exception is raised by {!exit}. *)
|
||
exception VariableScopeEscape
|
||
|
||
(**[exit ~rectypes roots] updates the current state by popping a frame off
|
||
the current constraint context. It is invoked when the left-hand side of
|
||
a [CLet] constraint is exited.
|
||
|
||
[exit] examines the {i young} fragment of the unification graph, that is,
|
||
the part of the unification graph that has been created or affected since
|
||
the most recent call to [enter]. The following actions are taken.
|
||
|
||
First, if [rectypes] is [false], then an occurs check is performed: that
|
||
is, if there is a cycle in the young fragment, then an exception of the
|
||
form [Cycle v] is raised, where the vertex [v] participates in the cycle.
|
||
|
||
Second, every young unification variable is inspected so as to
|
||
determine whether its logical binding site can be hoisted up to a
|
||
strictly older frame or must remain part of the most recent frame. In the
|
||
latter case, the variable is {i generalizable}. A list [vs] of the
|
||
generalizable variables is constructed. If a rigid variable is found
|
||
to be non-generalizable, then [VariableScopeEscape] is raised.
|
||
|
||
Third, for each variable [root] provided by the user in the list [roots],
|
||
a scheme is constructed. The body of this scheme is the variable [root].
|
||
Its quantifiers are the structureless generalizable variables that are
|
||
reachable from this root. They form a subset of [vs]. A list of schemes
|
||
[schemes], in correspondence with the list [roots], is constructed.
|
||
|
||
It may be the case that some variables in the list [vs] appear in none of
|
||
the quantifier lists of the constructed schemes. These variables are
|
||
generalizable and unreachable from the roots. They are logically
|
||
unconstrained.
|
||
|
||
The pair [(vs, schemes)] is returned. *)
|
||
val exit: rectypes:bool -> variable list -> variable list * scheme list
|
||
|
||
(**[instantiate sigma] creates a fresh instance of the scheme [sigma]. The
|
||
generic variables of the type scheme are replaced with fresh flexible
|
||
variables, obtained by invoking {!flexible}. The images of the scheme's
|
||
quantifiers and body through this copy are returned. The order of the
|
||
scheme's quantifiers, as determined by the function {!quantifiers}, is
|
||
preserved. *)
|
||
val instantiate: scheme -> variable list * variable
|
||
|
||
(**/**)
|
||
|
||
(**[show_state()] displays a representation of the internal state on the
|
||
standard output channel. It is used for debugging only. *)
|
||
val show_state: unit -> unit
|
||
|
||
end
|