Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets.

Reviewed-by: herbelin

5 files changed, 39 insertions, 29 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bb062bfc11..1f148e01fa 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -151,23 +151,15 @@ struct
 
  type t = Dn.t
 
-  let empty = Dn.empty
+  type pattern = Dn.pattern
 
-  let add = function
-    | None ->
-        (fun dn (c,v) ->
-           Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-    | Some st ->
-        (fun dn (c,v) ->
-           Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+  let pattern st pat = match st with
+  | None -> Dn.pattern bounded_constr_pat_discr (pat, !dnet_depth)
+  | Some st -> Dn.pattern (bounded_constr_pat_discr_st st) (pat, !dnet_depth)
 
-  let rmv = function
-    | None ->
-        (fun dn (c,v) ->
-           Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
-    | Some st ->
-        (fun dn (c,v) ->
-         Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+  let empty = Dn.empty
+  let add = Dn.add
+  let rmv = Dn.rmv
 
   let lookup sigma = function
     | None ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 4358e5a8d9..2caa193202 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -28,10 +28,14 @@ module Make :
 sig
   type t
 
+  type pattern
+
+  val pattern : TransparentState.t option -> constr_pattern -> pattern
+
   val empty : t
 
-  val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
-  val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
+  val add : t -> pattern -> Z.t -> t
+  val rmv : t -> pattern -> Z.t -> t
 
   val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
   val app : (Z.t -> unit) -> t -> unit
diff --git a/tactics/dn.ml b/tactics/dn.ml
index e1c9b7c0b5..07eb49442a 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -38,6 +38,8 @@ struct
 
   type  t = Trie.t
 
+  type pattern = (Y.t * int) option list
+
   let empty = Trie.empty
 
 (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
@@ -89,11 +91,13 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
     in
     List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
 
-  let add tm dna (pat,inf) =
-    let p = path_of dna pat in Trie.add p (ZSet.singleton inf) tm
+  let pattern dna pat = path_of dna pat
+
+  let add tm p inf =
+    Trie.add p (ZSet.singleton inf) tm
 
-  let rmv tm dna (pat,inf) =
-    let p = path_of dna pat in Trie.remove p (ZSet.singleton inf) tm
+  let rmv tm p inf =
+    Trie.remove p (ZSet.singleton inf) tm
 
   let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm
 
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 2a60c3eb82..287aa2b257 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -18,9 +18,13 @@ sig
      must decompose any tree into a label characterizing its root node and
      the list of its subtree *)
 
-  val add : t -> 'a decompose_fun -> 'a * Z.t -> t
+  type pattern
 
-  val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t
+  val pattern : 'a decompose_fun -> 'a -> pattern
+
+  val add : t -> pattern -> Z.t -> t
+
+  val rmv : t -> pattern -> Z.t -> t
 
   type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 386224824f..58bebe319b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -258,7 +258,7 @@ let empty_se = {
 
 let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
 
-let add_tac pat t st se =
+let add_tac pat t se =
   match pat with
   | None ->
     if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
@@ -267,12 +267,14 @@ let add_tac pat t st se =
     if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
     else { se with
         sentry_pat = List.insert pri_order t se.sentry_pat;
-        sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); }
+        sentry_bnet = Bounded_net.add se.sentry_bnet pat t; }
 
 let rebuild_dn st se =
   let dn' =
     List.fold_left
-      (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
+      (fun dn (id, t) ->
+        let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in
+        Bounded_net.add dn pat (id, t))
       Bounded_net.empty se.sentry_pat
   in
   { se with sentry_bnet = dn' }
@@ -636,8 +638,6 @@ struct
           is_unfold v.code.obj then None else Some gr
       | None -> None
     in
-    let dnst = if db.use_dn then Some db.hintdb_state else None in
-    let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in
       match k with
       | None ->
           let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
@@ -646,8 +646,14 @@ struct
             { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
           else db
       | Some gr ->
+        let pat =
+          if not db.use_dn && is_exact v.code.obj then None
+          else
+            let dnst = if db.use_dn then Some db.hintdb_state else None in
+            Option.map (fun p -> Bounded_net.pattern dnst p) v.pat
+        in
           let oval = find gr db in
-            { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+            { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map }
 
   let rebuild_db st' db =
     let db' =