Tables logarithmiques pour les coercions + nettoyage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4103 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 95 insertions, 134 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 7aa435984..f781ff755 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -439,43 +439,32 @@ open Classops
 
 let print_coercion_value v = prterm (get_coercion_value v)
 
-let print_index_coercion c = 
-  let _,v = coercion_info_from_index c in
-  print_coercion_value v
-
 let print_class i =
   let cl,_ = class_info_from_index i in
-  (str (string_of_class cl))
+  pr_class cl
   
 let print_path ((i,j),p) = 
   (str"[" ++ 
-     prlist_with_sep (fun () -> (str"; "))
-       (fun c ->  print_index_coercion c) p ++
+     prlist_with_sep pr_semicolon print_coercion_value p ++
      str"] : " ++ print_class i ++ str" >-> " ++
      print_class j)
 
 let _ = Classops.install_path_printer print_path
 
 let print_graph () = 
-  (prlist_with_sep pr_fnl print_path (inheritance_graph()))
+  prlist_with_sep pr_fnl print_path (inheritance_graph())
 
 let print_classes () = 
-  (prlist_with_sep pr_spc
-       (fun (_,(cl,x)) -> 
-          (str (string_of_class cl)
-	       (* ++ str(string_of_strength x.cl_strength) *))) 
-       (classes()))
+  prlist_with_sep pr_spc pr_class (classes())
 
 let print_coercions () = 
-  (prlist_with_sep pr_spc
-       (fun (_,(_,v)) -> (print_coercion_value v)) (coercions()))
+  prlist_with_sep pr_spc print_coercion_value (coercions())
   
 let index_of_class cl =
   try 
     fst (class_info cl)
   with _ -> 
-    errorlabstrm "index_of_class"
-      (str(string_of_class cl) ++ str" is not a defined class")
+    errorlabstrm "index_of_class" (pr_class cl ++ str" is not a defined class")
 
 let print_path_between cls clt = 
   let i = index_of_class cls in
@@ -485,8 +474,7 @@ let print_path_between cls clt =
       lookup_path_between (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
-        (str"No path between " ++str(string_of_class cls) ++ 
-	   str" and " ++str(string_of_class clt))
+        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt)
   in
   print_path ((i,j),p)
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index aa2c6c1db..3bc1292ea 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -49,21 +49,37 @@ type coe_info_typ = {
   coe_param : int }
 
 type cl_index = int
-type coe_index = int
 
-type inheritance_path = coe_index list
+type coe_index = coe_info_typ
 
