Module `Mode.Crossing`Source

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.

Sourcemodule Monadic : sig ... end

Sourcemodule Comonadic : sig ... end

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

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

Sourcemodule Axis : sig ... end

Source

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

For interfacing with the user only; potentially slow.

Source

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.

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

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

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

Set the specified axis to the specified crossing.

include Mode_intf.Lattice with type t := t

Sourceval min : t

Sourceval max : t

Sourceval le : t -> t -> bool

Sourceval equal : t -> t -> bool

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

Sourceval join : t -> t -> t

Sourceval meet : t -> t -> t

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

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

Sourceval apply_left : t -> ('l * 'r) Value.t -> ('l * disallowed) Value.t

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

Sourceval apply_right : t -> ('l * 'r) Value.t -> (disallowed * 'r) Value.t

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

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

Similar to apply_left but for Alloc via alloc_as_value

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

Similar to apply_right but for Alloc via alloc_as_value

Source

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.

Sourceval print : Ocaml_typing.Mode_intf.Fmt.formatter -> t -> unit

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

Module Mode.CrossingSource

Module `Mode.Crossing`Source