Module Mode.Value

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

module Monadic : sig ... end
module Comonadic : sig ... end
module Axis : sig ... end
type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) modes = {
  1. areality : 'a;
  2. linearity : 'b;
  3. uniqueness : 'c;
  4. portability : 'd;
  5. contention : 'e;
  6. forkable : 'f;
  7. yielding : 'g;
  8. statefulness : 'h;
  9. visibility : 'i;
  10. staticity : 'j;
}
module Const : sig ... end
type error =
  1. | Monadic of Monadic.error
  2. | Comonadic of Comonadic.error
type 'a simple_axerror := 'a simple_error
type simple_error =
  1. | Error : 'a Axis.t * 'a simple_axerror -> simple_error
include Mode_intf.Common with module Const := Const and type error := error and type simple_error := simple_error and type 'd t := 'd t

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.

type equate_error = Mode_intf.equate_step * error
val to_simple_error : error -> simple_error

Left-only mode

Right-only mode

Left-right mode

include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd t
type (_, _, '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.

val min : lr
val max : lr
val legacy : lr
val 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.

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

val equate_exn : lr -> lr -> unit
val join : (Allowance.allowed * 'r) t list -> Allowance.left_only t
val meet : ('l * Allowance.allowed) t list -> Allowance.right_only t
val newvar_above : (Allowance.allowed * 'r) t -> ('l * 'r_) t * bool
val newvar_below : ('l * Allowance.allowed) t -> ('l_ * 'r) t * bool
val print : ?verbose:bool -> unit -> Format.formatter -> ('l * 'r) t -> unit
val zap_to_ceil : ('l * Allowance.allowed) t -> Const.t
val 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
val to_const_exn : lr -> Const.t
module List : sig ... end
val proj_comonadic : 'a Comonadic.Axis.t -> ('l * 'r) t -> ('a, 'l * 'r) mode
val proj_monadic : 'a Monadic.Axis.t -> ('l * 'r) t -> ('a, 'r * 'l) mode
val meet_const : Comonadic.Const.t -> ('l * 'r) t -> ('l * 'r) t
val 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
val meet_with : 'a Comonadic.Axis.t -> 'a -> ('l * 'r) t -> ('l * 'r) t
val join_with : 'a Monadic.Axis.t -> 'a -> ('l * 'r) t -> ('l * 'r) t
val 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

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

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