further tweaks to the SPASS setup

--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 26 16:50:20 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 26 18:34:23 2005 +0200
@@ -73,18 +73,23 @@
 
 
 fun proofstep_to_string Axiom = "Axiom()"
-|   proofstep_to_string  (Binary ((a,b), (c,d)))= "Binary"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
-|   proofstep_to_string (Factor (a,b,c)) = "Factor"^"("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
-|   proofstep_to_string  (Para ((a,b), (c,d)))= "Para"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
-|   proofstep_to_string  (MRR ((a,b), (c,d)))= "MRR"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
-|   proofstep_to_string (Rewrite((a,b),(c,d))) = "Rewrite"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
+|   proofstep_to_string  (Binary ((a,b), (c,d)))=
+      "Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
+|   proofstep_to_string (Factor (a,b,c)) =
+      "Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
+|   proofstep_to_string  (Para ((a,b), (c,d)))= 
+      "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
+|   proofstep_to_string  (MRR ((a,b), (c,d))) =
+      "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
+|   proofstep_to_string (Rewrite((a,b),(c,d))) =
+      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
 
 fun list_to_string [] liststr = liststr
 |   list_to_string (x::[]) liststr = liststr^(string_of_int x)
 |   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
 
 
-fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
+fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
  
 
 fun proofs_to_string [] str = str
@@ -110,8 +115,8 @@
 fun origAx_to_string (num,(meta,thmvars)) =
     let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
     in
-       (string_of_int num)^"OrigAxiom()"^"["^
-       (clause_strs_to_string clause_strs "")^"]"^"["^
+       (string_of_int num)^"OrigAxiom()["^
+       (clause_strs_to_string clause_strs "")^"]["^
        (thmvars_to_string thmvars "")^"]"
     end
 
@@ -128,7 +133,7 @@
 fun extraAx_to_string (num, (meta,thmvars)) =
    let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
    in
-      (string_of_int num)^"ExtraAxiom()"^"["^
+      (string_of_int num)^"ExtraAxiom()["^
       (clause_strs_to_string clause_strs "")^"]"^
       "["^(thmvars_to_string thmvars "")^"]"
    end;
@@ -637,8 +642,8 @@
 |   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
 
 
-fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^" \\<Longrightarrow> False\""
-|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^"\\<Longrightarrow> False\""
+fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
+|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
 
 fun frees_to_string [] str = implode (change_nots (explode str))
 |   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
@@ -712,18 +717,22 @@
 fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
 
 
-fun  by_isar_line ((Binary ((a,b), (c,d))))="by(rule cl"^
-                                                  (string_of_int a)^" [BINARY "^(string_of_int b)^" "^"cl"^
-                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
-|   by_isar_line ( (Para ((a,b), (c,d)))) ="by (rule cl"^
-                                                  (string_of_int a)^" [PARAMOD "^(string_of_int b)^" "^"cl"^
-                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
-|   by_isar_line ((Factor ((a,b,c)))) =    "by (rule cl"^(string_of_int a)^" [FACTOR "^(string_of_int b)^" "^
-                                                  (string_of_int c)^" "^"])"^"\n"
-|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =  "by (rule cl"^(string_of_int a)^" [DEMOD "^(string_of_int b)^" "^
-                                                  (string_of_int c)^" "^(string_of_int d)^" "^"])"^"\n"
-
-|   by_isar_line ( (Obvious ((a,b)))) =  "by (rule cl"^(string_of_int a)^" [OBVIOUS "^(string_of_int b)^" ])"^"\n"
+fun by_isar_line ((Binary ((a,b), (c,d)))) = 
+    "by(rule cl"^
+		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
+		(string_of_int c)^" "^(string_of_int d)^"])\n"
+|   by_isar_line ( (Para ((a,b), (c,d)))) =
+    "by (rule cl"^
+		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
+		(string_of_int c)^" "^(string_of_int d)^"])\n"
+|   by_isar_line ((Factor ((a,b,c)))) = 
+    "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
+		(string_of_int c)^" ])\n"
+|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
+    "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
+		(string_of_int c)^" "^(string_of_int d)^" ])\n"
+|   by_isar_line ( (Obvious ((a,b)))) =
+    "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
 
 fun isar_line (numb, (step, clstrs, thmstrs))  = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
 
@@ -734,40 +743,38 @@
 fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
 
 
-fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
-                           val extraax_num = length extraaxioms
-                           val origaxioms_and_steps = Library.drop (extraax_num, xs)  
-                          
-  
-                           val origaxioms = get_origaxioms origaxioms_and_steps
-                           val origax_num = length origaxioms
-                           val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
-                           val axioms = get_axioms axioms_and_steps
-                           
-                           val steps = Library.drop (origax_num, axioms_and_steps)
-                           val firststeps = ReconOrderClauses.butlast steps
-                           val laststep = ReconOrderClauses.last steps
-                           val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
-                        
-                           val isar_proof = 
-                           ("show \""^goalstring^"\"\n")^
-                           ("proof (rule ccontr,skolemize, make_clauses) \n")^
-                           ("fix "^(frees_to_isar_str frees)^"\n")^
-                           (assume_isar_extraaxioms extraaxioms)^
-                           (assume_isar_origaxioms origaxioms)^
-                           (isar_axiomlines axioms "")^
-                           (isar_lines firststeps "")^
-                           (last_isar_line laststep)^
-                           ("qed")
-                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
-
-                                                  val _ = TextIO.output (outfile, isar_proof)
-                                                  val _ =  TextIO.closeOut outfile
-
-
-                       in
-                           isar_proof
-                       end
+fun to_isar_proof (frees, xs, goalstring) =
+    let val extraaxioms = get_extraaxioms xs
+	val extraax_num = length extraaxioms
+	val origaxioms_and_steps = Library.drop (extraax_num, xs)  
+	
+	val origaxioms = get_origaxioms origaxioms_and_steps
+	val origax_num = length origaxioms
+	val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
+	val axioms = get_axioms axioms_and_steps
+	
+	val steps = Library.drop (origax_num, axioms_and_steps)
+	val firststeps = ReconOrderClauses.butlast steps
+	val laststep = ReconOrderClauses.last steps
+	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
+	
+	val isar_proof = 
+		("show \""^goalstring^"\"\n")^
+		("proof (rule ccontr,skolemize, make_clauses) \n")^
+		("fix "^(frees_to_isar_str frees)^"\n")^
+		(assume_isar_extraaxioms extraaxioms)^
+		(assume_isar_origaxioms origaxioms)^
+		(isar_axiomlines axioms "")^
+		(isar_lines firststeps "")^
+		(last_isar_line laststep)^
+		("qed")
+	val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
+	
+	val _ = TextIO.output (outfile, isar_proof)
+	val _ =  TextIO.closeOut outfile
+    in
+	isar_proof
+    end;
 
 (* get fix vars from axioms - all Frees *)
 (* check each clause for meta-vars and /\ over them at each step*)

--- a/src/HOL/Tools/ATP/spassshell	Thu May 26 16:50:20 2005 +0200
+++ b/src/HOL/Tools/ATP/spassshell	Thu May 26 18:34:23 2005 +0200
@@ -1,4 +1,7 @@
-
+#!/bin/sh
+#  ID: $Id$
+# Shell script to invoke SPASS and filter the output
 
-`isatool getenv -b SPASS_HOME`/SPASS  $* |testoutput.py
-#$SPASS_HOME  $* |testoutput.py
+`isatool getenv -b SPASS_HOME`/SPASS  $* | \
+    `isatool getenv -b ISABELLE_HOME`/src/HOL/Tools/ATP/testoutput.py
+

--- a/src/HOL/Tools/ATP/watcher.ML	Thu May 26 16:50:20 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu May 26 18:34:23 2005 +0200
@@ -164,7 +164,7 @@
 			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
 	  val _ =  TextIO.closeOut outfile
 	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
-	 val probID = ReconOrderClauses.last(explode probfile)
+	  val probID = ReconOrderClauses.last(explode probfile)
 	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
 	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
 	  (*** hyps/local axioms just now                                                ***)
@@ -174,16 +174,16 @@
 			   else File.mkdir dfg_dir; 
 	  
 	  val dfg_path = File.sysify_path dfg_dir;
+	  val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
 	  val exec_tptp2x = 
-	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
-	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
+ 	      Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
 	(*val _ = Posix.Process.wait ()*)
 	(*val _ =Unix.reap exec_tptp2x*)
 	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
  
        in   
 	  goals_being_watched := (!goals_being_watched) + 1;
-	  Posix.Process.sleep(Time.fromSeconds 1); 
+	  Posix.Process.sleep(Time.fromSeconds 4); 
 	  (warning ("probfile is: "^probfile));
 	  (warning("dfg file is: "^newfile));
 	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
@@ -196,8 +196,8 @@
 	  if File.exists
 	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
 	  then callResProvers (toWatcherStr, args)
-	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
-	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
+	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^
+	              space_implode " " tptp2x_args)
       end
 (*
 fun callResProversStr (toWatcherStr,  []) =  "End of calls\n"