diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/cList.ml | 8 | ||||
-rw-r--r-- | lib/cList.mli | 4 |
2 files changed, 12 insertions, 0 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index 93ba0637e..3115826c6 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -61,6 +61,7 @@ sig val except : 'a eq -> 'a -> 'a list -> 'a list val remove : 'a eq -> 'a -> 'a list -> 'a list val remove_first : ('a -> bool) -> 'a list -> 'a list + val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val sep_last : 'a list -> 'a * 'a list val find_map : ('a -> 'b option) -> 'a list -> 'b @@ -442,6 +443,13 @@ let rec remove_first p = function | b::l -> b::remove_first p l | [] -> raise Not_found +let insert p v l = + let rec insrec = function + | [] -> [v] + | h::tl -> if p v h then v::h::tl else h::insrec tl + in + insrec l + let add_set cmp x l = if mem_f cmp x l then l else x :: l (** List equality up to permutation (but considering multiple occurrences) *) diff --git a/lib/cList.mli b/lib/cList.mli index 01ae83960..aa888679c 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -119,6 +119,10 @@ sig val remove_first : ('a -> bool) -> 'a list -> 'a list (** Remove the first element satisfying a predicate, or raise [Not_found] *) + val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list + (** Insert at the (first) position so that if the list is ordered wrt to the + total order given as argument, the order is preserved *) + val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val sep_last : 'a list -> 'a * 'a list |