Module `Flambda2_types`

The interface to the Flambda type system. This is parameterised over the expression language via Code_id.

type t

type flambda_type = Flambda2_types.t

val print : Stdlib.Format.formatter -> Flambda2_types.t -> unit

val arity_of_list : 
  Flambda2_types.t list ->
  [ `Unarized ] Flambda2_kinds.Flambda_arity.t

val apply_renaming : 
  Flambda2_types.t ->
  Flambda2_nominal.Renaming.t ->
  Flambda2_types.t

include Flambda2_nominal.Contains_ids.S with type t := Flambda2_types.t

val ids_for_export : Flambda2_types.t -> Flambda2_nominal.Ids_for_export.t

Gather all table identifiers to export them.

val remove_unused_value_slots_and_shortcut_aliases : 
  Flambda2_types.t ->
  used_value_slots:Flambda2_identifiers.Value_slot.Set.t ->
  canonicalise:(Flambda2_term_basics.Simple.t -> Flambda2_term_basics.Simple.t) ->
  Flambda2_types.t

type typing_env

type typing_env_extension

module Code_age_relation : sig ... end

module Typing_env_extension : sig ... end

module Typing_env : sig ... end

val meet : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.t ->
  (Flambda2_types.t * Flambda2_types.Typing_env.t)
    Flambda2_lattices.Or_bottom.t

val meet_shape : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  shape:Flambda2_types.t ->
  Flambda2_types.Typing_env.t Flambda2_lattices.Or_bottom.t

module Join_analysis : sig ... end

val cut_and_n_way_join : 
  Flambda2_types.Typing_env.t ->
  (Flambda2_types.Typing_env.t
   * Flambda2_identifiers.Apply_cont_rewrite_id.t
   * Flambda2_term_basics.Continuation_use_kind.t)
    list ->
  params:Flambda2_bound_identifiers.Bound_parameters.t ->
  cut_after:Flambda2_term_basics.Scope.t ->
  extra_lifted_consts_in_use_envs:Flambda2_identifiers.Symbol.Set.t ->
  extra_allowed_names:Flambda2_nominal.Name_occurrences.t ->
  Flambda2_types.Typing_env.t
  * Flambda2_identifiers.Apply_cont_rewrite_id.t Flambda2_types.Join_analysis.t
      option

module Function_type : sig ... end

module Closures_entry : sig ... end

val free_names : Flambda2_types.t -> Flambda2_nominal.Name_occurrences.t

type to_erase =

| Everything_not_in of Flambda2_types.Typing_env.t
| All_variables_except of Flambda2_identifiers.Variable.Set.t

val make_suitable_for_environment : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.to_erase ->
  (Flambda2_identifiers.Name.t * Flambda2_types.flambda_type) list ->
  Flambda2_types.Typing_env_extension.With_extra_variables.t

Adjust a type so it can be used in a different environment. There are two modes of operation: either a target environment can be specified, in which the resulting type is to be valid; or a set of variables may be supplied which are the only ones allowed to occur in the resulting type.

val apply_coercion : 
  Flambda2_types.flambda_type ->
  Flambda2_term_basics.Coercion.t ->
  Flambda2_types.flambda_type

val bottom : Flambda2_kinds.Flambda_kind.t -> Flambda2_types.t

Construct a bottom type of the given kind.

val unknown : Flambda2_kinds.Flambda_kind.t -> Flambda2_types.t

Construct a top ("unknown") type of the given kind.

val unknown_with_subkind : 
  ?alloc_mode:Flambda2_term_basics.Alloc_mode.For_types.t ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_kinds.Flambda_kind.With_subkind.t ->
  Flambda2_types.t

val bottom_like : Flambda2_types.t -> Flambda2_types.t

Create an bottom type with the same kind as the given type.

val unknown_like : Flambda2_types.t -> Flambda2_types.t

Create an "unknown" type with the same kind as the given type.

val any_value : Flambda2_types.t

val any_tagged_immediate : Flambda2_types.t

val any_tagged_immediate_or_null : Flambda2_types.t

val any_tagged_bool : 
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val any_boxed_float32 : Flambda2_types.t

val any_boxed_float : Flambda2_types.t

val any_boxed_int32 : Flambda2_types.t

val any_boxed_int64 : Flambda2_types.t

val any_boxed_nativeint : Flambda2_types.t

val any_naked_immediate : Flambda2_types.t

val any_naked_bool : 
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val any_naked_float32 : Flambda2_types.t

val any_naked_float : Flambda2_types.t

val any_naked_int8 : Flambda2_types.t

val any_naked_int16 : Flambda2_types.t

val any_naked_int32 : Flambda2_types.t

val any_naked_int64 : Flambda2_types.t

val any_naked_nativeint : Flambda2_types.t

val any_region : Flambda2_types.t

val any_rec_info : Flambda2_types.t

val this_tagged_immediate : 
  Flambda2_numbers.Target_ocaml_int.t ->
  Flambda2_types.t

Building of types representing tagged / boxed values from specified constants.

val this_boxed_float32 : 
  Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_float : 
  Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_int32 : 
  Flambda2_numbers.Numeric_types.Int32.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_int64 : 
  Flambda2_numbers.Numeric_types.Int64.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_nativeint : 
  Flambda2_numbers.Targetint_32_64.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_vec128 : 
  Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_vec256 : 
  Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_boxed_vec512 : 
  Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val these_tagged_immediates : 
  Flambda2_numbers.Target_ocaml_int.Set.t ->
  Flambda2_types.t

val these_boxed_float32s : 
  Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.Set.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val these_boxed_floats : 
  Flambda2_numbers.Numeric_types.Float_by_bit_pattern.Set.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val these_boxed_int32s : 
  Flambda2_numbers.Numeric_types.Int32.Set.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val these_boxed_int64s : 
  Flambda2_numbers.Numeric_types.Int64.Set.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val these_boxed_nativeints : 
  Flambda2_numbers.Targetint_32_64.Set.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_naked_immediate : 
  Flambda2_numbers.Target_ocaml_int.t ->
  Flambda2_types.t

Building of types representing untagged / unboxed values from specified constants.

val this_naked_float32 : 
  Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t ->
  Flambda2_types.t

val this_naked_float : 
  Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t ->
  Flambda2_types.t

val this_naked_int8 : Flambda2_numbers.Numeric_types.Int8.t -> Flambda2_types.t

val this_naked_int16 : 
  Flambda2_numbers.Numeric_types.Int16.t ->
  Flambda2_types.t

val this_naked_int32 : 
  Flambda2_numbers.Numeric_types.Int32.t ->
  Flambda2_types.t

val this_naked_int64 : 
  Flambda2_numbers.Numeric_types.Int64.t ->
  Flambda2_types.t

val this_naked_nativeint : 
  Flambda2_numbers.Targetint_32_64.t ->
  Flambda2_types.t

val this_naked_vec128 : 
  Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t ->
  Flambda2_types.t

val this_naked_vec256 : 
  Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t ->
  Flambda2_types.t

val this_naked_vec512 : 
  Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t ->
  Flambda2_types.t

val this_rec_info : Flambda2_term_basics.Rec_info_expr.t -> Flambda2_types.t

val these_naked_immediates : 
  Flambda2_numbers.Target_ocaml_int.Set.t ->
  Flambda2_types.t

val these_naked_float32s : 
  Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.Set.t ->
  Flambda2_types.t

val these_naked_floats : 
  Flambda2_numbers.Numeric_types.Float_by_bit_pattern.Set.t ->
  Flambda2_types.t

val these_naked_int8s : 
  Flambda2_numbers.Numeric_types.Int8.Set.t ->
  Flambda2_types.t

val these_naked_int16s : 
  Flambda2_numbers.Numeric_types.Int16.Set.t ->
  Flambda2_types.t

val these_naked_int32s : 
  Flambda2_numbers.Numeric_types.Int32.Set.t ->
  Flambda2_types.t

val these_naked_int64s : 
  Flambda2_numbers.Numeric_types.Int64.Set.t ->
  Flambda2_types.t

val these_naked_nativeints : 
  Flambda2_numbers.Targetint_32_64.Set.t ->
  Flambda2_types.t

val boxed_float32_alias_to : 
  naked_float32:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_float_alias_to : 
  naked_float:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val tagged_int8_alias_to : 
  naked_int8:Flambda2_identifiers.Variable.t ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val tagged_int16_alias_to : 
  naked_int16:Flambda2_identifiers.Variable.t ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val boxed_int32_alias_to : 
  naked_int32:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_int64_alias_to : 
  naked_int64:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_nativeint_alias_to : 
  naked_nativeint:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_vec128_alias_to : 
  naked_vec128:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_vec256_alias_to : 
  naked_vec256:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val boxed_vec512_alias_to : 
  naked_vec512:Flambda2_identifiers.Variable.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_float32 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_float : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_int32 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_int64 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_nativeint : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_vec128 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_vec256 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val box_vec512 : 
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val tagged_immediate_alias_to : 
  naked_immediate:Flambda2_identifiers.Variable.t ->
  Flambda2_types.t

val tag_immediate : Flambda2_types.t -> Flambda2_types.t

val any_block : Flambda2_types.t

val immutable_block : 
  machine_width:Target_system.Machine_width.t ->
  is_unique:bool ->
  Flambda2_kinds.Tag.t ->
  shape:Flambda2_kinds.Flambda_kind.Block_shape.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  fields:Flambda2_types.t list ->
  Flambda2_types.t

The type of an immutable block with a known tag, size and field types.

val immutable_block_with_size_at_least : 
  machine_width:Target_system.Machine_width.t ->
  tag:Flambda2_kinds.Tag.t Flambda2_lattices.Or_unknown.t ->
  n:Flambda2_numbers.Target_ocaml_int.t ->
  shape:Flambda2_kinds.Flambda_kind.Block_shape.t ->
  field_n_minus_one:Flambda2_identifiers.Variable.t ->
  Flambda2_types.t

The type of an immutable block with at least n fields and an unknown tag. The type of the n - 1th field is taken to be an Equals to the given variable.

val mutable_block : 
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val variant : 
  machine_width:Target_system.Machine_width.t ->
  const_ctors:Flambda2_types.t ->
  non_const_ctors:
    (Flambda2_kinds.Flambda_kind.Block_shape.t * Flambda2_types.t list)
      Flambda2_kinds.Tag.Scannable.Map.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.t

val this_immutable_string : 
  string ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val mutable_string : 
  size:int ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.t

val exactly_this_closure : 
  Flambda2_identifiers.Function_slot.t ->
  all_function_slots_in_set:
    Flambda2_types.Function_type.t Flambda2_lattices.Or_unknown.t
      Flambda2_identifiers.Function_slot.Map.t ->
  all_closure_types_in_set:
    Flambda2_types.t Flambda2_identifiers.Function_slot.Map.t ->
  all_value_slots_in_set:
    Flambda2_types.flambda_type Flambda2_identifiers.Value_slot.Map.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.flambda_type

val closure_with_at_least_these_function_slots : 
  this_function_slot:Flambda2_identifiers.Function_slot.t ->
  Flambda2_term_basics.Simple.t Flambda2_identifiers.Function_slot.Map.t ->
  Flambda2_types.flambda_type

val closure_with_at_least_this_value_slot : 
  this_function_slot:Flambda2_identifiers.Function_slot.t ->
  Flambda2_identifiers.Value_slot.t ->
  value_slot_var:Flambda2_identifiers.Variable.t ->
  value_slot_kind:Flambda2_kinds.Flambda_kind.t ->
  Flambda2_types.flambda_type

val closure_with_at_least_these_value_slots : 
  this_function_slot:Flambda2_identifiers.Function_slot.t ->
  (Flambda2_identifiers.Variable.t * Flambda2_kinds.Flambda_kind.t)
    Flambda2_identifiers.Value_slot.Map.t ->
  Flambda2_types.flambda_type

val array_of_length : 
  element_kind:
    Flambda2_kinds.Flambda_kind.With_subkind.t
      Flambda2_lattices.Or_unknown_or_bottom.t ->
  length:Flambda2_types.flambda_type ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.flambda_type

val mutable_array : 
  element_kind:
    Flambda2_kinds.Flambda_kind.With_subkind.t
      Flambda2_lattices.Or_unknown_or_bottom.t ->
  length:Flambda2_types.flambda_type ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  Flambda2_types.flambda_type

val immutable_array : 
  element_kind:
    Flambda2_kinds.Flambda_kind.With_subkind.t
      Flambda2_lattices.Or_unknown_or_bottom.t ->
  fields:Flambda2_types.flambda_type list ->
  Flambda2_term_basics.Alloc_mode.For_types.t ->
  machine_width:Target_system.Machine_width.t ->
  Flambda2_types.flambda_type

val alias_type_of : 
  Flambda2_kinds.Flambda_kind.t ->
  Flambda2_term_basics.Simple.t ->
  Flambda2_types.t

Construct a type equal to the type of the given name. (The name must be present in the given environment when calling e.g. join.)

val kind : Flambda2_types.t -> Flambda2_kinds.Flambda_kind.t

Determine the (unique) kind of a type.

val unknown_types_from_arity : 
  machine_width:Target_system.Machine_width.t ->
  [ `Unarized ] Flambda2_kinds.Flambda_arity.t ->
  Flambda2_types.t list

