Nouveau mécanisme pour les modules interactifs : les arguments de

foncteurs sont données un par un ce qui permet de faire les
load_objects correspondants au bon moment (càd juste après l'ajout des
déclarations logiques et avant l'ajout du paramètre suivant).  Ceci
clôt le bug #1118 et corrige des erreurs de localisation introduite
par le commit précédent.


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

2 files changed, 41 insertions, 40 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ca1bf6f65a..2a165f74e1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -223,29 +223,18 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module l params senv = 
+let start_module l senv = 
   check_label l senv.labset; 
-  let rec trans_params env = function 
-    | [] -> env,[] 
-    | (mbid,mte)::rest -> 
-	let mtb = translate_modtype env mte in
-	let env = 
-	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
-	in
-	let env,transrest = trans_params env rest in
-	env, (mbid,mtb)::transrest
-  in
-  let env,params_body = trans_params senv.env params in
   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 }
+		  variant = STRUCT [] }
   in
   mp, { old = senv;
-	env = env;
+	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
 	revsign = [];
@@ -253,8 +242,6 @@ let start_module l params senv =
 	imports = senv.imports;
 	loads = [] }
 
-
-
 let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
@@ -266,9 +253,10 @@ let end_module l restype senv =
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
-  let functorize_type = 
-    List.fold_right 
-      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+  let functorize_type tb = 
+    List.fold_left
+      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
+      tb
       params
   in
   let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
@@ -319,31 +307,44 @@ let end_module l restype senv =
 	loads = senv.loads@oldsenv.loads }
 
 
+(* Adding parameters to modules or module types *)
+
+let add_module_parameter mbid mte senv =
+  if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then
+    anomaly "Cannot add a module parameter to a non empty module";
+  let mtb = translate_modtype senv.env mte in
+  let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env 
+  in
+  let new_variant = match senv.modinfo.variant with
+    | STRUCT params -> STRUCT ((mbid,mtb) :: params)
+    | SIG params -> SIG ((mbid,mtb) :: params)
+    | _ -> 
+	anomaly "Module parameters can only be added to modules or signatures"
+  in
+  { old = senv.old;
+    env = env;
+    modinfo = { senv.modinfo with variant = new_variant };
+    labset = senv.labset;
+    revsign = [];
+    revstruct = [];
+    imports = senv.imports;
+    loads = [] }
+
+
 (* Interactive module types *)
 
-let start_modtype l params senv = 
+let start_modtype l senv = 
   check_label l senv.labset; 
-  let rec trans_params env = function 
-    | [] -> env,[] 
-    | (mbid,mte)::rest -> 
-	let mtb = translate_modtype env mte in
-	let env = 
-	  full_add_module (MPbound mbid) (module_body_of_type mtb) env 
-	in
-	let env,transrest = trans_params env rest in
-	env, (mbid,mtb)::transrest
-  in
-  let env,params_body = trans_params senv.env params in
   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 = SIG params_body }
+		  variant = SIG [] }
   in
   mp, { old = senv;
-	env = env;
+	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
 	revsign = [];
@@ -363,10 +364,10 @@ let end_modtype l senv =
   if not (empty_context senv.env) then error_local_context None;
   let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
   let mtb = 
-    List.fold_right 
-      (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
-      params
+    List.fold_left
+      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
       res_tb
+      params
   in
   let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
   let newenv = oldsenv.env in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 43755b9085..1b4d932b59 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -72,17 +72,17 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 
 (*s Interactive module functions *)
 val start_module : 
-  label -> (mod_bound_id * module_type_entry) list 
-      -> safe_environment -> module_path * safe_environment
+  label -> safe_environment -> module_path * safe_environment
 
 val end_module :
   label -> module_type_entry option 
       -> safe_environment -> module_path * safe_environment 
 
+val add_module_parameter :
+  mod_bound_id -> module_type_entry -> safe_environment -> safe_environment
 
 val start_modtype :
-  label -> (mod_bound_id * module_type_entry) list
-    -> safe_environment -> module_path * safe_environment
+  label -> safe_environment -> module_path * safe_environment
 
 val end_modtype :
   label -> safe_environment -> kernel_name * safe_environment