Syntax changes in typeclasses, remove "?" for usual implicit arguments

binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


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

6 files changed, 88 insertions, 54 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9972d9e248..68389c54a4 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -99,10 +99,34 @@ let lpar_id_coloneq =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let impl_ident =
+  Gram.Entry.of_parser "impl_ident"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+	| [("IDENT",("wf"|"struct"|"measure"))] ->
+	    raise Stream.Failure
+	| [("IDENT",s)] -> 
+	    Stream.junk strm;
+            Names.id_of_string s
+	| _ -> raise Stream.Failure)
+
+let ident_eq =
+  Gram.Entry.of_parser "ident_eq"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+	| [("IDENT",s)] ->
+            (match Stream.npeek 2 strm with
+              | [_; ("", ":")] ->
+                  Stream.junk strm; Stream.junk strm;
+                  Names.id_of_string s
+              | _ -> raise Stream.Failure)
+        | _ -> raise Stream.Failure)
+
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let delimited_binder_let delimited_binders_let typeclass_constraint pattern;
+  binder binder_let binders_let delimited_binder_let delimited_binders_let
+  binders_let_fixannot typeclass_constraint pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -244,16 +268,16 @@ GEXTEND Gram
       | "cofix" -> false ] ]
   ;
   fix_decl:
-    [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
-        c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
-  ;
-  fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
-      | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
-      | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
-      | ->  (None, CStructRec)
-      ] ]
-  ;
+    [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
+        c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
+  ;
+(*   fixannot: *)
+(*     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) *)
+(*       | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) *)
+(*       | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) *)
+(*       | ->  (None, CStructRec) *)
+(*       ] ] *)
+(*   ; *)
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
         br=branches; "end" -> CCases(loc,ty,ci,br) ] ]
@@ -332,53 +356,62 @@ GEXTEND Gram
 	  ctx @ bl
     | cl = LIST0 binder_let -> cl ] ]
   ;
+  binders_let_fixannot:
+    [ [ "{"; IDENT "struct"; id=name; "}" -> [], (Some id, CStructRec)
+    | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> [], (id, CWfRec rel)
+    | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> [], (id, CMeasureRec rel)
+    | b = binder_let; bl = binders_let_fixannot -> 
+	b :: fst bl, snd bl
+    | -> [], (None, CStructRec)
+    ] ]
+  ;
+
   binder_let:
     [ [ id=name ->
           LocalRawAssum ([id],Default Explicit,CHole (loc, None))
-      | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
+      | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
           LocalRawAssum (id::idl,Default Explicit,c)
-      | "("; id=name; ":"; c=lconstr; ")" -> 
+      | "("; id=name; ":"; c=lconstr; ")" ->
           LocalRawAssum ([id],Default Explicit,c)
-      | "`"; id=name; "`" ->
+      | "{"; id=name; "}" ->
           LocalRawAssum ([id],Default Implicit,CHole (loc, None))
-      | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
+      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
           LocalRawAssum (id::idl,Default Implicit,c)
-      | "`"; id=name; ":"; c=lconstr; "`" -> 
+      | "{"; id=name; ":"; c=lconstr; "}" ->
           LocalRawAssum ([id],Default Implicit,c)
-      | "`"; id=name; idl=LIST1 name; "`" -> 
+      | "{"; id=name; idl=LIST1 name; "}" ->
           LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
-      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
           LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
       | "["; tc = typeclass_constraint_binder; "]" -> tc
     ] ]
-(*     | b = delimited_binder_let -> b ] ] *)
   ;
   delimited_binder_let:
     [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
           LocalRawAssum (id::idl,Default Explicit,c)
       | "("; id=name; ":"; c=lconstr; ")" -> 
           LocalRawAssum ([id],Default Explicit,c)
-      | "`"; id=name; "`" ->
-          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
-      | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" -> 
-          LocalRawAssum (id::idl,Default Implicit,c)
-      | "`"; id=name; ":"; c=lconstr; "`" -> 
-          LocalRawAssum ([id],Default Implicit,c)
-      | "`"; id=name; idl=LIST1 name; "`" -> 
-          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
       | "("; id=name; ":="; c=lconstr; ")" ->
           LocalRawDef (id,c)
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
           LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
+      | "{"; id=name; "}" ->
+          LocalRawAssum ([id],Default Implicit,CHole (loc, None))
+      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> 
+          LocalRawAssum (id::idl,Default Implicit,c)
+      | "{"; id=name; ":"; c=lconstr; "}" -> 
+          LocalRawAssum ([id],Default Implicit,c)
+      | "{"; id=name; idl=LIST1 name; "}" -> 
+          LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
       | "["; tc = typeclass_constraint_binder; "]" -> tc
     ] ]
   ;
   binder:
     [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
       | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) 
