Remove polymorphic comparison with lists (OCamlPro#1114)

* Remove polymorphic comparison with lists

Some functions from stdlib's list contains polymorphic comparison. We
cannot use them safely on `Dolmen` identifiers.

This PR replaces these functions by new functions in `Lists` that
use monomorphic comparisons.

src/bin/common/dune

@@ -22,6 +22,11 @@
    Input_frontend
    Signals_profiling
    Solving_loop)
+  (preprocess
+    (pps
+      ppx_deriving.eq
+    )
+  )
 )
 
 (generate_sites_module

src/bin/common/parse_command.ml

@@ -70,7 +70,7 @@ let formats_list =
 
 let format_parser s =
   try
-    Ok (List.assoc s formats_list)
+    Ok (Lists.assoc String.equal s formats_list)
   with
     Not_found ->
     Error (`Msg (Format.sprintf
@@ -170,6 +170,7 @@ module Debug = struct
     | Warnings
     | Commands
     | Optimize
+  [@@deriving eq]
 
   let all = [
     Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
@@ -457,13 +458,13 @@ let mk_theory_opt () no_contracongru
     no_fm no_nla no_tcp no_theory restricted tighten_vars
     _use_fpa (theories)
   =
-  set_no_ac (not (List.mem Theories.AC theories));
+  set_no_ac (not (Lists.mem Theories.equal Theories.AC theories));
   set_no_fm no_fm;
   set_no_nla no_nla;
   set_no_tcp no_tcp;
   set_no_theory no_theory;
   set_restricted restricted;
-  set_disable_adts (not (List.mem Theories.ADT theories));
+  set_disable_adts (not (Lists.mem Theories.equal Theories.ADT theories));
   set_tighten_vars tighten_vars;
   set_no_contracongru no_contracongru;
   set_theory_preludes (Theories.preludes theories);
@@ -1313,7 +1314,7 @@ let parse_theory_opt =
 
   let inequalities_plugin =
     let load_inequalities_plugin debug path =
-      let debug = List.exists (List.mem Debug.Fm) debug in
+      let debug = List.exists (Lists.mem Debug.equal Debug.Fm) debug in
       match path with
       | "" ->
         if debug then
@@ -1449,7 +1450,7 @@ let parse_theory_opt =
           | [], [] -> Ok th
         in
         Result.bind theories @@ fun theories ->
-        if List.mem Theories.(Prelude Fpa) en then
+        if Lists.mem Theories.equal Theories.(Prelude Fpa) en then
           if List.for_all (fun th ->
               match (th : Theories.t) with
               | Prelude Nra | Prelude Ria -> false

src/lib/dune

@@ -30,6 +30,7 @@
     (pps
       ppx_blob
       ppx_deriving.ord
+      ppx_deriving.eq
       ppx_deriving.show
       ppx_deriving.enum
       ppx_deriving.fold

src/lib/reasoners/adt_rel.ml

@@ -211,7 +211,7 @@ let calc_destructor d e uf =
   let r, ex = Uf.find uf e in
   match Th.embed r with
   | Constr { c_args; _ } ->
-    begin match List.assoc d c_args with
+    begin match Lists.assoc Hstring.equal d c_args with
       | v -> Some (v, ex)
       | exception Not_found -> None
     end

src/lib/reasoners/bitv.ml

@@ -552,7 +552,7 @@ module Shostak(X : ALIEN) = struct
 
     exception Valid
 
-    let add elt l = if List.mem elt l then l else elt::l
+    let add elt l = if Lists.mem (equal_signed X.equal) elt l then l else elt::l
 
     let get_vars = List.fold_left
         (fun ac st -> match st.bv with
@@ -587,11 +587,17 @@ module Shostak(X : ALIEN) = struct
        Ensures: there are no duplicates in the result (in particular, [x = y]
                 and [y = x] cannot be both present)
        Ensures: there are no trivial equalities [x = x] in the result. *)
+
+    let equal_pair_simple_term (a1, b1) (a2, b2) =
+      let eq = equal_simple_term X.equal in
+      eq a1 a2 && eq b1 b2
+
     let slice t u  =
       let f_add (s1,s2) acc =
         let b =
           equal_simple_term X.equal s1 s2
-          || List.mem (s1,s2) acc || List.mem (s2,s1) acc
+          || Lists.mem equal_pair_simple_term (s1,s2) acc
+          || Lists.mem equal_pair_simple_term (s2,s1) acc
         in
         if b then acc else (s1,s2)::acc
       in let rec f_rec acc = function

src/lib/reasoners/records.ml

@@ -257,7 +257,7 @@ module Shostak (X : ALIEN) = struct
   let abstract_access field e ty acc =
     let xe = is_mine e in
     let abs_right_xe, acc =
-      try List.assoc xe acc, acc
+      try Lists.assoc X.equal xe acc, acc
       with Not_found ->
         let left_abs_xe2, acc = X.abstract_selectors xe acc in
         match X.type_info left_abs_xe2 with
@@ -364,7 +364,7 @@ module Shostak (X : ALIEN) = struct
 
 
   let orient_solved p v pb =
-    if List.mem p (X.leaves v) then raise Util.Unsolvable;
+    if Lists.mem X.equal p (X.leaves v) then raise Util.Unsolvable;
     Sig.{ pb with sbt = (p,v) :: pb.sbt }
 
   let solve r1 r2 (pb : _ Sig.solve_pb) =

src/lib/util/lists.ml

@@ -32,6 +32,27 @@ let is_empty = function
   | [] -> true
   | _ -> false
 
+let rec mem eq x = function
+  | [] -> false
+  | a::l -> eq a x || mem eq x l
+
+let rec assoc eq x = function
+  | [] -> raise Not_found
+  | (a,b)::l -> if eq a x then b else assoc eq x l
+
+let rec assoc_opt eq x = function
+    [] -> None
+  | (a,b)::l -> if eq a x then Some b else assoc_opt eq x l
+
+let rec mem_assoc eq x = function
+  | [] -> false
+  | (a, _) :: l -> eq a x || mem_assoc eq x l
+
+let rec remove_assoc eq x = function
+  | [] -> []
+  | (a, _ as pair) :: l ->
+    if eq a x then l else pair :: remove_assoc eq x l
+
 let apply f l =
   let res, same =
     List.fold_left

src/lib/util/lists.mli

@@ -38,6 +38,21 @@
 val is_empty : 'a list -> bool
 (** Is the list empty? *)
 
+val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
+(** Similar to [List.mem] but use a monomorphic comparison function. *)
+
+val assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+(** Similar to [List.assoc] but use a monomorphic comparison function. *)
+
+val assoc_opt : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b option
+(** Similar to [List.assoc_opt] but use a monomorphic comparison function. *)
+
+val mem_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> bool
+(** Similar to [List.mem_assoc] but use a monomorphic comparison function. *)
+
+val remove_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> ('a * 'b) list
+(** Similar to [List.remove_assoc] but use a monomorphic comparison function. *)
+
 val apply : ('a -> 'a) -> 'a list -> 'a list * bool
 (** [apply f [a_1; ...; a_n]] returns a couple [[f a_1; ...; f a_n], same]
     same such that: (1) "same" is true if and only if a_i == a_i for

src/lib/util/theories.ml

@@ -14,7 +14,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type prelude = Fpa | Ria | Nra
+type prelude = Fpa | Ria | Nra [@@deriving eq]
 
 let pp_prelude ppf = function
   | Fpa -> Format.fprintf ppf "fpa"
@@ -25,6 +25,7 @@ type t =
   | Prelude of prelude
   | ADT
   | AC
+[@@deriving eq]
 
 let pp ppf = function
   | Prelude p -> pp_prelude ppf p