Code factorization in Names.

We introduce a module type not to have to redeclare CanOrd, UserOrd and
SyntacticOrd all over the place.

2 files changed, 63 insertions, 132 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 65c602b863..5b6064fa9f 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -447,6 +447,22 @@ module KNset = KNmap.Set
 
 (** {6 Kernel pairs } *)
 
+module type EqType =
+sig
+  type t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
+module type QNameS =
+sig
+  type t
+  module CanOrd : EqType with type t = t
+  module UserOrd : EqType with type t = t
+  module SyntacticOrd : EqType with type t = t
+end
+
 (** For constant and inductive names, we use a kernel name couple (kn1,kn2)
    where kn1 corresponds to the name used at toplevel (i.e. what the user see)
    and kn2 corresponds to the canonical kernel name i.e. in the environment
@@ -945,6 +961,14 @@ struct
       x == x' || b = b' && Repr.CanOrd.equal c c'
     let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c
   end
+  module UserOrd = struct
+    type nonrec t = t
+    let compare (c, b) (c', b') =
+      if b = b' then Repr.UserOrd.compare c c' else -1
+    let equal (c, b as x) (c', b' as x') =
+      x == x' || b = b' && Repr.UserOrd.equal c c'
+    let hash (c, b) = (if b then 0 else 1) + Repr.UserOrd.hash c
+  end
 
   module Self_Hashcons =
     struct
@@ -1039,22 +1063,27 @@ module GlobRef = struct
   (* By default, [global_reference] are ordered on their canonical part *)
 
   module CanOrd = struct
-    open Constant.CanOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
-      GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2
-    let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2
-    let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
+      GlobRefInternal.global_ord_gen Constant.CanOrd.compare Ind.CanOrd.compare Construct.CanOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.CanOrd.equal Ind.CanOrd.equal Construct.CanOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.CanOrd.hash Ind.CanOrd.hash Construct.CanOrd.hash gr
   end
 
   module UserOrd = struct
-    open Constant.UserOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
-      GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
-    let equal gr1 gr2 =
-      GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
-    let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
+      GlobRefInternal.global_ord_gen Constant.UserOrd.compare Ind.UserOrd.compare Construct.UserOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.UserOrd.equal Ind.UserOrd.equal Construct.UserOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.UserOrd.hash Ind.UserOrd.hash Construct.UserOrd.hash gr
+  end
+
+  module SyntacticOrd = struct
+    type t = GlobRefInternal.t
+    let compare gr1 gr2 =
+      GlobRefInternal.global_ord_gen Constant.SyntacticOrd.compare Ind.SyntacticOrd.compare Construct.SyntacticOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.SyntacticOrd.equal Ind.SyntacticOrd.equal Construct.SyntacticOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.SyntacticOrd.hash Ind.SyntacticOrd.hash Construct.SyntacticOrd.hash gr
   end
 
   module Map = HMap.Make(CanOrd)
diff --git a/kernel/names.mli b/kernel/names.mli
index 1ba928a416..df4ddab3c2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -307,6 +307,24 @@ module KNset  : CSig.SetS with type elt = KerName.t
 module KNpred : Predicate.S with type elt = KerName.t
 module KNmap  : Map.ExtS with type key = KerName.t and module Set := KNset
 
+(** {6 Signature for quotiented names} *)
+
+module type EqType =
+sig
+  type t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
+module type QNameS =
+sig
+  type t
+  module CanOrd : EqType with type t = t
+  module UserOrd : EqType with type t = t
+  module SyntacticOrd : EqType with type t = t
+end
+
 (** {6 Constant Names } *)
 
 module Constant:
@@ -340,26 +358,7 @@ sig
 
   (** Comparisons *)
 
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module UserOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
   val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"]
   (** Default comparison, alias for [CanOrd.equal] *)
@@ -433,26 +432,7 @@ sig
 
   (** Comparisons *)
 
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module UserOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
   val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"]
  (** Default comparison, alias for [CanOrd.equal] *)
@@ -488,26 +468,7 @@ sig
                                     BEWARE: indexing starts from 0. *)
   val modpath : t -> ModPath.t
 
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module UserOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
 end
 
@@ -522,26 +483,7 @@ sig
 
   val modpath : t -> ModPath.t
 
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module UserOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
 end
 
@@ -642,24 +584,7 @@ module Projection : sig
 
     val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
 
-    module SyntacticOrd : sig
-      type nonrec t = t
-      val compare : t -> t -> int
-      val equal : t -> t -> bool
-      val hash : t -> int
-    end
-    module CanOrd : sig
-      type nonrec t = t
-      val compare : t -> t -> int
-      val equal : t -> t -> bool
-      val hash : t -> int
-    end
-    module UserOrd : sig
-      type nonrec t = t
-      val compare : t -> t -> int
-      val equal : t -> t -> bool
-      val hash : t -> int
-    end
+    include QNameS with type t := t
 
     val constant : t -> Constant.t
     (** Don't use this if you don't have to. *)
@@ -689,18 +614,7 @@ module Projection : sig
   val make : Repr.t -> bool -> t
   val repr : t -> Repr.t
 
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
   val constant : t -> Constant.t
   val mind : t -> MutInd.t
@@ -745,19 +659,7 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-
-  module UserOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
   module Set_env : CSig.SetS with type elt = t
   module Map_env : Map.ExtS