# HG changeset patch
# User paulson
# Date 1115905378 -7200
# Node ID 87cf2ce8ede8fd57389dd21bb75ae1173e580d57
# Parent  dd516176043a40403c35666f32ab22b2b9802f8b
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule

diff -r dd516176043a -r 87cf2ce8ede8 src/HOL/Tools/reconstruction.ML
--- a/src/HOL/Tools/reconstruction.ML	Thu May 12 10:48:46 2005 +0200
+++ b/src/HOL/Tools/reconstruction.ML	Thu May 12 15:42:58 2005 +0200
@@ -123,31 +123,10 @@
 
 (** Conversion of a theorem into clauses **)
 
-local
-
-  (*Cache for clauses: could be a hash table if we provided them.*)
-  val cc = ref (Symtab.empty : (thm * thm list) Symtab.table)
+(*For efficiency, we rely upon memo-izing in ResAxioms.*)
+fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
 
-  fun memo_cnf th =
-    case Thm.name_of_thm th of
-        "" => ResAxioms.meta_cnf_axiom th (*no name, so can't cache*)
-      | s  => case Symtab.lookup (!cc,s) of
-      	        NONE => 
-      	        	let val cls = ResAxioms.meta_cnf_axiom th
-      	        	in  cc := Symtab.update ((s, (th,cls)), !cc); cls
-      	        	end
-      	      | SOME(th',cls) =>
-      	      	    if eq_thm(th,th') then cls
-      	      	    else (*New theorem stored under the same name? Possible??*)
-      	      	      let val cls = ResAxioms.meta_cnf_axiom th
-      	        	  in  cc := Symtab.update ((s, (th,cls)), !cc); cls
-      	        	  end;
-
-in
-fun clausify_rule (A,i) = List.nth (memo_cnf A,i)
-end;
-
-fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
+fun clausify_syntax i (x, th) = (x, clausify_rule (th,i));
 
 fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
 
diff -r dd516176043a -r 87cf2ce8ede8 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu May 12 10:48:46 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu May 12 15:42:58 2005 +0200
@@ -211,25 +211,42 @@
 fun transfer_to_Reconstruction thm =
     transfer recon_thy thm handle THM _ => thm;
 
-(* remove "True" clause *)
-fun rm_redundant_cls [] = []
-  | rm_redundant_cls (thm::thms) =
-    let val t = prop_of thm
-    in
-	case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms
-		| _ => thm::(rm_redundant_cls thms)
-    end;
+fun is_taut th =
+      case (prop_of th) of
+           (Const ("Trueprop", _) $ Const ("True", _)) => true
+         | _ => false;
+
+(* remove tautologous clauses *)
+val rm_redundant_cls = List.filter (not o is_taut);
 
 (* transform an Isabelle thm into CNF *)
-fun cnf_axiom thm =
+fun cnf_axiom_aux thm =
     let val thm' = transfer_to_Reconstruction thm
 	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
     in
-	map Thm.varifyT (rm_redundant_cls thm'')
+	map (zero_var_indexes o Thm.varifyT) (rm_redundant_cls thm'')
     end;
+    
+(*Cache for clauses: could be a hash table if we provided them.*)
+val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
+
+fun cnf_axiom th =
+    case Thm.name_of_thm th of
+	  "" => cnf_axiom_aux th (*no name, so can't cache*)
+	| s  => case Symtab.lookup (!clause_cache,s) of
+	  	  NONE => 
+		    let val cls = cnf_axiom_aux th
+		    in  clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls
+		    end
+	        | SOME(th',cls) =>
+		    if eq_thm(th,th') then cls
+		    else (*New theorem stored under the same name? Possible??*)
+		      let val cls = cnf_axiom_aux th
+		      in  clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls
+		      end;
 
 fun meta_cnf_axiom thm = 
-    map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
+    map Meson.make_meta_clause (cnf_axiom thm);
 
 
 (* changed: with one extra case added *)