Get rid of Stdlib.compare and Stdlib.(=)

src/lib/frontend/typechecker.ml

@@ -87,7 +87,7 @@ module Types = struct
       List.for_all2
         (fun pp x ->
            match pp with
-           | PPTvarid (y, _) -> Stdlib.(=) x y
+           | PPTvarid (y, _) -> String.equal x y
            | _ -> false
         ) lpp lvars
     with Invalid_argument _ -> false
@@ -119,7 +119,7 @@ module Types = struct
     | PPTexternal (l, s, loc) ->
       begin
         match rectype with
-        | Some (id, vars, ty) when Stdlib.(=) s id &&
+        | Some (id, vars, ty) when String.equal s id &&
                                    equal_pp_vars l vars -> ty
         | _ ->
           try

src/lib/reasoners/bitv_rel.ml

@@ -164,7 +164,10 @@ end = struct
     | Bor -> Fmt.pf ppf "bvor"
     | Bxor -> Fmt.pf ppf "bvxor"
 
-  let equal_binop : binop -> binop -> bool = Stdlib.(=)
+  let equal_binop op1 op2 =
+    match op1, op2 with
+    | Band, Band | Bor, Bor | Bxor, Bxor -> true
+    | _ -> false
 
   let hash_binop : binop -> int = Hashtbl.hash
 

src/lib/reasoners/fun_sat.ml

@@ -73,7 +73,7 @@ module Make (Th : Theory.S) = struct
         SE.fold
           (fun f mp ->
              let w = var_inc +. try ME.find f mp with Not_found -> 0. in
-             stable := !stable && (Stdlib.compare w 1e100) <= 0;
+             stable := !stable && (Float.compare w 1e100) <= 0;
              ME.add f w mp
           )(Ex.bj_formulas_of expl) mp
       in
@@ -116,9 +116,9 @@ module Make (Th : Theory.S) = struct
       let dec =
         List.fast_sort
           (fun (_, x1, b1) (_, x2, b2) ->
-             let c = Stdlib.compare b2 b1 in
+             let c = Bool.compare b2 b1 in
              if c <> 0 then c
-             else Stdlib.compare x2 x1
+             else Float.compare x2 x1
           )dec
       in
       (*
@@ -1156,7 +1156,7 @@ module Make (Th : Theory.S) = struct
     let ti = Options.get_timelimit_interpretation () in
     if not i || (* not asked to gen a model *)
        !(env.model_gen_phase) ||  (* we timeouted in model-gen-phase *)
-       Stdlib.(=) ti 0. (* no time allocated for extra model search *)
+       Float.equal ti 0. (* no time allocated for extra model search *)
     then
       i_dont_know env (Timeout ProofSearch)
     else

src/lib/reasoners/ite_rel.ml

@@ -51,7 +51,7 @@ module TB =
       type t = E.t * bool
       let compare (a1, b1) (a2, b2) =
         let c = E.compare a1 a2 in
-        if c <> 0 then c else Stdlib.compare b1 b2
+        if c <> 0 then c else Bool.compare b1 b2
     end)
 
 let timer = Timers.M_Ite

src/lib/reasoners/satml.ml

@@ -155,7 +155,7 @@ module Vheap = Heap.Make(struct
 
     (* Note: comparison is flipped because we want maximum weight first and
        [Heap] is a min-heap. *)
-    let compare (a : t) (b : t) = Stdlib.compare b.weight a.weight
+    let compare (a : t) (b : t) = Float.compare b.weight a.weight
   end)
 
 let is_semantic (a : Atom.atom) =
@@ -571,7 +571,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   let var_bump_activity env (v : Atom.var) =
     v.weight <- v.weight +. env.var_inc;
-    if (Stdlib.compare v.weight 1e100) > 0 then begin
+    if Float.compare v.weight 1e100 > 0 then begin
       Vec.iter
         (fun (v : Atom.var) ->
            v.weight <- v.weight *. 1e-100
@@ -584,7 +584,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   let clause_bump_activity env (c : Atom.clause) =
     c.activity <- c.activity +. env.clause_inc;
-    if (Stdlib.compare c.activity 1e20) > 0 then begin
+    if Float.compare c.activity 1e20 > 0 then begin
       Vec.iter (fun (clause : Atom.clause) ->
           clause.activity <- clause.activity *. 1e-20
         ) env.learnts;

src/lib/structures/expr.ml

@@ -1955,9 +1955,9 @@ module Triggers = struct
     | { f = (Name _) as s1; xs=tl1; _ }, { f = (Name _) as s2; xs=tl2; _ } ->
       let l1 = List.map score_term tl1 in
       let l2 = List.map score_term tl2 in
-      let l1 = List.fast_sort Stdlib.compare l1 in
-      let l2 = List.fast_sort Stdlib.compare l2 in
-      let c  = Util.cmp_lists l1 l2 Stdlib.compare in
+      let l1 = List.fast_sort Int.compare l1 in
+      let l2 = List.fast_sort Int.compare l2 in
+      let c  = Util.cmp_lists l1 l2 Int.compare in
       if c <> 0 then c
       else
         let c = Sy.compare s1 s2 in
@@ -1990,15 +1990,15 @@ module Triggers = struct
 
     | { f = Op (Access a1) ; xs=[t1]; _ },
       { f = Op (Access a2) ; xs=[t2]; _ } ->
-      let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *)
+      let c = Hstring.compare a1 a2 in (* should be Hstring.compare *)
       if c<>0 then c else cmp_trig_term t1 t2
 
     | { f = Op (Access _); _ }, _ -> -1
     | _, { f = Op (Access _); _ } -> 1
 
     | { f = Op (Destruct a1) ; xs = [t1]; _ },
       { f = Op (Destruct a2) ; xs = [t2]; _ } ->
