new hash table module in HOL/Too/s
authorpaulson
Wed Dec 21 12:06:08 2005 +0100 (2005-12-21)
changeset 18449e314fb38307d
parent 18448 6e805f389355
child 18450 e57731ba01dd
new hash table module in HOL/Too/s
src/HOL/IsaMakefile
src/HOL/ROOT.ML
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/polyhash.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
src/Pure/General/hashtable.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Dec 21 12:05:47 2005 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Dec 21 12:06:08 2005 +0100
     1.3 @@ -90,7 +90,6 @@
     1.4    Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy			\
     1.5    Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
     1.6    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
     1.7 -  $(SRC)/Pure/General/hashtable.ML \
     1.8    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
     1.9    Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
    1.10    Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    1.11 @@ -105,6 +104,7 @@
    1.12    Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML			\
    1.13    Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML		\
    1.14    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
    1.15 +  Tools/polyhash.ML \
    1.16    Tools/recdef_package.ML Tools/recfun_codegen.ML				\
    1.17    Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML		\
    1.18    Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
     2.1 --- a/src/HOL/ROOT.ML	Wed Dec 21 12:05:47 2005 +0100
     2.2 +++ b/src/HOL/ROOT.ML	Wed Dec 21 12:06:08 2005 +0100
     2.3 @@ -11,7 +11,6 @@
     2.4  
     2.5  use "hologic.ML";
     2.6  
     2.7 -use "~~/src/Pure/General/hashtable.ML";
     2.8  use "~~/src/Provers/splitter.ML";
     2.9  use "~~/src/Provers/hypsubst.ML";
    2.10  use "~~/src/Provers/induct_method.ML";
     3.1 --- a/src/HOL/Reconstruction.thy	Wed Dec 21 12:05:47 2005 +0100
     3.2 +++ b/src/HOL/Reconstruction.thy	Wed Dec 21 12:06:08 2005 +0100
     3.3 @@ -8,8 +8,9 @@
     3.4  
     3.5  theory Reconstruction
     3.6  imports Hilbert_Choice Map Infinite_Set Extraction
     3.7 -uses "Tools/res_clause.ML"
     3.8 -         "Tools/res_hol_clause.ML"
     3.9 +uses 	 "Tools/polyhash.ML"
    3.10 +         "Tools/res_clause.ML"
    3.11 +	 "Tools/res_hol_clause.ML"
    3.12  	 "Tools/res_axioms.ML"
    3.13  	 "Tools/ATP/recon_order_clauses.ML"
    3.14  	 "Tools/ATP/recon_translate_proof.ML"
     4.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Dec 21 12:05:47 2005 +0100
     4.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Dec 21 12:06:08 2005 +0100
     4.3 @@ -143,27 +143,30 @@
     4.4      
     4.5  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute
     4.6  Some primes from http://primes.utm.edu/:
     4.7 -   1823   1831   1847   1861   1867   1871   1873   1877   1879   1889 
     4.8 -   1901   1907   1913   1931   1933   1949   1951   1973   1979   1987 
     4.9 -   1993   1997   1999   2003   2011   2017   2027   2029   2039   2053 
    4.10 -   2063   2069   2081   2083   2087   2089   2099   2111   2113   2129 
    4.11  *)
    4.12  
    4.13 -exception HASH_CLAUSE;
    4.14 +exception HASH_CLAUSE and HASH_STRING;
    4.15 +
    4.16 +(*Catches (for deletion) theorems automatically generated from other theorems*)
    4.17 +fun insert_suffixed_names ht x = 
    4.18 +     (Polyhash.insert ht (x^"_iff1", ()); 
    4.19 +      Polyhash.insert ht (x^"_iff2", ()); 
    4.20 +      Polyhash.insert ht (x^"_dest", ())); 
    4.21 +
    4.22 +fun make_suffix_test xs = 
    4.23 +  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    4.24 +                                (6000, HASH_STRING)
    4.25 +      fun suffixed s = isSome (Polyhash.peek ht s)
    4.26 +  in  app (insert_suffixed_names ht) xs; suffixed  end;
    4.27  
    4.28  (*Create a hash table for clauses, of the given size*)
    4.29 -fun mk_clause_table size =
    4.30 -      Hashtable.create{hash = ResClause.hash1_clause, 
    4.31 -		       exn = HASH_CLAUSE,
    4.32 -		       == = ResClause.clause_eq, 
    4.33 -		       size = size};
    4.34 -
    4.35 -(*Insert x only if fresh*)
    4.36 -fun insert_new ht (x,y) = ignore (Hashtable.lookup ht x)
    4.37 -            handle HASH_CLAUSE => Hashtable.insert ht (x,y); 
    4.38 +fun mk_clause_table n =
    4.39 +      Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq)
    4.40 +                       (n, HASH_CLAUSE);
    4.41  
    4.42  (*Use a hash table to eliminate duplicates from xs*)
    4.43 -fun make_unique ht xs = (app (insert_new ht) xs;  Hashtable.map Library.I ht);
    4.44 +fun make_unique ht xs = 
    4.45 +      (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
    4.46  
    4.47  (*Write out the claset and simpset rules of the supplied theory.
    4.48    FIXME: argument "goal" is a hack to allow relevance filtering.
    4.49 @@ -173,15 +176,17 @@
    4.50  	    map put_name_pair
    4.51  	      (ReduceAxiomsN.relevant_filter (!relevant) goal 
    4.52  		(ResAxioms.claset_rules_of_ctxt ctxt))
    4.53 -      val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms
    4.54 -      val simpset_cls_thms = 
    4.55 +      val simpset_thms = 
    4.56  	    if !use_simpset then 
    4.57 -	       ResAxioms.clausify_rules_pairs 
    4.58 -		  (map put_name_pair 
    4.59 +		  map put_name_pair 
    4.60  		    (ReduceAxiomsN.relevant_filter (!relevant) goal
    4.61 -		      (ResAxioms.simpset_rules_of_ctxt ctxt)))
    4.62 +		      (ResAxioms.simpset_rules_of_ctxt ctxt))
    4.63  	    else []
    4.64 -      val cls_thms_list = make_unique (mk_clause_table 2129) 
    4.65 +      val suffixed = make_suffix_test (map #1 (claset_thms@simpset_thms))
    4.66 +      fun ok (a,_) = not (suffixed a)
    4.67 +      val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms)
    4.68 +      val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms)
    4.69 +      val cls_thms_list = make_unique (mk_clause_table 2200) 
    4.70                                        (List.concat (simpset_cls_thms@claset_cls_thms))
    4.71        (* Identify the set of clauses to be written out *)
    4.72        val clauses = map #1(cls_thms_list);
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/polyhash.ML	Wed Dec 21 12:06:08 2005 +0100
     5.3 @@ -0,0 +1,416 @@
     5.4 +(* Modified for Poly/ML from SML/NJ Library version 0.2
     5.5 + *
     5.6 + * COPYRIGHT (c) 1992 by AT&T Bell Laboratories.
     5.7 + * See file mosml/copyrght/copyrght.att for details.
     5.8 + *
     5.9 + * Original author: John Reppy, AT&T Bell Laboratories, Murray Hill, NJ 07974
    5.10 + * Current version largely by Joseph Hurd
    5.11 + *)
    5.12 +
    5.13 +(* Polyhash -- polymorphic hashtables as in the SML/NJ Library *)
    5.14 +
    5.15 +signature Polyhash =
    5.16 +sig
    5.17 +
    5.18 +type ('key, 'data) hash_table
    5.19 +
    5.20 +val mkTable     : ('_key -> int) * ('_key * '_key -> bool) -> int * exn 
    5.21 +                  -> ('_key, '_data) hash_table
    5.22 +val numItems    : ('key, 'data) hash_table -> int
    5.23 +val insert      : ('_key, '_data) hash_table -> '_key * '_data -> unit
    5.24 +val peekInsert  : ('_key, '_data) hash_table -> '_key * '_data 
    5.25 +                  -> '_data option
    5.26 +val find        : ('key, 'data) hash_table -> 'key -> 'data
    5.27 +val peek        : ('key, 'data) hash_table -> 'key -> 'data option
    5.28 +val remove      : ('key, 'data) hash_table -> 'key -> 'data
    5.29 +val listItems   : ('key, 'data) hash_table -> ('key * 'data) list
    5.30 +val apply       : ('key * 'data -> unit) -> ('key, 'data) hash_table -> unit
    5.31 +val map         : ('_key * 'data -> '_res) -> ('_key, 'data) hash_table 
    5.32 +                  -> ('_key, '_res) hash_table
    5.33 +val filter      : ('key * 'data -> bool) -> ('key, 'data) hash_table -> unit
    5.34 +val transform   : ('data -> '_res) -> ('_key, 'data) hash_table 
    5.35 +                  -> ('_key, '_res) hash_table
    5.36 +val copy        : ('_key, '_data) hash_table -> ('_key, '_data) hash_table
    5.37 +val bucketSizes : ('key, 'data) hash_table -> int list
    5.38 +
    5.39 +(*Additions due to L. C. Paulson and Jia Meng*)
    5.40 +val hashw : word * word -> word
    5.41 +val hashw_char : Char.char * word -> word
    5.42 +val hashw_vector : word Vector.vector * word -> word
    5.43 +val hashw_string : string * word -> word
    5.44 +val hashw_strings : string list * word -> word
    5.45 +val hash_string : string -> int
    5.46 +
    5.47 +(* 
    5.48 +   [('key, 'data) hash_table] is the type of hashtables with keys of type
    5.49 +   'key and data values of type 'data.
    5.50 +
    5.51 +   [mkTable (hashVal, sameKey) (sz, exc)] returns a new hashtable,
    5.52 +   using hash function hashVal and equality predicate sameKey.  The sz
    5.53 +   is a size hint, and exc is the exception raised by function find.
    5.54 +   It must be the case that sameKey(k1, k2) implies hashVal(k1) =
    5.55 +   hashVal(k2) for all k1,k2.
    5.56 +
    5.57 +   [numItems htbl] is the number of items in the hash table.
    5.58 +
    5.59 +   [insert htbl (k, d)] inserts data d for key k.  If k already had an
    5.60 +   item associated with it, then the old item is overwritten.
    5.61 +
    5.62 +   [find htbl k] returns d, where d is the data item associated with key k, 
    5.63 +   or raises the exception (given at creation of htbl) if there is no such d.
    5.64 +
    5.65 +   [peek htbl k] returns SOME d, where d is the data item associated with 
    5.66 +   key k, or NONE if there is no such d.
    5.67 +
    5.68 +   [peekInsert htbl (k, d)] inserts data d for key k, if k is not
    5.69 +   already in the table, returning NONE.  If k is already in the
    5.70 +   table, and the associated data value is d', then returns SOME d'
    5.71 +   and leaves the table unmodified.
    5.72 +
    5.73 +   [remove htbl k] returns d, where d is the data item associated with key k, 
    5.74 +   removing d from the table; or raises the exception if there is no such d.
    5.75 +
    5.76 +   [listItems htbl] returns a list of the (key, data) pairs in the hashtable.
    5.77 +
    5.78 +   [apply f htbl] applies function f to all (key, data) pairs in the 
    5.79 +   hashtable, in some order.
    5.80 +
    5.81 +   [map f htbl] returns a new hashtable, whose data items have been
    5.82 +   obtained by applying f to the (key, data) pairs in htbl.  The new
    5.83 +   tables have the same keys, hash function, equality predicate, and
    5.84 +   exception, as htbl.
    5.85 +
    5.86 +   [filter p htbl] deletes from htbl all data items which do not
    5.87 +   satisfy predicate p.
    5.88 +
    5.89 +   [transform f htbl] as map, but only the (old) data values are used
    5.90 +   when computing the new data values.
    5.91 +
    5.92 +   [copy htbl] returns a complete copy of htbl.
    5.93 +
    5.94 +   [bucketSizes htbl] returns a list of the sizes of the buckets.
    5.95 +   This is to allow users to gauge the quality of their hashing
    5.96 +   function.  
    5.97 +*)
    5.98 +
    5.99 +end
   5.100 +
   5.101 +
   5.102 +structure Polyhash :> Polyhash =
   5.103 +struct
   5.104 +
   5.105 +datatype ('key, 'data) bucket_t
   5.106 +  = NIL
   5.107 +  | B of int * 'key * 'data * ('key, 'data) bucket_t
   5.108 +
   5.109 +datatype ('key, 'data) hash_table = 
   5.110 +    HT of {hashVal   : 'key -> int,
   5.111 +	   sameKey   : 'key * 'key -> bool,
   5.112 +	   not_found : exn,
   5.113 +	   table     : ('key, 'data) bucket_t Array.array ref,
   5.114 +	   n_items   : int ref}
   5.115 +
   5.116 +local
   5.117 +(*
   5.118 +    prim_val andb_      : int -> int -> int = 2 "and";
   5.119 +    prim_val lshift_    : int -> int -> int = 2 "shift_left";
   5.120 +*)
   5.121 +    fun andb_ x y = Word.toInt (Word.andb (Word.fromInt x, Word.fromInt y));
   5.122 +    fun lshift_ x y = Word.toInt (Word.<< (Word.fromInt x, Word.fromInt y));
   5.123 +in 
   5.124 +    fun index (i, sz) = andb_ i (sz-1)
   5.125 +
   5.126 +  (* find smallest power of 2 (>= 32) that is >= n *)
   5.127 +    fun roundUp n = 
   5.128 +	let fun f i = if (i >= n) then i else f (lshift_ i 1)
   5.129 +	in f 32 end
   5.130 +end;
   5.131 +
   5.132 +  (* Create a new table; the int is a size hint and the exception
   5.133 +   * is to be raised by find.
   5.134 +   *)
   5.135 +    fun mkTable (hashVal, sameKey) (sizeHint, notFound) = HT{
   5.136 +            hashVal=hashVal,
   5.137 +	    sameKey=sameKey,
   5.138 +	    not_found = notFound,
   5.139 +	    table = ref (Array.array(roundUp sizeHint, NIL)),
   5.140 +	    n_items = ref 0
   5.141 +	  };
   5.142 +
   5.143 +  (* conditionally grow a table *)
   5.144 +    fun growTable (HT{table, n_items, ...}) = let
   5.145 +	    val arr = !table
   5.146 +	    val sz = Array.length arr
   5.147 +	    in
   5.148 +	      if (!n_items >= sz)
   5.149 +		then let
   5.150 +		  val newSz = sz+sz
   5.151 +		  val newArr = Array.array (newSz, NIL)
   5.152 +		  fun copy NIL = ()
   5.153 +		    | copy (B(h, key, v, rest)) = let
   5.154 +			val indx = index (h, newSz)
   5.155 +			in
   5.156 +			  Array.update (newArr, indx,
   5.157 +			    B(h, key, v, Array.sub(newArr, indx)));
   5.158 +			  copy rest
   5.159 +			end
   5.160 +		  fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1))
   5.161 +		  in
   5.162 +		    (bucket 0) handle _ => ();
   5.163 +		    table := newArr
   5.164 +		  end
   5.165 +		else ()
   5.166 +	    end (* growTable *);
   5.167 +
   5.168 +  (* Insert an item.  If the key already has an item associated with it,
   5.169 +   * then the old item is discarded.
   5.170 +   *)
   5.171 +    fun insert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
   5.172 +	let
   5.173 +	  val arr = !table
   5.174 +	  val sz = Array.length arr
   5.175 +	  val hash = hashVal key
   5.176 +	  val indx = index (hash, sz)
   5.177 +	  fun look NIL = (
   5.178 +		Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
   5.179 +		n_items := !n_items + 1;
   5.180 +		growTable tbl;
   5.181 +		NIL)
   5.182 +	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   5.183 +		then B(hash, key, item, r)
   5.184 +		else (case (look r)
   5.185 +		   of NIL => NIL
   5.186 +		    | rest => B(h, k, v, rest)
   5.187 +		  (* end case *))
   5.188 +	  in
   5.189 +	    case (look (Array.sub (arr, indx)))
   5.190 +	     of NIL => ()
   5.191 +	      | b => Array.update(arr, indx, b)
   5.192 +	  end;
   5.193 +
   5.194 +  (* Insert an item if not there already; if it is there already, 
   5.195 +     then return the old data value and leave the table unmodified..
   5.196 +   *)
   5.197 +    fun peekInsert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) =
   5.198 +	let val arr = !table
   5.199 +	    val sz = Array.length arr
   5.200 +	    val hash = hashVal key
   5.201 +	    val indx = index (hash, sz)
   5.202 +	    fun look NIL = 
   5.203 +		(Array.update(arr, indx, B(hash, key, item, 
   5.204 +					   Array.sub(arr, indx)));
   5.205 +		 n_items := !n_items + 1;
   5.206 +		 growTable tbl;
   5.207 +		 NONE)
   5.208 +	      | look (B(h, k, v, r)) = 
   5.209 +		if hash = h andalso sameKey(key, k) then SOME v
   5.210 +		else look r
   5.211 +	in
   5.212 +	    look (Array.sub (arr, indx))
   5.213 +	end;
   5.214 +
   5.215 +  (* find an item, the table's exception is raised if the item doesn't exist *)
   5.216 +    fun find (HT{hashVal, sameKey, table, not_found, ...}) key = let
   5.217 +	  val arr = !table
   5.218 +	  val sz = Array.length arr
   5.219 +	  val hash = hashVal key
   5.220 +	  val indx = index (hash, sz)
   5.221 +	  fun look NIL = raise not_found
   5.222 +	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   5.223 +		then v
   5.224 +		else look r
   5.225 +	  in
   5.226 +	    look (Array.sub (arr, indx))
   5.227 +	  end;
   5.228 +
   5.229 +  (* look for an item, return NONE if the item doesn't exist *)
   5.230 +    fun peek (HT{hashVal, sameKey, table, ...}) key = let
   5.231 +	  val arr = !table
   5.232 +	  val sz = Array.length arr
   5.233 +	  val hash = hashVal key
   5.234 +	  val indx = index (hash, sz)
   5.235 +	  fun look NIL = NONE
   5.236 +	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   5.237 +		then SOME v
   5.238 +		else look r
   5.239 +	  in
   5.240 +	    look (Array.sub (arr, indx))
   5.241 +	  end;
   5.242 +
   5.243 +  (* Remove an item.  The table's exception is raised if
   5.244 +   * the item doesn't exist.
   5.245 +   *)
   5.246 +    fun remove (HT{hashVal, sameKey, not_found, table, n_items}) key = let
   5.247 +	  val arr = !table
   5.248 +	  val sz = Array.length arr
   5.249 +	  val hash = hashVal key
   5.250 +	  val indx = index (hash, sz)
   5.251 +	  fun look NIL = raise not_found
   5.252 +	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
   5.253 +		then (v, r)
   5.254 +		else let val (item, r') = look r in (item, B(h, k, v, r')) end
   5.255 +	  val (item, bucket) = look (Array.sub (arr, indx))
   5.256 +	  in
   5.257 +	    Array.update (arr, indx, bucket);
   5.258 +	    n_items := !n_items - 1;
   5.259 +	    item
   5.260 +	  end (* remove *);
   5.261 +
   5.262 +  (* Return the number of items in the table *)
   5.263 +   fun numItems (HT{n_items, ...}) = !n_items
   5.264 +
   5.265 +  (* return a list of the items in the table *)
   5.266 +    fun listItems (HT{table = ref arr, n_items, ...}) = let
   5.267 +	  fun f (_, l, 0) = l
   5.268 +	    | f (~1, l, _) = l
   5.269 +	    | f (i, l, n) = let
   5.270 +		fun g (NIL, l, n) = f (i-1, l, n)
   5.271 +		  | g (B(_, k, v, r), l, n) = g(r, (k, v)::l, n-1)
   5.272 +		in
   5.273 +		  g (Array.sub(arr, i), l, n)
   5.274 +		end
   5.275 +	  in
   5.276 +	    f ((Array.length arr) - 1, [], !n_items)
   5.277 +	  end (* listItems *);
   5.278 +
   5.279 +  (* Apply a function to the entries of the table *)
   5.280 +    fun apply f (HT{table, ...}) = let
   5.281 +	  fun appF NIL = ()
   5.282 +	    | appF (B(_, key, item, rest)) = (
   5.283 +		f (key, item);
   5.284 +		appF rest)
   5.285 +	  val arr = !table
   5.286 +	  val sz = Array.length arr
   5.287 +	  fun appToTbl i = if (i < sz)
   5.288 +		then (appF (Array.sub (arr, i)); appToTbl(i+1))
   5.289 +		else ()
   5.290 +	  in
   5.291 +	    appToTbl 0
   5.292 +	  end (* apply *);
   5.293 +
   5.294 +  (* Map a table to a new table that has the same keys and exception *)
   5.295 +    fun map f (HT{hashVal, sameKey, table, n_items, not_found}) = let
   5.296 +	  fun mapF NIL = NIL
   5.297 +	    | mapF (B(hash, key, item, rest)) =
   5.298 +		B(hash, key, f (key, item), mapF rest)
   5.299 +	  val arr = !table
   5.300 +	  val sz = Array.length arr
   5.301 +	  val newArr = Array.array (sz, NIL)
   5.302 +	  fun mapTbl i = if (i < sz)
   5.303 +		then (
   5.304 +		  Array.update(newArr, i, mapF (Array.sub(arr, i)));
   5.305 +		  mapTbl (i+1))
   5.306 +		else ()
   5.307 +	  in
   5.308 +	    mapTbl 0;
   5.309 +	    HT{hashVal=hashVal,
   5.310 +	       sameKey=sameKey,
   5.311 +	       table = ref newArr, 
   5.312 +	       n_items = ref(!n_items), 
   5.313 +	       not_found = not_found}
   5.314 +	  end (* transform *);
   5.315 +
   5.316 +  (* remove any hash table items that do not satisfy the given
   5.317 +   * predicate.
   5.318 +   *)
   5.319 +    fun filter pred (HT{table, n_items, not_found, ...}) = let
   5.320 +	  fun filterP NIL = NIL
   5.321 +	    | filterP (B(hash, key, item, rest)) = if (pred(key, item))
   5.322 +		then B(hash, key, item, filterP rest)
   5.323 +		else filterP rest
   5.324 +	  val arr = !table
   5.325 +	  val sz = Array.length arr
   5.326 +	  fun filterTbl i = if (i < sz)
   5.327 +		then (
   5.328 +		  Array.update (arr, i, filterP (Array.sub (arr, i)));
   5.329 +		  filterTbl (i+1))
   5.330 +		else ()
   5.331 +	  in
   5.332 +	    filterTbl 0
   5.333 +	  end (* filter *);
   5.334 +
   5.335 +  (* Map a table to a new table that has the same keys, exception,
   5.336 +     hash function, and equality function *)
   5.337 +
   5.338 +    fun transform f (HT{hashVal, sameKey, table, n_items, not_found}) = let
   5.339 +	  fun mapF NIL = NIL
   5.340 +	    | mapF (B(hash, key, item, rest)) = B(hash, key, f item, mapF rest)
   5.341 +	  val arr = !table
   5.342 +	  val sz = Array.length arr
   5.343 +	  val newArr = Array.array (sz, NIL)
   5.344 +	  fun mapTbl i = if (i < sz)
   5.345 +		then (
   5.346 +		  Array.update(newArr, i, mapF (Array.sub(arr, i)));
   5.347 +		  mapTbl (i+1))
   5.348 +		else ()
   5.349 +	  in
   5.350 +	    mapTbl 0;
   5.351 +	    HT{hashVal=hashVal, 
   5.352 +	       sameKey=sameKey, 
   5.353 +	       table = ref newArr, 
   5.354 +	       n_items = ref(!n_items), 
   5.355 +	       not_found = not_found}
   5.356 +	  end (* transform *);
   5.357 +
   5.358 +  (* Create a copy of a hash table *)
   5.359 +    fun copy (HT{hashVal, sameKey, table, n_items, not_found}) = let
   5.360 +	  val arr = !table
   5.361 +	  val sz = Array.length arr
   5.362 +	  val newArr = Array.array (sz, NIL)
   5.363 +	  fun mapTbl i = (
   5.364 +		Array.update (newArr, i, Array.sub(arr, i));
   5.365 +		mapTbl (i+1))
   5.366 +	  in
   5.367 +	    (mapTbl 0) handle _ => ();
   5.368 +	    HT{hashVal=hashVal, 
   5.369 +	       sameKey=sameKey,
   5.370 +	       table = ref newArr, 
   5.371 +	       n_items = ref(!n_items), 
   5.372 +	       not_found = not_found}
   5.373 +	  end (* copy *);
   5.374 +
   5.375 +  (* returns a list of the sizes of the various buckets.  This is to
   5.376 +   * allow users to gauge the quality of their hashing function.
   5.377 +   *)
   5.378 +    fun bucketSizes (HT{table = ref arr, ...}) = let
   5.379 +	  fun len (NIL, n) = n
   5.380 +	    | len (B(_, _, _, r), n) = len(r, n+1)
   5.381 +	  fun f (~1, l) = l
   5.382 +	    | f (i, l) = f (i-1, len (Array.sub (arr, i), 0) :: l)
   5.383 +	  in
   5.384 +	    f ((Array.length arr)-1, [])
   5.385 +	  end
   5.386 +
   5.387 +   (*Added by lcp.
   5.388 +      This is essentially the hashpjw function described in Compilers:
   5.389 +      Principles, Techniques, and Tools, by Aho, Sethi and Ullman.*)
   5.390 + (*  local infix << >>
   5.391 +	 val left = Word.fromInt (Word.wordSize - 4)
   5.392 +	 val right = Word.fromInt (Word.wordSize - 8)
   5.393 +	 open Word
   5.394 +   in  
   5.395 +   val mask = 0wxf << left
   5.396 +   fun hashw (u,w) =
   5.397 +     let val w' = (w << 0w4) + u
   5.398 +	 val g = Word.andb(w', mask)  
   5.399 +     in  
   5.400 +	 if g <> 0w0 then Word.xorb(g, Word.xorb(w', g >> right))
   5.401 +	 else w'
   5.402 +     end;
   5.403 +   end;*)
   5.404 +
   5.405 +   (*This version is also recommended by Aho et al. and does not trigger the Poly/ML bug*)
   5.406 +   val hmulti = Word.fromInt 65599;
   5.407 +   fun hashw (u,w) = Word.+ (u, Word.*(hmulti,w))
   5.408 +
   5.409 +   fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w);
   5.410 +   
   5.411 +   fun hashw_vector (v,w) = Vector.foldl hashw w v;
   5.412 +   
   5.413 +   fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s;
   5.414 +   
   5.415 +   fun hashw_strings (ss, w) = List.foldl hashw_string w ss;
   5.416 +
   5.417 +   fun hash_string s = Word.toIntX (hashw_string(s,0w0));
   5.418 +
   5.419 +end
     6.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 21 12:05:47 2005 +0100
     6.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Dec 21 12:06:08 2005 +0100
     6.3 @@ -71,7 +71,7 @@
     6.4  
     6.5    (*for hashing*)
     6.6    val clause_eq : clause * clause -> bool
     6.7 -  val hash1_clause : clause -> word
     6.8 +  val hash_clause : clause -> int
     6.9  
    6.10    val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
    6.11    type fol_type
    6.12 @@ -659,17 +659,17 @@
    6.13  
    6.14  val xor_words = List.foldl Word.xorb 0w0;
    6.15  
    6.16 -fun hash_term (UVar(_,_), w) = w
    6.17 -  | hash_term (Fun(f,tps,args), w) = 
    6.18 -      List.foldl hash_term (Hashtable.hash_string (f,w)) args;
    6.19 +fun hashw_term (UVar(_,_), w) = w
    6.20 +  | hashw_term (Fun(f,tps,args), w) = 
    6.21 +      List.foldl hashw_term (Polyhash.hashw_string (f,w)) args;
    6.22    
    6.23 -fun hash_pred (Predicate(pn,_,args), w) = 
    6.24 -    List.foldl hash_term (Hashtable.hash_string (pn,w)) args;
    6.25 +fun hashw_pred (Predicate(pn,_,args), w) = 
    6.26 +    List.foldl hashw_term (Polyhash.hashw_string (pn,w)) args;
    6.27      
    6.28 -fun hash1_literal (Literal(true,pred,_)) = hash_pred (pred, 0w0)
    6.29 -  | hash1_literal (Literal(false,pred,_)) = Word.notb (hash_pred (pred, 0w0));
    6.30 +fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0)
    6.31 +  | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0));
    6.32    
    6.33 -fun hash1_clause clause = xor_words (map hash1_literal (get_literals clause));
    6.34 +fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause)));
    6.35  
    6.36  
    6.37  (* FIX: not sure what to do with these funcs *)
     7.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Dec 21 12:05:47 2005 +0100
     7.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Dec 21 12:06:08 2005 +0100
     7.3 @@ -709,13 +709,12 @@
     7.4  val xor_words = List.foldl Word.xorb 0w0;
     7.5  
     7.6  fun hash_combterm (CombVar(_,_),w) = w
     7.7 -  | hash_combterm (CombFree(f,_),w) = Hashtable.hash_string(f,w)
     7.8 -  | hash_combterm (CombConst(c,tp,tps),w) = Hashtable.hash_string(c,w)
     7.9 -  | hash_combterm (CombApp(f,arg,tp),w) = 
    7.10 -    hash_combterm (arg, (hash_combterm (f,w)))
    7.11 +  | hash_combterm (CombFree(f,_),w) = Polyhash.hashw_string(f,w)
    7.12 +  | hash_combterm (CombConst(c,tp,tps),w) = Polyhash.hashw_string(c,w)
    7.13 +  | hash_combterm (CombApp(f,arg,tp),w) = hash_combterm (arg, hash_combterm (f,w))
    7.14    | hash_combterm (Bool(t),w) = hash_combterm (t,w)
    7.15    | hash_combterm (Equal(t1,t2),w) = 
    7.16 -    List.foldl hash_combterm (Hashtable.hash_string ("equal",w)) [t1,t2]
    7.17 +    List.foldl hash_combterm (Polyhash.hashw_string ("equal",w)) [t1,t2]
    7.18  
    7.19  fun hash_literal (Literal(true,pred)) = hash_combterm(pred,0w0)
    7.20    | hash_literal (Literal(false,pred)) = Word.notb(hash_combterm(pred,0w0));
     8.1 --- a/src/Pure/General/hashtable.ML	Wed Dec 21 12:05:47 2005 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,133 +0,0 @@
     8.4 -(*Hash tables. Taken from SML/NJ version 110.57.
     8.5 -  Copyright (c) 1989-2002 by Lucent Technologies*)
     8.6 -signature HASHTABLE =
     8.7 -sig
     8.8 -   type ('a,'b) table
     8.9 -
    8.10 -   val create : { hash : 'a -> word, 
    8.11 -                  ==   : 'a * 'a -> bool,
    8.12 -                  exn  : exn,
    8.13 -                  size : int 
    8.14 -                } -> ('a,'b) table 
    8.15 -
    8.16 -   val size         : ('a,'b) table -> int
    8.17 -   val clear        : ('a,'b) table -> unit
    8.18 -   val insert       : ('a,'b) table -> 'a * 'b -> unit
    8.19 -   val remove       : ('a,'b) table -> 'a -> unit
    8.20 -   val lookup       : ('a,'b) table -> 'a -> 'b 
    8.21 -   val copy         : ('a,'b) table -> ('a,'b) table
    8.22 -   val app          : ('a * 'b -> unit) -> ('a,'b) table -> unit
    8.23 -   val map          : ('a * 'b -> 'c) -> ('a,'b) table -> 'c list
    8.24 -   val fold         : ('a * 'b * 'c -> 'c) -> 'c -> ('a,'b) table -> 'c
    8.25 -
    8.26 -   (*Additions due to L. C. Paulson and Jia Meng*)
    8.27 -   val hash_word : word * word -> word
    8.28 -   val hash_char : Char.char * word -> word
    8.29 -   val hash_vector : word Vector.vector * word -> word
    8.30 -   val hash_string : string * word -> word
    8.31 -   val hash_strings : string list * word -> word
    8.32 -end
    8.33 -
    8.34 -structure Hashtable :> HASHTABLE =
    8.35 -struct
    8.36 -
    8.37 -   structure A = Array
    8.38 -
    8.39 -   type ('a,'b) table = ('a -> word) * 
    8.40 -                        ('a * 'a -> bool) *
    8.41 -                        exn *
    8.42 -                        ('a * 'b) list A.array ref * 
    8.43 -                        int ref
    8.44 -
    8.45 -   infix ==
    8.46 -
    8.47 -   fun create{hash,==,exn,size} = (hash,op==,exn,ref(A.array(size,[])),ref 0)
    8.48 -   fun copy(hash,op==,exn,ref a,ref c) = 
    8.49 -         (hash,op==,exn,ref(A.tabulate(A.length a,fn i => A.sub(a,i))), ref c)
    8.50 -   fun size (_,_,_,_,ref n) = n
    8.51 -   fun clear (_,_,_,ref a,c) =
    8.52 -       let fun f ~1 = ()
    8.53 -             | f i  = (A.update(a,i,[]); f(i-1))
    8.54 -       in  f(A.length a - 1); c := 0 end
    8.55 -   fun insert (hash,op==,exn,A as ref a,c) (k,v) =
    8.56 -   let val N  = A.length a
    8.57 -       val h  = Word.toIntX(hash k) mod N
    8.58 -       val es = A.sub(a,h)
    8.59 -       fun insrt ([],es') = (A.update(a,h,(k,v)::es'); 
    8.60 -			     c := !c + 1;
    8.61 -			     if !c >= N then grow(hash,A,N) else ())
    8.62 -         | insrt ((e as (k',_))::es,es') = 
    8.63 -            if k == k' then A.update(a,h,(k,v)::es'@es) 
    8.64 -            else insrt(es,e::es')
    8.65 -   in  insrt (es,[])
    8.66 -   end
    8.67 -
    8.68 -   and grow(hash,A as ref a,N) =
    8.69 -       let val M = N + N
    8.70 -           val M = if M < 13 then 13 else M
    8.71 -           val a' = A.array(M,[])
    8.72 -           fun insrt (k,v) = let val h = Word.toIntX(hash k) mod M
    8.73 -                             in  A.update(a',h,(k,v)::A.sub(a',h)) end
    8.74 -       in  A.app (fn es => app insrt es) a;
    8.75 -           A := a'
    8.76 -       end
    8.77 -
    8.78 -   fun remove (hash,op==,exn,ref a,c) k =
    8.79 -   let val N  = A.length a
    8.80 -       val h  = Word.toIntX(hash k) mod N
    8.81 -       val es = A.sub(a,h)
    8.82 -       fun del ([],es') = ()
    8.83 -         | del ((e as (k',_))::es,es') = 
    8.84 -            if k == k' then (A.update(a,h,es'@es); c := !c - 1)
    8.85 -            else del(es,e::es')
    8.86 -   in  del (es,[])
    8.87 -   end
    8.88 - 
    8.89 -   fun lookup(hash,op==,exn,ref a,_) k =
    8.90 -   let val N  = A.length a
    8.91 -       val h  = Word.toIntX(hash k) mod N
    8.92 -       fun find [] = raise exn
    8.93 -         | find ((k',v)::es) = if k == k' then v else find es
    8.94 -   in  find(A.sub(a,h))
    8.95 -   end
    8.96 -
    8.97 -   fun app f (_,_,_,ref A,_) = A.app (List.app f) A
    8.98 -
    8.99 -   fun map f (_,_,_,ref A,_) =
   8.100 -   let fun fl([],x) = x
   8.101 -         | fl((k,v)::es,x) = f(k,v)::fl(es,x)
   8.102 -   in  A.foldr fl [] A end
   8.103 -
   8.104 -   fun fold f x (_,_,_,ref A,_) = 
   8.105 -   let fun fl([],x) = x
   8.106 -         | fl((k,v)::es,x) = f(k,v,fl(es,x))
   8.107 -   in  A.foldr fl x A end
   8.108 -
   8.109 -
   8.110 -   (*Additions due to L. C. Paulson and Jia Meng*)
   8.111 -
   8.112 -   val myw = ref 0w0;
   8.113 -   val () = myw := 0wx70000000;  (*workaround for Poly/ML bug*)
   8.114 -
   8.115 -   local open Word
   8.116 -	 infix << >>
   8.117 -   in
   8.118 -   fun hash_word (u,w) =
   8.119 -     let val w' = (w << 0w4) + u
   8.120 -	 val g = Word.andb(w', !myw)    (*I hope this hex constant is correct!*)
   8.121 -     in  
   8.122 -	 if g = 0w0 then Word.xorb(w', Word.xorb(g, g >> 0w24))
   8.123 -	 else w'
   8.124 -     end;
   8.125 -   end;
   8.126 -   
   8.127 -   fun hash_char (c,w) = hash_word (Word.fromInt (Char.ord c), w);
   8.128 -   
   8.129 -   fun hash_vector (v,w) = Vector.foldl hash_word w v;
   8.130 -   
   8.131 -   fun hash_string (s:string, w) = CharVector.foldl hash_char w s;
   8.132 -   
   8.133 -   fun hash_strings (ss, w) = List.foldl hash_string w ss;
   8.134 -
   8.135 -end
   8.136 -