# HG changeset patch
# User wenzelm
# Date 1144601477 -7200
# Node ID a7c055012a8c0a247a4f514f8a65d7751b54c37e
# Parent  44937faf9e1a0d4ce122846641d82c2a34e2d14f
added coalesce;

diff -r 44937faf9e1a -r a7c055012a8c src/Pure/library.ML
--- 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 *)