replaced symtab.ML by table.ML;
authorwenzelm
Sun Dec 28 14:55:20 1997 +0100 (1997-12-28)
changeset 4484220ccae8a590
parent 4483 caf8ae95c61f
child 4485 697972696f71
replaced symtab.ML by table.ML;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/symtab.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun Dec 28 14:54:38 1997 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sun Dec 28 14:55:20 1997 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  	axclass.ML basis.ML deriv.ML display.ML drule.ML envir.ML \
     1.5  	goals.ML install_pp.ML library.ML logic.ML name_space.ML net.ML \
     1.6  	pattern.ML pure_thy.ML search.ML section_utils.ML seq.ML sign.ML \
     1.7 -	sorts.ML symtab.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
     1.8 +	sorts.ML table.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
     1.9  	type.ML type_infer.ML unify.ML
    1.10  
    1.11  $(OUT)/Pure: $(FILES)
     2.1 --- a/src/Pure/ROOT.ML	Sun Dec 28 14:54:38 1997 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Sun Dec 28 14:55:20 1997 +0100
     2.3 @@ -13,8 +13,8 @@
     2.4  print_depth 1;
     2.5  
     2.6  use "library.ML";
     2.7 +use "table.ML";
     2.8  use "seq.ML";
     2.9 -use "symtab.ML";
    2.10  use "name_space.ML";
    2.11  use "term.ML";
    2.12  
     3.1 --- a/src/Pure/symtab.ML	Sun Dec 28 14:54:38 1997 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,169 +0,0 @@
     3.4 -(*  Title:      Pure/symtab.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1989  University of Cambridge
     3.8 -
     3.9 -Unbalanced binary trees indexed by strings; no way to delete an entry.
    3.10 -*)
    3.11 -
    3.12 -signature SYMTAB =
    3.13 -sig
    3.14 -  exception DUP of string
    3.15 -  exception DUPS of string list
    3.16 -  type 'a table
    3.17 -  val empty: 'a table
    3.18 -  val is_empty: 'a table -> bool
    3.19 -  val lookup: 'a table * string -> 'a option
    3.20 -  val find_first: (string * 'a -> bool) -> 'a table -> (string * 'a) option
    3.21 -  val update: (string * 'a) * 'a table -> 'a table
    3.22 -  val update_new: (string * 'a) * 'a table -> 'a table
    3.23 -  val map: ('a -> 'b) -> 'a table -> 'b table
    3.24 -  val balance: 'a table -> 'a table
    3.25 -  val st_of_declist: (string list * 'a) list * 'a table -> 'a table
    3.26 -  val make: (string * 'a) list -> 'a table
    3.27 -  val dest: 'a table -> (string * 'a) list
    3.28 -  val extend: 'a table * (string * 'a) list -> 'a table
    3.29 -  val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    3.30 -  val lookup_multi: 'a list table * string -> 'a list
    3.31 -  val make_multi: (string * 'a) list -> 'a list table
    3.32 -  val dest_multi: 'a list table -> (string * 'a) list
    3.33 -end;
    3.34 -
    3.35 -structure Symtab: SYMTAB =
    3.36 -struct
    3.37 -
    3.38 -(*symbol table errors, such as from update_new*)
    3.39 -exception DUP of string;
    3.40 -exception DUPS of string list;
    3.41 -
    3.42 -datatype 'a table = Tip | Branch of (string * 'a * 'a table * 'a table);
    3.43 -
    3.44 -
    3.45 -val empty = Tip;
    3.46 -
    3.47 -fun is_empty Tip = true
    3.48 -  | is_empty _ = false;
    3.49 -
    3.50 -
    3.51 -fun lookup (symtab: 'a table, key: string) : 'a option =
    3.52 -  let fun look  Tip  = None
    3.53 -        | look (Branch (key', entry, left, right)) =
    3.54 -            if      key < key' then look left
    3.55 -            else if key' < key then look right
    3.56 -            else  Some entry
    3.57 -  in look symtab end;
    3.58 -
    3.59 -
    3.60 -fun find_first _ Tip = None
    3.61 -  | find_first pred (Branch (key, entry, left, right)) =
    3.62 -      (case find_first pred left of
    3.63 -        None =>
    3.64 -          if pred (key, entry) then Some (key, entry)
    3.65 -          else find_first pred right
    3.66 -      | some => some);
    3.67 -
    3.68 -
    3.69 -(*update, allows overwriting of an entry*)
    3.70 -fun update ((key: string, entry: 'a), symtab : 'a table)
    3.71 -  : 'a table =
    3.72 -  let fun upd  Tip  = Branch (key, entry, Tip, Tip)
    3.73 -        | upd (Branch(key', entry', left, right)) =
    3.74 -            if      key < key' then Branch (key', entry', upd left, right)
    3.75 -            else if key' < key then Branch (key', entry', left, upd right)
    3.76 -            else                    Branch (key, entry, left, right)
    3.77 -  in  upd symtab  end;
    3.78 -
    3.79 -(*Like update but fails if key is already defined in table.*)
    3.80 -fun update_new ((key: string, entry: 'a), symtab : 'a table)
    3.81 -  : 'a table =
    3.82 -  let fun upd Tip = Branch (key, entry, Tip, Tip)
    3.83 -        | upd (Branch(key', entry', left, right)) =
    3.84 -            if      key < key' then Branch (key', entry', upd left, right)
    3.85 -            else if key' < key then Branch (key', entry', left, upd right)
    3.86 -            else  raise DUP(key)
    3.87 -  in  upd symtab  end;
    3.88 -
    3.89 -
    3.90 -(*conversion of symbol table to sorted association list*)
    3.91 -fun dest (symtab : 'a table) : (string * 'a) list =
    3.92 -  let fun ali (symtab, cont) = case symtab of
    3.93 -                Tip => cont
    3.94 -        | Branch (key, entry, left, right) =>
    3.95 -            ali(left, (key, entry) :: ali(right, cont))
    3.96 -  in  ali (symtab, [])  end;
    3.97 -
    3.98 -
    3.99 -(*Make a balanced tree of the first n members of the sorted alist (sal).
   3.100 -  Utility for the function balance.*)
   3.101 -fun bal_of (sal, 0) = Tip
   3.102 -  | bal_of (sal, n) =
   3.103 -      let val mid = n div 2
   3.104 -      in  case  drop (mid, sal) of
   3.105 -            [] => bal_of (sal, mid)   (*should not occur*)
   3.106 -          | ((key, entry):: pairs) =>
   3.107 -                Branch(key, entry, bal_of(sal, mid), bal_of(pairs, n-mid-1))
   3.108 -      end;
   3.109 -
   3.110 -
   3.111 -fun balance symtab =
   3.112 -  let val sal = dest symtab
   3.113 -  in  bal_of (sal, length sal)  end;
   3.114 -
   3.115 -
   3.116 -(*A "declaration" associates the same entry with a list of keys;
   3.117 -  does not allow overwriting of an entry*)
   3.118 -fun decl_update_new ((keys : string list, entry: 'a), symtab)
   3.119 -  : 'a table =
   3.120 -  let fun decl (key, symtab) = update_new ((key, entry), symtab)
   3.121 -  in foldr decl (keys, symtab) end;
   3.122 -
   3.123 -(*Addition of a list of declarations to a symbol table*)
   3.124 -fun st_of_declist (dl, symtab) =
   3.125 -  balance (foldr decl_update_new (dl, symtab));
   3.126 -
   3.127 -
   3.128 -(* make, extend, merge tables *)
   3.129 -
   3.130 -fun eq_pair eq ((key1, entry1), (key2, entry2)) =
   3.131 -  key1 = key2 andalso eq (entry1, entry2);
   3.132 -
   3.133 -fun make alst =
   3.134 -  (case gen_duplicates eq_fst alst of
   3.135 -    [] => balance (foldr update_new (alst, Tip))
   3.136 -  | dups => raise DUPS (map fst dups));
   3.137 -
   3.138 -fun pre_extend eq (tab, alst) =
   3.139 -  generic_extend (eq_pair eq) dest make tab alst;
   3.140 -
   3.141 -fun extend (tab, alst) = pre_extend (K false) (tab, alst);
   3.142 -
   3.143 -fun merge eq (tab1, tab2) =
   3.144 -  generic_merge (eq_pair eq) dest make tab1 tab2;
   3.145 -
   3.146 -
   3.147 -(* tables with multiple entries per key *)
   3.148 -(*order of entries with same key is preserved*)
   3.149 -
   3.150 -fun lookup_multi (tab, key) =
   3.151 -  (case lookup (tab, key) of
   3.152 -    Some entries => entries
   3.153 -  | None => []);
   3.154 -
   3.155 -fun cons_entry ((key, entry), tab) =
   3.156 -  update ((key, entry :: lookup_multi (tab, key)), tab);
   3.157 -
   3.158 -fun make_multi alst =
   3.159 -  balance (foldr cons_entry (alst, Tip));
   3.160 -
   3.161 -fun dest_multi tab =
   3.162 -  List.concat (map (fn (key, entries) => map (pair key) entries) (dest tab));
   3.163 -
   3.164 -
   3.165 -(* map tables *)
   3.166 -
   3.167 -fun map _ Tip = Tip
   3.168 -  | map f (Branch (key, entry, left, right)) =
   3.169 -      Branch (key, f entry, map f left, map f right);
   3.170 -
   3.171 -end;
   3.172 -