# HG changeset patch # User paulson # Date 1117125263 -7200 # Node ID 3683f0486a11649e5e00b2e66b3726f993d4188d # Parent fbb5ae140535ddc0607fd5806e3294db8c5e9bd3 further tweaks to the SPASS setup diff -r fbb5ae140535 -r 3683f0486a11 src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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 [] = "\"\\"^(clstrs_to_string clstrs "")^"\\ "^" \\ False\"" -| clause_strs_to_isar clstrs thmvars = "\"\\"^(thmvars_to_quantstring thmvars "")^"\\"^(clstrs_to_string clstrs "")^"\\ "^"\\ False\"" +fun clause_strs_to_isar clstrs [] = "\"\\"^(clstrs_to_string clstrs "")^"\\ \\ False\"" +| clause_strs_to_isar clstrs thmvars = "\"\\"^(thmvars_to_quantstring thmvars "")^"\\"^(clstrs_to_string clstrs "")^"\\ \\ 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*) diff -r fbb5ae140535 -r 3683f0486a11 src/HOL/Tools/ATP/spassshell --- 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 + diff -r fbb5ae140535 -r 3683f0486a11 src/HOL/Tools/ATP/watcher.ML --- 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"