--- a/src/Pure/symtab.ML Wed Jan 19 14:10:54 1994 +0100
+++ b/src/Pure/symtab.ML Wed Jan 19 14:12:40 1994 +0100
@@ -1,37 +1,38 @@
-(* Title: symtab
+(* Title: Pure/symtab.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1989 University of Cambridge
-*)
-(*Unbalanced binary trees indexed by strings
- No way to delete an entry
- could generalize alist_of to a traversal functional
+Unbalanced binary trees indexed by strings; no way to delete an entry.
*)
-signature SYMTAB =
+signature SYMTAB =
sig
- type 'a table
- val alist_of : 'a table -> (string*'a) list
- val balance : 'a table -> 'a table
- val lookup : 'a table * string -> 'a option
- val null : 'a table
- val is_null : 'a table -> bool
- val st_of_alist : (string*'a)list * 'a table -> 'a table
- val st_of_declist : (string list * 'a)list * 'a table -> 'a table
- val update : (string*'a) * 'a table -> 'a table
- val update_new : (string*'a) * 'a table -> 'a table
- exception DUPLICATE of string
+ exception DUPLICATE of string
+ type 'a table
+ val null: 'a table
+ val is_null: 'a table -> bool
+ val lookup: 'a table * string -> 'a option
+ val update: (string * 'a) * 'a table -> 'a table
+ val update_new: (string * 'a) * 'a table -> 'a table
+ val alist_of: 'a table -> (string * 'a) list
+ val balance: 'a table -> 'a table
+ val st_of_alist: (string * 'a) list * 'a table -> 'a table
+ val st_of_declist: (string list * 'a) list * 'a table -> 'a table
+ val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
+ val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+ val lookup_multi: 'a list table * string -> 'a list
+ val make_multi: (string * 'a) list -> 'a list table
+ val dest_multi: 'a list table -> (string * 'a) list
end;
-
-functor SymtabFun () : SYMTAB =
+functor SymtabFun(): SYMTAB =
struct
(*symbol table errors, such as from update_new*)
exception DUPLICATE of string;
-datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
+datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
val null = Tip;
@@ -40,42 +41,42 @@
| is_null _ = false;
-fun lookup (symtab: 'a table, key: string) : 'a option =
+fun lookup (symtab: 'a table, key: string) : 'a option =
let fun look Tip = None
- | look (Branch (key',entry,left,right)) =
- if key < key' then look left
- else if key' < key then look right
- else Some entry
+ | look (Branch (key', entry, left, right)) =
+ if key < key' then look left
+ else if key' < key then look right
+ else Some entry
in look symtab end;
(*update, allows overwriting of an entry*)
fun update ((key: string, entry: 'a), symtab : 'a table)
: 'a table =
- let fun upd Tip = Branch (key,entry,Tip,Tip)
- | upd (Branch(key',entry',left,right)) =
- if key < key' then Branch (key',entry', upd left, right)
- else if key' < key then Branch (key',entry',left, upd right)
- else Branch (key,entry,left,right)
+ let fun upd Tip = Branch (key, entry, Tip, Tip)
+ | upd (Branch(key', entry', left, right)) =
+ if key < key' then Branch (key', entry', upd left, right)
+ else if key' < key then Branch (key', entry', left, upd right)
+ else Branch (key, entry, left, right)
in upd symtab end;
(*Like update but fails if key is already defined in table.
Allows st_of_alist, etc. to detect multiple definitions*)
fun update_new ((key: string, entry: 'a), symtab : 'a table)
: 'a table =
- let fun upd Tip = Branch (key,entry,Tip,Tip)
- | upd (Branch(key',entry',left,right)) =
- if key < key' then Branch (key',entry', upd left, right)
- else if key' < key then Branch (key',entry',left, upd right)
- else raise DUPLICATE(key)
+ let fun upd Tip = Branch (key, entry, Tip, Tip)
+ | upd (Branch(key', entry', left, right)) =
+ if key < key' then Branch (key', entry', upd left, right)
+ else if key' < key then Branch (key', entry', left, upd right)
+ else raise DUPLICATE(key)
in upd symtab end;
(*conversion of symbol table to sorted association list*)
fun alist_of (symtab : 'a table) : (string * 'a) list =
- let fun ali (symtab,cont) = case symtab of
- Tip => cont
- | Branch (key,entry,left,right) =>
- ali(left, (key,entry) :: ali(right,cont))
- in ali (symtab,[]) end;
+ let fun ali (symtab, cont) = case symtab of
+ Tip => cont
+ | Branch (key, entry, left, right) =>
+ ali(left, (key, entry) :: ali(right, cont))
+ in ali (symtab, []) end;
(*Make a balanced tree of the first n members of the sorted alist (sal).
@@ -83,10 +84,10 @@
fun bal_of (sal, 0) = Tip
| bal_of (sal, n) =
let val mid = n div 2
- in case drop (mid,sal) of
- [] => bal_of (sal, mid) (*should not occur*)
- | ((key,entry):: pairs) =>
- Branch(key,entry, bal_of(sal,mid), bal_of(pairs, n-mid-1))
+ in case drop (mid, sal) of
+ [] => bal_of (sal, mid) (*should not occur*)
+ | ((key, entry):: pairs) =>
+ Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
end;
@@ -97,18 +98,51 @@
(*Addition of association list to a symbol table*)
fun st_of_alist (al, symtab) =
- foldr update_new (al, symtab);
+ foldr update_new (al, symtab);
(*A "declaration" associates the same entry with a list of keys;
does not allow overwriting of an entry*)
fun decl_update_new ((keys : string list, entry: 'a), symtab)
: 'a table =
- let fun decl (key,symtab) = update_new((key,entry), symtab)
- in foldr decl (keys, symtab) end;
+ let fun decl (key, symtab) = update_new ((key, entry), symtab)
+ in foldr decl (keys, symtab) end;
(*Addition of a list of declarations to a symbol table*)
fun st_of_declist (dl, symtab) =
- balance (foldr decl_update_new (dl, symtab))
+ balance (foldr decl_update_new (dl, symtab));
+
+
+(* extend, merge tables *)
+
+fun eq_pair eq ((key1, entry1), (key2, entry2)) =
+ key1 = key2 andalso eq (entry1, entry2);
+
+fun mk_tab alst = balance (st_of_alist (alst, Tip));
+
+fun extend eq (tab, alst) =
+ generic_extend (eq_pair eq) alist_of mk_tab tab alst;
+
+fun merge eq (tab1, tab2) =
+ generic_merge (eq_pair eq) alist_of mk_tab tab1 tab2;
+
+
+(* tables with multiple entries per key *)
+(*order of entries with same key is preserved*)
+
+fun lookup_multi (tab, key) =
+ (case lookup (tab, key) of
+ Some entries => entries
+ | None => []);
+
+fun cons_entry ((key, entry), tab) =
+ update ((key, entry :: lookup_multi (tab, key)), tab);
+
+fun make_multi alst =
+ balance (foldr cons_entry (alst, Tip));
+
+fun dest_multi tab =
+ flat (map (fn (key, entries) => map (pair key) entries) (alist_of tab));
+
end;