Introduce a dummy name quotient API.

For now it does not do anything but eventually it should be used to replace
the reliance on canonical names for dual kerpairs such as e.g. constants and
inductive types.

2 files changed, 68 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index dec9e1deb8..ac7775b89c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -832,3 +832,36 @@ let set_retroknowledge env r = { env with retroknowledge = r }
 let set_native_symbols env native_symbols = { env with native_symbols }
 let add_native_symbols dir syms env =
   { env with native_symbols = DPmap.add dir syms env.native_symbols }
+
+module QConstant =
+struct
+  type t = Constant.t
+  let equal _env c1 c2 = Constant.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Constant.CanOrd.compare c1 c2
+  let hash _env c = Constant.CanOrd.hash c
+  let canonical _env c = (Constant.canonical c)
+end
+
+module QMutInd =
+struct
+  type t = MutInd.t
+  let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2
+  let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2
+  let hash _env c = MutInd.CanOrd.hash c
+  let canonical _env c = (MutInd.canonical c)
+end
+
+module QProjection =
+struct
+  type t = Projection.t
+  let equal _env c1 c2 = Projection.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Projection.CanOrd.compare c1 c2
+  let hash _env c = Projection.CanOrd.hash c
+  module Repr =
+  struct
+    type t = Projection.Repr.t
+    let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2
+    let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2
+    let hash _env c = Projection.Repr.CanOrd.hash c
+  end
+end
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f443ba38e1..370443857c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -284,6 +284,41 @@ val template_polymorphic_ind : inductive -> env -> bool
 val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
 
+(** {6 Name quotients} *)
+
+module QConstant :
+sig
+  type t = Constant.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  val canonical : env -> t -> KerName.t
+end
+
+module QMutInd :
+sig
+  type t = MutInd.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  val canonical : env -> t -> KerName.t
+end
+
+module QProjection :
+sig
+  type t = Projection.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  module Repr :
+  sig
+    type t = Projection.Repr.t
+    val equal : env -> t -> t -> bool
+    val compare : env -> t -> t -> int
+    val hash : env -> t -> int
+  end
+end
+
 (** {5 Modules } *)
 
 val add_modtype : module_type_body -> env -> env