Extract GobList.cartesian_map

Author: sim642

src/arg/myARG.ml

@@ -278,7 +278,7 @@ struct
   let next_opt _ = None
 end
 
-let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps
+let cartesian_append: cfg_path list -> cfg_path list -> cfg_path list = GobList.cartesian_map (@)
 
 let partition_if_next if_next =
   let (if_next_trues, if_next_falses) = List.partition (function
@@ -318,8 +318,8 @@ struct
           if Node.equal if_false_next_n if_true_next_false_next_n then
             let exp = BinOp (LAnd, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_true_next_n, cartesian_concat_paths if_true_next_ps if_true_next_true_next_ps);
-              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_concat_paths if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
+              (Test (exp, true), if_true_next_true_next_n, cartesian_append if_true_next_ps if_true_next_true_next_ps);
+              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_append if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
             ]
           else
             None
@@ -330,8 +330,8 @@ struct
           if Node.equal if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
-              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
-              (Test (exp, false), if_false_next_false_next_n, cartesian_concat_paths if_false_next_ps if_false_next_false_next_ps)
+              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_append if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
+              (Test (exp, false), if_false_next_false_next_n, cartesian_append if_false_next_ps if_false_next_false_next_ps)
             ]
           else
             None
@@ -366,8 +366,8 @@ struct
         | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_ps)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_ps)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
           let exp = ternary e_cond e_true e_false in
           Some [
-            (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps);
-            (Assign (v_false, exp), if_false_next_next_n, cartesian_concat_paths if_false_next_ps if_false_next_next_ps)
+            (Assign (v_true, exp), if_true_next_next_n, cartesian_append if_true_next_ps if_true_next_next_ps);
+            (Assign (v_false, exp), if_false_next_next_n, cartesian_append if_false_next_ps if_false_next_next_ps)
           ]
         | _, _ -> None
       else

src/cdomain/value/cdomains/structDomain.ml

@@ -177,7 +177,8 @@ struct
     in
     let x_list = HS.elements x in
     let y_list = HS.elements y in
-    List.concat_map (fun xss -> List.map (fun yss -> (xss, yss)) y_list) x_list
+    (* TODO: GobList.cartesian_filter_map? or just Seq? *)
+    BatList.cartesian_product x_list y_list
     |> List.filter (fun (ssx, ssy) -> maps_overlap ssx ssy)
     |> List.map (fun (ssx, ssy) -> f ssx ssy)
     |> HS.of_list
@@ -195,7 +196,7 @@ struct
   let widen_with_fct f =
     let product_widen op a b = (* assumes b to be bigger than a *) (* from HS.product_widen *)
       let xs,ys = HS.elements a, HS.elements b in
-      List.concat_map (fun x -> List.map (fun y -> op x y) ys) xs |> fun x -> HS.of_list (List.append x ys)
+      GobList.cartesian_map op xs ys |> fun x -> HS.of_list (List.append x ys)
     in
     product_widen (fun x y -> if SS.leq x y then (SS.widen_with_fct f) x y else SS.bot ())
 
@@ -367,7 +368,7 @@ struct
       let ((sx, kx), (sy, ky)) = (x, y) in
       let x_list = HS.elements sx in
       let y_list = HS.elements sy in
-      let s = List.concat_map (fun xss -> List.map (fun yss -> (xss, yss)) y_list) x_list
+      let s = BatList.cartesian_product x_list y_list (* TODO: GobList.cartesian_filter_map? or just Seq? *)
               |> List.filter (fun (ssx, ssy) -> maps_overlap ssx ssy)
               |> List.map (fun (ssx, ssy) -> f ssx ssy)
               |> HS.of_list
@@ -395,7 +396,7 @@ struct
   let widen_with_fct f (x, kx) (y, ky) =
     let product_widen op a b = (* assumes b to be bigger than a *) (* from HS.product_widen *)
       let xs,ys = HS.elements a, HS.elements b in
-      List.concat_map (fun x -> List.map (op x) ys) xs |> fun x -> HS.of_list (List.append x ys)
+      GobList.cartesian_map op xs ys |> fun x -> HS.of_list (List.append x ys)
     in
     let s = product_widen (fun x y -> if SS.leq x y then (SS.widen_with_fct f) x y else SS.bot ()) x y
     in reduce_key (s, take_some_key kx ky s)

src/cdomains/congruenceClosure.ml

@@ -209,15 +209,12 @@ module Disequalities = struct
     let arg = List.fold_left do_bindings TMap.empty clist in
     (uf, cmap, arg)
 
+  (* TODO: GobList.cartesian_fold_left? *)
   let fold_left2 f acc l1 l2 =
     List.fold_left (
       fun acc x -> List.fold_left (
           fun acc y -> f acc x y) acc l2) acc l1
 
-  let map2 f l1 l2 =
-    let map_f x = List.map (f x) l2 in
-    List.concat_map map_f l1
-
   let map_find_opt (v,r) map =
     let inner_map = TMap.find_opt v map in
     BatOption.map_default (ZMap.find_opt r) None inner_map

src/domain/hoareDomain.ml

@@ -199,10 +199,10 @@ struct
   let reduce s = filter (fun x -> not (exists (le x) s)) s
   let product_bot op a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun x -> List.map (fun y -> op x y) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map op a b |> fun x -> reduce (of_list x)
   let product_widen op a b = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun x -> List.map (fun y -> op x y) ys) xs |> fun x -> reduce (union b (of_list x))
+    GobList.cartesian_map op xs ys |> fun x -> reduce (union b (of_list x))
   let widen = product_widen (fun x y -> if B.leq x y then B.widen x y else B.bot ())
   let narrow = product_bot (fun x y -> if B.leq y x then B.narrow x y else x)
 
@@ -302,18 +302,18 @@ struct
     maximals
   let product_bot op op2 a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> (op x y, op2 xr yr)) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map (fun (x,xr) (y,yr) -> (op x y, op2 xr yr)) a b |> fun x -> reduce (of_list x)
   let product_bot2 op2 a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> op2 (x, xr) (y, yr)) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map op2 a b |> fun x -> reduce (of_list x)
   (* why are type annotations needed for product_widen? *)
   (* TODO: unused now *)
   let product_widen op op2 (a:t) (b:t): t = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> (op x y, op2 xr yr)) ys) xs |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
+    GobList.cartesian_map (fun (x,xr) (y,yr) -> (op x y, op2 xr yr)) xs ys |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
   let product_widen2 op2 (a:t) (b:t): t = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> op2 (x, xr) (y, yr)) ys) xs |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
+    GobList.cartesian_map op2 xs ys |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
   let join a b = join a b |> reduce
   let meet = product_bot SpecD.meet R.inter
   (* let narrow = product_bot (fun x y -> if SpecD.leq y x then SpecD.narrow x y else x) R.narrow *)
@@ -368,6 +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)
   let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None)
 

src/util/std/gobList.ml

@@ -55,6 +55,9 @@ let until_last_with (pred: 'a -> bool) (xs: 'a list) =
   in
   until_last_helper [] [] xs
 
+let cartesian_map f l1 l2 =
+  List.concat_map (fun x -> List.map (f x) l2) l1
+
 
 (** Open this to use applicative functor/monad syntax for {!list}. *)
 module Syntax =