src/HOL/Tools/ATP/SpassCommunication.ML
author quigley
Wed Apr 06 12:01:37 2005 +0200 (2005-04-06 ago)
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
permissions -rw-r--r--
watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley@15642
     1
(*  Title:      SpassCommunication.ml
quigley@15642
     2
    Author:     Claire Quigley
quigley@15642
     3
    Copyright   2004  University of Cambridge
quigley@15642
     4
*)
quigley@15642
     5
quigley@15642
     6
(***************************************************************************)
quigley@15642
     7
(*  Code to deal with the transfer of proofs from a Spass process          *)
quigley@15642
     8
(***************************************************************************)
quigley@15642
     9
quigley@15642
    10
(***********************************)
quigley@15642
    11
(*  Write Spass   output to a file *)
quigley@15642
    12
(***********************************)
quigley@15642
    13
quigley@15642
    14
fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
quigley@15642
    15
			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
quigley@15642
    16
			    then TextIO.output (fd, thisLine)
quigley@15642
    17
      			  else (
quigley@15642
    18
				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
quigley@15642
    19
 			 end;
quigley@15642
    20
quigley@15642
    21
quigley@15642
    22
(**********************************************************************)
quigley@15642
    23
(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
quigley@15642
    24
(*  Isabelle goal to be proved), then transfer the reconstruction     *)
quigley@15642
    25
(*  steps as a string to the input pipe of the main Isabelle process  *)
quigley@15642
    26
(**********************************************************************)
quigley@15642
    27
quigley@15642
    28
quigley@15642
    29
quigley@15642
    30
fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let 
quigley@15642
    31
                         val thisLine = TextIO.inputLine fromChild 
quigley@15642
    32
			 in 
quigley@15642
    33
                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
quigley@15642
    34
			    then ( 
quigley@15642
    35
                                    let val proofextract = extract_proof (currentString^thisLine)
quigley@15642
    36
                                        val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
quigley@15658
    37
                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
quigley@15642
    38
                               in
quigley@15642
    39
                                         TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
quigley@15642
    40
                                   
quigley@15642
    41
                                         TextIO.output (toParent, reconstr^"\n");
quigley@15642
    42
                                         TextIO.flushOut toParent;
quigley@15642
    43
                                         TextIO.output (toParent, thmstring^"\n");
quigley@15642
    44
                                         TextIO.flushOut toParent;
quigley@15642
    45
                                         TextIO.output (toParent, goalstring^"\n");
quigley@15642
    46
                                         TextIO.flushOut toParent;
quigley@15642
    47
                                          
quigley@15642
    48
                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
    49
                                         (* Attempt to prevent several signals from turning up simultaneously *)
quigley@15642
    50
                                         OS.Process.sleep(Time.fromSeconds 1)
quigley@15642
    51
                                               
quigley@15642
    52
                                    end
quigley@15642
    53
                                      
quigley@15642
    54
                                  )
quigley@15642
    55
      			    else (
quigley@15642
    56
				
quigley@15642
    57
                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine))
quigley@15642
    58
                                )
quigley@15642
    59
 			 end;
quigley@15642
    60
quigley@15642
    61
quigley@15642
    62
quigley@15642
    63
(*********************************************************************************)
quigley@15642
    64
(*  Inspect the output of a Spass   process to see if it has found a proof,      *)
quigley@15642
    65
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
quigley@15642
    66
(*********************************************************************************)
quigley@15642
    67
quigley@15642
    68
 
quigley@15642
    69
fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) = 
quigley@15642
    70
                                      (*let val _ = Posix.Process.wait ()
quigley@15642
    71
                                      in*)
quigley@15642
    72
                                       if (isSome (TextIO.canInput(fromChild, 5)))
quigley@15642
    73
                                       then
quigley@15642
    74
                                       (
quigley@15642
    75
                                       let val thisLine = TextIO.inputLine fromChild  
quigley@15642
    76
                                           in                 
quigley@15642
    77
                                             if (String.isPrefix "Here is a proof" thisLine )
quigley@15642
    78
                                             then     
quigley@15642
    79
                                              ( 
quigley@15642
    80
                                                 
quigley@15642
    81
                                                
quigley@15642
    82
                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine);
quigley@15642
    83
                                                true)
quigley@15642
    84
                                             
quigley@15642
    85
                                             else 
quigley@15642
    86
                                                (
quigley@15642
    87
                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd)
