author paulson Thu May 26 18:34:23 2005 +0200 (2005-05-26) 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 | revisions src/HOL/Tools/ATP/spassshell file | annotate | diff | revisions src/HOL/Tools/ATP/watcher.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 26 16:50:20 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu May 26 18:34:23 2005 +0200
1.3 @@ -73,18 +73,23 @@
1.4
1.5
1.6  fun proofstep_to_string Axiom = "Axiom()"
1.7 -|   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)^")"^")"
1.8 -|   proofstep_to_string (Factor (a,b,c)) = "Factor"^"("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
1.9 -|   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)^")"^")"
1.10 -|   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)^")"^")"
1.11 -|   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)^")"^")"
1.12 +|   proofstep_to_string  (Binary ((a,b), (c,d)))=
1.13 +      "Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
1.14 +|   proofstep_to_string (Factor (a,b,c)) =
1.15 +      "Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
1.16 +|   proofstep_to_string  (Para ((a,b), (c,d)))=
1.17 +      "Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
1.18 +|   proofstep_to_string  (MRR ((a,b), (c,d))) =
1.19 +      "MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
1.20 +|   proofstep_to_string (Rewrite((a,b),(c,d))) =
1.21 +      "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"
1.22
1.23  fun list_to_string [] liststr = liststr
1.24  |   list_to_string (x::[]) liststr = liststr^(string_of_int x)
1.25  |   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
1.26
1.27
1.28 -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 "")^"]"
1.29 +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 "")^"]"
1.30
1.31
1.32  fun proofs_to_string [] str = str
1.33 @@ -110,8 +115,8 @@
1.34  fun origAx_to_string (num,(meta,thmvars)) =
1.35      let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
1.36      in
1.37 -       (string_of_int num)^"OrigAxiom()"^"["^
1.38 -       (clause_strs_to_string clause_strs "")^"]"^"["^
1.39 +       (string_of_int num)^"OrigAxiom()["^
1.40 +       (clause_strs_to_string clause_strs "")^"]["^
1.41         (thmvars_to_string thmvars "")^"]"
1.42      end
1.43
1.44 @@ -128,7 +133,7 @@
1.45  fun extraAx_to_string (num, (meta,thmvars)) =
1.46     let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
1.47     in
1.48 -      (string_of_int num)^"ExtraAxiom()"^"["^
1.49 +      (string_of_int num)^"ExtraAxiom()["^
1.50        (clause_strs_to_string clause_strs "")^"]"^
1.51        "["^(thmvars_to_string thmvars "")^"]"
1.52     end;
1.53 @@ -637,8 +642,8 @@
1.54  |   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
1.55
1.56
1.57 -fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^" \\<Longrightarrow> False\""
1.58 -|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^"\\<Longrightarrow> False\""
1.59 +fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
1.60 +|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> \\<Longrightarrow> False\""
1.61
1.62  fun frees_to_string [] str = implode (change_nots (explode str))
1.63  |   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
1.64 @@ -712,18 +717,22 @@
1.65  fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
1.66
1.67
1.68 -fun  by_isar_line ((Binary ((a,b), (c,d))))="by(rule cl"^
1.69 -                                                  (string_of_int a)^" [BINARY "^(string_of_int b)^" "^"cl"^
1.70 -                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
1.71 -|   by_isar_line ( (Para ((a,b), (c,d)))) ="by (rule cl"^
1.72 -                                                  (string_of_int a)^" [PARAMOD "^(string_of_int b)^" "^"cl"^
1.73 -                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
1.74 -|   by_isar_line ((Factor ((a,b,c)))) =    "by (rule cl"^(string_of_int a)^" [FACTOR "^(string_of_int b)^" "^
1.75 -                                                  (string_of_int c)^" "^"])"^"\n"
1.76 -|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =  "by (rule cl"^(string_of_int a)^" [DEMOD "^(string_of_int b)^" "^
1.77 -                                                  (string_of_int c)^" "^(string_of_int d)^" "^"])"^"\n"
1.78 -
1.79 -|   by_isar_line ( (Obvious ((a,b)))) =  "by (rule cl"^(string_of_int a)^" [OBVIOUS "^(string_of_int b)^" ])"^"\n"
1.80 +fun by_isar_line ((Binary ((a,b), (c,d)))) =
1.81 +    "by(rule cl"^
1.82 +		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
1.83 +		(string_of_int c)^" "^(string_of_int d)^"])\n"
1.84 +|   by_isar_line ( (Para ((a,b), (c,d)))) =
1.85 +    "by (rule cl"^
1.86 +		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
1.87 +		(string_of_int c)^" "^(string_of_int d)^"])\n"
1.88 +|   by_isar_line ((Factor ((a,b,c)))) =
1.89 +    "by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^
1.90 +		(string_of_int c)^" ])\n"
1.91 +|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =
1.92 +    "by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^
1.93 +		(string_of_int c)^" "^(string_of_int d)^" ])\n"
1.94 +|   by_isar_line ( (Obvious ((a,b)))) =
1.95 +    "by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n"
1.96
1.97  fun isar_line (numb, (step, clstrs, thmstrs))  = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
1.98
1.99 @@ -734,40 +743,38 @@
1.100  fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
1.101
1.102
1.103 -fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
1.104 -                           val extraax_num = length extraaxioms
1.105 -                           val origaxioms_and_steps = Library.drop (extraax_num, xs)
1.106 -
1.107 -
1.108 -                           val origaxioms = get_origaxioms origaxioms_and_steps
1.109 -                           val origax_num = length origaxioms
1.110 -                           val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)
1.111 -                           val axioms = get_axioms axioms_and_steps
1.112 -
1.113 -                           val steps = Library.drop (origax_num, axioms_and_steps)
1.114 -                           val firststeps = ReconOrderClauses.butlast steps
1.115 -                           val laststep = ReconOrderClauses.last steps
1.116 -                           val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
1.117 -
1.118 -                           val isar_proof =
1.119 -                           ("show \""^goalstring^"\"\n")^
1.120 -                           ("proof (rule ccontr,skolemize, make_clauses) \n")^
1.121 -                           ("fix "^(frees_to_isar_str frees)^"\n")^
1.122 -                           (assume_isar_extraaxioms extraaxioms)^
1.123 -                           (assume_isar_origaxioms origaxioms)^
1.124 -                           (isar_axiomlines axioms "")^
1.125 -                           (isar_lines firststeps "")^
1.126 -                           (last_isar_line laststep)^
1.127 -                           ("qed")
1.128 -                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
1.129 -
1.130 -                                                  val _ = TextIO.output (outfile, isar_proof)
1.131 -                                                  val _ =  TextIO.closeOut outfile
1.132 -
1.133 -
1.134 -                       in
1.135 -                           isar_proof
1.136 -                       end
1.137 +fun to_isar_proof (frees, xs, goalstring) =
1.138 +    let val extraaxioms = get_extraaxioms xs
1.139 +	val extraax_num = length extraaxioms
1.140 +	val origaxioms_and_steps = Library.drop (extraax_num, xs)
1.141 +
1.142 +	val origaxioms = get_origaxioms origaxioms_and_steps
1.143 +	val origax_num = length origaxioms
1.144 +	val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)
1.145 +	val axioms = get_axioms axioms_and_steps
1.146 +
1.147 +	val steps = Library.drop (origax_num, axioms_and_steps)
1.148 +	val firststeps = ReconOrderClauses.butlast steps
1.149 +	val laststep = ReconOrderClauses.last steps
1.150 +	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
1.151 +
1.152 +	val isar_proof =
1.153 +		("show \""^goalstring^"\"\n")^
1.154 +		("proof (rule ccontr,skolemize, make_clauses) \n")^
1.155 +		("fix "^(frees_to_isar_str frees)^"\n")^
1.156 +		(assume_isar_extraaxioms extraaxioms)^
1.157 +		(assume_isar_origaxioms origaxioms)^
1.158 +		(isar_axiomlines axioms "")^
1.159 +		(isar_lines firststeps "")^
1.160 +		(last_isar_line laststep)^
1.161 +		("qed")
1.162 +	val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
1.163 +
1.164 +	val _ = TextIO.output (outfile, isar_proof)
1.165 +	val _ =  TextIO.closeOut outfile
1.166 +    in
1.167 +	isar_proof
1.168 +    end;
1.169
1.170  (* get fix vars from axioms - all Frees *)
1.171  (* check each clause for meta-vars and /\ over them at each step*)
```
```     2.1 --- a/src/HOL/Tools/ATP/spassshell	Thu May 26 16:50:20 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/spassshell	Thu May 26 18:34:23 2005 +0200
2.3 @@ -1,4 +1,7 @@
2.4 -
2.5 +#!/bin/sh
2.6 +#  ID: \$Id\$
2.7 +# Shell script to invoke SPASS and filter the output
2.8
2.9 -`isatool getenv -b SPASS_HOME`/SPASS  \$* |testoutput.py
2.10 -#\$SPASS_HOME  \$* |testoutput.py
2.11 +`isatool getenv -b SPASS_HOME`/SPASS  \$* | \
2.12 +    `isatool getenv -b ISABELLE_HOME`/src/HOL/Tools/ATP/testoutput.py
2.13 +
```
```     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu May 26 16:50:20 2005 +0200
3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu May 26 18:34:23 2005 +0200
3.3 @@ -164,7 +164,7 @@
3.4  			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
3.5  	  val _ =  TextIO.closeOut outfile
3.6  	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
3.7 -	 val probID = ReconOrderClauses.last(explode probfile)
3.8 +	  val probID = ReconOrderClauses.last(explode probfile)
3.9  	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
3.10  	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
3.11  	  (*** hyps/local axioms just now                                                ***)
3.12 @@ -174,16 +174,16 @@
3.13  			   else File.mkdir dfg_dir;
3.14
3.15  	  val dfg_path = File.sysify_path dfg_dir;
3.16 +	  val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
3.17  	  val exec_tptp2x =
3.18 -	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",
3.19 -	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
3.20 + 	      Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
3.21  	(*val _ = Posix.Process.wait ()*)
3.22  	(*val _ =Unix.reap exec_tptp2x*)
3.23  	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
3.24
3.25         in
3.26  	  goals_being_watched := (!goals_being_watched) + 1;
3.27 -	  Posix.Process.sleep(Time.fromSeconds 1);
3.28 +	  Posix.Process.sleep(Time.fromSeconds 4);
3.29  	  (warning ("probfile is: "^probfile));
3.30  	  (warning("dfg file is: "^newfile));
3.31  	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
3.32 @@ -196,8 +196,8 @@
3.33  	  if File.exists
3.34  	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
3.35  	  then callResProvers (toWatcherStr, args)
3.36 -	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
3.37 -	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
3.38 +	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^
3.39 +	              space_implode " " tptp2x_args)
3.40        end
3.41  (*
3.42  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n"
```