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, 89 insertions, 103 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 861dc9a3fd..41f4c640ce 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -33,7 +33,6 @@ type namedobject =
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
   | Modtype of module_type_body
-  | Alias of module_path * struct_expr_body option
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -61,10 +60,9 @@ let make_label_map mp list =
    match e with
     | SFBconst cb -> add_map (Constant cb)
     | SFBmind mib ->
-       add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
+       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
-    | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
   in
     List.fold_right add_one list Labmap.empty
 
@@ -75,15 +73,18 @@ let check_conv_error error cst f env a1 a2 =
       NotConvertible -> error ()
 
 (* for now we do not allow reorderings *)
-let check_inductive cst env msid1 l info1 mib2 spec2 =
-  let kn = make_kn (MPself msid1) empty_dirpath l in
+
+let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
+  let kn1 = make_mind mp1 empty_dirpath l in
+  let kn2 = make_mind mp2 empty_dirpath l in
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
   let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
+  let mib2 =  subst_mind subst2 mib2 in
   let check_inductive_type cst env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
@@ -141,8 +142,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
     array_fold_left2
       (fun cst t1 t2 -> check_conv cst conv env t1 t2)
       cst
-      (arities_of_specif kn (mib1,p1))
-      (arities_of_specif kn (mib2,p2))
+      (arities_of_specif kn1 (mib1,p1))
+      (arities_of_specif kn1 (mib2,p2))
   in
   let check f = if f mib1 <> f mib2 then error () in
   check (fun mib -> mib.mind_finite);
@@ -158,16 +159,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams);
 
-  begin
-    match mib2.mind_equiv with
-      | None -> ()
-      | Some kn2' ->
-	  let kn2 = scrape_mind env kn2' in
-	  let kn1 = match mib1.mind_equiv with
-	      None -> kn
-	    | Some kn1' -> scrape_mind env kn1'
-	  in
-	    if kn1 <> kn2 then error ()
+  begin  
+  match mind_of_delta reso2 kn2  with
+      | kn2' when kn2=kn2' -> ()
+      | kn2' -> 
+	  if not (eq_mind (mind_of_delta reso1 kn1) kn2') then 
+	    error ()
   end;
   (* we check that records and their field names are preserved. *)
   check (fun mib -> mib.mind_record);
@@ -194,7 +191,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   in
     cst
 
-let check_constant cst env msid1 l info1 cb2 spec2 =
+    
+let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
@@ -245,13 +243,15 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
   in
 
   match info1 with
-   | Constant cb1 ->
-      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-      (*Start by checking types*)
+    | Constant cb1 ->
+	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+	(*Start by checking types*)
+	let cb1 = subst_const_body subst1 cb1 in
+	let cb2 = subst_const_body subst2 cb2 in
       let typ1 = Typeops.type_of_constant_type env cb1.const_type in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = check_type cst env typ1 typ2 in
-      let con = make_con (MPself msid1) empty_dirpath l in
+      let con = make_con mp1 empty_dirpath l in
       let cst =
 	if cb2.const_opaque then
 	  match cb2.const_body with
@@ -264,7 +264,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 			begin
 			  match (kind_of_term c) with
 			      Const n ->
-				let cb = lookup_constant n env in
+				let cb = subst_const_body subst1
+				  (lookup_constant n env) in
 				  (match cb.const_opaque,
 				     cb.const_body with
 				       | true, Some lc1 ->
@@ -311,28 +312,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        check_conv cst conv env ty1 ty2
    | _ -> error ()
 
-let rec check_modules cst env msid1 l msb1 msb2 alias =
-  let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = module_type_of_module (Some mp) msb1 in
-  let alias1,struct_expr = match eval_struct env mty1.typ_expr with
-    	| SEBstruct (msid,sign) as str ->
-	    update_subst alias (map_msid msid mp),str
-	| _ as str -> empty_subst,str in
-  let mty1 = {mty1 with
-		typ_expr = struct_expr;
-		typ_alias = join alias1 mty1.typ_alias } in
-  let mty2 =  module_type_of_module None msb2 in
-  let cst = check_modtypes cst env mty1 mty2 false in
+let rec check_modules cst env msb1 msb2 subst1 subst2 =
+  let mty1 = module_type_of_module env None msb1 in
+  let mty2 =  module_type_of_module env None msb2 in
+  let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
     cst
 
-
-and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
-  let mp1 = MPself msid1 in
-  let env = add_signature mp1 sig1 env in
-  let sig1 = subst_structure alias sig1 in
-  let alias1 = update_subst alias (map_msid msid2 mp1) in
-  let sig2 = subst_structure alias1 sig2' in
-  let sig2 = subst_signature_msid msid2 mp1 sig2 in
+and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) =
     let info1 =
@@ -340,38 +326,19 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
 	Labmap.find l map1
       with
 	  Not_found -> error_no_such_label_sub l
-	    (string_of_msid msid1) (string_of_msid msid2)
+	    (string_of_mp mp1)
     in
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant cst env msid1 l info1 cb2 spec2
+	    check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive cst env msid1 l info1 mib2 spec2
+	    check_inductive cst env
+	      mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	| SFBmodule msb2 ->
 	    begin
 	      match info1 with
-		| Module msb -> check_modules cst env msid1 l msb msb2 alias
-		| Alias (mp,typ_opt) ->let msb =
-		    {mod_expr = Some (SEBident mp);
-		     mod_type = typ_opt;
-		     mod_constraints = Constraint.empty;
-		     mod_alias = (lookup_modtype mp env).typ_alias;
-		     mod_retroknowledge = []} in
-		    check_modules cst env msid1 l msb msb2 alias
-		| _ -> error_not_match l spec2
-	    end
-	| SFBalias (mp,typ_opt,_) ->
-	    begin
-	      match info1 with
-		| Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst
-		| Module msb ->
-		    let msb1 =
-		      {mod_expr = Some (SEBident mp);
-		       mod_type = typ_opt;
-		       mod_constraints = Constraint.empty;
-		       mod_alias = (lookup_modtype mp env).typ_alias;
-		       mod_retroknowledge = []} in
-			check_modules cst env msid1 l msb msb1 alias
+		| Module msb -> check_modules cst env msb msb2 
+		    subst1 subst2
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
@@ -380,50 +347,69 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
-	      check_modtypes cst env mtb1 mtb2 true
+	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
+	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
+	      check_modtypes cst env mtb1 mtb2 subst1 subst2 true
   in
     List.fold_left check_one_body cst sig2
 
-
-and check_modtypes cst env mtb1 mtb2 equiv =
-  if mtb1==mtb2 then cst else (* just in case  :) *)
-  let mtb1',mtb2'=
-    (match mtb1.typ_strength with
-	 None -> eval_struct env mtb1.typ_expr,
-	   eval_struct env mtb2.typ_expr
-       | Some mp -> strengthen  env mtb1.typ_expr mp,
-	   eval_struct env mtb2.typ_expr) in
-      let rec check_structure cst env str1 str2 equiv =
-	match str1, str2 with
-	  | SEBstruct (msid1,list1),
-	    SEBstruct (msid2,list2) ->
-	      let cst = check_signatures cst env
-		(msid1,list1) mtb1.typ_alias (msid2,list2) in
-		if equiv then
-		  check_signatures cst env
-		    (msid2,list2) mtb2.typ_alias  (msid1,list1)
-		else
-		  cst
+and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = 
+  if mtb1==mtb2 then cst else 
+  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
+  let rec check_structure cst env str1 str2 equiv subst1 subst2 = 
+	match str1,str2 with
+	  | SEBstruct (list1), 
+	    SEBstruct (list2) -> 
+	      if equiv then
+		let subst2 = 
+		  add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+		Univ.Constraint.union 
+		  (check_signatures cst env
+		     mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+		  mtb1.typ_delta mtb2.typ_delta) 
+		  (check_signatures cst env 
+		     mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
+		  mtb2.typ_delta  mtb1.typ_delta)
+	      else
+		check_signatures cst env
+		  mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+		  mtb1.typ_delta  mtb2.typ_delta
 	  | SEBfunctor (arg_id1,arg_t1,body_t1),
 	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	      let cst = check_modtypes cst env arg_t2 arg_t1 equiv in
