diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 419 |
1 files changed, 238 insertions, 181 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 84088292..42e69d34 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -1,18 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Miniml open Term open Declarations open Names open Libnames +open Globnames open Pp +open Errors open Util -open Miniml open Table open Extraction open Modutil @@ -24,33 +26,41 @@ open Mod_subst (***************************************) let toplevel_env () = - let seg = Lib.contents_after None in let get_reference = function | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in - let seb = match Libobject.object_tag o with - | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) - | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn)) - | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) + begin match Libobject.object_tag o with + | "CONSTANT" -> + let constant = Global.lookup_constant (constant_of_kn kn) in + Some (l, SFBconst constant) + | "INDUCTIVE" -> + let inductive = Global.lookup_mind (mind_of_kn kn) in + Some (l, SFBmind inductive) + | "MODULE" -> + let modl = Global.lookup_module (MPdot (mp, l)) in + Some (l, SFBmodule modl) | "MODULE TYPE" -> - SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) - | _ -> failwith "caught" - in l,seb - | _ -> failwith "caught" + let modtype = Global.lookup_modtype (MPdot (mp, l)) in + Some (l, SFBmodtype modtype) + | "INCLUDE" -> error "No extraction of toplevel Include yet." + | _ -> None + end + | _ -> None in - SEBstruct (List.rev (map_succeed get_reference seg)) + List.rev (List.map_filter get_reference (Lib.contents ())) let environment_until dir_opt = let rec parse = function - | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] + | [] when Option.is_empty dir_opt -> [Lib.current_mp (), toplevel_env ()] | [] -> [] | d :: 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 + let meb = + Modops.destr_nofunctor (Global.lookup_module (MPfile d)).mod_type + in + match dir_opt with + | Some d' when DirPath.equal d d' -> [MPfile d, meb] + | _ -> (MPfile d, meb) :: (parse l) in parse (Library.loaded_libraries ()) @@ -61,16 +71,12 @@ 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 - - (* Same, but we'll keep all fields of these modules *) + (* Add the module_path and all its prefixes to the mp visit list. + We'll keep all fields of these modules. *) val add_mp_all : module_path -> unit - (* Add kernel_name / constant / reference / ... in the visit lists. + (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_ind : mutual_inductive -> 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 @@ -84,9 +90,6 @@ module type VISIT = sig end module Visit : VISIT = struct - (* What used to be in a single KNset should now be split into a KNset - (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 mp_all : MPset.t } @@ -122,6 +125,15 @@ module Visit : VISIT = struct let add_spec_deps = spec_iter_references add_ref add_ref add_ref end +let add_field_label mp = function + | (lab, SFBconst _) -> Visit.add_ref (ConstRef (Constant.make2 mp lab)) + | (lab, SFBmind _) -> Visit.add_ref (IndRef (MutInd.make2 mp lab, 0)) + | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab)) + +let rec add_labels mp = function + | MoreFunctor (_,_,m) -> add_labels mp m + | NoFunctor sign -> List.iter (add_field_label mp) sign + exception Impossible let check_arity env cb = @@ -131,31 +143,31 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body 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) + (match kind_of_term (Mod_subst.force_constr lbody) with + | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) + | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> 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 + Array.equal Name.equal 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 let n = Array.length (let fi,_,_ = recd in fi) in - if n = 1 then [|l|], recd, msb + if Int.equal n 1 then [|l|], recd, msb else begin if List.length msb < n-1 then raise Impossible; - let msb', msb'' = list_chop (n-1) msb in + let msb', msb'' = List.chop (n-1) msb in let labels = Array.make n l in - list_iter_i + List.iteri (fun j -> function | (l,SFBconst cb') -> let check' = check_fix env cb' (j+1) in - if not (fst check = fst check' && + if not ((fst check : bool) == (fst check') && prec_declaration_equal (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; @@ -163,113 +175,102 @@ let factor_fix env l cb msb = labels, recd, msb'' end -(** Expanding a [struct_expr_body] into a version without abbreviations +(** Expanding a [module_alg_expr] into a version without abbreviations or functor applications. This is done via a detour to entries (hack proposed by Elie) *) -let rec seb2mse = function - | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s') - | SEBident mp -> Entries.MSEident mp - | _ -> failwith "seb2mse: received a non-atomic seb" - -let expand_seb env mp seb = - let 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 - instead of the expanded ones. *) - -let my_type_of_mb mb = - let m0 = mb.mod_type in - match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0 - -let my_type_of_mtb mtb = - let m0 = mtb.typ_expr in - match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0 +let expand_mexpr env mp me = + let inl = Some (Flags.get_inline_level()) in + let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in + sign (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) -let rec msid_of_seb = function - | SEBident mp -> mp - | SEBwith (seb,_) -> msid_of_seb seb +let rec mp_of_mexpr = function + | MEident mp -> mp + | MEwith (seb,_) -> mp_of_mexpr seb | _ -> assert false -let env_for_mtb_with_def env mp seb idl = - let sig_b = match seb with - | SEBstruct(sig_b) -> sig_b - | _ -> assert false - in - let l = label_of_id (List.hd idl) in - let spot = function (l',SFBconst _) -> l = l' | _ -> false in - let before = fst (list_split_when spot sig_b) in - Modops.add_signature mp before empty_delta_resolver env +let env_for_mtb_with_def env mp me idl = + let struc = Modops.destr_nofunctor me in + let l = Label.of_id (List.hd idl) in + let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in + let before = fst (List.split_when spot struc) in + Modops.add_structure mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) to specifications. *) -let rec extract_sfb_spec env mp = function +let rec extract_structure_spec env mp = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = make_con mp empty_dirpath l in + let kn = Constant.make2 mp l in let s = extract_constant_spec env kn cb in - let specs = extract_sfb_spec env mp msig in + let specs = extract_structure_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = make_mind mp empty_dirpath l in + let mind = MutInd.make2 mp l in let s = Sind (mind, extract_inductive env mind) in - let specs = extract_sfb_spec env mp msig in + let specs = extract_structure_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> - let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in + let specs = extract_structure_spec env mp msig in + let spec = extract_mbody_spec env mb.mod_mp mb in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> - let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in + let specs = extract_structure_spec env mp msig in + let spec = extract_mbody_spec env mtb.mod_mp mtb in (l,Smodtype spec) :: specs -(* From [struct_expr_body] to specifications *) +(* From [module_expression] to specifications *) -(* Invariant: the [seb] given to [extract_seb_spec] should either come +(* Invariant: the [me] given to [extract_mexpr_spec] should either come from a [mod_type] or [type_expr] field, or their [_alg] counterparts. - This way, any encountered [SEBident] should be a true module type. + This way, any encountered [MEident] should be a true module type. *) -and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with - | SEBident mp -> Visit.add_mp_all mp; MTident mp - | SEBwith(seb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in - let mt = extract_seb_spec env mp1 (seb,seb') in - (match extract_with_type env' cb with (* cb peut contenir des kn *) +and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with + | MEident mp -> Visit.add_mp_all mp; MTident mp + | MEwith(me',WithDef(idl,c))-> + let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in + let mt = extract_mexpr_spec env mp1 (me_struct,me') in + (match extract_with_type env' c with (* cb may contain some kn *) | None -> mt | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) - | SEBwith(seb',With_module_body(idl,mp))-> + | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; - MTwith(extract_seb_spec env mp1 (seb,seb'), - ML_With_module(idl,mp)) - | SEBfunctor (mbid, mtb, seb_alg') -> - let seb' = match seb with - | SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb' + MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) + | MEapply _ -> extract_msignature_spec env mp1 me_struct + +and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with + | MoreFunctor (mbid, mtb, me_alg') -> + let me_struct' = match me_struct with + | MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me' | _ -> assert false in let mp = MPbound mbid in - let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in - MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb), - extract_seb_spec env' mp1 (seb',seb_alg')) - | SEBstruct (msig) -> - let env' = Modops.add_signature mp1 msig empty_delta_resolver env in - MTsig (mp1, extract_sfb_spec env' mp1 msig) - | SEBapply _ -> - if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb) - else assert false - + let env' = Modops.add_module_type mp mtb env in + MTfunsig (mbid, extract_mbody_spec env mp mtb, + extract_mexpression_spec env' mp1 (me_struct',me_alg')) + | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) + +and extract_msignature_spec env mp1 = function + | NoFunctor struc -> + let env' = Modops.add_structure mp1 struc empty_delta_resolver env in + MTsig (mp1, extract_structure_spec env' mp1 struc) + | MoreFunctor (mbid, mtb, me) -> + let mp = MPbound mbid in + let env' = Modops.add_module_type mp mtb env in + MTfunsig (mbid, extract_mbody_spec env mp mtb, + extract_msignature_spec env' mp1 me) +and extract_mbody_spec env mp mb = match mb.mod_type_alg with + | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty) + | None -> extract_msignature_spec env mp mb.mod_type (* From a [structure_body] (i.e. a list of [structure_field_body]) to implementations. @@ -278,88 +279,117 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with important: last to first ensures correct dependencies. *) -let rec extract_sfb env mp all = function +let rec extract_structure env mp ~all = function | [] -> [] - | (l,SFBconst cb) :: msb -> + | (l,SFBconst cb) :: struc -> (try - let vl,recd,msb = factor_fix env l cb msb in - let vc = Array.map (make_con mp empty_dirpath) vl in - let ms = extract_sfb env mp all msb in - let b = array_exists Visit.needed_con vc in + let vl,recd,struc = factor_fix env l cb struc in + let vc = Array.map (Constant.make2 mp) vl in + let ms = extract_structure env mp ~all struc in + let b = Array.exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_sfb env mp all msb in - let c = make_con mp empty_dirpath l in + let ms = extract_structure env mp ~all struc in + let c = Constant.make2 mp l in let b = Visit.needed_con c in if all || b then let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) - | (l,SFBmind mib) :: msb -> - let ms = extract_sfb env mp all msb in - let mind = make_mind mp empty_dirpath l in + | (l,SFBmind mib) :: struc -> + let ms = extract_structure env mp ~all struc in + let mind = MutInd.make2 mp l in let b = Visit.needed_ind mind in if all || b then 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 - | (l,SFBmodule mb) :: msb -> - let ms = extract_sfb env mp all msb in + | (l,SFBmodule mb) :: struc -> + let ms = extract_structure env mp ~all struc in let mp = MPdot (mp,l) in - if all || Visit.needed_mp mp then - (l,SEmodule (extract_module env mp true mb)) :: ms + let all' = all || Visit.needed_mp_all mp in + if all' || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms else ms - | (l,SFBmodtype mtb) :: msb -> - let ms = extract_sfb env mp all msb in + | (l,SFBmodtype mtb) :: struc -> + let ms = extract_structure env mp ~all struc in let mp = MPdot (mp,l) in - if all || Visit.needed_mp mp then - (l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms + if all || Visit.needed_mp mp then + (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms else ms -(* From [struct_expr_body] to implementations *) +(* From [module_expr] and [module_expression] to implementations *) -and extract_seb env mp all = function - | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml -> - (* in Haskell/Scheme, we expand everything *) - extract_seb env mp all (expand_seb env mp seb) - | SEBident mp -> +and extract_mexpr env mp = function + | MEwith _ -> assert false (* no 'with' syntax for modules *) + | me when lang () != Ocaml -> + (* In Haskell/Scheme, we expand everything. + For now, we also extract everything, dead code will be removed later + (see [Modutil.optimize_struct]. *) + extract_msignature env mp ~all:true (expand_mexpr env mp me) + | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; - Visit.add_mp_all mp; MEident mp - | SEBapply (meb, meb',_) -> - MEapply (extract_seb env mp true meb, - extract_seb env mp true meb') - | SEBfunctor (mbid, mtb, meb) -> + Visit.add_mp_all mp; Miniml.MEident mp + | MEapply (me, arg) -> + Miniml.MEapply (extract_mexpr env mp me, + extract_mexpr env mp (MEident arg)) + +and extract_mexpression env mp = function + | NoFunctor me -> extract_mexpr env mp me + | MoreFunctor (mbid, mtb, me) -> + let mp1 = MPbound mbid in + let env' = Modops.add_module_type mp1 mtb env in + Miniml.MEfunctor + (mbid, + extract_mbody_spec env mp1 mtb, + extract_mexpression env' mp me) + +and extract_msignature env mp ~all = function + | NoFunctor struc -> + let env' = Modops.add_structure mp struc empty_delta_resolver env in + Miniml.MEstruct (mp,extract_structure env' mp ~all struc) + | MoreFunctor (mbid, mtb, me) -> let mp1 = MPbound mbid in - let env' = Modops.add_module (Modops.module_body_of_type mp1 mtb) - env in - MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb), - extract_seb env' mp true meb) - | SEBstruct (msb) -> - let env' = Modops.add_signature mp msb empty_delta_resolver env in - MEstruct (mp,extract_sfb env' mp all msb) - | SEBwith (_,_) -> anomaly "Not available yet" - -and extract_module env mp all mb = + let env' = Modops.add_module_type mp1 mtb env in + Miniml.MEfunctor + (mbid, + extract_mbody_spec env mp1 mtb, + extract_msignature env' mp ~all me) + +and extract_module env mp ~all mb = (* A module has an empty [mod_expr] when : - it is a module variable (for instance X inside a Module F [X:SIG]) - it is a module assumption (Declare Module). Since we look at modules from outside, we shouldn't have variables. But a Declare Module at toplevel seems legal (cf #2525). For the moment we don't support this situation. *) - match mb.mod_expr with - | None -> error_no_module_expr mp - | Some me -> - { ml_mod_expr = extract_seb env mp all me; - ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } - - -let unpack = function MEstruct (_,sel) -> sel | _ -> assert false + let impl = match mb.mod_expr with + | Abstract -> error_no_module_expr mp + | Algebraic me -> extract_mexpression env mp me + | Struct sign -> + (* This module has a signature, otherwise it would be FullStruct. + We extract just the elements required by this signature. *) + let () = add_labels mp mb.mod_type in + extract_msignature env mp ~all:false sign + | FullStruct -> extract_msignature env mp ~all mb.mod_type + in + (* Slight optimization: for modules without explicit signatures + ([FullStruct] case), we build the type out of the extracted + implementation *) + let typ = match mb.mod_expr with + | FullStruct -> + assert (Option.is_empty mb.mod_type_alg); + mtyp_of_mexpr impl + | _ -> extract_mbody_spec env mp mb + in + { ml_mod_expr = impl; + ml_mod_type = typ } let mono_environment refs mpl = Visit.reset (); @@ -368,7 +398,8 @@ let mono_environment refs 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 (Visit.needed_mp_all mp) m)) + (fun (mp,struc) -> + mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc) l (**************************************) @@ -383,7 +414,7 @@ let descr () = match lang () with (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" Works similarly for the other languages. *) -let default_id = id_of_string "Main" +let default_id = Id.of_string "Main" let mono_filename f = let d = descr () in @@ -396,10 +427,10 @@ let mono_filename f = else f in let id = - if lang () <> Haskell then default_id + if lang () != Haskell then default_id else - try id_of_string (Filename.basename f) - with e when Errors.noncritical e -> + try Id.of_string (Filename.basename f) + with UserError _ -> error "Extraction: provided filename is not a valid identifier" in Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id @@ -409,7 +440,7 @@ let mono_filename f = let module_filename mp = let f = file_of_modfile mp in let d = descr () in - Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f (*s Extraction of one decl to stdout. *) @@ -420,8 +451,9 @@ let print_one_decl struc mp decl = ignore (d.pp_struct struc); set_phase Impl; push_visible mp []; - msgnl (d.pp_decl decl); - pop_visible () + let ans = d.pp_decl decl in + pop_visible (); + ans (*s Extraction of a ml struct to a file. *) @@ -449,31 +481,39 @@ let formatter dry file = (* note: max_indent should be < margin above, otherwise it's ignored *) ft +let get_comment () = + let s = file_comment () in + if String.is_empty s then None + else + let split_comment = Str.split (Str.regexp "[ \t\n]+") s in + Some (prlist_with_sep spc str split_comment) + let print_structure_to_file (fn,si,mo) dry struc = Buffer.clear buf; let d = descr () in reset_renaming_tables AllButExternal; let unsafe_needs = { - mldummy = struct_ast_search ((=) MLdummy) struc; + mldummy = struct_ast_search ((==) MLdummy) struc; tdummy = struct_type_search Mlutil.isDummy struc; - tunknown = struct_type_search ((=) Tunknown) struc; + tunknown = struct_type_search ((==) Tunknown) struc; magic = - if lang () <> Haskell then false + if lang () != Haskell then false else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } in (* First, a dry run, for computing objects to rename or duplicate *) set_phase Pre; let devnull = formatter true None in - msg_with devnull (d.pp_struct struc); + pp_with devnull (d.pp_struct struc); let opened = opened_libraries () in (* Print the implementation *) let cout = if dry then None else Option.map open_out fn in let ft = formatter dry cout in + let comment = get_comment () in begin try (* The real printing of the implementation *) set_phase Impl; - msg_with ft (d.preamble mo opened unsafe_needs); - msg_with ft (d.pp_struct struc); + pp_with ft (d.preamble mo comment opened unsafe_needs); + pp_with ft (d.pp_struct struc); Option.iter close_out cout; with reraise -> Option.iter close_out cout; raise reraise @@ -486,8 +526,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let ft = formatter false (Some cout) in begin try set_phase Intf; - msg_with ft (d.sig_preamble mo opened unsafe_needs); - msg_with ft (d.pp_sig (signature_of_structure struc)); + pp_with ft (d.sig_preamble mo comment opened unsafe_needs); + pp_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; with reraise -> close_out cout; raise reraise @@ -495,8 +535,8 @@ let print_structure_to_file (fn,si,mo) dry struc = info_file si) (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) - if Buffer.length buf <> 0 then begin - Pp.message (Buffer.contents buf); + if not (Int.equal (Buffer.length buf) 0) then begin + Pp.msg_info (str (Buffer.contents buf)); Buffer.reset buf end @@ -515,7 +555,7 @@ let init modular library = set_modular modular; set_library library; reset (); - if modular && lang () = Scheme then error_scheme () + if modular && lang () == Scheme then error_scheme () let warns () = warning_opaques (access_opaque ()); @@ -531,7 +571,7 @@ let rec locate_ref = function let mpo = try Some (Nametab.locate_module q) with Not_found -> None and ro = try Some (Smartlocate.global_with_alias r) - with e when Errors.noncritical e -> None + with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with | None, None -> Nametab.error_global_not_found q @@ -576,7 +616,7 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global (Genarg.AN r); + Vernacentries.dump_global (Misctypes.AN r); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> @@ -584,9 +624,13 @@ let simple_extraction r = let struc = optimize_struct ([r],[]) (mono_environment [r] []) in let d = get_decl_in_structure r struc in warns (); - if is_custom r then msgnl (str "(** User defined extraction *)"); - print_one_decl struc (modpath_of_r r) d; - reset () + let flag = + if is_custom r then str "(** User defined extraction *)" ++ fnl() + else mt () + in + let ans = flag ++ print_one_decl struc (modpath_of_r r) d in + reset (); + Pp.msg_info ans | _ -> assert false @@ -602,9 +646,9 @@ let extraction_library is_rec 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) = + let select l (mp,struc) = if Visit.needed_mp mp - then (mp, unpack (extract_seb env mp true meb)) :: l + then (mp, extract_structure env mp true struc) :: l else l in let struc = List.fold_left select [] l in @@ -612,9 +656,22 @@ let extraction_library is_rec m = warns (); let print = function | (MPfile dir as mp, sel) as e -> - let dry = not is_rec && dir <> dir_m in + let dry = not is_rec && not (DirPath.equal dir dir_m) in print_structure_to_file (module_filename mp) dry [e] | _ -> assert false in List.iter print struc; reset () + +let structure_for_compute c = + init false false; + let env = Global.env () in + let ast, mlt = Extraction.extract_constr env c in + let ast = Mlutil.normalize ast in + let refs = ref Refset.empty in + let add_ref r = refs := Refset.add r !refs in + let () = ast_iter_references add_ref add_ref add_ref ast in + let refs = Refset.elements !refs in + let struc = optimize_struct (refs,[]) (mono_environment refs []) in + let flatstruc = List.map snd (List.flatten (List.map snd struc)) in + flatstruc, ast, mlt |