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

1 files changed, 43 insertions, 88 deletions

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)