Removed many calls to OCaml generic equality. This was done by

writing our own comparison functions, and enforcing monomorphization
in many places. This should be more efficient, btw. Still a work
in progress.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 132 insertions, 66 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 251c32ac5..51e264106 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -199,6 +199,15 @@ let unfold_red kn =
 
 type table_key = id_key
 
+module IdKeyHash =
+struct
+  type t = id_key
+  let equal = Names.eq_id_key
+  let hash = Hashtbl.hash
+end
+
+module KeyTable = Hashtbl.Make(IdKeyHash)
+
 let eq_table_key = Names.eq_id_key
 
 type 'a infos = {
@@ -208,13 +217,13 @@ type 'a infos = {
   i_sigma : existential -> constr option;
   i_rels : int * (int * constr) list;
   i_vars : (identifier * constr) list;
-  i_tab : (table_key, 'a) Hashtbl.t }
+  i_tab : 'a KeyTable.t }
 
 let info_flags info = info.i_flags
 
 let ref_value_cache info ref =
   try
-    Some (Hashtbl.find info.i_tab ref)
+    Some (KeyTable.find info.i_tab ref)
   with Not_found ->
   try
     let body =
@@ -225,7 +234,7 @@ let ref_value_cache info ref =
 	| ConstKey cst -> constant_value info.i_env cst
     in
     let v = info.i_repr info body in
-    Hashtbl.add info.i_tab ref v;
+    KeyTable.add info.i_tab ref v;
     Some v
   with
     | Not_found (* List.assoc *)
@@ -262,7 +271,7 @@ let create mk_cl flgs env evars =
     i_sigma = evars;
     i_rels = defined_rels flgs env;
     i_vars = defined_vars flgs env;
-    i_tab = Hashtbl.create 17 }
+    i_tab = KeyTable.create 17 }
 
 
 (**********************************************************************)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8bd0a653c..f2511dbde 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -50,7 +50,7 @@ let empty_delta_resolver = Deltamap.empty
 module MBImap = Map.Make
   (struct
     type t = mod_bound_id
-    let compare = Pervasives.compare
+    let compare = mod_bound_id_ord
    end)
 
 module Umap = struct
diff --git a/kernel/names.ml b/kernel/names.ml
index 520a9aa64..cbd66e03d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -42,10 +42,9 @@ let id_of_string s =
 
 let string_of_id id = String.copy id
 
-let id_ord (x:string) (y:string) =
-  if x == y
-  then 0
-  else Pervasives.compare x y
+let id_ord (x : string) (y : string) =
+  (* String.compare already checks for pointer equality *)
+  String.compare x y
 
 module IdOrdered =
   struct
@@ -81,6 +80,17 @@ type dir_path = module_ident list
 
 module ModIdmap = Idmap
 
+let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
+  if p1 == p2 then 0
+  else begin match p1, p2 with
+  | [], [] -> 0
+  | [], _ -> -1
+  | _, [] -> 1
+  | id1 :: p1, id2 :: p2 ->
+    let c = id_ord id1 id2 in
+    if c <> 0 then c else dir_path_ord p1 p2
+  end
+
 let make_dirpath x = x
 let repr_dirpath x = x
 
@@ -102,15 +112,28 @@ let make_uid dir s = incr u_number;(!u_number,s,dir)
 let string_of_uid (i,s,p) =
   string_of_dirpath p ^"."^s
 
-module Umap = Map.Make(struct
-			 type t = uniq_ident
-			 let compare x y =
-                           if x == y
-                           then 0
-                           else Pervasives.compare x y
-		       end)
+let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
+  if x == y then 0
+  else match (x, y) with
+  | (nl, idl, dpl), (nr, idr, dpr) ->
+    let ans = nl - nr in
+    if ans <> 0 then ans
+    else
+      let ans = id_ord idl idr in
+      if ans <> 0 then ans
+      else
+        dir_path_ord dpl dpr
+
+module UOrdered =
+struct
+  type t = uniq_ident
+  let compare = uniq_ident_ord
+end
+
+module Umap = Map.Make(UOrdered)
 
 type mod_bound_id = uniq_ident
+let mod_bound_id_ord = uniq_ident_ord
 let make_mbid = make_uid
 let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
@@ -150,14 +173,19 @@ let rec string_of_mp = function
 (** we compare labels first if both are MPdots *)
 let rec mp_ord mp1 mp2 =
   if mp1 == mp2 then 0
-  else match (mp1,mp2) with
-    MPdot(mp1,l1), MPdot(mp2,l2) ->
-      let c = Pervasives.compare l1 l2 in
-	if c<>0 then
-	  c
-	else
-	  mp_ord mp1 mp2
-  |  _,_ -> Pervasives.compare mp1 mp2
+  else match (mp1, mp2) with
+  | MPfile p1, MPfile p2 ->
+    dir_path_ord p1 p2
+  | MPbound id1, MPbound id2 ->
+    uniq_ident_ord id1 id2
+  | MPdot (mp1, l1), MPdot (mp2, l2) ->
+      let c = String.compare l1 l2 in
+        if c <> 0 then c
+        else mp_ord mp1 mp2
+  | MPfile _, _ -> -1
+  | MPbound _, MPfile _ -> 1
+  | MPbound _, MPdot _ -> -1
+  | MPdot _, _ -> 1
 
 module MPord = struct
   type t = module_path
