# HG changeset patch # User quigley # Date 1112290166 -7200 # Node ID 028059faa9631c80b60fdf2bfcd8c63da379a91d # Parent b389f108c4854c439920511a115628ad79a558e3 *** empty log message *** diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/SpassCommunication.ML --- /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","","") + + diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/VampireCommunication.ML --- /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; diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/modUnix.ML --- /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 diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_gandalf_base.ML --- /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); + diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_order_clauses.ML --- /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 diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_parse.ML --- /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 + +*) diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_prelim.ML --- /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 diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_reconstruct_proof.ML --- /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 + diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_transfer_proof.ML --- /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_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 [] = "\"\\"^(clstrs_to_string clstrs "")^"\\ "^" \\ False\"" +| clause_strs_to_isar clstrs thmvars = "\"\\"^(thmvars_to_quantstring thmvars "")^"\\"^(clstrs_to_string clstrs "")^"\\ "^"\\ 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 + + diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/recon_translate_proof.ML --- /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) diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/watcher.ML --- /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 *) diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/watcher.sig --- /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