Delete Jkind_axis.Modal in favor of Mode.Alloc.axis (#3409)

typing/jkind.ml

@@ -1205,10 +1205,10 @@ module Jkind_desc = struct
     in
     let upper_bounds = to_.upper_bounds in
     let upper_bounds, added1 =
-      add_crossing ~axis:(Modal Portability) upper_bounds
+      add_crossing ~axis:(Modal (Comonadic Portability)) upper_bounds
     in
     let upper_bounds, added2 =
-      add_crossing ~axis:(Modal Contention) upper_bounds
+      add_crossing ~axis:(Modal (Monadic Contention)) upper_bounds
     in
     { to_ with upper_bounds }, added1 || added2
 
@@ -1606,19 +1606,19 @@ let extract_layout jk = jk.jkind.layout
 let get_modal_upper_bounds ~type_equal ~jkind_of_type jk : Alloc.Const.t =
   let bounds = jk.jkind.upper_bounds in
   { areality =
-      Bound.reduce ~axis:(Modal Locality) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Comonadic Areality)) ~type_equal ~jkind_of_type
         bounds.locality;
     linearity =
-      Bound.reduce ~axis:(Modal Linearity) ~type_equal ~jkind_of_type
-        bounds.linearity;
+      Bound.reduce ~axis:(Modal (Comonadic Linearity)) ~type_equal
+        ~jkind_of_type bounds.linearity;
     uniqueness =
-      Bound.reduce ~axis:(Modal Uniqueness) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Monadic Uniqueness)) ~type_equal ~jkind_of_type
         bounds.uniqueness;
     portability =
-      Bound.reduce ~axis:(Modal Portability) ~type_equal ~jkind_of_type
-        bounds.portability;
+      Bound.reduce ~axis:(Modal (Comonadic Portability)) ~type_equal
+        ~jkind_of_type bounds.portability;
     contention =
-      Bound.reduce ~axis:(Modal Contention) ~type_equal ~jkind_of_type
+      Bound.reduce ~axis:(Modal (Monadic Contention)) ~type_equal ~jkind_of_type
         bounds.contention
   }
 

typing/jkind_axis.ml

@@ -115,130 +115,74 @@ module Nullability = struct
 end
 
 module Axis = struct
-  module Modal = struct
-    type 'a t =
-      | Locality : Mode.Locality.Const.t t
-      | Linearity : Mode.Linearity.Const.t t
-      | Uniqueness : Mode.Uniqueness.Const.t t
-      | Portability : Mode.Portability.Const.t t
-      | Contention : Mode.Contention.Const.t t
-  end
-
   module Nonmodal = struct
     type 'a t =
       | Externality : Externality.t t
       | Nullability : Nullability.t t
   end
 
   type 'a t =
-    | Modal of 'a Modal.t
-    | Nonmodal of 'a Nonmodal.t
+    | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
+    | Nonmodal : 'a Nonmodal.t -> 'a t
 
   type packed = Pack : 'a t -> packed
 
-  module Accent_lattice (M : Mode_intf.Lattice) : Axis_ops with type t = M.t =
-  struct
+  module Accent_lattice (M : Mode_intf.Lattice) = struct
     (* A functor to add some convenient functions to modal axes *)
     include M
 
-    let less_or_equal a b = Misc.Le_result.less_or_equal ~le a b
+    let less_or_equal a b : Misc.Le_result.t =
+      match le a b, le b a with
+      | true, true -> Equal
+      | true, false -> Less
+      | false, _ -> Not_le
 
-    let equal a b = Misc.Le_result.equal ~le a b
+    let equal a b = Misc.Le_result.is_equal (less_or_equal a b)
   end
 
   let get (type a) : a t -> (module Axis_ops with type t = a) = function
