src/HOL/Tools/ATP/watcher.ML
author paulson
Thu, 18 Aug 2005 13:09:21 +0200
changeset 17121 4c225f640b89
parent 16805 fadf80952202
child 17150 ce2a1aeb42aa
permissions -rw-r--r--
no need for TPTP2X unless SPASS is used
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15789
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     1
(*  Title:      Watcher.ML
16156
2f6fc19aba1e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents: 16100
diff changeset
     2
15789
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     3
    ID:         $Id$
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     4
    Author:     Claire Quigley
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     5
    Copyright   2004  University of Cambridge
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     6
 *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     7
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     8
 (***************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     9
 (*  The watcher process starts a resolution process when it receives a     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    10
(*  message from Isabelle                                                  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    11
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    12
(*  and removes dead processes.  Also possible to kill all the resolution  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    13
(*  processes currently running.                                           *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    14
(*  Hardwired version of where to pick up the tptp files for the moment    *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    15
(***************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    16
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    17
(*use "Proof_Transfer";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    18
use "VampireCommunication";
16089
9169bdf930f8 trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents: 16061
diff changeset
    19
use "SpassCommunication";*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    20
(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    21
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    22
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    23
structure Watcher: WATCHER =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    24
  struct
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    25
16805
fadf80952202 open ReconPrelim Recon_Transfer;
wenzelm
parents: 16767
diff changeset
    26
open ReconPrelim Recon_Transfer
fadf80952202 open ReconPrelim Recon_Transfer;
wenzelm
parents: 16767
diff changeset
    27
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    28
val goals_being_watched = ref 0;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    29
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    30
(*****************************************)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    31
(*  The result of calling createWatcher  *)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    32
(*****************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    33
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    34
datatype proc = PROC of {
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    35
        pid : Posix.Process.pid,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    36
        instr : TextIO.instream,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    37
        outstr : TextIO.outstream
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    38
      };
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    39
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    40
(*****************************************)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    41
(*  The result of calling executeToList  *)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    42
(*****************************************)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    43
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    44
datatype cmdproc = CMDPROC of {
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    45
        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    46
        cmd:  string,              (* The file containing the goal for res prover to prove *)     
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    47
        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    48
        goalstring: string,         (* string representation of subgoal*) 
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    49
        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    50
        instr : TextIO.instream,   (*  Input stream to child process *)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    51
        outstr : TextIO.outstream  (*  Output stream from child process *)
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    52
      };
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    53
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    54
type signal = Posix.Signal.signal
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    55
datatype exit_status = datatype Posix.Process.exit_status
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    56
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    57
val fromStatus = Posix.Process.fromStatus
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    58
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    59
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    60
fun reap(pid, instr, outstr) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    61
        let
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    62
		val u = TextIO.closeIn instr;
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    63
	        val u = TextIO.closeOut outstr;
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    64
	
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    65
		val (_, status) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    66
			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    67
	in
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    68
		status
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    69
	end
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    70
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    71
fun fdReader (name : string, fd : Posix.IO.file_desc) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    72
	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    73
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    74
fun fdWriter (name, fd) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    75
          Posix.IO.mkTextWriter {
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    76
	      appendMode = false,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    77
              initBlkMode = true,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    78
              name = name,  
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    79
              chunkSize=4096,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    80
              fd = fd
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    81
            };
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    82
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    83
fun openOutFD (name, fd) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    84
	  TextIO.mkOutstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    85
	    TextIO.StreamIO.mkOutstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    86
	      fdWriter (name, fd), IO.BLOCK_BUF));
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    87
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    88
fun openInFD (name, fd) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    89
	  TextIO.mkInstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    90
	    TextIO.StreamIO.mkInstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    91
	      fdReader (name, fd), ""));
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    92
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    93
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    94
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    95
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    96
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    97
fun killChild child_handle = Unix.reap child_handle 
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    98
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    99
fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   100
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   101
fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   102
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   103
fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   104
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   105
fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   106
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   107
fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   108
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   109
fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   110
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   111
fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   112
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   113
fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   114
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   115
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   116
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   117
(********************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   118
(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   119
(********************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   120
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   121
fun outputArgs (toWatcherStr, []) = ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   122
|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   123
                                          TextIO.flushOut toWatcherStr;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   124
                                         outputArgs (toWatcherStr, xs))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   125
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   126
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   127
(*    gets individual args from instream and concatenates them into a list      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   128
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   129
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   130
fun getArgs (fromParentStr, toParentStr,ys) =  let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   131
                                       val thisLine = TextIO.input fromParentStr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   132
                                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   133
                                        ((ys@[thisLine]))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   134
                                    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   135
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   136
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   137
(*  Remove the \n character from the end of each filename                       *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   138
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   139
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   140
(*fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   141
                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   142
                        if (String.isPrefix "\n"  (implode backList )) 
16089
9169bdf930f8 trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents: 16061
diff changeset
   143
                        then (implode (rev ((tl backList))))
9169bdf930f8 trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents: 16061
diff changeset
   144
                        else cmdStr
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   145
                    end*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   146
                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   147
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   148
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   149
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   150
                    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   151
fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
16089
9169bdf930f8 trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents: 16061
diff changeset
   152
                                     TextIO.flushOut toWatcherStr)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   153
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   154
(*****************************************************************************************)
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   155
(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   156
(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   157
(*****************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   158
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   159
    
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   160
(* need to modify to send over hyps file too *)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   161
fun callResProvers (toWatcherStr,  []) = 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   162
      (sendOutput (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   163
|   callResProvers (toWatcherStr,
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   164
                    (prover,thmstring,goalstring, proverCmd,settings,clasimpfile, 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   165
                     axfile, hypsfile,probfile)  ::  args) =
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   166
      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   167
                             (prover^thmstring^goalstring^proverCmd^settings^
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   168
                              clasimpfile^hypsfile^probfile)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   169
      in sendOutput (toWatcherStr,    
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   170
            (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   171
             settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n"));
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   172
         goals_being_watched := (!goals_being_watched) + 1;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   173
	 TextIO.flushOut toWatcherStr;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   174
	 callResProvers (toWatcherStr,args)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   175
      end   
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   176
                                                
16156
2f6fc19aba1e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents: 16100
diff changeset
   177
15782
a1863ea9052b Corrected the problem with the ATP directory.
quigley
parents: 15774
diff changeset
   178
(*
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   179
fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   180
                                     
15782
a1863ea9052b Corrected the problem with the ATP directory.
quigley
parents: 15774
diff changeset
   181
|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) =
a1863ea9052b Corrected the problem with the ATP directory.
quigley
parents: 15774
diff changeset
   182
                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n")
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   183
                                            
15782
a1863ea9052b Corrected the problem with the ATP directory.
quigley
parents: 15774
diff changeset
   184
     *)                                      
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   185
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   186
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   187
(* Send message to watcher to kill currently running vampires *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   188
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   189
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   190
fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   191
                            TextIO.flushOut toWatcherStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   192
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   193
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   194
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   195
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   196
(* Remove \n token from a vampire goal filename and extract   *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   197
(* prover, proverCmd, settings and file from input string     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   198
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   199
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   200
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   201
 fun takeUntil ch [] res  = (res, [])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   202
 |   takeUntil ch (x::xs) res = if   x = ch 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   203
                                then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   204
                                     (res, xs)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   205
                                else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   206
                                     takeUntil ch xs (res@[x])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   207
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   208
 fun getSettings [] settings = settings
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   209
|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   210
                                 in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   211
                                     getSettings rest (settings@[(implode set)])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   212
                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   213
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   214
fun separateFields str =
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   215
  let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   216
      val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   217
      val _ =  TextIO.closeOut outfile
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   218
      val (prover, rest) = takeUntil "$" str []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   219
      val prover = implode prover
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   220
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   221
      val (thmstring, rest) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   222
      val thmstring = implode thmstring
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   223
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   224
      val (goalstring, rest) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   225
      val goalstring = implode goalstring
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   226
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   227
      val (proverCmd, rest ) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   228
      val proverCmd = implode proverCmd
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   229
      
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   230
      val (settings, rest) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   231
      val settings = getSettings settings []
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   232
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   233
      val (clasimpfile, rest ) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   234
      val clasimpfile = implode clasimpfile
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   235
      
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   236
      val (hypsfile, rest ) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   237
      val hypsfile = implode hypsfile
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   238
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   239
      val (file, rest) =  takeUntil "$" rest []
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   240
      val file = implode file
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   241
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   242
      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   243
                  ("Sep comms are: "^(implode str)^"**"^
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   244
                   prover^" thmstring: "^thmstring^"\n goalstr:  "^goalstring^" \n provercmd: "^proverCmd^" \n  clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob  "^file^"\n\n")
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   245
  in
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   246
     (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   247
  end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   248
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   249
                      
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   250
(***********************************************************************************)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   251
(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   252
(***********************************************************************************)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   253
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   254
fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   255
  let
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   256
    (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   257
    val probID = List.last(explode probfile)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   258
    val wholefile = File.tmp_path (Path.basic ("ax_prob_" ^ probID))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   259
    
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   260
    (*** only include problem and clasimp for the moment, not sure 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   261
	 how to refer to hyps/local axioms just now ***)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   262
    val whole_prob_file = Unix.execute("/bin/cat", 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   263
	     [clasimpfile,(*axfile, hypsfile,*)probfile,  ">",
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   264
	      File.platform_path wholefile])
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   265
    
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   266
    val dfg_dir = File.tmp_path (Path.basic "dfg"); 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   267
    val dfg_path = File.platform_path dfg_dir;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   268
    
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   269
    (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   270
    val probID = List.last(explode probfile)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   271
    val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   272
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   273
    (*** only include problem and clasimp for the moment, not sure how to refer to ***)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   274
    (*** hyps/local axioms just now                                                ***)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   275
    val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   276
    (*** check if the directory exists and, if not, create it***)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   277
    val _ = 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   278
	if !SpassComm.spass
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   279
	then 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   280
	    if File.exists dfg_dir then warning("dfg dir exists")
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   281
	    else File.mkdir dfg_dir
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   282
	else
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   283
	    warning("not converting to dfg")
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   284
    
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   285
    val _ = if !SpassComm.spass then 
17121
4c225f640b89 no need for TPTP2X unless SPASS is used
paulson
parents: 16805
diff changeset
   286
		system (ResLib.helper_path "TPTP2X_HOME" "tptp2X" ^ 
4c225f640b89 no need for TPTP2X unless SPASS is used
paulson
parents: 16805
diff changeset
   287
		        " -fdfg -d " ^ dfg_path ^ " " ^
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   288
			File.platform_path wholefile)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   289
	      else 7
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   290
    val newfile =   if !SpassComm.spass 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   291
		    then 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   292
			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
16675
96bdc59afc05 Streamlined the signal handler in watcher.ML
quigley
parents: 16561
diff changeset
   293
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   294
		    else
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   295
			    (File.platform_path wholefile)
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   296
    val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   297
	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   298
  in
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   299
    (prover,thmstring,goalstring, proverCmd, settings,newfile)	
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   300
  end;
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   301
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   302
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   303
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   304
(* remove \n from end of command and put back into tuple format *)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   305
             
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   306
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   307
(*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n"
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   308
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   309
val cmdStr = "vampire*(length (rev xs) = length xs  [.]) & (length (rev (a # xs)) ~= length (a # xs) [.])*length (rev []) = length []*/homes/jm318/Vampire8/vkernel*-t 300%-m 100000*/local/scratch/clq20/23523/clasimp*/local/scratch/clq20/23523/hyps*/local/scratch/clq20/23523/prob_1\n"
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   310
 *)
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   311
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   312
(*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   313
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   314
 fun getCmd cmdStr = 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   315
       let val backList = rev(explode cmdStr)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   316
	   val _ = File.append (File.tmp_path (Path.basic"cmdStr")) cmdStr
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   317
       in
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   318
	   if (String.isPrefix "\n"  (implode backList )) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   319
	   then 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   320
	       let val newCmdStr = (rev(tl backList))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   321
	       in  File.write (File.tmp_path (Path.basic"backlist")) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   322
	                      ("about to call sepfields with "^(implode newCmdStr));
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   323
		   formatCmd (separateFields newCmdStr)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   324
	       end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   325
	   else formatCmd (separateFields (explode cmdStr))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   326
       end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   327
                      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   328
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   329
fun getProofCmd (a,b,c,d,e,f) = d
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   330
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   331
                        
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   332
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   333
(* Get commands from Isabelle                                 *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   334
(**************************************************************)
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   335
(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   336
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   337
fun getCmds (toParentStr,fromParentStr, cmdList) = 
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   338
  let val thisLine = TextIO.inputLine fromParentStr 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   339
      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   340
  in
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   341
     if (thisLine = "End of calls\n") 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   342
     then cmdList
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   343
     else if (thisLine = "Kill children\n") 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   344
     then 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   345
	 (   TextIO.output (toParentStr,thisLine ); 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   346
	     TextIO.flushOut toParentStr;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   347
	   (("","","","Kill children",[],"")::cmdList)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   348
	  )
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   349
     else  let val thisCmd = getCmd (thisLine) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   350
	       (*********************************************************)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   351
	       (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   352
	       (* i.e. put back into tuple format                       *)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   353
	       (*********************************************************)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   354
	   in
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   355
	     (*TextIO.output (toParentStr, thisCmd); 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   356
	       TextIO.flushOut toParentStr;*)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   357
	       getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   358
	   end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   359
  end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   360
	    
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   361
                                                                  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   362
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   363
(*  Get Io-descriptor for polling of an input stream          *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   364
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   365
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   366
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   367
fun getInIoDesc someInstr = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   368
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   369
        val _ = TextIO.output (TextIO.stdOut, buf)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   370
        val ioDesc = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   371
	    case rd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   372
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   373
	       | _ => NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   374
     in (* since getting the reader will have terminated the stream, we need
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   375
	 * to build a new stream. *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   376
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   377
	ioDesc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   378
    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   379
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   380
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   381
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   382
(*  Set up a Watcher Process         *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   383
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   384
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   385
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   386
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   387
fun setupWatcher (thm,clause_arr, num_of_clauses) = 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   388
  let
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   389
    (** pipes for communication between parent and watcher **)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   390
    val p1 = Posix.IO.pipe ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   391
    val p2 = Posix.IO.pipe ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   392
    fun closep () = (
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   393
	  Posix.IO.close (#outfd p1); 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   394
	  Posix.IO.close (#infd p1);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   395
	  Posix.IO.close (#outfd p2); 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   396
	  Posix.IO.close (#infd p2)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   397
	)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   398
    (***********************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   399
    (****** fork a watcher process and get it set up and going *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   400
    (***********************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   401
    fun startWatcher (procList) =
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   402
	     (case  Posix.Process.fork() (***************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   403
	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   404
					 (***************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   405
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   406
					   (*************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   407
	    | NONE => let                  (* child - i.e. watcher  *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   408
		val oldchildin = #infd p1  (*************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   409
		val fromParent = Posix.FileSys.wordToFD 0w0
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   410
		val oldchildout = #outfd p2
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   411
		val toParent = Posix.FileSys.wordToFD 0w1
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   412
		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   413
		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   414
		val toParentStr = openOutFD ("_exec_out_parent", toParent)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   415
		val sign = sign_of_thm thm
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   416
		val prems = prems_of thm
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   417
		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   418
		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   419
	       (* tracing *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   420
	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   421
		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   422
		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   423
		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   424
		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   425
		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   426
			 *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   427
		(*val goalstr = string_of_thm (the_goal)
16260
4a1f36eafe17 File.platform_path vs. File.shell_path;
wenzelm
parents: 16185
diff changeset
   428
		 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher")));  
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   429
		val _ = TextIO.output (outfile,goalstr )
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   430
		val _ =  TextIO.closeOut outfile*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   431
		fun killChildren [] = ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   432
	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   433
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   434
	       
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   435
     
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   436
	      (*************************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   437
	      (* take an instream and poll its underlying reader for input *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   438
	      (*************************************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   439
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   440
	      fun pollParentInput () = 
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   441
		 let val pd = OS.IO.pollDesc (fromParentIOD)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   442
		 in 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   443
		   if (isSome pd ) then 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   444
		       let val pd' = OS.IO.pollIn (valOf pd)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   445
			   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   446
			   val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   447
			     ("In parent_poll\n")	
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   448
		       in
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   449
			  if null pdl 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   450
			  then
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   451
			     NONE
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   452
			  else if (OS.IO.isIn (hd pdl)) 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   453
			       then
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   454
				  (SOME ( getCmds (toParentStr, fromParentStr, [])))
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   455
			       else
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   456
				   NONE
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   457
		       end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   458
		     else
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   459
			 NONE
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   460
		 end
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   461
		      
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   462
	       fun pollChildInput (fromStr) = 
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   463
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   464
		     let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   465
			           ("In child_poll\n")
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   466
                       val iod = getInIoDesc fromStr
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   467
		     in 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   468
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   469
		 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   470
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   471
		     if isSome iod 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   472
		     then 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   473
			 let val pd = OS.IO.pollDesc (valOf iod)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   474
			 in 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   475
			 if (isSome pd ) then 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   476
			     let val pd' = OS.IO.pollIn (valOf pd)
16156
2f6fc19aba1e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents: 16100
diff changeset
   477
				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   478
                                 
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   479
			     in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   480
				if null pdl 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   481
				then
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   482
				  ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   483
			           ("Null pdl \n");NONE)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   484
				else if (OS.IO.isIn (hd pdl)) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   485
				     then
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   486
					 (let val inval =  (TextIO.inputLine fromStr)
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   487
                              	              val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   488
					  in
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   489
						SOME inval
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   490
					  end)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   491
				     else
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   492
					   ( File.append (File.tmp_path (Path.basic "child_poll_res")) 
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   493
			           ("Null pdl \n");NONE)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   494
			     end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   495
			   else
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   496
			       NONE
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   497
			   end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   498
		       else 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   499
			   NONE
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   500
		 end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   501
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   502
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   503
	     (****************************************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   504
	     (* Check all vampire processes currently running for output                 *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   505
	     (****************************************************************************) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   506
							(*********************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   507
	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   508
							(*********************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   509
	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   510
		    let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   511
			           ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   512
                        val (childInput,childOutput) =  cmdstreamsOf childProc
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   513
			val child_handle= cmdchildHandle childProc
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   514
			(* childCmd is the .dfg file that the problem is in *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   515
			val childCmd = fst(snd (cmdchildInfo childProc))
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   516
                        val _ = File.append (File.tmp_path (Path.basic "child_command")) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   517
			           (childCmd^"\n")
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   518
			(* now get the number of the subgoal from the filename *)
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   519
			val sg_num = if (!SpassComm.spass )
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   520
				     then 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   521
					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   522
				     else
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   523
					int_of_string(hd (rev(explode childCmd)))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   524
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   525
			val childIncoming = pollChildInput childInput
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   526
 			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   527
			           ("finished polling child \n")
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   528
			val parentID = Posix.ProcEnv.getppid()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   529
			val prover = cmdProver childProc
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   530
			val thmstring = cmdThm childProc
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   531
			val sign = sign_of_thm thm
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   532
			val prems = prems_of thm
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   533
			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
16100
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   534
			val _ = warning("subgoals forked to checkChildren: "^prems_string)
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   535
			val goalstring = cmdGoal childProc							
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   536
			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   537
			           (prover^thmstring^goalstring^childCmd^"\n")
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   538
		    in 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   539
		      if (isSome childIncoming) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   540
		      then 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   541
			  (* check here for prover label on child*)
16100
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   542
			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
16478
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   543
		              val childDone = (case prover of
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   544
	                          "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
d0a1f6231e2f Added VampCommunication.ML.
quigley
parents: 16475
diff changeset
   545
                                 |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   546
			   in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   547
			    if childDone      (**********************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   548
			    then              (* child has found a proof and transferred it *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   549
					      (**********************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   550
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   551
			       (**********************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   552
			       (* Remove this child and go on to check others*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   553
			       (**********************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   554
			       ( Unix.reap child_handle;
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   555
				 checkChildren(otherChildren, toParentStr))
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   556
			    else 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   557
			       (**********************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   558
			       (* Keep this child and go on to check others  *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   559
			       (**********************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   560
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   561
				 (childProc::(checkChildren (otherChildren, toParentStr)))
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   562
			 end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   563
		       else
16100
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   564
			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   565
			  childProc::(checkChildren (otherChildren, toParentStr)))
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   566
		    end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   567
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   568
	     
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   569
	  (********************************************************************)                  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   570
	  (* call resolution processes                                        *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   571
	  (* settings should be a list of strings                             *)
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   572
	  (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   573
	  (* takes list of (string, string, string list, string)list proclist *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   574
	  (********************************************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   575
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   576
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   577
(*** add subgoal id num to this *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   578
	     fun execCmds  [] procList = procList
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   579
	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   580
	       in 
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   581
		 if (prover = "spass") 
16561
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   582
		 then 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   583
		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   584
		            (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   585
		       val (instr, outstr) = Unix.streamsOf childhandle
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   586
		       val newProcList =    (((CMDPROC{
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   587
					    prover = prover,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   588
					    cmd = file,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   589
					    thmstring = thmstring,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   590
					    goalstring = goalstring,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   591
					    proc_handle = childhandle,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   592
					    instr = instr,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   593
					    outstr = outstr })::procList))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   594
			val _ = File.append (File.tmp_path (Path.basic "exec_child"))  
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   595
			     ("\nexecuting command for goal:\n"^
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   596
			      goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   597
		   in
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   598
		      Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   599
		   end
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   600
		 else 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   601
		   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   602
		            (Unix.execute(proverCmd, (settings@[file])))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   603
		       val (instr, outstr) = Unix.streamsOf childhandle
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   604
		       
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   605
		       val newProcList =    (((CMDPROC{
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   606
					    prover = prover,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   607
					    cmd = file,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   608
					    thmstring = thmstring,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   609
					    goalstring = goalstring,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   610
					    proc_handle = childhandle,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   611
					    instr = instr,
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   612
					    outstr = outstr })::procList))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   613
	  
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   614
		       val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   615
		   in
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   616
		     Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
2bc33f0cfe9a tidying
paulson
parents: 16548
diff changeset
   617
		   end
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   618
		end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   619
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   620
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   621
	  (****************************************)                  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   622
	  (* call resolution processes remotely   *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   623
	  (* settings should be a list of strings *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   624
	  (* e.g. ["-t 300", "-m 100000"]         *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   625
	  (****************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   626
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   627
	   (*  fun execRemoteCmds  [] procList = procList
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   628
	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   629
				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   630
					   in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   631
						execRemoteCmds  cmds newProcList
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   632
					   end
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   633
*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   634
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   635
	     fun printList (outStr, []) = ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   636
	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   637
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   638
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   639
	  (**********************************************)                  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   640
	  (* Watcher Loop                               *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   641
	  (**********************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   642
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   643
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   644
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   645
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   646
	      fun keepWatching (toParentStr, fromParentStr,procList) = 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   647
		    let    fun loop (procList) =  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   648
			   (
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   649
			   let val cmdsFromIsa = pollParentInput ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   650
			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   651
					    TextIO.flushOut toParentStr;
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   652
					     killChildren (map (cmdchildHandle) procList);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   653
					      ())
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   654
			       
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   655
			   in 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   656
			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   657
										 (**********************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   658
			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   659
				   (                                             (**********************************)                             
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   660
				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   661
				    then 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   662
				      (
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   663
					let val child_handles = map cmdchildHandle procList 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   664
					in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   665
					   killChildren child_handles;
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   666
					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   667
					end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   668
					   
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   669
				       )
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   670
				    else
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   671
				      ( 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   672
					if ((length procList)<10)    (********************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   673
					then                        (* Execute locally  *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   674
					   (                        (********************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   675
					    let 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   676
					      val newProcList = execCmds (valOf cmdsFromIsa) procList
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   677
					      val parentID = Posix.ProcEnv.getppid()
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   678
          					 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   679
					      val newProcList' =checkChildren (newProcList, toParentStr) 
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   680
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   681
					      val _ = warning("off to keep watching...")
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   682
					     val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   683
					    in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   684
					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   685
					      loop (newProcList') 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   686
					    end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   687
					    )
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   688
					else                         (*********************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   689
								     (* Execute remotely              *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   690
								     (* (actually not remote for now )*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   691
					    (                        (*********************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   692
					    let 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   693
					      val newProcList = execCmds (valOf cmdsFromIsa) procList
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   694
					      val parentID = Posix.ProcEnv.getppid()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   695
					      val newProcList' =checkChildren (newProcList, toParentStr) 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   696
					    in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   697
					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   698
					      loop (newProcList') 
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   699
					    end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   700
					    )
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   701
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   702
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   703
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   704
					)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   705
				     )                                              (******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   706
			      else                                                  (* No new input from Isabelle *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   707
										    (******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   708
				  (    let val newProcList = checkChildren ((procList), toParentStr)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   709
				       in
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   710
					 (*Posix.Process.sleep (Time.fromSeconds 1);*)
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   711
					(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   712
					 loop (newProcList)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   713
				       end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   714
				   
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   715
				   )
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   716
			    end)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   717
		    in  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   718
			loop (procList)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   719
		    end
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   720
		
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   721
    
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   722
		in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   723
		 (***************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   724
		 (*** Sort out pipes ********)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   725
		 (***************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   726
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   727
		  Posix.IO.close (#outfd p1);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   728
		  Posix.IO.close (#infd p2);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   729
		  Posix.IO.dup2{old = oldchildin, new = fromParent};
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   730
		  Posix.IO.close oldchildin;
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   731
		  Posix.IO.dup2{old = oldchildout, new = toParent};
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   732
		  Posix.IO.close oldchildout;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   733
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   734
		  (***************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   735
		  (* start the watcher loop  *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   736
		  (***************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   737
		  keepWatching (toParentStr, fromParentStr, procList);
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   738
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   739
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   740
		  (****************************************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   741
		  (* fake return value - actually want the watcher to loop until killed       *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   742
		  (****************************************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   743
		  Posix.Process.wordToPid 0w0
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   744
		  
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   745
		end);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   746
	  (* end case *)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   747
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   748
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   749
    val _ = TextIO.flushOut TextIO.stdOut
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   750
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   751
    (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   752
    (***  set watcher going ********)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   753
    (*******************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   754
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   755
    val procList = []
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   756
    val pid = startWatcher (procList)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   757
    (**************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   758
    (* communication streams to watcher               *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   759
    (**************************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   760
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   761
    val instr = openInFD ("_exec_in", #infd p2)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   762
    val outstr = openOutFD ("_exec_out", #outfd p1)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   763
    
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   764
    in
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   765
     (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   766
     (* close the child-side fds    *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   767
     (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   768
      Posix.IO.close (#outfd p2);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   769
      Posix.IO.close (#infd p1);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   770
      (* set the fds close on exec *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   771
      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   772
      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   773
       
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   774
     (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   775
     (* return value                *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   776
     (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   777
      PROC{pid = pid,
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   778
	instr = instr,
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   779
	outstr = outstr
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   780
      }
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   781
   end;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   782
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   783
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   784
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   785
(**********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   786
(* Start a watcher and set up signal handlers             *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   787
(**********************************************************)
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   788
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   789
fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   790
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   791
fun reapWatcher(pid, instr, outstr) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   792
        let
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   793
		val u = TextIO.closeIn instr;
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   794
	        val u = TextIO.closeOut outstr;
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   795
	
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   796
		val (_, status) =
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   797
			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   798
	in
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   799
		status
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   800
	end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   801
16156
2f6fc19aba1e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents: 16100
diff changeset
   802
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   803
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   804
fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   805
			   val streams =snd mychild
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   806
                           val childin = fst streams
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   807
                           val childout = snd streams
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   808
                           val childpid = fst mychild
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   809
                           val sign = sign_of_thm thm
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   810
                           val prems = prems_of thm
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   811
                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   812
                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   813
                           fun vampire_proofHandler (n) =
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   814
                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   815
                           VampComm.getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   816
                          
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   817
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   818
fun spass_proofHandler (n) = (
16548
aa36ae6b955e Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents: 16520
diff changeset
   819
                                 let  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1")));
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   820
                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   821
                                      val _ =  TextIO.closeOut outfile
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   822
                                      val (reconstr, goalstring, thmstring) = SpassComm.getSpassInput childin
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   823
                                      val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal")));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   824
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   825
                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   826
                                      val _ =  TextIO.closeOut outfile
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   827
                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   828
                                                  if ( (substring (reconstr, 0,1))= "[")
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   829
                                                  then 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   830
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   831
                                                            (
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   832
                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   833
                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   834
                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   835
                                                                 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   836
                                                                 goals_being_watched := ((!goals_being_watched) - 1);
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   837
                                                         
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   838
                                                                 if ((!goals_being_watched) = 0)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   839
                                                                 then 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   840
                                                                    (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found")));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   841
                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   842
                                                                         val _ =  TextIO.closeOut outfile
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   843
                                                                     in
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   844
                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   845
                                                                     end)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   846
                                                                 else
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   847
                                                                    ()
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   848
                                                            )
16767
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   849
                                                    (* if there's no proof, but a message from Spass *)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   850
                                                    else if ((substring (reconstr, 0,5))= "SPASS")
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   851
                                                         then
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   852
                                                                 (
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   853
                                                                     goals_being_watched := (!goals_being_watched) -1;
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   854
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   855
                                                                      Pretty.writeln(Pretty.str ((Recon_Transfer.restore_linebreaks goalstring)^reconstr));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   856
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   857
                                                                      if (!goals_being_watched = 0)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   858
                                                                      then 
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   859
                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   860
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   861
                                                                               val _ =  TextIO.closeOut outfile
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   862
                                                                           in
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   863
                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   864
                                                                           end )
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   865
                                                                      else
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   866
                                                                         ()
16767
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   867
                                                                ) 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   868
						   (* print out a list of rules used from clasimpset*)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   869
                                                    else if ((substring (reconstr, 0,5))= "Rules")
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   870
                                                         then
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   871
                                                                 (
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   872
                                                                     goals_being_watched := (!goals_being_watched) -1;
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   873
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   874
                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   875
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   876
                                                                      if (!goals_being_watched = 0)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   877
                                                                      then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   878
                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   879
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   880
                                                                               val _ =  TextIO.closeOut outfile
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   881
                                                                           in
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   882
                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   883
                                                                           end )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   884
                                                                      else
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   885
                                                                         ()
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   886
                                                                )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   887
							
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   888
                                                          (* if proof translation failed *)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   889
                                                          else if ((substring (reconstr, 0,5)) = "Proof")
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   890
                                                               then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   891
                                                                   (
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   892
                                                                      goals_being_watched := (!goals_being_watched) -1;
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   893
                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   894
                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   895
                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   896
                                                                       if (!goals_being_watched = 0)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   897
                                                                       then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   898
                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   899
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   900
                                                                               val _ =  TextIO.closeOut outfile
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   901
                                                                            in
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   902
                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   903
                                                                            end )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   904
                                                                       else
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   905
                                                                          ( )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   906
                                                                      )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   907
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   908
							        else if ((substring (reconstr, 0,1)) = "%")
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   909
                                                               then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   910
                                                                   (
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   911
                                                                      goals_being_watched := (!goals_being_watched) -1;
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   912
                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   913
                                                                       Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   914
                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   915
                                                                       if (!goals_being_watched = 0)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   916
                                                                       then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   917
                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   918
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   919
                                                                               val _ =  TextIO.closeOut outfile
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   920
                                                                            in
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   921
                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   922
                                                                            end )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   923
                                                                       else
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   924
                                                                          ( )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   925
                                                                      )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   926
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   927
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   928
                                                                else  (* add something here ?*)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   929
                                                                   (
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   930
                                                                      goals_being_watched := (!goals_being_watched) -1;
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   931
                                                                      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   932
                                                                       Pretty.writeln(Pretty.str ("Ran out of options in handler"));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   933
                                                                       Pretty.writeln(Pretty.str  (oct_char "361"));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   934
                                                                       if (!goals_being_watched = 0)
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   935
                                                                       then 
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   936
                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   937
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   938
                                                                               val _ =  TextIO.closeOut outfile
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   939
                                                                            in
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   940
                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   941
                                                                            end )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   942
                                                                       else
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   943
                                                                          ( )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   944
                                                                      )
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   945
                                                                     
2d4433759b8d Fixed some problems with the signal handler.
quigley
parents: 16675
diff changeset
   946
                                                                           
16520
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   947
                                                            
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   948
                                       end)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   949
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   950
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   951
                        
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   952
                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   953
                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   954
                          (childin, childout, childpid)
7a9cda53bfa2 Integrated vampire lemma code.
quigley
parents: 16515
diff changeset
   955
16156
2f6fc19aba1e Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents: 16100
diff changeset
   956
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   957
16100
f80fc4bff933 Now uses File.write and File.append
paulson
parents: 16091
diff changeset
   958
  end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   959
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   960
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   961
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   962
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   963
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   964
end (* structure Watcher *)