src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17312 159783c74f75
parent 17306 5cde710a8a23
child 17315 5bf0e0aacc24
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 21:07:09 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 13:24:19 2005 +0200
     1.3 @@ -3,10 +3,6 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 -(******************)
     1.8 -(* complete later *)
     1.9 -(******************)
    1.10 -
    1.11  structure Recon_Transfer =
    1.12  struct
    1.13  
    1.14 @@ -104,10 +100,8 @@
    1.15  	  extraAxs_to_string xs (str^newstr)
    1.16        end;
    1.17  
    1.18 -fun is_axiom ( num:int,Axiom, str) = true
    1.19 -|   is_axiom (num, _,_) = false
    1.20 -
    1.21 -fun get_init_axioms xs = List.filter (is_axiom) ( xs)
    1.22 +fun is_axiom (_,Axiom,str) = true
    1.23 +|   is_axiom (_,_,_) = false
    1.24  
    1.25  fun get_step_nums [] nums = nums
    1.26  |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
    1.27 @@ -159,23 +153,22 @@
    1.28  
    1.29  (* retrieve the axioms that were obtained from the clasimpset *)
    1.30  
    1.31 -fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    1.32 +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = 
    1.33      let val realnums = map subone step_nums	
    1.34  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    1.35  (*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    1.36  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.37  	val _ = TextIO.closeOut(axnums)*)
    1.38      in
    1.39 -	retrieve_axioms clause_arr  clasimp_nums
    1.40 +	retrieve_axioms clause_arr clasimp_nums
    1.41      end
    1.42  
    1.43  
    1.44 -
    1.45  (*****************************************************)
    1.46  (* get names of clasimp axioms used                  *)
    1.47  (*****************************************************)
    1.48  
    1.49 - fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.50 + fun get_axiom_names step_nums thms clause_arr num_of_clauses =
    1.51     let 
    1.52       (* not sure why this is necessary again, but seems to be *)
    1.53        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.54 @@ -184,7 +177,7 @@
    1.55       (* here need to add the clauses from clause_arr*)
    1.56       (***********************************************)
    1.57    
    1.58 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.59 +      val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.60        val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.61    
    1.62        val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.63 @@ -195,7 +188,7 @@
    1.64     end
    1.65     
    1.66   fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    1.67 -   get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) 
    1.68 +   get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    1.69                         thms clause_arr num_of_clauses;
    1.70      
    1.71   fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    1.72 @@ -217,7 +210,7 @@
    1.73   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.74       let 
    1.75  	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.76 -	val axioms = get_init_axioms proof_steps
    1.77 +	val axioms = (List.filter is_axiom) proof_steps
    1.78  	val step_nums = get_step_nums axioms []
    1.79  
    1.80  	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    1.81 @@ -322,9 +315,7 @@
    1.82    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
    1.83    in 
    1.84       TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
    1.85 -      TextIO.flushOut toParent;
    1.86         TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
    1.87 -       TextIO.flushOut toParent;
    1.88         TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
    1.89         TextIO.flushOut toParent;
    1.90        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.91 @@ -343,11 +334,12 @@
    1.92      (* get vampire axiom names         *)
    1.93      (***********************************)
    1.94  
    1.95 -     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
    1.96 +     val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses
    1.97       val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
    1.98                    rules_to_string axiom_names
    1.99      in 
   1.100 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   1.101 +	 File.append(File.tmp_path (Path.basic "reconstrfile")) 
   1.102 +	            ("reconstring is: "^ax_str^"  "^goalstring);
   1.103           TextIO.output (toParent, ax_str^"\n");
   1.104  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.105  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.106 @@ -383,9 +375,10 @@
   1.107       val ax_str = "Rules from clasimpset used in proof found by E: " ^
   1.108                    rules_to_string axiom_names
   1.109      in 
   1.110 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   1.111 +	 File.append(File.tmp_path (Path.basic "reconstrfile"))
   1.112 +	            ("reconstring is: "^ax_str^"  "^goalstring);
   1.113           TextIO.output (toParent, ax_str^"\n");
   1.114 -	 TextIO.flushOut toParent;
   1.115 +	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.116  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.117  	 TextIO.flushOut toParent;
   1.118  
   1.119 @@ -771,7 +764,7 @@
   1.120  	
   1.121  	val steps = Library.drop (origax_num, axioms_and_steps)
   1.122  	val firststeps = ReconOrderClauses.butlast steps
   1.123 -	val laststep = ReconOrderClauses.last steps
   1.124 +	val laststep = List.last steps
   1.125  	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
   1.126  	
   1.127  	val isar_proof =