get rid of Polyhash, since it's no longer used
authorblanchet
Mon Mar 29 15:50:18 2010 +0200 (2010-03-29)
changeset 36062194cb6e3c13f
parent 36061 d267bdccc660
child 36063 cdc6855a6387
get rid of Polyhash, since it's no longer used
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/polyhash.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 29 15:26:19 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 29 15:50:18 2010 +0200
     1.3 @@ -296,7 +296,6 @@
     1.4    Tools/numeral.ML \
     1.5    Tools/numeral_simprocs.ML \
     1.6    Tools/numeral_syntax.ML \
     1.7 -  Tools/polyhash.ML \
     1.8    Tools/Predicate_Compile/predicate_compile_aux.ML \
     1.9    Tools/Predicate_Compile/predicate_compile_core.ML \
    1.10    Tools/Predicate_Compile/predicate_compile_data.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Mon Mar 29 15:26:19 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Mon Mar 29 15:50:18 2010 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  theory Sledgehammer
     2.5  imports Plain Hilbert_Choice
     2.6  uses
     2.7 -  "Tools/polyhash.ML"
     2.8    "~~/src/Tools/Metis/metis.ML"
     2.9    "Tools/Sledgehammer/sledgehammer_util.ML"
    2.10    ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 29 15:26:19 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 29 15:50:18 2010 +0200
     3.3 @@ -217,6 +217,7 @@
     3.4  structure Nitpick_HOL : NITPICK_HOL =
     3.5  struct
     3.6  
     3.7 +open Sledgehammer_Util
     3.8  open Nitpick_Util
     3.9  
    3.10  type const_table = term list Symtab.table
    3.11 @@ -1229,8 +1230,8 @@
    3.12    | is_ground_term _ = false
    3.13  
    3.14  (* term -> word -> word *)
    3.15 -fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
    3.16 -  | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
    3.17 +fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
    3.18 +  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
    3.19    | hashw_term _ = 0w0
    3.20  (* term -> int *)
    3.21  val hash_term = Word.toInt o hashw_term
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:26:19 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:50:18 2010 +0200
     4.3 @@ -180,11 +180,11 @@
     4.4        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
     4.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
     4.6  
     4.7 -(*HACK because SPASS truncates identifiers to 63 characters :-(( *)
     4.8 -(*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
     4.9 -fun controlled_length dfg_format s =
    4.10 -  if size s > 60 andalso dfg_format
    4.11 -  then Word.toString (Polyhash.hashw_string(s,0w0))
    4.12 +(* HACK because SPASS 3.0 truncates identifiers to 63 characters. (This is
    4.13 +   solved in 3.7 and perhaps in earlier versions too.) *)
    4.14 +(* 32-bit hash, so we expect no collisions. *)
    4.15 +fun controlled_length dfg s =
    4.16 +  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0))
    4.17    else s;
    4.18  
    4.19  fun lookup_const dfg c =
    4.20 @@ -197,8 +197,9 @@
    4.21          SOME c' => c'
    4.22        | NONE => controlled_length dfg (ascii_of c);
    4.23  
    4.24 -fun make_fixed_const _ "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
    4.25 -  | make_fixed_const dfg c      = const_prefix ^ lookup_const dfg c;
    4.26 +(* "op =" MUST BE "equal" because it's built into ATPs. *)
    4.27 +fun make_fixed_const _ (@{const_name "op ="}) = "equal"
    4.28 +  | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c;
    4.29  
    4.30  fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
    4.31  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Mar 29 15:26:19 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Mar 29 15:50:18 2010 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/Sledgehammer/sledgehammer_util.ML
     5.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_util.ML
     5.6      Author:     Jasmin Blanchette, TU Muenchen
     5.7  
     5.8  General-purpose functions used by the Sledgehammer modules.
     5.9 @@ -9,11 +9,21 @@
    5.10    val serial_commas : string -> string list -> string list
    5.11    val parse_bool_option : bool -> string -> string -> bool option
    5.12    val parse_time_option : string -> string -> Time.time option
    5.13 +  val hashw : word * word -> word
    5.14 +  val hashw_char : Char.char * word -> word
    5.15 +  val hashw_string : string * word -> word
    5.16  end;
    5.17  
    5.18  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    5.19  struct
    5.20  
    5.21 +(* This hash function is recommended in Compilers: Principles, Techniques, and
    5.22 +   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
    5.23 +   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
    5.24 +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
    5.25 +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
    5.26 +fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
    5.27 +
    5.28  fun serial_commas _ [] = ["??"]
    5.29    | serial_commas _ [s] = [s]
    5.30    | serial_commas conj [s1, s2] = [s1, conj, s2]
     6.1 --- a/src/HOL/Tools/polyhash.ML	Mon Mar 29 15:26:19 2010 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,406 +0,0 @@
     6.4 -(* Modified for Poly/ML from SML/NJ Library version 0.2
     6.5 - *
     6.6 - * COPYRIGHT (c) 1992 by AT&T Bell Laboratories.
     6.7 - * See file mosml/copyrght/copyrght.att for details.
     6.8 - *
     6.9 - * Original author: John Reppy, AT&T Bell Laboratories, Murray Hill, NJ 07974
    6.10 - * Current version from the Moscow ML distribution, copied by permission.
    6.11 - *)
    6.12 -
    6.13 -(* Polyhash -- polymorphic hashtables as in the SML/NJ Library *)
    6.14 -
    6.15 -signature Polyhash =
    6.16 -sig
    6.17 -
    6.18 -type ('key, 'data) hash_table
    6.19 -
    6.20 -val mkTable     : ('_key -> int) * ('_key * '_key -> bool) -> int * exn 
    6.21 -                  -> ('_key, '_data) hash_table
    6.22 -val numItems    : ('key, 'data) hash_table -> int
    6.23 -val insert      : ('_key, '_data) hash_table -> '_key * '_data -> unit
    6.24 -val peekInsert  : ('_key, '_data) hash_table -> '_key * '_data 
    6.25 -                  -> '_data option
    6.26 -val find        : ('key, 'data) hash_table -> 'key -> 'data
    6.27 -val peek        : ('key, 'data) hash_table -> 'key -> 'data option
    6.28 -val remove      : ('key, 'data) hash_table -> 'key -> 'data
    6.29 -val listItems   : ('key, 'data) hash_table -> ('key * 'data) list
    6.30 -val apply       : ('key * 'data -> unit) -> ('key, 'data) hash_table -> unit
    6.31 -val map         : ('_key * 'data -> '_res) -> ('_key, 'data) hash_table 
    6.32 -                  -> ('_key, '_res) hash_table
    6.33 -val filter      : ('key * 'data -> bool) -> ('key, 'data) hash_table -> unit
    6.34 -val transform   : ('data -> '_res) -> ('_key, 'data) hash_table 
    6.35 -                  -> ('_key, '_res) hash_table
    6.36 -val copy        : ('_key, '_data) hash_table -> ('_key, '_data) hash_table
    6.37 -val bucketSizes : ('key, 'data) hash_table -> int list
    6.38 -
    6.39 -(*Additions due to L. C. Paulson and Jia Meng*)
    6.40 -val hashw : word * word -> word
    6.41 -val hashw_char : Char.char * word -> word
    6.42 -val hashw_int : int * word -> word
    6.43 -val hashw_vector : word Vector.vector * word -> word
    6.44 -val hashw_string : string * word -> word
    6.45 -val hashw_strings : string list * word -> word
    6.46 -val hash_string : string -> int
    6.47 -
    6.48 -(* 
    6.49 -   [('key, 'data) hash_table] is the type of hashtables with keys of type
    6.50 -   'key and data values of type 'data.
    6.51 -
    6.52 -   [mkTable (hashVal, sameKey) (sz, exc)] returns a new hashtable,
    6.53 -   using hash function hashVal and equality predicate sameKey.  The sz
    6.54 -   is a size hint, and exc is the exception raised by function find.
    6.55 -   It must be the case that sameKey(k1, k2) implies hashVal(k1) =
    6.56 -   hashVal(k2) for all k1,k2.
    6.57 -
    6.58 -   [numItems htbl] is the number of items in the hash table.
    6.59 -
    6.60 -   [insert htbl (k, d)] inserts data d for key k.  If k already had an
    6.61 -   item associated with it, then the old item is overwritten.
    6.62 -
    6.63 -   [find htbl k] returns d, where d is the data item associated with key k, 
    6.64 -   or raises the exception (given at creation of htbl) if there is no such d.
    6.65 -
    6.66 -   [peek htbl k] returns SOME d, where d is the data item associated with 
    6.67 -   key k, or NONE if there is no such d.
    6.68 -
    6.69 -   [peekInsert htbl (k, d)] inserts data d for key k, if k is not
    6.70 -   already in the table, returning NONE.  If k is already in the
    6.71 -   table, and the associated data value is d', then returns SOME d'
    6.72 -   and leaves the table unmodified.
    6.73 -
    6.74 -   [remove htbl k] returns d, where d is the data item associated with key k, 
    6.75 -   removing d from the table; or raises the exception if there is no such d.
    6.76 -
    6.77 -   [listItems htbl] returns a list of the (key, data) pairs in the hashtable.
    6.78 -
    6.79 -   [apply f htbl] applies function f to all (key, data) pairs in the 
    6.80 -   hashtable, in some order.
    6.81 -
    6.82 -   [map f htbl] returns a new hashtable, whose data items have been
    6.83 -   obtained by applying f to the (key, data) pairs in htbl.  The new
    6.84 -   tables have the same keys, hash function, equality predicate, and
    6.85 -   exception, as htbl.
    6.86 -
    6.87 -   [filter p htbl] deletes from htbl all data items which do not
    6.88 -   satisfy predicate p.
    6.89 -
    6.90 -   [transform f htbl] as map, but only the (old) data values are used
    6.91 -   when computing the new data values.
    6.92 -
    6.93 -   [copy htbl] returns a complete copy of htbl.
    6.94 -
    6.95 -   [bucketSizes htbl] returns a list of the sizes of the buckets.
    6.96 -   This is to allow users to gauge the quality of their hashing
    6.97 -   function.  
    6.98 -*)
    6.99 -
   6.100 -end
   6.101 -
   6.102 -
   6.103 -structure Polyhash :> Polyhash =
   6.104 -struct
   6.105 -
   6.106 -datatype ('key, 'data) bucket_t
   6.107 -  = NIL
   6.108 -  | B of int * 'key * 'data * ('key, 'data) bucket_t
   6.109 -
   6.110 -datatype ('key, 'data) hash_table = 
   6.111 -    HT of {hashVal   : 'key -> int,
   6.112 -           sameKey   : 'key * 'key -> bool,
   6.113 -           not_found : exn,
   6.114 -           table     : ('key, 'data) bucket_t Array.array Unsynchronized.ref,
   6.115 -           n_items   : int Unsynchronized.ref}
   6.116 -
   6.117 -local
   6.118 -(*
   6.119 -    prim_val andb_      : int -> int -> int = 2 "and";
   6.120 -    prim_val lshift_    : int -> int -> int = 2 "shift_left";
   6.121 -*)
   6.122 -    fun andb_ x y = Word.toInt (Word.andb (Word.fromInt x, Word.fromInt y));
   6.123 -    fun lshift_ x y = Word.toInt (Word.<< (Word.fromInt x, Word.fromInt y));
   6.124 -in 
   6.125 -    fun index (i, sz) = andb_ i (sz-1)
   6.126 -
   6.127 -  (* find smallest power of 2 (>= 32) that is >= n *)
   6.128 -    fun roundUp n = 
   6.129 -        let fun f i = if (i >= n) then i else f (lshift_ i 1)
   6.130 -        in f 32 end
   6.131 -end;
   6.132 -
   6.133 -  (* Create a new table; the int is a size hint and the exception
   6.134 -   * is to be raised by find.
   6.135 -   *)
   6.136 -    fun mkTable (hashVal, sameKey) (sizeHint, notFound) = HT{
   6.137 -            hashVal=hashVal,
   6.138 -            sameKey=sameKey,
   6.139 -            not_found = notFound,
   6.140 -            table = Unsynchronized.ref (Array.array(roundUp sizeHint, NIL)),
   6.141 -            n_items = Unsynchronized.ref 0
   6.142 -          };
   6.143 -
   6.144 -  (* conditionally grow a table *)
   6.145 -    fun growTable (HT{table, n_items, ...}) = let
   6.146 -            val arr = !table
   6.147 -            val sz = Array.length arr
   6.148 -            in
   6.149 -              if (!n_items >= sz)
   6.150 -                then let
   6.151 -                  val newSz = sz+sz
   6.152 -                  val newArr = Array.array (newSz, NIL)
   6.153 -                  fun copy NIL = ()
   6.154 -                    | copy (B(h, key, v, rest)) = let
   6.155 -                        val indx = index (h, newSz)
   6.156 -                        in
   6.157 -                          Array.update (newArr, indx,
   6.158 -                            B(h, key, v, Array.sub(newArr, indx)));
   6.159 -                          copy rest
   6.160 -                        end
   6.161 -                  fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1))
   6.162 -                  in
   6.163 -                    (bucket 0) handle _ => ();  (* FIXME avoid handle _ *)
   6.164 -                    table := newArr
   6.165 -                  end
   6.166 -                else ()
   6.167 -            end (* growTable *);
   6.168 -
   6.169 -  (* Insert an item.  If the key already has an item associated with it,
   6.170 -   * then the old item is discarded.
   6.171 -   *)
   6.172 -    fun insert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
   6.173 -        let
   6.174 -          val arr = !table
   6.175 -          val sz = Array.length arr
   6.176 -          val hash = hashVal key
   6.177 -          val indx = index (hash, sz)
   6.178 -          fun look NIL = (
   6.179 -                Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
   6.180 -                Unsynchronized.inc n_items;
   6.181 -                growTable tbl;
   6.182 -                NIL)
   6.183 -            | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   6.184 -                then B(hash, key, item, r)
   6.185 -                else (case (look r)
   6.186 -                   of NIL => NIL
   6.187 -                    | rest => B(h, k, v, rest)
   6.188 -                  (* end case *))
   6.189 -          in
   6.190 -            case (look (Array.sub (arr, indx)))
   6.191 -             of NIL => ()
   6.192 -              | b => Array.update(arr, indx, b)
   6.193 -          end;
   6.194 -
   6.195 -  (* Insert an item if not there already; if it is there already, 
   6.196 -     then return the old data value and leave the table unmodified..
   6.197 -   *)
   6.198 -    fun peekInsert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
   6.199 -        let val arr = !table
   6.200 -            val sz = Array.length arr
   6.201 -            val hash = hashVal key
   6.202 -            val indx = index (hash, sz)
   6.203 -            fun look NIL = 
   6.204 -                (Array.update(arr, indx, B(hash, key, item, 
   6.205 -                                           Array.sub(arr, indx)));
   6.206 -                 Unsynchronized.inc n_items;
   6.207 -                 growTable tbl;
   6.208 -                 NONE)
   6.209 -              | look (B(h, k, v, r)) = 
   6.210 -                if hash = h andalso sameKey(key, k) then SOME v
   6.211 -                else look r
   6.212 -        in
   6.213 -            look (Array.sub (arr, indx))
   6.214 -        end;
   6.215 -
   6.216 -  (* find an item, the table's exception is raised if the item doesn't exist *)
   6.217 -    fun find (HT{hashVal, sameKey, table, not_found, ...}) key = let
   6.218 -          val arr = !table
   6.219 -          val sz = Array.length arr
   6.220 -          val hash = hashVal key
   6.221 -          val indx = index (hash, sz)
   6.222 -          fun look NIL = raise not_found
   6.223 -            | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   6.224 -                then v
   6.225 -                else look r
   6.226 -          in
   6.227 -            look (Array.sub (arr, indx))
   6.228 -          end;
   6.229 -
   6.230 -  (* look for an item, return NONE if the item doesn't exist *)
   6.231 -    fun peek (HT{hashVal, sameKey, table, ...}) key = let
   6.232 -          val arr = !table
   6.233 -          val sz = Array.length arr
   6.234 -          val hash = hashVal key
   6.235 -          val indx = index (hash, sz)
   6.236 -          fun look NIL = NONE
   6.237 -            | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   6.238 -                then SOME v
   6.239 -                else look r
   6.240 -          in
   6.241 -            look (Array.sub (arr, indx))
   6.242 -          end;
   6.243 -
   6.244 -  (* Remove an item.  The table's exception is raised if
   6.245 -   * the item doesn't exist.
   6.246 -   *)
   6.247 -    fun remove (HT{hashVal, sameKey, not_found, table, n_items}) key = let
   6.248 -          val arr = !table
   6.249 -          val sz = Array.length arr
   6.250 -          val hash = hashVal key
   6.251 -          val indx = index (hash, sz)
   6.252 -          fun look NIL = raise not_found
   6.253 -            | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   6.254 -                then (v, r)
   6.255 -                else let val (item, r') = look r in (item, B(h, k, v, r')) end
   6.256 -          val (item, bucket) = look (Array.sub (arr, indx))
   6.257 -          in
   6.258 -            Array.update (arr, indx, bucket);
   6.259 -            n_items := !n_items - 1;
   6.260 -            item
   6.261 -          end (* remove *);
   6.262 -
   6.263 -  (* Return the number of items in the table *)
   6.264 -   fun numItems (HT{n_items, ...}) = !n_items
   6.265 -
   6.266 -  (* return a list of the items in the table *)
   6.267 -    fun listItems (HT{table = Unsynchronized.ref arr, n_items, ...}) = let
   6.268 -          fun f (_, l, 0) = l
   6.269 -            | f (~1, l, _) = l
   6.270 -            | f (i, l, n) = let
   6.271 -                fun g (NIL, l, n) = f (i-1, l, n)
   6.272 -                  | g (B(_, k, v, r), l, n) = g(r, (k, v)::l, n-1)
   6.273 -                in
   6.274 -                  g (Array.sub(arr, i), l, n)
   6.275 -                end
   6.276 -          in
   6.277 -            f ((Array.length arr) - 1, [], !n_items)
   6.278 -          end (* listItems *);
   6.279 -
   6.280 -  (* Apply a function to the entries of the table *)
   6.281 -    fun apply f (HT{table, ...}) = let
   6.282 -          fun appF NIL = ()
   6.283 -            | appF (B(_, key, item, rest)) = (
   6.284 -                f (key, item);
   6.285 -                appF rest)
   6.286 -          val arr = !table
   6.287 -          val sz = Array.length arr
   6.288 -          fun appToTbl i = if (i < sz)
   6.289 -                then (appF (Array.sub (arr, i)); appToTbl(i+1))
   6.290 -                else ()
   6.291 -          in
   6.292 -            appToTbl 0
   6.293 -          end (* apply *);
   6.294 -
   6.295 -  (* Map a table to a new table that has the same keys and exception *)
   6.296 -    fun map f (HT{hashVal, sameKey, table, n_items, not_found}) = let
   6.297 -          fun mapF NIL = NIL
   6.298 -            | mapF (B(hash, key, item, rest)) =
   6.299 -                B(hash, key, f (key, item), mapF rest)
   6.300 -          val arr = !table
   6.301 -          val sz = Array.length arr
   6.302 -          val newArr = Array.array (sz, NIL)
   6.303 -          fun mapTbl i = if (i < sz)
   6.304 -                then (
   6.305 -                  Array.update(newArr, i, mapF (Array.sub(arr, i)));
   6.306 -                  mapTbl (i+1))
   6.307 -                else ()
   6.308 -          in
   6.309 -            mapTbl 0;
   6.310 -            HT{hashVal=hashVal,
   6.311 -               sameKey=sameKey,
   6.312 -               table = Unsynchronized.ref newArr, 
   6.313 -               n_items = Unsynchronized.ref(!n_items), 
   6.314 -               not_found = not_found}
   6.315 -          end (* transform *);
   6.316 -
   6.317 -  (* remove any hash table items that do not satisfy the given
   6.318 -   * predicate.
   6.319 -   *)
   6.320 -    fun filter pred (HT{table, n_items, not_found, ...}) = let
   6.321 -          fun filterP NIL = NIL
   6.322 -            | filterP (B(hash, key, item, rest)) = if (pred(key, item))
   6.323 -                then B(hash, key, item, filterP rest)
   6.324 -                else filterP rest
   6.325 -          val arr = !table
   6.326 -          val sz = Array.length arr
   6.327 -          fun filterTbl i = if (i < sz)
   6.328 -                then (
   6.329 -                  Array.update (arr, i, filterP (Array.sub (arr, i)));
   6.330 -                  filterTbl (i+1))
   6.331 -                else ()
   6.332 -          in
   6.333 -            filterTbl 0
   6.334 -          end (* filter *);
   6.335 -
   6.336 -  (* Map a table to a new table that has the same keys, exception,
   6.337 -     hash function, and equality function *)
   6.338 -
   6.339 -    fun transform f (HT{hashVal, sameKey, table, n_items, not_found}) = let
   6.340 -          fun mapF NIL = NIL
   6.341 -            | mapF (B(hash, key, item, rest)) = B(hash, key, f item, mapF rest)
   6.342 -          val arr = !table
   6.343 -          val sz = Array.length arr
   6.344 -          val newArr = Array.array (sz, NIL)
   6.345 -          fun mapTbl i = if (i < sz)
   6.346 -                then (
   6.347 -                  Array.update(newArr, i, mapF (Array.sub(arr, i)));
   6.348 -                  mapTbl (i+1))
   6.349 -                else ()
   6.350 -          in
   6.351 -            mapTbl 0;
   6.352 -            HT{hashVal=hashVal, 
   6.353 -               sameKey=sameKey, 
   6.354 -               table = Unsynchronized.ref newArr, 
   6.355 -               n_items = Unsynchronized.ref(!n_items), 
   6.356 -               not_found = not_found}
   6.357 -          end (* transform *);
   6.358 -
   6.359 -  (* Create a copy of a hash table *)
   6.360 -    fun copy (HT{hashVal, sameKey, table, n_items, not_found}) = let
   6.361 -          val arr = !table
   6.362 -          val sz = Array.length arr
   6.363 -          val newArr = Array.array (sz, NIL)
   6.364 -          fun mapTbl i = (
   6.365 -                Array.update (newArr, i, Array.sub(arr, i));
   6.366 -                mapTbl (i+1))
   6.367 -          in
   6.368 -            (mapTbl 0) handle _ => ();  (* FIXME avoid handle _ *)
   6.369 -            HT{hashVal=hashVal, 
   6.370 -               sameKey=sameKey,
   6.371 -               table = Unsynchronized.ref newArr, 
   6.372 -               n_items = Unsynchronized.ref(!n_items), 
   6.373 -               not_found = not_found}
   6.374 -          end (* copy *);
   6.375 -
   6.376 -  (* returns a list of the sizes of the various buckets.  This is to
   6.377 -   * allow users to gauge the quality of their hashing function.
   6.378 -   *)
   6.379 -    fun bucketSizes (HT{table = Unsynchronized.ref arr, ...}) = let
   6.380 -          fun len (NIL, n) = n
   6.381 -            | len (B(_, _, _, r), n) = len(r, n+1)
   6.382 -          fun f (~1, l) = l
   6.383 -            | f (i, l) = f (i-1, len (Array.sub (arr, i), 0) :: l)
   6.384 -          in
   6.385 -            f ((Array.length arr)-1, [])
   6.386 -          end
   6.387 -
   6.388 -   (*Added by lcp.
   6.389 -      This is essentially the  described in Compilers:
   6.390 -      Principles, Techniques, and Tools, by Aho, Sethi and Ullman.*)
   6.391 -
   6.392 -   (*This hash function is recommended in Compilers: Principles, Techniques, and
   6.393 -     Tools, by Aho, Sethi and Ullman. The hashpjw function, which they particularly
   6.394 -     recommend, triggers a bug in versions of Poly/ML up to 4.2.0.*)
   6.395 -   fun hashw (u,w) = Word.+ (u, Word.*(0w65599,w))
   6.396 -
   6.397 -   fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
   6.398 -   
   6.399 -   fun hashw_int (i,w) = hashw (Word.fromInt i, w);
   6.400 -   
   6.401 -   fun hashw_vector (v,w) = Vector.foldl hashw w v;
   6.402 -   
   6.403 -   fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s;
   6.404 -   
   6.405 -   fun hashw_strings (ss, w) = List.foldl hashw_string w ss;
   6.406 -
   6.407 -   fun hash_string s = Word.toIntX (hashw_string(s,0w0));
   6.408 -
   6.409 -end