# HG changeset patch
# User paulson
# Date 1129640918 -7200
# Node ID 116a8d1c7a678b5902a3dae593dc843702c55d12
# Parent  c10e68962ad39728cb4624d5e69d45c82eff09e6
new interface to make_conjecture_clauses

diff -r c10e68962ad3 -r 116a8d1c7a67 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Oct 17 23:10:25 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 18 15:08:38 2005 +0200
@@ -65,9 +65,9 @@
   | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
 
 (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
-fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
+fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) =
   let
-    val clss = ResClause.make_conjecture_clauses thms
+    val clss = ResClause.make_conjecture_clauses (map prop_of ths)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
     val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
     val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
@@ -80,8 +80,8 @@
   end;
 
 (* write out a subgoal in DFG format to the file "xxxx_N"*)
-fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
-    let val clss = ResClause.make_conjecture_clauses thms
+fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
+    let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
         (*FIXME: classrel_clauses and arity_clauses*)
         val probN = ResClause.clauses2dfg clss (!problem_name ^ "_" ^ Int.toString n)
                         axclauses [] [] []    
@@ -91,10 +91,7 @@
     end;
 
 
-(*********************************************************************)
 (* call prover with settings and problem file for the current subgoal *)
-(*********************************************************************)
-(* now passing in list of skolemized thms and list of sgterms to go with them *)
 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   let
     fun make_atp_list [] n = []
diff -r c10e68962ad3 -r 116a8d1c7a67 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Oct 17 23:10:25 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Tue Oct 18 15:08:38 2005 +0200
@@ -21,7 +21,7 @@
   type clause
   val init : theory -> unit
   val make_axiom_clause : Term.term -> string * int -> clause
-  val make_conjecture_clauses : thm list -> clause list
+  val make_conjecture_clauses : term list -> clause list
   val get_axiomName : clause ->  string
   val isTaut : clause -> bool
   val num_of_clauses : clause -> int
@@ -401,7 +401,7 @@
 	  val (ts2,ffuncs) = ListPair.unzip ts_funcs
 	  val ts3 = union_all (ts1::ts2)
 	  val ffuncs' = union_all ffuncs
-	  val newfuncs = distinct (pfuncs@ffuncs')
+	  val newfuncs = pfuncs union ffuncs'
 	  val arity = 
 	    case pred of
 		Const (c,_) => 
@@ -423,25 +423,21 @@
   | predicate_of (term,polarity,tag) =
         (pred_of (strip_comb term), polarity, tag);
 
-fun literals_of_term ((Const("Trueprop",_) $ P),lits_ts, preds, funcs) =    
-      literals_of_term(P,lits_ts, preds, funcs)
-  | literals_of_term ((Const("op |",_) $ P $ Q),(lits,ts), preds,funcs) = 
-      let val (lits',ts', preds', funcs') = 
-            literals_of_term(P,(lits,ts), preds,funcs)
+fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
+  | literals_of_term1 (args as (lits, ts, preds, funcs)) (Const("op |",_) $ P $ Q) = 
+      let val (lits', ts', preds', funcs') = literals_of_term1 args P
       in
-	  literals_of_term(Q, (lits',ts'), distinct(preds'@preds), 
-	                   distinct(funcs'@funcs))
+	  literals_of_term1 (lits', ts', preds' union preds, funcs' union funcs) Q
       end
-  | literals_of_term (P,(lits,ts), preds, funcs) = 
-      let val ((pred,ts', preds', funcs'), pol, tag) = 
-              predicate_of (P,true,false)
+  | literals_of_term1 (lits, ts, preds, funcs) P =
+      let val ((pred, ts', preds', funcs'), pol, tag) = predicate_of (P,true,false)
 	  val lits' = Literal(pol,pred,tag) :: lits
       in
-	  (lits', ts union ts', distinct(preds'@preds), distinct(funcs'@funcs))
+	  (lits', ts union ts', preds' union preds, funcs' union funcs)
       end;
 
 
-fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]), [], []);
+val literals_of_term = literals_of_term1 ([],[],[],[]);
 
 
 (* FIX: not sure what to do with these funcs *)
@@ -495,16 +491,15 @@
 fun get_tvar_strs [] = []
   | get_tvar_strs ((FOLTVar indx,s)::tss) = 
       let val vstr = make_schematic_type_var indx
-          val vstrs = get_tvar_strs tss
       in
-	  (distinct( vstr:: vstrs))
+	  vstr ins (get_tvar_strs tss)
       end
   | get_tvar_strs((FOLTFree x,s)::tss) = distinct (get_tvar_strs tss)
 
 (* FIX add preds and funcs to add typs aux here *)
 
 fun make_axiom_clause_thm thm (ax_name,cls_id) =
-    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
+    let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm)
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
         val tvars = get_tvar_strs types_sorts
     in 
@@ -515,8 +510,8 @@
 
 
 
-fun make_conjecture_clause n thm =
-    let val (lits,types_sorts, preds, funcs) = literals_of_thm thm
+fun make_conjecture_clause n t =
+    let val (lits,types_sorts, preds, funcs) = literals_of_term t
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
         val tvars = get_tvar_strs types_sorts
     in
@@ -526,14 +521,14 @@
     end;
     
 fun make_conjecture_clauses_aux _ [] = []
-  | make_conjecture_clauses_aux n (th::ths) =
-      make_conjecture_clause n th :: make_conjecture_clauses_aux (n+1) ths
+  | make_conjecture_clauses_aux n (t::ts) =
+      make_conjecture_clause n t :: make_conjecture_clauses_aux (n+1) ts
 
 val make_conjecture_clauses = make_conjecture_clauses_aux 0
 
 
 fun make_axiom_clause term (ax_name,cls_id) =
-    let val (lits,types_sorts, preds,funcs) = literals_of_term (term,([],[]), [],[])
+    let val (lits,types_sorts, preds,funcs) = literals_of_term term
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
         val tvars = get_tvar_strs types_sorts	
     in 
@@ -900,8 +895,8 @@
 	 val ax_name = get_axiomName cls
 	 val vars = dfg_vars cls
 	 val tvars = dfg_tvars cls
-	 val funcs' = distinct((funcs_of_cls cls)@funcs)
-	 val preds' = distinct((preds_of_cls cls)@preds)
+	 val funcs' = (funcs_of_cls cls) union funcs
+	 val preds' = (preds_of_cls cls) union preds
 	 val knd = string_of_kind cls
 	 val lits_str = concat_with ", " lits
 	 val axioms' = if knd = "axiom" then (cls::axioms) else axioms