author paulson Thu, 26 May 2005 18:34:23 +0200 changeset 16091 3683f0486a11 parent 16090 fbb5ae140535 child 16092 a1a481ee9425
further tweaks to the SPASS setup
 src/HOL/Tools/ATP/recon_transfer_proof.ML file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/spassshell file | annotate | diff | comparison | revisions src/HOL/Tools/ATP/watcher.ML file | annotate | diff | comparison | revisions
--- 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"