diff options
| -rw-r--r-- | tactics/btermdn.ml | 22 | ||||
| -rw-r--r-- | tactics/btermdn.mli | 8 | ||||
| -rw-r--r-- | tactics/dn.ml | 12 | ||||
| -rw-r--r-- | tactics/dn.mli | 8 | ||||
| -rw-r--r-- | tactics/hints.ml | 18 |
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' = |