New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Set.Make.split not very useful #6111
Comments
Comment author: berenger Here is my naive implementation in file set.ml:
I say naive because I see in set.ml functions such that add_min_element Regards, |
Comment author: berenger Maybe the smaller change is to create: Set.Make.split_opt : elt -> t -> t * elt option * t Then users could easily create the other functions |
Comment author: @xavierleroy Hello Francois, I can see where those new functions would be useful, having recently done something similar (but more general) in Coq, as part of CompCert. I am not sure this is general enough, though. Consider sets of pairs, lexicographically ordered, and assume you want to extract (efficiently) the set of pairs whose first component is equal to "x". If it's a set of int * int pairs, your API works fine: let (lt_x, ge_x) = split_lt (x, min_int) s in But if it's a set of string * string pairs, it doesn't work, as strings have no least element, no greater element, and no successor operation. The approach I used in CompCert is described here: It selects set elements according to two boolean predicates that must be compatible with the set order, in a way made precise in the Coq development. But I don't think this can be exposed as is in OCaml's Set API, because it can break the BST invariant. |
Comment author: berenger I don't know Coq unfortunately. https://github.com/UnixJunkie/interval-tree/blob/master/interval_tree.ml Would there be any problem with the following function for set.ml:
|
Comment author: berenger If we have a split_opt, then we can have:
I personally need only the splitting functions. |
Comment author: @xavierleroy The forthcoming 4.01 release has a new function "find" in module Set, which can be used to implement the splitting functions you need: let split_opt x s = let split_lt_ge x s = The cost of calling S.find (log n) is negligible compared with that of S.split (n). The even more general variants of "split" that I mentioned cannot be encoded efficiently this way, though. |
Comment author: berenger The cost of S.split is really O(n)? http://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.S.html Sorry if I am wrong, |
Comment author: berenger The functions split_opt, split_lt and split_le |
Comment author: berenger I think this issue can be closed: the functions |
Comment author: @xavierleroy Closing this PR as suggested. And, yes, S.split is logarithmic time, not linear; my mistake. |
Original bug ID: 6111
Reporter: berenger
Status: closed (set by @xavierleroy on 2013-08-28T13:55:32Z)
Resolution: not a bug
Priority: normal
Severity: feature
Version: 4.00.1
Category: standard library
Monitored by: @gasche @hcarty
Bug description
Hello,
Set.Make.split : elt -> t -> t * bool * t
As a scientific programmer, I would most times
want to split like this:
split_lt = (elements < x, elements >= x)
or
split_lte = (elements <= x, elements > x)
Would it be possible to introduce split_lt and split_lte?
Or maybe: split_lt_gte and split_lte_gt?
Thanks,
Francois.
PS: remember that x may be different from the
elements that compare = to x but that is
actually in the set being split
The text was updated successfully, but these errors were encountered: