src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16061 8a139c1557bf
parent 16039 dfe264950511
child 16091 3683f0486a11
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 24 07:43:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 24 10:23:24 2005 +0200
     1.3 @@ -107,10 +107,13 @@
     1.4  
     1.5  (*** get a string representing the Isabelle ordered axioms ***)
     1.6  
     1.7 -fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta
     1.8 -                                         in
     1.9 -                                            (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    1.10 -                                         end
    1.11 +fun origAx_to_string (num,(meta,thmvars)) =
    1.12 +    let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
    1.13 +    in
    1.14 +       (string_of_int num)^"OrigAxiom()"^"["^
    1.15 +       (clause_strs_to_string clause_strs "")^"]"^"["^
    1.16 +       (thmvars_to_string thmvars "")^"]"
    1.17 +    end
    1.18  
    1.19  
    1.20  fun  origAxs_to_string [] str = str
    1.21 @@ -122,20 +125,20 @@
    1.22  
    1.23  (*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
    1.24  
    1.25 -fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta
    1.26 -                                           in
    1.27 -                                              (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    1.28 -                                           end
    1.29 -
    1.30 -
    1.31 +fun extraAx_to_string (num, (meta,thmvars)) =
    1.32 +   let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
    1.33 +   in
    1.34 +      (string_of_int num)^"ExtraAxiom()"^"["^
    1.35 +      (clause_strs_to_string clause_strs "")^"]"^
    1.36 +      "["^(thmvars_to_string thmvars "")^"]"
    1.37 +   end;
    1.38  
    1.39 -fun  extraAxs_to_string [] str = str
    1.40 -|   extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x 
    1.41 -                                   in
    1.42 -                                       extraAxs_to_string xs (str^newstr)
    1.43 -                                   end
    1.44 -
    1.45 -
    1.46 +fun extraAxs_to_string [] str = str
    1.47 +|   extraAxs_to_string (x::xs) str =
    1.48 +      let val newstr = extraAx_to_string x 
    1.49 +      in
    1.50 +	  extraAxs_to_string xs (str^newstr)
    1.51 +      end;
    1.52  
    1.53  fun is_axiom ( num:int,Axiom, str) = true
    1.54  |   is_axiom (num, _,_) = false
    1.55 @@ -156,7 +159,7 @@
    1.56  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    1.57  *)
    1.58  (*FIX - should this have vars in it? *)
    1.59 -fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) 
    1.60 +fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
    1.61                                 handle _ => false
    1.62  
    1.63  fun assoc_out_of_order a [] = raise Noassoc
    1.64 @@ -202,94 +205,94 @@
    1.65  (* add array and table here, so can retrieve clasimp axioms *)
    1.66  
    1.67   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.68 -                                         let 
    1.69 -                                             (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.70 -                                             val _ = TextIO.output (outfile, thmstring)
    1.71 -                                             
    1.72 -                                             val _ =  TextIO.closeOut outfile*)
    1.73 -                                            (* not sure why this is necessary again, but seems to be *)
    1.74 +     let 
    1.75 +	 (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.76 +	 val _ = TextIO.output (outfile, thmstring)
    1.77 +	 
    1.78 +	 val _ =  TextIO.closeOut outfile*)
    1.79 +	(* not sure why this is necessary again, but seems to be *)
    1.80  
    1.81 -                                            val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.82 -                                            val axioms = get_init_axioms proof_steps
    1.83 -                                            val step_nums = get_step_nums axioms []
    1.84 +	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.85 +	val axioms = get_init_axioms proof_steps
    1.86 +	val step_nums = get_step_nums axioms []
    1.87  
    1.88 -                                           (***********************************************)
    1.89 -                                           (* here need to add the clauses from clause_arr*)
    1.90 -                                           (***********************************************)
    1.91 +       (***********************************************)
    1.92 +       (* here need to add the clauses from clause_arr*)
    1.93 +       (***********************************************)
    1.94  
    1.95 -                                           (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    1.96 -                                            val clasimp_names = map #1 clasimp_names_cls
    1.97 -                                            val clasimp_cls = map #2 clasimp_names_cls
    1.98 -                                            val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.99 -                                             val _ = TextIO.output (outfile,clasimp_namestr)
   1.100 -                                             
   1.101 -                                             val _ =  TextIO.closeOut outfile
   1.102 +       (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
   1.103 +	val clasimp_names = map #1 clasimp_names_cls
   1.104 +	val clasimp_cls = map #2 clasimp_names_cls
   1.105 +	val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
   1.106 +	 val _ = TextIO.output (outfile,clasimp_namestr)
   1.107 +	 
   1.108 +	 val _ =  TextIO.closeOut outfile
   1.109  *)
   1.110  
   1.111 -                                            val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   1.112 -                                            
   1.113 -                                            val vars = map thm_vars clauses
   1.114 -                                           
   1.115 -                                            val distvars = distinct (fold append vars [])
   1.116 -                                            val clause_terms = map prop_of clauses  
   1.117 -                                            val clause_frees = List.concat (map term_frees clause_terms)
   1.118 +	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   1.119 +	
   1.120 +	val vars = map thm_vars clauses
   1.121 +       
   1.122 +	val distvars = distinct (fold append vars [])
   1.123 +	val clause_terms = map prop_of clauses  
   1.124 +	val clause_frees = List.concat (map term_frees clause_terms)
   1.125  
   1.126 -                                            val frees = map lit_string_with_nums clause_frees;
   1.127 +	val frees = map lit_string_with_nums clause_frees;
   1.128  
   1.129 -                                            val distfrees = distinct frees
   1.130 +	val distfrees = distinct frees
   1.131  
   1.132 -                                            val metas = map Meson.make_meta_clause clauses
   1.133 -                                            val ax_strs = map #3 axioms
   1.134 +	val metas = map Meson.make_meta_clause clauses
   1.135 +	val ax_strs = map #3 axioms
   1.136  
   1.137 -                                            (* literals of -all- axioms, not just those used by spass *)
   1.138 -                                            val meta_strs = map get_meta_lits metas
   1.139 -                                           
   1.140 -                                            val metas_and_strs = ListPair.zip (metas,meta_strs)
   1.141 -                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
   1.142 -                                             val _ = TextIO.output (outfile, onestr ax_strs)
   1.143 -                                             
   1.144 -                                             val _ =  TextIO.closeOut outfile
   1.145 -                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
   1.146 -                                             val _ = TextIO.output (outfile, onestr meta_strs)
   1.147 -                                             val _ =  TextIO.closeOut outfile
   1.148 +	(* literals of -all- axioms, not just those used by spass *)
   1.149 +	val meta_strs = map ReconOrderClauses.get_meta_lits metas
   1.150 +       
   1.151 +	val metas_and_strs = ListPair.zip (metas,meta_strs)
   1.152 +	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
   1.153 +	 val _ = TextIO.output (outfile, onestr ax_strs)
   1.154 +	 
   1.155 +	 val _ =  TextIO.closeOut outfile
   1.156 +	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
   1.157 +	 val _ = TextIO.output (outfile, onestr meta_strs)
   1.158 +	 val _ =  TextIO.closeOut outfile
   1.159  
   1.160 -                                            (* get list of axioms as thms with their variables *)
   1.161 +	(* get list of axioms as thms with their variables *)
   1.162  
   1.163 -                                            val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   1.164 -                                            val ax_vars = map thm_vars ax_metas
   1.165 -                                            val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   1.166 +	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   1.167 +	val ax_vars = map thm_vars ax_metas
   1.168 +	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   1.169  
   1.170 -                                            (* get list of extra axioms as thms with their variables *)
   1.171 -                                            val extra_metas = add_if_not_inlist metas ax_metas []
   1.172 -                                            val extra_vars = map thm_vars extra_metas
   1.173 -                                            val extra_with_vars = if (not (extra_metas = []) ) 
   1.174 -                                                                  then
   1.175 - 									 ListPair.zip (extra_metas,extra_vars)
   1.176 -                                                                  else
   1.177 -                                                                         []
   1.178 +	(* get list of extra axioms as thms with their variables *)
   1.179 +	val extra_metas = add_if_not_inlist metas ax_metas []
   1.180 +	val extra_vars = map thm_vars extra_metas
   1.181 +	val extra_with_vars = if (not (extra_metas = []) ) 
   1.182 +			      then
   1.183 +				     ListPair.zip (extra_metas,extra_vars)
   1.184 +			      else
   1.185 +				     []
   1.186  
   1.187 -                                           (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.188 -                                           val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
   1.189 +       (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   1.190 +       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
   1.191  
   1.192 -                                           val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   1.193 -                                           val _ =  TextIO.closeOut outfile
   1.194 -                                          val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
   1.195 -                                          val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
   1.196 -                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   1.197 -                                         val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
   1.198 -                                        val ax_metas_str = TextIO.inputLine (infile)
   1.199 -                                        val _ = TextIO.closeIn infile
   1.200 -                                           val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   1.201 -                                           
   1.202 -                                         in
   1.203 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   1.204 -                                         end
   1.205 -                                        
   1.206 +       val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   1.207 +       val _ =  TextIO.closeOut outfile
   1.208 +      val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
   1.209 +      val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
   1.210 +	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   1.211 +     val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
   1.212 +    val ax_metas_str = TextIO.inputLine (infile)
   1.213 +    val _ = TextIO.closeIn infile
   1.214 +       val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   1.215 +       
   1.216 +     in
   1.217 +	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   1.218 +     end
   1.219 +    
   1.220  fun numclstr (vars, []) str = str
   1.221  |   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   1.222 -                               in
   1.223 -                                   numclstr  (vars,rest) newstr
   1.224 -                               end
   1.225 +in
   1.226 +numclstr  (vars,rest) newstr
   1.227 +end
   1.228  
   1.229  (*
   1.230  
   1.231 @@ -366,101 +369,101 @@
   1.232  val dummy_tac = PRIMITIVE(fn thm => thm );
   1.233  
   1.234  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.235 -                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.236 -                                                  (* val sign = sign_of_thm thm
   1.237 -                                                 val prems = prems_of thm
   1.238 -                                                 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   1.239 -                                                  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   1.240 -                                                  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   1.241 -             (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   1.242 -                                                  val _ =  TextIO.closeOut outfile
   1.243 +      let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.244 +	  (* val sign = sign_of_thm thm
   1.245 +	 val prems = prems_of thm
   1.246 +	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   1.247 +	  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   1.248 +	  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   1.249 +(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   1.250 +	  val _ =  TextIO.closeOut outfile
   1.251  
   1.252 -                                                  val tokens = #1(lex proofstr)
   1.253 +	  val tokens = #1(lex proofstr)
   1.254  
   1.255 -                                                    
   1.256 +	    
   1.257  
   1.258 -                                              (***********************************)
   1.259 -                                              (* parse spass proof into datatype *)
   1.260 -                                              (***********************************)
   1.261 +      (***********************************)
   1.262 +      (* parse spass proof into datatype *)
   1.263 +      (***********************************)
   1.264  
   1.265 -                                                  val proof_steps1 = parse tokens
   1.266 -                                                  val proof_steps = just_change_space proof_steps1
   1.267 +	  val proof_steps1 = parse tokens
   1.268 +	  val proof_steps = just_change_space proof_steps1
   1.269  
   1.270 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.271 -                                                  val _ =  TextIO.closeOut outfile
   1.272 -                                                
   1.273 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.274 -                                                  val _ =  TextIO.closeOut outfile
   1.275 -                                              (************************************)
   1.276 -                                              (* recreate original subgoal as thm *)
   1.277 -                                              (************************************)
   1.278 -                                                
   1.279 -                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.280 -                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.281 -                                                  (* subgoal this is, and turn it into meta_clauses *)
   1.282 -                                                  (* should prob add array and table here, so that we can get axioms*)
   1.283 -                                                  (* produced from the clasimpset rather than the problem *)
   1.284 -                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.285 -                                                  
   1.286 -                                                  (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.287 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   1.288 -                                                  val _ =  TextIO.closeOut outfile
   1.289 -                                                    
   1.290 -                                              (************************************)
   1.291 -                                              (* translate proof                  *)
   1.292 -                                              (************************************)
   1.293 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.294 -                                                  val _ =  TextIO.closeOut outfile
   1.295 -                                                  val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.296 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.297 -                                                  val _ =  TextIO.closeOut outfile
   1.298 -                                              (***************************************************)
   1.299 -                                              (* transfer necessary steps as strings to Isabelle *)
   1.300 -                                              (***************************************************)
   1.301 -                                                  (* turn the proof into a string *)
   1.302 -                                                  val reconProofStr = proofs_to_string proof ""
   1.303 -                                                  (* do the bit for the Isabelle ordered axioms at the top *)
   1.304 -                                                  val ax_nums = map #1 numcls
   1.305 -                                                  val ax_strs = map get_meta_lits_bracket (map #2 numcls)
   1.306 -                                                  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   1.307 -                                                  val num_cls_vars =  map (addvars vars) numcls_strs;
   1.308 -                                                  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   1.309 -                                                  
   1.310 -                                                  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   1.311 -                                                  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.312 -                                                  val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.313 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   1.314 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.315 +	  val _ =  TextIO.closeOut outfile
   1.316 +	
   1.317 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   1.318 +	  val _ =  TextIO.closeOut outfile
   1.319 +      (************************************)
   1.320 +      (* recreate original subgoal as thm *)
   1.321 +      (************************************)
   1.322 +	
   1.323 +	  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.324 +	  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.325 +	  (* subgoal this is, and turn it into meta_clauses *)
   1.326 +	  (* should prob add array and table here, so that we can get axioms*)
   1.327 +	  (* produced from the clasimpset rather than the problem *)
   1.328 +	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.329 +	  
   1.330 +	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.331 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   1.332 +	  val _ =  TextIO.closeOut outfile
   1.333 +	    
   1.334 +      (************************************)
   1.335 +      (* translate proof                  *)
   1.336 +      (************************************)
   1.337 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.338 +	  val _ =  TextIO.closeOut outfile
   1.339 +	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.340 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   1.341 +	  val _ =  TextIO.closeOut outfile
   1.342 +      (***************************************************)
   1.343 +      (* transfer necessary steps as strings to Isabelle *)
   1.344 +      (***************************************************)
   1.345 +	  (* turn the proof into a string *)
   1.346 +	  val reconProofStr = proofs_to_string proof ""
   1.347 +	  (* do the bit for the Isabelle ordered axioms at the top *)
   1.348 +	  val ax_nums = map #1 numcls
   1.349 +	  val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
   1.350 +	  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   1.351 +	  val num_cls_vars =  map (addvars vars) numcls_strs;
   1.352 +	  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   1.353 +	  
   1.354 +	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   1.355 +	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.356 +	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.357 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   1.358  
   1.359 -                                                  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   1.360 -                                                  val _ =  TextIO.closeOut outfile
   1.361 -    						  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.362 -                                              in 
   1.363 -                                                   TextIO.output (toParent, reconstr^"\n");
   1.364 -                                                   TextIO.flushOut toParent;
   1.365 -                                        	   TextIO.output (toParent, thmstring^"\n");
   1.366 -                                         	   TextIO.flushOut toParent;
   1.367 -                                         	   TextIO.output (toParent, goalstring^"\n");
   1.368 -                                         	   TextIO.flushOut toParent;
   1.369 -                                          
   1.370 -                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.371 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.372 -                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.373 -                                              end
   1.374 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.375 +	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   1.376 +	  val _ =  TextIO.closeOut outfile
   1.377 +	  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   1.378 +      in 
   1.379 +	   TextIO.output (toParent, reconstr^"\n");
   1.380 +	   TextIO.flushOut toParent;
   1.381 +	   TextIO.output (toParent, thmstring^"\n");
   1.382 +	   TextIO.flushOut toParent;
   1.383 +	   TextIO.output (toParent, goalstring^"\n");
   1.384 +	   TextIO.flushOut toParent;
   1.385 +  
   1.386 +	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.387 +	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.388 +	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.389 +      end
   1.390 +      handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.391  
   1.392 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   1.393 -                                                  val _ =  TextIO.closeOut outfile
   1.394 -                                              in 
   1.395 -                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   1.396 -                                                  TextIO.flushOut toParent;
   1.397 -						TextIO.output (toParent, thmstring^"\n");
   1.398 -                                         	   TextIO.flushOut toParent;
   1.399 -                                         	   TextIO.output (toParent, goalstring^"\n");
   1.400 -                                         	   TextIO.flushOut toParent;
   1.401 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.402 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.403 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.404 -                                              end)
   1.405 +	  val _ = TextIO.output (outfile, ("In exception handler"));
   1.406 +	  val _ =  TextIO.closeOut outfile
   1.407 +      in 
   1.408 +	  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   1.409 +	  TextIO.flushOut toParent;
   1.410 +	TextIO.output (toParent, thmstring^"\n");
   1.411 +	   TextIO.flushOut toParent;
   1.412 +	   TextIO.output (toParent, goalstring^"\n");
   1.413 +	   TextIO.flushOut toParent;
   1.414 +	  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.415 +	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.416 +	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   1.417 +      end)
   1.418  
   1.419  
   1.420  
   1.421 @@ -742,9 +745,9 @@
   1.422                             val axioms = get_axioms axioms_and_steps
   1.423                             
   1.424                             val steps = Library.drop (origax_num, axioms_and_steps)
   1.425 -                           val firststeps = butlast steps
   1.426 -                           val laststep = last steps
   1.427 -                           val goalstring = implode(butlast(explode goalstring))
   1.428 +                           val firststeps = ReconOrderClauses.butlast steps
   1.429 +                           val laststep = ReconOrderClauses.last steps
   1.430 +                           val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
   1.431                          
   1.432                             val isar_proof = 
   1.433                             ("show \""^goalstring^"\"\n")^