Corrections de gestion des univers et modules + meilleure gestions des noms uniques

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

9 files changed, 97 insertions, 55 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ae45c932cd..ee1167b8f4 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -168,7 +168,9 @@ and module_expr_body =
       * constraints
 
 and module_specification_body = 
-    module_type_body * module_path option * constraints
+    { msb_modtype : module_type_body;
+      msb_equiv : module_path option; 
+      msb_constraints : constraints }
 
 and structure_elem_body = 
   | SEBconst of constant_body
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index e37686c409..83ea8c713e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -108,12 +108,16 @@ and module_expr_body =
   | MEBident of module_path
   | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
   | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body
-      * constraints
+  | MEBapply of module_expr_body * module_expr_body  (* (F A) *)
+      * constraints  (* type_of(A) <: input_type_of(F) *)
 
 and module_specification_body = 
-    module_type_body * module_path option * constraints
-
+    { msb_modtype : module_type_body;
+      msb_equiv : module_path option; 
+      msb_constraints : constraints }
+    (*    type_of(equiv) <: modtype  (if given)  
+       +  substyping of past With_Module mergers *)
+    
 and structure_elem_body = 
   | SEBconst of constant_body
   | SEBmind of mutual_inductive_body
@@ -128,8 +132,8 @@ and module_body =
       mod_type : module_type_body;
       mod_equiv : module_path option;
       mod_constraints : constraints }
-
-
+    (*    type_of(mod_expr)  <: mod_user_type (if given)  *)
+    (*  if equiv given then constraints are empty *)
 
 
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ba4dcf0b7f..785e8ebdda 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -95,27 +95,34 @@ and merge_with env mtb with_decl =
 				      Some (Declarations.from_val j.uj_val);
 				    const_constraints = cst}
 		  | Some b -> 
-		      let cst1 = Reduction.conv env' c (Declarations.force b) in 
+		      let cst1 = Reduction.conv env' c (Declarations.force b) in
 		      let cst = Constraint.union cb.const_constraints cst1 in
 			SPBconst {cb with 
 				    const_body = Some (Declarations.from_val c);
 				    const_constraints = cst}
 	      end	
+(* and what about msid's ????? Don't they clash ? *)
 	| With_Module (id, mp) ->
-	    let (oldmtb,oldequiv,oldcst) = match spec with
-		SPBmodule (mtb,equiv,cst) -> (mtb,equiv,cst)
+	    let old = match spec with
+		SPBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	    let mtb = type_modpath env' mp in
-	    let cst = check_subtypes env' mtb oldmtb in
+	 (* here, we should assert that there is no msid in mtb *)
+	    let cst = check_subtypes env' mtb old.msb_modtype in
 	    let equiv = 
- 	      match oldequiv with
+ 	      match old.msb_equiv with
 		| None -> Some mp
 		| Some mp' -> 
 		    check_modpath_equiv env' mp mp';
 		    Some mp
 	    in
-	      SPBmodule (mtb, equiv, Constraint.union oldcst cst)
+	    let msb =
+	      {msb_modtype = mtb; 
+	       msb_equiv = equiv; 
+	       msb_constraints = Constraint.union old.msb_constraints cst }
+	    in
+	      SPBmodule msb
       in
 	MTBsig(msid,  before@(l,new_spec)::after)
     with
@@ -135,7 +142,11 @@ and translate_entry_list env msid is_definition sig_e =
 	    add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
       | SPEmodule me ->
 	  let mb = translate_module env is_definition me in
-	  let mspec = mb.mod_type, mb.mod_equiv, mb.mod_constraints in
+	  let mspec = 
+	    { msb_modtype = mb.mod_type;
+	      msb_equiv = mb.mod_equiv;
+	      msb_constraints = mb.mod_constraints }
+	  in
 	  let mp' = MPdot (mp,l) in
 	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
       | SPEmodtype mte ->
@@ -254,10 +265,17 @@ and add_struct_elem_constraints env = function
   | SEBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
+  (* if there is a body, the mb.mod_type is either inferred from the
+     body and hence uninteresting or equal to the non-empty
+     user_mod_type *)
   let env = match mb.mod_expr with
-    | None -> env
+    | None -> add_modtype_constraints env mb.mod_type
     | Some meb -> add_module_expr_constraints env meb
   in
