# HG changeset patch # User wenzelm # Date 758985160 -3600 # Node ID 1b3bee8d5d7e205d96f12b9191bbe63bd488e10a # Parent efd6b4bb14dda99aaf5038f2aba06bdb3e4219d2 minor cleanup; added extend, merge; added {lookup,make,dest}_multi; diff -r efd6b4bb14dd -r 1b3bee8d5d7e src/Pure/symtab.ML --- 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;