Typedecl_separabilityThe 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.
exception Error of Location.t * errorException raised when a type declaration is not separable, or when its separability cannot be established.
type mode = Types.Separability.t = | Ind| Sep| DeepsepThe 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 listcompute_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.
type prop = Types.Separability.signatureProperty interface (see Typedecl_properties). These functions rely on compute_decl and raise the Error exception on error.
val property : (prop, unit) Typedecl_properties.propertyval update_decls :
Env.t ->
(Ident.t * Typedecl_properties.decl) list ->
(Ident.t * Typedecl_properties.decl) list