diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 91 |
1 files changed, 60 insertions, 31 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index ffa38def..9e8dd828 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Names open Declarations open Environ @@ -28,7 +26,7 @@ let rec msid_of_mt = function (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) -let struct_iter do_decl do_spec s = +let se_iter do_decl do_spec = let rec mt_iter = function | MTident _ -> () | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' @@ -58,7 +56,10 @@ let struct_iter do_decl do_spec s = | MEapply (me,me') -> me_iter me; me_iter me' | MEstruct (msid, sel) -> List.iter se_iter sel in - List.iter (function (_,sel) -> List.iter se_iter sel) s + se_iter + +let struct_iter do_decl do_spec s = + List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) @@ -76,18 +77,26 @@ let type_iter_references do_type t = | _ -> () in iter t +let patt_iter_references do_cons p = + let rec iter = function + | Pcons (r,l) -> do_cons r; List.iter iter l + | Pusual r -> do_cons r + | Ptuple l -> List.iter iter l + | Prel _ | Pwild -> () + in iter p + let ast_iter_references do_term do_cons do_type a = let rec iter a = ast_iter iter a; match a with | MLglob r -> do_term r - | MLcons (i,r,_) -> - if lang () = Ocaml then record_iter_references do_term i.c_kind; - do_cons r - | MLcase (i,_,v) -> - if lang () = Ocaml then record_iter_references do_term i.m_kind; - Array.iter (fun (r,_,_) -> do_cons r) v - | _ -> () + | MLcons (_,r,_) -> do_cons r + | MLcase (ty,_,v) -> + type_iter_references do_type ty; + Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v + + | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ + | MLdummy | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -108,15 +117,14 @@ let decl_iter_references do_term do_cons do_type = let type_iter = type_iter_references do_type and ast_iter = ast_iter_references do_term do_cons do_type in function - | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type - (mind_of_kn kn) ind + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Dtype (r,_,t) -> do_type r; type_iter t | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t | Dfix(rv,c,t) -> Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t let spec_iter_references do_term do_cons do_type = function - | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind + | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot | Sval (r,t) -> do_term r; type_iter_references do_type t @@ -236,7 +244,7 @@ let rec optim_se top to_appear s = function let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - if top && i && not (modular ()) && not (List.mem r to_appear) + if top && i && not (library ()) && not (List.mem r to_appear) then optim_se top to_appear s lse else let d = match optimize_fix a with @@ -254,7 +262,7 @@ let rec optim_se top to_appear s = function then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; - if !all && top && not (modular ()) + if !all && top && not (library ()) && (array_for_all (fun r -> not (List.mem r to_appear)) rv) then optim_se top to_appear s lse else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) @@ -271,7 +279,8 @@ and optim_me to_appear s = function | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) (* After these optimisations, some dependencies may not be needed anymore. - For monolithic extraction, we recompute a minimal set of dependencies. *) + For non-library extraction, we recompute a minimal set of dependencies + for first-level objects *) exception NoDepCheck @@ -281,15 +290,19 @@ let base_r = function | 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), +let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = + let needed = ref Refset'.empty + and needed_mps = ref MPset.empty in + ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), + (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), - (fun r -> Refset'.mem (base_r r) !needed)) + (fun r -> + let r = base_r r in + Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps)) let declared_refs = function - | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)] + | Dind (kn,_) -> [IndRef (kn,0)] | Dtype (r,_,_) -> [r] | Dterm (r,_,_) -> [r] | Dfix (rv,_,_) -> Array.to_list rv @@ -300,7 +313,7 @@ let declared_refs = function let compute_deps_decl = function | Dind (kn,ind) -> (* Todo Later : avoid dependencies when Extract Inductive *) - ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind + 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) -> @@ -310,6 +323,15 @@ let compute_deps_decl = function | Dfix _ as d -> decl_iter_references add_needed add_needed add_needed d +let compute_deps_spec = function + | Sind (kn,ind) -> + (* Todo Later : avoid dependencies when Extract Inductive *) + ind_iter_references add_needed add_needed add_needed kn ind + | Stype (r,ids,t) -> + if not (is_custom r) then Option.iter (type_iter_references add_needed) t + | Sval (r,t) -> + type_iter_references add_needed t + let rec depcheck_se = function | [] -> [] | ((l,SEdecl d) as t) :: se -> @@ -317,7 +339,9 @@ let rec depcheck_se = function let refs = declared_refs d in let refs' = List.filter is_needed refs in if refs' = [] then - (List.iter remove_info_axiom refs; se') + (List.iter remove_info_axiom refs; + List.iter remove_opaque refs; + se') else begin List.iter found_needed refs'; (* Hack to avoid extracting unused part of a Dfix *) @@ -327,7 +351,10 @@ let rec depcheck_se = function ((l,SEdecl (Dfix (rv,trms',tys))) :: se') | _ -> (compute_deps_decl d; t::se') end - | _ -> raise NoDepCheck + | t :: se -> + let se' = depcheck_se se in + se_iter compute_deps_decl compute_deps_spec t; + t :: se' let rec depcheck_struct = function | [] -> [] @@ -350,13 +377,15 @@ let check_implicits = function 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 + List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) + struc in let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in ignore (struct_ast_search check_implicits opt_struc); - try - if modular () then raise NoDepCheck; + if library () then opt_struc + else begin reset_needed (); - List.iter add_needed to_appear; + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); depcheck_struct opt_struc - with NoDepCheck -> opt_struc + end |