moved coalesce to AList, added equality predicates to library
authorhaftmann
Mon Apr 24 16:35:30 2006 +0200 (2006-04-24)
changeset 1945446a7e133f802
parent 19453 e4f382a270ad
child 19455 d828bfab05af
moved coalesce to AList, added equality predicates to library
src/Pure/General/alist.ML
src/Pure/Isar/local_syntax.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/alist.ML	Sun Apr 23 10:57:48 2006 +0200
     1.2 +++ b/src/Pure/General/alist.ML	Mon Apr 24 16:35:30 2006 +0200
     1.3 @@ -2,9 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Association lists -- lists of (key, value) pairs with unique keys.
     1.8 -A light-weight representation of finite mappings;
     1.9 -see also Pure/General/table.ML for a more scalable implementation.
    1.10 +Association lists -- lists of (key, value) pairs.
    1.11  *)
    1.12  
    1.13  signature ALIST =
    1.14 @@ -22,12 +20,15 @@
    1.15      -> ('b * 'c) list -> ('b * 'c) list
    1.16    val map_entry_yield: ('a * 'b -> bool) -> 'a -> ('c -> 'd * 'c)
    1.17      -> ('b * 'c) list -> 'd option * ('b * 'c) list
    1.18 -  val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
    1.19    val join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b option) ->
    1.20      ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list         (*exception DUP*)
    1.21    val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
    1.22      -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
    1.23 +  val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
    1.24    val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
    1.25 +  val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
    1.26 +    (*coalesce ranges of equal neighbour keys*)
    1.27 +  val group: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
    1.28  end;
    1.29  
    1.30  structure AList: ALIST =
    1.31 @@ -112,4 +113,19 @@
    1.32          val values = find eq xs value';
    1.33        in if eq (value', value) then key :: values else values end;
    1.34  
    1.35 +fun coalesce eq =
    1.36 +  let
    1.37 +    fun vals _ [] = ([], [])
    1.38 +      | vals x (lst as (y, b) :: ps) =
    1.39 +          if eq (x, y) then vals x ps |>> cons b
    1.40 +          else ([], lst);
    1.41 +    fun coal [] = []
    1.42 +      | coal ((x, a) :: ps) =
    1.43 +          let val (bs, qs) = vals x ps
    1.44 +          in (x, a :: bs) :: coal qs end;
    1.45 +  in coal end;
    1.46 +
    1.47 +fun group eq xs =
    1.48 +  fold_rev (fn (k, v) => default eq (k, []) #> map_entry eq k (cons v)) xs [];
    1.49 +
    1.50  end;
     2.1 --- a/src/Pure/Isar/local_syntax.ML	Sun Apr 23 10:57:48 2006 +0200
     2.2 +++ b/src/Pure/Isar/local_syntax.ML	Mon Apr 24 16:35:30 2006 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4            (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
     2.5             map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
     2.6        |> fold (uncurry (Syntax.extend_const_gram is_logtype))
     2.7 -          (coalesce (op =) (rev (map snd mixfixes)));
     2.8 +          (AList.coalesce (op =) (rev (map snd mixfixes)));
     2.9    in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end;
    2.10  
    2.11  fun init thy = build_syntax thy ([], ([], []));
     3.1 --- a/src/Pure/library.ML	Sun Apr 23 10:57:48 2006 +0200
     3.2 +++ b/src/Pure/library.ML	Mon Apr 24 16:35:30 2006 +0200
     3.3 @@ -52,6 +52,8 @@
     3.4    val is_some: 'a option -> bool
     3.5    val is_none: 'a option -> bool
     3.6    val perhaps: ('a -> 'a option) -> 'a -> 'a
     3.7 +  val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool
     3.8 +  val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
     3.9  
    3.10    (*exceptions*)
    3.11    val try: ('a -> 'b) -> 'a -> 'b option
    3.12 @@ -81,6 +83,7 @@
    3.13    val snd: 'a * 'b -> 'b
    3.14    val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    3.15    val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    3.16 +  val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    3.17    val swap: 'a * 'b -> 'b * 'a
    3.18    val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
    3.19    val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
    3.20 @@ -130,6 +133,7 @@
    3.21    val find_first: ('a -> bool) -> 'a list -> 'a option
    3.22    val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
    3.23    val get_first: ('a -> 'b option) -> 'a list -> 'b option
    3.24 +  val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    3.25    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    3.26    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    3.27    val ~~ : 'a list * 'b list -> ('a * 'b) list
    3.28 @@ -138,7 +142,6 @@
    3.29    val replicate: int -> 'a -> 'a list
    3.30    val multiply: 'a list -> 'a list list -> 'a list list
    3.31    val product: 'a list -> 'b list -> ('a * 'b) list
    3.32 -  val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
    3.33    val filter: ('a -> bool) -> 'a list -> 'a list
    3.34    val filter_out: ('a -> bool) -> 'a list -> 'a list
    3.35    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    3.36 @@ -361,6 +364,13 @@
    3.37  
    3.38  fun perhaps f x = the_default x (f x);
    3.39  
    3.40 +fun eq_opt eq (NONE, NONE) = true
    3.41 +  | eq_opt eq (SOME x, SOME y) = eq (x, y)
    3.42 +  | eq_opt _ _ = false;
    3.43 +
    3.44 +fun merge_opt _ (NONE, y) = y
    3.45 +  | merge_opt _ (x, NONE) = x
    3.46 +  | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
    3.47  
    3.48  (* exceptions *)
    3.49  
    3.50 @@ -428,6 +438,7 @@
    3.51  
    3.52  fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
    3.53  fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
    3.54 +fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2);
    3.55  
    3.56  fun swap (x, y) = (y, x);
    3.57  
    3.58 @@ -649,6 +660,10 @@
    3.59              | SOME y => SOME (i, y)
    3.60    in get 0 end;
    3.61  
    3.62 +fun eq_list _ ([], []) = true
    3.63 +  | eq_list eq (x::xs, y::ys) = eq (x, y) andalso eq_list eq (xs, ys)
    3.64 +  | eq_list _ _ = false;
    3.65 +
    3.66  (*flatten a list of lists to a list*)
    3.67  val flat = List.concat;
    3.68  
    3.69 @@ -692,19 +707,6 @@
    3.70    | product [] _ = []
    3.71    | product (x :: xs) ys = map (pair x) ys @ product xs ys;
    3.72  
    3.73 -(*coalesce ranges of equal keys*)
    3.74 -fun coalesce eq =
    3.75 -  let
    3.76 -    fun vals _ [] = ([], [])
    3.77 -      | vals x (lst as (y, b) :: ps) =
    3.78 -          if eq (x, y) then vals x ps |>> cons b
    3.79 -          else ([], lst);
    3.80 -    fun coal [] = []
    3.81 -      | coal ((x, a) :: ps) =
    3.82 -          let val (bs, qs) = vals x ps
    3.83 -          in (x, a :: bs) :: coal qs end;
    3.84 -  in coal end;
    3.85 -
    3.86  
    3.87  (* filter *)
    3.88