src/Pure/symtab.ML
author wenzelm
Tue Aug 23 19:31:05 1994 +0200 (1994-08-23)
changeset 573 2fa5ef27bd0a
parent 563 e9bf62651beb
child 1415 cef540a0a10e
permissions -rw-r--r--
removed constant _constrain from Pure sig;
     1 (*  Title:      Pure/symtab.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1989  University of Cambridge
     5 
     6 Unbalanced binary trees indexed by strings; no way to delete an entry.
     7 *)
     8 
     9 signature SYMTAB =
    10 sig
    11   exception DUPLICATE of string
    12   exception DUPS of string list
    13   type 'a table
    14   val null: 'a table
    15   val is_null: 'a table -> bool
    16   val lookup: 'a table * string -> 'a option
    17   val find_first: (string * 'a -> bool) -> 'a table -> (string * 'a) option
    18   val update: (string * 'a) * 'a table -> 'a table
    19   val update_new: (string * 'a) * 'a table -> 'a table
    20   val map: ('a -> 'b) -> 'a table -> 'b table
    21   val alist_of: 'a table -> (string * 'a) list  (*obsolete*)
    22   val balance: 'a table -> 'a table
    23   val st_of_alist: (string * 'a) list * 'a table -> 'a table  (*obsolete*)
    24   val st_of_declist: (string list * 'a) list * 'a table -> 'a table
    25   val make: (string * 'a) list -> 'a table
    26   val dest: 'a table -> (string * 'a) list
    27   val extend: ('a * 'a -> bool) -> 'a table * (string * 'a) list -> 'a table
    28   val extend_new: 'a table * (string * 'a) list -> 'a table
    29   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    30   val lookup_multi: 'a list table * string -> 'a list
    31   val make_multi: (string * 'a) list -> 'a list table
    32   val dest_multi: 'a list table -> (string * 'a) list
    33 end;
    34 
    35 functor SymtabFun(): SYMTAB =
    36 struct
    37 
    38 (*symbol table errors, such as from update_new*)
    39 exception DUPLICATE of string;
    40 exception DUPS of string list;
    41 
    42 datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
    43 
    44 
    45 val null = Tip;
    46 
    47 fun is_null Tip = true
    48   | is_null _ = false;
    49 
    50 
    51 fun lookup (symtab: 'a table, key: string) : 'a option =
    52   let fun look  Tip  = None
    53         | look (Branch (key', entry, left, right)) =
    54             if      key < key' then look left
    55             else if key' < key then look right
    56             else  Some entry
    57   in look symtab end;
    58 
    59 
    60 fun find_first _ Tip = None
    61   | find_first pred (Branch (key, entry, left, right)) =
    62       (case find_first pred left of
    63         None =>
    64           if pred (key, entry) then Some (key, entry)
    65           else find_first pred right
    66       | some => some);
    67 
    68 
    69 (*update, allows overwriting of an entry*)
    70 fun update ((key: string, entry: 'a), symtab : 'a table)
    71   : 'a table =
    72   let fun upd  Tip  = Branch (key, entry, Tip, Tip)
    73         | upd (Branch(key', entry', left, right)) =
    74             if      key < key' then Branch (key', entry', upd left, right)
    75             else if key' < key then Branch (key', entry', left, upd right)
    76             else                    Branch (key, entry, left, right)
    77   in  upd symtab  end;
    78 
    79 (*Like update but fails if key is already defined in table.
    80   Allows st_of_alist, etc. to detect multiple definitions*)
    81 fun update_new ((key: string, entry: 'a), symtab : 'a table)
    82   : 'a table =
    83   let fun upd Tip = Branch (key, entry, Tip, Tip)
    84         | upd (Branch(key', entry', left, right)) =
    85             if      key < key' then Branch (key', entry', upd left, right)
    86             else if key' < key then Branch (key', entry', left, upd right)
    87             else  raise DUPLICATE(key)
    88   in  upd symtab  end;
    89 
    90 
    91 (*conversion of symbol table to sorted association list*)
    92 fun alist_of (symtab : 'a table) : (string * 'a) list =
    93   let fun ali (symtab, cont) = case symtab of
    94                 Tip => cont
    95         | Branch (key, entry, left, right) =>
    96             ali(left, (key, entry) :: ali(right, cont))
    97   in  ali (symtab, [])  end;
    98 
    99 val dest = alist_of;
   100 
   101 
   102 (*Make a balanced tree of the first n members of the sorted alist (sal).
   103   Utility for the function balance.*)
   104 fun bal_of (sal, 0) = Tip
   105   | bal_of (sal, n) =
   106       let val mid = n div 2
   107       in  case  drop (mid, sal) of
   108             [] => bal_of (sal, mid)   (*should not occur*)
   109           | ((key, entry):: pairs) =>
   110                 Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
   111       end;
   112 
   113 
   114 fun balance symtab =
   115   let val sal = alist_of symtab
   116   in  bal_of (sal, length sal)  end;
   117 
   118 
   119 (*Addition of association list to a symbol table*)
   120 fun st_of_alist (al, symtab) =
   121   foldr update_new (al, symtab);
   122 
   123 (*A "declaration" associates the same entry with a list of keys;
   124   does not allow overwriting of an entry*)
   125 fun decl_update_new ((keys : string list, entry: 'a), symtab)
   126   : 'a table =
   127   let fun decl (key, symtab) = update_new ((key, entry), symtab)
   128   in foldr decl (keys, symtab) end;
   129 
   130 (*Addition of a list of declarations to a symbol table*)
   131 fun st_of_declist (dl, symtab) =
   132   balance (foldr decl_update_new (dl, symtab));
   133 
   134 
   135 (* make, extend, merge tables *)
   136 
   137 fun eq_pair eq ((key1, entry1), (key2, entry2)) =
   138   key1 = key2 andalso eq (entry1, entry2);
   139 
   140 fun make alst =
   141   (case gen_duplicates eq_fst alst of
   142     [] => balance (st_of_alist (alst, Tip))
   143   | dups => raise DUPS (map fst dups));
   144 
   145 fun extend eq (tab, alst) =
   146   generic_extend (eq_pair eq) dest make tab alst;
   147 
   148 val extend_new = extend (K false);
   149 
   150 fun merge eq (tab1, tab2) =
   151   generic_merge (eq_pair eq) dest make tab1 tab2;
   152 
   153 
   154 (* tables with multiple entries per key *)
   155 (*order of entries with same key is preserved*)
   156 
   157 fun lookup_multi (tab, key) =
   158   (case lookup (tab, key) of
   159     Some entries => entries
   160   | None => []);
   161 
   162 fun cons_entry ((key, entry), tab) =
   163   update ((key, entry :: lookup_multi (tab, key)), tab);
   164 
   165 fun make_multi alst =
   166   balance (foldr cons_entry (alst, Tip));
   167 
   168 fun dest_multi tab =
   169   flat (map (fn (key, entries) => map (pair key) entries) (dest tab));
   170 
   171 
   172 (* map tables *)
   173 
   174 fun map _ Tip = Tip
   175   | map f (Branch (key, entry, left, right)) =
   176       Branch (key, f entry, map f left, map f right);
   177 
   178 end;
   179