src/HOL/Tools/ATP/SpassCommunication.ML
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15787 8fad4bd4e53c
child 15919 b30a35432f5a
permissions -rw-r--r--
added hearder lines and deleted some redundant material
quigley@15642
     1
(*  Title:      SpassCommunication.ml
paulson@15789
     2
    ID:         $Id$
quigley@15642
     3
    Author:     Claire Quigley
quigley@15642
     4
    Copyright   2004  University of Cambridge
quigley@15642
     5
*)
quigley@15642
     6
quigley@15642
     7
(***************************************************************************)
quigley@15642
     8
(*  Code to deal with the transfer of proofs from a Spass process          *)
quigley@15642
     9
(***************************************************************************)
quigley@15642
    10
quigley@15642
    11
(***********************************)
quigley@15642
    12
(*  Write Spass   output to a file *)
quigley@15642
    13
(***********************************)
quigley@15642
    14
quigley@15642
    15
fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
quigley@15642
    16
			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
quigley@15642
    17
			    then TextIO.output (fd, thisLine)
quigley@15642
    18
      			  else (
quigley@15642
    19
				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
quigley@15642
    20
 			 end;
quigley@15642
    21
quigley@15642
    22
quigley@15642
    23
(**********************************************************************)
quigley@15642
    24
(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
quigley@15642
    25
(*  Isabelle goal to be proved), then transfer the reconstruction     *)
quigley@15642
    26
(*  steps as a string to the input pipe of the main Isabelle process  *)
quigley@15642
    27
(**********************************************************************)
quigley@15642
    28
quigley@15642
    29
quigley@15782
    30
val atomize_tac =
quigley@15782
    31
    SUBGOAL
quigley@15782
    32
     (fn (prop,_) =>
quigley@15782
    33
	 let val ts = Logic.strip_assums_hyp prop
quigley@15782
    34
	 in EVERY1 
quigley@15782
    35
		[METAHYPS
quigley@15782
    36
		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
quigley@15782
    37
	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
quigley@15782
    38
     end);
quigley@15642
    39
quigley@15782
    40
quigley@15782
    41
fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num = 
quigley@15782
    42
 let val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
quigley@15782
    43
 in
quigley@15782
    44
SELECT_GOAL
quigley@15782
    45
  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
quigley@15782
    46
  METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs))]) sg_num
quigley@15782
    47
 end ;
quigley@15782
    48
quigley@15782
    49
quigley@15782
    50
fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
quigley@15642
    51
                         val thisLine = TextIO.inputLine fromChild 
quigley@15642
    52
			 in 
quigley@15642
    53
                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
quigley@15642
    54
			    then ( 
paulson@15684
    55
                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
quigley@15782
    56
                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
quigley@15782
    57
                                
quigley@15782
    58
			            in 
quigley@15782
    59
quigley@15782
    60
                                        TextIO.output(foo,(proofextract));TextIO.closeOut foo;
quigley@15782
    61
                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm
quigley@15782
    62
                                               
quigley@15782
    63
                                    end
quigley@15782
    64
                                  )
quigley@15782
    65
      			    else (
quigley@15782
    66
				
quigley@15782
    67
                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
quigley@15782
    68
                                )
quigley@15782
    69
 			 end;
quigley@15782
    70
quigley@15782
    71
quigley@15782
    72
(*
quigley@15782
    73
quigley@15782
    74
fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
quigley@15782
    75
                         val thisLine = TextIO.inputLine fromChild 
quigley@15782
    76
			 in 
quigley@15782
    77
                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
quigley@15782
    78
			    then ( 
quigley@15782
    79
                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
quigley@15782
    80
                                        val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring thm sg_num
quigley@15658
    81
                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
quigley@15642
    82
                               in
quigley@15642
    83
                                         TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
quigley@15642
    84
                                   
quigley@15642
    85
                                         TextIO.output (toParent, reconstr^"\n");
quigley@15642
    86
                                         TextIO.flushOut toParent;
quigley@15642
    87
                                         TextIO.output (toParent, thmstring^"\n");
quigley@15642
    88
                                         TextIO.flushOut toParent;
quigley@15642
    89
                                         TextIO.output (toParent, goalstring^"\n");
quigley@15642
    90
                                         TextIO.flushOut toParent;
quigley@15642
    91
                                          
quigley@15642
    92
                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
    93
                                         (* Attempt to prevent several signals from turning up simultaneously *)
paulson@15787
    94
                                         Posix.Process.sleep(Time.fromSeconds 1); ()
quigley@15642
    95
                                               
quigley@15642
    96
                                    end
quigley@15642
    97
                                      
quigley@15642
    98
                                  )
quigley@15642
    99
      			    else (
quigley@15642
   100
				
quigley@15782
   101
                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
quigley@15642
   102
                                )
quigley@15642
   103
 			 end;
quigley@15642
   104
quigley@15782
   105
*)
quigley@15642
   106
quigley@15642
   107
(*********************************************************************************)
quigley@15642
   108
(*  Inspect the output of a Spass   process to see if it has found a proof,      *)
quigley@15642
   109
