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

5 files changed, 56 insertions, 26 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1f2253d4f3..32803742a0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -33,13 +33,27 @@ open Entries
 
 let hint_db = "typeclass_instances"
 
-let add_instance_hint inst = 
-  Auto.add_hints false [hint_db] 
-    (Vernacexpr.HintsResolve [CAppExpl (dummy_loc, (None, Ident (dummy_loc, inst)), [])])
-
-let declare_instance (_,id) =
-  add_instance_hint id
-
+let _ =
+  Typeclasses.register_add_instance_hint 
+    (fun inst pri ->
+      Auto.add_hints false [hint_db] 
+	(Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, inst), [])]))
+
+let declare_instance_constant con =
+  let instance = Typeops.type_of_constant (Global.env ()) con in
+  let _, r = decompose_prod_assum instance in
+    match class_of_constr r with
+      | Some tc -> add_instance { is_class = tc ; is_pri = None; is_impl = con }
+      | None -> error "Constant does not build instances of a declared type class"
+
+let declare_instance idl =
+  let con = 
+    try (match global (Ident idl) with
+      | ConstRef x -> x
+      | _ -> raise Not_found)
+    with _ -> error "Instance definition not found"
+  in declare_instance_constant con
+	  
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 (* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -110,7 +124,8 @@ let declare_implicit_proj c proj imps sub =
       aux 1 [] ctx
   in 
   let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
-    if sub then add_instance_hint (id_of_label (con_label proj));
+    if sub then 
+      declare_instance_constant proj;
     Impargs.declare_manual_implicits true (ConstRef proj) true expls
       
 let declare_implicits impls subs cl =
@@ -263,7 +278,7 @@ let new_class id par ar sup props =
   let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
   let kn = 
     let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-    let params, subst = rel_of_named_context [] ctx_params (*  @ ctx_super @ ctx_super_ctx) *) in
+    let params, subst = rel_of_named_context [] ctx_params in
     let fields, _ = rel_of_named_context subst ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
       declare_structure env0 (snd id) idb params arity fields
@@ -362,7 +377,7 @@ open Pp
 
 let ($$) g f = fun x -> g (f x)
 
-let new_instance ctx (instid, bk, cl) props =
+let new_instance ctx (instid, bk, cl) props pri hook =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
@@ -472,13 +487,13 @@ let new_instance ctx (instid, bk, cl) props =
   let hook cst = 
     let inst = 
       { is_class = k;
-	is_name = id;
+	is_pri = pri;
 	is_impl = cst;
       }
     in
-      add_instance_hint id;
       Impargs.declare_manual_implicits false (ConstRef cst) false imps;
-      Typeclasses.add_instance inst
+      Typeclasses.add_instance inst;
+      hook cst
   in
   let evm = Evd.evars_of (undefined_evars !isevars) in
     if evm = Evd.empty then
@@ -518,7 +533,7 @@ let solve_by_tac env evd evar evi t =
 	else evd, false
     else evd, false
 
-let context l =
+let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let avoid = Termops.ids_of_context env in
@@ -529,8 +544,21 @@ let context l =
   let sigma = Evd.evars_of !isevars in
   let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
     List.iter (function (id,_,t) -> 
-      Command.declare_one_assumption false (Local (* global *), Definitional) t
-	[] false (* inline *) (dummy_loc, id))
+      if Lib.is_modtype () then 
+	let cst = Declare.declare_internal_constant id
+	  (ParameterEntry (t,false), IsAssumption Logical)
+	in
+	  match class_of_constr t with
+	    | Some tc ->
+		(add_instance { is_class = tc ; is_pri = None; is_impl = cst });
+		hook (ConstRef cst)
+	    | None -> ()
+      else
+	(Command.declare_one_assumption false (Local (* global *), Definitional) t
+	    [] false (* inline *) (dummy_loc, id);
+	 match class_of_constr t with
+	     None -> ()
+	   | Some tc -> hook (VarRef id)))
       (List.rev fullctx)
 
 open Libobject
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index d8f326698f..248ed8c956 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -43,11 +43,11 @@ val new_instance :
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  int option ->
+  (constant -> unit) ->
   identifier
-
-val context : typeclass_context -> unit
-
-val add_instance_hint : identifier -> unit
+    
+val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
 
 val declare_instance : identifier located -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 73e4e42f73..b94dffe1a0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -138,7 +138,8 @@ let declare_projections indsp coers fields =
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = Termops.named_hd (Global.env()) r Anonymous in
+  let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in
+    (* Termops.named_hd (Global.env()) r Anonymous  *)
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 770cc5ccf4..45a0f834ba 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -533,8 +533,8 @@ let vernac_identity_coercion stre id qids qidt =
 let vernac_class id par ar sup props =
   Classes.new_class id par ar sup props
 
-let vernac_instance sup inst props =
-  ignore(Classes.new_instance sup inst props)
+let vernac_instance sup inst props pri =
+  ignore(Classes.new_instance sup inst props pri (fun _ -> ()))
 
 let vernac_context l =
   Classes.context l
@@ -1222,7 +1222,7 @@ let interp c = match c with
   (* Type classes *)
   | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
 
-  | VernacInstance (sup, inst, props) -> vernac_instance sup inst props
+  | VernacInstance (sup, inst, props, pri) -> vernac_instance 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 a25cd09e74..ee0c42aa26 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -112,7 +112,7 @@ type comment =
   | CommentInt of int
 
 type hints =
-  | HintsResolve of constr_expr list
+  | HintsResolve of (int option * constr_expr) list
   | HintsImmediate of constr_expr list
   | HintsUnfold of reference list
   | HintsConstructors of reference list
@@ -235,7 +235,8 @@ type vernac_expr =
   | VernacInstance of
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
-	(lident * lident list * constr_expr) list (* props *)
+	(lident * lident list * constr_expr) list * (* props *)
+	int option (* Priority *)
 
   | VernacContext of typeclass_context