quigley@15642
    88
                                                )
quigley@15642
    89
                                            end
quigley@15642
    90
                                           )
quigley@15642
    91
                                         else (false)
quigley@15642
    92
                                     (*  end*)
quigley@15642
    93
quigley@15642
    94
fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) = 
quigley@15658
    95
                                       let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
quigley@15658
    96
                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
quigley@15642
    97
                                            val _ = TextIO.output (outfile, "checking proof found")
quigley@15642
    98
                                             
quigley@15642
    99
                                            val _ =  TextIO.closeOut outfile
quigley@15642
   100
                                       in 
quigley@15642
   101
                                       if (isSome (TextIO.canInput(fromChild, 5)))
quigley@15642
   102
                                       then
quigley@15642
   103
                                       (
quigley@15642
   104
                                       let val thisLine = TextIO.inputLine fromChild  
quigley@15642
   105
                                           in if ( thisLine = "SPASS beiseite: Proof found.\n" )
quigley@15642
   106
                                              then      
quigley@15642
   107
                                              (  
quigley@15658
   108
                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
quigley@15642
   109
                                                     val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   110
                                             
quigley@15642
   111
                                                     val _ =  TextIO.closeOut outfile
quigley@15642
   112
                                                 in 
quigley@15642
   113
                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) 
quigley@15642
   114
                                                 end
quigley@15642
   115
                                               )   
quigley@15642
   116
                                               else if (thisLine= "SPASS beiseite: Completion found.\n" )
quigley@15642
   117
                                                   then  
quigley@15642
   118
quigley@15642
   119
                                                 (
quigley@15658
   120
                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
quigley@15642
   121
                                                             val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   122
                                             
quigley@15642
   123
                                                             val _ =  TextIO.closeOut outfile
quigley@15642
   124
                                                      in
quigley@15642
   125
                                                       
quigley@15642
   126
                                                        (*TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   127
                                                        TextIO.flushOut toParent;*)
quigley@15642
   128
                                                        TextIO.output (spass_proof_file, (thisLine));
quigley@15642
   129
                                                        TextIO.flushOut spass_proof_file;
quigley@15642
   130
                                                        TextIO.closeOut spass_proof_file;
quigley@15642
   131
                                                        (*TextIO.output (toParent, thisLine);
quigley@15642
   132
                                                        TextIO.flushOut toParent;
quigley@15642
   133
                                                        TextIO.output (toParent, "bar\n");
quigley@15642
   134
                                                        TextIO.flushOut toParent;*)
quigley@15642
   135
quigley@15642
   136
                                                       TextIO.output (toParent, thisLine^"\n");
quigley@15642
   137
                                                       TextIO.flushOut toParent;
quigley@15642
   138
                                                       TextIO.output (toParent, thmstring^"\n");
quigley@15642
   139
                                                       TextIO.flushOut toParent;
quigley@15642
   140
                                                       TextIO.output (toParent, goalstring^"\n");
quigley@15642
   141
                                                       TextIO.flushOut toParent;
quigley@15642
   142
                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   143
                                                       (* Attempt to prevent several signals from turning up simultaneously *)
quigley@15642
   144
                                                       OS.Process.sleep(Time.fromSeconds 1);
quigley@15642
   145
                                                        true  
quigley@15642
   146
                                                      end) 
quigley@15642
   147
                                                     else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
quigley@15642
   148
                                                          then  
quigley@15642
   149
                                                (
quigley@15642
   150
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   151
                                                        TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   152
                                                        TextIO.flushOut toParent;
quigley@15642
   153
                                                        TextIO.output (toParent, thisLine);
quigley@15642
   154
                                                        TextIO.flushOut toParent;
quigley@15642
   155
quigley@15642
   156
                                                        true) 
quigley@15642
   157
                                                          else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
quigley@15642
   158
                                                 (
quigley@15642
   159
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   160
                                                        TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   161
                                                        TextIO.flushOut toParent;
quigley@15642
   162
                                                        TextIO.output (toParent, thisLine);
quigley@15642
   163
                                                        TextIO.flushOut toParent;
quigley@15642
   164
quigley@15642
   165
                                                        true)
quigley@15642
   166
                                                    else
quigley@15642
   167
                                                       (TextIO.output (spass_proof_file, (thisLine));
quigley@15642
   168
                                                       TextIO.flushOut spass_proof_file;
quigley@15642
   169
                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd))
