From ae7347691e73fe4f51b54c899b5ca8ec112bafe1 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Mon, 1 Jul 2024 15:59:11 +0200
Subject: [PATCH] [TC] bug fix: conversion str2gr should not be done in the
 cache

this avoids a bug source reproducible with tests/test_import/f2.v
---
 .../tc/src/coq_elpi_class_tactics_takeover.ml | 28 +++++++++----------
 apps/tc/tests/test_import/f1.v                |  4 +++
 apps/tc/tests/test_import/f2.v                |  1 +
 3 files changed, 19 insertions(+), 14 deletions(-)
 create mode 100644 apps/tc/tests/test_import/f1.v
 create mode 100644 apps/tc/tests/test_import/f2.v

diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/coq_elpi_class_tactics_takeover.ml
index 3fb018f66..035809037 100644
--- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml
+++ b/apps/tc/src/coq_elpi_class_tactics_takeover.ml
@@ -1580,7 +1580,8 @@ module type M = sig
   val add : elt -> t -> t
   val gr2elt : Names.GlobRef.t -> elt
   val mem : elt -> t -> bool
-  val strs2set : Libnames.qualid list -> t
+  val of_qualid_list : Libnames.qualid list -> t
+
 end
 
 (* Set of overridden class *)
@@ -1596,11 +1597,9 @@ module OSet : M = struct
   let mem = M.mem
   let gr2elt (x: Names.GlobRef.t) : elt = x
 
-  let strs2set x = 
-    let add_str x = add (str2gr x) in
-    let grl2set grl = List.fold_right add_str grl empty in
-    grl2set x
-
+  let of_qualid_list (x: Libnames.qualid list) : t = 
+    let add s x = add (Coq_elpi_utils.locate_simple_qualid x) s in
+    List.fold_left add empty x
 end
 
 module Modes = struct
@@ -1612,8 +1611,8 @@ module Modes = struct
 
   type action =
     | Set of omode
-    | Add of Libnames.qualid list
-    | Rm of Libnames.qualid list
+    | Add of OSet.t
+    | Rm of OSet.t
 
   let omodes = ref (CSMap.empty : omode CSMap.t)
 
@@ -1627,10 +1626,10 @@ module Modes = struct
     let new_mode =
       match old_mode, new_mode with
       | _, Set(mode) -> mode
-      | AllButFor s, Add grl -> AllButFor (OSet.diff s (OSet.strs2set grl))
-      | AllButFor s, Rm grl -> AllButFor (OSet.union s (OSet.strs2set grl))
-      | Only s, Add grl -> Only (OSet.union s (OSet.strs2set grl))
-      | Only s, Rm grl -> Only (OSet.diff s (OSet.strs2set grl))
+      | AllButFor s, Add grl -> AllButFor (OSet.diff s grl)
+      | AllButFor s, Rm grl -> AllButFor (OSet.union s grl)
+      | Only s, Add grl -> Only (OSet.union s grl)
+      | Only s, Rm grl -> Only (OSet.diff s grl)
       in
     omodes := CSMap.set name new_mode !omodes
 
@@ -1695,17 +1694,18 @@ end
  
 
 let set_solver_mode kind qname (l: Libnames.qualid list) = 
+  let l = OSet.of_qualid_list l in
   let cache_solver_mode = Modes.cache_solver_mode in
   match kind with
   | AAdd -> Lib.add_leaf (cache_solver_mode (qname, Add l, false))
   | ARm  -> Lib.add_leaf (cache_solver_mode (qname, Rm l, false))
   | AAll -> Lib.add_leaf (cache_solver_mode (qname, Set (AllButFor OSet.empty), false))
   | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false))
-  | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only (OSet.strs2set l)), false))
+  | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only l), false))
 
 let solver_register l =
   Lib.add_leaf (Solver.cache_solver (l, Create));
-  Lib.add_leaf (Modes.cache_solver_mode (l, Add [], true))
+  Lib.add_leaf (Modes.cache_solver_mode (l, Add OSet.empty, true))
 
 let solver_activate l = Lib.add_leaf (Solver.cache_solver (l, Activate))
 
diff --git a/apps/tc/tests/test_import/f1.v b/apps/tc/tests/test_import/f1.v
new file mode 100644
index 000000000..de8f271bc
--- /dev/null
+++ b/apps/tc/tests/test_import/f1.v
@@ -0,0 +1,4 @@
+From elpi.apps Require Export tc.
+From Coq Require Export Morphisms.
+
+Elpi TC Solver Override TC.Solver Rm Proper ProperProxy.
diff --git a/apps/tc/tests/test_import/f2.v b/apps/tc/tests/test_import/f2.v
new file mode 100644
index 000000000..efa2686e9
--- /dev/null
+++ b/apps/tc/tests/test_import/f2.v
@@ -0,0 +1 @@
+From elpi.apps.tc.tests.test_import Require Import f1.
\ No newline at end of file