Extraction: avoid printing unused mutual fix components (fix #2477)

 This happens for instance when the main component of the fixpoint
 block has been provided via Extract Constant

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

4 files changed, 55 insertions, 32 deletions

diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6cad5d294..ef8a1f9b4 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -312,10 +312,17 @@ let pp_decl = function
       in
       prvecti
 	(fun i r ->
-	  if is_inline_custom r then mt ()
+	  let void = is_inline_custom r ||
+	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	  in
+	  if void then mt ()
 	  else
-	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl ()
-	    ++ pp_function (empty_env ()) names.(i) defs.(i) ++ fnl2 ())
+	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
+	    (if is_custom r then
+		(names.(i) ++ str " = " ++ str (find_custom r))
+	     else
+		(pp_function (empty_env ()) names.(i) defs.(i)))
+	    ++ fnl2 ())
 	rv
   | Dterm (r, a, t) ->
       if is_inline_custom r then mt ()
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index fd1693d3d..21dfee666 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -295,10 +295,10 @@ let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
      Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps))
 
 let declared_refs = function
-  | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
-  | Dtype (r,_,_) -> [|r|]
-  | Dterm (r,_,_) -> [|r|]
-  | Dfix (rv,_,_) -> rv
+  | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)]
+  | Dtype (r,_,_) -> [r]
+  | Dterm (r,_,_) -> [r]
+  | Dfix (rv,_,_) -> Array.to_list rv
 
 (* Computes the dependencies of a declaration, except in case
    of custom extraction. *)
@@ -314,7 +314,6 @@ let compute_deps_decl = function
       if not (is_custom r) then
 	ast_iter_references add_needed add_needed add_needed u
   | Dfix _ as d ->
-      (* Todo Later : avoid dependencies when Extract Constant *)
       decl_iter_references add_needed add_needed add_needed d
 
 let compute_deps_spec = function
@@ -328,13 +327,21 @@ let compute_deps_spec = function
 
 let rec depcheck_se = function
   | [] -> []
-  | ((l,SEdecl d) as t)::se ->
-      let se' = depcheck_se se in
-      let rv = declared_refs d in
-      if not (array_exists is_needed rv) then
-	(Array.iter remove_info_axiom rv; se')
-      else
-	(Array.iter found_needed rv; compute_deps_decl d; t::se')
+  | ((l,SEdecl d) as t) :: se ->
+    let se' = depcheck_se se in
+    let refs = declared_refs d in
+    let refs' = List.filter is_needed refs in
+    if refs' = [] then
+      (List.iter remove_info_axiom refs; se')
+    else begin
+      List.iter found_needed refs';
+      (* Hack to avoid extracting unused part of a Dfix *)
+      match d with
+	| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
+	  let trms' =  Array.create (Array.length rv) (MLexn "UNUSED") in
+	  ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
+	| _ -> (compute_deps_decl d; t::se')
+    end
   | t :: se ->
     let se' = depcheck_se se in
     se_iter compute_deps_decl compute_deps_spec t;
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 543cec6e5..d3a6fceed 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -413,17 +413,24 @@ let pp_Dfix (rv,c,t) =
   let names = Array.map
     (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
   in
-  let rec pp sep letand i =
-    if i >= Array.length rv then mt ()
-    else if is_inline_custom rv.(i) then pp sep letand (i+1)
+  let rec pp init i =
+    if i >= Array.length rv then
+      (if init then failwith "empty phrase" else mt ())
     else
-      let def =
-	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
-	else pp_function (empty_env ()) c.(i)
+      let void = is_inline_custom rv.(i) ||
+	(not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED")
       in
-      sep () ++ pp_val names.(i) t.(i) ++
-      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
-  in pp mt "let rec " 0
+      if void then pp init (i+1)
+      else
+	let def =
+	  if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
+	  else pp_function (empty_env ()) c.(i)
+	in
+	(if init then mt () else fnl2 ()) ++
+	pp_val names.(i) t.(i) ++
+	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
+	pp false (i+1)
+  in pp true 0
 
 (*s Pretty-printing of inductive types declaration. *)
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index c07710713..8a781a8d9 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -169,22 +169,24 @@ let pp_decl = function
       in
       prvecti
 	(fun i r ->
-	  if is_inline_custom r then mt ()
+	  let void = is_inline_custom r ||
+	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	  in
+	  if void then mt ()
 	  else
 	    hov 2
 	      (paren (str "define " ++ names.(i) ++ spc () ++
-			(pp_expr (empty_env ()) [] defs.(i)))
+			(if is_custom r then str (find_custom r)
+			 else pp_expr (empty_env ()) [] defs.(i)))
 	       ++ fnl ()) ++ fnl ())
 	rv
   | Dterm (r, a, _) ->
       if is_inline_custom r then mt ()
       else
-	if is_custom r then
-	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
-			  str (find_custom r))) ++ fnl () ++ fnl ()
-	else
-	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
-			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
+	hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+			(if is_custom r then str (find_custom r)
+			 else pp_expr (empty_env ()) [] a)))
+	++ fnl2 ()
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d