watcher.ML and watcher.sig changed. Debug files now write to tmp.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Wed Apr 06 12:01:37 2005 +0200
@@ -34,7 +34,7 @@
then (
let val proofextract = extract_proof (currentString^thisLine)
val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
- val foo = TextIO.openOut "foobar2";
+ val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
in
TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
@@ -92,8 +92,8 @@
(* end*)
fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) =
- let val spass_proof_file = TextIO.openAppend("spass_proof")
- val outfile = TextIO.openOut("foo_checkspass");
+ let val spass_proof_file = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));
val _ = TextIO.output (outfile, "checking proof found")
val _ = TextIO.closeOut outfile
@@ -105,7 +105,7 @@
in if ( thisLine = "SPASS beiseite: Proof found.\n" )
then
(
- let val outfile = TextIO.openOut("foo_proof"); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -117,7 +117,7 @@
then
(
- let val outfile = TextIO.openOut("foo_proof"); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -214,7 +214,7 @@
fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
then
let val thisLine = TextIO.inputLine instr
- val outfile = TextIO.openOut("foo_thisLine"); val _ = TextIO.output (outfile, (thisLine))
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
in
@@ -243,7 +243,7 @@
let val reconstr = thisLine
val thmstring = TextIO.inputLine instr
val goalstring = TextIO.inputLine instr
- val outfile = TextIO.openOut("foo_getSpass");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
in
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Apr 06 12:01:37 2005 +0200
@@ -254,7 +254,7 @@
fun select_literal i cl = negate_head (make_last i cl);
fun get_axioms_used proof_steps thmstring = let
- val outfile = TextIO.openOut("foo_ax_thmstr");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
val _ = TextIO.output (outfile, thmstring)
val _ = TextIO.closeOut outfile
@@ -282,11 +282,11 @@
val meta_strs = map get_meta_lits metas
val metas_and_strs = zip metas meta_strs
- val outfile = TextIO.openOut("foo_clauses");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
val _ = TextIO.output (outfile, (onestr ax_strs ""))
val _ = TextIO.closeOut outfile
- val outfile = TextIO.openOut("foo_metastrs");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));
val _ = TextIO.output (outfile, (onestr meta_strs ""))
val _ = TextIO.closeOut outfile
@@ -306,12 +306,14 @@
[]
(* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
- val outfile = TextIO.openOut("foo_metas")
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
val _ = TextIO.closeOut outfile
- val execperl = Unix.execute("/usr/bin/perl", ["remchars2.pl <foo_metas >foo_metas2"])
- val infile = TextIO.openIn("foo_metas2")
+ val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
+ val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
+ val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2])
+ val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
val ax_metas_str = TextIO.inputLine (infile)
val _ = TextIO.closeIn infile
val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
@@ -400,7 +402,7 @@
fun spassString_to_reconString proofstr thmstring =
- let val outfile = TextIO.openOut("thmstringfile"); val _= warning("proofstr is: "^proofstr);
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile"))); val _= warning("proofstr is: "^proofstr);
val _ = warning ("thmstring is: "^thmstring);
val _ = TextIO.output (outfile, (thmstring))
val _ = TextIO.closeOut outfile
@@ -414,10 +416,10 @@
val proof_steps1 = parse tokens
val proof_steps = just_change_space proof_steps1
- val outfile = TextIO.openOut("foo_parse"); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
val _ = TextIO.closeOut outfile
- val outfile = TextIO.openOut("foo_thmstring_at_parse"); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
val _ = TextIO.closeOut outfile
(************************************)
(* recreate original subgoal as thm *)
@@ -427,16 +429,16 @@
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
(*val numcls_string = numclstr ( vars, numcls) ""*)
- val outfile = TextIO.openOut("foo_axiom"); val _ = TextIO.output (outfile,"got axioms")
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
val _ = TextIO.closeOut outfile
(************************************)
(* translate proof *)
(************************************)
- val outfile = TextIO.openOut("foo_steps"); val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
+ 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 "")))
val _ = TextIO.closeOut outfile
val (newthm,proof) = translate_proof numcls proof_steps vars
- val outfile = TextIO.openOut("foo_steps2"); val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
+ 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 "")))
val _ = TextIO.closeOut outfile
(***************************************************)
(* transfer necessary steps as strings to Isabelle *)
@@ -453,14 +455,14 @@
val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
val frees_str = "["^(thmvars_to_string frees "")^"]"
- val outfile = TextIO.openOut("reconstringfile");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
val _ = TextIO.closeOut outfile
in
(frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
end
- handle _ => (let val outfile = TextIO.openOut("foo_handler");
+ handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
val _ = TextIO.output (outfile, ("In exception handler"));
val _ = TextIO.closeOut outfile
@@ -765,7 +767,7 @@
(isar_lines firststeps "")^
(last_isar_line laststep)^
("qed")
- val outfile = TextIO.openOut("isar_proof_file");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
val _ = TextIO.output (outfile, isar_proof)
val _ = TextIO.closeOut outfile
@@ -801,7 +803,7 @@
val (frees,recon_steps) = parse_step tokens
val isar_str = to_isar_proof (frees, recon_steps, goalstring)
- val foo = TextIO.openOut "foobar";
+ val foo = TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
in
TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str isar_str); ()
end
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Apr 06 12:01:37 2005 +0200
@@ -437,7 +437,7 @@
val thmproofstring = proofstring ( thmstring)
val no_returns =List.filter not_newline ( thmproofstring)
val thmstr = implode no_returns
- val outfile = TextIO.openOut("thml_file")
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
val _ = TextIO.output(outfile, "thmstr is "^thmstr)
val _ = TextIO.flushOut outfile;
val _ = TextIO.closeOut outfile
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/remchars.pl Wed Apr 06 12:01:37 2005 +0200
@@ -0,0 +1,31 @@
+#!/usr/bin/perl
+#
+# isa2tex.pl - Converts isabelle formulae into LaTeX
+# A complete hack - needs more work.
+#
+# by Michael Dales (michael@dcs.gla.ac.uk)
+
+# Begin math mode
+#printf "\$";
+#ALL íxaè::ê'aè::étypeè. (~ (ìPè::ê'aè::étypeè => bool) (ìxè::ê'aè::étypeè) | ìPè íxaè) & (~ ìPè íxaè# | ìPè ìxè)((ìPè::ê'aè::étypeè => bool) (ìxaè::ê'aè::étypeè) | (ALL íxè::ê'aè::étypeè. ìPè íxè)) &((AL#L íxè::ê'aè::étypeè. ~ ìPè íxè) | ~ ìPè (ìxbè::ê'aè::étypeè))
+#perhaps change to all chars not in alphanumeric or a few symbols?
+
+while (<STDIN>)
+{
+
+ #chop();
+ s%\n$%%;
+ s%í%%g;
+ s%ì%%g;
+ s%è%%g;
+ s%î%%g;
+ s%ê%%g;
+ s%é%%g;
+
+ #printf "$_\\newline\n";
+ printf "$_";
+}
+
+# End math mode
+#printf "\$\n";
+#printf "\\end{tabbing}\n";
--- a/src/HOL/Tools/ATP/watcher.ML Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Wed Apr 06 12:01:37 2005 +0200
@@ -97,7 +97,7 @@
let
val dfg_dir = File.tmp_path (Path.basic "dfg");
(* need to check here if the directory exists and, if not, create it*)
- val outfile = TextIO.openAppend("thmstring_in_watcher");
+ val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));
val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
val dfg_create =if File.exists dfg_dir
@@ -172,7 +172,7 @@
val settings = getSettings settings []
val (file, rest) = takeUntil "*" rest []
val file = implode file
- val outfile = TextIO.openOut("sep_comms");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));
val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
val _ = TextIO.closeOut outfile
@@ -248,7 +248,7 @@
-fun setupWatcher (the_goal) = let
+fun setupWatcher () = let
(** pipes for communication between parent and watcher **)
val p1 = Posix.IO.pipe ()
val p2 = Posix.IO.pipe ()
@@ -275,10 +275,10 @@
val fromParentIOD = Posix.FileSys.fdToIOD fromParent
val fromParentStr = openInFD ("_exec_in_parent", fromParent)
val toParentStr = openOutFD ("_exec_out_parent", toParent)
- val goalstr = string_of_thm (the_goal)
- val outfile = TextIO.openOut("goal_in_watcher");
+ (*val goalstr = string_of_thm (the_goal)
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
val _ = TextIO.output (outfile,goalstr )
- val _ = TextIO.closeOut outfile
+ val _ = TextIO.closeOut outfile*)
fun killChildren [] = ()
| killChildren (childPid::children) = (killChild childPid; killChildren children)
@@ -354,7 +354,7 @@
val prover = cmdProver childProc
val thmstring = cmdThm childProc
val goalstring = cmdGoal childProc
- val outfile = TextIO.openOut("child_comms");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));
val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
val _ = TextIO.closeOut outfile
in
@@ -362,7 +362,7 @@
then
(* check here for prover label on child*)
- let val outfile = TextIO.openOut("child_incoming");
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
val _ = TextIO.closeOut outfile
val childDone = (case prover of
@@ -385,7 +385,7 @@
(childProc::(checkChildren (otherChildren, toParentStr)))
end
else
- let val outfile = TextIO.openAppend("child_incoming");
+ let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
val _ = TextIO.output (outfile,"No child output " )
val _ = TextIO.closeOut outfile
in
@@ -578,7 +578,7 @@
(**********************************************************)
fun killWatcher pid= killChild pid;
-fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
+fun createWatcher () = let val mychild = childInfo (setupWatcher())
val streams =snd mychild
val childin = fst streams
val childout = snd streams
@@ -590,7 +590,7 @@
(* fun spass_proofHandler (n:int) = (
let val (reconstr, thmstring, goalstring) = getSpassInput childin
- val outfile = TextIO.openOut("foo_signal");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
val _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring))
val _ = TextIO.closeOut outfile
@@ -605,12 +605,12 @@
(*
fun spass_proofHandler (n:int) = (
- let val outfile = TextIO.openOut("foo_signal1");
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
val _ = TextIO.closeOut outfile
val (reconstr, thmstring, goalstring) = getSpassInput childin
- val outfile = TextIO.openOut("foo_signal");
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
val _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring^goalstring))
val _ = TextIO.closeOut outfile
@@ -637,11 +637,11 @@
*)
fun spass_proofHandler (n:int) = (
- let val outfile = TextIO.openOut("foo_signal1");
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
val _ = TextIO.output (outfile, ("In signal handler now\n"))
val _ = TextIO.closeOut outfile
val (reconstr, thmstring, goalstring) = getSpassInput childin
- val outfile = TextIO.openAppend("foo_signal");
+ val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
val _ = TextIO.closeOut outfile
@@ -658,7 +658,7 @@
if ((!goals_being_watched) = 0)
then
- (let val outfile = TextIO.openOut("foo_reap_found");
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
in
@@ -677,7 +677,7 @@
Pretty.writeln(Pretty.str (oct_char "361"));
if (!goals_being_watched = 0)
then
- (let val outfile = TextIO.openOut("foo_reap_comp");
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
in
@@ -696,7 +696,7 @@
Pretty.writeln(Pretty.str (oct_char "361"));
if (!goals_being_watched = 0)
then
- (let val outfile = TextIO.openOut("foo_reap_comp");
+ (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
val _ = TextIO.closeOut outfile
in
--- a/src/HOL/Tools/ATP/watcher.sig Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.sig Wed Apr 06 12:01:37 2005 +0200
@@ -37,7 +37,7 @@
(* Start a watcher and set up signal handlers *)
(**********************************************************)
-val createWatcher : thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
+val createWatcher : unit -> TextIO.instream * TextIO.outstream * Posix.Process.pid