Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.

5 files changed, 34 insertions, 25 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d6a6162f9..1f13ab637 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -46,25 +46,32 @@ let set_typeclass_transparency c local b =
     
 let _ =
   Hook.set Typeclasses.add_instance_hint_hook
-    (fun inst path local pri poly ->
+    (fun inst path local info poly ->
      let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
-      Flags.silently (fun () ->
+     let info =
+       Vernacexpr.{ info with hint_pattern =
+		   Option.map
+		   (Constrintern.intern_constr_pattern (Global.env())) info.hint_pattern } in
+     Flags.silently (fun () ->
 	Hints.add_hints local [typeclasses_db]
 	  (Hints.HintsResolveEntry
-	     [pri, poly, false, Hints.PathHints path, inst'])) ());
+	     [info, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
-        
+
+open Vernacexpr
+
 (** TODO: add subinstances *)
-let existing_instance glob g pri =
+let existing_instance glob g info =
   let c = global g in
+  let info = Option.default Hints.empty_hint_info info in
   let instance = Global.type_of_global_unsafe c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob 
+      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
   (*FIXME*) (Flags.use_polymorphic_flag ()) c)
       | None -> user_err_loc (loc_of_reference g, "declare_instance",
 			     Pp.str "Constant does not build instances of a declared type class.")
@@ -98,12 +105,12 @@ let id_of_class cl =
 
 open Pp
 
-let instance_hook k pri global imps ?hook cst =
+let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
-  Typeclasses.declare_instance pri (not global) cst;
+  Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
@@ -118,7 +125,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
     Universes.register_universe_binders (ConstRef kn) pl;
-    instance_hook k pri global imps ?hook (ConstRef kn);
+    instance_hook k info global imps ?hook (ConstRef kn);
     id
 
 let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
@@ -130,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
   let evars = ref (Evd.from_ctx uctx) in
   let tclass, ids =
     match bk with
-    | Implicit ->
+    | Decl_kinds.Implicit ->
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
 	  (fun avoid (clname, _) ->
 	    match clname with
@@ -299,7 +306,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
+		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
 	      in
 	      let obls, constr, typ =
 		match term with 
@@ -378,7 +385,7 @@ let context poly l =
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
-	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+	    add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
 			    poly (ConstRef cst));
             status
 	    (* declare_subclasses (ConstRef cst) cl *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7beb873e6..d2cb788ea 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -20,12 +20,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> int option -> unit
-(** globality, reference, priority *)
+val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+(** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  int option -> (** priority *)
+  Vernacexpr.hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
@@ -48,7 +48,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
-  int option ->
+  Vernacexpr.hint_info_expr ->
   Id.t
 
 (** Setting opacity *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9c4d41ea5..63564fba1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -565,8 +565,9 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
       typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
   let gr = match kind with
-    | Class def ->
-	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+  | Class def ->
+     let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
+     let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b09425563..c50e57786 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,8 @@ val declare_structure :
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
+  plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4de1d9595..973f73ef6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -841,9 +841,9 @@ let vernac_instance abst locality poly sup inst props pri =
 let vernac_context poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_declare_instances locality ids pri =
+let vernac_declare_instances locality insts =
   let glob = not (make_section_locality locality) in
-  List.iter (fun id -> Classes.existing_instance glob id pri) ids
+  List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
 
 let vernac_declare_class id =
   Record.declare_existing_class (Nametab.global id)
@@ -1989,10 +1989,10 @@ let interp ?proof ~loc locality poly c =
       vernac_identity_coercion locality poly local id s t
 
   (* Type classes *)
-  | VernacInstance (abst, sup, inst, props, pri) ->
-      vernac_instance abst locality poly sup inst props pri
+  | VernacInstance (abst, sup, inst, props, info) ->
+      vernac_instance abst locality poly sup inst props info
   | VernacContext sup -> vernac_context poly sup
-  | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
+  | VernacDeclareInstances insts -> vernac_declare_instances locality insts
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)