jon.recoil.org

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 = t
val print : Format.formatter -> t -> unit
val arity_of_list : t list -> [ `Unarized ] Flambda2_kinds.Flambda_arity.t
val apply_renaming : t -> Flambda2_nominal.Renaming.t -> t
include Flambda2_nominal.Contains_ids.S with type t := t
val ids_for_export : t -> Flambda2_nominal.Ids_for_export.t

Gather all table identifiers to export them.

val remove_unused_value_slots_and_shortcut_aliases : t -> used_value_slots:Flambda2_identifiers.Value_slot.Set.t -> canonicalise:(Flambda2_term_basics.Simple.t -> Flambda2_term_basics.Simple.t) -> 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
module Join_analysis : sig ... end
module Function_type : sig ... end
module Closures_entry : sig ... end
type to_erase =
  1. | Everything_not_in of Typing_env.t
  2. | All_variables_except of Flambda2_identifiers.Variable.Set.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.

Construct a bottom type of the given kind.

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

val bottom_like : t -> t

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

val unknown_like : t -> t

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

val any_value : t
val any_tagged_immediate : t
val any_tagged_immediate_or_null : t
val any_tagged_bool : machine_width:Target_system.Machine_width.t -> t
val any_boxed_float32 : t
val any_boxed_float : t
val any_boxed_int32 : t
val any_boxed_int64 : t
val any_boxed_nativeint : t
val any_naked_immediate : t
val any_naked_bool : machine_width:Target_system.Machine_width.t -> t
val any_naked_float32 : t
val any_naked_float : t
val any_naked_int8 : t
val any_naked_int16 : t
val any_naked_int32 : t
val any_naked_int64 : t
val any_naked_nativeint : t
val any_region : t
val any_rec_info : t
val this_tagged_immediate : Flambda2_numbers.Target_ocaml_int.t -> t

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

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

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

val this_naked_int8 : Flambda2_numbers.Numeric_types.Int8.t -> t
val this_naked_int16 : Flambda2_numbers.Numeric_types.Int16.t -> t
val this_naked_int32 : Flambda2_numbers.Numeric_types.Int32.t -> t
val this_naked_int64 : Flambda2_numbers.Numeric_types.Int64.t -> t
val this_naked_nativeint : Flambda2_numbers.Targetint_32_64.t -> t
val these_naked_immediates : Flambda2_numbers.Target_ocaml_int.Set.t -> t
val these_naked_int8s : Flambda2_numbers.Numeric_types.Int8.Set.t -> t
val these_naked_int16s : Flambda2_numbers.Numeric_types.Int16.Set.t -> t
val these_naked_int32s : Flambda2_numbers.Numeric_types.Int32.Set.t -> t
val these_naked_int64s : Flambda2_numbers.Numeric_types.Int64.Set.t -> t
val these_naked_nativeints : Flambda2_numbers.Targetint_32_64.Set.t -> t
val tagged_int8_alias_to : naked_int8:Flambda2_identifiers.Variable.t -> machine_width:Target_system.Machine_width.t -> t
val tagged_int16_alias_to : naked_int16:Flambda2_identifiers.Variable.t -> machine_width:Target_system.Machine_width.t -> t
val boxed_nativeint_alias_to : naked_nativeint:Flambda2_identifiers.Variable.t -> Flambda2_bound_identifiers.Alloc_mode.For_types.t -> t
val tagged_immediate_alias_to : naked_immediate:Flambda2_identifiers.Variable.t -> t
val tag_immediate : t -> t
val any_block : t

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

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 this_immutable_string : string -> machine_width:Target_system.Machine_width.t -> t
val mutable_string : size:int -> machine_width:Target_system.Machine_width.t -> t
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 -> flambda_type

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.)

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 -> t list

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

val is_bottom : Typing_env.t -> 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 : Typing_env.t -> t -> bool
val is_unknown_maybe_null : Typing_env.t -> t -> bool

Whether the given type contains no information, except about nullability (i.e. returns `true` for both `value` and `value_or_null`, whereas `is_unknown` returns `false` for `value` because we know something -- it can't be `null`).

val is_alias_to_a_symbol : t -> bool
type 'a meet_shortcut = private
  1. | Known_result of 'a
  2. | Need_meet
  3. | Invalid
type 'a proof_of_property = private
  1. | Proved of 'a
  2. | Unknown
val prove_equals_tagged_immediates : Typing_env.t -> t -> Flambda2_numbers.Target_ocaml_int.Set.t proof_of_property
val meet_equals_tagged_immediates : Typing_env.t -> t -> Flambda2_numbers.Target_ocaml_int.Set.t meet_shortcut
val meet_equals_single_tagged_immediate : Typing_env.t -> t -> Flambda2_numbers.Target_ocaml_int.t meet_shortcut
val meet_variant_like : Typing_env.t -> t -> variant_like_proof meet_shortcut
val prove_variant_like : Typing_env.t -> t -> variant_like_proof proof_of_property
type boxed_or_tagged_number = private
  1. | Boxed of Flambda2_bound_identifiers.Alloc_mode.For_types.t * Flambda2_kinds.Flambda_kind.Boxable_number.t * t
  2. | 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 : Typing_env.t -> t -> boxed_or_tagged_number proof_of_property
val prove_nothing : Typing_env.t -> t -> _ proof_of_property
val prove_is_a_tagged_immediate : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_float32 : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_float : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_int32 : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_int64 : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_nativeint : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_vec128 : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_vec256 : Typing_env.t -> t -> unit proof_of_property
val prove_is_a_boxed_vec512 : Typing_env.t -> t -> unit proof_of_property
val prove_is_or_is_not_a_boxed_float : Typing_env.t -> t -> bool proof_of_property
val prove_is_int : Typing_env.t -> t -> bool proof_of_property
val prove_is_not_a_pointer : Typing_env.t -> t -> bool proof_of_property
val meet_is_flat_float_array : Typing_env.t -> t -> bool meet_shortcut
val meet_is_non_empty_naked_number_array : Flambda2_kinds.Flambda_kind.Naked_number_kind.t -> Typing_env.t -> t -> unit meet_shortcut
val prove_is_immediates_array : Typing_env.t -> t -> unit proof_of_property
val meet_single_closures_entry : Typing_env.t -> t -> (Flambda2_identifiers.Function_slot.t * Flambda2_bound_identifiers.Alloc_mode.For_types.t * Closures_entry.t * Function_type.t) meet_shortcut
val prove_single_closures_entry : Typing_env.t -> t -> (Flambda2_identifiers.Function_slot.t * Flambda2_bound_identifiers.Alloc_mode.For_types.t * Closures_entry.t * Function_type.t) 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 : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t 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 : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_float_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_int32_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_int64_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_nativeint_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_vec128_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_vec256_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val meet_boxed_vec512_containing_simple : Typing_env.t -> min_name_mode:Flambda2_nominal.Name_mode.t -> t -> Flambda2_term_basics.Simple.t meet_shortcut
val prove_physical_equality : Typing_env.t -> t -> t -> bool proof_of_property
type to_lift = private
  1. | 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;
    }
  2. | Boxed_float32 of Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t
  3. | Boxed_float of Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t
  4. | Boxed_int32 of Flambda2_numbers.Numeric_types.Int32.t
  5. | Boxed_int64 of Flambda2_numbers.Numeric_types.Int64.t
  6. | Boxed_nativeint of Flambda2_numbers.Targetint_32_64.t
  7. | Boxed_vec128 of Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t
  8. | Boxed_vec256 of Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t
  9. | Boxed_vec512 of Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t
  10. | Immutable_float32_array of {
    1. fields : Flambda2_numbers.Numeric_types.Float32_by_bit_pattern.t list;
    }
  11. | Immutable_float_array of {
    1. fields : Flambda2_numbers.Numeric_types.Float_by_bit_pattern.t list;
    }
  12. | Immutable_int_array of {
    1. fields : Flambda2_numbers.Target_ocaml_int.t list;
    }
  13. | Immutable_int8_array of {
    1. fields : Flambda2_numbers.Numeric_types.Int8.t list;
    }
  14. | Immutable_int16_array of {
    1. fields : Flambda2_numbers.Numeric_types.Int16.t list;
    }
  15. | Immutable_int32_array of {
    1. fields : Int32.t list;
    }
  16. | Immutable_int64_array of {
    1. fields : Int64.t list;
    }
  17. | Immutable_nativeint_array of {
    1. fields : Flambda2_numbers.Targetint_32_64.t list;
    }
  18. | Immutable_vec128_array of {
    1. fields : Flambda2_numbers.Vector_types.Vec128.Bit_pattern.t list;
    }
  19. | Immutable_vec256_array of {
    1. fields : Flambda2_numbers.Vector_types.Vec256.Bit_pattern.t list;
    }
  20. | Immutable_vec512_array of {
    1. fields : Flambda2_numbers.Vector_types.Vec512.Bit_pattern.t list;
    }
  21. | Immutable_value_array of {
    1. fields : Flambda2_term_basics.Simple.t list;
    }
  22. | Empty_array of Flambda2_term_basics.Empty_array_kind.t
type reification_result = private
  1. | Lift of to_lift
  2. | Simple of Flambda2_term_basics.Simple.t
  3. | Cannot_reify
  4. | Invalid
val reify : allowed_if_free_vars_defined_in:Typing_env.t -> var_is_defined_at_toplevel:(Flambda2_identifiers.Variable.t -> bool) -> var_is_symbol_projection:(Flambda2_identifiers.Variable.t -> bool) -> Typing_env.t -> t -> reification_result
val never_holds_locally_allocated_values : Typing_env.t -> Flambda2_identifiers.Variable.t -> unit proof_of_property
val remove_outermost_alias : Typing_env.t -> t -> t
module Equal_types_for_debug : sig ... end
module Rewriter : sig ... end