src/HOL/Tools/polyhash.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28397 389c5e494605
child 32740 9dd0a2f83429
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     1
(* Modified for Poly/ML from SML/NJ Library version 0.2
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     2
 *
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     3
 * COPYRIGHT (c) 1992 by AT&T Bell Laboratories.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     4
 * See file mosml/copyrght/copyrght.att for details.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     5
 *
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     6
 * Original author: John Reppy, AT&T Bell Laboratories, Murray Hill, NJ 07974
18508
paulson
parents: 18449
diff changeset
     7
 * Current version from the Moscow ML distribution, copied by permission.
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     8
 *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
     9
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    10
(* Polyhash -- polymorphic hashtables as in the SML/NJ Library *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    11
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    12
signature Polyhash =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    13
sig
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    14
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    15
type ('key, 'data) hash_table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    16
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    17
val mkTable     : ('_key -> int) * ('_key * '_key -> bool) -> int * exn 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    18
                  -> ('_key, '_data) hash_table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    19
val numItems    : ('key, 'data) hash_table -> int
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    20
val insert      : ('_key, '_data) hash_table -> '_key * '_data -> unit
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    21
val peekInsert  : ('_key, '_data) hash_table -> '_key * '_data 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    22
                  -> '_data option
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    23
val find        : ('key, 'data) hash_table -> 'key -> 'data
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    24
val peek        : ('key, 'data) hash_table -> 'key -> 'data option
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    25
val remove      : ('key, 'data) hash_table -> 'key -> 'data
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    26
val listItems   : ('key, 'data) hash_table -> ('key * 'data) list
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    27
val apply       : ('key * 'data -> unit) -> ('key, 'data) hash_table -> unit
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    28
val map         : ('_key * 'data -> '_res) -> ('_key, 'data) hash_table 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    29
                  -> ('_key, '_res) hash_table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    30
val filter      : ('key * 'data -> bool) -> ('key, 'data) hash_table -> unit
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    31
val transform   : ('data -> '_res) -> ('_key, 'data) hash_table 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    32
                  -> ('_key, '_res) hash_table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    33
val copy        : ('_key, '_data) hash_table -> ('_key, '_data) hash_table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    34
val bucketSizes : ('key, 'data) hash_table -> int list
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    35
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    36
(*Additions due to L. C. Paulson and Jia Meng*)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    37
val hashw : word * word -> word
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    38
val hashw_char : Char.char * word -> word
20662
9116dc6842e1 new function hashw_int
paulson
parents: 20416
diff changeset
    39
val hashw_int : int * word -> word
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    40
val hashw_vector : word Vector.vector * word -> word
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    41
val hashw_string : string * word -> word
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    42
val hashw_strings : string list * word -> word
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    43
val hash_string : string -> int
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    44
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    45
(* 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    46
   [('key, 'data) hash_table] is the type of hashtables with keys of type
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    47
   'key and data values of type 'data.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    48
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    49
   [mkTable (hashVal, sameKey) (sz, exc)] returns a new hashtable,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    50
   using hash function hashVal and equality predicate sameKey.  The sz
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    51
   is a size hint, and exc is the exception raised by function find.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    52
   It must be the case that sameKey(k1, k2) implies hashVal(k1) =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    53
   hashVal(k2) for all k1,k2.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    54
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    55
   [numItems htbl] is the number of items in the hash table.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    56
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    57
   [insert htbl (k, d)] inserts data d for key k.  If k already had an
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    58
   item associated with it, then the old item is overwritten.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    59
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    60
   [find htbl k] returns d, where d is the data item associated with key k, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    61
   or raises the exception (given at creation of htbl) if there is no such d.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    62
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    63
   [peek htbl k] returns SOME d, where d is the data item associated with 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    64
   key k, or NONE if there is no such d.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    65
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    66
   [peekInsert htbl (k, d)] inserts data d for key k, if k is not
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    67
   already in the table, returning NONE.  If k is already in the
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    68
   table, and the associated data value is d', then returns SOME d'
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    69
   and leaves the table unmodified.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    70
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    71
   [remove htbl k] returns d, where d is the data item associated with key k, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    72
   removing d from the table; or raises the exception if there is no such d.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    73
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    74
   [listItems htbl] returns a list of the (key, data) pairs in the hashtable.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    75
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    76
   [apply f htbl] applies function f to all (key, data) pairs in the 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    77
   hashtable, in some order.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    78
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    79
   [map f htbl] returns a new hashtable, whose data items have been
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    80
   obtained by applying f to the (key, data) pairs in htbl.  The new
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    81
   tables have the same keys, hash function, equality predicate, and
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    82
   exception, as htbl.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    83
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    84
   [filter p htbl] deletes from htbl all data items which do not
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    85
   satisfy predicate p.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    86
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    87
   [transform f htbl] as map, but only the (old) data values are used
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    88
   when computing the new data values.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    89
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    90
   [copy htbl] returns a complete copy of htbl.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    91
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    92
   [bucketSizes htbl] returns a list of the sizes of the buckets.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    93
   This is to allow users to gauge the quality of their hashing
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    94
   function.  
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    95
*)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    96
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    97
end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    98
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
    99
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   100
structure Polyhash :> Polyhash =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   101
struct
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   102
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   103
datatype ('key, 'data) bucket_t
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   104
  = NIL
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   105
  | B of int * 'key * 'data * ('key, 'data) bucket_t
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   106
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   107
datatype ('key, 'data) hash_table = 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   108
    HT of {hashVal   : 'key -> int,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   109
	   sameKey   : 'key * 'key -> bool,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   110
	   not_found : exn,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   111
	   table     : ('key, 'data) bucket_t Array.array ref,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   112
	   n_items   : int ref}
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   113
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   114
local
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   115
(*
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   116
    prim_val andb_      : int -> int -> int = 2 "and";
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   117
    prim_val lshift_    : int -> int -> int = 2 "shift_left";
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   118
*)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   119
    fun andb_ x y = Word.toInt (Word.andb (Word.fromInt x, Word.fromInt y));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   120
    fun lshift_ x y = Word.toInt (Word.<< (Word.fromInt x, Word.fromInt y));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   121
in 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   122
    fun index (i, sz) = andb_ i (sz-1)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   123
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   124
  (* find smallest power of 2 (>= 32) that is >= n *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   125
    fun roundUp n = 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   126
	let fun f i = if (i >= n) then i else f (lshift_ i 1)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   127
	in f 32 end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   128
end;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   129
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   130
  (* Create a new table; the int is a size hint and the exception
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   131
   * is to be raised by find.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   132
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   133
    fun mkTable (hashVal, sameKey) (sizeHint, notFound) = HT{
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   134
            hashVal=hashVal,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   135
	    sameKey=sameKey,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   136
	    not_found = notFound,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   137
	    table = ref (Array.array(roundUp sizeHint, NIL)),
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   138
	    n_items = ref 0
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   139
	  };
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   140
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   141
  (* conditionally grow a table *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   142
    fun growTable (HT{table, n_items, ...}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   143
	    val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   144
	    val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   145
	    in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   146
	      if (!n_items >= sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   147
		then let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   148
		  val newSz = sz+sz
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   149
		  val newArr = Array.array (newSz, NIL)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   150
		  fun copy NIL = ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   151
		    | copy (B(h, key, v, rest)) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   152
			val indx = index (h, newSz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   153
			in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   154
			  Array.update (newArr, indx,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   155
			    B(h, key, v, Array.sub(newArr, indx)));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   156
			  copy rest
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   157
			end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   158
		  fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   159
		  in
28397
389c5e494605 handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents: 20662
diff changeset
   160
		    (bucket 0) handle _ => ();  (* FIXME avoid handle _ *)
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   161
		    table := newArr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   162
		  end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   163
		else ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   164
	    end (* growTable *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   165
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   166
  (* Insert an item.  If the key already has an item associated with it,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   167
   * then the old item is discarded.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   168
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   169
    fun insert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   170
	let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   171
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   172
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   173
	  val hash = hashVal key
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   174
	  val indx = index (hash, sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   175
	  fun look NIL = (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   176
		Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
20416
f9cb300118ca using inc
paulson
parents: 18508
diff changeset
   177
		inc n_items;
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   178
		growTable tbl;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   179
		NIL)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   180
	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   181
		then B(hash, key, item, r)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   182
		else (case (look r)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   183
		   of NIL => NIL
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   184
		    | rest => B(h, k, v, rest)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   185
		  (* end case *))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   186
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   187
	    case (look (Array.sub (arr, indx)))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   188
	     of NIL => ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   189
	      | b => Array.update(arr, indx, b)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   190
	  end;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   191
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   192
  (* Insert an item if not there already; if it is there already, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   193
     then return the old data value and leave the table unmodified..
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   194
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   195
    fun peekInsert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   196
	let val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   197
	    val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   198
	    val hash = hashVal key
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   199
	    val indx = index (hash, sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   200
	    fun look NIL = 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   201
		(Array.update(arr, indx, B(hash, key, item, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   202
					   Array.sub(arr, indx)));
20416
f9cb300118ca using inc
paulson
parents: 18508
diff changeset
   203
		 inc n_items;
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   204
		 growTable tbl;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   205
		 NONE)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   206
	      | look (B(h, k, v, r)) = 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   207
		if hash = h andalso sameKey(key, k) then SOME v
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   208
		else look r
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   209
	in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   210
	    look (Array.sub (arr, indx))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   211
	end;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   212
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   213
  (* find an item, the table's exception is raised if the item doesn't exist *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   214
    fun find (HT{hashVal, sameKey, table, not_found, ...}) key = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   215
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   216
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   217
	  val hash = hashVal key
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   218
	  val indx = index (hash, sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   219
	  fun look NIL = raise not_found
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   220
	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   221
		then v
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   222
		else look r
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   223
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   224
	    look (Array.sub (arr, indx))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   225
	  end;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   226
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   227
  (* look for an item, return NONE if the item doesn't exist *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   228
    fun peek (HT{hashVal, sameKey, table, ...}) key = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   229
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   230
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   231
	  val hash = hashVal key
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   232
	  val indx = index (hash, sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   233
	  fun look NIL = NONE
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   234
	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   235
		then SOME v
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   236
		else look r
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   237
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   238
	    look (Array.sub (arr, indx))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   239
	  end;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   240
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   241
  (* Remove an item.  The table's exception is raised if
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   242
   * the item doesn't exist.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   243
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   244
    fun remove (HT{hashVal, sameKey, not_found, table, n_items}) key = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   245
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   246
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   247
	  val hash = hashVal key
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   248
	  val indx = index (hash, sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   249
	  fun look NIL = raise not_found
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   250
	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   251
		then (v, r)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   252
		else let val (item, r') = look r in (item, B(h, k, v, r')) end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   253
	  val (item, bucket) = look (Array.sub (arr, indx))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   254
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   255
	    Array.update (arr, indx, bucket);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   256
	    n_items := !n_items - 1;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   257
	    item
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   258
	  end (* remove *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   259
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   260
  (* Return the number of items in the table *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   261
   fun numItems (HT{n_items, ...}) = !n_items
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   262
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   263
  (* return a list of the items in the table *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   264
    fun listItems (HT{table = ref arr, n_items, ...}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   265
	  fun f (_, l, 0) = l
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   266
	    | f (~1, l, _) = l
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   267
	    | f (i, l, n) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   268
		fun g (NIL, l, n) = f (i-1, l, n)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   269
		  | g (B(_, k, v, r), l, n) = g(r, (k, v)::l, n-1)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   270
		in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   271
		  g (Array.sub(arr, i), l, n)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   272
		end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   273
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   274
	    f ((Array.length arr) - 1, [], !n_items)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   275
	  end (* listItems *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   276
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   277
  (* Apply a function to the entries of the table *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   278
    fun apply f (HT{table, ...}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   279
	  fun appF NIL = ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   280
	    | appF (B(_, key, item, rest)) = (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   281
		f (key, item);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   282
		appF rest)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   283
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   284
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   285
	  fun appToTbl i = if (i < sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   286
		then (appF (Array.sub (arr, i)); appToTbl(i+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   287
		else ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   288
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   289
	    appToTbl 0
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   290
	  end (* apply *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   291
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   292
  (* Map a table to a new table that has the same keys and exception *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   293
    fun map f (HT{hashVal, sameKey, table, n_items, not_found}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   294
	  fun mapF NIL = NIL
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   295
	    | mapF (B(hash, key, item, rest)) =
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   296
		B(hash, key, f (key, item), mapF rest)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   297
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   298
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   299
	  val newArr = Array.array (sz, NIL)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   300
	  fun mapTbl i = if (i < sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   301
		then (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   302
		  Array.update(newArr, i, mapF (Array.sub(arr, i)));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   303
		  mapTbl (i+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   304
		else ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   305
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   306
	    mapTbl 0;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   307
	    HT{hashVal=hashVal,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   308
	       sameKey=sameKey,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   309
	       table = ref newArr, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   310
	       n_items = ref(!n_items), 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   311
	       not_found = not_found}
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   312
	  end (* transform *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   313
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   314
  (* remove any hash table items that do not satisfy the given
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   315
   * predicate.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   316
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   317
    fun filter pred (HT{table, n_items, not_found, ...}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   318
	  fun filterP NIL = NIL
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   319
	    | filterP (B(hash, key, item, rest)) = if (pred(key, item))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   320
		then B(hash, key, item, filterP rest)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   321
		else filterP rest
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   322
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   323
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   324
	  fun filterTbl i = if (i < sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   325
		then (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   326
		  Array.update (arr, i, filterP (Array.sub (arr, i)));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   327
		  filterTbl (i+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   328
		else ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   329
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   330
	    filterTbl 0
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   331
	  end (* filter *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   332
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   333
  (* Map a table to a new table that has the same keys, exception,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   334
     hash function, and equality function *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   335
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   336
    fun transform f (HT{hashVal, sameKey, table, n_items, not_found}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   337
	  fun mapF NIL = NIL
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   338
	    | mapF (B(hash, key, item, rest)) = B(hash, key, f item, mapF rest)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   339
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   340
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   341
	  val newArr = Array.array (sz, NIL)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   342
	  fun mapTbl i = if (i < sz)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   343
		then (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   344
		  Array.update(newArr, i, mapF (Array.sub(arr, i)));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   345
		  mapTbl (i+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   346
		else ()
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   347
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   348
	    mapTbl 0;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   349
	    HT{hashVal=hashVal, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   350
	       sameKey=sameKey, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   351
	       table = ref newArr, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   352
	       n_items = ref(!n_items), 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   353
	       not_found = not_found}
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   354
	  end (* transform *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   355
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   356
  (* Create a copy of a hash table *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   357
    fun copy (HT{hashVal, sameKey, table, n_items, not_found}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   358
	  val arr = !table
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   359
	  val sz = Array.length arr
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   360
	  val newArr = Array.array (sz, NIL)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   361
	  fun mapTbl i = (
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   362
		Array.update (newArr, i, Array.sub(arr, i));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   363
		mapTbl (i+1))
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   364
	  in
28397
389c5e494605 handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents: 20662
diff changeset
   365
	    (mapTbl 0) handle _ => ();  (* FIXME avoid handle _ *)
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   366
	    HT{hashVal=hashVal, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   367
	       sameKey=sameKey,
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   368
	       table = ref newArr, 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   369
	       n_items = ref(!n_items), 
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   370
	       not_found = not_found}
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   371
	  end (* copy *);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   372
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   373
  (* returns a list of the sizes of the various buckets.  This is to
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   374
   * allow users to gauge the quality of their hashing function.
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   375
   *)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   376
    fun bucketSizes (HT{table = ref arr, ...}) = let
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   377
	  fun len (NIL, n) = n
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   378
	    | len (B(_, _, _, r), n) = len(r, n+1)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   379
	  fun f (~1, l) = l
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   380
	    | f (i, l) = f (i-1, len (Array.sub (arr, i), 0) :: l)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   381
	  in
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   382
	    f ((Array.length arr)-1, [])
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   383
	  end
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   384
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   385
   (*Added by lcp.
18508
paulson
parents: 18449
diff changeset
   386
      This is essentially the  described in Compilers:
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   387
      Principles, Techniques, and Tools, by Aho, Sethi and Ullman.*)
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   388
18508
paulson
parents: 18449
diff changeset
   389
   (*This hash function is recommended in Compilers: Principles, Techniques, and
paulson
parents: 18449
diff changeset
   390
     Tools, by Aho, Sethi and Ullman. The hashpjw function, which they particularly
paulson
parents: 18449
diff changeset
   391
     recommend, triggers a bug in versions of Poly/ML up to 4.2.0.*)
paulson
parents: 18449
diff changeset
   392
   fun hashw (u,w) = Word.+ (u, Word.*(0w65599,w))
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   393
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   394
   fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   395
   
20662
9116dc6842e1 new function hashw_int
paulson
parents: 20416
diff changeset
   396
   fun hashw_int (i,w) = hashw (Word.fromInt i, w);
9116dc6842e1 new function hashw_int
paulson
parents: 20416
diff changeset
   397
   
18449
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   398
   fun hashw_vector (v,w) = Vector.foldl hashw w v;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   399
   
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   400
   fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   401
   
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   402
   fun hashw_strings (ss, w) = List.foldl hashw_string w ss;
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   403
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   404
   fun hash_string s = Word.toIntX (hashw_string(s,0w0));
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   405
e314fb38307d new hash table module in HOL/Too/s
paulson
parents:
diff changeset
   406
end