For each of the kinds in an arity, create an "unknown" type.

val is_bottom : Flambda2_types.Typing_env.t -> Flambda2_types.t -> bool

Whether the given type says that a term of that type can never be constructed (in other words, it is Invalid).

val is_unknown : Flambda2_types.Typing_env.t -> Flambda2_types.t -> bool

val is_alias_to_a_symbol : Flambda2_types.t -> bool

val type_for_const : Flambda2_identifiers.Reg_width_const.t -> Flambda2_types.t

val kind_for_const : 
  Flambda2_identifiers.Reg_width_const.t ->
  Flambda2_kinds.Flambda_kind.t

type 'a meet_shortcut = private

| Known_result of 'a
| Need_meet
| Invalid

type 'a proof_of_property = private

| Proved of 'a
| Unknown

val prove_equals_tagged_immediates : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Target_ocaml_int.Set.t Flambda2_types.proof_of_property

val meet_equals_tagged_immediates : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Target_ocaml_int.Set.t Flambda2_types.meet_shortcut

val meet_naked_immediates : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Target_ocaml_int.Set.t Flambda2_types.meet_shortcut

val meet_equals_single_tagged_immediate : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Target_ocaml_int.t Flambda2_types.meet_shortcut

val meet_naked_float32s : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.Set.t
    Flambda2_types.meet_shortcut