+  let env = match mb.mod_user_type with
+    | None -> env
+    | Some mtb -> add_modtype_constraints env mtb
+  in
     Environ.add_constraints mb.mod_constraints env
 
 and add_modtype_constraints env = function
@@ -275,7 +293,7 @@ and add_modtype_constraints env = function
 and add_sig_elem_constraints env = function 
   | SPBconst cb -> Environ.add_constraints cb.const_constraints env
   | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SPBmodule (mtb,_,cst) -> 
+  | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> 
       add_modtype_constraints (Environ.add_constraints cst env) mtb
   | SPBmodtype mtb -> add_modtype_constraints env mtb
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index a75f2d4832..cd8cbe1ee1 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -70,13 +70,13 @@ let rec scrape_modtype env = function
   | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
   | mtb -> mtb
 
-
-let module_body_of_spec (mty,mpo,cst) = 
-    { mod_type = mty;
-      mod_equiv = mpo;
+(* the constraints are not important here *)
+let module_body_of_spec msb = 
+    { mod_type = msb.msb_modtype;
+      mod_equiv = msb.msb_equiv;
       mod_expr = None;
       mod_user_type = None;
-      mod_constraints = cst}
+      mod_constraints = Constraint.empty}
 
 let module_body_of_type mtb = 
   { mod_type = mtb;
@@ -86,7 +86,13 @@ let module_body_of_type mtb =
     mod_constraints = Constraint.empty}
 
 
-let module_spec_of_body mb = mb.mod_type, mb.mod_equiv, mb.mod_constraints
+(* the constraints are not important here *)
+let module_spec_of_body mb = 
+  { msb_modtype = mb.mod_type; 
+    msb_equiv = mb.mod_equiv; 
+    msb_constraints = Constraint.empty}
+
+
 
 let destr_functor = function
   | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
@@ -129,11 +135,14 @@ and subst_signature sub sign =
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
-and subst_module sub (mtb,mpo,cst as mb) =
-  let mtb' = subst_modtype sub mtb in
-  let mpo' = option_smartmap (subst_mp sub) mpo in
-    if mtb'==mtb && mpo'==mpo then mb else
-      (mtb',mpo',cst)
+and subst_module sub mb =
+  let mtb' = subst_modtype sub mb.msb_modtype in
+  let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in
+    if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
+      { msb_modtype=mtb'; 
+	msb_equiv=mpo'; 
+	msb_constraints=mb.msb_constraints}
+
 
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
@@ -179,13 +188,15 @@ let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
   | MTBident _ -> anomaly "scrape_modtype does not work!"
   | MTBfunsig _ -> mtb
   | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-and strengthen_mod env mp (mtb,mpo,cst) = 
-  let mtb' = strengthen_mtb env mp mtb in
-  let mpo' = match mpo with
-    | Some _ -> mpo
-    | None -> Some mp
-  in
-    (mtb',mpo',cst)
+
+and strengthen_mod env mp msb = 
+  { msb_modtype = strengthen_mtb env mp msb.msb_modtype;
+    msb_equiv = begin match msb.msb_equiv with
+      | Some _ -> msb.msb_equiv
+      | None -> Some mp 
+    end ;
+    msb_constraints = msb.msb_constraints; }
+
 and strengthen_sig env msid sign mp = match sign with
   | [] -> []
   | (l,SPBconst cb) :: rest ->
diff --git a/kernel/names.ml b/kernel/names.ml
index f25e6680d3..7b0078392d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -246,9 +246,12 @@ module KNpred = Predicate.Make(KNord)
 module KNset = Set.Make(KNord)
 
 
-let initial_msid = (make_msid [] "TOP")
-let initial_path = MPself initial_msid
+let default_module_name = id_of_string "Top"
+
+let initial_dir = make_dirpath [default_module_name]
 
+let initial_msid = (make_msid initial_dir "Top")
+let initial_path = MPself initial_msid
 
 type variable = identifier
 type constant = kernel_name
diff --git a/kernel/names.mli b/kernel/names.mli
index 83509075e4..31684371d3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -125,6 +125,9 @@ val occur_mbid : mod_bound_id -> substitution -> bool
 val initial_msid : mod_self_id
 val initial_path : module_path (* [= MPself initial_msid] *)
 
