Module `Mode.Modality`

module Comonadic : sig ... end

module Monadic : sig ... end

module Axis : sig ... end

type atom =

| Atom : 'a Ocaml_typing.Mode.Modality.Axis.t * 'a -> Ocaml_typing.Mode.Modality.atom

module Per_axis : sig ... end

type error =

| Error : 'a Ocaml_typing.Mode.Modality.Axis.t * 'a Ocaml_typing.Mode.simple_error -> Ocaml_typing.Mode.Modality.error

type nonrec equate_error =
  Ocaml_typing.Mode.equate_step * Ocaml_typing.Mode.Modality.error

module Const : sig ... end

type t

A modality that acts on Value modes. Conceptually it is a record where individual fields can be set or proj.

val id : Ocaml_typing.Mode.Modality.t

The identity modality.

val undefined : Ocaml_typing.Mode.Modality.t

The undefined modality.

val apply : 
  Ocaml_typing.Mode.Modality.t ->
  (Ocaml_typing.Mode.allowed * 'r) Ocaml_typing.Mode.Value.t ->
  Ocaml_typing.Mode.Value.l

Apply a modality on a left mode. The calller should ensure that apply t m is only called for m >= md_mode for inferred modalities.

val sub : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.t ->
  (unit, Ocaml_typing.Mode.Modality.error) Stdlib.Result.t

sub t0 t1 checks that t0 <= t1. Definition: t0 <= t1 iff forall a. t0(a) <= t1(a).

In case of failure, Error (ax, {left; right}) is returned, where ax is the axis on which the modalities disagree. left is the projection of t0 on ax, and right is the projection of t1 on ax.

val equate : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.t ->
  (unit, Ocaml_typing.Mode.Modality.equate_error) Stdlib.Result.t

equate t0 t1 checks that t0 = t1. Definition: t0 = t1 iff t0 <= t1 and t1 <= t0.

val print : Stdlib.Format.formatter -> Ocaml_typing.Mode.Modality.t -> unit

Printing for debugging.

val infer : 
  md_mode:Ocaml_typing.Mode.Value.lr ->
  mode:Ocaml_typing.Mode.Value.lr ->
  Ocaml_typing.Mode.Modality.t

Given md_mode the mode of a module, and mode the mode of a value to be put in that module, return the inferred modality to be put on the value description in the inferred module type.

The caller should ensure that for comonadic axes, md_mode >= mode.

val zap_to_id : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.Const.t

Zap an inferred modality towards identity modality.

val zap_to_floor : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.Const.t

Zap an inferred modality towards the lowest (strongest) modality.

val to_const_exn : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.Const.t

Asserts the given modality is a const modality, and returns it.

val to_const_opt : 
  Ocaml_typing.Mode.Modality.t ->
  Ocaml_typing.Mode.Modality.Const.t option

Checks if the given modality is a const modality

val of_const : 
  Ocaml_typing.Mode.Modality.Const.t ->
  Ocaml_typing.Mode.Modality.t

Inject a constant modality.

val max : Ocaml_typing.Mode.Modality.t

The top modality; sub x max succeeds for any x.

Module Mode.Modality

Module `Mode.Modality`