aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml10
-rw-r--r--plugins/firstorder/sequent.ml14
-rw-r--r--plugins/funind/functional_principles_proofs.ml5
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/mfourier.ml6
-rw-r--r--plugins/micromega/mutils.ml2
-rw-r--r--plugins/micromega/polynomial.ml21
-rw-r--r--plugins/micromega/sos_lib.ml12
-rw-r--r--plugins/rtauto/proof_search.ml2
9 files changed, 39 insertions, 35 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index d618e8426..810e4cf39 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -88,11 +88,11 @@ struct
type t = pa_constructor
let compare { cnode = cnode0; arity = arity0; args = args0 }
{ cnode = cnode1; arity = arity1; args = args1 } =
- let cmp = Pervasives.compare cnode0 cnode1 in
+ let cmp = Int.compare cnode0 cnode1 in
if cmp = 0 then
- let cmp' = Pervasives.compare arity0 arity1 in
+ let cmp' = Int.compare arity0 arity1 in
if cmp' = 0 then
- Pervasives.compare args0 args1
+ List.compare Int.compare args0 args1
else
cmp'
else
@@ -103,9 +103,9 @@ module PafOrd =
struct
type t = pa_fun
let compare { fsym = fsym0; fnargs = fnargs0 } { fsym = fsym1; fnargs = fnargs1 } =
- let cmp = Pervasives.compare fsym0 fsym1 in
+ let cmp = Int.compare fsym0 fsym1 in
if cmp = 0 then
- Pervasives.compare fnargs0 fnargs1
+ Int.compare fnargs0 fnargs1
else
cmp
end
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 8b831d595..72bde18f4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -67,12 +67,14 @@ module Hitem=
struct
type t = h_item
let compare (id1,co1) (id2,co2)=
- (Globnames.RefOrdered.compare
- =? (fun oc1 oc2 ->
- match oc1,oc2 with
- Some (m1,c1),Some (m2,c2) ->
- ((-) =? OrderedConstr.compare) m1 m2 c1 c2
- | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
+ let c = Globnames.RefOrdered.compare id1 id2 in
+ if c = 0 then
+ let cmp (i1, c1) (i2, c2) =
+ let c = Int.compare i1 i2 in
+ if c = 0 then OrderedConstr.compare c1 c2 else c
+ in
+ Option.compare cmp co1 co2
+ else c
end
module CM=Map.Make(OrderedConstr)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 265bd8a8b..f06d8fa53 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -288,11 +288,10 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
(* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
Can be safely replaced by the next comment for Ocaml >= 3.08.4
*)
- let sub' = Int.Map.fold (fun i t acc -> (i,t)::acc) sub [] in
- let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
+ let sub = Int.Map.bindings sub in
List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type))
end_of_type_with_pop
- sub''
+ sub
in
let old_context_length = List.length context + 1 in
let witness_fun =
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 8db2841c2..4f9129396 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -313,7 +313,7 @@ let primal l =
let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in
- let cmp x y = Pervasives.compare (fst x) (fst y) in
+ let cmp x y = Int.compare (fst x) (fst y) in
snd (List.fold_right (fun (p,op) (map,l) ->
let (mp,vect) = vect_of_poly map p in
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index a1f08d568..7d08f2116 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -10,6 +10,8 @@ let from_option = Utils.from_option
let debug = false
type ('a,'b) lr = Inl of 'a | Inr of 'b
+let compare_float (p : float) q = Pervasives.compare p q
+
(** Implementation of intervals *)
module Itv =
struct
@@ -590,7 +592,7 @@ struct
(ISet.fold (fun v (eval,s) -> let ts,vl = abstract_partition v s in
((v,vl)::eval, ts)) v ([],sl)) in
- List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) evals
+ List.sort (fun x y -> compare_float (snd x) (snd y) ) evals
end
@@ -704,7 +706,7 @@ struct
(* pp_list (fun o ((v,eq,_,_),cst) -> Printf.fprintf o "((%i,%a),%i)\n" v pp_vect eq cst) stdout all_costs ; *)
- List.sort (fun x y -> Pervasives.compare (snd x) (snd y) ) all_costs
+ List.sort (fun x y -> Int.compare (snd x) (snd y) ) all_costs
| Some (v,vect, const,prf,_) -> [(v,vect,const,prf),0]
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ae89364e6..ce7496fec 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -393,7 +393,7 @@ struct
let from i = i
let next i = i + 1
let pp o i = output_string o (string_of_int i)
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Int.compare
end
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index f993dc14f..6484e5382 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -44,7 +44,7 @@ end
=
struct
(* A monomial is represented by a multiset of variables *)
- module Map = Map.Make(struct type t = var let compare = Pervasives.compare end)
+ module Map = Map.Make(Int)
open Map
type t = int Map.t
@@ -65,8 +65,8 @@ struct
fun m1 m2 ->
let s1 = sum_degree m1
and s2 = sum_degree m2 in
- if s1 = s2 then Map.compare Pervasives.compare m1 m2
- else Pervasives.compare s1 s2
+ if Int.equal s1 s2 then Map.compare Int.compare m1 m2
+ else Int.compare s1 s2
let is_const m = (m = Map.empty)
@@ -241,8 +241,7 @@ module Vect =
type var = int
type t = (var * num) list
-(** [equal v1 v2 = true] if the vectors are syntactically equal.
- ([num] is not handled by [Pervasives.equal] *)
+(** [equal v1 v2 = true] if the vectors are syntactically equal. *)
let rec equal v1 v2 =
match v1 , v2 with
@@ -250,7 +249,7 @@ module Vect =
| [] , _ -> false
| _::_ , [] -> false
| (i1,n1)::v1 , (i2,n2)::v2 ->
- (i1 = i2) && n1 =/ n2 && equal v1 v2
+ (Int.equal i1 i2) && n1 =/ n2 && equal v1 v2
let hash v =
let rec hash i = function
@@ -294,7 +293,7 @@ module Vect =
match t with
| [] -> cons i (f zero_num) []
| (k,v)::l ->
- match Pervasives.compare i k with
+ match Int.compare i k with
| 0 -> cons k (f v) l
| -1 -> cons i (f zero_num) t
| 1 -> (k,v) ::(update i f l)
@@ -304,7 +303,7 @@ module Vect =
match t with
| [] -> cons i n []
| (k,v)::l ->
- match Pervasives.compare i k with
+ match Int.compare i k with
| 0 -> cons k n l
| -1 -> cons i n t
| 1 -> (k,v) :: (set i n l)
@@ -346,7 +345,7 @@ module Vect =
let compare : t -> t -> int = Utils.Cmp.compare_list (fun x y -> Utils.Cmp.compare_lexical
[
- (fun () -> Pervasives.compare (fst x) (fst y));
+ (fun () -> Int.compare (fst x) (fst y));
(fun () -> compare_num (snd x) (snd y))])
(** [tail v vect] returns
@@ -359,7 +358,7 @@ module Vect =
match vect with
| [] -> None
| (v',vl)::vect' ->
- match Pervasives.compare v' v with
+ match Int.compare v' v with
| 0 -> Some (vl,vect) (* Ok, found *)
| -1 -> tail v vect' (* Might be in the tail *)
| _ -> None (* Hopeless *)
@@ -615,7 +614,7 @@ struct
end
let normalise (v,c) =
- (List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) v , c)
+ (List.sort (fun x y -> Int.compare (fst x) (fst y)) v , c)
let output_mon o (x,v) =
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index efb3f9885..235f9ce9b 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -15,11 +15,13 @@ let debugging = ref false;;
(* Comparisons that are reflexive on NaN and also short-circuiting. *)
(* ------------------------------------------------------------------------- *)
-let (=?) = fun x y -> Pervasives.compare x y = 0;;
-let (<?) = fun x y -> Pervasives.compare x y < 0;;
-let (<=?) = fun x y -> Pervasives.compare x y <= 0;;
-let (>?) = fun x y -> Pervasives.compare x y > 0;;
-let (>=?) = fun x y -> Pervasives.compare x y >= 0;;
+let cmp = Pervasives.compare (** FIXME *)
+
+let (=?) = fun x y -> cmp x y = 0;;
+let (<?) = fun x y -> cmp x y < 0;;
+let (<=?) = fun x y -> cmp x y <= 0;;
+let (>?) = fun x y -> cmp x y > 0;;
+let (>=?) = fun x y -> cmp x y >= 0;;
(* ------------------------------------------------------------------------- *)
(* Combinators. *)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 101fe288b..1ed9b8269 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -69,7 +69,7 @@ module FOrd = struct
| Bot, Bot -> 0
| Bot, _ -> -1
| Atom _, Bot -> 1
- | Atom a1, Atom a2 -> Pervasives.compare a1 a2
+ | Atom a1, Atom a2 -> Int.compare a1 a2
| Atom _, _ -> -1
| Arrow _, (Bot | Atom _) -> 1
| Arrow (f1, g1), Arrow (f2, g2) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 03:02:30 +0000