Nouvelle syntaxe pour écrire des records (co)inductifs :

CoInductive stream (A:Type) := { hd : A ; tl : stream A }.

Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.

L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de 
la syntaxe qui était apparue dans la 8.2beta pour les records 
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" 
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il 
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.





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

2 files changed, 54 insertions, 36 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f0ea35d92..3f8adb92f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -224,7 +224,7 @@ GEXTEND Gram
       | "CoInductive" -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
+    [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]]
   ;
   (* Simple definitions *)
   def_body:
@@ -249,13 +249,18 @@ GEXTEND Gram
   inductive_definition:
     [ [ id = identref; indpar = binders_let; 
         c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
-        ":="; lc = constructor_list; ntn = decl_notation ->
-	  ((id,indpar,c,lc),ntn) ] ]
-  ;
-  constructor_list:
-    [ [ "|"; l = LIST1 constructor SEP "|" -> l
-      | l = LIST1 constructor SEP "|" -> l
-      |  -> [] ] ]
+        ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
+	   ((id,indpar,c,lc),ntn) ] ]
+  ;
+  constructor_list_or_record_decl:
+    [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
+      | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> 
+	      Constructors ((c id)::l)
+      | id = identref ; c = constructor_type -> Constructors [ c id ]
+      | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
+	     RecordDecl (Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) 
+      |  -> Constructors [] ] ]
   ;
 (*
   csort:
@@ -346,12 +351,19 @@ GEXTEND Gram
     [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> 
         (oc,(idl,c)) ] ]
   ;
+
+  constructor_type:
+    [[ l = binders_let; 
+      t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+	            fun l id -> (coe,(id,mkCProdN loc l c))
+            |  ->
+		 fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ]
+	 -> t l
+     ]]
+;
+
   constructor:
-    [ [ id = identref; l = binders_let; 
-        coe = of_type_with_opt_coercion; c = lconstr ->
-	  (coe,(id,mkCProdN loc l c))
-      | id = identref; l = binders_let ->
-	  (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
+    [ [ id = identref; c=constructor_type -> c id ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 2233bbd6a..e2237450c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -412,6 +412,27 @@ 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))
+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"}")
+in
+
 let rec pr_vernac = function
   
   (* Proof management *)
@@ -565,12 +586,15 @@ let rec pr_vernac = function
                (if coe then str":>" else str":") ++
                 pr_spc_lconstr c) in
       let pr_constructor_list l = match l with
-        | [] -> mt()
-        | _ ->
+        | Constructors [] -> mt()
+        | Constructors l ->
             pr_com_at (begin_of_inductive l) ++
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
-            prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
+            prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l 
+       | RecordDecl (c,fs) ->   
+	    spc() ++
+	    pr_record_decl c fs in
       let pr_oneind key ((id,indpar,s,lc),ntn) =
 	hov 0 (
           str key ++ spc() ++
@@ -644,30 +668,12 @@ let rec pr_vernac = function
 	
 
   (* Gallina extensions *)
-  | VernacRecord (b,(oc,name),ps,s,c,fs) ->
-      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)) in
+  | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
       hov 2
         (str (if b then "Record" else "Structure") ++
          (if oc then str" > " else str" ") ++ pr_lident name ++ 
           pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
-	  pr_lconstr_expr s ++ str" := " ++
-         (match c with
-           | None -> mt()
-           | Some sc -> pr_lident sc) ++
-	spc() ++ str"{"  ++
-        hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
+	  pr_lconstr_expr s ++ str" := " ++ pr_record_decl c fs)
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2