After the approval of Bruno, here the patch for the checker.

In checker:
- delta_resolver inferred by the module system is checked through regular delta reduction steps
- the old mind_equiv field of mutual_inductive is simulated through a special table in environ
- small optimization, if the signature and the implementation of a module are physically equal
(always happen for the toplevel module of a vo) then the checker checks only the signature.
In kernel
- in names i have added two special equality functions over constant and inductive names for the checker,
so that the checker does not take in account the cannonical name inferred by the module system. 



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

11 files changed, 101 insertions, 44 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 054057d1f..27848efa7 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -376,7 +376,12 @@ let defined_rels flags env =
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
-let mind_equiv_infos info = eq_ind
+let mind_equiv_infos info = mind_equiv info.i_env
+
+let eq_table_key k1 k2 = 
+ match k1,k2 with
+   | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2
+   | _,_  -> k1=k2
 
 let create mk_cl flgs env =
   { i_flags = flgs;
diff --git a/checker/closure.mli b/checker/closure.mli
index ada7ded1e..bc0704d91 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -175,6 +175,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
 (* [mind_equiv] checks whether two inductive types are intentionally equal *)
 val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
+val eq_table_key : table_key -> table_key -> bool
 (************************************************************************)
 (*i This is for lazy debug *)
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2a5d3114c..699f6c90e 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -492,21 +492,30 @@ let val_substituted val_a =
       [|[|val_a|];[|val_list val_subst;val_a|]|])
 
 let from_val a = ref (LSval a)
-
+ 
+let rec replace_mp_in_mp mpfrom mpto mp =
+  match mp with
+    | _ when mp = mpfrom -> mpto
+    | MPdot (mp1,l) ->
+	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+	  if mp1==mp1' then mp
+	  else MPdot (mp1',l)
+    | _ -> mp
+
+let rec mp_in_mp mp mp1 =
+  match mp1 with
+    | _ when mp1 = mp -> true
+    | MPdot (mp2,l) -> mp_in_mp mp mp2
+    | _ -> false
+	
 let mp_in_key mp key = 
-  let rec mp_rec mp1 = 
-    match mp1 with
-      | _ when mp1 = mp -> true
-      | MPdot (mp2,l) -> mp_rec mp2
-      | _ -> false
-  in 
-    match key with
+  match key with
     | MP mp1 -> 
-	mp_rec mp1
+	mp_in_mp mp mp1
     | KN kn -> 
 	let mp1,dir,l = repr_kn kn in
-	  mp_rec mp1
-   
+	  mp_in_mp mp mp1
+  
 let subset_prefixed_by mp resolver =
   let prefixmp key hint resolv =
     if mp_in_key mp key then
@@ -583,10 +592,23 @@ let add_delta_resolver resolver1 resolver2 =
     Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
       resolver2
 
+let substition_prefixed_by k mp subst =
+  let prefixmp key (mp_to,reso) sub =
+    match key with 
+      | MPI mpk ->
+	  if mp_in_mp mp mpk && mp <> mpk then
+	    let new_key = replace_mp_in_mp mp k mpk in
+	      Umap.add (MPI new_key) (mp_to,reso) sub
+	  else 
+	    sub
+      |  _ -> sub
+  in
+    Umap.fold prefixmp subst empty_subst
+
 let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,resolve) =
+  let apply_subst key (mp,resolve) res =
     let mp',resolve' =
-      match subst_mp0 sub mp with
+      match subst_mp0 subst2 mp with
 	  None -> mp, None
 	| Some (mp',resolve') ->  mp'
 	    ,Some resolve' in
@@ -594,15 +616,16 @@ let join (subst1 : substitution) (subst2 : substitution) =
       match resolve' with
           Some res -> 
 	    add_delta_resolver 
-	      (subst_dom_codom_delta_resolver sub resolve)
-	      res
+	      (subst_dom_codom_delta_resolver subst2 resolve) res
 	| None -> 
-	    subst_codom_delta_resolver sub resolve
+	    subst_codom_delta_resolver subst2 resolve
     in
