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, 11 insertions, 31 deletions

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index e455e54cb..bb880aeea 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -215,45 +215,25 @@ let get_decl_in_structure r struc =
 let dfix_to_mlfix rv av i =
   let rec make_subst n s =
     if n < 0 then s
-    else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
+    else make_subst (n-1) (Refmap'.add rv.(n) (n+1) s)
   in
-  let s = make_subst (Array.length rv - 1) Refmap.empty
+  let s = make_subst (Array.length rv - 1) Refmap'.empty
   in
   let rec subst n t = match t with
     | MLglob ((ConstRef kn) as refe) ->
-	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
+	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
   let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
   let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
-let rec optim to_appear s = function
-  | [] -> []
-  | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r to_appear
-      then d :: (optim to_appear s l)
-      else optim to_appear s l
-  | Dterm (r,t,typ) :: l ->
-      let t = normalize (ast_glob_subst !s t) in
-      let i = inline r t in
-      if i then s := Refmap.add r t !s;
-      if not i || modular () || List.mem r to_appear
-      then
-	let d = match optimize_fix t with
-	  | MLfix (0, _, [|c|]) ->
-	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
-	  | t -> Dterm (r, t, typ)
-	in d :: (optim to_appear s l)
-      else optim to_appear s l
-  | d :: l -> d :: (optim to_appear s l)
-
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
-      if i then s := Refmap.add r a !s;
+      if i then s := Refmap'.add r a !s;
       if top && i && not (modular ()) && not (List.mem r to_appear)
       then optim_se top to_appear s lse
       else
@@ -269,7 +249,7 @@ let rec optim_se top to_appear s = function
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
 	if inline rv.(i) fake_body
-	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
+	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done;
       if !all && top && not (modular ())
@@ -300,11 +280,11 @@ let base_r = function
   | _ -> assert false
 
 let reset_needed, add_needed, found_needed, is_needed =
-  let needed = ref Refset.empty in
-  ((fun l -> needed := Refset.empty),
-   (fun r -> needed := Refset.add (base_r r) !needed),
-   (fun r -> needed := Refset.remove (base_r r) !needed),
-   (fun r -> Refset.mem (base_r r) !needed))
+  let needed = ref Refset'.empty in
+  ((fun l -> needed := Refset'.empty),
+   (fun r -> needed := Refset'.add (base_r r) !needed),
+   (fun r -> needed := Refset'.remove (base_r r) !needed),
+   (fun r -> Refset'.mem (base_r r) !needed))
 
 let declared_refs = function
   | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
@@ -359,7 +339,7 @@ let check_implicits = function
   | _ -> false
 
 let optimize_struct to_appear struc =
-  let subst = ref (Refmap.empty : ml_ast Refmap.t) in
+  let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
   let opt_struc =
     List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
   in