src/HOL/Tools/res_atp.ML
changeset 16357 f1275d2a1dee
parent 16259 aed1a8ae4b23
child 16475 8f3ba52a7937
--- a/src/HOL/Tools/res_atp.ML	Thu Jun 09 23:33:28 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Jun 10 16:15:36 2005 +0200
@@ -31,12 +31,13 @@
 val subgoals = [];
 
 val traceflag = ref true;
+(* used for debug *)
+val debug = ref false;
 
-val debug = ref false;
 fun debug_tac tac = (warning "testing";tac);
-
+(* default value is false *)
+val full_spass = ref false;
 val trace_res = ref false;
-val full_spass = ref false;
 
 val skolem_tac = skolemize_tac;
 
@@ -69,10 +70,13 @@
  
 (**** for Isabelle/ML interface  ****)
 
-fun is_proof_char ch = (ch = " ") orelse
-     ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?"))  
+fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
 
-fun proofstring x = List.filter (is_proof_char) (explode x);
+fun proofstring x = let val exp = explode x 
+                    in
+                        List.filter (is_proof_char ) exp
+                    end
+
 
 
 (*
@@ -130,113 +134,90 @@
         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
 	val out = TextIO.openOut(probfile)
     in
-	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
-	 if !trace_res then (warning probfile) else ())
+	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
     end;
 
 
+
 (*********************************************************************)
 (* call SPASS with settings and problem file for the current subgoal *)
 (* should be modified to allow other provers to be called            *)
 (*********************************************************************)
+(* now passing in list of skolemized thms and list of sgterms to go with them *)
+fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
+   val axfile = (File.platform_path axiom_file)
+    val hypsfile = (File.platform_path hyps_file)
+     val clasimpfile = (File.platform_path clasimp_file)
+    val spass_home = getenv "SPASS_HOME"
+     
+fun make_atp_list [] sign n = []
+|   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
+let 
+	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
+	val thmproofstr = proofstring ( skothmstr)
+	val no_returns =List.filter   not_newline ( thmproofstr)
+	val thmstr = implode no_returns
+	val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
 
-fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  =
-    let val thmstring = Meson.concat_with_and (map string_of_thm thms) 
-	val thm_no = length thms
-	val _ = warning ("number of thms is : "^(string_of_int thm_no))
-	val _ = warning ("thmstring in call_res is: "^thmstring)
-   
-	val goalstr = Sign.string_of_term sign sg_term 
-	val goalproofstring = proofstring goalstr
-	val no_returns =List.filter not_newline ( goalproofstring)
-	val goalstring = implode no_returns
-	val _ = warning ("goalstring in call_res is: "^goalstring)
-   
-	(*val prob_file =File.tmp_path (Path.basic newprobfile); *)
-	(*val _ =( warning ("calling make_clauses "))
-	val clauses = make_clauses thms
-	val _ =( warning ("called make_clauses "))*)
-	(*val _ = tptp_inputs clauses prob_file*)
-	val thmstring = Meson.concat_with_and (map string_of_thm thms) 
-      
-	val goalstr = Sign.string_of_term sign sg_term 
-	val goalproofstring = proofstring goalstr
+	val sgstr = Sign.string_of_term sign sg_term 
+	val goalproofstring = proofstring sgstr
 	val no_returns =List.filter not_newline ( goalproofstring)
 	val goalstring = implode no_returns
-   
-	val thmproofstring = proofstring ( thmstring)
-	val no_returns =List.filter   not_newline ( thmproofstring)
-	val thmstr = implode no_returns
-       
+	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
+
 	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
