Use stdcompat to support old OCaml version

This PR removes the `compat` modules and some functions in `lists` that
were defined for compatibility purpose with old versions of OCaml.

Use stdcompat to keep this backward compatibility.

src/bin/common/input_frontend.ml

@@ -42,11 +42,11 @@ let register_legacy () =
 
     let parse_file ~content ~format =
       let l = Parsers.parse_problem_as_string ~content ~format in
-      Lists.to_seq l
+      Stdcompat.List.to_seq l
 
     let parse_files ~filename ~preludes =
       let l = Parsers.parse_problem ~filename ~preludes in
-      Lists.to_seq l
+      Stdcompat.List.to_seq l
 
     (* Typechecking *)
 

src/bin/common/parse_command.ml

@@ -660,13 +660,13 @@ let parse_execution_opt =
       else
         match Config.lookup_prelude p with
         | Some p' ->
-          begin if Compat.String.starts_with ~prefix:"b-set-theory" p then
+          begin if Stdcompat.String.starts_with ~prefix:"b-set-theory" p then
               Printer.print_wrn ~header:true
                 "Support for the B set theory is deprecated since version \
                  2.5.0 and may be removed in a future version. If you are \
                  actively using it, please make yourself known to the Alt-Ergo \
                  developers by writing to <[email protected]>."
-            else if Compat.String.starts_with ~prefix:"fpa-theory" p then
+            else if Stdcompat.String.starts_with ~prefix:"fpa-theory" p then
               Printer.print_wrn ~header:true
                 "@[Support for the FPA theory has been integrated as a builtin \
                  theory prelude in version 2.5.0. Please use \

src/bin/common/solving_loop.ml

@@ -181,7 +181,7 @@ let main () =
                 ~format:(Some (Filename.extension filename)))
         in
         let preludes = Options.get_preludes () in
-        Compat.Seq.append theory_preludes @@
+        Stdcompat.Seq.append theory_preludes @@
         I.parse_files ~filename ~preludes
       with
       | Util.Timeout ->

src/lib/dune

@@ -50,7 +50,7 @@
     Emap Gc_debug Hconsing Hstring Iheap Lists Loc
     MyUnix Numbers
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories Compat
+    Theories
   )
 
  (js_of_ocaml

src/lib/reasoners/bitv.ml

@@ -102,7 +102,7 @@ let equal_simple_term eq = equal_alpha_term (equal_simple_term_aux eq)
 
 type 'a abstract =  'a simple_term list
 
-let equal_abstract eq = Lists.equal (equal_simple_term eq)
+let equal_abstract eq = Stdcompat.List.equal (equal_simple_term eq)
 
 (* for the solver *)
 
@@ -172,7 +172,7 @@ module Shostak(X : ALIEN) = struct
           if c2 <> 0 then c2 else X.str_cmp t1 t2
     )
 
-  let compare_abstract = Lists.compare compare_simple_term
+  let compare_abstract = Stdcompat.List.compare compare_simple_term
 
   (* Compare two simple terms. The [equalities_propagation] function below
      requires that : [false ≤ st ≤ true] for all simple terms [st]. *)
@@ -960,9 +960,9 @@ module Shostak(X : ALIEN) = struct
               let _fw = apply_subs subs r in
               let eq (_, l1) (_, l2) =
                 (* [apply_subs] does not change the left-hand sides *)
-                Lists.equal (Lists.equal equal_solver_simple_term) l1 l2
+                Stdcompat.List.(equal (equal equal_solver_simple_term) l1 l2)
               in
-              if Lists.equal eq _bw bw
+              if Stdcompat.List.equal eq _bw bw
               then slice_rec ((t,vls')::bw) _fw
               else slice_rec [] (_bw@((t,vls'):: _fw))
             end

src/lib/reasoners/satml.ml

@@ -756,7 +756,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
             List.fold_left (add_aux env) ma l
 
           | OR l  ->
-            match Lists.find_opt (fun e ->
+            match Stdcompat.List.find_opt (fun e ->
                 let p = get_atom_or_proxy e env.proxies in
                 p.is_true) l
             with

src/lib/structures/symbols.ml

@@ -107,7 +107,7 @@ let var s = Var s
 let int i = Int (Z.of_string i)
 let bitv s =
   let biv =
-    Compat.String.fold_left (fun n c ->
+    Stdcompat.String.fold_left (fun n c ->
         match c with
         | '0' -> Z.(n lsl 1)
         | '1' -> Z.((n lsl 1) lor ~$1)
@@ -135,8 +135,8 @@ let is_internal sy =
   match sy with
   | Name (hs, _, _) ->
     let s = Hstring.view hs in
-    Compat.String.starts_with ~prefix:"." s ||
-    Compat.String.starts_with ~prefix:"@" s
+    Stdcompat.String.starts_with ~prefix:"." s ||
+    Stdcompat.String.starts_with ~prefix:"@" s
   | _ -> false
 
 let underscore =

src/lib/util/lists.ml

@@ -51,36 +51,3 @@ let apply_right f l =
       )([], true) l
   in
   (if same then l else List.rev res), same
-
-let rec find_opt pred l =
-  match l with
-  | [] -> None
-  | e :: r ->
-    if pred e then Some e
-    else find_opt pred r
-
-let to_seq l =
-  let rec aux l () = match l with
-    | [] -> Seq.Nil
-    | x :: tail -> Seq.Cons (x, aux tail)
-  in
-  aux l
-
-(* TODO: This function is supported by the Stdlib from OCaml 4.12. *)
-let rec compare cmp l1 l2 =
-  match l1, l2 with
-  | [], [] -> 0
-  | [], _ -> -1
-  | _, [] -> 1
-  | hd1::tl1, hd2::tl2 ->
-    let c = cmp hd1 hd2 in
-    if c <> 0 then c
-    else
-      compare cmp tl1 tl2
-
-(* List.equal in OCaml 4.12+ *)
-let rec equal eq l1 l2 =
-  match l1, l2 with
-  | [], [] -> true
-  | hd1 :: tl1, hd2 :: tl2 when eq hd1 hd2 -> equal eq tl1 tl2
-  | _ -> false

src/lib/util/lists.mli

@@ -38,9 +38,6 @@
 val is_empty : 'a list -> bool
 (** Is the list empty? *)
 
-val to_seq : 'a list -> 'a Seq.t
-(** Iterate on the list *)
-
 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
@@ -50,17 +47,3 @@ val apply : ('a -> 'a) -> 'a list -> 'a list * bool
 val apply_right : ('a -> 'a) -> ('b * 'a) list -> ('b * 'a) list * bool
 (** similar to function apply, but the elements of the list are
     couples **)
-
-val find_opt : ('a -> bool) -> 'a list -> 'a option
-(** Tries and find the first element of the list satisfying the predicate. *)
-
-val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
-(** [compare cmp l1 l2] compares the lists [l1] and [l2] using the comparison
-    function [cmp] on elements. *)
-
-val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
-(** [equal eq l1 l2] holds when the two input lists have the same length and for
-    each pair of elements [ai], [bi] at the same position in [l1] and [l2]
-    respectively, we have [eq ai bi].
-
-    This is a backport of List.equal from OCaml 4.12.0 *)