src/HOL/Tools/res_atp.ML
changeset 20661 46832fee1215
parent 20643 267f30cbe2cb
child 20757 fe84fe0dfd30
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 21 17:31:10 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Sep 21 17:33:11 2006 +0200
     1.3 @@ -456,12 +456,6 @@
     1.4  
     1.5  (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
     1.6  
     1.7 -fun fake_thm_name th = 
     1.8 -    Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
     1.9 -
    1.10 -fun put_name_pair ("",th) = (fake_thm_name th, th)
    1.11 -  | put_name_pair (a,th)  = (a,th);
    1.12 -
    1.13  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
    1.14  
    1.15  exception HASH_CLAUSE and HASH_STRING;
    1.16 @@ -501,9 +495,9 @@
    1.17  val xor_words = List.foldl Word.xorb 0w0;
    1.18  
    1.19  fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
    1.20 -  | hashw_term ((Free(_,_)), w) = w
    1.21 +  | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
    1.22    | hashw_term ((Var(_,_)), w) = w
    1.23 -  | hashw_term ((Bound _), w) = w
    1.24 +  | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
    1.25    | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
    1.26    | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
    1.27  
    1.28 @@ -524,6 +518,26 @@
    1.29  
    1.30  fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
    1.31  
    1.32 +(*Versions ONLY for "faking" a theorem name. Here we take variable names into account
    1.33 +  so that similar theorems don't collide.  FIXME: this entire business of "faking" 
    1.34 +  theorem names must end!*)
    1.35 +fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
    1.36 +  | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
    1.37 +  | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
    1.38 +
    1.39 +fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
    1.40 +  | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
    1.41 +  | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
    1.42 +  | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
    1.43 +  | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
    1.44 +  | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
    1.45 +
    1.46 +fun full_hashw_thm (th,w) = 
    1.47 +  let val {prop,hyps,...} = rep_thm th
    1.48 +  in List.foldl full_hashw_term w (prop::hyps) end
    1.49 +
    1.50 +fun full_hash_thm th = full_hashw_thm (th,0w0);
    1.51 +
    1.52  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
    1.53  
    1.54  (*Create a hash table for clauses, of the given size*)
    1.55 @@ -556,6 +570,12 @@
    1.56  fun get_relevant_clauses thy cls_thms white_cls goals =
    1.57    insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
    1.58  
    1.59 +(*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
    1.60 +fun fake_thm_name th = 
    1.61 +    Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
    1.62 +
    1.63 +fun put_name_pair ("",th) = (fake_thm_name th, th)
    1.64 +  | put_name_pair (a,th)  = (a,th);
    1.65  
    1.66  fun display_thms [] = ()
    1.67    | display_thms ((name,thm)::nthms) =