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, 39 insertions, 43 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e2304f1194..4cb6fc2fd3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -36,10 +36,14 @@ let rec mp_from_mexpr = function
   | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
   | MSEwith (expr,_) -> mp_from_mexpr expr
 
-let rec list_split_assoc k rev_before = function
+let is_modular = function
+  | SFBmodule _ | SFBmodtype _ -> true
+  | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
   | [] -> raise Not_found
-  | (k',b)::after when k=k' -> rev_before,b,after
-  | h::tail -> list_split_assoc k (h::rev_before) tail
+  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+  | h::tail -> list_split_assoc km (h::rev_before) tail
 
 let discr_resolver env mtb =
      match mtb.typ_expr with
@@ -55,35 +59,34 @@ let rec rebuild_mp mp l =
 	
 let rec check_with env sign with_decl alg_sign mp equiv = 
   let sign,wd,equiv,cst= match with_decl with
-    | With_Definition (id,_) ->
-	let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
-	  sign,With_definition_body(id,cb),equiv,cst
-    | With_Module (id,mp1) -> 
-	let sign,equiv,cst = 
-	  check_with_aux_mod env sign with_decl mp equiv in
-	  sign,With_module_body(id,mp1),equiv,cst in
+    | With_Definition (idl,c) ->
+	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
+	sign,With_definition_body(idl,cb),equiv,cst
+    | With_Module (idl,mp1) ->
+	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
+	sign,With_module_body(idl,mp1),equiv,cst
+  in
     if alg_sign = None then
       sign,None,equiv,cst
     else
       sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
 	    
-and check_with_aux_def env sign with_decl mp equiv = 
+and check_with_def env sign (idl,c) mp equiv =
   let sig_b = match sign with 
     | SEBstruct(sig_b) -> sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match with_decl with
-    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
-    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature mp before equiv env in
-	match with_decl with
-          | With_Definition ([],_) -> assert false
-	  | With_Definition ([id],c) ->
+      if idl = [] then
+	      (* Toplevel definition *)
 	      let cb = match spec with
 		| SFBconst cb -> cb
 		| _ -> error_not_a_constant l
@@ -116,8 +119,9 @@ and check_with_aux_def env sign with_decl mp equiv =
 		    Cemitcodes.from_val (compile_constant_body env' def);
 		  const_constraints = cst }
 	      in
-	      SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
-	  | With_Definition (_::_,c) ->
+	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
+      else
+	      (* Definition inside a sub-module *)
 	      let old = match spec with
 		| SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -125,43 +129,36 @@ and check_with_aux_def env sign with_decl mp equiv =
 		begin
 		  match old.mod_expr with
                     | None ->
-			let new_with_decl = With_Definition (idl,c) in 
 			let sign,cb,cst = 
-			  check_with_aux_def env' old.mod_type new_with_decl 
+			  check_with_def env' old.mod_type (idl,c)
 			    (MPdot(mp,l)) old.mod_delta in
 			let new_spec = SFBmodule({old with
 						    mod_type = sign;
 						    mod_type_alg = None}) in
-			  SEBstruct(before@((l,new_spec)::after)),cb,cst
+			  SEBstruct(before@(l,new_spec)::after),cb,cst
                     | Some msb ->
 			error_generative_module_expected l
 		end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
       | Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
-and check_with_aux_mod env sign with_decl mp equiv = 
+and check_with_mod env sign (idl,mp1) mp equiv = 
   let sig_b = match sign with 
     | SEBstruct(sig_b) ->sig_b
     | _ -> error_signature_expected sign
   in
-  let id,idl = match with_decl with
-    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
-    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  let id,idl = match idl with
+    | [] -> assert false
+    | id::idl -> id,idl
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
       let before = List.rev rev_before in
-      let rec mp_rec = function
-	| [] -> mp
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-      in
       let env' = Modops.add_signature mp before equiv env in
-	match with_decl with
-          | With_Module ([],_) -> assert false
-	  | With_Module ([id], mp1) ->
+      if idl = [] then
+	      (* Toplevel module definition *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -195,7 +192,8 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
 		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
 	      add_delta_resolver equiv new_mb.mod_delta,cst
-          | With_Module (idc,mp1) -> 
+      else
+	      (* Module definition of a sub-module *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module (string_of_label l)
@@ -203,10 +201,9 @@ and check_with_aux_mod env sign with_decl mp equiv =
 	      begin
 		match old.mod_expr with
 		    None ->
-		      let new_with_decl = With_Module (idl,mp1) in
 		      let sign,equiv',cst =
-			check_with_aux_mod env'
-			  old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in
+			check_with_mod env'
+			  old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
 		      let new_equiv = add_delta_resolver equiv equiv' in
 		      let new_spec = SFBmodule {old with 
 						  mod_type = sign;
@@ -224,7 +221,6 @@ and check_with_aux_mod env sign with_decl mp equiv =
 		  | _ ->
 		      error_generative_module_expected l
               end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_incorrect_with_constraint l
@@ -369,7 +365,7 @@ let rec add_struct_expr_constraints env = function
 
   | SEBstruct (structure_body) ->
       List.fold_left
-        (fun env (l,item) -> add_struct_elem_constraints env item)
+        (fun env (_,item) -> add_struct_elem_constraints env item)
         env
         structure_body
 
@@ -414,7 +410,7 @@ let rec struct_expr_constraints cst = function
 
   | SEBstruct (structure_body) ->
       List.fold_left
-        (fun cst (l,item) -> struct_elem_constraints cst item)
+        (fun cst (_,item) -> struct_elem_constraints cst item)
         cst
         structure_body