using TPTP2X_HOME; indentation, etc
authorpaulson
Mon Jun 20 15:55:44 2005 +0200 (2005-06-20)
changeset 164758f3ba52a7937
parent 16474 c3c0208988c0
child 16476 baa008d0fee9
using TPTP2X_HOME; indentation, etc
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Jun 20 15:54:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Jun 20 15:55:44 2005 +0200
     1.3 @@ -156,19 +156,21 @@
     1.4  
     1.5      
     1.6  (* need to modify to send over hyps file too *)
     1.7 -fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
     1.8 -                                     TextIO.flushOut toWatcherStr)
     1.9 -|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
    1.10 -                                          let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "tog_comms")));                                                                                    
    1.11 -                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^settings^clasimpfile^hypsfile^probfile) )
    1.12 -                              val _ =  TextIO.closeOut outfile
    1.13 -                                        in   (sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
    1.14 -							             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
    1.15 -                                          goals_being_watched := (!goals_being_watched) + 1;
    1.16 -                                          TextIO.flushOut toWatcherStr;
    1.17 -					  
    1.18 -                                          callResProvers (toWatcherStr,args))
    1.19 -                                        end   
    1.20 +fun callResProvers (toWatcherStr,  []) = 
    1.21 +      (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    1.22 +|   callResProvers (toWatcherStr,
    1.23 +                    (prover,thmstring,goalstring, proverCmd,settings,clasimpfile, 
    1.24 +                     axfile, hypsfile,probfile)  ::  args) =
    1.25 +      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
    1.26 +                             (prover^thmstring^goalstring^proverCmd^settings^
    1.27 +                              clasimpfile^hypsfile^probfile)
    1.28 +      in sendOutput (toWatcherStr,    
    1.29 +            (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
    1.30 +             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
    1.31 +         goals_being_watched := (!goals_being_watched) + 1;
    1.32 +	 TextIO.flushOut toWatcherStr;
    1.33 +	 callResProvers (toWatcherStr,args)
    1.34 +      end   
    1.35                                                  
    1.36  
    1.37  (*
    1.38 @@ -207,79 +209,80 @@
    1.39                                       getSettings rest (settings@[(implode set)])
    1.40                                   end
    1.41  
    1.42 -fun separateFields str = let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
    1.43 -                              val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
    1.44 -                              val _ =  TextIO.closeOut outfile
    1.45 -                              val (prover, rest) = takeUntil "*" str []
    1.46 -                              val prover = implode prover
    1.47 -
    1.48 -                              val (thmstring, rest) =  takeUntil "*" rest []
    1.49 -                              val thmstring = implode thmstring
    1.50 +fun separateFields str =
    1.51 +  let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
    1.52 +      val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
    1.53 +      val _ =  TextIO.closeOut outfile
    1.54 +      val (prover, rest) = takeUntil "*" str []
    1.55 +      val prover = implode prover
    1.56  
    1.57 -                              val (goalstring, rest) =  takeUntil "*" rest []
    1.58 -                              val goalstring = implode goalstring
    1.59 +      val (thmstring, rest) =  takeUntil "*" rest []
    1.60 +      val thmstring = implode thmstring
    1.61  
    1.62 -                              val (proverCmd, rest ) =  takeUntil "*" rest []
    1.63 -                              val proverCmd = implode proverCmd
    1.64 -                              
    1.65 -                              val (settings, rest) =  takeUntil "*" rest []
    1.66 -                              val settings = getSettings settings []
    1.67 +      val (goalstring, rest) =  takeUntil "*" rest []
    1.68 +      val goalstring = implode goalstring
    1.69  
    1.70 -			      val (clasimpfile, rest ) =  takeUntil "*" rest []
    1.71 -                              val clasimpfile = implode clasimpfile
    1.72 -                              
    1.73 -  			      val (hypsfile, rest ) =  takeUntil "*" rest []
    1.74 -                              val hypsfile = implode hypsfile
    1.75 -
    1.76 -                              val (file, rest) =  takeUntil "*" rest []
    1.77 -                              val file = implode file
    1.78 +      val (proverCmd, rest ) =  takeUntil "*" rest []
    1.79 +      val proverCmd = implode proverCmd
    1.80 +      
    1.81 +      val (settings, rest) =  takeUntil "*" rest []
    1.82 +      val settings = getSettings settings []
    1.83  
    1.84 -                              val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
    1.85 -                              val _ = TextIO.output (outfile,("Sep comms are: "^(implode str)^"**"^prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n") )
    1.86 -                              val _ =  TextIO.closeOut outfile
    1.87 -                              
    1.88 -                          in
    1.89 -                             (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
    1.90 -                          end
    1.91 +      val (clasimpfile, rest ) =  takeUntil "*" rest []
    1.92 +      val clasimpfile = implode clasimpfile
    1.93 +      
    1.94 +      val (hypsfile, rest ) =  takeUntil "*" rest []
    1.95 +      val hypsfile = implode hypsfile
    1.96  
    1.97 - 
    1.98 +      val (file, rest) =  takeUntil "*" rest []
    1.99 +      val file = implode file
   1.100 +
   1.101 +      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
   1.102 +                  ("Sep comms are: "^(implode str)^"**"^
   1.103 +                   prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n")
   1.104 +  in
   1.105 +     (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
   1.106 +  end
   1.107 +
   1.108                        
   1.109  (***********************************************************************************)
   1.110  (* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *)
   1.111  (***********************************************************************************)
   1.112  
   1.113  fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 
   1.114 - let
   1.115 -		val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   1.116 -
   1.117 -  		(*** need to check here if the directory exists and, if not, create it***)
   1.118 -  		
   1.119 -
   1.120 - 		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   1.121 -		val probID = List.last(explode probfile)
   1.122 -    		val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   1.123 +  let
   1.124 +    (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   1.125 +    val probID = List.last(explode probfile)
   1.126 +    val wholefile = File.tmp_path (Path.basic ("ax_prob_" ^ probID))
   1.127 +    
   1.128 +    (*** only include problem and clasimp for the moment, not sure 
   1.129 +	 how to refer to hyps/local axioms just now ***)
   1.130 +    val whole_prob_file = Unix.execute("/bin/cat", 
   1.131 +	     [clasimpfile,(*axfile, hypsfile,*)probfile,  ">",
   1.132 +	      File.platform_path wholefile])
   1.133 +    
   1.134 +    val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   1.135 +    (*** check if the directory exists and, if not, create it***)
   1.136 +    val dfg_create =
   1.137 +	  if File.exists dfg_dir then warning("dfg dir exists")
   1.138 +	  else File.mkdir dfg_dir; 
   1.139 +    val dfg_path = File.platform_path dfg_dir;
   1.140 +    
   1.141 +    val tptp2X = getenv "TPTP2X_HOME" ^ "/tptp2X"
   1.142  
   1.143 -    		(*** only include problem and clasimp for the moment, not sure how to refer to ***)
   1.144 -   		(*** hyps/local axioms just now                                                ***)
   1.145 -   		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
   1.146 -    		val dfg_create =
   1.147 - 		if File.exists dfg_dir 
   1.148 -     	        then
   1.149 -     	            ((warning("dfg dir exists"));())
   1.150 - 		else
   1.151 - 		     File.mkdir dfg_dir; 
   1.152 -   		val dfg_path = File.platform_path dfg_dir;
   1.153 -   		
   1.154 -   		val bar = system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^
   1.155 -                                 (File.platform_path wholefile)^" -d "^dfg_path)
   1.156 -    		val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   1.157 -                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));   
   1.158 -   		val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))
   1.159 - 		val _ =  TextIO.closeOut outfile
   1.160 -
   1.161 - 	     in
   1.162 - 		(prover,thmstring,goalstring, proverCmd, settings,newfile)	
   1.163 -	     end;
   1.164 +    val _ = if File.exists (File.unpack_platform_path tptp2X) then () 
   1.165 +	    else error ("Could not find the file " ^ tptp2X)
   1.166 +    
   1.167 +    val bar = (fn s => (File.write (File.tmp_path (Path.basic "tptp2X-call")) s; system s)) 
   1.168 +              (tptp2X ^ " -fdfg -d " ^ dfg_path ^ " " ^ File.platform_path wholefile)
   1.169 +    val newfile = dfg_path ^ "/ax_prob" ^ "_" ^ probID ^ ".dfg"
   1.170 +    val _ = File.append (File.tmp_path (Path.basic "thmstring_in_watcher"))
   1.171 +			(thmstring ^ "\n goals_watched" ^
   1.172 +			string_of_int(!goals_being_watched) ^ newfile ^ "\n")
   1.173 +    
   1.174 +  in
   1.175 +    (prover,thmstring,goalstring, proverCmd, settings,newfile)	
   1.176 +  end;
   1.177  
   1.178  
   1.179  (* remove \n from end of command and put back into tuple format *)
   1.180 @@ -289,31 +292,19 @@
   1.181  
   1.182  (*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)
   1.183  
   1.184 - fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   1.185 -                         val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"cmdStr")));   
   1.186 -   		val _ = TextIO.output (outfile, (cmdStr))
   1.187 - 		val _ =  TextIO.closeOut outfile
   1.188 -                     in
   1.189 -
   1.190 -                         if (String.isPrefix "\n"  (implode backList )) 
   1.191 -                         then 
   1.192 -                            ( let 
   1.193 -              val newCmdStr = (rev(tl backList))
   1.194 -              val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic"backlist")));   
   1.195 -   		val _ = TextIO.output (outfile, ("about to call sepfields with "^(implode newCmdStr)))
   1.196 - 		val _ =  TextIO.closeOut outfile 
   1.197 -				 val cmdtuple = separateFields newCmdStr
   1.198 -                             in 
   1.199 - 				 formatCmd cmdtuple
   1.200 -			     end)
   1.201 -                         else
   1.202 -                          ( let 
   1.203 -			      val cmdtuple =(separateFields (explode cmdStr))
   1.204 -			   in
   1.205 - 				formatCmd cmdtuple
   1.206 -			   end)
   1.207 -			   
   1.208 -                     end
   1.209 + fun getCmd cmdStr = 
   1.210 +       let val backList = rev(explode cmdStr)
   1.211 +	   val _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr
   1.212 +       in
   1.213 +	   if (String.isPrefix "\n"  (implode backList )) 
   1.214 +	   then 
   1.215 +	       let val newCmdStr = (rev(tl backList))
   1.216 +	       in  File.write (File.tmp_path (Path.basic"backlist")) 
   1.217 +	                      ("about to call sepfields with "^(implode newCmdStr));
   1.218 +		   formatCmd (separateFields newCmdStr)
   1.219 +	       end
   1.220 +	   else formatCmd (separateFields (explode cmdStr))
   1.221 +       end
   1.222                        
   1.223  
   1.224  fun getProofCmd (a,b,c,d,e,f) = d
   1.225 @@ -325,36 +316,29 @@
   1.226  (* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
   1.227  
   1.228  fun getCmds (toParentStr,fromParentStr, cmdList) = 
   1.229 -                                       let val thisLine = TextIO.inputLine fromParentStr 
   1.230 -                                           val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "parent_comms")));                                                                                    
   1.231 -                              val _ = TextIO.output (outfile,(thisLine) )
   1.232 -                              val _ =  TextIO.closeOut outfile
   1.233 -                                       in
   1.234 -                                          (if (thisLine = "End of calls\n") 
   1.235 -                                           then 
   1.236 - 					      
   1.237 -                                              (cmdList)
   1.238 - 					      
   1.239 -                                           else if (thisLine = "Kill children\n") 
   1.240 -                                                then 
   1.241 -                                                    (   TextIO.output (toParentStr,thisLine ); 
   1.242 -                                                        TextIO.flushOut toParentStr;
   1.243 -                                                      (("","","","Kill children",[],"")::cmdList)
   1.244 -                                                     )
   1.245 -                                              else (let val thisCmd = getCmd (thisLine) 
   1.246 -							(*********************************************************)
   1.247 -                                                        (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.248 -						        (* i.e. put back into tuple format                       *)
   1.249 -							(*********************************************************)
   1.250 -                                                    in
   1.251 -                                                      (*TextIO.output (toParentStr, thisCmd); 
   1.252 -                                                        TextIO.flushOut toParentStr;*)
   1.253 -                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   1.254 -                                                    end
   1.255 -                                                    )
   1.256 -                                            )
   1.257 -                                        end
   1.258 -                                    
   1.259 +  let val thisLine = TextIO.inputLine fromParentStr 
   1.260 +      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   1.261 +  in
   1.262 +     if (thisLine = "End of calls\n") 
   1.263 +     then cmdList
   1.264 +     else if (thisLine = "Kill children\n") 
   1.265 +     then 
   1.266 +	 (   TextIO.output (toParentStr,thisLine ); 
   1.267 +	     TextIO.flushOut toParentStr;
   1.268 +	   (("","","","Kill children",[],"")::cmdList)
   1.269 +	  )
   1.270 +     else  let val thisCmd = getCmd (thisLine) 
   1.271 +	       (*********************************************************)
   1.272 +	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.273 +	       (* i.e. put back into tuple format                       *)
   1.274 +	       (*********************************************************)
   1.275 +	   in
   1.276 +	     (*TextIO.output (toParentStr, thisCmd); 
   1.277 +	       TextIO.flushOut toParentStr;*)
   1.278 +	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   1.279 +	   end
   1.280 +  end
   1.281 +	    
   1.282                                                                    
   1.283  (**************************************************************)
   1.284  (*  Get Io-descriptor for polling of an input stream          *)
   1.285 @@ -435,33 +419,30 @@
   1.286  	      (*************************************************************)
   1.287  
   1.288  	      fun pollParentInput () = 
   1.289 -		     
   1.290 -			 let val pd = OS.IO.pollDesc (fromParentIOD)
   1.291 -			 in 
   1.292 -			 if (isSome pd ) then 
   1.293 -			     let val pd' = OS.IO.pollIn (valOf pd)
   1.294 -				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.295 -				 val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   1.296 -			           ("In parent_poll\n")	
   1.297 -			     in
   1.298 -				if null pdl 
   1.299 -				then
   1.300 +		 let val pd = OS.IO.pollDesc (fromParentIOD)
   1.301 +		 in 
   1.302 +		   if (isSome pd ) then 
   1.303 +		       let val pd' = OS.IO.pollIn (valOf pd)
   1.304 +			   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   1.305 +			   val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   1.306 +			     ("In parent_poll\n")	
   1.307 +		       in
   1.308 +			  if null pdl 
   1.309 +			  then
   1.310 +			     NONE
   1.311 +			  else if (OS.IO.isIn (hd pdl)) 
   1.312 +			       then
   1.313 +				  (SOME ( getCmds (toParentStr, fromParentStr, [])))
   1.314 +			       else
   1.315  				   NONE
   1.316 -				else if (OS.IO.isIn (hd pdl)) 
   1.317 -				     then
   1.318 -					(SOME ( getCmds (toParentStr, fromParentStr, [])))
   1.319 -				     else
   1.320 -					 NONE
   1.321 -			     end
   1.322 -			   else
   1.323 -			       NONE
   1.324 -			   end
   1.325 +		       end
   1.326 +		     else
   1.327 +			 NONE
   1.328 +		 end
   1.329  		      
   1.330 -	     
   1.331 -
   1.332  	       fun pollChildInput (fromStr) = 
   1.333 -		     let val iod = getInIoDesc fromStr
   1.334 -		     in 
   1.335 +		 let val iod = getInIoDesc fromStr
   1.336 +		 in 
   1.337  		     if isSome iod 
   1.338  		     then 
   1.339  			 let val pd = OS.IO.pollDesc (valOf iod)
   1.340 @@ -486,7 +467,7 @@
   1.341  			   end
   1.342  		       else 
   1.343  			   NONE
   1.344 -		      end
   1.345 +		 end
   1.346  
   1.347  
   1.348  	     (****************************************************************************)
     2.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jun 20 15:54:39 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jun 20 15:55:44 2005 +0200
     2.3 @@ -146,13 +146,16 @@
     2.4  (* now passing in list of skolemized thms and list of sgterms to go with them *)
     2.5  fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
     2.6     val axfile = (File.platform_path axiom_file)
     2.7 -    val hypsfile = (File.platform_path hyps_file)
     2.8 -     val clasimpfile = (File.platform_path clasimp_file)
     2.9 -    val spass_home = getenv "SPASS_HOME"
    2.10 +   val hypsfile = (File.platform_path hyps_file)
    2.11 +   val clasimpfile = (File.platform_path clasimp_file)
    2.12 +   val spass_home = getenv "SPASS_HOME"
    2.13 +   val spass = spass_home ^ "/SPASS"
    2.14 +   val _ = if File.exists (File.unpack_platform_path spass) then () 
    2.15 +	   else error ("Could not find the file " ^ spass)
    2.16       
    2.17 -fun make_atp_list [] sign n = []
    2.18 -|   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    2.19 -let 
    2.20 +   fun make_atp_list [] sign n = []
    2.21 +   |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    2.22 +   let 
    2.23  	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    2.24  	val thmproofstr = proofstring ( skothmstr)
    2.25  	val no_returns =List.filter   not_newline ( thmproofstr)