+	      let subst1 = 
+		(join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
+	      let cst = check_modtypes cst env 
+		arg_t2 arg_t1 subst2 subst1
+		equiv in 
 		(* contravariant *)
-	      let env =
-		add_module (MPbound arg_id2) (module_body_of_type arg_t2) env
+	      let env = add_module 
+		(module_body_of_type (MPbound arg_id2) arg_t2) env 
 	      in
-	      let body_t1' =
-		(* since we are just checking well-typedness we do not need
-		   to expand any constant. Hence the identity resolver. *)
-		subst_struct_expr
-		  (map_mbid arg_id1 (MPbound arg_id2) None)
-		  body_t1
+	      let subst1 = 
+		(join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
+	      let env = match body_t1 with
+		  SEBstruct str -> 
+		    add_module {mod_mp = mtb1.typ_mp;
+				mod_expr = None;
+				mod_type = subst_struct_expr subst1 body_t1;
+				mod_type_alg= None;
+				mod_constraints=mtb1.typ_constraints;
+				mod_retroknowledge = [];
+				mod_delta = mtb1.typ_delta} env
+		| _ -> env
 	      in
-		check_structure cst env (eval_struct env body_t1')
-		  (eval_struct env body_t2) equiv
+		check_structure cst env body_t1 body_t2 equiv 
+		  subst1
+		  subst2
 	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
       in
      if mtb1'== mtb2' then cst
-     else check_structure cst env mtb1' mtb2' equiv
+     else check_structure cst env mtb1' mtb2' equiv subst1 subst2
 
 let check_subtypes env sup super =
-  check_modtypes Constraint.empty env sup super false
+  let env = add_module 
+		(module_body_of_type sup.typ_mp sup) env in
+  check_modtypes Constraint.empty env 
+    (strengthen env sup sup.typ_mp) super empty_subst 
+    (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
+