# HG changeset patch # User paulson # Date 1158852791 -7200 # Node ID 46832fee12157cd273d482be2ba0bef7a70406ae # Parent 8606ddd42554810da64c7e714238af36c8dcbde8 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing. diff -r 8606ddd42554 -r 46832fee1215 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Sep 21 17:31:10 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Sep 21 17:33:11 2006 +0200 @@ -456,12 +456,6 @@ (*** retrieve lemmas from clasimpset and atpset, may filter them ***) -fun fake_thm_name th = - Context.theory_name (theory_of_thm th) ^ "." ^ gensym""; - -fun put_name_pair ("",th) = (fake_thm_name th, th) - | put_name_pair (a,th) = (a,th); - (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*) exception HASH_CLAUSE and HASH_STRING; @@ -501,9 +495,9 @@ val xor_words = List.foldl Word.xorb 0w0; fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w) - | hashw_term ((Free(_,_)), w) = w + | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) | hashw_term ((Var(_,_)), w) = w - | hashw_term ((Bound _), w) = w + | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w) | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w))); @@ -524,6 +518,26 @@ fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t []))); +(*Versions ONLY for "faking" a theorem name. Here we take variable names into account + so that similar theorems don't collide. FIXME: this entire business of "faking" + theorem names must end!*) +fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) + | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w) + | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts); + +fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w)) + | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w) + | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w)) + | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w) + | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w)) + | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w))); + +fun full_hashw_thm (th,w) = + let val {prop,hyps,...} = rep_thm th + in List.foldl full_hashw_term w (prop::hyps) end + +fun full_hash_thm th = full_hashw_thm (th,0w0); + fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2); (*Create a hash table for clauses, of the given size*) @@ -556,6 +570,12 @@ fun get_relevant_clauses thy cls_thms white_cls goals = insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals); +(*This name is cryptic but short. Unlike gensym, we get the same name each time.*) +fun fake_thm_name th = + Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th); + +fun put_name_pair ("",th) = (fake_thm_name th, th) + | put_name_pair (a,th) = (a,th); fun display_thms [] = () | display_thms ((name,thm)::nthms) =