*** empty log message ***
authorquigley
Thu Mar 31 19:29:26 2005 +0200 (2005-03-31)
changeset 15642028059faa963
parent 15641 b389f108c485
child 15643 5829f30fc20a
*** empty log message ***
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/VampireCommunication.ML
src/HOL/Tools/ATP/modUnix.ML
src/HOL/Tools/ATP/recon_gandalf_base.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_prelim.ML
src/HOL/Tools/ATP/recon_reconstruct_proof.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/ATP/watcher.sig
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Mar 31 19:29:26 2005 +0200
     1.3 @@ -0,0 +1,260 @@
     1.4 +(*  Title:      SpassCommunication.ml
     1.5 +    Author:     Claire Quigley
     1.6 +    Copyright   2004  University of Cambridge
     1.7 +*)
     1.8 +
     1.9 +(***************************************************************************)
    1.10 +(*  Code to deal with the transfer of proofs from a Spass process          *)
    1.11 +(***************************************************************************)
    1.12 +
    1.13 +(***********************************)
    1.14 +(*  Write Spass   output to a file *)
    1.15 +(***********************************)
    1.16 +
    1.17 +fun logSpassInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    1.18 +			 in if thisLine = "--------------------------SPASS-STOP------------------------------\n" 
    1.19 +			    then TextIO.output (fd, thisLine)
    1.20 +      			  else (
    1.21 +				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
    1.22 + 			 end;
    1.23 +
    1.24 +
    1.25 +(**********************************************************************)
    1.26 +(*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    1.27 +(*  Isabelle goal to be proved), then transfer the reconstruction     *)
    1.28 +(*  steps as a string to the input pipe of the main Isabelle process  *)
    1.29 +(**********************************************************************)
    1.30 +
    1.31 +
    1.32 +
    1.33 +fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString) = let 
    1.34 +                         val thisLine = TextIO.inputLine fromChild 
    1.35 +			 in 
    1.36 +                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    1.37 +			    then ( 
    1.38 +                                    let val proofextract = extract_proof (currentString^thisLine)
    1.39 +                                        val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
    1.40 +                                        val foo =   TextIO.openOut "foobar2";
    1.41 +                               in
    1.42 +                                         TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
    1.43 +                                   
    1.44 +                                         TextIO.output (toParent, reconstr^"\n");
    1.45 +                                         TextIO.flushOut toParent;
    1.46 +                                         TextIO.output (toParent, thmstring^"\n");
    1.47 +                                         TextIO.flushOut toParent;
    1.48 +                                         TextIO.output (toParent, goalstring^"\n");
    1.49 +                                         TextIO.flushOut toParent;
    1.50 +                                          
    1.51 +                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.52 +                                         (* Attempt to prevent several signals from turning up simultaneously *)
    1.53 +                                         OS.Process.sleep(Time.fromSeconds 1)
    1.54 +                                               
    1.55 +                                    end
    1.56 +                                      
    1.57 +                                  )
    1.58 +      			    else (
    1.59 +				
    1.60 +                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine))
    1.61 +                                )
    1.62 + 			 end;
    1.63 +
    1.64 +
    1.65 +
    1.66 +(*********************************************************************************)
    1.67 +(*  Inspect the output of a Spass   process to see if it has found a proof,      *)
    1.68 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.69 +(*********************************************************************************)
    1.70 +
    1.71 + 
    1.72 +fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) = 
    1.73 +                                      (*let val _ = Posix.Process.wait ()
    1.74 +                                      in*)
    1.75 +                                       if (isSome (TextIO.canInput(fromChild, 5)))
    1.76 +                                       then
    1.77 +                                       (
    1.78 +                                       let val thisLine = TextIO.inputLine fromChild  
    1.79 +                                           in                 
    1.80 +                                             if (String.isPrefix "Here is a proof" thisLine )
    1.81 +                                             then     
    1.82 +                                              ( 
    1.83 +                                                 
    1.84 +                                                
    1.85 +                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine);
    1.86 +                                                true)
    1.87 +                                             
    1.88 +                                             else 
    1.89 +                                                (
    1.90 +                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd)
    1.91 +                                                )
    1.92 +                                            end
    1.93 +                                           )
    1.94 +                                         else (false)
    1.95 +                                     (*  end*)
    1.96 +
    1.97 +fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) = 
    1.98 +                                       let val spass_proof_file =  TextIO.openAppend("spass_proof")
    1.99 +                                            val  outfile = TextIO.openOut("foo_checkspass");                                                                            
   1.100 +                                            val _ = TextIO.output (outfile, "checking proof found")
   1.101 +                                             
   1.102 +                                            val _ =  TextIO.closeOut outfile
   1.103 +                                       in 
   1.104 +                                       if (isSome (TextIO.canInput(fromChild, 5)))
   1.105 +                                       then
   1.106 +                                       (
   1.107 +                                       let val thisLine = TextIO.inputLine fromChild  
   1.108 +                                           in if ( thisLine = "SPASS beiseite: Proof found.\n" )
   1.109 +                                              then      
   1.110 +                                              (  
   1.111 +                                                 let val  outfile = TextIO.openOut("foo_proof");                                                                                (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
   1.112 +                                                     val _ = TextIO.output (outfile, (thisLine))
   1.113 +                                             
   1.114 +                                                     val _ =  TextIO.closeOut outfile
   1.115 +                                                 in 
   1.116 +                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd) 
   1.117 +                                                 end
   1.118 +                                               )   
   1.119 +                                               else if (thisLine= "SPASS beiseite: Completion found.\n" )
   1.120 +                                                   then  
   1.121 +
   1.122 +                                                 (
   1.123 +                                                      let    val  outfile = TextIO.openOut("foo_proof");                                                                               (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
   1.124 +                                                             val _ = TextIO.output (outfile, (thisLine))
   1.125 +                                             
   1.126 +                                                             val _ =  TextIO.closeOut outfile
   1.127 +                                                      in
   1.128 +                                                       
   1.129 +                                                        (*TextIO.output (toParent,childCmd^"\n" );
   1.130 +                                                        TextIO.flushOut toParent;*)
   1.131 +                                                        TextIO.output (spass_proof_file, (thisLine));
   1.132 +                                                        TextIO.flushOut spass_proof_file;
   1.133 +                                                        TextIO.closeOut spass_proof_file;
   1.134 +                                                        (*TextIO.output (toParent, thisLine);
   1.135 +                                                        TextIO.flushOut toParent;
   1.136 +                                                        TextIO.output (toParent, "bar\n");
   1.137 +                                                        TextIO.flushOut toParent;*)
   1.138 +
   1.139 +                                                       TextIO.output (toParent, thisLine^"\n");
   1.140 +                                                       TextIO.flushOut toParent;
   1.141 +                                                       TextIO.output (toParent, thmstring^"\n");
   1.142 +                                                       TextIO.flushOut toParent;
   1.143 +                                                       TextIO.output (toParent, goalstring^"\n");
   1.144 +                                                       TextIO.flushOut toParent;
   1.145 +                                                       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.146 +                                                       (* Attempt to prevent several signals from turning up simultaneously *)
   1.147 +                                                       OS.Process.sleep(Time.fromSeconds 1);
   1.148 +                                                        true  
   1.149 +                                                      end) 
   1.150 +                                                     else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
   1.151 +                                                          then  
   1.152 +                                                (
   1.153 +                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.154 +                                                        TextIO.output (toParent,childCmd^"\n" );
   1.155 +                                                        TextIO.flushOut toParent;
   1.156 +                                                        TextIO.output (toParent, thisLine);
   1.157 +                                                        TextIO.flushOut toParent;
   1.158 +
   1.159 +                                                        true) 
   1.160 +                                                          else if ( thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n" )                                                             then
   1.161 +                                                 (
   1.162 +                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.163 +                                                        TextIO.output (toParent,childCmd^"\n" );
   1.164 +                                                        TextIO.flushOut toParent;
   1.165 +                                                        TextIO.output (toParent, thisLine);
   1.166 +                                                        TextIO.flushOut toParent;
   1.167 +
   1.168 +                                                        true)
   1.169 +                                                    else
   1.170 +                                                       (TextIO.output (spass_proof_file, (thisLine));
   1.171 +                                                       TextIO.flushOut spass_proof_file;
   1.172 +                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd))
   1.173 +
   1.174 +                                              end
   1.175 +                                          )
   1.176 +                                         else 
   1.177 +                                             (TextIO.output (spass_proof_file, ("No proof output seen \n"));TextIO.closeOut spass_proof_file;false)
   1.178 +                                      end
   1.179 +
   1.180 +  
   1.181 +(***********************************************************************)
   1.182 +(*  Function used by the Isabelle process to read in a spass proof   *)
   1.183 +(***********************************************************************)
   1.184 +
   1.185 +
   1.186 +(***********************************************************************)
   1.187 +(*  Function used by the Isabelle process to read in a vampire proof   *)
   1.188 +(***********************************************************************)
   1.189 +
   1.190 +(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
   1.191 +			 in 
   1.192 +                           if (thisLine = "%==============  End of proof. ==================\n" )
   1.193 +			    then
   1.194 +                               (
   1.195 +                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   1.196 +                               )
   1.197 +                             else if (thisLine = "% Unprovable.\n" ) 
   1.198 +                                  then 
   1.199 +                                     (
   1.200 +                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   1.201 +                                      )
   1.202 +                                   else if (thisLine = "% Proof not found.\n")
   1.203 +                                        then 
   1.204 +                                            (
   1.205 +                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   1.206 +                                             )
   1.207 +
   1.208 +
   1.209 +                                         else 
   1.210 +                                            (
   1.211 +				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   1.212 +                                             )
   1.213 + 			 end;
   1.214 +
   1.215 +*)
   1.216 +
   1.217 +fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
   1.218 +                          then
   1.219 +                               let val thisLine = TextIO.inputLine instr 
   1.220 +                                   val  outfile = TextIO.openOut("foo_thisLine");                                                                     val _ = TextIO.output (outfile, (thisLine))
   1.221 +                                             
   1.222 +                                   val _ =  TextIO.closeOut outfile
   1.223 +			       in 
   1.224 +                                     if ( (substring (thisLine, 0,1))= "[")
   1.225 +                                     then 
   1.226 +			                 (*Pretty.writeln(Pretty.str (thisLine))*)
   1.227 +                                             let val reconstr = thisLine
   1.228 +                                                 val thmstring = TextIO.inputLine instr 
   1.229 +                                                 val goalstring = TextIO.inputLine instr   
   1.230 +                                             in
   1.231 +                                                 (reconstr, thmstring, goalstring)
   1.232 +                                             end
   1.233 +                                     else if (thisLine = "SPASS beiseite: Completion found.\n" ) 
   1.234 +                                          then 
   1.235 +                                          (
   1.236 +                                             let val reconstr = thisLine
   1.237 +                                                 val thmstring = TextIO.inputLine instr
   1.238 +                                                 val goalstring = TextIO.inputLine instr
   1.239 +                                             in
   1.240 +                                                 (reconstr, thmstring, goalstring)
   1.241 +                                             end
   1.242 +                                          )
   1.243 +                                         else if (thisLine = "Proof found but translation failed!")
   1.244 +                                              then
   1.245 +  						(
   1.246 +						   let val reconstr = thisLine
   1.247 +                                                       val thmstring = TextIO.inputLine instr
   1.248 +                                                       val goalstring = TextIO.inputLine instr
   1.249 +						      val  outfile = TextIO.openOut("foo_getSpass");
   1.250 +                                    		val _ = TextIO.output (outfile, (thisLine))
   1.251 +                                     			 val _ =  TextIO.closeOut outfile
   1.252 +                                                   in
   1.253 +                                                      (reconstr, thmstring, goalstring)
   1.254 +                                                   end
   1.255 +						)
   1.256 +                                        	 else
   1.257 +                                                     getSpassInput instr
   1.258 +                                            
   1.259 + 			        end
   1.260 +                          else 
   1.261 +                              ("No output from Spass.\n","","")
   1.262 +
   1.263 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Mar 31 19:29:26 2005 +0200
     2.3 @@ -0,0 +1,117 @@
     2.4 +(*  Title:      VampireCommunication.ml
     2.5 +    Author:     Claire Quigley
     2.6 +    Copyright   2004  University of Cambridge
     2.7 +*)
     2.8 +
     2.9 +(***************************************************************************)
    2.10 +(*  Code to deal with the transfer of proofs from a Vampire process        *)
    2.11 +(***************************************************************************)
    2.12 +
    2.13 +(***********************************)
    2.14 +(*  Write vampire output to a file *)
    2.15 +(***********************************)
    2.16 +
    2.17 +fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
    2.18 +			 in if thisLine = "%==============  End of proof. ==================\n" 
    2.19 +			    then TextIO.output (fd, thisLine)
    2.20 +      			  else (
    2.21 +				TextIO.output (fd, thisLine); logVampInput (instr,fd))
    2.22 + 			 end;
    2.23 +
    2.24 +(**********************************************************************)
    2.25 +(*  Transfer the vampire output from the watcher to the input pipe of *)
    2.26 +(*  the main Isabelle process                                         *)
    2.27 +(**********************************************************************)
    2.28 +
    2.29 +fun transferVampInput (fromChild, toParent, ppid) = let 
    2.30 +                         val thisLine = TextIO.inputLine fromChild 
    2.31 +			 in 
    2.32 +                            if (thisLine = "%==============  End of proof. ==================\n" )
    2.33 +			    then ( 
    2.34 +                                   TextIO.output (toParent, thisLine);
    2.35 +                                   TextIO.flushOut toParent
    2.36 +                                  )
    2.37 +      			    else (
    2.38 +				TextIO.output (toParent, thisLine); 
    2.39 +                                TextIO.flushOut toParent;
    2.40 +                                transferVampInput (fromChild, toParent, ppid)
    2.41 +                                )
    2.42 + 			 end;
    2.43 +
    2.44 +
    2.45 +(*********************************************************************************)
    2.46 +(*  Inspect the output of a vampire process to see if it has found a proof,      *)
    2.47 +(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    2.48 +(*********************************************************************************)
    2.49 +
    2.50 +fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = 
    2.51 +                                       if (isSome (TextIO.canInput(fromChild, 5)))
    2.52 +                                       then
    2.53 +                                       (
    2.54 +                                       let val thisLine = TextIO.inputLine fromChild  
    2.55 +                                           in                 
    2.56 +                                             if (thisLine = "% Proof found. Thanks to Tanya!\n" )
    2.57 +                                             then      
    2.58 +                                              ( 
    2.59 +                                                Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    2.60 +                                                TextIO.output (toParent,childCmd^"\n" );
    2.61 +                                                TextIO.flushOut toParent;
    2.62 +                                                TextIO.output (toParent, thisLine);
    2.63 +                                                TextIO.flushOut toParent;
    2.64 +
    2.65 +                                                transferVampInput (fromChild, toParent, ppid);
    2.66 +                                                true)
    2.67 +                                              else if (thisLine = "% Unprovable.\n" ) 
    2.68 +                                                   then 
    2.69 +                                                       (
    2.70 +                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
    2.71 +                                                        TextIO.output (toParent,childCmd^"\n" );
    2.72 +                                                        TextIO.flushOut toParent;
    2.73 +                                                        TextIO.output (toParent, thisLine);
    2.74 +                                                        TextIO.flushOut toParent;
    2.75 +
    2.76 +                                                        true)
    2.77 +                                                   else if (thisLine = "% Proof not found.\n")
    2.78 +                                                        then 
    2.79 +                                                            (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);                                                            TextIO.output (toParent,childCmd^"\n" );
    2.80 +                                                             TextIO.flushOut toParent;
    2.81 +                                                             TextIO.output (toParent, thisLine);
    2.82 +                                                             TextIO.flushOut toParent;
    2.83 +                                                             true)
    2.84 +                                                        else 
    2.85 +                                                           (
    2.86 +                                                             startVampireTransfer (fromChild, toParent, ppid, childCmd)
    2.87 +                                                            )
    2.88 +                                            end
    2.89 +                                           )
    2.90 +                                         else (false)
    2.91 +
    2.92 +
    2.93 +(***********************************************************************)
    2.94 +(*  Function used by the Isabelle process to read in a vampire proof   *)
    2.95 +(***********************************************************************)
    2.96 +
    2.97 +fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
    2.98 +			 in 
    2.99 +                           if (thisLine = "%==============  End of proof. ==================\n" )
   2.100 +			    then
   2.101 +                               (
   2.102 +                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   2.103 +                               )
   2.104 +                             else if (thisLine = "% Unprovable.\n" ) 
   2.105 +                                  then 
   2.106 +                                     (
   2.107 +                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   2.108 +                                      )
   2.109 +                                   else if (thisLine = "% Proof not found.\n")
   2.110 +                                        then 
   2.111 +                                            (
   2.112 +                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   2.113 +                                             )
   2.114 +
   2.115 +
   2.116 +                                         else 
   2.117 +                                            (
   2.118 +				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   2.119 +                                             )
   2.120 + 			 end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/ATP/modUnix.ML	Thu Mar 31 19:29:26 2005 +0200
     3.3 @@ -0,0 +1,295 @@
     3.4 +
     3.5 +(****************************************************************)
     3.6 +(****** Slightly modified version of sml Unix structure *********)
     3.7 +(****************************************************************)
     3.8 +
     3.9 +type signal = Posix.Signal.signal
    3.10 +datatype exit_status = datatype Posix.Process.exit_status
    3.11 +
    3.12 +val fromStatus = Posix.Process.fromStatus
    3.13 +
    3.14 +
    3.15 +
    3.16 +(* Internal function - inverse of Posix.Process.fromStatus. *)
    3.17 +local
    3.18 +	val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific
    3.19 +	in
    3.20 +		fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0))
    3.21 +		 |  toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w))
    3.22 +		 |  toStatus(W_SIGNALED s) =
    3.23 +		 	doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s)))
    3.24 +		 |  toStatus(W_STOPPED s) = 
    3.25 +		 	doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s)))
    3.26 +	end
    3.27 +
    3.28 +(*	fun reap{pid, infd, outfd} =
    3.29 +	let
    3.30 +		val u = Posix.IO.close infd;
    3.31 +		val u = Posix.IO.close outfd;
    3.32 +		val (_, status) =
    3.33 +			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    3.34 +	in
    3.35 +		toStatus status
    3.36 +	end
    3.37 +
    3.38 +*)
    3.39 +
    3.40 +	fun reap(pid, instr, outstr) =
    3.41 +	let
    3.42 +		val u = TextIO.closeIn instr;
    3.43 +	        val u = TextIO.closeOut outstr;
    3.44 +	
    3.45 +		val (_, status) =
    3.46 +			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    3.47 +	in
    3.48 +		toStatus status
    3.49 +	end
    3.50 +
    3.51 +fun fdReader (name : string, fd : Posix.IO.file_desc) =
    3.52 +	  Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
    3.53 +
    3.54 +fun fdWriter (name, fd) =
    3.55 +          Posix.IO.mkWriter {
    3.56 +	      appendMode = false,
    3.57 +              initBlkMode = true,
    3.58 +              name = name,  
    3.59 +              chunkSize=4096,
    3.60 +              fd = fd
    3.61 +            };
    3.62 +
    3.63 +fun openOutFD (name, fd) =
    3.64 +	  TextIO.mkOutstream (
    3.65 +	    TextIO.StreamIO.mkOutstream (
    3.66 +	      fdWriter (name, fd), IO.BLOCK_BUF));
    3.67 +
    3.68 +fun openInFD (name, fd) =
    3.69 +	  TextIO.mkInstream (
    3.70 +	    TextIO.StreamIO.mkInstream (
    3.71 +	      fdReader (name, fd), ""));
    3.72 +
    3.73 +
    3.74 +
    3.75 +
    3.76 +
    3.77 +(*****************************************)
    3.78 +(*  The result of calling createWatcher  *)
    3.79 +(*****************************************)
    3.80 +
    3.81 +datatype proc = PROC of {
    3.82 +        pid : Posix.Process.pid,
    3.83 +        instr : TextIO.instream,
    3.84 +        outstr : TextIO.outstream
    3.85 +      };
    3.86 +
    3.87 +
    3.88 +
    3.89 +(*****************************************)
    3.90 +(*  The result of calling executeToList  *)
    3.91 +(*****************************************)
    3.92 +
    3.93 +datatype cmdproc = CMDPROC of {
    3.94 +        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
    3.95 +        cmd:  string,              (* The file containing the goal for res prover to prove *)     
    3.96 +        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
    3.97 +        goalstring: string,         (* string representation of subgoal*) 
    3.98 +        pid : Posix.Process.pid,
    3.99 +        instr : TextIO.instream,   (*  Input stream to child process *)
   3.100 +        outstr : TextIO.outstream  (*  Output stream from child process *)
   3.101 +      };
   3.102 +
   3.103 +
   3.104 +
   3.105 +fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   3.106 +
   3.107 +fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr)));
   3.108 +
   3.109 +fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
   3.110 +
   3.111 +fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
   3.112 +
   3.113 +fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr))));
   3.114 +
   3.115 +fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (pid);
   3.116 +
   3.117 +fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (prover);
   3.118 +
   3.119 +fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (thmstring);
   3.120 +
   3.121 +fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr})  = (goalstring);
   3.122 +(***************************************************************************)
   3.123 +(*  Takes a command - e.g. 'vampire', a list of arguments for the command, *)
   3.124 +(*  and a list of currently running processes.  Creates a new process for  *)
   3.125 +(*  cmd and argv and adds it to procList                                   *)
   3.126 +(***************************************************************************)
   3.127 +
   3.128 +
   3.129 +
   3.130 +
   3.131 +fun mySshExecuteToList (cmd, argv, procList) = let
   3.132 +          val p1 = Posix.IO.pipe ()
   3.133 +          val p2 = Posix.IO.pipe ()
   3.134 +          val prover = hd argv
   3.135 +          val thmstring = hd(tl argv)
   3.136 +          val goalstring = hd(tl(tl argv))
   3.137 +          val argv = tl (tl argv)
   3.138 +          
   3.139 +          (* Turn the arguments into a single string.  Perhaps we should quote the
   3.140 +                   arguments.  *)
   3.141 +                fun convArgs [] = []
   3.142 +                  | convArgs [s] = [s]
   3.143 +                  | convArgs (hd::tl) = hd :: " " :: convArgs tl
   3.144 +                val cmd_args = concat(convArgs(cmd :: argv))
   3.145 +
   3.146 +	  fun closep () = (
   3.147 +                Posix.IO.close (#outfd p1); 
   3.148 +                Posix.IO.close (#infd p1);
   3.149 +                Posix.IO.close (#outfd p2); 
   3.150 +                Posix.IO.close (#infd p2)
   3.151 +              )
   3.152 +          fun startChild () =(case  Posix.Process.fork()
   3.153 +		 of SOME pid =>  pid           (* parent *)
   3.154 +                  | NONE => let                 
   3.155 +		      val oldchildin = #infd p1
   3.156 +		      val newchildin = Posix.FileSys.wordToFD 0w0
   3.157 +		      val oldchildout = #outfd p2
   3.158 +		      val newchildout = Posix.FileSys.wordToFD 0w1
   3.159 +                      (*val args = (["shep"]@([cmd]@argv))
   3.160 +                      val newcmd = "/usr/bin/ssh"*)
   3.161 +                      
   3.162 +                      in
   3.163 +			Posix.IO.close (#outfd p1);
   3.164 +			Posix.IO.close (#infd p2);
   3.165 +			Posix.IO.dup2{old = oldchildin, new = newchildin};
   3.166 +                        Posix.IO.close oldchildin;
   3.167 +			Posix.IO.dup2{old = oldchildout, new = newchildout};
   3.168 +                        Posix.IO.close oldchildout;
   3.169 +                       (* Run the command. *)
   3.170 +                       (* Run this as a shell command.  The command and arguments have
   3.171 +                          to be a single argument. *)
   3.172 +                       Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args])
   3.173 +			(*Posix.Process.exec(newcmd, args)*)
   3.174 +		      end
   3.175 +		(* end case *))
   3.176 +          val _ = TextIO.flushOut TextIO.stdOut
   3.177 +          val pid = (startChild ()) handle ex => (closep(); raise ex)
   3.178 +	  val instr = openInFD ("_exec_in", #infd p2)
   3.179 +          val outstr = openOutFD ("_exec_out", #outfd p1)
   3.180 +          val cmd = hd (rev argv)
   3.181 +          in
   3.182 +              (* close the child-side fds *)
   3.183 +            Posix.IO.close (#outfd p2);
   3.184 +            Posix.IO.close (#infd p1);
   3.185 +              (* set the fds close on exec *)
   3.186 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.187 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.188 +            (((CMDPROC{
   3.189 +              prover = prover,
   3.190 +              cmd = cmd,
   3.191 +              thmstring = thmstring,
   3.192 +              goalstring = goalstring,
   3.193 +              pid = pid,
   3.194 +              instr = instr,
   3.195 +              outstr = outstr
   3.196 +            })::procList))
   3.197 +          end;
   3.198 +
   3.199 +
   3.200 +fun myexecuteInEnv (cmd, argv, env) = let
   3.201 +          val p1 = Posix.IO.pipe ()
   3.202 +          val p2 = Posix.IO.pipe ()
   3.203 +          fun closep () = (
   3.204 +                Posix.IO.close (#outfd p1); 
   3.205 +                Posix.IO.close (#infd p1);
   3.206 +                Posix.IO.close (#outfd p2); 
   3.207 +                Posix.IO.close (#infd p2)
   3.208 +              )
   3.209 +          fun startChild () =(case  Posix.Process.fork()
   3.210 +                 of SOME pid =>  pid           (* parent *)
   3.211 +                  | NONE => let
   3.212 +                      val oldchildin = #infd p1
   3.213 +                      val newchildin = Posix.FileSys.wordToFD 0w0
   3.214 +                      val oldchildout = #outfd p2
   3.215 +                      val newchildout = Posix.FileSys.wordToFD 0w1
   3.216 +                      in
   3.217 +                        Posix.IO.close (#outfd p1);
   3.218 +                        Posix.IO.close (#infd p2);
   3.219 +                        Posix.IO.dup2{old = oldchildin, new = newchildin};
   3.220 +                        Posix.IO.close oldchildin;
   3.221 +                        Posix.IO.dup2{old = oldchildout, new = newchildout};
   3.222 +                        Posix.IO.close oldchildout;
   3.223 +                        Posix.Process.exece(cmd, argv, env)
   3.224 +                      end
   3.225 +                (* end case *))
   3.226 +          val _ = TextIO.flushOut TextIO.stdOut
   3.227 +          val pid = (startChild ()) handle ex => (closep(); raise ex)
   3.228 +          val instr = openInFD ("_exec_in", #infd p2)
   3.229 +          val outstr = openOutFD ("_exec_out", #outfd p1)
   3.230 +          in
   3.231 +              (* close the child-side fds *)
   3.232 +            Posix.IO.close (#outfd p2);
   3.233 +            Posix.IO.close (#infd p1);
   3.234 +              (* set the fds close on exec *)
   3.235 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.236 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.237 +            PROC{pid = pid,
   3.238 +              instr = instr,
   3.239 +              outstr = outstr
   3.240 +            }
   3.241 +          end;
   3.242 +
   3.243 +
   3.244 +
   3.245 +
   3.246 +fun myexecuteToList (cmd, argv, procList) = let
   3.247 +          val p1 = Posix.IO.pipe ()
   3.248 +          val p2 = Posix.IO.pipe ()
   3.249 +          val prover = hd argv
   3.250 +          val thmstring = hd(tl argv)
   3.251 +          val goalstring = hd(tl(tl argv))
   3.252 +          val argv = tl (tl (tl(argv)))
   3.253 +          
   3.254 +	  fun closep () = (
   3.255 +                Posix.IO.close (#outfd p1); 
   3.256 +                Posix.IO.close (#infd p1);
   3.257 +                Posix.IO.close (#outfd p2); 
   3.258 +                Posix.IO.close (#infd p2)
   3.259 +              )
   3.260 +          fun startChild () =(case  Posix.Process.fork()
   3.261 +		 of SOME pid =>  pid           (* parent *)
   3.262 +                  | NONE => let
   3.263 +		      val oldchildin = #infd p1
   3.264 +		      val newchildin = Posix.FileSys.wordToFD 0w0
   3.265 +		      val oldchildout = #outfd p2
   3.266 +		      val newchildout = Posix.FileSys.wordToFD 0w1
   3.267 +                      in
   3.268 +			Posix.IO.close (#outfd p1);
   3.269 +			Posix.IO.close (#infd p2);
   3.270 +			Posix.IO.dup2{old = oldchildin, new = newchildin};
   3.271 +                        Posix.IO.close oldchildin;
   3.272 +			Posix.IO.dup2{old = oldchildout, new = newchildout};
   3.273 +                        Posix.IO.close oldchildout;
   3.274 +			Posix.Process.exec(cmd, argv)
   3.275 +		      end
   3.276 +		(* end case *))
   3.277 +          val _ = TextIO.flushOut TextIO.stdOut
   3.278 +          val pid = (startChild ()) handle ex => (closep(); raise ex)
   3.279 +	  val instr = openInFD ("_exec_in", #infd p2)
   3.280 +          val outstr = openOutFD ("_exec_out", #outfd p1)
   3.281 +          val cmd = hd (rev argv)
   3.282 +          in
   3.283 +              (* close the child-side fds *)
   3.284 +            Posix.IO.close (#outfd p2);
   3.285 +            Posix.IO.close (#infd p1);
   3.286 +              (* set the fds close on exec *)
   3.287 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.288 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.289 +            (((CMDPROC{
   3.290 +              prover = prover,
   3.291 +              cmd = cmd,
   3.292 +              thmstring = thmstring,
   3.293 +              goalstring = goalstring,
   3.294 +              pid = pid,
   3.295 +              instr = instr,
   3.296 +              outstr = outstr
   3.297 +            })::procList))
   3.298 +          end;
   3.299 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP/recon_gandalf_base.ML	Thu Mar 31 19:29:26 2005 +0200
     4.3 @@ -0,0 +1,38 @@
     4.4 +(* Auxiliary functions *)
     4.5 +
     4.6 +exception Assertion of string;
     4.7 +
     4.8 +val DEBUG = ref true;
     4.9 +fun TRACE s = if !DEBUG then print s else ();
    4.10 +
    4.11 +fun id x = x;
    4.12 +fun K x y = x;
    4.13 +
    4.14 +exception Noassoc;
    4.15 +fun assoc a [] = raise Noassoc
    4.16 +  | assoc a ((x, y)::t) = if a = x then y else assoc a t;
    4.17 +fun assoc_exists a [] = false
    4.18 +  | assoc_exists a ((x, y)::t) = if a = x then true else assoc_exists a t;
    4.19 +fun assoc_update (a, b) [] = raise Noassoc
    4.20 +  | assoc_update (a, b) ((x, y)::t)
    4.21 +    = if a = x then (a, b)::t else (x, y)::(assoc_update (a, b) t)
    4.22 +fun assoc_inv a [] = raise Noassoc
    4.23 +  | assoc_inv a ((x, y)::t) = if a = y then x else assoc a t;
    4.24 +fun assoc_inv_exists a [] = false
    4.25 +  | assoc_inv_exists a ((x, y)::t) = if a = y then true else assoc_inv_exists a t;
    4.26 +
    4.27 +fun is_mem x [] = false
    4.28 +  | is_mem x (h::t) = (x = h) orelse is_mem x t;
    4.29 +fun elt 0 (h::t) = h
    4.30 +  | elt n (h::t) = elt (n - 1) t
    4.31 +  | elt n l = raise (Assertion "elt: out of range");
    4.32 +fun remove_elt _ [] = raise (Assertion "remove_elt: out of range")
    4.33 +  | remove_elt 0 (h::t) = t
    4.34 +  | remove_elt n (h::t) = h::(remove_elt (n - 1) t);
    4.35 +fun elt_num x [] = raise (Assertion "elt_num: not in list")
    4.36 +  | elt_num x (h::t) = if h = x then 0 else 1 + elt_num x t;
    4.37 +fun set_add x l = if is_mem x l then l else x::l;
    4.38 +
    4.39 +fun iter f a [] = a
    4.40 +  | iter f a (h::t) = f h (iter f a t);
    4.41 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Thu Mar 31 19:29:26 2005 +0200
     5.3 @@ -0,0 +1,492 @@
     5.4 +
     5.5 +
     5.6 +(*----------------------------------------------*)
     5.7 +(* Reorder clauses for use in binary resolution *)
     5.8 +(*----------------------------------------------*)
     5.9 +fun take n [] = []
    5.10 +|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
    5.11 +
    5.12 +fun drop n [] = []
    5.13 +|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    5.14 +
    5.15 +fun remove n [] = []
    5.16 +|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    5.17 +
    5.18 +fun remove_nth n [] = []
    5.19 +|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
    5.20 +
    5.21 +fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    5.22 +
    5.23 +
    5.24 + fun literals (Const("Trueprop",_) $ P) = literals P
    5.25 +   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    5.26 +   | literals (Const("Not",_) $ P) = [(false,P)]
    5.27 +   | literals P = [(true,P)];
    5.28 +
    5.29 + (*number of literals in a term*)
    5.30 + val nliterals = length o literals; 
    5.31 +     
    5.32 +exception Not_in_list;  
    5.33 +
    5.34 +
    5.35 +
    5.36 +
    5.37 +   (* get the literals from a disjunctive clause *)
    5.38 +
    5.39 +(*fun get_disj_literals t = if is_disj t then
    5.40 +			           let 
    5.41 +                                      val {disj1, disj2} = dest_disj t  
    5.42 +                                   in 
    5.43 +                                      disj1::(get_disj_literals disj2)
    5.44 +                                   end
    5.45 +                                else
    5.46 +                                    ([t])
    5.47 +   
    5.48 +*)
    5.49 +             
    5.50 +(*
    5.51 +(* gives horn clause with kth disj as concl (starting at 1) *)
    5.52 +fun rots (0,th) =  (Meson.make_horn Meson.crules th)
    5.53 +         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
    5.54 +
    5.55 +
    5.56 +                
    5.57 +Goal " (~~P) == P";
    5.58 +by Auto_tac;
    5.59 +qed "notnotEq";
    5.60 +
    5.61 +Goal "A | A ==> A";
    5.62 +by Auto_tac;
    5.63 +qed "rem_dup_disj";
    5.64 +
    5.65 +
    5.66 +
    5.67 +
    5.68 +(* New Meson code  Versions of make_neg_rule and make_pos_rule that don't insert new *)
    5.69 +(* assumptions, for ordinary resolution. *)
    5.70 +
    5.71 +
    5.72 +
    5.73 +
    5.74 + val not_conjD = thm "meson_not_conjD";
    5.75 + val not_disjD = thm "meson_not_disjD";
    5.76 + val not_notD = thm "meson_not_notD";
    5.77 + val not_allD = thm "meson_not_allD";
    5.78 + val not_exD = thm "meson_not_exD";
    5.79 + val imp_to_disjD = thm "meson_imp_to_disjD";
    5.80 + val not_impD = thm "meson_not_impD";
    5.81 + val iff_to_disjD = thm "meson_iff_to_disjD";
    5.82 + val not_iffD = thm "meson_not_iffD";
    5.83 + val conj_exD1 = thm "meson_conj_exD1";
    5.84 + val conj_exD2 = thm "meson_conj_exD2";
    5.85 + val disj_exD = thm "meson_disj_exD";
    5.86 + val disj_exD1 = thm "meson_disj_exD1";
    5.87 + val disj_exD2 = thm "meson_disj_exD2";
    5.88 + val disj_assoc = thm "meson_disj_assoc";
    5.89 + val disj_comm = thm "meson_disj_comm";
    5.90 + val disj_FalseD1 = thm "meson_disj_FalseD1";
    5.91 + val disj_FalseD2 = thm "meson_disj_FalseD2";
    5.92 +
    5.93 +
    5.94 + fun literals (Const("Trueprop",_) $ P) = literals P
    5.95 +   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    5.96 +   | literals (Const("Not",_) $ P) = [(false,P)]
    5.97 +   | literals P = [(true,P)];
    5.98 +
    5.99 + (*number of literals in a term*)
   5.100 + val nliterals = length o literals; 
   5.101 +     
   5.102 +exception Not_in_list;  
   5.103 +
   5.104 +
   5.105 +(*Permute a rule's premises to move the i-th premise to the last position.*)
   5.106 +fun make_last i th =
   5.107 +  let val n = nprems_of th 
   5.108 +  in  if 1 <= i andalso i <= n 
   5.109 +      then Thm.permute_prems (i-1) 1 th
   5.110 +      else raise THM("make_last", i, [th])
   5.111 +  end;
   5.112 +
   5.113 +(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   5.114 +  double-negations.*)
   5.115 +val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   5.116 +
   5.117 +(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   5.118 +fun select_literal i cl = negate_head (make_last i cl);
   5.119 +
   5.120 +
   5.121 +(* get a meta-clause for resolution with correct order of literals *)
   5.122 +fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
   5.123 +                              val contra =  if lits = 1 
   5.124 +                                                 then
   5.125 +                                                     th
   5.126 +                                                 else
   5.127 +                                                     rots (n,th)   
   5.128 +                          in 
   5.129 +                               if lits = 1 
   5.130 +                               then
   5.131 +                                            
   5.132 +                                  contra
   5.133 +                               else
   5.134 +                                  rotate_prems (lits - n) contra
   5.135 +                          end
   5.136 +
   5.137 +
   5.138 +
   5.139 +
   5.140 +
   5.141 +
   5.142 +
   5.143 +fun zip xs [] = []
   5.144 +|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
   5.145 +
   5.146 +
   5.147 +fun unzip [] = ([],[])
   5.148 +    | unzip((x,y)::pairs) =
   5.149 +	  let val (xs,ys) = unzip pairs
   5.150 +	  in  (x::xs, y::ys)  end;
   5.151 +
   5.152 +fun numlist 0 = []
   5.153 +|   numlist n = (numlist (n - 1))@[n]
   5.154 +
   5.155 +
   5.156 +fun is_abs t = can dest_abs t;
   5.157 +fun is_comb t = can dest_comb t;
   5.158 +
   5.159 +fun iscomb a = if is_Free a then
   5.160 +			false
   5.161 +	      else if is_Var a then
   5.162 +			false
   5.163 +		else if is_conj a then
   5.164 +			false
   5.165 +		else if is_disj a then
   5.166 +			false
   5.167 +		else if is_forall a then
   5.168 +			false
   5.169 +		else if is_exists a then
   5.170 +			false
   5.171 +		else
   5.172 +			true;
   5.173 +
   5.174 +
   5.175 +
   5.176 +
   5.177 +fun last(x::xs) = if xs=[] then x else last xs
   5.178 +fun butlast []= []
   5.179 +|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   5.180 +
   5.181 +
   5.182 +fun minus a b = b - a;
   5.183 +
   5.184 +
   5.185 +
   5.186 +
   5.187 +(* gives meta clause with kth disj as concl (starting at 1) *)
   5.188 +(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules  th)
   5.189 +         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
   5.190 +
   5.191 +
   5.192 +(* get a meta-clause for resolution with correct order of literals *)
   5.193 +fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
   5.194 +                                   val contra =  if lits = 1 
   5.195 +                                                 then
   5.196 +                                                     th
   5.197 +                                                 else
   5.198 +                                                     rots (n,th)   
   5.199 +                                in 
   5.200 +                                   if lits = 1 
   5.201 +                                   then
   5.202 +                                            
   5.203 +                                     contra
   5.204 +                                   else
   5.205 +                                     rotate_prems (lits - n) contra
   5.206 +                               end
   5.207 +*)
   5.208 +
   5.209 +
   5.210 +
   5.211 +
   5.212 +fun zip xs [] = []
   5.213 +|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
   5.214 +
   5.215 +
   5.216 +fun unzip [] = ([],[])
   5.217 +    | unzip((x,y)::pairs) =
   5.218 +	  let val (xs,ys) = unzip pairs
   5.219 +	  in  (x::xs, y::ys)  end;
   5.220 +
   5.221 +fun numlist 0 = []
   5.222 +|   numlist n = (numlist (n - 1))@[n]
   5.223 +
   5.224 +
   5.225 +fun is_abs t = can dest_abs t;
   5.226 +fun is_comb t = can dest_comb t;
   5.227 +
   5.228 +fun iscomb a = if is_Free a then
   5.229 +			false
   5.230 +	      else if is_Var a then
   5.231 +			false
   5.232 +		else if is_conj a then
   5.233 +			false
   5.234 +		else if is_disj a then
   5.235 +			false
   5.236 +		else if is_forall a then
   5.237 +			false
   5.238 +		else if is_exists a then
   5.239 +			false
   5.240 +		else
   5.241 +			true;
   5.242 +
   5.243 +
   5.244 +
   5.245 +
   5.246 +fun last(x::xs) = if xs=[] then x else last xs
   5.247 +fun butlast []= []
   5.248 +|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   5.249 +
   5.250 +
   5.251 +fun minus a b = b - a;
   5.252 +
   5.253 +
   5.254 +(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
   5.255 +
   5.256 +fun assoc3 a [] = raise Noassoc
   5.257 +  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
   5.258 +
   5.259 +
   5.260 +fun third (a,b,c) = c;
   5.261 +
   5.262 +
   5.263 + fun takeUntil ch [] res  = (res, [])
   5.264 + |   takeUntil ch (x::xs) res = if   x = ch 
   5.265 +                                then
   5.266 +                                     (res, xs)
   5.267 +                                else
   5.268 +                                     takeUntil ch xs (res@[x])
   5.269 +fun contains_eq str = inlist "=" str 
   5.270 +
   5.271 +fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
   5.272 +                     in
   5.273 +                        if ((last uptoeq) = "~")
   5.274 +                        then 
   5.275 +                            false
   5.276 +                        else
   5.277 +                            true
   5.278 +                     end
   5.279 +                   
   5.280 +
   5.281 +
   5.282 +
   5.283 +fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
   5.284 +                       then 
   5.285 +                           let val (left, right) = takeUntil "=" str []
   5.286 +                           in
   5.287 +                               ((butlast left), (drop 1 right))
   5.288 +                           end
   5.289 +                       else                  (* is an inequality *)
   5.290 +                           let val (left, right) = takeUntil "~" str []
   5.291 +                           in 
   5.292 +                              ((butlast left), (drop 2 right))
   5.293 +                           end
   5.294 +                
   5.295 +
   5.296 +
   5.297 +fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
   5.298 +                           val (x_lhs, x_rhs) = get_eq_strs x
   5.299 +
   5.300 +                       in
   5.301 +                           (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
   5.302 +                       end
   5.303 +
   5.304 +fun equal_pair (a,b) = equal a b
   5.305 +
   5.306 +fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
   5.307 +
   5.308 +fun var_equiv vars (a,b)  = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
   5.309 +
   5.310 +fun all_true [] = false
   5.311 +|   all_true xs = let val falselist = List.filter (equal false ) xs 
   5.312 +                  in
   5.313 +                      falselist = []
   5.314 +                  end
   5.315 +
   5.316 +
   5.317 +
   5.318 +fun var_pos_eq vars x y = let val xs = explode x
   5.319 +                              val ys = explode y
   5.320 +                          in
   5.321 +                              if not_equal (length xs) (length ys)
   5.322 +                              then 
   5.323 +                                  false
   5.324 +                              else
   5.325 +                                  let val xsys = zip xs ys
   5.326 +                                      val are_var_pairs = map (var_equiv vars) xsys
   5.327 +                                  in
   5.328 +                                      all_true are_var_pairs 
   5.329 +                                  end
   5.330 +                          end
   5.331 +
   5.332 +
   5.333 +
   5.334 +
   5.335 +fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
   5.336 +    |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
   5.337 +                                 let val y = explode x 
   5.338 +                                     val b = explode a
   5.339 +                                 in
   5.340 +                                    if  b = y
   5.341 +                                    then 
   5.342 +                                         (pos_num, symlist, nsymlist)
   5.343 +                                    else 
   5.344 +                                         if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   5.345 +                                         then 
   5.346 +                                             (pos_num, symlist, nsymlist)
   5.347 +                                         else 
   5.348 +                                             if (contains_eq b) andalso (contains_eq y)
   5.349 +                                             then 
   5.350 +                                                 if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   5.351 +                                                 then 
   5.352 +                                                     (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   5.353 +                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   5.354 +                                                      then 
   5.355 +                                                          (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   5.356 +                                                      else 
   5.357 +                                                           raise Not_in_list
   5.358 +                                             else 
   5.359 +                                                  raise Not_in_list
   5.360 +                                              
   5.361 +                                 end   
   5.362 +                                 
   5.363 +    | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
   5.364 +                                 let val y = explode x 
   5.365 +                                     val b = explode a
   5.366 +                                 in
   5.367 +                                    if  b = y
   5.368 +                                    then 
   5.369 +                                         (pos_num, symlist, nsymlist)
   5.370 +                                    
   5.371 +                                    else
   5.372 +                                          if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   5.373 +                                          then 
   5.374 +                                             (pos_num, symlist, nsymlist)
   5.375 +                                          else 
   5.376 +                                              if (contains_eq b) andalso (contains_eq y)
   5.377 +                                              then 
   5.378 +                                                  if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   5.379 +                                                  then 
   5.380 +                                                      (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   5.381 +                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   5.382 +                                                      then 
   5.383 +                                                           (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   5.384 +                                                      else 
   5.385 +                                                           pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   5.386 +                                              else 
   5.387 +                                                    pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   5.388 +                                              
   5.389 +                                 end   
   5.390 +
   5.391 +
   5.392 +
   5.393 +
   5.394 +
   5.395 +
   5.396 +
   5.397 +                                (* in
   5.398 +                                    if  b = y
   5.399 +                                    then 
   5.400 +                                         (pos_num, symlist, nsymlist)
   5.401 +                                    else if (contains_eq b) andalso (contains_eq y)
   5.402 +                                         then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
   5.403 +                                              then if (switch_equal b y )              (* if they're equal under sym *)
   5.404 +                                                   then 
   5.405 +                                                       (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
   5.406 +                                                   else 
   5.407 +                                                         pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   5.408 +                                              else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
   5.409 +                                                   then if (switch_equal b y )  (* if they're equal under not_sym *)
   5.410 +                                                        then 
   5.411 +                                                            (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   5.412 +                                                        else 
   5.413 +                                                                 pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   5.414 +                                                   else
   5.415 +                                                          pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   5.416 +                                               else  
   5.417 +                                                       pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   5.418 +                                          else 
   5.419 +                                                  pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   5.420 +                                 end   
   5.421 +
   5.422 +                                *)
   5.423 +
   5.424 +
   5.425 +
   5.426 +
   5.427 +
   5.428 +
   5.429 +
   5.430 +
   5.431 +
   5.432 +
   5.433 +(* checkorder Spass Isabelle [] *)
   5.434 +
   5.435 +fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
   5.436 +|   checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =  
   5.437 +         let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) 
   5.438 +         in
   5.439 +             checkorder xs  strlist allvars ((numlist@[posnum]), symlist', not_symlist') 
   5.440 +         end
   5.441 +
   5.442 +fun is_digit ch =
   5.443 +    ( ch >=  "0" andalso ch <=  "9")
   5.444 +
   5.445 +
   5.446 +fun is_alpha ch =
   5.447 +    (ch >=  "A" andalso  ch <=  "Z") orelse
   5.448 +    (ch >=  "a" andalso ch <=  "z")
   5.449 +
   5.450 +
   5.451 +fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
   5.452 +
   5.453 +fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
   5.454 +                       val exp_term = explode termstr
   5.455 +                   in
   5.456 +                       implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
   5.457 +                   end
   5.458 +
   5.459 +fun get_meta_lits thm = map lit_string (prems_of thm)
   5.460 +
   5.461 +
   5.462 +
   5.463 +
   5.464 +fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
   5.465 +
   5.466 +fun lit_string_bracket  t = let val termstr = (Sign.string_of_term Mainsign ) t
   5.467 +                       val exp_term = explode termstr
   5.468 +                   in
   5.469 +                       implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
   5.470 +                   end
   5.471 +
   5.472 +fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
   5.473 +
   5.474 +
   5.475 +
   5.476 +      
   5.477 +fun apply_rule rule [] thm = thm
   5.478 +|   apply_rule rule  (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
   5.479 +                                  in
   5.480 +                                      apply_rule rule xs thm'
   5.481 +                                  end
   5.482 +
   5.483 +
   5.484 +
   5.485 +                    (* resulting thm, clause-strs in spass order, vars *)
   5.486 +
   5.487 +fun rearrange_clause thm res_strlist allvars = 
   5.488 +                          let val isa_strlist = get_meta_lits thm
   5.489 +                              val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
   5.490 +                              val symmed = apply_rule sym symlist thm
   5.491 +                              val not_symmed = apply_rule not_sym not_symlist symmed
   5.492 +                                           
   5.493 +                          in
   5.494 +                             ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
   5.495 +                          end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Mar 31 19:29:26 2005 +0200
     6.3 @@ -0,0 +1,482 @@
     6.4 +(*use "Translate_Proof";*)
     6.5 +(* Parsing functions *)
     6.6 +
     6.7 +(* Auxiliary functions *)
     6.8 +
     6.9 +exception ASSERTION of string;
    6.10 +
    6.11 +exception NOPARSE_WORD
    6.12 +exception NOPARSE_NUM
    6.13 +fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
    6.14 +
    6.15 +fun string2int s =
    6.16 +  let
    6.17 +    val io = Int.fromString s
    6.18 +  in
    6.19 +    case io of
    6.20 +      (SOME i) => i
    6.21 +      | _ => raise ASSERTION "string -> int failed"
    6.22 +  end
    6.23 +
    6.24 +(* Parser combinators *)
    6.25 +
    6.26 +exception Noparse;
    6.27 +exception SPASSError of string;
    6.28 +
    6.29 +fun ++ (parser1, parser2) input =
    6.30 +      let
    6.31 +        val (result1, rest1) = parser1 input
    6.32 +        val (result2, rest2) = parser2 rest1
    6.33 +      in
    6.34 +        ((result1, result2), rest2)
    6.35 +      end;
    6.36 +
    6.37 +fun many parser input =
    6.38 +      let   (* Tree * token list*)
    6.39 +        val (result, next) = parser input
    6.40 +        val (results, rest) = many parser next
    6.41 +      in
    6.42 +        ((result::results), rest)
    6.43 +      end
    6.44 +      handle Noparse => ([], input)
    6.45 +|            NOPARSE_WORD => ([], input)
    6.46 +|            NOPARSE_NUM  => ([], input);
    6.47 +
    6.48 +
    6.49 +
    6.50 +fun >> (parser, treatment) input =
    6.51 +      let
    6.52 +        val (result, rest) = parser input
    6.53 +      in
    6.54 +        (treatment result, rest)
    6.55 +      end;
    6.56 +
    6.57 +fun || (parser1, parser2) input = parser1 input
    6.58 +handle Noparse => parser2 input;
    6.59 +
    6.60 +infixr 8 ++; infixr 7 >>; infixr 6 ||;
    6.61 +
    6.62 +fun some p [] = raise Noparse
    6.63 +  | some p (h::t) = if p h then (h, t) else raise Noparse;
    6.64 +
    6.65 +fun a tok = some (fn item => item = tok);
    6.66 +
    6.67 +fun finished input = if input = [] then (0, input) else raise Noparse;
    6.68 +
    6.69 +
    6.70 +
    6.71 +
    6.72 +
    6.73 +  (* Parsing the output from gandalf *)
    6.74 +datatype token = Word of string
    6.75 +               | Number of int
    6.76 +               | Other of string
    6.77 +
    6.78 +
    6.79 +      exception NOCUT
    6.80 +      fun is_prefix [] l = true
    6.81 +        | is_prefix (h::t) [] = false
    6.82 +        | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
    6.83 +      fun remove_prefix [] l = l
    6.84 +        | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
    6.85 +        | remove_prefix (h::t) (h'::t') = remove_prefix t t'
    6.86 +      fun ccut t [] = raise NOCUT
    6.87 +        | ccut t s =
    6.88 +            if is_prefix t s then ([], remove_prefix t s) else
    6.89 +              let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
    6.90 +      fun cut t s =
    6.91 +        let
    6.92 +          val t' = explode t
    6.93 +          val s' = explode s
    6.94 +          val (a, b) = ccut t' s'
    6.95 +        in
    6.96 +          (implode a, implode b)
    6.97 +        end
    6.98 +    
    6.99 +      fun cut_exists t s
   6.100 +          = let val (a, b) = cut t s in true end handle NOCUT => false
   6.101 +
   6.102 +      fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
   6.103 +      fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
   6.104 +    
   6.105 +
   6.106 +    fun kill_lines 0 = id
   6.107 +      | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
   6.108 +
   6.109 +    (*fun extract_proof s
   6.110 +      = if cut_exists "EMPTY CLAUSE DERIVED" s then
   6.111 +          (kill_lines 6
   6.112 +           o snd o cut_after "EMPTY CLAUSE DERIVED"
   6.113 +           o fst o cut_after "contradiction.\n") s
   6.114 +        else
   6.115 +          raise (GandalfError "Couldn't find a proof.")
   6.116 +*)
   6.117 +
   6.118 +val proofstring =
   6.119 +"0:00:00.00 for the reduction.\
   6.120 +\\
   6.121 +\Here is a proof with depth 3, length 7 :\
   6.122 +\1[0:Inp] ||  -> P(xa)*.\
   6.123 +\2[0:Inp] ||  -> Q(xb)*.\
   6.124 +\3[0:Inp] || R(U)* -> .\
   6.125 +\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
   6.126 +\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
   6.127 +\11[0:Res:2.0,9.0] || P(U)* -> .\
   6.128 +\12[0:Res:1.0,11.0] ||  -> .\
   6.129 +\Formulae used in the proof :\
   6.130 +\\
   6.131 +\--------------------------SPASS-STOP------------------------------"
   6.132 +
   6.133 +
   6.134 +fun extract_proof s
   6.135 +      = if cut_exists "Here is a proof with" s then
   6.136 +          (kill_lines 0
   6.137 +           o snd o cut_after ":"
   6.138 +           o snd o cut_after "Here is a proof with"
   6.139 +           o fst o cut_after " ||  -> .") s
   6.140 +        else
   6.141 +          raise SPASSError "Couldn't find a proof."
   6.142 +
   6.143 +
   6.144 +
   6.145 +fun several p = many (some p)
   6.146 +      fun collect (h, t) = h ^ (itlist (fn s1 => fn s2 => s1 ^ s2) t "")
   6.147 +  
   6.148 +      fun lower_letter s = ("a" <= s) andalso (s <= "z")
   6.149 +      fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   6.150 +      fun digit s = ("0" <= s) andalso (s <= "9")
   6.151 +      fun letter s = lower_letter s orelse upper_letter s
   6.152 +      fun alpha s = letter s orelse (s = "_")
   6.153 +      fun alphanum s = alpha s orelse digit s
   6.154 +      fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
   6.155 +      (* FIX this is stopping it picking up numbers *)
   6.156 +      val word = (some alpha ++ several alphanum) >> (Word o collect)
   6.157 +      val number =
   6.158 +            (some digit ++ several digit) >> (Number o string2int o collect)
   6.159 +      val other = some (K true) >> Other
   6.160 +      
   6.161 +      val token = (word || number || other) ++ several space >> fst
   6.162 +      val tokens = (several space ++ many token) >> snd
   6.163 +      val alltokens = (tokens ++ finished) >> fst
   6.164 +    
   6.165 +     (* val lex = fst ( alltokens ( (map str)  explode))*)
   6.166 +     fun lex s =  alltokens  (explode s)
   6.167 +
   6.168 +datatype Tree = Leaf of string
   6.169 +                | Branch of Tree * Tree
   6.170 +
   6.171 +
   6.172 +
   6.173 +   
   6.174 +      fun number ((Number n)::rest) = (n, rest)
   6.175 +        | number _ = raise NOPARSE_NUM
   6.176 +      fun word ((Word w)::rest) = (w, rest)
   6.177 +        | word _ = raise NOPARSE_WORD
   6.178 +
   6.179 +      fun other_char ( (Other p)::rest) = (p, rest)
   6.180 +      | other_char _ =raise NOPARSE_WORD
   6.181 +     
   6.182 +      val number_list =
   6.183 +        (number ++ many number)
   6.184 +        >> (fn (a, b) => (a::b))
   6.185 +     
   6.186 +      val term_num =
   6.187 +        (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
   6.188 +
   6.189 +      val axiom = (a (Word "Inp"))
   6.190 +            >> (fn (_) => Axiom)
   6.191 +      
   6.192 +      
   6.193 +      val binary = (a (Word "Res")) ++ (a (Other ":"))
   6.194 +                   ++ term_num ++ (a (Other ","))
   6.195 +                   ++ term_num
   6.196 +            >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
   6.197 +      
   6.198 +
   6.199 +
   6.200 +      val factor = (a (Word "Fac")) ++ (a (Other ":")) 
   6.201 +                    ++ term_num ++ (a (Other ",")) 
   6.202 +                    ++ term_num
   6.203 +            >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
   6.204 +     
   6.205 +      val para  = (a (Word "SPm")) ++ (a (Other ":"))
   6.206 +                   ++ term_num ++ (a (Other ","))
   6.207 +                   ++ term_num
   6.208 +            >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
   6.209 +      
   6.210 +      val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
   6.211 +                    ++ term_num ++ (a (Other ",")) 
   6.212 +                    ++ term_num
   6.213 +            >> (fn (_, (_, (c, (_, e)))) =>  Rewrite (c, e))
   6.214 +
   6.215 +
   6.216 +      val mrr = (a (Word "MRR")) ++ (a (Other ":"))
   6.217 +                   ++ term_num ++ (a (Other ","))
   6.218 +                   ++ term_num
   6.219 +            >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
   6.220 +
   6.221 +
   6.222 +      val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
   6.223 +                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   6.224 +     
   6.225 +(*
   6.226 +      val hyper = a (Word "hyper")
   6.227 +                  ++ many ((a (Other ",") ++ number) >> snd)
   6.228 +                  >> (Hyper o snd)
   6.229 +*)
   6.230 +     (* val method = axiom ||binary || factor || para || hyper*)
   6.231 +
   6.232 +      val method = axiom || binary || factor || para || rewrite || mrr || obv
   6.233 +      val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
   6.234 +            >> (fn (_, (_, a)) => Binary_s a)
   6.235 +      val factor_s = a (Word "factor_s")
   6.236 +            >> (fn _ => Factor_s ())
   6.237 +      val demod_s = a (Word "demod")
   6.238 +                    ++ (many ((a (Other ",") ++ term_num) >> snd))
   6.239 +            >> (fn (_, a) => Demod_s a)
   6.240 +
   6.241 +      val hyper_s = a (Word "hyper_s")
   6.242 +                    ++ many ((a (Other ",") ++ number) >> snd)
   6.243 +                    >> (Hyper_s o snd)
   6.244 +      val simp_method = binary_s || factor_s || demod_s || hyper_s
   6.245 +      val simp = a (Other ",") ++ simp_method >> snd
   6.246 +      val simps = many simp
   6.247 + 
   6.248 +
   6.249 +      val justification =
   6.250 +           a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
   6.251 +                 >> (fn (_,(_, (_,(b, _)))) => b)
   6.252 +
   6.253 +     
   6.254 +exception NOTERM
   6.255 +
   6.256 +
   6.257 +fun implode_with_space [] = implode []
   6.258 +|   implode_with_space [x] = implode [x]
   6.259 +|   implode_with_space (x::[y]) = x^" "^y
   6.260 +|   implode_with_space (x::xs) =  (x^" "^(implode_with_space xs))
   6.261 +
   6.262 +(* FIX - should change the stars and pluses to many rather than explicit patterns *)
   6.263 +
   6.264 +(* FIX - add the other things later *)
   6.265 +fun remove_typeinfo x  =  if (String.isPrefix "v_" x )
   6.266 +                            then 
   6.267 +                                 (String.substring (x,2, ((size x) - 2)))
   6.268 +                            else if (String.isPrefix "V_" x )
   6.269 +                                 then 
   6.270 +                                      (String.substring (x,2, ((size x) - 2)))
   6.271 +                                 else if (String.isPrefix "typ_" x )
   6.272 +                                      then 
   6.273 +                                          ""
   6.274 +                                      else if (String.isPrefix "Typ_" x )
   6.275 +                                           then 
   6.276 +                                                ""
   6.277 +                                           else  if (String.isPrefix "tconst_" x )
   6.278 +                                                 then 
   6.279 +                                                      ""
   6.280 +                                                 else  if (String.isPrefix "const_" x )
   6.281 +                                                       then 
   6.282 +                                                            (String.substring  (x,6, ((size x) - 6)))
   6.283 +                                                       else
   6.284 +                                                           x
   6.285 +                                               
   6.286 +
   6.287 +fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
   6.288 +                  ) input
   6.289 +
   6.290 +(* pterms are terms from the rhs of the -> in the spass proof.  *)
   6.291 +(* they should have a "~" in front of them so that they match with *)
   6.292 +(* positive terms in the meta-clause *)
   6.293 +(* nterm are terms from the lhs of the spass proof, and shouldn't *)
   6.294 +(* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)
   6.295 +
   6.296 +and  pterm input = (
   6.297 +           peqterm >> (fn (a) => a)
   6.298 +        
   6.299 +         || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
   6.300 +           >> (fn (a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   6.301 +         
   6.302 +        || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*") ++ a (Other "+")
   6.303 +           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   6.304 +        
   6.305 +        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   6.306 +           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   6.307 +        
   6.308 +	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   6.309 +           >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   6.310 +
   6.311 +        || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
   6.312 +           >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
   6.313 +
   6.314 +        || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
   6.315 +
   6.316 +and  nterm input =
   6.317 +    
   6.318 +       (  
   6.319 +           neqterm >> (fn (a) => a)
   6.320 +
   6.321 +        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   6.322 +           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   6.323 +
   6.324 +        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
   6.325 +           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   6.326 +        
   6.327 +        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   6.328 +           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   6.329 +        
   6.330 +	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   6.331 +           >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))
   6.332 +
   6.333 +        || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
   6.334 +           >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
   6.335 +
   6.336 +        || word >> (fn w =>  (remove_typeinfo w)) ) input 
   6.337 +
   6.338 +
   6.339 +and peqterm input =(
   6.340 + 
   6.341 +         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.342 +         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   6.343 +            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
   6.344 +
   6.345 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.346 +          ++ a (Other "*") ++ a (Other "+")
   6.347 +            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   6.348 +
   6.349 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.350 +         ++ a (Other "*") ++ a (Other "*")
   6.351 +            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   6.352 +
   6.353 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.354 +         ++ a (Other "*") 
   6.355 +            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
   6.356 +
   6.357 +
   6.358 +       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.359 +            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
   6.360 +
   6.361 +
   6.362 +
   6.363 +and neqterm input =(
   6.364 + 
   6.365 +         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.366 +         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   6.367 +            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
   6.368 +
   6.369 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.370 +          ++ a (Other "*") ++ a (Other "+")
   6.371 +            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   6.372 +
   6.373 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.374 +         ++ a (Other "*") ++ a (Other "*")
   6.375 +            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   6.376 +
   6.377 +      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.378 +         ++ a (Other "*") 
   6.379 +            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
   6.380 +
   6.381 +
   6.382 +       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   6.383 +            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
   6.384 +
   6.385 +
   6.386 +
   6.387 +and ptermlist input = (many  pterm
   6.388 +                      >> (fn (a) => (a))) input
   6.389 +
   6.390 +and ntermlist input = (many  nterm
   6.391 +                      >> (fn (a) => (a))) input
   6.392 +
   6.393 +(*and arglist input = (    nterm >> (fn (a) => (a))
   6.394 +                     ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
   6.395 +                      >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)
   6.396 +
   6.397 +and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
   6.398 +                      >> (fn (a, b) => (a^" "^(implode_with_space b))) 
   6.399 +                      ||    nterm >> (fn (a) => (a)))input
   6.400 +
   6.401 + val clause =  term
   6.402 +
   6.403 + val line = number ++ justification ++ a (Other "|") ++ 
   6.404 +            a (Other "|") ++ clause ++ a (Other ".")
   6.405 +          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))
   6.406 +    
   6.407 + val lines = many line
   6.408 + val alllines = (lines ++ finished) >> fst
   6.409 +    
   6.410 + val parse = fst o alllines
   6.411 + val s = proofstring;
   6.412 + 
   6.413 + 
   6.414 +
   6.415 +
   6.416 +fun dropUntilNot ch []   = ( [])
   6.417 + |   dropUntilNot ch (x::xs)  = if  not(x = ch )
   6.418 +                                then
   6.419 +                                     (x::xs)
   6.420 +                                else
   6.421 +                                     dropUntilNot ch xs
   6.422 +
   6.423 +
   6.424 +
   6.425 +
   6.426 +
   6.427 +fun remove_spaces str  []  = str
   6.428 +|   remove_spaces str (x::[]) = if x = " " 
   6.429 +                                then 
   6.430 +                                    str 
   6.431 +                                else 
   6.432 +                                    (str^x)
   6.433 +|   remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
   6.434 +                                    val (next) = dropUntilNot " " rest 
   6.435 +                                in 
   6.436 +                                    if next = []
   6.437 +                                    then 
   6.438 +                                         (str^(implode first)) 
   6.439 +                                    else remove_spaces  (str^(implode first)^" ") next 
   6.440 +                                end
   6.441 +
   6.442 +
   6.443 +fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
   6.444 +
   6.445 +
   6.446 +fun all_spaces xs = List.filter  (not_equal " " ) xs
   6.447 +
   6.448 +fun just_change_space []  = []
   6.449 +|   just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
   6.450 +                                                 in
   6.451 +                                                    if (all_spaces newstrs = [] ) (* all type_info *)                                                    then    
   6.452 +                                                       (clausenum, step, newstrs)::(just_change_space xs)
   6.453 +                                                    else 
   6.454 +                                                        (clausenum, step, newstrs)::(just_change_space xs) 
   6.455 +                                                 end
   6.456 +
   6.457 +
   6.458 +
   6.459 +
   6.460 +fun change_space []  = []
   6.461 +|   change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
   6.462 +                                                 in
   6.463 +                                                    if (all_spaces newstrs = [] ) (* all type_info *)
   6.464 +                                                    then    
   6.465 +                                                       (clausenum, step, T_info, newstrs)::(change_space xs)
   6.466 +                                                    else 
   6.467 +                                                        (clausenum, step, P_info, newstrs)::(change_space xs) 
   6.468 +                                                 end
   6.469 +
   6.470 +
   6.471 +
   6.472 +
   6.473 +
   6.474 +
   6.475 +(*
   6.476 +    fun gandalf_parse s =
   6.477 +      let
   6.478 +        val e = extract_proof;
   6.479 +        val t = fst(lex e)
   6.480 +        val r = parse t
   6.481 +      in
   6.482 +        r
   6.483 +      end
   6.484 +  
   6.485 +*)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML	Thu Mar 31 19:29:26 2005 +0200
     7.3 @@ -0,0 +1,470 @@
     7.4 +
     7.5 +open Goals;
     7.6 +open Unify;
     7.7 +open USyntax;
     7.8 +open Utils;
     7.9 +open Envir;
    7.10 +open Tfl;
    7.11 +open Rules;
    7.12 +
    7.13 +goal Main.thy "A -->A";
    7.14 +by Auto_tac;
    7.15 +qed "foo";
    7.16 +
    7.17 +
    7.18 +val Mainsign = #sign (rep_thm foo);
    7.19 +
    7.20 +
    7.21 +
    7.22 +(*val myhol = sign_of thy;*)
    7.23 +
    7.24 +val myenv = empty 0;
    7.25 +
    7.26 +
    7.27 +val gcounter = ref 0; 
    7.28 +      
    7.29 +exception NOMATES;
    7.30 +exception UNMATEABLE;
    7.31 +exception NOTSOME;
    7.32 +exception UNSPANNED;
    7.33 +
    7.34 +fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
    7.35 +
    7.36 +fun dest_neg(Const("Not",_) $ M) = M
    7.37 +  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
    7.38 +
    7.39 +fun is_abs t = can dest_abs t;
    7.40 +fun is_comb t = can dest_comb t;
    7.41 +
    7.42 +fun iscomb a = if is_Free a then
    7.43 +			false
    7.44 +	      else if is_Var a then
    7.45 +			false
    7.46 +		else if is_conj a then
    7.47 +			false
    7.48 +		else if is_disj a then
    7.49 +			false
    7.50 +		else if is_forall a then
    7.51 +			false
    7.52 +		else if is_exists a then
    7.53 +			false
    7.54 +		else
    7.55 +			true;
    7.56 +fun getstring (Var (v,T)) = fst v
    7.57 +   |getstring (Free (v,T))= v;
    7.58 +
    7.59 +
    7.60 +fun getindexstring ((a:string),(b:int))= a;  
    7.61 +
    7.62 +fun getstrings (a,b) = let val astring = getstring a
    7.63 +                           val bstring = getstring b in
    7.64 +                           (astring,bstring)
    7.65 +                       end;
    7.66 +
    7.67 +
    7.68 +fun alltrue [] = true
    7.69 +   |alltrue (true::xs) = true andalso (alltrue xs)
    7.70 +   |alltrue (false::xs) = false;
    7.71 +
    7.72 +fun allfalse [] = true
    7.73 +   |allfalse (false::xs) = true andalso (allfalse xs)
    7.74 +   |allfalse (true::xs) = false;
    7.75 +
    7.76 +fun not_empty [] = false 
    7.77 +    | not_empty _ = true;
    7.78 +
    7.79 +fun twoisvar (a,b) = is_Var b;
    7.80 +fun twoisfree (a,b) = is_Free b;
    7.81 +fun twoiscomb (a,b) = iscomb b;
    7.82 +
    7.83 +fun strequalfirst a (b,c) = (getstring a) = (getstring b);
    7.84 +
    7.85 +fun fstequal a b = a = fst b;
    7.86 +
    7.87 +fun takeout (i,[])  = []
    7.88 +   | takeout (i,(x::xs)) = if (i>0) then
    7.89 +                               (x::(takeout(i-1,xs)))
    7.90 +                           else
    7.91 +                               [];
    7.92 +		
    7.93 +
    7.94 +
    7.95 +(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
    7.96 +fun is_Abs (Abs _) = true
    7.97 +  | is_Abs _ = false;
    7.98 +fun is_Bound (Bound _) = true
    7.99 +  | is_Bound _ = false;
   7.100 +
   7.101 +
   7.102 +
   7.103 +
   7.104 +fun is_hol_tm t =
   7.105 +                if (is_Free t) then 
   7.106 +                        true 
   7.107 +                else if (is_Var t) then
   7.108 +                        true
   7.109 +                else if (is_Const t) then
   7.110 +                        true
   7.111 +                else if (is_Abs t) then
   7.112 +                        true
   7.113 +                else if (is_Bound t) then
   7.114 +                        true
   7.115 +                else 
   7.116 +                        let val (f, args) = strip_comb t in
   7.117 +                            if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then 
   7.118 +                                true            (* should be is_const *)
   7.119 +                            else 
   7.120 +                                false
   7.121 +                       end;
   7.122 +
   7.123 +fun is_hol_fm f =  if is_neg f then
   7.124 +                        let val newf = dest_neg f in
   7.125 +                            is_hol_fm newf
   7.126 +                        end
   7.127 +                    
   7.128 +               else if is_disj f then
   7.129 +                        let val {disj1,disj2} = dest_disj f in
   7.130 +                            (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
   7.131 +                        end 
   7.132 +               else if is_conj f then
   7.133 +                        let val {conj1,conj2} = dest_conj f in
   7.134 +                            (is_hol_fm conj1) andalso (is_hol_fm conj2)
   7.135 +                        end 
   7.136 +               else if (is_forall f) then
   7.137 +                        let val {Body, Bvar} = dest_forall f in
   7.138 +                            is_hol_fm Body
   7.139 +                        end
   7.140 +               else if (is_exists f) then
   7.141 +                        let val {Body, Bvar} = dest_exists f in
   7.142 +                            is_hol_fm Body
   7.143 +                        end
   7.144 +               else if (iscomb f) then
   7.145 +                        let val (P, args) = strip_comb f in
   7.146 +                            ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args))
   7.147 +                        end
   7.148 +                else
   7.149 +                        is_hol_tm f;                              (* should be is_const, nee
   7.150 +d to check args *)
   7.151 +               
   7.152 +
   7.153 +fun hol_literal t =  (is_hol_fm t) andalso ( not ((is_conj t) orelse (is_disj t) orelse (is_forall t) orelse (is_exists t)));
   7.154 +
   7.155 +
   7.156 +
   7.157 +
   7.158 +(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
   7.159 +fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in
   7.160 +			if (iscomb rand) then
   7.161 +				getcombvar rand
   7.162 +			else
   7.163 +				rand
   7.164 +		   end;
   7.165 +
   7.166 +
   7.167 +
   7.168 +fun free2var v = let val thing = dest_Free v 
   7.169 +                     val (name,vtype) = thing
   7.170 +                     val index = (name,0) in
   7.171 +                     Var (index,vtype)
   7.172 +                 end;
   7.173 +
   7.174 +fun var2free v = let val (index, tv) = dest_Var v 
   7.175 +                     val istr = fst index in
   7.176 +                     Free (istr,tv)
   7.177 +                 end;
   7.178 +
   7.179 +fun  inlist v [] = false
   7.180 +    | inlist v (first::rest) = if first = v then
   7.181 +				true
   7.182 +			     else inlist v rest;
   7.183 +
   7.184 +(*fun in_vars v [] = false
   7.185 +    | in_vars v ((a,b)::rest) = if v = a then
   7.186 +				  true
   7.187 +			       else if v = b then
   7.188 +				  true
   7.189 +			       else in_vars v rest;*)
   7.190 +
   7.191 +fun in_vars v [] = false
   7.192 +    | in_vars v (a::rest) = if (fst v) = a then
   7.193 +				  true
   7.194 +			      
   7.195 +			       else in_vars v rest;
   7.196 +
   7.197 +fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
   7.198 +					true
   7.199 +			    else if (a,b) = (d,c) then
   7.200 +					true
   7.201 +			    else false;
   7.202 +
   7.203 +
   7.204 +fun is_empty_seq thisseq =  case Seq.chop (1, thisseq) of
   7.205 +                             ([],_)   => true
   7.206 +                           |      _   => false
   7.207 +
   7.208 +fun getnewenv thisseq = 
   7.209 +			   let val seqlist = Seq.list_of thisseq
   7.210 +			   val envpair =hd seqlist in
   7.211 +			   fst envpair 
   7.212 +			end;
   7.213 +
   7.214 +fun getnewsubsts thisseq =  let val seqlist = Seq.list_of thisseq
   7.215 +			   val envpair =hd seqlist in
   7.216 +			   snd envpair 
   7.217 +			end;
   7.218 +
   7.219 +fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv
   7.220 +			   val envpair = hd seqlist
   7.221 +			   val env = fst envpair
   7.222 +			   val envlist = alist_of env in
   7.223 +			hd envlist
   7.224 +			end;
   7.225 +
   7.226 +
   7.227 +fun readenv thisenv = let val envlist = alist_of thisenv in
   7.228 +			
   7.229 +				hd envlist
   7.230 +			end;
   7.231 +
   7.232 +
   7.233 +
   7.234 +
   7.235 +
   7.236 +fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
   7.237 +
   7.238 +fun oneofthree (a,b,c) = a;
   7.239 +
   7.240 +fun twoofthree (a,b,c) = b;
   7.241 +
   7.242 +fun threeofthree (a,b,c) = c;
   7.243 +
   7.244 +val my_simps = map prover
   7.245 + [ "(x=x) = True",
   7.246 +    "(~ ~ P) = P",
   7.247 +   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
   7.248 +   
   7.249 +   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
   7.250 +   "((~P) = (~Q)) = (P=Q)" ];
   7.251 +
   7.252 +
   7.253 +(*val myss = HOL_basic_ss addsimps (my_simps@[not_all, not_ex, de_Morgan_conj, de_Morgan_disj, U_def, intersect_def, setEq_def, proposEq_def, hashset_def, subset_def]@ex_simps @ all_simps);
   7.254 +
   7.255 +*)
   7.256 +
   7.257 +(*--------------------------*)
   7.258 +(* NNF stuff from meson_tac *)
   7.259 +(*--------------------------*)
   7.260 +
   7.261 +
   7.262 +(*Prove theorems using fast_tac*)
   7.263 +fun prove_fun s = 
   7.264 +    prove_goal HOL.thy s
   7.265 +         (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
   7.266 +
   7.267 +(*------------------------------------------------------------------------*)
   7.268 +(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
   7.269 +(*------------------------------------------------------------------------*)
   7.270 +fun mygenvar ty thisenv =
   7.271 +  let val count = !gcounter
   7.272 +      val genstring = "GEN"^(string_of_int count)^"VAR" in
   7.273 +	    	gcounter := count + 1;
   7.274 +              	genvar genstring (thisenv,ty)
   7.275 +  end;  
   7.276 +
   7.277 +fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
   7.278 +			t
   7.279 +	 	
   7.280 +		else if is_forall t then
   7.281 +			let val {Body, Bvar} = dest_forall t 
   7.282 +                            val newvarenv = mygenvar(type_of Bvar) thisenv
   7.283 +                            val newvar = snd(newvarenv)
   7.284 +                            val newbod = subst_free [(Bvar,newvar)] Body
   7.285 +                            val newbod2 = renameBounds newbod thisenv in
   7.286 +                            mk_forall{Body = newbod2, Bvar = newvar}
   7.287 +                        end
   7.288 +		else if is_exists t then
   7.289 +                        let val {Body, Bvar} =dest_exists t 
   7.290 +			    val newvarenv = mygenvar(type_of Bvar) thisenv
   7.291 +                            val newvar = snd(newvarenv)
   7.292 +                            val newbod = subst_free [(Bvar,newvar)] Body
   7.293 +                            val newbod2 = renameBounds newbod thisenv in
   7.294 +                            mk_exists{Body = newbod2, Bvar = newvar}    
   7.295 +			end
   7.296 +		else if is_conj t then
   7.297 +			let val {conj1,conj2} = dest_conj t
   7.298 +			    val vpl = renameBounds conj1 thisenv
   7.299 +			    val vpr = renameBounds conj2 thisenv in
   7.300 +		            mk_conj {conj1 = vpl, conj2 = vpr}
   7.301 +			end
   7.302 +		else 
   7.303 +			let val {disj1, disj2} = dest_disj t 
   7.304 +			    val vpl = renameBounds disj1 thisenv
   7.305 +			    val  vpr = renameBounds disj2  thisenv in
   7.306 +			    mk_disj {disj1 = vpl,disj2= vpr}  
   7.307 +			end;
   7.308 +                	
   7.309 +
   7.310 +(*-----------------*)
   7.311 +(* from hologic.ml *)
   7.312 +(*-----------------*)
   7.313 +val boolT = Type ("bool", []);
   7.314 +
   7.315 +val Trueprop = Const ("Trueprop", boolT --> propT);
   7.316 +
   7.317 +fun mk_Trueprop P = Trueprop $ P;
   7.318 +
   7.319 +fun eq_const T = Const ("op =", [T, T] ---> boolT);
   7.320 +fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   7.321 +
   7.322 +fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   7.323 + | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   7.324 +
   7.325 +
   7.326 +(*-----------------------------------------------------------------------*)
   7.327 +(* Making a THM from a subgoal and other such things                     *)
   7.328 +(*-----------------------------------------------------------------------*)
   7.329 +
   7.330 +fun thmfromgoal goalnum = let val mygoal = getgoal goalnum
   7.331 +                              val  mycgoal = cterm_of Mainsign mygoal in
   7.332 +                              assume mycgoal
   7.333 +                          end;
   7.334 +
   7.335 +fun termfromgoal goalnum = let val mygoal = getgoal goalnum
   7.336 +                               val {Rand = myra, Rator = myrat} = dest_comb mygoal in
   7.337 +                               myra
   7.338 +                           end;
   7.339 +
   7.340 +fun thmfromterm t = let val propterm = mk_Trueprop t 
   7.341 +                        val mycterm = cterm_of Mainsign propterm in
   7.342 +                        assume mycterm
   7.343 +                    end;
   7.344 +
   7.345 +fun termfromthm t = let val conc = concl_of t 
   7.346 +                        val {Rand = myra, Rator = myrat} = dest_comb conc in
   7.347 +                        myra
   7.348 +                    end;
   7.349 +
   7.350 +fun goalfromterm t = let val pterm = mk_Trueprop t  
   7.351 +                         val ct = cterm_of Mainsign  pterm in
   7.352 +                         goalw_cterm [] ct
   7.353 +                     end;
   7.354 +
   7.355 +fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum
   7.356 +                               val {Rand = myra1, Rator = myrat1} = dest_comb mygoal 
   7.357 +                               val  {Rand = myra, Rator = myrat} = dest_comb myra1 in
   7.358 +                               myra
   7.359 +                           end;
   7.360 +
   7.361 +
   7.362 +fun mkvars (a,b:term) = let val thetype = type_of b 
   7.363 +                           val stringa =( fst a)
   7.364 +                            val newa = Free (stringa, thetype) in
   7.365 +                            (newa,b)
   7.366 +                        end;
   7.367 +
   7.368 +fun glue [] thestring = thestring
   7.369 +  |glue (""::[]) thestring = thestring 
   7.370 +  |glue (a::[]) thestring = thestring^" "^a 
   7.371 +  |glue (a::rest) thestring = let val newstring = thestring^" "^a in
   7.372 +                                 glue rest newstring
   7.373 +                             end;
   7.374 +
   7.375 +exception STRINGEXCEP;
   7.376 + 
   7.377 +fun getvstring (Var (v,T)) = fst v
   7.378 +   |getvstring (Free (v,T))= v;
   7.379 +
   7.380 +  
   7.381 +fun getindexstring ((a:string),(b:int))= a;  
   7.382 +
   7.383 +fun getstrings (a,b) = let val astring = getstring a
   7.384 +                           val bstring = getstring b in
   7.385 +                           (astring,bstring)
   7.386 +                       end;
   7.387 +(*
   7.388 +fun getvstrings (a,b) = let val astring = getvstring a
   7.389 +                           val bstring = getvstring b in
   7.390 +                           (astring,bstring)
   7.391 +                       end;
   7.392 +*)
   7.393 + 
   7.394 +
   7.395 +
   7.396 +(*------------------------------------------------------------------------*)
   7.397 +(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
   7.398 +(*------------------------------------------------------------------------*)
   7.399 +fun mygenvar ty thisenv =
   7.400 +  let val count = !gcounter
   7.401 +      val genstring = "GEN"^(string_of_int count)^"VAR" in
   7.402 +	    	gcounter := count + 1;
   7.403 +              	genvar genstring (thisenv,ty)
   7.404 +  end;  
   7.405 +
   7.406 +fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
   7.407 +			t
   7.408 +	 	
   7.409 +		else if is_forall t then
   7.410 +			let val {Body, Bvar} = dest_forall t 
   7.411 +                            val newvarenv = mygenvar(type_of Bvar) thisenv
   7.412 +                            val newvar = snd(newvarenv)
   7.413 +                            val newbod = subst_free [(Bvar,newvar)] Body
   7.414 +                            val newbod2 = renameBounds newbod thisenv in
   7.415 +                            mk_forall{Body = newbod2, Bvar = newvar}
   7.416 +                        end
   7.417 +		else if is_exists t then
   7.418 +                        let val {Body, Bvar} =dest_exists t 
   7.419 +			    val newvarenv = mygenvar(type_of Bvar) thisenv
   7.420 +                            val newvar = snd(newvarenv)
   7.421 +                            val newbod = subst_free [(Bvar,newvar)] Body
   7.422 +                            val newbod2 = renameBounds newbod thisenv in
   7.423 +                            mk_exists{Body = newbod2, Bvar = newvar}    
   7.424 +			end
   7.425 +		else if is_conj t then
   7.426 +			let val {conj1,conj2} = dest_conj t
   7.427 +			    val vpl = renameBounds conj1 thisenv
   7.428 +			    val vpr = renameBounds conj2 thisenv in
   7.429 +		            mk_conj {conj1 = vpl, conj2 = vpr}
   7.430 +			end
   7.431 +		else 
   7.432 +			let val {disj1, disj2} = dest_disj t 
   7.433 +			    val vpl = renameBounds disj1 thisenv
   7.434 +			    val  vpr = renameBounds disj2  thisenv in
   7.435 +			    mk_disj {disj1 = vpl,disj2= vpr}  
   7.436 +			end;
   7.437 +                	
   7.438 +
   7.439 +
   7.440 +exception VARFORM_PROBLEM;
   7.441 +		
   7.442 +fun varform t = if (hol_literal t) then
   7.443 +			t
   7.444 +	 	
   7.445 +		else if is_forall t then
   7.446 +			let val {Body, Bvar} = dest_forall t 
   7.447 +         (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *)
   7.448 +                         val newB = free2var Bvar
   7.449 +                         val newBody = subst_free[(Bvar, newB)] Body in
   7.450 +			    varform newBody
   7.451 +			end
   7.452 +		else if is_exists t then
   7.453 +        (* Shouldn't really be any exists in term due to Skolemisation*)
   7.454 +			let val {Body, Bvar} =dest_exists t in
   7.455 +			    varform Body
   7.456 +			end
   7.457 +		else if is_conj t then
   7.458 +			let val {conj1,conj2} = dest_conj t
   7.459 +			    val vpl = varform conj1 
   7.460 +			    val vpr = varform conj2 in
   7.461 +		            mk_conj {conj1 = vpl, conj2 = vpr}
   7.462 +			end
   7.463 +		else if is_disj t then
   7.464 +			let val {disj1, disj2} = dest_disj t 
   7.465 +			    val vpl = varform disj1
   7.466 +			    val  vpr = varform disj2 in
   7.467 +			    mk_disj {disj1 = vpl,disj2= vpr}  
   7.468 +			end
   7.469 +                else
   7.470 +                        raise VARFORM_PROBLEM;
   7.471 +                	
   7.472 + 
   7.473 +exception ASSERTION of string;
   7.474 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Thu Mar 31 19:29:26 2005 +0200
     8.3 @@ -0,0 +1,312 @@
     8.4 +
     8.5 +
     8.6 +(****************************************)
     8.7 +(* Reconstruct an axiom resolution step *)
     8.8 +(****************************************)
     8.9 +
    8.10 + fun reconstruct_axiom clauses (clausenum:int) thml (numlist, symlist, nsymlist ) =  
    8.11 +                                     let val this_axiom =(assoc  clausenum clauses)
    8.12 +                                         val symmed = (apply_rule sym  symlist this_axiom)
    8.13 +                                         val nsymmed = (apply_rule not_sym nsymlist  symmed )
    8.14 +                                     in
    8.15 +                                         rearrange_prems numlist nsymmed
    8.16 +                                     end
    8.17 +
    8.18 +(****************************************)
    8.19 +(* Reconstruct a binary resolution step *)
    8.20 +(****************************************)
    8.21 +
    8.22 +fun reconstruct_binary ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
    8.23 +        = let
    8.24 +              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
    8.25 +              val thm2 =  assoc  clause2 thml
    8.26 +              val res =   thm1 RSN ((lit2 +1), thm2)
    8.27 +              val symmed = (apply_rule sym  symlist res)
    8.28 +              val nsymmed = (apply_rule not_sym nsymlist  symmed )
    8.29 +          in
    8.30 +              rearrange_prems numlist nsymmed
    8.31 +          end
    8.32 +
    8.33 +
    8.34 +(****************************************)
    8.35 +(* Reconstruct a binary resolution step *)
    8.36 +(****************************************)
    8.37 +
    8.38 +fun reconstruct_mrr ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
    8.39 +        = let
    8.40 +              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
    8.41 +              val thm2 =  assoc  clause2 thml
    8.42 +              val res =   thm1 RSN ((lit2 +1), thm2)
    8.43 +              val symmed = (apply_rule sym  symlist res)
    8.44 +              val nsymmed = (apply_rule not_sym nsymlist  symmed )
    8.45 +          in
    8.46 +              rearrange_prems numlist nsymmed
    8.47 +          end
    8.48 +
    8.49 +(*******************************************)
    8.50 +(* Reconstruct a factoring resolution step *)
    8.51 +(*******************************************)
    8.52 +
    8.53 +fun reconstruct_factor (clause,  lit1, lit2) thml (numlist, symlist, nsymlist )= 
    8.54 +                          let 
    8.55 +                            val th =  assoc clause thml
    8.56 +                            val prems = prems_of th
    8.57 +                            val fac1 = get_nth (lit1+1) prems
    8.58 +                            val fac2 = get_nth (lit2+1) prems
    8.59 +                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
    8.60 +                            val newenv = getnewenv unif_env
    8.61 +                            val envlist = alist_of newenv
    8.62 +                            
    8.63 +                            val newsubsts = mksubstlist envlist []
    8.64 +                          in 
    8.65 +                            if (is_Var (fst(hd(newsubsts))))
    8.66 +                            then
    8.67 +                                let 
    8.68 +                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
    8.69 +                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
    8.70 +                                   val facthm = read_instantiate [(str1,str2)] th;
    8.71 +                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    8.72 +                                   val symmed = (apply_rule sym  symlist res)
    8.73 +                                   val nsymmed = (apply_rule not_sym nsymlist  symmed )
    8.74 +         
    8.75 +                                in 
    8.76 +                                   rearrange_prems numlist nsymmed
    8.77 +                                end
    8.78 +                            else
    8.79 +                                let
    8.80 +                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
    8.81 +                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
    8.82 +                                   val facthm = read_instantiate [(str1,str2)] th;
    8.83 +                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    8.84 +                                   val symmed = (apply_rule sym  symlist res)
    8.85 +                                   val nsymmed = (apply_rule not_sym nsymlist  symmed )
    8.86 +                                in 
    8.87 +                                    rearrange_prems numlist nsymmed    
    8.88 +                                end
    8.89 +                         end;
    8.90 +
    8.91 +
    8.92 +(****************************************)
    8.93 +(* Reconstruct a paramodulation step    *)
    8.94 +(****************************************)
    8.95 +
    8.96 +                          (* clause1, lit1 is thing to rewrite with *)
    8.97 +fun reconstruct_standard_para_left ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= 
    8.98 +
    8.99 +                          let 
   8.100 +                             
   8.101 +                              val newthm = para_left ((clause1, lit1), (clause2 , lit2))  thml 
   8.102 +                              val symmed = (apply_rule sym  symlist newthm)
   8.103 +                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   8.104 +                                
   8.105 +                         in
   8.106 +                              rearrange_prems numlist nsymmed  
   8.107 +                         end
   8.108 +
   8.109 +
   8.110 +
   8.111 +                        (* clause1, lit1 is thing to rewrite with *)
   8.112 +fun reconstruct_standard_para_right ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= 
   8.113 +
   8.114 +                          let 
   8.115 +                             
   8.116 +                              val newthm = para_right ((clause1, lit1), (clause2 , lit2))  thml 
   8.117 +                              val symmed = (apply_rule sym  symlist newthm)
   8.118 +                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   8.119 +                                
   8.120 +                         in
   8.121 +                              rearrange_prems numlist nsymmed  
   8.122 +                         end
   8.123 +
   8.124 +
   8.125 +
   8.126 +
   8.127 +
   8.128 +
   8.129 +
   8.130 +
   8.131 +                        (*  let 
   8.132 +                            val th1 =  assoc clause1 thml
   8.133 +                            val th2 =  assoc clause2 thml 
   8.134 +                            val prems1 = prems_of th1
   8.135 +                            val prems2 = prems_of th2
   8.136 +                            (* want to get first element of equality *)
   8.137 +
   8.138 +                            val fac1 = get_nth (lit1+1) prems1
   8.139 +                            val {lhs, rhs} = dest_eq(dest_Trueprop fac1)
   8.140 +                                             handle ERR _ => dest_eq(dest_neg (dest_Trueprop fac1))
   8.141 +                            (* get other literal involved in the paramodulation *)
   8.142 +                            val fac2 = get_nth (lit2+1) prems2
   8.143 +
   8.144 +                           (* get bit of th2 to unify with lhs of th1 *)
   8.145 +                            val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
   8.146 +                            val unif_env = unifiers (Mainsign,myenv, [(unif_lit, lhs)])
   8.147 +                            val newenv = getnewenv unif_env
   8.148 +                            val envlist = alist_of newenv
   8.149 +                            val newsubsts = mksubstlist envlist []
   8.150 +                           (* instantiate th2 with unifiers *)
   8.151 +                          
   8.152 +                            val newth1 =  
   8.153 +                              if (is_Var (fst(hd(newsubsts))))
   8.154 +                              then
   8.155 +                                  let 
   8.156 +                                     val str1 = lit_string_with_nums (fst (hd newsubsts));
   8.157 +                                     val str2 = lit_string_with_nums (snd (hd newsubsts));
   8.158 +                                     val facthm = read_instantiate [(str1,str2)] th1
   8.159 +                                  in 
   8.160 +                                     hd (Seq.list_of(distinct_subgoals_tac facthm))
   8.161 +                                  end
   8.162 +                              else
   8.163 +                                  let
   8.164 +                                     val str2 = lit_string_with_nums (fst (hd newsubsts));
   8.165 +                                     val str1 = lit_string_with_nums  (snd (hd newsubsts));
   8.166 +                                     val facthm = read_instantiate [(str1,str2)] th1
   8.167 +                                  in 
   8.168 +                                     hd (Seq.list_of(distinct_subgoals_tac facthm))
   8.169 +                                  end
   8.170 +                           (*rewrite th2 with the equality bit of th2 i.e. lit2 *)
   8.171 +                              val facthm' = select_literal  (lit1 + 1) newth1
   8.172 +                              val equal_lit = concl_of facthm'
   8.173 +                              val cterm_eq = cterm_of Mainsign equal_lit  
   8.174 +                              val eq_thm = assume cterm_eq
   8.175 +                              val meta_eq_thm = mk_meta_eq eq_thm
   8.176 +                              val newth2= rewrite_rule [meta_eq_thm] th2
   8.177 +                           (*thin lit2 from th2 *)
   8.178 +                           (* get th1 with lit one as concl, then resolve with thin_rl *)
   8.179 +                              val thm' = facthm' RS thin_rl
   8.180 +                           (* now resolve th2 with last premise of thm' *)
   8.181 +                              val newthm = newth2  RSN ((length prems1), thm')
   8.182 +                              val symmed = (apply_rule sym  symlist newthm)
   8.183 +                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   8.184 +                                
   8.185 +                         in
   8.186 +                              rearrange_prems numlist nsymmed  
   8.187 +                         end
   8.188 +
   8.189 +*)
   8.190 +
   8.191 +
   8.192 +(********************************************)
   8.193 +(* Reconstruct a rewrite step               *)
   8.194 +(********************************************)
   8.195 +
   8.196 +
   8.197 +
   8.198 +
   8.199 +
   8.200 +
   8.201 +(* does rewriting involve every literal in rewritten clause? *)
   8.202 +                    (* clause1, lit1 is thing to rewrite with *)
   8.203 +
   8.204 +fun reconstruct_rewrite (clause1, lit1, clause2) thml  (numlist, symlist, nsymlist )=
   8.205 +
   8.206 +                          let val th1 =  assoc clause1 thml
   8.207 +                              val th2 =  assoc clause2 thml 
   8.208 +                              val eq_lit_th = select_literal (lit1+1) th1
   8.209 +                              val equal_lit = concl_of eq_lit_th
   8.210 +                              val cterm_eq = cterm_of Mainsign  equal_lit 
   8.211 +                              val eq_thm = assume cterm_eq
   8.212 +                              val meta_eq_thm = mk_meta_eq eq_thm
   8.213 +                              val newth2= rewrite_rule [meta_eq_thm] th2
   8.214 +                             val symmed = (apply_rule sym  symlist newth2)
   8.215 +                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   8.216 +                                
   8.217 +                           in
   8.218 +                              rearrange_prems numlist nsymmed  
   8.219 +                           end
   8.220 +
   8.221 +
   8.222 +
   8.223 +(*****************************************)
   8.224 +(* Reconstruct an obvious reduction step *)
   8.225 +(*****************************************)
   8.226 +
   8.227 +
   8.228 +fun reconstruct_obvious  (clause1, lit1)  allvars thml clause_strs= 
   8.229 +                           let val th1 =  assoc clause1 thml
   8.230 +                               val prems1 = prems_of th1
   8.231 +                               val newthm = refl RSN ((lit1+ 1), th1)
   8.232 +                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   8.233 +                               val symmed = (apply_rule sym  symlist newthm)
   8.234 +                               val nsymmed = (apply_rule not_sym nsymlist  symmed )
   8.235 +                           in 
   8.236 +                               rearrange_prems numlist nsymmed  
   8.237 +                           end
   8.238 +
   8.239 +
   8.240 +
   8.241 +(********************************************************************************************)
   8.242 +(* reconstruct a single step of the res. proof - depending on what sort of proof step it was*)
   8.243 +(********************************************************************************************)
   8.244 +
   8.245 +
   8.246 + fun reconstruct_proof clauses clausenum thml  Axiom (numlist, symlist, nsymlist)
   8.247 +        = reconstruct_axiom clauses clausenum thml  (numlist, symlist, nsymlist)
   8.248 +      | reconstruct_proof clauses clausenum  thml (Binary (a, b)) (numlist, symlist, nsymlist)
   8.249 +        = reconstruct_binary (a, b) thml (numlist, symlist, nsymlist)
   8.250 +       | reconstruct_proof clauses clausenum  thml (MRR (a, b)) (numlist, symlist, nsymlist)
   8.251 +        = reconstruct_mrr (a, b) thml (numlist, symlist, nsymlist)
   8.252 +      | reconstruct_proof clauses clausenum  thml (Factor (a, b, c)) (numlist, symlist, nsymlist)
   8.253 +         = reconstruct_factor (a ,b ,c) thml (numlist, symlist, nsymlist)
   8.254 +      | reconstruct_proof clauses clausenum  thml (Para (a, b)) (numlist, symlist, nsymlist)
   8.255 +        = reconstruct_standard_para (a, b) thml (numlist, symlist, nsymlist)
   8.256 +      | reconstruct_proof clauses clausenum thml (Rewrite (a,b,c)) (numlist, symlist, nsymlist)
   8.257 +        = reconstruct_rewrite (a,b,c) thml (numlist, symlist, nsymlist)
   8.258 +      | reconstruct_proof clauses clausenum thml (Obvious (a,b)) (numlist, symlist, nsymlist)
   8.259 +        = reconstruct_obvious (a,b) thml (numlist, symlist, nsymlist)
   8.260 +      (*| reconstruct_proof clauses  clausenum thml (Hyper l)
   8.261 +        = reconstruct_hyper l thml*)
   8.262 +      | reconstruct_proof clauses clausenum  thml _ _ =
   8.263 +          raise ASSERTION  "proof step not implemented"
   8.264 +
   8.265 +
   8.266 +(********************************************************************************************)
   8.267 +(* reconstruct a single line of the res. proof - at the moment do only inference steps      *)
   8.268 +(********************************************************************************************)
   8.269 +
   8.270 +    fun reconstruct_line clauses thml (clause_num, (proof_step, numlist, symlist,nsymlist))
   8.271 +        = let
   8.272 +            val thm = reconstruct_proof clauses clause_num thml proof_step (numlist, symlist,nsymlist)
   8.273 +            
   8.274 +          in
   8.275 +            (clause_num, thm)::thml
   8.276 +          end
   8.277 +
   8.278 +(********************************************************************)
   8.279 +(* reconstruct through the res. proof, creating an Isabelle theorem *)
   8.280 +(********************************************************************)
   8.281 +
   8.282 +
   8.283 +fun reconstruct clauses [] thml  = ((snd( hd thml)))
   8.284 +      | reconstruct clauses (h::t) thml  
   8.285 +        = let
   8.286 +            val (thml') = reconstruct_line clauses thml h 
   8.287 +            val  (thm) = reconstruct clauses t thml' 
   8.288 +          in
   8.289 +             (thm)
   8.290 +          end
   8.291 +
   8.292 +
   8.293 +(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
   8.294 + (* and the proof as a list of the proper datatype *)
   8.295 +(* take the cnf clauses of the goal and the proof from the res. prover *)
   8.296 +(* as a list of type Proofstep and return the thm goal ==> False *)
   8.297 +
   8.298 +fun first_pair (a,b,c) = (a,b);
   8.299 +
   8.300 +fun second_pair (a,b,c) = (b,c);
   8.301 +
   8.302 +fun one_of_three (a,b,c) = a;
   8.303 +fun two_of_three (a,b,c) = b;
   8.304 +fun three_of_three (a,b,c) = c;
   8.305 +
   8.306 +(*************************)
   8.307 +(* reconstruct res proof *)
   8.308 +(*************************)
   8.309 +
   8.310 +fun reconstruct_proof clauses proof
   8.311 +        = let val thm = reconstruct clauses proof [] 
   8.312 +          in
   8.313 +             thm
   8.314 +          end
   8.315 +  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Mar 31 19:29:26 2005 +0200
     9.3 @@ -0,0 +1,809 @@
     9.4 +(******************)
     9.5 +(* complete later *)
     9.6 +(******************)
     9.7 +
     9.8 +fun not_newline ch = not (ch = "\n");
     9.9 +
    9.10 +
    9.11 +
    9.12 +(* Versions that include type information *)
    9.13 + 
    9.14 +fun string_of_thm thm = let val _ = set show_sorts
    9.15 +                                val str = Sign.string_of_term Mainsign (prop_of thm)
    9.16 +                                val no_returns =List.filter not_newline (explode str)
    9.17 +                                val _ = reset show_sorts
    9.18 +                            in 
    9.19 +                                implode no_returns
    9.20 +                            end
    9.21 +
    9.22 +
    9.23 +fun thm_of_string str = let val _ = set show_sorts
    9.24 +                                val term = read str
    9.25 +                                val propterm = mk_Trueprop term
    9.26 +                                val cterm = cterm_of Mainsign propterm
    9.27 +                                val _ = reset show_sorts
    9.28 +                            in
    9.29 +                                assume cterm
    9.30 +                            end
    9.31 +
    9.32 +(* check separate args in the watcher program for separating strings with a * or ; or something *)
    9.33 +
    9.34 +fun clause_strs_to_string [] str = str
    9.35 +|   clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
    9.36 +
    9.37 +
    9.38 +
    9.39 +fun thmvars_to_string [] str = str
    9.40 +|   thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
    9.41 +
    9.42 +
    9.43 +fun proofstep_to_string Axiom = "Axiom()"
    9.44 +|   proofstep_to_string  (Binary ((a,b), (c,d)))= "Binary"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
    9.45 +|   proofstep_to_string (Factor (a,b,c)) = "Factor"^"("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")"
    9.46 +|   proofstep_to_string  (Para ((a,b), (c,d)))= "Para"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
    9.47 +|   proofstep_to_string  (MRR ((a,b), (c,d)))= "MRR"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
    9.48 +|   proofstep_to_string (Rewrite((a,b),(c,d))) = "Rewrite"^"("^"("^(string_of_int a)^","^(string_of_int b)^")"^","^"("^(string_of_int c)^","^(string_of_int d)^")"^")"
    9.49 +
    9.50 +fun list_to_string [] liststr = liststr
    9.51 +|   list_to_string (x::[]) liststr = liststr^(string_of_int x)
    9.52 +|   list_to_string (x::xs) liststr = list_to_string xs (liststr^(string_of_int x)^",")
    9.53 +
    9.54 +
    9.55 +fun proof_to_string (num,(step,clause_strs, thmvars)) = (string_of_int num)^(proofstep_to_string step)^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    9.56 + 
    9.57 +
    9.58 +fun proofs_to_string [] str = str
    9.59 +|   proofs_to_string (x::xs) str = let val newstr = proof_to_string x 
    9.60 +                                   in
    9.61 +                                       proofs_to_string xs (str^newstr)
    9.62 +                                   end
    9.63 +
    9.64 +
    9.65 +
    9.66 +fun init_proofstep_to_string (num, step, clause_strs) = (string_of_int num)^" "^(proofstep_to_string step)^" "^(clause_strs_to_string clause_strs "")^" "
    9.67 +
    9.68 +fun init_proofsteps_to_string [] str = str
    9.69 +|   init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 
    9.70 +                                   in
    9.71 +                                       init_proofsteps_to_string xs (str^newstr)
    9.72 +                                   end
    9.73 +  
    9.74 +
    9.75 +
    9.76 +(*** get a string representing the Isabelle ordered axioms ***)
    9.77 +
    9.78 +fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta
    9.79 +                                         in
    9.80 +                                            (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    9.81 +                                         end
    9.82 +
    9.83 +
    9.84 +fun  origAxs_to_string [] str = str
    9.85 +|   origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x 
    9.86 +                                   in
    9.87 +                                       origAxs_to_string xs (str^newstr)
    9.88 +                                   end
    9.89 +
    9.90 +
    9.91 +(*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
    9.92 +
    9.93 +fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta
    9.94 +                                           in
    9.95 +                                              (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    9.96 +                                           end
    9.97 +
    9.98 +
    9.99 +
   9.100 +fun  extraAxs_to_string [] str = str
   9.101 +|   extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x 
   9.102 +                                   in
   9.103 +                                       extraAxs_to_string xs (str^newstr)
   9.104 +                                   end
   9.105 +
   9.106 +
   9.107 +
   9.108 +
   9.109 +
   9.110 +
   9.111 +fun is_axiom ( num:int,Axiom, str) = true
   9.112 +|   is_axiom (num, _,_) = false
   9.113 +
   9.114 +fun get_init_axioms xs = List.filter (is_axiom) ( xs)
   9.115 +
   9.116 +fun get_step_nums [] nums = nums
   9.117 +|   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
   9.118 +
   9.119 +fun assoc_snd a [] = raise Noassoc
   9.120 +  | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
   9.121 +
   9.122 +(* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
   9.123 +
   9.124 +(*fun get_assoc_snds [] xs assocs= assocs
   9.125 +|   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
   9.126 +*)
   9.127 +(*FIX - should this have vars in it? *)
   9.128 +fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) 
   9.129 +                                   
   9.130 +                               in 
   9.131 +                                   true
   9.132 +                              end
   9.133 +                              handle EXCEP => false
   9.134 +
   9.135 +fun assoc_out_of_order a [] = raise Noassoc
   9.136 +|   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
   9.137 +
   9.138 +fun get_assoc_snds [] xs assocs= assocs
   9.139 +|   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
   9.140 +
   9.141 +
   9.142 +
   9.143 +
   9.144 +fun add_if_not_inlist [] xs newlist = newlist
   9.145 +|   add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then 
   9.146 +                                      add_if_not_inlist ys xs (y::newlist)
   9.147 +                                        else add_if_not_inlist ys xs (newlist)
   9.148 +
   9.149 +(*
   9.150 +fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse  ( ch = ";") orelse( ch = "=")
   9.151 +
   9.152 +(* replace | by ; here *)
   9.153 +fun change_or [] = []
   9.154 +|   change_or (x::xs) = if x = "|" 
   9.155 +                          then 
   9.156 +                             [";"]@(change_or xs)
   9.157 +                          else (x::(change_or xs))
   9.158 +
   9.159 +
   9.160 +fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
   9.161 +                              val exp_term = explode termstr
   9.162 +                              val colon_term = change_or exp_term
   9.163 +                   in
   9.164 +                             implode(List.filter is_alpha_space_neg_eq_colon colon_term)
   9.165 +                   end
   9.166 +
   9.167 +fun get_clause_lits thm =  clause_lit_string (prop_of thm)
   9.168 +*)
   9.169 +
   9.170 +
   9.171 +fun onestr [] str = str
   9.172 +|   onestr (x::xs) str = onestr xs (str^(concat x))
   9.173 +
   9.174 +fun thmstrings [] str = str
   9.175 +|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
   9.176 +
   9.177 +fun onelist [] newlist = newlist
   9.178 +|   onelist (x::xs) newlist = onelist xs (newlist@x)
   9.179 +
   9.180 +
   9.181 +(**** Code to support ordinary resolution, rather than Model Elimination ****)
   9.182 +
   9.183 +(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
   9.184 +  with no contrapositives, for ordinary resolution.*)
   9.185 +
   9.186 +(*raises exception if no rules apply -- unlike RL*)
   9.187 +fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
   9.188 +  | tryres (th, []) = raise THM("tryres", 0, [th]);
   9.189 +
   9.190 +val prop_of = #prop o rep_thm;
   9.191 +
   9.192 +
   9.193 +(*For ordinary resolution. *)
   9.194 +val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
   9.195 +(*Use "theorem naming" to label the clauses*)
   9.196 +fun name_thms label =
   9.197 +    let fun name1 (th, (k,ths)) =
   9.198 +	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
   9.199 +
   9.200 +    in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
   9.201 +
   9.202 +(*Find an all-negative support clause*)
   9.203 +fun is_negative th = forall (not o #1) (literals (prop_of th));
   9.204 +
   9.205 +val neg_clauses = List.filter is_negative;
   9.206 +
   9.207 +
   9.208 +
   9.209 +(*True if the given type contains bool anywhere*)
   9.210 +fun has_bool (Type("bool",_)) = true
   9.211 +  | has_bool (Type(_, Ts)) = exists has_bool Ts
   9.212 +  | has_bool _ = false;
   9.213 +  
   9.214 +
   9.215 +(*Create a meta-level Horn clause*)
   9.216 +fun make_horn crules th = make_horn crules (tryres(th,crules))
   9.217 +			  handle THM _ => th;
   9.218 +
   9.219 +
   9.220 +(*Raises an exception if any Vars in the theorem mention type bool. That would mean
   9.221 +  they are higher-order, and in addition, they could cause make_horn to loop!*)
   9.222 +fun check_no_bool th =
   9.223 +  if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th)))
   9.224 +  then raise THM ("check_no_bool", 0, [th]) else th;
   9.225 +
   9.226 +
   9.227 +(*Rules to convert the head literal into a negated assumption. If the head
   9.228 +  literal is already negated, then using notEfalse instead of notEfalse'
   9.229 +  prevents a double negation.*)
   9.230 +val notEfalse = read_instantiate [("R","False")] notE;
   9.231 +val notEfalse' = rotate_prems 1 notEfalse;
   9.232 +
   9.233 +fun negated_asm_of_head th = 
   9.234 +    th RS notEfalse handle THM _ => th RS notEfalse';
   9.235 +
   9.236 +(*Converting one clause*)
   9.237 +fun make_meta_clause th = 
   9.238 +	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
   9.239 +
   9.240 +fun make_meta_clauses ths =
   9.241 +    name_thms "MClause#"
   9.242 +      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   9.243 +
   9.244 +(*Permute a rule's premises to move the i-th premise to the last position.*)
   9.245 +fun make_last i th =
   9.246 +  let val n = nprems_of th 
   9.247 +  in  if 1 <= i andalso i <= n 
   9.248 +      then Thm.permute_prems (i-1) 1 th
   9.249 +      else raise THM("select_literal", i, [th])
   9.250 +  end;
   9.251 +
   9.252 +(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   9.253 +  double-negations.*)
   9.254 +val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   9.255 +
   9.256 +(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   9.257 +fun select_literal i cl = negate_head (make_last i cl);
   9.258 +
   9.259 + fun get_axioms_used proof_steps thmstring = let 
   9.260 +                                             val  outfile = TextIO.openOut("foo_ax_thmstr");                                                                       
   9.261 +                                             val _ = TextIO.output (outfile, thmstring)
   9.262 +                                             
   9.263 +                                             val _ =  TextIO.closeOut outfile
   9.264 +                                            (* not sure why this is necessary again, but seems to be *)
   9.265 +                                            val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   9.266 +                                            val axioms = get_init_axioms proof_steps
   9.267 +                                            val step_nums = get_step_nums axioms []
   9.268 +                                            val thm = thm_of_string thmstring
   9.269 +                                            val clauses = make_clauses [thm]
   9.270 +                                            
   9.271 +                                            val vars = map thm_vars clauses
   9.272 +                                           
   9.273 +                                            val distvars = distinct (fold append vars [])
   9.274 +                                            val clause_terms = map prop_of clauses  
   9.275 +                                            val clause_frees = onelist (map term_frees clause_terms) []
   9.276 +
   9.277 +                                            val frees = map lit_string_with_nums clause_frees;
   9.278 +
   9.279 +                                            val distfrees = distinct frees
   9.280 +
   9.281 +                                            val metas = map make_meta_clause clauses
   9.282 +                                            val ax_strs = map (three_of_three ) axioms
   9.283 +
   9.284 +                                            (* literals of -all- axioms, not just those used by spass *)
   9.285 +                                            val meta_strs = map get_meta_lits metas
   9.286 +                                           
   9.287 +                                            val metas_and_strs = zip  metas meta_strs
   9.288 +                                             val  outfile = TextIO.openOut("foo_clauses");                                                                       
   9.289 +                                             val _ = TextIO.output (outfile, (onestr ax_strs ""))
   9.290 +                                             
   9.291 +                                             val _ =  TextIO.closeOut outfile
   9.292 +                                             val  outfile = TextIO.openOut("foo_metastrs");                                                                       
   9.293 +                                             val _ = TextIO.output (outfile, (onestr meta_strs ""))
   9.294 +                                             val _ =  TextIO.closeOut outfile
   9.295 +
   9.296 +                                            (* get list of axioms as thms with their variables *)
   9.297 +
   9.298 +                                            val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   9.299 +                                            val ax_vars = map thm_vars ax_metas
   9.300 +                                            val ax_with_vars = zip ax_metas ax_vars
   9.301 +
   9.302 +                                            (* get list of extra axioms as thms with their variables *)
   9.303 +                                            val extra_metas = add_if_not_inlist metas ax_metas []
   9.304 +                                            val extra_vars = map thm_vars extra_metas
   9.305 +                                            val extra_with_vars = if (not (extra_metas = []) ) 
   9.306 +                                                                  then
   9.307 + 									 zip extra_metas extra_vars
   9.308 +                                                                  else
   9.309 +                                                                         []
   9.310 +
   9.311 +                                           (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   9.312 +                                           val  outfile = TextIO.openOut("foo_metas")
   9.313 +
   9.314 +                                           val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   9.315 +                                           val _ =  TextIO.closeOut outfile
   9.316 +                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars2.pl <foo_metas >foo_metas2"])
   9.317 +                                         val infile = TextIO.openIn("foo_metas2")
   9.318 +                                        val ax_metas_str = TextIO.inputLine (infile)
   9.319 +                                        val _ = TextIO.closeIn infile
   9.320 +                                           val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   9.321 +                                           
   9.322 +                                         in
   9.323 +                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas))
   9.324 +                                         end
   9.325 +                                        
   9.326 +fun thmstrings [] str = str
   9.327 +|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
   9.328 +
   9.329 +fun numclstr (vars, []) str = str
   9.330 +|   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   9.331 +                               in
   9.332 +                                   numclstr  (vars,rest) newstr
   9.333 +                               end
   9.334 +
   9.335 +(*
   9.336 +
   9.337 +val proofstr = "Did parsing on Here is a proof with depth 4, length 9 :\
   9.338 +\1[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
   9.339 +\3[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
   9.340 +\5[0:Inp] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),U)* v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
   9.341 +\7[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
   9.342 +\9[0:Fac:5.0,5.1] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
   9.343 +\10[0:Res:9.0,3.0] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
   9.344 +\11[0:Res:10.0,1.0] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
   9.345 +\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
   9.346 +\14[0:Res:11.0,12.0] ||  -> .\
   9.347 +\Formulae used in the proof :"
   9.348 +
   9.349 +*)
   9.350 +
   9.351 +
   9.352 +fun addvars  c (a,b)  = (a,b,c)
   9.353 +
   9.354 +
   9.355 +
   9.356 +(*********************************************************************)
   9.357 +(* Pass in spass string of proof and string version of isabelle goal *)
   9.358 +(* Get out reconstruction steps as a string to be sent to Isabelle   *)
   9.359 +(*********************************************************************)
   9.360 +
   9.361 +
   9.362 +(*
   9.363 +
   9.364 +
   9.365 +val proofstr = "Here is a proof with depth 2, length 5 :\
   9.366 +\1[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   9.367 +\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
   9.368 +\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa).\
   9.369 +\7[0:Res:1.0,5.0] ||  -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   9.370 +\9[0:Res:7.0,3.0] ||  -> .\
   9.371 +\Formulae used in the proof :"
   9.372 +
   9.373 +
   9.374 +val proofstr = "Here is a proof with depth 4, length 9 :\
   9.375 +\1[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   9.376 +\3[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
   9.377 +\5[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)* v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   9.378 +\7[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
   9.379 +\9[0:Fac:5.0,5.1] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   9.380 +\10[0:Res:9.0,3.0] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
   9.381 +\11[0:Res:10.0,1.0] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   9.382 +\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
   9.383 +\14[0:Res:11.0,12.0] ||  -> .\
   9.384 +\Formulae used in the proof :";
   9.385 +
   9.386 +
   9.387 +val thmstring = " (~ (P::'a::type => bool) (x::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | P (x::'a::type)) & ((P::'a::type => bool) (xa::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | ~ P (xb::'a::type))";
   9.388 +
   9.389 +val thmstring = "(ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)"
   9.390 +
   9.391 +
   9.392 +val thmstring ="(ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)"
   9.393 +
   9.394 +val proofstr = "Did parsing on Here is a proof with depth 2, length 5 :\
   9.395 +\1[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   9.396 +\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
   9.397 +\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x(tconst_fun(typ__asc39_a,typ__asc39_a),U))* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U)).\
   9.398 +\7[0:Res:1.0,5.0] ||  -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U))*.\
   9.399 +\9[0:Res:7.0,3.0] ||  -> .\
   9.400 +\Formulae used in the proof :";
   9.401 +
   9.402 +*)
   9.403 +
   9.404 +
   9.405 +fun spassString_to_reconString proofstr thmstring = 
   9.406 +                                              let val  outfile = TextIO.openOut("thmstringfile");                                                                                      val _= warning("proofstr is: "^proofstr);
   9.407 +                                                  val _ = warning ("thmstring is: "^thmstring);
   9.408 +                                                  val _ = TextIO.output (outfile, (thmstring))
   9.409 +                                                  val _ =  TextIO.closeOut outfile
   9.410 +                                                  val proofextract = extract_proof proofstr
   9.411 +                                                  val tokens = fst(lex proofextract)
   9.412 +                                                     
   9.413 +                                              (***********************************)
   9.414 +                                              (* parse spass proof into datatype *)
   9.415 +                                              (***********************************)
   9.416 +
   9.417 +                                                  val proof_steps1 = parse tokens
   9.418 +                                                  val proof_steps = just_change_space proof_steps1
   9.419 +
   9.420 +                                                  val  outfile = TextIO.openOut("foo_parse");                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   9.421 +                                                  val _ =  TextIO.closeOut outfile
   9.422 +                                                
   9.423 +                                                  val  outfile = TextIO.openOut("foo_thmstring_at_parse");                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   9.424 +                                                  val _ =  TextIO.closeOut outfile
   9.425 +                                              (************************************)
   9.426 +                                              (* recreate original subgoal as thm *)
   9.427 +                                              (************************************)
   9.428 +                                                
   9.429 +                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   9.430 +                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
   9.431 +                                                  
   9.432 +                                                  (*val numcls_string = numclstr ( vars, numcls) ""*)
   9.433 +                                                  val  outfile = TextIO.openOut("foo_axiom");                                                                            val _ = TextIO.output (outfile,"got axioms")
   9.434 +                                                  val _ =  TextIO.closeOut outfile
   9.435 +                                                    
   9.436 +                                              (************************************)
   9.437 +                                              (* translate proof                  *)
   9.438 +                                              (************************************)
   9.439 +                                                  val  outfile = TextIO.openOut("foo_steps");                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   9.440 +                                                  val _ =  TextIO.closeOut outfile
   9.441 +                                                  val (newthm,proof) = translate_proof numcls  proof_steps vars
   9.442 +                                                  val  outfile = TextIO.openOut("foo_steps2");                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   9.443 +                                                  val _ =  TextIO.closeOut outfile
   9.444 +                                              (***************************************************)
   9.445 +                                              (* transfer necessary steps as strings to Isabelle *)
   9.446 +                                              (***************************************************)
   9.447 +                                                  (* turn the proof into a string *)
   9.448 +                                                  val reconProofStr = proofs_to_string proof ""
   9.449 +                                                  (* do the bit for the Isabelle ordered axioms at the top *)
   9.450 +                                                  val ax_nums = map fst numcls
   9.451 +                                                  val ax_strs = map get_meta_lits_bracket (map snd numcls)
   9.452 +                                                  val numcls_strs = zip ax_nums ax_strs
   9.453 +                                                  val num_cls_vars =  map (addvars vars) numcls_strs;
   9.454 +                                                  val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
   9.455 +                                                  
   9.456 +                                                  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   9.457 +                                                  val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
   9.458 +                                                  val frees_str = "["^(thmvars_to_string frees "")^"]"
   9.459 +                                                  val  outfile = TextIO.openOut("reconstringfile");
   9.460 +
   9.461 +                                                  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   9.462 +                                                  val _ =  TextIO.closeOut outfile
   9.463 +                                              in 
   9.464 +                                                   (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   9.465 +                                              end
   9.466 +                                              handle _ => (let val  outfile = TextIO.openOut("foo_handler");
   9.467 +
   9.468 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   9.469 +                                                  val _ =  TextIO.closeOut outfile
   9.470 +                                              in 
   9.471 +                                                 "Proof found but translation failed!"
   9.472 +                                              end)
   9.473 +
   9.474 +
   9.475 +
   9.476 +
   9.477 +
   9.478 +
   9.479 +
   9.480 +
   9.481 +
   9.482 +(**********************************************************************************)
   9.483 +(* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
   9.484 +(* This will be done by the signal handler                                        *)
   9.485 +(**********************************************************************************)
   9.486 +
   9.487 +(* Parse in the string version of the proof steps for reconstruction *)
   9.488 +(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*)
   9.489 +
   9.490 +
   9.491 + val term_numstep =
   9.492 +        (number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c))
   9.493 +
   9.494 +val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")"))
   9.495 +            >> (fn (_) => ExtraAxiom)
   9.496 +
   9.497 +
   9.498 +
   9.499 +val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")"))
   9.500 +            >> (fn (_) => OrigAxiom)
   9.501 +
   9.502 +
   9.503 + val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")"))
   9.504 +            >> (fn (_) => Axiom)
   9.505 +     
   9.506 +
   9.507 +
   9.508 +      
   9.509 + val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "(")) 
   9.510 +                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   9.511 +                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   9.512 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e))
   9.513 +      
   9.514 +
   9.515 + val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "(")) 
   9.516 +                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   9.517 +                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   9.518 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e))
   9.519 +      
   9.520 + val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "(")) 
   9.521 +                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   9.522 +                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   9.523 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e))
   9.524 +      
   9.525 +
   9.526 + val factorstep = (a (Word "Factor")) ++ (a (Other "("))
   9.527 +                    ++ number ++ (a (Other ","))
   9.528 +                       ++ number ++ (a (Other ","))
   9.529 +                       ++ number ++  (a (Other ")"))
   9.530 +                   
   9.531 +            >> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) =>  Factor (c,e,f))
   9.532 +
   9.533 +
   9.534 +val rewritestep = (a (Word "Rewrite"))  ++ (a (Other "(")) ++ (a (Other "(")) 
   9.535 +                   ++ term_numstep  ++ (a (Other ")")) ++ (a (Other ","))
   9.536 +                   ++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")"))
   9.537 +            >> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))
   9.538 +
   9.539 +val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 
   9.540 +                   ++ term_numstep  ++ (a (Other ")")) 
   9.541 +            >> (fn (_, (_, (c,_))) => Obvious (c))
   9.542 +
   9.543 + val methodstep = extraaxiomstep || origaxiomstep || axiomstep ||binarystep || factorstep|| parastep || mrrstep || rewritestep || obviousstep
   9.544 +
   9.545 +
   9.546 + val number_list_step =
   9.547 +        ( number ++ many ((a (Other ",") ++ number)>> snd))
   9.548 +        >> (fn (a,b) => (a::b))
   9.549 +        
   9.550 + val numberlist_step = a (Other "[")  ++ a (Other "]")
   9.551 +                        >>(fn (_,_) => ([]:int list))
   9.552 +                       || a (Other "[") ++ number_list_step ++ a (Other "]")
   9.553 +                        >>(fn (_,(a,_)) => a)
   9.554 +                    
   9.555 +
   9.556 +
   9.557 +(** change this to allow P (x U) *)
   9.558 + fun arglist_step input = ( word ++ many  word >> (fn (a, b) => (a^" "^(implode_with_space b)))
   9.559 +                           ||word >> (fn (a) => (a)))input
   9.560 +                
   9.561 +
   9.562 +fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++  a (Other ")")
   9.563 +                                          >>(fn (a, (b, (c,d))) => (a^" ("^(c)^")"))
   9.564 +                        || arglist_step >> (fn (a) => (a)))input
   9.565 +                           
   9.566 +
   9.567 +
   9.568 +(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
   9.569 +                     ||  arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input
   9.570 +*)
   9.571 +
   9.572 +
   9.573 + fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b))
   9.574 +                     ||  literal_step ++ a (Other "%")>> (fn (a,b) => a ))input
   9.575 +
   9.576 +
   9.577 +         
   9.578 +
   9.579 + val term_list_step =
   9.580 +        (  term_step ++ many ( term_step))
   9.581 +        >> (fn (a,b) => (a::b))
   9.582 +        
   9.583 + 
   9.584 +val term_lists_step = a (Other "[")  ++ a (Other "]")
   9.585 +                        >>(fn (_,_) => ([]:string list))
   9.586 +                       || a (Other "[") ++ term_list_step ++ a (Other "]")
   9.587 +                        >>(fn (_,(a,_)) => a)
   9.588 +                     
   9.589 +
   9.590 +
   9.591 +
   9.592 +fun anytoken_step input  = (word>> (fn (a) => a)  ) input
   9.593 +                       handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a)  ) input
   9.594 +                      handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
   9.595 +
   9.596 +
   9.597 +
   9.598 +fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
   9.599 +                  >> (fn (a,b) =>  (a^" "^(implode b)))) input
   9.600 +
   9.601 +
   9.602 +
   9.603 + val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
   9.604 +                >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
   9.605 +    
   9.606 + val lines_step = many linestep
   9.607 +
   9.608 + val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
   9.609 +    
   9.610 + val parse_step = fst o alllines_step
   9.611 +
   9.612 +
   9.613 + (*
   9.614 +val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) -->(EX x::'a::type. P x) = (ALL y::'a::type. P y)"
   9.615 +*)
   9.616 +
   9.617 +(************************************************************)
   9.618 +(* Construct an Isar style proof from a list of proof steps *)
   9.619 +(************************************************************)
   9.620 +(* want to assume all axioms, then do haves for the other clauses*)
   9.621 +(* then show for the last step *)
   9.622 +fun one_of_three (a,b,c) = a;
   9.623 +fun two_of_three (a,b,c) = b;
   9.624 +fun three_of_three (a,b,c) = c;
   9.625 +
   9.626 +(* replace ~ by not here *)
   9.627 +fun change_nots [] = []
   9.628 +|   change_nots (x::xs) = if x = "~" 
   9.629 +                          then 
   9.630 +                             ["\\", "<", "n", "o", "t", ">"]@(change_nots xs)
   9.631 +                          else (x::(change_nots xs))
   9.632 +
   9.633 +(*
   9.634 +fun clstrs_to_string [] str = str
   9.635 +|   clstrs_to_string (x::[]) str = str^x
   9.636 +|   clstrs_to_string (x::xs) str = clstrs_to_string xs (str^(x^"; "))
   9.637 +*)
   9.638 +fun clstrs_to_string [] str = implode (change_nots (explode str))
   9.639 +|   clstrs_to_string (x::[]) str = implode (change_nots (explode (str^x)))
   9.640 +|   clstrs_to_string (x::xs) str = implode (change_nots (explode (clstrs_to_string xs (str^(x^"; ")))))
   9.641 +
   9.642 +
   9.643 +
   9.644 +fun thmvars_to_quantstring [] str = str
   9.645 +|   thmvars_to_quantstring (x::[]) str =str^x^". "
   9.646 +|   thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" "))
   9.647 +
   9.648 +
   9.649 +fun clause_strs_to_isar clstrs [] =  "\"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^" \\<Longrightarrow> False\""
   9.650 +|   clause_strs_to_isar clstrs thmvars = "\"\\<And>"^(thmvars_to_quantstring thmvars "")^"\\<lbrakk>"^(clstrs_to_string clstrs "")^"\\<rbrakk> "^"\\<Longrightarrow> False\""
   9.651 +
   9.652 +fun frees_to_string [] str = implode (change_nots (explode str))
   9.653 +|   frees_to_string (x::[]) str = implode (change_nots (explode (str^x)))
   9.654 +|   frees_to_string  (x::xs) str = implode (change_nots (explode (frees_to_string xs (str^(x^" ")))))
   9.655 +
   9.656 +fun frees_to_isar_str [] =  ""
   9.657 +|   frees_to_isar_str  clstrs = (frees_to_string clstrs "")
   9.658 +
   9.659 +
   9.660 +(***********************************************************************)
   9.661 +(* functions for producing assumptions for the Isabelle ordered axioms *)
   9.662 +(***********************************************************************)
   9.663 +(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";       
   9.664 +num, rule, clausestrs, vars*)
   9.665 +
   9.666 +
   9.667 +(* assume the extra clauses - not used in Spass proof *)
   9.668 +
   9.669 +fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true
   9.670 +|   is_extraaxiom_step (num, _) = false
   9.671 +
   9.672 +fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs)
   9.673 +
   9.674 +fun assume_isar_extraaxiom [] str  = str
   9.675 +|   assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str  = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
   9.676 +
   9.677 +
   9.678 +
   9.679 +fun assume_isar_extraaxioms  [] = ""
   9.680 +|assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 
   9.681 +                                         in
   9.682 +                                             assume_isar_extraaxiom xs str
   9.683 +                                         end
   9.684 +
   9.685 +(* assume the Isabelle ordered clauses *)
   9.686 +
   9.687 +fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true
   9.688 +|   is_origaxiom_step (num, _) = false
   9.689 +
   9.690 +fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs)
   9.691 +
   9.692 +fun assume_isar_origaxiom [] str  = str
   9.693 +|   assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str  = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " )
   9.694 +
   9.695 +
   9.696 +
   9.697 +fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 
   9.698 +                                         in
   9.699 +                                             assume_isar_origaxiom xs str
   9.700 +                                         end
   9.701 +
   9.702 +
   9.703 +
   9.704 +fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true
   9.705 +|   is_axiom_step (num, _) = false
   9.706 +
   9.707 +fun get_axioms xs = List.filter  (is_axiom_step) ( xs)
   9.708 +
   9.709 +fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   9.710 +
   9.711 +fun  by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n"
   9.712 +
   9.713 +
   9.714 +fun isar_axiomline (numb, (step, clstrs, thmstrs))  = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) )
   9.715 +
   9.716 +
   9.717 +fun isar_axiomlines [] str = str
   9.718 +|   isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x))
   9.719 +
   9.720 +
   9.721 +fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   9.722 +
   9.723 +
   9.724 +fun  by_isar_line ((Binary ((a,b), (c,d))))="by(rule cl"^
   9.725 +                                                  (string_of_int a)^" [BINARY "^(string_of_int b)^" "^"cl"^
   9.726 +                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
   9.727 +|   by_isar_line ( (Para ((a,b), (c,d)))) ="by (rule cl"^
   9.728 +                                                  (string_of_int a)^" [PARAMOD "^(string_of_int b)^" "^"cl"^
   9.729 +                                                  (string_of_int c)^" "^(string_of_int d)^"])"^"\n"
   9.730 +|   by_isar_line ((Factor ((a,b,c)))) =    "by (rule cl"^(string_of_int a)^" [FACTOR "^(string_of_int b)^" "^
   9.731 +                                                  (string_of_int c)^" "^"])"^"\n"
   9.732 +|   by_isar_line ( (Rewrite ((a,b),(c,d)))) =  "by (rule cl"^(string_of_int a)^" [DEMOD "^(string_of_int b)^" "^
   9.733 +                                                  (string_of_int c)^" "^(string_of_int d)^" "^"])"^"\n"
   9.734 +
   9.735 +|   by_isar_line ( (Obvious ((a,b)))) =  "by (rule cl"^(string_of_int a)^" [OBVIOUS "^(string_of_int b)^" ])"^"\n"
   9.736 +
   9.737 +fun isar_line (numb, (step, clstrs, thmstrs))  = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step)
   9.738 +
   9.739 +
   9.740 +fun isar_lines [] str = str
   9.741 +|   isar_lines (x::xs) str = isar_lines xs (str^(isar_line x))
   9.742 +
   9.743 +fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
   9.744 +
   9.745 +
   9.746 +fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
   9.747 +                           val extraax_num = length extraaxioms
   9.748 +                           val origaxioms_and_steps = drop (extraax_num) xs  
   9.749 +                          
   9.750 +  
   9.751 +                           val origaxioms = get_origaxioms origaxioms_and_steps
   9.752 +                           val origax_num = length origaxioms
   9.753 +                           val axioms_and_steps = drop (origax_num + extraax_num) xs  
   9.754 +                           val axioms = get_axioms axioms_and_steps
   9.755 +                           
   9.756 +                           val steps = drop origax_num axioms_and_steps
   9.757 +                           val firststeps = butlast steps
   9.758 +                           val laststep = last steps
   9.759 +                           val goalstring = implode(butlast(explode goalstring))
   9.760 +                        
   9.761 +                           val isar_proof = 
   9.762 +                           ("show \""^goalstring^"\"\n")^
   9.763 +                           ("proof (rule ccontr,skolemize, make_clauses) \n")^
   9.764 +                           ("fix "^(frees_to_isar_str frees)^"\n")^
   9.765 +                           (assume_isar_extraaxioms extraaxioms)^
   9.766 +                           (assume_isar_origaxioms origaxioms)^
   9.767 +                           (isar_axiomlines axioms "")^
   9.768 +                           (isar_lines firststeps "")^
   9.769 +                           (last_isar_line laststep)^
   9.770 +                           ("qed")
   9.771 +                          val  outfile = TextIO.openOut("isar_proof_file");
   9.772 +
   9.773 +                                                  val _ = TextIO.output (outfile, isar_proof)
   9.774 +                                                  val _ =  TextIO.closeOut outfile
   9.775 +
   9.776 +
   9.777 +                       in
   9.778 +                           isar_proof
   9.779 +                       end
   9.780 +
   9.781 +(* get fix vars from axioms - all Frees *)
   9.782 +(* check each clause for meta-vars and /\ over them at each step*)
   9.783 +
   9.784 +(*******************************************************)
   9.785 +(* This assumes the thm list  "numcls" is still there  *)
   9.786 +(* In reality, should probably label it with an        *)
   9.787 +(* ID number identifying the subgoal.  This could      *)
   9.788 +(* be passed over to the watcher, e.g.  numcls25       *)
   9.789 +(*******************************************************)
   9.790 +
   9.791 +(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
   9.792 +
   9.793 +val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   9.794 +
   9.795 +val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)";
   9.796 +
   9.797 +
   9.798 +val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   9.799 +
   9.800 +val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
   9.801 +*)
   9.802 +
   9.803 +fun apply_res_thm str goalstring  = let val tokens = fst (lex str);
   9.804 +
   9.805 +                                   val (frees,recon_steps) = parse_step tokens 
   9.806 +                                   val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   9.807 +                                   val foo =   TextIO.openOut "foobar";
   9.808 +                               in 
   9.809 +                                  TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   9.810 +                               end 
   9.811 +
   9.812 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Mar 31 19:29:26 2005 +0200
    10.3 @@ -0,0 +1,510 @@
    10.4 +
    10.5 +fun take n [] = []
    10.6 +|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
    10.7 +
    10.8 +fun drop n [] = []
    10.9 +|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
   10.10 +
   10.11 +fun remove n [] = []
   10.12 +|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
   10.13 +
   10.14 +fun remove_nth n [] = []
   10.15 +|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
   10.16 +
   10.17 +fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
   10.18 +
   10.19 +fun add_in_order (x:string) [] = [x]
   10.20 +|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
   10.21 +                             then 
   10.22 +                                  (x::(y::ys))
   10.23 +                             else
   10.24 +                                  (y::(add_in_order x ys))
   10.25 +fun add_once x [] = [x]
   10.26 +|   add_once x (y::ys) = if (inlist x (y::ys)) then 
   10.27 +                            (y::ys)
   10.28 +                        else
   10.29 +                            add_in_order x (y::ys)
   10.30 +     
   10.31 +fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
   10.32 +
   10.33 +Goal "False ==> False";
   10.34 +by Auto_tac;
   10.35 +qed "False_imp";
   10.36 +
   10.37 +exception Reflex_equal;
   10.38 +
   10.39 +(********************************)
   10.40 +(* Proofstep datatype           *)
   10.41 +(********************************)
   10.42 +(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)
   10.43 +
   10.44 +datatype Side = Left |Right
   10.45 +
   10.46 + datatype Proofstep = ExtraAxiom
   10.47 +                     |OrigAxiom
   10.48 +                     | Axiom
   10.49 +                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
   10.50 +                     | MRR of (int * int) * (int * int) 
   10.51 +                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
   10.52 +                     | Para of (int * int) * (int * int) 
   10.53 +                     | Rewrite of (int * int) * (int * int)  
   10.54 +                     | Obvious of (int * int)
   10.55 +                     (*| Hyper of int list*)
   10.56 +                     | Unusedstep of unit
   10.57 +
   10.58 +
   10.59 +datatype Clausesimp = Binary_s of int * int
   10.60 +                      | Factor_s of unit
   10.61 +                      | Demod_s of (int * int) list
   10.62 +                      | Hyper_s of int list
   10.63 +                      | Unusedstep_s of unit
   10.64 +
   10.65 +
   10.66 +
   10.67 +datatype Step_label = T_info
   10.68 +                     |P_info
   10.69 +
   10.70 +
   10.71 +fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
   10.72 +
   10.73 +
   10.74 +
   10.75 +fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t
   10.76 +                                 val exp_term = explode termstr
   10.77 +                             in
   10.78 +                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
   10.79 +                             end
   10.80 +
   10.81 +
   10.82 +(****************************************)
   10.83 +(* Reconstruct an axiom resolution step *)
   10.84 +(****************************************)
   10.85 +
   10.86 + fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
   10.87 +                                     let val this_axiom =(assoc  clausenum clauses)
   10.88 +                                         val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
   10.89 +                                         val thmvars = thm_vars res
   10.90 +                                     in
   10.91 +                                         (res, (Axiom,clause_strs,thmvars )  )
   10.92 +                                     end
   10.93 +
   10.94 +(****************************************)
   10.95 +(* Reconstruct a binary resolution step *)
   10.96 +(****************************************)
   10.97 +
   10.98 +                 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
   10.99 +fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
  10.100 +        = let
  10.101 +              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
  10.102 +              val thm2 =  assoc  clause2 thml
  10.103 +              val res =   thm1 RSN ((lit2 +1), thm2)
  10.104 +              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
  10.105 +              val thmvars = thm_vars res
  10.106 +          in
  10.107 +             (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
  10.108 +          end
  10.109 +
  10.110 +
  10.111 +
  10.112 +(******************************************************)
  10.113 +(* Reconstruct a matching replacement resolution step *)
  10.114 +(******************************************************)
  10.115 +
  10.116 +
  10.117 +fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
  10.118 +        = let
  10.119 +              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
  10.120 +              val thm2 =  assoc  clause2 thml
  10.121 +              val res =   thm1 RSN ((lit2 +1), thm2)
  10.122 +              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
  10.123 +              val thmvars = thm_vars res
  10.124 +          in
  10.125 +             (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
  10.126 +          end
  10.127 +
  10.128 +
  10.129 +(*******************************************)
  10.130 +(* Reconstruct a factoring resolution step *)
  10.131 +(*******************************************)
  10.132 +
  10.133 +fun mksubstlist [] sublist = sublist
  10.134 +   |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b 
  10.135 +                                          val avar = Var(a,vartype)
  10.136 +                                          val newlist = ((avar,b)::sublist) in
  10.137 +                                          mksubstlist rest newlist
  10.138 +                                      end;
  10.139 +
  10.140 +(* based on Tactic.distinct_subgoals_tac *)
  10.141 +
  10.142 +fun delete_assump_tac state lit =
  10.143 +    let val (frozth,thawfn) = freeze_thaw state
  10.144 +        val froz_prems = cprems_of frozth
  10.145 +        val assumed = implies_elim_list frozth (map assume froz_prems)
  10.146 +        val new_prems = remove_nth lit froz_prems
  10.147 +        val implied = implies_intr_list new_prems assumed
  10.148 +    in  
  10.149 +        Seq.single (thawfn implied)  
  10.150 +    end
  10.151 +
  10.152 +
  10.153 +
  10.154 +
  10.155 +
  10.156 +(*************************************)
  10.157 +(* Reconstruct a factoring step      *)
  10.158 +(*************************************)
  10.159 +
  10.160 +fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
  10.161 +                          let 
  10.162 +                            val th =  assoc clause thml
  10.163 +                            val prems = prems_of th
  10.164 +                            val fac1 = get_nth (lit1+1) prems
  10.165 +                            val fac2 = get_nth (lit2+1) prems
  10.166 +                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
  10.167 +                            val newenv = getnewenv unif_env
  10.168 +                            val envlist = alist_of newenv
  10.169 +                            
  10.170 +                            val newsubsts = mksubstlist envlist []
  10.171 +                          in 
  10.172 +                            if (is_Var (fst(hd(newsubsts))))
  10.173 +                            then
  10.174 +                                let 
  10.175 +                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
  10.176 +                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
  10.177 +                                   val facthm = read_instantiate [(str1,str2)] th;
  10.178 +                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
  10.179 +                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
  10.180 +                                   val thmvars = thm_vars res'
  10.181 +                                in 
  10.182 +                                       (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
  10.183 +                                end
  10.184 +                            else
  10.185 +                                let
  10.186 +                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
  10.187 +                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
  10.188 +                                   val facthm = read_instantiate [(str1,str2)] th;
  10.189 +                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
  10.190 +                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
  10.191 +                                  val thmvars = thm_vars res'
  10.192 +                                in 
  10.193 +                                       (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
  10.194 +                                end
  10.195 +                         end;
  10.196 +
  10.197 +
  10.198 +
  10.199 +Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
  10.200 +val prems = it;
  10.201 +br (hd prems) 1;
  10.202 +br (hd(tl(tl prems))) 1;
  10.203 +qed "merge";
  10.204 +
  10.205 +
  10.206 +
  10.207 +fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm))
  10.208 +                             then 
  10.209 +                                  t
  10.210 +                             else 
  10.211 +                                 let val {Rand, Rator} = dest_comb t
  10.212 +                                 in
  10.213 +                                     get_unif_comb Rand eqterm
  10.214 +                                 end
  10.215 +
  10.216 +fun get_rhs_unif_lit t eqterm = if (can dest_eq t)
  10.217 +                            then 
  10.218 +                                let val {lhs, rhs} = dest_eq( t)
  10.219 +                                in
  10.220 +                                    rhs
  10.221 +                                end
  10.222 +                            else
  10.223 +                                get_unif_comb t eqterm
  10.224 +                         
  10.225 +fun get_lhs_unif_lit t eqterm = if (can dest_eq t)
  10.226 +                            then 
  10.227 +                                let val {lhs, rhs} = dest_eq( t)
  10.228 +                                in
  10.229 +                                    lhs
  10.230 +                                end
  10.231 +                            else
  10.232 +                                get_unif_comb t eqterm
  10.233 +
  10.234 +
  10.235 +(*************************************)
  10.236 +(* Reconstruct a paramodulation step *)
  10.237 +(*************************************)
  10.238 +
  10.239 +val rev_subst = rotate_prems 1 subst;
  10.240 +val rev_ssubst = rotate_prems 1 ssubst;
  10.241 +
  10.242 +
  10.243 +(* have changed from negate_nead to negate_head.  God knows if this will actually work *)
  10.244 +fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
  10.245 +                          let 
  10.246 +                            val th1 =  assoc clause1 thml
  10.247 +                            val th2 =  assoc clause2 thml 
  10.248 +                            val eq_lit_th = select_literal (lit1+1) th1
  10.249 +                            val mod_lit_th = select_literal (lit2+1) th2
  10.250 +                            val eqsubst = eq_lit_th RSN (2,rev_subst)
  10.251 +                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
  10.252 +			    val newth' =negate_head newth 
  10.253 +                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars 
  10.254 +                                handle Not_in_list => let 
  10.255 +                                                  val mod_lit_th' = mod_lit_th RS not_sym
  10.256 +                                                   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
  10.257 +			                           val newth' =negate_head newth 
  10.258 +                                               in 
  10.259 +                                                  (rearrange_clause newth' clause_strs allvars)
  10.260 +                                               end)
  10.261 +                            val thmvars = thm_vars res
  10.262 +                         in 
  10.263 +                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
  10.264 +                         end
  10.265 +
  10.266 +(*              
  10.267 +fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
  10.268 +                          let 
  10.269 +                            val th1 =  assoc clause1 thml
  10.270 +                            val th2 =  assoc clause2 thml 
  10.271 +                            val eq_lit_th = select_literal (lit1+1) th1
  10.272 +                            val mod_lit_th = select_literal (lit2+1) th2
  10.273 +                            val eqsubst = eq_lit_th RSN (2,rev_subst)
  10.274 +                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
  10.275 +			    val newth' =negate_nead newth 
  10.276 +                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars)
  10.277 +                            val thmvars = thm_vars res
  10.278 +                         in 
  10.279 +                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
  10.280 +                         end
  10.281 +
  10.282 +*)
  10.283 +
  10.284 +
  10.285 +(********************************)
  10.286 +(* Reconstruct a rewriting step *)
  10.287 +(********************************)
  10.288 + 
  10.289 +(*
  10.290 +
  10.291 +val rev_subst = rotate_prems 1 subst;
  10.292 +
  10.293 +fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
  10.294 +     let  val eq_lit_th = select_literal (lit1+1) cl1
  10.295 +          val mod_lit_th = select_literal (lit2+1) cl2
  10.296 +          val eqsubst = eq_lit_th RSN (2,rev_subst)
  10.297 +          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
  10.298 +eqsubst)
  10.299 +     in negated_asm_of_head newth end;
  10.300 +
  10.301 +val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
  10.302 +eqsubst)
  10.303 +
  10.304 +val mod_lit_th' = mod_lit_th RS not_sym
  10.305 +
  10.306 +*)
  10.307 +
  10.308 +
  10.309 +fun delete_assumps 0 th = th 
  10.310 +|   delete_assumps n th = let val th_prems = length (prems_of th)
  10.311 +                              val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
  10.312 +                          in
  10.313 +                              delete_assumps (n-1) th'
  10.314 +                          end
  10.315 +
  10.316 +(* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
  10.317 +(* changed negate_nead to negate_head here too*)
  10.318 +                    (* clause1, lit1 is thing to rewrite with *)
  10.319 +fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
  10.320 +
  10.321 +                          let val th1 =  assoc clause1 thml
  10.322 +                              val th2 = assoc clause2 thml
  10.323 +                              val eq_lit_th = select_literal (lit1+1) th1
  10.324 +                              val mod_lit_th = select_literal (lit2+1) th2
  10.325 +                              val eqsubst = eq_lit_th RSN (2,rev_subst)
  10.326 +                              val eq_lit_prem_num = length (prems_of eq_lit_th)
  10.327 +                              val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
  10.328 +                              val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
  10.329 +eqsubst)
  10.330 +                         
  10.331 +                              val newthm = negate_head newth
  10.332 +                              val newthm' = delete_assumps eq_lit_prem_num newthm
  10.333 +                              val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
  10.334 +                              val thmvars = thm_vars res
  10.335 +                           in
  10.336 +                               (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
  10.337 +                           end
  10.338 +
  10.339 +
  10.340 +
  10.341 +(*****************************************)
  10.342 +(* Reconstruct an obvious reduction step *)
  10.343 +(*****************************************)
  10.344 +
  10.345 +
  10.346 +fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
  10.347 +                           let val th1 =  assoc clause1 thml
  10.348 +                               val prems1 = prems_of th1
  10.349 +                               val newthm = refl RSN ((lit1+ 1), th1)
  10.350 +                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
  10.351 +                               val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
  10.352 +                               val thmvars = thm_vars res
  10.353 +                           in 
  10.354 +                               (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
  10.355 +                           end
  10.356 +
  10.357 +(**************************************************************************************)
  10.358 +(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
  10.359 +(**************************************************************************************)
  10.360 +
  10.361 + fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
  10.362 +        = follow_axiom clauses allvars  clausenum thml clause_strs
  10.363 +
  10.364 +      | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
  10.365 +        = follow_binary  (a, b)  allvars thml clause_strs
  10.366 +
  10.367 +      | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
  10.368 +        = follow_mrr (a, b)  allvars thml clause_strs
  10.369 +
  10.370 +      | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
  10.371 +         = follow_factor a b c  allvars thml clause_strs
  10.372 +
  10.373 +      | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
  10.374 +        = follow_standard_para (a, b) allvars  thml clause_strs
  10.375 +
  10.376 +      | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
  10.377 +        = follow_rewrite (a,b)  allvars thml clause_strs
  10.378 +
  10.379 +      | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
  10.380 +        = follow_obvious (a,b)  allvars thml clause_strs
  10.381 +
  10.382 +      (*| follow_proof clauses  clausenum thml (Hyper l)
  10.383 +        = follow_hyper l thml*)
  10.384 +      | follow_proof clauses  allvars clausenum  thml _ _ =
  10.385 +          raise ASSERTION  "proof step not implemented"
  10.386 +
  10.387 +
  10.388 +
  10.389 + 
  10.390 +(**************************************************************************************)
  10.391 +(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
  10.392 +(**************************************************************************************)
  10.393 +
  10.394 +    fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons
  10.395 +        = let
  10.396 +            val (thm, recon_fun) = follow_proof clauses  allvars clause_num thml proof_step clause_strs 
  10.397 +            val recon_step = (recon_fun)
  10.398 +          in
  10.399 +            (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
  10.400 +          end
  10.401 +
  10.402 +(***************************************************************)
  10.403 +(* follow through the res. proof, creating an Isabelle theorem *)
  10.404 +(***************************************************************)
  10.405 +
  10.406 +
  10.407 +
  10.408 +(*fun is_proof_char ch = (case ch of 
  10.409 +                       
  10.410 +                        "(" => true
  10.411 +                       |  ")" => true
  10.412 +                         | ":" => true
  10.413 +                        |  "'" => true
  10.414 +                        |  "&" => true
  10.415 +                        | "|" => true
  10.416 +                        | "~" => true
  10.417 +                        |  "." => true
  10.418 +                        |(is_alpha ) => true
  10.419 +                       |(is_digit) => true
  10.420 +                         | _ => false)*)
  10.421 +
  10.422 +fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
  10.423 +
  10.424 +fun proofstring x = let val exp = explode x 
  10.425 +                    in
  10.426 +                        List.filter (is_proof_char ) exp
  10.427 +                    end
  10.428 +
  10.429 +
  10.430 +fun not_newline ch = not (ch = "\n");
  10.431 +
  10.432 +fun concat_with_and [] str = str
  10.433 +|   concat_with_and (x::[]) str = str^"("^x^")"
  10.434 +|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
  10.435 +(*
  10.436 +
  10.437 +fun follow clauses [] allvars thml recons = 
  10.438 +                             let (* val _ = reset show_sorts*)
  10.439 +                              val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
  10.440 +                              val thmproofstring = proofstring ( thmstring)
  10.441 +                            val no_returns =List.filter  not_newline ( thmproofstring)
  10.442 +                            val thmstr = implode no_returns
  10.443 +                               val outfile = TextIO.openOut("thml_file")
  10.444 +                               val _ = TextIO.output(outfile, "thmstr is "^thmstr)
  10.445 +                               val _ = TextIO.flushOut outfile;
  10.446 +                               val _ =  TextIO.closeOut outfile
  10.447 +                                 (*val _ = set show_sorts*)
  10.448 +                             in
  10.449 +                                  ((snd( hd thml)), recons)
  10.450 +                             end
  10.451 +      | follow clauses (h::t) allvars thml recons 
  10.452 +        = let
  10.453 +            val (thml', recons') = follow_line clauses allvars  thml h recons
  10.454 +            val  (thm, recons_list) = follow clauses t  allvars thml' recons'
  10.455 +            
  10.456 +
  10.457 +          in
  10.458 +             (thm,recons_list)
  10.459 +          end
  10.460 +
  10.461 +*)
  10.462 +
  10.463 +fun replace_clause_strs [] recons newrecons= (newrecons)
  10.464 +|   replace_clause_strs ((thmnum, thm)::thml)  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
  10.465 +                           let val new_clause_strs = get_meta_lits_bracket thm
  10.466 +                           in
  10.467 +                               replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
  10.468 +                           end
  10.469 +
  10.470 +
  10.471 +fun follow clauses [] allvars thml recons = 
  10.472 +                             let 
  10.473 +                                 val new_recons = replace_clause_strs thml recons []
  10.474 +                             in
  10.475 +                                  ((snd( hd thml)), new_recons)
  10.476 +                             end
  10.477 +
  10.478 + |  follow clauses (h::t) allvars thml recons 
  10.479 +        = let
  10.480 +            val (thml', recons') = follow_line clauses allvars  thml h recons
  10.481 +            val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
  10.482 +          in
  10.483 +             (thm,recons_list)
  10.484 +          end
  10.485 +
  10.486 +
  10.487 +
  10.488 +(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
  10.489 + (* and the proof as a list of the proper datatype *)
  10.490 +(* take the cnf clauses of the goal and the proof from the res. prover *)
  10.491 +(* as a list of type Proofstep and return the thm goal ==> False *)
  10.492 +
  10.493 +fun first_pair (a,b,c) = (a,b);
  10.494 +
  10.495 +fun second_pair (a,b,c) = (b,c);
  10.496 +
  10.497 +fun one_of_three (a,b,c) = a;
  10.498 +fun two_of_three (a,b,c) = b;
  10.499 +fun three_of_three (a,b,c) = c;
  10.500 +
  10.501 +
  10.502 +(* takes original axioms, proof_steps parsed from spass, variables *)
  10.503 +
  10.504 +fun translate_proof clauses proof allvars
  10.505 +        = let val (thm, recons) = follow clauses proof allvars [] []
  10.506 +          in
  10.507 +             (thm, (recons))
  10.508 +          end
  10.509 +  
  10.510 +
  10.511 +
  10.512 +fun remove_tinfo [] = []
  10.513 +|   remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Mar 31 19:29:26 2005 +0200
    11.3 @@ -0,0 +1,729 @@
    11.4 +
    11.5 + (*  Title:      Watcher.ML
    11.6 +     Author:     Claire Quigley
    11.7 +     Copyright   2004  University of Cambridge
    11.8 + *)
    11.9 +
   11.10 + (***************************************************************************)
   11.11 + (*  The watcher process starts a resolution process when it receives a     *)
   11.12 +(*  message from Isabelle                                                  *)
   11.13 +(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
   11.14 +(*  and removes dead processes.  Also possible to kill all the resolution  *)
   11.15 +(*  processes currently running.                                           *)
   11.16 +(*  Hardwired version of where to pick up the tptp files for the moment    *)
   11.17 +(***************************************************************************)
   11.18 +
   11.19 +(*use "Proof_Transfer";
   11.20 +use "VampireCommunication";
   11.21 +use "SpassCommunication";
   11.22 +use "modUnix";*)
   11.23 +(*use "/homes/clq20/Jia_Code/TransStartIsar";*)
   11.24 +
   11.25 +use "~~/VampireCommunication";
   11.26 +use "~~/SpassCommunication";
   11.27 +
   11.28 +
   11.29 +use "~~/modUnix";
   11.30 +
   11.31 +
   11.32 +structure Watcher: WATCHER =
   11.33 +  struct
   11.34 +
   11.35 +fun fst (a,b) = a;
   11.36 +fun snd (a,b) = b;
   11.37 +
   11.38 +val goals_being_watched = ref 0;
   11.39 +
   11.40 +
   11.41 +fun remove y [] = []
   11.42 +|   remove y (x::xs) = (if y = x 
   11.43 +                       then 
   11.44 +                           remove y xs 
   11.45 +                       else ((x::(remove y  xs))))
   11.46 +
   11.47 +
   11.48 +
   11.49 +fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
   11.50 +
   11.51 +(********************************************************************************************)
   11.52 +(*  takes a list of arguments and sends them individually to the watcher process by pipe    *)
   11.53 +(********************************************************************************************)
   11.54 +
   11.55 +fun outputArgs (toWatcherStr, []) = ()
   11.56 +|   outputArgs (toWatcherStr, (x::xs)) = (TextIO.output (toWatcherStr, x); 
   11.57 +                                          TextIO.flushOut toWatcherStr;
   11.58 +                                         outputArgs (toWatcherStr, xs))
   11.59 +
   11.60 +(********************************************************************************)
   11.61 +(*    gets individual args from instream and concatenates them into a list      *)
   11.62 +(********************************************************************************)
   11.63 +
   11.64 +fun getArgs (fromParentStr, toParentStr,ys) =  let 
   11.65 +                                       val thisLine = TextIO.input fromParentStr
   11.66 +                                    in
   11.67 +                                        ((ys@[thisLine]))
   11.68 +                                    end
   11.69 +
   11.70 +(********************************************************************************)
   11.71 +(*  Remove the \n character from the end of each filename                       *)
   11.72 +(********************************************************************************)
   11.73 +
   11.74 +fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   11.75 +                    in
   11.76 +
   11.77 +                        if (String.isPrefix "\n"  (implode backList )) 
   11.78 +                        then 
   11.79 +                             (implode (rev ((tl backList))))
   11.80 +                        else
   11.81 +                           (cmdStr)
   11.82 +                    end
   11.83 +                            
   11.84 +(********************************************************************************)
   11.85 +(*  Send request to Watcher for a vampire to be called for filename in arg      *)
   11.86 +(********************************************************************************)
   11.87 +                    
   11.88 +fun callResProver (toWatcherStr,  arg) = (sendOutput (toWatcherStr, arg^"\n"); 
   11.89 +                                     TextIO.flushOut toWatcherStr
   11.90 +                                    
   11.91 +                                     )
   11.92 +
   11.93 +(*****************************************************************************************)
   11.94 +(*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
   11.95 +(*****************************************************************************************)
   11.96 +
   11.97 +(* need to modify to send over hyps file too *)
   11.98 +fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
   11.99 +                                     TextIO.flushOut toWatcherStr)
  11.100 +|   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
  11.101 +                                                     let 
  11.102 +                                                        val dfg_dir = File.tmp_path (Path.basic "dfg");
  11.103 +                                                        (* need to check here if the directory exists and, if not, create it*)
  11.104 +                                                         val  outfile = TextIO.openAppend(" /thmstring_in_watcher");                                                                                    
  11.105 +                                                         val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
  11.106 +                                                         val _ =  TextIO.closeOut outfile
  11.107 +                                                         val dfg_create =if File.exists dfg_dir 
  11.108 +                                                                         then
  11.109 +                                                                             ()
  11.110 +                                                                         else
  11.111 +                                                                               File.mkdir dfg_dir; 
  11.112 +                                                         val probID = last(explode probfile)
  11.113 +                                                         val dfg_path = File.sysify_path dfg_dir;
  11.114 +                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v2.6.0/TPTP2X/tptp2X", ["-fdfg "^probfile^" -d "^dfg_path])
  11.115 +                                                       (*val _ = Posix.Process.wait ()*)
  11.116 +                                                       (*val _ =Unix.reap exec_tptp2x*)
  11.117 +                                                         val newfile = dfg_path^"/prob"^(probID)^".dfg"
  11.118 +                                       
  11.119 +                                                      in   
  11.120 +                                                         goals_being_watched := (!goals_being_watched) + 1;
  11.121 +                                                         OS.Process.sleep(Time.fromSeconds 1); 
  11.122 +                                                         (warning("dfg file is: "^newfile));
  11.123 +                                                         sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
  11.124 +                                                         TextIO.flushOut toWatcherStr;
  11.125 +                                                         Unix.reap exec_tptp2x; 
  11.126 +                                                         
  11.127 +                                                         callResProvers (toWatcherStr,args)
  11.128 +                                           
  11.129 +                                                     end
  11.130 +
  11.131 +fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
  11.132 +                                     
  11.133 +|   callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings, file)::args) =
  11.134 +                                            ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^file^"\n")
  11.135 +                                            
  11.136 +                                           )
  11.137 + 
  11.138 +(**************************************************************)
  11.139 +(* Send message to watcher to kill currently running vampires *)
  11.140 +(**************************************************************)
  11.141 +
  11.142 +fun callSlayer (toWatcherStr) = (sendOutput (toWatcherStr, "Kill vampires\n"); 
  11.143 +                            TextIO.flushOut toWatcherStr)
  11.144 +
  11.145 +
  11.146 +
  11.147 +(**************************************************************)
  11.148 +(* Remove \n token from a vampire goal filename and extract   *)
  11.149 +(* prover, proverCmd, settings and file from input string     *)
  11.150 +(**************************************************************)
  11.151 +
  11.152 +
  11.153 + fun takeUntil ch [] res  = (res, [])
  11.154 + |   takeUntil ch (x::xs) res = if   x = ch 
  11.155 +                                then
  11.156 +                                     (res, xs)
  11.157 +                                else
  11.158 +                                     takeUntil ch xs (res@[x])
  11.159 +
  11.160 + fun getSettings [] settings = settings
  11.161 +|    getSettings (xs) settings = let val (set, rest ) = takeUntil "%" xs []
  11.162 +                                 in
  11.163 +                                     getSettings rest (settings@[(implode set)])
  11.164 +                                 end
  11.165 +
  11.166 +fun separateFields str = let val (prover, rest) = takeUntil "*" str []
  11.167 +                              val prover = implode prover
  11.168 +                              val (thmstring, rest) =  takeUntil "*" rest []
  11.169 +                              val thmstring = implode thmstring
  11.170 +                              val (goalstring, rest) =  takeUntil "*" rest []
  11.171 +                              val goalstring = implode goalstring
  11.172 +                              val (proverCmd, rest ) =  takeUntil "*" rest []
  11.173 +                              val proverCmd = implode proverCmd
  11.174 +                              
  11.175 +                              val (settings, rest) =  takeUntil "*" rest []
  11.176 +                              val settings = getSettings settings []
  11.177 +                              val (file, rest) =  takeUntil "*" rest []
  11.178 +                              val file = implode file
  11.179 +                              val  outfile = TextIO.openOut("sep_comms");                                                                                    
  11.180 +                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
  11.181 +                              val _ =  TextIO.closeOut outfile
  11.182 +                              
  11.183 +                          in
  11.184 +                             (prover,thmstring,goalstring, proverCmd, settings, file)
  11.185 +                          end
  11.186 +
  11.187 + 
  11.188 +
  11.189 + fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
  11.190 +                     in
  11.191 +
  11.192 +                         if (String.isPrefix "\n"  (implode backList )) 
  11.193 +                         then 
  11.194 +                             separateFields ((rev ((tl backList))))
  11.195 +                         else
  11.196 +                           (separateFields (explode cmdStr))
  11.197 +                     end
  11.198 +                      
  11.199 +
  11.200 +fun getProofCmd (a,b,c,d,e,f) = d
  11.201 +
  11.202 +
  11.203 +(**************************************************************)
  11.204 +(* Get commands from Isabelle                                 *)
  11.205 +(**************************************************************)
  11.206 +
  11.207 +fun getCmds (toParentStr,fromParentStr, cmdList) = 
  11.208 +                                       let val thisLine = TextIO.inputLine fromParentStr 
  11.209 +                                       in
  11.210 +                                          (if (thisLine = "End of calls\n") 
  11.211 +                                           then 
  11.212 +                                              (cmdList)
  11.213 +                                           else if (thisLine = "Kill children\n") 
  11.214 +                                                then 
  11.215 +                                                    (   TextIO.output (toParentStr,thisLine ); 
  11.216 +                                                        TextIO.flushOut toParentStr;
  11.217 +                                                      (("","","","Kill children",[],"")::cmdList)
  11.218 +                                                     )
  11.219 +                                              else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
  11.220 +                                                    in
  11.221 +                                                      (*TextIO.output (toParentStr, thisCmd); 
  11.222 +                                                        TextIO.flushOut toParentStr;*)
  11.223 +                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
  11.224 +                                                    end
  11.225 +                                                    )
  11.226 +                                            )
  11.227 +                                        end
  11.228 +                                    
  11.229 +                                    
  11.230 +(**************************************************************)
  11.231 +(*  Get Io-descriptor for polling of an input stream          *)
  11.232 +(**************************************************************)
  11.233 +
  11.234 +
  11.235 +fun getInIoDesc someInstr = 
  11.236 +    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
  11.237 +        val _ = print (TextIO.stdOut, buf)
  11.238 +        val ioDesc = 
  11.239 +	    case rd
  11.240 +	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
  11.241 +	       | _ => NONE
  11.242 +     in (* since getting the reader will have terminated the stream, we need
  11.243 +	 * to build a new stream. *)
  11.244 +	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
  11.245 +	ioDesc
  11.246 +    end
  11.247 +
  11.248 +
  11.249 +(*************************************)
  11.250 +(*  Set up a Watcher Process         *)
  11.251 +(*************************************)
  11.252 +
  11.253 +
  11.254 +
  11.255 +fun setupWatcher (the_goal) = let
  11.256 +          (** pipes for communication between parent and watcher **)
  11.257 +          val p1 = Posix.IO.pipe ()
  11.258 +          val p2 = Posix.IO.pipe ()
  11.259 +	  fun closep () = (
  11.260 +                Posix.IO.close (#outfd p1); 
  11.261 +                Posix.IO.close (#infd p1);
  11.262 +                Posix.IO.close (#outfd p2); 
  11.263 +                Posix.IO.close (#infd p2)
  11.264 +              )
  11.265 +          (***********************************************************)
  11.266 +          (****** fork a watcher process and get it set up and going *)
  11.267 +          (***********************************************************)
  11.268 +          fun startWatcher (procList) =
  11.269 +                   (case  Posix.Process.fork() (***************************************)
  11.270 +		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
  11.271 +                                               (***************************************)
  11.272 + 
  11.273 +                                                 (*************************)
  11.274 +                  | NONE => let                  (* child - i.e. watcher  *)
  11.275 +		      val oldchildin = #infd p1  (*************************)
  11.276 +		      val fromParent = Posix.FileSys.wordToFD 0w0
  11.277 +		      val oldchildout = #outfd p2
  11.278 +		      val toParent = Posix.FileSys.wordToFD 0w1
  11.279 +                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
  11.280 +                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
  11.281 +                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
  11.282 +                      val goalstr = string_of_thm (the_goal)
  11.283 +                       val  outfile = TextIO.openOut("goal_in_watcher");  
  11.284 +                      val _ = TextIO.output (outfile,goalstr )
  11.285 +                      val _ =  TextIO.closeOut outfile
  11.286 +                      fun killChildren [] = ()
  11.287 +                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
  11.288 +
  11.289 +                     
  11.290 +           
  11.291 +                    (*************************************************************)
  11.292 +                    (* take an instream and poll its underlying reader for input *)
  11.293 +                    (*************************************************************)
  11.294 +
  11.295 +                    fun pollParentInput () = 
  11.296 +                           
  11.297 +                               let val pd = OS.IO.pollDesc (fromParentIOD)
  11.298 +                               in 
  11.299 +                               if (isSome pd ) then 
  11.300 +                                   let val pd' = OS.IO.pollIn (valOf pd)
  11.301 +                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
  11.302 +                                   in
  11.303 +                                      if null pdl 
  11.304 +                                      then
  11.305 +                                         NONE
  11.306 +                                      else if (OS.IO.isIn (hd pdl)) 
  11.307 +                                           then
  11.308 +                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
  11.309 +                                           else
  11.310 +                                               NONE
  11.311 +                                   end
  11.312 +                                 else
  11.313 +                                     NONE
  11.314 +                                 end
  11.315 +                            
  11.316 +                   
  11.317 +
  11.318 +                     fun pollChildInput (fromStr) = 
  11.319 +                           let val iod = getInIoDesc fromStr
  11.320 +                           in 
  11.321 +                           if isSome iod 
  11.322 +                           then 
  11.323 +                               let val pd = OS.IO.pollDesc (valOf iod)
  11.324 +                               in 
  11.325 +                               if (isSome pd ) then 
  11.326 +                                   let val pd' = OS.IO.pollIn (valOf pd)
  11.327 +                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
  11.328 +                                   in
  11.329 +                                      if null pdl 
  11.330 +                                      then
  11.331 +                                         NONE
  11.332 +                                      else if (OS.IO.isIn (hd pdl)) 
  11.333 +                                           then
  11.334 +                                               SOME (getCmd (TextIO.inputLine fromStr))
  11.335 +                                           else
  11.336 +                                               NONE
  11.337 +                                   end
  11.338 +                                 else
  11.339 +                                     NONE
  11.340 +                                 end
  11.341 +                             else 
  11.342 +                                 NONE
  11.343 +                            end
  11.344 +
  11.345 +
  11.346 +                   (****************************************************************************)
  11.347 +                   (* Check all vampire processes currently running for output                 *)
  11.348 +                   (****************************************************************************) 
  11.349 +                                                              (*********************************)
  11.350 +                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
  11.351 +                                                              (*********************************)
  11.352 +                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
  11.353 +                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
  11.354 +                                                val childPid = cmdchildPid childProc
  11.355 +                                                val childCmd = fst(snd (cmdchildInfo childProc))
  11.356 +                                                val childIncoming = pollChildInput childInput
  11.357 +                                                val parentID = Posix.ProcEnv.getppid()
  11.358 +                                                val prover = cmdProver childProc
  11.359 +                                                val thmstring = cmdThm childProc
  11.360 +                                                val goalstring = cmdGoal childProc
  11.361 +                                                val  outfile = TextIO.openOut("child_comms");  
  11.362 +                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
  11.363 +                                                val _ =  TextIO.closeOut outfile
  11.364 +                                            in 
  11.365 +                                              if (isSome childIncoming) 
  11.366 +                                              then 
  11.367 +                                                  (* check here for prover label on child*)
  11.368 +                                                   
  11.369 +                                                  let val  outfile = TextIO.openOut("child_incoming");  
  11.370 +                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
  11.371 +                                                val _ =  TextIO.closeOut outfile
  11.372 +                                              val childDone = (case prover of
  11.373 +                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
  11.374 +                                                   in
  11.375 +                                                    if childDone      (**********************************************)
  11.376 +                                                    then              (* child has found a proof and transferred it *)
  11.377 +                                                                      (**********************************************)
  11.378 +
  11.379 +                                                       (**********************************************)
  11.380 +                                                       (* Remove this child and go on to check others*)
  11.381 +                                                       (**********************************************)
  11.382 +                                                       ( reap(childPid, childInput, childOutput);
  11.383 +                                                         checkChildren(otherChildren, toParentStr))
  11.384 +                                                    else 
  11.385 +                                                       (**********************************************)
  11.386 +                                                       (* Keep this child and go on to check others  *)
  11.387 +                                                       (**********************************************)
  11.388 +
  11.389 +                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
  11.390 +                                                 end
  11.391 +                                               else
  11.392 +                                                   let val  outfile = TextIO.openOut("child_incoming");  
  11.393 +                                                val _ = TextIO.output (outfile,"No child output " )
  11.394 +                                                val _ =  TextIO.closeOut outfile
  11.395 +                                                 in
  11.396 +                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
  11.397 +                                                 end
  11.398 +                                            end
  11.399 +
  11.400 +                   
  11.401 +                (********************************************************************)                  
  11.402 +                (* call resolution processes                                        *)
  11.403 +                (* settings should be a list of strings                             *)
  11.404 +                (* e.g. ["-t 300", "-m 100000"]                                     *)
  11.405 +                (* takes list of (string, string, string list, string)list proclist *)
  11.406 +                (********************************************************************)
  11.407 +
  11.408 +                   fun execCmds  [] procList = procList
  11.409 +                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
  11.410 +                                                     if (prover = "spass") 
  11.411 +                                                     then 
  11.412 +                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
  11.413 +                                                         in
  11.414 +                                                            execCmds cmds newProcList
  11.415 +                                                         end
  11.416 +                                                     else 
  11.417 +                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
  11.418 +                                                         in
  11.419 +                                                            execCmds cmds newProcList
  11.420 +                                                         end
  11.421 +
  11.422 +
  11.423 +                (****************************************)                  
  11.424 +                (* call resolution processes remotely   *)
  11.425 +                (* settings should be a list of strings *)
  11.426 +                (* e.g. ["-t 300", "-m 100000"]         *)
  11.427 +                (****************************************)
  11.428 +  
  11.429 +                   fun execRemoteCmds  [] procList = procList
  11.430 +                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
  11.431 +                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
  11.432 +                                                 in
  11.433 +                                                      execRemoteCmds  cmds newProcList
  11.434 +                                                 end
  11.435 +
  11.436 +
  11.437 +                   fun printList (outStr, []) = ()
  11.438 +                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
  11.439 +
  11.440 +
  11.441 +                (**********************************************)                  
  11.442 +                (* Watcher Loop                               *)
  11.443 +                (**********************************************)
  11.444 +
  11.445 +
  11.446 +
  11.447 +   
  11.448 +                    fun keepWatching (toParentStr, fromParentStr,procList) = 
  11.449 +                          let    fun loop (procList) =  
  11.450 +                                 (
  11.451 +                                 let val cmdsFromIsa = pollParentInput ()
  11.452 +                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
  11.453 +                                                  TextIO.flushOut toParentStr;
  11.454 +                                                   killChildren (map (cmdchildPid) procList);
  11.455 +                                                    ())
  11.456 +                                     
  11.457 +                                 in 
  11.458 +                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
  11.459 +                                                                                       (**********************************)
  11.460 +                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
  11.461 +                                         (                                             (**********************************)                             
  11.462 +                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
  11.463 +                                          then 
  11.464 +                                            (
  11.465 +                                              let val childPids = map cmdchildPid procList 
  11.466 +                                              in
  11.467 +                                                 killChildren childPids;
  11.468 +                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
  11.469 +                                              end
  11.470 +                                             )
  11.471 +                                          else
  11.472 +                                            ( 
  11.473 +                                              if ((length procList)<2)    (********************)
  11.474 +                                              then                        (* Execute locally  *)
  11.475 +                                                 (                        (********************)
  11.476 +                                                  let 
  11.477 +                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
  11.478 +                                                    val parentID = Posix.ProcEnv.getppid()
  11.479 +                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
  11.480 +                                                  in
  11.481 +                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
  11.482 +                                                    loop (newProcList') 
  11.483 +                                                  end
  11.484 +                                                  )
  11.485 +                                              else                         (************************)
  11.486 +                                                                           (* Execute remotely     *)
  11.487 +                                                  (                        (************************)
  11.488 +                                                  let 
  11.489 +                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
  11.490 +                                                    val parentID = Posix.ProcEnv.getppid()
  11.491 +                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
  11.492 +                                                  in
  11.493 +                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
  11.494 +                                                    loop (newProcList') 
  11.495 +                                                  end
  11.496 +                                                  )
  11.497 +
  11.498 +
  11.499 +
  11.500 +                                              )
  11.501 +                                           )                                              (******************************)
  11.502 +                                    else                                                  (* No new input from Isabelle *)
  11.503 +                                                                                          (******************************)
  11.504 +                                        (    let val newProcList = checkChildren ((procList), toParentStr)
  11.505 +                                             in
  11.506 +                                               OS.Process.sleep (Time.fromSeconds 1);
  11.507 +                                               loop (newProcList)
  11.508 +                                             end
  11.509 +                                         
  11.510 +                                         )
  11.511 +                                  end)
  11.512 +                          in  
  11.513 +                              loop (procList)
  11.514 +                          end
  11.515 +                      
  11.516 +          
  11.517 +                      in
  11.518 +                       (***************************)
  11.519 +                       (*** Sort out pipes ********)
  11.520 +                       (***************************)
  11.521 +
  11.522 +			Posix.IO.close (#outfd p1);
  11.523 +			Posix.IO.close (#infd p2);
  11.524 +			Posix.IO.dup2{old = oldchildin, new = fromParent};
  11.525 +                        Posix.IO.close oldchildin;
  11.526 +			Posix.IO.dup2{old = oldchildout, new = toParent};
  11.527 +                        Posix.IO.close oldchildout;
  11.528 +
  11.529 +                        (***************************)
  11.530 +                        (* start the watcher loop  *)
  11.531 +                        (***************************)
  11.532 +                        keepWatching (toParentStr, fromParentStr, procList);
  11.533 +
  11.534 +
  11.535 +                        (****************************************************************************)
  11.536 +                        (* fake return value - actually want the watcher to loop until killed       *)
  11.537 +                        (****************************************************************************)
  11.538 +                        Posix.Process.wordToPid 0w0
  11.539 +			
  11.540 +		      end);
  11.541 +		(* end case *)
  11.542 +
  11.543 +
  11.544 +          val _ = TextIO.flushOut TextIO.stdOut
  11.545 +
  11.546 +          (*******************************)
  11.547 +          (***  set watcher going ********)
  11.548 +          (*******************************)
  11.549 +
  11.550 +          val procList = []
  11.551 +          val pid = startWatcher (procList)
  11.552 +          (**************************************************)
  11.553 +          (* communication streams to watcher               *)
  11.554 +          (**************************************************)
  11.555 +
  11.556 +	  val instr = openInFD ("_exec_in", #infd p2)
  11.557 +          val outstr = openOutFD ("_exec_out", #outfd p1)
  11.558 +          
  11.559 +          in
  11.560 +           (*******************************)
  11.561 +           (* close the child-side fds    *)
  11.562 +           (*******************************)
  11.563 +            Posix.IO.close (#outfd p2);
  11.564 +            Posix.IO.close (#infd p1);
  11.565 +            (* set the fds close on exec *)
  11.566 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
  11.567 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
  11.568 +             
  11.569 +           (*******************************)
  11.570 +           (* return value                *)
  11.571 +           (*******************************)
  11.572 +            PROC{pid = pid,
  11.573 +              instr = instr,
  11.574 +              outstr = outstr
  11.575 +            }
  11.576 +         end;
  11.577 +
  11.578 +
  11.579 +
  11.580 +(**********************************************************)
  11.581 +(* Start a watcher and set up signal handlers             *)
  11.582 +(**********************************************************)
  11.583 +fun killWatcher pid= killChild pid;
  11.584 +
  11.585 +fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
  11.586 +			   val streams =snd mychild
  11.587 +                           val childin = fst streams
  11.588 +                           val childout = snd streams
  11.589 +                           val childpid = fst mychild
  11.590 +                           
  11.591 +                           fun vampire_proofHandler (n:int) =
  11.592 +                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.593 +                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )                   
  11.594 +                          
  11.595 +                          (* fun spass_proofHandler (n:int) = (
  11.596 +                                                      let val (reconstr, thmstring, goalstring) = getSpassInput childin
  11.597 +                                                          val  outfile = TextIO.openOut("foo_signal");
  11.598 +
  11.599 +                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
  11.600 +                                                         val _ =  TextIO.closeOut outfile
  11.601 +                                                      in
  11.602 +                                                         Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.603 +                                                          Pretty.writeln(Pretty.str reconstr) ;
  11.604 +                                                         Pretty.writeln(Pretty.str  (oct_char "361"));
  11.605 +                                                         (*killWatcher childpid;*) () 
  11.606 +                                                      end)*)
  11.607 +
  11.608 +
  11.609 +(*
  11.610 +
  11.611 +fun spass_proofHandler (n:int) = (
  11.612 +                                                      let  val  outfile = TextIO.openOut("foo_signal1");
  11.613 +
  11.614 +                                                         val _ = TextIO.output (outfile, ("In signal handler now\n"))
  11.615 +                                                         val _ =  TextIO.closeOut outfile
  11.616 +                                                          val (reconstr, thmstring, goalstring) = getSpassInput childin
  11.617 +                                                         val  outfile = TextIO.openOut("foo_signal");
  11.618 +
  11.619 +                                                         val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
  11.620 +                                                         val _ =  TextIO.closeOut outfile
  11.621 +                                                       in
  11.622 +                                                        if ( (substring (reconstr, 0,1))= "[")
  11.623 +                                                         then 
  11.624 +
  11.625 +                                                          let val thm = thm_of_string thmstring
  11.626 +                                                              val clauses = make_clauses [thm]
  11.627 +                                                              val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
  11.628 +                                                         
  11.629 +                                                          in
  11.630 +                                                             Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.631 +                                                             apply_res_thm reconstr goalstring;
  11.632 +                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
  11.633 +                                                             killWatcher childpid; () 
  11.634 +                                                          end
  11.635 +                                                       else
  11.636 +                                                           Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.637 +                                                              Pretty.writeln(Pretty.str (goalstring^reconstr));
  11.638 +                                                             Pretty.writeln(Pretty.str  (oct_char "361"));
  11.639 +                                                             (*killWatcher childpid; *) reap (childpid,childin, childout);()   
  11.640 +                                                      end )
  11.641 +*)
  11.642 +
  11.643 +fun spass_proofHandler (n:int) = (
  11.644 +                                 let  val  outfile = TextIO.openOut("foo_signal1");
  11.645 +                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
  11.646 +                                      val _ =  TextIO.closeOut outfile
  11.647 +                                      val (reconstr, thmstring, goalstring) = getSpassInput childin
  11.648 +                                      val  outfile = TextIO.openAppend("foo_signal");
  11.649 +
  11.650 +                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
  11.651 +                                      val _ =  TextIO.closeOut outfile
  11.652 +                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
  11.653 +                                                  if ( (substring (reconstr, 0,1))= "[")
  11.654 +                                                  then 
  11.655 +
  11.656 +                                                            (
  11.657 +                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.658 +                                                                 apply_res_thm reconstr goalstring;
  11.659 +                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
  11.660 +                                                                 
  11.661 +                                                                 goals_being_watched := ((!goals_being_watched) - 1);
  11.662 +                                                         
  11.663 +                                                                 if ((!goals_being_watched) = 0)
  11.664 +                                                                 then 
  11.665 +                                                                    (let val  outfile = TextIO.openOut("foo_reap_found");
  11.666 +                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
  11.667 +                                                                         val _ =  TextIO.closeOut outfile
  11.668 +                                                                     in
  11.669 +                                                                         reap (childpid,childin, childout); ()
  11.670 +                                                                     end)
  11.671 +                                                                 else
  11.672 +                                                                    ()
  11.673 +                                                            )
  11.674 +                                                    (* if there's no proof, but a message from Spass *)
  11.675 +                                                    else if ((substring (reconstr, 0,5))= "SPASS")
  11.676 +                                                         then
  11.677 +                                                                 (
  11.678 +                                                                     goals_being_watched := (!goals_being_watched) -1;
  11.679 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.680 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
  11.681 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
  11.682 +                                                                      if (!goals_being_watched = 0)
  11.683 +                                                                      then 
  11.684 +                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
  11.685 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
  11.686 +                                                                               val _ =  TextIO.closeOut outfile
  11.687 +                                                                           in
  11.688 +                                                                              reap (childpid,childin, childout); ()
  11.689 +                                                                           end )
  11.690 +                                                                      else
  11.691 +                                                                         ()
  11.692 +                                                                )
  11.693 +                                                          (* if proof translation failed *)
  11.694 +                                                          else if ((substring (reconstr, 0,5)) = "Proof")
  11.695 +                                                               then 
  11.696 +                                                                   (
  11.697 +                                                                     goals_being_watched := (!goals_being_watched) -1;
  11.698 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
  11.699 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
  11.700 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
  11.701 +                                                                      if (!goals_being_watched = 0)
  11.702 +                                                                      then 
  11.703 +                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
  11.704 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
  11.705 +                                                                               val _ =  TextIO.closeOut outfile
  11.706 +                                                                           in
  11.707 +                                                                              reap (childpid,childin, childout); ()
  11.708 +                                                                           end )
  11.709 +                                                                      else
  11.710 +                                                                         ()
  11.711 +                                                                )
  11.712 +
  11.713 +
  11.714 +                                                                else  (* add something here ?*)
  11.715 +                                                                   ()
  11.716 +                                                             
  11.717 +                                       end)
  11.718 +
  11.719 +
  11.720 +                        
  11.721 +                       in 
  11.722 +                          Signal.signal (Posix.Signal.usr1, Signal.SIG_HANDLE vampire_proofHandler);
  11.723 +                          Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE spass_proofHandler);
  11.724 +                          (childin, childout, childpid)
  11.725 +
  11.726 +                       end
  11.727 +
  11.728 +
  11.729 +
  11.730 +
  11.731 +
  11.732 +end (* structure Watcher *)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/ATP/watcher.sig	Thu Mar 31 19:29:26 2005 +0200
    12.3 @@ -0,0 +1,51 @@
    12.4 +
    12.5 +(*  Title:      Watcher.ML
    12.6 +    Author:     Claire Quigley
    12.7 +    Copyright   2004  University of Cambridge
    12.8 +*)
    12.9 +
   12.10 +(***************************************************************************)
   12.11 +(*  The watcher process starts a Spass process when it receives a        *)
   12.12 +(*  message from Isabelle                                                  *)
   12.13 +(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
   12.14 +(*  and removes dead processes.  Also possible to kill all the vampire     *)
   12.15 +(*  processes currently running.                                           *)
   12.16 +(***************************************************************************)
   12.17 +
   12.18 +
   12.19 +signature WATCHER =
   12.20 +  sig
   12.21 +
   12.22 +(*****************************************************************************************)
   12.23 +(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
   12.24 +(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
   12.25 +(*****************************************************************************************)
   12.26 +
   12.27 +val callResProvers : TextIO.outstream *(string* string*string *string*string*string) list -> unit
   12.28 +
   12.29 +
   12.30 +
   12.31 +(************************************************************************)
   12.32 +(* Send message to watcher to kill currently running resolution provers *)
   12.33 +(************************************************************************)
   12.34 +
   12.35 +val callSlayer : TextIO.outstream -> unit
   12.36 +
   12.37 +
   12.38 +
   12.39 +(**********************************************************)
   12.40 +(* Start a watcher and set up signal handlers             *)
   12.41 +(**********************************************************)
   12.42 +
   12.43 +val createWatcher : thm  -> TextIO.instream * TextIO.outstream * Posix.Process.pid
   12.44 +
   12.45 +
   12.46 +
   12.47 +(**********************************************************)
   12.48 +(* Kill watcher process                                   *)
   12.49 +(**********************************************************)
   12.50 +
   12.51 +val killWatcher : (Posix.Process.pid) -> unit
   12.52 +
   12.53 +
   12.54 +end