Mise en place possibilité de définitions locales dans les paramètres des records

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

8 files changed, 39 insertions, 55 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 7394a41c5d..bef1e2a23c 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -47,7 +47,10 @@ let ast_set = CSort (dummy_loc,RProp Pos)
 let tuple_n n =
   let id = make_ident "tuple_" (Some n) in
   let l1n = Util.interval 1 n in
-  let params = List.map (fun i -> (make_ident "T" (Some i), ast_set)) l1n in
+  let params =
+    List.map (fun i ->
+      (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set)))
+      l1n in
   let fields = 
     List.map
       (fun i -> 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 72cf41ad45..3e4d486a8f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1508,7 +1508,8 @@ let xlate_vernac =
       CT_record
        ((if add_coercion then CT_coercion_atm else
           CT_coerce_NONE_to_COERCION_OPT(CT_none)),
-        xlate_ident s, cvt_vernac_binders binders, xlate_sort c1, record_constructor,
+        xlate_ident s, xlate_binder_list binders, 
+	xlate_sort c1, record_constructor,
          build_record_field_list field_list)
 
   |    VernacRecord _ -> xlate_error "TODO: Record in a defined sort"
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 21906628cd..d21c46cea8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -222,9 +222,6 @@ GEXTEND Gram
   oneind:
     [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
         ntn = OPT decl_notation ; ":="; lc = constructor_list ->
-	  let indpar = 
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
-	      indpar in
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
@@ -286,7 +283,9 @@ GEXTEND Gram
     [ [ "["; bll = LIST1 simple_params SEP ";"; "]" -> List.flatten bll ] ]
   ;
   ne_simple_binders_list:
-    [ [ bll = LIST1 simple_binders -> List.flatten bll ] ]
+    [ [ bll = LIST1 simple_binders ->
+          List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
+            (List.flatten bll) ] ]
   ;
   fix_params:
     [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
@@ -306,9 +305,6 @@ GEXTEND Gram
   gallina_ext:
     [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
         indl = block_old_style ->
-	  let bl = 
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t)) bl
-	  in
 	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
       | b = record_token; oc = opt_coercion; name = base_ident;
@@ -327,9 +323,6 @@ GEXTEND Gram
       | IDENT "Scheme"; l = schemes -> VernacScheme l
       | f = finite_token; s = csort; id = base_ident;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
-	  let indpar =
-	    List.map (fun (id,t) -> LocalRawAssum ([dummy_loc,Name id],t))
-	      indpar in
           VernacInductive (f,[id,None,indpar,s,lc]) ] ]
   ;
   csort:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 3c1fad5d18..34bdbbb8cc 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -120,7 +120,7 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = base_ident;
-        ps = LIST0 simple_binder; ":";
+        ps = LIST0 binder_let; ":";
 	s = lconstr; ":="; cstr = OPT base_ident; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
@@ -250,9 +250,6 @@ GEXTEND Gram
   ;
   (* Various Binders *)
   (* ... without coercions *)