-      let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *)
+      let c = Hstring.compare a1 a2 in (* should be Hstring.compare *)
       if c<>0 then c else cmp_trig_term t1 t2
 
     | { f = Op (Destruct _); _ }, _ -> -1
@@ -2013,9 +2013,9 @@ module Triggers = struct
       (* ops that are not infix or prefix *)
       let l1 = List.map score_term tl1 in
       let l2 = List.map score_term tl2 in
-      let l1 = List.fast_sort Stdlib.compare l1 in
-      let l2 = List.fast_sort Stdlib.compare l2 in
-      let c = Util.cmp_lists l1 l2 Stdlib.compare in
+      let l1 = List.fast_sort Int.compare l1 in
+      let l2 = List.fast_sort Int.compare l2 in
+      let c = Util.cmp_lists l1 l2 Int.compare in
       if c <> 0 then c
       else
         let c = Sy.compare s1 s2 in
@@ -2029,9 +2029,9 @@ module Triggers = struct
   let cmp_trig_term_list tl2 tl1 =
     let l1 = List.map score_term tl1 in
     let l2 = List.map score_term tl2 in
-    let l1 = List.rev (List.fast_sort Stdlib.compare l1) in
-    let l2 = List.rev (List.fast_sort Stdlib.compare l2) in
-    let c = Util.cmp_lists l1 l2 Stdlib.compare in
+    let l1 = List.rev (List.fast_sort Int.compare l1) in
+    let l2 = List.rev (List.fast_sort Int.compare l2) in
+    let c = Util.cmp_lists l1 l2 Int.compare in
     if c <> 0 then c else Util.cmp_lists tl1 tl2 cmp_trig_term
 
   let unique_stable_sort =

src/lib/structures/fpa_rounding.ml

@@ -42,6 +42,7 @@ type rounding_mode =
   | Up
   | Down
   | NearestTiesToAway
+[@@deriving ord]
 
 let cstrs =
   [
@@ -215,7 +216,7 @@ module MQ =
         else
           let c = exp1 - exp2 in
           if c <> 0 then c
-          else Stdlib.compare mode1 mode2
+          else compare_rounding_mode mode1 mode2
   end)
 
 let cache = ref MQ.empty

src/lib/structures/fpa_rounding.mli

@@ -40,6 +40,7 @@ type rounding_mode =
   | Up
   | Down
   | NearestTiesToAway
+[@@deriving ord]
 
 (** Equal to ["RoundingMode"], the SMT2 type of rounding modes. *)
 val fpa_rounding_mode_type_name : string

src/lib/structures/profiling.ml

@@ -121,7 +121,7 @@ let get_timers () = (Lazy.force state).timers
 let set_sigprof () =
   let tm =
     let v = Options.get_profiling_period () in
