Cleaner quantifiers for type classes, breaks clrewrite for the moment but implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.

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

5 files changed, 26 insertions, 17 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a7d905032..bd6c15ffa 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -102,7 +102,7 @@ let lpar_id_coloneq =
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let typeclass_constraint typeclass_param pattern;
+  binder binder_let binders_let typeclass_constraint pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -359,11 +359,11 @@ GEXTEND Gram
   ;
   typeclass_constraint:
     [ [ id=identref ; cl = LIST1 typeclass_param -> 
-      (loc, Anonymous), Explicit, mkAppC (mkIdentC (snd id), cl)
+      (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
     | "?" ; id=identref ; cl = LIST1 typeclass_param -> 
-	(loc, Anonymous), Implicit, mkAppC (mkIdentC (snd id), cl)
+	(loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
     | iid=identref ; ":" ; id=typeclass_name ; cl = LIST1 typeclass_param -> 
-	(fst iid, Name (snd iid)), (fst id), mkAppC (mkIdentC (snd (snd id)), cl)
+	(fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
     ] ]
   ;
   typeclass_name:
@@ -371,10 +371,14 @@ GEXTEND Gram
     | "?"; id = identref -> (Implicit, id)
     ] ]
   ;
+
   typeclass_param: 
-    [ [ id = identref -> CRef (Libnames.Ident id)
-    | c = sort -> CSort (loc, c)
-    | "("; c = lconstr; ")" -> c ] ]
+    [ [ id = identref -> CRef (Libnames.Ident id), None
+    | c = sort -> CSort (loc, c), None
+    | id = lpar_id_coloneq; c=lconstr; ")" ->
+	(c,Some (loc,ExplByName id))
+    | c=operconstr LEVEL "9" -> c, None
+    ] ]
   ;
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ee2036167..540d1aac0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -436,7 +436,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)   
 GEXTEND Gram
-  GLOBAL: gallina_ext typeclass_param;
+  GLOBAL: gallina_ext;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -472,9 +472,15 @@ GEXTEND Gram
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
 
+      (* Type classes, new syntax without artificial sup. *)
+      | IDENT "Class"; qid = identref; pars = binders_let;
+	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
+	 props = typeclass_field_types ->
+	   VernacClass (qid, pars, s, [], props)
+
       (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = typeclass_context; "=>" -> l ];
-	 qid = identref; pars = LIST0 typeclass_param_type;
+      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
+	 qid = identref; pars = binders_let;
 	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
 	 props = typeclass_field_types ->
 	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
@@ -517,10 +523,10 @@ GEXTEND Gram
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-  typeclass_param_type:
-    [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t 
-    | id = identref -> id, CHole loc ] ]
-  ;
+(*   typeclass_param_type: *)
+(*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
+(*     | id = identref -> id, CHole loc ] ] *)
+(*   ; *)
   typeclass_field_type:
     [ [ id = identref; ":"; t = lconstr -> id, t ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 56d547cb5..2430b8863 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -436,7 +436,6 @@ module Constr =
     let binder_let = Gram.Entry.create "constr:binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
-    let typeclass_param = Gram.Entry.create "constr:typeclass_param"
   end
 
 module Module =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index eaf298e06..89bdf13eb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -165,7 +165,6 @@ module Constr :
     val binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
-    val typeclass_param : constr_expr Gram.Entry.e
   end
 
 module Module : 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1470f6902..0b889bf08 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -696,7 +696,8 @@ let rec pr_vernac = function
   | VernacClass (id, par, ar, sup, props) ->
       hov 1 (
 	str"Class" ++ spc () ++ pr_lident id ++
-	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ 
+(* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *)
+	  pr_and_type_binders_arg par ++
 	  spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) ++
 	  spc () ++ str"where" ++ spc () ++
 	  prlist_with_sep (fun () -> str";" ++ spc()) (pr_lident_constr (spc () ++ str":" ++ spc())) props )