-    | Modal Locality -> (module Accent_lattice (Mode.Locality.Const))
-    | Modal Linearity -> (module Accent_lattice (Mode.Linearity.Const))
-    | Modal Uniqueness -> (module Accent_lattice (Mode.Uniqueness.Const))
-    | Modal Portability -> (module Accent_lattice (Mode.Portability.Const))
-    | Modal Contention -> (module Accent_lattice (Mode.Contention.Const))
+    | Modal axis -> (module Accent_lattice (val Mode.Alloc.lattice_of_axis axis))
     | Nonmodal Externality -> (module Externality)
     | Nonmodal Nullability -> (module Nullability)
 
   let all =
-    [ Pack (Modal Locality);
-      Pack (Modal Uniqueness);
-      Pack (Modal Linearity);
-      Pack (Modal Contention);
-      Pack (Modal Portability);
+    [ Pack (Modal (Comonadic Areality));
+      Pack (Modal (Monadic Uniqueness));
+      Pack (Modal (Comonadic Linearity));
+      Pack (Modal (Monadic Contention));
+      Pack (Modal (Comonadic Portability));
       Pack (Nonmodal Externality);
       Pack (Nonmodal Nullability) ]
 
   let name (type a) : a t -> string = function
-    | Modal Locality -> "locality"
-    | Modal Linearity -> "linearity"
-    | Modal Uniqueness -> "uniqueness"
-    | Modal Portability -> "portability"
-    | Modal Contention -> "contention"
+    | Modal axis -> Format.asprintf "%a" Mode.Alloc.print_axis axis
     | Nonmodal Externality -> "externality"
     | Nonmodal Nullability -> "nullability"
 
   let is_modal (type a) : a t -> bool = function
-    | Modal Locality -> true
-    | Modal Linearity -> true
-    | Modal Uniqueness -> true
-    | Modal Portability -> true
-    | Modal Contention -> true
+    | Modal (Comonadic Areality) -> true
+    | Modal (Comonadic Linearity) -> true
+    | Modal (Monadic Uniqueness) -> true
+    | Modal (Comonadic Portability) -> true
+    | Modal (Monadic Contention) -> true
     | Nonmodal Externality -> true
     | Nonmodal Nullability -> false
 
-  (* CR aspsmith: This can get a lot simpler once we unify jkind axes with the axes in
-     Mode *)
-  let modality_is_const_for_axis (type a) (t : a t) modality =
+  let modality_is_const_for_axis (type a) (t : a t)
+      (modality : Mode.Modality.Value.Const.t) =
     match t with
     | Nonmodal Nullability | Nonmodal Externality -> false
     | Modal axis ->
-      let atoms = Mode.Modality.Value.Const.to_list modality in
-      List.exists
-        (fun (modality : Mode.Modality.t) ->
-          match axis, modality with
-          (* Constant modalities *)
-          | Locality, Atom (Comonadic Areality, Meet_with Global) -> true
-          | Linearity, Atom (Comonadic Linearity, Meet_with Many) -> true
-          | Uniqueness, Atom (Monadic Uniqueness, Join_with Aliased) -> true
-          | Portability, Atom (Comonadic Portability, Meet_with Portable) ->
-            true
-          | Contention, Atom (Monadic Contention, Join_with Contended) -> true
-          (* Modalities which are actually identity *)
-          | Locality, Atom (Comonadic Areality, Meet_with Local)
-          | Linearity, Atom (Comonadic Linearity, Meet_with Once)
-          | Uniqueness, Atom (Monadic Uniqueness, Join_with Unique)
-          | Portability, Atom (Comonadic Portability, Meet_with Nonportable)
-          | Contention, Atom (Monadic Contention, Join_with Uncontended) ->
-            false
-          (* Modalities which are neither constant nor identiy *)
-          | Locality, Atom (Comonadic Areality, Meet_with Regional)
-          | Contention, Atom (Monadic Contention, Join_with Shared) ->
-            Misc.fatal_error
-              "Don't yet know how to interpret non-constant, non-identity \
-               modalities"
-          (* Modalities which join or meet on an illegal axis *)
-          | _, Atom (Comonadic _, Join_with _) | _, Atom (Monadic _, Meet_with _)
-            ->
-            Misc.fatal_error "Illegal modality"
-          (* Mismatched axes *)
-          | Locality, Atom (Monadic Uniqueness, _)
-          | Locality, Atom (Monadic Contention, _)
-          | Locality, Atom (Comonadic Linearity, _)
-          | Locality, Atom (Comonadic Portability, _)
-          | Linearity, Atom (Comonadic Areality, _)
-          | Linearity, Atom (Monadic Uniqueness, _)
-          | Portability, Atom (Monadic Uniqueness, _)
-          | Contention, Atom (Monadic Uniqueness, _)
-          | Linearity, Atom (Comonadic Portability, _)
-          | Linearity, Atom (Monadic Contention, _)
-          | Uniqueness, Atom (Comonadic Areality, _)
-          | Uniqueness, Atom (Comonadic Linearity, _)
-          | Uniqueness, Atom (Comonadic Portability, _)
-          | Contention, Atom (Comonadic Areality, _)
-          | Contention, Atom (Comonadic Linearity, _)
-          | Contention, Atom (Comonadic Portability, _)
-          | Uniqueness, Atom (Monadic Contention, _)
-          | Portability, Atom (Comonadic Areality, _)
-          | Portability, Atom (Comonadic Linearity, _)
-          | Portability, Atom (Monadic Contention, _) ->
-            false)
-        atoms
+      let (P axis) = Mode.Const.Axis.alloc_as_value (P axis) in
+      let modality = Mode.Modality.Value.Const.proj axis modality in
+      if Mode.Modality.is_constant modality
+      then true
+      else if Mode.Modality.is_id modality
+      then false
+      else
+        Misc.fatal_error
+          "Don't yet know how to interpret non-constant, non-identity \
+           modalities"
 end
 
 module type Axed = sig
@@ -259,21 +203,21 @@ module Axis_collection (T : Axed) = struct
 
   let get (type a) ~(axis : a Axis.t) values : (_, _, a) T.t =
     match axis with
-    | Modal Locality -> values.locality
-    | Modal Linearity -> values.linearity
-    | Modal Uniqueness -> values.uniqueness
-    | Modal Portability -> values.portability
-    | Modal Contention -> values.contention
+    | Modal (Comonadic Areality) -> values.locality
+    | Modal (Comonadic Linearity) -> values.linearity
+    | Modal (Monadic Uniqueness) -> values.uniqueness
+    | Modal (Comonadic Portability) -> values.portability
+    | Modal (Monadic Contention) -> values.contention
     | Nonmodal Externality -> values.externality
     | Nonmodal Nullability -> values.nullability
 
   let set (type a) ~(axis : a Axis.t) values (value : (_, _, a) T.t) =
     match axis with
-    | Modal Locality -> { values with locality = value }
-    | Modal Linearity -> { values with linearity = value }
-    | Modal Uniqueness -> { values with uniqueness = value }
-    | Modal Portability -> { values with portability = value }
-    | Modal Contention -> { values with contention = value }
+    | Modal (Comonadic Areality) -> { values with locality = value }
+    | Modal (Comonadic Linearity) -> { values with linearity = value }
+    | Modal (Monadic Uniqueness) -> { values with uniqueness = value }
+    | Modal (Comonadic Portability) -> { values with portability = value }
+    | Modal (Monadic Contention) -> { values with contention = value }
     | Nonmodal Externality -> { values with externality = value }
     | Nonmodal Nullability -> { values with nullability = value }
 
@@ -287,11 +231,11 @@ module Axis_collection (T : Axed) = struct
 
       let[@inline] f { f } =
         let open M.Syntax in
-        let* locality = f ~axis:Axis.(Modal Locality) in
-        let* uniqueness = f ~axis:Axis.(Modal Uniqueness) in
-        let* linearity = f ~axis:Axis.(Modal Linearity) in
-        let* contention = f ~axis:Axis.(Modal Contention) in
-        let* portability = f ~axis:Axis.(Modal Portability) in
+        let* locality = f ~axis:Axis.(Modal (Comonadic Areality)) in
+        let* uniqueness = f ~axis:Axis.(Modal (Monadic Uniqueness)) in
+        let* linearity = f ~axis:Axis.(Modal (Comonadic Linearity)) in
+        let* contention = f ~axis:Axis.(Modal (Monadic Contention)) in
+        let* portability = f ~axis:Axis.(Modal (Comonadic Portability)) in
         let* externality = f ~axis:Axis.(Nonmodal Externality) in
         let* nullability = f ~axis:Axis.(Nonmodal Nullability) in
         M.return
@@ -380,11 +324,11 @@ module Axis_collection (T : Axed) = struct
           externality;
           nullability
         } ~combine =
