This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



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

1 files changed, 116 insertions, 138 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 99babe632..e95109fc5 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -65,10 +65,6 @@ let rec list_fold_map2 f e = function
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
-
-let check_alias (s1:substitution) s2 =
-  if s1 <> s2 then failwith "Incorrect alias"
-
 let check_definition_sub env cb1 cb2 =
   let check_type env t1 t2 =
 
@@ -135,31 +131,31 @@ let lookup_modtype mp env =
   with Not_found ->
     failwith ("Unknown module type: "^string_of_mp mp)
 
-
-let rec check_with env mtb with_decl =
+let rec check_with env mtb with_decl mp=
   match with_decl with
     | With_definition_body _ ->
-	check_with_aux_def env mtb with_decl;
-	empty_subst
+	check_with_aux_def env mtb with_decl mp;
+	mtb
     | With_module_body _ ->
-	check_with_aux_mod env mtb with_decl
+	check_with_aux_mod env mtb with_decl mp;
+	mtb
 
-and check_with_aux_def env mtb with_decl =
-  let msid,sig_b = match (eval_struct env mtb) with
-    | SEBstruct(msid,sig_b) ->
-	msid,sig_b
+and check_with_aux_def env mtb with_decl 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,_,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
                                            id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
-      let env' = Modops.add_signature (MPself msid) before env 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) ->
@@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl =
 			let new_with_decl = match with_decl with
 			    With_definition_body (_,c) ->
                               With_definition_body (idl,c)
-			  | With_module_body (_,c,t,cst) ->
-                              With_module_body (idl,c,t,cst) in
-			  check_with_aux_def env' (type_of_mb env old) new_with_decl
+			  | With_module_body (_,c) ->
+                              With_module_body (idl,c) in
+			  check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
                     | Some msb ->
 			error_a_generative_module_expected l
 		end
@@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and check_with_aux_mod env mtb with_decl =
-  let initmsid,msid,sig_b =
-    match eval_struct env mtb with
-    | SEBstruct(msid,sig_b) ->
-        let msid'=(refresh_msid msid) in
-	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+and check_with_aux_mod env mtb with_decl 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,_,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_) ->
         id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_) -> assert false
   in
   let l = label_of_id id in
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
       let rec mp_rec = function
-	| [] -> MPself initmsid
+	| [] -> mp
 	| i::r -> MPdot(mp_rec r,label_of_id i)
       in
