Better use of tables for storing results of extract_ind (bug #1709)

 It is critical to avoid duplicated calls to extract_ind (see e.g. 
 example in #1709). But the same kernel_name can lead to different 
 inductive bodies, due to module substitutions. So we used to 
 factorize only "visible" kn, that were not subject to change under 
 substitution. As shown by P. Cregut in #1709, this is not enough. 
 New approach is now to store also Coq inductive data (mib). If the 
 recorded mib matches the current one, we trust the recorded result, 
 otherwise we start a fresh computation of extract_ind. 



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

3 files changed, 18 insertions, 19 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 5a192b62e..3fa318e7e 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -31,10 +31,6 @@ open Mlutil
 
 exception I of inductive_info
 
-(* A set of all inductive currently being computed, 
-   to avoid loops in [extract_inductive] *)
-let internal_call = ref KNset.empty
-
 (* A set of all fixpoint functions currently being extracted *)
 let current_fixpoints = ref ([] : constant list)
 
@@ -303,13 +299,15 @@ and extract_type_scheme env db c p =
 (*S Extraction of an inductive type. *)
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
-  try 
-    if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *)
-    else if visible_kn kn then lookup_ind kn (* Standard situation. *)
-    else raise Not_found (* Never trust the table for a internal kn. *)
+  let mib = Environ.lookup_mind kn env in
+  try
+    (* For a same kn, we can get various bodies due to module substitutions.
+       We hence check that the mib has not changed from recording 
+       time to retrieving time. Ideally we should also check the env. *)
+    let (mib0,ml_ind) = lookup_ind kn in 
+    if not (mib = mib0) then raise Not_found; 
+    ml_ind
   with Not_found -> 
-    internal_call := KNset.add kn !internal_call;
-    let mib = Environ.lookup_mind kn env in 
     (* First, if this inductive is aliased via a Module, *)
     (* we process the original inductive. *)
     option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
@@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_types = t }) 
 	mib.mind_packets 
     in 
-    add_ind kn 
+    add_ind kn mib
       {ind_info = Standard; 
        ind_nparams = npar; 
        ind_packets = packets; 
@@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ind_packets = packets; 
 	     ind_equiv = mib.mind_equiv}
     in
-    add_ind kn i; 
-    internal_call := KNset.remove kn !internal_call;
+    add_ind kn mib i; 
     i
 
 (*s [extract_type_cons] extracts the type of an inductive 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 47a0977a5..22778ccff 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -77,9 +77,9 @@ let lookup_type kn = Cmap.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
 let init_inductives () = inductives := KNmap.empty
-let add_ind kn m = inductives := KNmap.add kn m !inductives
+let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
 let lookup_ind kn = KNmap.find kn !inductives
 
 (*s Recursors table. *)
@@ -124,8 +124,9 @@ let reset_tables () =
 
 let id_of_global = function 
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
-  | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
+  | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+  | ConstructRef ((kn,i),j) -> 
+      (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
 let pr_global r = pr_id (id_of_global r)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 6be869e59..cc793b1a1 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -11,6 +11,7 @@
 open Names
 open Libnames
 open Miniml
+open Declarations
 
 val id_of_global : global_reference -> identifier
 
@@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl
 val add_type : constant -> ml_schema -> unit
 val lookup_type : constant -> ml_schema
 
-val add_ind : kernel_name -> ml_ind -> unit
-val lookup_ind : kernel_name -> ml_ind
+val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
 
 val add_recursors : Environ.env -> kernel_name -> unit
 val is_recursor : global_reference -> bool