From 76c005d5d27e140cb9f0b70ed6390e5f291b3b37 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 14 Nov 2008 17:16:44 +0000
Subject: Faster comparison of universes  - compare the integer indexes first,
 in order to avoid    comparing the dirpath part if possible  - use an ad-hoc
 comparison function rather than Pervasives.compare    (slightly faster during
 my tests on the compcert contrib)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.ml | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index a681210acf..1251d09f5d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -43,13 +43,24 @@ type universe_level =
   | Set
   | Level of Names.dir_path * int
 
+(* A specialized comparison function: we compare the [int] part first.
+   This way, most of the time, the [dir_path] part is not considered. *)
+
+let cmp_univ_level u v = match u,v with
+  | Set, Set -> 0
+  | Set, _ -> -1
+  | _, Set -> 1
+  | Level (dp1,i1), Level (dp2,i2) ->
+      let c = compare i1 i2 in
+      if c = 0 then compare dp1 dp2 else c
+
 type universe =
   | Atom of universe_level
   | Max of universe_level list * universe_level list
   
 module UniverseOrdered = struct
   type t = universe_level
-  let compare = Pervasives.compare
+  let compare = cmp_univ_level
 end
 
 let string_of_univ_level = function
@@ -86,7 +97,8 @@ let super = function
    Used to type the products. *)
 let sup u v =
   match u,v with
-    | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[])
+    | Atom u, Atom v ->
+	if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[])
     | u, Max ([],[]) -> u
     | Max ([],[]), v -> v
     | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
-- 
cgit v1.2.3