From 9e6f453aff9716a6417c78800aeffea494069001 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 15 Apr 2021 22:16:50 +0100 Subject: [PATCH] feat(CCRAL): add `get_and_remove_exn` operation It seems like a waste to repeat the search for an index to both get the element at that index and then to remove it. The added `get_and_remove_exn` operation performs a `remove` but returns the found element rather than forgetting it. --- src/data/CCRAL.ml | 11 +++++++++++ src/data/CCRAL.mli | 6 +++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/data/CCRAL.ml b/src/data/CCRAL.ml index 7e4b4614..65397b92 100644 --- a/src/data/CCRAL.ml +++ b/src/data/CCRAL.ml @@ -125,6 +125,17 @@ let remove l i = _remove [] l i [1;2;4] (to_list @@ remove (of_list [1;2;3;4]) 2) *) +let rec _get_and_remove_exn found prefix l i = + let x, l' = front_exn l in + if i=0 + then (found := Some x; List.fold_left (fun l x -> cons x l) l' prefix) + else _get_and_remove_exn found (x::prefix) l' (i-1) + +let get_and_remove_exn l i = + let found = ref None in + let l' = _get_and_remove_exn found [] l i in + (Option.get !found, l') + let rec _map_tree f t = match t with | Leaf x -> Leaf (f x) | Node (x, l, r) -> Node (f x, _map_tree f l, _map_tree f r) diff --git a/src/data/CCRAL.mli b/src/data/CCRAL.mli index 6f5bcbad..2a9d2d16 100644 --- a/src/data/CCRAL.mli +++ b/src/data/CCRAL.mli @@ -65,7 +65,11 @@ val set : 'a t -> int -> 'a -> 'a t @raise Invalid_argument if the list has less than [i+1] elements. *) val remove : 'a t -> int -> 'a t -(** [remove l i] removes the [i]-th element of [v]. +(** [remove l i] removes the [i]-th element of [l]. + @raise Invalid_argument if the list has less than [i+1] elements. *) + +val get_and_remove_exn : 'a t -> int -> 'a * 'a t +(** [get_and_remove_exn l i] accesses and removes the [i]-th element of [l]. @raise Invalid_argument if the list has less than [i+1] elements. *) val append : 'a t -> 'a t -> 'a t