diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 23:03:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-18 19:35:57 +0200 |
| commit | 8303c9cab6bc403dfc209f65287b67e883a35711 (patch) | |
| tree | 9e6a086583aec8c58ab43c489cc3b863f500a48f /clib/hMap.ml | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
[clib] Provide `filter_range` function.
This is very useful to compute efficiently a list of prefixes. Will be
used in conjunction with the nametab to provide completion.
Example of use:
```
let cprefix x y = String.(compare x (sub y 0 (min (length x) (length y)))) in
M.filter_range (cprefix "foo") m
```
We could of course maintain a trie, but this is less invasive an
should work at our scale.
Diffstat (limited to 'clib/hMap.ml')
| -rw-r--r-- | clib/hMap.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/clib/hMap.ml b/clib/hMap.ml index 33cb6d0131..9c80398e4d 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -398,6 +398,10 @@ struct let height s = Int.Map.height s + (* Not as efficient as the original version *) + let filter_range f s = + filter (fun x _ -> f x = 0) s + module Unsafe = struct let map f s = |