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