More factorization of inductive/record and typeclasses: move class

declaration code to toplevel/record, including support for singleton
classes as definitions. Parsing code also factorized. Arnaud: one more
thing to think about when refactoring the definitions in vernacentries.
Add support for specifying what to do with anonymous variables in
contexts during internalisation (fixes bug #1982), current choice is to
generate a name for typeclass bindings.


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

4 files changed, 22 insertions, 27 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b061da5a8..3e3b61e1b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -147,7 +147,7 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let
+  binder binder_let binders_let record_declaration
   binders_let_fixannot typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e1df1cf49..b48548f98 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -48,6 +48,7 @@ let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
 let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
+let record_field = Gram.Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
 
 let get_command_entry () =
@@ -129,7 +130,7 @@ let no_coercion loc (c,x) =
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_context typeclass_constraint decl_notation;
+    typeclass_context typeclass_constraint record_field decl_notation;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -168,7 +169,7 @@ GEXTEND Gram
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = identref;
         ps = binders_let; 
-	s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
+	s = OPT [ ":"; s = lconstr -> s ];
 	":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
@@ -243,7 +244,7 @@ GEXTEND Gram
   (* Inductives and records *)
   inductive_definition:
     [ [ id = identref; indpar = binders_let; 
-        c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
+        c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
 	   ((id,indpar,c,lc),ntn) ] ]
   ;
@@ -253,8 +254,8 @@ GEXTEND Gram
 	      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) 
+	     RecordDecl (false,Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (false,None,fs) 
       |  -> Constructors [] ] ]
   ;
 (*
@@ -500,16 +501,17 @@ GEXTEND Gram
 
       (* Type classes, new syntax without artificial sup. *)
       | IDENT "Class"; qid = identref; pars = binders_let;
-	 s = [ ":"; c = sort -> Some (loc, c) | -> None ];
-	 props = typeclass_field_types ->
-	   VernacClass (qid, pars, s, [], props)
+           s = OPT [ ":"; c = lconstr -> c ];
+	   fs = class_fields ->
+	   VernacInductive (false, [((qid,pars,s,RecordDecl (false,None,fs)),None)])
 
       (* Type classes *)
       | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
 	 qid = identref; pars = binders_let;
-	 s = [ ":"; c = sort -> Some (loc, c) | -> None ];
-	 props = typeclass_field_types ->
-	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
+         s = OPT [ ":"; c = lconstr -> c ];
+	 fs = class_fields ->
+	   VernacInductive 
+	     (false, [((qid,Option.cata (fun x -> x) [] sup @ pars,s,RecordDecl (false,None,fs)),None)])
 	     
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
@@ -517,7 +519,8 @@ GEXTEND Gram
       | IDENT "Instance"; local = non_locality; name = identref; 
 	 sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
+	 pri = OPT [ "|"; i = natural -> i ] ; 
+	 props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
 	   let sup =
 	     match sup with
 		 None -> []
@@ -542,26 +545,16 @@ 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)
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-  typeclass_field_type:
-    [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ]
-  ;
-  typeclass_field_def:
-    [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ]
-  ;
-  typeclass_field_types:
-    [ [ ":="; l = LIST1 typeclass_field_type SEP ";" -> l
-    | -> [] ] ]
-  ;
-  typeclass_field_defs:
-    [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l
-    | -> [] ] ]
-  ;
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 69c1164f1..ed4f41c4e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -445,6 +445,7 @@ module Constr =
     let binders_let = Gram.Entry.create "constr:binders_let"
     let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
+    let record_declaration = Gram.Entry.create "constr:record_declaration"
     let appl_arg = Gram.Entry.create "constr:appl_arg"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fa8c2a6f5..e089389fe 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -167,6 +167,7 @@ module Constr :
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
     val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e
+    val record_declaration : constr_expr Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end