Module `Mode.Modality`Source

Sourcemodule Comonadic : sig ... end

Sourcemodule Monadic : sig ... end

Sourcemodule Axis : sig ... end

Sourcetype atom =

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

Sourcemodule Per_axis : sig ... end

For interfacing with the user only; potentially slow.

Sourcetype error =

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

Sourcetype nonrec equate_error = equate_step * error

Sourcemodule Const : sig ... end

Sourcetype t

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

Sourceval undefined : t

The undefined modality.

Sourceval is_undefined : t -> bool

Check if the given modality is undefined.

Source

val apply : 
  ?hint:
    ((allowed * 'r) Allowance.neg Hint.morph,
      (allowed * 'r) Allowance.pos Hint.morph)
      monadic_comonadic ->
  t ->
  (allowed * 'r) Value.t ->
  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.

Sourceval sub : t -> t -> (unit, error) 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.

Sourceval equate : t -> t -> (unit, equate_error) Result.t

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

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

Printing for debugging.

Sourceval infer : md_mode:Value.lr -> mode:Value.lr -> 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.

Sourceval zap_to_id : t -> Const.t

Zap an inferred modality towards identity modality.

Sourceval zap_to_floor : t -> Const.t

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

Sourceval to_const_exn : t -> Const.t

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

Sourceval to_const_opt : t -> Const.t option

Checks if the given modality is a const modality

Sourceval of_const : Const.t -> t

Inject a constant modality.

Sourceval max : t

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

Module Mode.ModalitySource

Module `Mode.Modality`Source