Module names and constant/inductive names are now in two separate nam…

…espaces

 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

CHANGES

@@ -19,6 +19,12 @@ Program
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
 
+Module System
+
+- The names of modules (and module types) are now in a fully separated
+  namespace from ordinary definitions : "Definition E:=0. Module E. End E."
+  is now accepted.
+
 CoqIDE
 
 - Coqide now supports the Restart command, and Undo (with a warning).

checker/mod_checking.ml

@@ -54,10 +54,14 @@ let path_of_mexpr = function
   | SEBident mp -> mp
   | _ -> raise Not_path
 
-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 check_definition_sub env cb1 cb2 =
   let check_type env t1 t2 =
@@ -132,106 +136,84 @@ let lookup_modtype mp env =
 
 let rec check_with env mtb with_decl mp=
   match with_decl with
-    | With_definition_body _ ->
-	check_with_aux_def env mtb with_decl mp;
+    | With_definition_body (idl,c) ->
+	check_with_def env mtb (idl,c) mp;
 	mtb
-    | With_module_body _ ->
-	check_with_aux_mod env mtb with_decl mp;
+    | With_module_body (idl,mp1) ->
+	check_with_mod env mtb (idl,mp1) mp;
 	mtb
 
-and check_with_aux_def env mtb with_decl mp =
+and check_with_def env mtb (idl,c) mp =
   let sig_b = match mtb with
     | SEBstruct(sig_b) ->
 	sig_b
     | _ -> error_signature_expected mtb
   in
-  let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
-                                           id,idl
-    | With_definition_body ([],_) | With_module_body ([],_) -> 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 empty_delta_resolver env in
-	match with_decl with
-          | With_definition_body ([],_) -> assert false
-	  | With_definition_body ([id],c) ->
+      if idl = [] then
 	      let cb = match spec with
 		  SFBconst cb -> cb
 		| _ -> error_not_a_constant l
 	      in
               check_definition_sub env' c cb
-	  | With_definition_body (_::_,_) ->
+      else
 	      let old = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
 		begin
 		  match old.mod_expr with
                     | None ->
-			let new_with_decl = match with_decl with
-			    With_definition_body (_,c) ->
-                              With_definition_body (idl,c)
-			  | With_module_body (_,c) ->
-                              With_module_body (idl,c) in
-			  check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
+		        check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
                     | Some msb ->
 			error_a_generative_module_expected l
 		end
-	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl mp =
+and check_with_mod env mtb (idl,mp1) mp =
   let sig_b =
     match mtb with
     | SEBstruct(sig_b) ->
 	sig_b
     | _ -> error_signature_expected mtb in
-  let id,idl = match with_decl with
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
-        id,idl
-    | With_definition_body ([],_) | With_module_body ([],_) -> 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,false) [] 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 empty_delta_resolver env in
-	match with_decl with
-          | With_module_body ([],_) -> assert false
-	  | With_module_body ([id], mp1) ->
+      if idl = [] then
 	      let _ = match spec with
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
 	      let (_:module_body) = (lookup_module mp1 env) in ()
-        | With_module_body (_::_,mp) ->
+      else
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
 	    in
 	      begin
 		match old.mod_expr with
                     None ->
-                      let new_with_decl = match with_decl with
-			  With_definition_body (_,c) ->
-			    With_definition_body (idl,c)
-			| With_module_body (_,c) ->
-                            With_module_body (idl,c) in
-		 	check_with_aux_mod env'
-			  old.mod_type new_with_decl (MPdot(mp,l))
+		      check_with_mod env'
+			  old.mod_type (idl,mp1) (MPdot(mp,l))
                   | Some msb ->
                       error_a_generative_module_expected l
               end
-	| _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l

checker/subtyping.ml

@@ -29,15 +29,18 @@ type namedobject =
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
   | Module of module_body
   | Modtype of module_type_body
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
 
-let add_nameobjects_of_mib ln mib map =
-  let add_nameobjects_of_one j oib map =
-    let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+  let ind = make_mind mp empty_dirpath l in
+  let add_mip_nameobjects j oib map =
+    let ip = (ind,j) in
     let map =
       array_fold_right_i
       (fun i id map ->
@@ -47,22 +50,32 @@ let add_nameobjects_of_mib ln mib map =
     in
       Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
   in
-    array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+    array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
 
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
 
-(* creates namedobject map for the whole signature *)
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
 
-let make_label_map mp list =
+let get_obj mp map l =
+  try Labmap.find l map.objs
+  with Not_found -> error_no_such_label_sub l mp
+
+let get_mod mp map l =
+  try Labmap.find l map.mods
+  with Not_found -> error_no_such_label_sub l mp
+
+let make_labmap mp list =
   let add_one (l,e) map =
-   let add_map obj = Labmap.add l obj map in
    match e with
-    | SFBconst cb -> add_map (Constant cb)
-    | SFBmind mib ->
-       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
-    | SFBmodule mb -> add_map (Module mb)
-    | SFBmodtype mtb -> add_map (Modtype mtb)
+    | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+    | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+    | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+    | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
   in
-    List.fold_right add_one list Labmap.empty
+  List.fold_right add_one list empty_labmap
 
 
 let check_conv_error error f env a1 a2 =
@@ -283,7 +296,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
-   | _ -> error ()
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
@@ -292,29 +304,25 @@ let rec check_modules  env msb1 msb2 subst1 subst2 =
 
 
 and check_signatures env mp1 sig1 sig2 subst1 subst2 = 
-  let map1 = make_label_map mp1 sig1 in
+  let map1 = make_labmap mp1 sig1 in
   let check_one_body  (l,spec2) =
-    let info1 =
-      try
-	Labmap.find l map1
-      with
-	  Not_found -> error_no_such_label_sub l mp1
-    in
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant  env mp1 l info1 cb2 spec2 subst1 subst2
+	    check_constant  env mp1 l (get_obj mp1 map1 l)
+	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+	    check_inductive env mp1 l (get_obj mp1 map1 l)
+	      mib2 spec2 subst1 subst2
 	| SFBmodule msb2 ->
 	    begin
-	      match info1 with
+	      match get_mod mp1 map1 l with
 		| Module msb -> check_modules env msb msb2 
 		    subst1 subst2
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
-	      match info1 with
+	      match get_mod mp1 map1 l with
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in

kernel/declarations.mli

@@ -192,6 +192,10 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
+(** NB: we may encounter now (at most) twice the same label in
+    a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+    and once for an object ([SFBconst] or [SFBmind]) *)
+
 and structure_body = (label * structure_field_body) list
 
 and struct_expr_body =