Ocaml_typing.Jkindmodule Sort : sig ... endtype sort = Sort.tmodule Sub_failure_reason : sig ... endmodule Sub_result : sig ... endmodule Layout : sig ... endmodule Mod_bounds : sig ... endmodule With_bounds : sig ... endA jkind is a full description of the runtime representation of values of a given type. It includes sorts, but also the abstract top jkind Any and subjkinds of other sorts, such as Immediate.
The type parameter gives information about whether the jkind can meaningfully appear to the left of a subjkind check (this is an l-jkind) or on the right of a subjkind check (this is an r-jkind).
It may be convenient to use synonyms exported from Types:
* jkind_l: This is the jkind of an actual type; it is returned from estimate_type_jkind, for example. We can compute the joins (unions) of l-jkinds and check that an l-jkind is less than an r-jkind.
* jkind_r: This is the jkind we want some type to have. Type variables have r-jkinds (because we will someday instantiate those variables). The type passed to constrain_type_jkind is an r-jkind. We can compute the meets (intersections) of r-jkinds and check that an l-jkind is less than an r-jkind.
include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd Types.jkindtype (_, _, 'd) sided = 'd Types.jkindval disallow_right :
('a, 'b, 'l * 'r) sided ->
('a, 'b, 'l * Allowance.disallowed) sidedDisallows on the right.
val disallow_left :
('a, 'b, 'l * 'r) sided ->
('a, 'b, Allowance.disallowed * 'r) sidedDisallows a the left.
val allow_right :
('a, 'b, 'l * Allowance.allowed) sided ->
('a, 'b, 'l * 'r) sidedGeneralizes a right-hand-side allowed to be any allowance.
val allow_left :
('a, 'b, Allowance.allowed * 'r) sided ->
('a, 'b, 'l * 'r) sidedGeneralizes a left-hand-side allowed to be any allowance.
val try_allow_r :
('l * 'r) Types.jkind ->
('l * Allowance.allowed) Types.jkind optionTry to treat this jkind as an r-jkind.
module History : sig ... endtype jkind_context = {jkind_of_type : Types.type_expr -> Types.jkind_l option;is_abstract : Path.t -> bool;}Context for jkind operations.
module Violation : sig ... endmodule Const : sig ... endmodule Builtin : sig ... endval unsafely_set_bounds :
from:'d Types.jkind ->
'd Types.jkind ->
'd Types.jkindForcibly change the mod- and with-bounds of a t based on the mod- and with-bounds of from.
val add_with_bounds :
modality:Mode.Modality.Const.t ->
type_expr:Types.type_expr ->
Types.jkind_l ->
Types.jkind_lTake an existing jkind_l and add some with-bounds.
val has_with_bounds : Types.jkind_l -> boolDoes this jkind have with-bounds?
val mark_best :
('l * 'r) Types.jkind ->
('l * Allowance.disallowed) Types.jkindMark the given jkind as best, meaning we can never learn any more information about it that will cause it to become lower in the preorder of kinds
val is_best : ('l * Allowance.disallowed) Types.jkind -> boolIs the given kind best?
val of_new_sort_var :
why:History.concrete_creation_reason ->
level:int ->
'd Types.jkind * sortCreate a fresh sort variable, packed into a jkind, returning both the resulting kind and the sort.
val of_new_sort :
why:History.concrete_creation_reason ->
level:int ->
'd Types.jkindCreate a fresh sort variable, packed into a jkind.
val of_new_legacy_sort_var :
why:History.concrete_legacy_creation_reason ->
level:int ->
'd Types.jkind * sortSame as of_new_sort_var, but the jkind is lowered to Non_null to mirror "legacy" OCaml values. Defaulting the sort variable produces exactly value.
val of_new_legacy_sort :
why:History.concrete_legacy_creation_reason ->
level:int ->
'd Types.jkindSame as of_new_sort, but the jkind is lowered to Non_null to mirror "legacy" OCaml values. Defaulting the sort variable produces exactly value.
val of_new_non_float_sort_var :
why:History.concrete_creation_reason ->
level:int ->
'd Types.jkind * sortSame as of_new_sort_var, but the jkind is lowered to Non_float. Defaulting the sort variable produces exactly the sort value.
val of_const :
annotation:Ocaml_parsing.Parsetree.jkind_annotation option ->
why:History.creation_reason ->
quality:'d Types.jkind_quality ->
ran_out_of_fuel_during_normalize:bool ->
'd Const.t ->
'd Types.jkindConstruct a jkind from a constant jkind, at quality Not_best
val of_builtin :
why:History.creation_reason ->
Const.Builtin.t ->
('l * Allowance.disallowed) Types.jkindConstruct a jkind from a builtin kind, at quality Best.
val of_annotation :
context:('l * Allowance.allowed) History.annotation_context ->
Ocaml_parsing.Parsetree.jkind_annotation ->
('l * Allowance.allowed) Types.jkindval of_annotation_option_default :
default:('l * Allowance.allowed) Types.jkind ->
context:('l * Allowance.allowed) History.annotation_context ->
Ocaml_parsing.Parsetree.jkind_annotation option ->
('l * Allowance.allowed) Types.jkindval of_type_decl :
context:History.annotation_context_l ->
transl_type:(Ocaml_parsing.Parsetree.core_type -> Types.type_expr) ->
Ocaml_parsing.Parsetree.type_declaration ->
(Types.jkind_l * Ocaml_parsing.Parsetree.jkind_annotation option) optionFind a jkind from a type declaration. Type declarations are special because the jkind may have been provided via : jkind syntax (which goes through Jane Syntax) or via the old-style [@@immediate] or [@@immediate64] attributes, and of_type_decl needs to look in two different places on the type_declaration to account for these two alternatives.
Returns the jkind (at quality Not_best) and the user-written annotation.
Raises if a disallowed or unknown jkind is present.
val of_type_decl_default :
context:History.annotation_context_l ->
transl_type:(Ocaml_parsing.Parsetree.core_type -> Types.type_expr) ->
default:Types.jkind_l ->
Ocaml_parsing.Parsetree.type_declaration ->
Types.jkind_lFind a jkind from a type declaration in the same way as of_type_decl, defaulting to ~default. Returns a jkind at quality Not_best; call mark_best to mark it as Best.
Raises if a disallowed or unknown jkind is present.
val for_boxed_record : Types.label_declaration list -> Types.jkind_lChoose an appropriate jkind for a boxed record type
val for_unboxed_record : Types.label_declaration list -> Types.jkind_lChoose an appropriate jkind for an unboxed record type.
val for_boxed_variant :
loc:Ocaml_parsing.Location.t ->
decl_params:Types.type_expr list ->
type_apply:
(Types.type_expr list ->
Types.type_expr ->
Types.type_expr list ->
Types.type_expr) ->
free_vars:(Types.type_expr list -> Btype.TypeSet.t) ->
Types.constructor_declaration list ->
Types.jkind_lChoose an appropriate jkind for a boxed variant type.
decl_params is the parameters in the head of the type declaration. type_apply should be Ctype.apply partially applied to an env.
free_vars is a function that, given a list of Types.type_exprs that are used in the boxed variant, returns all type variables that are free within the Types.type_exprs. Ctype.free_variable_set_of_list is a good candidate for implementing this function.
val for_boxed_tuple : (string option * Types.type_expr) list -> Types.jkind_lChoose an appropriate jkind for a boxed tuple type.
val for_boxed_row : Types.row_desc -> Types.jkind_lChoose an appropriate jkind for a row type.
val for_arrow : Types.jkind_lThe jkind of an arrow type.
val for_object : Types.jkind_lThe jkind of an object type.
val for_float : Ident.t -> Types.jkind_lThe jkind of a float.
val for_non_float : why:History.value_creation_reason -> 'd Types.jkindThe jkind for values that are not floats.
val for_or_null_argument : Ident.t -> 'd Types.jkindThe jkind for or_null type arguments.
val for_abbreviation :
type_jkind_purely:(Types.type_expr -> Types.jkind_l) ->
modality:Mode.Modality.Const.t ->
Types.type_expr ->
Types.jkind_lThe jkind for an abbreviation declaration. This implements the design in rule FIND_ABBREV in kind-inference.md, where we consider a definition
type ... = rhsto have the kind <<layout of rhs>> mod everything with rhs. This is important to allow code like this to type-check:
module M : sig
type 'a t : value mod portable with 'a
end = struct
type 'a t = 'a
endval for_array_argument : Types.jkind_lrThe jkind for array type arguments.
val for_array_element_sort : level:int -> Types.jkind_lr * sortThe jkind for array elements, creating a new sort variable.
module Desc : sig ... endval get : 'd Types.jkind -> 'd Desc.tGet a description of a jkind.
val get_layout_defaulting_to_value : 'd Types.jkind -> Layout.Const.tget_layout_defaulting_to_value extracts a constant layout, defaulting any sort variable to value.
val get_const : 'd Types.jkind -> 'd Const.t optionget_const returns a Const.t if the layout has no sort variables, returning None otherwise
val default_to_value : 'd Types.jkind -> unitdefault_to_value t is ignore (get_layout_defaulting_to_value t)
val is_void_defaulting : 'd Types.jkind -> boolis_void t is Void = get_layout_defaulting_to_value t. In particular, it will default the jkind to value if needed to make this false.
val sort_of_jkind : Types.jkind_l -> sortReturns the sort corresponding to the jkind. Call only on representable jkinds - raises on Any.
val get_layout : 'd Types.jkind -> Layout.Const.t optionGets the layout of a jkind; returns None if the layout is still unknown. Never does mutation.
val extract_layout : 'd Types.jkind -> Sort.t Layout.tGets the layout of a jkind, without looking through sort variables.
val get_mode_crossing :
context:jkind_context ->
'd Types.jkind ->
Mode.Crossing.tGets the mode crossing for types of this jkind.
val to_unsafe_mode_crossing : Types.jkind_l -> Types.unsafe_mode_crossingval get_externality_upper_bound :
context:jkind_context ->
'd Types.jkind ->
Jkind_axis.Externality.tval set_externality_upper_bound :
Types.jkind_r ->
Jkind_axis.Externality.t ->
Types.jkind_rComputes a jkind that is the same as the input but with an updated maximum mode for the externality axis
val get_nullability :
context:jkind_context ->
Types.jkind_l ->
Jkind_axis.Nullability.tGets the nullability from a jkind.
val set_nullability_upper_bound :
Types.jkind_r ->
Jkind_axis.Nullability.t ->
Types.jkind_rComputes a jkind that is the same as the input but with an updated maximum mode for the nullability axis
val set_separability_upper_bound :
Types.jkind_r ->
Jkind_axis.Separability.t ->
Types.jkind_rComputes a jkind that is the same as the input but with an updated maximum mode for the separability axis
val set_layout : 'd Types.jkind -> Sort.t Layout.t -> 'd Types.jkindSets the layout in a jkind.
val apply_modality_l :
Mode.Modality.Const.t ->
(Allowance.allowed * 'r) Types.jkind ->
Types.jkind_lChange a jkind to be appropriate for a type that appears under a modality. This means that the jkind will definitely cross the axes modified by the modality, by setting the mod-bounds appropriately and propagating the modality into any with-bounds.
val apply_modality_r :
Mode.Modality.Const.t ->
('l * Allowance.allowed) Types.jkind ->
Types.jkind_rChange a jkind to be appropriate for an expectation of a type under a modality. This means that the jkind's axes affected by the modality will all be top. The with-bounds are left unchanged.
val apply_or_null_l : Types.jkind_l -> (Types.jkind_l, unit) resultChange a jkind to be appropriate for 'a or_null based on passed 'a. Adjusts nullability to be Maybe_null, and separability to be Maybe_separable if it is already Separable. If the jkind is already Maybe_null, fails.
val apply_or_null_r : Types.jkind_r -> (Types.jkind_r, unit) resultChange a jkind to be appropriate for an expectation of a type passed to the or_null constructor. Adjusts nullability to be Non_null, and separability to be Non_float if it is demanded to be Separable. If the jkind is already Non_null, fails.
val decompose_product : 'd Types.jkind -> 'd Types.jkind list optionExtract out component jkinds from the product. Because there are no product jkinds, this is a bit of a lie: instead, this decomposes the layout but just reuses the non-layout parts of the original jkind. Never does any mutation. Because it just reuses the mode information, the resulting jkinds are higher in the jkind lattice than they might need to be.
val get_annotation :
'd Types.jkind ->
Ocaml_parsing.Parsetree.jkind_annotation optionGet an annotation (that a user might write) for this t.
type normalize_mode = | Require_bestNormalize a jkind without losing any precision. That is, keep any with-bounds if the kind of the type is not best (a stronger kind may be found).
*)| Ignore_bestNormalize a left jkind, conservatively rounding up. That is, if the kind of a type is not best, use the not-best kind. The resulting jkind will have no with-bounds.
*)val normalize :
mode:normalize_mode ->
context:jkind_context ->
Types.jkind_l ->
Types.jkind_lval set_outcometree_of_type : (Types.type_expr -> Outcometree.out_type) -> unitCall these before trying to print.
val set_outcometree_of_modalities :
(Types.mutability -> Mode.Modality.Const.t -> Outcometree.out_mode list) ->
unitval set_printtyp_path : (Format.formatter -> Path.t -> unit) -> unitProvides the Printtyp.path formatter back up the dependency chain to this module.
val set_print_type_expr : (Format.formatter -> Types.type_expr -> unit) -> unitProvides the type_expr formatter back up the dependency chain to this module.
val set_raw_type_expr : (Format.formatter -> Types.type_expr -> unit) -> unitProvides the raw_type_expr formatter back up the dependency chain to this module.
val format : Format.formatter -> 'd Types.jkind -> unitval format_expanded : Format.formatter -> 'd Types.jkind -> unitSimilar to format, but the kind is expanded as much as possible rather than written in terms of a kind abbreviation. This is used by Merlin.
val format_history :
intro:(Format.formatter -> unit) ->
Format.formatter ->
'd Types.jkind ->
unitFormat the history of this jkind: what interactions it has had and why it is the jkind that it is. Might be a no-op: see display_histories in the implementation of the Jkind module.
The intro is something like "The jkind of t is".
val equate : Types.jkind_lr -> Types.jkind_lr -> boolThis checks for equality, and sets any variables to make two jkinds equal, if possible. e.g. equate on a var and value will set the variable to be value
val equal : Types.jkind_lr -> Types.jkind_lr -> boolThis checks for equality, but has the invariant that it can only be called when there is no need for unification; e.g. equal on a var and value will crash.
CR layouts (v1.5): At the moment, this is actually the same as equate!
val has_intersection : level:int -> 'd1 Types.jkind -> 'd2 Types.jkind -> boolChecks whether two jkinds have a non-empty intersection. Might mutate sort variables. Works over any mix of l- and r-jkinds, because the only way not to have an intersection is by looking at the layout: all axes have a bottom element.
val intersection_or_error :
type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
context:jkind_context ->
reason:History.interact_reason ->
level:int ->
('l1 * Allowance.allowed) Types.jkind ->
('l2 * Allowance.allowed) Types.jkind ->
(('l1 * Allowance.allowed) Types.jkind, Violation.t) Result.tFinds the intersection of two jkinds, constraining sort variables to create one if needed, or returns a Violation.t if an intersection does not exist. Can update the jkinds. The returned jkind's history consists of the provided reason followed by the history of the first jkind argument. That is, due to histories, this function is asymmetric; it should be thought of as modifying the first jkind to be the intersection of the two, not something that modifies the second jkind.
val sub :
type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
context:jkind_context ->
level:int ->
Types.jkind_l ->
Types.jkind_r ->
boolsub t1 t2 says whether t1 is a subjkind of t2. Might update either t1 or t2 to make their layouts equal.
type sub_or_intersect = | SubThe first jkind is a subjkind of the second.
*)| Disjoint of Sub_failure_reason.t Ocaml_utils.Misc_stdlib.Nonempty_list.tThe two jkinds have no common ground.
*)| Has_intersection of Sub_failure_reason.t
Ocaml_utils.Misc_stdlib.Nonempty_list.tThe first jkind is not a subjkind of the second, but the two jkinds have an intersection: try harder.
*)val sub_or_intersect :
type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
context:jkind_context ->
level:int ->
(Allowance.allowed * 'r) Types.jkind ->
('l * Allowance.allowed) Types.jkind ->
sub_or_intersectsub_or_intersect t1 t2 does a subtype check, returning a sub_or_intersect; see comments there for more info.
val sub_or_error :
type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
context:jkind_context ->
level:int ->
(Allowance.allowed * 'r) Types.jkind ->
('l * Allowance.allowed) Types.jkind ->
(unit, Violation.t) resultsub_or_error t1 t2 does a subtype check, returning an appropriate Violation.t upon failure.
val sub_jkind_l :
type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
context:jkind_context ->
level:int ->
?allow_any_crossing:bool ->
Types.jkind_l ->
Types.jkind_l ->
(unit, Violation.t) resultLike sub, but compares a left jkind against another left jkind. Pre-condition: the super jkind must be fully settled; no variables which might be filled in later.
val round_up :
context:jkind_context ->
(Allowance.allowed * 'r) Types.jkind ->
('l * Allowance.allowed) Types.jkind"round up" a jkind_l to a jkind_r such that the input is less than the output.
val map_type_expr :
(Types.type_expr -> Types.type_expr) ->
(Allowance.allowed * 'r) Types.jkind ->
(Allowance.allowed * 'r) Types.jkindMap a function over types in upper_bounds
val is_max : ('l * Allowance.allowed) Types.jkind -> boolChecks to see whether a right-jkind is the maximum jkind. Never does any mutation.
val mod_bounds_are_max : ('l * Allowance.allowed) Types.jkind -> boolChecks to see whether a right-jkind's mod-bounds are the maximum mod-bounds. Never does any mutation.
val has_layout_any : ('l * Allowance.allowed) Types.jkind -> boolChecks to see whether a jkind has layout any. Never does any mutation.
val is_value_for_printing : ignore_null:bool -> 'd Types.jkind -> boolChecks whether a jkind is value. This really should require a jkind_lr, but it works on any jkind, because it's used in printing and is somewhat unprincipled.
module Debug_printers : sig ... endmodule Error : sig ... end