Module `Mode.Value`Source

The most general mode. Used in most type checking, including in value bindings in Env

Sourcemodule Monadic : sig ... end

Sourcemodule Comonadic : sig ... end

Sourcemodule Axis : sig ... end

Sourcetype ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) modes = {

areality : 'a;
linearity : 'b;
uniqueness : 'c;
portability : 'd;
contention : 'e;
forkable : 'f;
yielding : 'g;
statefulness : 'h;
visibility : 'i;
staticity : 'j;

}

Sourcemodule Const : sig ... end

Sourcetype atom =

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

Existentially holds a mode together with its axis.

Sourcetype error =

| Monadic of Monadic.error
| Comonadic of Comonadic.error

type 'a simple_axerror := 'a simple_error

Sourcetype simple_error =

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

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

include Mode_intf.Common
  with module Const := Const
   and type error := error
   and type simple_error := simple_error
   and type 'd t := 'd t

Sourceval print_error : Mode_hint.pinpoint -> error -> Mode_intf.print_error

Takes a submode error accompanied by a pinpoint of the original submode, returns an explaining printer for each side. Each printer prints either a mode constant name, or "mode because ...". The function assumes pinpoint is already printed, which allows simplifying its own printing. The caller is responsible for printing pinpoint and placing the result of this function in a suitable linguistic context.

Sourcetype equate_error = Mode_intf.equate_step * error

Sourceval to_simple_error : error -> simple_error

Sourcetype l = (Allowance.allowed * Allowance.disallowed) t

Left-only mode

Sourcetype r = (Allowance.disallowed * Allowance.allowed) t

Right-only mode

Sourcetype lr = (Allowance.allowed * Allowance.allowed) t

Left-right mode

include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd t

Sourcetype (_, _, 'd) sided = 'd t

val disallow_right : 
  ('a, 'b, 'l * 'r) sided ->
  ('a, 'b, 'l * Allowance.disallowed) sided

Disallows on the right.

val disallow_left : 
  ('a, 'b, 'l * 'r) sided ->
  ('a, 'b, Allowance.disallowed * 'r) sided

Disallows a the left.

val allow_right : 
  ('a, 'b, 'l * Allowance.allowed) sided ->
  ('a, 'b, 'l * 'r) sided

Generalizes a right-hand-side allowed to be any allowance.

val allow_left : 
  ('a, 'b, Allowance.allowed * 'r) sided ->
  ('a, 'b, 'l * 'r) sided

Generalizes a left-hand-side allowed to be any allowance.

Sourceval min : lr

Sourceval max : lr

Sourceval legacy : lr

Sourceval newvar : unit -> ('l * 'r) t

val submode : 
  ?pp:Mode_hint.pinpoint ->
  (Allowance.allowed * 'r) t ->
  ('l * Allowance.allowed) t ->
  (unit, error) result

Takes the actual and expected mode of something, check that the actual mode is less than the expected mode. In case of error, the error is returned and no mutation is done.

The two modes should be hinted sufficently that the submode is self-evident. In particular, the two modes should be about the "same thing". See the notes How to submode for details.

val submode_err : 
  Mode_hint.pinpoint ->
  (Allowance.allowed * 'r) t ->
  ('l * Allowance.allowed) t ->
  unit

Similar to submode, but instead of returning an error, raise user-friendly errors directly, with pinpoint describing the thing whose actual and expected modes are being checked.

If you need more than pinpoint as the context in the error message, consider submode.

Sourceval equate : lr -> lr -> (unit, equate_error) result

val submode_exn : 
  ?pp:Mode_hint.pinpoint ->
  (Allowance.allowed * 'r) t ->
  ('l * Allowance.allowed) t ->
  unit

Similiar to submode, but crashes the compiler if errors. Use this function if the submode is guaranteed to succeed.

Sourceval equate_exn : lr -> lr -> unit

Sourceval join : (Allowance.allowed * 'r) t list -> Allowance.left_only t

Sourceval meet : ('l * Allowance.allowed) t list -> Allowance.right_only t

Sourceval newvar_above : (Allowance.allowed * 'r) t -> ('l * 'r_) t * bool

Sourceval newvar_below : ('l * Allowance.allowed) t -> ('l_ * 'r) t * bool

val print : 
  ?verbose:bool ->
  unit ->
  Ocaml_typing.Mode_intf.Fmt.formatter ->
  ('l * 'r) t ->
  unit

Sourceval zap_to_ceil : ('l * Allowance.allowed) t -> Const.t

Sourceval zap_to_floor : (Allowance.allowed * 'r) t -> Const.t

val of_const : 
  ?hint_monadic:('l * 'r) Allowance.neg Hint.const ->
  ?hint_comonadic:('l * 'r) Allowance.pos Hint.const ->
  Const.t ->
  ('l * 'r) t

Sourceval to_const_exn : lr -> Const.t

Sourcemodule List : sig ... end

Sourceval proj_comonadic : 'a Comonadic.Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode

Sourceval proj_monadic : 'a Monadic.Axis.t -> ('l * 'r) t -> ('a, 'r * 'l) mode

Sourceval meet_const : Comonadic.Const.t -> ('l * 'r) t -> ('l * 'r) t

Sourceval join_const : Monadic.Const.t -> ('l * 'r) t -> ('l * 'r) t

val max_with_comonadic : 
  'a Comonadic.Axis.t ->
  ('a, 'l * 'r) mode ->
  (disallowed * 'r) t

max_with ax elt returns max but with the axis ax set to elt.

val min_with_comonadic : 
  'a Comonadic.Axis.t ->
  ('a, 'l * 'r) mode ->
  ('l * disallowed) t

min_with ax elt returns min but with the axis ax set to elt.

val min_with_monadic : 
  'a Monadic.Axis.t ->
  ('a, 'l * 'r) mode ->
  ('r * disallowed) t

Sourceval meet_const_with : 'a Comonadic.Axis.t -> 'a -> ('l * 'r) t -> ('l * 'r) t

Sourceval join_const_with : 'a Monadic.Axis.t -> 'a -> ('l * 'r) t -> ('l * 'r) t

Sourceval zap_to_legacy : lr -> Const.t

val comonadic_to_monadic_min : 
  ?hint:('r * disallowed) Allowance.neg Hint.morph ->
  ('l * 'r) Comonadic.t ->
  ('r * disallowed) Monadic.t

val monadic_to_comonadic_max : 
  ('r * disallowed) Monadic.t ->
  (disallowed * 'r) Comonadic.t

val close_over : 
  (('l * allowed) Monadic.t, (allowed * 'r) Comonadic.t) monadic_comonadic ->
  l

Returns the lower bound needed for B -> C in relation to A

Sourceval partial_apply : (allowed * 'r) t -> l

Returns the lower bound needed for B -> C in relation to A -> B -> C