diff options
Diffstat (limited to 'contrib/extraction/extract_env.ml')
-rw-r--r-- | contrib/extraction/extract_env.ml | 299 |
1 files changed, 161 insertions, 138 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 2d425e9f..e31b701c 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) +(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*) open Term open Declarations @@ -53,23 +53,55 @@ let environment_until dir_opt = | _ -> assert false in parse (Library.loaded_libraries ()) -type visit = - { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t } -let in_kn v kn = KNset.mem kn v.kn -let in_ref v ref = Refset.mem ref v.ref -let in_mp v mp = MPset.mem mp v.mp - -let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp -let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn) -let visit_ref v r = - let r = - (* if we meet a constructor we must export the inductive definition *) - match r with - ConstructRef (r,_) -> IndRef r - | _ -> r - in - v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) +(*s Visit: + a structure recording the needed dependencies for the current extraction *) + +module type VISIT = sig + (* Reset the dependencies by emptying the visit lists *) + val reset : unit -> unit + + (* Add the module_path and all its prefixes to the mp visit list *) + val add_mp : 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_kn : kernel_name -> unit + val add_con : constant -> unit + val add_ref : global_reference -> unit + val add_decl_deps : ml_decl -> unit + val add_spec_deps : ml_spec -> unit + + (* Test functions: + is a particular object a needed dependency for the current extraction ? *) + val needed_kn : kernel_name -> bool + val needed_con : constant -> bool + val needed_mp : module_path -> bool +end + +module Visit : VISIT = struct + (* Thanks to C.S.C, what used to be in a single KNset should now be split + into a KNset (for inductives and modules names) and a Cset for constants + (and still the remaining MPset) *) + type must_visit = + { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t } + (* the imperative internal visit lists *) + let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } + (* the accessor functions *) + let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty + let needed_kn kn = KNset.mem kn v.kn + let needed_con c = Cset.mem c v.con + let needed_mp mp = MPset.mem mp v.mp + let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) + let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) + let add_ref = function + | ConstRef c -> add_con c + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn + | VarRef _ -> assert false + let add_decl_deps = decl_iter_references add_ref add_ref add_ref + let add_spec_deps = spec_iter_references add_ref add_ref add_ref +end exception Impossible @@ -104,115 +136,108 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let get_decl_references v d = - let f = visit_ref v in decl_iter_references f f f d - -let get_spec_references v s = - let f = visit_ref v in spec_iter_references f f f s - -let rec extract_msig env v mp = function +let rec extract_msig env mp = function | [] -> [] | (l,SPBconst cb) :: msig -> let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmind cb) :: msig -> let kn = make_kn mp empty_dirpath l in let s = Sind (kn, extract_inductive env kn) in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmodule {msb_modtype=mtb}) :: msig -> -(*i let mpo = Some (MPdot (mp,l)) in i*) - (l,Smodule (extract_mtb env v None (*i mpo i*) mtb)) :: (extract_msig env v mp msig) + (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig) + (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) -and extract_mtb env v mpo = function - | MTBident kn -> visit_kn v kn; MTident kn +and extract_mtb env mpo = function + | MTBident kn -> Visit.add_kn kn; MTident kn | MTBfunsig (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_mtb env v None mtb, - extract_mtb env' v None mtb') + MTfunsig (mbid, extract_mtb env None mtb, + extract_mtb env' None mtb') | MTBsig (msid, msig) -> let mp, msig = match mpo with | None -> MPself msid, msig | Some mp -> mp, Modops.subst_signature_msid msid mp msig in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' v mp msig) + MTsig (msid, extract_msig env' mp msig) -let rec extract_msb env v mp all = function +let rec extract_msb env mp all = function | [] -> [] | (l,SEBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in - let ms = extract_msb env v mp all msb in - let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in + let vc = Array.map (make_con mp empty_dirpath) vl in + let ms = extract_msb env mp all msb in + let b = array_exists Visit.needed_con vc in if all || b then - let d = extract_fixpoint env vkn recd in + let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_msb env v mp all msb in - let kn = make_con mp empty_dirpath l in - let b = in_ref v (ConstRef kn) in + let ms = extract_msb env mp all msb in + let c = make_con mp empty_dirpath l in + let b = Visit.needed_con c in if all || b then - let d = extract_constant env kn cb in + let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SEBmind mib) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *) + let b = Visit.needed_kn kn in if all || b then let d = Dind (kn, extract_inductive env kn) in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SEBmodule mb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let mp = MPdot (mp,l) in - if all || in_mp v mp then - (l,SEmodule (extract_module env v mp true mb)) :: ms + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true mb)) :: ms else ms | (l,SEBmodtype mtb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - if all || in_kn v kn then - (l,SEmodtype (extract_mtb env v None mtb)) :: ms + if all || Visit.needed_kn kn then + (l,SEmodtype (extract_mtb env None mtb)) :: ms else ms -and extract_meb env v mpo all = function +and extract_meb env mpo all = function | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> visit_mp v mp; MEident mp + | MEBident mp -> Visit.add_mp mp; MEident mp | MEBapply (meb, meb',_) -> - MEapply (extract_meb env v None true meb, - extract_meb env v None true meb') + MEapply (extract_meb env None true meb, + extract_meb env None true meb') | MEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_mtb env v None mtb, - extract_meb env' v None true meb) + MEfunctor (mbid, extract_mtb env None mtb, + extract_meb env' None true meb) | MEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb | Some mp -> mp, subst_msb (map_msid msid mp) msb in let env' = add_structure mp msb env in - MEstruct (msid, extract_msb env' v mp all msb) + MEstruct (msid, extract_msb env' mp all msb) -and extract_module env v mp all mb = +and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) let meb = out_some mb.mod_expr in @@ -220,25 +245,21 @@ and extract_module env v mp all mb = (* Because of the "with" construct, the module type can be [MTBsig] with *) (* a msid different from the one of the module. Here is the patch. *) let mtb = replicate_msid meb mtb in - { ml_mod_expr = extract_meb env v (Some mp) all meb; - ml_mod_type = extract_mtb env v None mtb } + { ml_mod_expr = extract_meb env (Some mp) all meb; + ml_mod_type = extract_mtb env None mtb } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = - let l = environment_until None in - let v = - let add_ref r = Refset.add r in - let refs = List.fold_right add_ref refs Refset.empty in - let add_mp mp = MPset.union (prefixes_mp mp) in - let mps = List.fold_right add_mp mpl MPset.empty in - let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in - { kn = KNset.empty; ref = refs; mp = mps } - in + Visit.reset (); + List.iter Visit.add_ref refs; + List.iter Visit.add_mp mpl; let env = Global.env () in - List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) - (List.rev l) + let l = List.rev (environment_until None) in + List.rev_map + (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l + (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) @@ -259,6 +280,7 @@ let mono_extraction (f,m) qualids = let prm = {modular=false; mod_name = m; to_appear= refs} in let struc = optimize_struct prm None (mono_environment refs mps) in print_structure_to_file f prm struc; + Visit.reset (); reset_tables () let extraction_rec = mono_extraction (None,id_of_string "Main") @@ -277,15 +299,15 @@ let extraction qid = let r = Nametab.global qid in if is_custom r then msgnl (str "User defined extraction:" ++ spc () ++ - str (find_custom r) ++ fnl ()) - else begin + str (find_custom r) ++ fnl ()) + else let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in + { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in let struc = optimize_struct prm None (mono_environment [r] []) in let d = get_decl_in_structure r struc in print_one_decl struc (modpath_of_r r) d; - reset_tables () - end + Visit.reset (); + reset_tables () (*s Extraction to a file (necessarily recursive). The vernacular command is @@ -313,32 +335,33 @@ let extraction_file f vl = let extraction_module m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let q = snd (qualid_of_reference m) in - let mp = - try Nametab.locate_module q - with Not_found -> error_unknown_module q - in - let b = is_modfile mp in - let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in - let l = environment_until None in - let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in - let env = Global.env () in - let struc = - List.rev_map - (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m)) - (List.rev l) - in - let struc = optimize_struct prm None struc in - let struc = - let bmp = base_mp mp in - try [bmp, List.assoc bmp struc] with Not_found -> assert false - in - print_structure_to_file None prm struc; - reset_tables () + | _ -> () + end; + let q = snd (qualid_of_reference m) in + let mp = + try Nametab.locate_module q with Not_found -> error_unknown_module q + in + let b = is_modfile mp in + let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in + Visit.reset (); + Visit.add_mp mp; + let env = Global.env () in + let l = List.rev (environment_until None) in + let struc = + List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l + in + let struc = optimize_struct prm None struc in + let struc = + let bmp = base_mp mp in + try [bmp, List.assoc bmp struc] with Not_found -> assert false + in + print_structure_to_file None prm struc; + Visit.reset (); + reset_tables () + (*s (Recursive) Extraction of a library. The vernacular command is \verb!(Recursive) Extraction Library! [M]. *) @@ -355,38 +378,38 @@ let dir_module_of_id m = let extraction_library is_rec m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let dir_m = dir_module_of_id m in - let v = - { kn = KNset.empty; ref = Refset.empty; - mp = MPset.singleton (MPfile dir_m) } in - let l = environment_until (Some dir_m) in - let struc = - let env = Global.env () in - let select l (mp,meb) = - if in_mp v mp (* [mp] est long -> [in_mp] peut etre sans [long_mp] *) - then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l - else l - in - List.fold_left select [] (List.rev l) - in - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let struc = optimize_struct dummy_prm None struc in - let rec print = function - | [] -> () - | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l - | (MPfile dir, sel) as e :: l -> - let short_m = snd (split_dirpath dir) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - print_structure_to_file (Some f) prm [e]; - print l - | _ -> assert false - in print struc; - reset_tables () + | _ -> () + end; + let dir_m = dir_module_of_id m in + Visit.reset (); + Visit.add_mp (MPfile dir_m); + let env = Global.env () in + let l = List.rev (environment_until (Some dir_m)) in + let select l (mp,meb) = + if Visit.needed_mp mp + then (mp, unpack (extract_meb env (Some mp) true meb)) :: l + else l + in + let struc = List.fold_left select [] l in + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let struc = optimize_struct dummy_prm None struc in + let rec print = function + | [] -> () + | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l + | (MPfile dir, sel) as e :: l -> + let short_m = snd (split_dirpath dir) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + print_structure_to_file (Some f) prm [e]; + print l + | _ -> assert false + in + print struc; + Visit.reset (); + reset_tables () |