diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/modutil.ml | 75 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 3 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 3 |
3 files changed, 75 insertions, 6 deletions
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 48444509..0c906712 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 10665 2008-03-14 12:10:09Z soubiran $ i*) +(*i $Id: modutil.ml 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Declarations @@ -347,6 +347,73 @@ and optim_me to_appear s = function MEapply (optim_me to_appear s me, optim_me to_appear s me') | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) -let optimize_struct to_appear struc = - let subst = ref (Refmap.empty : ml_ast Refmap.t) in - List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc +(* After these optimisations, some dependencies may not be needed anymore. + For monolithic extraction, we recompute a minimal set of dependencies. *) + +exception NoDepCheck + +let base_r = function + | ConstRef c as r -> r + | IndRef (kn,_) -> IndRef (kn,0) + | ConstructRef ((kn,_),_) -> IndRef (kn,0) + | _ -> 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 declared_refs = function + | Dind (kn,_) -> [|IndRef (kn,0)|] + | Dtype (r,_,_) -> [|r|] + | Dterm (r,_,_) -> [|r|] + | Dfix (rv,_,_) -> rv + +(* Computes the dependencies of a declaration, except in case + of custom extraction. *) + +let compute_deps_decl = function + | Dind (kn,ind) -> + (* Todo Later : avoid dependencies when Extract Inductive *) + ind_iter_references add_needed add_needed add_needed kn ind + | Dtype (r,ids,t) -> + if not (is_custom r) then type_iter_references add_needed t + | Dterm (r,u,t) -> + type_iter_references add_needed t; + 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') + | _ -> raise NoDepCheck + +let rec depcheck_struct = function + | [] -> [] + | (mp,lse)::struc -> + let struc' = depcheck_struct struc in + let lse' = depcheck_se lse in + (mp,lse')::struc' + +let optimize_struct to_appear struc = + 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 + try + if modular () then raise NoDepCheck; + reset_needed (); + List.iter add_needed to_appear; + depcheck_struct opt_struc + with NoDepCheck -> opt_struc diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index abf461c1..10f669e1 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 10348 2007-12-06 17:36:14Z aspiwack $ i*) +(*i $Id: table.ml 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Term @@ -175,6 +175,7 @@ let info_axioms = ref Refset.empty let log_axioms = ref Refset.empty let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms let add_log_axiom r = log_axioms := Refset.add r !log_axioms (*s Extraction mode: modular or monolithic *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index ca02cb4d..4dbccd08 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 10245 2007-10-21 13:41:53Z letouzey $ i*) +(*i $Id: table.mli 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Libnames @@ -77,6 +77,7 @@ val is_projection : global_reference -> bool val projection_arity : global_reference -> int val add_info_axiom : global_reference -> unit +val remove_info_axiom : global_reference -> unit val add_log_axiom : global_reference -> unit val reset_tables : unit -> unit |