val meet_naked_floats : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Float_by_bit_pattern.Set.t
    Flambda2_types.meet_shortcut

val meet_naked_int8s : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Int8.Set.t Flambda2_types.meet_shortcut

val meet_naked_int16s : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Int16.Set.t Flambda2_types.meet_shortcut

val meet_naked_int32s : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Int32.Set.t Flambda2_types.meet_shortcut

val meet_naked_int64s : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Numeric_types.Int64.Set.t Flambda2_types.meet_shortcut

val meet_naked_nativeints : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Targetint_32_64.Set.t Flambda2_types.meet_shortcut

type variant_like_proof = private {

const_ctors : Flambda2_numbers.Target_ocaml_int.Set.t Flambda2_lattices.Or_unknown.t;
non_const_ctors_with_sizes : (Flambda2_numbers.Target_ocaml_int.t * Flambda2_kinds.Flambda_kind.Block_shape.t) Flambda2_kinds.Tag.Scannable.Map.t;

}

val meet_variant_like : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.variant_like_proof Flambda2_types.meet_shortcut

val prove_variant_like : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.variant_like_proof Flambda2_types.proof_of_property

type boxed_or_tagged_number = private

| Boxed of Flambda2_term_basics.Alloc_mode.For_types.t * Flambda2_kinds.Flambda_kind.Boxable_number.t * Flambda2_types.t
| Tagged_immediate

