Inversion de l'ordre de chargement des objets logiques et non logiques

à la déclaration des paramètres de foncteurs (problème de
synchronisation révélé par bug #1118, apparu suite à l'appel de
lookup_mind par load_struct, suite au passage à un discharge local)

Les objets non logiques sont maintenant chargés après car ils peuvent
dépendre d'objets logiques. Et comme les objets non logiques
(p.ex. l'import récursif de modules dans la nametab) sont nécessaires
au typage de l'éventuelle contrainte de module, on reporte la gestion
de la contrainte au moment du end_module (on aurait peut-être pu faire
plus fin et extraire dans do_module la partie purement module, mais
après tout le report de la contrainte de type dans le end_module ne
semble pas génante).

À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les
définitions de module non interactives.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8721 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 79 insertions, 48 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index b33b12d2b..0c1cafdd7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -122,6 +122,18 @@ let msid_of_prefix (_,(mp,sec)) =
     anomaly ("Non-empty section in module name!" ^ 
 	     string_of_mp mp ^ "." ^ string_of_dirpath sec)
 
+(* Check that a module type is not functorial *)
+
+let rec check_sig env = function
+  | MTBident kn -> check_sig env (Environ.lookup_modtype kn env)
+  | MTBsig _ -> ()
+  | MTBfunsig _ -> Modops.error_result_must_be_signature ()
+
+let rec check_sig_entry env = function
+  | MTEident kn -> check_sig env (Environ.lookup_modtype kn env)
+  | MTEsig _ -> ()
+  | MTEfunsig _ -> Modops.error_result_must_be_signature ()
+  | MTEwith (mte,_) -> check_sig_entry env mte
 
 (* This function checks if the type calculated for the module [mp] is
    a subtype of [sub_mtb]. Uses only the global environment. *)
@@ -434,57 +446,60 @@ let rec get_some_body mty env = match mty with
       replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
 
 
-let intern_args interp_modtype (env,oldargs) (idl,arg) = 
+let intern_args interp_modtype (env,oldargs,oldsubst) (idl,arg) = 
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype env arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
   let mps = List.map (fun mbid -> MPbound mbid) mbids in
   let substobjs = get_modtype_substobjs mty in
-  let substituted's = 
+  let substituted's =
     List.map2 
-      (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) 
-      dirs mps  
+      (fun dir mp -> dir, mp, substobjs, subst_substobjs dir mp substobjs) 
+      dirs mps 
   in
-    List.iter 
-      (fun (dir, mp, substituted) -> 
-	 do_module false "interp" load_objects 1 dir mp substobjs substituted)
-      substituted's;
-    let body = Modops.module_body_of_type (get_some_body mty env) in
-    let env = 
-      List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
-    in
-    env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
-      
+  let body = Modops.module_body_of_type (get_some_body mty env) in
+  let env = 
+    List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
+  in
+    env, List.map (fun mbid -> mbid,mty) mbids :: oldargs, 
+        substituted's :: oldsubst
+
+let load_args_object (dir,mp,substobjs,substituted) =
+  do_module false "interp" load_objects 1 dir mp substobjs substituted
+
 let start_module interp_modtype export id args res_o =
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  let env,arg_entries_revlist,substituted_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[],[]) args 
   in
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
 
+  let mp = Global.start_module id arg_entries in
+
+  List.iter (List.iter load_args_object) (List.rev substituted_revlist);
+
   let res_entry_o, sub_body_o = match res_o with
       None -> None, None
