Added VampCommunication.ML.
authorquigley
Mon Jun 20 18:39:24 2005 +0200 (2005-06-20)
changeset 16478d0a1f6231e2f
parent 16477 e1a36498a30f
child 16479 cf872f3e16d9
Added VampCommunication.ML.
Changed small set of Spass rules to Ordered version.
Fixed printing out of resolution proofs if parsing/translation fails.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/VampCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Mon Jun 20 16:41:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Mon Jun 20 18:39:24 2005 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  signature SPASS_COMM =
     1.5    sig
     1.6      val reconstruct : bool ref
     1.7 +    val spass: bool ref
     1.8      val getSpassInput : TextIO.instream -> string * string * string
     1.9      val checkSpassProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    1.10                                 string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
    1.11 @@ -21,6 +22,7 @@
    1.12  
    1.13  (* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    1.14  val reconstruct = ref true;
    1.15 +val spass = ref true;
    1.16  
    1.17  (***********************************)
    1.18  (*  Write Spass   output to a file *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/ATP/VampCommunication.ML	Mon Jun 20 18:39:24 2005 +0200
     2.3 @@ -0,0 +1,281 @@
     2.4 +(*  Title:      VampCommunication.ml
     2.5 +    ID:         $Id$
     2.6 +    Author:     Claire Quigley
     2.7 +    Copyright   2004  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +(***************************************************************************)
    2.11 +(*  Code to deal with the transfer of proofs from a Vamp process          *)
    2.12 +(***************************************************************************)
    2.13 +signature VAMP_COMM =
    2.14 +  sig
    2.15 +    val reconstruct : bool ref
    2.16 +    val getVampInput : TextIO.instream -> string * string * string
    2.17 +    val checkVampProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    2.18 +                               string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
    2.19 +    
    2.20 +  end;
    2.21 +
    2.22 +structure VampComm :VAMP_COMM =
    2.23 +struct
    2.24 +
    2.25 +(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    2.26 +val reconstruct = ref true;
    2.27 +
    2.28 +(***********************************)
    2.29 +(*  Write Vamp   output to a file *)
    2.30 +(***********************************)
    2.31 +
    2.32 +fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    2.33 +			 in if (thisLine = "%==============  End of proof. ==================\n" )
    2.34 +			    then TextIO.output (fd, thisLine)
    2.35 +      			  else (
    2.36 +				TextIO.output (fd, thisLine); logVampInput (instr,fd))
    2.37 + 			 end;
    2.38 +
    2.39 +(**********************************************************************)
    2.40 +(*  Reconstruct the Vamp proof w.r.t. thmstring (string version of   *)
    2.41 +(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    2.42 +(*  steps as a string to the input pipe of the main Isabelle process  *)
    2.43 +(**********************************************************************)
    2.44 +
    2.45 +
    2.46 +val atomize_tac =
    2.47 +    SUBGOAL
    2.48 +     (fn (prop,_) =>
    2.49 +	 let val ts = Logic.strip_assums_hyp prop
    2.50 +	 in EVERY1 
    2.51 +		[METAHYPS
    2.52 +		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    2.53 +	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    2.54 +     end);
    2.55 +
    2.56 +
    2.57 +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) = 
    2.58 + let val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
    2.59 + in
    2.60 +SELECT_GOAL
    2.61 +  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    2.62 +  METAHYPS(fn negs => ((*if !reconstruct 
    2.63 +		       then 
    2.64 +			   Recon_Transfer.vampString_to_reconString proofextract thmstring goalstring 
    2.65 +								     toParent ppid negs clause_arr  num_of_clauses 
    2.66 +		       else*)
    2.67 +			   Recon_Transfer.vampString_to_lemmaString proofextract thmstring goalstring 
    2.68 +								     toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    2.69 + end ;
    2.70 +
    2.71 +
    2.72 +fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = let 
    2.73 +                         val thisLine = TextIO.inputLine fromChild 
    2.74 +			 in 
    2.75 +                            if (thisLine = "%==============  End of proof. ==================\n" )
    2.76 +			    then ( 
    2.77 +                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    2.78 +                                        val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
    2.79 +                                
    2.80 +			            in 
    2.81 +
    2.82 +                                        TextIO.output(foo,(proofextract));TextIO.closeOut foo;
    2.83 +                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  clause_arr  num_of_clauses thm
    2.84 +                                               
    2.85 +                                    end
    2.86 +                                  )
    2.87 +      			    else (
    2.88 +				
    2.89 +                                transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr,  num_of_clauses)
    2.90 +                                )
    2.91 + 			 end;
    2.92 +
    2.93 +
    2.94 +
    2.95 +
    2.96 +(*********************************************************************************)
    2.97 +(*  Inspect the output of a Vamp   process to see if it has found a proof,      *)
    2.98 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    2.99 +(*********************************************************************************)
   2.100 +
   2.101 + 
   2.102 +fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = 
   2.103 +                                      (*let val _ = Posix.Process.wait ()
   2.104 +                                      in*)
   2.105 +                                       
   2.106 +                                       if (isSome (TextIO.canInput(fromChild, 5)))
   2.107 +                                       then
   2.108 +                                       (
   2.109 +                                       let val thisLine = TextIO.inputLine fromChild  
   2.110 +                                           in                 
   2.111 +                                              if (thisLine = "%================== Proof: ======================\n")
   2.112 +                                             then     
   2.113 +                                              ( 
   2.114 +                                                 let 
   2.115 +                                               val outfile =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
   2.116 +                                               val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
   2.117 +                                               val _ =  TextIO.closeOut outfile;
   2.118 +                                               in
   2.119 +                                                transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr,  num_of_clauses);
   2.120 +                                                true
   2.121 +                                               end)
   2.122 +                                             
   2.123 +                                             else 
   2.124 +                                                (
   2.125 +                                                 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
   2.126 +                                                )
   2.127 +                                            end
   2.128 +                                           )
   2.129 +                                         else (false)
   2.130 +                                     (*  end*)
   2.131 +
   2.132 +
   2.133 +
   2.134 +fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
   2.135 +                                       let val vamp_proof_file =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "vamp_proof")))
   2.136 +                                            val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkvamp")));                                                                            
   2.137 +                                            val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
   2.138 +                                             
   2.139 +                                            val _ =  TextIO.closeOut outfile
   2.140 +                                       in 
   2.141 +                                       if (isSome (TextIO.canInput(fromChild, 5)))
   2.142 +                                       then
   2.143 +                                       (
   2.144 +                                       let val thisLine = TextIO.inputLine fromChild  
   2.145 +                                           in if (thisLine = "% Proof found. Thanks to Tanya!\n" )
   2.146 +                                              then      
   2.147 +                                              (  
   2.148 +                                                 let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   2.149 +                                                     val _ = TextIO.output (outfile, (thisLine))
   2.150 +                                             
   2.151 +                                                     val _ =  TextIO.closeOut outfile
   2.152 +                                                 in 
   2.153 +                                                    startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
   2.154 +                                                 end
   2.155 +                                               )   
   2.156 +                                               else if (thisLine = "% Unprovable.\n" ) 
   2.157 +                                                   then  
   2.158 +
   2.159 +                                                 (
   2.160 +                                                      let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
   2.161 +                                                             val _ = TextIO.output (outfile, (thisLine))
   2.162 +                                             
   2.163 +                                                             val _ =  TextIO.closeOut outfile
   2.164 +                                                      in
   2.165 +                                                       
   2.166 +                                                        TextIO.output (toParent,childCmd^"\n" );
   2.167 +                                                        TextIO.flushOut toParent;
   2.168 +                                                        TextIO.output (vamp_proof_file, (thisLine));
   2.169 +                                                        TextIO.flushOut vamp_proof_file;
   2.170 +                                                        TextIO.closeOut vamp_proof_file;
   2.171 +                                                        (*TextIO.output (toParent, thisLine);
   2.172 +                                                        TextIO.flushOut toParent;
   2.173 +                                                        TextIO.output (toParent, "bar\n");
   2.174 +                                                        TextIO.flushOut toParent;*)
   2.175 +
   2.176 +                                                       TextIO.output (toParent, thisLine^"\n");
   2.177 +                                                       TextIO.flushOut toParent;
   2.178 +                                                       TextIO.output (toParent, thmstring^"\n");
   2.179 +                                                       TextIO.flushOut toParent;
   2.180 +                                                       TextIO.output (toParent, goalstring^"\n");
   2.181 +                                                       TextIO.flushOut toParent;
   2.182 +                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.183 +                                                       (* Attempt to prevent several signals from turning up simultaneously *)
   2.184 +                                                       Posix.Process.sleep(Time.fromSeconds 1);
   2.185 +                                                        true  
   2.186 +                                                      end) 
   2.187 +                                                     else if (thisLine = "% Proof not found.\n")
   2.188 +                                                          then  
   2.189 +                                                (
   2.190 +                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.191 +                                                        TextIO.output (toParent,childCmd^"\n" );
   2.192 +                                                        TextIO.flushOut toParent;
   2.193 +                                                        TextIO.output (toParent, thisLine);
   2.194 +                                                        TextIO.flushOut toParent;
   2.195 +
   2.196 +                                                        true) 
   2.197 +                                                          
   2.198 +                                                    else
   2.199 +                                                       (TextIO.output (vamp_proof_file, (thisLine));
   2.200 +                                                       TextIO.flushOut vamp_proof_file;
   2.201 +                                                       checkVampProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   2.202 +
   2.203 +                                              end
   2.204 +                                          )
   2.205 +                                         else 
   2.206 +                                             (TextIO.output (vamp_proof_file, ("No proof output seen \n"));TextIO.closeOut vamp_proof_file;false)
   2.207 +                                      end
   2.208 +
   2.209 +  
   2.210 +(***********************************************************************)
   2.211 +(*  Function used by the Isabelle process to read in a vamp proof   *)
   2.212 +(***********************************************************************)
   2.213 +
   2.214 +
   2.215 +
   2.216 +fun getVampInput instr = if (isSome (TextIO.canInput(instr, 2)))
   2.217 +                          then
   2.218 +                               let val thisLine = TextIO.inputLine instr 
   2.219 +                                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
   2.220 +                                             
   2.221 +                                   val _ =  TextIO.closeOut outfile
   2.222 +			       in    (* reconstructed proof string *)
   2.223 +                                     if ( (substring (thisLine, 0,1))= "[")
   2.224 +                                     then 
   2.225 +			                 (*Pretty.writeln(Pretty.str (thisLine))*)
   2.226 +                                             let val reconstr = thisLine
   2.227 +                                                 val thmstring = TextIO.inputLine instr 
   2.228 +                                                 val goalstring = TextIO.inputLine instr   
   2.229 +                                             in
   2.230 +                                                 (reconstr, thmstring, goalstring)
   2.231 +                                             end
   2.232 +                                     else if (thisLine = "% Unprovable.\n" ) 
   2.233 +                                          then 
   2.234 +                                          (
   2.235 +                                             let val reconstr = thisLine
   2.236 +                                                 val thmstring = TextIO.inputLine instr
   2.237 +                                                 val goalstring = TextIO.inputLine instr
   2.238 +                                             in
   2.239 +                                                 (reconstr, thmstring, goalstring)
   2.240 +                                             end
   2.241 +                                          )
   2.242 +					else  if (thisLine = "% Proof not found.\n")
   2.243 +                                          then 
   2.244 +                                          (
   2.245 +                                             let val reconstr = thisLine
   2.246 +                                                 val thmstring = TextIO.inputLine instr
   2.247 +                                                 val goalstring = TextIO.inputLine instr
   2.248 +                                             in
   2.249 +                                                 (reconstr, thmstring, goalstring)
   2.250 +                                             end
   2.251 +                                          )
   2.252 +					else if (String.isPrefix   "Rules from"  thisLine)
   2.253 +                                        then 
   2.254 +                                          (
   2.255 +                                             let val reconstr = thisLine
   2.256 +                                                 val thmstring = TextIO.inputLine instr
   2.257 +                                                 val goalstring = TextIO.inputLine instr
   2.258 +                                             in
   2.259 +                                                 (reconstr, thmstring, goalstring)
   2.260 +                                             end
   2.261 +                                          )
   2.262 +
   2.263 +                                         else if (thisLine = "Proof found but translation failed!")
   2.264 +                                              then
   2.265 +  						(
   2.266 +						   let val reconstr = thisLine
   2.267 +                                                       val thmstring = TextIO.inputLine instr
   2.268 +                                                       val goalstring = TextIO.inputLine instr
   2.269 +						      val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getVamp")));
   2.270 +                                    		val _ = TextIO.output (outfile, (thisLine))
   2.271 +                                     			 val _ =  TextIO.closeOut outfile
   2.272 +                                                   in
   2.273 +                                                      (reconstr, thmstring, goalstring)
   2.274 +                                                   end
   2.275 +						)
   2.276 +                                        	 else
   2.277 +                                                     getVampInput instr
   2.278 +                                            
   2.279 + 			        end
   2.280 +                          else 
   2.281 +                              ("No output from reconstruction process.\n","","")
   2.282 +
   2.283 +
   2.284 +end;
     3.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Mon Jun 20 16:41:47 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Mon Jun 20 18:39:24 2005 +0200
     3.3 @@ -30,6 +30,8 @@
     3.4  
     3.5  exception Noparse;
     3.6  exception SPASSError of string;
     3.7 +exception VampError of string;
     3.8 +
     3.9  
    3.10  fun (parser1 ++ parser2) input =
    3.11        let
    3.12 @@ -159,6 +161,9 @@
    3.13  *)
    3.14  
    3.15  
    3.16 +
    3.17 +
    3.18 +
    3.19  fun several p = many (some p)
    3.20        fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
    3.21    
    3.22 @@ -182,11 +187,54 @@
    3.23       (* val lex = fst ( alltokens ( (map str)  explode))*)
    3.24       fun lex s =  alltokens  (explode s)
    3.25  
    3.26 +
    3.27 +(*********************************************************)
    3.28 +(*  Temporary code to "parse" Vampire proofs             *)
    3.29 +(*********************************************************)
    3.30 +
    3.31 +fun num_int (Number n) = n
    3.32 +|   num_int _ = raise VampError "Not a number"
    3.33 +
    3.34 + fun takeUntil ch [] res  = (res, [])
    3.35 + |   takeUntil ch (x::xs) res = if   x = ch 
    3.36 +                                then
    3.37 +                                     (res, xs)
    3.38 +                                else
    3.39 +                                     takeUntil ch xs (res@[x])
    3.40 +       
    3.41 +fun linenums [] nums = nums
    3.42 +|   linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) []
    3.43 +                                in 
    3.44 +				  if rest = [] 
    3.45 +				  then 
    3.46 +				      nums
    3.47 +				  else
    3.48 +			          let val num = hd rest
    3.49 +                                      val int_of = num_int num
    3.50 +	
    3.51 +			          in
    3.52 +				     linenums rest (int_of::nums)
    3.53 +			         end
    3.54 +                                end
    3.55 +
    3.56 +fun get_linenums proofstr = let val s = extract_proof proofstr
    3.57 +                                val tokens = #1(lex s)
    3.58 +	                 
    3.59 +	                    in
    3.60 +		                rev (linenums tokens [])
    3.61 +		            end
    3.62 +
    3.63 +(************************************************************)
    3.64 +(************************************************************)
    3.65 +
    3.66 +
    3.67 +(**************************************************)
    3.68 +(* Code to parse SPASS proofs                     *)
    3.69 +(**************************************************)
    3.70 +
    3.71  datatype Tree = Leaf of string
    3.72                  | Branch of Tree * Tree
    3.73  
    3.74 -
    3.75 -
    3.76     
    3.77        fun number ((Number n)::rest) = (n, rest)
    3.78          | number _ = raise NOPARSE_NUM
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jun 20 16:41:47 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Jun 20 18:39:24 2005 +0200
     4.3 @@ -201,9 +201,9 @@
     4.4  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
     4.5      let val realnums = map subone step_nums	
     4.6  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
     4.7 -	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
     4.8 +(*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
     4.9  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    4.10 -	val _ = TextIO.closeOut(axnums)
    4.11 +	val _ = TextIO.closeOut(axnums)*)
    4.12      in
    4.13  	retrieve_axioms clause_arr  clasimp_nums
    4.14      end
    4.15 @@ -235,12 +235,11 @@
    4.16        clasimp_names
    4.17     end
    4.18      
    4.19 - fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    4.20 + fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    4.21     let 
    4.22       (* not sure why this is necessary again, but seems to be *)
    4.23        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    4.24 -      val axioms = get_init_axioms proof_steps
    4.25 -      val step_nums = get_step_nums axioms []
    4.26 +      val step_nums =get_linenums proofstr
    4.27    
    4.28       (***********************************************)
    4.29       (* here need to add the clauses from clause_arr*)
    4.30 @@ -455,7 +454,49 @@
    4.31                                                    val _ = TextIO.output (outfile, ("In exception handler"));
    4.32                                                    val _ =  TextIO.closeOut outfile
    4.33                                                in 
    4.34 -                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n");
    4.35 +                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
    4.36 +                                                  TextIO.flushOut toParent;
    4.37 +						   TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
    4.38 +                                         	   TextIO.flushOut toParent;
    4.39 +                                         	   TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
    4.40 +                                         	   TextIO.flushOut toParent;
    4.41 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    4.42 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    4.43 +                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
    4.44 +                                              end)
    4.45 +
    4.46 +
    4.47 +fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    4.48 +           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						       val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    4.49 +                                               val _ =  TextIO.closeOut outfile
    4.50 +
    4.51 +                                              (***********************************)
    4.52 +                                              (* get vampire axiom names         *)
    4.53 +                                              (***********************************)
    4.54 +         
    4.55 +                                               val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
    4.56 +                                               val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
    4.57 +                                               val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
    4.58 +                                               val _ =  TextIO.closeOut outfile
    4.59 +                                                   
    4.60 +                                              in 
    4.61 +                                                   TextIO.output (toParent, ax_str^"\n");
    4.62 +                                                   TextIO.flushOut toParent;
    4.63 +                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    4.64 +                                         	   TextIO.flushOut toParent;
    4.65 +                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    4.66 +                                         	   TextIO.flushOut toParent;
    4.67 +                                          
    4.68 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    4.69 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
    4.70 +                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
    4.71 +                                              end
    4.72 +                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
    4.73 +
    4.74 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
    4.75 +                                                  val _ =  TextIO.closeOut outfile
    4.76 +                                              in 
    4.77 +                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    4.78                                                    TextIO.flushOut toParent;
    4.79  						   TextIO.output (toParent, thmstring^"\n");
    4.80                                           	   TextIO.flushOut toParent;
    4.81 @@ -467,66 +508,6 @@
    4.82                                                end)
    4.83  
    4.84  
    4.85 -(*fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    4.86 -           let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    4.87 -                                                  val _ =  TextIO.closeOut outfile
    4.88 -
    4.89 -                                              (***********************************)
    4.90 -                                              (* parse spass proof into datatype *)
    4.91 -                                              (***********************************)
    4.92 -         
    4.93 -                                                  val tokens = #1(lex proofstr)
    4.94 -                                                  val proof_steps = VampParse.parse tokens
    4.95 -                                                  (*val proof_steps = just_change_space proof_steps1*)
    4.96 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    4.97 -                                                  val _ =  TextIO.closeOut outfile
    4.98 -                                                
    4.99 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   4.100 -                                                  val _ =  TextIO.closeOut outfile
   4.101 -                                              (************************************)
   4.102 -                                              (* recreate original subgoal as thm *)
   4.103 -                                              (************************************)
   4.104 -                                                
   4.105 -                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   4.106 -                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   4.107 -                                                  (* subgoal this is, and turn it into meta_clauses *)
   4.108 -                                                  (* should prob add array and table here, so that we can get axioms*)
   4.109 -                                                  (* produced from the clasimpset rather than the problem *)
   4.110 -
   4.111 -                                                  val (axiom_names) = get_axiom_names_vamp proof_steps  thms clause_arr  num_of_clauses
   4.112 -                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   4.113 -                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   4.114 -                                                  val _ =  TextIO.closeOut outfile
   4.115 -                                                   
   4.116 -                                              in 
   4.117 -                                                   TextIO.output (toParent, ax_str^"\n");
   4.118 -                                                   TextIO.flushOut toParent;
   4.119 -                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   4.120 -                                         	   TextIO.flushOut toParent;fdsa
   4.121 -                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   4.122 -                                         	   TextIO.flushOut toParent;
   4.123 -                                          
   4.124 -                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.125 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   4.126 -                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   4.127 -                                              end
   4.128 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   4.129 -
   4.130 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   4.131 -                                                  val _ =  TextIO.closeOut outfile
   4.132 -                                              in 
   4.133 -                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^(remove_linebreaks proofstr) ^"\n");
   4.134 -                                                  TextIO.flushOut toParent;
   4.135 -						   TextIO.output (toParent, thmstring^"\n");
   4.136 -                                         	   TextIO.flushOut toParent;
   4.137 -                                         	   TextIO.output (toParent, goalstring^"\n");
   4.138 -                                         	   TextIO.flushOut toParent;
   4.139 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   4.140 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   4.141 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   4.142 -                                              end)
   4.143 -*)
   4.144 -
   4.145  
   4.146  
   4.147  (* val proofstr = "1582[0:Inp] || -> v_P*.\
   4.148 @@ -619,7 +600,7 @@
   4.149  	  val _ = TextIO.output (outfile, ("In exception handler"));
   4.150  	  val _ =  TextIO.closeOut outfile
   4.151        in 
   4.152 -	   TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n");
   4.153 +	   TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   4.154  	  TextIO.flushOut toParent;
   4.155  	TextIO.output (toParent, thmstring^"\n");
   4.156  	   TextIO.flushOut toParent;
     5.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Jun 20 16:41:47 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Jun 20 18:39:24 2005 +0200
     5.3 @@ -135,12 +135,12 @@
     5.4  (*  Remove the \n character from the end of each filename                       *)
     5.5  (********************************************************************************)
     5.6  
     5.7 -fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
     5.8 +(*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
     5.9                      in
    5.10                          if (String.isPrefix "\n"  (implode backList )) 
    5.11                          then (implode (rev ((tl backList))))
    5.12                          else cmdStr
    5.13 -                    end
    5.14 +                    end*)
    5.15                              
    5.16  (********************************************************************************)
    5.17  (*  Send request to Watcher for a vampire to be called for filename in arg      *)
    5.18 @@ -270,25 +270,57 @@
    5.19      
    5.20      val tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X"
    5.21  
    5.22 -    val _ = if File.exists (File.unpack_platform_path tptp2X) then () 
    5.23 -	    else error ("Could not find the file " ^ tptp2X)
    5.24 -    
    5.25 -    val bar = (fn s => (File.write (File.tmp_path (Path.basic "tptp2X-call")) s; system s)) 
    5.26 -              (tptp2X ^ " -fdfg -d " ^ dfg_path ^ " " ^ File.platform_path wholefile)
    5.27 -    val newfile = dfg_path ^ "/ax_prob" ^ "_" ^ probID ^ ".dfg"
    5.28 -    val _ = File.append (File.tmp_path (Path.basic "thmstring_in_watcher"))
    5.29 -			(thmstring ^ "\n goals_watched" ^
    5.30 -			string_of_int(!goals_being_watched) ^ newfile ^ "\n")
    5.31 -    
    5.32 -  in
    5.33 -    (prover,thmstring,goalstring, proverCmd, settings,newfile)	
    5.34 -  end;
    5.35 +
    5.36 +  		(*** need to check here if the directory exists and, if not, create it***)
    5.37 +  		
    5.38 +
    5.39 + 		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    5.40 +		val probID = List.last(explode probfile)
    5.41 +    		val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    5.42 +
    5.43 +    		(*** only include problem and clasimp for the moment, not sure how to refer to ***)
    5.44 +   		(*** hyps/local axioms just now                                                ***)
    5.45 +   		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    5.46 +    		val dfg_create = 
    5.47 +		    if !SpassComm.spass
    5.48 +                    then 
    5.49 + 	     		if File.exists dfg_dir 
    5.50 +     	        	then
    5.51 +     	           	    ((warning("dfg dir exists"));())
    5.52 + 			else
    5.53 + 		    	    File.mkdir dfg_dir
    5.54 +		    else
    5.55 +			(warning("not converting to dfg");())
    5.56 +   		val dfg_path = File.platform_path dfg_dir;
    5.57 +   		
    5.58 +   		val bar = if !SpassComm.spass then system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^
    5.59 +                                 (File.platform_path wholefile)^" -d "^dfg_path)
    5.60 +			  else
    5.61 +				7
    5.62 +
    5.63 +    		val newfile =   if !SpassComm.spass 
    5.64 +				then 
    5.65 +					dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    5.66 +			        else
    5.67 +					(File.platform_path wholefile)
    5.68 +				  
    5.69 +                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));   
    5.70 +   		val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))
    5.71 + 		val _ =  TextIO.closeOut outfile
    5.72 +
    5.73 + 	     in
    5.74 + 		(prover,thmstring,goalstring, proverCmd, settings,newfile)	
    5.75 +	     end;
    5.76 +
    5.77  
    5.78  
    5.79  (* remove \n from end of command and put back into tuple format *)
    5.80               
    5.81  
    5.82 -(*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" *)
    5.83 +(*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n"
    5.84 +
    5.85 +val cmdStr = "vampire*(length (rev xs) = length xs  [.]) & (length (rev (a # xs)) ~= length (a # xs) [.])*length (rev []) = length []*/homes/jm318/Vampire8/vkernel*-t 300%-m 100000*/local/scratch/clq20/23523/clasimp*/local/scratch/clq20/23523/hyps*/local/scratch/clq20/23523/prob_1\n"
    5.86 + *)
    5.87  
    5.88  (*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)
    5.89  
    5.90 @@ -441,8 +473,14 @@
    5.91  		 end
    5.92  		      
    5.93  	       fun pollChildInput (fromStr) = 
    5.94 -		 let val iod = getInIoDesc fromStr
    5.95 -		 in 
    5.96 +
    5.97 +		     let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
    5.98 +			           ("In child_poll\n")
    5.99 +                       val iod = getInIoDesc fromStr
   5.100 +		     in 
   5.101 +
   5.102 +		 
   5.103 +
   5.104  		     if isSome iod 
   5.105  		     then 
   5.106  			 let val pd = OS.IO.pollDesc (valOf iod)
   5.107 @@ -450,17 +488,22 @@
   5.108  			 if (isSome pd ) then 
   5.109  			     let val pd' = OS.IO.pollIn (valOf pd)
   5.110  				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   5.111 -                                 val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   5.112 -			           ("In child_poll\n")
   5.113 +                                 
   5.114  			     in
   5.115  				if null pdl 
   5.116  				then
   5.117 -				   NONE
   5.118 +				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   5.119 +			           ("Null pdl \n");NONE)
   5.120  				else if (OS.IO.isIn (hd pdl)) 
   5.121  				     then
   5.122 -					 SOME ((*getCmd*) (TextIO.inputLine fromStr))
   5.123 +					 (let val inval =  (TextIO.inputLine fromStr)
   5.124 +                              	              val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
   5.125 +					  in
   5.126 +						SOME inval
   5.127 +					  end)
   5.128  				     else
   5.129 -					 NONE
   5.130 +					   ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
   5.131 +			           ("Null pdl \n");NONE)
   5.132  			     end
   5.133  			   else
   5.134  			       NONE
   5.135 @@ -505,8 +548,9 @@
   5.136  		      then 
   5.137  			  (* check here for prover label on child*)
   5.138  			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   5.139 -		      val childDone = (case prover of
   5.140 -	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   5.141 +		              val childDone = (case prover of
   5.142 +	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
   5.143 +                                 |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   5.144  			   in
   5.145  			    if childDone      (**********************************************)
   5.146  			    then              (* child has found a proof and transferred it *)
   5.147 @@ -561,6 +605,7 @@
   5.148  		   else 
   5.149  		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (settings@[file])))
   5.150  			   val (instr, outstr)=Unix.streamsOf childhandle
   5.151 +                           
   5.152  			   val newProcList =    (((CMDPROC{
   5.153  						prover = prover,
   5.154  						cmd = file,
   5.155 @@ -569,6 +614,8 @@
   5.156  						proc_handle = childhandle,
   5.157  						instr = instr,
   5.158  						outstr = outstr })::procList))
   5.159 +              
   5.160 +                           val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^(TextIO.input instr)^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   5.161  		       in
   5.162  			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   5.163  		       end
   5.164 @@ -768,14 +815,14 @@
   5.165                             val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   5.166                             fun vampire_proofHandler (n) =
   5.167                             (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   5.168 -                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   5.169 +                           VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   5.170                            
   5.171  
   5.172  fun spass_proofHandler (n) = (
   5.173                                   let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
   5.174                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
   5.175                                        val _ =  TextIO.closeOut outfile
   5.176 -                                      val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin
   5.177 +                                      val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   5.178                                        val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
   5.179  
   5.180                                        val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   5.181 @@ -808,7 +855,7 @@
   5.182                                                                   (
   5.183                                                                       goals_being_watched := (!goals_being_watched) -1;
   5.184                                                                       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   5.185 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   5.186 +                                                                      Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
   5.187                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   5.188                                                                        if (!goals_being_watched = 0)
   5.189                                                                        then 
     6.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jun 20 16:41:47 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jun 20 18:39:24 2005 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4  
     6.5  
     6.6  signature RES_ATP = 
     6.7 -sig
     6.8 +sig  
     6.9  val trace_res : bool ref
    6.10  val subgoals: Thm.thm list
    6.11  val traceflag : bool ref
    6.12 @@ -22,6 +22,8 @@
    6.13  (*val atp_tac : int -> Tactical.tactic*)
    6.14  val debug: bool ref
    6.15  val full_spass: bool ref
    6.16 +(*val spass: bool ref*)
    6.17 +val vampire: bool ref
    6.18  end;
    6.19  
    6.20  structure ResAtp : RES_ATP =
    6.21 @@ -36,7 +38,14 @@
    6.22  
    6.23  fun debug_tac tac = (warning "testing";tac);
    6.24  (* default value is false *)
    6.25 +
    6.26  val full_spass = ref false;
    6.27 +
    6.28 +(* use spass as default prover *)
    6.29 +(*val spass = ref true;*)
    6.30 +
    6.31 +val vampire = ref false;
    6.32 +
    6.33  val trace_res = ref false;
    6.34  
    6.35  val skolem_tac = skolemize_tac;
    6.36 @@ -171,16 +180,22 @@
    6.37  	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    6.38  	val _ = (warning ("prob file in cal_res_tac is: "^probfile))                                                                           
    6.39  in
    6.40 - 	if !full_spass 
    6.41 -  	then
    6.42 +     if !SpassComm.spass 
    6.43 +       then if !full_spass 
    6.44 +            then
    6.45     		([("spass", thmstr, goalstring (*,spass_home*), 
    6.46  	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    6.47  	     	"-DocProof%-TimeLimit=60", 
    6.48  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    6.49 -  	else	
    6.50 +  	    else	
    6.51     		([("spass", thmstr, goalstring (*,spass_home*), 
    6.52  	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
    6.53 -	     	"-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
    6.54 +	     	"-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
    6.55 +	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    6.56 +     else
    6.57 +	   ([("vampire", thmstr, goalstring (*,spass_home*), 
    6.58 +	    	 "/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    6.59 +	     	"-t 300%-m 100000", 
    6.60  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    6.61  end
    6.62