206 lines
9.3 KiB
OCaml
206 lines
9.3 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
|
||
(UserS : sig (** @inline *) include HSTRUCTURE end)
|
||
: sig
|
||
|
||
module S : sig
|
||
type 'a structure =
|
||
| Abstract of int
|
||
| User of 'a UserS.structure
|
||
end
|
||
|
||
(** {2 Unification} *)
|
||
|
||
(**This submodule defines the data attached with a unification variable. *)
|
||
module Data : sig
|
||
|
||
(** @inline *)
|
||
include OSTRUCTURE
|
||
|
||
(**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
|
||
|
||
val rank : 'a structure -> int
|
||
|
||
val scope : 'a structure -> int
|
||
|
||
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
|
||
|
||
(* Existentially-bound variables can "move" in the constraint: some
|
||
constraint-solving steps have the effect of hoisting their
|
||
existential quantifier out, to scope over a larger part of the
|
||
constraint -- this corresponds to lowering the rank of the
|
||
variable. They can also be unified with some structure. *)
|
||
|
||
(* We also support "rigidly-bound" variables that are not allowed to
|
||
move to a different binding place, or to unify with anything else
|
||
than themselves. This models language features with abstract
|
||
variables/types that cannot escape their scope, such as local
|
||
abstract types or existential unpacking. *)
|
||
|
||
type status = Active | Generic
|
||
|
||
(* The literature defines a type scheme as a type (the ``body''), placed in
|
||
the scope of a list of universal quantifiers. Here, the quantifiers are
|
||
just variables (which definitely carry no structure), while the body is
|
||
just a variable too (which possibly/probably carries some structure).
|
||
One may think of a type scheme as a fragment of the unification graph,
|
||
part of which is marked ``generic'' and is meant to be copied when the
|
||
type scheme is instantiated, part of which is not (the free variables, so
|
||
to speak). *)
|
||
|
||
(** {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: {!fresh}, {!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. *)
|
||
|
||
(**[fresh s] creates a fresh flexible unifier variable with structure [s].
|
||
This variable is initially bound at the most recent stack frame. Invoking
|
||
{!fresh} 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 fresh: variable S.structure -> variable
|
||
|
||
(** [fresh_rigid ()] behaves as [fresh] above but with an abstract
|
||
structure. *)
|
||
val fresh_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
|
||
|
||
(**These exceptions are raised by {!exit}. *)
|
||
exception Cycle of variable
|
||
exception VariableScopeEscape of { rank: int; scope: int }
|
||
|
||
(**[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 "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.
|
||
|
||
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 variables,
|
||
obtained by invoking {!fresh}. 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
|