Generalized binding syntax overhaul: only two new binders: `() and `{},

guessing the binding name by default and making all generalized
variables implicit. At the same time, continue refactoring of
Record/Class/Inductive etc.., getting rid of [VernacRecord]
definitively. The AST is not completely satisfying, but leaning towards 
Record/Class as restrictions of inductive (Arnaud, anyone ?).
Now, [Class] declaration bodies are either of the form [meth : type] or 
[{ meth : type ; ... }], distinguishing singleton "definitional" classes
and inductive classes based on records. The constructor syntax is
accepted ([meth1 : type1 | meth1 : type2]) but raises an error
immediately, as support for defining a class by a general inductive type
is not there yet (this is a bugfix!).


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

3 files changed, 32 insertions, 54 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e3b61e1b1..37c09704e6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -241,8 +241,8 @@ GEXTEND Gram
   ;
   record_declaration:
     [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
-      | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" ->
-	  CRecord (loc, Some c, fs)
+(*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
+(* 	  CRecord (loc, Some c, fs) *)
     ] ]
   ;
   record_field_declaration:
@@ -432,15 +432,9 @@ GEXTEND Gram
         [LocalRawAssum ([id],Default Implicit,c)]
     | "{"; id=name; idl=LIST1 name; "}" -> 
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
-    | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc
-    | "{"; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; "}" ->
+    | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
-    | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
-    | "("; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Implicit, b), t)) tc
-    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+    | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
 	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d870c85eb0..4ffd53fe4e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -170,10 +170,11 @@ GEXTEND Gram
     [ [ b = record_token; oc = opt_coercion; name = identref;
         ps = binders_let; 
 	s = OPT [ ":"; s = lconstr -> s ];
-	":="; cstr = OPT identref; "{";
-        fs = LIST0 record_field SEP ";"; "}" ->
-	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
-    ] ]
+	cfs = [ ":="; l = constructor_list_or_record_decl -> l
+	  | -> RecordDecl (None, []) ] ->
+	  let (recf,indf) = b in
+	    VernacInductive (indf,[((oc,name),ps,s,Some recf,cfs),None])
+  ] ]
   ;
   typeclass_context:
     [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l 
@@ -222,7 +223,7 @@ GEXTEND Gram
   record_token:
     [ [ IDENT "Record" -> (Record,true)
       | IDENT "Structure" -> (Structure,true) 
-      | IDENT "Class" -> (Class,true) ] ]
+      | IDENT "Class" -> (Class true,true) ] ]
   ;
   (* Simple definitions *)
   def_body:
@@ -245,19 +246,19 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = binders_let; 
+    [ [ id = identref; oc = opt_coercion; indpar = binders_let; 
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
-	   ((id,indpar,c,lc),ntn) ] ]
+	   (((oc,id),indpar,c,None,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)
+	  Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
       | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
-	     RecordDecl (Record,Some cstr,fs) 
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (Record,None,fs) 
+	  RecordDecl (Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) 
       |  -> Constructors [] ] ]
   ;
 (*
@@ -500,20 +501,6 @@ GEXTEND Gram
       | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
-
-      (* Type classes, new syntax without artificial sup. *)
-      | IDENT "Class"; qid = identref; pars = binders_let;
-           s = OPT [ ":"; c = lconstr -> c ];
-	   fs = class_fields ->
-	   VernacInductive (false, [((qid,pars,s,RecordDecl (Class,None,fs)),None)])
-
-      (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
-	 qid = identref; pars = binders_let;
-         s = OPT [ ":"; c = lconstr -> c ];
-	 fs = class_fields ->
-	   VernacInductive 
-	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (Class,None,fs)),None)])
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
@@ -547,10 +534,6 @@ GEXTEND Gram
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
-  class_fields:
-    [ [ ":="; fs = LIST1 record_field SEP ";" -> fs
-      | -> [] ] ]
-  ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
     | id = ident -> (id,false,false)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 01e44f84c9..33c7654d25 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -582,24 +582,31 @@ let rec pr_vernac = function
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
                 pr_spc_lconstr c) in
-      let pr_constructor_list l = match l with
+      let pr_constructor_list b l = match l with
         | 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 
-       | RecordDecl (b,c,fs) ->   
+       | RecordDecl (c,fs) ->   
 	    spc() ++
 	    pr_record_decl b c fs in
-      let pr_oneind key ((id,indpar,s,lc),ntn) =
-	hov 0 (
-          str key ++ spc() ++
-          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ 
-	    Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
-	  str" :=") ++ pr_constructor_list lc ++ 
-	pr_decl_notation pr_constr ntn in
-
+      let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+	let kw =
+	  match k with
+	  | None -> str key
+	  | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" 
+	    | Class b -> if b then "Definitional Class" else "Class")
+	in
+	  hov 0 (
+	    kw ++ spc() ++
+              (if coe then str" > " else str" ") ++ pr_lident id ++
+              pr_and_type_binders_arg indpar ++ spc() ++ 
+	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
+	      str" :=") ++ pr_constructor_list k lc ++ 
+	    pr_decl_notation pr_constr ntn 
+      in
       hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
       ++ 
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
@@ -665,12 +672,6 @@ let rec pr_vernac = function
 	
 
   (* Gallina extensions *)
-  | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
-      hov 2
-        (str (match b with Record -> "Record" | Structure -> "Structure" | Class -> "Class") ++
-         (if oc then str" > " else str" ") ++ pr_lident name ++ 
-          pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
-	  Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b 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