-    | Some (res, true) ->
-	Some (interp_modtype env res), None
-    | Some (res, false) ->
-	(* If the module type is non-restricting, we must translate it
-	   here to catch errors as early as possible. If it is
-	   estricting, the kernel takes care of it.  *)
-	let sub_mte = 
-	  List.fold_right 
-	    (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
-	    arg_entries 
-	    (interp_modtype env res)
+    | Some (res, restricted) ->
+	(* we translate the module here to catch errors as early as possible *)
+	let mte = interp_modtype env res in
+	check_sig_entry env mte;
+	if restricted then 
+	  Some mte, None
+	else
+	  let mtb = Mod_typing.translate_modtype (Global.env()) mte in
+	  let sub_mtb = 
+	    List.fold_right 
+	      (fun (arg_id,arg_t) mte -> 
+		let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t
+		in MTBfunsig(arg_id,arg_t,mte))
+	      arg_entries mtb
 	in
-	let sub_mtb = 
-	  Mod_typing.translate_modtype (Global.env()) sub_mte
-	in
-	  None, Some sub_mtb
-  in
+	None, Some sub_mtb
 
-  let mp = Global.start_module id arg_entries res_entry_o in
+  in
 
   let mbids = List.map fst arg_entries in
   openmod_info:=(mbids,res_entry_o,sub_body_o);
@@ -496,8 +511,8 @@ let start_module interp_modtype export id args res_o =
 let end_module id =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
-  let mp = Global.end_module id in
   let mbids, res_o, sub_o = !openmod_info in
+  let mp = Global.end_module id res_o in
     
   begin match sub_o with
       None -> ()
@@ -645,13 +660,15 @@ let import_module export mp =
 let start_modtype interp_modtype id args =
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  let env,arg_entries_revlist,substituted_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[],[]) args 
   in
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
 
   let mp = Global.start_modtype id arg_entries in
 
+  List.iter (List.iter load_args_object) (List.rev substituted_revlist);
+
   let mbids = List.map fst arg_entries in
   openmodtype_info := mbids;
   let prefix = Lib.start_modtype id mp fs in
@@ -686,10 +703,23 @@ let end_modtype id =
 let declare_modtype interp_modtype id args mty = 
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  let env,arg_entries_revlist,substituted_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[],[]) args 
   in
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  (* Too strong: may depend of the logical object which are not registered,
+     while only names are needed in the constraint and the body;
+     The example
+
+     Module Type T. Record t : Set := { a : nat }. Parameter b:Set. End T.
+     Module A.      Record t : Set := { a : nat }. Definition b:=t. End A.
+     Module F (X:T) : T with Definition b:=X.t := A.
+
+     fails (15 Apr 2006) *)
+
+  List.iter (List.iter load_args_object) (List.rev substituted_revlist);
+
   let base_mty = interp_modtype env mty in
   let entry = 
     List.fold_right 
@@ -733,10 +763,13 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 
   let fs = Summary.freeze_summaries () in
   let env = Global.env () in
-  let env,arg_entries_revlist = 
-    List.fold_left (intern_args interp_modtype) (env,[]) args 
+  let env,arg_entries_revlist,substituted_revlist = 
+    List.fold_left (intern_args interp_modtype) (env,[],[]) args 
   in
   let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+  List.iter (List.iter load_args_object) (List.rev substituted_revlist);
+
   let mty_entry_o, mty_sub_o = match mty_o with
       None -> None, None
     | (Some (mty, true)) -> 
diff --git a/library/global.ml b/library/global.ml
index d4ad97a8c..6ad414339 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -73,15 +73,15 @@ let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let start_module id params mtyo =
+let start_module id params =
   let l = label_of_id id in
-  let mp,newenv = start_module l params mtyo !global_env in
+  let mp,newenv = start_module l params !global_env in
     global_env := newenv;
     mp
   
-let end_module id =
+let end_module id mtyo =
   let l = label_of_id id in
-  let mp,newenv = end_module l !global_env in
+  let mp,newenv = end_module l mtyo !global_env in
     global_env := newenv;
     mp
 
diff --git a/library/global.mli b/library/global.mli
index 579882498..af6ec6ae9 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -64,12 +64,10 @@ val set_engagement : engagement -> unit
    of the started module / module type *)
 
 val start_module : 
-  identifier -> (mod_bound_id * module_type_entry) list 
-    -> module_type_entry option 
-      -> module_path
+  identifier -> (mod_bound_id * module_type_entry) list -> module_path
 
 val end_module :
-  identifier -> module_path
+  identifier -> module_type_entry option -> module_path
 
 val start_modtype :
   identifier -> (mod_bound_id * module_type_entry) list