-    if (Stdlib.compare v 0.) > 0 then v else -. v
+    if (Float.compare v 0.) > 0 then v else -. v
   in
   ignore
     (Unix.setitimer Unix.ITIMER_PROF
@@ -643,9 +643,9 @@ let switch fmt =
 let float_print =
   let open Format in
   fun fmt v ->
-    if Stdlib.(=) v 0. then fprintf fmt "--     "
-    else if (Stdlib.compare v 10.) < 0 then fprintf fmt "%0.5f" v
-    else if (Stdlib.compare v 100.) < 0 then fprintf fmt "%0.4f" v
+    if Float.equal v 0. then fprintf fmt "--     "
+    else if Float.compare v 10. < 0 then fprintf fmt "%0.5f" v
+    else if Float.compare v 100. < 0 then fprintf fmt "%0.4f" v
     else fprintf fmt "%0.3f" v
 
 let line_of_module =

src/lib/structures/symbols.ml

@@ -121,8 +121,6 @@ type t =
   | MapsTo of Var.t
   | Let
 
-type s = t
-
 let mangle ns s =
   match ns with
   | User when String.length s > 0 && Char.equal '.' s.[0] -> ".." ^ s
@@ -219,7 +217,7 @@ let compare_forms f1 f2 =
   Util.compare_algebraic f1 f2
     (function
       | F_Unit b1, F_Unit b2
-      | F_Clause b1, F_Clause b2 -> Stdlib.compare b1 b2
+      | F_Clause b1, F_Clause b2 -> Bool.compare b1 b2
       | _, (F_Unit _ | F_Clause _ | F_Lemma | F_Skolem
            | F_Iff | F_Xor) ->
         assert false
@@ -237,10 +235,10 @@ let compare_bounds a b =
   let c = Ty.compare a.sort b.sort in
   if c <> 0 then c
   else
-    let c = Stdlib.compare a.is_open b.is_open in
+    let c = Bool.compare a.is_open b.is_open in
     if c <> 0 then c
     else
-      let c = Stdlib.compare a.is_lower b.is_lower in
+      let c = Bool.compare a.is_lower b.is_lower in
       if c <> 0 then c
       else compare_bounds_kind a.kind b.kind
 
@@ -503,7 +501,7 @@ let is_get f = equal f (Op Get)
 let is_set f = equal f (Op Set)
 
 module Labels = Hashtbl.Make(struct
-    type t = s
+    type nonrec t = t
     let equal = equal
     let hash = hash
   end)
@@ -517,7 +515,7 @@ let label t = try Labels.find labels t with Not_found -> Hstring.empty
 let clear_labels () = Labels.clear labels
 
 module Set : Set.S with type elt = t =
-  Set.Make (struct type t=s let compare=compare end)
+  Set.Make (struct type nonrec t = t let compare=compare end)
 
 module Map : Map.S with type key = t =
-  Map.Make (struct type t = s let compare = compare end)
+  Map.Make (struct type nonrec t = t let compare = compare end)

src/lib/structures/ty.ml

@@ -239,7 +239,7 @@ and shorten_body _ _ =
 
 let rec compare t1 t2 =
   match shorten t1 , shorten t2 with
-  | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Stdlib.compare v1 v2
+  | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Int.compare v1 v2
   | Tvar _, _ -> -1 | _ , Tvar _ -> 1
   | Text(l1, s1) , Text(l2, s2) ->
     let c = Hstring.compare s1 s2 in
@@ -272,8 +272,19 @@ let rec compare t1 t2 =
 
   | Tadt _, _ -> -1 | _ , Tadt _ -> 1
 
-  | t1 , t2 -> Stdlib.compare t1 t2
+  | Tint, Tint -> 0
+  | Tint, _ -> -1 | _, Tint -> 1
 
+  | Treal, Treal -> 0
+  | Treal, _ -> -1 | _, Treal -> 1
+
+  | Tbool, Tbool -> 0
+  | Tbool, _ -> -1 | _, Tbool -> 1
+
+  | Tunit, Tunit -> 0
+  | Tunit, _ -> -1 | _, Tunit -> 1
+
+  | Tbitv sz1, Tbitv sz2 -> Int.compare sz1 sz2
 
 and compare_list l1 l2 = match l1, l2 with
   | [] , [] -> 0
@@ -644,9 +655,9 @@ let instantiate lvar lty ty =
 let union_subst s1 s2 =
   M.fold (fun k x s2 -> M.add k x s2) (M.map (apply_subst s2)  s1) s2
 
-let compare_subst = M.compare Stdlib.compare
+let compare_subst = M.compare compare
 
-let equal_subst = M.equal Stdlib.(=)
+let equal_subst = M.equal equal
 
 module Svty = Util.SI
 

src/lib/structures/xliteral.ml

@@ -143,7 +143,7 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
 
   type t = { at : atom; neg : bool; tpos : int; tneg : int }
 
-  let compare a1 a2 = Stdlib.compare a1.tpos a2.tpos
+  let compare a1 a2 = compare a1.tpos a2.tpos
   let equal a1 a2 = a1.tpos = a2.tpos (* XXX == *)
   let hash a1 = a1.tpos
   let uid a1 = a1.tpos

src/lib/util/numbers.ml

@@ -178,8 +178,8 @@ module Q = struct
     else
       let v = to_float q in
       let w =
-        if (Stdlib.compare v min_float) < 0 then min_float
-        else if (Stdlib.compare v max_float) > 0 then max_float
+        if (Float.compare v min_float) < 0 then min_float
+        else if (Float.compare v max_float) > 0 then max_float
         else v
       in
       let flt = if n = 2 then sqrt w else w ** (1. /. float n) in

src/lib/util/steps.ml

@@ -115,8 +115,7 @@ let incr k =
       naive_steps := !naive_steps + n;
   end;
   if !steps_bound <> -1
-  && ((Stdlib.compare !steps !steps_bound > 0)
-      || (Stdlib.compare !naive_steps !steps_bound > 0)) then
+  && (!steps > !steps_bound || !naive_steps > !steps_bound) then
     begin
       let n =
         if !naive_steps > 0 then !naive_steps

src/lib/util/util.ml

@@ -47,14 +47,10 @@ let () =
       | _ -> None
     )
 
-module MI = Map.Make(struct type t = int
-    let compare (x: int) y = Stdlib.compare x y end)
-
-module SI = Set.Make(struct type t = int
-    let compare (x: int) y = Stdlib.compare x y end)
+module MI = Map.Make (Int)
+module SI = Set.Make (Int)
 
 module MS = Map.Make(String)
-
 module SS = Set.Make(String)