From 486609ffa656bdffc3272a9bc2b08dc893ef69de Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 15 Nov 2023 10:33:57 +0100
Subject: [PATCH 1/9] bug correction: get_instances of a hint rule has priority
 none

---
 apps/tc/elpi/create_tc_predicate.elpi | 11 ++++++-----
 apps/tc/elpi/tc_aux.elpi              |  5 ++++-
 apps/tc/theories/db.v                 |  3 +++
 apps/tc/theories/tc.v                 |  2 +-
 elpi-builtin.elpi                     |  4 ++++
 src/coq_elpi_builtins.ml              | 20 +++++++++++++-------
 6 files changed, 31 insertions(+), 14 deletions(-)

diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index 77ef64d7f..8984a9b05 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -15,13 +15,14 @@ coq-mode->elpi mode-input (pr in "term").
 coq-mode->elpi mode-output (pr out "term").
 
 pred modes-of-class i:gref, o:list (pair argument_mode string).
-modes-of-class ClassGr Modes :- 
-  coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
+modes-of-class ClassGR Modes :- 
+  not (is-option-active {oTC-modes}),
+  coq.hints.modes ClassGR "typeclass_instances" CoqModesList,
   not (CoqModesList = []),
-  std.assert! (CoqModesList = [HintModesFst]) "At the moment we only allow TC with one Hint Mode",
+  std.assert! (CoqModesList = [HintModesFst]) {calc ("At the moment we only allow TC with one Hint Mode (cause by class" ^ {coq.gref->string ClassGR} ^ ")")},
   std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
-modes-of-class ClassGr Modes :- 
-  coq.env.typeof ClassGr ClassTy,
+modes-of-class ClassGR Modes :- 
+  coq.env.typeof ClassGR ClassTy,
   N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
   list-init N (x\r\ r = (pr out "term")) Modes.
 
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 3cb72af47..84bfd64ac 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -72,7 +72,10 @@ gref->pred-name Gr S :-
     (coq.gref->path Gr [Hd | Tl], 
       std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 
       Path is Path' ^ ".tc-"),
-  S is "tc-" ^ Path ^ {coq.gref->id Gr}.
+  % CAVEAT : Non-ascii caractars can't be part of a pred
+  %          name, we replace ö with o
+  rex.replace "ö" "o" {coq.gref->id Gr} GrStr,
+  S is "tc-" ^ Path ^ GrStr.
 
 pred no-backtrack i:list prop, o:list prop. 
 no-backtrack [] [].
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index a51fd422c..cf63cb255 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -26,6 +26,9 @@ Elpi Db tc_options.db lp:{{
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].
 
+  pred oTC-modes o:list string. 
+  oTC-modes ["TC", "Disable", "Modes"].
+
   pred is-option-active i:list string.
   is-option-active Opt :- 
     coq.option.get Opt (coq.option.bool tt).
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 65f422da9..6ca03ee33 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -47,7 +47,7 @@ Elpi Query lp:{{
   sigma Options\ 
     Options = [oTC-ignore-eta-reduction, oTC-resolution-time, 
       oTC-clauseNameShortName, oTC-time-refine, oTC-debug, 
-      oTC-use-pattern-fragment-compiler],
+      oTC-use-pattern-fragment-compiler, oTC-modes],
     std.forall Options (x\ sigma Args\ x Args, 
       coq.option.add Args (coq.option.bool ff) ff).
 }}.
diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index 4c6705dd6..0c1dd7f4d 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -537,6 +537,10 @@ pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
 fold [] A _ A.
 fold [X|XS] A F R :- F X A A1, fold XS A1 F R.
 
+pred fold-right i:list B, i:A, i:(B -> A -> A -> prop), o:A.
+fold-right [] A _ A.
+fold-right [X|XS] A F R :- fold-right XS A F A', F X A' R.
+
 pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
 fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
 fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 324203a49..de5ffe7ca 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -485,8 +485,8 @@ let tc_instance = let open Conv in let open API.AlgebraicData in declare {
       M (fun ~ok ~ko { implementation; priority } -> ok implementation priority));
 ]} |> CConv.(!<)
 