(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
quigley@15642
   110
(*********************************************************************************)
quigley@15642
   111
quigley@15642
   112
 
quigley@15782
   113
fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) = 
quigley@15642
   114
                                      (*let val _ = Posix.Process.wait ()
quigley@15642
   115
                                      in*)
quigley@15782
   116
                                       
quigley@15642
   117
                                       if (isSome (TextIO.canInput(fromChild, 5)))
quigley@15642
   118
                                       then
quigley@15642
   119
                                       (
quigley@15642
   120
                                       let val thisLine = TextIO.inputLine fromChild  
quigley@15642
   121
                                           in                 
quigley@15642
   122
                                             if (String.isPrefix "Here is a proof" thisLine )
quigley@15642
   123
                                             then     
quigley@15642
   124
                                              ( 
quigley@15782
   125
                                                 let 
quigley@15782
   126
                                               val outfile =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_transfer")));
quigley@15782
   127
                                               val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
quigley@15782
   128
                                               val _ =  TextIO.closeOut outfile;
quigley@15782
   129
                                               in
quigley@15782
   130
                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num);
quigley@15782
   131
                                                true
quigley@15782
   132
                                               end)
quigley@15642
   133
                                             
quigley@15642
   134
                                             else 
quigley@15642
   135
                                                (
quigley@15782
   136
                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num)
quigley@15642
   137
                                                )
quigley@15642
   138
                                            end
quigley@15642
   139
                                           )
quigley@15642
   140
                                         else (false)
quigley@15642
   141
                                     (*  end*)
quigley@15642
   142
quigley@15782
   143
fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num) = 
quigley@15658
   144
                                       let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
quigley@15658
   145
                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
quigley@15782
   146
                                            val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
quigley@15642
   147
                                             
quigley@15642
   148
                                            val _ =  TextIO.closeOut outfile
quigley@15642
   149
                                       in 
quigley@15642
   150
                                       if (isSome (TextIO.canInput(fromChild, 5)))
quigley@15642
   151
                                       then
quigley@15642
   152
                                       (
quigley@15642
   153
                                       let val thisLine = TextIO.inputLine fromChild  
quigley@15642
   154
                                           in if ( thisLine = "SPASS beiseite: Proof found.\n" )
quigley@15642
   155
                                              then      
quigley@15642
   156
                                              (  
paulson@15787
   157
                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
quigley@15642
   158
                                                     val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   159
                                             
quigley@15642
   160
                                                     val _ =  TextIO.closeOut outfile
quigley@15642
   161
                                                 in 
quigley@15782
   162
                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num) 
quigley@15642
   163
                                                 end
quigley@15642
   164
                                               )   
quigley@15642
   165
                                               else if (thisLine= "SPASS beiseite: Completion found.\n" )
quigley@15642
   166
                                                   then  
quigley@15642
   167
quigley@15642
   168
                                                 (
paulson@15787
   169
                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
quigley@15642
   170
                                                             val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   171
                                             
quigley@15642
   172
                                                             val _ =  TextIO.closeOut outfile
quigley@15642
   173
                                                      in
quigley@15642
   174
                                                       
quigley@15642
   175
                                                        (*TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   176
                                                        TextIO.flushOut toParent;*)
quigley@15642
   177
                                                        TextIO.output (spass_proof_file, (thisLine));
quigley@15642
   178
                                                        TextIO.flushOut spass_proof_file;
quigley@15642
   179
                                                        TextIO.closeOut spass_proof_file;
quigley@15642
   180
                                                        (*TextIO.output (toParent, thisLine);
quigley@15642
   181
                                                        TextIO.flushOut toParent;
quigley@15642
   182
                                                        TextIO.output (toParent, "bar\n");
quigley@15642
   183
                                                        TextIO.flushOut toParent;*)
quigley@15642
   184
quigley@15642
   185
                                                       TextIO.output (toParent, thisLine^"\n");
quigley@15642
   186
                                                       TextIO.flushOut toParent;
quigley@15642
   187
                                                       TextIO.output (toParent, thmstring^"\n");
quigley@15642
   188
                                                       TextIO.flushOut toParent;
quigley@15642
   189
                                                       TextIO.output (toParent, goalstring^"\n");
quigley@15642
   190
                                                       TextIO.flushOut toParent;
quigley@15642
   191
                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   192
                                                       (* Attempt to prevent several signals from turning up simultaneously *)
paulson@15787
   193
                                                       Posix.Process.sleep(Time.fromSeconds 1);
quigley@15642
   194
                                                        true  
quigley@15642
   195
                                                      end) 
quigley@15642
   196
                                                     else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
quigley@15642
   197
                                                          then  
quigley@15642
   198
                                                (
quigley@15642
   199
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   200
                                                        TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   201
                                                        TextIO.flushOut toParent;
quigley@15642
   202
                                                        TextIO.output (toParent, thisLine);
quigley@15642
   203
                                                        TextIO.flushOut toParent;
quigley@15642
   204
quigley@15642
   205
                                                        true) 
quigley@15642
   206
                                                          else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
