tuned updates, added map_entry;
authorwenzelm
Thu Apr 07 09:26:40 2005 +0200 (2005-04-07 ago)
changeset 156657e7412fffc0c
parent 15664 7c150afba112
child 15666 5c5925dc4921
tuned updates, added map_entry;
src/Pure/General/table.ML
     1.1 --- a/src/Pure/General/table.ML	Thu Apr 07 09:26:29 2005 +0200
     1.2 +++ b/src/Pure/General/table.ML	Thu Apr 07 09:26:40 2005 +0200
     1.3 @@ -31,11 +31,12 @@
     1.4    val lookup: 'a table * key -> 'a option
     1.5    val update: (key * 'a) * 'a table -> 'a table
     1.6    val update_new: (key * 'a) * 'a table -> 'a table                    (*exception DUP*)
     1.7 +  val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
     1.8    val make: (key * 'a) list -> 'a table                                (*exception DUPS*)
     1.9    val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUPS*)
    1.10    val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table  (*exception DUPS*)
    1.11    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUPS*)
    1.12 -  val delete: key -> 'a table -> 'a table    (* exception UNDEF *)
    1.13 +  val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
    1.14    val lookup_multi: 'a list table * key -> 'a list
    1.15    val update_multi: (key * 'a) * 'a list table -> 'a list table
    1.16    val make_multi: (key * 'a) list -> 'a list table
    1.17 @@ -90,12 +91,13 @@
    1.18  fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
    1.19  
    1.20  fun min_key Empty = NONE
    1.21 -  | min_key (Branch2 (left, (k, _), _)) = SOME (getOpt (min_key left,k))
    1.22 -  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (getOpt (min_key left,k));
    1.23 +  | min_key (Branch2 (left, (k, _), _)) = SOME (getOpt (min_key left, k))
    1.24 +  | min_key (Branch3 (left, (k, _), _, _, _)) = SOME (getOpt (min_key left, k));
    1.25  
    1.26  fun max_key Empty = NONE
    1.27 -  | max_key (Branch2 (_, (k, _), right)) = SOME (getOpt (max_key right,k))
    1.28 -  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (getOpt (max_key right,k));
    1.29 +  | max_key (Branch2 (_, (k, _), right)) = SOME (getOpt (max_key right, k))
    1.30 +  | max_key (Branch3 (_, _, _, (k,_), right)) = SOME (getOpt (max_key right, k));
    1.31 +
    1.32  
    1.33  (* lookup *)
    1.34  
    1.35 @@ -116,57 +118,67 @@
    1.36            | GREATER => lookup (right, key)));
    1.37  
    1.38  
    1.39 -(* update *)
    1.40 +(* updates *)
    1.41  
    1.42 -fun compare (k1, _) (k2, _) = Key.ord (k1, k2);
    1.43 +local
    1.44 +
    1.45 +exception SAME;
    1.46  
    1.47  datatype 'a growth =
    1.48    Stay of 'a table |
    1.49    Sprout of 'a table * (key * 'a) * 'a table;
    1.50  
    1.51 -fun insert pair Empty = Sprout (Empty, pair, Empty)
    1.52 -  | insert pair (Branch2 (left, p, right)) =
    1.53 -      (case compare pair p of
    1.54 -        LESS =>
    1.55 -          (case insert pair left of
    1.56 -            Stay left' => Stay (Branch2 (left', p, right))
    1.57 -          | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
    1.58 -      | EQUAL => Stay (Branch2 (left, pair, right))
    1.59 -      | GREATER =>
    1.60 -          (case insert pair right of
    1.61 -            Stay right' => Stay (Branch2 (left, p, right'))
    1.62 -          | Sprout (right1, q, right2) =>
    1.63 -              Stay (Branch3 (left, p, right1, q, right2))))
    1.64 -  | insert pair (Branch3 (left, p1, mid, p2, right)) =
    1.65 -      (case compare pair p1 of
    1.66 -        LESS =>
    1.67 -          (case insert pair left of
    1.68 -            Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
    1.69 -          | Sprout (left1, q, left2) =>
    1.70 -              Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
    1.71 -      | EQUAL => Stay (Branch3 (left, pair, mid, p2, right))
    1.72 -      | GREATER =>
    1.73 -          (case compare pair p2 of
    1.74 +fun modify key f tab =
    1.75 +  let
    1.76 +    fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
    1.77 +      | modfy (Branch2 (left, p as (k, x), right)) =
    1.78 +          (case Key.ord (key, k) of
    1.79 +            LESS =>
    1.80 +              (case modfy left of
    1.81 +                Stay left' => Stay (Branch2 (left', p, right))
    1.82 +              | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
    1.83 +          | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right))
    1.84 +          | GREATER =>
    1.85 +              (case modfy right of
    1.86 +                Stay right' => Stay (Branch2 (left, p, right'))
    1.87 +              | Sprout (right1, q, right2) =>
    1.88 +                  Stay (Branch3 (left, p, right1, q, right2))))
    1.89 +      | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
    1.90 +          (case Key.ord (key, k1) of
    1.91              LESS =>
    1.92 -              (case insert pair mid of
    1.93 -                Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
    1.94 -              | Sprout (mid1, q, mid2) =>
    1.95 -                  Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
    1.96 -          | EQUAL => Stay (Branch3 (left, p1, mid, pair, right))
    1.97 +              (case modfy left of
    1.98 +                Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
    1.99 +              | Sprout (left1, q, left2) =>
   1.100 +                  Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
   1.101 +          | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right))
   1.102            | GREATER =>
   1.103 -              (case insert pair right of
   1.104 -                Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
   1.105 -              | Sprout (right1, q, right2) =>
   1.106 -                  Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
   1.107 +              (case Key.ord (key, k2) of
   1.108 +                LESS =>
   1.109 +                  (case modfy mid of
   1.110 +                    Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
   1.111 +                  | Sprout (mid1, q, mid2) =>
   1.112 +                      Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
   1.113 +              | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right))
   1.114 +              | GREATER =>
   1.115 +                  (case modfy right of
   1.116 +                    Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
   1.117 +                  | Sprout (right1, q, right2) =>
   1.118 +                      Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
   1.119  
   1.120 -fun update (pair, tab) =
   1.121 -  (case insert pair tab of
   1.122 -    Stay tab => tab
   1.123 -  | Sprout br => Branch2 br);
   1.124 +  in
   1.125 +    (case modfy tab of
   1.126 +      Stay tab' => tab'
   1.127 +    | Sprout br => Branch2 br)
   1.128 +    handle SAME => tab
   1.129 +  end;
   1.130  
   1.131 -fun update_new (pair as (key, _), tab) =
   1.132 -  if is_none (lookup (tab, key)) then update (pair, tab)
   1.133 -  else raise DUP key;
   1.134 +in
   1.135 +
   1.136 +fun update ((k, x), tab) = modify k (fn _ => x) tab;
   1.137 +fun update_new ((k, x), tab) = modify k (fn NONE => x | SOME _ => raise DUP k) tab;
   1.138 +fun map_entry k f = modify k (fn NONE => raise SAME | SOME x => f x);
   1.139 +
   1.140 +end;
   1.141  
   1.142  
   1.143  (* extend and make *)
   1.144 @@ -188,26 +200,28 @@
   1.145  
   1.146  (* delete *)
   1.147  
   1.148 -fun compare' NONE (k2, _) = LESS
   1.149 -  | compare' (SOME k1) (k2, _) = Key.ord (k1, k2);
   1.150 +exception UNDEF of key;
   1.151 +
   1.152 +local
   1.153 +
   1.154 +fun compare NONE (k2, _) = LESS
   1.155 +  | compare (SOME k1) (k2, _) = Key.ord (k1, k2);
   1.156  
   1.157  fun if_eq EQUAL x y = x
   1.158    | if_eq _ x y = y;
   1.159  
   1.160 -exception UNDEF of key;
   1.161 -
   1.162  fun del (SOME k) Empty = raise UNDEF k
   1.163    | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
   1.164    | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
   1.165        (p, (false, Branch2 (Empty, q, Empty)))
   1.166 -  | del k (Branch2 (Empty, p, Empty)) = (case compare' k p of
   1.167 +  | del k (Branch2 (Empty, p, Empty)) = (case compare k p of
   1.168        EQUAL => (p, (true, Empty)) | _ => raise UNDEF (valOf k))
   1.169 -  | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare' k p of
   1.170 +  | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
   1.171        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
   1.172 -    | _ => (case compare' k q of
   1.173 +    | _ => (case compare k q of
   1.174          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
   1.175        | _ => raise UNDEF (valOf k)))
   1.176 -  | del k (Branch2 (l, p, r)) = (case compare' k p of
   1.177 +  | del k (Branch2 (l, p, r)) = (case compare k p of
   1.178        LESS => (case del k l of
   1.179          (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
   1.180        | (p', (true, l')) => (p', case r of
   1.181 @@ -222,8 +236,8 @@
   1.182              (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
   1.183          | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
   1.184              (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
   1.185 -  | del k (Branch3 (l, p, m, q, r)) = (case compare' k q of
   1.186 -      LESS => (case compare' k p of
   1.187 +  | del k (Branch3 (l, p, m, q, r)) = (case compare k q of
   1.188 +      LESS => (case compare k p of
   1.189          LESS => (case del k l of
   1.190            (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
   1.191          | (p', (true, l')) => (p', (false, case (m, r) of
   1.192 @@ -259,8 +273,12 @@
   1.193              Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
   1.194                Branch2 (mr, if_eq ord q' q, r'))))));
   1.195  
   1.196 +in
   1.197 +
   1.198  fun delete k t = snd (snd (del (SOME k) t));
   1.199  
   1.200 +end;
   1.201 +
   1.202  
   1.203  (* join and merge *)
   1.204