Merge remote-tracking branch 'github/pr/339' into v8.6

Was PR#339: Documenting type class options, typeclasses eauto

2 files changed, 32 insertions, 33 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 31ef3dfdd..b8da6b685 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -65,7 +65,8 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+	      * constant option) list;
   
   cl_strict : bool;
 
@@ -76,10 +77,9 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: global_reference;
-  is_pri: int option;
+  is_info: Vernacexpr.hint_info_expr;
   (* Sections where the instance should be redeclared,
-     -1 for discard, 0 for none, mutable to avoid redeclarations
-     when multiple rebuild_object happen. *)
+     -1 for discard, 0 for none. *)
   is_global: int;
   is_poly: bool;
   is_impl: global_reference;
@@ -89,15 +89,15 @@ type instances = (instance Refmap.t) Refmap.t
 
 let instance_impl is = is.is_impl
 
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
 
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
   let global =
     if glob then Lib.sections_depth ()
     else -1
   in
     { is_class = cl.cl_impl;
-      is_pri = pri ;
+      is_info = info ;
       is_global = global ;
       is_poly = poly;
       is_impl = impl }
@@ -274,7 +274,9 @@ let check_instance env sigma c =
       not (Evd.has_undefined evd)
   with e when CErrors.noncritical e -> false
 
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
   let _next_id = 
     let i = ref (-1) in 
@@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri =
 	   match b with 
 	   | None -> None
 	   | Some (Backward, _) -> None
-	   | Some (Forward, pri') ->
+	   | Some (Forward, info) ->
 	     let proj = Option.get proj in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
 	       if check && check_instance env sigma body then None
 	       else 
-		 let pri = 
-		   match pri, pri' with
+		 let newpri =
+		   match pri, info.hint_priority with
 		   | Some p, Some p' -> Some (p + p')
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, pri, body)) tc.cl_projs 
+		   Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
 	in
-	let declare_proj hints (cref, pri, body) =
+	let declare_proj hints (cref, info, body) =
 	  let path' = cref :: path in
 	  let ty = Retyping.get_type_of env sigma body in
 	  let rest = aux pri body ty path' in
-	    hints @ (path', pri, body) :: rest
+	    hints @ (path', info, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in
   let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1)
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
   add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) 
-    inst.is_pri poly;
+    inst.is_info poly;
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
     (is_local inst) pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
 let rebuild_instance (action, inst) =
   let () = match action with
@@ -404,26 +406,22 @@ let remove_instance i =
   Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
   remove_instance_hint i.is_impl
 
-let declare_instance pri local glob =
+let declare_instance info local glob =
   let ty = Global.type_of_global_unsafe glob in
+  let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr ty with
     | Some (rels, ((tc,_), args) as _cl) ->
-      add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(*       let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(*       let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* 	Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* 	Auto.add_hints local [typeclasses_db]  *)
-(* 	(Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+      add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
     | None -> ()
 
 let add_class cl =
   add_class cl;
   List.iter (fun (n, inst, body) ->
 	     match inst with
-	     | Some (Backward, pri) ->
+	     | Some (Backward, info) ->
 	       (match body with
 	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
-	       | Some b -> declare_instance pri false (ConstRef b))
+	       | Some b -> declare_instance (Some info) false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2530f5dfa..620bc367b 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,7 +32,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -50,7 +50,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> 
+val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic ->
   global_reference -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
@@ -71,7 +71,7 @@ val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr
   
 val instance_impl : instance -> global_reference
 
-val instance_priority : instance -> int option
+val hint_priority : instance -> int option
 
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
@@ -113,21 +113,22 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook : 
   (global_reference_or_constr -> global_reference list ->
-   bool (* local? *) -> int option -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
-  bool -> int option -> Decl_kinds.polymorphic -> unit
+  bool -> Vernacexpr.hint_info_expr -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t
 
-val declare_instance : int option -> bool -> global_reference -> unit
+val declare_instance : Vernacexpr.hint_info_expr option -> bool -> global_reference -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)
 
-val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (global_reference list * int option * constr) list
+val build_subclasses : check:bool -> env -> evar_map -> global_reference ->
+		       Vernacexpr.hint_info_expr ->
+		       (global_reference list * Vernacexpr.hint_info_expr * constr) list