quigley@15642
   207
                                                 (
quigley@15642
   208
                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
quigley@15642
   209
                                                        TextIO.output (toParent,childCmd^"\n" );
quigley@15642
   210
                                                        TextIO.flushOut toParent;
quigley@15642
   211
                                                        TextIO.output (toParent, thisLine);
quigley@15642
   212
                                                        TextIO.flushOut toParent;
quigley@15642
   213
quigley@15642
   214
                                                        true)
quigley@15642
   215
                                                    else
quigley@15642
   216
                                                       (TextIO.output (spass_proof_file, (thisLine));
quigley@15642
   217
                                                       TextIO.flushOut spass_proof_file;
quigley@15782
   218
                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num))
quigley@15642
   219
quigley@15642
   220
                                              end
quigley@15642
   221
                                          )
quigley@15642
   222
                                         else 
quigley@15642
   223
                                             (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
quigley@15642
   224
                                      end
quigley@15642
   225
quigley@15642
   226
  
quigley@15642
   227
(***********************************************************************)
quigley@15642
   228
(*  Function used by the Isabelle process to read in a spass proof   *)
quigley@15642
   229
(***********************************************************************)
quigley@15642
   230
quigley@15642
   231
quigley@15642
   232
(***********************************************************************)
quigley@15642
   233
(*  Function used by the Isabelle process to read in a vampire proof   *)
quigley@15642
   234
(***********************************************************************)
quigley@15642
   235
quigley@15642
   236
(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
quigley@15642
   237
			 in 
quigley@15642
   238
                           if (thisLine = "%==============  End of proof. ==================\n" )
quigley@15642
   239
			    then
quigley@15642
   240
                               (
quigley@15642
   241
                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
quigley@15642
   242
                               )
quigley@15642
   243
                             else if (thisLine = "% Unprovable.\n" ) 
quigley@15642
   244
                                  then 
quigley@15642
   245
                                     (
quigley@15642
   246
                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
quigley@15642
   247
                                      )
quigley@15642
   248
                                   else if (thisLine = "% Proof not found.\n")
quigley@15642
   249
                                        then 
quigley@15642
   250
                                            (
quigley@15642
   251
                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
quigley@15642
   252
                                             )
quigley@15642
   253
quigley@15642
   254
quigley@15642
   255
                                         else 
quigley@15642
   256
                                            (
quigley@15642
   257
				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
quigley@15642
   258
                                             )
quigley@15642
   259
 			 end;
quigley@15642
   260
quigley@15642
   261
*)
quigley@15642
   262
quigley@15642
   263
fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
quigley@15642
   264
                          then
quigley@15642
   265
                               let val thisLine = TextIO.inputLine instr 
quigley@15658
   266
                                   val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   267
                                             
quigley@15642
   268
                                   val _ =  TextIO.closeOut outfile
quigley@15642
   269
			       in 
quigley@15642
   270
                                     if ( (substring (thisLine, 0,1))= "[")
quigley@15642
   271
                                     then 
quigley@15642
   272
			                 (*Pretty.writeln(Pretty.str (thisLine))*)
quigley@15642
   273
                                             let val reconstr = thisLine
quigley@15642
   274
                                                 val thmstring = TextIO.inputLine instr 
quigley@15642
   275
                                                 val goalstring = TextIO.inputLine instr   
quigley@15642
   276
                                             in
quigley@15642
   277
                                                 (reconstr, thmstring, goalstring)
quigley@15642
   278
                                             end
quigley@15642
   279
                                     else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
quigley@15642
   280
                                          then 
quigley@15642
   281
                                          (
quigley@15642
   282
                                             let val reconstr = thisLine
quigley@15642
   283
                                                 val thmstring = TextIO.inputLine instr
quigley@15642
   284
                                                 val goalstring = TextIO.inputLine instr
quigley@15642
   285
                                             in
quigley@15642
   286
                                                 (reconstr, thmstring, goalstring)
quigley@15642
   287
                                             end
quigley@15642
   288
                                          )
quigley@15642
   289
                                         else if (thisLine = "Proof found but translation failed!")
quigley@15642
   290
                                              then
quigley@15642
   291
  						(
quigley@15642
   292
						   let val reconstr = thisLine
quigley@15642
   293
                                                       val thmstring = TextIO.inputLine instr
quigley@15642
   294
                                                       val goalstring = TextIO.inputLine instr
quigley@15658
   295
						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
quigley@15642
   296
                                    		val _ = TextIO.output (outfile, (thisLine))
quigley@15642
   297
                                     			 val _ =  TextIO.closeOut outfile
quigley@15642
   298
                                                   in
quigley@15642
   299
                                                      (reconstr, thmstring, goalstring)
quigley@15642
   300
                                                   end
quigley@15642
   301
						)
quigley@15642
   302
                                        	 else
quigley@15642
   303
                                                     getSpassInput instr
quigley@15642
   304
                                            
quigley@15642
   305
 			        end
quigley@15642
   306
                          else 
quigley@15782
   307
                              ("No output from reconstruction process.\n","","")
quigley@15642
   308
quigley@15642
   309