-let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : tc_priority =
-  match info.hint_priority with
+let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority =
+  match hint_priority with
   | Some p -> UserGiven p
   | None -> 
     let rec nb_hyp sigma c = match EConstr.kind sigma c with
@@ -533,14 +533,20 @@ 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 =
+  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 x = 
+  let instances_grefs2istance inst_gr : type_class_instance = 
     let open Typeclasses in 
-    let inst = GlobRef.Map.find x inst_of_tc in
-    let priority = get_instance_prio x env sigma inst.is_info in 
-    { implementation = x; priority } 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
 
 type scope = ExecutionSite | CurrentModule | Library

From cbdb2067fc5fc6e40910ebdd5fee21d2cb7aec3b Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 15 Nov 2023 10:52:21 +0100
Subject: [PATCH 2/9] warning if more than one mode for a class

---
 apps/tc/elpi/create_tc_predicate.elpi | 8 ++++++--
 apps/tc/theories/db.v                 | 3 ---
 apps/tc/theories/tc.v                 | 2 +-
 3 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index 8984a9b05..53dd00a5a 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -14,12 +14,16 @@ coq-mode->elpi mode-ground (pr in "term"). % approximation
 coq-mode->elpi mode-input (pr in "term").
 coq-mode->elpi mode-output (pr out "term").
 
+% Here we build the elpi modes a class CL. If CL has either zero or more than
+% one mode, then we consider all its parameter to be in output mode. If the
+% class has exactly one mode, then it is considered for the signature of the
+% predicate for CL 
 pred modes-of-class i:gref, o:list (pair argument_mode string).
 modes-of-class ClassGR Modes :- 
-  not (is-option-active {oTC-modes}),
   coq.hints.modes ClassGR "typeclass_instances" CoqModesList,
   not (CoqModesList = []),
-  std.assert! (CoqModesList = [HintModesFst]) {calc ("At the moment we only allow TC with one Hint Mode (cause by class" ^ {coq.gref->string ClassGR} ^ ")")},
+  not (CoqModesList = [_,_|_], coq.warning "TC.Modes" "At the moment we only allow TC with at most 1 hint Mode (caused by class" {coq.gref->string ClassGR} ")"),
+  CoqModesList = [HintModesFst],
   std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
 modes-of-class ClassGR Modes :- 
   coq.env.typeof ClassGR ClassTy,
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index cf63cb255..a51fd422c 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -26,9 +26,6 @@ Elpi Db tc_options.db lp:{{
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].
 
-  pred oTC-modes o:list string. 
-  oTC-modes ["TC", "Disable", "Modes"].
-
   pred is-option-active i:list string.
   is-option-active Opt :- 
     coq.option.get Opt (coq.option.bool tt).
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 6ca03ee33..65f422da9 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -47,7 +47,7 @@ Elpi Query lp:{{
   sigma Options\ 
     Options = [oTC-ignore-eta-reduction, oTC-resolution-time, 
       oTC-clauseNameShortName, oTC-time-refine, oTC-debug, 
-      oTC-use-pattern-fragment-compiler, oTC-modes],
+      oTC-use-pattern-fragment-compiler],
     std.forall Options (x\ sigma Args\ x Args, 
       coq.option.add Args (coq.option.bool ff) ff).
 }}.

From ebf039fb2757a2a99df7530f7b7ae6b46220abaf Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 15 Nov 2023 11:30:17 +0100
Subject: [PATCH 3/9] New API to get instance priority

---
 Changelog.md             |  1 +
 apps/tc/elpi/tc_aux.elpi | 23 ++++++++---------
 coq-builtin.elpi         |  4 +++
 src/coq_elpi_builtins.ml | 54 ++++++++++++++++++++++++++--------------
 4 files changed, 52 insertions(+), 30 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index e1c8c652f..f77579134 100644
--- a/Changelog.md
+++ b/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.
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 84bfd64ac..24b952d79 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/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 _ _.
\ No newline at end of file
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 7e2efa79f..2e9741208 100644
--- a/coq-builtin.elpi
+++ b/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.
 
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index de5ffe7ca..cac35f766 100644
--- a/src/coq_elpi_builtins.ml
+++ b/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"),

