further tweaks to the SPASS setup
authorpaulson
Thu May 26 18:34:23 2005 +0200 (2005-05-26)
changeset 160913683f0486a11
parent 16090 fbb5ae140535
child 16092 a1a481ee9425
further tweaks to the SPASS setup
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/spassshell
src/HOL/Tools/ATP/watcher.ML
     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"