New API to get instance priority

Author: FissoreD

Changelog.md

@@ -12,6 +12,7 @@
 - Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore
 - New `coq.ltac.fresh-id` to generate fresh names in the proof context
 - New `@no-tc!` attribute supported by `coq.ltac.call-ltac1`
+- New `coq.TC.get-inst-prio` returns the `tc-priority` of an instance
 
 ### Apps 
 - New `tc` app providing an implementation of a type class solver written in elpi.

apps/tc/elpi/tc_aux.elpi

@@ -5,6 +5,8 @@
 % cannot be compiled
 
 % returns the TC from the type of an instance
+% TODO: This gould be replaced with an api 
+% coq.TC.get-class-of-inst i:gref, o:gref
 pred get-TC-of-inst-type i:term, o:gref.
 get-TC-of-inst-type (prod _ _ A) GR:-
   pi x\ get-TC-of-inst-type (A x) GR.
@@ -93,23 +95,20 @@ make-tc _IsHead Ty Inst Hyp Clause :-
       (Hyp = [Hd]) (Clause = (Q :- Hd)) 
       (Clause = (Q :- Hyp)).
 
+pred unwrap-prio i:tc-priority, o:int.
+unwrap-prio (tc-priority-given Prio) Prio.
+unwrap-prio (tc-priority-computed Prio) Prio.
+
 % returns the priority of an instance from the gref of an instance
 pred get-inst-prio i:gref, o:int.
-get-inst-prio InstGr Prio :-
-  coq.env.typeof InstGr InstTy,
-  get-TC-of-inst-type InstTy TC,
-  find-opt {coq.TC.db-for TC} 
-    (x\ tc-instance InstGr (tc-priority-given Prio) = x ;
-        tc-instance InstGr (tc-priority-computed Prio) = x)
-      (some _), !.
-get-inst-prio _ 0.
-
-% TODO: @FissoreD improve this method complexity
+get-inst-prio InstGR Prio :-
+  coq.env.typeof InstGR InstTy,
+  get-TC-of-inst-type InstTy ClassGR,
+  unwrap-prio {coq.TC.get-inst-prio ClassGR InstGR} Prio.
+
 pred get-full-path i:gref, o:string.
-% :if "get-full-path"
 get-full-path Gr Res' :-
   coq.gref->string Gr Path,
   coq.env.current-section-path SectionPath,
   std.fold SectionPath "" (e\acc\r\ r is acc ^ "." ^ e) Res,
   Res' is Res ^ Path.
-% get-full-path _ _.

coq-builtin.elpi

@@ -1154,6 +1154,10 @@ external pred coq.TC.db-tc o:list gref.
 % Instances are in their precedence order.
 external pred coq.TC.db-for i:gref, o:list tc-instance.
 
+% [coq.TC.get-inst-prio ClassGR InstGR InstPrio] reads the priority of an
+% instance
+external pred coq.TC.get-inst-prio i:gref, i:gref, o:tc-priority.
+
 % [coq.TC.class? GR] checks if GR is a class
 external pred coq.TC.class? i:gref.
 

src/coq_elpi_builtins.ml

@@ -511,7 +511,31 @@ let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority =
     let hyps = nb_hyp sigma' cty in
     Computed (hyps + nmiss)
 
-let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instance list = 
+(* TODO: this algorithm is quite inefficient since we have not yet the
+         possibility to get the implementation of an instance from its gref in
+         coq. Currently we have to get all the instances of the tc and the find
+         its implementation.  
+  NOTE: if we have coq's API to retrieve this implementation from the GlobRef of
+        the instance the parameter tc will be useless
+*)
+let get_instance (env: Environ.env) (sigma: Evd.evar_map) (tc : GlobRef.t) (instance : GlobRef.t) : type_class_instance =
+  let inst_of_tc = (* contains all the instances of a type class *)
+    Typeclasses.instances_exn env sigma tc |>
+    List.fold_left (fun m i -> GlobRef.Map.add i.Typeclasses.is_impl i m) GlobRef.Map.empty in
+  let instances_grefs2istance inst_gr : type_class_instance = 
+    let open Typeclasses in 
+    let user_hint_prio = 
+      (* Note: in general we deal with an instance I of a type class. Here we
+               look if the user has given a priority to I. However, external
+               hints are not in the inst_of_tc (the Not_found exception) *)
+      try (GlobRef.Map.find inst_gr inst_of_tc).is_info.hint_priority 
+      with Not_found -> None in
+    let priority = get_instance_prio inst_gr env sigma user_hint_prio in 
+    { implementation = inst_gr; priority } 
+  in
+  instances_grefs2istance instance
+
+let get_instances (env: Environ.env) (sigma: Evd.evar_map) tc : type_class_instance list = 
   let hint_db = Hints.searchtable_map "typeclass_instances" in 
   let secvars : Names.Id.Pred.t = Names.Id.Pred.full in 
   let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in 
@@ -523,8 +547,6 @@ let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instan
     | Give_exact a -> Some a
     | Res_pf_THEN_trivial_fail e -> Some e
     | Unfold_nth e -> None) hint_asts in 
-  let sigma, _ = 
-    let env = Global.env () in Evd.(from_env env, env) in 
   let constrs = List.map (fun a -> Hints.hint_as_term a |> snd) hints in 
   (* Printer.pr_global tc |> Pp.string_of_ppcmds |> Printf.printf "%s\n"; *)
   let instances_grefs = List.filter_map (fun e ->
@@ -533,21 +555,7 @@ let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instan
     | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a)
     | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a)
     | _ -> None) constrs in 
-  let inst_of_tc = (* contains all the instances of a type class *)
-    Typeclasses.instances_exn env emap tc |>
-    List.fold_left (fun m i -> GlobRef.Map.add i.Typeclasses.is_impl i m) GlobRef.Map.empty in
-  let instances_grefs2istance inst_gr : type_class_instance = 
-    let open Typeclasses in 
-    let user_hint_prio = 
-      (* Note: in general we deal with an instance I of a type class. Here we look if 
-               the user has given a priority to I. However, external hints are 
-               not in the inst_of_tc (the Not_found exception)*)
-      try (GlobRef.Map.find inst_gr inst_of_tc).is_info.hint_priority 
-      with Not_found -> None in
-    let priority = get_instance_prio inst_gr env sigma user_hint_prio in 
-    { implementation = inst_gr; priority } 
-  in
-  List.map instances_grefs2istance instances_grefs
+  List.map (get_instance env sigma tc) instances_grefs
 
 type scope = ExecutionSite | CurrentModule | Library
 
@@ -2836,6 +2844,16 @@ Supported attributes:
   (fun gr _ ~depth { env } _ state -> !: (get_instances env (get_sigma state) gr))),
   DocAbove);
 
+  MLCode(Pred("coq.TC.get-inst-prio", 
+    In(gref, "ClassGR",
+    In(gref, "InstGR",
+    Out(tc_priority, "InstPrio",
+    Read (global, "reads the priority of an instance")))),
+    (fun class_gr inst_gr _ ~depth { env } _ state -> 
+      let {priority} = get_instance env (get_sigma state) class_gr inst_gr in 
+      !: priority)),
+  DocAbove);
+
   MLCode(Pred("coq.TC.class?",
     In(gref, "GR",
     Easy "checks if GR is a class"),