Extract GobList.cartesian_filter_map

Author: sim642

src/domain/hoareDomain.ml

@@ -368,8 +368,7 @@ struct
   (* TODO: move to Set above? *)
   let product_widen (op: elt -> elt -> elt option) a b = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    (* TODO: GobList.cartesian_filter_map? *)
-    List.concat_map (fun x -> List.filter_map (fun y -> op x y) ys) xs |> fun x -> join b (of_list x)
+    GobList.cartesian_filter_map op xs ys |> fun x -> join b (of_list x)
   let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None)
 
   (* above widen is actually extrapolation operator, so define connector-based widening instead *)

src/util/std/gobList.ml

@@ -58,6 +58,9 @@ let until_last_with (pred: 'a -> bool) (xs: 'a list) =
 let cartesian_map f l1 l2 =
   List.concat_map (fun x -> List.map (f x) l2) l1
 
+let cartesian_filter_map f l1 l2 =
+  List.concat_map (fun x -> List.filter_map (f x) l2) l1
+
 let cartesian_concat_map f l1 l2 =
   List.concat_map (fun x -> List.concat_map (f x) l2) l1