correspondance des records et noms de champs de records entre un module et sa signature

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

6 files changed, 26 insertions, 4 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 481171652..0aa5c9948 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -104,6 +104,7 @@ type one_inductive_body = {
  }
 
 type mutual_inductive_body = {
+  mind_record : bool;
   mind_finite : bool;
   mind_ntypes : int;
   mind_hyps : section_context;
@@ -139,7 +140,8 @@ let subst_mind_packet sub mbp =
 }
 
 let subst_mind sub mib = 
-  { mind_finite = mib.mind_finite ;
+  { mind_record = mib.mind_record ; 
+    mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (assert (mib.mind_hyps=[]); []) ;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 452cbc972..7c6d3ecdf 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -77,6 +77,7 @@ type one_inductive_body = {
  }
 
 type mutual_inductive_body = {
+  mind_record : bool;
   mind_finite : bool;
   mind_ntypes : int;
   mind_hyps : section_context;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index edba6e608..e383dbabd 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -49,6 +49,7 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
+  mind_entry_record : bool;
   mind_entry_finite : bool;
   mind_entry_inds : one_inductive_entry list }
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index edba6e608..e383dbabd 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -49,6 +49,7 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
+  mind_entry_record : bool;
   mind_entry_finite : bool;
   mind_entry_inds : one_inductive_entry list }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d14010dbe..1f357eb29 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -481,7 +481,7 @@ let allowed_sorts env issmall isunit = function
         then logical_sorts else impredicative_sorts
       else logical_sorts
 
-let build_inductive env env_ar finite inds recargs cst =
+let build_inductive env env_ar record finite inds recargs cst =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
@@ -527,7 +527,8 @@ let build_inductive env env_ar finite inds recargs cst =
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)
-  { mind_ntypes = ntypes;
+  { mind_record = record;
+    mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
     mind_packets = packets;
@@ -544,5 +545,6 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let recargs = check_positivity env_arities inds in
   (* Build the inductive packets *)
-  build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+  build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite 
+    inds recargs cst
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 50aeaf347..099e93117 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -132,6 +132,21 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 	  in
 	    if kn1 <> kn2 then error ()
   end;
+  (* we check that records and their field names are preserved. *)
+  check (fun mib -> mib.mind_record);
+  if mib1.mind_record then begin 
+    let rec names_prod_letin t = match kind_of_term t with 
+      | Prod(n,_,t) -> n::(names_prod_letin t)
+      | LetIn(n,_,_,t) -> n::(names_prod_letin t)
+      | Cast(t,_) -> names_prod_letin t
+      | _ -> []
+    in 
+    assert (Array.length mib1.mind_packets = 1);
+    assert (Array.length mib2.mind_packets = 1);
+    assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); 
+    assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); 
+    check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+  end;
   (* we first check simple things *)
   let cst = 
     array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets