src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17484 f6a225f97f0a
parent 17422 3b237822985d
child 17488 67376a311a2b
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 14:20:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 15:12:13 2005 +0200
     1.3 @@ -39,12 +39,10 @@
     1.4  (*|   proofstep_to_string (Rewrite((a,b),(c,d))) =
     1.5        "Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*)
     1.6  
     1.7 -fun list_to_string [] liststr = liststr
     1.8 -|   list_to_string (x::[]) liststr = liststr^(string_of_int x)
     1.9 -|   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
    1.10  
    1.11 -
    1.12 -fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
    1.13 +fun proof_to_string (num,(step,clause_strs, thmvars)) =
    1.14 + (string_of_int num)^(proofstep_to_string step)^
    1.15 + "["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]"
    1.16   
    1.17  
    1.18  fun proofs_to_string [] str = str
    1.19 @@ -55,7 +53,9 @@
    1.20  
    1.21  
    1.22  
    1.23 -fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
    1.24 +fun init_proofstep_to_string (num, step, clause_strs) =
    1.25 + (string_of_int num)^" "^(proofstep_to_string step)^" "^
    1.26 + (clause_strs_to_string clause_strs "")^" "
    1.27  
    1.28  fun init_proofsteps_to_string [] str = str
    1.29  |   init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 
    1.30 @@ -144,12 +144,11 @@
    1.31  
    1.32  (* retrieve the axioms that were obtained from the clasimpset *)
    1.33  
    1.34 -fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) clasimp_num step_nums = 
    1.35 -    let val realnums = map subone step_nums	
    1.36 -	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    1.37 -(*	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    1.38 -	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.39 -	val _ = TextIO.closeOut(axnums)*)
    1.40 +fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
    1.41 +    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) 
    1.42 +	                   (map subone step_nums)
    1.43 +(*	val _ = File.write (File.tmp_path (Path.basic "axnums")) 
    1.44 +                     (numstr clasimp_nums) *)
    1.45      in
    1.46  	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    1.47      end
    1.48 @@ -159,7 +158,7 @@
    1.49  (* get names of clasimp axioms used                  *)
    1.50  (*****************************************************)
    1.51  
    1.52 - fun get_axiom_names step_nums thms clause_arr num_of_clauses =
    1.53 + fun get_axiom_names step_nums thms clause_arr =
    1.54     let 
    1.55       (* not sure why this is necessary again, but seems to be *)
    1.56        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.57 @@ -168,7 +167,7 @@
    1.58       (* here need to add the clauses from clause_arr*)
    1.59       (***********************************************)
    1.60    
    1.61 -      val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.62 +      val clasimp_names_cls = get_clasimp_cls clause_arr step_nums 
    1.63        val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    1.64        val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.65                           (concat clasimp_names)
    1.66 @@ -178,20 +177,30 @@
    1.67     end
    1.68     
    1.69  
    1.70 -fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
    1.71 +fun get_axiom_names_spass proofstr thms clause_arr =
    1.72    let (* parse spass proof into datatype *)
    1.73 +      val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) 
    1.74 +                         ("Started parsing:\n" ^ proofstr)
    1.75        val tokens = #1(lex proofstr)
    1.76        val proof_steps = parse tokens
    1.77 -      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
    1.78 -                         ("Did parsing on "^proofstr)
    1.79 +      val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
    1.80        (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    1.81    in
    1.82      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    1.83 -                    thms clause_arr num_of_clauses
    1.84 +                    thms clause_arr
    1.85    end;
    1.86      
    1.87 - fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    1.88 -   get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    1.89 + (*String contains multiple lines, terminated with newline characters.
    1.90 +  A list consisting of the first number in each line is returned. *)
    1.91 +fun get_linenums proofstr = 
    1.92 +  let val numerics = String.tokens (not o Char.isDigit)
    1.93 +      fun firstno [] = NONE
    1.94 +        | firstno (x::xs) = Int.fromString x
    1.95 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    1.96 +  in  List.mapPartial (firstno o numerics) lines  end
    1.97 +
    1.98 +fun get_axiom_names_vamp_E proofstr thms clause_arr  =
    1.99 +   get_axiom_names (get_linenums proofstr) thms clause_arr;
   1.100      
   1.101  
   1.102  (***********************************************)
   1.103 @@ -206,13 +215,13 @@
   1.104  
   1.105  fun addvars c (a,b)  = (a,b,c)
   1.106  
   1.107 -fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
   1.108 +fun get_axioms_used proof_steps thms clause_arr  =
   1.109    let 
   1.110       val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.111       val axioms = (List.filter is_axiom) proof_steps
   1.112       val step_nums = get_step_nums axioms []
   1.113  
   1.114 -     val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   1.115 +     val clauses = make_clauses thms    (*FIXME: must this be repeated??*)
   1.116       
   1.117       val vars = map thm_vars clauses
   1.118      
   1.119 @@ -265,19 +274,19 @@
   1.120  val restore_linebreaks = subst_for #"\t" #"\n";
   1.121  
   1.122  
   1.123 -fun proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms clause_arr num_of_clauses getax = 
   1.124 - let val _ = File.append(File.tmp_path (Path.basic "spass_lemmastring"))
   1.125 +fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax = 
   1.126 + let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
   1.127                 ("proofstr is " ^ proofstr ^
   1.128                  "\ngoalstr is " ^ goalstring ^
   1.129 -                "\nnum of clauses is " ^ string_of_int num_of_clauses)
   1.130 +                "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
   1.131  
   1.132 -     val axiom_names = getax proofstr thms clause_arr num_of_clauses
   1.133 -     val ax_str = "Rules from clasimpset used in automatic proof: " ^
   1.134 -                  rules_to_string axiom_names
   1.135 +     val axiom_names = getax proofstr thms clause_arr
   1.136 +     val ax_str = rules_to_string axiom_names
   1.137      in 
   1.138 -	 File.append(File.tmp_path (Path.basic "spass_lemmastring"))
   1.139 -	            ("reconstring is: "^ax_str^"  "^goalstring);
   1.140 -         TextIO.output (toParent, ax_str^"\n");
   1.141 +	 File.append(File.tmp_path (Path.basic "prover_lemmastring"))
   1.142 +	            ("\nlemma list is: " ^ ax_str);
   1.143 +         TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
   1.144 +                  ax_str ^ "\n");
   1.145  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.146  	 TextIO.flushOut toParent;
   1.147  
   1.148 @@ -285,9 +294,10 @@
   1.149  	(* Attempt to prevent several signals from turning up simultaneously *)
   1.150  	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.151      end
   1.152 -    handle _ => (*FIXME: exn handler is too general!*)
   1.153 -     (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
   1.154 -      TextIO.output (toParent, "Proof found but translation failed : " ^ 
   1.155 +    handle exn => (*FIXME: exn handler is too general!*)
   1.156 +     (File.write(File.tmp_path (Path.basic "proverString_handler")) 
   1.157 +         ("In exception handler: " ^ Toplevel.exn_message exn);
   1.158 +      TextIO.output (toParent, "Translation failed for the proof: " ^ 
   1.159                       remove_linebreaks proofstr ^ "\n");
   1.160        TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
   1.161        TextIO.flushOut toParent;
   1.162 @@ -295,21 +305,19 @@
   1.163        (* Attempt to prevent several signals from turning up simultaneously *)
   1.164        Posix.Process.sleep(Time.fromSeconds 1); all_tac);
   1.165  
   1.166 -fun proverString_to_lemmaString proofstr goalstring toParent ppid thms
   1.167 -      clause_arr num_of_clauses  = 
   1.168 -  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
   1.169 -       clause_arr num_of_clauses get_axiom_names_vamp_E;
   1.170 +fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr  = 
   1.171 +  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
   1.172 +       clause_arr get_axiom_names_vamp_E;
   1.173  
   1.174 -fun spassString_to_lemmaString proofstr goalstring toParent ppid thms
   1.175 -      clause_arr  num_of_clauses  = 
   1.176 -  proverString_to_lemmaString_aux proofstr goalstring toParent ppid thms        
   1.177 -       clause_arr num_of_clauses get_axiom_names_spass;
   1.178 +fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr = 
   1.179 +  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
   1.180 +       clause_arr get_axiom_names_spass;
   1.181  
   1.182  
   1.183  (**** Full proof reconstruction for SPASS (not really working) ****)
   1.184  
   1.185 -fun spassString_to_reconString proofstr goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.186 -  let val _ = File.write(File.tmp_path (Path.basic "spass_reconstruction")) 
   1.187 +fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
   1.188 +  let val _ = File.write(File.tmp_path (Path.basic "prover_reconstruction")) 
   1.189                   ("proofstr is: "^proofstr)
   1.190        val tokens = #1(lex proofstr)
   1.191  
   1.192 @@ -318,7 +326,7 @@
   1.193    (***********************************)
   1.194        val proof_steps = parse tokens
   1.195  
   1.196 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))
   1.197 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))
   1.198                        ("Did parsing on "^proofstr)
   1.199      
   1.200    (************************************)
   1.201 @@ -329,19 +337,19 @@
   1.202        (* subgoal this is, and turn it into meta_clauses *)
   1.203        (* should prob add array and table here, so that we can get axioms*)
   1.204        (* produced from the clasimpset rather than the problem *)
   1.205 -      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.206 +      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
   1.207        
   1.208        (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.209 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction")) "got axioms"
   1.210 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction")) "got axioms"
   1.211  	
   1.212    (************************************)
   1.213    (* translate proof                  *)
   1.214    (************************************)
   1.215 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                           
   1.216 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                           
   1.217                         ("about to translate proof, steps: "
   1.218                         ^(init_proofsteps_to_string proof_steps ""))
   1.219        val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.220 -      val _ = File.append (File.tmp_path (Path.basic "spass_reconstruction"))                                                                       
   1.221 +      val _ = File.append (File.tmp_path (Path.basic "prover_reconstruction"))                                                                       
   1.222                         ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   1.223    (***************************************************)
   1.224    (* transfer necessary steps as strings to Isabelle *)
   1.225 @@ -371,9 +379,10 @@
   1.226        (* Attempt to prevent several signals from turning up simultaneously *)
   1.227         Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.228    end
   1.229 -  handle _ => 
   1.230 -   (File.append(File.tmp_path (Path.basic "spass_reconstruction")) "In exception handler";
   1.231 -    TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^
   1.232 +  handle exn => (*FIXME: exn handler is too general!*)
   1.233 +   (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
   1.234 +       ("In exception handler: " ^ Toplevel.exn_message exn);
   1.235 +    TextIO.output (toParent,"Translation failed for the proof:"^
   1.236           (remove_linebreaks proofstr) ^"\n");
   1.237      TextIO.output (toParent, goalstring^"\n");
   1.238      TextIO.flushOut toParent;