reformatting and tidying
authorpaulson
Fri Jul 22 17:43:03 2005 +0200 (2005-07-22)
changeset 16905fa26952fa7b6
parent 16904 6fb188ca5f91
child 16906 74eddde1de2f
reformatting and tidying
src/HOL/Tools/ATP/recon_transfer_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jul 22 17:42:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jul 22 17:43:03 2005 +0200
     1.3 @@ -15,40 +15,6 @@
     1.4  infixr 8 ++; infixr 7 >>; infixr 6 ||;
     1.5  
     1.6  
     1.7 -
     1.8 -(*
     1.9 -fun fill_cls_array array n [] = ()
    1.10 -|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
    1.11 -                                     in
    1.12 -                                        fill_cls_array array (n+1) (xs)
    1.13 -                                     end;
    1.14 -
    1.15 -
    1.16 -
    1.17 -fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
    1.18 -                        symtable := Symtab.update((name , cls), !symtable);
    1.19 -      	       
    1.20 -
    1.21 -fun memo_add_all ([], symtable) = ()
    1.22 -|   memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
    1.23 -                           in
    1.24 -                               memo_add_all (xs, symtable)
    1.25 -                           end
    1.26 -
    1.27 -fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
    1.28 -      	        NONE =>  []
    1.29 -                |SOME cls  => cls ;
    1.30 -      	        	
    1.31 -
    1.32 -fun retrieve_clause array symtable clausenum = let
    1.33 -                                                  val (name, clnum) = Array.sub(array, clausenum)
    1.34 -                                                  val clauses = memo_find_clause (name, symtable)
    1.35 -                                                  val clause = get_nth clnum clauses
    1.36 -                                               in
    1.37 -                                                  (name, clause)
    1.38 -                                               end
    1.39 - *)                                             
    1.40 -
    1.41  (* Versions that include type information *)
    1.42   
    1.43  (* FIXME rename to str_of_thm *)
    1.44 @@ -251,8 +217,6 @@
    1.45     end
    1.46      
    1.47  
    1.48 -
    1.49 -
    1.50  (***********************************************)
    1.51  (* get axioms for reconstruction               *)
    1.52  (***********************************************)
    1.53 @@ -267,12 +231,6 @@
    1.54  
    1.55   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.56       let 
    1.57 -	 (*val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.58 -	 val _ = TextIO.output (outfile, thmstring)
    1.59 -	 
    1.60 -	 val _ =  TextIO.closeOut outfile*)
    1.61 -	(* not sure why this is necessary again, but seems to be *)
    1.62 -
    1.63  	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.64  	val axioms = get_init_axioms proof_steps
    1.65  	val step_nums = get_step_nums axioms []
    1.66 @@ -284,7 +242,7 @@
    1.67         (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    1.68  	val clasimp_names = map #1 clasimp_names_cls
    1.69  	val clasimp_cls = map #2 clasimp_names_cls
    1.70 -	val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.71 +	val _ = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.72  	 val _ = TextIO.output (outfile,clasimp_namestr)
    1.73  	 
    1.74  	 val _ =  TextIO.closeOut outfile
    1.75 @@ -309,13 +267,8 @@
    1.76  	val meta_strs = map ReconOrderClauses.get_meta_lits metas
    1.77         
    1.78  	val metas_and_strs = ListPair.zip (metas,meta_strs)
    1.79 -	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.80 -	 val _ = TextIO.output (outfile, onestr ax_strs)
    1.81 -	 
    1.82 -	 val _ =  TextIO.closeOut outfile
    1.83 -	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    1.84 -	 val _ = TextIO.output (outfile, onestr meta_strs)
    1.85 -	 val _ =  TextIO.closeOut outfile
    1.86 +	val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
    1.87 +	val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
    1.88  
    1.89  	(* get list of axioms as thms with their variables *)
    1.90  
    1.91 @@ -327,13 +280,10 @@
    1.92  	val extra_metas = add_if_not_inlist metas ax_metas []
    1.93  	val extra_vars = map thm_vars extra_metas
    1.94  	val extra_with_vars = if (not (extra_metas = []) ) 
    1.95 -			      then
    1.96 -				     ListPair.zip (extra_metas,extra_vars)
    1.97 -			      else
    1.98 -				     []
    1.99 -
   1.100 +			      then ListPair.zip (extra_metas,extra_vars)
   1.101 +			      else []
   1.102         (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.103 -       val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
   1.104 +       val _ = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
   1.105  
   1.106         val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   1.107         val _ =  TextIO.closeOut outfile
   1.108 @@ -344,13 +294,10 @@
   1.109      val ax_metas_str = TextIO.inputLine (infile)
   1.110      val _ = TextIO.closeIn infile
   1.111         val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   1.112 -       
   1.113       in
   1.114  	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   1.115 -     end
   1.116 -    
   1.117 -
   1.118 -                                        
   1.119 +     end;
   1.120 +                                            
   1.121  
   1.122  (*********************************************************************)
   1.123  (* Pass in spass string of proof and string version of isabelle goal *)
   1.124 @@ -372,122 +319,103 @@
   1.125  \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
   1.126  \1454[0:Obv:1453.0] ||  -> .";*)
   1.127  
   1.128 -fun subst_for a b [] = ""
   1.129 -  | subst_for a b (x :: xs) =
   1.130 -      if x = a
   1.131 -      then 
   1.132 -	b ^ subst_for a b xs
   1.133 -      else
   1.134 -	x ^ subst_for a b xs;
   1.135 +fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
   1.136  
   1.137 -val remove_linebreaks = subst_for "\n" "\t" o explode;
   1.138 -val restore_linebreaks = subst_for "\t" "\n" o explode;
   1.139 -
   1.140 +val remove_linebreaks = subst_for #"\n" #"\t";
   1.141 +val restore_linebreaks = subst_for #"\t" #"\n";
   1.142  
   1.143  fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.144 -           let 	val  outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile")));          
   1.145 -		val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses)))
   1.146 -
   1.147 -              	val _ =  TextIO.closeOut outfile
   1.148 +  let val _ = File.append(File.tmp_path (Path.basic"thmstringfile"))
   1.149 +                  ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses))
   1.150  
   1.151 -                 (***********************************)
   1.152 -                 (* parse spass proof into datatype *)
   1.153 -                 (***********************************)
   1.154 -         
   1.155 -                  val tokens = #1(lex proofstr)
   1.156 -                  val proof_steps1 = parse tokens
   1.157 -                  val proof_steps = just_change_space proof_steps1
   1.158 -                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));        val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.159 -                                                  val _ =  TextIO.closeOut outfile
   1.160 -                                                
   1.161 -                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.162 -                                                  val _ =  TextIO.closeOut outfile
   1.163 -                                              (************************************)
   1.164 -                                              (* recreate original subgoal as thm *)
   1.165 -                                              (************************************)
   1.166 -                                                
   1.167 -                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.168 -                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.169 -                                                  (* subgoal this is, and turn it into meta_clauses *)
   1.170 -                                                  (* should prob add array and table here, so that we can get axioms*)
   1.171 -                                                  (* produced from the clasimpset rather than the problem *)
   1.172 +     (***********************************)
   1.173 +     (* parse spass proof into datatype *)
   1.174 +     (***********************************)
   1.175 +      val tokens = #1(lex proofstr)
   1.176 +      val proof_steps1 = parse tokens
   1.177 +      val proof_steps = just_change_space proof_steps1
   1.178 +      val _ = File.write (File.tmp_path (Path.basic "foo_parse")) ("Did parsing on "^proofstr)
   1.179 +      val _ = File.write(File.tmp_path (Path.basic "foo_thmstring_at_parse"))
   1.180 +                        ("Parsing for thmstring: "^thmstring)
   1.181 +      (************************************)
   1.182 +      (* recreate original subgoal as thm *)
   1.183 +      (************************************)
   1.184 +    
   1.185 +      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.186 +      (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.187 +      (* subgoal this is, and turn it into meta_clauses *)
   1.188 +      (* should prob add array and table here, so that we can get axioms*)
   1.189 +      (* produced from the clasimpset rather than the problem *)
   1.190  
   1.191 -                                                  val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   1.192 -                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   1.193 -                                                  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.194 -                                                  val _ =  TextIO.closeOut outfile
   1.195 -                                                   
   1.196 -                                              in 
   1.197 -                                                   TextIO.output (toParent, ax_str^"\n");
   1.198 -                                                   TextIO.flushOut toParent;
   1.199 -                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.200 -                                         	   TextIO.flushOut toParent;
   1.201 -                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.202 -                                         	   TextIO.flushOut toParent;
   1.203 -                                          
   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 -                                              end
   1.208 -                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   1.209 +      val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   1.210 +      val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   1.211 +      val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
   1.212 +                         ("reconstring is: "^ax_str^"  "^goalstring)       
   1.213 +  in 
   1.214 +       TextIO.output (toParent, ax_str^"\n");
   1.215 +       TextIO.flushOut toParent;
   1.216 +       TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.217 +       TextIO.flushOut toParent;
   1.218 +       TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.219 +       TextIO.flushOut toParent;
   1.220  
   1.221 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   1.222 -                                                  val _ =  TextIO.closeOut outfile
   1.223 -                                              in 
   1.224 -                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
   1.225 -                                                  TextIO.flushOut toParent;
   1.226 -						   TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
   1.227 -                                         	   TextIO.flushOut toParent;
   1.228 -                                         	   TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
   1.229 -                                         	   TextIO.flushOut toParent;
   1.230 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.231 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.232 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.233 -                                              end)
   1.234 +       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.235 +      (* Attempt to prevent several signals from turning up simultaneously *)
   1.236 +       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.237 +  end
   1.238 +  handle _ => 
   1.239 +  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.240 +  in 
   1.241 +     TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
   1.242 +      TextIO.flushOut toParent;
   1.243 +       TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
   1.244 +       TextIO.flushOut toParent;
   1.245 +       TextIO.output (toParent, ( (remove_linebreaks 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 +  end
   1.251  
   1.252  
   1.253  fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.254 -           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						       val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
   1.255 -                                               val _ =  TextIO.closeOut outfile
   1.256 + let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
   1.257 +               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
   1.258 +                "goalstr is: "^goalstring^" num of clauses is: "^
   1.259 +                (string_of_int num_of_clauses))
   1.260 +
   1.261 +    (***********************************)
   1.262 +    (* get vampire axiom names         *)
   1.263 +    (***********************************)
   1.264  
   1.265 -                                              (***********************************)
   1.266 -                                              (* get vampire axiom names         *)
   1.267 -                                              (***********************************)
   1.268 -         
   1.269 -                                               val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
   1.270 -                                               val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
   1.271 -                                               val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                    val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.272 -                                               val _ =  TextIO.closeOut outfile
   1.273 -                                                   
   1.274 -                                              in 
   1.275 -                                                   TextIO.output (toParent, ax_str^"\n");
   1.276 -                                                   TextIO.flushOut toParent;
   1.277 -                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.278 -                                         	   TextIO.flushOut toParent;
   1.279 -                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.280 -                                         	   TextIO.flushOut toParent;
   1.281 -                                          
   1.282 -                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.283 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.284 -                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.285 -                                              end
   1.286 -                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   1.287 +     val (axiom_names) = get_axiom_names_vamp proofstr  thms clause_arr  num_of_clauses
   1.288 +     val ax_str = "Rules from clasimpset used in proof found by Vampire: "^(rules_to_string axiom_names "")
   1.289 +    in 
   1.290 +	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
   1.291 +         TextIO.output (toParent, ax_str^"\n");
   1.292 +	 TextIO.flushOut toParent;
   1.293 +	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.294 +	 TextIO.flushOut toParent;
   1.295 +	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.296 +	 TextIO.flushOut toParent;
   1.297  
   1.298 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   1.299 -                                                  val _ =  TextIO.closeOut outfile
   1.300 -                                              in 
   1.301 -                                                  TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.302 -                                                  TextIO.flushOut toParent;
   1.303 -						   TextIO.output (toParent, thmstring^"\n");
   1.304 -                                         	   TextIO.flushOut toParent;
   1.305 -                                         	   TextIO.output (toParent, goalstring^"\n");
   1.306 -                                         	   TextIO.flushOut toParent;
   1.307 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.308 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.309 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.310 -                                              end)
   1.311 -
   1.312 -
   1.313 +	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.314 +	(* Attempt to prevent several signals from turning up simultaneously *)
   1.315 +	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.316 +    end
   1.317 +    handle _ => 
   1.318 +    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.319 +    in 
   1.320 +	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.321 +	TextIO.flushOut toParent;
   1.322 +	 TextIO.output (toParent, thmstring^"\n");
   1.323 +	 TextIO.flushOut toParent;
   1.324 +	 TextIO.output (toParent, goalstring^"\n");
   1.325 +	 TextIO.flushOut toParent;
   1.326 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.327 +	(* Attempt to prevent several signals from turning up simultaneously *)
   1.328 +	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.329 +    end;
   1.330  
   1.331  
   1.332  (* val proofstr = "1582[0:Inp] || -> v_P*.\
   1.333 @@ -495,104 +423,87 @@
   1.334  		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   1.335  
   1.336  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.337 -      let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.338 -	  (* val sign = sign_of_thm thm
   1.339 -	 val prems = prems_of thm
   1.340 -	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   1.341 -	  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   1.342 -	  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   1.343 -(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   1.344 -	  val _ =  TextIO.closeOut outfile
   1.345 +  let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
   1.346 +                 (" thmstring is: "^thmstring^"proofstr is: "^proofstr)
   1.347 +      val tokens = #1(lex proofstr)
   1.348  
   1.349 -	  val tokens = #1(lex proofstr)
   1.350 -
   1.351 -	    
   1.352 +  (***********************************)
   1.353 +  (* parse spass proof into datatype *)
   1.354 +  (***********************************)
   1.355 +      val proof_steps1 = parse tokens
   1.356 +      val proof_steps = just_change_space proof_steps1
   1.357  
   1.358 -      (***********************************)
   1.359 -      (* parse spass proof into datatype *)
   1.360 -      (***********************************)
   1.361 -
   1.362 -	  val proof_steps1 = parse tokens
   1.363 -	  val proof_steps = just_change_space proof_steps1
   1.364 -
   1.365 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.366 -	  val _ =  TextIO.closeOut outfile
   1.367 -	
   1.368 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.369 -	  val _ =  TextIO.closeOut outfile
   1.370 -      (************************************)
   1.371 -      (* recreate original subgoal as thm *)
   1.372 -      (************************************)
   1.373 +      val _ = File.write (File.tmp_path (Path.basic "foo_parse"))
   1.374 +                      ("Did parsing on "^proofstr)
   1.375 +    
   1.376 +      val _ = File.write (File.tmp_path (Path.basic "foo_thmstring_at_parse"))
   1.377 +                                ("Parsing for thmstring: "^thmstring)
   1.378 +  (************************************)
   1.379 +  (* recreate original subgoal as thm *)
   1.380 +  (************************************)
   1.381 +      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.382 +      (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.383 +      (* subgoal this is, and turn it into meta_clauses *)
   1.384 +      (* should prob add array and table here, so that we can get axioms*)
   1.385 +      (* produced from the clasimpset rather than the problem *)
   1.386 +      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.387 +      
   1.388 +      (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.389 +      val _ = File.write (File.tmp_path (Path.basic "foo_axiom")) "got axioms"
   1.390  	
   1.391 -	  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.392 -	  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.393 -	  (* subgoal this is, and turn it into meta_clauses *)
   1.394 -	  (* should prob add array and table here, so that we can get axioms*)
   1.395 -	  (* produced from the clasimpset rather than the problem *)
   1.396 -	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.397 -	  
   1.398 -	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.399 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   1.400 -	  val _ =  TextIO.closeOut outfile
   1.401 -	    
   1.402 -      (************************************)
   1.403 -      (* translate proof                  *)
   1.404 -      (************************************)
   1.405 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.406 -	  val _ =  TextIO.closeOut outfile
   1.407 -	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.408 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.409 -	  val _ =  TextIO.closeOut outfile
   1.410 -      (***************************************************)
   1.411 -      (* transfer necessary steps as strings to Isabelle *)
   1.412 -      (***************************************************)
   1.413 -	  (* turn the proof into a string *)
   1.414 -	  val reconProofStr = proofs_to_string proof ""
   1.415 -	  (* do the bit for the Isabelle ordered axioms at the top *)
   1.416 -	  val ax_nums = map #1 numcls
   1.417 -	  val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
   1.418 -	  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   1.419 -	  val num_cls_vars =  map (addvars vars) numcls_strs;
   1.420 -	  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   1.421 -	  
   1.422 -	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   1.423 -	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.424 -	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.425 -	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
   1.426 +  (************************************)
   1.427 +  (* translate proof                  *)
   1.428 +  (************************************)
   1.429 +      val _ = File.write (File.tmp_path (Path.basic "foo_steps"))                                                                           
   1.430 +                       ("about to translate proof, steps: "
   1.431 +                       ^(init_proofsteps_to_string proof_steps ""))
   1.432 +      val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.433 +      val _ = File.write (File.tmp_path (Path.basic "foo_steps2"))                                                                       
   1.434 +                       ("translated proof, steps: "^(init_proofsteps_to_string proof_steps ""))
   1.435 +  (***************************************************)
   1.436 +  (* transfer necessary steps as strings to Isabelle *)
   1.437 +  (***************************************************)
   1.438 +      (* turn the proof into a string *)
   1.439 +      val reconProofStr = proofs_to_string proof ""
   1.440 +      (* do the bit for the Isabelle ordered axioms at the top *)
   1.441 +      val ax_nums = map #1 numcls
   1.442 +      val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
   1.443 +      val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   1.444 +      val num_cls_vars =  map (addvars vars) numcls_strs;
   1.445 +      val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   1.446 +      
   1.447 +      val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars))
   1.448 +                       else []
   1.449 +      val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.450 +      val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.451 +      val _ = File.write (File.tmp_path (Path.basic "reconstringfile"))
   1.452 +                          (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.453 +      val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.454 +  in 
   1.455 +       TextIO.output (toParent, reconstr^"\n");
   1.456 +       TextIO.flushOut toParent;
   1.457 +       TextIO.output (toParent, thmstring^"\n");
   1.458 +       TextIO.flushOut toParent;
   1.459 +       TextIO.output (toParent, goalstring^"\n");
   1.460 +       TextIO.flushOut toParent;
   1.461  
   1.462 -	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   1.463 -	  val _ =  TextIO.closeOut outfile
   1.464 -	  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.465 -      in 
   1.466 -	   TextIO.output (toParent, reconstr^"\n");
   1.467 -	   TextIO.flushOut toParent;
   1.468 -	   TextIO.output (toParent, thmstring^"\n");
   1.469 -	   TextIO.flushOut toParent;
   1.470 -	   TextIO.output (toParent, goalstring^"\n");
   1.471 -	   TextIO.flushOut toParent;
   1.472 -  
   1.473 -	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.474 -	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.475 -	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.476 -      end
   1.477 -      handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   1.478 -
   1.479 -	  val _ = TextIO.output (outfile, ("In exception handler"));
   1.480 -	  val _ =  TextIO.closeOut outfile
   1.481 -      in 
   1.482 -	   TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   1.483 -	  TextIO.flushOut toParent;
   1.484 -	TextIO.output (toParent, thmstring^"\n");
   1.485 -	   TextIO.flushOut toParent;
   1.486 -	   TextIO.output (toParent, goalstring^"\n");
   1.487 -	   TextIO.flushOut toParent;
   1.488 -	  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.489 -	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.490 -	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.491 -      end)
   1.492 -
   1.493 -
   1.494 -
   1.495 +       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.496 +      (* Attempt to prevent several signals from turning up simultaneously *)
   1.497 +       Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.498 +  end
   1.499 +  handle _ => 
   1.500 +  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.501 +  in 
   1.502 +       TextIO.output (toParent,"Proof found but translation failed for resolution proof:"^(remove_linebreaks proofstr) ^"\n");
   1.503 +      TextIO.flushOut toParent;
   1.504 +    TextIO.output (toParent, thmstring^"\n");
   1.505 +       TextIO.flushOut toParent;
   1.506 +       TextIO.output (toParent, goalstring^"\n");
   1.507 +       TextIO.flushOut toParent;
   1.508 +      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.509 +      (* Attempt to prevent several signals from turning up simultaneously *)
   1.510 +      Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.511 +  end
   1.512  
   1.513  
   1.514  (**********************************************************************************)
   1.515 @@ -889,10 +800,7 @@
   1.516  		(isar_lines firststeps "")^
   1.517  		(last_isar_line laststep)^
   1.518  		("qed")
   1.519 -	val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
   1.520 -	
   1.521 -	val _ = TextIO.output (outfile, isar_proof)
   1.522 -	val _ =  TextIO.closeOut outfile
   1.523 +	val _ = File.write (File.tmp_path (Path.basic "isar_proof_file")) isar_proof
   1.524      in
   1.525  	isar_proof
   1.526      end;