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

7 files changed, 89 insertions, 65 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index b20e7259d..166b23007 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -41,7 +41,7 @@ let error_incompatible_labels l l' =
   error ("Opening and closing labels are not the same: "
 	 ^string_of_label l^" <> "^string_of_label l'^" !")
 
-let error_result_must_be_signature mtb = 
+let error_result_must_be_signature () = 
   error "The result module type must be a signature"
 
 let error_signature_expected mtb =
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f102a5b2c..b8f1f66a3 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -74,7 +74,7 @@ val error_incompatible_labels : label -> label -> 'a
 
 val error_no_such_label : label -> 'a
 
-val error_result_must_be_signature : module_type_body -> 'a
+val error_result_must_be_signature : unit -> 'a
 
 val error_signature_expected : module_type_body -> 'a
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9b638427c..ca1bf6f65 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -30,7 +30,6 @@ type modvariant =
   | NONE 
   | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
   | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
-      * (* optional result type *) module_type_body option
   | LIBRARY of dir_path
 
 type module_info = 
@@ -224,7 +223,7 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module l params result senv = 
+let start_module l params senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -237,20 +236,13 @@ let start_module l params result senv =
 	env, (mbid,mtb)::transrest
   in
   let env,params_body = trans_params senv.env params in
-  let check_sig mtb = match scrape_modtype env mtb with
-    | MTBsig _ -> ()
-    | MTBfunsig _ -> error_result_must_be_signature mtb 
-    | _ -> anomaly "start_module: modtype not scraped"
-  in
-  let result_body = option_app (translate_modtype env) result in
-  ignore (option_app check_sig result_body);
   let msid = make_msid senv.modinfo.seed (string_of_label l) in
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = STRUCT(params_body,result_body) }
+		  variant = STRUCT params_body }
   in
   mp, { old = senv;
 	env = env;
@@ -263,13 +255,14 @@ let start_module l params result senv =
 
 
 
-let end_module l senv = 
+let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let params, restype = 
+  let restype = option_app (translate_modtype senv.env) restype in
+  let params = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
-      | STRUCT(params,restype) -> (params,restype)
+      | STRUCT params -> params
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5412287ee..43755b908 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,11 +73,11 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 (*s Interactive module functions *)
 val start_module : 
   label -> (mod_bound_id * module_type_entry) list 
-    -> module_type_entry option 
       -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> safe_environment -> module_path * safe_environment 
+  label -> module_type_entry option 
+      -> safe_environment -> module_path * safe_environment 
 
 
 val start_modtype :
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