diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 313fc58d..23ec108a 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i*) open Names open Declarations @@ -289,10 +289,10 @@ let reset_needed, add_needed, found_needed, is_needed = (fun r -> Refset'.mem (base_r r) !needed)) 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. *) @@ -308,18 +308,25 @@ 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 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 | _ -> raise NoDepCheck let rec depcheck_struct = function |