Source file mode.ml

(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*                    Zesen Qian, Jane Street, London                     *)
(*                                                                        *)
(*   Copyright 2024 Jane Street Group LLC                                 *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

(* warn on fragile matches *)
[@@@warning "+4"]

open Allowance
open Solver_intf
open Solver
open Mode_intf
module Hint = Mode_hint
module Fmt = Format_doc

module Hint_for_solver (* : Solver_intf.Hint *) = struct
  module Pinpoint = struct
    type t = Hint.pinpoint

    let unknown : t = Location.none, Unknown
  end

  module Morph = struct
    type 'd t = 'd Hint.morph

    let unknown : _ t = Unknown

    let id : _ t = Skip

    let left_adjoint : type l.
        Hint.pinpoint ->
        (l * allowed) t ->
        Hint.pinpoint * (allowed * disallowed) t =
     fun pp t ->
      match t with
      | Skip -> pp, Skip
      | Is_closed_by (Monadic, co) -> co.closure, Close_over (Monadic, co)
      | Is_closed_by (Comonadic, co) -> co.closure, Close_over (Comonadic, co)
      | Captured_by_partial_application ->
        (Location.none, Expression), Adj_captured_by_partial_application
      | Crossing -> pp, Crossing
      | Unknown -> (Location.none, Unknown), Unknown
      | Allocation_r loc -> pp, Allocation_l loc
      | Contains_r (Comonadic, { containing; contained }) ->
        contained, Is_contained_by (Comonadic, { containing; container = pp })
      | Contains_l (Monadic, { containing; contained }) ->
        contained, Is_contained_by (Monadic, { containing; container = pp })
      | Is_contained_by (Comonadic, { containing; container }) ->
        container, Contains_l (Comonadic, { containing; contained = pp })
      | Is_contained_by (Monadic, { containing; container }) ->
        container, Contains_r (Monadic, { containing; contained = pp })

    let right_adjoint : type r.
        Hint.pinpoint ->
        (allowed * r) t ->
        Hint.pinpoint * (disallowed * allowed) t =
     fun pp t ->
      match t with
      | Skip -> pp, Skip
      | Close_over (Monadic, co) -> co.closed, Is_closed_by (Monadic, co)
      | Close_over (Comonadic, co) -> co.closed, Is_closed_by (Comonadic, co)
      | Adj_captured_by_partial_application ->
        (Location.none, Expression), Captured_by_partial_application
      | Crossing -> pp, Crossing
      | Unknown -> (Location.none, Unknown), Unknown
      | Allocation_l loc -> pp, Allocation_r loc
      | Contains_l (Comonadic, { containing; contained }) ->
        contained, Is_contained_by (Comonadic, { containing; container = pp })
      | Contains_r (Monadic, { containing; contained }) ->
        contained, Is_contained_by (Monadic, { containing; container = pp })
      | Is_contained_by (Comonadic, { containing; container }) ->
        container, Contains_r (Comonadic, { containing; contained = pp })
      | Is_contained_by (Monadic, { containing; container }) ->
        container, Contains_l (Monadic, { containing; contained = pp })

    include Magic_allow_disallow (struct
      type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r

      let allow_left : type l r. (allowed * r) t -> (l * r) t =
       fun (type l r) (h : (allowed * r) t) : (l * r) t ->
        match h with
        | Skip -> Skip
        | Unknown -> Unknown
        | Close_over (Monadic, x) -> Close_over (Monadic, x)
        | Close_over (Comonadic, x) -> Close_over (Comonadic, x)
        | Adj_captured_by_partial_application ->
          Adj_captured_by_partial_application
        | Crossing -> Crossing
        | Allocation_l loc -> Allocation_l loc
        | Contains_l (Comonadic, x) -> Contains_l (Comonadic, x)
        | Contains_r (Monadic, x) -> Contains_r (Monadic, x)
        | Is_contained_by (Comonadic, x) -> Is_contained_by (Comonadic, x)
        | Is_contained_by (Monadic, x) -> Is_contained_by (Monadic, x)

      let allow_right : type l r. (l * allowed) t -> (l * r) t =
       fun (type l r) (h : (l * allowed) t) : (l * r) t ->
        match h with
        | Skip -> Skip
        | Unknown -> Unknown
        | Is_closed_by (Monadic, x) -> Is_closed_by (Monadic, x)
        | Is_closed_by (Comonadic, x) -> Is_closed_by (Comonadic, x)
        | Captured_by_partial_application -> Captured_by_partial_application
        | Crossing -> Crossing
        | Allocation_r loc -> Allocation_r loc
        | Contains_r (Comonadic, x) -> Contains_r (Comonadic, x)
        | Contains_l (Monadic, x) -> Contains_l (Monadic, x)
        | Is_contained_by (Comonadic, x) -> Is_contained_by (Comonadic, x)
        | Is_contained_by (Monadic, x) -> Is_contained_by (Monadic, x)

      let disallow_left : type l r. (l * r) t -> (disallowed * r) t =
       fun (type l r) (h : (l * r) t) : (disallowed * r) t ->
        match h with
        | Skip -> Skip
        | Unknown -> Unknown
        | Close_over (Monadic, x) -> Close_over (Monadic, x)
        | Close_over (Comonadic, x) -> Close_over (Comonadic, x)
        | Is_closed_by (Monadic, x) -> Is_closed_by (Monadic, x)
        | Is_closed_by (Comonadic, x) -> Is_closed_by (Comonadic, x)
        | Captured_by_partial_application -> Captured_by_partial_application
        | Adj_captured_by_partial_application ->
          Adj_captured_by_partial_application
        | Crossing -> Crossing
        | Allocation_r loc -> Allocation_r loc
        | Allocation_l loc -> Allocation_l loc
        | Contains_r (Comonadic, x) -> Contains_r (Comonadic, x)
        | Contains_l (Monadic, x) -> Contains_l (Monadic, x)
        | Is_contained_by (Comonadic, x) -> Is_contained_by (Comonadic, x)
        | Is_contained_by (Monadic, x) -> Is_contained_by (Monadic, x)
        | Contains_r (Monadic, x) -> Contains_r (Monadic, x)
        | Contains_l (Comonadic, x) -> Contains_l (Comonadic, x)

      let disallow_right : type l r. (l * r) t -> (l * disallowed) t =
       fun (type l r) (h : (l * r) t) : (l * disallowed) t ->
        match h with
        | Skip -> Skip
        | Unknown -> Unknown
        | Close_over (Monadic, x) -> Close_over (Monadic, x)
        | Close_over (Comonadic, x) -> Close_over (Comonadic, x)
        | Is_closed_by (Monadic, x) -> Is_closed_by (Monadic, x)
        | Is_closed_by (Comonadic, x) -> Is_closed_by (Comonadic, x)
        | Captured_by_partial_application -> Captured_by_partial_application
        | Adj_captured_by_partial_application ->
          Adj_captured_by_partial_application
        | Crossing -> Crossing
        | Allocation_l loc -> Allocation_l loc
        | Allocation_r loc -> Allocation_r loc
        | Contains_l (Comonadic, x) -> Contains_l (Comonadic, x)
        | Contains_r (Monadic, x) -> Contains_r (Monadic, x)
        | Is_contained_by (Comonadic, x) -> Is_contained_by (Comonadic, x)
        | Is_contained_by (Monadic, x) -> Is_contained_by (Monadic, x)
        | Contains_l (Monadic, x) -> Contains_l (Monadic, x)
        | Contains_r (Comonadic, x) -> Contains_r (Comonadic, x)
    end)
  end

  module Const = struct
    type 'd t = 'd Hint.const

    let unknown : _ t = Unknown

    let max : _ t = Unknown

    let min : _ t = Unknown

    include Magic_allow_disallow (struct
      type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r

      let allow_left : type l r. (allowed * r) t -> (l * r) t =
       fun (type l r) (h : (allowed * r) t) : (l * r) t ->
        match h with
        | Unknown -> Unknown
        | Legacy x -> Legacy x
        | Stack_expression -> Stack_expression
        | Mutable_read m -> Mutable_read m
        | Mutable_write m -> Mutable_write m
        | Lazy_forced -> Lazy_forced
        | Borrowed (loc, Comonadic) -> Borrowed (loc, Comonadic)
        | Borrowed (loc, Monadic) -> Borrowed (loc, Monadic)
        | Quoted_computation -> Quoted_computation
        | Spliced Monadic -> Spliced Monadic
        | Spliced Comonadic -> Spliced Comonadic
        | Lpoly_inst -> Lpoly_inst

      let allow_right : type l r. (l * allowed) t -> (l * r) t =
       fun (type l r) (h : (l * allowed) t) : (l * r) t ->
        match h with
        | Unknown -> Unknown
        | Legacy x -> Legacy x
        | Toplevel_expression -> Toplevel_expression
        | Lazy_allocated_on_heap -> Lazy_allocated_on_heap
        | Tailcall_function -> Tailcall_function
        | Tailcall_argument -> Tailcall_argument
        | Function_return -> Function_return
        | Module_allocated_on_heap -> Module_allocated_on_heap
        | Is_used_in pp -> Is_used_in pp
        | Always_dynamic x -> Always_dynamic x
        | Branching -> Branching
        | Borrowed (loc, Monadic) -> Borrowed (loc, Monadic)
        | Borrowed (loc, Comonadic) -> Borrowed (loc, Comonadic)
        | Escape_region x -> Escape_region x
        | Spliced Monadic -> Spliced Monadic
        | Spliced Comonadic -> Spliced Comonadic

      let disallow_left : type l r. (l * r) t -> (disallowed * r) t =
       fun (type l r) (h : (l * r) t) : (disallowed * r) t ->
        match h with
        | Unknown -> Unknown
        | Lazy_allocated_on_heap -> Lazy_allocated_on_heap
        | Legacy x -> Legacy x
        | Toplevel_expression -> Toplevel_expression
        | Tailcall_function -> Tailcall_function
        | Tailcall_argument -> Tailcall_argument
        | Mutable_read m -> Mutable_read m
        | Mutable_write m -> Mutable_write m
        | Lazy_forced -> Lazy_forced
        | Function_return -> Function_return
        | Stack_expression -> Stack_expression
        | Module_allocated_on_heap -> Module_allocated_on_heap
        | Is_used_in pp -> Is_used_in pp
        | Always_dynamic x -> Always_dynamic x
        | Branching -> Branching
        | Borrowed (loc, Monadic) -> Borrowed (loc, Monadic)
        | Borrowed (loc, Comonadic) -> Borrowed (loc, Comonadic)
        | Escape_region x -> Escape_region x
        | Quoted_computation -> Quoted_computation
        | Lpoly_inst -> Lpoly_inst
        | Spliced Monadic -> Spliced Monadic
        | Spliced Comonadic -> Spliced Comonadic

      let disallow_right : type l r. (l * r) t -> (l * disallowed) t =
       fun (type l r) (h : (l * r) t) : (l * disallowed) t ->
        match h with
        | Unknown -> Unknown
        | Lazy_allocated_on_heap -> Lazy_allocated_on_heap
        | Legacy x -> Legacy x
        | Toplevel_expression -> Toplevel_expression
        | Tailcall_function -> Tailcall_function
        | Tailcall_argument -> Tailcall_argument
        | Mutable_read m -> Mutable_read m
        | Mutable_write m -> Mutable_write m
        | Lazy_forced -> Lazy_forced
        | Function_return -> Function_return
        | Stack_expression -> Stack_expression
        | Module_allocated_on_heap -> Module_allocated_on_heap
        | Is_used_in pp -> Is_used_in pp
        | Always_dynamic x -> Always_dynamic x
        | Branching -> Branching
        | Borrowed (loc, Monadic) -> Borrowed (loc, Monadic)
        | Borrowed (loc, Comonadic) -> Borrowed (loc, Comonadic)
        | Escape_region x -> Escape_region x
        | Lpoly_inst -> Lpoly_inst
        | Quoted_computation -> Quoted_computation
        | Spliced Monadic -> Spliced Monadic
        | Spliced Comonadic -> Spliced Comonadic
    end)
  end
end

type nonrec allowed = allowed

type nonrec disallowed = disallowed

type nonrec equate_step = equate_step

module type Heyting = sig
  (** Extend the [Lattice] interface with operations of Heyting algebras *)

  include Lattice

  (** A total structural order used for map keys. This is not lattice order:
      [compare_total a b = 0] must agree with semantic equality of [a] and [b].
  *)
  val compare_total : t -> t -> int

  (** [imply c] is the right adjoint of [meet c]; That is, for any [a] and [b],
      [meet c a <= b] iff [a <= imply c b] *)
  val imply : t -> t -> t
end

module type CoHeyting = sig
  (** Extend the [Lattice] interface with operations of co-Heyting algebras *)

  include Lattice

  (** A total structural order used for map keys. This is not lattice order:
      [compare_total a b = 0] must agree with semantic equality of [a] and [b].
  *)
  val compare_total : t -> t -> int

  (** [subtract _ c] is the left adjoint of [join c]. That is, for any [a] and
      [b], [subtract a c <= b] iff [a <= join c b] *)
  val subtract : t -> t -> t
end

(* Even though our lattices are all bi-heyting algebras, that knowledge is
   internal to this module. Externally they are seen as normal lattices. *)
module Lattices = struct
  module Total (L : Total) = struct
    let min = L.min

    let max = L.max

    let le a b = L.ord a <= L.ord b

    let equal a b = L.ord a = L.ord b

    let compare_total a b = Int.compare (L.ord a) (L.ord b)

    let join a b = if L.ord a > L.ord b then a else b

    let meet a b = if L.ord a < L.ord b then a else b

    (* A total lattice has a co-heyting structure.
       Prove the [subtract] below is the left adjoint of [join].
        - If [subtract a c <= b], by the definition of [subtract] below,
          that could mean one of two things:
          - Took the branch [a <= c], and [min <= b]. In this case, we have [a <= c <= join c b].
          - Took the other branch, and [a <= b]. In this case, we have [a <= b <= join c b].

        - In the other direction: Given [a <= join c b], compare [c] and [b]:
          - if [c <= b], then [a <= join c b = b], and:
            - either [a <= c], then [subtract a c = min <= b]
            - or the other branch, then [subtract a c = a <= b]
          - if [b <= c], then [a <= join c b = c], then [subtract a c = min <= b]
    *)
    let subtract a c = if le a c then L.min else a

    (* A total lattice has a heyting structure. The proof for [imply] is dual
       and omitted. *)
    let imply c b = if le c b then L.max else b
  end
  [@@inline]

  module type Diamond = sig
    (** A lattice is a partial order, if for any [a] [b], either:
        - [a <= b] or [b <= a]
        - [a] and [b] are incomparable.

        This interface and the [Diamond] functor below are specialized to
        partial lattices of the form
        {v
            Max
            / \
          Fst Snd
            \ /
            Min
        v}
        where [Fst] and [Snd] are incomparable.

        The [Diamond] functor relies on the representation of immediate variant
        types to efficiently implement bitwise operations over such lattices. *)

    (** This must be an enumeration with four constructors, in the order of
        [min], [fst], [snd], and [max]. Anything else will fail in the [Diamond]
        functor. *)
    type t [@@immediate]

    val min : t

    val fst : t

    val snd : t

    val max : t
  end

  module Diamond (L : Diamond) = struct
    open struct
      external l_to_int : L.t -> int = "%identity"

      external l_of_int : int -> L.t = "%identity"

      let mask = 0b11

      let () =
        assert (l_to_int L.min = 0b00);
        assert (l_to_int L.fst = 0b01);
        assert (l_to_int L.snd = 0b10);
        assert (l_to_int L.max = 0b11)
    end

    let min = L.min

    let max = L.max

    let equal a b = a = b

    let compare_total a b = Int.compare (l_to_int a) (l_to_int b)

    let join a b = l_of_int (l_to_int a lor l_to_int b)

    let meet a b = l_of_int (l_to_int a land l_to_int b)

    let le a b = meet a b = a

    (* We can treat [fst] and [snd] as independent axes.
       0b0 land (lnot 0b0) = 0b0 (min = min => min)
       0b0 land (lnot 0b1) = 0b0 (min < max => min)
       0b1 land (lnot 0b0) = 0b1 (max > min => max)
       0b1 land (lnot 0b1) = 0b0 (max = max => min) *)
    let subtract a c = l_of_int (l_to_int a land lnot (l_to_int c))

    (* We can treat [fst] and [snd] as independent axes.
       (lnot 0b0) lor 0b0 = 0b1 (min = min => max)
       (lnot 0b0) lor 0b1 = 0b1 (min < max => max)
       (lnot 0b1) lor 0b0 = 0b0 (max > min => min)
       (lnot 0b1) lor 0b1 = 0b1 (max = max => max)

       [lnot c lor b] sets the top 61 bits to 1, so we must mask them out. *)
    let imply c b = l_of_int (lnot (l_to_int c) lor l_to_int b land mask)
  end
  [@@inline]

  (* Make the type of [Locality] and [Regionality] below distinguishable,
     so that we can be sure [Comonadic_with] is applied correctly. *)
  module type Areality = sig
    include Const

    include Heyting with type t := t

    val _is_areality : unit
  end

  module Locality = struct
    type t =
      | Global
      | Local

    include Total (struct
      type nonrec t = t

      let min = Global

      let max = Local

      let ord = function Global -> 0 | Local -> 1
    end)

    let legacy = Global

    let print ppf = function
      | Global -> Fmt.fprintf ppf "global"
      | Local -> Fmt.fprintf ppf "local"

    let _is_areality = ()
  end

  module Regionality = struct
    type t =
      | Global
      | Regional
      | Local

    include Total (struct
      type nonrec t = t

      let min = Global

      let max = Local

      let ord = function Global -> 0 | Regional -> 1 | Local -> 2
    end)

    let legacy = Global

    let print ppf = function
      | Global -> Fmt.fprintf ppf "global"
      | Regional -> Fmt.fprintf ppf "regional"
      | Local -> Fmt.fprintf ppf "local"

    let _is_areality = ()
  end

  module Uniqueness = struct
    type t =
      | Unique
      | Aliased

    include Total (struct
      type nonrec t = t

      let min = Unique

      let max = Aliased

      let ord = function Unique -> 0 | Aliased -> 1
    end)

    let legacy = Aliased

    let print ppf = function
      | Aliased -> Fmt.fprintf ppf "aliased"
      | Unique -> Fmt.fprintf ppf "unique"
  end

  module Linearity = struct
    type t =
      | Many
      | Once

    include Total (struct
      type nonrec t = t

      let min = Many

      let max = Once

      let ord = function Many -> 0 | Once -> 1
    end)

    let legacy = Many

    let print ppf = function
      | Once -> Fmt.fprintf ppf "once"
      | Many -> Fmt.fprintf ppf "many"
  end

  module Portability = struct
    (* Changes to this type must consider the implementation of [Diamond]. *)
    type t =
      | Portable (* 0b00 *)
      | Shareable (* 0b01 *)
      | Corruptible (* 0b10 *)
      | Nonportable (* 0b11 *)

    include Diamond (struct
      type nonrec t = t

      let min = Portable

      let fst = Shareable

      let snd = Corruptible

      let max = Nonportable
    end)

    let legacy = Nonportable

    let print ppf = function
      | Portable -> Fmt.fprintf ppf "portable"
      | Shareable -> Fmt.fprintf ppf "shareable"
      | Corruptible -> Fmt.fprintf ppf "corruptible"
      | Nonportable -> Fmt.fprintf ppf "nonportable"
  end

  module Contention = struct
    (* Changes to this type must consider the implementation of [Diamond]. *)
    type t =
      | Uncontended (* 0b00 *)
      | Corrupted (* 0b01 *)
      | Shared (* 0b10 *)
      | Contended (* 0b11 *)

    include Diamond (struct
      type nonrec t = t

      let min = Uncontended

      let fst = Corrupted

      let snd = Shared

      let max = Contended
    end)

    let legacy = Uncontended

    let print ppf = function
      | Contended -> Fmt.fprintf ppf "contended"
      | Corrupted -> Fmt.fprintf ppf "corrupted"
      | Shared -> Fmt.fprintf ppf "shared"
      | Uncontended -> Fmt.fprintf ppf "uncontended"
  end

  module Forkable = struct
    type t =
      | Forkable
      | Unforkable

    include Total (struct
      type nonrec t = t

      let min = Forkable

      let max = Unforkable

      let ord = function Forkable -> 0 | Unforkable -> 1
    end)

    let legacy = Forkable

    let print ppf = function
      | Unforkable -> Fmt.fprintf ppf "unforkable"
      | Forkable -> Fmt.fprintf ppf "forkable"
  end

  module Yielding = struct
    type t =
      | Unyielding
      | Yielding

    include Total (struct
      type nonrec t = t

      let min = Unyielding

      let max = Yielding

      let ord = function Unyielding -> 0 | Yielding -> 1
    end)

    let legacy = Unyielding

    let print ppf = function
      | Yielding -> Fmt.fprintf ppf "yielding"
      | Unyielding -> Fmt.fprintf ppf "unyielding"
  end

  module Statefulness = struct
    (* Changes to this type must consider the implementation of [Diamond]. *)
    type t =
      | Stateless (* 0b00 *)
      | Writing (* 0b01 *)
      | Reading (* 0b10 *)
      | Stateful (* 0b11 *)

    include Diamond (struct
      type nonrec t = t

      let min = Stateless

      let fst = Writing

      let snd = Reading

      let max = Stateful
    end)

    let legacy = Stateful

    let print ppf = function
      | Stateless -> Fmt.fprintf ppf "stateless"
      | Writing -> Fmt.fprintf ppf "writing"
      | Reading -> Fmt.fprintf ppf "reading"
      | Stateful -> Fmt.fprintf ppf "stateful"
  end

  module Visibility = struct
    (* Changes to this type must consider the implementation of [Diamond]. *)
    type t =
      | Read_write (* 0b00 *)
      | Read (* 0b01 *)
      | Write (* 0b10 *)
      | Immutable (* 0b11 *)

    include Diamond (struct
      type nonrec t = t

      let min = Read_write

      let fst = Read

      let snd = Write

      let max = Immutable
    end)

    let legacy = Read_write

    let print ppf = function
      | Immutable -> Fmt.fprintf ppf "immutable"
      | Read -> Fmt.fprintf ppf "read"
      | Write -> Fmt.fprintf ppf "write"
      | Read_write -> Fmt.fprintf ppf "read_write"
  end

  module Staticity = struct
    type t =
      | Static
      | Dynamic

    include Total (struct
      type nonrec t = t

      let min = Static

      let max = Dynamic

      let ord = function Static -> 0 | Dynamic -> 1
    end)

    let legacy = Dynamic

    let print ppf = function
      | Dynamic -> Fmt.fprintf ppf "dynamic"
      | Static -> Fmt.fprintf ppf "static"
  end

  type monadic =
    { uniqueness : Uniqueness.t;
      contention : Contention.t;
      visibility : Visibility.t;
      staticity : Staticity.t
    }

  module Monadic = struct
    type t = monadic

    let min =
      let uniqueness = Uniqueness.min in
      let contention = Contention.min in
      let visibility = Visibility.min in
      let staticity = Staticity.min in
      { uniqueness; contention; visibility; staticity }

    let max =
      let uniqueness = Uniqueness.max in
      let contention = Contention.max in
      let visibility = Visibility.max in
      let staticity = Staticity.max in
      { uniqueness; contention; visibility; staticity }

    let legacy =
      let uniqueness = Uniqueness.legacy in
      let contention = Contention.legacy in
      let visibility = Visibility.legacy in
      let staticity = Staticity.legacy in
      { uniqueness; contention; visibility; staticity }

    let le m1 m2 =
      let { uniqueness = uniqueness1;
            contention = contention1;
            visibility = visibility1;
            staticity = staticity1
          } =
        m1
      in
      let { uniqueness = uniqueness2;
            contention = contention2;
            visibility = visibility2;
            staticity = staticity2
          } =
        m2
      in
      Uniqueness.le uniqueness1 uniqueness2
      && Contention.le contention1 contention2
      && Visibility.le visibility1 visibility2
      && Staticity.le staticity1 staticity2

    let equal m1 m2 =
      let { uniqueness = uniqueness1;
            contention = contention1;
            visibility = visibility1;
            staticity = staticity1
          } =
        m1
      in
      let { uniqueness = uniqueness2;
            contention = contention2;
            visibility = visibility2;
            staticity = staticity2
          } =
        m2
      in
      Uniqueness.equal uniqueness1 uniqueness2
      && Contention.equal contention1 contention2
      && Visibility.equal visibility1 visibility2
      && Staticity.equal staticity1 staticity2

    let compare_total m1 m2 =
      let c = Uniqueness.compare_total m1.uniqueness m2.uniqueness in
      if c <> 0
      then c
      else
        let c = Contention.compare_total m1.contention m2.contention in
        if c <> 0
        then c
        else
          let c = Visibility.compare_total m1.visibility m2.visibility in
          if c <> 0
          then c
          else Staticity.compare_total m1.staticity m2.staticity

    let join m1 m2 =
      let uniqueness = Uniqueness.join m1.uniqueness m2.uniqueness in
      let contention = Contention.join m1.contention m2.contention in
      let visibility = Visibility.join m1.visibility m2.visibility in
      let staticity = Staticity.join m1.staticity m2.staticity in
      { uniqueness; contention; visibility; staticity }

    let meet m1 m2 =
      let uniqueness = Uniqueness.meet m1.uniqueness m2.uniqueness in
      let contention = Contention.meet m1.contention m2.contention in
      let visibility = Visibility.meet m1.visibility m2.visibility in
      let staticity = Staticity.meet m1.staticity m2.staticity in
      { uniqueness; contention; visibility; staticity }

    let subtract m1 m2 =
      let uniqueness = Uniqueness.subtract m1.uniqueness m2.uniqueness in
      let contention = Contention.subtract m1.contention m2.contention in
      let visibility = Visibility.subtract m1.visibility m2.visibility in
      let staticity = Staticity.subtract m1.staticity m2.staticity in
      { uniqueness; contention; visibility; staticity }

    let print ppf m =
      Fmt.fprintf ppf "%a,%a,%a,%a" Uniqueness.print m.uniqueness
        Contention.print m.contention Visibility.print m.visibility
        Staticity.print m.staticity
  end

  type 'areality comonadic_with =
    { areality : 'areality;
      linearity : Linearity.t;
      portability : Portability.t;
      forkable : Forkable.t;
      yielding : Yielding.t;
      statefulness : Statefulness.t
    }

  module Comonadic_with (Areality : Areality) = struct
    type t = Areality.t comonadic_with

    let min =
      let areality = Areality.min in
      let linearity = Linearity.min in
      let portability = Portability.min in
      let forkable = Forkable.min in
      let yielding = Yielding.min in
      let statefulness = Statefulness.min in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let max =
      let areality = Areality.max in
      let linearity = Linearity.max in
      let portability = Portability.max in
      let forkable = Forkable.max in
      let yielding = Yielding.max in
      let statefulness = Statefulness.max in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let legacy =
      let areality = Areality.legacy in
      let linearity = Linearity.legacy in
      let portability = Portability.legacy in
      let forkable = Forkable.legacy in
      let yielding = Yielding.legacy in
      let statefulness = Statefulness.legacy in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let le m1 m2 =
      let { areality = areality1;
            linearity = linearity1;
            portability = portability1;
            forkable = forkable1;
            yielding = yielding1;
            statefulness = statefulness1
          } =
        m1
      in
      let { areality = areality2;
            linearity = linearity2;
            portability = portability2;
            forkable = forkable2;
            yielding = yielding2;
            statefulness = statefulness2
          } =
        m2
      in
      Areality.le areality1 areality2
      && Linearity.le linearity1 linearity2
      && Portability.le portability1 portability2
      && Forkable.le forkable1 forkable2
      && Yielding.le yielding1 yielding2
      && Statefulness.le statefulness1 statefulness2

    let equal m1 m2 =
      let { areality = areality1;
            linearity = linearity1;
            portability = portability1;
            forkable = forkable1;
            yielding = yielding1;
            statefulness = statefulness1
          } =
        m1
      in
      let { areality = areality2;
            linearity = linearity2;
            portability = portability2;
            forkable = forkable2;
            yielding = yielding2;
            statefulness = statefulness2
          } =
        m2
      in
      Areality.equal areality1 areality2
      && Linearity.equal linearity1 linearity2
      && Portability.equal portability1 portability2
      && Forkable.equal forkable1 forkable2
      && Yielding.equal yielding1 yielding2
      && Statefulness.equal statefulness1 statefulness2

    let compare_total m1 m2 =
      let c = Areality.compare_total m1.areality m2.areality in
      if c <> 0
      then c
      else
        let c = Linearity.compare_total m1.linearity m2.linearity in
        if c <> 0
        then c
        else
          let c = Portability.compare_total m1.portability m2.portability in
          if c <> 0
          then c
          else
            let c = Forkable.compare_total m1.forkable m2.forkable in
            if c <> 0
            then c
            else
              let c = Yielding.compare_total m1.yielding m2.yielding in
              if c <> 0
              then c
              else Statefulness.compare_total m1.statefulness m2.statefulness

    let join m1 m2 =
      let areality = Areality.join m1.areality m2.areality in
      let linearity = Linearity.join m1.linearity m2.linearity in
      let portability = Portability.join m1.portability m2.portability in
      let forkable = Forkable.join m1.forkable m2.forkable in
      let yielding = Yielding.join m1.yielding m2.yielding in
      let statefulness = Statefulness.join m1.statefulness m2.statefulness in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let meet m1 m2 =
      let areality = Areality.meet m1.areality m2.areality in
      let linearity = Linearity.meet m1.linearity m2.linearity in
      let portability = Portability.meet m1.portability m2.portability in
      let forkable = Forkable.meet m1.forkable m2.forkable in
      let yielding = Yielding.meet m1.yielding m2.yielding in
      let statefulness = Statefulness.meet m1.statefulness m2.statefulness in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let imply m1 m2 =
      let areality = Areality.imply m1.areality m2.areality in
      let linearity = Linearity.imply m1.linearity m2.linearity in
      let portability = Portability.imply m1.portability m2.portability in
      let forkable = Forkable.imply m1.forkable m2.forkable in
      let yielding = Yielding.imply m1.yielding m2.yielding in
      let statefulness = Statefulness.imply m1.statefulness m2.statefulness in
      { areality; linearity; portability; forkable; yielding; statefulness }

    let print ppf m =
      Fmt.fprintf ppf "%a,%a,%a,%a,%a,%a" Areality.print m.areality
        Linearity.print m.linearity Portability.print m.portability
        Forkable.print m.forkable Yielding.print m.yielding Statefulness.print
        m.statefulness
  end
  [@@inline]

  module Opposite (L : CoHeyting) : Heyting with type t = L.t = struct
    type t = L.t

    let min = L.max

    let max = L.min

    let[@inline] le a b = L.le b a

    let equal = L.equal

    let compare_total = L.compare_total

    let join = L.meet

    let meet = L.join

    let print = L.print

    let imply a b = L.subtract b a
  end
  [@@inline]

  (* Notes on flipping

     Our lattices are split into two opposite fragments: monadic and comonadic.
     Moreover:
     - Morphisms between lattices in the same fragment are always monotone.
     - Morphisms between lattices from opposite fragments are always antitone.

     [Solver_mono] only supports monotone morphisms. Due to this limitation,
     here, we flip all lattices in the monadic fragment, which makes morphisms
     between opposite fragments monotone. We submit this category of lattices
     (original comonadic lattices + flipped monadic lattices) to [Solver_mono].

     The resulted interface given by [Solver_mono] therefore has the monadic
     lattices flipped. We build on top of that and provide an interface to the
     downstream code where monadic lattices are flipped back to its original
     ordering. See [module Monadic_gen] and [module Monadic].
  *)
  module Uniqueness_op = Opposite (Uniqueness)
  module Contention_op = Opposite (Contention)
  module Visibility_op = Opposite (Visibility)
  module Staticity_op = Opposite (Staticity)
  module Monadic_op = Opposite (Monadic)
  module Comonadic_with_locality = Comonadic_with (Locality)
  module Comonadic_with_regionality = Comonadic_with (Regionality)

  type 'a obj =
    | Locality : Locality.t obj
    | Regionality : Regionality.t obj
    | Uniqueness_op : Uniqueness_op.t obj
    | Linearity : Linearity.t obj
    | Portability : Portability.t obj
    | Forkable : Forkable.t obj
    | Yielding : Yielding.t obj
    | Statefulness : Statefulness.t obj
    | Contention_op : Contention_op.t obj
    | Visibility_op : Visibility_op.t obj
    | Staticity_op : Staticity_op.t obj
    | Monadic_op : Monadic_op.t obj
    | Comonadic_with_regionality : Comonadic_with_regionality.t obj
    | Comonadic_with_locality : Comonadic_with_locality.t obj

  let is_opposite : type a. a obj -> bool = function
    | Locality -> false
    | Regionality -> false
    | Uniqueness_op -> true
    | Linearity -> false
    | Portability -> false
    | Forkable -> false
    | Yielding -> false
    | Statefulness -> false
    | Contention_op -> true
    | Visibility_op -> true
    | Staticity_op -> true
    | Monadic_op -> true
    | Comonadic_with_locality -> false
    | Comonadic_with_regionality -> false

  let print_obj : type a. _ -> a obj -> unit =
   fun ppf -> function
    | Locality -> Fmt.fprintf ppf "Locality"
    | Regionality -> Fmt.fprintf ppf "Regionality"
    | Uniqueness_op -> Fmt.fprintf ppf "Uniqueness_op"
    | Linearity -> Fmt.fprintf ppf "Linearity"
    | Portability -> Fmt.fprintf ppf "Portability"
    | Forkable -> Fmt.fprintf ppf "Forkable"
    | Yielding -> Fmt.fprintf ppf "Yielding"
    | Statefulness -> Fmt.fprintf ppf "Statefulness"
    | Contention_op -> Fmt.fprintf ppf "Contention_op"
    | Visibility_op -> Fmt.fprintf ppf "Visibility_op"
    | Staticity_op -> Fmt.fprintf ppf "Staticity_op"
    | Monadic_op -> Fmt.fprintf ppf "Monadic_op"
    | Comonadic_with_locality -> Fmt.fprintf ppf "Comonadic_with_locality"
    | Comonadic_with_regionality -> Fmt.fprintf ppf "Comonadic_with_regionality"

  let min : type a. a obj -> a = function
    | Locality -> Locality.min
    | Regionality -> Regionality.min
    | Uniqueness_op -> Uniqueness_op.min
    | Contention_op -> Contention_op.min
    | Visibility_op -> Visibility_op.min
    | Forkable -> Forkable.min
    | Yielding -> Yielding.min
    | Statefulness -> Statefulness.min
    | Linearity -> Linearity.min
    | Portability -> Portability.min
    | Staticity_op -> Staticity_op.min
    | Monadic_op -> Monadic_op.min
    | Comonadic_with_locality -> Comonadic_with_locality.min
    | Comonadic_with_regionality -> Comonadic_with_regionality.min

  let max : type a. a obj -> a = function
    | Locality -> Locality.max
    | Regionality -> Regionality.max
    | Uniqueness_op -> Uniqueness_op.max
    | Contention_op -> Contention_op.max
    | Visibility_op -> Visibility_op.max
    | Linearity -> Linearity.max
    | Portability -> Portability.max
    | Forkable -> Forkable.max
    | Yielding -> Yielding.max
    | Statefulness -> Statefulness.max
    | Staticity_op -> Staticity_op.max
    | Monadic_op -> Monadic_op.max
    | Comonadic_with_locality -> Comonadic_with_locality.max
    | Comonadic_with_regionality -> Comonadic_with_regionality.max

  let le : type a. a obj -> a -> a -> bool =
   fun obj a b ->
    match obj with
    | Locality -> Locality.le a b
    | Regionality -> Regionality.le a b
    | Uniqueness_op -> Uniqueness_op.le a b
    | Contention_op -> Contention_op.le a b
    | Visibility_op -> Visibility_op.le a b
    | Linearity -> Linearity.le a b
    | Portability -> Portability.le a b
    | Forkable -> Forkable.le a b
    | Yielding -> Yielding.le a b
    | Statefulness -> Statefulness.le a b
    | Staticity_op -> Staticity_op.le a b
    | Monadic_op -> Monadic_op.le a b
    | Comonadic_with_locality -> Comonadic_with_locality.le a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.le a b

  let compare_total : type a. a obj -> a -> a -> int =
   fun obj a b ->
    match obj with
    | Locality -> Locality.compare_total a b
    | Regionality -> Regionality.compare_total a b
    | Uniqueness_op -> Uniqueness_op.compare_total a b
    | Contention_op -> Contention_op.compare_total a b
    | Visibility_op -> Visibility_op.compare_total a b
    | Linearity -> Linearity.compare_total a b
    | Portability -> Portability.compare_total a b
    | Forkable -> Forkable.compare_total a b
    | Yielding -> Yielding.compare_total a b
    | Statefulness -> Statefulness.compare_total a b
    | Staticity_op -> Staticity_op.compare_total a b
    | Monadic_op -> Monadic_op.compare_total a b
    | Comonadic_with_locality -> Comonadic_with_locality.compare_total a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.compare_total a b

  let equal : type a. a obj -> a -> a -> bool =
   fun obj a b ->
    match obj with
    | Locality -> Locality.equal a b
    | Regionality -> Regionality.equal a b
    | Uniqueness_op -> Uniqueness_op.equal a b
    | Contention_op -> Contention_op.equal a b
    | Visibility_op -> Visibility_op.equal a b
    | Linearity -> Linearity.equal a b
    | Portability -> Portability.equal a b
    | Forkable -> Forkable.equal a b
    | Yielding -> Yielding.equal a b
    | Statefulness -> Statefulness.equal a b
    | Staticity_op -> Staticity_op.equal a b
    | Monadic_op -> Monadic_op.equal a b
    | Comonadic_with_locality -> Comonadic_with_locality.equal a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.equal a b

  let join : type a. a obj -> a -> a -> a =
   fun obj a b ->
    match obj with
    | Locality -> Locality.join a b
    | Regionality -> Regionality.join a b
    | Uniqueness_op -> Uniqueness_op.join a b
    | Contention_op -> Contention_op.join a b
    | Visibility_op -> Visibility_op.join a b
    | Linearity -> Linearity.join a b
    | Portability -> Portability.join a b
    | Forkable -> Forkable.join a b
    | Yielding -> Yielding.join a b
    | Statefulness -> Statefulness.join a b
    | Staticity_op -> Staticity_op.join a b
    | Monadic_op -> Monadic_op.join a b
    | Comonadic_with_locality -> Comonadic_with_locality.join a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.join a b

  let meet : type a. a obj -> a -> a -> a =
   fun obj a b ->
    match obj with
    | Locality -> Locality.meet a b
    | Regionality -> Regionality.meet a b
    | Uniqueness_op -> Uniqueness_op.meet a b
    | Contention_op -> Contention_op.meet a b
    | Visibility_op -> Visibility_op.meet a b
    | Linearity -> Linearity.meet a b
    | Portability -> Portability.meet a b
    | Forkable -> Forkable.meet a b
    | Yielding -> Yielding.meet a b
    | Statefulness -> Statefulness.meet a b
    | Staticity_op -> Staticity_op.meet a b
    | Monadic_op -> Monadic_op.meet a b
    | Comonadic_with_locality -> Comonadic_with_locality.meet a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.meet a b

  let imply : type a. a obj -> a -> a -> a =
   fun obj a b ->
    match obj with
    | Locality -> Locality.imply a b
    | Regionality -> Regionality.imply a b
    | Uniqueness_op -> Uniqueness_op.imply a b
    | Contention_op -> Contention_op.imply a b
    | Visibility_op -> Visibility_op.imply a b
    | Linearity -> Linearity.imply a b
    | Portability -> Portability.imply a b
    | Forkable -> Forkable.imply a b
    | Yielding -> Yielding.imply a b
    | Statefulness -> Statefulness.imply a b
    | Staticity_op -> Staticity_op.imply a b
    | Comonadic_with_locality -> Comonadic_with_locality.imply a b
    | Comonadic_with_regionality -> Comonadic_with_regionality.imply a b
    | Monadic_op -> Monadic_op.imply a b

  (* not hotpath, Ok to curry *)
  let print : type a. a obj -> _ -> a -> unit = function
    | Locality -> Locality.print
    | Regionality -> Regionality.print
    | Uniqueness_op -> Uniqueness_op.print
    | Contention_op -> Contention_op.print
    | Visibility_op -> Visibility_op.print
    | Linearity -> Linearity.print
    | Portability -> Portability.print
    | Forkable -> Forkable.print
    | Yielding -> Yielding.print
    | Statefulness -> Statefulness.print
    | Staticity_op -> Staticity_op.print
    | Monadic_op -> Monadic_op.print
    | Comonadic_with_locality -> Comonadic_with_locality.print
    | Comonadic_with_regionality -> Comonadic_with_regionality.print

  let compare_obj : type a b. a obj -> b obj -> int =
   fun a b ->
    match a, b with
    | Locality, Locality -> 0
    | Locality, _ -> -1
    | _, Locality -> 1
    | Regionality, Regionality -> 0
    | Regionality, _ -> -1
    | _, Regionality -> 1
    | Uniqueness_op, Uniqueness_op -> 0
    | Uniqueness_op, _ -> -1
    | _, Uniqueness_op -> 1
    | Linearity, Linearity -> 0
    | Linearity, _ -> -1
    | _, Linearity -> 1
    | Portability, Portability -> 0
    | Portability, _ -> -1
    | _, Portability -> 1
    | Forkable, Forkable -> 0
    | Forkable, _ -> -1
    | _, Forkable -> 1
    | Yielding, Yielding -> 0
    | Yielding, _ -> -1
    | _, Yielding -> 1
    | Statefulness, Statefulness -> 0
    | Statefulness, _ -> -1
    | _, Statefulness -> 1
    | Contention_op, Contention_op -> 0
    | Contention_op, _ -> -1
    | _, Contention_op -> 1
    | Visibility_op, Visibility_op -> 0
    | Visibility_op, _ -> -1
    | _, Visibility_op -> 1
    | Staticity_op, Staticity_op -> 0
    | Staticity_op, _ -> -1
    | _, Staticity_op -> 1
    | Monadic_op, Monadic_op -> 0
    | Monadic_op, _ -> -1
    | _, Monadic_op -> 1
    | Comonadic_with_regionality, Comonadic_with_regionality -> 0
    | Comonadic_with_regionality, _ -> -1
    | _, Comonadic_with_regionality -> 1
    | Comonadic_with_locality, Comonadic_with_locality -> 0

  let equal_obj : type a b. a obj -> b obj -> (a, b) Misc.is_eq =
   fun a b ->
    match a, b with
    | Locality, Locality -> Misc.Is_eq
    | Regionality, Regionality -> Misc.Is_eq
    | Uniqueness_op, Uniqueness_op -> Misc.Is_eq
    | Linearity, Linearity -> Misc.Is_eq
    | Portability, Portability -> Misc.Is_eq
    | Forkable, Forkable -> Misc.Is_eq
    | Yielding, Yielding -> Misc.Is_eq
    | Statefulness, Statefulness -> Misc.Is_eq
    | Contention_op, Contention_op -> Misc.Is_eq
    | Visibility_op, Visibility_op -> Misc.Is_eq
    | Staticity_op, Staticity_op -> Misc.Is_eq
    | Monadic_op, Monadic_op -> Misc.Is_eq
    | Comonadic_with_regionality, Comonadic_with_regionality -> Misc.Is_eq
    | Comonadic_with_locality, Comonadic_with_locality -> Misc.Is_eq
    | ( ( Locality | Regionality | Uniqueness_op | Linearity | Portability
        | Forkable | Yielding | Statefulness | Contention_op | Visibility_op
        | Staticity_op | Monadic_op | Comonadic_with_regionality
        | Comonadic_with_locality ),
        _ ) ->
      Misc.Is_not_eq
end

module Lattices_mono = struct
  include Lattices

  module Axis = struct
    type ('t, 'r) t =
      | Areality : ('a comonadic_with, 'a) t
      | Forkable : ('areality comonadic_with, Forkable.t) t
      | Yielding : ('areality comonadic_with, Yielding.t) t
      | Linearity : ('areality comonadic_with, Linearity.t) t
      | Statefulness : ('areality comonadic_with, Statefulness.t) t
      | Portability : ('areality comonadic_with, Portability.t) t
      | Uniqueness : (Monadic_op.t, Uniqueness_op.t) t
      | Visibility : (Monadic_op.t, Visibility_op.t) t
      | Contention : (Monadic_op.t, Contention_op.t) t
      | Staticity : (Monadic_op.t, Staticity_op.t) t

    let print : type p r. _ -> (p, r) t -> unit =
     fun ppf -> function
      | Areality -> Fmt.fprintf ppf "locality"
      | Linearity -> Fmt.fprintf ppf "linearity"
      | Portability -> Fmt.fprintf ppf "portability"
      | Uniqueness -> Fmt.fprintf ppf "uniqueness"
      | Contention -> Fmt.fprintf ppf "contention"
      | Forkable -> Fmt.fprintf ppf "forkable"
      | Yielding -> Fmt.fprintf ppf "yielding"
      | Statefulness -> Fmt.fprintf ppf "statefulness"
      | Visibility -> Fmt.fprintf ppf "visibility"
      | Staticity -> Fmt.fprintf ppf "staticity"

    let equal : type p r1 r2. (p, r1) t -> (p, r2) t -> (r1, r2) Misc.is_eq =
     fun ax1 ax2 ->
      match ax1, ax2 with
      | Areality, Areality -> Is_eq
      | Linearity, Linearity -> Is_eq
      | Portability, Portability -> Is_eq
      | Uniqueness, Uniqueness -> Is_eq
      | Contention, Contention -> Is_eq
      | Forkable, Forkable -> Is_eq
      | Yielding, Yielding -> Is_eq
      | Statefulness, Statefulness -> Is_eq
      | Visibility, Visibility -> Is_eq
      | Staticity, Staticity -> Is_eq
      | ( ( Areality | Linearity | Uniqueness | Portability | Contention
          | Forkable | Yielding | Statefulness | Visibility | Staticity ),
          _ ) ->
        Is_not_eq

    let ord : type p r. (p, r) t -> int = function
      | Areality -> 0
      | Forkable -> 1
      | Yielding -> 2
      | Linearity -> 3
      | Statefulness -> 4
      | Portability -> 5
      | Uniqueness -> 6
      | Visibility -> 7
      | Contention -> 8
      | Staticity -> 9

    let compare : type p r1 r2. (p, r1) t -> (p, r2) t -> int =
     fun ax1 ax2 -> Int.compare (ord ax1) (ord ax2)

    let proj : type p r. (p, r) t -> p -> r =
     fun ax t ->
      match ax with
      | Areality -> t.areality
      | Linearity -> t.linearity
      | Portability -> t.portability
      | Forkable -> t.forkable
      | Yielding -> t.yielding
      | Statefulness -> t.statefulness
      | Uniqueness -> t.uniqueness
      | Contention -> t.contention
      | Visibility -> t.visibility
      | Staticity -> t.staticity

    let set : type p r. (p, r) t -> r -> p -> p =
     fun ax r t ->
      match ax with
      | Areality -> { t with areality = r }
      | Linearity -> { t with linearity = r }
      | Portability -> { t with portability = r }
      | Forkable -> { t with forkable = r }
      | Yielding -> { t with yielding = r }
      | Statefulness -> { t with statefulness = r }
      | Uniqueness -> { t with uniqueness = r }
      | Contention -> { t with contention = r }
      | Visibility -> { t with visibility = r }
      | Staticity -> { t with staticity = r }
  end

  type ('a, 'b, 'd) morph =
    | Id : ('a, 'a, 'l * 'r) morph  (** identity morphism *)
    | Meet_const : 'a -> ('a, 'a, 'l * 'r) morph
        (** Meet the input with the parameter *)
    | Imply_const : 'a -> ('a, 'a, disallowed * 'r) morph
        (** The right adjoint of [Meet_const] *)
    | Proj : 't obj * ('t, 'r_) Axis.t -> ('t, 'r_, 'l * 'r) morph
        (** Project from a product to an axis *)
    | Max_with : ('t, 'r_) Axis.t -> ('r_, 't, disallowed * 'r) morph
        (** Combine an axis with maxima along other axes *)
    | Min_with : ('t, 'r_) Axis.t -> ('r_, 't, 'l * disallowed) morph
        (** Combine an axis with minima along other axes *)
    | Map_comonadic :
        ('a1, 'a2, 'l * 'r) morph
        -> ('a1 comonadic_with, 'a2 comonadic_with, 'l * 'r) morph
        (** Lift an morphism on areality to a morphism on the comonadic fragment
        *)
    | Monadic_to_comonadic_min :
        (Monadic_op.t, 'a comonadic_with, 'l * disallowed) morph
        (** Dualize the monadic fragment to the comonadic fragment. The areality
            is set to min. *)
    | Comonadic_to_monadic_min :
        'a comonadic_with obj
        -> ('a comonadic_with, Monadic_op.t, 'l * disallowed) morph
        (** Dualize the comonadic fragment to the monadic fragment. The
            staticity_op is set to min. *)
    | Monadic_to_comonadic_max :
        (Monadic_op.t, 'a comonadic_with, disallowed * 'r) morph
        (** Dualize the monadic fragment to the comonadic fragment. The areality
            is set to max. *)
    | Comonadic_to_monadic_max :
        'a comonadic_with obj
        -> ('a comonadic_with, Monadic_op.t, disallowed * 'r) morph
        (** Dualize the comonadic fragment to the monadic fragment. The
            staticity_op is set to max. *)
    (* Following is a chain of adjunction (complete and cannot extend in
       either direction) *)
    | Local_to_regional : (Locality.t, Regionality.t, 'l * disallowed) morph
        (** Maps local to regional, global to global *)
    | Regional_to_local : (Regionality.t, Locality.t, 'l * 'r) morph
        (** Maps regional to local, identity otherwise *)
    | Locality_as_regionality : (Locality.t, Regionality.t, 'l * 'r) morph
        (** Inject locality into regionality *)
    | Regional_to_global : (Regionality.t, Locality.t, 'l * 'r) morph
        (** Maps regional to global, identity otherwise *)
    | Global_to_regional : (Locality.t, Regionality.t, disallowed * 'r) morph
        (** Maps global to regional, local to local *)
    | Compose :
        ('b, 'c, 'l * 'r) morph * ('a, 'b, 'l * 'r) morph
        -> ('a, 'c, 'l * 'r) morph  (** Compoistion of two morphisms *)
    constraint 'd = _ * _
  [@@ocaml.warning "-62"]

  include Magic_allow_disallow (struct
    type ('a, 'b, 'd) sided = ('a, 'b, 'd) morph constraint 'd = 'l * 'r

    let rec allow_left : type a b l r.
        (a, b, allowed * r) morph -> (a, b, l * r) morph = function
      | Id -> Id
      | Proj (src, ax) -> Proj (src, ax)
      | Min_with ax -> Min_with ax
      | Meet_const c -> Meet_const c
      | Compose (f, g) ->
        let f = allow_left f in
        let g = allow_left g in
        Compose (f, g)
      | Monadic_to_comonadic_min -> Monadic_to_comonadic_min
      | Comonadic_to_monadic_min a -> Comonadic_to_monadic_min a
      | Local_to_regional -> Local_to_regional
      | Locality_as_regionality -> Locality_as_regionality
      | Regional_to_local -> Regional_to_local
      | Regional_to_global -> Regional_to_global
      | Map_comonadic f ->
        let f = allow_left f in
        Map_comonadic f

    let rec allow_right : type a b l r.
        (a, b, l * allowed) morph -> (a, b, l * r) morph = function
      | Id -> Id
      | Proj (src, ax) -> Proj (src, ax)
      | Max_with ax -> Max_with ax
      | Meet_const c -> Meet_const c
      | Imply_const c -> Imply_const c
      | Compose (f, g) ->
        let f = allow_right f in
        let g = allow_right g in
        Compose (f, g)
      | Comonadic_to_monadic_max a -> Comonadic_to_monadic_max a
      | Monadic_to_comonadic_max -> Monadic_to_comonadic_max
      | Global_to_regional -> Global_to_regional
      | Locality_as_regionality -> Locality_as_regionality
      | Regional_to_local -> Regional_to_local
      | Regional_to_global -> Regional_to_global
      | Map_comonadic f ->
        let f = allow_right f in
        Map_comonadic f

    let rec disallow_left : type a b l r.
        (a, b, l * r) morph -> (a, b, disallowed * r) morph = function
      | Id -> Id
      | Proj (src, ax) -> Proj (src, ax)
      | Min_with ax -> Min_with ax
      | Max_with ax -> Max_with ax
      | Meet_const c -> Meet_const c
      | Imply_const c -> Imply_const c
      | Compose (f, g) ->
        let f = disallow_left f in
        let g = disallow_left g in
        Compose (f, g)
      | Monadic_to_comonadic_min -> Monadic_to_comonadic_min
      | Comonadic_to_monadic_min a -> Comonadic_to_monadic_min a
      | Monadic_to_comonadic_max -> Monadic_to_comonadic_max
      | Comonadic_to_monadic_max a -> Comonadic_to_monadic_max a
      | Local_to_regional -> Local_to_regional
      | Global_to_regional -> Global_to_regional
      | Locality_as_regionality -> Locality_as_regionality
      | Regional_to_local -> Regional_to_local
      | Regional_to_global -> Regional_to_global
      | Map_comonadic f ->
        let f = disallow_left f in
        Map_comonadic f

    let rec disallow_right : type a b l r.
        (a, b, l * r) morph -> (a, b, l * disallowed) morph = function
      | Id -> Id
      | Proj (src, ax) -> Proj (src, ax)
      | Min_with ax -> Min_with ax
      | Max_with ax -> Max_with ax
      | Meet_const c -> Meet_const c
      | Imply_const c -> Imply_const c
      | Compose (f, g) ->
        let f = disallow_right f in
        let g = disallow_right g in
        Compose (f, g)
      | Monadic_to_comonadic_min -> Monadic_to_comonadic_min
      | Comonadic_to_monadic_min a -> Comonadic_to_monadic_min a
      | Monadic_to_comonadic_max -> Monadic_to_comonadic_max
      | Comonadic_to_monadic_max a -> Comonadic_to_monadic_max a
      | Local_to_regional -> Local_to_regional
      | Global_to_regional -> Global_to_regional
      | Locality_as_regionality -> Locality_as_regionality
      | Regional_to_local -> Regional_to_local
      | Regional_to_global -> Regional_to_global
      | Map_comonadic f ->
        let f = disallow_right f in
        Map_comonadic f
  end)

  let set_areality : type a1 a2. a2 -> a1 comonadic_with -> a2 comonadic_with =
   fun r t -> { t with areality = r }

  let proj_obj : type t r. (t, r) Axis.t -> t obj -> r obj =
   fun ax obj ->
    match ax, obj with
    | Areality, Comonadic_with_locality -> Locality
    | Areality, Comonadic_with_regionality -> Regionality
    | Linearity, Comonadic_with_locality -> Linearity
    | Linearity, Comonadic_with_regionality -> Linearity
    | Portability, Comonadic_with_locality -> Portability
    | Portability, Comonadic_with_regionality -> Portability
    | Forkable, Comonadic_with_locality -> Forkable
    | Forkable, Comonadic_with_regionality -> Forkable
    | Yielding, Comonadic_with_locality -> Yielding
    | Yielding, Comonadic_with_regionality -> Yielding
    | Statefulness, Comonadic_with_locality -> Statefulness
    | Statefulness, Comonadic_with_regionality -> Statefulness
    | Uniqueness, Monadic_op -> Uniqueness_op
    | Contention, Monadic_op -> Contention_op
    | Visibility, Monadic_op -> Visibility_op
    | Staticity, Monadic_op -> Staticity_op

  let comonadic_with_obj : type a. a obj -> a comonadic_with obj =
   fun a0 ->
    match a0 with
    | Locality -> Comonadic_with_locality
    | Regionality -> Comonadic_with_regionality
    | Uniqueness_op | Linearity | Monadic_op | Comonadic_with_regionality
    | Comonadic_with_locality | Contention_op | Visibility_op | Portability
    | Forkable | Yielding | Statefulness | Staticity_op ->
      assert false

  let rec src : type a b l r. b obj -> (a, b, l * r) morph -> a obj =
   fun dst f ->
    match f with
    | Id -> dst
    | Proj (src, _) -> src
    | Max_with ax -> proj_obj ax dst
    | Min_with ax -> proj_obj ax dst
    | Meet_const _ -> dst
    | Imply_const _ -> dst
    | Compose (f, g) ->
      let mid = src dst f in
      src mid g
    | Monadic_to_comonadic_min -> Monadic_op
    | Comonadic_to_monadic_min src -> src
    | Comonadic_to_monadic_max src -> src
    | Monadic_to_comonadic_max -> Monadic_op
    | Local_to_regional -> Locality
    | Locality_as_regionality -> Locality
    | Global_to_regional -> Locality
    | Regional_to_local -> Regionality
    | Regional_to_global -> Regionality
    | Map_comonadic f ->
      let dst0 = proj_obj Areality dst in
      let src0 = src dst0 f in
      comonadic_with_obj src0

  let rec compare_morph : type a1 l1 r1 a2 b l2 r2.
      b obj -> (a1, b, l1 * r1) morph -> (a2, b, l2 * r2) morph -> int =
   fun dst f1 f2 ->
    match f1, f2 with
    | Id, Id -> 0
    | Id, _ -> -1
    | _, Id -> 1
    | Proj (src1, ax1), Proj (src2, ax2) -> (
      let c = compare_obj src1 src2 in
      if c <> 0
      then c
      else
        match equal_obj src1 src2 with
        | Misc.Is_eq -> Axis.compare ax1 ax2
        | Misc.Is_not_eq ->
          Misc.fatal_error
            "Mode.Lattices_mono.compare_morph: inconsistent object equality")
    | Proj _, _ -> -1
    | _, Proj _ -> 1
    | Max_with ax1, Max_with ax2 -> Axis.compare ax1 ax2
    | Max_with _, _ -> -1
    | _, Max_with _ -> 1
    | Min_with ax1, Min_with ax2 -> Axis.compare ax1 ax2
    | Min_with _, _ -> -1
    | _, Min_with _ -> 1
    | Meet_const c1, Meet_const c2 -> compare_total dst c1 c2
    | Meet_const _, _ -> -1
    | _, Meet_const _ -> 1
    | Imply_const c1, Imply_const c2 -> compare_total dst c1 c2
    | Imply_const _, _ -> -1
    | _, Imply_const _ -> 1
    | Monadic_to_comonadic_min, Monadic_to_comonadic_min -> 0
    | Monadic_to_comonadic_min, _ -> -1
    | _, Monadic_to_comonadic_min -> 1
    | Comonadic_to_monadic_min a1, Comonadic_to_monadic_min a2 ->
      compare_obj a1 a2
    | Comonadic_to_monadic_min _, _ -> -1
    | _, Comonadic_to_monadic_min _ -> 1
    | Monadic_to_comonadic_max, Monadic_to_comonadic_max -> 0
    | Monadic_to_comonadic_max, _ -> -1
    | _, Monadic_to_comonadic_max -> 1
    | Comonadic_to_monadic_max a1, Comonadic_to_monadic_max a2 ->
      compare_obj a1 a2
    | Comonadic_to_monadic_max _, _ -> -1
    | _, Comonadic_to_monadic_max _ -> 1
    | Local_to_regional, Local_to_regional -> 0
    | Local_to_regional, _ -> -1
    | _, Local_to_regional -> 1
    | Locality_as_regionality, Locality_as_regionality -> 0
    | Locality_as_regionality, _ -> -1
    | _, Locality_as_regionality -> 1
    | Global_to_regional, Global_to_regional -> 0
    | Global_to_regional, _ -> -1
    | _, Global_to_regional -> 1
    | Regional_to_local, Regional_to_local -> 0
    | Regional_to_local, _ -> -1
    | _, Regional_to_local -> 1
    | Regional_to_global, Regional_to_global -> 0
    | Regional_to_global, _ -> -1
    | _, Regional_to_global -> 1
    | Compose (f1, g1), Compose (f2, g2) -> (
      let c = compare_morph dst f1 f2 in
      if c <> 0
      then c
      else
        match equal_morph dst f1 f2 with
        | Misc.Is_eq -> compare_morph (src dst f1) g1 g2
        | Misc.Is_not_eq ->
          Misc.fatal_error
            "Mode.Lattices_mono.compare_morph: inconsistent equality")
    | Compose _, _ -> -1
    | _, Compose _ -> 1
    | Map_comonadic f, Map_comonadic g ->
      compare_morph (proj_obj Areality dst) f g

  and equal_morph : type a1 l1 r1 a2 b l2 r2.
      b obj ->
      (a1, b, l1 * r1) morph ->
      (a2, b, l2 * r2) morph ->
      (a1, a2) Misc.is_eq =
   fun dst f1 f2 ->
    match f1, f2 with
    | Id, Id -> Misc.Is_eq
    | Proj (src1, ax1), Proj (src2, ax2) -> (
      match equal_obj src1 src2 with
      | Misc.Is_not_eq -> Misc.Is_not_eq
      | Misc.Is_eq -> (
        match Axis.equal ax1 ax2 with
        | Misc.Is_eq -> Misc.Is_eq
        | Misc.Is_not_eq -> Misc.Is_not_eq))
    | Max_with ax1, Max_with ax2 -> Axis.equal ax1 ax2
    | Min_with ax1, Min_with ax2 -> Axis.equal ax1 ax2
    | Meet_const c1, Meet_const c2 ->
      if equal dst c1 c2 then Misc.Is_eq else Misc.Is_not_eq
    | Imply_const c1, Imply_const c2 ->
      if equal dst c1 c2 then Misc.Is_eq else Misc.Is_not_eq
    | Monadic_to_comonadic_min, Monadic_to_comonadic_min -> Misc.Is_eq
    | Comonadic_to_monadic_min a1, Comonadic_to_monadic_min a2 ->
      equal_obj a1 a2
    | Monadic_to_comonadic_max, Monadic_to_comonadic_max -> Misc.Is_eq
    | Comonadic_to_monadic_max a1, Comonadic_to_monadic_max a2 ->
      equal_obj a1 a2
    | Local_to_regional, Local_to_regional -> Misc.Is_eq
    | Locality_as_regionality, Locality_as_regionality -> Misc.Is_eq
    | Global_to_regional, Global_to_regional -> Misc.Is_eq
    | Regional_to_local, Regional_to_local -> Misc.Is_eq
    | Regional_to_global, Regional_to_global -> Misc.Is_eq
    | Compose (f1, g1), Compose (f2, g2) -> (
      match equal_morph dst f1 f2 with
      | Misc.Is_not_eq -> Misc.Is_not_eq
      | Misc.Is_eq -> equal_morph (src dst f1) g1 g2)
    | Map_comonadic f, Map_comonadic g ->
      begin match equal_morph (proj_obj Areality dst) f g with
      | Misc.Is_not_eq -> Misc.Is_not_eq
      | Misc.Is_eq -> Misc.Is_eq
      end
    | ( ( Id | Proj _ | Max_with _ | Min_with _ | Meet_const _ | Imply_const _
        | Monadic_to_comonadic_min | Comonadic_to_monadic_min _
        | Monadic_to_comonadic_max | Comonadic_to_monadic_max _
        | Local_to_regional | Locality_as_regionality | Global_to_regional
        | Regional_to_local | Regional_to_global | Compose _ | Map_comonadic _
          ),
        _ ) ->
      Misc.Is_not_eq

  let rec print_morph : type a b l r.
      b obj -> Fmt.formatter -> (a, b, l * r) morph -> unit =
   fun dst ppf -> function
    | Id -> Fmt.fprintf ppf "id"
    | Meet_const c -> Fmt.fprintf ppf "meet_const(%a)" (print dst) c
    | Imply_const c -> Fmt.fprintf ppf "imply_const(%a)" (print dst) c
    | Proj (_, ax) -> Fmt.fprintf ppf "proj_%a" Axis.print ax
    | Max_with ax -> Fmt.fprintf ppf "max_with_%a" Axis.print ax
    | Min_with ax -> Fmt.fprintf ppf "min_with_%a" Axis.print ax
    | Map_comonadic f ->
      let dst0 = proj_obj Areality dst in
      Fmt.fprintf ppf "map_comonadic(%a)" (print_morph dst0) f
    | Monadic_to_comonadic_min -> Fmt.fprintf ppf "monadic_to_comonadic_min"
    | Comonadic_to_monadic_min _ -> Fmt.fprintf ppf "comonadic_to_monadic_min"
    | Comonadic_to_monadic_max _ -> Fmt.fprintf ppf "comonadic_to_monadic_max"
    | Monadic_to_comonadic_max -> Fmt.fprintf ppf "monadic_to_comonadic_max"
    | Local_to_regional -> Fmt.fprintf ppf "local_to_regional"
    | Regional_to_local -> Fmt.fprintf ppf "regional_to_local"
    | Locality_as_regionality -> Fmt.fprintf ppf "locality_as_regionality"
    | Regional_to_global -> Fmt.fprintf ppf "regional_to_global"
    | Global_to_regional -> Fmt.fprintf ppf "global_to_regional"
    | Compose (f1, f2) ->
      let mid = src dst f1 in
      Fmt.fprintf ppf "%a ∘ %a" (print_morph dst) f1 (print_morph mid) f2

  let id = Id

  let linear_to_unique = function
    | Linearity.Many -> Uniqueness.Aliased
    | Linearity.Once -> Uniqueness.Unique

  let unique_to_linear = function
    | Uniqueness.Unique -> Linearity.Once
    | Uniqueness.Aliased -> Linearity.Many

  let portable_to_contended = function
    | Portability.Portable -> Contention.Contended
    | Portability.Shareable -> Contention.Shared
    | Portability.Corruptible -> Contention.Corrupted
    | Portability.Nonportable -> Contention.Uncontended

  let contended_to_portable = function
    | Contention.Contended -> Portability.Portable
    | Contention.Shared -> Portability.Shareable
    | Contention.Corrupted -> Portability.Corruptible
    | Contention.Uncontended -> Portability.Nonportable

  let local_to_regional = function
    | Locality.Global -> Regionality.Global
    | Locality.Local -> Regionality.Regional

  let regional_to_local = function
    | Regionality.Local -> Locality.Local
    | Regionality.Regional -> Locality.Local
    | Regionality.Global -> Locality.Global

  let locality_as_regionality = function
    | Locality.Local -> Regionality.Local
    | Locality.Global -> Regionality.Global

  let regional_to_global = function
    | Regionality.Local -> Locality.Local
    | Regionality.Regional -> Locality.Global
    | Regionality.Global -> Locality.Global

  let global_to_regional = function
    | Locality.Local -> Regionality.Local
    | Locality.Global -> Regionality.Regional

  let statefulness_to_visibility = function
    | Statefulness.Stateless -> Visibility.Immutable
    | Statefulness.Writing -> Visibility.Write
    | Statefulness.Reading -> Visibility.Read
    | Statefulness.Stateful -> Visibility.Read_write

  let visibility_to_statefulness = function
    | Visibility.Immutable -> Statefulness.Stateless
    | Visibility.Read -> Statefulness.Reading
    | Visibility.Write -> Statefulness.Writing
    | Visibility.Read_write -> Statefulness.Stateful

  let min_with dst ax a = Axis.set ax a (min dst)

  let max_with dst ax a = Axis.set ax a (max dst)

  let monadic_to_comonadic_min : type a.
      a comonadic_with obj -> Monadic_op.t -> a comonadic_with =
   fun obj m ->
    let areality : a =
      match obj with
      | Comonadic_with_locality -> Locality.min
      | Comonadic_with_regionality -> Regionality.min
    in
    let linearity = unique_to_linear m.uniqueness in
    let portability = contended_to_portable m.contention in
    let forkable = Forkable.min in
    let yielding = Yielding.min in
    let statefulness = visibility_to_statefulness m.visibility in
    { areality; linearity; portability; forkable; yielding; statefulness }

  let comonadic_to_monadic_min : type a.
      a comonadic_with obj -> a comonadic_with -> Monadic_op.t =
   fun _ m ->
    let uniqueness = linear_to_unique m.linearity in
    let contention = portable_to_contended m.portability in
    let visibility = statefulness_to_visibility m.statefulness in
    let staticity = Staticity_op.min in
    { uniqueness; contention; visibility; staticity }

  let comonadic_to_monadic_max : type a.
      a comonadic_with obj -> a comonadic_with -> Monadic_op.t =
   fun _ m ->
    let uniqueness = linear_to_unique m.linearity in
    let contention = portable_to_contended m.portability in
    let visibility = statefulness_to_visibility m.statefulness in
    let staticity = Staticity_op.max in
    { uniqueness; contention; visibility; staticity }

  let monadic_to_comonadic_max : type a.
      a comonadic_with obj -> Monadic_op.t -> a comonadic_with =
   fun obj m ->
    let areality : a =
      match obj with
      | Comonadic_with_locality -> Locality.max
      | Comonadic_with_regionality -> Regionality.max
    in
    let linearity = unique_to_linear m.uniqueness in
    let portability = contended_to_portable m.contention in
    let forkable = Forkable.max in
    let yielding = Yielding.max in
    let statefulness = visibility_to_statefulness m.visibility in
    { areality; linearity; portability; forkable; yielding; statefulness }

  let rec apply : type a b l r. b obj -> (a, b, l * r) morph -> a -> b =
   fun dst f a ->
    match f with
    | Compose (f, g) ->
      let mid = src dst f in
      let g' = apply mid g in
      let f' = apply dst f in
      f' (g' a)
    | Id -> a
    | Proj (_, ax) -> Axis.proj ax a
    | Max_with ax -> max_with dst ax a
    | Min_with ax -> min_with dst ax a
    | Meet_const c -> meet dst c a
    | Imply_const c -> imply dst c a
    | Monadic_to_comonadic_min -> monadic_to_comonadic_min dst a
    | Comonadic_to_monadic_min src -> comonadic_to_monadic_min src a
    | Comonadic_to_monadic_max src -> comonadic_to_monadic_max src a
    | Monadic_to_comonadic_max -> monadic_to_comonadic_max dst a
    | Local_to_regional -> local_to_regional a
    | Regional_to_local -> regional_to_local a
    | Locality_as_regionality -> locality_as_regionality a
    | Regional_to_global -> regional_to_global a
    | Global_to_regional -> global_to_regional a
    | Map_comonadic f ->
      let dst0 = proj_obj Areality dst in
      let a0 = Axis.proj Areality a in
      set_areality (apply dst0 f a0) a

  module For_hint = struct
    (** Describes the portion of the input that's responsible for a portion of
        the output of a morphism *)
    type 'a responsible_axis =
      | NoneResponsible : 'a responsible_axis
          (** The input is not responsible for the output; instead, the morphism
              is solely responsible for the output. *)
      | SourceIsSingle : 'a responsible_axis
          (** The input of the morphism is single axis, and is responsible for
              the output. *)
      | Axis : ('a, 'a_x) Axis.t -> 'a responsible_axis
          (** The specified axis of the input object is responsible for the
              output. *)

    (* CR zqian: the following functions are hard to write, and are redundant since all
       the information are already in [apply]. A general and simpler apporach would work
       like this: Say we have [b = f a] on RHS, and we want to figure out which axis of
       [a] is responsible for a specific axis [ax] of [b] being low. We will iterate
       through all axes; for each axis, set that to [max] and get [a'], and calculate [b'
       = f a']. If [b'] is not strictly higher than [b] on [ax], then the current axis of
       [a] is not responsible for the [ax] of [b] being low. The iteration might end with
       no axis of [a] being responsible, in which case the morphism is solely
       respoonsible. *)

    (** Given a morphism either from a single axis to a single axis, or from a
        product object to a single axis, return the portion of the input that's
        responsible for the output. *)
    let rec find_responsible_axis_single : type a b l r.
        (a, b, l * r) morph -> a responsible_axis = function
      | Proj (_a_obj, ax) -> Axis ax
      | Compose (g, f) -> (
        match find_responsible_axis_single g with
        | NoneResponsible -> NoneResponsible
        | SourceIsSingle -> find_responsible_axis_single f
        | Axis c_ax -> find_responsible_axis_prod f c_ax)
      | Id | Meet_const _ | Imply_const _ -> SourceIsSingle
      | Max_with _ | Min_with _ | Map_comonadic _ | Monadic_to_comonadic_min
      | Comonadic_to_monadic_min _ | Monadic_to_comonadic_max
      | Comonadic_to_monadic_max _ ->
        assert false
      | Local_to_regional | Regional_to_local | Locality_as_regionality
      | Regional_to_global | Global_to_regional ->
        SourceIsSingle

    (** Given a morphism either from a single axis to a product, or from a
        product to a product, return the portion of the input that's responsible
        for the specified axis of the output. *)
    and find_responsible_axis_prod : type a b b_ax l r.
        (a, b, l * r) morph -> (b, b_ax) Axis.t -> a responsible_axis =
     fun m ax ->
      let handle_monadic_to_comonadic (type x y)
          (ax : (x comonadic_with, y) Axis.t) =
        (* See [Lattices_mono.monadic_to_comonadic_min] for why these are as they are *)
        match ax with
        | Areality -> NoneResponsible
        | Linearity -> Axis Uniqueness
        | Portability -> Axis Contention
        | Forkable -> NoneResponsible
        | Yielding -> NoneResponsible
        | Statefulness -> Axis Visibility
      in
      let handle_comonadic_to_monadic (type y) (ax : (monadic, y) Axis.t) =
        (* See [Lattices_mono.comonadic_to_monadic_min] for why these are as they are *)
        match ax with
        | Uniqueness -> Axis Linearity
        | Contention -> Axis Portability
        | Visibility -> Axis Statefulness
        | Staticity -> NoneResponsible
      in
      match m, ax with
      | Compose (g, f), ax -> (
        (* Operates similarly to the equivalent branch in [find_responsible_axis_single] *)
        match find_responsible_axis_prod g ax with
        | NoneResponsible -> NoneResponsible
        | SourceIsSingle -> find_responsible_axis_single f
        | Axis c_ax -> find_responsible_axis_prod f c_ax)
      | Id, ax -> Axis ax
      | Meet_const _, ax -> Axis ax
      | Imply_const _, ax -> Axis ax
      | Map_comonadic _, ax -> (
        (* The [Map_comonadic] morphism applies a morphsim to the areality axis and
           the result is put back into the areality axis. See [Lattices_mono.apply] *)
        match ax with
        | Areality -> Axis Areality
        | Forkable -> Axis Forkable
        | Yielding -> Axis Yielding
        | Linearity -> Axis Linearity
        | Statefulness -> Axis Statefulness
        | Portability -> Axis Portability)
      | Max_with m_ax, ax | Min_with m_ax, ax -> (
        match Axis.equal m_ax ax with
        | Is_not_eq -> NoneResponsible
        | Is_eq -> SourceIsSingle)
      | Monadic_to_comonadic_min, ax -> handle_monadic_to_comonadic ax
      | Monadic_to_comonadic_max, ax -> handle_monadic_to_comonadic ax
      | Comonadic_to_monadic_min _, ax -> handle_comonadic_to_monadic ax
      | Comonadic_to_monadic_max _, ax -> handle_comonadic_to_monadic ax
      | Proj _, _
      | Local_to_regional, _
      | Regional_to_local, _
      | Locality_as_regionality, _
      | Regional_to_global, _
      | Global_to_regional, _ ->
        .
  end

  (** Compose m1 after m2. Returns [Some f] if the composition can be
      represented by [f] instead of [Compose m1 m2]. [None] otherwise. *)
  let rec maybe_compose : type a b c l r.
      c obj ->
      (b, c, l * r) morph ->
      (a, b, l * r) morph ->
      (a, c, l * r) morph option =
   fun dst m1 m2 ->
    let is_max c = le dst (max dst) c in
    let is_mid_max c =
      let mid = src dst m1 in
      le mid (max mid) c
    in
    match m1, m2 with
    | Id, m -> Some m
    | m, Id -> Some m
    | Meet_const c1, Meet_const c2 -> Some (Meet_const (meet dst c1 c2))
    | Imply_const c1, Imply_const c2 -> Some (Imply_const (meet dst c1 c2))
    | Imply_const c1, Meet_const c2 when le dst c1 c2 -> Some (Imply_const c1)
    | Meet_const c1, m2 when is_max c1 -> Some m2
    | Imply_const c1, m2 when is_max c1 -> Some m2
    | m2, Meet_const c1 when is_mid_max c1 -> Some m2
    | m2, Imply_const c1 when is_mid_max c1 -> Some m2
    | Compose (f1, f2), g -> (
      let mid = src dst f1 in
      match maybe_compose mid f2 g with
      | Some m -> Some (compose dst f1 m)
      (* the check needed to prevent infinite loop *)
      | None -> None)
    | f, Compose (g1, g2) -> (
      match maybe_compose dst f g1 with
      | Some m -> Some (compose dst m g2)
      | None -> None)
    | Proj (mid, ax), Meet_const c ->
      Some (compose dst (Meet_const (Axis.proj ax c)) (Proj (mid, ax)))
    | Proj (_, ax1), Max_with ax2 -> (
      match Axis.equal ax1 ax2 with Is_not_eq -> None | Is_eq -> Some Id)
    | Proj (_, ax1), Min_with ax2 -> (
      match Axis.equal ax1 ax2 with Is_not_eq -> None | Is_eq -> Some Id)
    | Proj (mid, ax), Map_comonadic f -> (
      let src' = src mid m2 in
      match ax with
      | Areality -> Some (compose dst f (Proj (src', Areality)))
      | Linearity -> Some (Proj (src', Linearity))
      | Portability -> Some (Proj (src', Portability))
      | Forkable -> Some (Proj (src', Forkable))
      | Yielding -> Some (Proj (src', Yielding))
      | Statefulness -> Some (Proj (src', Statefulness)))
    | Proj _, Monadic_to_comonadic_min -> None
    | Proj _, Monadic_to_comonadic_max -> None
    | Proj _, Comonadic_to_monadic_min _ -> None
    | Proj _, Comonadic_to_monadic_max _ -> None
    | Map_comonadic f, Map_comonadic g ->
      let dst0 = proj_obj Areality dst in
      Some (Map_comonadic (compose dst0 f g))
    | Regional_to_local, Local_to_regional -> Some Id
    | Regional_to_local, Global_to_regional ->
      Some (Imply_const Locality.Global)
    | Regional_to_local, Locality_as_regionality -> Some Id
    | Regional_to_local, Meet_const c ->
      Some (compose dst (Meet_const (regional_to_local c)) Regional_to_local)
    | Regional_to_global, Meet_const c ->
      Some (compose dst (Meet_const (regional_to_global c)) Regional_to_global)
    | Local_to_regional, Meet_const c ->
      Some (compose dst (Meet_const (local_to_regional c)) Local_to_regional)
    | Global_to_regional, Meet_const c ->
      Some (compose dst (Meet_const (global_to_regional c)) Global_to_regional)
    | Locality_as_regionality, Meet_const c ->
      Some
        (compose dst
           (Meet_const (locality_as_regionality c))
           Locality_as_regionality)
    | Map_comonadic f, Meet_const c ->
      let dst0 = proj_obj Areality dst in
      let areality = Axis.proj Areality c in
      Some
        (compose dst
           (Meet_const (set_areality (max dst0) c))
           (Map_comonadic (compose dst0 f (Meet_const areality))))
    | Map_comonadic f, Imply_const c ->
      let dst0 = proj_obj Areality dst in
      let areality = Axis.proj Areality c in
      Some
        (compose dst
           (Imply_const (set_areality (max dst0) c))
           (Map_comonadic (compose dst0 f (Imply_const areality))))
    | Regional_to_global, Locality_as_regionality -> Some Id
    | Regional_to_global, Local_to_regional -> Some (Meet_const Locality.Global)
    | Local_to_regional, Regional_to_local -> None
    | Local_to_regional, Regional_to_global -> None
    | Locality_as_regionality, Regional_to_local -> None
    | Locality_as_regionality, Regional_to_global -> None
    | Global_to_regional, Regional_to_local -> None
    | Regional_to_global, Global_to_regional -> Some Id
    | Global_to_regional, Regional_to_global -> None
    | Min_with _, _ -> None
    | Max_with _, _ -> None
    | _, Meet_const _ -> None
    | Meet_const _, _ -> None
    | _, Imply_const _ -> None
    | Imply_const _, _ -> None
    | _, Proj _ -> None
    | Map_comonadic _, _ -> None
    | Monadic_to_comonadic_min, _ -> None
    | Monadic_to_comonadic_max, _ -> None
    | Comonadic_to_monadic_min _, _ -> None
    | Comonadic_to_monadic_max _, _ -> None
    | ( Proj _,
        ( Local_to_regional | Regional_to_local | Locality_as_regionality
        | Regional_to_global | Global_to_regional ) ) ->
      .
    | ( ( Local_to_regional | Regional_to_local | Locality_as_regionality
        | Regional_to_global | Global_to_regional ),
        Min_with _ ) ->
      .
    | ( ( Local_to_regional | Regional_to_local | Locality_as_regionality
        | Regional_to_global | Global_to_regional ),
        Max_with _ ) ->
      .

  and compose : type a b c l r.
      c obj -> (b, c, l * r) morph -> (a, b, l * r) morph -> (a, c, l * r) morph
      =
   fun dst f g ->
    match maybe_compose dst f g with Some m -> m | None -> Compose (f, g)

  let rec left_adjoint : type a b l.
      b obj -> (a, b, l * allowed) morph -> (b, a, allowed * disallowed) morph =
   fun dst f ->
    match f with
    | Id -> Id
    | Proj (_, ax) -> Min_with ax
    | Max_with ax -> Proj (dst, ax)
    | Compose (f, g) ->
      let mid = src dst f in
      let f' = left_adjoint dst f in
      let g' = left_adjoint mid g in
      Compose (g', f')
    | Meet_const _c ->
      (* The downward closure of [Meet_const c]'s image is all [x <= c].
         For those, [x <= meet c y] is equivalent to [x <= y]. *)
      Id
    | Imply_const c -> Meet_const c
    | Comonadic_to_monadic_max _ -> Monadic_to_comonadic_min
    | Monadic_to_comonadic_max -> Comonadic_to_monadic_min dst
    | Global_to_regional -> Regional_to_global
    | Regional_to_global -> Locality_as_regionality
    | Locality_as_regionality -> Regional_to_local
    | Regional_to_local -> Local_to_regional
    | Map_comonadic f ->
      let dst0 = proj_obj Areality dst in
      let f' = left_adjoint dst0 f in
      Map_comonadic f'

  and right_adjoint : type a b r.
      b obj -> (a, b, allowed * r) morph -> (b, a, disallowed * allowed) morph =
   fun dst f ->
    match f with
    | Id -> Id
    | Proj (_, ax) -> Max_with ax
    | Min_with ax -> Proj (dst, ax)
    | Compose (f, g) ->
      let mid = src dst f in
      let f' = right_adjoint dst f in
      let g' = right_adjoint mid g in
      Compose (g', f')
    | Meet_const c -> Imply_const c
    | Comonadic_to_monadic_min _ -> Monadic_to_comonadic_max
    | Monadic_to_comonadic_min -> Comonadic_to_monadic_max dst
    | Local_to_regional -> Regional_to_local
    | Regional_to_local -> Locality_as_regionality
    | Locality_as_regionality -> Regional_to_global
    | Regional_to_global -> Global_to_regional
    | Map_comonadic f ->
      let dst0 = proj_obj Areality dst in
      let f' = right_adjoint dst0 f in
      Map_comonadic f'
end

module C = Lattices_mono
module S = Solver_mono (Hint_for_solver) (C)

let erase_hints () = S.erase_hints ()

type monadic = C.monadic =
  { uniqueness : C.Uniqueness.t;
    contention : C.Contention.t;
    visibility : C.Visibility.t;
    staticity : C.Staticity.t
  }

type 'a comonadic_with = 'a C.comonadic_with =
  { areality : 'a;
    linearity : C.Linearity.t;
    portability : C.Portability.t;
    forkable : C.Forkable.t;
    yielding : C.Yielding.t;
    statefulness : C.Statefulness.t
  }

module Axis = C.Axis

type nonrec 'a simple_error = 'a simple_error

let print_longident =
  ref (fun _ _ -> assert false : Fmt.formatter -> Longident.t -> unit)

module Report = struct
  open Hint

  (** Human-readable mode error hints. Compared to [S.error]:
      - This doesn't contain branch, and thus forms a chain.
      - Each node on the chain talks about a single axis, instead of potentially
        on a product lattice. *)
  type 'd hint =
    | Apply : 'd morph * 'b C.obj * ('b, 'd) ahint -> 'd hint
    | Const : 'd const -> 'd hint
    | Irrelevant : ('l * 'r) hint
        (** The current mode is not responsible for the error (that is, the
            surrounding morphism is solely responsible), and should not be
            printed. *)
    constraint 'd = 'l * 'r
  [@@ocaml.warning "-62"]

  and ('a, 'd) ahint = 'a * 'd hint constraint 'd = 'l * 'r

  (** Human-readible mode error report. *)
  type 'a t =
    { left : loosening * ('a, left_only) ahint;
      right : loosening * ('a, right_only) ahint
    }

  (** Convert Solver error to report. *)
  module Of_solver = struct
    (** Given a branch of two constant bounds on a single axis, choose the the
        one that's responsible for the branch. *)
    let choose_branch_axis : type a l r.
        (l * r) Solver_intf.branch ->
        a C.obj ->
        a ->
        a ->
        other:a ->
        [`First | `Second] =
     fun b a_obj x y ~other ->
      (* CR-someday zqian: in the case where each of [x] and [y] can be
         responsible independently, for not satisfying [~other], we currently
         arbitrarily prioritize `Second. In the future we might want to
         prioritize for better error messages. For example, prioritize the first
         element in a [join]. This requires inspecting the [solver.ml] to ensure
         the ordering in the [join] list is preserved. *)
      match b with
      | Meet ->
        if C.le a_obj other x
        then begin
          assert (not (C.le a_obj other y));
          `Second
        end
        else `First
      | Join ->
        if C.le a_obj x other
        then begin
          assert (not (C.le a_obj y other));
          `Second
        end
        else `First

    type 'd side =
      | Left : left_only side
      | Right : right_only side
      constraint 'd = 'l * 'r
    [@@ocaml.warning "-62"]

    let adjoint : type a b l r.
        a C.obj ->
        (l * r) side ->
        (b, a, l * r) C.morph ->
        (a, b, r * l) C.morph =
     fun obj side morph ->
      match side with
      | Left -> C.right_adjoint obj morph
      | Right -> C.left_adjoint obj morph

    (** Given a solver hint on a product lattice, and an axis in that product
        that we are interested in, returns a human-readible hint.*)
    let rec hint_apply : type a b l r.
        a C.obj ->
        (l * r) side ->
        a ->
        (l * r) morph ->
        (b, a, l * r) C.morph ->
        other:a ->
        (b, l * r) S.ahint ->
        b C.For_hint.responsible_axis ->
        (a, l * r) ahint =
     fun obj side a morph_hint morph ~other ahint res ->
      let src = C.src obj morph in
      match res with
      | NoneResponsible -> a, Irrelevant
      | SourceIsSingle ->
        let morph' = adjoint obj side morph in
        let other = C.apply src morph' other in
        let ahint = hint_axis src side ~other ahint in
        let ma = C.apply obj morph (fst ahint) in
        ma, Apply (morph_hint, src, ahint)
      | Axis ax ->
        let b, hint = ahint in
        let morph' = adjoint obj side morph in
        let other = C.apply src morph' other in
        let x, hint = hint_prod src side ax ~other (b, hint) in
        let b = C.Axis.set ax x b in
        let a = C.apply obj morph b in
        let src = C.proj_obj ax src in
        a, Apply (morph_hint, src, (x, hint))

    and hint_prod : type t a l r.
        t C.obj ->
        (l * r) side ->
        (t, a) Axis.t ->
        other:t ->
        (t, l * r) S.ahint ->
        (a, l * r) ahint =
     fun obj side ax ~other (a, hint) ->
      match hint with
      | Apply (morph_hint, morph, ahint) ->
        let t, hint =
          hint_apply obj side a morph_hint morph ~other ahint
            (C.For_hint.find_responsible_axis_prod morph ax)
        in
        Axis.proj ax t, hint
      | Const c -> Axis.proj ax a, Const c
      | Branch (b, (a1, hint1), (a2, hint2)) ->
        let chosen_ahint =
          let other = Axis.proj ax other in
          let proj1 = Axis.proj ax a1 in
          let proj2 = Axis.proj ax a2 in
          let obj = C.proj_obj ax obj in
          match choose_branch_axis b obj proj1 proj2 ~other with
          | `First -> a1, hint1
          | `Second -> a2, hint2
        in
        hint_prod obj side ax ~other chosen_ahint

    (** Given a solver hint on a single axis lattice, returns a human-readible
        hint. *)
    and hint_axis : type a l r.
        a C.obj ->
        (l * r) side ->
        other:a ->
        (a, l * r) S.ahint ->
        (a, l * r) ahint =
     fun obj side ~other (a, hint) ->
      match hint with
      | Apply (morph_hint, morph, ahint) ->
        hint_apply obj side a morph_hint morph ~other ahint
          (C.For_hint.find_responsible_axis_single morph)
      | Const c -> a, Const c
      | Branch (b, (a1, hint1), (a2, hint2)) ->
        let chosen_ahint =
          match choose_branch_axis b obj a1 a2 ~other with
          | `First -> a1, hint1
          | `Second -> a2, hint2
        in
        hint_axis obj side ~other chosen_ahint

    let hint_prod_loosening : type t a l r.
        t C.obj ->
        (l * r) side ->
        (t, a) Axis.t ->
        other:t ->
        (t, l * r) S.ahint ->
        loosening * (a, l * r) ahint =
     fun obj side ax ~other ((t, _) as ahint) ->
      let axis_obj = C.proj_obj ax obj in
      let a, hint = hint_prod obj side ax ~other ahint in
      let loosening =
        if Misc.Le_result.equal ~le:(C.le axis_obj) a (Axis.proj ax t)
        then Not_loosened
        else Loosened
      in
      loosening, (a, hint)

    let hint_axis_loosening : type a l r.
        a C.obj ->
        (l * r) side ->
        other:a ->
        (a, l * r) S.ahint ->
        loosening * (a, l * r) ahint =
     fun obj side ~other ((original, _) as ahint) ->
      let a, hint = hint_axis obj side ~other ahint in
      let loosening =
        if Misc.Le_result.equal ~le:(C.le obj) a original
        then Not_loosened
        else Loosened
      in
      loosening, (a, hint)

    let error_prod : type r a. r C.obj -> (r, a) Axis.t -> r S.error -> a t =
     fun obj axis { left; right } ->
      let left = hint_prod_loosening obj Left axis ~other:(fst right) left in
      let right =
        hint_prod_loosening obj Right axis
          ~other:(Axis.set axis (fst (snd left)) (fst right))
          right
      in
      { left; right }

    let error_axis : type a. a C.obj -> a S.error -> a t =
     fun obj { left; right } ->
      let left = hint_axis_loosening obj Left ~other:(fst right) left in
      let right = hint_axis_loosening obj Right ~other:(fst (snd left)) right in
      { left; right }
  end

  [@@@warning "-4"]

  type sound =
    | Consonant
    | Vowel

  let print_article_noun ~definite ~capitalize sound s =
    let article =
      match definite, sound with
      | true, _ -> "the"
      | false, Consonant -> "a"
      | false, Vowel -> "an"
    in
    let article =
      if capitalize then String.capitalize_ascii article else article
    in
    Fmt.dprintf "%s %s" article s

  let print_lock_item : lock_item -> _ = function
    | Module -> print_article_noun Consonant "module"
    | Class -> print_article_noun Consonant "class"
    | Value -> print_article_noun Consonant "value"
    | Constructor -> print_article_noun Consonant "constructor"

  let print_structure_item : structure_item -> _ =
   fun (category, id) ~capitalize ->
    Fmt.dprintf "%t %a"
      (print_lock_item ~definite:true ~capitalize category)
      Misc.Style.inline_code (Ident.name id)

  let print_pinpoint_desc : pinpoint_desc -> _ = function
    | Unknown -> None
    | Ident { category; lid } ->
      Some
        (fun ~definite ~capitalize ->
          Fmt.dprintf "%t %a"
            (print_lock_item ~definite ~capitalize category)
            (Misc.Style.as_inline_code !print_longident)
            lid)
    | Function -> Some (print_article_noun Consonant "function")
    | Functor -> Some (print_article_noun Consonant "functor")
    | Lazy -> Some (print_article_noun Consonant "lazy expression")
    | Quote -> Some (print_article_noun Consonant "quoted expression")
    | Expression -> Some (print_article_noun Vowel "expression")
    | Allocation -> Some (print_article_noun Vowel "allocation")
    | Class -> Some (print_article_noun Consonant "class")
    | Object -> Some (print_article_noun Vowel "object")
    | Loop -> Some (print_article_noun Consonant "loop")
    | Letop -> Some (print_article_noun Consonant "letop")
    | Cases_result ->
      Some
        (fun ~definite ~capitalize ->
          Fmt.dprintf "%t of %t"
            (print_article_noun ~definite:true ~capitalize Consonant "result")
            (print_article_noun ~definite ~capitalize:false Consonant "cases"))
    | Pattern -> Some (print_article_noun Consonant "pattern")
    | Module -> Some (print_article_noun Consonant "module")
    | Structure -> Some (print_article_noun Consonant "structure")
    | Structure_item x ->
      Some
        (fun ~definite:_ ~capitalize ->
          Fmt.dprintf "%t in the structure" (print_structure_item ~capitalize x))

  let print_pinpoint : pinpoint -> _ =
   fun (loc, desc) ->
    print_pinpoint_desc desc
    |> Option.map (fun print_desc ~definite ~capitalize ppf ->
        match Location.is_none loc, definite with
        | true, _ -> print_desc ~definite:false ~capitalize ppf
        | false, true ->
          Fmt.fprintf ppf "%t at %a"
            (print_desc ~definite ~capitalize)
            (Location.Doc.loc ~capitalize_first:false)
            loc
        | false, false ->
          Fmt.fprintf ppf "%t (at %a)"
            (print_desc ~definite ~capitalize)
            (Location.Doc.loc ~capitalize_first:false)
            loc)

  let is_known_pinpoint : pinpoint -> bool = function
    | _, Unknown -> false
    | _ -> true

  let print_mutable_part ppf = function
    | Record_field s ->
      Fmt.fprintf ppf "mutable field %a" Misc.Style.inline_code s
    | Array_elements -> Fmt.fprintf ppf "array elements"

  let print_always_dynamic = function
    | Application -> Fmt.dprintf "function applications"
    | Try_with -> Fmt.dprintf "try-with clauses"

  let print_legacy = function
    | Toplevel -> print_article_noun Consonant "top-level clause"
    | Compilation_unit -> print_article_noun Consonant "compilation unit"
    | Class -> print_article_noun Consonant "class"
    | Quoted -> print_article_noun Consonant "quoted expression's result"

  let print_region_desc : region_desc -> _ = function
    | Borrow -> print_article_noun Consonant "borrow region"

  let print_region : capitalize:_ -> region -> _ =
   fun ~capitalize (loc, desc) ->
    Fmt.dprintf "%t at %a"
      (print_region_desc desc ~definite:true ~capitalize)
      (Location.Doc.loc ~capitalize_first:false)
      loc

  (** Given a pinpoint and a const, where the pinpoint has been expressed,
      prints the const to explain the mode on the pinpoint. *)
  let print_const (type l r) ((_, pp_desc) : pinpoint) ppf :
      (l * r) const -> unit = function
    | Unknown -> Misc.fatal_error "Unknown hint should not be printed"
    | Lazy_allocated_on_heap ->
      (match pp_desc with
      | Lazy ->
        (* if we already said it's a lazy, we don't need to emphasize it again. *)
        Fmt.pp_print_string ppf "lazy expressions always need"
      | _ -> Fmt.pp_print_string ppf "it is a lazy expression and thus needs");
      Fmt.pp_print_string ppf " to be allocated on the heap"
    | Legacy m ->
      (match pp_desc, m with
      | ( (Ident { category = Class; _ } | Class | Structure_item (Class, _)),
          Class ) ->
        (* if we already said it's a class, we don't need to emphasize it again. *)
        Fmt.pp_print_string ppf "classes are always"
      | _ ->
        Fmt.fprintf ppf "it is %t and thus always"
          (print_legacy m ~definite:false ~capitalize:false));
      Fmt.pp_print_string ppf " at the legacy modes"
    | Toplevel_expression ->
      Fmt.pp_print_string ppf "it is a top-level expression"
    | Tailcall_function ->
      Fmt.pp_print_string ppf "it is the function in a tail call"
    | Tailcall_argument ->
      Fmt.pp_print_string ppf "it is an argument in a tail call"
    | Mutable_read m ->
      Fmt.fprintf ppf "its %a is being read" print_mutable_part m
    | Mutable_write m ->
      Fmt.fprintf ppf "its %a is being written" print_mutable_part m
    | Lazy_forced -> (
      match pp_desc with
      | Lazy ->
        (* if we already said it's a lazy, we don't need to emphasize it again. *)
        Fmt.pp_print_string ppf "it is being forced"
      | _ -> Fmt.pp_print_string ppf "it is a lazy value being forced")
    | Function_return ->
      Fmt.fprintf ppf
        "it is a function return value.@ Hint: Use exclave_ to return a local \
         value"
    | Stack_expression ->
      Fmt.fprintf ppf "it is %a-allocated" Misc.Style.inline_code "stack_"
    | Module_allocated_on_heap ->
      (match pp_desc with
      | Ident { category = Module; _ }
      | Functor | Module | Structure
      | Structure_item (Module, _) ->
        (* if we already said it's a module, we don't need to emphasize it again. *)
        Fmt.pp_print_string ppf "modules always need"
      | _ -> Fmt.pp_print_string ppf "it is a module and thus needs");
      Fmt.pp_print_string ppf " to be allocated on the heap"
    | Is_used_in pp ->
      let print_pp = print_pinpoint pp |> Option.get in
      Fmt.fprintf ppf "it is used in %t"
        (print_pp ~definite:false ~capitalize:false)
    | Always_dynamic x ->
      Fmt.fprintf ppf "%t are always dynamic" (print_always_dynamic x)
    | Branching -> Fmt.fprintf ppf "it has branches"
    | Borrowed _ -> Fmt.fprintf ppf "it is borrowed"
    | Escape_region reg ->
      Fmt.fprintf ppf "it escapes %t" (print_region ~capitalize:false reg)
    | Quoted_computation -> Fmt.fprintf ppf "it is the quote of a computation"
    | Lpoly_inst ->
      Fmt.pp_print_string ppf
        "it is layout-polymorphic and being instantiated here"
    | Spliced _ -> Fmt.fprintf ppf "it is spliced"

  let print_allocation_l : allocation -> Fmt.formatter -> unit =
   fun { txt; loc } ->
    match txt with
    | Unknown ->
      Fmt.dprintf "is allocated at %a containing data"
        (Location.Doc.loc ~capitalize_first:false)
        loc
    | Optional_argument ->
      Fmt.dprintf
        "is an optional argument wrapper (and thus allocated) of the value at \
         %a"
        (Location.Doc.loc ~capitalize_first:false)
        loc
    | Function_coercion ->
      Fmt.dprintf
        "is a partial application of the function at %a on omittable parameters"
        (Location.Doc.loc ~capitalize_first:false)
        loc
    | Float_projection ->
      Fmt.dprintf
        "is projected (at %a) from a float record (and thus allocated)"
        (Location.Doc.loc ~capitalize_first:false)
        loc
    | Lpoly_captured_environment ->
      Fmt.dprintf "is defined by a layout-polymorphic expression (at %a)"
        (Location.Doc.loc ~capitalize_first:false)
        loc

  let print_allocation_r : allocation -> Fmt.formatter -> unit =
   fun { txt; _ } ->
    match txt with
    | Unknown -> Fmt.dprintf "is an allocation"
    | Optional_argument ->
      Fmt.dprintf
        "is to be put in an optional argument wrapper (and thus an allocation)"
    | Function_coercion ->
      Fmt.dprintf
        "is to omit some parameters by partial application (and thus an \
         allocation)"
    | Float_projection ->
      Fmt.dprintf "is a float-record projection (and thus an allocation)"
    | Lpoly_captured_environment ->
      (* currently not testable *)
      Fmt.dprintf "is a layout-polymorphic expression"

  let modality_if_relevant ~fixpoint pp =
    if
      fixpoint
      (* if the modality doesn't change the bound, we omit the modality and
          print the remaining chain. *)
    then (fun _ppf Modality -> ()), pp
    else
      (* if the modality change the bound, we signal that. Moreover, since each
         axis is total ordering, the modality is solely responsible for the
         bound, and we omit the remaining chain. *)
      (* CR-someday zqian: print the modality on the offending axis. *)
      ( (fun ppf Modality -> Fmt.fprintf ppf " (with some modality)"),
        (Location.none, Unknown : pinpoint) )

  let print_contains :
      fixpoint:bool -> contains -> ((Fmt.formatter -> unit) * pinpoint) option =
   fun ~fixpoint { containing; contained } ->
    print_pinpoint contained
    |> Option.map (fun print_pp ->
        let print_pp = print_pp ~definite:true ~capitalize:false in
        let maybe_modality, contained =
          modality_if_relevant ~fixpoint contained
        in
        let pr =
          match containing with
          | Tuple -> Fmt.dprintf "is a tuple that contains %t" print_pp
          | Record (s, moda) ->
            Fmt.dprintf "is a record whose field %a%a is %t"
              Misc.Style.inline_code s maybe_modality moda print_pp
          | Array moda ->
            Fmt.dprintf "is an array that contains%a %t" maybe_modality moda
              print_pp
          | Constructor (s, moda) ->
            Fmt.dprintf "contains (via constructor %a)%a %t"
              Misc.Style.inline_code s maybe_modality moda print_pp
          | Structure (x, moda) ->
            Fmt.dprintf "contains %t%a defined as %t"
              (print_structure_item ~capitalize:false x)
              maybe_modality moda print_pp
        in
        pr, contained)

  let print_is_contained_by :
      fixpoint:bool -> is_contained_by -> (Fmt.formatter -> unit) * pinpoint =
   fun ~fixpoint { containing; container } ->
    let maybe_modality, pp = modality_if_relevant ~fixpoint container in
    (* CR-someday zqian: Use the full [container] to improve the printing below.
       E.g., insted of printing "the tuple at XXX", we can print "the tuple
       pattern at XXX" or "the tuple expression at XXX". *)
    let container = fst container in
    let pr =
      match containing with
      | Tuple ->
        Fmt.dprintf "is an element of the tuple at %a"
          (Location.Doc.loc ~capitalize_first:false)
          container
      | Record (s, moda) ->
        Fmt.dprintf "is the field %a%a of the record at %a"
          Misc.Style.inline_code s maybe_modality moda
          (Location.Doc.loc ~capitalize_first:false)
          container
      | Array moda ->
        Fmt.dprintf "is an element%a of the array at %a" maybe_modality moda
          (Location.Doc.loc ~capitalize_first:false)
          container
      | Constructor (s, moda) ->
        Fmt.dprintf "is contained (via constructor %a)%a in the value at %a"
          Misc.Style.inline_code s maybe_modality moda
          (Location.Doc.loc ~capitalize_first:false)
          container
      | Structure (x, moda) ->
        Fmt.dprintf "is %t%a in the structure at %a"
          (print_structure_item ~capitalize:false x)
          maybe_modality moda
          (Location.Doc.loc ~capitalize_first:false)
          container
    in
    pr, pp

  (** Given a pinpoint and a morph, where the pinpoint is the destination of the
      morph and have been expressed already, print the morph and return the
      source pinpoint. The source pinpoint could be [Unknown], in which case the
      rest of the chain will not be printed. *)
  let print_morph : type l r.
      fixpoint:bool ->
      pinpoint ->
      (l * r) morph ->
      ((Fmt.formatter -> unit) * pinpoint) option =
   fun ~fixpoint pp -> function
    | Skip -> Misc.fatal_error "Skip hint should not be printed"
    | Unknown -> None
    | Close_over (Comonadic, { closed = pp; _ }) ->
      print_pinpoint pp
      |> Option.map (fun print_pp ->
          ( Fmt.dprintf "closes over %t"
              (print_pp ~definite:true ~capitalize:false),
            pp ))
    | Close_over (Monadic, { closed = pp; _ }) ->
      print_pinpoint pp
      |> Option.map (fun print_pp ->
          ( Fmt.dprintf "contains a usage (of %t)"
              (print_pp ~definite:true ~capitalize:false),
            pp ))
    | Is_closed_by (_, { closure = pp; _ }) ->
      print_pinpoint pp
      |> Option.map (fun print_pp ->
          ( Fmt.dprintf "is used inside %t"
              (print_pp ~definite:true ~capitalize:false),
            pp ))
    | Captured_by_partial_application ->
      Some
        ( Fmt.dprintf "is captured by a partial application",
          (Location.none, Expression) )
    | Adj_captured_by_partial_application ->
      Some
        ( Fmt.dprintf "has a partial application capturing a value",
          (Location.none, Expression) )
    | Crossing -> Some (Fmt.dprintf "crosses with something", pp)
    | Allocation_r alloc -> Some (print_allocation_r alloc, pp)
    | Allocation_l alloc -> Some (print_allocation_l alloc, pp)
    | Contains_l (_, contains) -> print_contains ~fixpoint contains
    | Contains_r (_, contains) -> print_contains ~fixpoint contains
    | Is_contained_by (_, is_contained_by) ->
      Some (print_is_contained_by ~fixpoint is_contained_by)

  let print_mode : type a.
      [`Actual | `Expected] -> a C.obj -> Fmt.formatter -> a -> unit =
   fun side obj ppf x ->
    let mode_printer = Misc.Style.as_inline_code (C.print obj) in
    match side, obj, x with
    | `Actual, Regionality, Regional ->
      Fmt.fprintf ppf "%a to the parent region" mode_printer C.Regionality.Local
      (* CR-someday zqian: treat the following cases generally. *)
    | `Expected, Contention_op, Shared ->
      (* When "shared" is expected, we tell the user that either shared or
         uncontended is expected. *)
      Fmt.fprintf ppf "%a or %a" mode_printer C.Contention.Shared mode_printer
        C.Contention.Uncontended
    | `Expected, Contention_op, Corrupted ->
      Fmt.fprintf ppf "%a or %a" mode_printer C.Contention.Corrupted
        mode_printer C.Contention.Uncontended
    | `Expected, Visibility_op, Read ->
      Fmt.fprintf ppf "%a or %a" mode_printer C.Visibility.Read mode_printer
        C.Visibility.Read_write
    | `Expected, Visibility_op, Write ->
      Fmt.fprintf ppf "%a or %a" mode_printer C.Visibility.Write mode_printer
        C.Visibility.Read_write
    | `Expected, Regionality, Regional ->
      Fmt.fprintf ppf "%a to the parent region or %a" mode_printer
        C.Regionality.Local mode_printer C.Regionality.Global
    | _ -> mode_printer ppf x
  [@@ocaml.warning "-4"]

  let adjust_side : type a. a C.obj -> [`Left | `Right] -> [`Actual | `Expected]
      =
   fun obj side ->
    match C.is_opposite obj, side with
    | true, `Left -> `Expected
    | true, `Right -> `Actual
    | false, `Left -> `Actual
    | false, `Right -> `Expected

  let print_mode_with_side : type a.
      sub:bool -> [`Left | `Right] -> a C.obj -> Fmt.formatter -> a -> unit =
   fun ~sub side obj ppf a ->
    let side = adjust_side obj side in
    if sub
    then (
      Fmt.fprintf ppf "@ which ";
      match side with
      | `Actual -> Fmt.pp_print_string ppf "is "
      | `Expected -> Fmt.pp_print_string ppf "is expected to be ");
    print_mode side obj ppf a

  (** Some morph hints are said to be "non-rigid", because they should be
      printed only when they change modes. *)
  let is_rigid : type l r. (l * r) morph -> bool = function
    | Unknown -> true
    | Close_over _ | Is_closed_by _ | Captured_by_partial_application
    | Contains_l _ | Contains_r _ | Is_contained_by _
    | Adj_captured_by_partial_application ->
      true
    | Allocation_r _ | Allocation_l _ | Skip | Crossing -> false

  let equal_mode : type a b. a C.obj -> b C.obj -> a -> b -> bool =
   fun a_obj b_obj a b ->
    match C.equal_obj a_obj b_obj with
    | Misc.Is_eq -> Misc.Le_result.equal ~le:(C.le a_obj) a b
    | Misc.Is_not_eq -> false

  let rec print_ahint : type a l r.
      ?sub:bool ->
      [`Left | `Right] ->
      pinpoint ->
      a C.obj ->
      Fmt.formatter ->
      (a, l * r) ahint ->
      print_error_result option =
   fun ?(sub = false) side pp (obj : a C.obj) ppf (a, hint) ->
    match hint with
    | Apply (morph_hint, src, ahint) ->
      let fixpoint = equal_mode obj src a (fst ahint) in
      if (not (is_rigid morph_hint)) && fixpoint
      then print_ahint ~sub side pp src ppf ahint
      else (
        print_mode_with_side ~sub side obj ppf a;
        match print_morph ~fixpoint pp morph_hint with
        | None -> Some Mode
        | Some (t, pp) ->
          Fmt.fprintf ppf "@ because it %t" t;
          if is_known_pinpoint pp
          then ignore (print_ahint ~sub:true side pp src ppf ahint);
          Some Mode_with_hint)
    | Const Unknown ->
      print_mode_with_side ~sub side obj ppf a;
      Some Mode
    | Irrelevant ->
      if not sub
      then
        Misc.fatal_error
          "the current mode is not responsible for the error, so must be \
           inside a responsible morphism";
      None
    | Const c ->
      Fmt.fprintf ppf "%a@ because %a"
        (print_mode_with_side ~sub side obj)
        a (print_const pp) c;
      Some Mode_with_hint
  [@@ocaml.warning "-4"]

  let print_ahint_loosening : type a l r.
      [`Left | `Right] ->
      pinpoint ->
      a C.obj ->
      Fmt.formatter ->
      loosening ->
      (a, l * r) ahint ->
      print_error_result option =
   fun side pp obj ppf loosening ahint ->
    (match loosening with
    | Loosened ->
      begin match adjust_side obj side with
      | `Actual -> Fmt.fprintf ppf "weaker than "
      | `Expected -> Fmt.fprintf ppf "stronger than "
      end
    | Not_loosened -> ());
    print_ahint side pp obj ppf ahint

  type 'a ahint_sided =
    | Left of (loosening * ('a, left_only) ahint)
    | Right of (loosening * ('a, right_only) ahint)

  let print_ahint_sided : type a.
      pinpoint ->
      a C.obj ->
      Fmt.formatter ->
      a ahint_sided ->
      print_error_result option =
   fun pp obj ppf ahint_sided ->
    match ahint_sided with
    | Left (loosening, ahint) ->
      print_ahint_loosening `Left pp obj ppf loosening ahint
    | Right (loosening, ahint) ->
      print_ahint_loosening `Right pp obj ppf loosening ahint

  let print : type a. pinpoint -> a C.obj -> a t -> print_error =
   fun pp obj { left; right } ->
    let actual, expected =
      if C.is_opposite obj
      then Right right, Left left
      else Left left, Right right
    in
    let left ppf = Option.get (print_ahint_sided pp obj ppf actual) in
    let right ppf = Option.get (print_ahint_sided pp obj ppf expected) in
    { left; right }
end

let print_pinpoint = Report.print_pinpoint

type changes = S.changes

let undo_changes = S.undo_changes

(* To be filled in by [types.ml] *)
let append_changes : (changes ref -> unit) ref = ref (fun _ -> assert false)

let set_append_changes f = append_changes := f

type ('a, 'd) mode = ('a, 'd) S.mode

module Error = struct
  type 'a t = 'a S.error_raw

  type packed =
    | Product : 'r C.obj * ('r, 'a) Axis.t * 'r t -> packed
    | Axis : 'a C.obj * 'a t -> packed

  let print_product : type r a.
      Hint.pinpoint -> r C.obj -> (r, a) Axis.t -> r t -> print_error =
   fun pp obj ax err ->
    let err = S.populate_error obj err in
    let err = Report.Of_solver.error_prod obj ax err in
    let obj = C.proj_obj ax obj in
    Report.print pp obj err

  let print_axis : type a. Hint.pinpoint -> a C.obj -> a t -> print_error =
   fun pp obj err ->
    let err = S.populate_error obj err in
    let err = Report.Of_solver.error_axis obj err in
    Report.print pp obj err

  let print_packed : Hint.pinpoint -> packed -> print_error =
   fun pp -> function
    | Product (obj, ax, err) -> print_product pp obj ax err
    | Axis (obj, err) -> print_axis pp obj err

  let print_packed_simple_context : Hint.pinpoint -> packed -> Location.error =
   fun pp packed ->
    let open Format_doc in
    let loc, desc = pp in
    let print ppf () =
      let open_box = Fmt.dprintf "@[<hov 2>" in
      let reopen_box = Fmt.dprintf "@]@ %t" open_box in
      let print_desc = Report.print_pinpoint_desc desc in
      (let print_desc =
         match print_desc with
         | None -> Fmt.dprintf "This"
         | Some print_desc -> print_desc ~definite:true ~capitalize:true
       in
       fprintf ppf "%t%t is " open_box print_desc);
      let ({ left; right } : print_error) = print_packed pp packed in
      (match left ppf with
      | Mode_with_hint ->
        let print_desc =
          match print_desc with
          | None -> Fmt.dprintf "the highlighted"
          | Some print_desc ->
            Fmt.dprintf "%t highlighted"
              (print_desc ~definite:true ~capitalize:false)
        in
        fprintf ppf ".%tHowever, %t is expected to be " reopen_box print_desc
      | Mode -> fprintf ppf "%tbut is expected to be " reopen_box);
      ignore (right ppf);
      fprintf ppf ".@]"
    in
    Location.error_of_printer ~loc print ()
end

exception Submode_error_simple_context of Hint.pinpoint * Error.packed

let () =
  Location.register_error_of_exn (function
    | Submode_error_simple_context (pp, err) ->
      Some (Error.print_packed_simple_context pp err)
    | _ -> None)

module type Common_axis_pos = sig
  module Const : Const

  include
    Common_axis
      with module Const := Const
       and type 'd t = (Const.t, 'd pos) mode
       and type 'd hint_const := 'd pos_hint_const
end

module type Common_axis_neg = sig
  module Const : Const

  include
    Common_axis
      with module Const := Const
       and type 'd t = (Const.t, 'd neg) mode
       and type 'd hint_const := 'd neg_hint_const
end

(** Representing a single object *)
module type Obj = sig
  type const

  val obj : const C.obj
end

let try_with_log op =
  let log' = ref S.empty_changes in
  let log = Some log' in
  match op ~log with
  | Ok _ as x ->
    !append_changes log';
    x
  | Error _ as x ->
    S.undo_changes !log';
    x
[@@inline]

let with_log op =
  let log' = ref S.empty_changes in
  let log = Some log' in
  let r = op ~log in
  !append_changes log';
  r
[@@inline]

let equate_from_submode submode_log m1 m2 ~log =
  match submode_log m1 m2 ~log with
  | Error e -> Error (Left_le_right, e)
  | Ok () -> (
    match submode_log m2 m1 ~log with
    | Error e -> Error (Right_le_left, e)
    | Ok () -> Ok ())
[@@inline]

let equate_from_submode' submode m1 m2 =
  match submode m1 m2 with
  | Error e -> Error (Left_le_right, e)
  | Ok () -> (
    match submode m2 m1 with
    | Error e -> Error (Right_le_left, e)
    | Ok () -> Ok ())
[@@inline]

module Comonadic_gen (Obj : Obj) = struct
  open Obj

  type 'd t = (const, 'l * 'r) S.mode constraint 'd = 'l * 'r

  type l = (allowed * disallowed) t

  type r = (disallowed * allowed) t

  type lr = (allowed * allowed) t

  type nonrec simple_error = const simple_error

  type nonrec error = const Error.t

  type equate_error = equate_step * error

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

  let disallow_right m = S.disallow_right m

  let disallow_left m = S.disallow_left m

  let allow_left m = S.allow_left m

  let allow_right m = S.allow_right m

  let newvar () = S.newvar obj

  let min = S.min obj

  let max = S.max obj

  let newvar_above m = S.newvar_above obj m

  let newvar_below m = S.newvar_below obj m

  let submode_log ?(pp = (Location.none, Unknown : Hint.pinpoint)) a b ~log =
    S.submode pp obj a b ~log

  let to_simple_error ({ left; right; _ } : error) : simple_error =
    { left; right }

  let submode ?pp a b = try_with_log (submode_log ?pp a b)

  let submode_err pp a b =
    match submode ~pp a b with
    | Ok () -> ()
    | Error e -> raise (Submode_error_simple_context (pp, Axis (obj, e)))

  let print_error pp err = Error.print_axis pp obj err

  let join l = S.join obj l

  let meet l = S.meet obj l

  let submode_exn ?pp m1 m2 = submode ?pp m1 m2 |> Result.get_ok

  let equate a b = try_with_log (equate_from_submode (submode_log ?pp:None) a b)

  let equate_exn m1 m2 = equate m1 m2 |> Result.get_ok

  let print ?verbose () ppf m = S.print ?verbose obj ppf m

  let zap_to_ceil m = with_log (S.zap_to_ceil obj m)

  let zap_to_floor m = with_log (S.zap_to_floor obj m)

  let of_const : type l r. ?hint:(l * r) pos Hint.const -> const -> (l * r) t =
   fun ?hint a -> S.of_const ?hint obj a

  let to_const_exn m = S.to_const_exn obj m

  let unhint = S.Unhint.unhint

  let hint ?hint = S.Unhint.hint obj ?hint

  let wrap ?hint:h f m = m |> unhint |> f |> hint ?hint:h

  let apply_hint hint m = wrap ~hint Fun.id m

  let meet_const_unhint c m = S.Unhint.apply obj (Meet_const c) m

  let meet_const ?hint c m = wrap ?hint (meet_const_unhint c) m

  let imply_const_unhint c m = S.Unhint.apply obj (Imply_const c) m

  let imply_const c m = m |> disallow_left |> wrap (imply_const_unhint c)

  module Guts = struct
    let get_floor m = S.get_floor obj m

    let get_ceil m = S.get_ceil obj m

    let get_loose_floor m = S.get_loose_floor obj m

    let get_loose_ceil m = S.get_loose_ceil obj m
  end
end
[@@inline]

module Monadic_gen (Obj : Obj) = struct
  (* Monadic lattices are flipped. See "Notes on flipping". *)
  open Obj

  type 'd t = (const, 'r * 'l) S.mode constraint 'd = 'l * 'r

  type l = (allowed * disallowed) t

  type r = (disallowed * allowed) t

  type lr = (allowed * allowed) t

  type nonrec simple_error = const simple_error

  type nonrec error = const Error.t

  type equate_error = equate_step * error

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

  let disallow_right m = S.disallow_left m

  let disallow_left m = S.disallow_right m

  let allow_left m = S.allow_right m

  let allow_right m = S.allow_left m

  let newvar () = S.newvar obj

  let min = S.max obj

  let max = S.min obj

  let newvar_above m = S.newvar_below obj m

  let newvar_below m = S.newvar_above obj m

  let submode_log ?(pp = (Location.none, Unknown : Hint.pinpoint)) a b ~log =
    S.submode pp obj b a ~log

  let to_simple_error ({ left; right; _ } : error) : simple_error =
    { left = right; right = left }

  let submode ?pp a b = try_with_log (submode_log ?pp a b)

  let submode_err pp a b =
    match submode ~pp a b with
    | Ok () -> ()
    | Error e -> raise (Submode_error_simple_context (pp, Axis (obj, e)))

  let print_error pp err = Error.print_axis pp obj err

  let join l = S.meet obj l

  let meet l = S.join obj l

  let submode_exn ?pp m1 m2 = submode ?pp m1 m2 |> Result.get_ok

  let equate a b = try_with_log (equate_from_submode (submode_log ?pp:None) a b)

  let equate_exn m1 m2 = equate m1 m2 |> Result.get_ok

  let print ?verbose () ppf m = S.print ?verbose obj ppf m

  let zap_to_ceil m = with_log (S.zap_to_floor obj m)

  let zap_to_floor m = with_log (S.zap_to_ceil obj m)

  let of_const : type l r. ?hint:(l * r) neg Hint.const -> const -> (l * r) t =
   fun ?hint a -> S.of_const ?hint obj a

  let to_const_exn m = S.to_const_exn obj m

  let unhint = S.Unhint.unhint

  let hint ?hint = S.Unhint.hint obj ?hint

  let wrap ?hint:h f m = m |> unhint |> f |> hint ?hint:h

  let apply_hint hint m = wrap ~hint Fun.id m

  let join_const_unhint c m = S.Unhint.apply Obj.obj (Meet_const c) m

  let join_const ?hint c m = wrap ?hint (join_const_unhint c) m

  let subtract_const_unhint c m = S.Unhint.apply obj (Imply_const c) m

  let subtract_const c m = m |> disallow_right |> wrap (subtract_const_unhint c)

  module Guts = struct
    let get_ceil m = S.get_floor obj m
  end
end
[@@inline]

module Locality = struct
  module Const = C.Locality

  module Obj = struct
    type const = Const.t

    let obj = C.Locality
  end

  include Comonadic_gen (Obj)

  let global = of_const Global

  let local = of_const Local

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_floor

  module Guts = struct
    let check_const m =
      let floor = Guts.get_floor m in
      let ceil = Guts.get_ceil m in
      if Const.le ceil floor then Some ceil else None

    let check_const_conservative m =
      let floor = Guts.get_loose_floor m in
      let ceil = Guts.get_loose_ceil m in
      if Const.le ceil floor then Some ceil else None
  end
end

module Regionality = struct
  module Const = C.Regionality

  module Obj = struct
    type const = Const.t

    let obj = C.Regionality
  end

  include Comonadic_gen (Obj)

  let local = of_const Const.Local

  let regional = of_const Const.Regional

  let global = of_const Const.Global

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_floor
end

module Linearity = struct
  module Const = C.Linearity

  module Obj = struct
    type const = Const.t

    let obj : _ C.obj = C.Linearity
  end

  include Comonadic_gen (Obj)

  let many = of_const Many

  let once = of_const Once

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_floor
end

module Statefulness = struct
  module Const = C.Statefulness

  module Obj = struct
    type const = Const.t

    let obj = C.Statefulness
  end

  include Comonadic_gen (Obj)

  let stateless = of_const Stateless

  let reading = of_const Reading

  let writing = of_const Writing

  let stateful = of_const Stateful

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_ceil
end

module Visibility = struct
  module Const = C.Visibility

  module Obj = struct
    type const = Const.t

    let obj = C.Visibility_op
  end

  include Monadic_gen (Obj)

  let immutable = of_const Immutable

  let read = of_const Read

  let write = of_const Write

  let read_write = of_const Read_write

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_floor
end

module Portability = struct
  module Const = C.Portability

  module Obj = struct
    type const = Const.t

    let obj : _ C.obj = C.Portability
  end

  include Comonadic_gen (Obj)

  let legacy = of_const Const.legacy

  (* CR dkalinichenko: ideally, [reading] should zap to [shareable]. *)
  let zap_to_legacy ~statefulness =
    match statefulness with
    | Statefulness.Const.Stateful | Statefulness.Const.Reading
    | Statefulness.Const.Writing ->
      zap_to_ceil
    | Statefulness.Const.Stateless -> zap_to_floor
end

module Uniqueness = struct
  module Const = C.Uniqueness

  module Obj = struct
    type const = Const.t

    let obj = C.Uniqueness_op
  end

  include Monadic_gen (Obj)

  let aliased = of_const Aliased

  let unique = of_const Unique

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_ceil
end

module Contention = struct
  module Const = C.Contention

  module Obj = struct
    type const = Const.t

    let obj = C.Contention_op
  end

  include Monadic_gen (Obj)

  let legacy = of_const Const.legacy

  (* CR dkalinichenko: ideally, [read] should zap to [shared]. *)
  let zap_to_legacy ~visibility =
    match visibility with
    | Visibility.Const.Read_write | Visibility.Const.Read
    | Visibility.Const.Write ->
      zap_to_floor
    | Visibility.Const.Immutable -> zap_to_ceil
end

module Forkable = struct
  module Const = C.Forkable

  module Obj = struct
    type const = Const.t

    let obj = C.Forkable
  end

  include Comonadic_gen (Obj)

  let unforkable = of_const Unforkable

  let forkable = of_const Forkable

  let legacy = of_const Const.legacy

  (* [forkable] is the default for [global]s and [unforkable] for [local]
     or [regional] values, so we vary [zap_to_legacy] accordingly. *)
  let zap_to_legacy ~global =
    match global with true -> zap_to_floor | false -> zap_to_ceil
end

module Yielding = struct
  module Const = C.Yielding

  module Obj = struct
    type const = Const.t

    let obj = C.Yielding
  end

  include Comonadic_gen (Obj)

  let yielding = of_const Yielding

  let unyielding = of_const Unyielding

  let legacy = of_const Const.legacy

  (* [unyielding] is the default for [global]s and [yielding] for [local]
     or [regional] values, so we vary [zap_to_legacy] accordingly. *)
  let zap_to_legacy ~global =
    match global with true -> zap_to_floor | false -> zap_to_ceil
end

module Staticity = struct
  module Const = C.Staticity

  type const = Const.t =
    | Static
    | Dynamic

  module Obj = struct
    type const = Const.t

    let obj = C.Staticity_op
  end

  include Monadic_gen (Obj)

  let legacy = of_const Const.legacy

  let zap_to_legacy = zap_to_ceil
end

let regional_to_local m = S.apply Locality.Obj.obj C.Regional_to_local m

let locality_as_regionality m =
  S.apply Regionality.Obj.obj C.Locality_as_regionality m

let regional_to_global m = S.apply Locality.Obj.obj C.Regional_to_global m

module type Areality = sig
  module Const : C.Areality

  module Obj : Obj with type const = Const.t

  val zap_to_legacy : (Const.t, allowed * 'r) S.mode -> Const.t
end

module Lattice_Product (L : Lattice) = struct
  open L

  let min_with ax c = Axis.set ax c min

  let max_with ax c = Axis.set ax c max
end

module Comonadic_with (Areality : Areality) = struct
  module Obj = struct
    type const = Areality.Const.t C.comonadic_with

    let obj = C.comonadic_with_obj Areality.Obj.obj
  end

  include Comonadic_gen (Obj)

  module Axis = struct
    type 'a t = (Obj.const, 'a) Axis.t

    type packed = P : 'a t -> packed

    let print = Axis.print

    let compare = Axis.compare

    let proj = Axis.proj

    let all =
      [ P Areality;
        P Linearity;
        P Portability;
        P Forkable;
        P Yielding;
        P Statefulness ]
      |> List.sort (fun (P ax1) (P ax2) -> compare ax1 ax2)
  end

  let proj_obj ax = (C.proj_obj [@inlined hint]) ax Obj.obj

  module Const = struct
    include C.Comonadic_with (Areality.Const)
    include Lattice_Product (C.Comonadic_with (Areality.Const))

    let proj = Axis.proj

    module Per_axis = struct
      let print ax ppf a =
        let obj = proj_obj ax in
        C.print obj ppf a

      let le ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.le [@inlined hint]) obj a b

      let equal ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.equal [@inlined hint]) obj a b

      let join ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.join [@inlined hint]) obj a b

      let meet ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.meet [@inlined hint]) obj a b

      let max ax =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.max [@inlined hint]) obj

      let min ax =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.min [@inlined hint]) obj

      let compare_obj ax1 ax2 =
        let obj1 = proj_obj ax1 in
        let obj2 = proj_obj ax2 in
        C.compare_obj obj1 obj2

      let equal_obj ax1 ax2 =
        let obj1 = proj_obj ax1 in
        let obj2 = proj_obj ax2 in
        C.equal_obj obj1 obj2

      let print_obj ppf ax =
        let obj = proj_obj ax in
        C.print_obj ppf obj
    end
  end

  let proj ax m = S.apply ~hint:Skip (proj_obj ax) (Proj (Obj.obj, ax)) m

  module Per_axis = struct
    let zap_to_floor ax m =
      let obj = proj_obj ax in
      with_log (S.zap_to_floor obj m)

    let zap_to_ceil ax m =
      let obj = proj_obj ax in
      with_log (S.zap_to_ceil obj m)
  end

  let min_with ax m =
    S.apply ~hint:Skip Obj.obj (Min_with ax) (S.disallow_right m)

  let max_with ax m =
    S.apply ~hint:Skip Obj.obj (Max_with ax) (S.disallow_left m)

  let meet_const_with ax c m = meet_const (Const.max_with ax c) m

  let zap_to_legacy m : Const.t =
    let areality = proj Areality m |> Areality.zap_to_legacy in
    let linearity = proj Linearity m |> Linearity.zap_to_legacy in
    let statefulness = proj Statefulness m |> Statefulness.zap_to_legacy in
    let portability =
      proj Portability m |> Portability.zap_to_legacy ~statefulness
    in
    let global = Areality.Const.(equal areality legacy) in
    let forkable = proj Forkable m |> Forkable.zap_to_legacy ~global in
    let yielding = proj Yielding m |> Yielding.zap_to_legacy ~global in
    { areality; linearity; portability; forkable; yielding; statefulness }

  let legacy = of_const Const.legacy

  type simple_error =
    | Error : 'a Axis.t * 'a Mode_intf.simple_error -> simple_error

  let axis_of_error (actual : Obj.const) (expected : Obj.const) : simple_error =
    List.find_map
      (fun (Axis.P ax) ->
        let left = Const.proj ax actual in
        let right = Const.proj ax expected in
        if Const.Per_axis.le ax left right
        then None
        else Some (Error (ax, { left; right })))
      Axis.all
    |> Option.get

  (* overriding to report the offending axis *)
  let to_simple_error ({ left; right; _ } : error) = axis_of_error left right

  let submode_err pp a b =
    match submode ~pp a b with
    | Ok () -> ()
    | Error e ->
      let (Error (ax, _)) = to_simple_error e in
      raise (Submode_error_simple_context (pp, Product (Obj.obj, ax, e)))

  let print_error pp err =
    let (Error (ax, _)) = to_simple_error err in
    Error.print_product pp Obj.obj ax err
end
[@@inline]

module Monadic = struct
  (* Monadic lattices are flipped. See "Notes on flipping". *)
  module Obj = struct
    type const = C.Monadic_op.t

    let obj = C.Monadic_op
  end

  include Monadic_gen (Obj)

  module Axis = struct
    type 'a t = (Obj.const, 'a) C.Axis.t

    type packed = P : 'a t -> packed

    let compare = Axis.compare

    let print = Axis.print

    let proj = Axis.proj

    let all =
      [P Uniqueness; P Contention; P Visibility; P Staticity]
      |> List.sort (fun (P ax1) (P ax2) -> compare ax1 ax2)
  end

  let proj_obj ax = (C.proj_obj [@inlined hint]) ax Obj.obj

  module Const = struct
    include C.Monadic
    include Lattice_Product (C.Monadic)

    let proj = Axis.proj

    module Per_axis = struct
      let print ax ppf a =
        let obj = proj_obj ax in
        C.print obj ppf a

      (* See "Notes on flipping" *)

      let le ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.le [@inlined hint]) obj b a

      let equal ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.equal [@inlined hint]) obj b a

      let join ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.meet [@inlined hint]) obj a b

      let meet ax a b =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.join [@inlined hint]) obj a b

      let max ax =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.min [@inlined hint]) obj

      let min ax =
        let obj = (proj_obj [@inlined hint]) ax in
        (C.max [@inlined hint]) obj

      let compare_obj ax1 ax2 =
        let obj1 = proj_obj ax1 in
        let obj2 = proj_obj ax2 in
        C.compare_obj obj1 obj2

      let equal_obj ax1 ax2 =
        let obj1 = proj_obj ax1 in
        let obj2 = proj_obj ax2 in
        C.equal_obj obj1 obj2

      let print_obj ppf ax =
        let obj = proj_obj ax in
        C.print_obj ppf obj
    end
  end

  let proj ax m = S.apply ~hint:Skip (proj_obj ax) (Proj (Obj.obj, ax)) m

  module Per_axis = struct
    let zap_to_floor ax m =
      let obj = proj_obj ax in
      with_log (S.zap_to_ceil obj m)

    let zap_to_ceil ax m =
      let obj = proj_obj ax in
      with_log (S.zap_to_floor obj m)
  end

  (* The monadic fragment is inverted. *)

  let join_const_with ax c m = join_const (Const.min_with ax c) m

  let min_with ax m =
    S.apply ~hint:Skip Obj.obj (Max_with ax) (S.disallow_left m)

  let zap_to_legacy m : Const.t =
    let uniqueness = proj Uniqueness m |> Uniqueness.zap_to_legacy in
    let visibility = proj Visibility m |> Visibility.zap_to_legacy in
    let contention =
      proj Contention m |> Contention.zap_to_legacy ~visibility
    in
    let staticity = proj Staticity m |> Staticity.zap_to_legacy in
    { uniqueness; contention; visibility; staticity }

  let legacy = of_const Const.legacy

  type simple_error =
    | Error : 'a Axis.t * 'a Mode_intf.simple_error -> simple_error

  let axis_of_error (actual : Obj.const) (expected : Obj.const) : simple_error =
    List.find_map
      (fun (Axis.P ax) ->
        let left = Const.proj ax actual in
        let right = Const.proj ax expected in
        if Const.Per_axis.le ax left right
        then None
        else Some (Error (ax, { left; right })))
      Axis.all
    |> Option.get

  let to_simple_error ({ left; right; _ } : error) =
    (* monadic fragment is flipped *)
    axis_of_error right left

  let submode_err pp a b =
    match submode ~pp a b with
    | Ok () -> ()
    | Error e ->
      let (Error (ax, _)) = to_simple_error e in
      raise (Submode_error_simple_context (pp, Product (Obj.obj, ax, e)))

  let print_error pp err =
    let (Error (ax, _)) = to_simple_error err in
    Error.print_product pp Obj.obj ax err
end

type ('mo, 'como) monadic_comonadic =
  { monadic : 'mo;
    comonadic : 'como
  }

module Value_with (Areality : Areality) = struct
  module Comonadic = Comonadic_with (Areality)
  module Monadic = Monadic

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

  type l = (allowed * disallowed) t

  type r = (disallowed * allowed) t

  type lr = (allowed * allowed) t

  module Axis = struct
    type 'a t =
      | Comonadic : 'a Comonadic.Axis.t -> 'a t
      | Monadic : 'a Monadic.Axis.t -> 'a t

    let compare : type a b. a t -> b t -> int =
     fun t1 t2 ->
      match t1, t2 with
      | Comonadic t1, Comonadic t2 -> Axis.compare t1 t2
      | Comonadic _, _ -> -1
      | _, Comonadic _ -> 1
      | Monadic t1, Monadic t2 -> Axis.compare t1 t2

    type packed = P : 'a t -> packed

    let print (type a) ppf (t : a t) =
      match t with
      | Monadic ax -> Axis.print ppf ax
      | Comonadic ax -> Axis.print ppf ax

    let all =
      List.map (fun (Monadic.Axis.P ax) -> P (Monadic ax)) Monadic.Axis.all
      @ List.map
          (fun (Comonadic.Axis.P ax) -> P (Comonadic ax))
          Comonadic.Axis.all
      |> List.sort (fun (P ax1) (P ax2) -> compare ax1 ax2)
  end

  let proj_obj : type a. a Axis.t -> a C.obj = function
    | Monadic ax -> Monadic.proj_obj ax
    | Comonadic ax -> Comonadic.proj_obj ax

  (* CR-soon zqian: make a functor [Mode.Value.Const.Make] to generalize over any type
     operator applied on each mode constants. *)
  type ('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
    }

  let split
      { areality;
        linearity;
        portability;
        forkable;
        yielding;
        statefulness;
        uniqueness;
        contention;
        visibility;
        staticity
      } =
    let monadic : Monadic.Const.t =
      { uniqueness; contention; visibility; staticity }
    in
    let comonadic : Comonadic.Const.t =
      { areality; linearity; portability; forkable; yielding; statefulness }
    in
    { comonadic; monadic }

  let merge { comonadic; monadic } =
    let ({ areality; linearity; portability; forkable; yielding; statefulness }
          : Comonadic.Const.t) =
      comonadic
    in
    let ({ uniqueness; contention; visibility; staticity } : Monadic.Const.t) =
      monadic
    in
    { areality;
      linearity;
      portability;
      forkable;
      yielding;
      statefulness;
      uniqueness;
      contention;
      visibility;
      staticity
    }

  let print ?verbose () ppf { monadic; comonadic } =
    Fmt.fprintf ppf "%a;%a"
      (Comonadic.print ?verbose ())
      comonadic
      (Monadic.print ?verbose ())
      monadic

  let of_const ?hint_monadic ?hint_comonadic c =
    let { monadic; comonadic } = split c in
    let comonadic = Comonadic.of_const ?hint:hint_comonadic comonadic in
    let monadic = Monadic.of_const ?hint:hint_monadic monadic in
    { comonadic; monadic }

  let to_const_exn m =
    let { comonadic; monadic } = m in
    let comonadic = Comonadic.to_const_exn comonadic in
    let monadic = Monadic.to_const_exn monadic in
    { comonadic; monadic } |> merge

  let unhint { monadic; comonadic } =
    let comonadic = Comonadic.unhint comonadic in
    let monadic = Monadic.unhint monadic in
    { monadic; comonadic }

  let hint ?monadic ?comonadic t =
    let comonadic = Comonadic.hint ?hint:comonadic t.comonadic in
    let monadic = Monadic.hint ?hint:monadic t.monadic in
    { monadic; comonadic }

  let wrap ?monadic ?comonadic f t =
    t |> unhint |> f |> hint ?monadic ?comonadic

  module Const = struct
    let comonadic_to_monadic_min = C.comonadic_to_monadic_min Comonadic.Obj.obj

    module Monadic = Monadic.Const
    module Comonadic = Comonadic.Const

    (* CR-soon zqian: make a functor [Mode.Value.Const.Make] to generalize over any type
       operator applied on each mode constants. *)
    type t =
      ( Areality.Const.t,
        Linearity.Const.t,
        Uniqueness.Const.t,
        Portability.Const.t,
        Contention.Const.t,
        Forkable.Const.t,
        Yielding.Const.t,
        Statefulness.Const.t,
        Visibility.Const.t,
        Staticity.Const.t )
      modes

    let min = merge { comonadic = Comonadic.min; monadic = Monadic.min }

    let max = merge { comonadic = Comonadic.max; monadic = Monadic.max }

    let le m1 m2 =
      let m1 = split m1 in
      let m2 = split m2 in
      Comonadic.le m1.comonadic m2.comonadic && Monadic.le m1.monadic m2.monadic

    let equal m1 m2 =
      let m1 = split m1 in
      let m2 = split m2 in
      Comonadic.equal m1.comonadic m2.comonadic
      && Monadic.equal m1.monadic m2.monadic

    let print ppf m =
      let { monadic; comonadic } = split m in
      Fmt.fprintf ppf "%a,%a" Comonadic.print comonadic Monadic.print monadic

    let legacy =
      merge { comonadic = Comonadic.legacy; monadic = Monadic.legacy }

    let meet m1 m2 =
      let m1 = split m1 in
      let m2 = split m2 in
      let monadic = Monadic.meet m1.monadic m2.monadic in
      let comonadic = Comonadic.meet m1.comonadic m2.comonadic in
      merge { monadic; comonadic }

    let join m1 m2 =
      let m1 = split m1 in
      let m2 = split m2 in
      let monadic = Monadic.join m1.monadic m2.monadic in
      let comonadic = Comonadic.join m1.comonadic m2.comonadic in
      merge { monadic; comonadic }

    module Option = struct
      type some = t

      type t =
        ( Areality.Const.t option,
          Linearity.Const.t option,
          Uniqueness.Const.t option,
          Portability.Const.t option,
          Contention.Const.t option,
          Forkable.Const.t option,
          Yielding.Const.t option,
          Statefulness.Const.t option,
          Visibility.Const.t option,
          Staticity.Const.t option )
        modes

      let none =
        { areality = None;
          uniqueness = None;
          linearity = None;
          portability = None;
          contention = None;
          forkable = None;
          yielding = None;
          statefulness = None;
          visibility = None;
          staticity = None
        }

      let value opt ~default =
        let areality = Option.value opt.areality ~default:default.areality in
        let uniqueness =
          Option.value opt.uniqueness ~default:default.uniqueness
        in
        let linearity = Option.value opt.linearity ~default:default.linearity in
        let portability =
          Option.value opt.portability ~default:default.portability
        in
        let contention =
          Option.value opt.contention ~default:default.contention
        in
        let yielding = Option.value opt.yielding ~default:default.yielding in
        let forkable = Option.value opt.forkable ~default:default.forkable in
        let statefulness =
          Option.value opt.statefulness ~default:default.statefulness
        in
        let visibility =
          Option.value opt.visibility ~default:default.visibility
        in
        let staticity = Option.value opt.staticity ~default:default.staticity in
        { areality;
          uniqueness;
          linearity;
          portability;
          contention;
          forkable;
          yielding;
          statefulness;
          visibility;
          staticity
        }

      let proj (type a) (ax : a Axis.t) (t : t) : a option =
        match ax with
        | Monadic ax -> (
          match ax with
          | Uniqueness -> t.uniqueness
          | Contention -> t.contention
          | Visibility -> t.visibility
          | Staticity -> t.staticity)
        | Comonadic ax -> (
          match ax with
          | Areality -> t.areality
          | Linearity -> t.linearity
          | Portability -> t.portability
          | Forkable -> t.forkable
          | Yielding -> t.yielding
          | Statefulness -> t.statefulness)

      let set (type a) (ax : a Axis.t) (a : a option) (t : t) : t =
        match ax with
        | Monadic ax -> (
          match ax with
          | Uniqueness -> { t with uniqueness = a }
          | Contention -> { t with contention = a }
          | Visibility -> { t with visibility = a }
          | Staticity -> { t with staticity = a })
        | Comonadic ax -> (
          match ax with
          | Areality -> { t with areality = a }
          | Linearity -> { t with linearity = a }
          | Portability -> { t with portability = a }
          | Yielding -> { t with yielding = a }
          | Forkable -> { t with forkable = a }
          | Statefulness -> { t with statefulness = a })

      let print ppf
          { areality;
            uniqueness;
            linearity;
            portability;
            contention;
            forkable;
            yielding;
            statefulness;
            visibility;
            staticity
          } =
        let option_print print ppf = function
          | None -> Fmt.fprintf ppf "None"
          | Some a -> Fmt.fprintf ppf "Some %a" print a
        in
        Fmt.fprintf ppf "%a,%a,%a,%a,%a,%a,%a,%a,%a,%a"
          (option_print Areality.Const.print)
          areality
          (option_print Linearity.Const.print)
          linearity
          (option_print Uniqueness.Const.print)
          uniqueness
          (option_print Portability.Const.print)
          portability
          (option_print Contention.Const.print)
          contention
          (option_print Forkable.Const.print)
          forkable
          (option_print Yielding.Const.print)
          yielding
          (option_print Statefulness.Const.print)
          statefulness
          (option_print Visibility.Const.print)
          visibility
          (option_print Staticity.Const.print)
          staticity
    end

    let diff m1 m2 =
      let diff le a1 a2 = if le a1 a2 && le a2 a1 then None else Some a1 in
      let areality = diff Areality.Const.le m1.areality m2.areality in
      let linearity = diff Linearity.Const.le m1.linearity m2.linearity in
      let uniqueness = diff Uniqueness.Const.le m1.uniqueness m2.uniqueness in
      let portability =
        diff Portability.Const.le m1.portability m2.portability
      in
      let contention = diff Contention.Const.le m1.contention m2.contention in
      let forkable = diff Forkable.Const.le m1.forkable m2.forkable in
      let yielding = diff Yielding.Const.le m1.yielding m2.yielding in
      let statefulness =
        diff Statefulness.Const.le m1.statefulness m2.statefulness
      in
      let visibility = diff Visibility.Const.le m1.visibility m2.visibility in
      let staticity = diff Staticity.Const.le m1.staticity m2.staticity in
      { areality;
        linearity;
        uniqueness;
        portability;
        contention;
        forkable;
        yielding;
        statefulness;
        visibility;
        staticity
      }

    (** See [Alloc.close_over] for explanation. *)
    let close_over m =
      let { monadic; comonadic } = split m in
      Comonadic.join comonadic
        (C.monadic_to_comonadic_min
           (C.comonadic_with_obj Areality.Obj.obj)
           monadic)

    (** See [Alloc.partial_apply] for explanation. *)
    let partial_apply m =
      let { comonadic; _ } = split m in
      comonadic

    let print_axis : type a. a Axis.t -> Fmt.formatter -> a -> unit =
     fun ax ppf a ->
      let obj = proj_obj ax in
      C.print obj ppf a

    let le_axis : type a. a Axis.t -> a -> a -> bool =
     fun ax m1 m2 ->
      match ax with
      | Comonadic ax -> Comonadic.Per_axis.le ax m1 m2
      | Monadic ax -> Monadic.Per_axis.le ax m1 m2

    let min_axis : type a. a Axis.t -> a = function
      | Comonadic ax -> Comonadic.Per_axis.min ax
      | Monadic ax -> Monadic.Per_axis.min ax

    let max_axis : type a. a Axis.t -> a = function
      | Comonadic ax -> Comonadic.Per_axis.max ax
      | Monadic ax -> Monadic.Per_axis.max ax

    let is_max : type a. a Axis.t -> a -> bool =
     fun ax m -> le_axis ax (max_axis ax) m

    let is_min : type a. a Axis.t -> a -> bool =
     fun ax m -> le_axis ax m (min_axis ax)

    let split = split

    let merge = merge
  end

  let min = { comonadic = Comonadic.min; monadic = Monadic.min }

  let max = { comonadic = Comonadic.max; monadic = Monadic.max }

  include Magic_allow_disallow (struct
    type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r

    let allow_left { monadic; comonadic } =
      let monadic = Monadic.allow_left monadic in
      let comonadic = Comonadic.allow_left comonadic in
      { monadic; comonadic }

    let allow_right { monadic; comonadic } =
      let monadic = Monadic.allow_right monadic in
      let comonadic = Comonadic.allow_right comonadic in
      { monadic; comonadic }

    let disallow_left { monadic; comonadic } =
      let monadic = Monadic.disallow_left monadic in
      let comonadic = Comonadic.disallow_left comonadic in
      { monadic; comonadic }

    let disallow_right { monadic; comonadic } =
      let monadic = Monadic.disallow_right monadic in
      let comonadic = Comonadic.disallow_right comonadic in
      { monadic; comonadic }
  end)

  let newvar () =
    let comonadic = Comonadic.newvar () in
    let monadic = Monadic.newvar () in
    { comonadic; monadic }

  let newvar_above { comonadic; monadic } =
    let comonadic, b1 = Comonadic.newvar_above comonadic in
    let monadic, b2 = Monadic.newvar_above monadic in
    { monadic; comonadic }, b1 || b2

  let newvar_below { comonadic; monadic } =
    let comonadic, b1 = Comonadic.newvar_below comonadic in
    let monadic, b2 = Monadic.newvar_below monadic in
    { monadic; comonadic }, b1 || b2

  type atom = Atom : 'a Axis.t * 'a -> atom

  type error =
    | Monadic of Monadic.error
    | Comonadic of Comonadic.error

  type equate_error = equate_step * error

  type simple_error =
    | Error : 'a Axis.t * 'a Mode_intf.simple_error -> simple_error

  let to_simple_error = function
    | Monadic e ->
      let (Error (ax, e)) = Monadic.to_simple_error e in
      Error (Monadic ax, e)
    | Comonadic e ->
      let (Error (ax, e)) = Comonadic.to_simple_error e in
      Error (Comonadic ax, e)

  let print_error pp = function
    | Monadic e -> Monadic.print_error pp e
    | Comonadic e -> Comonadic.print_error pp e

  let submode_log ?pp { monadic = monadic1; comonadic = comonadic1 }
      { monadic = monadic2; comonadic = comonadic2 } ~log : (_, error) result =
    (* comonadic before monadic, so that locality errors dominate
       (error message backward compatibility) *)
    match Comonadic.submode_log ?pp comonadic1 comonadic2 ~log with
    | Error e -> Error (Comonadic e)
    | Ok () -> (
      match Monadic.submode_log ?pp monadic1 monadic2 ~log with
      | Error e -> Error (Monadic e)
      | Ok () -> Ok ())

  let submode ?pp a b = try_with_log (submode_log ?pp a b)

  let submode_err pp a b =
    Comonadic.submode_err pp a.comonadic b.comonadic;
    Monadic.submode_err pp a.monadic b.monadic

  let equate a b = try_with_log (equate_from_submode (submode_log ?pp:None) a b)

  let submode_exn ?pp m1 m2 =
    match submode ?pp m1 m2 with
    | Ok () -> ()
    | Error _ -> invalid_arg "submode_exn"

  let equate_exn m1 m2 =
    match equate m1 m2 with Ok () -> () | Error _ -> invalid_arg "equate_exn"

  let legacy =
    let comonadic = Comonadic.legacy in
    let monadic = Monadic.legacy in
    { comonadic; monadic }

  let proj_monadic ax { monadic; _ } = Monadic.proj ax monadic

  let proj_comonadic ax { comonadic; _ } = Comonadic.proj ax comonadic

  let max_with_comonadic ax m =
    let comonadic = Comonadic.max_with ax m in
    let monadic = Monadic.max |> Monadic.disallow_left |> Monadic.allow_right in
    { comonadic; monadic }

  let min_with_comonadic ax m =
    let comonadic = Comonadic.min_with ax m in
    let monadic = Monadic.min |> Monadic.disallow_right |> Monadic.allow_left in
    { comonadic; monadic }

  let min_with_monadic ax m =
    let monadic = Monadic.min_with ax m in
    let comonadic =
      Comonadic.min |> Comonadic.disallow_right |> Comonadic.allow_left
    in
    { comonadic; monadic }

  let join_const_with ax c { monadic; comonadic } =
    let monadic = Monadic.join_const_with ax c monadic in
    { monadic; comonadic }

  let meet_const_with ax c { monadic; comonadic } =
    let comonadic = Comonadic.meet_const_with ax c comonadic in
    { comonadic; monadic }

  let join l =
    let como, mo =
      List.fold_left
        (fun (como, mo) { comonadic; monadic } ->
          comonadic :: como, monadic :: mo)
        ([], []) l
    in
    let comonadic = Comonadic.join como in
    let monadic = Monadic.join mo in
    { comonadic; monadic }

  let meet l =
    let como, mo =
      List.fold_left
        (fun (como, mo) { comonadic; monadic } ->
          comonadic :: como, monadic :: mo)
        ([], []) l
    in
    let comonadic = Comonadic.meet como in
    let monadic = Monadic.meet mo in
    { comonadic; monadic }

  let comonadic_to_monadic_min ?hint m =
    S.apply ?hint Monadic.Obj.obj (Comonadic_to_monadic_max Comonadic.Obj.obj)
      (Comonadic.disallow_left m)

  let monadic_to_comonadic_min m =
    S.apply Comonadic.Obj.obj Monadic_to_comonadic_min (Monadic.disallow_left m)

  let monadic_to_comonadic_max m =
    S.apply Comonadic.Obj.obj Monadic_to_comonadic_max
      (Monadic.disallow_right m)

  let meet_const c { comonadic; monadic } =
    let comonadic = Comonadic.meet_const c comonadic in
    { monadic; comonadic }

  let join_const c { comonadic; monadic } =
    let monadic = Monadic.join_const c monadic in
    { monadic; comonadic }

  let zap_to_ceil { comonadic; monadic } =
    let monadic = Monadic.zap_to_ceil monadic in
    let comonadic = Comonadic.zap_to_ceil comonadic in
    merge { monadic; comonadic }

  let zap_to_floor { comonadic; monadic } =
    let monadic = Monadic.zap_to_floor monadic in
    let comonadic = Comonadic.zap_to_floor comonadic in
    merge { monadic; comonadic }

  let zap_to_legacy { comonadic; monadic } =
    let monadic = Monadic.zap_to_legacy monadic in
    let comonadic = Comonadic.zap_to_legacy comonadic in
    merge { monadic; comonadic }

  (** This is about partially applying [A -> B -> C] to [A] and getting
      [B -> C]. [comonadic] and [monadic] constutute the mode of [A], and we
      need to give the lower bound mode of [B -> C]. *)
  let close_over { comonadic; monadic } =
    let comonadic = Comonadic.disallow_right comonadic in
    (* The comonadic of the returned function is constrained by the monadic of the closed argument via the dualizing morphism. *)
    let comonadic1 = monadic_to_comonadic_min monadic in
    (* It's also constrained by the comonadic of the closed argument. *)
    let comonadic = Comonadic.join [comonadic; comonadic1] in
    (* The closure will access [A] at the specified monadic modes, and thus the
       monadic mode of the closure itself is not constrained by it. *)
    let monadic = Monadic.disallow_right Monadic.min in
    { comonadic; monadic }

  (** Similar to above, but we are given the mode of [A -> B -> C], and need to
      give the lower bound mode of [B -> C]. *)
  let partial_apply { comonadic; _ } =
    (* The closure will invoke the original function at the specified monadic
       modes, and thus the monadic mode of the closure itself is not constrained by
       it. *)
    let monadic = Monadic.disallow_right Monadic.min in
    let comonadic = Comonadic.disallow_right comonadic in
    { comonadic; monadic }

  module List = struct
    type nonrec 'd t = 'd t list

    include Magic_allow_disallow (struct
      type (_, _, 'd) sided = 'd t constraint 'd = 'l * 'r

      let allow_left l = List.map allow_left l

      let allow_right l = List.map allow_right l

      let disallow_left l = List.map disallow_left l

      let disallow_right l = List.map disallow_right l
    end)
  end
end
[@@inline]

module Value = Value_with (Regionality)
module Alloc = Value_with (Locality)

module Const = struct
  let alloc_as_value
      ({ areality;
         linearity;
         portability;
         uniqueness;
         contention;
         forkable;
         yielding;
         statefulness;
         visibility;
         staticity
       } :
        Alloc.Const.t) : Value.Const.t =
    let areality = C.locality_as_regionality areality in
    { areality;
      linearity;
      portability;
      uniqueness;
      contention;
      forkable;
      yielding;
      statefulness;
      visibility;
      staticity
    }

  module Axis = struct
    let is_areality (type a) :
        a Alloc.Axis.t ->
        ((a, Locality.Const.t) Misc.eq, a Value.Axis.t) Either.t = function
      | Comonadic Areality -> Left Refl
      | Comonadic Linearity -> Right (Comonadic Linearity)
      | Comonadic Portability -> Right (Comonadic Portability)
      | Comonadic Forkable -> Right (Comonadic Forkable)
      | Comonadic Yielding -> Right (Comonadic Yielding)
      | Comonadic Statefulness -> Right (Comonadic Statefulness)
      | Monadic Uniqueness -> Right (Monadic Uniqueness)
      | Monadic Contention -> Right (Monadic Contention)
      | Monadic Visibility -> Right (Monadic Visibility)
      | Monadic Staticity -> Right (Monadic Staticity)

    let alloc_as_value : Alloc.Axis.packed -> Value.Axis.packed =
     fun (P ax) ->
      match is_areality ax with
      | Left Refl -> P (Comonadic Areality)
      | Right ax -> P ax
  end

  let locality_as_regionality = C.locality_as_regionality
end

(* CR-someday zqian: all the function that converts between [Alloc] and [Value] should
   operate on [Unhint] so they can be composed and assigned hint as a whole. *)

let comonadic_locality_as_regionality comonadic =
  S.Unhint.apply Value.Comonadic.Obj.obj (Map_comonadic Locality_as_regionality)
    comonadic

let comonadic_regional_to_local comonadic =
  S.Unhint.apply Alloc.Comonadic.Obj.obj (Map_comonadic Regional_to_local)
    comonadic

let alloc_as_value_unhint m =
  let { comonadic; monadic } = m in
  let comonadic = comonadic_locality_as_regionality comonadic in
  { comonadic; monadic }

let alloc_as_value m =
  m |> Alloc.unhint |> alloc_as_value_unhint |> Value.hint ~monadic:Skip

let alloc_to_value_l2r_unhint m =
  let { comonadic; monadic } = m in
  let comonadic =
    S.Unhint.apply Value.Comonadic.Obj.obj (Map_comonadic Local_to_regional)
      comonadic
  in
  { comonadic; monadic }

let alloc_to_value_l2r m =
  m |> Alloc.disallow_right |> Alloc.unhint |> alloc_to_value_l2r_unhint
  |> Value.hint ~monadic:Skip

let value_to_alloc_r2g_unhint m =
  let { comonadic; monadic } = m in
  let comonadic =
    S.Unhint.apply Alloc.Comonadic.Obj.obj (Map_comonadic Regional_to_global)
      comonadic
  in
  { comonadic; monadic }

let value_to_alloc_r2g m =
  m |> Value.unhint |> value_to_alloc_r2g_unhint |> Alloc.hint ~monadic:Skip

let value_r2g ?hint m =
  Value.wrap ~monadic:Skip ?comonadic:hint
    (fun m -> m |> value_to_alloc_r2g_unhint |> alloc_as_value_unhint)
    m

let value_to_alloc_r2l_unhint m =
  let { comonadic; monadic } = m in
  let comonadic = comonadic_regional_to_local comonadic in
  { comonadic; monadic }

let value_to_alloc_r2l m =
  m |> Value.unhint |> value_to_alloc_r2l_unhint |> Alloc.hint ~monadic:Skip

module Modality = struct
  (* Inferred modalities

      Similar to constant modalities, an inferred modality maps the mode of a
      record/structure to the mode of a value therein. An inferred modality [f]
      is inferred from the structure/record mode [mm] and the value mode [m]. It
      will only be applied on some [x >= mm]: That is, it will only be applied
      on the original module.

      It should satisfy the following conditions:

      Zapping: [f] should be of the form [join_c] for monadic axes, or [meet_c]
      for comonadic axes.

      Soundness: You should not get a value from a record/structure at a mode
      strictly stronger than how it was put in. That is, for any [x >= mm], [f x
      >= m].

      Completeness: Ideally we also want [f mm <= m].

      Monadic axes

      Soundness condition says [join_c x >= m] for any [x >= mm]. Equivalently,
      [join_c mm >= m]. By adjunction, [c >= subtract_mm m]. We take the lower
      bound [c := subtract_mm m]. Note that this is equivalent to taking [c := m
      >= subtract_mm m]. Proof:

      - [join_m x >= join_(subtract_mm m) x] is trivial since [m >= subtract_mm
        m].
      - [join_m x <= join_(subtract_mm m) x], or equivalently [m <=
      join_(subtract_mm m) x], or equivalently [subtract_x m <= subtract_mm m],
      which is trivial since [x >= mm].

      Taking [c := subtract_mm m] is better for zapping since it's lower and
      thus closer to identity modality. Taking [c := m] is easier for [apply]
      and [sub].

      Comonadic axes

      Soundness condition says [meet_c x >= m] for any [x >= mm]. Equivalently,
      [meet_c mm >= m]. By def. of [meet], we have both [c >= m] and [mm >= m].
      The latter is guaranteed by the user of [infer]. We guarantee the former
      by taking [c := imply_mm m >= m]. One might worry that this is too relaxed
      and will be "less complete" than taking [c := m]; however, note that
      [imply_mm m <= imply_mm m] and thus by adjunction [meet_(imply_mm m) mm <=
      m], which means the chosen [c] is complete.

      Taking [c := m] is easier for [apply] and [sub]. Taking [c := imply_mm m]
      is better for zapping since it's higher and thus closer to identity
      modality. However, note that we DON'T have [meet_m x = meet_(imply_mm m)
      x], which means [apply/sub] and [zap] might behave in a confusing (albeit
      sound) manner.

      CR zqian: once we support binary mode solver, [c := imply_mm m] will be
      used uniformly by [apply] [sub] and [zap].
  *)

  module Monadic = struct
    module Mode = Value.Monadic

    type 'a axis = 'a Mode.Axis.t

    module Atom = struct
      type 'a t = Join_const of 'a [@@unboxed]

      let is_id ax (Join_const c) = Mode.Const.Per_axis.(le ax c (min ax))

      let is_constant ax (Join_const c) = Mode.Const.Per_axis.(le ax (max ax) c)
    end

    type error = Error : 'a axis * 'a Atom.t simple_error -> error

    module Const = struct
      type t = Join_const of Mode.Const.t [@@unboxed]

      let id = Join_const Mode.Const.min

      let is_id t = t = id

      let max = Join_const Mode.Const.max

      let sub left right : (_, error) Result.t =
        match left, right with
        | Join_const c1, Join_const c2 ->
          if Mode.Const.le c1 c2
          then Ok ()
          else
            let (Error (ax, { left; right })) = Mode.axis_of_error c1 c2 in
            Error
              (Error (ax, { left = Join_const left; right = Join_const right }))

      let concat ~then_ t =
        match then_, t with
        | Join_const c1, Join_const c2 -> Join_const (Mode.Const.join c1 c2)

      let apply : type l r.
          ?hint:(l * r) neg Hint.morph -> t -> (l * r) Mode.t -> (l * r) Mode.t
          =
       fun ?(hint = Hint.Unknown) t x ->
        match t with Join_const c -> Mode.join_const ~hint c x

      let proj ax (Join_const c) : _ Atom.t = Join_const (Axis.proj ax c)

      let set ax (Join_const a : _ Atom.t) (Join_const c) =
        Join_const (Axis.set ax a c)

      let print ppf = function
        | Join_const c -> Fmt.fprintf ppf "join_const(%a)" Mode.Const.print c
    end

    type t =
      | Const of Const.t
      | Diff of Mode.lr * Mode.lr  (** See "Inferred modalities" comments *)
      | Undefined

    let sub_log left right ~log : (unit, error) Result.t =
      match left, right with
      | Const c1, Const c2 -> Const.sub c1 c2
      | Diff (mm, m), Const (Join_const c) -> (
        (* Check that for any x >= mm, join(x, m) <= join(x, c), which (by
           definition of join) is equivalent to m <= join(x, c). This has to
           hold for all x >= mm, so we check m <= join(mm, c). *)
        match Mode.submode_log m (Mode.join_const c mm) ~log with
        | Ok () -> Ok ()
        | Error err ->
          let (Error (ax, { left; _ })) = Mode.to_simple_error err in
          Error
            (Error
               ( ax,
                 { left = Join_const left; right = Join_const (Axis.proj ax c) }
               )))
      | Diff (_, _m1), Diff (_, _m2) ->
        (* [m1] is a left mode so it cannot appear on the right. So we can't do
           a proper check. However, this branch is only hit by
           [wrap_constraint_with_shape], in which case LHS and RHS should be
           physically equal. *)
        assert (left == right);
        Ok ()
      | Const _, Diff _ ->
        Misc.fatal_error
          "inferred modality Diff should not be on the RHS of sub."
      | Undefined, _ | _, Undefined ->
        Misc.fatal_error "modality Undefined should not be in sub."

    let apply : type r.
        ?hint:(allowed * r) neg Hint.morph ->
        t ->
        (allowed * r) Mode.t ->
        Mode.l =
     fun ?hint t x ->
      match t with
      | Const c -> Const.apply ?hint c x |> Mode.disallow_right
      | Undefined ->
        Misc.fatal_error "modality Undefined should not be applied."
      | Diff (_, m) -> Mode.join [Mode.allow_right m; x]

    let print ppf = function
      | Const c -> Const.print ppf c
      | Undefined -> Fmt.fprintf ppf "undefined"
      | Diff _ -> Fmt.fprintf ppf "diff"

    (* All zapping functions mutate [mm] and [m] to the degree that's sufficient
       to fix [subtract_mm m], and return it. [subtract] is antitone for [mm]
       and monotone for [m]. *)

    let zap_to_floor = function
      | Const c -> c
      | Undefined -> Misc.fatal_error "modality Undefined should not be zapped."
      | Diff (mm, m) ->
        (* Ideally we will take [c = subtract_mm m] and zap it to floor.
           However, [subtract] requires [mm] to be constant. We get the ceil of
           [mm] to construct the floor of [c]. *)
        let cc = Mode.Guts.get_ceil mm in
        let c = Mode.subtract_const cc m in
        let c = Mode.zap_to_floor c in
        (* Note that we did not mutate [mm] but simply took its ceil, which
           might be mutated later. To satisfy the coherence condition (see the
           comment in the mli), we want to:

           - make it impossible that [subtract_mm m < c], which is trivial since
           [mm <= cc] and thus [subtract_mm m >= subtract_cc m = c].
           - make it impossible that [subtract_mm m > c], which is to ensure
           [subtract_mm m <= c], equivalently [m <= join_mm c], which is
           achieved by the following [submode].
        *)
        Mode.submode_exn m (Mode.join_const c mm);
        Const.Join_const c

    let zap_to_id = zap_to_floor

    let to_const_opt = function
      | Const c -> Some c
      | Undefined ->
        Misc.fatal_error "modality Undefined should not be looked at"
      | Diff _ -> None

    let of_const c = Const c

    let infer ~md_mode ~mode = Diff (md_mode, mode)

    let max = Const Const.max
  end

  module Comonadic = struct
    module Mode = Value.Comonadic

    type 'a axis = 'a Mode.Axis.t

    module Atom = struct
      type 'a t = Meet_const of 'a [@@unboxed]

      let is_id ax (Meet_const c) = Mode.Const.Per_axis.(le ax (max ax) c)

      let is_constant ax (Meet_const c) = Mode.Const.Per_axis.(le ax c (min ax))
    end

    type error = Error : 'a axis * 'a Atom.t simple_error -> error

    module Const = struct
      type t = Meet_const of Mode.Const.t [@@unboxed]

      let id = Meet_const Mode.Const.max

      let is_id t = t = id

      let max = Meet_const Mode.Const.max

      let sub left right : (_, error) Result.t =
        match left, right with
        | Meet_const c1, Meet_const c2 ->
          if Mode.Const.le c1 c2
          then Ok ()
          else
            let (Error (ax, { left; right })) = Mode.axis_of_error c1 c2 in
            Error
              (Error (ax, { left = Meet_const left; right = Meet_const right }))

      let concat ~then_ t =
        match then_, t with
        | Meet_const c1, Meet_const c2 -> Meet_const (Mode.Const.meet c1 c2)

      let apply : type l r.
          ?hint:(l * r) pos Hint.morph -> t -> (l * r) Mode.t -> (l * r) Mode.t
          =
       fun ?(hint = Hint.Unknown) t x ->
        match t with Meet_const c -> Mode.meet_const ~hint c x

      let proj ax (Meet_const c) : _ Atom.t = Meet_const (Axis.proj ax c)

      let set ax (Meet_const a : _ Atom.t) (Meet_const c) =
        Meet_const (Axis.set ax a c)

      let print ppf = function
        | Meet_const c -> Fmt.fprintf ppf "meet_const(%a)" Mode.Const.print c
    end

    type t =
      | Const of Const.t
      | Undefined
      | Exactly of Mode.lr * Mode.lr  (** See "Inferred modalities" comments *)

    let sub_log left right ~log : (unit, error) Result.t =
      match left, right with
      | Const c1, Const c2 -> Const.sub c1 c2
      | Exactly (_mm, m), Const (Meet_const c) -> (
        (* Check for all [x >= mm], [meet_(imply_mm m) x <= meet_c x], or
           equivalently [meet_(imply_mm m) x <= c], or equivalently [meet_(imply_mm
           m) max <= c], or equivalently [imply_mm m <= c]. We can't check this
           without binary mode solver.

           So instead we check [meet_m x <= meet_c x] (See "Inferred modalities"
           comments), which amounts to [m <= c]. *)
        match Mode.submode_log m (Mode.of_const c) ~log with
        | Ok () -> Ok ()
        | Error err ->
          let (Error (ax, { left; _ })) = Mode.to_simple_error err in
          Error
            (Error
               ( ax,
                 { left = Meet_const left; right = Meet_const (Axis.proj ax c) }
               )))
      | Exactly (_, _m1), Exactly (_, _m2) ->
        (* [m1] is a left mode, so there is no good way to check.
           However, this branch only hit by [wrap_constraint_with_shape],
           in which case LHS and RHS should be physically equal. *)
        assert (left == right);
        Ok ()
      | Const _, Exactly _ ->
        Misc.fatal_error
          "inferred modaltiy Exactly should not be on the RHS of sub."
      | Undefined, _ | _, Undefined ->
        Misc.fatal_error "modality Undefined should not be in sub."

    let apply : type r.
        ?hint:(allowed * r) pos Hint.morph ->
        t ->
        (allowed * r) Mode.t ->
        Mode.l =
     fun ?hint t x ->
      match t with
      | Const c -> Const.apply ?hint c x |> Mode.disallow_right
      | Undefined ->
        Misc.fatal_error "modality Undefined should not be applied."
      | Exactly (_mm, m) ->
        (* Ideally want to return [meet_(imply_mm m) x], which we can't do
           without binary mode solver, so instead we return [meet_m x] (See
           "Inferred modalities" comments), which because of [x >= mm >= m] is
           equal to [m]. *)
        Mode.disallow_right m

    let print ppf = function
      | Const c -> Const.print ppf c
      | Undefined -> Fmt.fprintf ppf "undefined"
      | Exactly _ -> Fmt.fprintf ppf "exactly"

    let infer ~md_mode ~mode = Exactly (md_mode, mode)

    let max = Const Const.max

    (* All zapping functions mutate [mm] and [m] to the degree that's sufficient
       to fix [imply_mm m], and return it. [imply] is antitone for [mm] and
       monotone for [m]. *)

    let zap_to_ceil = function
      | Const c -> c
      | Undefined -> Misc.fatal_error "modality Undefined should not be zapped."
      | Exactly (mm, m) ->
        (* Ideally we will take [c = imply_mm m] and zap it to ceil. However,
           [imply] requires [mm] to be constant. We get the floor of [mm] to
           construct the ceil of [c]. *)
        let cc = Mode.Guts.get_floor mm in
        let c = Mode.imply_const cc m in
        let c = Mode.zap_to_ceil c in
        (* Note that we did not mutate [mm] but simply took its floor, which
           might be mutated later. To satisfy the coherence condition (see the
           comment in the mli), we want to:

           - make it impossible that [imply_mm m > c], which is trivial since
           [mm >= cc] and thus [imply_mm m <= imply_cc m = c].
           - make it impossible that [imply_mm m < c], which is to ensure
           [imply_mm m >= c], equivalently [m >= meet_mm c], which is achieved
           by the following [submode].
        *)
        Mode.submode_exn (Mode.meet_const c mm) m;
        Const.Meet_const c

    let zap_to_id = zap_to_ceil

    let zap_to_floor = function
      | Const c -> c
      | Undefined -> Misc.fatal_error "modality Undefined should not be zapped."
      | Exactly (mm, m) ->
        (* The following zaps [mm] to ceil, which might conflict with future
           mode constraints on [mm]. We find constraining [mm] to [legacy] a
           good workaround. *)
        (* CR zqian: Find a better solution *)
        Mode.submode mm Mode.legacy |> ignore;
        let m = Mode.zap_to_floor m in
        let mm = Mode.zap_to_ceil mm in
        let c = Mode.Const.imply mm m in
        Const.Meet_const c

    let to_const_opt = function
      | Const c -> Some c
      | Undefined ->
        Misc.fatal_error "modality Undefined should not be looked at"
      | Exactly _ -> None

    let of_const c = Const c
  end

  module Axis = struct
    type 'a t =
      | Monadic : 'a Monadic.axis -> 'a Monadic.Atom.t t
      | Comonadic : 'a Comonadic.axis -> 'a Comonadic.Atom.t t

    type packed = P : 'a t -> packed

    let of_value : Value.Axis.packed -> packed = function
      | P (Monadic ax) -> P (Monadic ax)
      | P (Comonadic ax) -> P (Comonadic ax)

    let to_value : packed -> Value.Axis.packed = function
      | P (Monadic ax) -> P (Monadic ax)
      | P (Comonadic ax) -> P (Comonadic ax)
  end

  type atom = Atom : 'a Axis.t * 'a -> atom

  module Per_axis = struct
    open struct
      module Monadic = Monadic.Atom
      module Comonadic = Comonadic.Atom
    end

    let is_id : type a. a Axis.t -> a -> bool =
     fun ax t ->
      match ax with
      | Monadic ax -> Monadic.is_id ax t
      | Comonadic ax -> Comonadic.is_id ax t

    let is_constant : type a. a Axis.t -> a -> bool =
     fun ax t ->
      match ax with
      | Monadic ax -> Monadic.is_constant ax t
      | Comonadic ax -> Comonadic.is_constant ax t

    let print (type a) (ax : a Axis.t) ppf (t : a) =
      match ax, t with
      | Comonadic ax, Meet_const t ->
        Value.Comonadic.Const.Per_axis.print ax ppf t
      | Monadic ax, Join_const t -> Value.Monadic.Const.Per_axis.print ax ppf t
  end

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

  type equate_error = equate_step * error

  module Const = struct
    module Monadic = Monadic.Const
    module Comonadic = Comonadic.Const

    type t = (Monadic.t, Comonadic.t) monadic_comonadic

    let id = { monadic = Monadic.id; comonadic = Comonadic.id }

    let is_id { monadic; comonadic } =
      Monadic.is_id monadic && Comonadic.is_id comonadic

    let sub t1 t2 : (unit, error) Result.t =
      match Monadic.sub t1.monadic t2.monadic with
      | Error (Error (ax, e)) -> Error (Error (Monadic ax, e))
      | Ok () -> (
        match Comonadic.sub t1.comonadic t2.comonadic with
        | Ok () -> Ok ()
        | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)))

    let equate = equate_from_submode' sub

    let apply ?hint t { monadic; comonadic } =
      let monadic =
        Monadic.apply
          ?hint:(Option.map (fun { monadic; _ } -> monadic) hint)
          t.monadic monadic
      in
      let comonadic =
        Comonadic.apply
          ?hint:(Option.map (fun { comonadic; _ } -> comonadic) hint)
          t.comonadic comonadic
      in
      { monadic; comonadic }

    let concat ~then_ t =
      let monadic = Monadic.concat ~then_:then_.monadic t.monadic in
      let comonadic = Comonadic.concat ~then_:then_.comonadic t.comonadic in
      { monadic; comonadic }

    let proj (type a) (ax : a Axis.t) { monadic; comonadic } : a =
      match ax with
      | Monadic ax -> Monadic.proj ax monadic
      | Comonadic ax -> Comonadic.proj ax comonadic

    let set (type a) (ax : a Axis.t) (a : a) { monadic; comonadic } : t =
      match ax with
      | Monadic ax -> { monadic = Monadic.set ax a monadic; comonadic }
      | Comonadic ax -> { monadic; comonadic = Comonadic.set ax a comonadic }

    let diff t1 t2 =
      List.filter_map
        (fun ax : atom option ->
          let (P ax) = Axis.of_value ax in
          let a1 = proj ax t1 in
          let a2 = proj ax t2 in
          if a1 = a2 then None else Some (Atom (ax, a2)))
        Value.Axis.all

    let print ppf { monadic; comonadic } =
      Fmt.fprintf ppf "%a;%a" Monadic.print monadic Comonadic.print comonadic
  end

  type t = (Monadic.t, Comonadic.t) monadic_comonadic

  let undefined : t = { monadic = Undefined; comonadic = Undefined }

  let is_undefined : t -> bool = function
    | { monadic = Undefined; comonadic = Undefined } -> true
    | _ -> false
  [@@ocaml.warning "-4"]

  let apply ?hint t { monadic; comonadic } =
    let monadic =
      Monadic.apply
        ?hint:(Option.map (fun { monadic; _ } -> monadic) hint)
        t.monadic monadic
    in
    let comonadic =
      Comonadic.apply
        ?hint:(Option.map (fun { comonadic; _ } -> comonadic) hint)
        t.comonadic comonadic
    in
    { monadic; comonadic }

  let sub_log t1 t2 ~log : (unit, error) Result.t =
    match Monadic.sub_log t1.monadic t2.monadic ~log with
    | Error (Error (ax, e)) -> Error (Error (Monadic ax, e))
    | Ok () -> (
      match Comonadic.sub_log t1.comonadic t2.comonadic ~log with
      | Ok () -> Ok ()
      | Error (Error (ax, e)) -> Error (Error (Comonadic ax, e)))

  let sub l r = try_with_log (sub_log l r)

  let equate m1 m2 = try_with_log (equate_from_submode sub_log m1 m2)

  let print ppf ({ monadic; comonadic } : t) =
    Fmt.fprintf ppf "%a;%a" Monadic.print monadic Comonadic.print comonadic

  let infer ~md_mode ~mode : t =
    let comonadic =
      Comonadic.infer ~md_mode:md_mode.comonadic ~mode:mode.comonadic
    in
    let monadic = Monadic.infer ~md_mode:md_mode.monadic ~mode:mode.monadic in
    { monadic; comonadic }

  let zap_to_id t =
    let { monadic; comonadic } = t in
    let comonadic = Comonadic.zap_to_id comonadic in
    let monadic = Monadic.zap_to_id monadic in
    { monadic; comonadic }

  let zap_to_floor t =
    let { monadic; comonadic } = t in
    let comonadic = Comonadic.zap_to_floor comonadic in
    let monadic = Monadic.zap_to_floor monadic in
    { monadic; comonadic }

  let to_const_opt t =
    let { monadic; comonadic } = t in
    Option.bind (Comonadic.to_const_opt comonadic) (fun comonadic ->
        Option.bind (Monadic.to_const_opt monadic) (fun monadic ->
            Some { monadic; comonadic }))

  let to_const_exn t = t |> to_const_opt |> Option.get

  let of_const { monadic; comonadic } =
    let comonadic = Comonadic.of_const comonadic in
    let monadic = Monadic.of_const monadic in
    { monadic; comonadic }

  let max =
    let monadic = Monadic.max in
    let comonadic = Comonadic.max in
    { monadic; comonadic }
end

module Crossing = struct
  (* The mode crossing capability of a type [t] is characterized by a monotone
     function [f] from modes to some lattice [L], in the following way:

     To check [e : t @ m1<= m2], we should instead check [f m1 <= f m2] to
     allow more programs.

     For example, if [f] is the identity function, then [t] does not cross modes
     at all. If [f] maps to the unit lattice (containing only one element), [f
     m1 <= f m2] always succeeds, which means [t] crosses modes fully.

     In practice, during mode checking we usually have either [m1] or [m2], but
     not both. In order to perform mode crossing one-sided, we require [f] to
     have left adjoint [fl] and right adjoint [fr], which gives:

     [f m1 <= f m2] is equivalent to [fl (f m1) <= m2] is equivalent to [m1 <=
     fr (f m2)]

     Therefore, we can perform any of the following for mode crossing:
     - Apply [f] on both [m1] and [m2]
     - Apply [fl ∘ f] on [m1]
     - Apply [fr ∘ f] on [m2]

     Mode crossing forms a lattice: [f1 <= f2] iff [f1] allows more mode
     crossing than [f2]. Concretely:

     [f1 <= f2] iff, for any [m1, m2], if [f2 m1 <= f2 m2],
     then [f1 m1 <= f1 m2].
  *)

  module Monadic = struct
    module Modality = Modality.Monadic
    module Mode = Value.Monadic

    module Atom = struct
      type 'a t = Modality of 'a Modality.Atom.t [@@unboxed]

      (* By the ordering of crossings (see comments above) [join_c1 <= join_c2]
         iff the following holds:
         For all [a,b], if [join_c2 a <= join_c2 b](E1), then [join_c1 a <=
         join_c1 b](E2)

         Case analysis by the relation between [c1] and [c2]:
         - If [c1 >= c2], then [c1] can be written as [join c2 k] for some [k].
           Then apply [join k] to E1 and we get E2 (by monotonicity of join).
         - If [c1 <= c2], take [a := c2] and [b := c1]. E1 holds but E2 doesn't.
         - If neither, then we take [a := c2] and [b := meet a c1]. E1 is
           satisfied:
           [join_c2 a = c2 <= c2 = join_c2 (meet a c1) = join_c2 b]. But E2 is
           not satisfied:
           [join_c1 a = join c1 c2 </= c1 = join_c1 (meet c1 c2) = join_c1 b]

         Therefore, [join_c1 <= join_c2] iff [c1 >= c2]. *)

      let min ax =
        Modality (Join_const ((Mode.Const.Per_axis.max [@inlined hint]) ax))

      let max ax =
        Modality (Join_const ((Mode.Const.Per_axis.min [@inlined hint]) ax))

      let le ax (Modality (Join_const c1)) (Modality (Join_const c2)) =
        (Mode.Const.Per_axis.le [@inlined hint]) ax c2 c1

      let equal ax (Modality (Join_const c1)) (Modality (Join_const c2)) =
        (Mode.Const.Per_axis.equal [@inlined hint]) ax c2 c1

      let join ax (Modality (Join_const c1)) (Modality (Join_const c2)) =
        Modality
          (Join_const ((Mode.Const.Per_axis.meet [@inlined hint]) ax c1 c2))

      let meet ax (Modality (Join_const c1)) (Modality (Join_const c2)) =
        Modality (Join_const (Mode.Const.Per_axis.join ax c1 c2))

      let print ax ppf (Modality (Join_const c)) =
        Mode.Const.Per_axis.print ax ppf c
    end

    type t = Modality of Modality.Const.t [@@unboxed]

    let create ~uniqueness:(Atom.Modality (Join_const uniqueness))
        ~contention:(Atom.Modality (Join_const contention))
        ~visibility:(Atom.Modality (Join_const visibility))
        ~staticity:(Atom.Modality (Join_const staticity)) =
      Modality (Join_const { uniqueness; contention; visibility; staticity })

    let modality m (Modality t) = Modality (Modality.Const.concat ~then_:t m)

    let apply_left (Modality (Join_const c)) m =
      Mode.subtract_const_unhint c (Mode.join_const_unhint c m)

    let apply_right (Modality (Join_const c)) m =
      (* The right adjoint of join is a restriction of identity *)
      Mode.join_const_unhint c m

    let proj (type a) (ax : a Mode.Axis.t) (Modality (Join_const c)) : a Atom.t
        =
      Modality (Join_const ((Axis.proj [@inlined hint]) ax c))

    let set (type a) (ax : a Mode.Axis.t) (Modality (Join_const a) : a Atom.t)
        (Modality (Join_const c)) =
      Modality (Join_const ((Axis.set [@inlined hint]) ax a c))

    let le (Modality (Join_const c1)) (Modality (Join_const c2)) =
      Mode.Const.le c2 c1

    let equal (Modality (Join_const c1)) (Modality (Join_const c2)) =
      Mode.Const.equal c1 c2

    let max = Modality (Join_const Mode.Const.min)

    let min = Modality (Join_const Mode.Const.max)

    let join (Modality (Join_const c1)) (Modality (Join_const c2)) =
      Modality (Join_const (Mode.Const.meet c1 c2))

    let meet (Modality (Join_const c1)) (Modality (Join_const c2)) =
      Modality (Join_const (Mode.Const.join c1 c2))

    let print ppf (Modality m) =
      Fmt.fprintf ppf "Modality %a" Modality.Const.print m
  end

  module Comonadic = struct
    module Modality = Modality.Comonadic
    module Mode = Value.Comonadic

    module Atom = struct
      type 'a t = Modality of 'a Modality.Atom.t [@@unboxed]

      (* The ordering of crossing here is derived similarly to the monadic
         fragment. See comments there. *)

      let min ax =
        Modality (Meet_const ((Mode.Const.Per_axis.min [@inlined hint]) ax))

      let max ax =
        Modality (Meet_const ((Mode.Const.Per_axis.max [@inlined hint]) ax))

      let le ax (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
        (Mode.Const.Per_axis.le [@inlined hint]) ax c1 c2

      let equal ax (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
        (Mode.Const.Per_axis.equal [@inlined hint]) ax c1 c2

      let join ax (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
        Modality
          (Meet_const ((Mode.Const.Per_axis.join [@inlined hint]) ax c1 c2))

      let meet ax (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
        Modality (Meet_const (Mode.Const.Per_axis.meet ax c1 c2))

      let print ax ppf (Modality (Meet_const c)) =
        Mode.Const.Per_axis.print ax ppf c
    end

    type t = Modality of Modality.Const.t [@@unboxed]

    let create ~regionality:(Atom.Modality (Meet_const areality))
        ~linearity:(Atom.Modality (Meet_const linearity))
        ~portability:(Atom.Modality (Meet_const portability))
        ~forkable:(Atom.Modality (Meet_const forkable))
        ~yielding:(Atom.Modality (Meet_const yielding))
        ~statefulness:(Atom.Modality (Meet_const statefulness)) =
      Modality
        (Meet_const
           { areality;
             linearity;
             portability;
             statefulness;
             forkable;
             yielding
           })

    let always_constructed_at c = Modality (Meet_const c)

    let proj (type a) (ax : a Mode.Axis.t) (Modality (Meet_const c)) : a Atom.t
        =
      Modality (Meet_const ((Axis.proj [@inlined hint]) ax c))

    let set (type a) (ax : a Mode.Axis.t) (Modality (Meet_const a) : a Atom.t)
        (Modality (Meet_const c)) =
      Modality (Meet_const ((Axis.set [@inlined hint]) ax a c))

    let modality m (Modality t) = Modality (Modality.Const.concat ~then_:t m)

    let apply_left (Modality (Meet_const c)) m =
      (* The left adjoint of meet is a restriction of identity *)
      Mode.meet_const_unhint c m

    let apply_right (Modality (Meet_const c)) m =
      Mode.imply_const_unhint c (Mode.meet_const_unhint c m)

    let le (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
      Mode.Const.le c1 c2

    let equal (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
      Mode.Const.equal c1 c2

    let max = Modality (Meet_const Mode.Const.max)

    let min = Modality (Meet_const Mode.Const.min)

    let join (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
      Modality (Meet_const (Mode.Const.join c1 c2))

    let meet (Modality (Meet_const c1)) (Modality (Meet_const c2)) =
      Modality (Meet_const (Mode.Const.meet c1 c2))

    let print ppf (Modality m) =
      Fmt.fprintf ppf "Modality %a" Modality.Const.print m
  end

  module Axis = struct
    type 'a t =
      | Monadic : 'a Value.Monadic.Axis.t -> 'a Monadic.Atom.t t
      | Comonadic : 'a Value.Comonadic.Axis.t -> 'a Comonadic.Atom.t t

    type packed = P : 'a t -> packed

    let of_modality : Modality.Axis.packed -> packed = function
      | P (Monadic ax) -> P (Monadic ax)
      | P (Comonadic ax) -> P (Comonadic ax)

    let to_modality : packed -> Modality.Axis.packed = function
      | P (Monadic ax) -> P (Monadic ax)
      | P (Comonadic ax) -> P (Comonadic ax)

    let compare : type a b. a t -> b t -> int =
     fun ax1 ax2 ->
      match ax1, ax2 with
      | Monadic ax1, Monadic ax2 -> Axis.compare ax1 ax2
      | Monadic _, _ -> -1
      | _, Monadic _ -> 1
      | Comonadic ax1, Comonadic ax2 -> Axis.compare ax1 ax2

    let equal : type a b. a t -> b t -> (a, b) Misc.is_eq =
     fun ax1 ax2 ->
      match ax1, ax2 with
      | Monadic ax1, Monadic ax2 -> (
        match Axis.equal ax1 ax2 with Is_eq -> Is_eq | Is_not_eq -> Is_not_eq)
      | Comonadic ax1, Comonadic ax2 -> (
        match Axis.equal ax1 ax2 with Is_eq -> Is_eq | Is_not_eq -> Is_not_eq)
      | (Monadic _ | Comonadic _), _ -> Is_not_eq

    let print : type a. Fmt.formatter -> a t -> unit =
     fun ppf -> function
      | Monadic ax -> Axis.print ppf ax
      | Comonadic ax -> Axis.print ppf ax
  end

  module Per_axis = struct
    open Axis

    let le : type a. a t -> a -> a -> bool =
     fun[@inline available] ax a b ->
      match ax with
      | Monadic ax -> (Monadic.Atom.le [@inlined hint]) ax a b
      | Comonadic ax -> (Comonadic.Atom.le [@inlined hint]) ax a b

    let equal : type a. a t -> a -> a -> bool =
     fun[@inline available] ax a b ->
      match ax with
      | Monadic ax -> (Monadic.Atom.equal [@inlined hint]) ax a b
      | Comonadic ax -> (Comonadic.Atom.equal [@inlined hint]) ax a b

    let min : type a. a t -> a = function[@inline available]
      | Monadic ax -> (Monadic.Atom.min [@inlined hint]) ax
      | Comonadic ax -> (Comonadic.Atom.min [@inlined hint]) ax

    let max : type a. a t -> a = function[@inline available]
      | Monadic ax -> (Monadic.Atom.max [@inlined hint]) ax
      | Comonadic ax -> (Comonadic.Atom.max [@inlined hint]) ax

    let meet : type a. a t -> a -> a -> a =
     fun[@inline available] ax a b ->
      match ax with
      | Monadic ax -> (Monadic.Atom.meet [@inlined hint]) ax a b
      | Comonadic ax -> (Comonadic.Atom.meet [@inlined hint]) ax a b

    let join : type a. a t -> a -> a -> a =
     fun[@inline available] ax a b ->
      match ax with
      | Monadic ax -> (Monadic.Atom.join [@inlined hint]) ax a b
      | Comonadic ax -> (Comonadic.Atom.join [@inlined hint]) ax a b

    let print : type a. a t -> Fmt.formatter -> a -> unit = function
      | Monadic ax -> Monadic.Atom.print ax
      | Comonadic ax -> Comonadic.Atom.print ax

    let print_obj = Axis.print

    let compare_obj = Axis.compare

    let equal_obj = Axis.equal
  end

  type t = (Monadic.t, Comonadic.t) monadic_comonadic

  let modality m { monadic; comonadic } =
    let monadic = Monadic.modality m.monadic monadic in
    let comonadic = Comonadic.modality m.comonadic comonadic in
    { monadic; comonadic }

  let apply_left_unhint t { monadic; comonadic } =
    let monadic = Monadic.apply_left t.monadic monadic in
    let comonadic = Comonadic.apply_left t.comonadic comonadic in
    { monadic; comonadic }

  let apply_left t m =
    m |> Value.disallow_right |> Value.unhint |> apply_left_unhint t
    |> Value.hint ~monadic:Crossing ~comonadic:Crossing

  let apply_right_unhint t { monadic; comonadic } =
    let monadic = Monadic.apply_right t.monadic monadic in
    let comonadic = Comonadic.apply_right t.comonadic comonadic in
    { monadic; comonadic }

  let apply_right t m =
    m |> Value.disallow_left |> Value.unhint |> apply_right_unhint t
    |> Value.hint ~monadic:Crossing ~comonadic:Crossing

  (* Our mode crossing is for [Value] modes, but can be extended to [Alloc]
     modes via [alloc_as_value], defined as follows:

     Given a mode crossing [f] for [Value], and we are to check [Alloc] submoding
     [m1 <= m2], we will instead check
     [f (alloc_as_value m1) <= f (alloc_as_value m2)].

     By adjunction tricks, this is equivalent to
     - [ m1 <= regional_to_global ∘ fr ∘ f ∘ alloc_as_value m2 ]
     - [ regional_to_local ∘ fl ∘ f ∘ alloc_as_value m1 <= m2 ]
     where [regional_to_global] is the right adjoint of [alloc_as_value], and
     [regional_to_local] the left adjoint. *)

  let apply_left_alloc t m =
    m |> Alloc.unhint |> alloc_as_value_unhint |> apply_left_unhint t
    |> value_to_alloc_r2l_unhint
    |> Alloc.hint ~comonadic:Crossing ~monadic:Crossing

  let apply_right_alloc t m =
    m |> Alloc.unhint |> alloc_as_value_unhint |> apply_right_unhint t
    |> value_to_alloc_r2g_unhint
    |> Alloc.hint ~comonadic:Crossing ~monadic:Crossing

  let apply_left_right_alloc t m =
    let { monadic; comonadic } = Alloc.unhint m in
    let monadic = Monadic.apply_right t.monadic monadic in
    let comonadic =
      comonadic |> comonadic_locality_as_regionality
      |> Comonadic.apply_left t.comonadic
      |> comonadic_regional_to_local
      (* the left adjoint of [locality_as_regionality]*)
    in
    Alloc.hint ~monadic:Crossing ~comonadic:Crossing { monadic; comonadic }

  let le t1 t2 =
    Monadic.le t1.monadic t2.monadic && Comonadic.le t1.comonadic t2.comonadic

  let max = { monadic = Monadic.max; comonadic = Comonadic.max }

  let min = { monadic = Monadic.min; comonadic = Comonadic.min }

  let join t1 t2 =
    { monadic = Monadic.join t1.monadic t2.monadic;
      comonadic = Comonadic.join t1.comonadic t2.comonadic
    }

  let meet t1 t2 =
    { monadic = Monadic.meet t1.monadic t2.monadic;
      comonadic = Comonadic.meet t1.comonadic t2.comonadic
    }

  let equal t1 t2 = le t1 t2 && le t2 t1

  let[@inline available] proj (type a) (ax : a Axis.t) { monadic; comonadic } :
      a =
    match ax with
    | Monadic ax -> (Monadic.proj [@inlined hint]) ax monadic
    | Comonadic ax -> (Comonadic.proj [@inlined hint]) ax comonadic

  let[@inline available] set (type a) (ax : a Axis.t) (a : a)
      { monadic; comonadic } : t =
    match ax with
    | Monadic ax ->
      { monadic = (Monadic.set [@inlined hint]) ax a monadic; comonadic }
    | Comonadic ax ->
      { monadic; comonadic = (Comonadic.set [@inlined hint]) ax a comonadic }

  let create ~regionality ~linearity ~uniqueness ~portability ~contention
      ~forkable ~yielding ~statefulness ~visibility ~staticity =
    let comonadic b ax =
      if b then Per_axis.min (Comonadic ax) else Per_axis.max (Comonadic ax)
    in
    let monadic b ax =
      if b then Per_axis.min (Monadic ax) else Per_axis.max (Monadic ax)
    in
    let regionality = comonadic regionality Areality in
    let linearity = comonadic linearity Linearity in
    let uniqueness = monadic uniqueness Uniqueness in
    let portability = comonadic portability Portability in
    let contention = monadic contention Contention in
    let forkable = comonadic forkable Forkable in
    let yielding = comonadic yielding Yielding in
    let statefulness = comonadic statefulness Statefulness in
    let visibility = monadic visibility Visibility in
    let staticity = monadic staticity Staticity in
    let monadic =
      Monadic.create ~uniqueness ~contention ~visibility ~staticity
    in
    let comonadic =
      Comonadic.create ~regionality ~linearity ~portability ~yielding ~forkable
        ~statefulness
    in
    { monadic; comonadic }

  let print ppf t =
    let l =
      List.filter_map
        (fun ax ->
          let (P ax) = ax |> Modality.Axis.of_value |> Axis.of_modality in
          let a = proj ax t in
          if Per_axis.(le ax (max ax) a)
          then None
          else Some (Fmt.asprintf "%a" (Per_axis.print ax) a))
        Value.Axis.all
    in
    Fmt.(pp_print_list ~pp_sep:pp_print_space pp_print_string ppf l)

  let to_modality
      { monadic = Monadic.Modality monadic;
        comonadic = Comonadic.Modality comonadic
      } =
    { monadic; comonadic }
end