added make, dest, extend_new;
authorwenzelm
Wed May 18 15:19:25 1994 +0200 (1994-05-18)
changeset 374caf9a9b7f605
parent 373 68400ea32f7b
child 375 d7ae7ac22d48
added make, dest, extend_new;
added exception DUPS;
src/Pure/symtab.ML
     1.1 --- a/src/Pure/symtab.ML	Tue May 17 14:42:34 1994 +0200
     1.2 +++ b/src/Pure/symtab.ML	Wed May 18 15:19:25 1994 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  signature SYMTAB =
     1.5  sig
     1.6    exception DUPLICATE of string
     1.7 +  exception DUPS of string list
     1.8    type 'a table
     1.9    val null: 'a table
    1.10    val is_null: 'a table -> bool
    1.11 @@ -19,7 +20,10 @@
    1.12    val balance: 'a table -> 'a table
    1.13    val st_of_alist: (string * 'a) list * 'a table -> 'a table
    1.14    val st_of_declist: (string list * 'a) list * 'a table -> 'a table
    1.15 +  val make: (string * 'a) list -> 'a table
    1.16 +  val dest: 'a table -> (string * 'a) list
    1.17    val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
    1.18 +  val extend_new: 'a table * (string * 'a) list -> 'a table
    1.19    val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.20    val lookup_multi: 'a list table * string -> 'a list
    1.21    val make_multi: (string * 'a) list -> 'a list table
    1.22 @@ -31,6 +35,7 @@
    1.23  
    1.24  (*symbol table errors, such as from update_new*)
    1.25  exception DUPLICATE of string;
    1.26 +exception DUPS of string list;
    1.27  
    1.28  datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
    1.29  
    1.30 @@ -78,6 +83,8 @@
    1.31              ali(left, (key, entry) :: ali(right, cont))
    1.32    in  ali (symtab, [])  end;
    1.33  
    1.34 +val dest = alist_of;
    1.35 +
    1.36  
    1.37  (*Make a balanced tree of the first n members of the sorted alist (sal).
    1.38    Utility for the function balance.*)
    1.39 @@ -112,18 +119,23 @@
    1.40    balance (foldr decl_update_new (dl, symtab));
    1.41  
    1.42  
    1.43 -(* extend, merge tables *)
    1.44 +(* make, extend, merge tables *)
    1.45  
    1.46  fun eq_pair eq ((key1, entry1), (key2, entry2)) =
    1.47    key1 = key2 andalso eq (entry1, entry2);
    1.48  
    1.49 -fun mk_tab alst = balance (st_of_alist (alst, Tip));
    1.50 +fun make alst =
    1.51 +  (case gen_duplicates eq_fst alst of
    1.52 +    [] => balance (st_of_alist (alst, Tip))
    1.53 +  | dups => raise DUPS (map fst dups));
    1.54  
    1.55  fun extend eq (tab, alst) =
    1.56 -  generic_extend (eq_pair eq) alist_of mk_tab tab alst;
    1.57 +  generic_extend (eq_pair eq) dest make tab alst;
    1.58 +
    1.59 +val extend_new = extend (K false);
    1.60  
    1.61  fun merge eq (tab1, tab2) =
    1.62 -  generic_merge (eq_pair eq) alist_of mk_tab tab1 tab2;
    1.63 +  generic_merge (eq_pair eq) dest make tab1 tab2;
    1.64  
    1.65  
    1.66  (* tables with multiple entries per key *)
    1.67 @@ -141,7 +153,7 @@
    1.68    balance (foldr cons_entry (alst, Tip));
    1.69  
    1.70  fun dest_multi tab =
    1.71 -  flat (map (fn (key, entries) => map (pair key) entries) (alist_of tab));
    1.72 +  flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
    1.73  
    1.74  
    1.75  end;