Get rid of stdcompat (OCamlPro#1191)

* Get rid of `stdcompat`

We do not need to use `stdcompat` because we only need to support few
new functions from `stdlib`. This PR removes the `stdcompat` dependency
and create a new module `compat` which contains all the functions we
need to compile on OCaml 4.08.

I also rename `Lists` to `my_list` and `myUnix` to `my_unix` and now
`my_list` only contains extra functions (which are not part of any
stdlib versions).

CHANGES.md

@@ -91,7 +91,6 @@
    `(alt-ergo plugins)` site to be picked up by Alt-Ergo (#1049).
  - Add a release workflow (#827)
  - Mark the dune.inc file as linguist-generated to avoid huge diffs (#830)
- - Use stdcompat to support older OCaml versions (#866)
  - Use GitHub Actions badges in the README (#882)
  - Use `dune build @check` to build the project (#887)
  - Enable warnings as errors on the CI (#888)

alt-ergo-lib.opam

@@ -30,7 +30,6 @@ depends: [
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
   "ppx_deriving"
-  "stdcompat"
   "qcheck" {with-test}
 ]
 conflicts: [

alt-ergo-lib.opam.locked

@@ -57,7 +57,6 @@ depends: [
   "seq" {= "base"}
   "sexplib0" {= "v0.16.0"}
   "spelll" {= "0.4"}
-  "stdcompat" {= "19"}
   "topkg" {= "1.0.7"}
   "uutf" {= "1.0.3"}
   "yojson" {= "2.1.1"}

default.nix

@@ -24,7 +24,6 @@ let
       dolmen_loop
       camlzip
       ppx_deriving
-      stdcompat
     ];
   };
 

dune-project

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

shell.nix

@@ -40,7 +40,6 @@ pkgs.mkShell {
     ppx_blob
     odoc
     ppx_deriving
-    stdcompat
     landmarks
     landmarks-ppx
     qcheck

src/bin/common/input_frontend.ml

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

src/bin/common/parse_command.ml

@@ -69,7 +69,7 @@ let formats_list =
 
 let format_parser s =
   try
-    Ok (Lists.assoc String.equal s formats_list)
+    Ok (My_list.assoc String.equal s formats_list)
   with
     Not_found ->
     Error (`Msg (Format.sprintf
@@ -462,13 +462,14 @@ let mk_theory_opt () no_contracongru
     no_fm no_nla no_tcp no_theory restricted tighten_vars
     _use_fpa (theories)
   =
-  set_no_ac (not (Lists.mem Theories.equal Theories.AC theories));
+  set_no_ac (not (List.exists (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 (Lists.mem Theories.equal Theories.ADT theories));
+  set_disable_adts
+    (not (List.exists (Theories.equal Theories.ADT) theories));
   set_tighten_vars tighten_vars;
   set_no_contracongru no_contracongru;
   set_theory_preludes (Theories.preludes theories);
@@ -680,13 +681,13 @@ let parse_execution_opt =
       else
         match Config.lookup_prelude p with
         | Some p' ->
-          begin if Stdcompat.String.starts_with ~prefix:"b-set-theory" p then
+          begin if Compat.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 Stdcompat.String.starts_with ~prefix:"fpa-theory" p then
+            else if Compat.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 and is enabled \
@@ -1316,7 +1317,7 @@ let parse_theory_opt =
 
   let inequalities_plugin =
     let load_inequalities_plugin debug path =
-      let debug = List.exists (Lists.mem Debug.equal Debug.Fm) debug in
+      let debug = List.exists (List.exists (Debug.equal Debug.Fm)) debug in
       match path with
       | "" ->
         if debug then

src/bin/common/solving_loop.ml

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

src/bin/text/dune

@@ -3,7 +3,7 @@
 
 (executable
   (name gen_link_flags)
-  (libraries unix fmt stdcompat)
+  (libraries unix fmt)
   (modules gen_link_flags))
 
 (rule

src/bin/text/gen_link_flags.ml

@@ -5,12 +5,21 @@ let pkgconfig lib archive =
 
 let pp_lib ppf s = Fmt.pf ppf "-cclib %s" s
 
+let starts_with ~prefix s =
+  let open String in
+  let len_s = length s
+  and len_pre = length prefix in
+  let rec aux i =
+    if i = len_pre then true
+    else if unsafe_get s i <> unsafe_get prefix i then false
+    else aux (i + 1)
+  in len_s >= len_pre && aux 0
+
 let () =
   let mixed_flags = ["-noautolink"] in
   (* Note: for OCaml 5, use -lcamlstrnat and -lunixnat and mind zlib
      https://github.com/ocaml/ocaml/issues/12562 *)
   let mixed_cclib = [
-    "-lstdcompat_stubs";
     "-lcamlzip";
     "-lzarith";
     "-lcamlstr";
@@ -32,7 +41,7 @@ let () =
                   List.map
                     (fun lib ->
                        let archive =
-                         if Stdcompat.String.starts_with
+                         if starts_with
                              ~prefix:"lib" lib then
                            Fmt.str "%s.a" lib
                          else

src/lib/dune

@@ -24,7 +24,6 @@
     dune-build-info
     alt_ergo_prelude
     fmt
-    stdcompat
   )
   (preprocess
     (pps
@@ -59,10 +58,9 @@
     Parsed Profiling Satml_types Symbols
     Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal
     ; util
-    Emap Gc_debug Hconsing Hstring Heap Lists Loc
-    MyUnix Numbers Uqueue
-    Options Timers Util Vec Version Steps Printer My_zip
-    Theories Nest
+    Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
+    Options Timers Util Vec Version Steps Printer
+    My_zip My_unix My_list Theories Nest Compat
   )
 
  (js_of_ocaml

src/lib/frontend/d_cnf.ml

@@ -1597,7 +1597,7 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
   (* clean trigger:
      remove useless terms in multi-triggers after inlining of lets*)
   let trigger = E.mk_trigger ~user:from_user ~hyp content in
-  if not in_theory && not (Lists.is_empty trigger.semantic) then
+  if not in_theory && not (Compat.List.is_empty trigger.semantic) then
     Errors.typing_error ThSemTriggerError loc;
   E.clean_trigger ~in_theory name trigger
 

src/lib/frontend/typechecker.ml

@@ -142,7 +142,7 @@ module Types = struct
       let ty = Ty.text ty_vars (Uid.of_string id) in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Enum l ->
-      if not (Lists.is_empty ty_vars) then
+      if not (Compat.List.is_empty ty_vars) then
         Errors.typing_error (PolymorphicEnum id) loc;
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
       let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
@@ -202,7 +202,7 @@ module Types = struct
         Errors.typing_error WrongNumberOfLabels loc;
       List.iter
         (fun (lb, _) ->
-           try ignore (Lists.assoc Uid.equal lb l)
+           try ignore (My_list.assoc Uid.equal lb l)
            with Not_found ->
              Errors.typing_error
                (WrongLabel((Hstring.make @@ Uid.show lb), ty)) loc) lbs;
@@ -869,7 +869,7 @@ let rec type_term ?(call_from_type_form=false) env f =
           begin
             try
               TTdot(te, Hstring.make a),
-              Lists.assoc Uid.equal (Uid.of_string a) lbs
+              My_list.assoc Uid.equal (Uid.of_string a) lbs
             with Not_found ->
               let g = Uid.show g in
               Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc

src/lib/index.mld

@@ -148,13 +148,14 @@ AltErgoLib.Util
 AltErgoLib.Heap
 AltErgoLib.Emap
 AltErgoLib.Hstring
-AltErgoLib.Lists
+AltErgoLib.Compat
 AltErgoLib.Gc_debug
 AltErgoLib.Timers
 AltErgoLib.Hconsing
 AltErgoLib.Vec
 AltErgoLib.Loc
-AltErgoLib.MyUnix
+AltErgoLib.My_unix
+AltErgoLib.My_list
 AltErgoLib.Numbers
 }
 

src/lib/reasoners/adt.ml

@@ -416,7 +416,9 @@ module Shostak (X : ALIEN) = struct
   let to_model_term r =
     match embed r with
     | Constr { c_name; c_ty; c_args } ->
-      let args = Lists.try_map (fun (_, arg) -> X.to_model_term arg) c_args in
+      let args =
+        My_list.try_map (fun (_, arg) -> X.to_model_term arg) c_args
+      in
       Option.bind args @@ fun args ->
       Some (E.mk_constr c_name args c_ty)
 

src/lib/reasoners/adt_rel.ml

@@ -177,7 +177,7 @@ module Domains = struct
     match X.type_info r with
     | Tadt (name, args) ->
       let cases = Ty.type_body name args in
-      Lists.is_empty @@ Ty.assoc_destrs c cases
+      Compat.List.is_empty @@ Ty.assoc_destrs c cases
     | _ -> assert false
 
   let internal_update r nd t =
@@ -267,7 +267,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 Lists.assoc Uid.equal d c_args with
+    begin match My_list.assoc Uid.equal d c_args with
       | v -> Some (v, ex)
       | exception Not_found -> None
     end
@@ -511,7 +511,7 @@ let build_constr_eq r c =
            a nonempty context only for interpreted semantic values
            of the `Arith` and `Records` theories. The semantic
            values `cons` never involves such values. *)
-        assert (Lists.is_empty ctx);
+        assert (Compat.List.is_empty ctx);
         let eq = Shostak.L.(view @@ mk_eq r r') in
         Some (eq, E.mk_constr c xs ty)
 
@@ -674,7 +674,7 @@ let split_domain ~for_model env uf =
        a nonempty context only for interpreted semantic values
        of the `Arith` and `Records` theories. The semantic
        values `cons` never involves such values. *)
-    assert (Lists.is_empty ctx);
+    assert (Compat.List.is_empty ctx);
     Some (LR.mkv_eq r nr)
   else
     None

src/lib/reasoners/bitv.ml

@@ -273,9 +273,9 @@ let to_Z_opt r = to_Z_opt_aux Z.zero r
 let int2bv_const n z =
   [ { bv = Cte (Z.extract z 0 n) ; sz = n } ]
 
-let equal_abstract eq = Stdcompat.List.equal (equal_simple_term eq)
+let equal_abstract eq = Compat.List.equal (equal_simple_term eq)
 
-let compare_abstract cmp = Stdcompat.List.compare (compare_simple_term cmp)
+let compare_abstract cmp = Compat.List.compare (compare_simple_term cmp)
 
 let hash_abstract hash =
   List.fold_left (fun acc e -> acc + 19 * hash_simple_term hash e) 19
@@ -557,7 +557,8 @@ module Shostak(X : ALIEN) = struct
 
     exception Valid
 
-    let add elt l = if Lists.mem (equal_signed X.equal) elt l then l else elt::l
+    let add elt l =
+      if List.exists (equal_signed X.equal elt) l then l else elt::l
 
     let get_vars = List.fold_left
         (fun ac st -> match st.bv with
@@ -601,8 +602,8 @@ module Shostak(X : ALIEN) = struct
       let f_add (s1,s2) acc =
         let b =
           equal_simple_term X.equal s1 s2
-          || Lists.mem equal_pair_simple_term (s1,s2) acc
-          || Lists.mem equal_pair_simple_term (s2,s1) acc
+          || List.exists (equal_pair_simple_term (s1,s2)) acc
+          || List.exists (equal_pair_simple_term (s2,s1)) acc
         in
         if b then acc else (s1,s2)::acc
       in let rec f_rec acc = function
@@ -1035,7 +1036,7 @@ module Shostak(X : ALIEN) = struct
            a B-variable has been split into parts below.
            Therefore we assert that the variable is indeed a B variable and that
            list of substitutions for B variables is not empty. *)
-        assert (not (Lists.is_empty (fst subs)));
+        assert (not (Compat.List.is_empty (fst subs)));
         assert (
           match st.bv.defn with Droot { sorte = B; _ } -> true | _ -> false
         );
@@ -1163,17 +1164,17 @@ module Shostak(X : ALIEN) = struct
         |[] -> bw
         |(t,vls)::r ->
           let (vls', csub) = uniforme_slice vls in
-          if Lists.is_empty csub then slice_rec ((t,vls')::bw) r
+          if Compat.List.is_empty csub then slice_rec ((t,vls')::bw) r
           else
             begin
               let _bw = apply_subs csub bw in
               let _fw = apply_subs csub r in
               let eq (_, l1) (_, l2) =
                 (* [apply_subs] does not change the left-hand sides *)
-                Stdcompat.List.(equal (equal (equal_alpha_term equal_tvar)))
+                Compat.List.(equal (equal (equal_alpha_term equal_tvar)))
                   l1 l2
               in
-              if Stdcompat.List.equal eq _bw bw
+              if Compat.List.equal eq _bw bw
               then slice_rec ((t,vls')::bw) _fw
               else slice_rec [] (_bw@((t,vls'):: _fw))
             end
@@ -1243,7 +1244,7 @@ module Shostak(X : ALIEN) = struct
       else begin
         let varsU = get_vars u in
         let varsV = get_vars v in
-        if Lists.is_empty varsU && Lists.is_empty varsV
+        if Compat.List.is_empty varsU && Compat.List.is_empty varsV
         then raise Util.Unsolvable
         else
           begin
@@ -1451,7 +1452,7 @@ module Shostak(X : ALIEN) = struct
       Printer.print_dbg
         ~module_name:"Bitv" ~function_name:"subst"
         "subst %a |-> %a in %a" X.print x X.print subs print biv;
-    if Lists.is_empty biv then is_mine biv
+    if Compat.List.is_empty biv then is_mine biv
     else
       let r = Canon.normalize (subst_rec x subs biv) in
       is_mine r
@@ -1484,7 +1485,7 @@ module Shostak(X : ALIEN) = struct
 
   let abstract_selectors v acc =
     let acc, v =
-      Stdcompat.List.fold_left_map (fun acc bv ->
+      Compat.List.fold_left_map (fun acc bv ->
           match bv with
           | { bv = Cte _ ; _ } -> acc, bv
           | { bv = Other { negated ; value = r } ; sz } ->

src/lib/reasoners/bitv_rel.ml

@@ -1316,7 +1316,7 @@ let assume env uf la =
       let eqs, constraints, domain, int_domain =
         propagate_all eqs constraints domain int_domain
       in
-      if Options.get_debug_bitv () && not (Lists.is_empty eqs) then (
+      if Options.get_debug_bitv () && not (Compat.List.is_empty eqs) then (
         Printer.print_dbg
           ~module_name:"Bitv_rel" ~function_name:"assume"
           "bitlist domain: @[%a@]" Bitlist_domains.pp domain;

src/lib/reasoners/intervals.ml

@@ -1190,5 +1190,5 @@ module DebugExplanations : Explanations with type t = string list = struct
     List.rev_append l1 l2 |> List.sort_uniq String.compare
 
   let compare l1 l2 =
-    Stdcompat.List.compare String.compare l1 l2
+    Compat.List.compare String.compare l1 l2
 end