Replace cl_index with cl_typ in coercionops.ml

The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.

3 files changed, 78 insertions, 138 deletions

diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index ac89dfd747..b62dbdb412 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -34,6 +34,31 @@ type cl_info_typ = {
   cl_param : int
 }
 
+let cl_typ_ord t1 t2 = match t1, t2 with
+  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
+  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
+  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
+  | _ -> pervasives_compare t1 t2 (** OK *)
+
+let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
+
+module ClTyp = struct
+  type t = cl_typ
+  let compare = cl_typ_ord
+end
+
+module ClPairOrd =
+struct
+  type t = cl_typ * cl_typ
+  let compare (i1, j1) (i2, j2) =
+    let c = cl_typ_ord i1 i2 in
+    if Int.equal c 0 then cl_typ_ord j1 j2 else c
+end
+
+module ClTypMap = Map.Make(ClTyp)
+module ClPairMap = Map.Make(ClPairOrd)
+
 type coe_typ = GlobRef.t
 
 module CoeTypMap = GlobRef.Map_env
@@ -53,88 +78,26 @@ let coe_info_typ_equal c1 c2 =
     c1.coe_is_projection == c2.coe_is_projection &&
     Int.equal c1.coe_param c2.coe_param
 
-let cl_typ_ord t1 t2 = match t1, t2 with
-  | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
-  | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
-  | _ -> pervasives_compare t1 t2 (** OK *)
-
-module ClTyp = struct
-  type t = cl_typ
-  let compare = cl_typ_ord
-end
-
-module ClTypMap = Map.Make(ClTyp)
-
-let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
-
 type inheritance_path = coe_info_typ list
 
-(* table des classes, des coercions et graphe d'heritage *)
-
-module Bijint :
-sig
-  module Index :
-  sig
-    type t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val print : t -> Pp.t
-  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) Int.Map.t; s : int; inv : int ClTypMap.t }
-  let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
-  let mem y b = ClTypMap.mem y b.inv
-  let map x b = Int.Map.find x b.v
-  let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
-  let add x y b =
-    { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
-  let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
-end
-
-type cl_index = Bijint.Index.t
-
 let init_class_tab =
-  let open Bijint in
+  let open ClTypMap in
   add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
 
 let class_tab =
-  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
+  Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)
 
 let coercion_tab =
   Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
-module ClPairOrd =
-struct
-  type t = cl_index * cl_index
-  let compare (i1, j1) (i2, j2) =
-    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)
-
 let inheritance_graph =
   Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t)
 
 (* ajout de nouveaux "objets" *)
 
 let add_new_class cl s =
-  if not (Bijint.mem cl !class_tab) then
-    class_tab := Bijint.add cl s !class_tab
+  if not (ClTypMap.mem cl !class_tab) then
+    class_tab := ClTypMap.add cl s !class_tab
 
 let add_new_coercion coe s =
   coercion_tab := CoeTypMap.add coe s !coercion_tab
@@ -144,17 +107,9 @@ let add_new_path x y =
 
 (* class_info : cl_typ -> int * cl_info_typ *)
 
-let class_info cl = Bijint.revmap cl !class_tab
+let class_info cl = ClTypMap.find cl !class_tab
 
-let class_exists cl = Bijint.mem cl !class_tab
-
-(* class_info_from_index : int -> cl_typ * cl_info_typ *)
-
-let class_info_from_index i = Bijint.map i !class_tab
-
-let cl_fun_index = fst(class_info CL_FUN)
-
-let cl_sort_index = fst(class_info CL_SORT)
+let class_exists cl = ClTypMap.mem cl !class_tab
 
 let coercion_info coe = CoeTypMap.find coe !coercion_tab
 
@@ -200,20 +155,18 @@ let subst_coe_typ subst t = subst_global_reference subst t
 (* class_of : Term.constr -> int *)
 
 let class_of env sigma t =
-  let (t, n1, i, u, args) =
+  let (t, n1, cl, u, args) =
     try
       let (cl, u, args) = find_class_type env sigma t in
