[Eva] Lattice_bounds: open variants for Operators

src/kernel_services/abstract_interp/lattice_bounds.ml

@@ -24,17 +24,6 @@ type 'a or_bottom = [ `Value of 'a | `Bottom ]
 type 'a or_top = [ `Value of 'a | `Top ]
 type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
 
-module type Operators =
-sig
-  type 'a t
-  val (>>-) : 'a t -> ('a -> 'b t) -> 'b t
-  val (>>-:) : 'a t -> ('a -> 'b) -> 'b t
-  val (let+) : 'a t -> ('a -> 'b) -> 'b t
-  val (and+) : 'a t -> 'b t -> ('a * 'b) t
-  val (let*) : 'a t -> ('a -> 'b t) -> 'b t
-  val (and*) : 'a t -> 'b t -> ('a * 'b) t
-end
-
 (** Common functions *)
 
 module Common =
@@ -181,8 +170,6 @@ module Bottom = struct
 
   module Operators =
   struct
-    type 'a t = 'a or_bottom
-
     let (>>-) t f = match t with
       | `Bottom  -> `Bottom
       | `Value t -> f t
@@ -278,8 +265,6 @@ struct
   (** Operators *)
 
   module Operators = struct
-    type 'a t = 'a or_top
-
     let (>>-) t f = match t with
       | `Top -> `Top
       | `Value t -> f t
@@ -325,8 +310,6 @@ struct
   (** Operators *)
 
   module Operators = struct
-    type 'a t = 'a or_top_bottom
-
     let (>>-) t f = match t with
       | `Top -> `Top
       | `Bottom -> `Bottom

src/kernel_services/abstract_interp/lattice_bounds.mli

@@ -27,32 +27,27 @@ type 'a or_bottom = [ `Value of 'a | `Bottom ]
 type 'a or_top = [ `Value of 'a | `Top ]
 type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
 
-module type Operators =
-sig
-  type 'a t
 
+module Bottom : sig
+  type 'a t = 'a or_bottom
+
+  (** Operators *)
+  module Operators : sig
     (** This monad propagates `Bottom and or `Top if needed. *)
-  val (>>-) : 'a t -> ('a -> 'b t) -> 'b t
+    val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
 
     (** Use this monad if the following function returns a simple value. *)
-  val (>>-:) : 'a t -> ('a -> 'b) -> 'b t
+    val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
 
     (* Binding operators, applicative syntax *)
-  val (let+) : 'a t -> ('a -> 'b) -> 'b t
-  val (and+) : 'a t -> 'b t -> ('a * 'b) t
+    val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+    val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
 
     (* Binding operators, monad syntax *)
-  val (let*) : 'a t -> ('a -> 'b t) -> 'b t
-  val (and*) : 'a t -> 'b t -> ('a * 'b) t
+    val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+    val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
   end
 
-
-module Bottom : sig
-  type 'a t = 'a or_bottom
-
-  (** Operators *)
-  module Operators : Operators with type 'a t = 'a or_bottom
-
   (** Datatype constructor *)
   module Make_Datatype
       (Domain: Datatype.S)
@@ -113,7 +108,21 @@ module Top : sig
   type 'a t = 'a or_top
 
   (** Operators *)
-  module Operators : Operators with type 'a t = 'a or_top
+  module Operators : sig
+    (** This monad propagates `Bottom and or `Top if needed. *)
+    val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+
+    (** Use this monad if the following function returns a simple value. *)
+    val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+
+    (* Binding operators, applicative syntax *)
+    val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+    val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
+    (* Binding operators, monad syntax *)
+    val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+    val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+  end
 
   (** Access *)
   val is_top: 'a t -> bool
@@ -147,6 +156,25 @@ end
 module TopBottom: sig
   type 'a t = 'a or_top_bottom
 
+  (** Operators *)
+  (* In presence of simultaneous `Bottom and `Top in and+ / and*, everything
+     narrows down to `Bottom *)
+  module Operators : sig
+    (** This monad propagates `Bottom and or `Top if needed. *)
+    val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+
+    (** Use this monad if the following function returns a simple value. *)
+    val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+
+    (* Binding operators, applicative syntax *)
+    val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+    val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
+    (* Binding operators, monad syntax *)
+    val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+    val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+  end
+
   (** Datatype *)
   val hash: ('a -> int) -> 'a t -> int
   val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
@@ -160,9 +188,4 @@ module TopBottom: sig
   (* Lattice operators *)
   val join: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
   val narrow: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
-
-  (** Operators *)
-  (* In presence of simultaneous `Bottom and `Top in and+ / and*, everything
-     narrows down to `Bottom *)
-  module Operators : Operators with type 'a t = 'a or_top_bottom
 end

src/plugins/value/utils/results.ml

@@ -174,9 +174,8 @@ struct
   let map_join' : type c. ('a -> [< 'b or_top_bottom]) -> ('b -> 'b -> 'b) ->
     ('a, c) t -> 'b or_top_bottom =
     fun map join ->
-    let map' x = (map x :> 'b or_top_bottom)
-    and join' = TopBottom.join (fun x y -> `Value (join x y)) in
-    map_reduce default map' join'
+    let join' = TopBottom.join (fun x y -> `Value (join x y)) in
+    map_reduce default map join'
 end
 
 
@@ -305,7 +304,7 @@ struct
     let join = (@)
     and extract state =
       let r,_alarms = A.Eval.eval_function_exp exp state in
-      (r :> _ or_top_bottom) >>-: List.map fst
+      r >>-: List.map fst
     in
     get req |> Response.map_join' extract join |> convert |>
     Result.map (List.sort_uniq Kernel_function.compare)
@@ -318,11 +317,11 @@ struct
     | None -> `Top
     | Some get ->
       let make_expr (x, _alarms) =
-        (x :> _ or_top_bottom) >>-: fun (_valuation, v) ->
+        x >>-: fun (_valuation, v) ->
         Cvalue.V_Or_Uninitialized.make ~initialized:true ~escaping:false (get v)
       in
       let make_lval (x, _alarms) =
-        (x :> _ or_top_bottom) >>-: fun (_valuation, v) ->
+        let+ _valuation, v = x in
         let Eval.{ v; initialized; escaping } = v in
         let v =
           match v with
@@ -354,7 +353,7 @@ struct
     | Some get ->
       let join = Main_values.CVal.join in
       let extract value =
-        (value :> _ or_top_bottom) >>-: get
+        value >>-: get
       in
       extract_value res |> Response.map_join' extract join |> convert
 
@@ -381,7 +380,7 @@ struct
         assert (Int_Base.equal loc2.size size);
         make_loc loc size
       and extract loc =
-        (loc :> _ or_top_bottom) >>-: get >>-: Precise_locs.imprecise_location
+        loc >>-: get >>-: Precise_locs.imprecise_location
       in
       extract_loc res |> fst |> Response.map_join' extract join |> convert
 
@@ -393,7 +392,7 @@ struct
       let response_loc, access = extract_loc res in
       let join = Locations.Zone.join
       and extract loc =
-        (loc :> _ or_top_bottom) >>-: get >>-:
+        loc >>-: get >>-:
         Precise_locs.enumerate_valid_bits access
       in
       response_loc |> Response.map_join' extract join |> convert
@@ -403,7 +402,7 @@ struct
     | LValue r ->
       let join = (&&)
       and extract (x, _alarms) =
-        (x :> _ or_top_bottom) >>-: (fun (_valuation,fv) -> fv.Eval.initialized)
+        x >>-: (fun (_valuation,fv) -> fv.Eval.initialized)
       in
       begin match Response.map_join' extract join r with
         | `Bottom | `Top -> false