# HG changeset patch
# User haftmann
# Date 1145889330 -7200
# Node ID 46a7e133f8027a28dc2ec9ef41c5b343047dc5a0
# Parent  e4f382a270ad0417af0ff6194c25f8d9f11a0d2f
moved coalesce to AList, added equality predicates to library

diff -r e4f382a270ad -r 46a7e133f802 src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Sun Apr 23 10:57:48 2006 +0200
+++ b/src/Pure/General/alist.ML	Mon Apr 24 16:35:30 2006 +0200
@@ -2,9 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Association lists -- lists of (key, value) pairs with unique keys.
-A light-weight representation of finite mappings;
-see also Pure/General/table.ML for a more scalable implementation.
+Association lists -- lists of (key, value) pairs.
 *)
 
 signature ALIST =
@@ -22,12 +20,15 @@
     -> ('b * 'c) list -> ('b * 'c) list
   val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c)
     -> ('b * 'c) list -> 'd option * ('b * 'c) list
-  val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
   val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) ->
     ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list         (*exception DUP*)
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
     -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
+  val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
+  val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
+    (*coalesce ranges of equal neighbour keys*)
+  val group: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
 end;
 
 structure AList: ALIST =
@@ -112,4 +113,19 @@
         val values = find eq xs value';
       in if eq (value', value) then key :: values else values end;
 
+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;
+
+fun group eq xs =
+  fold_rev (fn (k, v) => default eq (k, []) #> map_entry eq k (cons v)) xs [];
+
 end;
diff -r e4f382a270ad -r 46a7e133f802 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Sun Apr 23 10:57:48 2006 +0200
+++ b/src/Pure/Isar/local_syntax.ML	Mon Apr 24 16:35:30 2006 +0200
@@ -61,7 +61,7 @@
           (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
            map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
       |> fold (uncurry (Syntax.extend_const_gram is_logtype))
-          (coalesce (op =) (rev (map snd mixfixes)));
+          (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end;
 
 fun init thy = build_syntax thy ([], ([], []));
diff -r e4f382a270ad -r 46a7e133f802 src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Apr 23 10:57:48 2006 +0200
+++ b/src/Pure/library.ML	Mon Apr 24 16:35:30 2006 +0200
@@ -52,6 +52,8 @@
   val is_some: 'a option -> bool
   val is_none: 'a option -> bool
   val perhaps: ('a -> 'a option) -> 'a -> 'a
+  val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool
+  val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
 
   (*exceptions*)
   val try: ('a -> 'b) -> 'a -> 'b option
@@ -81,6 +83,7 @@
   val snd: 'a * 'b -> 'b
   val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
   val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
+  val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
   val swap: 'a * 'b -> 'b * 'a
   val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
   val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
@@ -130,6 +133,7 @@
   val find_first: ('a -> bool) -> 'a list -> 'a option
   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
+  val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -138,7 +142,6 @@
   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
@@ -361,6 +364,13 @@
 
 fun perhaps f x = the_default x (f x);
 
+fun eq_opt eq (NONE, NONE) = true
+  | eq_opt eq (SOME x, SOME y) = eq (x, y)
+  | eq_opt _ _ = false;
+
+fun merge_opt _ (NONE, y) = y
+  | merge_opt _ (x, NONE) = x
+  | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
 
 (* exceptions *)
 
@@ -428,6 +438,7 @@
 
 fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
 fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
+fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2);
 
 fun swap (x, y) = (y, x);
 
@@ -649,6 +660,10 @@
             | SOME y => SOME (i, y)
   in get 0 end;
 
+fun eq_list _ ([], []) = true
+  | eq_list eq (x::xs, y::ys) = eq (x, y) andalso eq_list eq (xs, ys)
+  | eq_list _ _ = false;
+
 (*flatten a list of lists to a list*)
 val flat = List.concat;
 
@@ -692,19 +707,6 @@
   | 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 *)