- solver returns gap

- refactor polarized_solver (avoid wrapper around const)

Author: riaqn

ocaml/typing/ctype.ml

@@ -4364,9 +4364,9 @@ let relevant_pairs pairs v =
 let moregen_alloc_mode v a1 a2 =
   match
     match v with
-    | Invariant -> Alloc.equate a1 a2
-    | Covariant -> Alloc.submode a1 a2
-    | Contravariant -> Alloc.submode a2 a1
+    | Invariant -> Result.map_error ignore (Alloc.equate a1 a2)
+    | Covariant -> Result.map_error ignore (Alloc.submode a1 a2)
+    | Contravariant -> Result.map_error ignore (Alloc.submode a2 a1)
     | Bivariant -> Ok ()
   with
   | Ok () -> ()

ocaml/typing/mode.ml

@@ -664,27 +664,33 @@ let append_changes = S.S.append_changes
 module type Obj = sig
   type const
 
-  type const_s
+  type polarity
 
-  val obj_s : const_s S.obj
-
-  val unpack : const_s -> const
-
-  val pack : const -> const_s
+  val obj_s : (const * polarity) S.obj
 end
 
+let equate_from_submode submode m0 m1 =
+  match submode m0 m1 with
+  | Error e -> Error (Left_le_right, e)
+  | Ok () -> (
+    match submode m1 m0 with
+    | Error e -> Error (Right_le_left, e)
+    | Ok () -> Ok ())
+
 module Common (Obj : Obj) = struct
   open Obj
 
-  type 'd t = (const_s, 'd) S.mode
+  type 'd t = (const * polarity, 'd) S.mode
 
   type l = (allowed * disallowed) t
 
   type r = (disallowed * allowed) t
 
   type lr = (allowed * allowed) t
 
-  type error = unit
+  type nonrec error = const error
+
+  type equate_error = equate_step * error
 
   let disallow_right m = S.disallow_right m
 
@@ -712,24 +718,19 @@ module Common (Obj : Obj) = struct
 
   let submode_exn m0 m1 = assert (submode m0 m1 |> Result.is_ok)
 
-  let equate m0 m1 =
-    match submode m0 m1 with
-    | Error () -> Error ()
-    | Ok () -> (
-      match submode m1 m0 with Error () -> Error () | Ok () -> Ok ())
+  let equate = equate_from_submode submode
 
   let equate_exn m0 m1 = assert (equate m0 m1 |> Result.is_ok)
 
   let print ?verbose ?axis () ppf m = S.print obj_s ?verbose ?axis ppf m
 
-  let constrain_upper m = Obj.unpack (S.constrain_upper obj_s m)
+  let constrain_upper m = S.constrain_upper obj_s m
 
-  let constrain_lower m = Obj.unpack (S.constrain_lower obj_s m)
+  let constrain_lower m = S.constrain_lower obj_s m
 
-  let of_const : type l r. const -> (l * r) t =
-   fun a -> S.of_const obj_s (Obj.pack a)
+  let of_const : type l r. const -> (l * r) t = fun a -> S.of_const obj_s a
 
-  let check_const m = Option.map Obj.unpack (S.check_const obj_s m)
+  let check_const m = S.check_const obj_s m
 end
 
 module Locality = struct
@@ -738,15 +739,11 @@ module Locality = struct
   module Obj = struct
     type const = Const.t
 
-    type const_s = Const.t S.pos
+    type polarity = positive
 
     let obj = C.Locality
 
-    let obj_s : const_s S.obj = S.Positive obj
-
-    let unpack (S.Pos a) = a
-
-    let pack a = S.Pos a
+    let obj_s : (const * polarity) S.obj = S.Positive obj
   end
 
   include Common (Obj)
@@ -766,13 +763,9 @@ module Regionality = struct
   module Obj = struct
     type const = Const.t
 
-    type const_s = Const.t S.pos
-
-    let obj_s : const_s S.obj = S.Positive C.Regionality
-
-    let unpack (S.Pos a) = a
+    type polarity = positive
 
-    let pack a = S.Pos a
+    let obj_s : (const * polarity) S.obj = S.Positive C.Regionality
   end
 
   include Common (Obj)
