Extraction: fix a few little glitches with my last commit (replacing unused vars by _)

5 files changed, 19 insertions, 20 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 97f856944..8cf3b8194 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -171,10 +171,7 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let get_db_name n (db,_) =
-  let id = List.nth db (pred n) in
-  if Id.equal id dummy_name then Id.of_string "__" else id
-
+let get_db_name n (db,_) = List.nth db (pred n)
 
 (*S Renamings of global objects. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 00259750d..da7a4265e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -143,7 +143,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 2b606bf13..eb3046f03 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -514,11 +514,6 @@ let nb_occur_match =
 (* Replace unused variables by _ *)
 
 let dump_unused_vars a =
-  let dump_id = function
-    | Dummy -> Dummy
-    | Id _ -> Id dummy_name
-    | Tmp _ -> Tmp dummy_name
-  in
   let rec ren env a = match a with
     | MLrel i ->
        let () = (List.nth env (i-1)) := true in a
@@ -527,7 +522,7 @@ let dump_unused_vars a =
        let occ_id = ref false in
        let b' = ren (occ_id::env) b in
        if !occ_id then if b' == b then a else MLlam(id,b')
-       else MLlam(dump_id id,b')
+       else MLlam(Dummy,b')
 
     | MLletin (id,b,c) ->
        let occ_id = ref false in
@@ -537,7 +532,7 @@ let dump_unused_vars a =
          if b' == b && c' == c then a else MLletin(id,b',c')
        else
          (* 'let' without occurrence: shouldn't happen after simpl *)
-         MLletin(dump_id id,b',c')
+         MLletin(Dummy,b',c')
 
     | MLcase (t,e,br) ->
        let e' = ren env e in
@@ -572,7 +567,7 @@ let dump_unused_vars a =
       let b' = ren (List.rev_append occs env) b in
       let ids' =
         List.map2
-          (fun id occ -> if !occ then id else dump_id id)
+          (fun id occ -> if !occ then id else Dummy)
           ids occs
       in
       if b' == b && List.equal eq_ml_ident ids ids' then tr
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 6f354b1ce..c3dc286cd 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -263,29 +263,28 @@ let dfix_to_mlfix rv av i =
    order to preserve the global interface, later [depcheck_se] will get
    rid of them if possible *)
 
-let optim_ast t = dump_unused_vars (normalize t)
-
 let rec optim_se top to_appear s = function
   | [] -> []
   | (l,SEdecl (Dterm (r,a,t))) :: lse ->
-      let a = optim_ast (ast_glob_subst !s a) in
+      let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      let d = match optimize_fix a with
+      let d = match dump_unused_vars (optimize_fix a) with
 	| MLfix (0, _, [|c|]) ->
 	  Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
 	| a -> Dterm (r, a, t)
       in
       (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
-      let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in
+      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       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
       done;
-      (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+      let av' = Array.map dump_unused_vars av in
+      (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse ->
       let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
       in (l,SEmodule m) :: (optim_se top to_appear s lse)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 6ff4c25ec..8c86c7711 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -178,7 +178,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f