From 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 29 Oct 2015 20:52:32 +0100
Subject: Make the code of compare functions linear in the number of
 constructors.

This scheme has been advised by @gashe on #79.

Interestingly there are several comparison functions in Coq which were already implemented with this scheme.
---
 library/globnames.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/globnames.ml b/library/globnames.ml
index 3befaa9a94..5fdb6115ee 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -112,12 +112,12 @@ let global_ord_gen ord_cst ord_ind ord_cons x y =
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
   | VarRef v1, VarRef v2 -> Id.compare v1 v2
 
-  | VarRef _, (ConstRef _ | IndRef _ | ConstructRef _) -> -1
-  | ConstRef _, VarRef _ -> 1
-  | ConstRef _, (IndRef _ | ConstructRef _) -> -1
-  | IndRef _, (VarRef _ | ConstRef _) -> 1
-  | IndRef _, ConstructRef _ -> -1
-  | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
+  | VarRef _, _ -> -1
+  | _, VarRef _ -> 1
+  | ConstRef _, _ -> -1
+  | _, ConstRef _ -> 1
+  | IndRef _, _ -> -1
+  | _ , IndRef _ -> -1
 
 let global_hash_gen hash_cst hash_ind hash_cons gr =
   let open Hashset.Combine in
-- 
cgit v1.2.3


From 441ea07e3c8ba56b9e7d44e7802246dc06814415 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 30 Oct 2015 10:06:24 +0100
Subject: More uniformity in the style of comparison functions.

---
 library/globnames.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'library')

diff --git a/library/globnames.ml b/library/globnames.ml
index 5fdb6115ee..829e2cefcc 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -107,17 +107,16 @@ let global_eq_gen eq_cst eq_ind eq_cons x y =
 let global_ord_gen ord_cst ord_ind ord_cons x y =
   if x == y then 0
   else match x, y with
-  | ConstRef cx, ConstRef cy -> ord_cst cx cy
-  | IndRef indx, IndRef indy -> ord_ind indx indy
-  | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
   | VarRef v1, VarRef v2 -> Id.compare v1 v2
-
   | VarRef _, _ -> -1
   | _, VarRef _ -> 1
+  | ConstRef cx, ConstRef cy -> ord_cst cx cy
   | ConstRef _, _ -> -1
   | _, ConstRef _ -> 1
+  | IndRef indx, IndRef indy -> ord_ind indx indy
   | IndRef _, _ -> -1
   | _ , IndRef _ -> -1
+  | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
 
 let global_hash_gen hash_cst hash_ind hash_cons gr =
   let open Hashset.Combine in
-- 
cgit v1.2.3