If ty is known to represent a boxed number or a tagged integer, prove_is_a_boxed_number env ty is Proved (alloc_mode,kind,contents_ty). kind is the kind of the unboxed number.

If ty is known to represent something of kind value that is not a number prove_is_a_boxed_number env ty is Invalid.

Otherwise it is Unknown or Wrong_kind when ty is not of kind value.

val prove_is_a_boxed_or_tagged_number : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.boxed_or_tagged_number Flambda2_types.proof_of_property

val prove_nothing : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  _ Flambda2_types.proof_of_property

val prove_is_a_tagged_immediate : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_float32 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_float : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_int32 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_int64 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_nativeint : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_vec128 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_vec256 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_a_boxed_vec512 : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val prove_is_or_is_not_a_boxed_float : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  bool Flambda2_types.proof_of_property

val prove_unique_tag_and_size : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_kinds.Tag.t
   * Flambda2_kinds.Flambda_kind.Block_shape.t
   * Flambda2_numbers.Target_ocaml_int.t)
    Flambda2_types.proof_of_property

val prove_unique_fully_constructed_immutable_heap_block : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_kinds.Tag.t
   * Flambda2_kinds.Flambda_kind.Block_shape.t
   * Flambda2_numbers.Target_ocaml_int.t
   * Flambda2_term_basics.Simple.t list)
    Flambda2_types.proof_of_property

