From 48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
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 ++++++------
 printing/printer.ml  | 23 +++++++++++------------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/library/globnames.ml b/library/globnames.ml
index 3befaa9a9..5fdb6115e 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
diff --git a/printing/printer.ml b/printing/printer.ml
index 18e490225..12782a428 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -724,18 +724,17 @@ module OrderedContextObject =
 struct
   type t = context_object
   let compare x y =
-      match x , y with
-      | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
-      | Opaque k1 , Opaque k2 -> con_ord k1 k2
-      | Transparent k1 , Transparent k2 -> con_ord k1 k2
-      | Axiom _ , Variable _ -> 1
-      | Opaque _ , Variable _
-      | Opaque _ , Axiom _ -> 1
-      | Transparent _ , Variable _
-      | Transparent _ , Axiom _
-      | Transparent _ , Opaque _ -> 1
-      | _ , _ -> -1
+    match x , y with
+    | Variable i1 , Variable i2 -> Id.compare i1 i2
+    | Variable _ , _ -> -1
+    | _ , Variable _ -> 1
+    | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+    | Axiom _ , _ -> -1
+    | _ , Axiom _ -> 1
+    | Opaque k1 , Opaque k2 -> con_ord k1 k2
+    | Opaque _ , _ -> -1
+    | _ , Opaque _ -> 1
+    | Transparent k1 , Transparent k2 -> con_ord k1 k2
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
-- 
cgit v1.2.3


From 441ea07e3c8ba56b9e7d44e7802246dc06814415 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
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(-)

diff --git a/library/globnames.ml b/library/globnames.ml
index 5fdb6115e..829e2cefc 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