-  simple_binder:
-    [ [ b = simple_binder_coe -> no_coercion loc b ] ]
-  ;
   binder_nodef:
     [ [ b = binder_let ->
       (match b with
@@ -283,13 +280,6 @@ GEXTEND Gram
     [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr -> 
         (oc,(idl,c)) ] ]
   ;
-  simple_binder_coe:
-    [ [ id=base_ident -> (false,(id,CHole loc))
-      | "("; id = base_ident; ")" -> (false,(id,CHole loc))
-      | "("; id = base_ident; oc = of_type_with_opt_coercion;
-             t = lconstr; ")" ->
-         (oc,(id,t)) ] ]
-  ;
   constructor:
     [ [ id = base_ident; l = LIST0 binder_let; 
         coe = of_type_with_opt_coercion; c = lconstr ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 7e0286b218..a165f006d8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -44,16 +44,20 @@ let interp_decl sigma env = function
       let j = judgment_of_rawconstr Evd.empty env c in
       (Name id,Some j.uj_val, j.uj_type)
 
-let build_decl_entry sigma env (id,t) =
-  (id,Entries.LocalAssum (interp_type Evd.empty env t))
-
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
   let env1,newps =
     List.fold_left
-      (fun (env,newps) (id,t) -> 
-        let decl = interp_decl Evd.empty env (Vernacexpr.AssumExpr (id,t)) in
-        (push_rel decl env,decl::newps))
+      (fun (env,newps) d -> match d with
+	| LocalRawAssum (nal,t) ->
+	    let t = interp_type Evd.empty env t in
+	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
+	    let ctx = List.rev ctx in
+	    (push_rel_context ctx env, ctx@newps)
+	| LocalRawDef ((_,na),c) ->
+	    let c = judgment_of_rawconstr Evd.empty env c in
+	    let d = (na, Some c.uj_val, c.uj_type) in
+	    (push_rel d env, d::newps))
       (env0,[]) ps
   in
   let env2,newfs =
@@ -65,9 +69,13 @@ let typecheck_params_and_fields ps fs =
   in
   newps, newfs
 
-let degenerate_decl id = function
-    (_,None,t) -> (id,Entries.LocalAssum t)
-  | (_,Some c,t) -> (id,Entries.LocalDef c)
+let degenerate_decl (na,b,t) =
+  let id = match na with
+    | Name id -> id
+    | Anonymous -> anomaly "Unnamed record variable" in 
+  match b with
+    | None -> (id, Entries.LocalAssum t)
+    | Some b -> (id, Entries.LocalDef b)
 
 type record_error =
   | MissingProj of identifier * identifier list
@@ -172,7 +180,10 @@ let declare_projections indsp coers fields =
 		    const_entry_body = proj;
                     const_entry_type = Some projtyp;
                     const_entry_opaque = false } in
-		  declare_constant fid (DefinitionEntry cie,IsDefinition)
+		  let k = (DefinitionEntry cie,IsDefinition) in
+		  let sp = declare_constant fid k in
+		  Options.if_verbose message (string_of_id fid ^" is defined");
+		  sp
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
@@ -194,23 +205,17 @@ let declare_projections indsp coers fields =
    list telling if the corresponding fields must me declared as coercion *)
 let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
-  let nparams = List.length ps in
-  let idps = List.map fst ps in
+  let nparams = local_binders_length ps in
   let extract_name = function Vernacexpr.AssumExpr(id,_) -> id | Vernacexpr.DefExpr (id,_,_) -> id in
-  let allnames =  idstruc::idps@(List.map extract_name fs) in
+  let allnames =  idstruc::(List.map extract_name fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
   let params,fields = typecheck_params_and_fields ps fs in
-(*  let args =  List.map mkVar idps in*)
   let args = extended_rel_list (List.length fields) params in
-(*  let ind = applist (mkVar idstruc, args) in*)
   let ind = applist (mkRel (1+List.length params+List.length fields), args) in
-  let subst = List.rev (idstruc::idps) in
-(*  let named_type_constructor = it_mkNamedProd_or_LetIn ind fields in*)
-  let named_type_constructor = it_mkProd_or_LetIn ind fields in
-  let type_constructor = (* subst_vars subst *) named_type_constructor in
+  let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_params = List.map2 degenerate_decl (List.rev idps) params;
+    { mind_entry_params = List.map degenerate_decl params;
       mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
diff --git a/toplevel/record.mli b/toplevel/record.mli
index ddee8f1d8f..45d6e69ba6 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -24,5 +24,5 @@ val declare_projections :
   inductive -> bool list -> rel_context -> constant option list
 
 val definition_structure :
-  identifier with_coercion * (identifier * constr_expr) list *
+  identifier with_coercion * local_binder list *
   (local_decl_expr with_coercion) list * identifier * sorts -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index fc57d23aa8..4594939470 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -184,7 +184,7 @@ type vernac_expr =
 
   (* Gallina extensions *)
   | VernacRecord of bool (* = Record or Structure *)
-      * identifier with_coercion * simple_binder list
+      * identifier with_coercion * local_binder list
       * constr_expr * identifier option * local_decl_expr with_coercion list
   | VernacBeginSection of identifier
   | VernacEndSegment of identifier
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index f3a0798eff..a8ccc7dcf4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -324,14 +324,6 @@ let pr_vbinders l =
 let pr_binders_arg bl =
   if bl = [] then mt () else spc () ++ pr_binders bl
 
-let pr_sbinders sbl =
-  if sbl = [] then mt () else
-    let bl =
-      List.map (fun (id,c) -> 
-        let c = anonymize_binder (Name id) c in
-        LocalRawAssum ([(dummy_loc,Name id)],c)) sbl in
-    pr_binders bl ++ spc ()
-
 let pr_onescheme (id,dep,ind,s) =
   hov 0 (pr_id id ++ str" :=") ++ spc() ++
   hov 0 ((if dep then str"Induction for" else str"Minimality for")
@@ -843,8 +835,8 @@ pr_vbinders bl ++ spc())
                 pr_lconstr b)) in
       hov 2
         (str (if b then "Record" else "Structure") ++
-         (if oc then str" > " else str" ") ++ pr_id name ++ spc() ++
-         pr_sbinders ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++
+         (if oc then str" > " else str" ") ++ pr_id name ++ 
+         pr_binders_arg ps ++ str" :" ++ spc() ++ pr_lconstr s ++ str" := " ++
          (match c with
            | None -> mt()
            | Some sc -> pr_id sc) ++