@@ -192,21 +220,17 @@ let string_of_kn (mp,dir,l) =
 
 let pr_kn kn = str (string_of_kn kn)
 
-let kn_ord kn1 kn2 =
-  if kn1 == kn2 then
-    0
+let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) =
+  if kn1 == kn2 then 0
   else
-    let mp1,dir1,l1 = kn1 in
-    let mp2,dir2,l2 = kn2 in
-    let c = Pervasives.compare l1 l2 in
-      if c <> 0 then
-	c
+    let mp1, dir1, l1 = kn1 in
+    let mp2, dir2, l2 = kn2 in
+    let c = String.compare l1 l2 in
+      if c <> 0 then c
       else
-	let c = Pervasives.compare dir1 dir2 in
-	  if c<>0 then
-	    c
-	  else
-	    MPord.compare mp1 mp2
+        let c = dir_path_ord dir1 dir2 in
+        if c <> 0 then c
+        else MPord.compare mp1 mp2
 
 module KNord = struct
   type t = kernel_name
@@ -392,7 +416,7 @@ module Huniqid = Hashcons.Make(
     let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
       (x == y) ||
-      (n1 = n2 && s1 == s2 && dir1 == dir2)
+      (n1 - n2 = 0 && s1 == s2 && dir1 == dir2)
     let hash = Hashtbl.hash
   end)
 
@@ -454,7 +478,7 @@ module Hconstruct = Hashcons.Make(
     type t = constructor
     type u = inductive -> inductive
     let hashcons hind (ind, j) = (hind ind, j)
-    let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
+    let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && (j1 - j2 = 0)
     let hash = Hashtbl.hash
   end)
 
@@ -493,11 +517,17 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
 type id_key = inv_rel_key tableKey
 
 let eq_id_key ik1 ik2 =
-  (ik1 == ik2) ||
-  (match ik1,ik2 with
-    ConstKey (_,kn1),
-      ConstKey (_,kn2) -> kn1=kn2
-    | a,b -> a=b)
+  if ik1 == ik2 then true
+  else match ik1,ik2 with
+  | ConstKey (u1, kn1), ConstKey (u2, kn2) ->
+    let ans = (kn_ord u1 u2 = 0) in
+    if ans then kn_ord kn1 kn2 = 0
+    else ans
+  | VarKey id1, VarKey id2 ->
+    id_ord id1 id2 = 0
+  | RelKey k1, RelKey k2 ->
+    k1 - k2 = 0
+  | _ -> false
 
 let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
 let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index bb6696389..5c2bd5b0a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -40,6 +40,8 @@ module ModIdmap : Map.S with type key = module_ident
 
 type dir_path
 
+val dir_path_ord : dir_path -> dir_path -> int
+
 (** Inner modules idents on top of list (to improve sharing).
    For instance: A.B.C is ["C";"B";"A"] *)
 val make_dirpath : module_ident list -> dir_path
@@ -68,6 +70,8 @@ module Labmap : Map.S with type key = label
 
 type mod_bound_id
 
+val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+
 (** The first argument is a file name - to prevent conflict between
    different files *)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 39cb6bc10..635991494 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -53,11 +53,12 @@ module UniverseLevel = struct
     | Level (i1, dp1), Level (i2, dp2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
-      else compare dp1 dp2)
+      else Names.dir_path_ord dp1 dp2)
 
   let equal u v = match u,v with
     | Set, Set -> true
-    | Level (i1, dp1), Level (i2, dp2) -> i1 = i2 && dp1 = dp2
+    | Level (i1, dp1), Level (i2, dp2) ->
+      i1 = i2 && (Names.dir_path_ord dp1 dp2 = 0)
     | _ -> false
 
   let to_string = function
@@ -272,6 +273,15 @@ let between g arcu arcv =
 type constraint_type = Lt | Le | Eq
 type explanation = (constraint_type * universe) list
 
