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, 23 insertions, 18 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 59559f9234..79d34e878e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -274,7 +274,7 @@ let declare_instance_cst glob con =
       | Some tc -> add_instance (new_instance tc None glob con)
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
-let declare_class finite id idbuild paramimpls params arity fieldimpls fields
+let declare_class finite def id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers =
   let fieldimpls = 
     (* Make the class and all params implicits in the projections *)
@@ -284,7 +284,7 @@ let declare_class finite id idbuild paramimpls params arity fieldimpls fields
   in
   let impl, projs =
     match fields with
-    | [(Name proj_name, _, field)] ->
+    | [(Name proj_name, _, field)] when def ->
 	let class_body = it_mkLambda_or_LetIn field params in
 	let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
 	let class_entry =
@@ -373,5 +373,5 @@ let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
 	in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
-    | Class ->
-	declare_class finite (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+    | Class b ->
+	declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5f5dab6146..f5603535b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -387,7 +387,7 @@ let vernac_record k finite struc binders sort nameopt cfs =
       
 let vernac_inductive finite indl = 
   if Dumpglob.dump () then
-    List.iter (fun ((lid, _, _, cstrs), _) ->
+    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
       match cstrs with 
 	| Constructors cstrs ->
 	    Dumpglob.dump_definition lid false "ind";
@@ -396,12 +396,22 @@ let vernac_inductive finite indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( id , bl , c ,RecordDecl (b,oc,fs) ), None ] -> 
-      vernac_record b finite (false,id) bl c oc fs
-  | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> 
+  | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> 
+      vernac_record (match b with Class true -> Class false | _ -> b)
+	finite id bl c oc fs
+  | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> 
+      let f = 
+	let (coe, ((loc, id), ce)) = l in
+	  ((coe, AssumExpr ((loc, Name id), ce)), None)
+      in vernac_record (Class true) finite id bl c None [f]
+  | [ ( id , bl , c , Some (Class true), _), _ ] -> 
+      Util.error "Definitional classes must have a single method"
+  | [ ( id , bl , c , Some (Class false), Constructors _), _ ] ->
+      Util.error "Inductive classes not supported"
+  | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> 
       Util.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function 
-      | ( id , bl , c , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
+      | ( (_, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
       | _ -> Util.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
@@ -1314,7 +1324,6 @@ let interp c = match c with
 
   | VernacEndSegment lid -> vernac_end_segment lid
 
-  | VernacRecord ((k,finite),id,bl,s,idopt,fs) -> vernac_record k finite id bl s idopt fs
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
@@ -1322,8 +1331,6 @@ let interp c = match c with
   | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
   (* Type classes *)
-(*   | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props *)
-
   | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance id -> vernac_declare_instance id
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5fff24fef7..8e797a8834 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -155,7 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type record_kind = Record | Structure | Class
+type record_kind = Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
@@ -164,9 +164,10 @@ type 'a with_notation = 'a * decl_notation
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of record_kind * lident option * local_decl_expr with_coercion with_notation list
+  | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-  lident * local_binder list * constr_expr option * constructor_list_or_record_decl_expr
+  lident with_coercion * local_binder list * constr_expr option * record_kind option * 
+    constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast
 
@@ -217,9 +218,6 @@ type vernac_expr =
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
-  | VernacRecord of (record_kind*bool) (* = Structure or Class * Inductive or CoInductive *)
-      * lident with_coercion * local_binder list
-      * constr_expr option * lident option * local_decl_expr with_coercion with_notation list
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of