src/HOL/Tools/ATP/watcher.ML
changeset 17422 3b237822985d
parent 17317 3f12de2e2e6e
child 17435 0eed5a1c00c1
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 15 17:45:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 15 17:46:00 2005 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  (*****************************************************************************************)
     1.5  
     1.6  val callResProvers :
     1.7 -    TextIO.outstream * (string*string*string*string*string*string*string*string) list 
     1.8 +    TextIO.outstream * (string*string*string*string*string) list 
     1.9      -> unit
    1.10  
    1.11  (************************************************************************)
    1.12 @@ -73,7 +73,6 @@
    1.13  datatype cmdproc = CMDPROC of {
    1.14          prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    1.15          cmd:  string,              (* The file containing the goal for res prover to prove *)     
    1.16 -        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    1.17          goalstring: string,         (* string representation of subgoal*) 
    1.18          proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    1.19          instr : TextIO.instream,   (*  Input stream to child process *)
    1.20 @@ -123,19 +122,16 @@
    1.21  
    1.22  fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    1.23  
    1.24 -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = 
    1.25 +fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
    1.26    (prover,(cmd, (instr,outstr)));
    1.27  
    1.28 -fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    1.29 +fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
    1.30    proc_handle;
    1.31  
    1.32 -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    1.33 +fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    1.34    prover;
    1.35  
    1.36 -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = 
    1.37 -  thmstring;
    1.38 -
    1.39 -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  =
    1.40 +fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    1.41    goalstring;
    1.42  
    1.43  
    1.44 @@ -166,14 +162,14 @@
    1.45  fun callResProvers (toWatcherStr,  []) = 
    1.46        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    1.47  |   callResProvers (toWatcherStr,
    1.48 -                    (prover,thmstring,goalstring, proverCmd,settings, 
    1.49 -                     axfile, hypsfile,probfile)  ::  args) =
    1.50 +                    (prover,goalstring, proverCmd,settings, 
    1.51 +                     probfile)  ::  args) =
    1.52        let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
    1.53 -                             (prover^thmstring^goalstring^proverCmd^settings^
    1.54 -                              hypsfile^probfile)
    1.55 +                             (prover^goalstring^proverCmd^settings^
    1.56 +                              probfile)
    1.57        in TextIO.output (toWatcherStr,    
    1.58 -            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
    1.59 -             settings^"$"^hypsfile^"$"^probfile^"\n"));
    1.60 +            (prover^"$"^goalstring^"$"^proverCmd^"$"^
    1.61 +             settings^"$"^probfile^"\n"));
    1.62           goals_being_watched := (!goals_being_watched) + 1;
    1.63  	 TextIO.flushOut toWatcherStr;
    1.64  	 callResProvers (toWatcherStr,args)
    1.65 @@ -198,68 +194,52 @@
    1.66  fun separateFields str =
    1.67    let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
    1.68                            ("In separateFields, str is: " ^ str ^ "\n\n") 
    1.69 -      val [prover,thmstring,goalstring,proverCmd,settingstr,hypsfile,probfile] = 
    1.70 +      val [prover,goalstring,proverCmd,settingstr,probfile] = 
    1.71            String.tokens (fn c => c = #"$") str
    1.72        val settings = String.tokens (fn c => c = #"%") settingstr
    1.73        val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
    1.74                    ("Sep comms are: "^ str ^"**"^
    1.75 -                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^
    1.76 -                   " \n provercmd: "^proverCmd^
    1.77 -                   " \n hyps "^hypsfile^"\n prob  "^probfile^"\n\n")
    1.78 +                   prover^" goalstr:  "^goalstring^
    1.79 +                   "\n provercmd: "^proverCmd^
    1.80 +                   "\n prob  "^probfile^"\n\n")
    1.81    in
    1.82 -     (prover,thmstring,goalstring, proverCmd, settings, hypsfile, probfile)
    1.83 +     (prover,goalstring, proverCmd, settings, probfile)
    1.84    end
    1.85  
    1.86 -                      
    1.87 -fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, hypsfile ,probfile) = 
    1.88 -  let
    1.89 -    val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.90 -	       (thmstring ^ "\n goals_watched" ^ 
    1.91 -	       (string_of_int(!goals_being_watched)) ^ probfile^"\n")
    1.92 -  in
    1.93 -    (prover, thmstring, goalstring, proverCmd, settings, probfile)	
    1.94 -  end;
    1.95 -
    1.96  val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    1.97  
    1.98  fun getCmd cmdStr = 
    1.99    let val cmdStr' = remove_newlines cmdStr
   1.100    in
   1.101        File.write (File.tmp_path (Path.basic"sepfields_call")) 
   1.102 -		 ("about to call sepfields with " ^ cmdStr');
   1.103 -      formatCmd (separateFields cmdStr')
   1.104 +		 ("about to call separateFields with " ^ cmdStr');
   1.105 +      separateFields cmdStr'
   1.106    end;
   1.107                        
   1.108 -
   1.109 -fun getProofCmd (a,b,c,d,e,f) = d
   1.110 -
   1.111 -                        
   1.112  (**************************************************************)
   1.113  (* Get commands from Isabelle                                 *)
   1.114  (**************************************************************)
   1.115 -(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
   1.116  
   1.117  fun getCmds (toParentStr,fromParentStr, cmdList) = 
   1.118    let val thisLine = TextIO.inputLine fromParentStr 
   1.119        val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
   1.120    in
   1.121 -     if (thisLine = "End of calls\n") 
   1.122 -     then cmdList
   1.123 -     else if (thisLine = "Kill children\n") 
   1.124 +     if thisLine = "End of calls\n" then cmdList
   1.125 +     else if thisLine = "Kill children\n"
   1.126       then 
   1.127  	 (   TextIO.output (toParentStr,thisLine ); 
   1.128  	     TextIO.flushOut toParentStr;
   1.129 -	   (("","","","Kill children",[],"")::cmdList)
   1.130 +	   (("","","Kill children",[],"")::cmdList)
   1.131  	  )
   1.132 -     else  let val thisCmd = getCmd thisLine 
   1.133 +     else let val thisCmd = getCmd thisLine 
   1.134  	       (*********************************************************)
   1.135 -	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.136 +	       (* thisCmd = (prover,proverCmd, settings, file)*)
   1.137  	       (* i.e. put back into tuple format                       *)
   1.138  	       (*********************************************************)
   1.139  	   in
   1.140  	     (*TextIO.output (toParentStr, thisCmd); 
   1.141  	       TextIO.flushOut toParentStr;*)
   1.142 -	       getCmds (toParentStr, fromParentStr, (thisCmd::cmdList))
   1.143 +	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
   1.144  	   end
   1.145    end
   1.146  	    
   1.147 @@ -286,6 +266,8 @@
   1.148  (*  Set up a Watcher Process         *)
   1.149  (*************************************)
   1.150  
   1.151 +fun getProofCmd (a,c,d,e,f) = d
   1.152 +
   1.153  fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   1.154    let
   1.155      (** pipes for communication between parent and watcher **)
   1.156 @@ -405,25 +387,24 @@
   1.157  			      ("finished polling child \n")
   1.158  		   val parentID = Posix.ProcEnv.getppid()
   1.159  		   val prover = cmdProver childProc
   1.160 -		   val thmstring = cmdThm childProc
   1.161  		   val sign = sign_of_thm thm
   1.162  		   val prems = prems_of thm
   1.163  		   val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.164  		   val _ = debug("subgoals forked to checkChildren: "^prems_string)
   1.165  		   val goalstring = cmdGoal childProc							
   1.166  		   val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   1.167 -			      (prover^thmstring^goalstring^childCmd^"\n")
   1.168 +			      (prover^goalstring^childCmd^"\n")
   1.169  	       in 
   1.170  		 if isSome childIncoming
   1.171  		 then 
   1.172  		   (* check here for prover label on child*)
   1.173  		   let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) 
   1.174  			      ("subgoals forked to checkChildren:"^
   1.175 -			      prems_string^prover^thmstring^goalstring^childCmd) 
   1.176 +			      prems_string^prover^goalstring^childCmd) 
   1.177  		       val childDone = (case prover of
   1.178 -			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   1.179 -			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   1.180 -			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   1.181 +			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
   1.182 +			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
   1.183 +			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
   1.184  		    in
   1.185  		     if childDone      (**********************************************)
   1.186  		     then (* child has found a proof and transferred it *)
   1.187 @@ -453,7 +434,7 @@
   1.188  
   1.189  (*** add subgoal id num to this *)
   1.190  	fun execCmds  [] procList = procList
   1.191 -	|   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =
   1.192 +	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   1.193  	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
   1.194  	                    (space_implode "\n" 
   1.195  	                      (["About to execute command for goal:",
   1.196 @@ -466,7 +447,6 @@
   1.197  		  val newProcList = (CMDPROC{
   1.198  				       prover = prover,
   1.199  				       cmd = file,
   1.200 -				       thmstring = thmstring,
   1.201  				       goalstring = goalstring,
   1.202  				       proc_handle = childhandle,
   1.203  				       instr = instr,
   1.204 @@ -488,11 +468,11 @@
   1.205       (****************************************)
   1.206  
   1.207        (*  fun execRemoteCmds  [] procList = procList
   1.208 -	|   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.209 -				  let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.210 -				      in
   1.211 -					   execRemoteCmds  cmds newProcList
   1.212 -				      end
   1.213 +	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   1.214 +	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   1.215 +		  in
   1.216 +		       execRemoteCmds  cmds newProcList
   1.217 +		  end
   1.218  *)
   1.219  
   1.220       (**********************************************)                  
   1.221 @@ -648,11 +628,11 @@
   1.222  	(Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.223  	 VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361")))               
   1.224       fun spass_proofHandler n = (
   1.225 -       let val _ = File.append (File.tmp_path (Path.basic "spass_signal_in"))
   1.226 +       let val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   1.227                                 "Starting SPASS signal handler\n"
   1.228 -	   val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
   1.229 -	   val _ = File.append (File.tmp_path (Path.basic "spass_signal_out"))
   1.230 -		       ("In SPASS signal handler "^reconstr^thmstring^goalstring^
   1.231 +	   val (reconstr, goalstring) = SpassComm.getSpassInput childin
   1.232 +	   val _ = File.append (File.tmp_path (Path.basic "spass_signal"))
   1.233 +		       ("In SPASS signal handler "^reconstr^goalstring^
   1.234  		       "goals_being_watched: "^ string_of_int (!goals_being_watched))
   1.235         in (* if a proof has been found and sent back as a reconstruction proof *)
   1.236  	 if substring (reconstr, 0,1) = "["