Module `Axis_lattice`

type t = private int

val bot : t

Lattice operations expected by the solver.

val top : t

val join : t -> t -> t

val meet : t -> t -> t

val leq : t -> t -> bool

val co_sub : t -> t -> t

val equal : t -> t -> bool

val hash : t -> int

val to_string : t -> string

val non_bot_axes : t -> int list

val of_axis_set : Jkind_axis.Axis_set.t -> t

Build a mask from a set of relevant axes.

val mask_of_modality : Mode.Modality.Const.t -> t

Relevant axes of a constant modality and the corresponding mask.

val create : 
  areality:Mode.Regionality.Const.t ->
  linearity:Mode.Linearity.Const.t ->
  uniqueness:Mode.Uniqueness.Const.t ->
  portability:Mode.Portability.Const.t ->
  contention:Mode.Contention.Const.t ->
  forkable:Mode.Forkable.Const.t ->
  yielding:Mode.Yielding.Const.t ->
  statefulness:Mode.Statefulness.Const.t ->
  visibility:Mode.Visibility.Const.t ->
  staticity:Mode.Staticity.const ->
  externality:Jkind_axis.Externality.t ->
  t

val areality : t -> Mode.Regionality.Const.t

val linearity : t -> Mode.Linearity.Const.t

val uniqueness : t -> Mode.Uniqueness.Const.t

val portability : t -> Mode.Portability.Const.t

val contention : t -> Mode.Contention.Const.t

val forkable : t -> Mode.Forkable.Const.t

val yielding : t -> Mode.Yielding.Const.t

val statefulness : t -> Mode.Statefulness.Const.t

val visibility : t -> Mode.Visibility.Const.t

val staticity : t -> Mode.Staticity.const

val externality : t -> Jkind_axis.Externality.t

val to_mode_crossing : t -> Mode.Crossing.t

val nonfloat_value : t

Canonical lattice constants used by ikinds.

val immutable_data : t

val mutable_data : t

val sync_data : t

val value : t

val arrow : t

val immediate : t

val object_legacy : t

val axis_number_to_axis_packed : int -> Jkind_axis.Axis.packed

Map from internal axis number (used in diagnostics) to an axis descriptor.

Module Axis_lattice

Module `Axis_lattice`