From 873e45eec01d6ca8f9bb321c6c0ed169834f95af Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sat, 25 Nov 2023 15:57:07 +0100
Subject: [PATCH 4/9] refactor option names

---
 apps/tc/elpi/solver.elpi        | 39 ++++++++++++++++++++-------------
 apps/tc/theories/add_commands.v |  7 +++---
 apps/tc/theories/db.v           | 23 ++++++++++++++-----
 apps/tc/theories/tc.v           |  4 +---
 4 files changed, 47 insertions(+), 26 deletions(-)

diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 8aeb3c19e..ef3abc101 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -1,8 +1,16 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+pred time-solve i:prop.
+time-solve P :-
+  std.time P Time,
+  if (is-option-active {oTC-time}) (coq.say "[TC] Total resolution time is:" Time) true.
+
 msolve L N :- !,
-  coq.ltac.all (coq.ltac.open solve) {std.rev L} N.
+  time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
+
+solve A L :- time-solve (solve-aux A L).
+
 
 pred build-context-clauses i:list prop, o:list prop.
 % Add the section's definition to the given context
@@ -20,48 +28,49 @@ tc-recursive-search Ty Sol :-
   std.time (coq.safe-dest-app Ty (global TC) TL',
     std.append TL' [Sol] TL,
     coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
-  if (is-option-active {oTC-resolution-time}) (coq.say "Instance search" Time) true.
+  if (is-option-active {oTC-time-instance-search}) (coq.say "[TC] Instance search time is:" Time) true.
 
 :if "solve-print-goal"
 solve (goal Ctx _ Ty _ _) _ :-
   coq.say "Ctx" Ctx "Ty" Ty, fail.
 
-% solve (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
+pred solve-aux i:goal, o:list sealed-goal.
+% solve-aux (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
 %   @pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
 %     if (Sol x = app [HD, x]) (S = HD) (S = fun N Ty Sol).
-% solve (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
+% solve-aux (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
 %   % intros_if_needed Prod C [] 
 %   (@pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
 %     coq.safe-dest-app (Sol x) Hd (Args x)),
 %     if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs)
 %     (coq.mk-app Hd NewArgs Out, refine Out G GL) (
 %       % coq.say "Not eta" (Sol x) x (fun N Ty Sol),
 %       XX = (fun N Ty Sol)).
-% solve (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
+% solve-aux (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
 %   declare-evar C T P S',
 %   G' = (goal C T P S' A),
 %   refine (fun N _ _) G' GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 _,
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 _,
 %   refine S' G GL.
-solve (goal C _ (prod N Ty F) _ _ as G) GL :- !,
+solve-aux (goal C _ (prod N Ty F) _ _ as G) GL :- !,
   (@pi-decl N Ty x\
     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-    solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
+    solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
     if (pi x\ 
       % also check the head does not contain x
       coq.safe-dest-app (Sol x) Hd (Args x), 
       last-no-error (Args x) x, 
       std.drop-last 1 (Args x) NewArgs)
     (coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1),
-    coq.ltac.all (coq.ltac.open solve) GL1 GL.
-% solve (goal _ _ (prod N _ _) _ _ as G) GL :- !,
+    coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+% solve-aux (goal _ _ (prod N _ _) _ _ as G) GL :- !,
 %   refine (fun N _ _) G GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 GL.
-solve (goal Ctx _ Ty Sol _ as G) GL :-
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
   var Sol,
   build-context-clauses Ctx Clauses,
   % @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1,
@@ -74,7 +83,7 @@ solve (goal Ctx _ Ty Sol _ as G) GL :-
       if (is-option-active {oTC-ignore-eta-reduction}) 
         (Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
       std.time (refine Proof' G GL) Refine-Time, 
-      if (is-option-active {oTC-time-refine}) (coq.say "Refine Time" Refine-Time) true;
+      if (is-option-active {oTC-time-refine}) (coq.say "[TC] Refine time is:" Refine-Time) true;
       coq.error "illtyped solution:" {coq.term->string Proof}
     ) 
     (GL = [seal G]).
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index ac5bd8629..56d271504 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -43,9 +43,10 @@ Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
-  main _ :-
-    coq.TC.db-tc TC,
-    std.forall TC (add-class-gr classic).
+  % Ignore is the list of classes we do not want to add
+  main IgnoreStr :-
+    std.map IgnoreStr (x\r\ sigma S\ str S = x, coq.locate S r) IgnoreGR,
+    std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (add-class-gr classic x)).
 }}.
 Elpi Typecheck.
 
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index a51fd422c..a87afc40b 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -11,14 +11,20 @@ Elpi Db tc_options.db lp:{{
   pred oTC-ignore-eta-reduction o:list string. 
   oTC-ignore-eta-reduction ["TC", "IgnoreEtaReduction"].
 
-  pred oTC-resolution-time o:list string. 
-  oTC-resolution-time ["TC", "ResolutionTime"].
+  % Time taken by only instance search (we time tc-recursive-search) 
+  pred oTC-time-instance-search o:list string. 
+  oTC-time-instance-search ["TC", "Time", "Instance", "Search"].
 
-  pred oTC-clauseNameShortName o:list string. 
-  oTC-clauseNameShortName ["TC", "NameShortPath"].
+  % Time taken by the whole search in tc
+  pred oTC-time o:list string.
+  oTC-time ["TC", "Time"].
 
+  % Time taken to refine the solution
   pred oTC-time-refine o:list string. 
-  oTC-time-refine ["TC", "TimeRefine"].
+  oTC-time-refine ["TC", "Time", "Refine"].
+
+  pred oTC-clauseNameShortName o:list string. 
+  oTC-clauseNameShortName ["TC", "NameShortPath"].
 
   pred oTC-debug o:list string.
   oTC-debug ["TC", "Debug"].
@@ -26,6 +32,13 @@ Elpi Db tc_options.db lp:{{
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].
 
+  pred all-options o:list ((list string) -> prop).
+  all-options [
+    oTC-ignore-eta-reduction, oTC-time-refine, oTC-time,
+    oTC-clauseNameShortName, oTC-time-instance-search, oTC-debug, 
+    oTC-use-pattern-fragment-compiler
+  ].
+
   pred is-option-active i:list string.
   is-option-active Opt :- 
     coq.option.get Opt (coq.option.bool tt).
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 65f422da9..94280b4a3 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -45,9 +45,7 @@ Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
-    Options = [oTC-ignore-eta-reduction, oTC-resolution-time, 
-      oTC-clauseNameShortName, oTC-time-refine, oTC-debug, 
-      oTC-use-pattern-fragment-compiler],
+    all-options Options,
     std.forall Options (x\ sigma Args\ x Args, 
       coq.option.add Args (coq.option.bool ff) ff).
 }}.

From 080718830aa9d83ba5ad67dc0e3906edb85c26d8 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sun, 26 Nov 2023 11:09:50 +0100
Subject: [PATCH 5/9] Change signature of is-option-active

---
 apps/tc/elpi/compiler.elpi | 2 +-
 apps/tc/elpi/solver.elpi   | 8 ++++----
 apps/tc/elpi/tc_aux.elpi   | 2 +-
 apps/tc/theories/db.v      | 6 +++---
 apps/tc/theories/tc.v      | 5 ++---
 5 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
index 504160b98..88a29fd41 100644
--- a/apps/tc/elpi/compiler.elpi
+++ b/apps/tc/elpi/compiler.elpi
@@ -97,7 +97,7 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
         (L = [NewPremise | RevPremises])) (L = RevPremises),
     compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _.
 compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- 
-  not (is-option-active {oTC-use-pattern-fragment-compiler}), !,
+  not (is-option-active oTC-use-pattern-fragment-compiler), !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
   make-tc IsHead Ty AppInst Premises Clause.
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index ef3abc101..22fc59cf6 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -4,7 +4,7 @@
 pred time-solve i:prop.
 time-solve P :-
   std.time P Time,
-  if (is-option-active {oTC-time}) (coq.say "[TC] Total resolution time is:" Time) true.
+  if (is-option-active oTC-time) (coq.say "[TC] Total resolution time is:" Time) true.
 
 msolve L N :- !,
   time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
@@ -28,7 +28,7 @@ tc-recursive-search Ty Sol :-
   std.time (coq.safe-dest-app Ty (global TC) TL',
     std.append TL' [Sol] TL,
     coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
-  if (is-option-active {oTC-time-instance-search}) (coq.say "[TC] Instance search time is:" Time) true.
+  if (is-option-active oTC-time-instance-search) (coq.say "[TC] Instance search time is:" Time) true.
 
 :if "solve-print-goal"
 solve (goal Ctx _ Ty _ _) _ :-
@@ -80,10 +80,10 @@ solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
       % coq.say "Solution " X "end" X' "caio",
       % std.assert! (ground_term X') "solution not complete",
       % (pi F\ (copy (fun _ _ x\ (app [F, x])) F :- !)) => copy X X',
-      if (is-option-active {oTC-ignore-eta-reduction}) 
+      if (is-option-active oTC-ignore-eta-reduction) 
         (Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
       std.time (refine Proof' G GL) Refine-Time, 
-      if (is-option-active {oTC-time-refine}) (coq.say "[TC] Refine time is:" Refine-Time) true;
+      if (is-option-active oTC-time-refine) (coq.say "[TC] Refine time is:" Refine-Time) true;
       coq.error "illtyped solution:" {coq.term->string Proof}
     ) 
     (GL = [seal G]).
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 24b952d79..643eec08a 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -69,7 +69,7 @@ get-last (app L) R :-
 % TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name]
 pred gref->pred-name i:gref, o:string.
 gref->pred-name Gr S :-
-  if (is-option-active {oTC-clauseNameShortName})
+  if (is-option-active oTC-clauseNameShortName)
     (Path = "")
     (coq.gref->path Gr [Hd | Tl], 
       std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index a87afc40b..f9c511b65 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -39,9 +39,9 @@ Elpi Db tc_options.db lp:{{
     oTC-use-pattern-fragment-compiler
   ].
 
-  pred is-option-active i:list string.
-  is-option-active Opt :- 
-    coq.option.get Opt (coq.option.bool tt).
+  pred is-option-active i:(list string -> prop).
+  is-option-active Opt :-
+    Opt X, coq.option.get X (coq.option.bool tt).
 }}.
 
 Elpi Db tc.db lp:{{
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 94280b4a3..f8fb2cd49 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -45,9 +45,8 @@ Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
-    all-options Options,
-    std.forall Options (x\ sigma Args\ x Args, 
-      coq.option.add Args (coq.option.bool ff) ff).
+    std.forall {all-options} (x\ sigma L\ x L, 
+      coq.option.add L (coq.option.bool ff) ff).
 }}.
 Elpi Typecheck.
 

From 87fe6106fc1b8f7574197c68abf5a2b86b0d0ab2 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Sun, 26 Nov 2023 11:31:17 +0100
Subject: [PATCH 6/9] refactor imports in apps/tc

---
 apps/tc/elpi/alias.elpi               |  2 ++
 apps/tc/elpi/compiler.elpi            |  3 +++
 apps/tc/elpi/create_tc_predicate.elpi |  4 ++++
 apps/tc/elpi/parser_addInstances.elpi |  4 ++++
 apps/tc/elpi/rewrite_forward.elpi     |  2 ++
 apps/tc/elpi/solver.elpi              |  2 ++
 apps/tc/elpi/tc_aux.elpi              |  2 ++
 apps/tc/theories/add_commands.v       | 16 +---------------
 apps/tc/theories/tc.v                 | 13 +++----------
 9 files changed, 23 insertions(+), 25 deletions(-)

diff --git a/apps/tc/elpi/alias.elpi b/apps/tc/elpi/alias.elpi
index 7f8844038..bf7f420ab 100644
--- a/apps/tc/elpi/alias.elpi
+++ b/apps/tc/elpi/alias.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred alias i:term, o:term.
 
 pred replace-with-alias.aux i:list term, o:list term, o:bool.
diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
index 88a29fd41..36faf5933 100644
--- a/apps/tc/elpi/compiler.elpi
+++ b/apps/tc/elpi/compiler.elpi
@@ -1,6 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+
 % returns the classes on which the current gref depends
 pred get-class-dependencies i:gref, o:list gref.
 get-class-dependencies GR Res :-
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index 53dd00a5a..8e06a3d77 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -1,5 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
+
+accumulate base.
+accumulate tc_aux.
+
 pred string->coq-mode i:string, o:hint-mode.
 string->coq-mode "bang" mode-ground :- !.
 string->coq-mode "plus" mode-input :- !.
diff --git a/apps/tc/elpi/parser_addInstances.elpi b/apps/tc/elpi/parser_addInstances.elpi
index 386dbc766..0c0631c7a 100644
--- a/apps/tc/elpi/parser_addInstances.elpi
+++ b/apps/tc/elpi/parser_addInstances.elpi
@@ -1,6 +1,10 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+accumulate compiler.
+
 kind enum type.
 type path  string -> string -> enum.
 type addInstPrio int -> string -> enum.
diff --git a/apps/tc/elpi/rewrite_forward.elpi b/apps/tc/elpi/rewrite_forward.elpi
index b602a9a13..fca7fc60e 100644
--- a/apps/tc/elpi/rewrite_forward.elpi
+++ b/apps/tc/elpi/rewrite_forward.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred forward i:term, o:term, o:list (pair (list term) term).
 
 % Auxiliary function for rewrite-forward
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 22fc59cf6..8c6453e49 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred time-solve i:prop.
 time-solve P :-
   std.time P Time,
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 643eec08a..dab16588d 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 % Contains the list of classes that
 % cannot be compiled
 
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 56d271504..201f6971d 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -3,18 +3,14 @@
 
 From elpi.apps Require Import db.
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{  
   main L :- 
@@ -26,9 +22,6 @@ Elpi Typecheck.
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File compiler.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -39,8 +32,6 @@ Elpi Typecheck.
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % Ignore is the list of classes we do not want to add
@@ -53,8 +44,6 @@ Elpi Typecheck.
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main L :-
@@ -68,9 +57,8 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
+  accumulate elpi/tc_aux.
   pred addHook i:grafting, i:string. 
   addHook Grafting NewName :- 
     @global! => add-tc-db NewName Grafting (hook NewName).
@@ -99,8 +87,6 @@ Elpi Typecheck.
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main [indt-decl D] :- declare-class D.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index f8fb2cd49..2cc15c0ec 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -3,11 +3,8 @@
 
 Declare ML Module "coq-elpi-tc.plugin".
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
-From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
 From elpi.apps Require Import db.
@@ -38,14 +35,13 @@ Elpi Typecheck.
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File compiler.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
-    std.forall {all-options} (x\ sigma L\ x L, 
+    all-options Options,
+    std.forall Options (x\ sigma L\ x L, 
       coq.option.add L (coq.option.bool ff) ff).
 }}.
 Elpi Typecheck.
@@ -62,8 +58,6 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{
@@ -87,9 +81,8 @@ Elpi Typecheck.
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
+  accumulate elpi/tc_aux.
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
     std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",

From 9ebf370a09ab865f7d917122e8dddcc1c2e3fde8 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 28 Nov 2023 17:01:51 +0100
Subject: [PATCH 7/9] Refactor import for Coq_Dep

---
 apps/tc/theories/add_commands.v | 3 ++-
 apps/tc/theories/db.v           | 3 +++
 apps/tc/theories/tc.v           | 3 ++-
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index 201f6971d..fa7a01e3f 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -3,6 +3,7 @@
 
 From elpi.apps Require Import db.
 
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
@@ -57,8 +58,8 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
-  accumulate elpi/tc_aux.
   pred addHook i:grafting, i:string. 
   addHook Grafting NewName :- 
     @global! => add-tc-db NewName Grafting (hook NewName).
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index f9c511b65..7eb299707 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -3,6 +3,9 @@
 
 From elpi Require Import elpi.
 
+From elpi.apps.tc Extra Dependency "base.elpi".
+From elpi.apps.tc Extra Dependency "tc_aux.elpi".
+
 (* 
   tc_option.db contains the set of options used by the solver of tc. 
   all the options are set to false by default
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 2cc15c0ec..3b255f23d 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -3,6 +3,7 @@
 
 Declare ML Module "coq-elpi-tc.plugin".
 
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -81,8 +82,8 @@ Elpi Typecheck.
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
-  accumulate elpi/tc_aux.
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
     std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",

From 1c767a224e4276904ebe25b7fc39e8e640ad809d Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 28 Nov 2023 17:54:39 +0100
Subject: [PATCH 8/9] warning on hints immediate|external|unfold

---
 apps/tc/_CoqProject.test |  1 +
 src/coq_elpi_builtins.ml | 22 ++++++++++++++--------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test
index 6d683f46f..293e86d66 100644
--- a/apps/tc/_CoqProject.test
+++ b/apps/tc/_CoqProject.test
@@ -1,4 +1,5 @@
 -arg -w -arg -Not-added
+-arg -w -arg -TC.hints
 
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index cac35f766..a86bcee5a 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -535,18 +535,24 @@ let get_instance (env: Environ.env) (sigma: Evd.evar_map) (tc : GlobRef.t) (inst
   in
   instances_grefs2istance instance
 
+let warning_tc_hints = CWarnings.create ~name:"TC.hints" ~category:elpi_cat Pp.str
+
 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 
-  let hint_asts = List.map Hints.FullHint.repr full_hints in 
-  let hints = List.filter_map (function
-    | Hints.Res_pf a -> Some a 
-    | ERes_pf a -> Some a
-    | Extern (a, b) -> None 
-    | Give_exact a -> Some a
-    | Res_pf_THEN_trivial_fail e -> Some e
-    | Unfold_nth e -> None) hint_asts in 
+  (* let hint_asts = List.map Hints.FullHint.repr full_hints in  *)
+  let hints = List.filter_map (fun (e : Hints.FullHint.t) -> match Hints.FullHint.repr e with
+    | Hints.Res_pf a | ERes_pf a | Give_exact a -> Some a (* Respectively Hint Apply | EApply | Exact *)
+    | Extern _ -> 
+      warning_tc_hints (Printf.sprintf "There is an hint extern in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None
+    | Res_pf_THEN_trivial_fail _ -> (* Hint Immediate *)
+      warning_tc_hints (Printf.sprintf "There is an hint immediate in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None
+    | Unfold_nth _ -> 
+      warning_tc_hints (Printf.sprintf "There is an hint unfold in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None) full_hints 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 ->

From d03e8213e292cb471ef548c517ef770df2617809 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 29 Nov 2023 16:22:07 +0100
Subject: [PATCH 9/9] small refactor

---
 src/coq_elpi_builtins.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index a86bcee5a..bfb59afa6 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -514,14 +514,15 @@ let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority =
 (* 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
+         its implementation.
 *)
-let get_instance (env: Environ.env) (sigma: Evd.evar_map) (tc : GlobRef.t) (instance : GlobRef.t) : type_class_instance =
+let get_isntances_of_tc env sigma (tc : GlobRef.t) = 
   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
+  inst_of_tc
+
+let get_instance env sigma inst_of_tc instance : type_class_instance =
   let instances_grefs2istance inst_gr : type_class_instance = 
     let open Typeclasses in 
     let user_hint_prio = 
@@ -537,6 +538,7 @@ let get_instance (env: Environ.env) (sigma: Evd.evar_map) (tc : GlobRef.t) (inst
 
 let warning_tc_hints = CWarnings.create ~name:"TC.hints" ~category:elpi_cat Pp.str
 
+
 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 
@@ -560,8 +562,9 @@ let get_instances (env: Environ.env) (sigma: Evd.evar_map) tc : type_class_insta
     | Constr.Ind (a, _) -> Some (Names.GlobRef.IndRef a)
     | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a)
     | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a)
-    | _ -> None) constrs in 
-  List.map (get_instance env sigma tc) instances_grefs
+    | _ -> None) constrs in
+  let isnt_of_tc = get_isntances_of_tc env sigma tc in
+  List.map (get_instance env sigma isnt_of_tc) instances_grefs
 
 type scope = ExecutionSite | CurrentModule | Library
 
@@ -2855,8 +2858,10 @@ Supported attributes:
     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 
+    (fun class_gr inst_gr _ ~depth { env } _ state ->
+      let sigma = get_sigma state in
+      let inst_of_tc = get_isntances_of_tc env sigma class_gr in
+      let {priority} = get_instance env sigma inst_of_tc inst_gr in 
       !: priority)),
   DocAbove);