diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r-- | plugins/extraction/extract_env.ml | 128 |
1 files changed, 83 insertions, 45 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3fa674d3..73062328 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.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: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Term open Declarations open Names @@ -40,21 +38,19 @@ let toplevel_env () = in l,seb | _ -> failwith "caught" in - match current_toplevel () with - | _ -> SEBstruct (List.rev (map_succeed get_reference seg)) - + SEBstruct (List.rev (map_succeed get_reference seg)) + let environment_until dir_opt = let rec parse = function | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] | [] -> [] | d :: l -> - let mb = Global.lookup_module (MPfile d) in - (* If -dont-load-proof has been used, mod_expr is None, - we try with mod_type *) - let meb = Option.default mb.mod_type mb.mod_expr in - if dir_opt = Some d then [MPfile d, meb] - else (MPfile d, meb) :: (parse l) + match (Global.lookup_module (MPfile d)).mod_expr with + | Some meb -> + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) + | _ -> assert false in parse (Library.loaded_libraries ()) @@ -68,6 +64,9 @@ module type VISIT = sig (* Add the module_path and all its prefixes to the mp visit list *) val add_mp : module_path -> unit + (* Same, but we'll keep all fields of these modules *) + val add_mp_all : module_path -> unit + (* Add kernel_name / constant / reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) val add_ind : mutual_inductive -> unit @@ -81,6 +80,7 @@ module type VISIT = sig val needed_ind : mutual_inductive -> bool val needed_con : constant -> bool val needed_mp : module_path -> bool + val needed_mp_all : module_path -> bool end module Visit : VISIT = struct @@ -88,16 +88,26 @@ module Visit : VISIT = struct (for inductives and modules names) and a Cset_env for constants (and still the remaining MPset) *) type must_visit = - { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t } + { mutable ind : KNset.t; mutable con : KNset.t; + mutable mp : MPset.t; mutable mp_all : MPset.t } (* the imperative internal visit lists *) - let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty } + let v = { ind = KNset.empty ; con = KNset.empty ; + mp = MPset.empty; mp_all = MPset.empty } (* the accessor functions *) - let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty + let reset () = + v.ind <- KNset.empty; + v.con <- KNset.empty; + v.mp <- MPset.empty; + v.mp_all <- MPset.empty let needed_ind i = KNset.mem (user_mind i) v.ind let needed_con c = KNset.mem (user_con c) v.con - let needed_mp mp = MPset.mem mp v.mp + let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all + let needed_mp_all mp = MPset.mem mp v.mp_all let add_mp mp = check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_mp_all mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp; + v.mp_all <- MPset.add mp v.mp_all let add_ind i = let kn = user_mind i in v.ind <- KNset.add kn v.ind; add_mp (modpath kn) @@ -120,12 +130,17 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with - | None -> raise Impossible - | Some lbody -> - match kind_of_term (Declarations.force lbody) with + | Def lbody -> + (match kind_of_term (Declarations.force lbody) with | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd) | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd) - | _ -> raise Impossible + | _ -> raise Impossible) + | Undef _ | OpaqueDef _ -> raise Impossible + +let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = + na1 = na2 && + array_equal eq_constr ca1 ca2 && + array_equal eq_constr ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in @@ -139,7 +154,8 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - if check <> check_fix env cb' (j+1) then raise Impossible; + let check' = check_fix env cb' (j+1) in + if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' @@ -157,7 +173,8 @@ let rec seb2mse = function let expand_seb env mp seb = let seb,_,_,_ = - Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) + let inl = Some (Flags.get_inline_level()) in + Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb) in seb (** When possible, we use the nicer, shorter, algebraic type structures @@ -200,9 +217,8 @@ let rec extract_sfb_spec env mp = function if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in - let s = Sind (kn, extract_inductive env mind) in + let mind = make_mind mp empty_dirpath l in + let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end @@ -223,7 +239,7 @@ let rec extract_sfb_spec env mp = function *) and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with - | SEBident mp -> Visit.add_mp mp; MTident mp + | SEBident mp -> Visit.add_mp_all mp; MTident mp | SEBwith(seb',With_definition_body(idl,cb))-> let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in let mt = extract_seb_spec env mp1 (seb,seb') in @@ -231,7 +247,7 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with | None -> mt | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) | SEBwith(seb',With_module_body(idl,mp))-> - Visit.add_mp mp; + Visit.add_mp_all mp; MTwith(extract_seb_spec env mp1 (seb,seb'), ML_With_module(idl,mp)) | SEBfunctor (mbid, mtb, seb_alg') -> @@ -283,11 +299,10 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in + let mind = make_mind mp empty_dirpath l in let b = Visit.needed_ind mind in if all || b then - let d = Dind (kn, extract_inductive env mind) in + let d = Dind (mind, extract_inductive env mind) in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -312,7 +327,7 @@ and extract_seb env mp all = function extract_seb env mp all (expand_seb env mp seb) | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; - Visit.add_mp mp; MEident mp + Visit.add_mp_all mp; MEident mp | SEBapply (meb, meb',_) -> MEapply (extract_seb env mp true meb, extract_seb env mp true meb') @@ -346,11 +361,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = Visit.reset (); List.iter Visit.add_ref refs; - List.iter Visit.add_mp mpl; + List.iter Visit.add_mp_all mpl; let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m)) + l (**************************************) (*S Part II : Input/Output primitives *) @@ -488,13 +504,18 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init modular = +let init modular library = check_inside_section (); check_inside_module (); set_keywords (descr ()).keywords; set_modular modular; + set_library library; reset (); if modular && lang () = Scheme then error_scheme () +let warns () = + warning_opaques (access_opaque ()); + warning_axioms () + (* From a list of [reference], let's retrieve whether they correspond to modules or [global_reference]. Warn the user if both is possible. *) @@ -503,7 +524,8 @@ let rec locate_ref = function | r::l -> let q = snd (qualid_of_reference r) in let mpo = try Some (Nametab.locate_module q) with Not_found -> None - and ro = try Some (Nametab.locate q) with Not_found -> None in + and ro = try Some (Smartlocate.global_with_alias r) with _ -> None + in match mpo, ro with | None, None -> Nametab.error_global_not_found q | None, Some r -> let refs,mps = locate_ref l in r::refs,mps @@ -518,25 +540,41 @@ let rec locate_ref = function \verb!Extraction "file"! [qualid1] ... [qualidn]. *) let full_extr f (refs,mps) = - init false; + init false false; List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps; - let struc = optimize_struct refs (mono_environment refs mps) in - warning_axioms (); + let struc = optimize_struct (refs,mps) (mono_environment refs mps) in + warns (); print_structure_to_file (mono_filename f) false struc; reset () let full_extraction f lr = full_extr f (locate_ref lr) +(*s Separate extraction is similar to recursive extraction, with the output + decomposed in many files, one per Coq .v file *) + +let separate_extraction lr = + init true false; + let refs,mps = locate_ref lr in + let struc = optimize_struct (refs,mps) (mono_environment refs mps) in + warns (); + let print = function + | (MPfile dir as mp, sel) as e -> + print_structure_to_file (module_filename mp) false [e] + | _ -> assert false + in + List.iter print struc; + reset () + (*s Simple extraction in the Coq toplevel. The vernacular command is \verb!Extraction! [qualid]. *) let simple_extraction r = match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> - init false; - let struc = optimize_struct [r] (mono_environment [r] []) in + init false false; + let struc = optimize_struct ([r],[]) (mono_environment [r] []) in let d = get_decl_in_structure r struc in - warning_axioms (); + warns (); if is_custom r then msgnl (str "(** User defined extraction *)"); print_one_decl struc (modpath_of_r r) d; reset () @@ -547,12 +585,12 @@ let simple_extraction r = match locate_ref [r] with \verb!(Recursive) Extraction Library! [M]. *) let extraction_library is_rec m = - init true; + init true true; let dir_m = let q = qualid_of_ident m in try Nametab.full_name_module q with Not_found -> error_unknown_module q in - Visit.add_mp (MPfile dir_m); + Visit.add_mp_all (MPfile dir_m); let env = Global.env () in let l = List.rev (environment_until (Some dir_m)) in let select l (mp,meb) = @@ -561,8 +599,8 @@ let extraction_library is_rec m = else l in let struc = List.fold_left select [] l in - let struc = optimize_struct [] struc in - warning_axioms (); + let struc = optimize_struct ([],[]) struc in + warns (); let print = function | (MPfile dir as mp, sel) as e -> let dry = not is_rec && dir <> dir_m in |