+let constraint_type_ord c1 c2 = match c1, c2 with
+| Lt, Lt -> 0
+| Lt, _ -> -1
+| Le, Lt -> 1
+| Le, Le -> 0
+| Le, Eq -> -1
+| Eq, Eq -> 0
+| Eq, _ -> 1
+
 (* Assuming the current universe has been reached by [p] and [l]
    correspond to the universes in (direct) relation [rel] with it,
    make a list of canonical universe, updating the relation with
@@ -527,7 +537,7 @@ module Constraint = Set.Make(
   struct
     type t = univ_constraint
     let compare (u,c,v) (u',c',v') =
-      let i = Pervasives.compare c c' in
+      let i = constraint_type_ord c c' in
       if i <> 0 then i
       else
 	let i' = UniverseLevel.compare u u' in
diff --git a/lib/flags.ml b/lib/flags.ml
index 2b10125a0..4ec378793 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -101,7 +101,13 @@ let print_hyps_limit () = !print_hyps_limit
 (* A list of the areas of the system where "unsafe" operation
  * has been requested *)
 
-module Stringset = Set.Make(struct type t = string let compare = compare end)
+module StringOrd =
+struct
+  type t = string
+  let compare (x : t) (y : t) = String.compare x y
+end
+
+module Stringset = Set.Make(StringOrd)
 
 let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 8daeec944..745169dc0 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -132,8 +132,7 @@ module Hstring = Make(
     type t = string
     type u = unit
     let hashcons () s =(* incr accesstr;*) s
-    let equal s1 s2 =(* incr comparaisonstr;
-      if*) s1=s2(* then (incr successtr; true) else false*)
+    let equal (s1 : t) (s2 : t) = s1 = s2
     let hash = Hashtbl.hash
   end)
 
diff --git a/lib/hashset.ml b/lib/hashset.ml
index fd3d1a554..6f62e1a90 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -79,6 +79,8 @@ module Make (E : EqType) =
     if i >= Weak.length b then accu else
     count_bucket (i+1) b (accu + (if Weak.check b i then 1 else 0))
 
+  let min x y = if x - y < 0 then x else y
+
   let next_sz n = min (3 * n / 2 + 3) Sys.max_array_length
   let prev_sz n = ((n - 3) * 2 + 2) / 3
 
diff --git a/lib/util.ml b/lib/util.ml
index af3b13fa7..6a0ba470a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -137,9 +137,14 @@ let subst_command_placeholder s t =
   done;
   Buffer.contents buff
 
-module Stringset = Set.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module StringOrd =
+struct
+  type t = string
+  external compare : string -> string -> int = "caml_string_compare"
+end
 
-module Stringmap = Map.Make(struct type t = string let compare (x:t) (y:t) = compare x y end)
+module Stringset = Set.Make(StringOrd)
+module Stringmap = Map.Make(StringOrd)
 
 (* Lists *)
 
@@ -202,9 +207,14 @@ let delayed_force f = f ()
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
-module Intset = Set.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module IntOrd =
+struct
+  type t  = int
+  external compare : int -> int -> int = "caml_int_compare"
+end
 
-module Intmap = Map.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
+module Intset = Set.Make(IntOrd)
+module Intmap = Map.Make(IntOrd)
 
 (*s interruption *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 3555766f8..197588f53 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -69,8 +69,8 @@ let dirpath_of_string s =
 let string_of_dirpath = Names.string_of_dirpath
 
 
-module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
-module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
+module Dirset = Set.Make(struct type t = dir_path let compare = dir_path_ord end)
+module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end)
 
 (*s Section paths are absolute names *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index dab4ee9c7..d696db3e7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -568,7 +568,7 @@ let undefined_metas evd =
     | (n,Cltyp (_,typ))  -> Some n
   in
   let m = List.map_filter filter (meta_list evd) in
-  List.sort Pervasives.compare m
+  List.sort (-) m
 
 let metas_of evd =
   List.map (function
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f32eb0879..fdc7875d7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,6 +114,8 @@ module MethodsDnet : Term_dnet.S
   = Term_dnet.Make
   (struct
      type t = global_reference * Evd.evar * Evd.evar_map
+     (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to 
+         do w.r.t. evar maps. *)
      let compare = Pervasives.compare
      let subst = subst_id
      let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e25a880f8..447ee8e3b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -103,13 +103,9 @@ let extract_instance_status = function
   | CUMUL -> add_type_status (IsSubType, IsSuperType)
   | CONV -> add_type_status (Conv, Conv)
 
-let rec assoc_pair x = function
-    [] -> raise Not_found
-  | (a,b,_)::l -> if compare a x = 0 then b else assoc_pair x l
-
 let rec subst_meta_instances bl c =
   match kind_of_term c with
-    | Meta i -> (try assoc_pair i bl with Not_found -> c)
+    | Meta i -> (try List.assoc_snd_in_triple i bl with Not_found -> c)
     | _ -> map_constr (subst_meta_instances bl) c
 
 let pose_all_metas_as_evars env evd t =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6a96d5bb7..e1a4d4f36 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -41,9 +41,7 @@ module HintIdent =
 struct
   type t = int * rew_rule
 
-  let compare (i,t) (i',t') =
-    Pervasives.compare i i'
-(*     Pervasives.compare t.rew_lemma t'.rew_lemma *)
+  let compare (i, t) (j, t') = i - j
 
   let subst s (i,t) = (i,subst_hint s t)
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 775212eda..6277faf27 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -428,7 +428,7 @@ let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
-module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
+module ProgMap = Map.Make(struct type t = identifier let compare = id_ord end)
 
 let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)