# HG changeset patch # User berghofe # Date 1088861218 -7200 # Node ID 97ab70c3d9552ae5614bf0ba8d5599c8129053d1 # Parent 34264f5e469148496dafeab48b4796c0d7d16a81 Added delete operation. diff -r 34264f5e4691 -r 97ab70c3d955 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Jul 01 12:29:53 2004 +0200 +++ b/src/Pure/General/table.ML Sat Jul 03 15:26:58 2004 +0200 @@ -1,10 +1,9 @@ (* Title: Pure/General/table.ML ID: $Id$ - Author: Markus Wenzel, TU Muenchen + Author: Markus Wenzel and Stefan Berghofer, TU Muenchen Generic tables and tables indexed by strings. Efficient purely -functional implementation using balanced 2-3 trees. No delete -operation (may store options instead). +functional implementation using balanced 2-3 trees. *) signature KEY = @@ -19,6 +18,7 @@ type 'a table exception DUP of key exception DUPS of key list + exception UNDEF of key val empty: 'a table val is_empty: 'a table -> bool val map: ('a -> 'b) -> 'a table -> 'b table @@ -34,6 +34,7 @@ val extend: 'a table * (key * 'a) list -> 'a table (*exception DUPS*) val join: ('a * 'a -> 'a option) -> 'a table * 'a table -> 'a table (*exception DUPS*) val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*) + val delete: key -> 'a table -> 'a table (* exception UNDEF *) val lookup_multi: 'a list table * key -> 'a list val update_multi: (key * 'a) * 'a list table -> 'a list table val make_multi: (key * 'a) list -> 'a list table @@ -181,6 +182,82 @@ fun make pairs = extend (empty, pairs); +(* delete *) + +fun compare' None (k2, _) = LESS + | compare' (Some k1) (k2, _) = Key.ord (k1, k2); + +fun if_eq EQUAL x y = x + | if_eq _ x y = y; + +exception UNDEF of key; + +fun del (Some k) Empty = raise UNDEF k + | del None (Branch2 (Empty, p, Empty)) = (p, (true, Empty)) + | del None (Branch3 (Empty, p, Empty, q, Empty)) = + (p, (false, Branch2 (Empty, q, Empty))) + | del k (Branch2 (Empty, p, Empty)) = (case compare' k p of + EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k)) + | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare' k p of + EQUAL => (p, (false, Branch2 (Empty, q, Empty))) + | _ => (case compare' k q of + EQUAL => (q, (false, Branch2 (Empty, p, Empty))) + | _ => raise UNDEF (the k))) + | del k (Branch2 (l, p, r)) = (case compare' k p of + LESS => (case del k l of + (p', (false, l')) => (p', (false, Branch2 (l', p, r))) + | (p', (true, l')) => (p', case r of + Branch2 (rl, rp, rr) => + (true, Branch3 (l', p, rl, rp, rr)) + | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2 + (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr))))) + | ord => (case del (if_eq ord None k) r of + (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r'))) + | (p', (true, r')) => (p', case l of + Branch2 (ll, lp, lr) => + (true, Branch3 (ll, lp, lr, if_eq ord p' p, r')) + | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2 + (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r')))))) + | del k (Branch3 (l, p, m, q, r)) = (case compare' k q of + LESS => (case compare' k p of + LESS => (case del k l of + (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r))) + | (p', (true, l')) => (p', (false, case (m, r) of + (Branch2 (ml, mp, mr), Branch2 _) => + Branch2 (Branch3 (l', p, ml, mp, mr), q, r) + | (Branch3 (ml, mp, mm, mq, mr), _) => + Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r) + | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) => + Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp, + Branch2 (rm, rq, rr))))) + | ord => (case del (if_eq ord None k) m of + (p', (false, m')) => + (p', (false, Branch3 (l, if_eq ord p' p, m', q, r))) + | (p', (true, m')) => (p', (false, case (l, r) of + (Branch2 (ll, lp, lr), Branch2 _) => + Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r) + | (Branch3 (ll, lp, lm, lq, lr), _) => + Branch3 (Branch2 (ll, lp, lm), lq, + Branch2 (lr, if_eq ord p' p, m'), q, r) + | (_, Branch3 (rl, rp, rm, rq, rr)) => + Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp, + Branch2 (rm, rq, rr)))))) + | ord => (case del (if_eq ord None k) r of + (q', (false, r')) => + (q', (false, Branch3 (l, p, m, if_eq ord q' q, r'))) + | (q', (true, r')) => (q', (false, case (l, m) of + (Branch2 _, Branch2 (ml, mp, mr)) => + Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r')) + | (_, Branch3 (ml, mp, mm, mq, mr)) => + Branch3 (l, p, Branch2 (ml, mp, mm), mq, + Branch2 (mr, if_eq ord q' q, r')) + | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) => + Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp, + Branch2 (mr, if_eq ord q' q, r')))))); + +fun delete k t = snd (snd (del (Some k) t)); + + (* join and merge *) fun join f (table1, table2) =