src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17772 818cec5f82a4
parent 17746 af59c748371d
child 17775 2679ba74411f
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 06 10:13:34 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 06 10:14:22 2005 +0200
     1.3 @@ -280,18 +280,19 @@
     1.4    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
     1.5  
     1.6  
     1.7 -fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
     1.8 +(*The signal handler in watcher.ML must be able to read the output of this.*)
     1.9 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
    1.10   let val _ = trace
    1.11                 ("\nGetting lemma names. proofstr is " ^ proofstr ^
    1.12 -                "\ngoalstring is " ^ goalstring ^
    1.13 -                "num of clauses is " ^ string_of_int (Array.length clause_arr))
    1.14 +                "\nprobfile is " ^ probfile ^
    1.15 +                "  num of clauses is " ^ string_of_int (Array.length clause_arr))
    1.16       val axiom_names = getax proofstr clause_arr
    1.17       val ax_str = rules_to_string axiom_names
    1.18      in 
    1.19  	 trace ("\nDone. Lemma list is " ^ ax_str);
    1.20           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    1.21                    ax_str ^ "\n");
    1.22 -	 TextIO.output (toParent, goalstring);
    1.23 +	 TextIO.output (toParent, probfile ^ "\n");
    1.24  	 TextIO.flushOut toParent;
    1.25  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    1.26      end
    1.27 @@ -300,7 +301,7 @@
    1.28               Toplevel.exn_message exn);
    1.29        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    1.30                       String.toString proofstr ^ "\n");
    1.31 -      TextIO.output (toParent, goalstring);
    1.32 +      TextIO.output (toParent, probfile);
    1.33        TextIO.flushOut toParent;
    1.34        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.35  
    1.36 @@ -313,7 +314,7 @@
    1.37  
    1.38  (**** Full proof reconstruction for SPASS (not really working) ****)
    1.39  
    1.40 -fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
    1.41 +fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = 
    1.42    let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
    1.43        val tokens = #1(lex proofstr)
    1.44  
    1.45 @@ -362,16 +363,16 @@
    1.46        val _ = trace ("\nReconstruction:\n" ^ reconstr)
    1.47    in 
    1.48         TextIO.output (toParent, reconstr^"\n");
    1.49 -       TextIO.output (toParent, goalstring);
    1.50 +       TextIO.output (toParent, probfile ^ "\n");
    1.51         TextIO.flushOut toParent;
    1.52         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.53         all_tac
    1.54    end
    1.55    handle exn => (*FIXME: exn handler is too general!*)
    1.56     (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
    1.57 -    TextIO.output (toParent,"Translation failed for the proof:"^
    1.58 +    TextIO.output (toParent,"Translation failed for SPASS proof:"^
    1.59           String.toString proofstr ^"\n");
    1.60 -    TextIO.output (toParent, goalstring);
    1.61 +    TextIO.output (toParent, probfile ^ "\n");
    1.62      TextIO.flushOut toParent;
    1.63      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    1.64  
    1.65 @@ -484,19 +485,6 @@
    1.66                          >>(fn (_,(a,_)) => a)
    1.67                       
    1.68  
    1.69 -
    1.70 -
    1.71 -fun anytoken_step input  = (word>> (fn (a) => a)  ) input
    1.72 -                       handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a)  ) input
    1.73 -                      handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
    1.74 -
    1.75 -
    1.76 -
    1.77 -fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
    1.78 -                  >> (fn (a,b) =>  (a^" "^(implode b)))) input
    1.79 -
    1.80 -
    1.81 -
    1.82   val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
    1.83                  >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
    1.84      
    1.85 @@ -630,7 +618,7 @@
    1.86  fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
    1.87  
    1.88  
    1.89 -fun to_isar_proof (frees, xs, goalstring) =
    1.90 +fun to_isar_proof (frees, xs) =
    1.91      let val extraaxioms = get_extraaxioms xs
    1.92  	val extraax_num = length extraaxioms
    1.93  	val origaxioms_and_steps = Library.drop (extraax_num, xs)  
    1.94 @@ -643,10 +631,9 @@
    1.95  	val steps = Library.drop (origax_num, axioms_and_steps)
    1.96  	val firststeps = ReconOrderClauses.butlast steps
    1.97  	val laststep = List.last steps
    1.98 -	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
    1.99  	
   1.100  	val isar_proof = 
   1.101 -		("show \""^goalstring^"\"\n")^
   1.102 +		("show \"[your goal]\"\n")^
   1.103  		("proof (rule ccontr,skolemize, make_clauses) \n")^
   1.104  		("fix "^(frees_to_isar_str frees)^"\n")^
   1.105  		(assume_isar_extraaxioms extraaxioms)^
   1.106 @@ -670,13 +657,12 @@
   1.107  (* be passed over to the watcher, e.g.  numcls25       *)
   1.108  (*******************************************************)
   1.109  
   1.110 -fun apply_res_thm str goalstring  = 
   1.111 +fun apply_res_thm str  = 
   1.112    let val tokens = #1 (lex str);
   1.113 -      val _ = trace ("\napply_res_thm. str is: "^str^
   1.114 -                     "\ngoalstring is: \n"^goalstring^"\n")	
   1.115 +      val _ = trace ("\napply_res_thm. str is: "^str^"\n")	
   1.116        val (frees,recon_steps) = parse_step tokens 
   1.117    in 
   1.118 -      to_isar_proof (frees, recon_steps, goalstring)
   1.119 +      to_isar_proof (frees, recon_steps)
   1.120    end 
   1.121  
   1.122  end;