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

3 files changed, 46 insertions, 22 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 399264859..ee5acffd9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -157,7 +157,7 @@ sig
     rawconstr -> unsafe_type_judgment
 
   val pretype_gen :
-    evar_defs ref -> env -> 
+    evar_defs ref -> env ->
     var_map * (identifier * identifier option) list ->
     typing_constraint -> rawconstr -> constr
 
@@ -667,11 +667,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let evd = nf_evar_defs evd in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
-    let c' = nf_evar (evars_of evd) c' in
       evdref := evd;
-      c'
+      nf_evar (evars_of evd) c'
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7a95f9c35..c18b0e045 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Libnames
 open Decl_kinds
 open Term
 open Sign
@@ -48,12 +49,8 @@ type typeclasses = (identifier, typeclass) Gmap.t
 
 type instance = {
   is_class: typeclass;
-  is_name: identifier; (* Name of the instance *)
-(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
-(*   is_super: named_context; (\* The corresponding superclasses *\) *)
-(*   is_defs: named_context; (\* Context of the definitions, instanciated *\) *)
+  is_pri: int option;
   is_impl: constant; 
-(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
 }
 
 type instances = (identifier, instance list) Gmap.t
@@ -81,19 +78,20 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_module = true;
+      Summary.survive_module = false;
       Summary.survive_section = true }
 
 let gmap_merge old ne =
   Gmap.fold (fun k v acc -> Gmap.add k v acc) ne old
 
-let gmap_list_merge old ne =
+let gmap_list_merge old upd ne =
   let ne = 
     Gmap.fold (fun k v acc -> 
       let oldv = try Gmap.find k old with Not_found -> [] in
       let v' = 
 	List.fold_left (fun acc x -> 
-	  if not (List.exists (fun y -> y.is_name = x.is_name) v) then x :: acc else acc)
+	  if not (List.exists (fun y -> y.is_impl = x.is_impl) v) then
+	    (x :: acc) else acc)
 	v oldv
       in Gmap.add k v' acc)
       ne Gmap.empty
@@ -102,15 +100,24 @@ let gmap_list_merge old ne =
       let newv = try Gmap.find k ne with Not_found -> [] in
       let v' = 
 	List.fold_left (fun acc x -> 
-	  if not (List.exists (fun y -> y.is_name = x.is_name) acc) then x :: acc else acc)
+	  if not (List.exists (fun y -> y.is_impl = x.is_impl) acc) then x :: acc else acc)
 	  newv v
       in Gmap.add k v' acc)
       old ne
 
+let add_instance_hint_ref = ref (fun id pri -> assert false)
+let register_add_instance_hint = (:=) add_instance_hint_ref
+let add_instance_hint id = !add_instance_hint_ref id
+
+let qualid_of_con c = 
+  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+
 let cache (_, (cl, m, inst)) =
   classes := gmap_merge !classes cl;
   methods := gmap_merge !methods m;
-  instances := gmap_list_merge !instances inst
+  instances := gmap_list_merge !instances 
+    (fun i -> add_instance_hint (qualid_of_con i.is_impl))
+    inst
 
 open Libobject
 
@@ -137,8 +144,11 @@ let subst (_,subst,(cl,m,inst)) =
   in
   let subst_inst classes insts =
     List.map (fun is -> 
-      { is with is_class = Gmap.find is.is_class.cl_name classes; 
-	is_impl = do_subst_con is.is_impl }) insts
+      let is' = 
+	{ is_class = Gmap.find is.is_class.cl_name classes; 
+	  is_pri = is.is_pri;
+	  is_impl = do_subst_con is.is_impl }
+      in if is' = is then is else is') insts
   in
   let classes = Gmap.map subst_class cl in
   let instances = Gmap.map (subst_inst classes) inst in
@@ -149,8 +159,9 @@ let discharge (_,(cl,m,inst)) =
     { cl with cl_impl = Lib.discharge_inductive cl.cl_impl }
   in
   let subst_inst classes insts =
-    List.map (fun is -> { is with is_impl = Lib.discharge_con is.is_impl;
-      is_class = Gmap.find is.is_class.cl_name classes; }) insts
+    List.map (fun is -> { is_impl = Lib.discharge_con is.is_impl;
+			  is_pri = is.is_pri;
+			  is_class = Gmap.find is.is_class.cl_name classes; }) insts
   in
   let classes = Gmap.map subst_class cl in
   let instances = Gmap.map (subst_inst classes) inst in
@@ -202,8 +213,12 @@ let instances_of c =
   try Gmap.find c.cl_name !instances with Not_found -> []
 
 let add_instance i =
-  instances := gmapl_add i.is_class.cl_name i !instances;
-  update ()
+  try
+    let cl = Gmap.find i.is_class.cl_name !classes in
+      instances := gmapl_add cl.cl_name { i with is_class = cl } !instances;
+      add_instance_hint (qualid_of_con i.is_impl) i.is_pri;
+      update ()
+  with Not_found -> unbound_class (Global.env ()) (dummy_loc, i.is_class.cl_name)
 
 open Libnames
       
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f231c7406..c06006ad0 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Libnames
 open Decl_kinds
 open Term
 open Sign
@@ -41,8 +42,8 @@ type typeclass = {
 
 type instance = {
   is_class: typeclass;
-  is_name: identifier; (* Name of the instance *)
-  is_impl: constant; 
+  is_pri : int option;
+  is_impl: constant;
 }
   
 val instances : Libnames.reference -> instance list
@@ -50,6 +51,9 @@ val typeclasses : unit -> typeclass list
 val add_class : typeclass -> unit
 val add_instance : instance -> unit
 
+val register_add_instance_hint : (reference -> int option -> unit) -> unit
+val add_instance_hint : reference -> int option -> unit
+
 val class_info : identifier -> typeclass (* raises Not_found *)
 val class_of_inductive : inductive -> typeclass (* raises Not_found *)
 
@@ -75,3 +79,10 @@ val substitution_of_named_context :
 val nf_substitution : evar_map -> substitution -> substitution
 
 val is_implicit_arg : hole_kind -> bool
+
+
+val subst :  'a * Mod_subst.substitution *
+    ((Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t) ->
+    (Names.identifier, typeclass) Gmap.t * 'b * ('c, instance list) Gmap.t
+
+val qualid_of_con : Names.constant -> Libnames.reference