-      combine (f ~axis:Axis.(Modal Locality) locality)
-      @@ combine (f ~axis:Axis.(Modal Uniqueness) uniqueness)
-      @@ combine (f ~axis:Axis.(Modal Linearity) linearity)
-      @@ combine (f ~axis:Axis.(Modal Contention) contention)
-      @@ combine (f ~axis:Axis.(Modal Portability) portability)
+      combine (f ~axis:Axis.(Modal (Comonadic Areality)) locality)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uniqueness)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) linearity)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) contention)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) portability)
       @@ combine (f ~axis:Axis.(Nonmodal Externality) externality)
       @@ f ~axis:Axis.(Nonmodal Nullability) nullability
   end
@@ -417,11 +361,11 @@ module Axis_collection (T : Axed) = struct
           externality = ext2;
           nullability = nul2
         } ~combine =
-      combine (f ~axis:Axis.(Modal Locality) loc1 loc2)
-      @@ combine (f ~axis:Axis.(Modal Uniqueness) uni1 uni2)
-      @@ combine (f ~axis:Axis.(Modal Linearity) lin1 lin2)
-      @@ combine (f ~axis:Axis.(Modal Contention) con1 con2)
-      @@ combine (f ~axis:Axis.(Modal Portability) por1 por2)
+      combine (f ~axis:Axis.(Modal (Comonadic Areality)) loc1 loc2)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Uniqueness)) uni1 uni2)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Linearity)) lin1 lin2)
+      @@ combine (f ~axis:Axis.(Modal (Monadic Contention)) con1 con2)
+      @@ combine (f ~axis:Axis.(Modal (Comonadic Portability)) por1 por2)
       @@ combine (f ~axis:Axis.(Nonmodal Externality) ext1 ext2)
       @@ f ~axis:Axis.(Nonmodal Nullability) nul1 nul2
   end

typing/jkind_axis.mli

@@ -41,16 +41,6 @@ module Nullability : sig
 end
 
 module Axis : sig
-  (* CR zqian: remove this and use [Mode.Alloc.axis] instead *)
-  module Modal : sig
-    type 'a t =
-      | Locality : Mode.Locality.Const.t t
-      | Linearity : Mode.Linearity.Const.t t
-      | Uniqueness : Mode.Uniqueness.Const.t t
-      | Portability : Mode.Portability.Const.t t
-      | Contention : Mode.Contention.Const.t t
-  end
-
   module Nonmodal : sig
     type 'a t =
       | Externality : Externality.t t
@@ -59,8 +49,8 @@ module Axis : sig
 
   (** Represents an axis of a jkind *)
   type 'a t =
-    | Modal of 'a Modal.t
-    | Nonmodal of 'a Nonmodal.t
+    | Modal : ('m, 'a, 'd) Mode.Alloc.axis -> 'a t
+    | Nonmodal : 'a Nonmodal.t -> 'a t
 
   type packed = Pack : 'a t -> packed