Move Record desugaring to constrintern and add ability to use notations

for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).


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

3 files changed, 27 insertions, 24 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5ecbab90ed..b061da5a89 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -42,6 +42,11 @@ let loc_of_binder_let = function
   | LocalRawDef ((loc,_),_)::_ -> loc
   | _ -> dummy_loc
 
+let binders_of_lidents l =
+  List.map (fun (loc, id) -> 
+    LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, 
+		  CHole (loc, Some (Evd.BinderType (Name id))))) l
+    
 let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
     | [loc,Name id], (None, r) -> Some (loc, id), r
@@ -241,7 +246,8 @@ GEXTEND Gram
     ] ]
   ;
   record_field_declaration:
-    [ [ id = identref; ":="; c = lconstr -> (id, c) ] ]
+    [ [ id = identref; params = LIST0 identref; ":="; c = lconstr -> 
+      (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
     [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3f8adb92f9..e1df1cf49e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -172,11 +172,6 @@ GEXTEND Gram
 	":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
-(* Non porté ?
-      | f = finite_token; s = csort; id = identref;
-        indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
-          VernacInductive (f,[id,None,indpar,s,lc])
-*)
     ] ]
   ;
   typeclass_context:
@@ -331,6 +326,9 @@ GEXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
+    [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
+  ;
+  record_binder:
     [ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
       | id = name; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e2237450ce..3c8613aad4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -411,23 +411,22 @@ let pr_intarg n = spc () ++ int n in
 let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
 let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
   ++ sep ++ pr_constrarg c in
-
- let pr_record_field = function
-   | (oc,AssumExpr (id,t)) ->
-       hov 1 (pr_lname id ++
-		(if oc then str" :>" else str" :") ++ spc() ++
-		pr_lconstr_expr t)
-   | (oc,DefExpr(id,b,opt)) -> 
-       (match opt with
-	  | Some t ->
-	      hov 1 (pr_lname id ++
-		       (if oc then str" :>" else str" :") ++ spc() ++
-		       pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
-	  | None ->
-	      hov 1 (pr_lname id ++ str" :=" ++ spc() ++
-		       pr_lconstr b))
+let pr_record_field (x, ntn) = 
+  let prx = match x with
+    | (oc,AssumExpr (id,t)) ->
+	hov 1 (pr_lname id ++
+		  (if oc then str" :>" else str" :") ++ spc() ++
+		  pr_lconstr_expr t)
+    | (oc,DefExpr(id,b,opt)) -> (match opt with
+      | Some t ->
+          hov 1 (pr_lname id ++
+                    (if oc then str" :>" else str" :") ++ spc() ++
+                    pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+      | None ->
+          hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+                    pr_lconstr b)) in
+    prx ++ pr_decl_notation pr_constr ntn
 in
-
 let pr_record_decl c fs = 
     pr_opt pr_lident c ++ str"{"  ++
     hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
@@ -708,7 +707,7 @@ let rec pr_vernac = function
 (* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *)
 	  pr_and_type_binders_arg par ++
 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++
-	  spc () ++ str"where" ++ spc () ++
+	  spc () ++ str":=" ++ spc () ++
 	  prlist_with_sep (fun () -> str";" ++ spc()) 
 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
 	
@@ -720,7 +719,7 @@ let rec pr_vernac = function
 	 str"=>" ++ spc () ++ 
 	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
 	 pr_constr_expr cl ++ spc () ++
-	 spc () ++ str"where" ++ spc () ++
+	 spc () ++ str":=" ++ spc () ++
 	 prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props)
 
  | VernacContext l ->