-      mp',resolve'' in
-  let subst = Umap.mapi (apply_subst subst2) subst1 in
-    (Umap.fold Umap.add subst2 subst)   
-
+    let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
+    let prefixed_subst = substition_prefixed_by k mp subst2 in
+      Umap.fold Umap.add prefixed_subst 
+	(Umap.add key (mp',resolve'') res) in
+  let subst = Umap.fold apply_subst subst1 empty_subst in
+    (Umap.fold Umap.add subst2 subst) 
 
 let force fsubst r =
   match !r with
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 8afe09dac..b39fd6f2f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -199,6 +199,7 @@ val add_mp   : module_path -> module_path -> substitution -> substitution
 val map_mbid : mod_bound_id -> module_path -> substitution
 val map_mp   : module_path -> module_path -> substitution
 val mp_in_delta : module_path -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun
diff --git a/checker/environ.ml b/checker/environ.ml
index 3d14b995b..a72aae91d 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,6 +7,7 @@ open Declarations
 type globals = {
   env_constants : constant_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
+  env_inductives_eq : kernel_name  KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body MPmap.t}
 
@@ -26,6 +27,7 @@ let empty_env = {
   env_globals =
   { env_constants = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
+    env_inductives_eq = KNmap.empty;
     env_modules = MPmap.empty;
     env_modtypes = MPmap.empty};
   env_named_context = [];
@@ -142,14 +144,31 @@ let evaluable_constant cst env =
   with Not_found | NotEvaluableConst _ -> false
 
 (* Mutual Inductives *)
+let scrape_mind env kn=
+  try
+    KNmap.find kn env.env_globals.env_inductives_eq
+  with 
+      Not_found -> kn
+
+let mind_equiv env (kn1,i1) (kn2,i2) =
+  i1 = i2 && 
+  scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2)
+
+
 let lookup_mind kn env =
   Mindmap_env.find kn env.env_globals.env_inductives
 
 let add_mind kn mib env =
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+  let kn1,kn2 =  user_mind kn,canonical_mind kn in
+  let new_inds_eq = if kn1=kn2 then 
+    env.env_globals.env_inductives_eq
+  else
+    KNmap.add kn1 kn2  env.env_globals.env_inductives_eq in
   let new_globals =
     { env.env_globals with
-	env_inductives = new_inds } in
+	env_inductives = new_inds;
+	env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 776698ed8..023acd0bf 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -6,6 +6,7 @@ open Term
 type globals = {
   env_constants : Declarations.constant_body Cmap_env.t;
   env_inductives : Declarations.mutual_inductive_body Mindmap_env.t;
+  env_inductives_eq : kernel_name KNmap.t;
   env_modules : Declarations.module_body MPmap.t;
   env_modtypes : Declarations.module_type_body MPmap.t}
 type stratification = {
@@ -57,6 +58,8 @@ val constant_opt_value : env -> constant -> constr option
 val evaluable_constant : constant -> env -> bool
 
 (* Inductives *)
+val mind_equiv : env -> inductive -> inductive -> bool
+
 val lookup_mind :
   mutual_inductive -> env -> Declarations.mutual_inductive_body
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index e95109fc5..23ba4893a 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -245,27 +245,30 @@ 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, mtb when mtb==mexpr ->
+	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
+	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
+	let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta 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_delta = mb.mod_delta;}
 	    {typ_mp=mp;
 	     typ_expr=mb.mod_type;
 	     typ_expr_alg=None;
 	     typ_constraints=Univ.Constraint.empty;
-	     typ_delta = empty_delta_resolver;};
+	     typ_delta = mb.mod_delta;};
 	  
-and check_structure_field env mp lab = function
+and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
 	check_constant_declaration env c cb
   | SFBmind mib ->
       let kn = make_mind mp empty_dirpath lab in
+      let kn = mind_of_delta res kn in
 	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
       let _= check_module env (MPdot(mp,lab)) msb in
@@ -274,17 +277,17 @@ and check_structure_field env mp lab = function
       check_module_type env mty;
       add_modtype (MPdot(mp,lab)) mty env
 	
-and check_modexpr env mse mp_mse = match mse with
+and check_modexpr env mse mp_mse res = 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
+      let sign = check_modexpr env' body mp_mse res in
 	SEBfunctor (arg_id, mtb, sign)
   | SEBapply (f,m,cst) ->
-      let sign = check_modexpr env f mp_mse in
+      let sign = check_modexpr env f mp_mse res in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mp =
 	try (path_of_mexpr m)
@@ -294,25 +297,25 @@ and check_modexpr env mse mp_mse = match mse with
 	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_modexpr env mte mp_mse res 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
+		   check_structure_field env mp_mse lab res mb) env msb in
 	SEBstruct(msb)
 	
-and check_modtype env mse mp_mse= match mse with
+and check_modtype env mse mp_mse res = match mse with
   | SEBident mp ->
       let mtb = lookup_modtype mp env in
 	mtb.typ_expr
   | 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 body = check_modtype env' body mp_mse in
+      let body = check_modtype env' body mp_mse res in
 	SEBfunctor(arg_id,mtb,body)
   | SEBapply (f,m,cst) ->
-      let sign = check_modtype env f mp_mse in
+      let sign = check_modtype env f mp_mse res in
       let farg_id, farg_b, fbody_b = destr_functor env sign in
       let mp =
 	try (path_of_mexpr m)
@@ -322,12 +325,12 @@ and check_modtype env mse mp_mse= match mse with
 	check_subtypes env mtb farg_b;
 	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
-      let sign = check_modtype env mte mp_mse in
+      let sign = check_modtype env mte mp_mse res 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
+		   check_structure_field env mp_mse lab res mb) env msb in
       SEBstruct(msb)
 	
 (*
diff --git a/checker/modops.ml b/checker/modops.ml
index e6428d5ab..f5d54c361 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -85,7 +85,7 @@ let rec add_signature mp sign resolver env =
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
     let con = constant_of_kn kn in
-    let mind = mind_of_kn kn in
+    let mind = mind_of_delta resolver (mind_of_kn kn) in
       match elem with
 	| SFBconst cb -> 
 	   (* let con =  constant_of_delta resolver con in*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 776edb243..e00ece11a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -254,7 +254,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
 	(try (* try first intensional equality *)
-	  if fl1 = fl2
+	  if  eq_table_key fl1 fl2
           then convert_stacks univ infos lft1 lft2 v1 v2
           else raise NotConvertible
         with NotConvertible ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 9df49630c..d66a49546 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -361,8 +361,10 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   (*if sup<>super then*)
-  check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst 
-    (map_mp super.typ_mp sup.typ_mp) false 
+  let env = add_module 
+    (module_body_of_type sup.typ_mp sup) env in
+    check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst 
+      (map_mp super.typ_mp sup.typ_mp) false 
 
 let check_equal env sup super =
   (*if sup<>super then*)
diff --git a/checker/term.ml b/checker/term.ml
index 8d65bbe17..c39491ab5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -487,9 +487,9 @@ let compare_constr f t1 t2 =
           f h1 h2 & List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
-  | Const c1, Const c2 -> eq_constant c1 c2
-  | Ind c1, Ind c2 -> c1 = c2
-  | Construct c1, Construct c2 -> c1 = c2
+  | Const c1, Const c2 -> eq_con_chk c1 c2
+  | Ind c1, Ind c2 -> eq_ind_chk c1 c2
+  | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
       f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
   | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->