Module names and constant/inductive names are now in two separate namespaces

 We now accept the following code: Definition E := 0. Module E. End E.

 Techically, we simply allow the same label to occur at most twice in
 a structure_body, which is a (label * structure_field_body) list).
 These two label occurences should not be at the same level of fields
 (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
 a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
 Drawback : no more simple List.assoc or equivalent should be performed
 on a structure_body ...

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

1 files changed, 36 insertions, 20 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e87bc9c1c1..94be2602e0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -102,7 +102,8 @@ type safe_environment =
     { old : safe_environment;
       env : env;
       modinfo : module_info;
-      labset : Labset.t;
+      modlabels : Labset.t;
+      objlabels : Labset.t;
       revstruct : structure_body;
       univ : Univ.constraints;
       engagement : engagement option;
@@ -110,13 +111,16 @@ type safe_environment =
       loads : (module_path * module_body) list;
       local_retroknowledge : Retroknowledge.action list}
 
-let exists_label l senv = Labset.mem l senv.labset
+let exists_modlabel l senv = Labset.mem l senv.modlabels
+let exists_objlabel l senv = Labset.mem l senv.objlabels
 
-let check_label l senv =
-  if exists_label l senv then error_existing_label l
+let check_modlabel l senv =
+  if exists_modlabel l senv then error_existing_label l
+let check_objlabel l senv =
+  if exists_objlabel l senv then error_existing_label l
 
-let check_labels ls senv =
-  Labset.iter (fun l -> check_label l senv) ls
+let check_objlabels ls senv =
+  Labset.iter (fun l -> check_objlabel l senv) ls
 
 let labels_of_mib mib =
   let add,get =
@@ -141,7 +145,8 @@ let rec empty_environment =
       variant = NONE;
       resolver = empty_delta_resolver;
       resolver_of_param = empty_delta_resolver};
-    labset = Labset.empty;
+    modlabels = Labset.empty;
+    objlabels = Labset.empty;
     revstruct = [];
     univ = Univ.empty_constraint;
     engagement = None;
@@ -173,11 +178,15 @@ type generic_name =
   | M
 
 let add_field ((l,sfb) as field) gn senv =
-  let labels = match sfb with
-    | SFBmind mib -> labels_of_mib mib
-    | _ -> Labset.singleton l
+  let mlabs,olabs = match sfb with
+    | SFBmind mib ->
+      let l = labels_of_mib mib in
+      check_objlabels l senv; (Labset.empty,l)
+    | SFBconst _ ->
+      check_objlabel l senv; (Labset.empty, Labset.singleton l)
+    | SFBmodule _ | SFBmodtype _ ->
+      check_modlabel l senv; (Labset.singleton l, Labset.empty)
   in
-  check_labels labels senv;
   let senv = add_constraints (constraints_of_sfb sfb) senv in
   let env' = match sfb, gn with
     | SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -188,7 +197,8 @@ let add_field ((l,sfb) as field) gn senv =
   in
   { senv with
     env = env';
-    labset = Labset.union labels senv.labset;
+    modlabels = Labset.union mlabs senv.modlabels;
+    objlabels = Labset.union olabs senv.objlabels;
     revstruct = field :: senv.revstruct }
 
 (* Applying a certain function to the resolver of a safe environment *)
@@ -321,7 +331,7 @@ let add_module l me inl senv =
 (* Interactive modules *)
 
 let start_module l senv =
-  check_label l senv;
+  check_modlabel l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;
@@ -332,7 +342,8 @@ let start_module l senv =
    mp, { old = senv;
 	 env = senv.env;
 	 modinfo = modinfo;
-	 labset = Labset.empty;
+	 modlabels = Labset.empty;
+	 objlabels = Labset.empty;
 	 revstruct = [];
          univ = Univ.empty_constraint;
          engagement = None;
@@ -416,7 +427,8 @@ let end_module l restype senv =
     mp,resolver,{ old = oldsenv.old;
 		  env = newenv;
 		  modinfo = modinfo;
-		  labset = Labset.add l oldsenv.labset;
+		  modlabels = Labset.add l oldsenv.modlabels;
+		  objlabels = oldsenv.objlabels;
 		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
 		  univ = Univ.union_constraints senv'.univ oldsenv.univ;
 		  (* engagement is propagated to the upper level *)
@@ -511,7 +523,8 @@ let add_module_parameter mbid mte inl senv =
 				   variant = new_variant;
 				   resolver_of_param = add_delta_resolver
 			      resolver_of_param senv.modinfo.resolver_of_param};
-		     labset = senv.labset;
+		     modlabels = senv.modlabels;
+		     objlabels = senv.objlabels;
 		     revstruct = [];
 		     univ = senv.univ;
 		     engagement = senv.engagement;
@@ -523,7 +536,7 @@ let add_module_parameter mbid mte inl senv =
 (* Interactive module types *)
 
 let start_modtype l senv =
-  check_label l senv;
+  check_modlabel l senv;
  let mp = MPdot(senv.modinfo.modpath, l) in
  let modinfo = { modpath = mp;
 		 label = l;
@@ -534,7 +547,8 @@ let start_modtype l senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	labset = Labset.empty;
+	modlabels = Labset.empty;
+	objlabels = Labset.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;
@@ -585,7 +599,8 @@ let end_modtype l senv =
     mp, { old = oldsenv.old;
 	  env = newenv;
 	  modinfo = oldsenv.modinfo;
-	  labset = Labset.add l oldsenv.labset;
+	  modlabels = Labset.add l oldsenv.modlabels;
+	  objlabels = oldsenv.objlabels;
 	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
           univ = Univ.union_constraints senv.univ oldsenv.univ;
           engagement = senv.engagement;
@@ -644,7 +659,8 @@ let start_library dir senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	labset = Labset.empty;
+	modlabels = Labset.empty;
+	objlabels = Labset.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;