-      | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c) 
+      | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) 
     ] ]
   ;
   typeclass_constraint_binder:
@@ -388,22 +421,22 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ id=identref ; cl = LIST0 typeclass_param -> 
-      (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | "?" ; id=identref ; cl = LIST0 typeclass_param -> 
-	(loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
-    | iid=identref ; ":" ; id=typeclass_name ; cl = LIST0 typeclass_param -> 
-	(fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
+    [ [ "!" ; qid=global ; cl = LIST0 typeclass_param -> 
+	(loc, Anonymous), Explicit, CApp (loc, (None, mkRefC qid), cl)
+    | iid=ident_eq ; qid=typeclass_name ; cl = LIST0 typeclass_param -> 
+	(loc, Name iid), (fst qid), CApp (loc, (None, mkRefC (snd qid)), cl)
+    | qid=global ; cl = LIST0 typeclass_param -> 
+	(loc, Anonymous), Implicit, CApp (loc, (None, mkRefC qid), cl)
     ] ]
   ;
   typeclass_name:
-    [ [ id=identref -> (Explicit, id)
-    | "?"; id = identref -> (Implicit, id)
+    [ [ id=global -> (Implicit, id)
+    | "!"; id=global -> (Explicit, id)
     ] ]
   ;
 
   typeclass_param: 
-    [ [ id = identref -> CRef (Libnames.Ident id), None
+    [ [ id = global -> CRef id, None
     | c = sort -> CSort (loc, c), None
     | id = lpar_id_coloneq; c=lconstr; ")" ->
 	(c,Some (loc,ExplByName id))
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 796636c0e0..32a2427ed1 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -105,7 +105,8 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+    [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> 
+          HintsResolve (List.map (fun x -> (n, x)) lc)
       | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
       | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5c34f2e884..3b67407311 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -256,17 +256,19 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = ident; bl = LIST1 binder_let;
-        annot = rec_annotation; ty = type_cstr; 
+    [ [ id = ident; b = binder_let;
+	bl = binders_let_fixannot;
+        ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
+	  let bl, annot = (b :: fst bl, snd bl) in
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
             match fst annot with
-                Some id ->
-                  (try Some (list_index0 (Name id) names)
+                Some (_, id) ->
+                  (try Some (list_index0 id names)
                    with Not_found ->  Util.user_err_loc
                      (loc,"Fixpoint",
-                      Pp.str "No argument named " ++ Nameops.pr_id id))
+                      Pp.str "No argument named " ++ Nameops.pr_name id))
               | None -> 
 		  (* If there is only one argument, it is the recursive one, 
 		     otherwise, we search the recursive index later *)
@@ -279,13 +281,6 @@ GEXTEND Gram
         def = lconstr; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
-  rec_annotation:
-    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
-      | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel) 
-      | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel) 
-      | ->  (None, CStructRec)
-      ] ]
-  ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
       | -> CHole (loc, None) ] ]
@@ -495,9 +490,9 @@ GEXTEND Gram
 	  VernacContext c
 
       | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
-	 is = typeclass_constraint ; props = typeclass_field_defs ->
+	 is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
-	     VernacInstance (sup, is, props)
+	     VernacInstance (sup, is, props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 68ddc19292..9976e07cc8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -436,6 +436,7 @@ module Constr =
     let binder_let = Gram.Entry.create "constr:binder_let"
     let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
+    let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
     let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
   end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d5cffd35bd..4fb9d03594 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -165,6 +165,7 @@ module Constr :
     val binder_let : local_binder Gram.Entry.e
     val delimited_binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
+    val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e
     val delimited_binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
   end
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0daccbba53..92d56e078d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -191,7 +191,10 @@ let pr_hints local db h pr_c pr_pat =
   let pph =
     match h with
     | HintsResolve l ->
-        str "Resolve " ++ prlist_with_sep sep pr_c l
+        str "Resolve " ++ prlist_with_sep sep 
+	  (fun (pri, c) -> pr_c c ++ 
+	    match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+	  l
     | HintsImmediate l ->
         str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
     | HintsUnfold l ->
@@ -703,7 +706,7 @@ let rec pr_vernac = function
 	  prlist_with_sep (fun () -> str";" ++ spc()) 
 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
 	
- | VernacInstance (sup, (instid, bk, cl), props) -> 
+ | VernacInstance (sup, (instid, bk, cl), props, pri) -> 
      hov 1 (
        str"Instance" ++ spc () ++ 
 	 pr_and_type_binders_arg sup ++