src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16259 aed1a8ae4b23
parent 16157 1764cc98bafd
child 16357 f1275d2a1dee
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun Jun 05 11:31:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun Jun 05 11:31:22 2005 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4 -
     1.5  (*  ID:         $Id$
     1.6 - Author:     Claire Quigley
     1.7 - Copyright   2004  University of Cambridge
     1.8 +    Author:     Claire Quigley
     1.9 +    Copyright   2004  University of Cambridge
    1.10  *)
    1.11  
    1.12  (******************)
    1.13 @@ -203,7 +202,7 @@
    1.14  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    1.15      let val realnums = map subone step_nums	
    1.16  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    1.17 -	val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    1.18 +	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    1.19  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.20  	val _ = TextIO.closeOut(axnums)
    1.21      in
    1.22 @@ -245,7 +244,7 @@
    1.23  
    1.24   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.25       let 
    1.26 -	 (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.27 +	 (*val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    1.28  	 val _ = TextIO.output (outfile, thmstring)
    1.29  	 
    1.30  	 val _ =  TextIO.closeOut outfile*)
    1.31 @@ -262,7 +261,7 @@
    1.32         (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    1.33  	val clasimp_names = map #1 clasimp_names_cls
    1.34  	val clasimp_cls = map #2 clasimp_names_cls
    1.35 -	val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.36 +	val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    1.37  	 val _ = TextIO.output (outfile,clasimp_namestr)
    1.38  	 
    1.39  	 val _ =  TextIO.closeOut outfile
    1.40 @@ -287,11 +286,11 @@
    1.41  	val meta_strs = map ReconOrderClauses.get_meta_lits metas
    1.42         
    1.43  	val metas_and_strs = ListPair.zip (metas,meta_strs)
    1.44 -	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.45 +	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.46  	 val _ = TextIO.output (outfile, onestr ax_strs)
    1.47  	 
    1.48  	 val _ =  TextIO.closeOut outfile
    1.49 -	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    1.50 +	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    1.51  	 val _ = TextIO.output (outfile, onestr meta_strs)
    1.52  	 val _ =  TextIO.closeOut outfile
    1.53  
    1.54 @@ -311,14 +310,14 @@
    1.55  				     []
    1.56  
    1.57         (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.58 -       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
    1.59 +       val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
    1.60  
    1.61         val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
    1.62         val _ =  TextIO.closeOut outfile
    1.63 -      val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
    1.64 -      val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
    1.65 +      val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
    1.66 +      val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
    1.67  	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
    1.68 -     val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
    1.69 +     val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
    1.70      val ax_metas_str = TextIO.inputLine (infile)
    1.71      val _ = TextIO.closeIn infile
    1.72         val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    1.73 @@ -345,7 +344,7 @@
    1.74  
    1.75  
    1.76  fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.77 -           let val  outfile = TextIO.openAppend(File.sysify_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.78 +           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.79                                                    val _ =  TextIO.closeOut outfile
    1.80  
    1.81                                                (***********************************)
    1.82 @@ -355,10 +354,10 @@
    1.83                                                    val tokens = #1(lex proofstr)
    1.84                                                    val proof_steps1 = parse tokens
    1.85                                                    val proof_steps = just_change_space proof_steps1
    1.86 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    1.87 +                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    1.88                                                    val _ =  TextIO.closeOut outfile
    1.89                                                  
    1.90 -                                                  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.91 +                                                  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.92                                                    val _ =  TextIO.closeOut outfile
    1.93                                                (************************************)
    1.94                                                (* recreate original subgoal as thm *)
    1.95 @@ -372,7 +371,7 @@
    1.96  
    1.97                                                    val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
    1.98                                                    val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
    1.99 -                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.100 +                                                  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   1.101                                                    val _ =  TextIO.closeOut outfile
   1.102                                                     
   1.103                                                in 
   1.104 @@ -387,7 +386,7 @@
   1.105                                           	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.106                                           	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.107                                                end
   1.108 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.109 +                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   1.110  
   1.111                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   1.112                                                    val _ =  TextIO.closeOut outfile
   1.113 @@ -406,7 +405,7 @@
   1.114  
   1.115  
   1.116  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.117 -      let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.118 +      let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   1.119  	  (* val sign = sign_of_thm thm
   1.120  	 val prems = prems_of thm
   1.121  	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   1.122 @@ -426,10 +425,10 @@
   1.123  	  val proof_steps1 = parse tokens
   1.124  	  val proof_steps = just_change_space proof_steps1
   1.125  
   1.126 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.127 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   1.128  	  val _ =  TextIO.closeOut outfile
   1.129  	
   1.130 -	  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.131 +	  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.132  	  val _ =  TextIO.closeOut outfile
   1.133        (************************************)
   1.134        (* recreate original subgoal as thm *)
   1.135 @@ -443,16 +442,16 @@
   1.136  	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   1.137  	  
   1.138  	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   1.139 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   1.140 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   1.141  	  val _ =  TextIO.closeOut outfile
   1.142  	    
   1.143        (************************************)
   1.144        (* translate proof                  *)
   1.145        (************************************)
   1.146 -	  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.147 +	  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.148  	  val _ =  TextIO.closeOut outfile
   1.149  	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   1.150 -	  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.151 +	  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.152  	  val _ =  TextIO.closeOut outfile
   1.153        (***************************************************)
   1.154        (* transfer necessary steps as strings to Isabelle *)
   1.155 @@ -469,7 +468,7 @@
   1.156  	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   1.157  	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   1.158  	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   1.159 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   1.160 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
   1.161  
   1.162  	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   1.163  	  val _ =  TextIO.closeOut outfile
   1.164 @@ -486,7 +485,7 @@
   1.165  	  (* Attempt to prevent several signals from turning up simultaneously *)
   1.166  	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   1.167        end
   1.168 -      handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.169 +      handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   1.170  
   1.171  	  val _ = TextIO.output (outfile, ("In exception handler"));
   1.172  	  val _ =  TextIO.closeOut outfile
   1.173 @@ -796,7 +795,7 @@
   1.174  		(isar_lines firststeps "")^
   1.175  		(last_isar_line laststep)^
   1.176  		("qed")
   1.177 -	val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
   1.178 +	val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
   1.179  	
   1.180  	val _ = TextIO.output (outfile, isar_proof)
   1.181  	val _ =  TextIO.closeOut outfile
   1.182 @@ -830,7 +829,7 @@
   1.183  
   1.184                                     val (frees,recon_steps) = parse_step tokens 
   1.185                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   1.186 -                                   val foo =   TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
   1.187 +                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   1.188                                 in 
   1.189                                    TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   1.190                                 end