diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 15:37:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 15:37:51 +0000 |
commit | 2d0293367d13ac8ef8c337ba1dd0085f83dc501b (patch) | |
tree | 536ce1b2bb5adb54cc49350a2f7555d61ae289f3 | |
parent | 695bf462bba223c8870634bac7cb149ffb0b28b6 (diff) |
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
-rw-r--r-- | plugins/extraction/haskell.ml | 13 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 31 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 25 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 18 |
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 |