+(* Initial "seed" of the unique identifier generator *)
+val initial_dir : dir_path
+
 (*s The absolute names of objects seen by kernel *)
 
 type kernel_name
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 663c6b6958..f82921ba95 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -36,6 +36,7 @@ type modvariant =
 type module_info = 
     { msid : mod_self_id;
       modpath : module_path;
+      seed : dir_path; (* the "seed" of unique identifier generator *)
       label : label;
       variant : modvariant}
 
@@ -72,6 +73,7 @@ let rec empty_environment =
     modinfo = {
       msid = initial_msid;
       modpath = initial_path;
+      seed = initial_dir;
       label = mk_label "_";
       variant = NONE};
     labset = Labset.empty;
@@ -220,7 +222,7 @@ let add_module l me senv =
 
 (* Interactive modules *)
 
-let start_module dir l params result senv = 
+let start_module l params result senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -240,10 +242,11 @@ let start_module dir l params result senv =
   in
   let result_body = option_app (translate_modtype env) result in
   ignore (option_app check_sig result_body);
-  let msid = make_msid dir (string_of_label l) 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,result_body) }
   in
@@ -294,7 +297,11 @@ let end_module l senv =
       mod_equiv = None;
       mod_constraints = cst }
   in
-  let mspec = mtb, None, Constraint.empty in
+  let mspec = 
+    { msb_modtype = mtb;
+      msb_equiv = None;
+      msb_constraints = Constraint.empty } 
+  in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   let newenv = 
@@ -318,7 +325,7 @@ let end_module l senv =
 
 (* Interactive module types *)
 
-let start_modtype dir l params senv = 
+let start_modtype l params senv = 
   check_label l senv.labset; 
   let rec trans_params env = function 
     | [] -> env,[] 
@@ -331,10 +338,11 @@ let start_modtype dir l params senv =
 	env, (mbid,mtb)::transrest
   in
   let env,params_body = trans_params senv.env params in
-  let msid = make_msid dir (string_of_label l) 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 }
   in
@@ -421,6 +429,7 @@ let start_library dir senv =
   let mp = MPself msid in
   let modinfo = { msid = msid;
 		  modpath = mp;
+		  seed = dir;
 		  label = l;
 		  variant = LIBRARY dir }
   in
@@ -456,13 +465,6 @@ let export senv dir =
     modinfo.msid, (dir,mb,senv.imports)
 
 
-let import_constraints g kn cst =
-  try
-    merge_constraints cst g
-  with UniverseInconsistency ->
-    error "import_constraints: Universe Inconsistency during import"
-
-
 let check_imports senv needed =
   let imports = senv.imports in
   let check (id,stamp) =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2d4d2403ce..3efe0d16c2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -68,7 +68,7 @@ val add_constraints :
 
 (*s Interactive module functions *)
 val start_module : 
-  dir_path -> label -> (mod_bound_id * module_type_entry) list 
+  label -> (mod_bound_id * module_type_entry) list 
     -> module_type_entry option 
       -> safe_environment -> module_path * safe_environment
 
@@ -77,7 +77,7 @@ val end_module :
 
 
 val start_modtype :
-  dir_path -> label -> (mod_bound_id * module_type_entry) list
+  label -> (mod_bound_id * module_type_entry) list
     -> safe_environment -> module_path * safe_environment
 
 val end_modtype :
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bf53c69658..6b0931a9e3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -163,13 +163,12 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	  in
 	    check_conv cst conv env c1 c2
 	      
-let rec check_modules cst env msid1 l 
-  (mtb1,mpo1,cst1 as msb1) (mtb2,mpo2,cst2 as msb2) =
+let rec check_modules cst env msid1 l msb1 msb2 =
   let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = strengthen env mtb1 mp in
-  let cst = check_modtypes cst env mty1 mtb2 false in
+  let mty1 = strengthen env msb1.msb_modtype mp in
+  let cst = check_modtypes cst env mty1 msb2.msb_modtype false in
   begin
-    match mpo1, mpo2 with
+    match msb1.msb_equiv, msb2.msb_equiv with
       | _, None -> ()
       | None, Some mp2 -> 
 	  check_modpath_equiv env mp mp2