src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17306 5cde710a8a23
parent 17235 8e55ad29b690
child 17312 159783c74f75
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 09:54:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 07 18:14:26 2005 +0200
     1.3 @@ -175,12 +175,10 @@
     1.4  (* get names of clasimp axioms used                  *)
     1.5  (*****************************************************)
     1.6  
     1.7 - fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     1.8 + fun get_axiom_names step_nums thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     1.9     let 
    1.10       (* not sure why this is necessary again, but seems to be *)
    1.11        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.12 -      val axioms = get_init_axioms proof_steps
    1.13 -      val step_nums = get_step_nums axioms []
    1.14    
    1.15       (***********************************************)
    1.16       (* here need to add the clauses from clause_arr*)
    1.17 @@ -195,47 +193,14 @@
    1.18     in
    1.19        clasimp_names
    1.20     end
    1.21 -    
    1.22 - fun get_axiom_names_vamp proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.23 -   let 
    1.24 -     (* not sure why this is necessary again, but seems to be *)
    1.25 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.26 -      val step_nums =get_linenums proofstr
    1.27 -  
    1.28 -     (***********************************************)
    1.29 -     (* here need to add the clauses from clause_arr*)
    1.30 -     (***********************************************)
    1.31 -  
    1.32 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.33 -      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.34 -  
    1.35 -      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.36 -                         (concat clasimp_names)
    1.37 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.38 -   in
    1.39 -      clasimp_names
    1.40 -   end
    1.41 +   
    1.42 + fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    1.43 +   get_axiom_names (get_step_nums (get_init_axioms proof_steps) []) 
    1.44 +                       thms clause_arr num_of_clauses;
    1.45      
    1.46 -
    1.47 -fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    1.48 -   let 
    1.49 -     (* not sure why this is necessary again, but seems to be *)
    1.50 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.51 -      val step_nums =get_linenums proofstr
    1.52 -  
    1.53 -     (***********************************************)
    1.54 -     (* here need to add the clauses from clause_arr*)
    1.55 -     (***********************************************)
    1.56 -  
    1.57 -      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.58 -      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.59 -  
    1.60 -      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.61 -                         (concat clasimp_names)
    1.62 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.63 -   in
    1.64 -      clasimp_names
    1.65 -   end
    1.66 + fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    1.67 +   get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    1.68 +    
    1.69  
    1.70  (***********************************************)
    1.71  (* get axioms for reconstruction               *)
    1.72 @@ -255,19 +220,6 @@
    1.73  	val axioms = get_init_axioms proof_steps
    1.74  	val step_nums = get_step_nums axioms []
    1.75  
    1.76 -       (***********************************************)
    1.77 -       (* here need to add the clauses from clause_arr*)
    1.78 -       (***********************************************)
    1.79 -
    1.80 -       (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    1.81 -	val clasimp_names = map #1 clasimp_names_cls
    1.82 -	val clasimp_cls = map #2 clasimp_names_cls
    1.83 -	val _ = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.84 -	 val _ = TextIO.output (outfile,clasimp_namestr)
    1.85 -	 
    1.86 -	 val _ =  TextIO.closeOut outfile
    1.87 -*)
    1.88 -
    1.89  	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    1.90  	
    1.91  	val vars = map thm_vars clauses
    1.92 @@ -302,20 +254,8 @@
    1.93  	val extra_with_vars = if (not (extra_metas = []) ) 
    1.94  			      then ListPair.zip (extra_metas,extra_vars)
    1.95  			      else []
    1.96 -       (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.97 -       val _ = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
    1.98 -
    1.99 -       val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   1.100 -       val _ =  TextIO.closeOut outfile
   1.101 -      val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
   1.102 -      val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
   1.103 -	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   1.104 -     val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
   1.105 -    val ax_metas_str = TextIO.inputLine (infile)
   1.106 -    val _ = TextIO.closeIn infile
   1.107 -       val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   1.108       in
   1.109 -	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   1.110 +	(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   1.111       end;
   1.112                                              
   1.113  
   1.114 @@ -329,9 +269,6 @@
   1.115    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
   1.116                                    
   1.117  
   1.118 -val dummy_tac = PRIMITIVE(fn thm => thm );
   1.119 -
   1.120 -
   1.121  (*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
   1.122  \1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
   1.123  \1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
   1.124 @@ -351,10 +288,10 @@
   1.125       (* parse spass proof into datatype *)
   1.126       (***********************************)
   1.127        val tokens = #1(lex proofstr)
   1.128 -      val proof_steps1 = parse tokens
   1.129 -      val proof_steps = just_change_space proof_steps1
   1.130 -      val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr)
   1.131 -      val _ = File.write(File.tmp_path (Path.basic "foo_thmstring_at_parse"))
   1.132 +      val proof_steps = parse tokens
   1.133 +      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
   1.134 +                         ("Did parsing on "^proofstr)
   1.135 +      val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring"))
   1.136                          ("Parsing for thmstring: "^thmstring)
   1.137        (************************************)
   1.138        (* recreate original subgoal as thm *)
   1.139 @@ -366,22 +303,20 @@
   1.140        (* should prob add array and table here, so that we can get axioms*)
   1.141        (* produced from the clasimpset rather than the problem *)
   1.142  
   1.143 -      val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   1.144 +      val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses
   1.145        val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
   1.146                     rules_to_string axiom_names 
   1.147        val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
   1.148                           ("reconstring is: "^ax_str^"  "^goalstring)       
   1.149    in 
   1.150         TextIO.output (toParent, ax_str^"\n");
   1.151 -       TextIO.flushOut toParent;
   1.152         TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.153 -       TextIO.flushOut toParent;
   1.154         TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.155         TextIO.flushOut toParent;
   1.156  
   1.157         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.158        (* Attempt to prevent several signals from turning up simultaneously *)
   1.159 -       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.160 +       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.161    end
   1.162    handle _ => 
   1.163    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.164 @@ -394,7 +329,7 @@
   1.165         TextIO.flushOut toParent;
   1.166        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.167        (* Attempt to prevent several signals from turning up simultaneously *)
   1.168 -      Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.169 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.170    end
   1.171  
   1.172  
   1.173 @@ -408,34 +343,29 @@
   1.174      (* get vampire axiom names         *)
   1.175      (***********************************)
   1.176  
   1.177 -     val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
   1.178 +     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   1.179       val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
   1.180                    rules_to_string axiom_names
   1.181      in 
   1.182  	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   1.183           TextIO.output (toParent, ax_str^"\n");
   1.184 -	 TextIO.flushOut toParent;
   1.185  	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.186 -	 TextIO.flushOut toParent;
   1.187  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.188  	 TextIO.flushOut toParent;
   1.189  
   1.190  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.191  	(* Attempt to prevent several signals from turning up simultaneously *)
   1.192 -	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.193 +	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.194      end
   1.195      handle _ => 
   1.196      let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.197      in 
   1.198  	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.199 -	TextIO.flushOut toParent;
   1.200  	 TextIO.output (toParent, thmstring^"\n");
   1.201 -	 TextIO.flushOut toParent;
   1.202  	 TextIO.output (toParent, goalstring^"\n");
   1.203  	 TextIO.flushOut toParent;
   1.204  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.205 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.206 -	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.207 +	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.208      end;
   1.209  
   1.210  
   1.211 @@ -446,42 +376,35 @@
   1.212                  (string_of_int num_of_clauses))
   1.213  
   1.214      (***********************************)
   1.215 -    (* get vampire axiom names         *)
   1.216 +    (* get E axiom names         *)
   1.217      (***********************************)
   1.218  
   1.219 -     val (axiom_names) = get_axiom_names_E proofstr  thms clause_arr  num_of_clauses
   1.220 +     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   1.221       val ax_str = "Rules from clasimpset used in proof found by E: " ^
   1.222                    rules_to_string axiom_names
   1.223      in 
   1.224  	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   1.225           TextIO.output (toParent, ax_str^"\n");
   1.226  	 TextIO.flushOut toParent;
   1.227 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.228 -	 TextIO.flushOut toParent;
   1.229  	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.230  	 TextIO.flushOut toParent;
   1.231  
   1.232  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.233  	(* Attempt to prevent several signals from turning up simultaneously *)
   1.234 -	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.235 +	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.236      end
   1.237      handle _ => 
   1.238      let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.239      in 
   1.240 -	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.241 -	TextIO.flushOut toParent;
   1.242 +	TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.243  	 TextIO.output (toParent, thmstring^"\n");
   1.244 -	 TextIO.flushOut toParent;
   1.245  	 TextIO.output (toParent, goalstring^"\n");
   1.246  	 TextIO.flushOut toParent;
   1.247  	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.248  	(* Attempt to prevent several signals from turning up simultaneously *)
   1.249 -	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.250 +	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.251      end;
   1.252  
   1.253 -(* val proofstr = "1582[0:Inp] || -> v_P*.\
   1.254 -                 \1583[0:Inp] || v_P* -> .\
   1.255 -		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   1.256  
   1.257  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.258    let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
   1.259 @@ -491,8 +414,7 @@
   1.260    (***********************************)
   1.261    (* parse spass proof into datatype *)
   1.262    (***********************************)
   1.263 -      val proof_steps1 = parse tokens
   1.264 -      val proof_steps = just_change_space proof_steps1
   1.265 +      val proof_steps = parse tokens
   1.266  
   1.267        val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
   1.268                        ("Did parsing on "^proofstr)
   1.269 @@ -550,7 +472,7 @@
   1.270  
   1.271         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.272        (* Attempt to prevent several signals from turning up simultaneously *)
   1.273 -       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.274 +       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.275    end
   1.276    handle _ => 
   1.277    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.278 @@ -563,7 +485,7 @@
   1.279         TextIO.flushOut toParent;
   1.280        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.281        (* Attempt to prevent several signals from turning up simultaneously *)
   1.282 -      Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.283 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.284    end
   1.285  
   1.286  
   1.287 @@ -643,8 +565,9 @@
   1.288  
   1.289  
   1.290  (** change this to allow P (x U) *)
   1.291 - fun arglist_step input = ( word ++ many  word >> (fn (a, b) => (a^" "^(implode_with_space b)))
   1.292 -                           ||word >> (fn (a) => (a)))input
   1.293 + fun arglist_step input = 
   1.294 +   ( word ++ many word >> (fn (a, b) => (a^" "^(space_implode " " b)))
   1.295 +    ||word >> (fn (a) => (a)))input
   1.296                  
   1.297  
   1.298  fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++  a (Other ")")