src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 05 16:32:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 06 12:01:37 2005 +0200
     1.3 @@ -254,7 +254,7 @@
     1.4  fun select_literal i cl = negate_head (make_last i cl);
     1.5  
     1.6   fun get_axioms_used proof_steps thmstring = let 
     1.7 -                                             val  outfile = TextIO.openOut("foo_ax_thmstr");                                                                       
     1.8 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
     1.9                                               val _ = TextIO.output (outfile, thmstring)
    1.10                                               
    1.11                                               val _ =  TextIO.closeOut outfile
    1.12 @@ -282,11 +282,11 @@
    1.13                                              val meta_strs = map get_meta_lits metas
    1.14                                             
    1.15                                              val metas_and_strs = zip  metas meta_strs
    1.16 -                                             val  outfile = TextIO.openOut("foo_clauses");                                                                       
    1.17 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.18                                               val _ = TextIO.output (outfile, (onestr ax_strs ""))
    1.19                                               
    1.20                                               val _ =  TextIO.closeOut outfile
    1.21 -                                             val  outfile = TextIO.openOut("foo_metastrs");                                                                       
    1.22 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    1.23                                               val _ = TextIO.output (outfile, (onestr meta_strs ""))
    1.24                                               val _ =  TextIO.closeOut outfile
    1.25  
    1.26 @@ -306,12 +306,14 @@
    1.27                                                                           []
    1.28  
    1.29                                             (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.30 -                                           val  outfile = TextIO.openOut("foo_metas")
    1.31 +                                           val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
    1.32  
    1.33                                             val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
    1.34                                             val _ =  TextIO.closeOut outfile
    1.35 -                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars2.pl <foo_metas >foo_metas2"])
    1.36 -                                         val infile = TextIO.openIn("foo_metas2")
    1.37 +                                          val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
    1.38 +                                          val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
    1.39 +                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
    1.40 +                                         val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
    1.41                                          val ax_metas_str = TextIO.inputLine (infile)
    1.42                                          val _ = TextIO.closeIn infile
    1.43                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    1.44 @@ -400,7 +402,7 @@
    1.45  
    1.46  
    1.47  fun spassString_to_reconString proofstr thmstring = 
    1.48 -                                              let val  outfile = TextIO.openOut("thmstringfile");                                                                                      val _= warning("proofstr is: "^proofstr);
    1.49 +                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                                                                      val _= warning("proofstr is: "^proofstr);
    1.50                                                    val _ = warning ("thmstring is: "^thmstring);
    1.51                                                    val _ = TextIO.output (outfile, (thmstring))
    1.52                                                    val _ =  TextIO.closeOut outfile
    1.53 @@ -414,10 +416,10 @@
    1.54                                                    val proof_steps1 = parse tokens
    1.55                                                    val proof_steps = just_change_space proof_steps1
    1.56  
    1.57 -                                                  val  outfile = TextIO.openOut("foo_parse");                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    1.58 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    1.59                                                    val _ =  TextIO.closeOut outfile
    1.60                                                  
    1.61 -                                                  val  outfile = TextIO.openOut("foo_thmstring_at_parse");                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
    1.62 +                                                  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.63                                                    val _ =  TextIO.closeOut outfile
    1.64                                                (************************************)
    1.65                                                (* recreate original subgoal as thm *)
    1.66 @@ -427,16 +429,16 @@
    1.67                                                    val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
    1.68                                                    
    1.69                                                    (*val numcls_string = numclstr ( vars, numcls) ""*)
    1.70 -                                                  val  outfile = TextIO.openOut("foo_axiom");                                                                            val _ = TextIO.output (outfile,"got axioms")
    1.71 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
    1.72                                                    val _ =  TextIO.closeOut outfile
    1.73                                                      
    1.74                                                (************************************)
    1.75                                                (* translate proof                  *)
    1.76                                                (************************************)
    1.77 -                                                  val  outfile = TextIO.openOut("foo_steps");                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    1.78 +                                                  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.79                                                    val _ =  TextIO.closeOut outfile
    1.80                                                    val (newthm,proof) = translate_proof numcls  proof_steps vars
    1.81 -                                                  val  outfile = TextIO.openOut("foo_steps2");                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    1.82 +                                                  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.83                                                    val _ =  TextIO.closeOut outfile
    1.84                                                (***************************************************)
    1.85                                                (* transfer necessary steps as strings to Isabelle *)
    1.86 @@ -453,14 +455,14 @@
    1.87                                                    val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
    1.88                                                    val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
    1.89                                                    val frees_str = "["^(thmvars_to_string frees "")^"]"
    1.90 -                                                  val  outfile = TextIO.openOut("reconstringfile");
    1.91 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
    1.92  
    1.93                                                    val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
    1.94                                                    val _ =  TextIO.closeOut outfile
    1.95                                                in 
    1.96                                                     (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
    1.97                                                end
    1.98 -                                              handle _ => (let val  outfile = TextIO.openOut("foo_handler");
    1.99 +                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   1.100  
   1.101                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   1.102                                                    val _ =  TextIO.closeOut outfile
   1.103 @@ -765,7 +767,7 @@
   1.104                             (isar_lines firststeps "")^
   1.105                             (last_isar_line laststep)^
   1.106                             ("qed")
   1.107 -                          val  outfile = TextIO.openOut("isar_proof_file");
   1.108 +                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
   1.109  
   1.110                                                    val _ = TextIO.output (outfile, isar_proof)
   1.111                                                    val _ =  TextIO.closeOut outfile
   1.112 @@ -801,7 +803,7 @@
   1.113  
   1.114                                     val (frees,recon_steps) = parse_step tokens 
   1.115                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   1.116 -                                   val foo =   TextIO.openOut "foobar";
   1.117 +                                   val foo =   TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
   1.118                                 in 
   1.119                                    TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   1.120                                 end