-      let env' = Modops.add_signature (MPself msid) before env 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], mp,_,_) ->
-	      let old,alias = match spec with
-		  SFBmodule msb -> Some msb,None
-		| SFBalias (mp',_,_) -> None,Some mp'
+          | With_module_body ([],_) -> assert false
+	  | With_module_body ([id], mp1) ->
+	      let _ = match spec with
+		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
-	      let mtb' = lookup_modtype mp env' in
-	      let _ =
-		match old,alias with
-		    Some msb,None -> ()
-		  | None,Some mp' ->
-		      check_modpath_equiv env' mp mp'
-		  | _,_ ->
-		      anomaly "Mod_typing:no implementation and no alias"
-	      in
-		join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
-        | With_module_body (_::_,mp,_,_) ->
+	      let _ = (lookup_module mp1 env) in ()
+        | With_module_body (_::_,mp) ->
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -240,12 +225,10 @@ and check_with_aux_mod env mtb with_decl =
                       let new_with_decl = match with_decl with
 			  With_definition_body (_,c) ->
 			    With_definition_body (idl,c)
-			| With_module_body (_,c,t,cst) ->
-                            With_module_body (idl,c,t,cst) in
-		      let sub =
-			check_with_aux_mod env'
-			  (type_of_mb env old) new_with_decl in
-		      join (map_mp (mp_rec idl) mp) sub
+			| With_module_body (_,c) ->
+                            With_module_body (idl,c) in
+		 	check_with_aux_mod env'
+			  old.mod_type new_with_decl (MPdot(mp,l))
                   | Some msb ->
                       error_a_generative_module_expected l
               end
@@ -255,110 +238,105 @@ and check_with_aux_mod env mtb with_decl =
       | Reduction.NotConvertible -> error_with_incorrect l
 
 and check_module_type env mty =
-  if mty.typ_strength <> None then
-    failwith "strengthening of module types not supported";
-  let sub = check_modexpr env mty.typ_expr in
-  check_alias mty.typ_alias sub
-
-and check_module env mb =
-  let sub =
-    match mb.mod_expr, mb.mod_type with
-      | None, None ->
-	  anomaly "Mod_typing.translate_module: empty type and expr in module entry"
-      | None, Some mtb -> check_modexpr env mtb
-
-      | Some mexpr, _ ->
-	  let sub1 = check_modexpr env mexpr in
-	  (match mb.mod_type with
-	    | None ->  sub1
-	    | Some mte ->
-		let sub2 = check_modexpr env mte in
-                check_subtypes env
-		  {typ_expr = mexpr;
-		   typ_strength = None;
-		   typ_alias = sub1;}
-		  {typ_expr = mte;
-		   typ_strength = None;
-		   typ_alias = sub2;};
-		sub2) in
-  check_alias mb.mod_alias sub
-
-and check_structure_field (s,env) mp lab = function
+  let _ = check_modtype env mty.typ_expr mty.typ_mp in ()
+
+							 
+and check_module env mp mb =
+  match mb.mod_expr, mb.mod_type with
+    | None,mtb -> 
+	let _ = check_modtype env mtb mb.mod_mp in ()
+    | Some mexpr, _ ->
+	let sign = check_modexpr env mexpr mb.mod_mp in
+	let _ = check_modtype env mb.mod_type mb.mod_mp in
+          check_subtypes env 
+	    {typ_mp=mp;
+	     typ_expr=sign;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = empty_delta_resolver;}
+	    {typ_mp=mp;
+	     typ_expr=mb.mod_type;
+	     typ_expr_alg=None;
+	     typ_constraints=Univ.Constraint.empty;
+	     typ_delta = empty_delta_resolver;};
+	  
+and check_structure_field env mp lab = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
-      (s,check_constant_declaration env c cb)
+	check_constant_declaration env c cb
   | SFBmind mib ->
-      let kn = make_kn mp empty_dirpath lab in
-      (s,Indtypes.check_inductive env kn mib)
+      let kn = make_mind mp empty_dirpath lab in
+	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      check_module env msb;
-      let mp1 = MPdot(mp,lab) in
-      let is_fun, sub = Modops.update_subst env msb mp1 in
-      ((if is_fun then s else join s sub),
-       Modops.add_module (MPdot(mp,lab)) msb env)
-  | SFBalias(mp2,_,cst) ->
-      (* cf Safe_typing.add_alias *)
-      (try
-        let mp' = MPdot(mp,lab) in
-        let mp2' = scrape_alias mp2 env in
-        let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
-        let sub = update_subst sub (map_mp mp' mp2') in
-        let sub = join_alias sub (map_mp mp' mp2') in
-        let sub = add_mp mp' mp2' sub in
-        (join s sub, register_alias mp' mp2 env)
-      with Not_found -> failwith "unkown aliased module")
+      let _= check_module env (MPdot(mp,lab)) msb in
+	Modops.add_module msb env
   | SFBmodtype mty ->
-      let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      (join s mty.typ_alias, add_modtype kn mty env)
-
-and check_modexpr env mse = match mse with
+      add_modtype (MPdot(mp,lab)) mty env
+	
+and check_modexpr env mse mp_mse = match mse with
+  | SEBident mp ->
+      let mb = lookup_module mp env in
+      	(subst_and_strengthen mb mp_mse env).mod_type
+  | SEBfunctor (arg_id, mtb, body) ->
+      check_module_type env mtb ;
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let sign = check_modexpr env' body mp_mse in
+	SEBfunctor (arg_id, mtb, sign)
+  | SEBapply (f,m,cst) ->
+      let sign = check_modexpr env f mp_mse in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
+      let mp =
+	try (path_of_mexpr m)
+	with Not_path -> error_application_to_not_path m
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
+  | SEBwith(mte, with_decl) ->
+      let sign = check_modexpr env mte mp_mse in
+      let sign = check_with env sign with_decl mp_mse in 
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab mb) env msb in
+	SEBstruct(msb)
+	
+and check_modtype env mse mp_mse= match mse with
   | SEBident mp ->
-      let mp = scrape_alias mp env in
       let mtb = lookup_modtype mp env in
-      mtb.typ_alias
+	mtb.typ_expr
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
-      let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
-      let sub = check_modexpr env' body in
-      sub
+      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+      let body = check_modtype env' body mp_mse in
+	SEBfunctor(arg_id,mtb,body)
   | SEBapply (f,m,cst) ->
-      let sub1 = check_modexpr env f in
-      let f'= eval_struct env f in
-      let farg_id, farg_b, fbody_b = destr_functor env f' in
+      let sign = check_modtype env f mp_mse in
+      let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mp =
-	try scrape_alias (path_of_mexpr m) env
+	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
-	      (* place for nondep_supertype *) in
-      let mtb = lookup_modtype mp env in
-      check_subtypes env mtb farg_b;
-      let sub2 = match eval_struct env m with
-	| SEBstruct (msid,sign) ->
-	    join_alias
-	      (subst_key (map_msid msid mp) mtb.typ_alias)
-	      (map_msid msid mp)
-	| _ -> mtb.typ_alias in
-      let sub3 = join_alias sub1 (map_mbid farg_id mp) in
-      let sub4 = update_subst sub2 sub3 in
-      join sub3 sub4
+	  (* place for nondep_supertype *) in
+      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+	check_subtypes env mtb farg_b;
+	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
-	let sub1 = check_modexpr env mte in
-	let sub2 = check_with env mte with_decl in
-	join sub1 sub2
-  | SEBstruct(msid,msb) ->
-      let mp = MPself msid in
-      let (sub,_) =
-        List.fold_left (fun env (lab,mb) ->
-          check_structure_field env mp lab mb) (empty_subst,env) msb in
-      sub
-
+      let sign = check_modtype env mte mp_mse in
+      let sign = check_with env sign with_decl mp_mse in
+	sign
+  | SEBstruct(msb) ->
+      let _ = List.fold_left (fun env (lab,mb) ->
+		   check_structure_field env mp_mse lab mb) env msb in
+      SEBstruct(msb)
+	
 (*
-let rec add_struct_expr_constraints env = function
+  let rec add_struct_expr_constraints env = function
   | SEBident _ -> env
-
+  
   | SEBfunctor (_,mtb,meb) ->
-      add_struct_expr_constraints
-	(add_modtype_constraints env mtb) meb
+  add_struct_expr_constraints
+  (add_modtype_constraints env mtb) meb
 
   | SEBstruct (_,structure_body) ->
       List.fold_left