wenzelm@6118: (* Title: Pure/General/table.ML wenzelm@5015: ID: $Id$ berghofe@15014: Author: Markus Wenzel and Stefan Berghofer, TU Muenchen wenzelm@5015: wenzelm@16342: Generic tables. Efficient purely functional implementation using wenzelm@16342: balanced 2-3 trees. wenzelm@5015: *) wenzelm@5015: wenzelm@5015: signature KEY = wenzelm@5015: sig wenzelm@5015: type key wenzelm@5015: val ord: key * key -> order wenzelm@5015: end; wenzelm@5015: wenzelm@5015: signature TABLE = wenzelm@5015: sig wenzelm@5015: type key wenzelm@5015: type 'a table wenzelm@5015: exception DUP of key wenzelm@19031: exception SAME berghofe@15014: exception UNDEF of key wenzelm@5015: val empty: 'a table wenzelm@5015: val is_empty: 'a table -> bool wenzelm@5681: val map: ('a -> 'b) -> 'a table -> 'b table wenzelm@16446: val map': (key -> 'a -> 'b) -> 'a table -> 'b table wenzelm@16446: val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a wenzelm@28334: val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a haftmann@17579: val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a wenzelm@5015: val dest: 'a table -> (key * 'a) list wenzelm@5681: val keys: 'a table -> key list wenzelm@27508: val exists: (key * 'a -> bool) -> 'a table -> bool wenzelm@27508: val forall: (key * 'a -> bool) -> 'a table -> bool wenzelm@27508: val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option berghofe@8409: val min_key: 'a table -> key option obua@15160: val max_key: 'a table -> key option wenzelm@16887: val defined: 'a table -> key -> bool wenzelm@17412: val lookup: 'a table -> key -> 'a option wenzelm@17412: val update: (key * 'a) -> 'a table -> 'a table wenzelm@17412: val update_new: (key * 'a) -> 'a table -> 'a table (*exception DUP*) haftmann@17179: val default: key * 'a -> 'a table -> 'a table wenzelm@15665: val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table haftmann@20141: val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table wenzelm@23655: val make: (key * 'a) list -> 'a table (*exception DUP*) wenzelm@19031: val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> wenzelm@23655: 'a table * 'a table -> 'a table (*exception DUP*) wenzelm@23655: val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*) wenzelm@15665: val delete: key -> 'a table -> 'a table (*exception UNDEF*) wenzelm@15761: val delete_safe: key -> 'a table -> 'a table wenzelm@16466: val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool wenzelm@15761: val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table (*exception DUP*) wenzelm@16139: val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table wenzelm@18946: val lookup_list: 'a list table -> key -> 'a list wenzelm@25391: val cons_list: (key * 'a) -> 'a list table -> 'a list table wenzelm@19506: val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table wenzelm@18946: val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table wenzelm@25391: val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table wenzelm@18946: val make_list: (key * 'a) list -> 'a list table wenzelm@18946: val dest_list: 'a list table -> (key * 'a) list wenzelm@18946: val merge_list: ('a * 'a -> bool) -> wenzelm@23655: 'a list table * 'a list table -> 'a list table (*exception DUP*) wenzelm@5015: end; wenzelm@5015: wenzelm@5015: functor TableFun(Key: KEY): TABLE = wenzelm@5015: struct wenzelm@5015: wenzelm@5015: wenzelm@5015: (* datatype table *) wenzelm@5015: wenzelm@5015: type key = Key.key; wenzelm@5015: wenzelm@5015: datatype 'a table = wenzelm@5015: Empty | wenzelm@5015: Branch2 of 'a table * (key * 'a) * 'a table | wenzelm@5015: Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table; wenzelm@5015: wenzelm@5015: exception DUP of key; wenzelm@5015: wenzelm@5015: wenzelm@5681: (* empty *) wenzelm@5681: wenzelm@5015: val empty = Empty; wenzelm@5015: wenzelm@5015: fun is_empty Empty = true wenzelm@5015: | is_empty _ = false; wenzelm@5015: wenzelm@5681: wenzelm@5681: (* map and fold combinators *) wenzelm@5681: wenzelm@16657: fun map_table f = wenzelm@16657: let wenzelm@16657: fun map Empty = Empty wenzelm@16657: | map (Branch2 (left, (k, x), right)) = wenzelm@16657: Branch2 (map left, (k, f k x), map right) wenzelm@16657: | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = wenzelm@16657: Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right); wenzelm@16657: in map end; wenzelm@5681: wenzelm@16657: fun fold_table f = wenzelm@16657: let wenzelm@16657: fun fold Empty x = x wenzelm@16657: | fold (Branch2 (left, p, right)) x = wenzelm@16657: fold right (f p (fold left x)) wenzelm@16657: | fold (Branch3 (left, p1, mid, p2, right)) x = wenzelm@16657: fold right (f p2 (fold mid (f p1 (fold left x)))); wenzelm@16657: in fold end; wenzelm@5681: wenzelm@28334: fun fold_rev_table f = wenzelm@28334: let wenzelm@28334: fun fold Empty x = x wenzelm@28334: | fold (Branch2 (left, p, right)) x = wenzelm@28334: fold left (f p (fold right x)) wenzelm@28334: | fold (Branch3 (left, p1, mid, p2, right)) x = wenzelm@28334: fold left (f p1 (fold mid (f p2 (fold right x)))); wenzelm@28334: in fold end; wenzelm@28334: wenzelm@17709: fun fold_map_table f = haftmann@17579: let haftmann@17579: fun fold_map Empty s = (Empty, s) haftmann@17579: | fold_map (Branch2 (left, p as (k, x), right)) s = haftmann@17579: s haftmann@17579: |> fold_map left haftmann@17579: ||>> f p haftmann@17579: ||>> fold_map right haftmann@17579: |-> (fn ((l, e), r) => pair (Branch2 (l, (k, e), r))) haftmann@17579: | fold_map (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) s = haftmann@17579: s haftmann@17579: |> fold_map left haftmann@17579: ||>> f p1 haftmann@17579: ||>> fold_map mid haftmann@17579: ||>> f p2 haftmann@17579: ||>> fold_map right haftmann@17579: |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r))) haftmann@17579: in fold_map end; haftmann@17579: wenzelm@28334: fun dest tab = fold_rev_table cons tab []; wenzelm@28334: fun keys tab = fold_rev_table (cons o #1) tab []; wenzelm@16192: wenzelm@27508: fun get_first f tab = wenzelm@27508: let wenzelm@27508: exception FOUND of 'b option; wenzelm@27508: fun get entry () = (case f entry of NONE => () | some => raise FOUND some); wenzelm@27508: in (fold_table get tab (); NONE) handle FOUND res => res end; wenzelm@16192: wenzelm@27508: fun exists pred = wenzelm@27508: is_some o get_first (fn entry => if pred entry then SOME () else NONE); wenzelm@16192: wenzelm@16192: fun forall pred = not o exists (not o pred); wenzelm@16192: wenzelm@27508: wenzelm@27508: (* min/max keys *) wenzelm@5015: skalberg@15531: fun min_key Empty = NONE wenzelm@16864: | min_key (Branch2 (Empty, (k, _), _)) = SOME k wenzelm@16864: | min_key (Branch3 (Empty, (k, _), _, _, _)) = SOME k wenzelm@16864: | min_key (Branch2 (left, _, _)) = min_key left wenzelm@16864: | min_key (Branch3 (left, _, _, _, _)) = min_key left; berghofe@8409: skalberg@15531: fun max_key Empty = NONE wenzelm@16864: | max_key (Branch2 (_, (k, _), Empty)) = SOME k wenzelm@16864: | max_key (Branch3 (_, _, _, (k, _), Empty)) = SOME k wenzelm@16864: | max_key (Branch2 (_, _, right)) = max_key right wenzelm@16864: | max_key (Branch3 (_, _, _, _, right)) = max_key right; wenzelm@15665: wenzelm@5015: wenzelm@5015: (* lookup *) wenzelm@5015: wenzelm@19031: fun lookup tab key = wenzelm@19031: let wenzelm@19031: fun look Empty = NONE wenzelm@19031: | look (Branch2 (left, (k, x), right)) = wenzelm@19031: (case Key.ord (key, k) of wenzelm@19031: LESS => look left wenzelm@19031: | EQUAL => SOME x wenzelm@19031: | GREATER => look right) wenzelm@19031: | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = wenzelm@19031: (case Key.ord (key, k1) of wenzelm@19031: LESS => look left wenzelm@19031: | EQUAL => SOME x1 wenzelm@19031: | GREATER => wenzelm@19031: (case Key.ord (key, k2) of wenzelm@19031: LESS => look mid wenzelm@19031: | EQUAL => SOME x2 wenzelm@19031: | GREATER => look right)); wenzelm@19031: in look tab end; wenzelm@5015: wenzelm@19031: fun defined tab key = wenzelm@19031: let wenzelm@19031: fun def Empty = false wenzelm@19031: | def (Branch2 (left, (k, x), right)) = wenzelm@19031: (case Key.ord (key, k) of wenzelm@19031: LESS => def left wenzelm@19031: | EQUAL => true wenzelm@19031: | GREATER => def right) wenzelm@19031: | def (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = wenzelm@19031: (case Key.ord (key, k1) of wenzelm@19031: LESS => def left wenzelm@19031: | EQUAL => true wenzelm@19031: | GREATER => wenzelm@19031: (case Key.ord (key, k2) of wenzelm@19031: LESS => def mid wenzelm@19031: | EQUAL => true wenzelm@19031: | GREATER => def right)); wenzelm@19031: in def tab end; wenzelm@16887: wenzelm@5015: wenzelm@19031: (* modify *) wenzelm@5015: wenzelm@5015: datatype 'a growth = wenzelm@5015: Stay of 'a table | wenzelm@5015: Sprout of 'a table * (key * 'a) * 'a table; wenzelm@5015: wenzelm@15761: exception SAME; wenzelm@15761: wenzelm@15665: fun modify key f tab = wenzelm@15665: let wenzelm@15665: fun modfy Empty = Sprout (Empty, (key, f NONE), Empty) wenzelm@15665: | modfy (Branch2 (left, p as (k, x), right)) = wenzelm@15665: (case Key.ord (key, k) of wenzelm@15665: LESS => wenzelm@15665: (case modfy left of wenzelm@15665: Stay left' => Stay (Branch2 (left', p, right)) wenzelm@15665: | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right))) wenzelm@15665: | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right)) wenzelm@15665: | GREATER => wenzelm@15665: (case modfy right of wenzelm@15665: Stay right' => Stay (Branch2 (left, p, right')) wenzelm@15665: | Sprout (right1, q, right2) => wenzelm@15665: Stay (Branch3 (left, p, right1, q, right2)))) wenzelm@15665: | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) = wenzelm@15665: (case Key.ord (key, k1) of wenzelm@5015: LESS => wenzelm@15665: (case modfy left of wenzelm@15665: Stay left' => Stay (Branch3 (left', p1, mid, p2, right)) wenzelm@15665: | Sprout (left1, q, left2) => wenzelm@15665: Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right))) wenzelm@15665: | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right)) wenzelm@5015: | GREATER => wenzelm@15665: (case Key.ord (key, k2) of wenzelm@15665: LESS => wenzelm@15665: (case modfy mid of wenzelm@15665: Stay mid' => Stay (Branch3 (left, p1, mid', p2, right)) wenzelm@15665: | Sprout (mid1, q, mid2) => wenzelm@15665: Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right))) wenzelm@15665: | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right)) wenzelm@15665: | GREATER => wenzelm@15665: (case modfy right of wenzelm@15665: Stay right' => Stay (Branch3 (left, p1, mid, p2, right')) wenzelm@15665: | Sprout (right1, q, right2) => wenzelm@15665: Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2))))); wenzelm@5015: wenzelm@15665: in wenzelm@15665: (case modfy tab of wenzelm@15665: Stay tab' => tab' wenzelm@15665: | Sprout br => Branch2 br) wenzelm@15665: handle SAME => tab wenzelm@15665: end; wenzelm@5015: wenzelm@17412: fun update (key, x) tab = modify key (fn _ => x) tab; wenzelm@17412: fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab; wenzelm@17709: fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab; wenzelm@15761: fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x); wenzelm@27783: fun map_default (key, x) f = modify key (fn NONE => f x | SOME y => f y); wenzelm@5015: wenzelm@5015: berghofe@15014: (* delete *) berghofe@15014: wenzelm@15665: exception UNDEF of key; wenzelm@15665: wenzelm@15665: local wenzelm@15665: wenzelm@15665: fun compare NONE (k2, _) = LESS wenzelm@15665: | compare (SOME k1) (k2, _) = Key.ord (k1, k2); berghofe@15014: berghofe@15014: fun if_eq EQUAL x y = x berghofe@15014: | if_eq _ x y = y; berghofe@15014: skalberg@15531: fun del (SOME k) Empty = raise UNDEF k skalberg@15531: | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty)) skalberg@15531: | del NONE (Branch3 (Empty, p, Empty, q, Empty)) = berghofe@15014: (p, (false, Branch2 (Empty, q, Empty))) wenzelm@15665: | del k (Branch2 (Empty, p, Empty)) = (case compare k p of wenzelm@16002: EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k)) wenzelm@15665: | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of berghofe@15014: EQUAL => (p, (false, Branch2 (Empty, q, Empty))) wenzelm@15665: | _ => (case compare k q of berghofe@15014: EQUAL => (q, (false, Branch2 (Empty, p, Empty))) wenzelm@16002: | _ => raise UNDEF (the k))) wenzelm@15665: | del k (Branch2 (l, p, r)) = (case compare k p of berghofe@15014: LESS => (case del k l of berghofe@15014: (p', (false, l')) => (p', (false, Branch2 (l', p, r))) berghofe@15014: | (p', (true, l')) => (p', case r of berghofe@15014: Branch2 (rl, rp, rr) => berghofe@15014: (true, Branch3 (l', p, rl, rp, rr)) berghofe@15014: | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2 berghofe@15014: (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr))))) skalberg@15531: | ord => (case del (if_eq ord NONE k) r of berghofe@15014: (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r'))) berghofe@15014: | (p', (true, r')) => (p', case l of berghofe@15014: Branch2 (ll, lp, lr) => berghofe@15014: (true, Branch3 (ll, lp, lr, if_eq ord p' p, r')) berghofe@15014: | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2 berghofe@15014: (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r')))))) wenzelm@15665: | del k (Branch3 (l, p, m, q, r)) = (case compare k q of wenzelm@15665: LESS => (case compare k p of berghofe@15014: LESS => (case del k l of berghofe@15014: (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r))) berghofe@15014: | (p', (true, l')) => (p', (false, case (m, r) of berghofe@15014: (Branch2 (ml, mp, mr), Branch2 _) => berghofe@15014: Branch2 (Branch3 (l', p, ml, mp, mr), q, r) berghofe@15014: | (Branch3 (ml, mp, mm, mq, mr), _) => berghofe@15014: Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r) berghofe@15014: | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) => berghofe@15014: Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp, berghofe@15014: Branch2 (rm, rq, rr))))) skalberg@15531: | ord => (case del (if_eq ord NONE k) m of berghofe@15014: (p', (false, m')) => berghofe@15014: (p', (false, Branch3 (l, if_eq ord p' p, m', q, r))) berghofe@15014: | (p', (true, m')) => (p', (false, case (l, r) of berghofe@15014: (Branch2 (ll, lp, lr), Branch2 _) => berghofe@15014: Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r) berghofe@15014: | (Branch3 (ll, lp, lm, lq, lr), _) => berghofe@15014: Branch3 (Branch2 (ll, lp, lm), lq, berghofe@15014: Branch2 (lr, if_eq ord p' p, m'), q, r) berghofe@15014: | (_, Branch3 (rl, rp, rm, rq, rr)) => berghofe@15014: Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp, berghofe@15014: Branch2 (rm, rq, rr)))))) skalberg@15531: | ord => (case del (if_eq ord NONE k) r of berghofe@15014: (q', (false, r')) => berghofe@15014: (q', (false, Branch3 (l, p, m, if_eq ord q' q, r'))) berghofe@15014: | (q', (true, r')) => (q', (false, case (l, m) of berghofe@15014: (Branch2 _, Branch2 (ml, mp, mr)) => berghofe@15014: Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r')) berghofe@15014: | (_, Branch3 (ml, mp, mm, mq, mr)) => berghofe@15014: Branch3 (l, p, Branch2 (ml, mp, mm), mq, berghofe@15014: Branch2 (mr, if_eq ord q' q, r')) berghofe@15014: | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) => berghofe@15014: Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp, berghofe@15014: Branch2 (mr, if_eq ord q' q, r')))))); berghofe@15014: wenzelm@15665: in wenzelm@15665: wenzelm@15761: fun delete key tab = snd (snd (del (SOME key) tab)); wenzelm@15761: fun delete_safe key tab = delete key tab handle UNDEF _ => tab; berghofe@15014: wenzelm@15665: end; wenzelm@15665: berghofe@15014: wenzelm@19031: (* membership operations *) wenzelm@16466: wenzelm@16466: fun member eq tab (key, x) = wenzelm@17412: (case lookup tab key of wenzelm@16466: NONE => false wenzelm@16466: | SOME y => eq (x, y)); wenzelm@15761: wenzelm@15761: fun insert eq (key, x) = wenzelm@15761: modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key); wenzelm@15761: wenzelm@15761: fun remove eq (key, x) tab = wenzelm@17412: (case lookup tab key of wenzelm@15761: NONE => tab wenzelm@15761: | SOME y => if eq (x, y) then delete key tab else tab); wenzelm@15761: wenzelm@15761: wenzelm@19031: (* simultaneous modifications *) wenzelm@19031: haftmann@29004: fun make entries = fold update_new entries empty; wenzelm@5015: wenzelm@12287: fun join f (table1, table2) = wenzelm@23655: let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; wenzelm@23655: in fold_table add table2 table1 end; wenzelm@12287: wenzelm@19031: fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); wenzelm@5015: wenzelm@5015: wenzelm@19031: (* list tables *) wenzelm@15761: wenzelm@18946: fun lookup_list tab key = these (lookup tab key); wenzelm@25391: wenzelm@25391: fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab; wenzelm@5015: wenzelm@20124: fun insert_list eq (key, x) = wenzelm@20124: modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs); wenzelm@25391: wenzelm@18946: fun remove_list eq (key, x) tab = wenzelm@15761: map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab wenzelm@15761: handle UNDEF _ => delete key tab; wenzelm@5015: wenzelm@25391: fun update_list eq (key, x) = wenzelm@25391: modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) => wenzelm@25391: if eq (x, y) then raise SAME else Library.update eq x xs); wenzelm@25391: wenzelm@25391: fun make_list args = fold_rev cons_list args empty; wenzelm@19482: fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); wenzelm@19031: fun merge_list eq = join (fn _ => Library.merge eq); wenzelm@5015: wenzelm@5015: wenzelm@5681: (*final declarations of this structure!*) wenzelm@16446: fun map f = map_table (K f); wenzelm@16446: val map' = map_table; wenzelm@16446: val fold = fold_table; wenzelm@28334: val fold_rev = fold_rev_table; haftmann@17579: val fold_map = fold_map_table; wenzelm@5015: wenzelm@5015: end; wenzelm@5015: wenzelm@16342: structure Inttab = TableFun(type key = int val ord = int_ord); wenzelm@16687: structure Symtab = TableFun(type key = string val ord = fast_string_ord);