-      let (i, { cl_param = n1 } ) = class_info cl in
-      (t, n1, i, u, args)
+      let { cl_param = n1 } = class_info cl in
+      (t, n1, cl, u, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
       let (cl, u, args) = find_class_type env sigma t in
-      let (i, { cl_param = n1 } ) = class_info cl in
-      (t, n1, i, u, args)
+      let { cl_param = n1 } = class_info cl in
+      (t, n1, cl, u, args)
   in
-  if Int.equal (List.length args) n1 then t, i else raise Not_found
-
-let inductive_class_of ind = fst (class_info (CL_IND ind))
+  if Int.equal (List.length args) n1 then t, cl else raise Not_found
 
 let class_args_of env sigma c = pi3 (find_class_type env sigma c)
 
@@ -238,26 +191,26 @@ let lookup_path_between_class (s,t) =
   ClPairMap.find (s,t) !inheritance_graph
 
 let lookup_path_to_fun_from_class s =
-  lookup_path_between_class (s,cl_fun_index)
+  lookup_path_between_class (s, CL_FUN)
 
 let lookup_path_to_sort_from_class s =
-  lookup_path_between_class (s,cl_sort_index)
+  lookup_path_between_class (s, CL_SORT)
 
 (* advanced path lookup *)
 
 let apply_on_class_of env sigma t cont =
   try
     let (cl,u,args) = find_class_type env sigma t in
-    let (i, { cl_param = n1 } ) = class_info cl in
+    let { cl_param = n1 } = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
-    t, cont i
+    t, cont cl
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
     let (cl, u, args) = find_class_type env sigma t in
-    let (i, { cl_param = n1 } ) = class_info cl in
+    let { cl_param = n1 } = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
-    t, cont i
+    t, cont cl
 
 let lookup_path_between env sigma (s,t) =
   let (s,(t,p)) =
@@ -287,25 +240,25 @@ let get_coercion_constructor env coe =
   | _ -> raise Not_found
 
 let lookup_pattern_path_between env (s,t) =
-  let i = inductive_class_of s in
-  let j = inductive_class_of t in
-  List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
+  List.map (get_coercion_constructor env)
+    (ClPairMap.find (CL_IND s, CL_IND t) !inheritance_graph)
 
 (* rajouter une coercion dans le graphe *)
 
-let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref =
+let path_printer : ((cl_typ * cl_typ) * inheritance_path -> Pp.t) ref =
   ref (fun _ -> str "<a class path>")
 
 let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref =
+let path_comparator :
+  (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref =
   ref (fun _ _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
-let compare_path p q = !path_comparator p q
+let compare_path env sigma cl p q = !path_comparator env sigma cl p q
 
 let warn_ambiguous_path =
   CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
@@ -316,29 +269,29 @@ let warn_ambiguous_path =
          else
            str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
 
-(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
+(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit
                          coercion,source,target *)
 
-let different_class_params env i =
-  let ci = class_info_from_index i in
-    if (snd ci).cl_param > 0 then true
-    else
-      match fst ci with
-      | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
-      | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
-      | _ -> false
+let different_class_params env ci =
+  if (class_info ci).cl_param > 0 then true
+  else
+    match ci with
+    | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
+    | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
+    | _ -> false
 
 let add_coercion_in_graph env sigma (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
-  let ambig_paths =
-    (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
+  let ambig_paths :
+    ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
+    ref [] in
   let try_add_new_path (i,j as ij) p =
     (* If p is a cycle, we check whether p is definitionally an identity
        function or not. If it is not, we report p as an ambiguous inheritance
        path. *)
-    if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
+    if cl_typ_eq i j && not (compare_path env sigma i p []) then
       ambig_paths := (ij,p,[])::!ambig_paths;
-    if not (Bijint.Index.equal i j) || different_class_params env i then
+    if not (cl_typ_eq i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
         (* p has the same source and target classes as an existing path q. We
@@ -362,16 +315,16 @@ let add_coercion_in_graph env sigma (ic,source,target) =
   if try_add_new_path (source,target) [ic] then begin
     ClPairMap.iter
       (fun (s,t) p ->
-         if not (Bijint.Index.equal s t) then begin
-           if Bijint.Index.equal t source then begin
+         if not (cl_typ_eq s t) then begin
+           if cl_typ_eq t source then begin
              try_add_new_path1 (s,target) (p@[ic]);
              ClPairMap.iter
                (fun (u,v) q ->
-                  if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then
+                  if not (cl_typ_eq u v) && cl_typ_eq u target then
                     try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
-           if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
+           if cl_typ_eq s target then try_add_new_path1 (source,t) (ic::p)
          end)
       old_inheritance_graph
   end;
@@ -424,8 +377,6 @@ let add_class env sigma cl =
 let declare_coercion env sigma c =
   let () = add_class env sigma c.coercion_source in
   let () = add_class env sigma c.coercion_target in
-  let is, _ = class_info c.coercion_source in
-  let it, _ = class_info c.coercion_target in
   let xf =
     { coe_value = c.coercion_type;
       coe_local = c.coercion_local;
@@ -434,12 +385,11 @@ let declare_coercion env sigma c =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph env sigma (xf,is,it)
+  add_coercion_in_graph env sigma (xf, c.coercion_source, c.coercion_target)
 
 (* For printing purpose *)
-let pr_cl_index = Bijint.Index.print
-
-let classes () = Bijint.dom !class_tab
+let classes () =
+  List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab [])
 let coercions () =
   List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])
 
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 073500b155..b7c46122a4 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -47,9 +47,6 @@ type coe_info_typ = {
   coe_param : int;
 }
 
-(** [cl_index] is the type of class keys *)
-type cl_index
-
 (** This is the type of paths from a class to another *)
 type inheritance_path = coe_info_typ list
 
@@ -57,20 +54,15 @@ type inheritance_path = coe_info_typ list
 
 val class_exists : cl_typ -> bool
 
-val class_info : cl_typ -> (cl_index * cl_info_typ)
 (** @raise Not_found if this type is not a class *)
-
-val class_info_from_index : cl_index -> cl_typ * cl_info_typ
+val class_info : cl_typ -> cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
 val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list
 
 (** raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> types -> types * cl_index
-
-(** raises [Not_found] if not mapped to a class *)
-val inductive_class_of : inductive -> cl_index
+val class_of : env -> evar_map -> types -> types * cl_typ
 
 val class_args_of : env -> evar_map -> types -> constr list
 
@@ -98,7 +90,7 @@ val coercion_info : coe_typ -> coe_info_typ
 
 (** @raise Not_found in the following functions when no path exists *)
 
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
 val lookup_path_to_fun_from : env -> evar_map -> types ->
@@ -111,16 +103,15 @@ val lookup_pattern_path_between :
 (**/**)
 (* Crade *)
 val install_path_printer :
-  ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+  ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
 val string_of_class : cl_typ -> string
 val pr_class : cl_typ -> Pp.t
-val pr_cl_index : cl_index -> Pp.t
-val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
+val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list
 val classes : unit -> cl_typ list
 val coercions : unit -> coe_info_typ list
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e86a8a28c9..3ccc6ea125 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1398,7 +1398,7 @@ let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let path_convertible env sigma i p q =
+let path_convertible env sigma cl p q =
   let open Coercionops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
@@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q =
           p'
     | [] ->
       (* identity function for the class [i]. *)
-      let cl,params = class_info_from_index i in
+      let params = (class_info cl).cl_param in
       let clty =
         match cl with
         | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
@@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q =
         | CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p))
       in
       let names =
-        List.init params.cl_param
-          (fun n -> Id.of_string ("x" ^ string_of_int n))
+        List.init params (fun n -> Id.of_string ("x" ^ string_of_int n))
       in
       List.fold_right
         (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@