src/HOL/Tools/ATP/watcher.ML
author paulson
Thu, 22 Sep 2005 14:09:48 +0200
changeset 17583 c272b91b619f
parent 17568 e93f7510e1e1
child 17690 8ba7c3cd24a8
permissions -rw-r--r--
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
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
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     2
    ID:         $Id$
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     3
    Author:     Claire Quigley
4cb16144c81b added hearder lines and deleted some redundant material
paulson
parents: 15787
diff changeset
     4
    Copyright   2004  University of Cambridge
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     5
 *)
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
 (*  The watcher process starts a resolution process when it receives a     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     9
(*  message from Isabelle                                                  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    10
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    11
(*  and removes dead processes.  Also possible to kill all the resolution  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    12
(*  processes currently running.                                           *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    13
(*  Hardwired version of where to pick up the tptp files for the moment    *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    14
(***************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    15
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    16
signature WATCHER =
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    17
sig
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    18
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    19
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    20
(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    21
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    22
val callResProvers :
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
    23
    TextIO.outstream * (string*string*string*string*string) list 
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    24
    -> unit
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    25
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    26
(* Send message to watcher to kill currently running resolution provers *)
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    27
val callSlayer : TextIO.outstream -> unit
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    28
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    29
(* Start a watcher and set up signal handlers             *)
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    30
val createWatcher : 
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    31
    thm * (ResClause.clause * thm) Array.array -> 
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    32
    TextIO.instream * TextIO.outstream * Posix.Process.pid
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    33
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    34
(* Kill watcher process                                   *)
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    35
val killWatcher : Posix.Process.pid -> unit
17488
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
diff changeset
    36
val killWatcher' : int -> unit
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    37
end
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    38
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    39
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    40
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    41
structure Watcher: WATCHER =
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    42
struct
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    43
17488
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
diff changeset
    44
open Recon_Transfer
16805
fadf80952202 open ReconPrelim Recon_Transfer;
wenzelm
parents: 16767
diff changeset
    45
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    46
val goals_being_watched = ref 0;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    47
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
    48
val trace_path = Path.basic "watcher_trace";
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
    49
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
    50
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    51
(*  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
    52
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
    53
        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
    54
        instr : TextIO.instream,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    55
        outstr : TextIO.outstream
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
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    58
(*  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
    59
datatype cmdproc = CMDPROC of {
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    60
        prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    61
        cmd:  string,         (* The file containing the goal for res prover to prove *)     
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    62
        goalstring: string,   (* string representation of subgoal*) 
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    63
        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
    64
        instr : TextIO.instream,   (*  Input stream to child process *)
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    65
        outstr : TextIO.outstream};  (*  Output stream from child process *)
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    66
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    67
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
    68
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
    69
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    70
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
    71
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    72
fun reap(pid, instr, outstr) =
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
    73
  let val u = TextIO.closeIn instr;
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
    74
      val u = TextIO.closeOut outstr;
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
    75
      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
    76
  in status end
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    77
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    78
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
    79
	  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
    80
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    81
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
    82
          Posix.IO.mkTextWriter {
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    83
	      appendMode = false,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    84
              initBlkMode = true,
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    85
              name = name,  
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    86
              chunkSize=4096,
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
    87
              fd = fd};
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    88
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    89
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
    90
	  TextIO.mkOutstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    91
	    TextIO.StreamIO.mkOutstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    92
	      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
    93
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    94
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
    95
	  TextIO.mkInstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    96
	    TextIO.StreamIO.mkInstream (
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
    97
	      fdReader (name, fd), ""));
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
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   103
fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   104
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   105
fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   106
  (prover,(cmd, (instr,outstr)));
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   107
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   108
fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   109
  proc_handle;
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   110
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   111
fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   112
  prover;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   113
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   114
fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   115
  goalstring;
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   116
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   117
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   118
(*    gets individual args from instream and concatenates them into a list      *)
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   119
fun getArgs (fromParentStr, toParentStr, ys) =  
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   120
  let val thisLine = TextIO.input fromParentStr
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   121
  in ys@[thisLine] end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   122
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   123
                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   124
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   125
                   
17231
f42bc4f7afdf tidying up the Isabelle/ATP interface
paulson
parents: 17216
diff changeset
   126
fun callResProver (toWatcherStr,  arg) = 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   127
      (TextIO.output (toWatcherStr, arg^"\n"); 
17231
f42bc4f7afdf tidying up the Isabelle/ATP interface
paulson
parents: 17216
diff changeset
   128
       TextIO.flushOut toWatcherStr)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   129
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   130
(*****************************************************************************************)
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   131
(*  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
   132
(*  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
   133
(*****************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   134
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   135
    
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   136
(*Uses the $-character to separate items sent to watcher*)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   137
fun callResProvers (toWatcherStr,  []) = 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   138
      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   139
|   callResProvers (toWatcherStr,
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   140
                    (prover,goalstring, proverCmd,settings, 
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   141
                     probfile)  ::  args) =
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   142
      let val _ = File.write (File.tmp_path (Path.basic "tog_comms"))
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   143
                             (prover^goalstring^proverCmd^settings^
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   144
                              probfile)
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   145
      in TextIO.output (toWatcherStr,    
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   146
            (prover^"$"^goalstring^"$"^proverCmd^"$"^
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   147
             settings^"$"^probfile^"\n"));
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   148
         goals_being_watched := (!goals_being_watched) + 1;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   149
	 TextIO.flushOut toWatcherStr;
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   150
	 callResProvers (toWatcherStr,args)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   151
      end   
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   152
                                                
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   153
                                    
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   154
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   155
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   156
(* Send message to watcher to kill currently running vampires *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   157
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   158
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   159
fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   160
                            TextIO.flushOut toWatcherStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   161
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   162
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   163
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   164
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   165
(* Remove \n token from a vampire goal filename and extract   *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   166
(* prover, proverCmd, settings and file from input string     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   167
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   168
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   169
fun separateFields str =
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   170
  let val _ = File.append (File.tmp_path (Path.basic "sep_field"))
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   171
                          ("In separateFields, str is: " ^ str ^ "\n\n") 
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   172
      val [prover,goalstring,proverCmd,settingstr,probfile] = 
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   173
          String.tokens (fn c => c = #"$") str
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   174
      val settings = String.tokens (fn c => c = #"%") settingstr
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   175
      val _ = File.append (File.tmp_path (Path.basic "sep_comms"))                                                                                
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   176
                  ("Sep comms are: "^ str ^"**"^
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   177
                   prover^" goalstr:  "^goalstring^
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   178
                   "\n provercmd: "^proverCmd^
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   179
                   "\n prob  "^probfile^"\n\n")
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   180
  in
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   181
     (prover,goalstring, proverCmd, settings, probfile)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   182
  end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   183
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   184
val remove_newlines = String.translate (fn c => if c = #"\n" then "" else str c);
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   185
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   186
fun getCmd cmdStr = 
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   187
  let val cmdStr' = remove_newlines cmdStr
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   188
  in
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   189
      File.write (File.tmp_path (Path.basic"sepfields_call")) 
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   190
		 ("about to call separateFields with " ^ cmdStr');
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   191
      separateFields cmdStr'
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
   192
  end;
15642
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
(* Get commands from Isabelle                                 *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   196
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   197
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   198
fun getCmds (toParentStr,fromParentStr, cmdList) = 
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   199
  let val thisLine = TextIO.inputLine fromParentStr 
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   200
      val _ = File.append (File.tmp_path (Path.basic "parent_comms")) thisLine
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   201
  in
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   202
     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   203
     else if thisLine = "Kill children\n"
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   204
     then (TextIO.output (toParentStr,thisLine ); 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   205
	   TextIO.flushOut toParentStr;
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   206
	   (("","","Kill children",[],"")::cmdList)  )
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   207
     else let val thisCmd = getCmd thisLine 
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   208
	       (*********************************************************)
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   209
	       (* thisCmd = (prover,proverCmd, settings, file)*)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   210
	       (* i.e. put back into tuple format                       *)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   211
	       (*********************************************************)
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   212
	   in
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   213
	       getCmds (toParentStr, fromParentStr, thisCmd::cmdList)
16475
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   214
	   end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   215
  end
8f3ba52a7937 using TPTP2X_HOME; indentation, etc
paulson
parents: 16357
diff changeset
   216
	    
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16260
diff changeset
   217
                                                                  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   218
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   219
(*  Get Io-descriptor for polling of an input stream          *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   220
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   221
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   222
fun getInIoDesc someInstr = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   223
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   224
        val _ = TextIO.output (TextIO.stdOut, buf)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   225
        val ioDesc = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   226
	    case rd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   227
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   228
	       | _ => NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   229
     in (* since getting the reader will have terminated the stream, we need
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   230
	 * to build a new stream. *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   231
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   232
	ioDesc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   233
    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   234
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   235
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   236
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   237
(*  Set up a Watcher Process         *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   238
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   239
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   240
fun getProofCmd (a,c,d,e,f) = d
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   241
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   242
fun prems_string_of th =
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   243
  Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   244
17525
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   245
fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   246
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   247
fun killChildren procs = List.app (ignore o killChild) procs;
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   248
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   249
 (*************************************************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   250
 (* take an instream and poll its underlying reader for input *)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   251
 (*************************************************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   252
 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   253
 fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   254
   case OS.IO.pollDesc fromParentIOD
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   255
   of SOME pd =>
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   256
       let val pd' = OS.IO.pollIn pd
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   257
	   val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   258
       in
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   259
	  if null pdl 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   260
	  then NONE
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   261
	  else if OS.IO.isIn (hd pdl)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   262
	       then SOME (getCmds (toParentStr, fromParentStr, []))
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   263
	       else NONE
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   264
       end
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   265
   | NONE => NONE;
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   266
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   267
(*get the number of the subgoal from the filename: the last digit string*)
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   268
fun number_from_filename s =
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   269
  case String.tokens (not o Char.isDigit) s of
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   270
      [] => (File.append (File.tmp_path trace_path) 
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   271
		    "\nWatcher could not read subgoal nunber!!";
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   272
		    raise ERROR)
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   273
    | numbers => valOf (Int.fromString (List.last numbers));
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   274
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   275
fun setupWatcher (thm,clause_arr) = 
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   276
  let
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   277
    (** pipes for communication between parent and watcher **)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   278
    val p1 = Posix.IO.pipe ()
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   279
    val p2 = Posix.IO.pipe ()
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   280
    fun closep () = 
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   281
	 (Posix.IO.close (#outfd p1); 
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   282
	  Posix.IO.close (#infd p1);
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   283
	  Posix.IO.close (#outfd p2); 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   284
	  Posix.IO.close (#infd p2))
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   285
    (***********************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   286
    (****** fork a watcher process and get it set up and going *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   287
    (***********************************************************)
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   288
    fun startWatcher procList =
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   289
     (case  Posix.Process.fork() (***************************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   290
      of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   291
				    (***************************************)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   292
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   293
				      (*************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   294
       | NONE => let                  (* child - i.e. watcher  *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   295
	   val oldchildin = #infd p1  (*************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   296
	   val fromParent = Posix.FileSys.wordToFD 0w0
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   297
	   val oldchildout = #outfd p2
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   298
	   val toParent = Posix.FileSys.wordToFD 0w1
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   299
	   val fromParentIOD = Posix.FileSys.fdToIOD fromParent
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   300
	   val fromParentStr = openInFD ("_exec_in_parent", fromParent)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   301
	   val toParentStr = openOutFD ("_exec_out_parent", toParent)
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   302
	   val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   303
	 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   304
	  fun pollChildInput fromStr = 
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   305
	   let val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   306
			 ("\nIn child_poll")
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   307
	       val iod = getInIoDesc fromStr
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   308
	   in 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   309
	     if isSome iod 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   310
	     then 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   311
	       let val pd = OS.IO.pollDesc (valOf iod)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   312
	       in 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   313
	       if isSome pd then 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   314
		   let val pd' = OS.IO.pollIn (valOf pd)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   315
		       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   316
		   in
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   317
		      if null pdl 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   318
		      then
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   319
			(File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl\n"; 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   320
			 NONE)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   321
		      else if OS.IO.isIn (hd pdl)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   322
		      then
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   323
			   let val inval = TextIO.inputLine fromStr
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   324
			       val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n")
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   325
			   in SOME inval end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   326
		      else
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   327
                        (File.append (File.tmp_path (Path.basic"child_poll_res")) "Null pdl \n";
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   328
                         NONE)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   329
		   end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   330
		 else NONE
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   331
		 end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   332
	     else NONE
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   333
	   end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   334
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   335
	(* Check all ATP processes currently running for output                 *)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   336
						   (*********************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   337
	 fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   338
						   (*********************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   339
	 |   checkChildren ((childProc::otherChildren), toParentStr) = 
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   340
	       let val _ = File.append (File.tmp_path trace_path) 
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   341
			      ("\nIn check child, length of queue:"^
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   342
			        Int.toString (length (childProc::otherChildren)))
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   343
		   val (childInput,childOutput) = cmdstreamsOf childProc
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   344
		   val child_handle = cmdchildHandle childProc
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   345
		   (* childCmd is the .dfg file that the problem is in *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   346
		   val childCmd = fst(snd (cmdchildInfo childProc))
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   347
		   val _ = File.append (File.tmp_path trace_path) 
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   348
			      ("\nchildCmd = " ^ childCmd)
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   349
		   val sg_num = number_from_filename childCmd
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   350
		   val childIncoming = pollChildInput childInput
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   351
		   val _ = File.append (File.tmp_path trace_path) 
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   352
			         "\nfinished polling child"
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   353
		   val parentID = Posix.ProcEnv.getppid()
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   354
		   val prover = cmdProver childProc
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   355
		   val prems_string = prems_string_of thm
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   356
		   val goalstring = cmdGoal childProc							
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   357
		   val _ =  File.append (File.tmp_path trace_path) 
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   358
		             ("\nsubgoals forked to checkChildren: " ^ goalstring)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   359
	       in 
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   360
		 if isSome childIncoming
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   361
		 then 
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   362
		   (* check here for prover label on child*)
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   363
		   let val _ = File.append (File.tmp_path trace_path) 
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   364
			        ("\nInput available from childIncoming" ^
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   365
			         "\nchecking if proof found." ^
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   366
			         "\nchildCmd is " ^ childCmd ^ 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   367
			         "\ngoalstring is: " ^ goalstring ^ "\n\n")
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   368
		       val childDone = (case prover of
17488
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
diff changeset
   369
			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
diff changeset
   370
			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   371
			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   372
		    in
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   373
		     if childDone
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   374
		     then (* child has found a proof and transferred it *)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   375
			(* Remove this child and go on to check others*)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   376
			(**********************************************)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   377
			(Unix.reap child_handle;
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   378
			 checkChildren(otherChildren, toParentStr))
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   379
		     else 
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   380
			(**********************************************)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   381
			(* Keep this child and go on to check others  *)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   382
			(**********************************************)
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   383
		       (childProc::(checkChildren (otherChildren, toParentStr)))
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   384
		  end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   385
		else
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   386
		  (File.append (File.tmp_path trace_path)
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   387
		               "\nNo child output";
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   388
		   childProc::(checkChildren (otherChildren, toParentStr)))
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   389
	       end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   390
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   391
	
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   392
     (********************************************************************)                  
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   393
     (* call resolution processes                                        *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   394
     (* settings should be a list of strings                             *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   395
     (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   396
     (* takes list of (string, string, string list, string)list proclist *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   397
     (********************************************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   398
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   399
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   400
(*** add subgoal id num to this *)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   401
	fun execCmds  [] procList = procList
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   402
	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   403
	      let val _ = File.write (File.tmp_path (Path.basic "exec_child"))  
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   404
	                    (space_implode "\n" 
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   405
	                      (["About to execute command for goal:",
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   406
	                        goalstring, proverCmd] @ settings @
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   407
	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   408
	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   409
		       (Unix.execute(proverCmd, (settings@[file])))
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   410
		  val (instr, outstr) = Unix.streamsOf childhandle
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   411
		  
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   412
		  val newProcList = (CMDPROC{
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   413
				       prover = prover,
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   414
				       cmd = file,
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   415
				       goalstring = goalstring,
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   416
				       proc_handle = childhandle,
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   417
				       instr = instr,
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   418
				       outstr = outstr }) :: procList
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   419
     
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   420
		  val _ = File.append (File.tmp_path (Path.basic "exec_child")) 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   421
			    ("\nFinished at " ^
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   422
			     Date.toString(Date.fromTimeLocal(Time.now())))
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   423
	      in
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   424
		execCmds cmds newProcList
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   425
	      end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   426
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   427
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   428
     (****************************************)                  
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   429
     (* call resolution processes remotely   *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   430
     (* settings should be a list of strings *)
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   431
     (* e.g. ["-t300", "-m100000"]         *)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   432
     (****************************************)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   433
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   434
      (*  fun execRemoteCmds  [] procList = procList
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   435
	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   436
	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   437
		  in
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   438
		       execRemoteCmds  cmds newProcList
3b237822985d massive tidy-up and simplification
paulson
parents: 17317
diff changeset
   439
		  end
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   440
*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   441
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   442
     (**********************************************)                  
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   443
     (* Watcher Loop                               *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   444
     (**********************************************)
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   445
         val iterations_left = ref 500;  (*don't let it run forever*)
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   446
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   447
	 fun keepWatching (procList) = 
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   448
	   let fun loop procList =  
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   449
		let val _ = File.append (File.tmp_path trace_path) 
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   450
			       ("\nCalling pollParentInput: " ^ 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   451
			        Int.toString (!iterations_left));
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   452
		    val cmdsFromIsa = pollParentInput 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   453
		                       (fromParentIOD, fromParentStr, toParentStr)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   454
		in 
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   455
		   iterations_left := !iterations_left - 1;
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   456
		   if !iterations_left <= 0 
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   457
		   then (*Sadly, this code fails to terminate the watcher!*)
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   458
		    (File.append (File.tmp_path trace_path) 
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   459
			         "\nTimeout: Killing proof processes";
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   460
	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   461
		     TextIO.flushOut toParentStr;
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   462
		     killChildren (map cmdchildHandle procList);
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   463
		     exit 0)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   464
		   else if isSome cmdsFromIsa
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   465
		   then (*  deal with input from Isabelle *)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   466
		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   467
		     then 
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   468
		       let val child_handles = map cmdchildHandle procList 
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   469
		       in
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   470
			  killChildren child_handles;
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   471
			  loop []
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   472
		       end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   473
		     else
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   474
		       if length procList < 5     (********************)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   475
		       then                        (* Execute locally  *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   476
			 let 
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   477
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   478
			   val _ = Posix.ProcEnv.getppid()
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   479
			   val _ = File.append (File.tmp_path trace_path)
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   480
			      "\nJust execed a child"
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   481
			   val newProcList' = checkChildren (newProcList, toParentStr) 
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   482
			 in
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   483
			   File.append (File.tmp_path trace_path) 
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   484
			       ("\nOff to keep watching: " ^ 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   485
			        Int.toString (!iterations_left));
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   486
			   loop newProcList'
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   487
			 end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   488
		       else  (* Execute remotely              *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   489
			     (* (actually not remote for now )*)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   490
			 let 
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   491
			   val newProcList = execCmds (valOf cmdsFromIsa) procList
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   492
			   val _ = Posix.ProcEnv.getppid()
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   493
			   val newProcList' =checkChildren (newProcList, toParentStr) 
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   494
			 in
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   495
			   loop newProcList'
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   496
			 end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   497
		   else (* No new input from Isabelle *)
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   498
		     let val newProcList = checkChildren (procList, toParentStr)
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   499
		     in
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   500
		       File.append (File.tmp_path trace_path) 
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   501
			       ("\nNo new input, still watching: " ^ 
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   502
			        Int.toString (!iterations_left));
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   503
		       loop newProcList
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   504
		     end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   505
		 end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   506
	   in  
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   507
	       loop procList
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   508
	   end
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   509
	   
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   510
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   511
	   in
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   512
	    (***************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   513
	    (*** Sort out pipes ********)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   514
	    (***************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   515
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   516
	     Posix.IO.close (#outfd p1);
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   517
	     Posix.IO.close (#infd p2);
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   518
	     Posix.IO.dup2{old = oldchildin, new = fromParent};
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   519
	     Posix.IO.close oldchildin;
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   520
	     Posix.IO.dup2{old = oldchildout, new = toParent};
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   521
	     Posix.IO.close oldchildout;
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   522
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   523
	     (***************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   524
	     (* start the watcher loop  *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   525
	     (***************************)
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   526
	     keepWatching (procList);
17234
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   527
	     (****************************************************************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   528
(* fake return value - actually want the watcher to loop until killed *)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   529
	     (****************************************************************************)
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   530
	     Posix.Process.wordToPid 0w0
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   531
	   end);
12a9393c5d77 further tidying up of Isabelle-ATP link
paulson
parents: 17231
diff changeset
   532
     (* end case *)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   533
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   534
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   535
    val _ = TextIO.flushOut TextIO.stdOut
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   536
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   537
    (*******************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   538
    (***  set watcher going ********)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   539
    (*******************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   540
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   541
    val procList = []
17317
3f12de2e2e6e Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents: 17315
diff changeset
   542
    val pid = startWatcher procList
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   543
    (**************************************************)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   544
    (* communication streams to watcher               *)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   545
    (**************************************************)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   546
16061
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   547
    val instr = openInFD ("_exec_in", #infd p2)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   548
    val outstr = openOutFD ("_exec_out", #outfd p1)
8a139c1557bf A new structure and reduced indentation
paulson
parents: 16039
diff changeset
   549
    
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   550
  in
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   551
   (*******************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   552
   (* close the child-side fds    *)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   553
   (*******************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   554
    Posix.IO.close (#outfd p2);
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   555
    Posix.IO.close (#infd p1);
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   556
    (* set the fds close on exec *)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   557
    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   558
    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   559
     
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   560
   (*******************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   561
   (* return value                *)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   562
   (*******************************)
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   563
    PROC{pid = pid, instr = instr, outstr = outstr}
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   564
  end;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   565
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   566
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   567
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   568
(**********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   569
(* Start a watcher and set up signal handlers             *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   570
(**********************************************************)
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   571
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   572
fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
16039
dfe264950511 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents: 15919
diff changeset
   573
17488
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
diff changeset
   574
val killWatcher' = killWatcher o ResLib.pidOfInt;
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 17484
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
fun reapWatcher(pid, instr, outstr) =
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   577
  (TextIO.closeIn instr; TextIO.closeOut outstr;
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   578
   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   579
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   580
fun createWatcher (thm, clause_arr) =
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   581
 let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   582
     fun decr_watched() =
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   583
	  (goals_being_watched := !goals_being_watched - 1;
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   584
	   if !goals_being_watched = 0
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   585
	   then 
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   586
	     (File.append (File.tmp_path (Path.basic "reap_found"))
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   587
	       ("Reaping a watcher, childpid = "^
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   588
		LargeWord.toString (Posix.Process.pidToWord childpid)^"\n");
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   589
	      killWatcher childpid; reapWatcher (childpid,childin, childout))
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   590
	    else ())
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   591
     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   592
     fun proofHandler n = 
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   593
       let val outcome = TextIO.inputLine childin
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   594
	   val goalstring = TextIO.inputLine childin
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   595
	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   596
		        "\"\ngoalstring = " ^ goalstring ^
17568
e93f7510e1e1 trying to limit the looping
paulson
parents: 17525
diff changeset
   597
		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   598
       in 
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   599
	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   600
	 then (tracing (Recon_Transfer.apply_res_thm outcome goalstring);
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   601
	       decr_watched())
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   602
	 else if String.isPrefix "Invalid" outcome
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   603
	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "is not provable");
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   604
	       decr_watched())
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   605
	 else if String.isPrefix "Failure" outcome
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   606
	 then (tracing (Recon_Transfer.restore_linebreaks goalstring ^ "proof attempt failed");
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   607
	       decr_watched()) 
17216
df66d8feec63 improved formatting
paulson
parents: 17150
diff changeset
   608
	(* print out a list of rules used from clasimpset*)
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   609
	 else if String.isPrefix "Success" outcome
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   610
	 then (tracing (goalstring^outcome);
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   611
	       decr_watched())
17216
df66d8feec63 improved formatting
paulson
parents: 17150
diff changeset
   612
	  (* if proof translation failed *)
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   613
	 else if String.isPrefix "Translation failed" outcome
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   614
	 then (tracing (goalstring ^ Recon_Transfer.restore_linebreaks outcome);
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   615
	       decr_watched())
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   616
	 else  
17583
c272b91b619f removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents: 17568
diff changeset
   617
	      (tracing "System error in proof handler";
17435
0eed5a1c00c1 PARTIAL conversion to Vampire8
paulson
parents: 17422
diff changeset
   618
	       decr_watched())
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   619
       end
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   620
 in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
17216
df66d8feec63 improved formatting
paulson
parents: 17150
diff changeset
   621
    (childin, childout, childpid)
df66d8feec63 improved formatting
paulson
parents: 17150
diff changeset
   622
  end
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   623
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   624
end (* structure Watcher *)