--- a/src/Pure/library.ML Sun Apr 09 18:51:16 2006 +0200
+++ b/src/Pure/library.ML Sun Apr 09 18:51:17 2006 +0200
@@ -137,6 +137,7 @@
val replicate: int -> 'a -> 'a list
val multiply: 'a list -> 'a list list -> 'a list list
val product: 'a list -> 'b list -> ('a * 'b) list
+ val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
val filter: ('a -> bool) -> 'a list -> 'a list
val filter_out: ('a -> bool) -> 'a list -> 'a list
val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
@@ -690,6 +691,19 @@
| product [] _ = []
| product (x :: xs) ys = map (pair x) ys @ product xs ys;
+(*coalesce ranges of equal keys*)
+fun coalesce eq =
+ let
+ fun vals _ [] = ([], [])
+ | vals x (lst as (y, b) :: ps) =
+ if eq (x, y) then vals x ps |>> cons b
+ else ([], lst);
+ fun coal [] = []
+ | coal ((x, a) :: ps) =
+ let val (bs, qs) = vals x ps
+ in (x, a :: bs) :: coal qs end;
+ in coal end;
+
(* filter *)