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 ... endmodule Comonadic : sig ... endtype t =
(Ocaml_typing.Mode.Crossing.Monadic.t,
Ocaml_typing.Mode.Crossing.Comonadic.t)
Ocaml_typing.Mode.monadic_comonadicThe mode crossing capability on all axes, split into monadic and comonadic fragments.
module Axis : sig ... endmodule Per_axis :
Ocaml_typing.Solver_intf.Lattices
with type 'a elt := 'a
and type 'a obj := 'a Ocaml_typing.Mode.Crossing.Axis.tval create :
regionality:bool ->
linearity:bool ->
uniqueness:bool ->
portability:bool ->
contention:bool ->
forkable:bool ->
yielding:bool ->
statefulness:bool ->
visibility:bool ->
staticity:bool ->
Ocaml_typing.Mode.Crossing.tConvenience 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 Ocaml_typing.Mode.Crossing.Axis.t ->
Ocaml_typing.Mode.Crossing.t ->
'aProject a mode crossing (of all axes) onto the specified axis.
val set :
'a Ocaml_typing.Mode.Crossing.Axis.t ->
'a ->
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Crossing.tSet the specified axis to the specified crossing.
include Ocaml_typing.Mode_intf.Lattice
with type t := Ocaml_typing.Mode.Crossing.t
val min : Ocaml_typing.Mode.Crossing.tval max : Ocaml_typing.Mode.Crossing.tval le : Ocaml_typing.Mode.Crossing.t -> Ocaml_typing.Mode.Crossing.t -> boolval equal :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Crossing.t ->
boolequal a b is equivalent to le a b && le b a, but defined separately for performance reasons
val modality :
Ocaml_typing.Mode.Modality.Const.t ->
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Crossing.tmodality m t gives the mode crossing of type T wrapped in modality m where T has mode crossing t.
val to_modality :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Modality.Const.tTakes 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 :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Value.l ->
Ocaml_typing.Mode.Value.lApply mode crossing on a left mode, making it stronger.
val apply_right :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Value.r ->
Ocaml_typing.Mode.Value.rApply mode crossing on a right mode, making it more permissive.
val apply_left_alloc :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Alloc.l ->
Ocaml_typing.Mode.Alloc.lSimilar to apply_left but for Alloc via alloc_as_value
val apply_right_alloc :
Ocaml_typing.Mode.Crossing.t ->
Ocaml_typing.Mode.Alloc.r ->
Ocaml_typing.Mode.Alloc.rSimilar to apply_right but for Alloc via alloc_as_value
val apply_left_right_alloc :
Ocaml_typing.Mode.Crossing.t ->
(Ocaml_typing.Mode.Alloc.Monadic.r, Ocaml_typing.Mode.Alloc.Comonadic.l)
Ocaml_typing.Mode.monadic_comonadic ->
(Ocaml_typing.Mode.Alloc.Monadic.r, Ocaml_typing.Mode.Alloc.Comonadic.l)
Ocaml_typing.Mode.monadic_comonadicApply mode crossong on the left comonadic fragment, and the right monadic fragment.
val print : Stdlib.Format.formatter -> Ocaml_typing.Mode.Crossing.t -> unitPrint the mode crossing by axis. Omit axes that do not cross.