# HG changeset patch # User quigley # Date 1112781697 -7200 # Node ID 2edb384bf61fd2d7ad8d4df366415736d2498905 # Parent bd946fbc7c2bbbb82860226c5a55690209b93345 watcher.ML and watcher.sig changed. Debug files now write to tmp. diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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_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 diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/recon_translate_proof.ML --- 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 diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/remchars.pl --- /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 () +{ + + #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"; diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/watcher.ML --- 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 diff -r bd946fbc7c2b -r 2edb384bf61f src/HOL/Tools/ATP/watcher.sig --- 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