@@ -794,15 +787,11 @@ module Linearity = struct
   module Obj = struct
     type const = Const.t
 
-    type const_s = Const.t S.pos
+    type polarity = positive
 
     let obj = C.Linearity
 
-    let obj_s : const_s S.obj = S.Positive obj
-
-    let unpack (S.Pos a) = a
-
-    let pack a = S.Pos a
+    let obj_s : (const * polarity) S.obj = S.Positive obj
   end
 
   include Common (Obj)
@@ -823,15 +812,11 @@ module Uniqueness = struct
     type const = Const.t
 
     (* the negation of Uniqueness_op gives us the proper uniqueness *)
-    type const_s = Const.t S.neg
+    type polarity = negative
 
     let obj = C.Uniqueness_op
 
-    let obj_s : const_s S.obj = S.Negative obj
-
-    let unpack (S.Neg a) = a
-
-    let pack a = S.Neg a
+    let obj_s : (const * polarity) S.obj = S.Negative obj
   end
 
   include Common (Obj)
@@ -870,22 +855,20 @@ module Comonadic_with_regionality = struct
   module Obj = struct
     type const = Const.t
 
-    type const_s = Const.t S.pos
+    type polarity = positive
 
     let obj : const C.obj = C.Comonadic_with_regionality
 
-    let obj_s : const_s S.obj = S.Positive obj
-
-    let unpack (S.Pos a) = a
-
-    let pack a = S.Pos a
+    let obj_s : (const * polarity) S.obj = S.Positive obj
   end
 
   include Common (Obj)
 
   type error =
-    [ `Regionality
-    | `Linearity ]
+    [ `Regionality of Regionality.error
+    | `Linearity of Linearity.error ]
+
+  type equate_error = equate_step * error
 
   let regionality m =
     S.apply Regionality.Obj.obj_s (S.Pos_Pos (C.Proj (Obj.obj, Axis0))) m
@@ -933,27 +916,16 @@ module Comonadic_with_regionality = struct
   let submode m0 m1 =
     match submode m0 m1 with
     | Ok () -> Ok ()
-    | Error () -> (
-      (* find out the offending axis *)
-      match Regionality.submode (regionality m0) (regionality m1) with
-      | Error () -> Error `Regionality
-      | Ok () -> (
-        match Linearity.submode (linearity m0) (linearity m1) with
-        | Error () -> Error `Linearity
-        | Ok () -> assert false (* sanity *)))
+    | Error { left = reg0, lin0; right = reg1, lin1 } ->
+      if Regionality.Const.le reg0 reg1
+      then
+        if Linearity.Const.le lin0 lin1
+        then assert false
+        else Error (`Linearity { left = lin0; right = lin1 })
+      else Error (`Regionality { left = reg0; right = reg1 })
 
   (* override to report the offending axis *)
-  let equate m0 m1 =
-    match equate m0 m1 with
-    | Ok () -> Ok ()
-    | Error () -> (
-      (* find out the offending axis *)
-      match Regionality.equate (regionality m0) (regionality m1) with
-      | Error () -> Error `Regionality
-      | Ok () -> (
-        match Linearity.equate (linearity m0) (linearity m1) with
-        | Ok () -> assert false (* sanity *)
-        | Error () -> Error `Linearity))
+  let equate = equate_from_submode submode
 
   (** overriding to check per-axis *)
   let check_const m =
@@ -970,22 +942,20 @@ module Comonadic_with_locality = struct
   module Obj = struct
     type const = Const.t
 
-    type const_s = Const.t S.pos
+    type polarity = positive
 
     let obj : const C.obj = C.Comonadic_with_locality
 
-    let obj_s : const_s S.obj = S.Positive obj
-
-    let unpack (S.Pos a) = a
-
-    let pack a = S.Pos a
+    let obj_s : (const * polarity) S.obj = S.Positive obj
   end
 
   include Common (Obj)
 
   type error =
-    [ `Locality
-    | `Linearity ]
+    [ `Locality of Locality.error
+    | `Linearity of Linearity.error ]
+
+  type equate_error = equate_step * error
 
   let locality m =
     S.apply Locality.Obj.obj_s (S.Pos_Pos (C.Proj (Obj.obj, Axis0))) m
