src/HOL/Tools/ATP/watcher.ML
changeset 16561 2bc33f0cfe9a
parent 16548 aa36ae6b955e
child 16675 96bdc59afc05
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Jun 24 13:22:08 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Jun 24 16:18:41 2005 +0200
     1.3 @@ -266,36 +266,36 @@
     1.4      
     1.5      val tptp2X = ResLib.helper_path "TPTP2X_HOME" "tptp2X"  		
     1.6  
     1.7 - 		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
     1.8 -		val probID = List.last(explode probfile)
     1.9 -    		val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.10 +    (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.11 +    val probID = List.last(explode probfile)
    1.12 +    val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.13  
    1.14 -    		(*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.15 -   		(*** hyps/local axioms just now                                                ***)
    1.16 -   		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    1.17 -                (*** check if the directory exists and, if not, create it***)
    1.18 -    		val _ = 
    1.19 -		    if !SpassComm.spass
    1.20 -                    then 
    1.21 -			if File.exists dfg_dir then warning("dfg dir exists")
    1.22 -			else File.mkdir dfg_dir
    1.23 +    (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.24 +    (*** hyps/local axioms just now                                                ***)
    1.25 +    val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
    1.26 +    (*** check if the directory exists and, if not, create it***)
    1.27 +    val _ = 
    1.28 +	if !SpassComm.spass
    1.29 +	then 
    1.30 +	    if File.exists dfg_dir then warning("dfg dir exists")
    1.31 +	    else File.mkdir dfg_dir
    1.32 +	else
    1.33 +	    warning("not converting to dfg")
    1.34 +    
    1.35 +    val _ = if !SpassComm.spass then 
    1.36 +		system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
    1.37 +			File.platform_path wholefile)
    1.38 +	      else 7
    1.39 +    val newfile =   if !SpassComm.spass 
    1.40 +		    then 
    1.41 +			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    1.42  		    else
    1.43 -			warning("not converting to dfg")
    1.44 -   		
    1.45 -   		val _ = if !SpassComm.spass then 
    1.46 -   		            system (tptp2X ^ " -fdfg -d "^dfg_path^" "^
    1.47 -                                    File.platform_path wholefile)
    1.48 -			  else 7
    1.49 -    		val newfile =   if !SpassComm.spass 
    1.50 -				then 
    1.51 -					dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    1.52 -			        else
    1.53 -					(File.platform_path wholefile)
    1.54 - 		val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.55 - 		           (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    1.56 - 	     in
    1.57 - 		(prover,thmstring,goalstring, proverCmd, settings,newfile)	
    1.58 -	     end;
    1.59 +			    (File.platform_path wholefile)
    1.60 +    val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.61 +	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    1.62 +  in
    1.63 +    (prover,thmstring,goalstring, proverCmd, settings,newfile)	
    1.64 +  end;
    1.65  
    1.66  
    1.67  
    1.68 @@ -574,41 +574,45 @@
    1.69  
    1.70  (*** add subgoal id num to this *)
    1.71  	     fun execCmds  [] procList = procList
    1.72 -	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("About to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
    1.73 +	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
    1.74  	       in 
    1.75  		 if (prover = "spass") 
    1.76 -		   then 
    1.77 -		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
    1.78 -			   val (instr, outstr)=Unix.streamsOf childhandle
    1.79 -			   val newProcList =    (((CMDPROC{
    1.80 -						prover = prover,
    1.81 -						cmd = file,
    1.82 -						thmstring = thmstring,
    1.83 -						goalstring = goalstring,
    1.84 -						proc_handle = childhandle,
    1.85 -						instr = instr,
    1.86 -						outstr = outstr })::procList))
    1.87 -			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
    1.88 -		       in
    1.89 -			  Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
    1.90 -		       end
    1.91 -		   else 
    1.92 -		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (settings@[file])))
    1.93 -			   val (instr, outstr)=Unix.streamsOf childhandle
    1.94 -                           
    1.95 -			   val newProcList =    (((CMDPROC{
    1.96 -						prover = prover,
    1.97 -						cmd = file,
    1.98 -						thmstring = thmstring,
    1.99 -						goalstring = goalstring,
   1.100 -						proc_handle = childhandle,
   1.101 -						instr = instr,
   1.102 -						outstr = outstr })::procList))
   1.103 -              
   1.104 -                           val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.105 -		       in
   1.106 -			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   1.107 -		       end
   1.108 +		 then 
   1.109 +		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.110 +		            (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.111 +		       val (instr, outstr) = Unix.streamsOf childhandle
   1.112 +		       val newProcList =    (((CMDPROC{
   1.113 +					    prover = prover,
   1.114 +					    cmd = file,
   1.115 +					    thmstring = thmstring,
   1.116 +					    goalstring = goalstring,
   1.117 +					    proc_handle = childhandle,
   1.118 +					    instr = instr,
   1.119 +					    outstr = outstr })::procList))
   1.120 +			val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
   1.121 +			     ("\nexecuting command for goal:\n"^
   1.122 +			      goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.123 +		   in
   1.124 +		      Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
   1.125 +		   end
   1.126 +		 else 
   1.127 +		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   1.128 +		            (Unix.execute(proverCmd, (settings@[file])))
   1.129 +		       val (instr, outstr) = Unix.streamsOf childhandle
   1.130 +		       
   1.131 +		       val newProcList =    (((CMDPROC{
   1.132 +					    prover = prover,
   1.133 +					    cmd = file,
   1.134 +					    thmstring = thmstring,
   1.135 +					    goalstring = goalstring,
   1.136 +					    proc_handle = childhandle,
   1.137 +					    instr = instr,
   1.138 +					    outstr = outstr })::procList))
   1.139 +	  
   1.140 +		       val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   1.141 +		   in
   1.142 +		     Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   1.143 +		   end
   1.144  		end
   1.145  
   1.146