Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 47 insertions, 53 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 34071182..95092814 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 7602 2005-11-23 15:10:16Z barras $ *)
+(* $Id: safe_typing.ml 8898 2006-06-05 23:15:51Z letouzey $ *)
 
 open Util
 open Names
@@ -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,36 +223,18 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module l params result 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 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 [] }
   in
   mp, { old = senv;
-	env = env;
+	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
 	revsign = [];
@@ -261,21 +242,21 @@ let start_module l params result senv =
 	imports = senv.imports;
 	loads = [] }
 
-
-
-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_map (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;
-  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
@@ -288,10 +269,10 @@ let end_module l senv =
 	    mtb, Some mtb, cst
   in
   let mexpr = 
-    List.fold_right
-      (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
-      params
+    List.fold_left
+      (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
       (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
+      params
   in
   let mb = 
     { mod_expr = Some mexpr;
@@ -326,31 +307,44 @@ let end_module l 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 = [];
@@ -370,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
@@ -520,9 +514,9 @@ let import (dp,mb,depends,engmt) digest senv =
  
 let rec lighten_module mb =
   { mb with
-    mod_expr = option_app lighten_modexpr mb.mod_expr;
+    mod_expr = option_map lighten_modexpr mb.mod_expr;
     mod_type = lighten_modtype mb.mod_type;
-    mod_user_type = option_app lighten_modtype mb.mod_user_type }
+    mod_user_type = option_map lighten_modtype mb.mod_user_type }
 
 and lighten_modtype = function
   | MTBident kn as x -> x