diff options
-rw-r--r-- | interp/notation.ml | 8 | ||||
-rw-r--r-- | interp/notation_ops.ml | 6 | ||||
-rw-r--r-- | lib/option.ml | 6 | ||||
-rw-r--r-- | lib/option.mli | 3 | ||||
-rw-r--r-- | library/globnames.ml | 3 | ||||
-rw-r--r-- | library/impargs.ml | 9 | ||||
-rw-r--r-- | library/impargs.mli | 2 | ||||
-rw-r--r-- | plugins/cc/ccalgo.ml | 10 | ||||
-rw-r--r-- | plugins/firstorder/sequent.ml | 14 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 5 | ||||
-rw-r--r-- | plugins/micromega/certificate.ml | 2 | ||||
-rw-r--r-- | plugins/micromega/mfourier.ml | 6 | ||||
-rw-r--r-- | plugins/micromega/mutils.ml | 2 | ||||
-rw-r--r-- | plugins/micromega/polynomial.ml | 21 | ||||
-rw-r--r-- | plugins/micromega/sos_lib.ml | 12 | ||||
-rw-r--r-- | plugins/rtauto/proof_search.ml | 2 | ||||
-rw-r--r-- | pretyping/classops.ml | 2 | ||||
-rw-r--r-- | pretyping/coercion.ml | 2 | ||||
-rw-r--r-- | pretyping/recordops.ml | 19 | ||||
-rw-r--r-- | proofs/clenv.ml | 7 | ||||
-rw-r--r-- | tactics/equality.ml | 2 |
21 files changed, 93 insertions, 50 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index a9206b933..867e23395 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -116,6 +116,12 @@ let normalize_scope sc = type scope_elem = Scope of scope_name | SingleNotation of string type scopes = scope_elem list +let scope_eq s1 s2 = match s1, s2 with +| Scope s1, Scope s2 +| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2 +| Scope _, SingleNotation _ +| SingleNotation _, Scope _ -> false + let scope_stack = ref [] let current_scopes () = !scope_stack @@ -136,7 +142,7 @@ let open_scope i (_,(local,op,sc)) = in scope_stack := if op then sc :: !scope_stack - else List.except Pervasives.(=) sc !scope_stack (* FIXME *) + else List.except scope_eq sc !scope_stack let cache_scope o = open_scope 1 o diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 57fc15f8e..bd61ba28f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -512,12 +512,6 @@ let rec alpha_var id1 id2 = function | _::idl -> alpha_var id1 id2 idl | [] -> Id.equal id1 id2 -let compare_var v1 v2 = - match v1, v2 with - | GHole _, _ -> (true,true) - | _, GHole _ -> (false,false) - | _, _ -> (true,Pervasives.(=) v1 v2 (** FIXME *)) - let add_env alp (sigma,sigmalist,sigmabinders) var v = (* Check that no capture of binding variables occur *) if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; diff --git a/lib/option.ml b/lib/option.ml index 02adc6947..1ef45d232 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -29,6 +29,12 @@ let equal f x y = match x, y with | Some x, Some y -> f x y | _, _ -> false +let compare f x y = match x, y with +| None, None -> 0 +| Some x, Some y -> f x y +| None, Some _ -> -1 +| Some _, None -> 1 + exception IsNone (** [get x] returns [y] where [x] is [Some y]. It raises IsNone diff --git a/lib/option.mli b/lib/option.mli index 0b50c588b..d390edb63 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -28,6 +28,9 @@ val is_empty : 'a option -> bool [f] is called. Otherwise it returns [false]. *) val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool +(** Same as [equal], but with comparison. *) +val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int + (** [get x] returns [y] where [x] is [Some y]. It raises IsNone if [x] equals [None]. *) val get : 'a option -> 'a diff --git a/library/globnames.ml b/library/globnames.ml index cb9e4c872..1eb21b6eb 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -132,7 +132,8 @@ module ExtRefOrdered = struct match x, y with | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry | SynDef knx, SynDef kny -> kn_ord knx kny - | _, _ -> Pervasives.compare x y + | TrueGlobal _, SynDef _ -> -1 + | SynDef _, TrueGlobal _ -> 1 end type global_reference_or_constr = diff --git a/library/impargs.ml b/library/impargs.ml index 61ea7a87a..5ec21a3c9 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -119,6 +119,13 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false +let explicitation_eq ex1 ex2 = match ex1, ex2 with +| ExplByPos (i1, id1), ExplByPos (i2, id2) -> + Int.equal i1 i2 && Option.equal Id.equal id1 id2 +| ExplByName id1, ExplByName id2 -> + Id.equal id1 id2 +| _ -> false + type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position @@ -352,7 +359,7 @@ let set_manual_implicits env flags enriching autoimps l = | (Name id,imp)::imps -> let l',imp,m = try - let eq = (Pervasives.(=) : explicitation -> explicitation -> bool) in (* FIXME *) + let eq = explicitation_eq in let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) with Not_found -> diff --git a/library/impargs.mli b/library/impargs.mli index de8d89166..4fb056986 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -143,3 +143,5 @@ type implicit_discharge_request = | ImplInteractive of global_reference * implicits_flags * implicit_interactive_request +val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool +(** Equality on [explicitation]. *) 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) -> diff --git a/pretyping/classops.ml b/pretyping/classops.ml index cd7cd2e0a..3fe3b3ff2 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -59,7 +59,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2 | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2 - | _ -> Pervasives.compare t1 t2 + | _ -> Pervasives.compare t1 t2 (** OK *) module ClTyp = struct type t = cl_typ diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index d2c3282df..1db4119be 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -274,7 +274,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) (* else subco () *) else subco () - | x, y when Pervasives.(=) x y -> (** FIXME *) + | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in let lam_type = Typing.type_of env evm c in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index dfbe9a0b5..9f8ba956a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,6 +144,21 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs +let eq_obj_typ o1 o2 = + Constr.equal o1.o_DEF o2.o_DEF && + Int.equal o1.o_INJ o2.o_INJ && + List.equal Constr.equal o1.o_TABS o2.o_TABS && + List.equal Constr.equal o1.o_TPARAMS o2.o_TPARAMS && + Int.equal o1.o_NPARAMS o2.o_NPARAMS && + List.equal Constr.equal o1.o_TCOMPS o2.o_TCOMPS + +let eq_cs_pattern p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Prod_cs, Prod_cs -> true +| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 +| Default_cs, Default_cs -> true +| _ -> false + let object_table = Summary.ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) ~name:"record-canonical-structs" @@ -221,7 +236,7 @@ let open_canonical_structure i (_,o) = let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let ocs = try Some (List.assoc_f Pervasives.(=) cs_pat l) (* FIXME *) + let ocs = try Some (List.assoc_f eq_cs_pattern cs_pat l) with Not_found -> None in match ocs with | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table; @@ -287,7 +302,7 @@ let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) let lookup_canonical_conversion (proj,pat) = - List.assoc_f Pervasives.(=) pat (Refmap.find proj !object_table) (* FIXME *) + List.assoc_f eq_cs_pattern pat (Refmap.find proj !object_table) let is_open_canonical_projection env sigma (c,args) = try diff --git a/proofs/clenv.ml b/proofs/clenv.ml index a8bbfe127..966d247e0 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -378,8 +378,13 @@ let clenv_independent clenv = let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs +let qhyp_eq h1 h2 = match h1, h2 with +| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2 +| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2 +| _ -> false + let check_bindings bl = - match List.duplicates Pervasives.(=) (List.map pi2 bl) with (* FIXME *) + match List.duplicates qhyp_eq (List.map pi2 bl) with | NamedHyp s :: _ -> errorlabstrm "" (str "The variable " ++ pr_id s ++ diff --git a/tactics/equality.ml b/tactics/equality.ml index d6139f529..1006fd2de 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1126,7 +1126,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in - let sorted_rels = List.sort Pervasives.compare (Int.Set.elements rels) in + let sorted_rels = Int.Set.elements rels in let (tuple,tuplety) = List.fold_left (make_tuple env sigma) (z,zty) sorted_rels in |