diff options
| author | Pierre-Marie Pédrot | 2020-06-23 13:53:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-27 19:01:46 +0200 |
| commit | 82caf82d9d2282b00771d38b8b607a134497b192 (patch) | |
| tree | 1ff295b95ed505ba66887cefe446ceedac9ac87b /tactics/dn.ml | |
| parent | 9d8efb01fde0f9e24157872213c0595cc72efc0c (diff) | |
Do not rely on higher-order interfaces for patterns in dnets.
The old API was taking a function to decompose constr patterns into dnet
patterns, but it was applying it in an eager way. So there is not point in
exposing such a complex interface. Instead, we make explicit the dnet pattern
type, export a function that turns a constr pattern into a dnet pattern, and
make the add and remove dnet functions take a dnet pattern instead.
This only affects pattern-consuming functions. The lookup function, which
operates on kernel terms instead of constr patterns, is still relying on HO
primitives.
Diffstat (limited to 'tactics/dn.ml')
| -rw-r--r-- | tactics/dn.ml | 12 |
1 files changed, 8 insertions, 4 deletions
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 |