# HG changeset patch
# User quigley
# Date 1125689373 -7200
# Node ID 8e55ad29b690e130e87a526891e5119b2eee1f09
# Parent  12a9393c5d77c543391e66904710b228ff7fa18f
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
recon_transfer_proof.ML to deal with the E theorem prover.

diff -r 12a9393c5d77 -r 8e55ad29b690 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 21:29:33 2005 +0200
@@ -217,6 +217,26 @@
    end
     
 
+fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
+   let 
+     (* not sure why this is necessary again, but seems to be *)
+      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+      val step_nums =get_linenums proofstr
+  
+     (***********************************************)
+     (* here need to add the clauses from clause_arr*)
+     (***********************************************)
+  
+      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
+      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
+  
+      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
+                         (concat clasimp_names)
+      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
+   in
+      clasimp_names
+   end
+
 (***********************************************)
 (* get axioms for reconstruction               *)
 (***********************************************)
@@ -419,6 +439,46 @@
     end;
 
 
+fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
+ let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
+               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
+                "goalstr is: "^goalstring^" num of clauses is: "^
+                (string_of_int num_of_clauses))
+
+    (***********************************)
+    (* get vampire axiom names         *)
+    (***********************************)
+
+     val (axiom_names) = get_axiom_names_E proofstr  thms clause_arr  num_of_clauses
+     val ax_str = "Rules from clasimpset used in proof found by E: " ^
+                  rules_to_string axiom_names
+    in 
+	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
+         TextIO.output (toParent, ax_str^"\n");
+	 TextIO.flushOut toParent;
+	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
+	 TextIO.flushOut toParent;
+	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
+	 TextIO.flushOut toParent;
+
+	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	(* Attempt to prevent several signals from turning up simultaneously *)
+	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
+    end
+    handle _ => 
+    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
+    in 
+	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
+	TextIO.flushOut toParent;
+	 TextIO.output (toParent, thmstring^"\n");
+	 TextIO.flushOut toParent;
+	 TextIO.output (toParent, goalstring^"\n");
+	 TextIO.flushOut toParent;
+	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	(* Attempt to prevent several signals from turning up simultaneously *)
+	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
+    end;
+
 (* val proofstr = "1582[0:Inp] || -> v_P*.\
                  \1583[0:Inp] || v_P* -> .\
 		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
diff -r 12a9393c5d77 -r 8e55ad29b690 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 21:29:33 2005 +0200
@@ -502,7 +502,8 @@
 				("subgoals forked to checkChildren:"^
 				prems_string^prover^thmstring^goalstring^childCmd) 
 			 val childDone = (case prover of
-			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
+			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
+                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
 			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
 		      in
 		       if childDone      (**********************************************)
diff -r 12a9393c5d77 -r 8e55ad29b690 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:55:24 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Sep 02 21:29:33 2005 +0200
@@ -189,13 +189,22 @@
                      optionline, clasimpfile, axfile, hypsfile, probfile)] @ 
                   (make_atp_list xs sign (n+1)))
               end
-            else
+            else if !vampire 
+	    then 
               let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
               in
                 ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
                    clasimpfile, axfile, hypsfile, probfile)] @
                  (make_atp_list xs sign (n+1)))
               end
+      	     else
+             let val Eprover = ResLib.helper_path "E_HOME" "eproof"
+              in
+                ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
+                   clasimpfile, axfile, hypsfile, probfile)] @
+                 (make_atp_list xs sign (n+1)))
+              end
+
           end
 
     val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1