From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- library/declare.ml | 19 ++++++++++++++++--- library/declare.mli | 5 +++++ library/declaremods.ml | 23 +++++++++++++++++++++-- library/declaremods.mli | 7 +++++++ library/lib.ml | 6 ++++++ library/lib.mli | 4 ++++ library/library.ml | 3 +++ library/library.mli | 3 +++ 8 files changed, 65 insertions(+), 5 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 994a6557a..8d86c4cf0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -32,6 +32,14 @@ type internal_flag = | InternalTacticRequest (* kernel action, no message is displayed *) | UserIndividualRequest (* user action, a message is displayed *) +(** XML output hooks *) + +let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore () +let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore () +let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** Declaration of section variables and local definitions *) type section_variable_entry = @@ -83,6 +91,7 @@ let declare_variable id obj = declare_var_implicits id; Notation.declare_ref_arguments_scope (VarRef id); Heads.declare_head (EvalVarRef id); + if_xml (Hook.get f_xml_declare_variable) oname; oname @@ -216,6 +225,7 @@ let declare_constant_common id cst = let id = Label.to_id (pi3 (Constant.repr3 c)) in ignore(add_leaf id o); update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in match role with | Safe_typing.Subproof -> () | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) @@ -257,6 +267,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e cst_was_seff = false; } in let kn = declare_constant_common id cst in + let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn let declare_definition ?(internal=UserIndividualRequest) @@ -365,8 +376,9 @@ let declare_projections mind = let kn' = declare_constant id (ProjectionEntry entry, IsDefinition StructureComponent) in - assert(eq_constant kn kn')) kns; true - | Some None | None -> false + assert(eq_constant kn kn')) kns; true,true + | Some None -> true,false + | None -> false,false (* for initial declaration *) let declare_mind mie = @@ -375,9 +387,10 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mind in + let isrecord,isprim = declare_projections mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; + if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname); oname, isprim (* Declaration messages *) diff --git a/library/declare.mli b/library/declare.mli index c6119a58a..60676ff43 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -71,6 +71,11 @@ val set_declare_scheme : the whole block and a boolean indicating if it is a primitive record. *) val declare_mind : mutual_inductive_entry -> object_name * bool +(** Hooks for XML output *) +val xml_declare_variable : (object_name -> unit) Hook.t +val xml_declare_constant : (internal_flag * constant -> unit) Hook.t +val xml_declare_inductive : (bool * object_name -> unit) Hook.t + (** Declaration messages *) val definition_message : Id.t -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index 7f607a51c..0162de10c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -557,6 +557,17 @@ let openmodtype_info = Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" +(** XML output hooks *) + +let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore () +let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore () +let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore () +let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore () +let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore () +let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore () + +let if_xml f x = if !Flags.xml_export then f x else () + (** {6 Modules : start, end, declare} *) module RawModOps = struct @@ -578,7 +589,9 @@ let start_module interp_modast export id args res fs = openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module) mp; + mp let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in @@ -617,6 +630,7 @@ let end_module () = assert (ModPath.equal (mp_of_kn (snd newoname)) mp); Lib.add_frozen_state () (* to prevent recaching *); + if_xml (Hook.get f_xml_end_module) mp; mp let declare_module interp_modast id args res mexpr_o fs = @@ -666,6 +680,7 @@ let declare_module interp_modast id args res mexpr_o fs = let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in ignore (Lib.add_leaf id (in_module sobjs)); + if_xml (Hook.get f_xml_declare_module) mp; mp end @@ -682,7 +697,9 @@ let start_modtype interp_modast id args mtys fs = openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); - Lib.add_frozen_state (); mp + Lib.add_frozen_state (); + if_xml (Hook.get f_xml_start_module_type) mp; + mp let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in @@ -699,6 +716,7 @@ let end_modtype () = assert (ModPath.equal (mp_of_kn (snd oname)) mp); Lib.add_frozen_state ()(* to prevent recaching *); + if_xml (Hook.get f_xml_end_module_type) mp; mp let declare_modtype interp_modast id args mtys (mty,ann) fs = @@ -729,6 +747,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = check_subtypes_mt mp sub_mty_l; ignore (Lib.add_leaf id (in_modtype sobjs)); + if_xml (Hook.get f_xml_declare_module_type) mp; mp end diff --git a/library/declaremods.mli b/library/declaremods.mli index 319d168d0..8b9f70b35 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -63,6 +63,13 @@ val start_modtype : val end_modtype : unit -> module_path +(** Hooks for XML output *) +val xml_declare_module : (module_path -> unit) Hook.t +val xml_start_module : (module_path -> unit) Hook.t +val xml_end_module : (module_path -> unit) Hook.t +val xml_declare_module_type : (module_path -> unit) Hook.t +val xml_start_module_type : (module_path -> unit) Hook.t +val xml_end_module_type : (module_path -> unit) Hook.t (** {6 Libraries i.e. modules on disk } *) diff --git a/library/lib.ml b/library/lib.ml index 297441e6e..42cea4de8 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -497,6 +497,10 @@ let full_section_segment_of_constant con = (*************) (* Sections. *) +(* XML output hooks *) +let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore () +let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore () + let open_section id = let olddir,(mp,oldsec) = !path_prefix in let dir = add_dirpath_suffix olddir id in @@ -508,6 +512,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; + if !Flags.xml_export then Hook.get f_xml_open_section id; add_section () @@ -536,6 +541,7 @@ let close_section () = let full_olddir = fst !path_prefix in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); + if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/lib.mli b/library/lib.mli index bb8831759..398149a50 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -157,6 +157,10 @@ val unfreeze : frozen -> unit val init : unit -> unit +(** XML output hooks *) +val xml_open_section : (Names.Id.t -> unit) Hook.t +val xml_close_section : (Names.Id.t -> unit) Hook.t + (** {6 Section management for discharge } *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types diff --git a/library/library.ml b/library/library.ml index 024ac9e6f..365d119dd 100644 --- a/library/library.ml +++ b/library/library.ml @@ -555,6 +555,8 @@ let in_require : require_obj -> obj = (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) +let (f_xml_require, xml_require) = Hook.make ~default:ignore () + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in @@ -568,6 +570,7 @@ let require_library_from_dirpath modrefl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); + if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl; add_frozen_state () (* the function called by Vernacentries.vernac_import *) diff --git a/library/library.mli b/library/library.mli index d5e610dd6..fb0ce4795 100644 --- a/library/library.mli +++ b/library/library.mli @@ -67,6 +67,9 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit +(** {6 Hook for the xml exportation of libraries } *) +val xml_require : (DirPath.t -> unit) Hook.t + (** {6 Locate a library in the load paths } *) exception LibUnmappedDir exception LibNotFound -- cgit v1.2.3