src/Pure/symtab.ML
changeset 4484 220ccae8a590
parent 4483 caf8ae95c61f
child 4485 697972696f71
equal deleted inserted replaced
4483:caf8ae95c61f 4484:220ccae8a590
     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 DUP of string
       
    12   exception DUPS of string list
       
    13   type 'a table
       
    14   val empty: 'a table
       
    15   val is_empty: '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 balance: 'a table -> 'a table
       
    22   val st_of_declist: (string list * 'a) list * 'a table -> 'a table
       
    23   val make: (string * 'a) list -> 'a table
       
    24   val dest: 'a table -> (string * 'a) list
       
    25   val extend: 'a table * (string * 'a) list -> 'a table
       
    26   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
       
    27   val lookup_multi: 'a list table * string -> 'a list
       
    28   val make_multi: (string * 'a) list -> 'a list table
       
    29   val dest_multi: 'a list table -> (string * 'a) list
       
    30 end;
       
    31 
       
    32 structure Symtab: SYMTAB =
       
    33 struct
       
    34 
       
    35 (*symbol table errors, such as from update_new*)
       
    36 exception DUP of string;
       
    37 exception DUPS of string list;
       
    38 
       
    39 datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
       
    40 
       
    41 
       
    42 val empty = Tip;
       
    43 
       
    44 fun is_empty Tip = true
       
    45   | is_empty _ = false;
       
    46 
       
    47 
       
    48 fun lookup (symtab: 'a table, key: string) : 'a option =
       
    49   let fun look  Tip  = None
       
    50         | look (Branch (key', entry, left, right)) =
       
    51             if      key < key' then look left
       
    52             else if key' < key then look right
       
    53             else  Some entry
       
    54   in look symtab end;
       
    55 
       
    56 
       
    57 fun find_first _ Tip = None
       
    58   | find_first pred (Branch (key, entry, left, right)) =
       
    59       (case find_first pred left of
       
    60         None =>
       
    61           if pred (key, entry) then Some (key, entry)
       
    62           else find_first pred right
       
    63       | some => some);
       
    64 
       
    65 
       
    66 (*update, allows overwriting of an entry*)
       
    67 fun update ((key: string, entry: 'a), symtab : 'a table)
       
    68   : 'a table =
       
    69   let fun upd  Tip  = Branch (key, entry, Tip, Tip)
       
    70         | upd (Branch(key', entry', left, right)) =
       
    71             if      key < key' then Branch (key', entry', upd left, right)
       
    72             else if key' < key then Branch (key', entry', left, upd right)
       
    73             else                    Branch (key, entry, left, right)
       
    74   in  upd symtab  end;
       
    75 
       
    76 (*Like update but fails if key is already defined in table.*)
       
    77 fun update_new ((key: string, entry: 'a), symtab : 'a table)
       
    78   : 'a table =
       
    79   let fun upd Tip = Branch (key, entry, Tip, Tip)
       
    80         | upd (Branch(key', entry', left, right)) =
       
    81             if      key < key' then Branch (key', entry', upd left, right)
       
    82             else if key' < key then Branch (key', entry', left, upd right)
       
    83             else  raise DUP(key)
       
    84   in  upd symtab  end;
       
    85 
       
    86 
       
    87 (*conversion of symbol table to sorted association list*)
       
    88 fun dest (symtab : 'a table) : (string * 'a) list =
       
    89   let fun ali (symtab, cont) = case symtab of
       
    90                 Tip => cont
       
    91         | Branch (key, entry, left, right) =>
       
    92             ali(left, (key, entry) :: ali(right, cont))
       
    93   in  ali (symtab, [])  end;
       
    94 
       
    95 
       
    96 (*Make a balanced tree of the first n members of the sorted alist (sal).
       
    97   Utility for the function balance.*)
       
    98 fun bal_of (sal, 0) = Tip
       
    99   | bal_of (sal, n) =
       
   100       let val mid = n div 2
       
   101       in  case  drop (mid, sal) of
       
   102             [] => bal_of (sal, mid)   (*should not occur*)
       
   103           | ((key, entry):: pairs) =>
       
   104                 Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
       
   105       end;
       
   106 
       
   107 
       
   108 fun balance symtab =
       
   109   let val sal = dest symtab
       
   110   in  bal_of (sal, length sal)  end;
       
   111 
       
   112 
       
   113 (*A "declaration" associates the same entry with a list of keys;
       
   114   does not allow overwriting of an entry*)
       
   115 fun decl_update_new ((keys : string list, entry: 'a), symtab)
       
   116   : 'a table =
       
   117   let fun decl (key, symtab) = update_new ((key, entry), symtab)
       
   118   in foldr decl (keys, symtab) end;
       
   119 
       
   120 (*Addition of a list of declarations to a symbol table*)
       
   121 fun st_of_declist (dl, symtab) =
       
   122   balance (foldr decl_update_new (dl, symtab));
       
   123 
       
   124 
       
   125 (* make, extend, merge tables *)
       
   126 
       
   127 fun eq_pair eq ((key1, entry1), (key2, entry2)) =
       
   128   key1 = key2 andalso eq (entry1, entry2);
       
   129 
       
   130 fun make alst =
       
   131   (case gen_duplicates eq_fst alst of
       
   132     [] => balance (foldr update_new (alst, Tip))
       
   133   | dups => raise DUPS (map fst dups));
       
   134 
       
   135 fun pre_extend eq (tab, alst) =
       
   136   generic_extend (eq_pair eq) dest make tab alst;
       
   137 
       
   138 fun extend (tab, alst) = pre_extend (K false) (tab, alst);
       
   139 
       
   140 fun merge eq (tab1, tab2) =
       
   141   generic_merge (eq_pair eq) dest make tab1 tab2;
       
   142 
       
   143 
       
   144 (* tables with multiple entries per key *)
       
   145 (*order of entries with same key is preserved*)
       
   146 
       
   147 fun lookup_multi (tab, key) =
       
   148   (case lookup (tab, key) of
       
   149     Some entries => entries
       
   150   | None => []);
       
   151 
       
   152 fun cons_entry ((key, entry), tab) =
       
   153   update ((key, entry :: lookup_multi (tab, key)), tab);
       
   154 
       
   155 fun make_multi alst =
       
   156   balance (foldr cons_entry (alst, Tip));
       
   157 
       
   158 fun dest_multi tab =
       
   159   List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
       
   160 
       
   161 
       
   162 (* map tables *)
       
   163 
       
   164 fun map _ Tip = Tip
       
   165   | map f (Branch (key, entry, left, right)) =
       
   166       Branch (key, f entry, map f left, map f right);
       
   167 
       
   168 end;
       
   169