src/HOL/Tools/ATP/watcher.ML
changeset 17746 af59c748371d
parent 17716 89932e53f31d
child 17764 fde495b9e24b
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Oct 04 09:58:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Oct 04 09:59:01 2005 +0200
     1.3 @@ -145,8 +145,9 @@
     1.4  		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
     1.5  			  probfile]))
     1.6        in TextIO.output (toWatcherStr,    
     1.7 -            (prover^"$"^goalstring^"$"^proverCmd^"$"^
     1.8 -             settings^"$"^probfile^"\n"));
     1.9 +                        prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
    1.10 +         TextIO.output (toWatcherStr, String.toString goalstring^"\n");
    1.11 +              (*goalstring is a single string literal, with all specials escaped.*)
    1.12           goals_being_watched := (!goals_being_watched) + 1;
    1.13  	 TextIO.flushOut toWatcherStr;
    1.14  	 callResProvers (toWatcherStr,args)
    1.15 @@ -161,24 +162,7 @@
    1.16  fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
    1.17                              TextIO.flushOut toWatcherStr)
    1.18  
    1.19 -
    1.20 -(**************************************************************)
    1.21 -(* Remove \n token from a vampire goal filename and extract   *)
    1.22 -(* prover, proverCmd, settings and file from input string     *)
    1.23 -(**************************************************************)
    1.24 -
    1.25 -val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    1.26 -
    1.27 -fun getCmd cmdStr = 
    1.28 -  let val [prover,goalstring,proverCmd,settingstr,probfile] = 
    1.29 -            String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
    1.30 -      val settings = String.tokens (fn c => c = #"%") settingstr
    1.31 -      val _ = trace ("getCmd: " ^ cmdStr ^
    1.32 -		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
    1.33 -		    "\nprovercmd: " ^ proverCmd^
    1.34 -		    "\nprob  " ^ probfile ^ "\n\n")
    1.35 -  in (prover,goalstring, proverCmd, settings, probfile) end
    1.36 -                      
    1.37 +                    
    1.38  (**************************************************************)
    1.39  (* Get commands from Isabelle                                 *)
    1.40  (**************************************************************)
    1.41 @@ -191,8 +175,18 @@
    1.42       then (TextIO.output (toParentStr,thisLine ); 
    1.43  	   TextIO.flushOut toParentStr;
    1.44  	   (("","","Kill children",[],"")::cmdList)  )
    1.45 -     else let val thisCmd = getCmd thisLine 
    1.46 -	   in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
    1.47 +     else
    1.48 +       let val [prover,proverCmd,settingstr,probfile,_] = 
    1.49 +                   String.tokens (fn c => c = #"$") thisLine
    1.50 +           val settings = String.tokens (fn c => c = #"%") settingstr
    1.51 +	   val goalstring = TextIO.inputLine fromParentStr 
    1.52 +       in
    1.53 +           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
    1.54 +                  "  problem file: " ^ probfile ^ 
    1.55 +		  "\ngoalstring:  "^goalstring);
    1.56 +           getCmds (toParentStr, fromParentStr, 
    1.57 +                    (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
    1.58 +       end
    1.59    end
    1.60  	    
    1.61                                                                    
    1.62 @@ -317,7 +311,7 @@
    1.63  		   (* check here for prover label on child*)
    1.64  		   let val _ = trace ("\nInput available from child: " ^
    1.65  				      childCmd ^ 
    1.66 -				      "\ngoalstring is " ^ goalstring ^ "\n\n")
    1.67 +				      "\ngoalstring is " ^ goalstring)
    1.68  		       val childDone = (case prover of
    1.69  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
    1.70  			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
    1.71 @@ -530,7 +524,7 @@
    1.72       val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
    1.73       fun proofHandler n = 
    1.74         let val outcome = TextIO.inputLine childin
    1.75 -	   val goalstring = TextIO.inputLine childin
    1.76 +	   val goalstring = valOf (String.fromString (TextIO.inputLine childin))
    1.77  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
    1.78  		        "\"\ngoalstring = " ^ goalstring ^
    1.79  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
    1.80 @@ -539,18 +533,18 @@
    1.81  	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
    1.82  	       decr_watched())
    1.83  	 else if String.isPrefix "Invalid" outcome
    1.84 -	 then (priority (goalstring ^ "is not provable");
    1.85 +	 then (priority ("Subgoal is not provable:\n" ^ goalstring);
    1.86  	       decr_watched())
    1.87  	 else if String.isPrefix "Failure" outcome
    1.88 -	 then (priority (goalstring ^ "proof attempt failed");
    1.89 +	 then (priority ("Proof attempt failed:\n" ^ goalstring);
    1.90  	       decr_watched()) 
    1.91  	(* print out a list of rules used from clasimpset*)
    1.92  	 else if String.isPrefix "Success" outcome
    1.93 -	 then (priority (goalstring^outcome);
    1.94 +	 then (priority (outcome ^ goalstring);
    1.95  	       decr_watched())
    1.96  	  (* if proof translation failed *)
    1.97  	 else if String.isPrefix "Translation failed" outcome
    1.98 -	 then (priority (goalstring ^ outcome);
    1.99 +	 then (priority (outcome ^ goalstring);
   1.100  	       decr_watched())
   1.101  	 else (priority "System error in proof handler";
   1.102  	       decr_watched())