bug correction: get_instances of a hint rule has priority none

Author: FissoreD

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.
 

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 [] [].

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).

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).
 }}.

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".

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