src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17422 3b237822985d
parent 17317 3f12de2e2e6e
child 17484 f6a225f97f0a
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 15 17:45:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 15 17:46:00 2005 +0200
     1.3 @@ -134,9 +134,6 @@
     1.4  (*Flattens a list of list of strings to one string*)
     1.5  fun onestr ls = String.concat (map String.concat ls);
     1.6  
     1.7 -fun thmstrings [] str = str
     1.8 -|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
     1.9 -
    1.10  fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
    1.11  
    1.12  fun subone x = x - 1
    1.13 @@ -268,10 +265,9 @@
    1.14  val restore_linebreaks = subst_for #"\t" #"\n";
    1.15  
    1.16  
    1.17 -fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax = 
    1.18 - let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
    1.19 -               ("thmstring is " ^ thmstring ^ 
    1.20 -                "\nproofstr is " ^ proofstr ^
    1.21 +fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax = 
    1.22 + let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring"))
    1.23 +               ("proofstr is " ^ proofstr ^
    1.24                  "\ngoalstr is " ^ goalstring ^
    1.25                  "\nnum of clauses is " ^ string_of_int num_of_clauses)
    1.26  
    1.27 @@ -279,11 +275,10 @@
    1.28       val ax_str = "Rules from clasimpset used in automatic proof: " ^
    1.29                    rules_to_string axiom_names
    1.30      in 
    1.31 -	 File.append(File.tmp_path (Path.basic "reconstrfile"))
    1.32 +	 File.append(File.tmp_path (Path.basic "spass_lemmastring"))
    1.33  	            ("reconstring is: "^ax_str^"  "^goalstring);
    1.34           TextIO.output (toParent, ax_str^"\n");
    1.35  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.36 -	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    1.37  	 TextIO.flushOut toParent;
    1.38  
    1.39  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.40 @@ -294,29 +289,28 @@
    1.41       (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
    1.42        TextIO.output (toParent, "Proof found but translation failed : " ^ 
    1.43                       remove_linebreaks proofstr ^ "\n");
    1.44 -      TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
    1.45        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
    1.46        TextIO.flushOut toParent;
    1.47        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.48        (* Attempt to prevent several signals from turning up simultaneously *)
    1.49        Posix.Process.sleep(Time.fromSeconds 1); all_tac);
    1.50  
    1.51 -fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
    1.52 +fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
    1.53        clause_arr num_of_clauses  = 
    1.54 -  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
    1.55 +  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
    1.56         clause_arr num_of_clauses get_axiom_names_vamp_E;
    1.57  
    1.58 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
    1.59 +fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
    1.60        clause_arr  num_of_clauses  = 
    1.61 -  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
    1.62 +  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
    1.63         clause_arr num_of_clauses get_axiom_names_spass;
    1.64  
    1.65  
    1.66  (**** Full proof reconstruction for SPASS (not really working) ****)
    1.67  
    1.68 -fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.69 -  let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
    1.70 -                 (" thmstring is: "^thmstring^"proofstr is: "^proofstr)
    1.71 +fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.72 +  let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction")) 
    1.73 +                 ("proofstr is: "^proofstr)
    1.74        val tokens = #1(lex proofstr)
    1.75  
    1.76    (***********************************)
    1.77 @@ -324,11 +318,9 @@
    1.78    (***********************************)
    1.79        val proof_steps = parse tokens
    1.80  
    1.81 -      val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
    1.82 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
    1.83                        ("Did parsing on "^proofstr)
    1.84      
    1.85 -      val _ = File.write (File.tmp_path (Path.basic "foo_thmstring_at_parse"))
    1.86 -                                ("Parsing for thmstring: "^thmstring)
    1.87    (************************************)
    1.88    (* recreate original subgoal as thm *)
    1.89    (************************************)
    1.90 @@ -340,16 +332,16 @@
    1.91        val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
    1.92        
    1.93        (*val numcls_string = numclstr ( vars, numcls) ""*)
    1.94 -      val _ = File.write (File.tmp_path (Path.basic "foo_axiom")) "got axioms"
    1.95 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
    1.96  	
    1.97    (************************************)
    1.98    (* translate proof                  *)
    1.99    (************************************)
   1.100 -      val _ = File.write (File.tmp_path (Path.basic "foo_steps"))                                                                           
   1.101 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                           
   1.102                         ("about to translate proof, steps: "
   1.103                         ^(init_proofsteps_to_string proof_steps ""))
   1.104        val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.105 -      val _ = File.write (File.tmp_path (Path.basic "foo_steps2"))                                                                       
   1.106 +      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                       
   1.107                         ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   1.108    (***************************************************)
   1.109    (* transfer necessary steps as strings to Isabelle *)
   1.110 @@ -372,9 +364,6 @@
   1.111        val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.112    in 
   1.113         TextIO.output (toParent, reconstr^"\n");
   1.114 -       TextIO.flushOut toParent;
   1.115 -       TextIO.output (toParent, thmstring^"\n");
   1.116 -       TextIO.flushOut toParent;
   1.117         TextIO.output (toParent, goalstring^"\n");
   1.118         TextIO.flushOut toParent;
   1.119  
   1.120 @@ -383,19 +372,14 @@
   1.121         Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.122    end
   1.123    handle _ => 
   1.124 -  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.125 -  in 
   1.126 -       TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   1.127 -      TextIO.flushOut toParent;
   1.128 -    TextIO.output (toParent, thmstring^"\n");
   1.129 -       TextIO.flushOut toParent;
   1.130 -       TextIO.output (toParent, goalstring^"\n");
   1.131 -       TextIO.flushOut toParent;
   1.132 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.133 -      (* Attempt to prevent several signals from turning up simultaneously *)
   1.134 -      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.135 -  end
   1.136 -
   1.137 +   (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
   1.138 +    TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
   1.139 +         (remove_linebreaks proofstr) ^"\n");
   1.140 +    TextIO.output (toParent, goalstring^"\n");
   1.141 +    TextIO.flushOut toParent;
   1.142 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.143 +    (* Attempt to prevent several signals from turning up simultaneously *)
   1.144 +    Posix.Process.sleep(Time.fromSeconds 1); all_tac)
   1.145  
   1.146  (**********************************************************************************)
   1.147  (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)