src/Pure/symtab.ML
changeset 4484 220ccae8a590
parent 4483 caf8ae95c61f
child 4485 697972696f71
     1.1 --- a/src/Pure/symtab.ML	Sun Dec 28 14:54:38 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,169 +0,0 @@
     1.4 -(*  Title:      Pure/symtab.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1989  University of Cambridge
     1.8 -
     1.9 -Unbalanced binary trees indexed by strings; no way to delete an entry.
    1.10 -*)
    1.11 -
    1.12 -signature SYMTAB =
    1.13 -sig
    1.14 -  exception DUP of string
    1.15 -  exception DUPS of string list
    1.16 -  type 'a table
    1.17 -  val empty: 'a table
    1.18 -  val is_empty: 'a table -> bool
    1.19 -  val lookup: 'a table * string -> 'a option
    1.20 -  val find_first: (string * 'a -> bool) -> 'a table -> (string * 'a) option
    1.21 -  val update: (string * 'a) * 'a table -> 'a table
    1.22 -  val update_new: (string * 'a) * 'a table -> 'a table
    1.23 -  val map: ('a -> 'b) -> 'a table -> 'b table
    1.24 -  val balance: 'a table -> 'a table
    1.25 -  val st_of_declist: (string list * 'a) list * 'a table -> 'a table
    1.26 -  val make: (string * 'a) list -> 'a table
    1.27 -  val dest: 'a table -> (string * 'a) list
    1.28 -  val extend: 'a table * (string * 'a) list -> 'a table
    1.29 -  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.30 -  val lookup_multi: 'a list table * string -> 'a list
    1.31 -  val make_multi: (string * 'a) list -> 'a list table
    1.32 -  val dest_multi: 'a list table -> (string * 'a) list
    1.33 -end;
    1.34 -
    1.35 -structure Symtab: SYMTAB =
    1.36 -struct
    1.37 -
    1.38 -(*symbol table errors, such as from update_new*)
    1.39 -exception DUP of string;
    1.40 -exception DUPS of string list;
    1.41 -
    1.42 -datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
    1.43 -
    1.44 -
    1.45 -val empty = Tip;
    1.46 -
    1.47 -fun is_empty Tip = true
    1.48 -  | is_empty _ = false;
    1.49 -
    1.50 -
    1.51 -fun lookup (symtab: 'a table, key: string) : 'a option =
    1.52 -  let fun look  Tip  = None
    1.53 -        | look (Branch (key', entry, left, right)) =
    1.54 -            if      key < key' then look left
    1.55 -            else if key' < key then look right
    1.56 -            else  Some entry
    1.57 -  in look symtab end;
    1.58 -
    1.59 -
    1.60 -fun find_first _ Tip = None
    1.61 -  | find_first pred (Branch (key, entry, left, right)) =
    1.62 -      (case find_first pred left of
    1.63 -        None =>
    1.64 -          if pred (key, entry) then Some (key, entry)
    1.65 -          else find_first pred right
    1.66 -      | some => some);
    1.67 -
    1.68 -
    1.69 -(*update, allows overwriting of an entry*)
    1.70 -fun update ((key: string, entry: 'a), symtab : 'a table)
    1.71 -  : 'a table =
    1.72 -  let fun upd  Tip  = Branch (key, entry, Tip, Tip)
    1.73 -        | upd (Branch(key', entry', left, right)) =
    1.74 -            if      key < key' then Branch (key', entry', upd left, right)
    1.75 -            else if key' < key then Branch (key', entry', left, upd right)
    1.76 -            else                    Branch (key, entry, left, right)
    1.77 -  in  upd symtab  end;
    1.78 -
    1.79 -(*Like update but fails if key is already defined in table.*)
    1.80 -fun update_new ((key: string, entry: 'a), symtab : 'a table)
    1.81 -  : 'a table =
    1.82 -  let fun upd Tip = Branch (key, entry, Tip, Tip)
    1.83 -        | upd (Branch(key', entry', left, right)) =
    1.84 -            if      key < key' then Branch (key', entry', upd left, right)
    1.85 -            else if key' < key then Branch (key', entry', left, upd right)
    1.86 -            else  raise DUP(key)
    1.87 -  in  upd symtab  end;
    1.88 -
    1.89 -
    1.90 -(*conversion of symbol table to sorted association list*)
    1.91 -fun dest (symtab : 'a table) : (string * 'a) list =
    1.92 -  let fun ali (symtab, cont) = case symtab of
    1.93 -                Tip => cont
    1.94 -        | Branch (key, entry, left, right) =>
    1.95 -            ali(left, (key, entry) :: ali(right, cont))
    1.96 -  in  ali (symtab, [])  end;
    1.97 -
    1.98 -
    1.99 -(*Make a balanced tree of the first n members of the sorted alist (sal).
   1.100 -  Utility for the function balance.*)
   1.101 -fun bal_of (sal, 0) = Tip
   1.102 -  | bal_of (sal, n) =
   1.103 -      let val mid = n div 2
   1.104 -      in  case  drop (mid, sal) of
   1.105 -            [] => bal_of (sal, mid)   (*should not occur*)
   1.106 -          | ((key, entry):: pairs) =>
   1.107 -                Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
   1.108 -      end;
   1.109 -
   1.110 -
   1.111 -fun balance symtab =
   1.112 -  let val sal = dest symtab
   1.113 -  in  bal_of (sal, length sal)  end;
   1.114 -
   1.115 -
   1.116 -(*A "declaration" associates the same entry with a list of keys;
   1.117 -  does not allow overwriting of an entry*)
   1.118 -fun decl_update_new ((keys : string list, entry: 'a), symtab)
   1.119 -  : 'a table =
   1.120 -  let fun decl (key, symtab) = update_new ((key, entry), symtab)
   1.121 -  in foldr decl (keys, symtab) end;
   1.122 -
   1.123 -(*Addition of a list of declarations to a symbol table*)
   1.124 -fun st_of_declist (dl, symtab) =
   1.125 -  balance (foldr decl_update_new (dl, symtab));
   1.126 -
   1.127 -
   1.128 -(* make, extend, merge tables *)
   1.129 -
   1.130 -fun eq_pair eq ((key1, entry1), (key2, entry2)) =
   1.131 -  key1 = key2 andalso eq (entry1, entry2);
   1.132 -
   1.133 -fun make alst =
   1.134 -  (case gen_duplicates eq_fst alst of
   1.135 -    [] => balance (foldr update_new (alst, Tip))
   1.136 -  | dups => raise DUPS (map fst dups));
   1.137 -
   1.138 -fun pre_extend eq (tab, alst) =
   1.139 -  generic_extend (eq_pair eq) dest make tab alst;
   1.140 -
   1.141 -fun extend (tab, alst) = pre_extend (K false) (tab, alst);
   1.142 -
   1.143 -fun merge eq (tab1, tab2) =
   1.144 -  generic_merge (eq_pair eq) dest make tab1 tab2;
   1.145 -
   1.146 -
   1.147 -(* tables with multiple entries per key *)
   1.148 -(*order of entries with same key is preserved*)
   1.149 -
   1.150 -fun lookup_multi (tab, key) =
   1.151 -  (case lookup (tab, key) of
   1.152 -    Some entries => entries
   1.153 -  | None => []);
   1.154 -
   1.155 -fun cons_entry ((key, entry), tab) =
   1.156 -  update ((key, entry :: lookup_multi (tab, key)), tab);
   1.157 -
   1.158 -fun make_multi alst =
   1.159 -  balance (foldr cons_entry (alst, Tip));
   1.160 -
   1.161 -fun dest_multi tab =
   1.162 -  List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
   1.163 -
   1.164 -
   1.165 -(* map tables *)
   1.166 -
   1.167 -fun map _ Tip = Tip
   1.168 -  | map f (Branch (key, entry, left, right)) =
   1.169 -      Branch (key, f entry, map f left, map f right);
   1.170 -
   1.171 -end;
   1.172 -