-	val axfile = (File.platform_path axiom_file)
-	val hypsfile = (File.platform_path hyps_file)
-	val clasimpfile = (File.platform_path clasimp_file)
-	val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile")))
-	val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
-	val _ = TextIO.flushOut outfile;
-	val _ =  TextIO.closeOut outfile
-     in
-	(* without paramodulation *)
-	(warning ("goalstring in call_res_tac is: "^goalstring));
-	(warning ("prob file in cal_res_tac is: "^probfile));
-     (* Watcher.callResProvers(childout,
-     [("spass",thmstr,goalstring,*spass_home*,  
-     "-DocProof", 
-     clasimpfile, axfile, hypsfile, probfile)]);*)
-  if !full_spass 
-  then
-   (Watcher.callResProvers(childout,
-	    [("spass", thmstr, goalstring (*,spass_home*), 
-	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
-	     "-DocProof%-TimeLimit=60", 
-	     clasimpfile, axfile, hypsfile, probfile)]))
-  else	
-   (Watcher.callResProvers(childout,
-	    [("spass", thmstr, goalstring (*,spass_home*), 
-	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
-	     "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
-	     clasimpfile, axfile, hypsfile, probfile)]));
-     
-	(* with paramodulation *)
-	(*Watcher.callResProvers(childout,
-	       [("spass",thmstr,goalstring,spass_home,
-	       "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
-		 prob_path)]); *)
-       (* Watcher.callResProvers(childout,
-	[("spass",thmstr,goalstring,spass_home, 
-	"-DocProof",  prob_path)]);*)
-	dummy_tac
-    end
+	val _ = (warning ("prob file in cal_res_tac is: "^probfile))                                                                           
+in
+ 	if !full_spass 
+  	then
+   		([("spass", thmstr, goalstring (*,spass_home*), 
+	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
+	     	"-DocProof%-TimeLimit=60", 
+	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
+  	else	
+   		([("spass", thmstr, goalstring (*,spass_home*), 
+	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
+	     	"-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
+	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
+end
 
+val thms_goals = ListPair.zip( thms, sg_terms) 
+val atp_list = make_atp_list  thms_goals sign 1
+in
+	Watcher.callResProvers(childout,atp_list);
+        warning("Sent commands to watcher!");
+  	dummy_tac
+ end
+(*
+  val axfile = (File.platform_path axiom_file)
+    val hypsfile = (File.platform_path hyps_file)
+     val clasimpfile = (File.platform_path  clasimp_file)
+    val spass_home = getenv "SPASS_HOME"
+ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1)
+    
+ val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ;
+ val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses);
+Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home,  "-DocProof", clasimpfile, axfile, hypsfile,probfile)]);
+
+Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell",  "", clasimpfile, axfile, hypsfile,probfile)]);
+
+
+*)
 (**********************************************************)
 (* write out the current subgoal as a tptp file, probN,   *)
 (* then call dummy_tac - should be call_res_tac           *)
 (**********************************************************)
 
 
-fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
- (
-   warning("in call_atp_tac_tfrees");
-   tptp_inputs_tfrees (make_clauses thms) n tfrees;
-   call_resolve_tac sign thms sg_term (childin, childout, pid) n;
-   dummy_tac);
-
-fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n st = 
-  let val sign = sign_of_thm st
-      val _ = warning ("in atp_tac_tfrees ")
-      val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
-  in  
-    SELECT_GOAL
-      (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
-       METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term
-                            (childin, childout,pid) ))]) n st
-  end;
-
-
-fun isar_atp_g tfrees sg_term (childin, childout, pid) n =       
-  ((warning("in isar_atp_g"));
-   atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
+fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
+                       if (equal n 0) then 
+				(call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
+			else
+                           
+               		( SELECT_GOAL
+  				(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
+  				 METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
+                                                    get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
 
 
 
@@ -246,24 +227,26 @@
 (* in proof reconstruction                    *)
 (**********************************************)
 
-fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
-      if (k > n) 
-      then () 
-      else 
-	  let val prems = prems_of thm 
-	      val sg_term = ReconOrderClauses.get_nth n prems
-	      val thmstring = string_of_thm thm
-	  in   
-	      (warning("in isar_atp_goal'"));
-	      (warning("thmstring in isar_atp_goal': "^thmstring));
-	       isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
-	       isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
-	  end;
+fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
+                  
+                           (let val  prems = prems_of thm 
+                              (*val sg_term = get_nth k prems*)
+                                val sign = sign_of_thm thm
+                                val thmstring = string_of_thm thm
+                            in   
+                                 
+                		(warning("in isar_atp_goal'"));
+                                (warning("thmstring in isar_atp_goal': "^thmstring));
+ 				(* go and call callResProvers with this subgoal *)
+ 				(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
+ 				(* recursive call to pick up the remaining subgoals *)
+                                (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
+                                get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
+                            end);
 
-
-fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
+(*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
               (if (!debug) then warning (string_of_thm thm) 
-               else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
+               else (isar_atp_goal' thm n_subgoals tfree_lits  (childin, childout, pid) ));*)
 
 (**************************************************)
 (* convert clauses from "assume" to conjecture.   *)
@@ -276,8 +259,9 @@
 
 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
     let val tfree_lits = isar_atp_h thms 
-    in warning("in isar_atp_aux");
-       isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
+    in
+	(warning("in isar_atp_aux"));
+         isar_atp_goal' thm n_subgoals tfree_lits   (childin, childout, pid)
     end;
 
 (******************************************************************)
@@ -287,8 +271,9 @@
 (* turns off xsymbol at start of function, restoring it at end    *)
 (******************************************************************)
 (*FIX changed to clasimp_file *)
-fun isar_atp' (ctxt, thms, thm) =
-    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+fun isar_atp' (ctxt,thms, thm) =
+    let 
+	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
         val _= (warning ("in isar_atp'"))
         val prems  = prems_of thm
         val sign = sign_of_thm thm
@@ -298,12 +283,11 @@
         
 	(* set up variables for writing out the clasimps to a tptp file *)
 	val (clause_arr, num_of_clauses) =
-	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
+	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
 	                                 (ProofContext.theory_of ctxt)
-        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file)
+        val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
 
         (* cq: add write out clasimps to file *)
-
         (* cq:create watcher and pass to isar_atp_aux *)
         (* tracing *) 
         (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
@@ -324,7 +308,7 @@
                            (warning ("subgoals: "^prems_string));
                            (warning ("pid: "^ pidstring))); 
                             isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
-                           
+                           (warning("turning xsymbol back on!"));
                            print_mode := (["xsymbols", "symbols"] @ ! print_mode)
     end;
 
@@ -343,6 +327,8 @@
 	safeEs @ safeIs @ hazEs @ hazIs
     end;
 
+
+
 fun append_name name [] _ = []
   | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
 
@@ -352,6 +338,7 @@
 	thms'::(append_names names thmss)
     end;
 
+
 fun get_thms_ss [] = []
   | get_thms_ss thms =
     let val names = map Thm.name_of_thm thms 
@@ -361,6 +348,9 @@
 	ResLib.flat_noDup thms''
     end;
 
+
+
+
 in
 
 
@@ -369,7 +359,7 @@
 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
 (*claset file and prob file*)
-(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
+(* FIX*)
 (*fun isar_local_thms (delta_cs, delta_ss_thms) =
     let val thms_cs = get_thms_cs delta_cs
 	val thms_ss = get_thms_ss delta_ss_thms
@@ -383,6 +373,8 @@
 *)
 
 
+
+
 (* called in Isar automatically *)
 
 fun isar_atp (ctxt,thm) =
@@ -398,13 +390,15 @@
           (warning ("initial thm in isar_atp: "^thmstring));
           (warning ("subgoals in isar_atp: "^prems_string));
     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
-          ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
-           isar_atp' (ctxt, prems, thm))
+          (*isar_local_thms (d_cs,d_ss_thms);*)
+           isar_atp' (ctxt,prems, thm)
     end;
 
 end
 
 
+
+
 end;
 
 Proof.atp_hook := ResAtp.isar_atp;