From 466c4cbacfb5ffb19ad9a042af7ab1f43441f925 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 17 Jul 2013 15:32:11 +0000 Subject: Declaremods: major refactoring, stop duplicating libobjects in modules When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.mli | 80 ++++++++++++++++++++++++------------------------- 1 file changed, 39 insertions(+), 41 deletions(-) (limited to 'library/declaremods.mli') diff --git a/library/declaremods.mli b/library/declaremods.mli index b76017286..f18ed2807 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,42 +6,36 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc -open Pp open Names -open Entries -open Environ -open Libnames -open Libobject -open Lib open Vernacexpr (** {6 Modules } *) -(** [declare_module interp_modtype interp_modexpr id fargs typ expr] - declares module [id], with type constructed by [interp_modtype] - from functor arguments [fargs] and [typ] and with module body - constructed by [interp_modtype] from functor arguments [fargs] and - by [interp_modexpr] from [expr]. At least one of [typ], [expr] must - be non-empty. +type 'modast module_interpretor = + Environ.env -> Misctypes.module_kind -> 'modast -> + Entries.module_struct_entry * Misctypes.module_kind - The [bool] in [typ] tells if the module must be abstracted [true] - with respect to the module type or merely matched without any - restriction [false]. -*) +type 'modast module_params = + (Id.t Loc.located list * ('modast * inline)) list + +(** [declare_module interp_modast id fargs typ exprs] + declares module [id], with structure constructed by [interp_modast] + from functor arguments [fargs], with final type [typ]. + [exprs] is usually of length 1 (Module definition with a concrete + body), but it could also be empty ("Declare Module", with non-empty [typ]), + or multiple (body of the shape M <+ N <+ ...). *) val declare_module : - (env -> 'modast -> module_struct_entry) -> - (env -> 'modast -> module_struct_entry) -> - (env -> 'modast -> module_struct_entry * bool) -> + 'modast module_interpretor -> Id.t -> - (Id.t located list * ('modast * inline)) list -> + 'modast module_params -> ('modast * inline) module_signature -> ('modast * inline) list -> module_path -val start_module : (env -> 'modast -> module_struct_entry) -> +val start_module : + 'modast module_interpretor -> bool option -> Id.t -> - (Id.t located list * ('modast * inline)) list -> + 'modast module_params -> ('modast * inline) module_signature -> module_path val end_module : unit -> module_path @@ -50,28 +44,26 @@ val end_module : unit -> module_path (** {6 Module types } *) -val declare_modtype : (env -> 'modast -> module_struct_entry) -> - (env -> 'modast -> module_struct_entry * bool) -> +(** [declare_modtype interp_modast id fargs typs exprs] + Similar to [declare_module], except that the types could be multiple *) + +val declare_modtype : + 'modast module_interpretor -> Id.t -> - (Id.t located list * ('modast * inline)) list -> + 'modast module_params -> ('modast * inline) list -> ('modast * inline) list -> module_path -val start_modtype : (env -> 'modast -> module_struct_entry) -> - Id.t -> (Id.t located list * ('modast * inline)) list -> +val start_modtype : + 'modast module_interpretor -> + Id.t -> + 'modast module_params -> ('modast * inline) list -> module_path val end_modtype : unit -> module_path -(** {6 ... } *) -(** Objects of a module. They come in two lists: the substitutive ones - and the other *) - -val module_objects : module_path -> library_segment - - (** {6 Libraries i.e. modules on disk } *) type library_name = DirPath.t @@ -92,7 +84,8 @@ val end_library : (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for - every object of the module. Raises [Not_found] when [mp] is unknown. *) + every object of the module. Raises [Not_found] when [mp] is unknown + or when [mp] corresponds to a functor. *) val really_import_module : module_path -> unit @@ -104,8 +97,8 @@ val import_module : bool -> module_path -> unit (** Include *) -val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * inline) list -> unit +val declare_include : + 'modast module_interpretor -> ('modast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' @@ -113,11 +106,16 @@ val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> in an arbitrary order. The given function is applied to all leaves (together with their section path). *) -val iter_all_segments : (object_name -> obj -> unit) -> unit +val iter_all_segments : + (Libnames.object_name -> Libobject.obj -> unit) -> unit val debug_print_modtab : unit -> Pp.std_ppcmds -(** For Printer *) -val process_module_seb_binding : +(** For printing modules, [process_module_binding] adds names of + bound module (and its components) to Nametab. It also loads + objects associated to it. It may raise a [Failure] when the + bound module hasn't an atomic type. *) + +val process_module_binding : MBId.t -> Declarations.struct_expr_body -> unit -- cgit v1.2.3