src/HOL/Tools/ATP/watcher.ML
author paulson
Wed, 13 Apr 2005 09:48:41 +0200
changeset 15702 2677db44c795
parent 15684 5ec4d21889d6
child 15774 9df37a0e935d
permissions -rw-r--r--
new signalling primmitives for sml/nj compatibility
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     2
 (*  Title:      Watcher.ML
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     3
     Author:     Claire Quigley
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
     4
     Copyright   2004  University of Cambridge
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
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    16
(*use "Proof_Transfer";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    17
use "VampireCommunication";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    18
use "SpassCommunication";
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    19
use "modUnix";*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    20
(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    21
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    22
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    23
structure Watcher: WATCHER =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    24
  struct
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    25
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    26
val goals_being_watched = ref 0;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    27
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    28
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    29
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    30
fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    31
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    32
(********************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    33
(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    34
(********************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    35
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    36
fun outputArgs (toWatcherStr, []) = ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    37
|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    38
                                          TextIO.flushOut toWatcherStr;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    39
                                         outputArgs (toWatcherStr, xs))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    40
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    41
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    42
(*    gets individual args from instream and concatenates them into a list      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    43
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    44
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    45
fun getArgs (fromParentStr, toParentStr,ys) =  let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    46
                                       val thisLine = TextIO.input fromParentStr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    47
                                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    48
                                        ((ys@[thisLine]))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    49
                                    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    50
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    51
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    52
(*  Remove the \n character from the end of each filename                       *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    53
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    54
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    55
fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    56
                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    57
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    58
                        if (String.isPrefix "\n"  (implode backList )) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    59
                        then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    60
                             (implode (rev ((tl backList))))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    61
                        else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    62
                           (cmdStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    63
                    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    64
                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    65
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    66
(*  Send request to Watcher for a vampire to be called for filename in arg      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    67
(********************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    68
                    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    69
fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    70
                                     TextIO.flushOut toWatcherStr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    71
                                    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    72
                                     )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    73
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    74
(*****************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    75
(*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    76
(*****************************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    77
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    78
(* need to modify to send over hyps file too *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    79
fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    80
                                     TextIO.flushOut toWatcherStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    81
|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    82
                                                     let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    83
                                                        val dfg_dir = File.tmp_path (Path.basic "dfg");
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    84
                                                        (* need to check here if the directory exists and, if not, create it*)
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
    85
                                                         val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                                    
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    86
                                                         val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    87
                                                         val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    88
                                                         val dfg_create =if File.exists dfg_dir 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    89
                                                                         then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    90
                                                                             ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    91
                                                                         else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    92
                                                                               File.mkdir dfg_dir; 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    93
                                                         val probID = last(explode probfile)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    94
                                                         val dfg_path = File.sysify_path dfg_dir;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    95
                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    96
                                                       (*val _ = Posix.Process.wait ()*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    97
                                                       (*val _ =Unix.reap exec_tptp2x*)
15681
b667c22edb36 Changed prob1.dfg to prob_1.dfg
quigley
parents: 15658
diff changeset
    98
                                                         val newfile = dfg_path^"/prob"^"_"^(probID)^".dfg"
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
    99
                                       
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   100
                                                      in   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   101
                                                         goals_being_watched := (!goals_being_watched) + 1;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   102
                                                         OS.Process.sleep(Time.fromSeconds 1); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   103
                                                         (warning("dfg file is: "^newfile));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   104
                                                         sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   105
                                                         TextIO.flushOut toWatcherStr;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   106
                                                         Unix.reap exec_tptp2x; 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   107
                                                         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   108
                                                         callResProvers (toWatcherStr,args)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   109
                                           
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   110
                                                     end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   111
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   112
fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   113
                                     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   114
|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   115
                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   116
                                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   117
                                           )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   118
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   119
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   120
(* Send message to watcher to kill currently running vampires *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   121
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   122
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   123
fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   124
                            TextIO.flushOut toWatcherStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   125
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   126
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   127
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   128
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   129
(* Remove \n token from a vampire goal filename and extract   *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   130
(* prover, proverCmd, settings and file from input string     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   131
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   132
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   133
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   134
 fun takeUntil ch [] res  = (res, [])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   135
 |   takeUntil ch (x::xs) res = if   x = ch 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   136
                                then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   137
                                     (res, xs)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   138
                                else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   139
                                     takeUntil ch xs (res@[x])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   140
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   141
 fun getSettings [] settings = settings
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   142
|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   143
                                 in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   144
                                     getSettings rest (settings@[(implode set)])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   145
                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   146
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   147
fun separateFields str = let val (prover, rest) = takeUntil "*" str []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   148
                              val prover = implode prover
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   149
                              val (thmstring, rest) =  takeUntil "*" rest []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   150
                              val thmstring = implode thmstring
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   151
                              val (goalstring, rest) =  takeUntil "*" rest []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   152
                              val goalstring = implode goalstring
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   153
                              val (proverCmd, rest ) =  takeUntil "*" rest []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   154
                              val proverCmd = implode proverCmd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   155
                              
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   156
                              val (settings, rest) =  takeUntil "*" rest []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   157
                              val settings = getSettings settings []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   158
                              val (file, rest) =  takeUntil "*" rest []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   159
                              val file = implode file
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   160
                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   161
                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   162
                              val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   163
                              
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   164
                          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   165
                             (prover,thmstring,goalstring, proverCmd, settings, file)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   166
                          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   167
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   168
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   169
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   170
 fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   171
                     in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   172
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   173
                         if (String.isPrefix "\n"  (implode backList )) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   174
                         then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   175
                             separateFields ((rev ((tl backList))))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   176
                         else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   177
                           (separateFields (explode cmdStr))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   178
                     end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   179
                      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   180
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   181
fun getProofCmd (a,b,c,d,e,f) = d
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   182
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   183
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   184
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   185
(* Get commands from Isabelle                                 *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   186
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   187
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   188
fun getCmds (toParentStr,fromParentStr, cmdList) = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   189
                                       let val thisLine = TextIO.inputLine fromParentStr 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   190
                                       in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   191
                                          (if (thisLine = "End of calls\n") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   192
                                           then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   193
                                              (cmdList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   194
                                           else if (thisLine = "Kill children\n") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   195
                                                then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   196
                                                    (   TextIO.output (toParentStr,thisLine ); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   197
                                                        TextIO.flushOut toParentStr;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   198
                                                      (("","","","Kill children",[],"")::cmdList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   199
                                                     )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   200
                                              else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   201
                                                    in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   202
                                                      (*TextIO.output (toParentStr, thisCmd); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   203
                                                        TextIO.flushOut toParentStr;*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   204
                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   205
                                                    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   206
                                                    )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   207
                                            )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   208
                                        end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   209
                                    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   210
                                    
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   211
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   212
(*  Get Io-descriptor for polling of an input stream          *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   213
(**************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   214
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   215
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   216
fun getInIoDesc someInstr = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   217
    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   218
        val _ = TextIO.output (TextIO.stdOut, buf)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   219
        val ioDesc = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   220
	    case rd
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   221
	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   222
	       | _ => NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   223
     in (* since getting the reader will have terminated the stream, we need
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   224
	 * to build a new stream. *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   225
	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   226
	ioDesc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   227
    end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   228
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   229
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   230
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   231
(*  Set up a Watcher Process         *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   232
(*************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   233
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   234
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   235
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   236
fun setupWatcher () = let
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   237
          (** pipes for communication between parent and watcher **)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   238
          val p1 = Posix.IO.pipe ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   239
          val p2 = Posix.IO.pipe ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   240
	  fun closep () = (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   241
                Posix.IO.close (#outfd p1); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   242
                Posix.IO.close (#infd p1);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   243
                Posix.IO.close (#outfd p2); 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   244
                Posix.IO.close (#infd p2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   245
              )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   246
          (***********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   247
          (****** fork a watcher process and get it set up and going *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   248
          (***********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   249
          fun startWatcher (procList) =
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   250
                   (case  Posix.Process.fork() (***************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   251
		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   252
                                               (***************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   253
 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   254
                                                 (*************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   255
                  | NONE => let                  (* child - i.e. watcher  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   256
		      val oldchildin = #infd p1  (*************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   257
		      val fromParent = Posix.FileSys.wordToFD 0w0
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   258
		      val oldchildout = #outfd p2
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   259
		      val toParent = Posix.FileSys.wordToFD 0w1
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   260
                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   261
                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   262
                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   263
                      (*val goalstr = string_of_thm (the_goal)
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   264
                       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   265
                      val _ = TextIO.output (outfile,goalstr )
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   266
                      val _ =  TextIO.closeOut outfile*)
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   267
                      fun killChildren [] = ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   268
                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   269
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   270
                     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   271
           
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   272
                    (*************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   273
                    (* take an instream and poll its underlying reader for input *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   274
                    (*************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   275
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   276
                    fun pollParentInput () = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   277
                           
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   278
                               let val pd = OS.IO.pollDesc (fromParentIOD)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   279
                               in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   280
                               if (isSome pd ) then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   281
                                   let val pd' = OS.IO.pollIn (valOf pd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   282
                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   283
                                   in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   284
                                      if null pdl 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   285
                                      then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   286
                                         NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   287
                                      else if (OS.IO.isIn (hd pdl)) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   288
                                           then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   289
                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   290
                                           else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   291
                                               NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   292
                                   end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   293
                                 else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   294
                                     NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   295
                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   296
                            
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   297
                   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   298
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   299
                     fun pollChildInput (fromStr) = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   300
                           let val iod = getInIoDesc fromStr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   301
                           in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   302
                           if isSome iod 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   303
                           then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   304
                               let val pd = OS.IO.pollDesc (valOf iod)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   305
                               in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   306
                               if (isSome pd ) then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   307
                                   let val pd' = OS.IO.pollIn (valOf pd)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   308
                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   309
                                   in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   310
                                      if null pdl 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   311
                                      then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   312
                                         NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   313
                                      else if (OS.IO.isIn (hd pdl)) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   314
                                           then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   315
                                               SOME (getCmd (TextIO.inputLine fromStr))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   316
                                           else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   317
                                               NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   318
                                   end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   319
                                 else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   320
                                     NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   321
                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   322
                             else 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   323
                                 NONE
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   324
                            end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   325
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   326
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   327
                   (****************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   328
                   (* Check all vampire processes currently running for output                 *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   329
                   (****************************************************************************) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   330
                                                              (*********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   331
                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   332
                                                              (*********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   333
                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   334
                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   335
                                                val childPid = cmdchildPid childProc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   336
                                                val childCmd = fst(snd (cmdchildInfo childProc))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   337
                                                val childIncoming = pollChildInput childInput
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   338
                                                val parentID = Posix.ProcEnv.getppid()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   339
                                                val prover = cmdProver childProc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   340
                                                val thmstring = cmdThm childProc
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   341
                                                val goalstring = cmdGoal childProc
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   342
                                                val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   343
                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   344
                                                val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   345
                                            in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   346
                                              if (isSome childIncoming) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   347
                                              then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   348
                                                  (* check here for prover label on child*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   349
                                                   
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   350
                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   351
                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   352
                                                val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   353
                                              val childDone = (case prover of
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   354
                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   355
                                                   in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   356
                                                    if childDone      (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   357
                                                    then              (* child has found a proof and transferred it *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   358
                                                                      (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   359
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   360
                                                       (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   361
                                                       (* Remove this child and go on to check others*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   362
                                                       (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   363
                                                       ( reap(childPid, childInput, childOutput);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   364
                                                         checkChildren(otherChildren, toParentStr))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   365
                                                    else 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   366
                                                       (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   367
                                                       (* Keep this child and go on to check others  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   368
                                                       (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   369
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   370
                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   371
                                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   372
                                               else
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   373
                                                   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   374
                                                val _ = TextIO.output (outfile,"No child output " )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   375
                                                val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   376
                                                 in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   377
                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   378
                                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   379
                                            end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   380
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   381
                   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   382
                (********************************************************************)                  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   383
                (* call resolution processes                                        *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   384
                (* settings should be a list of strings                             *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   385
                (* e.g. ["-t 300", "-m 100000"]                                     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   386
                (* takes list of (string, string, string list, string)list proclist *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   387
                (********************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   388
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   389
                   fun execCmds  [] procList = procList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   390
                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   391
                                                     if (prover = "spass") 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   392
                                                     then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   393
                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   394
                                                         in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   395
                                                            execCmds cmds newProcList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   396
                                                         end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   397
                                                     else 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   398
                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   399
                                                         in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   400
                                                            execCmds cmds newProcList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   401
                                                         end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   402
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   403
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   404
                (****************************************)                  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   405
                (* call resolution processes remotely   *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   406
                (* settings should be a list of strings *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   407
                (* e.g. ["-t 300", "-m 100000"]         *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   408
                (****************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   409
  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   410
                   fun execRemoteCmds  [] procList = procList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   411
                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   412
                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   413
                                                 in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   414
                                                      execRemoteCmds  cmds newProcList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   415
                                                 end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   416
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   417
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   418
                   fun printList (outStr, []) = ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   419
                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   420
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   421
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   422
                (**********************************************)                  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   423
                (* Watcher Loop                               *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   424
                (**********************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   425
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   426
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   427
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   428
   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   429
                    fun keepWatching (toParentStr, fromParentStr,procList) = 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   430
                          let    fun loop (procList) =  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   431
                                 (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   432
                                 let val cmdsFromIsa = pollParentInput ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   433
                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   434
                                                  TextIO.flushOut toParentStr;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   435
                                                   killChildren (map (cmdchildPid) procList);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   436
                                                    ())
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   437
                                     
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   438
                                 in 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   439
                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   440
                                                                                       (**********************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   441
                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   442
                                         (                                             (**********************************)                             
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   443
                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   444
                                          then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   445
                                            (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   446
                                              let val childPids = map cmdchildPid procList 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   447
                                              in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   448
                                                 killChildren childPids;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   449
                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   450
                                              end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   451
                                             )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   452
                                          else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   453
                                            ( 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   454
                                              if ((length procList)<2)    (********************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   455
                                              then                        (* Execute locally  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   456
                                                 (                        (********************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   457
                                                  let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   458
                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   459
                                                    val parentID = Posix.ProcEnv.getppid()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   460
                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   461
                                                  in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   462
                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   463
                                                    loop (newProcList') 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   464
                                                  end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   465
                                                  )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   466
                                              else                         (************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   467
                                                                           (* Execute remotely     *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   468
                                                  (                        (************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   469
                                                  let 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   470
                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   471
                                                    val parentID = Posix.ProcEnv.getppid()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   472
                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   473
                                                  in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   474
                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   475
                                                    loop (newProcList') 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   476
                                                  end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   477
                                                  )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   478
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   479
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   480
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   481
                                              )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   482
                                           )                                              (******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   483
                                    else                                                  (* No new input from Isabelle *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   484
                                                                                          (******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   485
                                        (    let val newProcList = checkChildren ((procList), toParentStr)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   486
                                             in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   487
                                               OS.Process.sleep (Time.fromSeconds 1);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   488
                                               loop (newProcList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   489
                                             end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   490
                                         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   491
                                         )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   492
                                  end)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   493
                          in  
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   494
                              loop (procList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   495
                          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   496
                      
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   497
          
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   498
                      in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   499
                       (***************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   500
                       (*** Sort out pipes ********)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   501
                       (***************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   502
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   503
			Posix.IO.close (#outfd p1);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   504
			Posix.IO.close (#infd p2);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   505
			Posix.IO.dup2{old = oldchildin, new = fromParent};
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   506
                        Posix.IO.close oldchildin;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   507
			Posix.IO.dup2{old = oldchildout, new = toParent};
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   508
                        Posix.IO.close oldchildout;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   509
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   510
                        (***************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   511
                        (* start the watcher loop  *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   512
                        (***************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   513
                        keepWatching (toParentStr, fromParentStr, procList);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   514
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   515
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   516
                        (****************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   517
                        (* fake return value - actually want the watcher to loop until killed       *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   518
                        (****************************************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   519
                        Posix.Process.wordToPid 0w0
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   520
			
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   521
		      end);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   522
		(* end case *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   523
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   524
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   525
          val _ = TextIO.flushOut TextIO.stdOut
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   526
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   527
          (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   528
          (***  set watcher going ********)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   529
          (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   530
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   531
          val procList = []
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   532
          val pid = startWatcher (procList)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   533
          (**************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   534
          (* communication streams to watcher               *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   535
          (**************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   536
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   537
	  val instr = openInFD ("_exec_in", #infd p2)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   538
          val outstr = openOutFD ("_exec_out", #outfd p1)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   539
          
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   540
          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   541
           (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   542
           (* close the child-side fds    *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   543
           (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   544
            Posix.IO.close (#outfd p2);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   545
            Posix.IO.close (#infd p1);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   546
            (* set the fds close on exec *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   547
            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   548
            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   549
             
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   550
           (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   551
           (* return value                *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   552
           (*******************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   553
            PROC{pid = pid,
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   554
              instr = instr,
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   555
              outstr = outstr
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   556
            }
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   557
         end;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   558
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   559
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   560
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   561
(**********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   562
(* Start a watcher and set up signal handlers             *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   563
(**********************************************************)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   564
fun killWatcher pid= killChild pid;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   565
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   566
fun createWatcher () = let val mychild = childInfo (setupWatcher())
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   567
			   val streams =snd mychild
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   568
                           val childin = fst streams
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   569
                           val childout = snd streams
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   570
                           val childpid = fst mychild
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   571
                           
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   572
                           fun vampire_proofHandler (n) =
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   573
                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   574
                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   575
                          
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   576
                          (* fun spass_proofHandler (n:int) = (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   577
                                                      let val (reconstr, thmstring, goalstring) = getSpassInput childin
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   578
                                                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   579
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   580
                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   581
                                                         val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   582
                                                      in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   583
                                                         Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   584
                                                          Pretty.writeln(Pretty.str reconstr) ;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   585
                                                         Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   586
                                                         (*killWatcher childpid;*) () 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   587
                                                      end)*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   588
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   589
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   590
(*
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   591
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   592
fun spass_proofHandler (n:int) = (
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   593
                                                      let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   594
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   595
                                                         val _ = TextIO.output (outfile, ("In signal handler now\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   596
                                                         val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   597
                                                          val (reconstr, thmstring, goalstring) = getSpassInput childin
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   598
                                                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   599
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   600
                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   601
                                                         val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   602
                                                       in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   603
                                                        if ( (substring (reconstr, 0,1))= "[")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   604
                                                         then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   605
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   606
                                                          let val thm = thm_of_string thmstring
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   607
                                                              val clauses = make_clauses [thm]
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   608
                                                              val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   609
                                                         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   610
                                                          in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   611
                                                             Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15681
diff changeset
   612
                                                             Recon_Transfer.apply_res_thm reconstr goalstring;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   613
                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   614
                                                             killWatcher childpid; () 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   615
                                                          end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   616
                                                       else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   617
                                                           Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   618
                                                              Pretty.writeln(Pretty.str (goalstring^reconstr));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   619
                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   620
                                                             (*killWatcher childpid; *) reap (childpid,childin, childout);()   
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   621
                                                      end )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   622
*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   623
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   624
fun spass_proofHandler (n) = (
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   625
                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   626
                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   627
                                      val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   628
                                      val (reconstr, thmstring, goalstring) = getSpassInput childin
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   629
                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   630
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   631
                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   632
                                      val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   633
                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   634
                                                  if ( (substring (reconstr, 0,1))= "[")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   635
                                                  then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   636
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   637
                                                            (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   638
                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
15684
5ec4d21889d6 Reconstruction code, now packaged to avoid name clashes
paulson
parents: 15681
diff changeset
   639
                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   640
                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   641
                                                                 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   642
                                                                 goals_being_watched := ((!goals_being_watched) - 1);
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   643
                                                         
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   644
                                                                 if ((!goals_being_watched) = 0)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   645
                                                                 then 
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   646
                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   647
                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   648
                                                                         val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   649
                                                                     in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   650
                                                                         reap (childpid,childin, childout); ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   651
                                                                     end)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   652
                                                                 else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   653
                                                                    ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   654
                                                            )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   655
                                                    (* if there's no proof, but a message from Spass *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   656
                                                    else if ((substring (reconstr, 0,5))= "SPASS")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   657
                                                         then
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   658
                                                                 (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   659
                                                                     goals_being_watched := (!goals_being_watched) -1;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   660
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   661
                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   662
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   663
                                                                      if (!goals_being_watched = 0)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   664
                                                                      then 
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   665
                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   666
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   667
                                                                               val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   668
                                                                           in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   669
                                                                              reap (childpid,childin, childout); ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   670
                                                                           end )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   671
                                                                      else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   672
                                                                         ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   673
                                                                )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   674
                                                          (* if proof translation failed *)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   675
                                                          else if ((substring (reconstr, 0,5)) = "Proof")
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   676
                                                               then 
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   677
                                                                   (
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   678
                                                                     goals_being_watched := (!goals_being_watched) -1;
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   679
                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   680
                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   681
                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   682
                                                                      if (!goals_being_watched = 0)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   683
                                                                      then 
15658
2edb384bf61f watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents: 15652
diff changeset
   684
                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   685
                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   686
                                                                               val _ =  TextIO.closeOut outfile
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   687
                                                                           in
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   688
                                                                              reap (childpid,childin, childout); ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   689
                                                                           end )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   690
                                                                      else
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   691
                                                                         ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   692
                                                                )
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   693
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   694
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   695
                                                                else  (* add something here ?*)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   696
                                                                   ()
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   697
                                                             
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   698
                                       end)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   699
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   700
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   701
                        
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   702
                       in 
15702
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   703
                          IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
2677db44c795 new signalling primmitives for sml/nj compatibility
paulson
parents: 15684
diff changeset
   704
                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
15642
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   705
                          (childin, childout, childpid)
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   706
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   707
                       end
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   708
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   709
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   710
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   711
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   712
028059faa963 *** empty log message ***
quigley
parents:
diff changeset
   713
end (* structure Watcher *)