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