@@ -1033,27 +1003,16 @@ module Comonadic_with_locality = struct
   let submode m0 m1 =
     match submode m0 m1 with
     | Ok () -> Ok ()
-    | Error () -> (
-      (* find out the offending axis *)
-      match Locality.submode (locality m0) (locality m1) with
-      | Error () -> Error `Locality
-      | Ok () -> (
-        match Linearity.submode (linearity m0) (linearity m1) with
-        | Ok () -> assert false (* sanity *)
-        | Error () -> Error `Linearity))
+    | Error { left = loc0, lin0; right = loc1, lin1 } ->
+      if Locality.Const.le loc0 loc1
+      then
+        if Linearity.Const.le lin0 lin1
+        then assert false
+        else Error (`Linearity { left = lin0; right = lin1 })
+      else Error (`Locality { left = loc0; right = loc1 })
 
   (* override to report the offending axis *)
-  let equate m0 m1 =
-    match equate m0 m1 with
-    | Ok () -> Ok ()
-    | Error () -> (
-      (* find out the offending axis *)
-      match Locality.equate (locality m0) (locality m1) with
-      | Error () -> Error `Locality
-      | Ok () -> (
-        match Linearity.equate (linearity m0) (linearity m1) with
-        | Ok () -> assert false (* sanity *)
-        | Error () -> Error `Linearity))
+  let equate = equate_from_submode submode
 
   (** overriding to check per-axis *)
   let check_const m =
@@ -1068,7 +1027,9 @@ module Monadic = struct
   (* secretly just uniqueness *)
   include Uniqueness
 
-  type error = [`Uniqueness]
+  type error = [`Uniqueness of Uniqueness.error]
+
+  type equate_error = equate_step * error
 
   let max_with_uniqueness m = S.disallow_left m
 
@@ -1079,10 +1040,9 @@ module Monadic = struct
   let set_uniqueness_min _ = Uniqueness.min |> S.disallow_right |> S.allow_left
 
   let submode m0 m1 =
-    match submode m0 m1 with Ok () -> Ok () | Error () -> Error `Uniqueness
+    match submode m0 m1 with Ok () -> Ok () | Error e -> Error (`Uniqueness e)
 
-  let equate m0 m1 =
-    match equate m0 m1 with Ok () -> Ok () | Error () -> Error `Uniqueness
+  let equate = equate_from_submode submode
 end
 
 type ('mo, 'como) monadic_comonadic =
@@ -1139,9 +1099,11 @@ module Value = struct
   let regionality { comonadic; _ } = Comonadic.regionality comonadic
 
   type error =
-    [ `Regionality
-    | `Uniqueness
-    | `Linearity ]
+    [ `Regionality of Regionality.error
+    | `Uniqueness of Uniqueness.error
+    | `Linearity of Linearity.error ]
+
+  type equate_error = equate_step * error
 
   (* NB: state mutated when error *)
   let submode { monadic = monadic0; comonadic = comonadic0 }
@@ -1155,8 +1117,7 @@ module Value = struct
       | Error e -> Error e
       | Ok () -> Ok ())
 
-  let equate m0 m1 =
-    match submode m0 m1 with Error e -> Error e | Ok () -> submode m1 m0
+  let equate = equate_from_submode submode
 
   let submode_exn m0 m1 =
     match submode m0 m1 with
@@ -1368,9 +1329,11 @@ module Alloc = struct
   let locality { comonadic; _ } = Comonadic.locality comonadic
 
   type error =
-    [ `Locality
-    | `Uniqueness
-    | `Linearity ]
+    [ `Locality of Locality.error
+    | `Uniqueness of Uniqueness.error
+    | `Linearity of Linearity.error ]
+
+  type equate_error = equate_step * error
 
   (* NB: state mutated when error - should be fine as this always indicates type
      error in typecore.ml which triggers backtracking. *)
@@ -1383,8 +1346,7 @@ module Alloc = struct
       | Error e -> Error e
       | Ok () -> Ok ())
 
-  let equate m0 m1 =
-    match submode m0 m1 with Error e -> Error e | Ok () -> submode m1 m0
+  let equate = equate_from_submode submode
 
   let submode_exn m0 m1 =
     match submode m0 m1 with