Extraction: multiple fixes related with the Not_found encountered by X. Leroy

Cf. coqdev for the details of the bug report.

 - Protect some Hashtbl.find and other risky functions in order to avoid
   as much as possible to end with an irritating Anomaly : Not_found.
 - Re-enable in pp_ocaml_extern the case of a module-file used as
   a module (e.g. module A' := A for A.v) when doing modular extraction.
 - Rework the code that decides to "open" or not modules initially:
   opening A when A contains a submodule B hides the file B even when
   B isn't opened itself, we avoid that now.
 - Fix some tables (sets or maps) used by extraction for which it is
   critical to consider constants/inductives/global_reference _not_
   modulo the equivalence of Elie, but rather via Pervasives.compare.

 Still to do : avoid appearance of '_a in extracted code.

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

1 files changed, 65 insertions, 46 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b52cab204..5457d2e8c 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -19,6 +19,13 @@ open Util
 open Pp
 open Miniml
 
+(** Sets and maps for [global_reference] that do _not_ work modulo
+    name equivalence (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct type t = global_reference let compare = compare end
+module Refmap' = Map.Make(RefOrd)
+module Refset' = Set.Make(RefOrd)
+
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 let occur_kn_in_ref kn = function
@@ -117,37 +124,47 @@ let rec add_labels_mp mp = function
 
 (*s Constants tables. *)
 
-let terms = ref (Cmap.empty : ml_decl Cmap.t)
-let init_terms () = terms := Cmap.empty
-let add_term kn d = terms := Cmap.add kn d !terms
-let lookup_term kn = Cmap.find kn !terms
+let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
+let init_terms () = terms := Cmap_env.empty
+let add_term kn d = terms := Cmap_env.add kn d !terms
+let lookup_term kn = Cmap_env.find kn !terms
 
-let types = ref (Cmap.empty : ml_schema Cmap.t)
-let init_types () = types := Cmap.empty
-let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types
+let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
+let init_types () = types := Cmap_env.empty
+let add_type kn s = types := Cmap_env.add kn s !types
+let lookup_type kn = Cmap_env.find kn !types
 
 (*s Inductives table. *)
 
-let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t)
-let init_inductives () = inductives := Mindmap.empty
-let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap.find kn !inductives
+let inductives =
+  ref (Mindmap_env.empty : (mutual_inductive_body * ml_ind) Mindmap_env.t)
+let init_inductives () = inductives := Mindmap_env.empty
+let add_ind kn mib ml_ind =
+  inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
+let lookup_ind kn = Mindmap_env.find kn !inductives
 
 (*s Recursors table. *)
 
+(* NB: here we can use the equivalence between canonical
+   and user constant names : Cset is fine, no need for [Cset_env] *)
+
 let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
 let add_recursors env kn =
-  let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in
+  let mk_con id =
+    make_con_equiv
+      (modpath (user_mind kn))
+      (modpath (canonical_mind kn))
+      empty_dirpath (label_of_id id)
+  in
   let mib = Environ.lookup_mind kn env in
   Array.iter
     (fun mip ->
        let id = mip.mind_typename in
-       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
-       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
+       let c_rec = mk_con (Nameops.add_suffix id "_rec")
+       and c_rect = mk_con (Nameops.add_suffix id "_rect") in
+       recursors := Cset.add c_rec (Cset.add c_rect !recursors))
     mib.mind_packets
 
 let is_recursor = function
@@ -156,6 +173,8 @@ let is_recursor = function
 
 (*s Record tables. *)
 
+(* NB: here, working modulo name equivalence is ok *)
+
 let projs = ref (Refmap.empty : int Refmap.t)
 let init_projs () = projs := Refmap.empty
 let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
@@ -164,12 +183,12 @@ let projection_arity r = Refmap.find r !projs
 
 (*s Table of used axioms *)
 
-let info_axioms = ref Refset.empty
-let log_axioms = ref Refset.empty
-let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
-let add_info_axiom r = info_axioms := Refset.add r !info_axioms
-let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
-let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+let info_axioms = ref Refset'.empty
+let log_axioms = ref Refset'.empty
+let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty
+let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
+let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
+let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
 (*s Extraction mode: modular or monolithic *)
 
@@ -218,7 +237,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 let err s = errorlabstrm "Extraction" s
 
 let warning_axioms () =
-  let info_axioms = Refset.elements !info_axioms in
+  let info_axioms = Refset'.elements !info_axioms in
   if info_axioms = [] then ()
   else begin
     let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
@@ -227,7 +246,7 @@ let warning_axioms () =
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
-  let log_axioms = Refset.elements !log_axioms in
+  let log_axioms = Refset'.elements !log_axioms in
   if log_axioms = [] then ()
   else begin
     let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
@@ -455,16 +474,16 @@ let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
 
-let empty_inline_table = (Refset.empty,Refset.empty)
+let empty_inline_table = (Refset'.empty,Refset'.empty)
 
 let inline_table = ref empty_inline_table
 
-let to_inline r = Refset.mem r (fst !inline_table)
+let to_inline r = Refset'.mem r (fst !inline_table)
 
-let to_keep r = Refset.mem r (snd !inline_table)
+let to_keep r = Refset'.mem r (snd !inline_table)
 
 let add_inline_entries b l =
-  let f b = if b then Refset.add else Refset.remove in
+  let f b = if b then Refset'.add else Refset'.remove in
   let i,k = !inline_table in
   inline_table :=
   (List.fold_right (f b) l i),
@@ -502,14 +521,14 @@ let extraction_inline b l =
 
 let print_extraction_inline () =
   let (i,n)= !inline_table in
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+  let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
   msg
     (str "Extraction Inline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++
-     Refset.fold
+     Refset'.fold
        (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
@@ -527,10 +546,10 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 type int_or_id = ArgInt of int | ArgId of identifier
 
-let implicits_table = ref Refmap.empty
+let implicits_table = ref Refmap'.empty
 
 let implicits_of_global r =
- try Refmap.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
   let typ = Global.type_of_global r in
@@ -550,7 +569,7 @@ let add_implicits r l =
 		safe_pr_global r))
   in
   let l' = List.map check l in
-  implicits_table := Refmap.add r l' !implicits_table
+  implicits_table := Refmap'.add r l' !implicits_table
 
 (* Registration of operations for rollback. *)
 
@@ -566,7 +585,7 @@ let (implicit_extraction,_) =
 let _ = declare_summary "Extraction Implicit"
 	  { freeze_function = (fun () -> !implicits_table);
 	    unfreeze_function = ((:=) implicits_table);
-	    init_function = (fun () -> implicits_table := Refmap.empty) }
+	    init_function = (fun () -> implicits_table := Refmap'.empty) }
 
 (* Grammar entries. *)
 
@@ -656,22 +675,22 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 let use_type_scheme_nb_args, register_type_scheme_nb_args =
   let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
-let customs = ref Refmap.empty
+let customs = ref Refmap'.empty
 
-let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
+let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
 
-let is_custom r = Refmap.mem r !customs
+let is_custom r = Refmap'.mem r !customs
 
 let is_inline_custom r = (is_custom r) && (to_inline r)
 
-let find_custom r = snd (Refmap.find r !customs)
+let find_custom r = snd (Refmap'.find r !customs)
 
-let find_type_custom r = Refmap.find r !customs
+let find_type_custom r = Refmap'.find r !customs
 
-let custom_matchs = ref Refmap.empty
+let custom_matchs = ref Refmap'.empty
 
 let add_custom_match r s =
-  custom_matchs := Refmap.add r s !custom_matchs
+  custom_matchs := Refmap'.add r s !custom_matchs
 
 let indref_of_match pv =
   if Array.length pv = 0 then raise Not_found;
@@ -680,11 +699,11 @@ let indref_of_match pv =
     | _ -> raise Not_found
 
 let is_custom_match pv =
-  try Refmap.mem (indref_of_match pv) !custom_matchs
+  try Refmap'.mem (indref_of_match pv) !custom_matchs
   with Not_found -> false
 
 let find_custom_match pv =
-  Refmap.find (indref_of_match pv) !custom_matchs
+  Refmap'.find (indref_of_match pv) !custom_matchs
 
 (* Registration of operations for rollback. *)
 
@@ -701,7 +720,7 @@ let (in_customs,_) =
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !customs);
 	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap.empty) }
+	    init_function = (fun () -> customs := Refmap'.empty) }
 
 let (in_custom_matchs,_) =
   declare_object
@@ -715,7 +734,7 @@ let (in_custom_matchs,_) =
 let _ = declare_summary "ML extractions custom match"
 	  { freeze_function = (fun () -> !custom_matchs);
 	    unfreeze_function = ((:=) custom_matchs);
-	    init_function = (fun () -> custom_matchs := Refmap.empty) }
+	    init_function = (fun () -> custom_matchs := Refmap'.empty) }
 
 (* Grammar entries. *)