+type inheritance_path = coe_index list
 
 (* table des classes, des coercions et graphe d'heritage *)
 
+module Bijint = struct
+  type ('a,'b) t = { v : ('a * 'b) array; s : int; inv : ('a,int) Gmap.t }
+  let empty = { v = [||]; s = 0; inv = Gmap.empty }
+  let mem y b = Gmap.mem y b.inv
+  let map x b = if 0 <= x & x < b.s then b.v.(x) else raise Not_found
+  let revmap y b = let n = Gmap.find y b.inv in (n, snd (b.v.(n)))
+  let add x y b =
+    if mem x b then failwith "Bijint.add";
+    let v =
+      if b.s = Array.length b.v then
+	(let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
+      else b.v in
+    v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv }
+  let dom b = Gmap.dom b.inv
+end
+
 let class_tab =
-  (ref [] : (cl_index * (cl_typ * cl_info_typ)) list ref)
+  ref (Bijint.empty : (cl_typ, cl_info_typ) Bijint.t)
 
 let coercion_tab =
-  (ref [] : (coe_index * (coe_typ * coe_info_typ)) list ref)
+  ref (Gmap.empty : (coe_typ, coe_info_typ) Gmap.t)
 
 let inheritance_graph =
-  (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) 
+  ref (Gmap.empty : (cl_index * cl_index, inheritance_path) Gmap.t)
 
 let freeze () = (!class_tab, !coercion_tab, !inheritance_graph)
 
@@ -74,79 +90,44 @@ let unfreeze (fcl,fco,fig) =
 
 (* ajout de nouveaux "objets" *)
 
-let newNum_class = 
- let num = ref 0 in
- function () -> (num:=!num+1;!num)
-
-let newNum_coercion = 
- let num = ref 0 in
- function () -> (num:=!num+1;!num)
-
-let add_new_class_num (n,(cl,s)) = 
-  class_tab := (n,(cl,s))::(!class_tab)
-
-let add_new_class (cl,s) = 
-  add_new_class_num (newNum_class(),(cl,s))
-
-let add_new_coercion_num (n,(coe,s)) = 
-  coercion_tab := (n,(coe,s))::(!coercion_tab)
+let add_new_class cl s = 
+  class_tab := Bijint.add cl s !class_tab
 
-let add_new_coercion (coe,s) = 
-  let n = newNum_coercion() in 
-  add_new_coercion_num (n,(coe,s));n
+let add_new_coercion coe s = 
+  coercion_tab := Gmap.add coe s !coercion_tab
 
-let add_new_path x =
-  inheritance_graph := x::!inheritance_graph
+let add_new_path x y =
+  inheritance_graph := Gmap.add x y !inheritance_graph
 
 let init () =
-  class_tab:= []; 
-  add_new_class (CL_FUN,  { cl_param = 0; cl_strength = Global });
-  add_new_class (CL_SORT, { cl_param = 0; cl_strength = Global });
-  coercion_tab:= [];
-  inheritance_graph:= []
+  class_tab:= Bijint.empty; 
+  add_new_class CL_FUN  { cl_param = 0; cl_strength = Global };
+  add_new_class CL_SORT { cl_param = 0; cl_strength = Global };
+  coercion_tab:= Gmap.empty;
+  inheritance_graph:= Gmap.empty
 
 let _ = init()
 
-(* fonction de recherche *)
-
-let search_info x l = 
-  let rec aux = function 
-    | [] -> raise Not_found
-    | (n,(x1,r))::l -> if x=x1 then (n,r) else aux l
-  in 
-  aux l
-
 (* class_info : cl_typ -> int * cl_info_typ *)
 
-let class_info cl = search_info cl (!class_tab)
+let class_info cl = Bijint.revmap cl !class_tab
 
-let class_exists cl =
-  try let _ = class_info cl in true
-  with Not_found -> false
+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 = List.assoc i !class_tab
-
-(* coercion_info : coe_typ -> int * coe_info_typ *)
+let class_info_from_index i = Bijint.map i !class_tab
 
-let coercion_info coe = search_info coe !coercion_tab
+(* coercion_info : coe_typ -> coe_info_typ *)
 
-let coercion_exists coe =
-  try let _ = coercion_info coe in true
-  with Not_found -> false
+let coercion_info coe = Gmap.find coe !coercion_tab
 
-let coe_of_reference x = x
+let coercion_exists coe = Gmap.mem coe !coercion_tab
 
 let coercion_params coe_info = coe_info.coe_param
 
-(* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
-
-let coercion_info_from_index i = 
-  List.assoc i !coercion_tab
-
 let lookup_path_between (s,t) =
-  List.assoc (s,t) !inheritance_graph
+  Gmap.find (s,t) !inheritance_graph
 
 let lookup_path_to_fun_from s = 
   lookup_path_between (s,fst(class_info CL_FUN))
@@ -155,10 +136,9 @@ let lookup_path_to_sort_from s =
   lookup_path_between (s,fst(class_info CL_SORT))
 
 let lookup_pattern_path_between (s,t) =
-  let l = List.assoc (s,t) !inheritance_graph in
+  let l = Gmap.find (s,t) !inheritance_graph in
   List.map  
-    (fun i ->
-       let coe = snd (coercion_info_from_index i) in
+    (fun coe ->
        let c, _ =
 	 Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty 
 	   coe.coe_value.uj_val
@@ -195,7 +175,7 @@ let subst_coe_info subst info =
 (*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
  val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
 
-let cache_class (_,x) = add_new_class x
+let cache_class (_,(x,y)) = add_new_class x y
 
 let subst_class (_,subst,(ct,ci as obj)) = 
   let ct' = subst_cl_typ subst ct in
@@ -269,11 +249,11 @@ let string_of_class = function
   | CL_SECVAR sp ->
       string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp))
 
+let pr_class x = str (string_of_class x)
+
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
-let coercion_value i = 
-  let { coe_value = j; coe_is_identity = b } = snd (coercion_info_from_index i)
-  in (j,b)
+let coercion_value { coe_value = j; coe_is_identity = b } = (j,b)
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
@@ -299,66 +279,64 @@ let add_coercion_in_graph (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
-  let try_add_new_path (p,i,j) =
+  let try_add_new_path (i,j as ij) p =
     try 
       if i=j then begin
 	if different_class_params i j then begin
-	  let _ = lookup_path_between (i,j) in
-          ambig_paths := ((i,j),p)::!ambig_paths
+	  let _ = lookup_path_between ij in
+          ambig_paths := (ij,p)::!ambig_paths
 	end
       end else begin
         let _ = lookup_path_between (i,j) in
-        ambig_paths := ((i,j),p)::!ambig_paths
+        ambig_paths := (ij,p)::!ambig_paths
       end;
       false
     with Not_found -> begin
-      add_new_path ((i,j),p);
+      add_new_path ij p;
       true
     end
   in
-  let try_add_new_path1 (p,i,j) = 
-    let _ = try_add_new_path (p,i,j) in () 
+  let try_add_new_path1 ij p = 
+    let _ = try_add_new_path ij p in () 
   in
-  if try_add_new_path ([ic],source,target) then begin
-    List.iter 
-      (fun ((s,t),p) ->
+  if try_add_new_path (source,target) [ic] then begin
+    Gmap.iter 
+      (fun (s,t) p ->
          if s<>t then begin
 	   if t = source then begin
-             try_add_new_path1 (p @ [ ic ],s,target);
-             List.iter 
-	       (fun ((u,v),q) ->
+             try_add_new_path1 (s,target) (p@[ic]);
+             Gmap.iter
+	       (fun (u,v) q ->
                   if u<>v & (u = target) & (p <> q) then 
-		    try_add_new_path1 (p @ [ ic ] @ q,s,v))
+		    try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
-           if s = target then try_add_new_path1 (ic::p,source,t)
+           if s = target then try_add_new_path1 (source,t) (ic::p)
 	 end)
       old_inheritance_graph 
   end;
   if (!ambig_paths <> []) && is_verbose () then 
     ppnl (message_ambig !ambig_paths)
 
-type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
+type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
 
-let cache_coercion (_,((coe,xf),cls,clt)) =
+let cache_coercion (_,(coe,xf,cls,clt)) =
   let is,_ = class_info cls in
   let it,_ = class_info clt in
-  let jf = add_new_coercion (coe,xf) in
-  add_coercion_in_graph (jf,is,it)
+  add_new_coercion coe xf;
+  add_coercion_in_graph (xf,is,it)
 
-let subst_coercion (_,subst,((coe,xf),cls,clt as obj)) =
+let subst_coercion (_,subst,(coe,xf,cls,clt as obj)) =
   let coe' = subst_coe_typ subst coe in
   let xf' = subst_coe_info subst xf in
   let cls' = subst_cl_typ subst cls in
   let clt' = subst_cl_typ subst clt in
     if coe' == coe && xf' == xf && cls' == cls & clt' == clt then obj else
-      ((coe',xf'),cls',clt')
+      (coe',xf',cls',clt')
       
     
-(* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ  ->
-                    -> Libobject.object 
-   val outCoercion : Libobject.object -> (coe_typ * coe_info_typ) 
-                         * cl_typ * cl_typ *)
+(* val inCoercion : coercion -> Libobject.object 
+   val outCoercion : Libobject.object -> coercion *)
 
 let (inCoercion,outCoercion) =
   declare_object {(default_object "COERCION") with 
@@ -371,11 +349,11 @@ let (inCoercion,outCoercion) =
 let declare_coercion coef v stre ~isid ~src:cls ~target:clt ~params:ps =
   Lib.add_anonymous_leaf
     (inCoercion
-       ((coef,
+       (coef,
 	 { coe_value = v;
 	   coe_strength = stre;
 	   coe_is_identity = isid;
-	   coe_param = ps }),
+	   coe_param = ps },
 	cls, clt))
 
 let coercion_strength v = v.coe_strength
@@ -384,17 +362,16 @@ let coercion_identity v = v.coe_is_identity
 (* For printing purpose *)
 let get_coercion_value v = v.coe_value.uj_val
 
-let classes () = !class_tab
-let coercions () = !coercion_tab
-let inheritance_graph () = !inheritance_graph
+let classes () = Bijint.dom !class_tab
+let coercions () = Gmap.rng !coercion_tab
+let inheritance_graph () = Gmap.to_list !inheritance_graph
 
 let coercion_of_qualid qid =
   let ref = Nametab.global qid in
-  let coe = coe_of_reference ref in
-  if not (coercion_exists coe) then
+  if not (coercion_exists ref) then
     errorlabstrm "try_add_coercion" 
       (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion");
-  coe
+  ref
 
 module CoercionPrinting =
   struct
@@ -414,6 +391,6 @@ module PrintingCoercion  = Goptions.MakeRefTable(CoercionPrinting)
 
 let hide_coercion coe =
   if not (PrintingCoercion.active coe) then
-    let _,coe_info = coercion_info coe in
+    let coe_info = coercion_info coe in
     Some coe_info.coe_param
   else None
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 50af9840c..aa0cca3dc 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -46,8 +46,6 @@ type coe_index
 (* This is the type of paths from a class to another *)
 type inheritance_path = coe_index list
 
-val coe_of_reference : Libnames.global_reference -> coe_typ
-
 (*s [declare_class] adds a class to the set of declared classes *)
 val declare_class : cl_typ * strength * int -> unit
 
@@ -77,7 +75,6 @@ val declare_coercion :
 
 (*s Access to coercions infos *)
 val coercion_exists : coe_typ -> bool
-val coercion_info_from_index : coe_index -> coe_typ * coe_info_typ
 
 val coercion_value : coe_index -> (unsafe_judgment * bool)
 
@@ -89,7 +86,7 @@ val lookup_pattern_path_between :
   cl_index * cl_index -> (constructor * int) list
 
 (*i Pour le discharge *)
-type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
+type coercion = coe_typ * coe_info_typ * cl_typ * cl_typ
 
 open Libobject
 val inClass : (cl_typ * cl_info_typ) -> Libobject.obj
@@ -109,13 +106,12 @@ val install_path_printer :
 
 (*s This is for printing purpose *)
 val string_of_class : cl_typ -> string
-val get_coercion_value : coe_info_typ -> constr
+val pr_class : cl_typ -> std_ppcmds
+val get_coercion_value : coe_index -> constr
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
-val classes : unit -> (int * (cl_typ * cl_info_typ)) list
-val coercions : unit -> (int * (coe_typ * coe_info_typ)) list
+val classes : unit -> cl_typ list
+val coercions : unit -> coe_index list
 
 (* [hide_coercion] returns the number of params to skip if the coercion must
    be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
 val hide_coercion : coe_typ -> int option
-
-
diff --git a/toplevel/class.ml b/toplevel/class.ml
index e1ba8e736..75ab77bf0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -82,14 +82,14 @@ let explain_coercion_error g = function
   | NoTarget ->
       (str"Cannot find the target class")
   | WrongTarget (clt,cl) ->
-      (str"Found target class " ++ str(string_of_class cl) ++
-	str " while " ++ str(string_of_class clt) ++
+      (str"Found target class " ++ pr_class cl ++
+	str " while " ++ pr_class clt ++
 	str " is expected")
   | NotAClass ref ->
       (str "Type of " ++ Printer.pr_global ref ++
          str " does not end with a sort")
   | NotEnoughClassArgs cl ->
-      (str"Wrong number of parameters for " ++str(string_of_class cl))
+      (str"Wrong number of parameters for " ++ pr_class cl)
 
 (* Verifications pour l'ajout d'une classe *)
 
@@ -123,7 +123,7 @@ let try_add_class cl streopt fail_if_exists =
     declare_class (cl,stre,p)
   else
     if fail_if_exists then errorlabstrm "try_add_new_class" 
-      (str (string_of_class cl) ++ str " is already a class")
+      (pr_class cl ++ str " is already a class")
 
 
 (* Coercions *)
@@ -222,7 +222,7 @@ let get_strength stre ref cls clt =
 
 let error_not_transparent source =
   errorlabstrm "build_id_coercion"
-    (str ((string_of_class source)^" must be a transparent constant"))
+    (pr_class source ++ str " must be a transparent constant")
 
 let build_id_coercion idf_opt source =
   let env = Global.env () in
@@ -441,7 +441,7 @@ let process_cl sec_sp cl =
 	  cl
     | _ -> cl
 
-let process_coercion olddir ids_to_discard ((coe,coeinfo),cls,clt) =
+let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) =
   let hyps = context_of_global_reference coe in
   let nargs = count_extra_abstractions hyps ids_to_discard in
   (process_global olddir coe,
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 1eb74c7e7..d148a5343 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -253,7 +253,7 @@ let process_object oldenv olddir full_olddir newdir
           ((Class (y1,y2))::ops, ids_to_discard, work_alist)
 	  
     | "COERCION" -> 
-	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
+	let (_,coeinfo,_,_ as x) = outCoercion lobj in
 	if coercion_strength coeinfo = Local then
 	  (ops,ids_to_discard,work_alist)
         else