src/Pure/library.ML
changeset 19454 46a7e133f802
parent 19424 b701ea590259
child 19461 d3bc9c1ff241
     1.1 --- a/src/Pure/library.ML	Sun Apr 23 10:57:48 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Apr 24 16:35:30 2006 +0200
     1.3 @@ -52,6 +52,8 @@
     1.4    val is_some: 'a option -> bool
     1.5    val is_none: 'a option -> bool
     1.6    val perhaps: ('a -> 'a option) -> 'a -> 'a
     1.7 +  val eq_opt: ('a * 'b -> bool) -> 'a option * 'b option -> bool
     1.8 +  val merge_opt: ('a * 'a -> bool) -> 'a option * 'a option -> 'a option
     1.9  
    1.10    (*exceptions*)
    1.11    val try: ('a -> 'b) -> 'a -> 'b option
    1.12 @@ -81,6 +83,7 @@
    1.13    val snd: 'a * 'b -> 'b
    1.14    val eq_fst: ('a * 'c -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    1.15    val eq_snd: ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    1.16 +  val eq_pair: ('a * 'c -> bool) -> ('b * 'd -> bool) -> ('a * 'b) * ('c * 'd) -> bool
    1.17    val swap: 'a * 'b -> 'b * 'a
    1.18    val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
    1.19    val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
    1.20 @@ -130,6 +133,7 @@
    1.21    val find_first: ('a -> bool) -> 'a list -> 'a option
    1.22    val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
    1.23    val get_first: ('a -> 'b option) -> 'a list -> 'b option
    1.24 +  val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.25    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    1.26    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    1.27    val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.28 @@ -138,7 +142,6 @@
    1.29    val replicate: int -> 'a -> 'a list
    1.30    val multiply: 'a list -> 'a list list -> 'a list list
    1.31    val product: 'a list -> 'b list -> ('a * 'b) list
    1.32 -  val coalesce: ('a * 'a -> bool) -> ('a * 'b) list -> ('a * 'b list) list
    1.33    val filter: ('a -> bool) -> 'a list -> 'a list
    1.34    val filter_out: ('a -> bool) -> 'a list -> 'a list
    1.35    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.36 @@ -361,6 +364,13 @@
    1.37  
    1.38  fun perhaps f x = the_default x (f x);
    1.39  
    1.40 +fun eq_opt eq (NONE, NONE) = true
    1.41 +  | eq_opt eq (SOME x, SOME y) = eq (x, y)
    1.42 +  | eq_opt _ _ = false;
    1.43 +
    1.44 +fun merge_opt _ (NONE, y) = y
    1.45 +  | merge_opt _ (x, NONE) = x
    1.46 +  | merge_opt eq (SOME x, SOME y) = if eq (x, y) then SOME y else raise Option;
    1.47  
    1.48  (* exceptions *)
    1.49  
    1.50 @@ -428,6 +438,7 @@
    1.51  
    1.52  fun eq_fst eq ((x1, _), (x2, _)) = eq (x1, x2);
    1.53  fun eq_snd eq ((_, y1), (_, y2)) = eq (y1, y2);
    1.54 +fun eq_pair eqx eqy ((x1, y1), (x2, y2)) = eqx (x1, x2) andalso eqy (y1, y2);
    1.55  
    1.56  fun swap (x, y) = (y, x);
    1.57  
    1.58 @@ -649,6 +660,10 @@
    1.59              | SOME y => SOME (i, y)
    1.60    in get 0 end;
    1.61  
    1.62 +fun eq_list _ ([], []) = true
    1.63 +  | eq_list eq (x::xs, y::ys) = eq (x, y) andalso eq_list eq (xs, ys)
    1.64 +  | eq_list _ _ = false;
    1.65 +
    1.66  (*flatten a list of lists to a list*)
    1.67  val flat = List.concat;
    1.68  
    1.69 @@ -692,19 +707,6 @@
    1.70    | product [] _ = []
    1.71    | product (x :: xs) ys = map (pair x) ys @ product xs ys;
    1.72  
    1.73 -(*coalesce ranges of equal keys*)
    1.74 -fun coalesce eq =
    1.75 -  let
    1.76 -    fun vals _ [] = ([], [])
    1.77 -      | vals x (lst as (y, b) :: ps) =
    1.78 -          if eq (x, y) then vals x ps |>> cons b
    1.79 -          else ([], lst);
    1.80 -    fun coal [] = []
    1.81 -      | coal ((x, a) :: ps) =
    1.82 -          let val (bs, qs) = vals x ps
    1.83 -          in (x, a :: bs) :: coal qs end;
    1.84 -  in coal end;
    1.85 -
    1.86  
    1.87  (* filter *)
    1.88