(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Gabriel Scherer, projet Parsifal, INRIA Saclay *)
(* Rodolphe Lepigre, projet Deducteam, INRIA Saclay *)
(* *)
(* Copyright 2018 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(** The OCaml runtime assumes for type-directed optimizations that all types
are "separable". A type is "separable" if either all its inhabitants
(the values of this type) are floating-point numbers, or none of them are.
(Note: This assumption is required for the dynamic float array optimization;
it is only made if Config.flat_float_array is set,
otherwise the code in this module becomes trivial
-- see {!compute_decl}.)
This soundness requirement could be broken by type declarations mixing
existentials and the "[@@unboxed]" annotation. Consider the declaration
{[
type any = Any : 'a -> any [@@unboxed]
]}
which corresponds to the existential type "exists a. a". If this type is
allowed to be unboxed, then it is inhabited by both [float] values
and non-[float] values. On the contrary, if unboxing is disallowed, the
inhabitants are all blocks with the [Any] constructors pointing to its
parameter: they may point to a float, but they are not floats.
The present module contains a static analysis ensuring that declarations
annotated with "[@@unboxed]" can be safely unboxed. The idea is to check
the "separability" (in the above sense) of the argument type that would
be unboxed, and reject the unboxed declaration if it would create a
non-separable type.
Checking mutually-recursive type declarations is a bit subtle.
Consider, for example, the following declarations.
{[
type foo = Foo : 'a t -> foo [@@unboxed]
and 'a t = ...
]}
Deciding whether the type [foo] should be accepted requires inspecting
the declaration of ['a t], which may itself refer to [foo] in turn.
In general, the analysis performs a fixpoint computation. It is somewhat
similar to what is done for inferring the variance of type parameters.
Our analysis is defined using inference rules for our judgment
[Def; Gamma |- t : m], in which a type expression [t] is checked
against a "mode" [m]. This "mode" describes the separability
requirement on the type expression (see below for
more details). The mode [Gamma] maps type variables to modes and
[Def] records the "mode signature" of the mutually-recursive type
declarations that are being checked.
The "mode signature" of a type with parameters [('a, 'b) t] is of the
form [('a : m1, 'b : m2) t], where [m1] and [m2] are modes. Its meaning
is the following: a concrete instance [(foo, bar) t] of the type is
separable if [foo] has mode [m1] and [bar] has mode [m2]. *)
type error =
| Non_separable_evar of string option
exception Error of Location.t * error
(** Exception raised when a type declaration is not separable, or when its
separability cannot be established. *)
type mode = Types.Separability.t = Ind | Sep | Deepsep
(** The mode [Sep] ("separable") characterizes types that are indeed separable:
either they only contain floating-point values, or none of the values
at this type are floating-point values.
On a type parameter, it indicates that this parameter must be
separable for the whole type definition to be separable. For
example, the mode signature for the type declaration [type 'a
t = 'a] is [('a : Sep) t]. For the right-hand side to be
separable, the parameter ['a] must be separable.
The mode [Ind] ("indifferent") characterizes any type -- separable
or not.
On a type parameter, it indicates that this parameter needs not be
separable for the whole type definition to be separable. For
example, [type 'a t = 'a * bool] does not require its parameter
['a] to be separable as ['a * bool] can never contain [float]
values. Its mode signature is thus [('a : Ind) t].
Finally, the mode [Deepsep] ("deeply separable") characterizes
types that are separable, and whose type sub-expressions are also
separable. This advanced feature is only used in the presence of
constraints.
For example, [type 'a t = 'b constraint 'a = 'b * bool]
may not be separable even if ['a] is (its separately depends on 'b,
a fragment of 'a), so its mode signature is [('a : Deepsep) t].
The different modes are ordered as [Ind < Sep < Deepsep] (from the least
demanding to the most demanding). *)
val compute_decl : Env.t -> Types.type_declaration -> mode list
(** [compute_decl env def] returns the signature required
for the type definition [def] in the typing environment [env]
-- including signatures for the current recursive block.
The {!Error} exception is raised if no such signature exists
-- the definition will always be invalid. This only happens
when the definition is marked to be unboxed.
Variant (or record) declarations that are not marked with the
"[@@unboxed]" annotation, including those that contain several variants
(or labels), are always separable. In particular, their mode signatures
do not require anything of their type parameters, which are marked [Ind].
Finally, if {!Config.flat_float_array} is not set, then separability
is not required anymore; we just use [Ind] as the mode of each parameter
without any check.
*)
(** Property interface (see {!Typedecl_properties}). These functions
rely on {!compute_decl} and raise the {!Error} exception on error. *)
type prop = Types.Separability.signature
val property : (prop, unit) Typedecl_properties.property
val update_decls :
Env.t ->
(Ident.t * Typedecl_properties.decl) list ->
(Ident.t * Typedecl_properties.decl) list