src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17718 9dab1e491d10
parent 17690 8ba7c3cd24a8
child 17746 af59c748371d
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 29 12:45:04 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 29 12:45:16 2005 +0200
     1.3 @@ -10,6 +10,11 @@
     1.4  
     1.5  infixr 8 ++; infixr 7 >>; infixr 6 ||;
     1.6  
     1.7 +val trace_path = Path.basic "transfer_trace";
     1.8 +
     1.9 +fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    1.10 +              else ();
    1.11 +
    1.12  
    1.13  (* Versions that include type information *)
    1.14   
    1.15 @@ -175,11 +180,9 @@
    1.16  
    1.17  fun get_axiom_names_spass proofstr clause_arr =
    1.18    let (* parse spass proof into datatype *)
    1.19 -      val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) 
    1.20 -                         ("Started parsing:\n" ^ proofstr)
    1.21 -      val tokens = #1(lex proofstr)
    1.22 -      val proof_steps = parse tokens
    1.23 -      val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
    1.24 +      val _ = trace ("\nStarted parsing:\n" ^ proofstr)
    1.25 +      val proof_steps = parse (#1(lex proofstr))
    1.26 +      val _ = trace "\nParsing finished!"
    1.27        (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    1.28    in
    1.29      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
    1.30 @@ -248,8 +251,8 @@
    1.31       val meta_strs = map ReconOrderClauses.get_meta_lits metas
    1.32      
    1.33       val metas_and_strs = ListPair.zip (metas,meta_strs)
    1.34 -     val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
    1.35 -     val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
    1.36 +     val _ = trace ("\nAxioms: " ^ onestr ax_strs)
    1.37 +     val _ = trace ("\nMeta_strs: " ^ onestr meta_strs)
    1.38  
    1.39       (* get list of axioms as thms with their variables *)
    1.40  
    1.41 @@ -283,25 +286,23 @@
    1.42  
    1.43  
    1.44  fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
    1.45 - let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    1.46 -               ("proofstr is " ^ proofstr ^
    1.47 + let val _ = trace
    1.48 +               ("\nGetting lemma names. proofstr is " ^ proofstr ^
    1.49                  "\ngoalstr is " ^ goalstring ^
    1.50                  "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
    1.51       val axiom_names = getax proofstr clause_arr
    1.52       val ax_str = rules_to_string axiom_names
    1.53      in 
    1.54 -	 File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    1.55 -	            ("\nlemma list is: " ^ ax_str);
    1.56 +	 trace ("\nDone. Lemma list is " ^ ax_str);
    1.57           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    1.58                    ax_str ^ "\n");
    1.59  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.60  	 TextIO.flushOut toParent;
    1.61 -
    1.62  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    1.63      end
    1.64      handle exn => (*FIXME: exn handler is too general!*)
    1.65 -     (File.write(File.tmp_path (Path.basic "proverString_handler")) 
    1.66 -         ("In exception handler: " ^ Toplevel.exn_message exn);
    1.67 +     (trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
    1.68 +             Toplevel.exn_message exn);
    1.69        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    1.70                       remove_linebreaks proofstr ^ "\n");
    1.71        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    1.72 @@ -318,17 +319,13 @@
    1.73  (**** Full proof reconstruction for SPASS (not really working) ****)
    1.74  
    1.75  fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
    1.76 -  let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) 
    1.77 -                 ("proofstr is: "^proofstr)
    1.78 +  let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
    1.79        val tokens = #1(lex proofstr)
    1.80  
    1.81 -  (***********************************)
    1.82    (* parse spass proof into datatype *)
    1.83    (***********************************)
    1.84        val proof_steps = parse tokens
    1.85 -
    1.86 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
    1.87 -                      ("Did parsing on "^proofstr)
    1.88 +      val _ = trace "\nParsing finished"
    1.89      
    1.90    (************************************)
    1.91    (* recreate original subgoal as thm *)
    1.92 @@ -341,17 +338,15 @@
    1.93        val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
    1.94        
    1.95        (*val numcls_string = numclstr ( vars, numcls) ""*)
    1.96 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
    1.97 +      val _ = trace "\ngot axioms"
    1.98  	
    1.99    (************************************)
   1.100    (* translate proof                  *)
   1.101    (************************************)
   1.102 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                           
   1.103 -                       ("about to translate proof, steps: "
   1.104 -                       ^(init_proofsteps_to_string proof_steps ""))
   1.105 +      val _ = trace ("\nabout to translate proof, steps: "
   1.106 +                       ^ (init_proofsteps_to_string proof_steps ""))
   1.107        val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.108 -      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                       
   1.109 -                       ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   1.110 +      val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   1.111    (***************************************************)
   1.112    (* transfer necessary steps as strings to Isabelle *)
   1.113    (***************************************************)
   1.114 @@ -368,9 +363,8 @@
   1.115                         else []
   1.116        val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.117        val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.118 -      val _ = File.write (File.tmp_path (Path.basic "reconstringfile"))
   1.119 -                          (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.120        val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.121 +      val _ = trace ("\nReconstruction:\n" ^ reconstr)
   1.122    in 
   1.123         TextIO.output (toParent, reconstr^"\n");
   1.124         TextIO.output (toParent, goalstring^"\n");
   1.125 @@ -379,8 +373,7 @@
   1.126         all_tac
   1.127    end
   1.128    handle exn => (*FIXME: exn handler is too general!*)
   1.129 -   (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
   1.130 -       ("In exception handler: " ^ Toplevel.exn_message exn);
   1.131 +   (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
   1.132      TextIO.output (toParent,"Translation failed for the proof:"^
   1.133           (remove_linebreaks proofstr) ^"\n");
   1.134      TextIO.output (toParent, goalstring^"\n");
   1.135 @@ -667,7 +660,7 @@
   1.136  		(isar_lines firststeps "")^
   1.137  		(last_isar_line laststep)^
   1.138  		("qed")
   1.139 -	val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof
   1.140 +	val _ = trace ("\nto_isar_proof returns " ^ isar_proof)
   1.141      in
   1.142  	isar_proof
   1.143      end;
   1.144 @@ -684,8 +677,7 @@
   1.145  
   1.146  fun apply_res_thm str goalstring  = 
   1.147    let val tokens = #1 (lex str);
   1.148 -      val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
   1.149 -	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   1.150 +      val _ = trace ("\napply_res_thm. str is: "^str^" goalstr is: "^goalstring^"\n")	
   1.151        val (frees,recon_steps) = parse_step tokens 
   1.152    in 
   1.153        to_isar_proof (frees, recon_steps, goalstring)