fixed the ascii-armouring of goalstring
authorpaulson
Tue Oct 04 09:59:01 2005 +0200 (2005-10-04)
changeset 17746af59c748371d
parent 17745 38b4d8bf2627
child 17747 1ce1f62768bd
fixed the ascii-armouring of goalstring
src/HOL/Tools/ATP/AtpCommunication.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/AtpCommunication.ML	Tue Oct 04 09:58:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Tue Oct 04 09:59:01 2005 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  
     1.5  fun signal_parent (toParent, ppid, msg, goalstring) =
     1.6   (TextIO.output (toParent, msg);
     1.7 -  TextIO.output (toParent, goalstring^"\n");
     1.8 +  TextIO.output (toParent, goalstring);
     1.9    TextIO.flushOut toParent;
    1.10    trace ("\nSignalled parent: " ^ msg);
    1.11    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Oct 04 09:58:38 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Oct 04 09:59:01 2005 +0200
     2.3 @@ -279,24 +279,19 @@
     2.4  fun rules_to_string [] = "NONE"
     2.5    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
     2.6  
     2.7 -fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
     2.8 -
     2.9 -val remove_linebreaks = subst_for #"\n" #"\t";
    2.10 -val restore_linebreaks = subst_for #"\t" #"\n";
    2.11 -
    2.12  
    2.13  fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
    2.14   let val _ = trace
    2.15                 ("\nGetting lemma names. proofstr is " ^ proofstr ^
    2.16 -                "\ngoalstr is " ^ goalstring ^
    2.17 -                "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
    2.18 +                "\ngoalstring is " ^ goalstring ^
    2.19 +                "num of clauses is " ^ string_of_int (Array.length clause_arr))
    2.20       val axiom_names = getax proofstr clause_arr
    2.21       val ax_str = rules_to_string axiom_names
    2.22      in 
    2.23  	 trace ("\nDone. Lemma list is " ^ ax_str);
    2.24           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    2.25                    ax_str ^ "\n");
    2.26 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    2.27 +	 TextIO.output (toParent, goalstring);
    2.28  	 TextIO.flushOut toParent;
    2.29  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    2.30      end
    2.31 @@ -304,8 +299,8 @@
    2.32       (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
    2.33               Toplevel.exn_message exn);
    2.34        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    2.35 -                     remove_linebreaks proofstr ^ "\n");
    2.36 -      TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    2.37 +                     String.toString proofstr ^ "\n");
    2.38 +      TextIO.output (toParent, goalstring);
    2.39        TextIO.flushOut toParent;
    2.40        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    2.41  
    2.42 @@ -367,7 +362,7 @@
    2.43        val _ = trace ("\nReconstruction:\n" ^ reconstr)
    2.44    in 
    2.45         TextIO.output (toParent, reconstr^"\n");
    2.46 -       TextIO.output (toParent, goalstring^"\n");
    2.47 +       TextIO.output (toParent, goalstring);
    2.48         TextIO.flushOut toParent;
    2.49         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.50         all_tac
    2.51 @@ -375,8 +370,8 @@
    2.52    handle exn => (*FIXME: exn handler is too general!*)
    2.53     (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
    2.54      TextIO.output (toParent,"Translation failed for the proof:"^
    2.55 -         (remove_linebreaks proofstr) ^"\n");
    2.56 -    TextIO.output (toParent, goalstring^"\n");
    2.57 +         String.toString proofstr ^"\n");
    2.58 +    TextIO.output (toParent, goalstring);
    2.59      TextIO.flushOut toParent;
    2.60      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    2.61  
    2.62 @@ -677,7 +672,8 @@
    2.63  
    2.64  fun apply_res_thm str goalstring  = 
    2.65    let val tokens = #1 (lex str);
    2.66 -      val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")	
    2.67 +      val _ = trace ("\napply_res_thm. str is: "^str^
    2.68 +                     "\ngoalstring is: \n"^goalstring^"\n")	
    2.69        val (frees,recon_steps) = parse_step tokens 
    2.70    in 
    2.71        to_isar_proof (frees, recon_steps, goalstring)
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Oct 04 09:58:38 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue Oct 04 09:59:01 2005 +0200
     3.3 @@ -145,8 +145,9 @@
     3.4  		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
     3.5  			  probfile]))
     3.6        in TextIO.output (toWatcherStr,    
     3.7 -            (prover^"$"^goalstring^"$"^proverCmd^"$"^
     3.8 -             settings^"$"^probfile^"\n"));
     3.9 +                        prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
    3.10 +         TextIO.output (toWatcherStr, String.toString goalstring^"\n");
    3.11 +              (*goalstring is a single string literal, with all specials escaped.*)
    3.12           goals_being_watched := (!goals_being_watched) + 1;
    3.13  	 TextIO.flushOut toWatcherStr;
    3.14  	 callResProvers (toWatcherStr,args)
    3.15 @@ -161,24 +162,7 @@
    3.16  fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
    3.17                              TextIO.flushOut toWatcherStr)
    3.18  
    3.19 -
    3.20 -(**************************************************************)
    3.21 -(* Remove \n token from a vampire goal filename and extract   *)
    3.22 -(* prover, proverCmd, settings and file from input string     *)
    3.23 -(**************************************************************)
    3.24 -
    3.25 -val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
    3.26 -
    3.27 -fun getCmd cmdStr = 
    3.28 -  let val [prover,goalstring,proverCmd,settingstr,probfile] = 
    3.29 -            String.tokens (fn c => c = #"$") (remove_newlines cmdStr)
    3.30 -      val settings = String.tokens (fn c => c = #"%") settingstr
    3.31 -      val _ = trace ("getCmd: " ^ cmdStr ^
    3.32 -		    "\nprover" ^ prover ^ " goalstr:  "^goalstring^
    3.33 -		    "\nprovercmd: " ^ proverCmd^
    3.34 -		    "\nprob  " ^ probfile ^ "\n\n")
    3.35 -  in (prover,goalstring, proverCmd, settings, probfile) end
    3.36 -                      
    3.37 +                    
    3.38  (**************************************************************)
    3.39  (* Get commands from Isabelle                                 *)
    3.40  (**************************************************************)
    3.41 @@ -191,8 +175,18 @@
    3.42       then (TextIO.output (toParentStr,thisLine ); 
    3.43  	   TextIO.flushOut toParentStr;
    3.44  	   (("","","Kill children",[],"")::cmdList)  )
    3.45 -     else let val thisCmd = getCmd thisLine 
    3.46 -	   in getCmds (toParentStr, fromParentStr, thisCmd::cmdList) end
    3.47 +     else
    3.48 +       let val [prover,proverCmd,settingstr,probfile,_] = 
    3.49 +                   String.tokens (fn c => c = #"$") thisLine
    3.50 +           val settings = String.tokens (fn c => c = #"%") settingstr
    3.51 +	   val goalstring = TextIO.inputLine fromParentStr 
    3.52 +       in
    3.53 +           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
    3.54 +                  "  problem file: " ^ probfile ^ 
    3.55 +		  "\ngoalstring:  "^goalstring);
    3.56 +           getCmds (toParentStr, fromParentStr, 
    3.57 +                    (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
    3.58 +       end
    3.59    end
    3.60  	    
    3.61                                                                    
    3.62 @@ -317,7 +311,7 @@
    3.63  		   (* check here for prover label on child*)
    3.64  		   let val _ = trace ("\nInput available from child: " ^
    3.65  				      childCmd ^ 
    3.66 -				      "\ngoalstring is " ^ goalstring ^ "\n\n")
    3.67 +				      "\ngoalstring is " ^ goalstring)
    3.68  		       val childDone = (case prover of
    3.69  			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
    3.70  			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
    3.71 @@ -530,7 +524,7 @@
    3.72       val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
    3.73       fun proofHandler n = 
    3.74         let val outcome = TextIO.inputLine childin
    3.75 -	   val goalstring = TextIO.inputLine childin
    3.76 +	   val goalstring = valOf (String.fromString (TextIO.inputLine childin))
    3.77  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
    3.78  		        "\"\ngoalstring = " ^ goalstring ^
    3.79  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
    3.80 @@ -539,18 +533,18 @@
    3.81  	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
    3.82  	       decr_watched())
    3.83  	 else if String.isPrefix "Invalid" outcome
    3.84 -	 then (priority (goalstring ^ "is not provable");
    3.85 +	 then (priority ("Subgoal is not provable:\n" ^ goalstring);
    3.86  	       decr_watched())
    3.87  	 else if String.isPrefix "Failure" outcome
    3.88 -	 then (priority (goalstring ^ "proof attempt failed");
    3.89 +	 then (priority ("Proof attempt failed:\n" ^ goalstring);
    3.90  	       decr_watched()) 
    3.91  	(* print out a list of rules used from clasimpset*)
    3.92  	 else if String.isPrefix "Success" outcome
    3.93 -	 then (priority (goalstring^outcome);
    3.94 +	 then (priority (outcome ^ goalstring);
    3.95  	       decr_watched())
    3.96  	  (* if proof translation failed *)
    3.97  	 else if String.isPrefix "Translation failed" outcome
    3.98 -	 then (priority (goalstring ^ outcome);
    3.99 +	 then (priority (outcome ^ goalstring);
   3.100  	       decr_watched())
   3.101  	 else (priority "System error in proof handler";
   3.102  	       decr_watched())
     4.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 04 09:58:38 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 04 09:59:01 2005 +0200
     4.3 @@ -38,18 +38,6 @@
     4.4  fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
     4.5  
     4.6  
     4.7 -(**** for Isabelle/ML interface  ****)
     4.8 -
     4.9 -(*Remove unwanted characters such as ? and newline from the textural 
    4.10 -  representation of a theorem (surely they don't need to be produced in 
    4.11 -  the first place?) *)
    4.12 -
    4.13 -fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
    4.14 -
    4.15 -val proofstring =
    4.16 -    String.translate (fn c => if is_proof_char c then str c else "");
    4.17 -
    4.18 -
    4.19  (**** For running in Isar ****)
    4.20  
    4.21  (* same function as that in res_axioms.ML *)
    4.22 @@ -99,7 +87,7 @@
    4.23      fun make_atp_list [] n = []
    4.24        | make_atp_list (sg_term::xs) n =
    4.25            let
    4.26 -            val goalstring = proofstring (Sign.string_of_term sign sg_term)
    4.27 +            val goalstring = Sign.string_of_term sign sg_term
    4.28              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    4.29              val probfile = prob_pathname n
    4.30              val time = Int.toString (!time_limit)
    4.31 @@ -235,7 +223,7 @@
    4.32    end);
    4.33  
    4.34  val call_atpP =
    4.35 -  OuterSyntax.improper_command 
    4.36 +  OuterSyntax.command 
    4.37      "ProofGeneral.call_atp" 
    4.38      "call automatic theorem provers" 
    4.39      OuterKeyword.diag