--- 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 \
--- 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";
--- 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"
--- 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);
--- /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
--- 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 *)
--- 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));
--- 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
-