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

17 files changed, 48 insertions, 44 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 247bd137b..26a263942 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -351,6 +351,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	in 
 	let n = nb_default_params env mip0.mind_nf_arity in
 	let projs = try List.map out_some projs with _ -> raise (I Standard) in
+	(* avoid constant projections (records fields defined with [:=]) *)
 	let is_true_proj kn = 
           let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in
           match kind_of_term body with
@@ -366,6 +367,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
               if type_eq (mlt_env env) Tdummy typ then l1,l2 
               else 
                 let r = ConstRef kn in 
+		(* avoid dummy arguments for projectors *)
                 if List.mem false (type_to_sign (mlt_env env) typ) 
                 then r :: l1, l2 
                 else r :: l1, r :: l2
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 0498987b3..f4daa5a7a 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -421,8 +421,8 @@ let pp_singleton kn packet =
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn packet = 
-  let l = List.combine (find_projections kn) packet.ip_types.(0) in 
   let projs = find_projections kn in
+  let l = List.combine projs packet.ip_types.(0) in 
   let pl = rename_tvars keywords packet.ip_vars in 
   str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
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
diff --git a/library/declare.ml b/library/declare.ml
index 398fed704..6c8526b91 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -271,6 +271,7 @@ let dummy_one_inductive_entry mie = {
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_inductive_entry m = {
+  mind_entry_record = false;
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 238fd470f..7f56101a4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -60,10 +60,6 @@ let inh_pattern_coerce_to loc pat ind1 ind2 =
 (* appliquer le chemin de coercions p à hj *)
 
 let apply_coercion env p hj typ_cl =
-  if !compter then begin
-    nbpathc := !nbpathc +1; 
-    nbcoer := !nbcoer + (List.length p)
-  end;
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42af2bfe6..6917d6735 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -377,21 +377,16 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
 	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in
-  if (list_for_all2eq 
-	(fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
-	us2 us)
-    &
-    (list_for_all2eq 
-       (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
-       params1 params)
-    & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
-    & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
-  then
-    (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
-                              nbimplstruc:=!nbimplstruc+(List.length ks);true)
-            else true)
-  else false
-
+  (list_for_all2eq 
+     (fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
+     us2 us)
+  &
+  (list_for_all2eq 
+     (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
+     params1 params)
+  & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
+  & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
+    
 let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV  t1 t2
 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
  
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 49baf2ade..fb11eb558 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -238,7 +238,6 @@ let rec pretype tycon env isevars lvar = function
       anomaly "Found a pattern variable in a rawterm to type"
 	   
   | RHole (loc,k) ->
-      if !compter then nbimpl:=!nbimpl+1;
       (match tycon with
 	 | Some ty ->
 	     { uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
@@ -892,7 +891,6 @@ let rec pretype tycon env isevars lvar = function
 (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
 and pretype_type valcon env isevars lvar = function
   | RHole loc ->
-      if !compter then nbimpl:=!nbimpl+1;
       (match valcon with
 	 | Some v ->
              let s =
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e2e574d7f..4ea0da0a4 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,14 +20,6 @@ open Libobject
 open Library
 open Classops
 
-let nbimpl = ref 0
-let nbpathc = ref 0
-let nbcoer = ref 0
-let nbstruc = ref 0
-let nbimplstruc = ref 0
-
-let compter = ref false
-
 (*s Une structure S est un type inductif non récursif à un seul
    constructeur (de nom par défaut Build_S) *)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index f758776de..7989535b9 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -18,13 +18,6 @@ open Libobject
 open Library
 (*i*)
 
-val nbimpl : int ref
-val nbpathc : int ref
-val nbcoer : int ref
-val nbstruc : int ref
-val nbimplstruc : int ref
-val compter : bool ref
-
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index fc2c2cb29..411d42df5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -358,7 +358,9 @@ let interp_mutual lparams lnamearconstrs finite =
       (List.rev arityl) lnamearconstrs
   in
   States.unfreeze fs;
-  notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec }
+  notations, { mind_entry_record = false; 
+	       mind_entry_finite = finite; 
+	       mind_entry_inds = mispecvec }
   with e -> States.unfreeze fs; raise e
 
 let declare_mutual_with_eliminations isrecord mie =
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5f2c068fd..12c5056ee 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -118,6 +118,7 @@ let abstract_inductive sec_sp ids_to_abs hyps inds =
 
 let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   assert (Array.length mib.mind_packets > 0);
+  let record = mib.mind_record in 
   let finite = mib.mind_finite in
   let inds = 
     array_map_to_list
@@ -153,7 +154,8 @@ let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   in
   let indmodifs,cstrmodifs =
     List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
-  ({ mind_entry_finite = finite;
+  ({ mind_entry_record = record;
+     mind_entry_finite = finite;
      mind_entry_inds = inds' },
    indmodifs,
    List.flatten cstrmodifs,
diff --git a/toplevel/record.ml b/toplevel/record.ml
index acddd2e61..843e4e074 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -226,7 +226,8 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let mie =
-    { mind_entry_finite = true;
+    { mind_entry_record = true;
+      mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations true mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)