flambda-backend: Add missing morphism reductions (#2374)

* add missing reduction

* address comments; more improvement

Author: riaqn

typing/mode.ml

@@ -407,6 +407,9 @@ module Lattices = struct
     | Linearity, (area, _) -> area, r
     | Uniqueness, (_, ()) -> r, ()
 
+  let set_areality : type a0 a1. a1 -> a0 comonadic_with -> a1 comonadic_with =
+   fun r (_, lin) -> r, lin
+
   let proj_obj : type t r. (t, r) axis -> t obj -> r obj =
    fun ax obj ->
     match ax, obj with
@@ -885,13 +888,33 @@ module Lattices_mono = struct
       type a b c d.
       c obj -> (b, c, d) morph -> (a, b, d) morph -> (a, c, d) morph option =
    fun dst m0 m1 ->
+    let is_max c = le dst (max dst) c in
+    let is_min c = le dst c (min dst) in
+    let is_mid_max c =
+      let mid = src dst m0 in
+      le mid (max mid) c
+    in
+    let is_mid_min c =
+      let mid = src dst m0 in
+      le mid c (min mid)
+    in
     match m0, m1 with
     | Id, m -> Some m
     | m, Id -> Some m
     | Meet_with c0, Meet_with c1 -> Some (Meet_with (meet dst c0 c1))
     | Join_with c0, Join_with c1 -> Some (Join_with (join dst c0 c1))
-    | Meet_with c0, m1 when le dst (max dst) c0 -> Some m1
-    | Join_with c0, m1 when le dst c0 (min dst) -> Some m1
+    | Imply c0, Imply c1 -> Some (Imply (meet dst c0 c1))
+    | Subtract c0, Subtract c1 -> Some (Subtract (join dst c0 c1))
+    | Imply c0, Join_with c1 when le dst c0 c1 -> Some (Join_with (max dst))
+    | Subtract c0, Meet_with c1 when le dst c1 c0 -> Some (Meet_with (min dst))
+    | Meet_with c0, m1 when is_max c0 -> Some m1
+    | Join_with c0, m1 when is_min c0 -> Some m1
+    | Imply c0, m1 when is_max c0 -> Some m1
+    | Subtract c0, m1 when is_min c0 -> Some m1
+    | m1, Meet_with c0 when is_mid_max c0 -> Some m1
+    | m1, Join_with c0 when is_mid_min c0 -> Some m1
+    | m1, Imply c0 when is_mid_max c0 -> Some m1
+    | m1, Subtract c0 when is_mid_min c0 -> Some m1
     | Compose (f0, f1), g -> (
       let mid = src dst f0 in
       match maybe_compose mid f1 g with
@@ -903,9 +926,9 @@ module Lattices_mono = struct
       | Some m -> Some (compose dst m g1)
       | None -> None)
     | Proj (mid, ax), Meet_with c ->
-      Some (Compose (Meet_with (proj ax c), Proj (mid, ax)))
+      Some (compose dst (Meet_with (proj ax c)) (Proj (mid, ax)))
     | Proj (mid, ax), Join_with c ->
-      Some (Compose (Join_with (proj ax c), Proj (mid, ax)))
+      Some (compose dst (Join_with (proj ax c)) (Proj (mid, ax)))
     | Proj (_, ax0), Max_with ax1 -> (
       match eq_axis ax0 ax1 with None -> None | Some Refl -> Some Id)
     | Proj (_, ax0), Min_with ax1 -> (
@@ -952,18 +975,32 @@ module Lattices_mono = struct
            Locality_as_regionality)
     | Map_comonadic f, Join_with c ->
       let dst0 = proj_obj Areality dst in
-      let areality, linearity = c in
+      let areality = proj Areality c in
       Some
         (compose dst
-           (Join_with (min_with dst Linearity linearity))
+           (Join_with (set_areality (min dst0) c))
            (Map_comonadic (compose dst0 f (Join_with areality))))
     | Map_comonadic f, Meet_with c ->
       let dst0 = proj_obj Areality dst in
-      let areality, linearity = c in
+      let areality = proj Areality c in
       Some
         (compose dst
-           (Meet_with (max_with dst Linearity linearity))
+           (Meet_with (set_areality (max dst0) c))
            (Map_comonadic (compose dst0 f (Meet_with areality))))
+    | Map_comonadic f, Imply c ->
+      let dst0 = proj_obj Areality dst in
+      let areality = proj Areality c in
+      Some
+        (compose dst
+           (Imply (set_areality (max dst0) c))
+           (Map_comonadic (compose dst0 f (Imply areality))))
+    | Map_comonadic f, Subtract c ->
+      let dst0 = proj_obj Areality dst in
+      let areality = proj Areality c in
+      Some
+        (compose dst
+           (Subtract (set_areality (min dst0) c))
+           (Map_comonadic (compose dst0 f (Subtract areality))))
     | Regional_to_global, Locality_as_regionality -> Some Id
     | Regional_to_global, Local_to_regional -> Some (Meet_with Locality.Global)
     | Local_to_regional, Regional_to_local -> None