Use stdcompat to support old OCaml version (#866)

* Add stdcompat as dependency of alt-ergo-lib

* 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.

alt-ergo-lib.opam

@@ -29,6 +29,7 @@ depends: [
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
   "ppx_deriving"
+  "stdcompat"
 ]
 conflicts: [
   "ppxlib" {< "0.30.0"}

dune-project

@@ -89,6 +89,7 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (camlzip (>= 1.07))
   (odoc :with-doc)
   ppx_deriving
+  stdcompat
  )
  (conflicts
   (ppxlib (< 0.30.0))

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

@@ -666,13 +666,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

@@ -225,7 +225,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

@@ -24,6 +24,7 @@
     dune-build-info
     alt_ergo_prelude
     fmt
+    stdcompat
   )
   (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold))
   (preprocessor_deps (glob_files ../preludes/*.ae))
@@ -49,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

@@ -293,9 +293,9 @@ let int2bv_const n z =
   done;
   !acc
 
-let equal_abstract eq = Lists.equal (equal_simple_term eq)
+let equal_abstract eq = Stdcompat.List.equal (equal_simple_term eq)
 
-let compare_abstract cmp = Lists.compare (compare_simple_term cmp)
+let compare_abstract cmp = Stdcompat.List.compare (compare_simple_term cmp)
 
 let hash_abstract hash =
   List.fold_left (fun acc e -> acc + 19 * hash_simple_term hash e) 19
@@ -1149,9 +1149,10 @@ 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_alpha_term equal_tvar)) l1 l2
+                Stdcompat.List.(equal (equal (equal_alpha_term equal_tvar)))
+                  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 =
@@ -416,7 +416,7 @@ module MakeId(S : sig val prefix : string end) : Id = struct
     in
     fresh_string, reset_fresh_string_cpt
 
-  let is_id = Compat.String.starts_with ~prefix:S.prefix
+  let is_id = Stdcompat.String.starts_with ~prefix:S.prefix
 end
 
 module InternalId = MakeId(struct let prefix = ".k" end)

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 *)