val prove_is_int : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  bool Flambda2_types.proof_of_property

val prove_is_not_a_pointer : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  bool Flambda2_types.proof_of_property

val meet_is_flat_float_array : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  bool Flambda2_types.meet_shortcut

val meet_is_non_empty_naked_number_array : 
  Flambda2_kinds.Flambda_kind.Naked_number_kind.t ->
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.meet_shortcut

val prove_is_immediates_array : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  unit Flambda2_types.proof_of_property

val meet_is_immutable_array : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_kinds.Flambda_kind.With_subkind.t
     Flambda2_lattices.Or_unknown_or_bottom.t
   * Flambda2_types.t array
   * Flambda2_term_basics.Alloc_mode.For_types.t)
    Flambda2_types.meet_shortcut

val prove_is_immutable_array : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_kinds.Flambda_kind.With_subkind.t
     Flambda2_lattices.Or_unknown_or_bottom.t
   * Flambda2_types.t array
   * Flambda2_term_basics.Alloc_mode.For_types.t)
    Flambda2_types.proof_of_property

val meet_single_closures_entry : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_identifiers.Function_slot.t
   * Flambda2_term_basics.Alloc_mode.For_types.t
   * Flambda2_types.Closures_entry.t
   * Flambda2_types.Function_type.t)
    Flambda2_types.meet_shortcut

val prove_single_closures_entry : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  (Flambda2_identifiers.Function_slot.t
   * Flambda2_term_basics.Alloc_mode.For_types.t
   * Flambda2_types.Closures_entry.t
   * Flambda2_types.Function_type.t)
    Flambda2_types.proof_of_property

val meet_strings : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.String_info.Set.t Flambda2_types.meet_shortcut

val prove_strings : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.String_info.Set.t Flambda2_types.proof_of_property

val prove_tagging_of_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.proof_of_property

Attempt to show that the provided type describes the tagged version of a unique naked immediate Simple.

This function will return Unknown if values of the provided type might sometimes, but not always, be a tagged immediate (for example if it is a variant type involving blocks).

val meet_tagging_of_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

