Abstracting away coercion indexes in Classops.

1 files changed, 33 insertions, 12 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index fd5081fa3..cd7cd2e0a 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -72,15 +72,34 @@ module IntMap = Map.Make(Int)
 
 let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
 
-type cl_index = int
-
 type coe_index = coe_info_typ
 
 type inheritance_path = coe_index list
 
 (* table des classes, des coercions et graphe d'heritage *)
 
-module Bijint = struct
+module Bijint :
+sig
+  module Index :
+  sig
+    type t
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val print : t -> std_ppcmds
+  end
+  type 'a t
+  val empty : 'a t
+  val mem : cl_typ -> 'a t -> bool
+  val map : Index.t -> 'a t -> cl_typ * 'a
+  val revmap : cl_typ -> 'a t -> Index.t * 'a
+  val add : cl_typ -> 'a -> 'a t -> 'a t
+  val dom : 'a t -> cl_typ list
+end
+=
+struct
+
+  module Index = struct include Int let print = Pp.int end
+
   type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
   let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
   let mem y b = ClTypMap.mem y b.inv
@@ -91,6 +110,8 @@ module Bijint = struct
   let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
 end
 
+type cl_index = Bijint.Index.t
+
 let class_tab =
   ref (Bijint.empty : cl_info_typ Bijint.t)
 
@@ -101,8 +122,8 @@ module ClPairOrd =
 struct
   type t = cl_index * cl_index
   let compare (i1, j1) (i2, j2) =
-    let c = Int.compare i1 i2 in
-    if Int.equal c 0 then Int.compare j1 j2 else c
+    let c = Bijint.Index.compare i1 i2 in
+    if Int.equal c 0 then Bijint.Index.compare j1 j2 else c
 end
 
 module ClPairMap = Map.Make(ClPairOrd)
@@ -290,7 +311,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
 (* rajouter une coercion dans le graphe *)
 
 let path_printer = ref (fun _ -> str "<a class path>"
-                        : (int * int) * inheritance_path -> std_ppcmds)
+                        : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds)
 
 let install_path_printer f = path_printer := f
 
@@ -312,7 +333,7 @@ let add_coercion_in_graph (ic,source,target) =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
     try
-      if Int.equal i j then begin
+      if Bijint.Index.equal i j then begin
 	if different_class_params i j then begin
 	  let _ = lookup_path_between_class ij in
           ambig_paths := (ij,p)::!ambig_paths
@@ -333,16 +354,16 @@ let add_coercion_in_graph (ic,source,target) =
   if try_add_new_path (source,target) [ic] then begin
     ClPairMap.iter
       (fun (s,t) p ->
-         if not (Int.equal s t) then begin
-	   if Int.equal t source then begin
+         if not (Bijint.Index.equal s t) then begin
+	   if Bijint.Index.equal t source then begin
              try_add_new_path1 (s,target) (p@[ic]);
              ClPairMap.iter
 	       (fun (u,v) q ->
-                  if not (Int.equal u v) && Int.equal u target &&  not (List.equal coe_info_typ_equal p q) then
+                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target &&  not (List.equal coe_info_typ_equal p q) then
 		    try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
-           if Int.equal s target then try_add_new_path1 (source,t) (ic::p)
+           if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
 	 end)
       old_inheritance_graph
   end;
@@ -470,7 +491,7 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
 (* For printing purpose *)
 let get_coercion_value v = v.coe_value
 
-let pr_cl_index n = int n
+let pr_cl_index = Bijint.Index.print
 
 let classes () = Bijint.dom !class_tab
 let coercions () =