Crossing (merlin-lib.merlin-lib.ocaml_typing.Ocaml

Module Mode.Crossing

Some modes on an axis might be indistinguishable for values of some type, in which case the actual mode of values can be strenghthened (or equivalently the expected mode loosened) accordingly to make more programs mode-check. The capabilities/permissions to perform such adjustments are called mode crossing and depicted in this module.

We define an ordering on the crossings: t0 <= t1 iff t0 allows more adjustments than t1. By this ordering, the currently representable crossings form a lattice:

The bottom crossing allows any adjustments on this axis, which trivializes the axis.

The top crossing allows no adjustments on this axis, which is the safe default.

Joining two crossings gives a crossing that's less permissive than both.

Meeting two crossings gives a crossing that's more permissive than both.

module Monadic : sig ... end

module Comonadic : sig ... end

type t = (Monadic.t, Comonadic.t) monadic_comonadic

The mode crossing capability on all axes, split into monadic and comonadic fragments.

module Axis : sig ... end

module Per_axis : 
  Solver_intf.Lattices with type 'a elt := 'a and type 'a obj := 'a Axis.t

val create : 
  regionality:bool ->
  linearity:bool ->
  uniqueness:bool ->
  portability:bool ->
  contention:bool ->
  forkable:bool ->
  yielding:bool ->
  statefulness:bool ->
  visibility:bool ->
  staticity:bool ->
  t

Convenience for creating a mode crossing capability on all axes, using a boolean for each axis where true means full crossing and false means no crossing. Alternatively, call Monadic.create and Comonadic.create and pack the results into a record of type t.

val proj : 'a Axis.t -> t -> 'a

Project a mode crossing (of all axes) onto the specified axis.

val set : 'a Axis.t -> 'a -> t -> t

Set the specified axis to the specified crossing.

include Mode_intf.Lattice with type t := t

val min : t

val max : t

val le : t -> t -> bool

val equal : t -> t -> bool

equal a b is equivalent to le a b && le b a, but defined separately for performance reasons

val join : t -> t -> t

val meet : t -> t -> t

val modality : Modality.Const.t -> t -> t

modality m t gives the mode crossing of type T wrapped in modality m where T has mode crossing t.

val to_modality : t -> Modality.Const.t

Takes a mode crossing t, returns the modality needed to make max into t. More precisely, to_modality is the inverse of modality _ max.

val apply_left : t -> Value.l -> Value.l

Apply mode crossing on a left mode, making it stronger.

val apply_right : t -> Value.r -> Value.r

Apply mode crossing on a right mode, making it more permissive.

val apply_left_alloc : t -> Alloc.l -> Alloc.l

Similar to apply_left but for Alloc via alloc_as_value

val apply_right_alloc : t -> Alloc.r -> Alloc.r

Similar to apply_right but for Alloc via alloc_as_value

val apply_left_right_alloc : 
  t ->
  (Alloc.Monadic.r, Alloc.Comonadic.l) monadic_comonadic ->
  (Alloc.Monadic.r, Alloc.Comonadic.l) monadic_comonadic

Apply mode crossong on the left comonadic fragment, and the right monadic fragment.

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

Print the mode crossing by axis. Omit axes that do not cross.