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, 16 insertions, 12 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 90541ceff..30c88602d 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -66,7 +66,7 @@ module type VISIT = sig
 
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_kn : mutual_inductive -> unit
+  val add_ind : mutual_inductive -> unit
   val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
@@ -74,31 +74,35 @@ module type VISIT = sig
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
-  val needed_kn : mutual_inductive -> bool
+  val needed_ind : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
 end
 
 module Visit : VISIT = struct
   (* What used to be in a single KNset should now be split into a KNset
-     (for inductives and modules names) and a Cset for constants
+     (for inductives and modules names) and a Cset_env for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t }
+      { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty }
+  let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
-  let needed_kn kn = Mindset.mem kn v.kn
-  let needed_con c = Cset.mem c v.con
+  let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+  let needed_ind i = KNset.mem (user_mind i) v.ind
+  let needed_con c = KNset.mem (user_con c) v.con
   let needed_mp mp = MPset.mem mp v.mp
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
-  let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn)
-  let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
+  let add_ind i =
+    let kn = user_mind i in
+    v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
+  let add_con c =
+    let kn = user_con c in
+    v.con <- KNset.add kn v.con; add_mp (modpath kn)
   let add_ref = function
     | ConstRef c -> add_con c
-    | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind
     | VarRef _ -> assert false
   let add_decl_deps = decl_iter_references add_ref add_ref add_ref
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
@@ -277,7 +281,7 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let kn = make_kn mp empty_dirpath l in
       let mind = mind_of_kn kn in
-      let b = Visit.needed_kn mind in
+      let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (kn, extract_inductive env mind) in
 	if (not b) && (logical_decl d) then ms