quigley@15642
   170
quigley@15642
   171
                                              end
quigley@15642
   172
                                          )
quigley@15642
   173
                                         else 
quigley@15642
   174
                                             (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
quigley@15642
   175
                                      end
quigley@15642
   176
quigley@15642
   177
  
quigley@15642
   178
(***********************************************************************)
quigley@15642
   179
(*  Function used by the Isabelle process to read in a spass proof   *)
quigley@15642
   180
(***********************************************************************)
quigley@15642
   181
quigley@15642
   182
quigley@15642
   183
(***********************************************************************)
quigley@15642
   184
(*  Function used by the Isabelle process to read in a vampire proof   *)
quigley@15642
   185
(***********************************************************************)
quigley@15642
   186
quigley@15642
   187
(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
quigley@15642
   188
			 in 
quigley@15642
   189
                           if (thisLine = "%==============  End of proof. ==================\n" )
quigley@15642
   190
			    then
quigley@15642
   191
                               (
quigley@15642
   192
                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
quigley@15642
   193
                               )
quigley@15642
   194
                             else if (thisLine = "% Unprovable.\n" ) 
quigley@15642
   195
                                  then 
quigley@15642
   196
                                     (
quigley@15642
   197
                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
quigley@15642
   198
                                      )
quigley@15642
   199
                                   else if (thisLine = "% Proof not found.\n")
quigley@15642
   200
                                        then 
quigley@15642
   201
                                            (
quigley@15642
   202
                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
quigley@15642
   203
                                             )
quigley@15642
   204
quigley@15642
   205
quigley@15642
   206
                                         else 
quigley@15642
   207
                                            (
quigley@15642
   208
				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
quigley@15642
   209
                                             )
quigley@15642
   210
 			 end;
quigley@15642
   211
quigley@15642
   212
*)
quigley@15642
   213
quigley@15642
   214
fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
quigley@15642
   215
                          then
quigley@15642
   216
                               let val thisLine = TextIO.inputLine instr 
quigley@15658
   217
                                   val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   218
                                             
quigley@15642
   219
                                   val _ =  TextIO.closeOut outfile
quigley@15642
   220
			       in 
quigley@15642
   221
                                     if ( (substring (thisLine, 0,1))= "[")
quigley@15642
   222
                                     then 
quigley@15642
   223
			                 (*Pretty.writeln(Pretty.str (thisLine))*)
quigley@15642
   224
                                             let val reconstr = thisLine
quigley@15642
   225
                                                 val thmstring = TextIO.inputLine instr 
quigley@15642
   226
                                                 val goalstring = TextIO.inputLine instr   
quigley@15642
   227
                                             in
quigley@15642
   228
                                                 (reconstr, thmstring, goalstring)
quigley@15642
   229
                                             end
quigley@15642
   230
                                     else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
quigley@15642
   231
                                          then 
quigley@15642
   232
                                          (
quigley@15642
   233
                                             let val reconstr = thisLine
quigley@15642
   234
                                                 val thmstring = TextIO.inputLine instr
quigley@15642
   235
                                                 val goalstring = TextIO.inputLine instr
quigley@15642
   236
                                             in
quigley@15642
   237
                                                 (reconstr, thmstring, goalstring)
quigley@15642
   238
                                             end
quigley@15642
   239
                                          )
quigley@15642
   240
                                         else if (thisLine = "Proof found but translation failed!")
quigley@15642
   241
                                              then
quigley@15642
   242
  						(
quigley@15642
   243
						   let val reconstr = thisLine
quigley@15642
   244
                                                       val thmstring = TextIO.inputLine instr
quigley@15642
   245
                                                       val goalstring = TextIO.inputLine instr
quigley@15658
   246
						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
quigley@15642
   247
                                    		val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   248
                                     			 val _ =  TextIO.closeOut outfile
quigley@15642
   249
                                                   in
quigley@15642
   250
                                                      (reconstr, thmstring, goalstring)
quigley@15642
   251
                                                   end
quigley@15642
   252
						)
quigley@15642
   253
                                        	 else
quigley@15642
   254
                                                     getSpassInput instr
quigley@15642
   255
                                            
quigley@15642
   256
 			        end
quigley@15642
   257
                          else 
quigley@15642
   258
                              ("No output from Spass.\n","","")
quigley@15642
   259
quigley@15642
   260