Attempt to show that the provided type _can_ describe, but might not always describe, the tagged version of a unique naked immediate Simple. It is guaranteed that if a Simple is returned, the type does not describe any other tagged immediate.

val meet_boxed_float32_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_float_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_int32_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_int64_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_nativeint_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_vec128_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_vec256_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_boxed_vec512_containing_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_block_field_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  field_kind:Flambda2_kinds.Flambda_kind.t ->
  Flambda2_types.t ->
  Flambda2_numbers.Target_ocaml_int.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_project_value_slot_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_identifiers.Value_slot.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_project_function_slot_simple : 
  Flambda2_types.Typing_env.t ->
  min_name_mode:Flambda2_nominal.Name_mode.t ->
  Flambda2_types.t ->
  Flambda2_identifiers.Function_slot.t ->
  Flambda2_term_basics.Simple.t Flambda2_types.meet_shortcut

val meet_rec_info : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Rec_info_expr.t Flambda2_types.meet_shortcut

val prove_alloc_mode_of_boxed_number : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_term_basics.Alloc_mode.For_types.t Flambda2_types.proof_of_property

val prove_physical_equality : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.t ->
  bool Flambda2_types.proof_of_property

type to_lift = private

| Immutable_block of {
1. tag : Flambda2_kinds.Tag.Scannable.t;
2. is_unique : bool;
3. shape : Flambda2_kinds.Flambda_kind.Scannable_block_shape.t;
4. fields : Flambda2_term_basics.Simple.t list;
}
| Boxed_float32 of Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t
| Boxed_float of Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t
| Boxed_int32 of Flambda2_numbers.Numeric_types.Int32.t
| Boxed_int64 of Flambda2_numbers.Numeric_types.Int64.t
| Boxed_nativeint of Flambda2_numbers.Targetint_32_64.t
| Boxed_vec128 of Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t
| Boxed_vec256 of Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t
| Boxed_vec512 of Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t
| Immutable_float32_array of {
1. fields : Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t list;
}
| Immutable_float_array of {
1. fields : Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t list;
}
| Immutable_int_array of {
1. fields : Flambda2_numbers.Target_ocaml_int.t list;
}
| Immutable_int8_array of {
1. fields : Flambda2_numbers.Numeric_types.Int8.t list;
}
| Immutable_int16_array of {
1. fields : Flambda2_numbers.Numeric_types.Int16.t list;
}
| Immutable_int32_array of {
1. fields : Stdlib.Int32.t list;
}
| Immutable_int64_array of {
1. fields : Stdlib.Int64.t list;
}
| Immutable_nativeint_array of {
1. fields : Flambda2_numbers.Targetint_32_64.t list;
}
| Immutable_vec128_array of {
1. fields : Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t list;
}
| Immutable_vec256_array of {
1. fields : Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t list;
}
| Immutable_vec512_array of {
1. fields : Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t list;
}
| Immutable_value_array of {
1. fields : Flambda2_term_basics.Simple.t list;
}
| Empty_array of Flambda2_term_basics.Empty_array_kind.t

type reification_result = private

| Lift of Flambda2_types.to_lift
| Simple of Flambda2_term_basics.Simple.t
| Cannot_reify
| Invalid

val reify : 
  allowed_if_free_vars_defined_in:Flambda2_types.Typing_env.t ->
  var_is_defined_at_toplevel:(Flambda2_identifiers.Variable.t -> bool) ->
  var_is_symbol_projection:(Flambda2_identifiers.Variable.t -> bool) ->
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.reification_result

val never_holds_locally_allocated_values : 
  Flambda2_types.Typing_env.t ->
  Flambda2_identifiers.Variable.t ->
  unit Flambda2_types.proof_of_property

val remove_outermost_alias : 
  Flambda2_types.Typing_env.t ->
  Flambda2_types.t ->
  Flambda2_types.t

module Equal_types_for_debug : sig ... end

module Rewriter : sig ... end

Module Flambda2_types

Module `Flambda2_types`