Source file jkind_intf.ml

(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*               Richard Eisenberg, Jane Street, New York                 *)
(*                                                                        *)
(*   Copyright 2024 Jane Street Group LLC                                 *)
(*                                                                        *)
(*   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.          *)
(*                                                                        *)
(**************************************************************************)

(* This module contains definitions that we do not otherwise need to repeat
   between the various Jkind modules. See comment in jkind_types.mli. *)
module type Sort = sig
  (* CR layouts-scannable: The comment below is no longer entirely accurate,
     after the addition of scannable axes (which are needed when compiling to
     determine GC behavior).
     It may be desirable to make a refined data definition that separates "the
     thing that stores enough info to compiling" (sort + scannable axes, or
     similarly layout - any) from "the discrete thing used for unification". *)
  (** A sort classifies how a type is represented at runtime. Every concrete
      jkind has a sort, and knowing the sort is sufficient for knowing the
      calling convention of values of a given type. *)
  type t

  (** Rigid sort variables similiar to [Tunivar] for types. They can be
      specified to be equal by [enter_repr] but cannot be equated/unified. *)
  type univar = { name : string option }

  (** [enter_repr pairs f] establishes correspondence between sort univars (for
      Trepr) using the given list of pairs, then calls [f]. *)
  val enter_repr : (univar * univar) list -> (unit -> 'a) -> 'a

  (** These are the constant sorts -- fully determined and without variables *)
  type base =
    | Void  (** No run time representation at all *)
    | Scannable  (** Standard ocaml value representation *)
    | Untagged_immediate
        (** Untagged 31- or 63-bit immediates, but without the tag bit, so they
            must never be visible to the GC *)
    | Float64  (** Unboxed 64-bit floats *)
    | Float32  (** Unboxed 32-bit floats *)
    | Word  (** Unboxed native-size integers *)
    | Bits8  (** Unboxed 8-bit integers *)
    | Bits16  (** Unboxed 16-bit integers *)
    | Bits32  (** Unboxed 32-bit integers *)
    | Bits64  (** Unboxed 64-bit integers *)
    | Vec128  (** Unboxed 128-bit simd vectors *)
    | Vec256  (** Unboxed 256-bit simd vectors *)
    | Vec512  (** Unboxed 512-bit simd vectors *)

  (** A sort variable that can be unified during type-checking. *)
  type var

  module Const : sig
    type t =
      | Base of base
      | Product of t list
      | Univar of univar
      | Genvar of var
          (** A layout variable bound by a surrounding [val_lpoly]. It's a
              "fake" constant that will be instantiated to real layout constant
              by slambda. The [var] is used only for physical identity; its
              contents are not consumed and its level must be
              [Ident.highest_scope]. *)

    val equal : t -> t -> bool

    val format : Format_doc.formatter -> t -> unit

    val all_void : t -> bool

    val scannable : t

    val void : t

    val float64 : t

    val float32 : t

    val word : t

    val untagged_immediate : t

    val bits8 : t

    val bits16 : t

    val bits32 : t

    val bits64 : t

    val vec128 : t

    val vec256 : t

    val vec512 : t

    module Debug_printers : sig
      val t : Format.formatter -> t -> unit
    end

    (* CR layouts: These are sorts for the types of ocaml expressions that are
       currently required to be values, but for which we expect to relax that
       restriction in versions 2 and beyond.  Naming them makes it easy to find
       where in the translation to lambda they are assume to be value. *)
    (* CR layouts: add similarly named jkinds and use those names everywhere (not
       just the translation to lambda) rather than writing specific jkinds and
       sorts in the code. *)
    val for_class_arg : t

    val for_instance_var : t

    val for_lazy_body : t

    val for_tuple_element : t

    val for_variant_arg : t

    val for_boxed_record : t

    val for_block_element : t

    val for_array_get_result : t

    val for_array_comprehension_element : t

    val for_list_element : t

    (** These are sorts for the types of ocaml expressions that we expect will
        always be "value". These names are used in the translation to lambda to
        make the code clearer. *)
    val for_function : t

    val for_probe_body : t

    val for_poly_variant : t

    val for_object : t

    val for_initializer : t

    val for_method : t

    val for_module : t

    (** Predefined scannable types, e.g. [int] and [string] *)
    val for_predef_scannable : t

    val for_tuple : t

    val for_idx : t

    val for_loop_index : t

    val for_constructor : t

    val for_boxed_variant : t

    val for_exception : t

    val for_type_extension : t

    val for_class : t
  end

  module Var : sig
    type id = private int
    (* the [private int] allows the debugger to print it *)

    (** Checks whether a [var] satisfies the properties that hold for variables
        saved to a cmi. *)
    val is_cmi_var : var -> bool

    (** Extract the unique id for a [var]. Outside of a cmi, equal [id]s imply
        physical equality of [var]s. *)
    val get_id : var -> id

    (** Get the number of an [id], useful for printing. These numbers get
        allocated only when an [id] gets printed, and so they are less brittle
        than just printing the [id] itself. *)
    val get_print_number : id -> int

    (** These names are generated lazily and only when this function is called,
        and are not guaranteed to be efficient to create *)
    val name : var -> string
  end

  val void : t

  val scannable : t

  val float64 : t

  val float32 : t

  val word : t

  val bits32 : t

  val bits64 : t

  (** Create a new sort variable that can be unified. *)
  val new_var : level:int -> var

  val of_base : base -> t

  val of_const : Const.t -> t

  val of_var : var -> t

  (** This checks for equality, and sets any variables to make two sorts equal,
      if possible *)
  val equate : t -> t -> bool

  val format : Format_doc.formatter -> t -> unit

  (** [default_to_scannable_and_get] extracts the sort as a `const`. If it's a
      variable, it is set to [scannable] first. *)
  val default_to_scannable_and_get : t -> Const.t

  (* CR layouts v12: Default this to void. *)

  (** [default_for_transl_and_get] extracts the sort as a `const`. If it's a
      variable, it is set to [value] first. After we have support for [void],
      this will default to [void] instead. *)
  val default_for_transl_and_get : t -> Const.t

  (** Like [default_to_scannable_and_get] but operates directly on a [var]. *)
  val var_default_to_scannable_and_get : var -> Const.t

  (** To record changes to sorts, for use with [Types.snapshot] and
      [Types.backtrack]. *)
  type change

  val undo_change : change -> unit

  (** Create a fresh polymorphic sort variable (level = [Ident.highest_scope]).
  *)
  val new_genvar : unit -> var

  (** Create a polymorphic sort variable (level = [Ident.highest_scope]),
      intended for saving to a cmi. *)
  val new_genvar_for_cmi : unit -> var

  (** Returns [true] iff the variable was created by {!new_genvar} or
      {!new_genvar_for_cmi}. *)
  val is_genvar : var -> bool

  val reset_cmi_sort_id : unit -> unit

  (** Get the concrete content of a variable. The returned sort must be
      representable (including rigid sorts). *)
  val get_representable_var : var -> t option

  (** [subst s t] applies the variable substitution [s] to [t], replacing each
      [Var v] where [(v, t')] is in [subst] with [t']. *)
  val subst : (var * t) list -> t -> t

  (** [instance_with ~level vars f] creates a fresh sort var at [level] for each
      var in [vars], calls [f] with {!instance} configured to replace each var
      with its fresh copy, and returns the fresh vars together with the result
      of [f]. Raises if any var in [vars] is not a generic variable (see
      {!is_genvar}). *)
  val instance_with : level:int -> var list -> (unit -> 'a) -> var list * 'a

  (** Apply instantiation to every [Var] node in a sort. Generic variables (see
      {!is_genvar}) are replaced by fresh vars registered via {!instance_with};
      non-generic variables are left unchanged. Must be called within the
      dynamic extent of {!instance_with}. *)
  val instance : t -> t

  (** Returns a human-readable name for a generic variable. Must be called
      within the dynamic extent of {!print_with_genvars}. *)
  val to_string_genvar : var -> string

  (** [print_with_genvars vars f] assigns a fresh name to each var in [vars],
      calls [f] with those names, and returns the result. Within the call to
      [f], {!to_string_genvar} will return the assigned name for each var. *)
  val print_with_genvars : var list -> (string list -> 'a) -> 'a

  (** [generalize_with f] runs [f] with sort generalization enabled (for let
      poly_ support). Returns the result of [f] and the list of sort variables
      lifted to generic during [f]. *)
  val generalize_with : (unit -> 'a) -> 'a * var list

  (** Generalize sort variables when in sort generalization context. Sets the
      level of sort variables to Ident.highest_scope and accumulates them. This
      should be called from Ctype.generalize. Only has an effect when called
      within {!generalize_with}. *)
  val generalize : current_level:int -> t -> unit

  module Debug_printers : sig
    val base : Format.formatter -> base -> unit

    val t : Format.formatter -> t -> unit

    val var : Format.formatter -> var -> unit
  end
end

module History = struct
  (* For sort variables that are topmost on the jkind lattice. *)
  type concrete_creation_reason =
    | Merlin
    | Match
    | Constructor_declaration of int
    | Label_declaration of Ident.t
    | Record_projection
    | Record_assignment
    | Record_functional_update
    | Let_binding
    | Function_argument
    | Function_result
    | Structure_item_expression
    | External_argument
    | External_result
    | Statement
    | Optional_arg_default
    | Layout_poly_in_external
    | Unboxed_tuple_element
    | Peek_or_poke
    | Old_style_unboxed_type
    | Array_element
    | Idx_element
    | Structure_item
    | Signature_item
    | Layout_poly

  (* For sort variables that are in the "legacy" position
     on the jkind lattice, defaulting exactly to [value]. *)
  type concrete_legacy_creation_reason =
    | Unannotated_type_parameter of Path.t
    | Wildcard
    | Unification_var

  open Allowance

  type 'd annotation_context =
    | Type_declaration : Path.t -> (allowed * 'r) annotation_context
    | Type_parameter :
        Path.t * string option
        -> (allowed * allowed) annotation_context
    | Newtype_declaration : string -> (allowed * allowed) annotation_context
    | Constructor_type_parameter :
        Path.t * string
        -> (allowed * allowed) annotation_context
    | Existential_unpack : string -> (allowed * allowed) annotation_context
    | Univar : string -> (allowed * allowed) annotation_context
    | Type_variable : string -> (allowed * allowed) annotation_context
    | Implicit_jkind : string -> (allowed * allowed) annotation_context
    | Type_wildcard : Location.t -> (allowed * allowed) annotation_context
    | Type_of_kind : Location.t -> (allowed * allowed) annotation_context
    | Jkind_declaration : Path.t -> (allowed * allowed) annotation_context
    | With_error_message :
        string * 'd annotation_context
        -> 'd annotation_context

  and annotation_context_l = (allowed * disallowed) annotation_context

  and annotation_context_r = (disallowed * allowed) annotation_context

  and annotation_context_lr = (allowed * allowed) annotation_context

  (* CR layouts v3: move some [value_creation_reason]s
     related to objects here. *)
  type value_or_null_creation_reason =
    | Primitive of Ident.t
    | Tuple_element
    | Separability_check
    | Polymorphic_variant_field
    | V1_safety_check
    | Probe
    | Captured_in_object
    | Let_rec_variable of Ident.t
    | Type_argument of
        { parent_path : Path.t;
          position : int;
          arity : int
        }
    | Recmod_fun_arg
    | Array_comprehension_element
    | Array_comprehension_iterator_element
    | Idx_base

  type value_creation_reason =
    | Class_let_binding
    | Object
    | Instance_variable
    | Object_field
    | Class_field
    | Boxed_record
    | Boxed_variant
    | Extensible_variant
    | Primitive of Ident.t
    | Type_argument of
        { parent_path : Path.t;
          position : int;
          arity : int
        }
    (* [position] is 1-indexed *)
    | Tuple
    | Row_variable
    | Polymorphic_variant
    | Polymorphic_variant_too_big
    | Arrow
    | Tfield
    | Tnil
    | First_class_module
    | Univar
    | Default_type_jkind
    | Existential_type_variable
    | List_comprehension_iterator_element
    | Lazy_expression
    | Class_type_argument
    | Class_term_argument
    | Debug_printer_argument
    | Array_type_kind
    | Quoted_expression
    | Unknown of string (* CR layouts: get rid of these *)

  type immediate_creation_reason =
    | Empty_record
    | Enumeration
    | Primitive of Ident.t
    | Immediate_polymorphic_variant

  type immediate_or_null_creation_reason = Primitive of Ident.t

  type scannable_creation_reason = Dummy_jkind

  (* CR layouts v5: make new void_creation_reasons *)
  type void_creation_reason = |

  type any_creation_reason =
    | Missing_cmi of Path.t
    | Initial_typedecl_env
    | Dummy_jkind
      (* This is used when the jkind is about to get overwritten;
         key example: when creating a fresh tyvar that is immediately
         unified to correct levels *)
    | Type_expression_call
    | Inside_of_Tarrow
    | Wildcard
    | Unification_var
    | Array_type_argument
    | Type_argument of
        { parent_path : Path.t;
          position : int;
          arity : int
        }
    | Overapproximation_of_with_bounds
    | Inside_quote
    | Evaluated_quote

  type product_creation_reason =
    | Unboxed_tuple
    | Unboxed_record

  type creation_reason =
    | Annotated : ('l * 'r) annotation_context * Location.t -> creation_reason
    | Missing_cmi of Path.t
    | Value_or_null_creation of value_or_null_creation_reason
    | Value_creation of value_creation_reason
    | Immediate_creation of immediate_creation_reason
    | Immediate_or_null_creation of immediate_or_null_creation_reason
    | Scannable_creation of scannable_creation_reason
    | Void_creation of void_creation_reason
    | Any_creation of any_creation_reason
    | Product_creation of product_creation_reason
    | Concrete_creation of concrete_creation_reason
    | Concrete_legacy_creation of concrete_legacy_creation_reason
    | Primitive of Ident.t
    | Unboxed_primitive of Ident.t
    | Imported
    | Imported_type_argument of
        { parent_path : Path.t;
          position : int;
          arity : int
        }
    (* [position] is 1-indexed *)
    | Generalized of Ident.t option * Location.t
    (* See commentary on [Jkind.for_abbreviation] *)
    | Abbreviation

  type interact_reason =
    | Gadt_equation of Path.t
    | Tyvar_refinement_intersection
    (* CR layouts: this needs to carry a type_expr, but that's loopy *)
    | Subjkind
end