--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,260 @@
+(* Title: SpassCommunication.ml
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
+(***************************************************************************)
+(* Code to deal with the transfer of proofs from a Spass process *)
+(***************************************************************************)
+
+(***********************************)
+(* Write Spass output to a file *)
+(***********************************)
+
+fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr
+ in if thisLine = "--------------------------SPASS-STOP------------------------------\n"
+ then TextIO.output (fd, thisLine)
+ else (
+ TextIO.output (fd, thisLine); logSpassInput (instr,fd))
+ end;
+
+
+(**********************************************************************)
+(* Reconstruct the Spass proof w.r.t. thmstring (string version of *)
+(* Isabelle goal to be proved), then transfer the reconstruction *)
+(* steps as a string to the input pipe of the main Isabelle process *)
+(**********************************************************************)
+
+
+
+fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let
+ val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
+ then (
+ let val proofextract = extract_proof (currentString^thisLine)
+ val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
+ val foo = TextIO.openOut "foobar2";
+ in
+ TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
+
+ TextIO.output (toParent, reconstr^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thmstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ OS.Process.sleep(Time.fromSeconds 1)
+
+ end
+
+ )
+ else (
+
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine))
+ )
+ end;
+
+
+
+(*********************************************************************************)
+(* Inspect the output of a Spass process to see if it has found a proof, *)
+(* and if so, transfer output to the input pipe of the main Isabelle process *)
+(*********************************************************************************)
+
+
+fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) =
+ (*let val _ = Posix.Process.wait ()
+ in*)
+ if (isSome (TextIO.canInput(fromChild, 5)))
+ then
+ (
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if (String.isPrefix "Here is a proof" thisLine )
+ then
+ (
+
+
+ transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine);
+ true)
+
+ else
+ (
+ startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd)
+ )
+ end
+ )
+ else (false)
+ (* end*)
+
+fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) =
+ let val spass_proof_file = TextIO.openAppend("spass_proof")
+ val outfile = TextIO.openOut("foo_checkspass");
+ val _ = TextIO.output (outfile, "checking proof found")
+
+ val _ = TextIO.closeOut outfile
+ in
+ if (isSome (TextIO.canInput(fromChild, 5)))
+ then
+ (
+ let val thisLine = TextIO.inputLine fromChild
+ in if ( thisLine = "SPASS beiseite: Proof found.\n" )
+ then
+ (
+ let val outfile = TextIO.openOut("foo_proof"); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ val _ = TextIO.output (outfile, (thisLine))
+
+ val _ = TextIO.closeOut outfile
+ in
+ startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd)
+ end
+ )
+ else if (thisLine= "SPASS beiseite: Completion found.\n" )
+ then
+
+ (
+ let val outfile = TextIO.openOut("foo_proof"); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ val _ = TextIO.output (outfile, (thisLine))
+
+ val _ = TextIO.closeOut outfile
+ in
+
+ (*TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;*)
+ TextIO.output (spass_proof_file, (thisLine));
+ TextIO.flushOut spass_proof_file;
+ TextIO.closeOut spass_proof_file;
+ (*TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, "bar\n");
+ TextIO.flushOut toParent;*)
+
+ TextIO.output (toParent, thisLine^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thmstring^"\n");
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, goalstring^"\n");
+ TextIO.flushOut toParent;
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ (* Attempt to prevent several signals from turning up simultaneously *)
+ OS.Process.sleep(Time.fromSeconds 1);
+ true
+ end)
+ else if ( thisLine = "SPASS beiseite: Ran out of time.\n" )
+ then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ true)
+ else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" ) then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ true)
+ else
+ (TextIO.output (spass_proof_file, (thisLine));
+ TextIO.flushOut spass_proof_file;
+ checkSpassProofFound (fromChild, toParent, ppid, thmstring,goalstring,childCmd))
+
+ end
+ )
+ else
+ (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
+ end
+
+
+(***********************************************************************)
+(* Function used by the Isabelle process to read in a spass proof *)
+(***********************************************************************)
+
+
+(***********************************************************************)
+(* Function used by the Isabelle process to read in a vampire proof *)
+(***********************************************************************)
+
+(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr
+ in
+ if (thisLine = "%============== End of proof. ==================\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Unprovable.\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Proof not found.\n")
+ then
+ (
+ Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
+ )
+
+
+ else
+ (
+ Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
+ )
+ end;
+
+*)
+
+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 _ = TextIO.closeOut outfile
+ in
+ if ( (substring (thisLine, 0,1))= "[")
+ then
+ (*Pretty.writeln(Pretty.str (thisLine))*)
+ let val reconstr = thisLine
+ val thmstring = TextIO.inputLine instr
+ val goalstring = TextIO.inputLine instr
+ in
+ (reconstr, thmstring, goalstring)
+ end
+ else if (thisLine = "SPASS beiseite: Completion found.\n" )
+ then
+ (
+ let val reconstr = thisLine
+ val thmstring = TextIO.inputLine instr
+ val goalstring = TextIO.inputLine instr
+ in
+ (reconstr, thmstring, goalstring)
+ end
+ )
+ else if (thisLine = "Proof found but translation failed!")
+ then
+ (
+ let val reconstr = thisLine
+ val thmstring = TextIO.inputLine instr
+ val goalstring = TextIO.inputLine instr
+ val outfile = TextIO.openOut("foo_getSpass");
+ val _ = TextIO.output (outfile, (thisLine))
+ val _ = TextIO.closeOut outfile
+ in
+ (reconstr, thmstring, goalstring)
+ end
+ )
+ else
+ getSpassInput instr
+
+ end
+ else
+ ("No output from Spass.\n","","")
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/VampireCommunication.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,117 @@
+(* Title: VampireCommunication.ml
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
+(***************************************************************************)
+(* Code to deal with the transfer of proofs from a Vampire process *)
+(***************************************************************************)
+
+(***********************************)
+(* Write vampire output to a file *)
+(***********************************)
+
+fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr
+ in if thisLine = "%============== End of proof. ==================\n"
+ then TextIO.output (fd, thisLine)
+ else (
+ TextIO.output (fd, thisLine); logVampInput (instr,fd))
+ end;
+
+(**********************************************************************)
+(* Transfer the vampire output from the watcher to the input pipe of *)
+(* the main Isabelle process *)
+(**********************************************************************)
+
+fun transferVampInput (fromChild, toParent, ppid) = let
+ val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "%============== End of proof. ==================\n" )
+ then (
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent
+ )
+ else (
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ transferVampInput (fromChild, toParent, ppid)
+ )
+ end;
+
+
+(*********************************************************************************)
+(* Inspect the output of a vampire process to see if it has found a proof, *)
+(* and if so, transfer output to the input pipe of the main Isabelle process *)
+(*********************************************************************************)
+
+fun startVampireTransfer (fromChild, toParent, ppid, childCmd) =
+ if (isSome (TextIO.canInput(fromChild, 5)))
+ then
+ (
+ let val thisLine = TextIO.inputLine fromChild
+ in
+ if (thisLine = "% Proof found. Thanks to Tanya!\n" )
+ then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ transferVampInput (fromChild, toParent, ppid);
+ true)
+ else if (thisLine = "% Unprovable.\n" )
+ then
+ (
+ Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+ TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+
+ true)
+ else if (thisLine = "% Proof not found.\n")
+ then
+ (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1); TextIO.output (toParent,childCmd^"\n" );
+ TextIO.flushOut toParent;
+ TextIO.output (toParent, thisLine);
+ TextIO.flushOut toParent;
+ true)
+ else
+ (
+ startVampireTransfer (fromChild, toParent, ppid, childCmd)
+ )
+ end
+ )
+ else (false)
+
+
+(***********************************************************************)
+(* Function used by the Isabelle process to read in a vampire proof *)
+(***********************************************************************)
+
+fun getVampInput instr = let val thisLine = TextIO.inputLine instr
+ in
+ if (thisLine = "%============== End of proof. ==================\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Unprovable.\n" )
+ then
+ (
+ (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+ )
+ else if (thisLine = "% Proof not found.\n")
+ then
+ (
+ Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
+ )
+
+
+ else
+ (
+ Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
+ )
+ end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/modUnix.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,295 @@
+
+(****************************************************************)
+(****** Slightly modified version of sml Unix structure *********)
+(****************************************************************)
+
+type signal = Posix.Signal.signal
+datatype exit_status = datatype Posix.Process.exit_status
+
+val fromStatus = Posix.Process.fromStatus
+
+
+
+(* Internal function - inverse of Posix.Process.fromStatus. *)
+local
+ val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific
+ in
+ fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0))
+ | toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w))
+ | toStatus(W_SIGNALED s) =
+ doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s)))
+ | toStatus(W_STOPPED s) =
+ doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s)))
+ end
+
+(* fun reap{pid, infd, outfd} =
+ let
+ val u = Posix.IO.close infd;
+ val u = Posix.IO.close outfd;
+ val (_, status) =
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
+ in
+ toStatus status
+ end
+
+*)
+
+ fun reap(pid, instr, outstr) =
+ let
+ val u = TextIO.closeIn instr;
+ val u = TextIO.closeOut outstr;
+
+ val (_, status) =
+ Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
+ in
+ toStatus status
+ end
+
+fun fdReader (name : string, fd : Posix.IO.file_desc) =
+ Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
+
+fun fdWriter (name, fd) =
+ Posix.IO.mkWriter {
+ appendMode = false,
+ initBlkMode = true,
+ name = name,
+ chunkSize=4096,
+ fd = fd
+ };
+
+fun openOutFD (name, fd) =
+ TextIO.mkOutstream (
+ TextIO.StreamIO.mkOutstream (
+ fdWriter (name, fd), IO.BLOCK_BUF));
+
+fun openInFD (name, fd) =
+ TextIO.mkInstream (
+ TextIO.StreamIO.mkInstream (
+ fdReader (name, fd), ""));
+
+
+
+
+
+(*****************************************)
+(* The result of calling createWatcher *)
+(*****************************************)
+
+datatype proc = PROC of {
+ pid : Posix.Process.pid,
+ instr : TextIO.instream,
+ outstr : TextIO.outstream
+ };
+
+
+
+(*****************************************)
+(* The result of calling executeToList *)
+(*****************************************)
+
+datatype cmdproc = CMDPROC of {
+ prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *)
+ cmd: string, (* The file containing the goal for res prover to prove *)
+ thmstring: string, (* string representation of subgoal after negation, skolemization*)
+ goalstring: string, (* string representation of subgoal*)
+ pid : Posix.Process.pid,
+ instr : TextIO.instream, (* Input stream to child process *)
+ outstr : TextIO.outstream (* Output stream from child process *)
+ };
+
+
+
+fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
+
+fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr)));
+
+fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
+
+fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
+
+fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr))));
+
+fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (pid);
+
+fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover);
+
+fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (thmstring);
+
+fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (goalstring);
+(***************************************************************************)
+(* Takes a command - e.g. 'vampire', a list of arguments for the command, *)
+(* and a list of currently running processes. Creates a new process for *)
+(* cmd and argv and adds it to procList *)
+(***************************************************************************)
+
+
+
+
+fun mySshExecuteToList (cmd, argv, procList) = let
+ val p1 = Posix.IO.pipe ()
+ val p2 = Posix.IO.pipe ()
+ val prover = hd argv
+ val thmstring = hd(tl argv)
+ val goalstring = hd(tl(tl argv))
+ val argv = tl (tl argv)
+
+ (* Turn the arguments into a single string. Perhaps we should quote the
+ arguments. *)
+ fun convArgs [] = []
+ | convArgs [s] = [s]
+ | convArgs (hd::tl) = hd :: " " :: convArgs tl
+ val cmd_args = concat(convArgs(cmd :: argv))
+
+ fun closep () = (
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p2)
+ )
+ fun startChild () =(case Posix.Process.fork()
+ of SOME pid => pid (* parent *)
+ | NONE => let
+ val oldchildin = #infd p1
+ val newchildin = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val newchildout = Posix.FileSys.wordToFD 0w1
+ (*val args = (["shep"]@([cmd]@argv))
+ val newcmd = "/usr/bin/ssh"*)
+
+ in
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = newchildin};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = newchildout};
+ Posix.IO.close oldchildout;
+ (* Run the command. *)
+ (* Run this as a shell command. The command and arguments have
+ to be a single argument. *)
+ Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args])
+ (*Posix.Process.exec(newcmd, args)*)
+ end
+ (* end case *))
+ val _ = TextIO.flushOut TextIO.stdOut
+ val pid = (startChild ()) handle ex => (closep(); raise ex)
+ val instr = openInFD ("_exec_in", #infd p2)
+ val outstr = openOutFD ("_exec_out", #outfd p1)
+ val cmd = hd (rev argv)
+ in
+ (* close the child-side fds *)
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ (((CMDPROC{
+ prover = prover,
+ cmd = cmd,
+ thmstring = thmstring,
+ goalstring = goalstring,
+ pid = pid,
+ instr = instr,
+ outstr = outstr
+ })::procList))
+ end;
+
+
+fun myexecuteInEnv (cmd, argv, env) = let
+ val p1 = Posix.IO.pipe ()
+ val p2 = Posix.IO.pipe ()
+ fun closep () = (
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p2)
+ )
+ fun startChild () =(case Posix.Process.fork()
+ of SOME pid => pid (* parent *)
+ | NONE => let
+ val oldchildin = #infd p1
+ val newchildin = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val newchildout = Posix.FileSys.wordToFD 0w1
+ in
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = newchildin};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = newchildout};
+ Posix.IO.close oldchildout;
+ Posix.Process.exece(cmd, argv, env)
+ end
+ (* end case *))
+ val _ = TextIO.flushOut TextIO.stdOut
+ val pid = (startChild ()) handle ex => (closep(); raise ex)
+ val instr = openInFD ("_exec_in", #infd p2)
+ val outstr = openOutFD ("_exec_out", #outfd p1)
+ in
+ (* close the child-side fds *)
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ PROC{pid = pid,
+ instr = instr,
+ outstr = outstr
+ }
+ end;
+
+
+
+
+fun myexecuteToList (cmd, argv, procList) = let
+ val p1 = Posix.IO.pipe ()
+ val p2 = Posix.IO.pipe ()
+ val prover = hd argv
+ val thmstring = hd(tl argv)
+ val goalstring = hd(tl(tl argv))
+ val argv = tl (tl (tl(argv)))
+
+ fun closep () = (
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p2)
+ )
+ fun startChild () =(case Posix.Process.fork()
+ of SOME pid => pid (* parent *)
+ | NONE => let
+ val oldchildin = #infd p1
+ val newchildin = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val newchildout = Posix.FileSys.wordToFD 0w1
+ in
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = newchildin};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = newchildout};
+ Posix.IO.close oldchildout;
+ Posix.Process.exec(cmd, argv)
+ end
+ (* end case *))
+ val _ = TextIO.flushOut TextIO.stdOut
+ val pid = (startChild ()) handle ex => (closep(); raise ex)
+ val instr = openInFD ("_exec_in", #infd p2)
+ val outstr = openOutFD ("_exec_out", #outfd p1)
+ val cmd = hd (rev argv)
+ in
+ (* close the child-side fds *)
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ (((CMDPROC{
+ prover = prover,
+ cmd = cmd,
+ thmstring = thmstring,
+ goalstring = goalstring,
+ pid = pid,
+ instr = instr,
+ outstr = outstr
+ })::procList))
+ end;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_gandalf_base.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,38 @@
+(* Auxiliary functions *)
+
+exception Assertion of string;
+
+val DEBUG = ref true;
+fun TRACE s = if !DEBUG then print s else ();
+
+fun id x = x;
+fun K x y = x;
+
+exception Noassoc;
+fun assoc a [] = raise Noassoc
+ | assoc a ((x, y)::t) = if a = x then y else assoc a t;
+fun assoc_exists a [] = false
+ | assoc_exists a ((x, y)::t) = if a = x then true else assoc_exists a t;
+fun assoc_update (a, b) [] = raise Noassoc
+ | assoc_update (a, b) ((x, y)::t)
+ = if a = x then (a, b)::t else (x, y)::(assoc_update (a, b) t)
+fun assoc_inv a [] = raise Noassoc
+ | assoc_inv a ((x, y)::t) = if a = y then x else assoc a t;
+fun assoc_inv_exists a [] = false
+ | assoc_inv_exists a ((x, y)::t) = if a = y then true else assoc_inv_exists a t;
+
+fun is_mem x [] = false
+ | is_mem x (h::t) = (x = h) orelse is_mem x t;
+fun elt 0 (h::t) = h
+ | elt n (h::t) = elt (n - 1) t
+ | elt n l = raise (Assertion "elt: out of range");
+fun remove_elt _ [] = raise (Assertion "remove_elt: out of range")
+ | remove_elt 0 (h::t) = t
+ | remove_elt n (h::t) = h::(remove_elt (n - 1) t);
+fun elt_num x [] = raise (Assertion "elt_num: not in list")
+ | elt_num x (h::t) = if h = x then 0 else 1 + elt_num x t;
+fun set_add x l = if is_mem x l then l else x::l;
+
+fun iter f a [] = a
+ | iter f a (h::t) = f h (iter f a t);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,492 @@
+
+
+(*----------------------------------------------*)
+(* Reorder clauses for use in binary resolution *)
+(*----------------------------------------------*)
+fun take n [] = []
+| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
+
+fun drop n [] = []
+| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
+
+fun remove n [] = []
+| remove n (x::xs) = List.filter (not_equal n) (x::xs);
+
+fun remove_nth n [] = []
+| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
+
+fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
+
+
+ fun literals (Const("Trueprop",_) $ P) = literals P
+ | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
+ | literals (Const("Not",_) $ P) = [(false,P)]
+ | literals P = [(true,P)];
+
+ (*number of literals in a term*)
+ val nliterals = length o literals;
+
+exception Not_in_list;
+
+
+
+
+ (* get the literals from a disjunctive clause *)
+
+(*fun get_disj_literals t = if is_disj t then
+ let
+ val {disj1, disj2} = dest_disj t
+ in
+ disj1::(get_disj_literals disj2)
+ end
+ else
+ ([t])
+
+*)
+
+(*
+(* gives horn clause with kth disj as concl (starting at 1) *)
+fun rots (0,th) = (Meson.make_horn Meson.crules th)
+ | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
+
+
+
+Goal " (~~P) == P";
+by Auto_tac;
+qed "notnotEq";
+
+Goal "A | A ==> A";
+by Auto_tac;
+qed "rem_dup_disj";
+
+
+
+
+(* New Meson code Versions of make_neg_rule and make_pos_rule that don't insert new *)
+(* assumptions, for ordinary resolution. *)
+
+
+
+
+ val not_conjD = thm "meson_not_conjD";
+ val not_disjD = thm "meson_not_disjD";
+ val not_notD = thm "meson_not_notD";
+ val not_allD = thm "meson_not_allD";
+ val not_exD = thm "meson_not_exD";
+ val imp_to_disjD = thm "meson_imp_to_disjD";
+ val not_impD = thm "meson_not_impD";
+ val iff_to_disjD = thm "meson_iff_to_disjD";
+ val not_iffD = thm "meson_not_iffD";
+ val conj_exD1 = thm "meson_conj_exD1";
+ val conj_exD2 = thm "meson_conj_exD2";
+ val disj_exD = thm "meson_disj_exD";
+ val disj_exD1 = thm "meson_disj_exD1";
+ val disj_exD2 = thm "meson_disj_exD2";
+ val disj_assoc = thm "meson_disj_assoc";
+ val disj_comm = thm "meson_disj_comm";
+ val disj_FalseD1 = thm "meson_disj_FalseD1";
+ val disj_FalseD2 = thm "meson_disj_FalseD2";
+
+
+ fun literals (Const("Trueprop",_) $ P) = literals P
+ | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
+ | literals (Const("Not",_) $ P) = [(false,P)]
+ | literals P = [(true,P)];
+
+ (*number of literals in a term*)
+ val nliterals = length o literals;
+
+exception Not_in_list;
+
+
+(*Permute a rule's premises to move the i-th premise to the last position.*)
+fun make_last i th =
+ let val n = nprems_of th
+ in if 1 <= i andalso i <= n
+ then Thm.permute_prems (i-1) 1 th
+ else raise THM("make_last", i, [th])
+ end;
+
+(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+ double-negations.*)
+val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+
+(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
+fun select_literal i cl = negate_head (make_last i cl);
+
+
+(* get a meta-clause for resolution with correct order of literals *)
+fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
+ val contra = if lits = 1
+ then
+ th
+ else
+ rots (n,th)
+ in
+ if lits = 1
+ then
+
+ contra
+ else
+ rotate_prems (lits - n) contra
+ end
+
+
+
+
+
+
+
+fun zip xs [] = []
+| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
+
+
+fun unzip [] = ([],[])
+ | unzip((x,y)::pairs) =
+ let val (xs,ys) = unzip pairs
+ in (x::xs, y::ys) end;
+
+fun numlist 0 = []
+| numlist n = (numlist (n - 1))@[n]
+
+
+fun is_abs t = can dest_abs t;
+fun is_comb t = can dest_comb t;
+
+fun iscomb a = if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if is_conj a then
+ false
+ else if is_disj a then
+ false
+ else if is_forall a then
+ false
+ else if is_exists a then
+ false
+ else
+ true;
+
+
+
+
+fun last(x::xs) = if xs=[] then x else last xs
+fun butlast []= []
+| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
+
+
+fun minus a b = b - a;
+
+
+
+
+(* gives meta clause with kth disj as concl (starting at 1) *)
+(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules th)
+ | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
+
+
+(* get a meta-clause for resolution with correct order of literals *)
+fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
+ val contra = if lits = 1
+ then
+ th
+ else
+ rots (n,th)
+ in
+ if lits = 1
+ then
+
+ contra
+ else
+ rotate_prems (lits - n) contra
+ end
+*)
+
+
+
+
+fun zip xs [] = []
+| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
+
+
+fun unzip [] = ([],[])
+ | unzip((x,y)::pairs) =
+ let val (xs,ys) = unzip pairs
+ in (x::xs, y::ys) end;
+
+fun numlist 0 = []
+| numlist n = (numlist (n - 1))@[n]
+
+
+fun is_abs t = can dest_abs t;
+fun is_comb t = can dest_comb t;
+
+fun iscomb a = if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if is_conj a then
+ false
+ else if is_disj a then
+ false
+ else if is_forall a then
+ false
+ else if is_exists a then
+ false
+ else
+ true;
+
+
+
+
+fun last(x::xs) = if xs=[] then x else last xs
+fun butlast []= []
+| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
+
+
+fun minus a b = b - a;
+
+
+(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
+
+fun assoc3 a [] = raise Noassoc
+ | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
+
+
+fun third (a,b,c) = c;
+
+
+ fun takeUntil ch [] res = (res, [])
+ | takeUntil ch (x::xs) res = if x = ch
+ then
+ (res, xs)
+ else
+ takeUntil ch xs (res@[x])
+fun contains_eq str = inlist "=" str
+
+fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
+ in
+ if ((last uptoeq) = "~")
+ then
+ false
+ else
+ true
+ end
+
+
+
+
+fun get_eq_strs str = if eq_not_neq str (*not an inequality *)
+ then
+ let val (left, right) = takeUntil "=" str []
+ in
+ ((butlast left), (drop 1 right))
+ end
+ else (* is an inequality *)
+ let val (left, right) = takeUntil "~" str []
+ in
+ ((butlast left), (drop 2 right))
+ end
+
+
+
+fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
+ val (x_lhs, x_rhs) = get_eq_strs x
+
+ in
+ (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
+ end
+
+fun equal_pair (a,b) = equal a b
+
+fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
+
+fun var_equiv vars (a,b) = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
+
+fun all_true [] = false
+| all_true xs = let val falselist = List.filter (equal false ) xs
+ in
+ falselist = []
+ end
+
+
+
+fun var_pos_eq vars x y = let val xs = explode x
+ val ys = explode y
+ in
+ if not_equal (length xs) (length ys)
+ then
+ false
+ else
+ let val xsys = zip xs ys
+ val are_var_pairs = map (var_equiv vars) xsys
+ in
+ all_true are_var_pairs
+ end
+ end
+
+
+
+
+fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) = raise Not_in_list
+ |pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) =
+ let val y = explode x
+ val b = explode a
+ in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (contains_eq b) andalso (contains_eq y)
+ then
+ if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
+ if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ raise Not_in_list
+ else
+ raise Not_in_list
+
+ end
+
+ | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) =
+ let val y = explode x
+ val b = explode a
+ in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+
+ else
+ if (var_pos_eq allvars a x) (* Equal apart from meta-vars having different names *)
+ then
+ (pos_num, symlist, nsymlist)
+ else
+ if (contains_eq b) andalso (contains_eq y)
+ then
+ if (eq_not_neq b) andalso (eq_not_neq y) andalso (switch_equal b y ) (* both are equalities and equal under sym*)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *) else
+ if not(eq_not_neq b) andalso not(eq_not_neq y) andalso (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
+
+ end
+
+
+
+
+
+
+
+ (* in
+ if b = y
+ then
+ (pos_num, symlist, nsymlist)
+ else if (contains_eq b) andalso (contains_eq y)
+ then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
+ then if (switch_equal b y ) (* if they're equal under sym *)
+ then
+ (pos_num, (pos_num::symlist), nsymlist) (* add pos to symlist *)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else if not(eq_not_neq b) andalso not(eq_not_neq y) (* both are inequalities *)
+ then if (switch_equal b y ) (* if they're equal under not_sym *)
+ then
+ (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ else
+ pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
+ end
+
+ *)
+
+
+
+
+
+
+
+
+
+
+(* checkorder Spass Isabelle [] *)
+
+fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
+| checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =
+ let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist)
+ in
+ checkorder xs strlist allvars ((numlist@[posnum]), symlist', not_symlist')
+ end
+
+fun is_digit ch =
+ ( ch >= "0" andalso ch <= "9")
+
+
+fun is_alpha ch =
+ (ch >= "A" andalso ch <= "Z") orelse
+ (ch >= "a" andalso ch <= "z")
+
+
+fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
+
+fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
+ val exp_term = explode termstr
+ in
+ implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
+ end
+
+fun get_meta_lits thm = map lit_string (prems_of thm)
+
+
+
+
+fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
+
+fun lit_string_bracket t = let val termstr = (Sign.string_of_term Mainsign ) t
+ val exp_term = explode termstr
+ in
+ implode(List.filter is_alpha_space_or_neg_or_eq_or_bracket exp_term)
+ end
+
+fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
+
+
+
+
+fun apply_rule rule [] thm = thm
+| apply_rule rule (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
+ in
+ apply_rule rule xs thm'
+ end
+
+
+
+ (* resulting thm, clause-strs in spass order, vars *)
+
+fun rearrange_clause thm res_strlist allvars =
+ let val isa_strlist = get_meta_lits thm
+ val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
+ val symmed = apply_rule sym symlist thm
+ val not_symmed = apply_rule not_sym not_symlist symmed
+
+ in
+ ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
+ end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_parse.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,482 @@
+(*use "Translate_Proof";*)
+(* Parsing functions *)
+
+(* Auxiliary functions *)
+
+exception ASSERTION of string;
+
+exception NOPARSE_WORD
+exception NOPARSE_NUM
+fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
+
+fun string2int s =
+ let
+ val io = Int.fromString s
+ in
+ case io of
+ (SOME i) => i
+ | _ => raise ASSERTION "string -> int failed"
+ end
+
+(* Parser combinators *)
+
+exception Noparse;
+exception SPASSError of string;
+
+fun ++ (parser1, parser2) input =
+ let
+ val (result1, rest1) = parser1 input
+ val (result2, rest2) = parser2 rest1
+ in
+ ((result1, result2), rest2)
+ end;
+
+fun many parser input =
+ let (* Tree * token list*)
+ val (result, next) = parser input
+ val (results, rest) = many parser next
+ in
+ ((result::results), rest)
+ end
+ handle Noparse => ([], input)
+| NOPARSE_WORD => ([], input)
+| NOPARSE_NUM => ([], input);
+
+
+
+fun >> (parser, treatment) input =
+ let
+ val (result, rest) = parser input
+ in
+ (treatment result, rest)
+ end;
+
+fun || (parser1, parser2) input = parser1 input
+handle Noparse => parser2 input;
+
+infixr 8 ++; infixr 7 >>; infixr 6 ||;
+
+fun some p [] = raise Noparse
+ | some p (h::t) = if p h then (h, t) else raise Noparse;
+
+fun a tok = some (fn item => item = tok);
+
+fun finished input = if input = [] then (0, input) else raise Noparse;
+
+
+
+
+
+ (* Parsing the output from gandalf *)
+datatype token = Word of string
+ | Number of int
+ | Other of string
+
+
+ exception NOCUT
+ fun is_prefix [] l = true
+ | is_prefix (h::t) [] = false
+ | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
+ fun remove_prefix [] l = l
+ | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
+ | remove_prefix (h::t) (h'::t') = remove_prefix t t'
+ fun ccut t [] = raise NOCUT
+ | ccut t s =
+ if is_prefix t s then ([], remove_prefix t s) else
+ let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
+ fun cut t s =
+ let
+ val t' = explode t
+ val s' = explode s
+ val (a, b) = ccut t' s'
+ in
+ (implode a, implode b)
+ end
+
+ fun cut_exists t s
+ = let val (a, b) = cut t s in true end handle NOCUT => false
+
+ fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
+ fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
+
+
+ fun kill_lines 0 = id
+ | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
+
+ (*fun extract_proof s
+ = if cut_exists "EMPTY CLAUSE DERIVED" s then
+ (kill_lines 6
+ o snd o cut_after "EMPTY CLAUSE DERIVED"
+ o fst o cut_after "contradiction.\n") s
+ else
+ raise (GandalfError "Couldn't find a proof.")
+*)
+
+val proofstring =
+"0:00:00.00 for the reduction.\
+\\
+\Here is a proof with depth 3, length 7 :\
+\1[0:Inp] || -> P(xa)*.\
+\2[0:Inp] || -> Q(xb)*.\
+\3[0:Inp] || R(U)* -> .\
+\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
+\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
+\11[0:Res:2.0,9.0] || P(U)* -> .\
+\12[0:Res:1.0,11.0] || -> .\
+\Formulae used in the proof :\
+\\
+\--------------------------SPASS-STOP------------------------------"
+
+
+fun extract_proof s
+ = if cut_exists "Here is a proof with" s then
+ (kill_lines 0
+ o snd o cut_after ":"
+ o snd o cut_after "Here is a proof with"
+ o fst o cut_after " || -> .") s
+ else
+ raise SPASSError "Couldn't find a proof."
+
+
+
+fun several p = many (some p)
+ fun collect (h, t) = h ^ (itlist (fn s1 => fn s2 => s1 ^ s2) t "")
+
+ fun lower_letter s = ("a" <= s) andalso (s <= "z")
+ fun upper_letter s = ("A" <= s) andalso (s <= "Z")
+ fun digit s = ("0" <= s) andalso (s <= "9")
+ fun letter s = lower_letter s orelse upper_letter s
+ fun alpha s = letter s orelse (s = "_")
+ fun alphanum s = alpha s orelse digit s
+ fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
+ (* FIX this is stopping it picking up numbers *)
+ val word = (some alpha ++ several alphanum) >> (Word o collect)
+ val number =
+ (some digit ++ several digit) >> (Number o string2int o collect)
+ val other = some (K true) >> Other
+
+ val token = (word || number || other) ++ several space >> fst
+ val tokens = (several space ++ many token) >> snd
+ val alltokens = (tokens ++ finished) >> fst
+
+ (* val lex = fst ( alltokens ( (map str) explode))*)
+ fun lex s = alltokens (explode s)
+
+datatype Tree = Leaf of string
+ | Branch of Tree * Tree
+
+
+
+
+ fun number ((Number n)::rest) = (n, rest)
+ | number _ = raise NOPARSE_NUM
+ fun word ((Word w)::rest) = (w, rest)
+ | word _ = raise NOPARSE_WORD
+
+ fun other_char ( (Other p)::rest) = (p, rest)
+ | other_char _ =raise NOPARSE_WORD
+
+ val number_list =
+ (number ++ many number)
+ >> (fn (a, b) => (a::b))
+
+ val term_num =
+ (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
+
+ val axiom = (a (Word "Inp"))
+ >> (fn (_) => Axiom)
+
+
+ val binary = (a (Word "Res")) ++ (a (Other ":"))
+ ++ term_num ++ (a (Other ","))
+ ++ term_num
+ >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
+
+
+
+ val factor = (a (Word "Fac")) ++ (a (Other ":"))
+ ++ term_num ++ (a (Other ","))
+ ++ term_num
+ >> (fn (_, (_, (c, (_, e)))) => Factor ((fst c), (snd c),(snd e)))
+
+ val para = (a (Word "SPm")) ++ (a (Other ":"))
+ ++ term_num ++ (a (Other ","))
+ ++ term_num
+ >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
+
+ val rewrite = (a (Word "Rew")) ++ (a (Other ":"))
+ ++ term_num ++ (a (Other ","))
+ ++ term_num
+ >> (fn (_, (_, (c, (_, e)))) => Rewrite (c, e))
+
+
+ val mrr = (a (Word "MRR")) ++ (a (Other ":"))
+ ++ term_num ++ (a (Other ","))
+ ++ term_num
+ >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
+
+
+ val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
+ >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
+
+(*
+ val hyper = a (Word "hyper")
+ ++ many ((a (Other ",") ++ number) >> snd)
+ >> (Hyper o snd)
+*)
+ (* val method = axiom ||binary || factor || para || hyper*)
+
+ val method = axiom || binary || factor || para || rewrite || mrr || obv
+ val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
+ >> (fn (_, (_, a)) => Binary_s a)
+ val factor_s = a (Word "factor_s")
+ >> (fn _ => Factor_s ())
+ val demod_s = a (Word "demod")
+ ++ (many ((a (Other ",") ++ term_num) >> snd))
+ >> (fn (_, a) => Demod_s a)
+
+ val hyper_s = a (Word "hyper_s")
+ ++ many ((a (Other ",") ++ number) >> snd)
+ >> (Hyper_s o snd)
+ val simp_method = binary_s || factor_s || demod_s || hyper_s
+ val simp = a (Other ",") ++ simp_method >> snd
+ val simps = many simp
+
+
+ val justification =
+ a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
+ >> (fn (_,(_, (_,(b, _)))) => b)
+
+
+exception NOTERM
+
+
+fun implode_with_space [] = implode []
+| implode_with_space [x] = implode [x]
+| implode_with_space (x::[y]) = x^" "^y
+| implode_with_space (x::xs) = (x^" "^(implode_with_space xs))
+
+(* FIX - should change the stars and pluses to many rather than explicit patterns *)
+
+(* FIX - add the other things later *)
+fun remove_typeinfo x = if (String.isPrefix "v_" x )
+ then
+ (String.substring (x,2, ((size x) - 2)))
+ else if (String.isPrefix "V_" x )
+ then
+ (String.substring (x,2, ((size x) - 2)))
+ else if (String.isPrefix "typ_" x )
+ then
+ ""
+ else if (String.isPrefix "Typ_" x )
+ then
+ ""
+ else if (String.isPrefix "tconst_" x )
+ then
+ ""
+ else if (String.isPrefix "const_" x )
+ then
+ (String.substring (x,6, ((size x) - 6)))
+ else
+ x
+
+
+fun term input = ( ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) => (a@b))
+ ) input
+
+(* pterms are terms from the rhs of the -> in the spass proof. *)
+(* they should have a "~" in front of them so that they match with *)
+(* positive terms in the meta-clause *)
+(* nterm are terms from the lhs of the spass proof, and shouldn't *)
+(* "~"s added word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) => (a^" "^b)) *)
+
+and pterm input = (
+ peqterm >> (fn (a) => a)
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
+ >> (fn (a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
+ >> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
+ >> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
+ >> (fn (a, (_,(b, (_,_)))) => ("~"^" "^(remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")")
+ >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
+
+ || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
+
+and nterm input =
+
+ (
+ neqterm >> (fn (a) => a)
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
+ >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
+ >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
+ >> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
+ >> (fn ( a, (_,(b, (_,_)))) => ((remove_typeinfo a)^" "^b))
+
+ || word ++ a (Other "(") ++ arglist ++ a (Other ")")
+ >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
+
+ || word >> (fn w => (remove_typeinfo w)) ) input
+
+
+and peqterm input =(
+
+ a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "+")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "*")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*")
+ >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
+
+
+ ||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
+
+
+
+and neqterm input =(
+
+ a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "+")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*") ++ a (Other "*")
+ >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
+
+ || a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ ++ a (Other "*")
+ >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
+
+
+ ||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")")
+ >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
+
+
+
+and ptermlist input = (many pterm
+ >> (fn (a) => (a))) input
+
+and ntermlist input = (many nterm
+ >> (fn (a) => (a))) input
+
+(*and arglist input = ( nterm >> (fn (a) => (a))
+ || nterm ++ many (a (Other ",") ++ nterm >> snd)
+ >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)
+
+and arglist input = ( nterm ++ many (a (Other ",") ++ nterm >> snd)
+ >> (fn (a, b) => (a^" "^(implode_with_space b)))
+ || nterm >> (fn (a) => (a)))input
+
+ val clause = term
+
+ val line = number ++ justification ++ a (Other "|") ++
+ a (Other "|") ++ clause ++ a (Other ".")
+ >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))
+
+ val lines = many line
+ val alllines = (lines ++ finished) >> fst
+
+ val parse = fst o alllines
+ val s = proofstring;
+
+
+
+
+fun dropUntilNot ch [] = ( [])
+ | dropUntilNot ch (x::xs) = if not(x = ch )
+ then
+ (x::xs)
+ else
+ dropUntilNot ch xs
+
+
+
+
+
+fun remove_spaces str [] = str
+| remove_spaces str (x::[]) = if x = " "
+ then
+ str
+ else
+ (str^x)
+| remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
+ val (next) = dropUntilNot " " rest
+ in
+ if next = []
+ then
+ (str^(implode first))
+ else remove_spaces (str^(implode first)^" ") next
+ end
+
+
+fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
+
+
+fun all_spaces xs = List.filter (not_equal " " ) xs
+
+fun just_change_space [] = []
+| just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
+ in
+ if (all_spaces newstrs = [] ) (* all type_info *) then
+ (clausenum, step, newstrs)::(just_change_space xs)
+ else
+ (clausenum, step, newstrs)::(just_change_space xs)
+ end
+
+
+
+
+fun change_space [] = []
+| change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
+ in
+ if (all_spaces newstrs = [] ) (* all type_info *)
+ then
+ (clausenum, step, T_info, newstrs)::(change_space xs)
+ else
+ (clausenum, step, P_info, newstrs)::(change_space xs)
+ end
+
+
+
+
+
+
+(*
+ fun gandalf_parse s =
+ let
+ val e = extract_proof;
+ val t = fst(lex e)
+ val r = parse t
+ in
+ r
+ end
+
+*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,470 @@
+
+open Goals;
+open Unify;
+open USyntax;
+open Utils;
+open Envir;
+open Tfl;
+open Rules;
+
+goal Main.thy "A -->A";
+by Auto_tac;
+qed "foo";
+
+
+val Mainsign = #sign (rep_thm foo);
+
+
+
+(*val myhol = sign_of thy;*)
+
+val myenv = empty 0;
+
+
+val gcounter = ref 0;
+
+exception NOMATES;
+exception UNMATEABLE;
+exception NOTSOME;
+exception UNSPANNED;
+
+fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
+
+fun dest_neg(Const("Not",_) $ M) = M
+ | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
+
+fun is_abs t = can dest_abs t;
+fun is_comb t = can dest_comb t;
+
+fun iscomb a = if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if is_conj a then
+ false
+ else if is_disj a then
+ false
+ else if is_forall a then
+ false
+ else if is_exists a then
+ false
+ else
+ true;
+fun getstring (Var (v,T)) = fst v
+ |getstring (Free (v,T))= v;
+
+
+fun getindexstring ((a:string),(b:int))= a;
+
+fun getstrings (a,b) = let val astring = getstring a
+ val bstring = getstring b in
+ (astring,bstring)
+ end;
+
+
+fun alltrue [] = true
+ |alltrue (true::xs) = true andalso (alltrue xs)
+ |alltrue (false::xs) = false;
+
+fun allfalse [] = true
+ |allfalse (false::xs) = true andalso (allfalse xs)
+ |allfalse (true::xs) = false;
+
+fun not_empty [] = false
+ | not_empty _ = true;
+
+fun twoisvar (a,b) = is_Var b;
+fun twoisfree (a,b) = is_Free b;
+fun twoiscomb (a,b) = iscomb b;
+
+fun strequalfirst a (b,c) = (getstring a) = (getstring b);
+
+fun fstequal a b = a = fst b;
+
+fun takeout (i,[]) = []
+ | takeout (i,(x::xs)) = if (i>0) then
+ (x::(takeout(i-1,xs)))
+ else
+ [];
+
+
+
+(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
+fun is_Abs (Abs _) = true
+ | is_Abs _ = false;
+fun is_Bound (Bound _) = true
+ | is_Bound _ = false;
+
+
+
+
+fun is_hol_tm t =
+ if (is_Free t) then
+ true
+ else if (is_Var t) then
+ true
+ else if (is_Const t) then
+ true
+ else if (is_Abs t) then
+ true
+ else if (is_Bound t) then
+ true
+ else
+ let val (f, args) = strip_comb t in
+ if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then
+ true (* should be is_const *)
+ else
+ false
+ end;
+
+fun is_hol_fm f = if is_neg f then
+ let val newf = dest_neg f in
+ is_hol_fm newf
+ end
+
+ else if is_disj f then
+ let val {disj1,disj2} = dest_disj f in
+ (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *)
+ end
+ else if is_conj f then
+ let val {conj1,conj2} = dest_conj f in
+ (is_hol_fm conj1) andalso (is_hol_fm conj2)
+ end
+ else if (is_forall f) then
+ let val {Body, Bvar} = dest_forall f in
+ is_hol_fm Body
+ end
+ else if (is_exists f) then
+ let val {Body, Bvar} = dest_exists f in
+ is_hol_fm Body
+ end
+ else if (iscomb f) then
+ let val (P, args) = strip_comb f in
+ ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args))
+ end
+ else
+ is_hol_tm f; (* should be is_const, nee
+d to check args *)
+
+
+fun hol_literal t = (is_hol_fm t) andalso ( not ((is_conj t) orelse (is_disj t) orelse (is_forall t) orelse (is_exists t)));
+
+
+
+
+(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
+fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in
+ if (iscomb rand) then
+ getcombvar rand
+ else
+ rand
+ end;
+
+
+
+fun free2var v = let val thing = dest_Free v
+ val (name,vtype) = thing
+ val index = (name,0) in
+ Var (index,vtype)
+ end;
+
+fun var2free v = let val (index, tv) = dest_Var v
+ val istr = fst index in
+ Free (istr,tv)
+ end;
+
+fun inlist v [] = false
+ | inlist v (first::rest) = if first = v then
+ true
+ else inlist v rest;
+
+(*fun in_vars v [] = false
+ | in_vars v ((a,b)::rest) = if v = a then
+ true
+ else if v = b then
+ true
+ else in_vars v rest;*)
+
+fun in_vars v [] = false
+ | in_vars v (a::rest) = if (fst v) = a then
+ true
+
+ else in_vars v rest;
+
+fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
+ true
+ else if (a,b) = (d,c) then
+ true
+ else false;
+
+
+fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of
+ ([],_) => true
+ | _ => false
+
+fun getnewenv thisseq =
+ let val seqlist = Seq.list_of thisseq
+ val envpair =hd seqlist in
+ fst envpair
+ end;
+
+fun getnewsubsts thisseq = let val seqlist = Seq.list_of thisseq
+ val envpair =hd seqlist in
+ snd envpair
+ end;
+
+fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv
+ val envpair = hd seqlist
+ val env = fst envpair
+ val envlist = alist_of env in
+ hd envlist
+ end;
+
+
+fun readenv thisenv = let val envlist = alist_of thisenv in
+
+ hd envlist
+ end;
+
+
+
+
+
+fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
+
+fun oneofthree (a,b,c) = a;
+
+fun twoofthree (a,b,c) = b;
+
+fun threeofthree (a,b,c) = c;
+
+val my_simps = map prover
+ [ "(x=x) = True",
+ "(~ ~ P) = P",
+ "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
+
+ "(P | P) = P", "(P | (P | Q)) = (P | Q)",
+ "((~P) = (~Q)) = (P=Q)" ];
+
+
+(*val myss = HOL_basic_ss addsimps (my_simps@[not_all, not_ex, de_Morgan_conj, de_Morgan_disj, U_def, intersect_def, setEq_def, proposEq_def, hashset_def, subset_def]@ex_simps @ all_simps);
+
+*)
+
+(*--------------------------*)
+(* NNF stuff from meson_tac *)
+(*--------------------------*)
+
+
+(*Prove theorems using fast_tac*)
+fun prove_fun s =
+ prove_goal HOL.thy s
+ (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
+
+(*------------------------------------------------------------------------*)
+(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
+(*------------------------------------------------------------------------*)
+fun mygenvar ty thisenv =
+ let val count = !gcounter
+ val genstring = "GEN"^(string_of_int count)^"VAR" in
+ gcounter := count + 1;
+ genvar genstring (thisenv,ty)
+ end;
+
+fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
+ t
+
+ else if is_forall t then
+ let val {Body, Bvar} = dest_forall t
+ val newvarenv = mygenvar(type_of Bvar) thisenv
+ val newvar = snd(newvarenv)
+ val newbod = subst_free [(Bvar,newvar)] Body
+ val newbod2 = renameBounds newbod thisenv in
+ mk_forall{Body = newbod2, Bvar = newvar}
+ end
+ else if is_exists t then
+ let val {Body, Bvar} =dest_exists t
+ val newvarenv = mygenvar(type_of Bvar) thisenv
+ val newvar = snd(newvarenv)
+ val newbod = subst_free [(Bvar,newvar)] Body
+ val newbod2 = renameBounds newbod thisenv in
+ mk_exists{Body = newbod2, Bvar = newvar}
+ end
+ else if is_conj t then
+ let val {conj1,conj2} = dest_conj t
+ val vpl = renameBounds conj1 thisenv
+ val vpr = renameBounds conj2 thisenv in
+ mk_conj {conj1 = vpl, conj2 = vpr}
+ end
+ else
+ let val {disj1, disj2} = dest_disj t
+ val vpl = renameBounds disj1 thisenv
+ val vpr = renameBounds disj2 thisenv in
+ mk_disj {disj1 = vpl,disj2= vpr}
+ end;
+
+
+(*-----------------*)
+(* from hologic.ml *)
+(*-----------------*)
+val boolT = Type ("bool", []);
+
+val Trueprop = Const ("Trueprop", boolT --> propT);
+
+fun mk_Trueprop P = Trueprop $ P;
+
+fun eq_const T = Const ("op =", [T, T] ---> boolT);
+fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+
+fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+ | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+
+
+(*-----------------------------------------------------------------------*)
+(* Making a THM from a subgoal and other such things *)
+(*-----------------------------------------------------------------------*)
+
+fun thmfromgoal goalnum = let val mygoal = getgoal goalnum
+ val mycgoal = cterm_of Mainsign mygoal in
+ assume mycgoal
+ end;
+
+fun termfromgoal goalnum = let val mygoal = getgoal goalnum
+ val {Rand = myra, Rator = myrat} = dest_comb mygoal in
+ myra
+ end;
+
+fun thmfromterm t = let val propterm = mk_Trueprop t
+ val mycterm = cterm_of Mainsign propterm in
+ assume mycterm
+ end;
+
+fun termfromthm t = let val conc = concl_of t
+ val {Rand = myra, Rator = myrat} = dest_comb conc in
+ myra
+ end;
+
+fun goalfromterm t = let val pterm = mk_Trueprop t
+ val ct = cterm_of Mainsign pterm in
+ goalw_cterm [] ct
+ end;
+
+fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum
+ val {Rand = myra1, Rator = myrat1} = dest_comb mygoal
+ val {Rand = myra, Rator = myrat} = dest_comb myra1 in
+ myra
+ end;
+
+
+fun mkvars (a,b:term) = let val thetype = type_of b
+ val stringa =( fst a)
+ val newa = Free (stringa, thetype) in
+ (newa,b)
+ end;
+
+fun glue [] thestring = thestring
+ |glue (""::[]) thestring = thestring
+ |glue (a::[]) thestring = thestring^" "^a
+ |glue (a::rest) thestring = let val newstring = thestring^" "^a in
+ glue rest newstring
+ end;
+
+exception STRINGEXCEP;
+
+fun getvstring (Var (v,T)) = fst v
+ |getvstring (Free (v,T))= v;
+
+
+fun getindexstring ((a:string),(b:int))= a;
+
+fun getstrings (a,b) = let val astring = getstring a
+ val bstring = getstring b in
+ (astring,bstring)
+ end;
+(*
+fun getvstrings (a,b) = let val astring = getvstring a
+ val bstring = getvstring b in
+ (astring,bstring)
+ end;
+*)
+
+
+
+(*------------------------------------------------------------------------*)
+(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
+(*------------------------------------------------------------------------*)
+fun mygenvar ty thisenv =
+ let val count = !gcounter
+ val genstring = "GEN"^(string_of_int count)^"VAR" in
+ gcounter := count + 1;
+ genvar genstring (thisenv,ty)
+ end;
+
+fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
+ t
+
+ else if is_forall t then
+ let val {Body, Bvar} = dest_forall t
+ val newvarenv = mygenvar(type_of Bvar) thisenv
+ val newvar = snd(newvarenv)
+ val newbod = subst_free [(Bvar,newvar)] Body
+ val newbod2 = renameBounds newbod thisenv in
+ mk_forall{Body = newbod2, Bvar = newvar}
+ end
+ else if is_exists t then
+ let val {Body, Bvar} =dest_exists t
+ val newvarenv = mygenvar(type_of Bvar) thisenv
+ val newvar = snd(newvarenv)
+ val newbod = subst_free [(Bvar,newvar)] Body
+ val newbod2 = renameBounds newbod thisenv in
+ mk_exists{Body = newbod2, Bvar = newvar}
+ end
+ else if is_conj t then
+ let val {conj1,conj2} = dest_conj t
+ val vpl = renameBounds conj1 thisenv
+ val vpr = renameBounds conj2 thisenv in
+ mk_conj {conj1 = vpl, conj2 = vpr}
+ end
+ else
+ let val {disj1, disj2} = dest_disj t
+ val vpl = renameBounds disj1 thisenv
+ val vpr = renameBounds disj2 thisenv in
+ mk_disj {disj1 = vpl,disj2= vpr}
+ end;
+
+
+
+exception VARFORM_PROBLEM;
+
+fun varform t = if (hol_literal t) then
+ t
+
+ else if is_forall t then
+ let val {Body, Bvar} = dest_forall t
+ (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *)
+ val newB = free2var Bvar
+ val newBody = subst_free[(Bvar, newB)] Body in
+ varform newBody
+ end
+ else if is_exists t then
+ (* Shouldn't really be any exists in term due to Skolemisation*)
+ let val {Body, Bvar} =dest_exists t in
+ varform Body
+ end
+ else if is_conj t then
+ let val {conj1,conj2} = dest_conj t
+ val vpl = varform conj1
+ val vpr = varform conj2 in
+ mk_conj {conj1 = vpl, conj2 = vpr}
+ end
+ else if is_disj t then
+ let val {disj1, disj2} = dest_disj t
+ val vpl = varform disj1
+ val vpr = varform disj2 in
+ mk_disj {disj1 = vpl,disj2= vpr}
+ end
+ else
+ raise VARFORM_PROBLEM;
+
+
+exception ASSERTION of string;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_reconstruct_proof.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,312 @@
+
+
+(****************************************)
+(* Reconstruct an axiom resolution step *)
+(****************************************)
+
+ fun reconstruct_axiom clauses (clausenum:int) thml (numlist, symlist, nsymlist ) =
+ let val this_axiom =(assoc clausenum clauses)
+ val symmed = (apply_rule sym symlist this_axiom)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+(****************************************)
+(* Reconstruct a binary resolution step *)
+(****************************************)
+
+fun reconstruct_binary ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
+ = let
+ val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
+ val thm2 = assoc clause2 thml
+ val res = thm1 RSN ((lit2 +1), thm2)
+ val symmed = (apply_rule sym symlist res)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+
+(****************************************)
+(* Reconstruct a binary resolution step *)
+(****************************************)
+
+fun reconstruct_mrr ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
+ = let
+ val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
+ val thm2 = assoc clause2 thml
+ val res = thm1 RSN ((lit2 +1), thm2)
+ val symmed = (apply_rule sym symlist res)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+(*******************************************)
+(* Reconstruct a factoring resolution step *)
+(*******************************************)
+
+fun reconstruct_factor (clause, lit1, lit2) thml (numlist, symlist, nsymlist )=
+ let
+ val th = assoc clause thml
+ val prems = prems_of th
+ val fac1 = get_nth (lit1+1) prems
+ val fac2 = get_nth (lit2+1) prems
+ val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
+ val newenv = getnewenv unif_env
+ val envlist = alist_of newenv
+
+ val newsubsts = mksubstlist envlist []
+ in
+ if (is_Var (fst(hd(newsubsts))))
+ then
+ let
+ val str1 = lit_string_with_nums (fst (hd newsubsts));
+ val str2 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th;
+ val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
+ val symmed = (apply_rule sym symlist res)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+
+ in
+ rearrange_prems numlist nsymmed
+ end
+ else
+ let
+ val str2 = lit_string_with_nums (fst (hd newsubsts));
+ val str1 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th;
+ val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
+ val symmed = (apply_rule sym symlist res)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+ in
+ rearrange_prems numlist nsymmed
+ end
+ end;
+
+
+(****************************************)
+(* Reconstruct a paramodulation step *)
+(****************************************)
+
+ (* clause1, lit1 is thing to rewrite with *)
+fun reconstruct_standard_para_left ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )=
+
+ let
+
+ val newthm = para_left ((clause1, lit1), (clause2 , lit2)) thml
+ val symmed = (apply_rule sym symlist newthm)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+
+
+ (* clause1, lit1 is thing to rewrite with *)
+fun reconstruct_standard_para_right ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )=
+
+ let
+
+ val newthm = para_right ((clause1, lit1), (clause2 , lit2)) thml
+ val symmed = (apply_rule sym symlist newthm)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+
+
+
+
+
+
+
+ (* let
+ val th1 = assoc clause1 thml
+ val th2 = assoc clause2 thml
+ val prems1 = prems_of th1
+ val prems2 = prems_of th2
+ (* want to get first element of equality *)
+
+ val fac1 = get_nth (lit1+1) prems1
+ val {lhs, rhs} = dest_eq(dest_Trueprop fac1)
+ handle ERR _ => dest_eq(dest_neg (dest_Trueprop fac1))
+ (* get other literal involved in the paramodulation *)
+ val fac2 = get_nth (lit2+1) prems2
+
+ (* get bit of th2 to unify with lhs of th1 *)
+ val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
+ val unif_env = unifiers (Mainsign,myenv, [(unif_lit, lhs)])
+ val newenv = getnewenv unif_env
+ val envlist = alist_of newenv
+ val newsubsts = mksubstlist envlist []
+ (* instantiate th2 with unifiers *)
+
+ val newth1 =
+ if (is_Var (fst(hd(newsubsts))))
+ then
+ let
+ val str1 = lit_string_with_nums (fst (hd newsubsts));
+ val str2 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th1
+ in
+ hd (Seq.list_of(distinct_subgoals_tac facthm))
+ end
+ else
+ let
+ val str2 = lit_string_with_nums (fst (hd newsubsts));
+ val str1 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th1
+ in
+ hd (Seq.list_of(distinct_subgoals_tac facthm))
+ end
+ (*rewrite th2 with the equality bit of th2 i.e. lit2 *)
+ val facthm' = select_literal (lit1 + 1) newth1
+ val equal_lit = concl_of facthm'
+ val cterm_eq = cterm_of Mainsign equal_lit
+ val eq_thm = assume cterm_eq
+ val meta_eq_thm = mk_meta_eq eq_thm
+ val newth2= rewrite_rule [meta_eq_thm] th2
+ (*thin lit2 from th2 *)
+ (* get th1 with lit one as concl, then resolve with thin_rl *)
+ val thm' = facthm' RS thin_rl
+ (* now resolve th2 with last premise of thm' *)
+ val newthm = newth2 RSN ((length prems1), thm')
+ val symmed = (apply_rule sym symlist newthm)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+*)
+
+
+(********************************************)
+(* Reconstruct a rewrite step *)
+(********************************************)
+
+
+
+
+
+
+(* does rewriting involve every literal in rewritten clause? *)
+ (* clause1, lit1 is thing to rewrite with *)
+
+fun reconstruct_rewrite (clause1, lit1, clause2) thml (numlist, symlist, nsymlist )=
+
+ let val th1 = assoc clause1 thml
+ val th2 = assoc clause2 thml
+ val eq_lit_th = select_literal (lit1+1) th1
+ val equal_lit = concl_of eq_lit_th
+ val cterm_eq = cterm_of Mainsign equal_lit
+ val eq_thm = assume cterm_eq
+ val meta_eq_thm = mk_meta_eq eq_thm
+ val newth2= rewrite_rule [meta_eq_thm] th2
+ val symmed = (apply_rule sym symlist newth2)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+
+
+(*****************************************)
+(* Reconstruct an obvious reduction step *)
+(*****************************************)
+
+
+fun reconstruct_obvious (clause1, lit1) allvars thml clause_strs=
+ let val th1 = assoc clause1 thml
+ val prems1 = prems_of th1
+ val newthm = refl RSN ((lit1+ 1), th1)
+ handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
+ val symmed = (apply_rule sym symlist newthm)
+ val nsymmed = (apply_rule not_sym nsymlist symmed )
+ in
+ rearrange_prems numlist nsymmed
+ end
+
+
+
+(********************************************************************************************)
+(* reconstruct a single step of the res. proof - depending on what sort of proof step it was*)
+(********************************************************************************************)
+
+
+ fun reconstruct_proof clauses clausenum thml Axiom (numlist, symlist, nsymlist)
+ = reconstruct_axiom clauses clausenum thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (Binary (a, b)) (numlist, symlist, nsymlist)
+ = reconstruct_binary (a, b) thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (MRR (a, b)) (numlist, symlist, nsymlist)
+ = reconstruct_mrr (a, b) thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (Factor (a, b, c)) (numlist, symlist, nsymlist)
+ = reconstruct_factor (a ,b ,c) thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (Para (a, b)) (numlist, symlist, nsymlist)
+ = reconstruct_standard_para (a, b) thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (Rewrite (a,b,c)) (numlist, symlist, nsymlist)
+ = reconstruct_rewrite (a,b,c) thml (numlist, symlist, nsymlist)
+ | reconstruct_proof clauses clausenum thml (Obvious (a,b)) (numlist, symlist, nsymlist)
+ = reconstruct_obvious (a,b) thml (numlist, symlist, nsymlist)
+ (*| reconstruct_proof clauses clausenum thml (Hyper l)
+ = reconstruct_hyper l thml*)
+ | reconstruct_proof clauses clausenum thml _ _ =
+ raise ASSERTION "proof step not implemented"
+
+
+(********************************************************************************************)
+(* reconstruct a single line of the res. proof - at the moment do only inference steps *)
+(********************************************************************************************)
+
+ fun reconstruct_line clauses thml (clause_num, (proof_step, numlist, symlist,nsymlist))
+ = let
+ val thm = reconstruct_proof clauses clause_num thml proof_step (numlist, symlist,nsymlist)
+
+ in
+ (clause_num, thm)::thml
+ end
+
+(********************************************************************)
+(* reconstruct through the res. proof, creating an Isabelle theorem *)
+(********************************************************************)
+
+
+fun reconstruct clauses [] thml = ((snd( hd thml)))
+ | reconstruct clauses (h::t) thml
+ = let
+ val (thml') = reconstruct_line clauses thml h
+ val (thm) = reconstruct clauses t thml'
+ in
+ (thm)
+ end
+
+
+(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
+ (* and the proof as a list of the proper datatype *)
+(* take the cnf clauses of the goal and the proof from the res. prover *)
+(* as a list of type Proofstep and return the thm goal ==> False *)
+
+fun first_pair (a,b,c) = (a,b);
+
+fun second_pair (a,b,c) = (b,c);
+
+fun one_of_three (a,b,c) = a;
+fun two_of_three (a,b,c) = b;
+fun three_of_three (a,b,c) = c;
+
+(*************************)
+(* reconstruct res proof *)
+(*************************)
+
+fun reconstruct_proof clauses proof
+ = let val thm = reconstruct clauses proof []
+ in
+ thm
+ end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,809 @@
+(******************)
+(* complete later *)
+(******************)
+
+fun not_newline ch = not (ch = "\n");
+
+
+
+(* Versions that include type information *)
+
+fun string_of_thm thm = let val _ = set show_sorts
+ val str = Sign.string_of_term Mainsign (prop_of thm)
+ val no_returns =List.filter not_newline (explode str)
+ val _ = reset show_sorts
+ in
+ implode no_returns
+ end
+
+
+fun thm_of_string str = let val _ = set show_sorts
+ val term = read str
+ val propterm = mk_Trueprop term
+ val cterm = cterm_of Mainsign propterm
+ val _ = reset show_sorts
+ in
+ assume cterm
+ end
+
+(* check separate args in the watcher program for separating strings with a * or ; or something *)
+
+fun clause_strs_to_string [] str = str
+| clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
+
+
+
+fun thmvars_to_string [] str = str
+| thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
+
+
+fun proofstep_to_string Axiom = "Axiom()"
+| proofstep_to_string (Binary ((a,b), (c,d)))= "Binary"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
+| proofstep_to_string (Factor (a,b,c)) = "Factor"^"("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
+| proofstep_to_string (Para ((a,b), (c,d)))= "Para"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
+| proofstep_to_string (MRR ((a,b), (c,d)))= "MRR"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
+| proofstep_to_string (Rewrite((a,b),(c,d))) = "Rewrite"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
+
+fun list_to_string [] liststr = liststr
+| list_to_string (x::[]) liststr = liststr^(string_of_int x)
+| list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
+
+
+fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
+
+
+fun proofs_to_string [] str = str
+| proofs_to_string (x::xs) str = let val newstr = proof_to_string x
+ in
+ proofs_to_string xs (str^newstr)
+ end
+
+
+
+fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
+
+fun init_proofsteps_to_string [] str = str
+| init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x
+ in
+ init_proofsteps_to_string xs (str^newstr)
+ end
+
+
+
+(*** get a string representing the Isabelle ordered axioms ***)
+
+fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta
+ in
+ (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
+ end
+
+
+fun origAxs_to_string [] str = str
+| origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x
+ in
+ origAxs_to_string xs (str^newstr)
+ end
+
+
+(*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
+
+fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta
+ in
+ (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
+ end
+
+
+
+fun extraAxs_to_string [] str = str
+| extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x
+ in
+ extraAxs_to_string xs (str^newstr)
+ end
+
+
+
+
+
+
+fun is_axiom ( num:int,Axiom, str) = true
+| is_axiom (num, _,_) = false
+
+fun get_init_axioms xs = List.filter (is_axiom) ( xs)
+
+fun get_step_nums [] nums = nums
+| get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
+
+fun assoc_snd a [] = raise Noassoc
+ | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
+
+(* change to be something using check_order instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
+
+(*fun get_assoc_snds [] xs assocs= assocs
+| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
+*)
+(*FIX - should this have vars in it? *)
+fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))
+
+ in
+ true
+ end
+ handle EXCEP => false
+
+fun assoc_out_of_order a [] = raise Noassoc
+| assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
+
+fun get_assoc_snds [] xs assocs= assocs
+| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
+
+
+
+
+fun add_if_not_inlist [] xs newlist = newlist
+| add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then
+ add_if_not_inlist ys xs (y::newlist)
+ else add_if_not_inlist ys xs (newlist)
+
+(*
+fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = ";") orelse( ch = "=")
+
+(* replace | by ; here *)
+fun change_or [] = []
+| change_or (x::xs) = if x = "|"
+ then
+ [";"]@(change_or xs)
+ else (x::(change_or xs))
+
+
+fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
+ val exp_term = explode termstr
+ val colon_term = change_or exp_term
+ in
+ implode(List.filter is_alpha_space_neg_eq_colon colon_term)
+ end
+
+fun get_clause_lits thm = clause_lit_string (prop_of thm)
+*)
+
+
+fun onestr [] str = str
+| onestr (x::xs) str = onestr xs (str^(concat x))
+
+fun thmstrings [] str = str
+| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
+
+fun onelist [] newlist = newlist
+| onelist (x::xs) newlist = onelist xs (newlist@x)
+
+
+(**** Code to support ordinary resolution, rather than Model Elimination ****)
+
+(*Convert a list of clauses (disjunctions) to meta-level clauses (==>),
+ with no contrapositives, for ordinary resolution.*)
+
+(*raises exception if no rules apply -- unlike RL*)
+fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
+ | tryres (th, []) = raise THM("tryres", 0, [th]);
+
+val prop_of = #prop o rep_thm;
+
+
+(*For ordinary resolution. *)
+val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
+(*Use "theorem naming" to label the clauses*)
+fun name_thms label =
+ let fun name1 (th, (k,ths)) =
+ (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
+
+ in fn ths => #2 (foldr name1 (length ths, []) ths) end;
+
+(*Find an all-negative support clause*)
+fun is_negative th = forall (not o #1) (literals (prop_of th));
+
+val neg_clauses = List.filter is_negative;
+
+
+
+(*True if the given type contains bool anywhere*)
+fun has_bool (Type("bool",_)) = true
+ | has_bool (Type(_, Ts)) = exists has_bool Ts
+ | has_bool _ = false;
+
+
+(*Create a meta-level Horn clause*)
+fun make_horn crules th = make_horn crules (tryres(th,crules))
+ handle THM _ => th;
+
+
+(*Raises an exception if any Vars in the theorem mention type bool. That would mean
+ they are higher-order, and in addition, they could cause make_horn to loop!*)
+fun check_no_bool th =
+ if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th)))
+ then raise THM ("check_no_bool", 0, [th]) else th;
+
+
+(*Rules to convert the head literal into a negated assumption. If the head
+ literal is already negated, then using notEfalse instead of notEfalse'
+ prevents a double negation.*)
+val notEfalse = read_instantiate [("R","False")] notE;
+val notEfalse' = rotate_prems 1 notEfalse;
+
+fun negated_asm_of_head th =
+ th RS notEfalse handle THM _ => th RS notEfalse';
+
+(*Converting one clause*)
+fun make_meta_clause th =
+ negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
+
+fun make_meta_clauses ths =
+ name_thms "MClause#"
+ (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
+
+(*Permute a rule's premises to move the i-th premise to the last position.*)
+fun make_last i th =
+ let val n = nprems_of th
+ in if 1 <= i andalso i <= n
+ then Thm.permute_prems (i-1) 1 th
+ else raise THM("select_literal", i, [th])
+ end;
+
+(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+ double-negations.*)
+val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
+
+(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
+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 _ = TextIO.output (outfile, thmstring)
+
+ val _ = TextIO.closeOut outfile
+ (* not sure why this is necessary again, but seems to be *)
+ val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+ val axioms = get_init_axioms proof_steps
+ val step_nums = get_step_nums axioms []
+ val thm = thm_of_string thmstring
+ val clauses = make_clauses [thm]
+
+ val vars = map thm_vars clauses
+
+ val distvars = distinct (fold append vars [])
+ val clause_terms = map prop_of clauses
+ val clause_frees = onelist (map term_frees clause_terms) []
+
+ val frees = map lit_string_with_nums clause_frees;
+
+ val distfrees = distinct frees
+
+ val metas = map make_meta_clause clauses
+ val ax_strs = map (three_of_three ) axioms
+
+ (* literals of -all- axioms, not just those used by spass *)
+ val meta_strs = map get_meta_lits metas
+
+ val metas_and_strs = zip metas meta_strs
+ val outfile = TextIO.openOut("foo_clauses");
+ val _ = TextIO.output (outfile, (onestr ax_strs ""))
+
+ val _ = TextIO.closeOut outfile
+ val outfile = TextIO.openOut("foo_metastrs");
+ val _ = TextIO.output (outfile, (onestr meta_strs ""))
+ val _ = TextIO.closeOut outfile
+
+ (* get list of axioms as thms with their variables *)
+
+ val ax_metas = get_assoc_snds ax_strs metas_and_strs []
+ val ax_vars = map thm_vars ax_metas
+ val ax_with_vars = zip ax_metas ax_vars
+
+ (* get list of extra axioms as thms with their variables *)
+ val extra_metas = add_if_not_inlist metas ax_metas []
+ val extra_vars = map thm_vars extra_metas
+ val extra_with_vars = if (not (extra_metas = []) )
+ then
+ zip extra_metas extra_vars
+ else
+ []
+
+ (* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+ val outfile = TextIO.openOut("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 ax_metas_str = TextIO.inputLine (infile)
+ val _ = TextIO.closeIn infile
+ val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
+
+ in
+ (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas))
+ end
+
+fun thmstrings [] str = str
+| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
+
+fun numclstr (vars, []) str = str
+| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
+ in
+ numclstr (vars,rest) newstr
+ end
+
+(*
+
+val proofstr = "Did parsing on Here is a proof with depth 4, length 9 :\
+\1[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
+\3[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
+\5[0:Inp] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)* v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
+\7[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
+\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
+\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
+\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
+\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
+\14[0:Res:11.0,12.0] || -> .\
+\Formulae used in the proof :"
+
+*)
+
+
+fun addvars c (a,b) = (a,b,c)
+
+
+
+(*********************************************************************)
+(* Pass in spass string of proof and string version of isabelle goal *)
+(* Get out reconstruction steps as a string to be sent to Isabelle *)
+(*********************************************************************)
+
+
+(*
+
+
+val proofstr = "Here is a proof with depth 2, length 5 :\
+\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
+\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
+\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa).\
+\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
+\9[0:Res:7.0,3.0] || -> .\
+\Formulae used in the proof :"
+
+
+val proofstr = "Here is a proof with depth 4, length 9 :\
+\1[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
+\3[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
+\5[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)* v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
+\7[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
+\9[0:Fac:5.0,5.1] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
+\10[0:Res:9.0,3.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
+\11[0:Res:10.0,1.0] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
+\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
+\14[0:Res:11.0,12.0] || -> .\
+\Formulae used in the proof :";
+
+
+val thmstring = " (~ (P::'a::type => bool) (x::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | P (x::'a::type)) & ((P::'a::type => bool) (xa::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | ~ P (xb::'a::type))";
+
+val thmstring = "(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)"
+
+
+val thmstring ="(ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)"
+
+val proofstr = "Did parsing on Here is a proof with depth 2, length 5 :\
+\1[0:Inp] || -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
+\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
+\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x(tconst_fun(typ__asc39_a,typ__asc39_a),U))* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U)).\
+\7[0:Res:1.0,5.0] || -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U))*.\
+\9[0:Res:7.0,3.0] || -> .\
+\Formulae used in the proof :";
+
+*)
+
+
+fun spassString_to_reconString proofstr thmstring =
+ let val outfile = TextIO.openOut("thmstringfile"); val _= warning("proofstr is: "^proofstr);
+ val _ = warning ("thmstring is: "^thmstring);
+ val _ = TextIO.output (outfile, (thmstring))
+ val _ = TextIO.closeOut outfile
+ val proofextract = extract_proof proofstr
+ val tokens = fst(lex proofextract)
+
+ (***********************************)
+ (* parse spass proof into datatype *)
+ (***********************************)
+
+ 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 _ = TextIO.closeOut outfile
+
+ val outfile = TextIO.openOut("foo_thmstring_at_parse"); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
+ val _ = TextIO.closeOut outfile
+ (************************************)
+ (* recreate original subgoal as thm *)
+ (************************************)
+
+ (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
+ 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 _ = 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 _ = 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 _ = TextIO.closeOut outfile
+ (***************************************************)
+ (* transfer necessary steps as strings to Isabelle *)
+ (***************************************************)
+ (* turn the proof into a string *)
+ val reconProofStr = proofs_to_string proof ""
+ (* do the bit for the Isabelle ordered axioms at the top *)
+ val ax_nums = map fst numcls
+ val ax_strs = map get_meta_lits_bracket (map snd numcls)
+ val numcls_strs = zip ax_nums ax_strs
+ val num_cls_vars = map (addvars vars) numcls_strs;
+ val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
+
+ 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 _ = 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");
+
+ val _ = TextIO.output (outfile, ("In exception handler"));
+ val _ = TextIO.closeOut outfile
+ in
+ "Proof found but translation failed!"
+ end)
+
+
+
+
+
+
+
+
+
+(**********************************************************************************)
+(* At other end, want to turn back into datatype so can apply reconstruct_proof. *)
+(* This will be done by the signal handler *)
+(**********************************************************************************)
+
+(* Parse in the string version of the proof steps for reconstruction *)
+(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*)
+
+
+ val term_numstep =
+ (number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c))
+
+val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")"))
+ >> (fn (_) => ExtraAxiom)
+
+
+
+val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")"))
+ >> (fn (_) => OrigAxiom)
+
+
+ val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")"))
+ >> (fn (_) => Axiom)
+
+
+
+
+ val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "("))
+ ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
+ ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
+ >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e))
+
+
+ val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "("))
+ ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
+ ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
+ >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e))
+
+ val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "("))
+ ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
+ ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
+ >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e))
+
+
+ val factorstep = (a (Word "Factor")) ++ (a (Other "("))
+ ++ number ++ (a (Other ","))
+ ++ number ++ (a (Other ","))
+ ++ number ++ (a (Other ")"))
+
+ >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) => Factor (c,e,f))
+
+
+val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "("))
+ ++ term_numstep ++ (a (Other ")")) ++ (a (Other ","))
+ ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
+ >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))
+
+val obviousstep = (a (Word "Obvious")) ++ (a (Other "("))
+ ++ term_numstep ++ (a (Other ")"))
+ >> (fn (_, (_, (c,_))) => Obvious (c))
+
+ val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || rewritestep || obviousstep
+
+
+ val number_list_step =
+ ( number ++ many ((a (Other ",") ++ number)>> snd))
+ >> (fn (a,b) => (a::b))
+
+ val numberlist_step = a (Other "[") ++ a (Other "]")
+ >>(fn (_,_) => ([]:int list))
+ || a (Other "[") ++ number_list_step ++ a (Other "]")
+ >>(fn (_,(a,_)) => a)
+
+
+
+(** change this to allow P (x U) *)
+ fun arglist_step input = ( word ++ many word >> (fn (a, b) => (a^" "^(implode_with_space b)))
+ ||word >> (fn (a) => (a)))input
+
+
+fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++ a (Other ")")
+ >>(fn (a, (b, (c,d))) => (a^" ("^(c)^")"))
+ || arglist_step >> (fn (a) => (a)))input
+
+
+
+(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
+ || arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input
+*)
+
+
+ fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
+ || literal_step ++ a (Other "%")>> (fn (a,b) => a ))input
+
+
+
+
+ val term_list_step =
+ ( term_step ++ many ( term_step))
+ >> (fn (a,b) => (a::b))
+
+
+val term_lists_step = a (Other "[") ++ a (Other "]")
+ >>(fn (_,_) => ([]:string list))
+ || a (Other "[") ++ term_list_step ++ a (Other "]")
+ >>(fn (_,(a,_)) => a)
+
+
+
+
+fun anytoken_step input = (word>> (fn (a) => a) ) input
+ handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a) ) input
+ handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
+
+
+
+fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
+ >> (fn (a,b) => (a^" "^(implode b)))) input
+
+
+
+ val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
+ >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
+
+ val lines_step = many linestep
+
+ val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
+
+ val parse_step = fst o alllines_step
+
+
+ (*
+val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) -->(EX x::'a::type. P x) = (ALL y::'a::type. P y)"
+*)
+
+(************************************************************)
+(* Construct an Isar style proof from a list of proof steps *)
+(************************************************************)
+(* want to assume all axioms, then do haves for the other clauses*)
+(* then show for the last step *)
+fun one_of_three (a,b,c) = a;
+fun two_of_three (a,b,c) = b;
+fun three_of_three (a,b,c) = c;
+
+(* replace ~ by not here *)
+fun change_nots [] = []
+| change_nots (x::xs) = if x = "~"
+ then
+ ["\\", "<", "n", "o", "t", ">"]@(change_nots xs)
+ else (x::(change_nots xs))
+
+(*
+fun clstrs_to_string [] str = str
+| clstrs_to_string (x::[]) str = str^x
+| clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; "))
+*)
+fun clstrs_to_string [] str = implode (change_nots (explode str))
+| clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x)))
+| clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; ")))))
+
+
+
+fun thmvars_to_quantstring [] str = str
+| thmvars_to_quantstring (x::[]) str =str^x^". "
+| thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
+
+
+fun clause_strs_to_isar clstrs [] = "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^" \\<Longrightarrow> False\""
+| clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^"\\<Longrightarrow> False\""
+
+fun frees_to_string [] str = implode (change_nots (explode str))
+| frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
+| frees_to_string (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" ")))))
+
+fun frees_to_isar_str [] = ""
+| frees_to_isar_str clstrs = (frees_to_string clstrs "")
+
+
+(***********************************************************************)
+(* functions for producing assumptions for the Isabelle ordered axioms *)
+(***********************************************************************)
+(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
+num, rule, clausestrs, vars*)
+
+
+(* assume the extra clauses - not used in Spass proof *)
+
+fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true
+| is_extraaxiom_step (num, _) = false
+
+fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs)
+
+fun assume_isar_extraaxiom [] str = str
+| assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
+
+
+
+fun assume_isar_extraaxioms [] = ""
+|assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n"
+ in
+ assume_isar_extraaxiom xs str
+ end
+
+(* assume the Isabelle ordered clauses *)
+
+fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true
+| is_origaxiom_step (num, _) = false
+
+fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs)
+
+fun assume_isar_origaxiom [] str = str
+| assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
+
+
+
+fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n"
+ in
+ assume_isar_origaxiom xs str
+ end
+
+
+
+fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true
+| is_axiom_step (num, _) = false
+
+fun get_axioms xs = List.filter (is_axiom_step) ( xs)
+
+fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
+
+fun by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n"
+
+
+fun isar_axiomline (numb, (step, clstrs, thmstrs)) = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) )
+
+
+fun isar_axiomlines [] str = str
+| isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x))
+
+
+fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
+
+
+fun by_isar_line ((Binary ((a,b), (c,d))))="by(rule cl"^
+ (string_of_int a)^" [BINARY "^(string_of_int b)^" "^"cl"^
+ (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
+| by_isar_line ( (Para ((a,b), (c,d)))) ="by (rule cl"^
+ (string_of_int a)^" [PARAMOD "^(string_of_int b)^" "^"cl"^
+ (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
+| by_isar_line ((Factor ((a,b,c)))) = "by (rule cl"^(string_of_int a)^" [FACTOR "^(string_of_int b)^" "^
+ (string_of_int c)^" "^"])"^"\n"
+| by_isar_line ( (Rewrite ((a,b),(c,d)))) = "by (rule cl"^(string_of_int a)^" [DEMOD "^(string_of_int b)^" "^
+ (string_of_int c)^" "^(string_of_int d)^" "^"])"^"\n"
+
+| by_isar_line ( (Obvious ((a,b)))) = "by (rule cl"^(string_of_int a)^" [OBVIOUS "^(string_of_int b)^" ])"^"\n"
+
+fun isar_line (numb, (step, clstrs, thmstrs)) = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
+
+
+fun isar_lines [] str = str
+| isar_lines (x::xs) str = isar_lines xs (str^(isar_line x))
+
+fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
+
+
+fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
+ val extraax_num = length extraaxioms
+ val origaxioms_and_steps = drop (extraax_num) xs
+
+
+ val origaxioms = get_origaxioms origaxioms_and_steps
+ val origax_num = length origaxioms
+ val axioms_and_steps = drop (origax_num + extraax_num) xs
+ val axioms = get_axioms axioms_and_steps
+
+ val steps = drop origax_num axioms_and_steps
+ val firststeps = butlast steps
+ val laststep = last steps
+ val goalstring = implode(butlast(explode goalstring))
+
+ val isar_proof =
+ ("show \""^goalstring^"\"\n")^
+ ("proof (rule ccontr,skolemize, make_clauses) \n")^
+ ("fix "^(frees_to_isar_str frees)^"\n")^
+ (assume_isar_extraaxioms extraaxioms)^
+ (assume_isar_origaxioms origaxioms)^
+ (isar_axiomlines axioms "")^
+ (isar_lines firststeps "")^
+ (last_isar_line laststep)^
+ ("qed")
+ val outfile = TextIO.openOut("isar_proof_file");
+
+ val _ = TextIO.output (outfile, isar_proof)
+ val _ = TextIO.closeOut outfile
+
+
+ in
+ isar_proof
+ end
+
+(* get fix vars from axioms - all Frees *)
+(* check each clause for meta-vars and /\ over them at each step*)
+
+(*******************************************************)
+(* This assumes the thm list "numcls" is still there *)
+(* In reality, should probably label it with an *)
+(* ID number identifying the subgoal. This could *)
+(* be passed over to the watcher, e.g. numcls25 *)
+(*******************************************************)
+
+(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
+
+val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
+
+val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type. (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) | (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) & P xb & ~ Q xb)";
+
+
+val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
+
+val thmstring = " (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)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
+*)
+
+fun apply_res_thm str goalstring = let val tokens = fst (lex str);
+
+ val (frees,recon_steps) = parse_step tokens
+ val isar_str = to_isar_proof (frees, recon_steps, goalstring)
+ val foo = TextIO.openOut "foobar";
+ in
+ TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str isar_str); ()
+ end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,510 @@
+
+fun take n [] = []
+| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
+
+fun drop n [] = []
+| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
+
+fun remove n [] = []
+| remove n (x::xs) = List.filter (not_equal n) (x::xs);
+
+fun remove_nth n [] = []
+| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
+
+fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
+
+fun add_in_order (x:string) [] = [x]
+| add_in_order (x:string) ((y:string)::ys) = if (x < y)
+ then
+ (x::(y::ys))
+ else
+ (y::(add_in_order x ys))
+fun add_once x [] = [x]
+| add_once x (y::ys) = if (inlist x (y::ys)) then
+ (y::ys)
+ else
+ add_in_order x (y::ys)
+
+fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
+
+Goal "False ==> False";
+by Auto_tac;
+qed "False_imp";
+
+exception Reflex_equal;
+
+(********************************)
+(* Proofstep datatype *)
+(********************************)
+(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3] *)
+
+datatype Side = Left |Right
+
+ datatype Proofstep = ExtraAxiom
+ |OrigAxiom
+ | Axiom
+ | Binary of (int * int) * (int * int) (* (clause1,lit1), (clause2, lit2) *)
+ | MRR of (int * int) * (int * int)
+ | Factor of (int * int * int) (* (clause,lit1, lit2) *)
+ | Para of (int * int) * (int * int)
+ | Rewrite of (int * int) * (int * int)
+ | Obvious of (int * int)
+ (*| Hyper of int list*)
+ | Unusedstep of unit
+
+
+datatype Clausesimp = Binary_s of int * int
+ | Factor_s of unit
+ | Demod_s of (int * int) list
+ | Hyper_s of int list
+ | Unusedstep_s of unit
+
+
+
+datatype Step_label = T_info
+ |P_info
+
+
+fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
+
+
+
+fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t
+ val exp_term = explode termstr
+ in
+ implode(List.filter is_alpha_space_digit_or_neg exp_term)
+ end
+
+
+(****************************************)
+(* Reconstruct an axiom resolution step *)
+(****************************************)
+
+ fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
+ let val this_axiom =(assoc clausenum clauses)
+ val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res, (Axiom,clause_strs,thmvars ) )
+ end
+
+(****************************************)
+(* Reconstruct a binary resolution step *)
+(****************************************)
+
+ (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
+fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
+ = let
+ val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
+ val thm2 = assoc clause2 thml
+ val res = thm1 RSN ((lit2 +1), thm2)
+ val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
+ end
+
+
+
+(******************************************************)
+(* Reconstruct a matching replacement resolution step *)
+(******************************************************)
+
+
+fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
+ = let
+ val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
+ val thm2 = assoc clause2 thml
+ val res = thm1 RSN ((lit2 +1), thm2)
+ val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
+ end
+
+
+(*******************************************)
+(* Reconstruct a factoring resolution step *)
+(*******************************************)
+
+fun mksubstlist [] sublist = sublist
+ |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b
+ val avar = Var(a,vartype)
+ val newlist = ((avar,b)::sublist) in
+ mksubstlist rest newlist
+ end;
+
+(* based on Tactic.distinct_subgoals_tac *)
+
+fun delete_assump_tac state lit =
+ let val (frozth,thawfn) = freeze_thaw state
+ val froz_prems = cprems_of frozth
+ val assumed = implies_elim_list frozth (map assume froz_prems)
+ val new_prems = remove_nth lit froz_prems
+ val implied = implies_intr_list new_prems assumed
+ in
+ Seq.single (thawfn implied)
+ end
+
+
+
+
+
+(*************************************)
+(* Reconstruct a factoring step *)
+(*************************************)
+
+fun follow_factor clause lit1 lit2 allvars thml clause_strs=
+ let
+ val th = assoc clause thml
+ val prems = prems_of th
+ val fac1 = get_nth (lit1+1) prems
+ val fac2 = get_nth (lit2+1) prems
+ val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
+ val newenv = getnewenv unif_env
+ val envlist = alist_of newenv
+
+ val newsubsts = mksubstlist envlist []
+ in
+ if (is_Var (fst(hd(newsubsts))))
+ then
+ let
+ val str1 = lit_string_with_nums (fst (hd newsubsts));
+ val str2 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th;
+ val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
+ val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
+ val thmvars = thm_vars res'
+ in
+ (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars))
+ end
+ else
+ let
+ val str2 = lit_string_with_nums (fst (hd newsubsts));
+ val str1 = lit_string_with_nums (snd (hd newsubsts));
+ val facthm = read_instantiate [(str1,str2)] th;
+ val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1)))
+ val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
+ val thmvars = thm_vars res'
+ in
+ (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars))
+ end
+ end;
+
+
+
+Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
+val prems = it;
+br (hd prems) 1;
+br (hd(tl(tl prems))) 1;
+qed "merge";
+
+
+
+fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm))
+ then
+ t
+ else
+ let val {Rand, Rator} = dest_comb t
+ in
+ get_unif_comb Rand eqterm
+ end
+
+fun get_rhs_unif_lit t eqterm = if (can dest_eq t)
+ then
+ let val {lhs, rhs} = dest_eq( t)
+ in
+ rhs
+ end
+ else
+ get_unif_comb t eqterm
+
+fun get_lhs_unif_lit t eqterm = if (can dest_eq t)
+ then
+ let val {lhs, rhs} = dest_eq( t)
+ in
+ lhs
+ end
+ else
+ get_unif_comb t eqterm
+
+
+(*************************************)
+(* Reconstruct a paramodulation step *)
+(*************************************)
+
+val rev_subst = rotate_prems 1 subst;
+val rev_ssubst = rotate_prems 1 ssubst;
+
+
+(* have changed from negate_nead to negate_head. God knows if this will actually work *)
+fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
+ let
+ val th1 = assoc clause1 thml
+ val th2 = assoc clause2 thml
+ val eq_lit_th = select_literal (lit1+1) th1
+ val mod_lit_th = select_literal (lit2+1) th2
+ val eqsubst = eq_lit_th RSN (2,rev_subst)
+ val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
+ val newth' =negate_head newth
+ val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars
+ handle Not_in_list => let
+ val mod_lit_th' = mod_lit_th RS not_sym
+ val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
+ val newth' =negate_head newth
+ in
+ (rearrange_clause newth' clause_strs allvars)
+ end)
+ val thmvars = thm_vars res
+ in
+ (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
+ end
+
+(*
+fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
+ let
+ val th1 = assoc clause1 thml
+ val th2 = assoc clause2 thml
+ val eq_lit_th = select_literal (lit1+1) th1
+ val mod_lit_th = select_literal (lit2+1) th2
+ val eqsubst = eq_lit_th RSN (2,rev_subst)
+ val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
+ val newth' =negate_nead newth
+ val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
+ end
+
+*)
+
+
+(********************************)
+(* Reconstruct a rewriting step *)
+(********************************)
+
+(*
+
+val rev_subst = rotate_prems 1 subst;
+
+fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
+ let val eq_lit_th = select_literal (lit1+1) cl1
+ val mod_lit_th = select_literal (lit2+1) cl2
+ val eqsubst = eq_lit_th RSN (2,rev_subst)
+ val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
+eqsubst)
+ in negated_asm_of_head newth end;
+
+val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
+eqsubst)
+
+val mod_lit_th' = mod_lit_th RS not_sym
+
+*)
+
+
+fun delete_assumps 0 th = th
+| delete_assumps n th = let val th_prems = length (prems_of th)
+ val th' = hd (Seq.list_of(delete_assump_tac th (th_prems -1)))
+ in
+ delete_assumps (n-1) th'
+ end
+
+(* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *)
+(* changed negate_nead to negate_head here too*)
+ (* clause1, lit1 is thing to rewrite with *)
+fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs=
+
+ let val th1 = assoc clause1 thml
+ val th2 = assoc clause2 thml
+ val eq_lit_th = select_literal (lit1+1) th1
+ val mod_lit_th = select_literal (lit2+1) th2
+ val eqsubst = eq_lit_th RSN (2,rev_subst)
+ val eq_lit_prem_num = length (prems_of eq_lit_th)
+ val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
+ val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
+eqsubst)
+
+ val newthm = negate_head newth
+ val newthm' = delete_assumps eq_lit_prem_num newthm
+ val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars))
+ end
+
+
+
+(*****************************************)
+(* Reconstruct an obvious reduction step *)
+(*****************************************)
+
+
+fun follow_obvious (clause1, lit1) allvars thml clause_strs=
+ let val th1 = assoc clause1 thml
+ val prems1 = prems_of th1
+ val newthm = refl RSN ((lit1+ 1), th1)
+ handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
+ val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
+ val thmvars = thm_vars res
+ in
+ (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
+ end
+
+(**************************************************************************************)
+(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
+(**************************************************************************************)
+
+ fun follow_proof clauses allvars clausenum thml (Axiom ) clause_strs
+ = follow_axiom clauses allvars clausenum thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (Binary (a, b)) clause_strs
+ = follow_binary (a, b) allvars thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (MRR (a, b)) clause_strs
+ = follow_mrr (a, b) allvars thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (Factor (a, b, c)) clause_strs
+ = follow_factor a b c allvars thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs
+ = follow_standard_para (a, b) allvars thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs
+ = follow_rewrite (a,b) allvars thml clause_strs
+
+ | follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs
+ = follow_obvious (a,b) allvars thml clause_strs
+
+ (*| follow_proof clauses clausenum thml (Hyper l)
+ = follow_hyper l thml*)
+ | follow_proof clauses allvars clausenum thml _ _ =
+ raise ASSERTION "proof step not implemented"
+
+
+
+
+(**************************************************************************************)
+(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
+(**************************************************************************************)
+
+ fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons
+ = let
+ val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs
+ val recon_step = (recon_fun)
+ in
+ (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
+ end
+
+(***************************************************************)
+(* follow through the res. proof, creating an Isabelle theorem *)
+(***************************************************************)
+
+
+
+(*fun is_proof_char ch = (case ch of
+
+ "(" => true
+ | ")" => true
+ | ":" => true
+ | "'" => true
+ | "&" => true
+ | "|" => true
+ | "~" => true
+ | "." => true
+ |(is_alpha ) => true
+ |(is_digit) => true
+ | _ => false)*)
+
+fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
+
+fun proofstring x = let val exp = explode x
+ in
+ List.filter (is_proof_char ) exp
+ end
+
+
+fun not_newline ch = not (ch = "\n");
+
+fun concat_with_and [] str = str
+| concat_with_and (x::[]) str = str^"("^x^")"
+| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
+(*
+
+fun follow clauses [] allvars thml recons =
+ let (* val _ = reset show_sorts*)
+ val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
+ val thmproofstring = proofstring ( thmstring)
+ val no_returns =List.filter not_newline ( thmproofstring)
+ val thmstr = implode no_returns
+ val outfile = TextIO.openOut("thml_file")
+ val _ = TextIO.output(outfile, "thmstr is "^thmstr)
+ val _ = TextIO.flushOut outfile;
+ val _ = TextIO.closeOut outfile
+ (*val _ = set show_sorts*)
+ in
+ ((snd( hd thml)), recons)
+ end
+ | follow clauses (h::t) allvars thml recons
+ = let
+ val (thml', recons') = follow_line clauses allvars thml h recons
+ val (thm, recons_list) = follow clauses t allvars thml' recons'
+
+
+ in
+ (thm,recons_list)
+ end
+
+*)
+
+fun replace_clause_strs [] recons newrecons= (newrecons)
+| replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons =
+ let val new_clause_strs = get_meta_lits_bracket thm
+ in
+ replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
+ end
+
+
+fun follow clauses [] allvars thml recons =
+ let
+ val new_recons = replace_clause_strs thml recons []
+ in
+ ((snd( hd thml)), new_recons)
+ end
+
+ | follow clauses (h::t) allvars thml recons
+ = let
+ val (thml', recons') = follow_line clauses allvars thml h recons
+ val (thm, recons_list) = follow clauses t allvars thml' recons'
+ in
+ (thm,recons_list)
+ end
+
+
+
+(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
+ (* and the proof as a list of the proper datatype *)
+(* take the cnf clauses of the goal and the proof from the res. prover *)
+(* as a list of type Proofstep and return the thm goal ==> False *)
+
+fun first_pair (a,b,c) = (a,b);
+
+fun second_pair (a,b,c) = (b,c);
+
+fun one_of_three (a,b,c) = a;
+fun two_of_three (a,b,c) = b;
+fun three_of_three (a,b,c) = c;
+
+
+(* takes original axioms, proof_steps parsed from spass, variables *)
+
+fun translate_proof clauses proof allvars
+ = let val (thm, recons) = follow clauses proof allvars [] []
+ in
+ (thm, (recons))
+ end
+
+
+
+fun remove_tinfo [] = []
+| remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,729 @@
+
+ (* Title: Watcher.ML
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+ *)
+
+ (***************************************************************************)
+ (* The watcher process starts a resolution process when it receives a *)
+(* message from Isabelle *)
+(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
+(* and removes dead processes. Also possible to kill all the resolution *)
+(* processes currently running. *)
+(* Hardwired version of where to pick up the tptp files for the moment *)
+(***************************************************************************)
+
+(*use "Proof_Transfer";
+use "VampireCommunication";
+use "SpassCommunication";
+use "modUnix";*)
+(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
+
+use "~~/VampireCommunication";
+use "~~/SpassCommunication";
+
+
+use "~~/modUnix";
+
+
+structure Watcher: WATCHER =
+ struct
+
+fun fst (a,b) = a;
+fun snd (a,b) = b;
+
+val goals_being_watched = ref 0;
+
+
+fun remove y [] = []
+| remove y (x::xs) = (if y = x
+ then
+ remove y xs
+ else ((x::(remove y xs))))
+
+
+
+fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
+
+(********************************************************************************************)
+(* takes a list of arguments and sends them individually to the watcher process by pipe *)
+(********************************************************************************************)
+
+fun outputArgs (toWatcherStr, []) = ()
+| outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x);
+ TextIO.flushOut toWatcherStr;
+ outputArgs (toWatcherStr, xs))
+
+(********************************************************************************)
+(* gets individual args from instream and concatenates them into a list *)
+(********************************************************************************)
+
+fun getArgs (fromParentStr, toParentStr,ys) = let
+ val thisLine = TextIO.input fromParentStr
+ in
+ ((ys@[thisLine]))
+ end
+
+(********************************************************************************)
+(* Remove the \n character from the end of each filename *)
+(********************************************************************************)
+
+fun getCmd cmdStr = let val backList = ((rev(explode cmdStr)))
+ in
+
+ if (String.isPrefix "\n" (implode backList ))
+ then
+ (implode (rev ((tl backList))))
+ else
+ (cmdStr)
+ end
+
+(********************************************************************************)
+(* Send request to Watcher for a vampire to be called for filename in arg *)
+(********************************************************************************)
+
+fun callResProver (toWatcherStr, arg) = (sendOutput (toWatcherStr, arg^"\n");
+ TextIO.flushOut toWatcherStr
+
+ )
+
+(*****************************************************************************************)
+(* Send request to Watcher for multiple provers to be called for filenames in arg *)
+(*****************************************************************************************)
+
+(* need to modify to send over hyps file too *)
+fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n");
+ TextIO.flushOut toWatcherStr)
+| callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
+ 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 _ = 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
+ then
+ ()
+ else
+ File.mkdir dfg_dir;
+ val probID = last(explode probfile)
+ val dfg_path = File.sysify_path dfg_dir;
+ val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
+ (*val _ = Posix.Process.wait ()*)
+ (*val _ =Unix.reap exec_tptp2x*)
+ val newfile = dfg_path^"/prob"^(probID)^".dfg"
+
+ in
+ goals_being_watched := (!goals_being_watched) + 1;
+ OS.Process.sleep(Time.fromSeconds 1);
+ (warning("dfg file is: "^newfile));
+ sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
+ TextIO.flushOut toWatcherStr;
+ Unix.reap exec_tptp2x;
+
+ callResProvers (toWatcherStr,args)
+
+ end
+
+fun callResProversStr (toWatcherStr, []) = "End of calls\n"
+
+| callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
+ ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
+
+ )
+
+(**************************************************************)
+(* Send message to watcher to kill currently running vampires *)
+(**************************************************************)
+
+fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n");
+ TextIO.flushOut toWatcherStr)
+
+
+
+(**************************************************************)
+(* Remove \n token from a vampire goal filename and extract *)
+(* prover, proverCmd, settings and file from input string *)
+(**************************************************************)
+
+
+ fun takeUntil ch [] res = (res, [])
+ | takeUntil ch (x::xs) res = if x = ch
+ then
+ (res, xs)
+ else
+ takeUntil ch xs (res@[x])
+
+ fun getSettings [] settings = settings
+| getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
+ in
+ getSettings rest (settings@[(implode set)])
+ end
+
+fun separateFields str = let val (prover, rest) = takeUntil "*" str []
+ val prover = implode prover
+ val (thmstring, rest) = takeUntil "*" rest []
+ val thmstring = implode thmstring
+ val (goalstring, rest) = takeUntil "*" rest []
+ val goalstring = implode goalstring
+ val (proverCmd, rest ) = takeUntil "*" rest []
+ val proverCmd = implode proverCmd
+
+ val (settings, rest) = takeUntil "*" rest []
+ val settings = getSettings settings []
+ val (file, rest) = takeUntil "*" rest []
+ val file = implode file
+ val outfile = TextIO.openOut("sep_comms");
+ val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
+ val _ = TextIO.closeOut outfile
+
+ in
+ (prover,thmstring,goalstring, proverCmd, settings, file)
+ end
+
+
+
+ fun getCmd cmdStr = let val backList = ((rev(explode cmdStr)))
+ in
+
+ if (String.isPrefix "\n" (implode backList ))
+ then
+ separateFields ((rev ((tl backList))))
+ else
+ (separateFields (explode cmdStr))
+ end
+
+
+fun getProofCmd (a,b,c,d,e,f) = d
+
+
+(**************************************************************)
+(* Get commands from Isabelle *)
+(**************************************************************)
+
+fun getCmds (toParentStr,fromParentStr, cmdList) =
+ let val thisLine = TextIO.inputLine fromParentStr
+ in
+ (if (thisLine = "End of calls\n")
+ then
+ (cmdList)
+ else if (thisLine = "Kill children\n")
+ then
+ ( TextIO.output (toParentStr,thisLine );
+ TextIO.flushOut toParentStr;
+ (("","","","Kill children",[],"")::cmdList)
+ )
+ else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
+ in
+ (*TextIO.output (toParentStr, thisCmd);
+ TextIO.flushOut toParentStr;*)
+ getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
+ end
+ )
+ )
+ end
+
+
+(**************************************************************)
+(* Get Io-descriptor for polling of an input stream *)
+(**************************************************************)
+
+
+fun getInIoDesc someInstr =
+ let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
+ val _ = print (TextIO.stdOut, buf)
+ val ioDesc =
+ case rd
+ of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
+ | _ => NONE
+ in (* since getting the reader will have terminated the stream, we need
+ * to build a new stream. *)
+ TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
+ ioDesc
+ end
+
+
+(*************************************)
+(* Set up a Watcher Process *)
+(*************************************)
+
+
+
+fun setupWatcher (the_goal) = let
+ (** pipes for communication between parent and watcher **)
+ val p1 = Posix.IO.pipe ()
+ val p2 = Posix.IO.pipe ()
+ fun closep () = (
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p1);
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p2)
+ )
+ (***********************************************************)
+ (****** fork a watcher process and get it set up and going *)
+ (***********************************************************)
+ fun startWatcher (procList) =
+ (case Posix.Process.fork() (***************************************)
+ of SOME pid => pid (* parent - i.e. main Isabelle process *)
+ (***************************************)
+
+ (*************************)
+ | NONE => let (* child - i.e. watcher *)
+ val oldchildin = #infd p1 (*************************)
+ val fromParent = Posix.FileSys.wordToFD 0w0
+ val oldchildout = #outfd p2
+ val toParent = Posix.FileSys.wordToFD 0w1
+ 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 _ = TextIO.output (outfile,goalstr )
+ val _ = TextIO.closeOut outfile
+ fun killChildren [] = ()
+ | killChildren (childPid::children) = (killChild childPid; killChildren children)
+
+
+
+ (*************************************************************)
+ (* take an instream and poll its underlying reader for input *)
+ (*************************************************************)
+
+ fun pollParentInput () =
+
+ let val pd = OS.IO.pollDesc (fromParentIOD)
+ in
+ if (isSome pd ) then
+ let val pd' = OS.IO.pollIn (valOf pd)
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
+ in
+ if null pdl
+ then
+ NONE
+ else if (OS.IO.isIn (hd pdl))
+ then
+ (SOME ( getCmds (toParentStr, fromParentStr, [])))
+ else
+ NONE
+ end
+ else
+ NONE
+ end
+
+
+
+ fun pollChildInput (fromStr) =
+ let val iod = getInIoDesc fromStr
+ in
+ if isSome iod
+ then
+ let val pd = OS.IO.pollDesc (valOf iod)
+ in
+ if (isSome pd ) then
+ let val pd' = OS.IO.pollIn (valOf pd)
+ val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100))
+ in
+ if null pdl
+ then
+ NONE
+ else if (OS.IO.isIn (hd pdl))
+ then
+ SOME (getCmd (TextIO.inputLine fromStr))
+ else
+ NONE
+ end
+ else
+ NONE
+ end
+ else
+ NONE
+ end
+
+
+ (****************************************************************************)
+ (* Check all vampire processes currently running for output *)
+ (****************************************************************************)
+ (*********************************)
+ fun checkChildren ([], toParentStr) = [] (*** no children to check ********)
+ (*********************************)
+ | checkChildren ((childProc::otherChildren), toParentStr) =
+ let val (childInput,childOutput) = cmdstreamsOf childProc
+ val childPid = cmdchildPid childProc
+ val childCmd = fst(snd (cmdchildInfo childProc))
+ val childIncoming = pollChildInput childInput
+ val parentID = Posix.ProcEnv.getppid()
+ val prover = cmdProver childProc
+ val thmstring = cmdThm childProc
+ val goalstring = cmdGoal childProc
+ val outfile = TextIO.openOut("child_comms");
+ val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
+ val _ = TextIO.closeOut outfile
+ in
+ if (isSome childIncoming)
+ then
+ (* check here for prover label on child*)
+
+ let val outfile = TextIO.openOut("child_incoming");
+ val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
+ val _ = TextIO.closeOut outfile
+ val childDone = (case prover of
+ (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd) ) )
+ in
+ if childDone (**********************************************)
+ then (* child has found a proof and transferred it *)
+ (**********************************************)
+
+ (**********************************************)
+ (* Remove this child and go on to check others*)
+ (**********************************************)
+ ( reap(childPid, childInput, childOutput);
+ checkChildren(otherChildren, toParentStr))
+ else
+ (**********************************************)
+ (* Keep this child and go on to check others *)
+ (**********************************************)
+
+ (childProc::(checkChildren (otherChildren, toParentStr)))
+ end
+ else
+ let val outfile = TextIO.openOut("child_incoming");
+ val _ = TextIO.output (outfile,"No child output " )
+ val _ = TextIO.closeOut outfile
+ in
+ (childProc::(checkChildren (otherChildren, toParentStr)))
+ end
+ end
+
+
+ (********************************************************************)
+ (* call resolution processes *)
+ (* settings should be a list of strings *)
+ (* e.g. ["-t 300", "-m 100000"] *)
+ (* takes list of (string, string, string list, string)list proclist *)
+ (********************************************************************)
+
+ fun execCmds [] procList = procList
+ | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList =
+ if (prover = "spass")
+ then
+ let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
+ in
+ execCmds cmds newProcList
+ end
+ else
+ let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
+ in
+ execCmds cmds newProcList
+ end
+
+
+ (****************************************)
+ (* call resolution processes remotely *)
+ (* settings should be a list of strings *)
+ (* e.g. ["-t 300", "-m 100000"] *)
+ (****************************************)
+
+ fun execRemoteCmds [] procList = procList
+ | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList =
+ let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
+ in
+ execRemoteCmds cmds newProcList
+ end
+
+
+ fun printList (outStr, []) = ()
+ | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))
+
+
+ (**********************************************)
+ (* Watcher Loop *)
+ (**********************************************)
+
+
+
+
+ fun keepWatching (toParentStr, fromParentStr,procList) =
+ let fun loop (procList) =
+ (
+ let val cmdsFromIsa = pollParentInput ()
+ fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n");
+ TextIO.flushOut toParentStr;
+ killChildren (map (cmdchildPid) procList);
+ ())
+
+ in
+ (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
+ (**********************************)
+ if (isSome cmdsFromIsa) then (* deal with input from Isabelle *)
+ ( (**********************************)
+ if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
+ then
+ (
+ let val childPids = map cmdchildPid procList
+ in
+ killChildren childPids;
+ (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([])
+ end
+ )
+ else
+ (
+ if ((length procList)<2) (********************)
+ then (* Execute locally *)
+ ( (********************)
+ let
+ val newProcList = execCmds (valOf cmdsFromIsa) procList
+ val parentID = Posix.ProcEnv.getppid()
+ val newProcList' =checkChildren (newProcList, toParentStr)
+ in
+ (*OS.Process.sleep (Time.fromSeconds 1);*)
+ loop (newProcList')
+ end
+ )
+ else (************************)
+ (* Execute remotely *)
+ ( (************************)
+ let
+ val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
+ val parentID = Posix.ProcEnv.getppid()
+ val newProcList' =checkChildren (newProcList, toParentStr)
+ in
+ (*OS.Process.sleep (Time.fromSeconds 1);*)
+ loop (newProcList')
+ end
+ )
+
+
+
+ )
+ ) (******************************)
+ else (* No new input from Isabelle *)
+ (******************************)
+ ( let val newProcList = checkChildren ((procList), toParentStr)
+ in
+ OS.Process.sleep (Time.fromSeconds 1);
+ loop (newProcList)
+ end
+
+ )
+ end)
+ in
+ loop (procList)
+ end
+
+
+ in
+ (***************************)
+ (*** Sort out pipes ********)
+ (***************************)
+
+ Posix.IO.close (#outfd p1);
+ Posix.IO.close (#infd p2);
+ Posix.IO.dup2{old = oldchildin, new = fromParent};
+ Posix.IO.close oldchildin;
+ Posix.IO.dup2{old = oldchildout, new = toParent};
+ Posix.IO.close oldchildout;
+
+ (***************************)
+ (* start the watcher loop *)
+ (***************************)
+ keepWatching (toParentStr, fromParentStr, procList);
+
+
+ (****************************************************************************)
+ (* fake return value - actually want the watcher to loop until killed *)
+ (****************************************************************************)
+ Posix.Process.wordToPid 0w0
+
+ end);
+ (* end case *)
+
+
+ val _ = TextIO.flushOut TextIO.stdOut
+
+ (*******************************)
+ (*** set watcher going ********)
+ (*******************************)
+
+ val procList = []
+ val pid = startWatcher (procList)
+ (**************************************************)
+ (* communication streams to watcher *)
+ (**************************************************)
+
+ val instr = openInFD ("_exec_in", #infd p2)
+ val outstr = openOutFD ("_exec_out", #outfd p1)
+
+ in
+ (*******************************)
+ (* close the child-side fds *)
+ (*******************************)
+ Posix.IO.close (#outfd p2);
+ Posix.IO.close (#infd p1);
+ (* set the fds close on exec *)
+ Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+ Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
+
+ (*******************************)
+ (* return value *)
+ (*******************************)
+ PROC{pid = pid,
+ instr = instr,
+ outstr = outstr
+ }
+ end;
+
+
+
+(**********************************************************)
+(* Start a watcher and set up signal handlers *)
+(**********************************************************)
+fun killWatcher pid= killChild pid;
+
+fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
+ val streams =snd mychild
+ val childin = fst streams
+ val childout = snd streams
+ val childpid = fst mychild
+
+ fun vampire_proofHandler (n:int) =
+ (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() )
+
+ (* fun spass_proofHandler (n:int) = (
+ let val (reconstr, thmstring, goalstring) = getSpassInput childin
+ val outfile = TextIO.openOut("foo_signal");
+
+ val _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring))
+ val _ = TextIO.closeOut outfile
+ in
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str reconstr) ;
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ (*killWatcher childpid;*) ()
+ end)*)
+
+
+(*
+
+fun spass_proofHandler (n:int) = (
+ let val outfile = TextIO.openOut("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 _ = TextIO.output (outfile, ("In signal handler "^reconstr^" "^thmstring^goalstring))
+ val _ = TextIO.closeOut outfile
+ in
+ if ( (substring (reconstr, 0,1))= "[")
+ then
+
+ let val thm = thm_of_string thmstring
+ val clauses = make_clauses [thm]
+ val numcls = zip (numlist (length clauses)) (map make_meta_clause clauses)
+
+ in
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ apply_res_thm reconstr goalstring;
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ killWatcher childpid; ()
+ end
+ else
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ (*killWatcher childpid; *) reap (childpid,childin, childout);()
+ end )
+*)
+
+fun spass_proofHandler (n:int) = (
+ let val outfile = TextIO.openOut("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 _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
+ val _ = TextIO.closeOut outfile
+ in (* if a proof has been found and sent back as a reconstruction proof *)
+ if ( (substring (reconstr, 0,1))= "[")
+ then
+
+ (
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ apply_res_thm reconstr goalstring;
+ Pretty.writeln(Pretty.str (oct_char "361"));
+
+ goals_being_watched := ((!goals_being_watched) - 1);
+
+ if ((!goals_being_watched) = 0)
+ then
+ (let val outfile = TextIO.openOut("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
+ reap (childpid,childin, childout); ()
+ end)
+ else
+ ()
+ )
+ (* if there's no proof, but a message from Spass *)
+ else if ((substring (reconstr, 0,5))= "SPASS")
+ then
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut("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
+ reap (childpid,childin, childout); ()
+ end )
+ else
+ ()
+ )
+ (* if proof translation failed *)
+ else if ((substring (reconstr, 0,5)) = "Proof")
+ then
+ (
+ goals_being_watched := (!goals_being_watched) -1;
+ Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
+ Pretty.writeln(Pretty.str (goalstring^reconstr));
+ Pretty.writeln(Pretty.str (oct_char "361"));
+ if (!goals_being_watched = 0)
+ then
+ (let val outfile = TextIO.openOut("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
+ reap (childpid,childin, childout); ()
+ end )
+ else
+ ()
+ )
+
+
+ else (* add something here ?*)
+ ()
+
+ end)
+
+
+
+ in
+ Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
+ Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
+ (childin, childout, childpid)
+
+ end
+
+
+
+
+
+end (* structure Watcher *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/watcher.sig Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,51 @@
+
+(* Title: Watcher.ML
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
+*)
+
+(***************************************************************************)
+(* The watcher process starts a Spass process when it receives a *)
+(* message from Isabelle *)
+(* Signals Isabelle, puts output of child into pipe to Isabelle, *)
+(* and removes dead processes. Also possible to kill all the vampire *)
+(* processes currently running. *)
+(***************************************************************************)
+
+
+signature WATCHER =
+ sig
+
+(*****************************************************************************************)
+(* Send request to Watcher for multiple spasses to be called for filenames in arg *)
+(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
+(*****************************************************************************************)
+
+val callResProvers : TextIO.outstream *(string* string*string *string*string*string) list -> unit
+
+
+
+(************************************************************************)
+(* Send message to watcher to kill currently running resolution provers *)
+(************************************************************************)
+
+val callSlayer : TextIO.outstream -> unit
+
+
+
+(**********************************************************)
+(* Start a watcher and set up signal handlers *)
+(**********************************************************)
+
+val createWatcher : thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
+
+
+
+(**********************************************************)
+(* Kill watcher process *)
+(**********************************************************)
+
+val killWatcher : (Posix.Process.pid) -> unit
+
+
+end