# HG changeset patch # User paulson # Date 1135163168 -3600 # Node ID e314fb38307da34c3470ebff495325324f8b0f81 # Parent 6e805f389355972dd29b6a99fe457d289144740d new hash table module in HOL/Too/s diff -r 6e805f389355 -r e314fb38307d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 21 12:06:08 2005 +0100 @@ -90,7 +90,6 @@ Lattice_Locales.thy List.ML List.thy Main.ML Main.thy Map.thy \ Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy \ Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy \ - $(SRC)/Pure/General/hashtable.ML \ ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy \ Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML \ Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML \ @@ -105,6 +104,7 @@ Tools/datatype_rep_proofs.ML Tools/inductive_codegen.ML \ Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML \ + Tools/polyhash.ML \ Tools/recdef_package.ML Tools/recfun_codegen.ML \ Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML \ Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \ diff -r 6e805f389355 -r e314fb38307d src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/ROOT.ML Wed Dec 21 12:06:08 2005 +0100 @@ -11,7 +11,6 @@ use "hologic.ML"; -use "~~/src/Pure/General/hashtable.ML"; use "~~/src/Provers/splitter.ML"; use "~~/src/Provers/hypsubst.ML"; use "~~/src/Provers/induct_method.ML"; diff -r 6e805f389355 -r e314fb38307d src/HOL/Reconstruction.thy --- a/src/HOL/Reconstruction.thy Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/Reconstruction.thy Wed Dec 21 12:06:08 2005 +0100 @@ -8,8 +8,9 @@ theory Reconstruction imports Hilbert_Choice Map Infinite_Set Extraction -uses "Tools/res_clause.ML" - "Tools/res_hol_clause.ML" +uses "Tools/polyhash.ML" + "Tools/res_clause.ML" + "Tools/res_hol_clause.ML" "Tools/res_axioms.ML" "Tools/ATP/recon_order_clauses.ML" "Tools/ATP/recon_translate_proof.ML" diff -r 6e805f389355 -r e314fb38307d src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Dec 21 12:06:08 2005 +0100 @@ -143,27 +143,30 @@ (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute Some primes from http://primes.utm.edu/: - 1823 1831 1847 1861 1867 1871 1873 1877 1879 1889 - 1901 1907 1913 1931 1933 1949 1951 1973 1979 1987 - 1993 1997 1999 2003 2011 2017 2027 2029 2039 2053 - 2063 2069 2081 2083 2087 2089 2099 2111 2113 2129 *) -exception HASH_CLAUSE; +exception HASH_CLAUSE and HASH_STRING; + +(*Catches (for deletion) theorems automatically generated from other theorems*) +fun insert_suffixed_names ht x = + (Polyhash.insert ht (x^"_iff1", ()); + Polyhash.insert ht (x^"_iff2", ()); + Polyhash.insert ht (x^"_dest", ())); + +fun make_suffix_test xs = + let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) + (6000, HASH_STRING) + fun suffixed s = isSome (Polyhash.peek ht s) + in app (insert_suffixed_names ht) xs; suffixed end; (*Create a hash table for clauses, of the given size*) -fun mk_clause_table size = - Hashtable.create{hash = ResClause.hash1_clause, - exn = HASH_CLAUSE, - == = ResClause.clause_eq, - size = size}; - -(*Insert x only if fresh*) -fun insert_new ht (x,y) = ignore (Hashtable.lookup ht x) - handle HASH_CLAUSE => Hashtable.insert ht (x,y); +fun mk_clause_table n = + Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq) + (n, HASH_CLAUSE); (*Use a hash table to eliminate duplicates from xs*) -fun make_unique ht xs = (app (insert_new ht) xs; Hashtable.map Library.I ht); +fun make_unique ht xs = + (app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht); (*Write out the claset and simpset rules of the supplied theory. FIXME: argument "goal" is a hack to allow relevance filtering. @@ -173,15 +176,17 @@ map put_name_pair (ReduceAxiomsN.relevant_filter (!relevant) goal (ResAxioms.claset_rules_of_ctxt ctxt)) - val claset_cls_thms = ResAxioms.clausify_rules_pairs claset_thms - val simpset_cls_thms = + val simpset_thms = if !use_simpset then - ResAxioms.clausify_rules_pairs - (map put_name_pair + map put_name_pair (ReduceAxiomsN.relevant_filter (!relevant) goal - (ResAxioms.simpset_rules_of_ctxt ctxt))) + (ResAxioms.simpset_rules_of_ctxt ctxt)) else [] - val cls_thms_list = make_unique (mk_clause_table 2129) + val suffixed = make_suffix_test (map #1 (claset_thms@simpset_thms)) + fun ok (a,_) = not (suffixed a) + val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms) + val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms) + val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (simpset_cls_thms@claset_cls_thms)) (* Identify the set of clauses to be written out *) val clauses = map #1(cls_thms_list); diff -r 6e805f389355 -r e314fb38307d src/HOL/Tools/polyhash.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/polyhash.ML Wed Dec 21 12:06:08 2005 +0100 @@ -0,0 +1,416 @@ +(* Modified for Poly/ML from SML/NJ Library version 0.2 + * + * COPYRIGHT (c) 1992 by AT&T Bell Laboratories. + * See file mosml/copyrght/copyrght.att for details. + * + * Original author: John Reppy, AT&T Bell Laboratories, Murray Hill, NJ 07974 + * Current version largely by Joseph Hurd + *) + +(* Polyhash -- polymorphic hashtables as in the SML/NJ Library *) + +signature Polyhash = +sig + +type ('key, 'data) hash_table + +val mkTable : ('_key -> int) * ('_key * '_key -> bool) -> int * exn + -> ('_key, '_data) hash_table +val numItems : ('key, 'data) hash_table -> int +val insert : ('_key, '_data) hash_table -> '_key * '_data -> unit +val peekInsert : ('_key, '_data) hash_table -> '_key * '_data + -> '_data option +val find : ('key, 'data) hash_table -> 'key -> 'data +val peek : ('key, 'data) hash_table -> 'key -> 'data option +val remove : ('key, 'data) hash_table -> 'key -> 'data +val listItems : ('key, 'data) hash_table -> ('key * 'data) list +val apply : ('key * 'data -> unit) -> ('key, 'data) hash_table -> unit +val map : ('_key * 'data -> '_res) -> ('_key, 'data) hash_table + -> ('_key, '_res) hash_table +val filter : ('key * 'data -> bool) -> ('key, 'data) hash_table -> unit +val transform : ('data -> '_res) -> ('_key, 'data) hash_table + -> ('_key, '_res) hash_table +val copy : ('_key, '_data) hash_table -> ('_key, '_data) hash_table +val bucketSizes : ('key, 'data) hash_table -> int list + +(*Additions due to L. C. Paulson and Jia Meng*) +val hashw : word * word -> word +val hashw_char : Char.char * word -> word +val hashw_vector : word Vector.vector * word -> word +val hashw_string : string * word -> word +val hashw_strings : string list * word -> word +val hash_string : string -> int + +(* + [('key, 'data) hash_table] is the type of hashtables with keys of type + 'key and data values of type 'data. + + [mkTable (hashVal, sameKey) (sz, exc)] returns a new hashtable, + using hash function hashVal and equality predicate sameKey. The sz + is a size hint, and exc is the exception raised by function find. + It must be the case that sameKey(k1, k2) implies hashVal(k1) = + hashVal(k2) for all k1,k2. + + [numItems htbl] is the number of items in the hash table. + + [insert htbl (k, d)] inserts data d for key k. If k already had an + item associated with it, then the old item is overwritten. + + [find htbl k] returns d, where d is the data item associated with key k, + or raises the exception (given at creation of htbl) if there is no such d. + + [peek htbl k] returns SOME d, where d is the data item associated with + key k, or NONE if there is no such d. + + [peekInsert htbl (k, d)] inserts data d for key k, if k is not + already in the table, returning NONE. If k is already in the + table, and the associated data value is d', then returns SOME d' + and leaves the table unmodified. + + [remove htbl k] returns d, where d is the data item associated with key k, + removing d from the table; or raises the exception if there is no such d. + + [listItems htbl] returns a list of the (key, data) pairs in the hashtable. + + [apply f htbl] applies function f to all (key, data) pairs in the + hashtable, in some order. + + [map f htbl] returns a new hashtable, whose data items have been + obtained by applying f to the (key, data) pairs in htbl. The new + tables have the same keys, hash function, equality predicate, and + exception, as htbl. + + [filter p htbl] deletes from htbl all data items which do not + satisfy predicate p. + + [transform f htbl] as map, but only the (old) data values are used + when computing the new data values. + + [copy htbl] returns a complete copy of htbl. + + [bucketSizes htbl] returns a list of the sizes of the buckets. + This is to allow users to gauge the quality of their hashing + function. +*) + +end + + +structure Polyhash :> Polyhash = +struct + +datatype ('key, 'data) bucket_t + = NIL + | B of int * 'key * 'data * ('key, 'data) bucket_t + +datatype ('key, 'data) hash_table = + HT of {hashVal : 'key -> int, + sameKey : 'key * 'key -> bool, + not_found : exn, + table : ('key, 'data) bucket_t Array.array ref, + n_items : int ref} + +local +(* + prim_val andb_ : int -> int -> int = 2 "and"; + prim_val lshift_ : int -> int -> int = 2 "shift_left"; +*) + fun andb_ x y = Word.toInt (Word.andb (Word.fromInt x, Word.fromInt y)); + fun lshift_ x y = Word.toInt (Word.<< (Word.fromInt x, Word.fromInt y)); +in + fun index (i, sz) = andb_ i (sz-1) + + (* find smallest power of 2 (>= 32) that is >= n *) + fun roundUp n = + let fun f i = if (i >= n) then i else f (lshift_ i 1) + in f 32 end +end; + + (* Create a new table; the int is a size hint and the exception + * is to be raised by find. + *) + fun mkTable (hashVal, sameKey) (sizeHint, notFound) = HT{ + hashVal=hashVal, + sameKey=sameKey, + not_found = notFound, + table = ref (Array.array(roundUp sizeHint, NIL)), + n_items = ref 0 + }; + + (* conditionally grow a table *) + fun growTable (HT{table, n_items, ...}) = let + val arr = !table + val sz = Array.length arr + in + if (!n_items >= sz) + then let + val newSz = sz+sz + val newArr = Array.array (newSz, NIL) + fun copy NIL = () + | copy (B(h, key, v, rest)) = let + val indx = index (h, newSz) + in + Array.update (newArr, indx, + B(h, key, v, Array.sub(newArr, indx))); + copy rest + end + fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1)) + in + (bucket 0) handle _ => (); + table := newArr + end + else () + end (* growTable *); + + (* Insert an item. If the key already has an item associated with it, + * then the old item is discarded. + *) + fun insert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) = + let + val arr = !table + val sz = Array.length arr + val hash = hashVal key + val indx = index (hash, sz) + fun look NIL = ( + Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx))); + n_items := !n_items + 1; + growTable tbl; + NIL) + | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k)) + then B(hash, key, item, r) + else (case (look r) + of NIL => NIL + | rest => B(h, k, v, rest) + (* end case *)) + in + case (look (Array.sub (arr, indx))) + of NIL => () + | b => Array.update(arr, indx, b) + end; + + (* Insert an item if not there already; if it is there already, + then return the old data value and leave the table unmodified.. + *) + fun peekInsert (tbl as HT{hashVal, sameKey, table, n_items, ...}) (key, item) = + let val arr = !table + val sz = Array.length arr + val hash = hashVal key + val indx = index (hash, sz) + fun look NIL = + (Array.update(arr, indx, B(hash, key, item, + Array.sub(arr, indx))); + n_items := !n_items + 1; + growTable tbl; + NONE) + | look (B(h, k, v, r)) = + if hash = h andalso sameKey(key, k) then SOME v + else look r + in + look (Array.sub (arr, indx)) + end; + + (* find an item, the table's exception is raised if the item doesn't exist *) + fun find (HT{hashVal, sameKey, table, not_found, ...}) key = let + val arr = !table + val sz = Array.length arr + val hash = hashVal key + val indx = index (hash, sz) + fun look NIL = raise not_found + | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k)) + then v + else look r + in + look (Array.sub (arr, indx)) + end; + + (* look for an item, return NONE if the item doesn't exist *) + fun peek (HT{hashVal, sameKey, table, ...}) key = let + val arr = !table + val sz = Array.length arr + val hash = hashVal key + val indx = index (hash, sz) + fun look NIL = NONE + | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k)) + then SOME v + else look r + in + look (Array.sub (arr, indx)) + end; + + (* Remove an item. The table's exception is raised if + * the item doesn't exist. + *) + fun remove (HT{hashVal, sameKey, not_found, table, n_items}) key = let + val arr = !table + val sz = Array.length arr + val hash = hashVal key + val indx = index (hash, sz) + fun look NIL = raise not_found + | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k)) + then (v, r) + else let val (item, r') = look r in (item, B(h, k, v, r')) end + val (item, bucket) = look (Array.sub (arr, indx)) + in + Array.update (arr, indx, bucket); + n_items := !n_items - 1; + item + end (* remove *); + + (* Return the number of items in the table *) + fun numItems (HT{n_items, ...}) = !n_items + + (* return a list of the items in the table *) + fun listItems (HT{table = ref arr, n_items, ...}) = let + fun f (_, l, 0) = l + | f (~1, l, _) = l + | f (i, l, n) = let + fun g (NIL, l, n) = f (i-1, l, n) + | g (B(_, k, v, r), l, n) = g(r, (k, v)::l, n-1) + in + g (Array.sub(arr, i), l, n) + end + in + f ((Array.length arr) - 1, [], !n_items) + end (* listItems *); + + (* Apply a function to the entries of the table *) + fun apply f (HT{table, ...}) = let + fun appF NIL = () + | appF (B(_, key, item, rest)) = ( + f (key, item); + appF rest) + val arr = !table + val sz = Array.length arr + fun appToTbl i = if (i < sz) + then (appF (Array.sub (arr, i)); appToTbl(i+1)) + else () + in + appToTbl 0 + end (* apply *); + + (* Map a table to a new table that has the same keys and exception *) + fun map f (HT{hashVal, sameKey, table, n_items, not_found}) = let + fun mapF NIL = NIL + | mapF (B(hash, key, item, rest)) = + B(hash, key, f (key, item), mapF rest) + val arr = !table + val sz = Array.length arr + val newArr = Array.array (sz, NIL) + fun mapTbl i = if (i < sz) + then ( + Array.update(newArr, i, mapF (Array.sub(arr, i))); + mapTbl (i+1)) + else () + in + mapTbl 0; + HT{hashVal=hashVal, + sameKey=sameKey, + table = ref newArr, + n_items = ref(!n_items), + not_found = not_found} + end (* transform *); + + (* remove any hash table items that do not satisfy the given + * predicate. + *) + fun filter pred (HT{table, n_items, not_found, ...}) = let + fun filterP NIL = NIL + | filterP (B(hash, key, item, rest)) = if (pred(key, item)) + then B(hash, key, item, filterP rest) + else filterP rest + val arr = !table + val sz = Array.length arr + fun filterTbl i = if (i < sz) + then ( + Array.update (arr, i, filterP (Array.sub (arr, i))); + filterTbl (i+1)) + else () + in + filterTbl 0 + end (* filter *); + + (* Map a table to a new table that has the same keys, exception, + hash function, and equality function *) + + fun transform f (HT{hashVal, sameKey, table, n_items, not_found}) = let + fun mapF NIL = NIL + | mapF (B(hash, key, item, rest)) = B(hash, key, f item, mapF rest) + val arr = !table + val sz = Array.length arr + val newArr = Array.array (sz, NIL) + fun mapTbl i = if (i < sz) + then ( + Array.update(newArr, i, mapF (Array.sub(arr, i))); + mapTbl (i+1)) + else () + in + mapTbl 0; + HT{hashVal=hashVal, + sameKey=sameKey, + table = ref newArr, + n_items = ref(!n_items), + not_found = not_found} + end (* transform *); + + (* Create a copy of a hash table *) + fun copy (HT{hashVal, sameKey, table, n_items, not_found}) = let + val arr = !table + val sz = Array.length arr + val newArr = Array.array (sz, NIL) + fun mapTbl i = ( + Array.update (newArr, i, Array.sub(arr, i)); + mapTbl (i+1)) + in + (mapTbl 0) handle _ => (); + HT{hashVal=hashVal, + sameKey=sameKey, + table = ref newArr, + n_items = ref(!n_items), + not_found = not_found} + end (* copy *); + + (* returns a list of the sizes of the various buckets. This is to + * allow users to gauge the quality of their hashing function. + *) + fun bucketSizes (HT{table = ref arr, ...}) = let + fun len (NIL, n) = n + | len (B(_, _, _, r), n) = len(r, n+1) + fun f (~1, l) = l + | f (i, l) = f (i-1, len (Array.sub (arr, i), 0) :: l) + in + f ((Array.length arr)-1, []) + end + + (*Added by lcp. + This is essentially the hashpjw function described in Compilers: + Principles, Techniques, and Tools, by Aho, Sethi and Ullman.*) + (* local infix << >> + val left = Word.fromInt (Word.wordSize - 4) + val right = Word.fromInt (Word.wordSize - 8) + open Word + in + val mask = 0wxf << left + fun hashw (u,w) = + let val w' = (w << 0w4) + u + val g = Word.andb(w', mask) + in + if g <> 0w0 then Word.xorb(g, Word.xorb(w', g >> right)) + else w' + end; + end;*) + + (*This version is also recommended by Aho et al. and does not trigger the Poly/ML bug*) + val hmulti = Word.fromInt 65599; + fun hashw (u,w) = Word.+ (u, Word.*(hmulti,w)) + + fun hashw_char (c,w) = hashw (Word.fromInt (Char.ord c), w); + + fun hashw_vector (v,w) = Vector.foldl hashw w v; + + fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s; + + fun hashw_strings (ss, w) = List.foldl hashw_string w ss; + + fun hash_string s = Word.toIntX (hashw_string(s,0w0)); + +end diff -r 6e805f389355 -r e314fb38307d src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/Tools/res_clause.ML Wed Dec 21 12:06:08 2005 +0100 @@ -71,7 +71,7 @@ (*for hashing*) val clause_eq : clause * clause -> bool - val hash1_clause : clause -> word + val hash_clause : clause -> int val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order type fol_type @@ -659,17 +659,17 @@ val xor_words = List.foldl Word.xorb 0w0; -fun hash_term (UVar(_,_), w) = w - | hash_term (Fun(f,tps,args), w) = - List.foldl hash_term (Hashtable.hash_string (f,w)) args; +fun hashw_term (UVar(_,_), w) = w + | hashw_term (Fun(f,tps,args), w) = + List.foldl hashw_term (Polyhash.hashw_string (f,w)) args; -fun hash_pred (Predicate(pn,_,args), w) = - List.foldl hash_term (Hashtable.hash_string (pn,w)) args; +fun hashw_pred (Predicate(pn,_,args), w) = + List.foldl hashw_term (Polyhash.hashw_string (pn,w)) args; -fun hash1_literal (Literal(true,pred,_)) = hash_pred (pred, 0w0) - | hash1_literal (Literal(false,pred,_)) = Word.notb (hash_pred (pred, 0w0)); +fun hash1_literal (Literal(true,pred,_)) = hashw_pred (pred, 0w0) + | hash1_literal (Literal(false,pred,_)) = Word.notb (hashw_pred (pred, 0w0)); -fun hash1_clause clause = xor_words (map hash1_literal (get_literals clause)); +fun hash_clause clause = Word.toIntX (xor_words (map hash1_literal (get_literals clause))); (* FIX: not sure what to do with these funcs *) diff -r 6e805f389355 -r e314fb38307d src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Wed Dec 21 12:05:47 2005 +0100 +++ b/src/HOL/Tools/res_hol_clause.ML Wed Dec 21 12:06:08 2005 +0100 @@ -709,13 +709,12 @@ val xor_words = List.foldl Word.xorb 0w0; fun hash_combterm (CombVar(_,_),w) = w - | hash_combterm (CombFree(f,_),w) = Hashtable.hash_string(f,w) - | hash_combterm (CombConst(c,tp,tps),w) = Hashtable.hash_string(c,w) - | hash_combterm (CombApp(f,arg,tp),w) = - hash_combterm (arg, (hash_combterm (f,w))) + | hash_combterm (CombFree(f,_),w) = Polyhash.hashw_string(f,w) + | hash_combterm (CombConst(c,tp,tps),w) = Polyhash.hashw_string(c,w) + | hash_combterm (CombApp(f,arg,tp),w) = hash_combterm (arg, hash_combterm (f,w)) | hash_combterm (Bool(t),w) = hash_combterm (t,w) | hash_combterm (Equal(t1,t2),w) = - List.foldl hash_combterm (Hashtable.hash_string ("equal",w)) [t1,t2] + List.foldl hash_combterm (Polyhash.hashw_string ("equal",w)) [t1,t2] fun hash_literal (Literal(true,pred)) = hash_combterm(pred,0w0) | hash_literal (Literal(false,pred)) = Word.notb(hash_combterm(pred,0w0)); diff -r 6e805f389355 -r e314fb38307d src/Pure/General/hashtable.ML --- a/src/Pure/General/hashtable.ML Wed Dec 21 12:05:47 2005 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,133 +0,0 @@ -(*Hash tables. Taken from SML/NJ version 110.57. - Copyright (c) 1989-2002 by Lucent Technologies*) -signature HASHTABLE = -sig - type ('a,'b) table - - val create : { hash : 'a -> word, - == : 'a * 'a -> bool, - exn : exn, - size : int - } -> ('a,'b) table - - val size : ('a,'b) table -> int - val clear : ('a,'b) table -> unit - val insert : ('a,'b) table -> 'a * 'b -> unit - val remove : ('a,'b) table -> 'a -> unit - val lookup : ('a,'b) table -> 'a -> 'b - val copy : ('a,'b) table -> ('a,'b) table - val app : ('a * 'b -> unit) -> ('a,'b) table -> unit - val map : ('a * 'b -> 'c) -> ('a,'b) table -> 'c list - val fold : ('a * 'b * 'c -> 'c) -> 'c -> ('a,'b) table -> 'c - - (*Additions due to L. C. Paulson and Jia Meng*) - val hash_word : word * word -> word - val hash_char : Char.char * word -> word - val hash_vector : word Vector.vector * word -> word - val hash_string : string * word -> word - val hash_strings : string list * word -> word -end - -structure Hashtable :> HASHTABLE = -struct - - structure A = Array - - type ('a,'b) table = ('a -> word) * - ('a * 'a -> bool) * - exn * - ('a * 'b) list A.array ref * - int ref - - infix == - - fun create{hash,==,exn,size} = (hash,op==,exn,ref(A.array(size,[])),ref 0) - fun copy(hash,op==,exn,ref a,ref c) = - (hash,op==,exn,ref(A.tabulate(A.length a,fn i => A.sub(a,i))), ref c) - fun size (_,_,_,_,ref n) = n - fun clear (_,_,_,ref a,c) = - let fun f ~1 = () - | f i = (A.update(a,i,[]); f(i-1)) - in f(A.length a - 1); c := 0 end - fun insert (hash,op==,exn,A as ref a,c) (k,v) = - let val N = A.length a - val h = Word.toIntX(hash k) mod N - val es = A.sub(a,h) - fun insrt ([],es') = (A.update(a,h,(k,v)::es'); - c := !c + 1; - if !c >= N then grow(hash,A,N) else ()) - | insrt ((e as (k',_))::es,es') = - if k == k' then A.update(a,h,(k,v)::es'@es) - else insrt(es,e::es') - in insrt (es,[]) - end - - and grow(hash,A as ref a,N) = - let val M = N + N - val M = if M < 13 then 13 else M - val a' = A.array(M,[]) - fun insrt (k,v) = let val h = Word.toIntX(hash k) mod M - in A.update(a',h,(k,v)::A.sub(a',h)) end - in A.app (fn es => app insrt es) a; - A := a' - end - - fun remove (hash,op==,exn,ref a,c) k = - let val N = A.length a - val h = Word.toIntX(hash k) mod N - val es = A.sub(a,h) - fun del ([],es') = () - | del ((e as (k',_))::es,es') = - if k == k' then (A.update(a,h,es'@es); c := !c - 1) - else del(es,e::es') - in del (es,[]) - end - - fun lookup(hash,op==,exn,ref a,_) k = - let val N = A.length a - val h = Word.toIntX(hash k) mod N - fun find [] = raise exn - | find ((k',v)::es) = if k == k' then v else find es - in find(A.sub(a,h)) - end - - fun app f (_,_,_,ref A,_) = A.app (List.app f) A - - fun map f (_,_,_,ref A,_) = - let fun fl([],x) = x - | fl((k,v)::es,x) = f(k,v)::fl(es,x) - in A.foldr fl [] A end - - fun fold f x (_,_,_,ref A,_) = - let fun fl([],x) = x - | fl((k,v)::es,x) = f(k,v,fl(es,x)) - in A.foldr fl x A end - - - (*Additions due to L. C. Paulson and Jia Meng*) - - val myw = ref 0w0; - val () = myw := 0wx70000000; (*workaround for Poly/ML bug*) - - local open Word - infix << >> - in - fun hash_word (u,w) = - let val w' = (w << 0w4) + u - val g = Word.andb(w', !myw) (*I hope this hex constant is correct!*) - in - if g = 0w0 then Word.xorb(w', Word.xorb(g, g >> 0w24)) - else w' - end; - end; - - fun hash_char (c,w) = hash_word (Word.fromInt (Char.ord c), w); - - fun hash_vector (v,w) = Vector.foldl hash_word w v; - - fun hash_string (s:string, w) = CharVector.foldl hash_char w s; - - fun hash_strings (ss, w) = List.foldl hash_string w ss; - -end -