src/Pure/General/table.ML
changeset 16446 0ab34b9d1b1f
parent 16342 b146c31a2955
child 16466 82e2fc13ce54
     1.1 --- a/src/Pure/General/table.ML	Fri Jun 17 18:33:30 2005 +0200
     1.2 +++ b/src/Pure/General/table.ML	Fri Jun 17 18:33:31 2005 +0200
     1.3 @@ -22,6 +22,8 @@
     1.4    val empty: 'a table
     1.5    val is_empty: 'a table -> bool
     1.6    val map: ('a -> 'b) -> 'a table -> 'b table
     1.7 +  val map': (key -> 'a -> 'b) -> 'a table -> 'b table
     1.8 +  val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
     1.9    val foldl: ('a * (key * 'b) -> 'a) -> 'a * 'b table -> 'a
    1.10    val dest: 'a table -> (key * 'a) list
    1.11    val keys: 'a table -> key list
    1.12 @@ -35,7 +37,8 @@
    1.13    val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
    1.14    val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
    1.15    val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUPS*)
    1.16 -  val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table  (*exception DUPS*)
    1.17 +  val join: (key -> 'a * 'a -> 'a option) ->
    1.18 +    'a table * 'a table -> 'a table                                    (*exception DUPS*)
    1.19    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUPS*)
    1.20    val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
    1.21    val delete_safe: key -> 'a table -> 'a table
    1.22 @@ -81,23 +84,24 @@
    1.23  
    1.24  fun map_table _ Empty = Empty
    1.25    | map_table f (Branch2 (left, (k, x), right)) =
    1.26 -      Branch2 (map_table f left, (k, f x), map_table f right)
    1.27 +      Branch2 (map_table f left, (k, f k x), map_table f right)
    1.28    | map_table f (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
    1.29 -      Branch3 (map_table f left, (k1, f x1), map_table f mid, (k2, f x2), map_table f right);
    1.30 +      Branch3 (map_table f left, (k1, f k1 x1),
    1.31 +        map_table f mid, (k2, f k2 x2), map_table f right);
    1.32  
    1.33 -fun foldl_table _ (x, Empty) = x
    1.34 -  | foldl_table f (x, Branch2 (left, p, right)) =
    1.35 -      foldl_table f (f (foldl_table f (x, left), p), right)
    1.36 -  | foldl_table f (x, Branch3 (left, p1, mid, p2, right)) =
    1.37 -      foldl_table f (f (foldl_table f (f (foldl_table f (x, left), p1), mid), p2), right);
    1.38 +fun fold_table f Empty x = x
    1.39 +  | fold_table f (Branch2 (left, p, right)) x =
    1.40 +      fold_table f right (f p (fold_table f left x))
    1.41 +  | fold_table f (Branch3 (left, p1, mid, p2, right)) x =
    1.42 +      fold_table f right (f p2 (fold_table f mid (f p1 (fold_table f left x))));
    1.43  
    1.44 -fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));
    1.45 -fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
    1.46 +fun dest tab = rev (fold_table cons tab []);
    1.47 +fun keys tab = rev (fold_table (cons o #1) tab []);
    1.48  
    1.49  local exception TRUE in
    1.50  
    1.51  fun exists pred tab =
    1.52 -  (foldl_table (fn ((), e) => if pred e then raise TRUE else ()) ((), tab); false)
    1.53 +  (fold_table (fn p => fn () => if pred p then raise TRUE else ()) tab (); false)
    1.54      handle TRUE => true;
    1.55  
    1.56  fun forall pred = not o exists (not o pred);
    1.57 @@ -303,20 +307,20 @@
    1.58  
    1.59  fun join f (table1, table2) =
    1.60    let
    1.61 -    fun add ((tab, dups), (key, x)) =
    1.62 +    fun add (key, x) (tab, dups) =
    1.63        (case lookup (tab, key) of
    1.64          NONE => (update ((key, x), tab), dups)
    1.65        | SOME y =>
    1.66 -          (case f (y, x) of
    1.67 +          (case f key (y, x) of
    1.68              SOME z => (update ((key, z), tab), dups)
    1.69            | NONE => (tab, key :: dups)));
    1.70    in
    1.71 -    (case foldl_table add ((table1, []), table2) of
    1.72 +    (case fold_table add table2 (table1, []) of
    1.73        (table', []) => table'
    1.74      | (_, dups) => raise DUPS (rev dups))
    1.75    end;
    1.76  
    1.77 -fun merge eq tabs = join (fn (y, x) => if eq (y, x) then SOME y else NONE) tabs;
    1.78 +fun merge eq tabs = join (fn _ => fn (y, x) => if eq (y, x) then SOME y else NONE) tabs;
    1.79  
    1.80  
    1.81  (* tables with multiple entries per key *)
    1.82 @@ -331,13 +335,15 @@
    1.83  
    1.84  fun make_multi args = foldr update_multi empty args;
    1.85  fun dest_multi tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab));
    1.86 -fun merge_multi eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists eq xs xs')) tabs;
    1.87 -fun merge_multi' eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')) tabs;
    1.88 +fun merge_multi eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists eq xs xs'));
    1.89 +fun merge_multi' eq = join (fn _ => fn (xs, xs') => SOME (gen_merge_lists' eq xs xs'));
    1.90  
    1.91  
    1.92  (*final declarations of this structure!*)
    1.93 -val map = map_table;
    1.94 -val foldl = foldl_table;
    1.95 +fun map f = map_table (K f);
    1.96 +val map' = map_table;
    1.97 +val fold = fold_table;
    1.98 +fun foldl f (x, tab) = fold (fn p => fn x' => f (x', p)) tab x;
    1.99  
   1.100  end;
   1.101