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 --- interp/modintern.ml | 131 +++++++++++++++++----------------------------------- 1 file changed, 43 insertions(+), 88 deletions(-) (limited to 'interp/modintern.ml') diff --git a/interp/modintern.ml b/interp/modintern.ml index f91d9ff22..d809f0221 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -10,6 +10,7 @@ open Entries open Libnames open Constrexpr open Constrintern +open Misctypes type module_internalization_error = | NotAModuleNorModtype of string @@ -18,32 +19,17 @@ type module_internalization_error = exception ModuleInternalizationError of module_internalization_error -(* -val error_declaration_not_path : module_struct_entry -> 'a +let error_not_a_module_loc kind loc qid = + let s = string_of_qualid qid in + let e = match kind with + | Module -> Modops.ModuleTypingError (Modops.NotAModule s) + | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) + | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) + in + Loc.raise loc e -val error_not_a_functor : module_struct_entry -> 'a - -val error_not_equal : module_path -> module_path -> 'a - -oval error_not_a_modtype_loc : loc -> string -> 'a - -val error_not_a_module_loc : loc -> string -> 'a - -val error_not_a_module_or_modtype_loc : loc -> string -> 'a - -val error_with_in_module : unit -> 'a - -val error_application_to_module_type : unit -> 'a -*) - -let error_not_a_modtype_loc loc s = - Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) - -let error_not_a_module_loc loc s = - Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) - -let error_not_a_module_nor_modtype_loc loc s = - Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) +let error_application_to_not_path loc me = + Loc.raise loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me)) let error_incorrect_with_in_module loc = Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) @@ -51,35 +37,25 @@ let error_incorrect_with_in_module loc = let error_application_to_module_type loc = Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) +(** Searching for a module name in the Nametab. -(* Search for the head of [qid] in [binders]. - If found, returns the module_path/kernel_name created from the dirpath - and the basename. Searches Nametab otherwise. -*) -let lookup_module (loc,qid) = - try - let mp = Nametab.locate_module qid in - Dumpglob.dump_modref loc mp "modtype"; mp - with - | Not_found -> error_not_a_module_loc loc (string_of_qualid qid) - -let lookup_modtype (loc,qid) = - try - let mp = Nametab.locate_modtype qid in - Dumpglob.dump_modref loc mp "mod"; mp - with - | Not_found -> - error_not_a_modtype_loc loc (string_of_qualid qid) + According to the input module kind, modules or module types + or both are searched. The returned kind is never ModAny, and + it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype (loc,qid) = +let lookup_module_or_modtype kind (loc,qid) = try + if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in - Dumpglob.dump_modref loc mp "modtype"; (mp,true) - with Not_found -> try - let mp = Nametab.locate_modtype qid in - Dumpglob.dump_modref loc mp "mod"; (mp,false) + Dumpglob.dump_modref loc mp "modtype"; (mp,Module) with Not_found -> - error_not_a_module_nor_modtype_loc loc (string_of_qualid qid) + try + if kind == Module then raise Not_found; + let mp = Nametab.locate_modtype qid in + Dumpglob.dump_modref loc mp "mod"; (mp,ModType) + with Not_found -> error_not_a_module_loc kind loc qid + +let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> @@ -90,48 +66,27 @@ let transl_with_decl env = function let loc_of_module = function | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc -let check_module_argument_is_path me' = function - | CMident _ -> () - | (CMapply (loc,_,_) | CMwith (loc,_,_)) -> - Loc.raise loc - (Modops.ModuleTypingError (Modops.ApplicationToNotPath me')) - -let rec interp_modexpr env = function - | CMident qid -> - MSEident (lookup_module qid) - | CMapply (_,me1,me2) -> - let me1' = interp_modexpr env me1 in - let me2' = interp_modexpr env me2 in - check_module_argument_is_path me2' me2; - MSEapply(me1',me2') - | CMwith (loc,_,_) -> error_incorrect_with_in_module loc - +let is_path = function + | CMident _ -> true + | CMapply _ | CMwith _ -> false -let rec interp_modtype env = function - | CMident qid -> - MSEident (lookup_modtype qid) - | CMapply (_,mty1,me) -> - let mty' = interp_modtype env mty1 in - let me' = interp_modexpr env me in - check_module_argument_is_path me' me; - MSEapply(mty',me') - | CMwith (_,mty,decl) -> - let mty = interp_modtype env mty in - let decl = transl_with_decl env decl in - MSEwith(mty,decl) +(* Invariant : the returned kind is never ModAny, and it is + equal to the input kind when this one isn't ModAny. *) -let rec interp_modexpr_or_modtype env = function +let rec interp_module_ast env kind = function | CMident qid -> - let (mp,ismod) = lookup_module_or_modtype qid in - (MSEident mp, ismod) + let (mp,kind) = lookup_module_or_modtype kind qid in + (MSEident mp, kind) | CMapply (_,me1,me2) -> - let me1',ismod1 = interp_modexpr_or_modtype env me1 in - let me2',ismod2 = interp_modexpr_or_modtype env me2 in - check_module_argument_is_path me2' me2; - if not ismod2 then error_application_to_module_type (loc_of_module me2); - (MSEapply (me1',me2'), ismod1) + let me1',kind1 = interp_module_ast env kind me1 in + let me2',kind2 = interp_module_ast env ModAny me2 in + if not (is_path me2) then + error_application_to_not_path (loc_of_module me2) me2'; + if kind2 == ModType then + error_application_to_module_type (loc_of_module me2); + (MSEapply (me1',me2'), kind1) | CMwith (loc,me,decl) -> - let me,ismod = interp_modexpr_or_modtype env me in + let me,kind = interp_module_ast env kind me in + if kind == Module then error_incorrect_with_in_module loc; let decl = transl_with_decl env decl in - if ismod then error_incorrect_with_in_module loc; - (MSEwith(me,decl), ismod) + (MSEwith(me,decl), kind) -- cgit v1.2.3