[Eva] Lattice_bounds: implements [join] and [narrow] for the Top module.

src/kernel_services/abstract_interp/lattice_bounds.ml

@@ -250,6 +250,18 @@ struct
     | `Value v -> v
     | `Top -> top
 
+  (** Lattice *)
+
+  let join join_value x y =
+    match x, y with
+    | `Top, _ | _, `Top -> `Top
+    | `Value vx, `Value vy -> join_value vx vy
+
+  let narrow narrow_value x y =
+    match x, y with
+    | `Top, v | v, `Top -> v
+    | `Value vx, `Value vy -> `Value (narrow_value vx vy)
+
   (** Combination *)
 
   let zip x y =

src/kernel_services/abstract_interp/lattice_bounds.mli

@@ -131,6 +131,10 @@ module Top : sig
     (Format.formatter -> 'a -> unit) ->
     Format.formatter -> 'a t -> unit
 
+  (** Lattice operators *)
+  val join: ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+  val narrow: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+
   (** Combination *)
   val zip: 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *)