All subgoals sent to the watcher at once now.
authorquigley
Fri Jun 10 16:15:36 2005 +0200 (2005-06-10)
changeset 16357f1275d2a1dee
parent 16356 94011cf701a4
child 16358 2e2a506553a3
All subgoals sent to the watcher at once now.
Rules added to parser for Spass proofs.
If parsing or translation fails on a proof, the Spass proof is printed out in PG.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Jun 09 23:33:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Fri Jun 10 16:15:36 2005 +0200
     1.3 @@ -221,7 +221,8 @@
     1.4  fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
     1.5                            then
     1.6                                 let val thisLine = TextIO.inputLine instr 
     1.7 -                                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
     1.8 +                                   val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
     1.9 +
    1.10                                               
    1.11                                     val _ =  TextIO.closeOut outfile
    1.12  			       in 
    1.13 @@ -256,7 +257,7 @@
    1.14                                               end
    1.15                                            )
    1.16  
    1.17 -                                         else if (thisLine = "Proof found but translation failed!")
    1.18 +                                         else if ((substring (thisLine, 0,5)) = "Proof") 
    1.19                                                then
    1.20    						(
    1.21  						   let val reconstr = thisLine
     2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Jun 09 23:33:28 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 10 16:15:36 2005 +0200
     2.3 @@ -212,6 +212,21 @@
     2.4                     ++ term_num
     2.5              >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
     2.6        
     2.7 +      val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
     2.8 +                   ++ term_num ++ (a (Other ","))
     2.9 +                   ++ term_num
    2.10 +            >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
    2.11 +
    2.12 +
    2.13 +      val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
    2.14 +                   ++ term_num ++ (a (Other ","))
    2.15 +                   ++ term_num
    2.16 +            >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
    2.17 +
    2.18 +
    2.19 +      val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
    2.20 +                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
    2.21 +
    2.22        val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
    2.23                      ++ term_num ++ (a (Other ",")) 
    2.24                      ++ term_num
    2.25 @@ -223,10 +238,27 @@
    2.26                     ++ term_num
    2.27              >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
    2.28  
    2.29 +      val ssi = (a (Word "SSi")) ++ (a (Other ":"))
    2.30 +                   ++ term_num ++ (a (Other ","))
    2.31 +                   ++ term_num
    2.32 +            >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
    2.33 +
    2.34 +    val unc = (a (Word "UnC")) ++ (a (Other ":"))
    2.35 +                   ++ term_num ++ (a (Other ","))
    2.36 +                   ++ term_num
    2.37 +            >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
    2.38 +
    2.39 +
    2.40  
    2.41        val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
    2.42                   >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
    2.43 -     
    2.44 +
    2.45 +      val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
    2.46 +                 >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
    2.47 +   
    2.48 +      val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
    2.49 +                 >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
    2.50 +
    2.51  (*
    2.52        val hyper = a (Word "hyper")
    2.53                    ++ many ((a (Other ",") ++ number) >> snd)
    2.54 @@ -234,7 +266,8 @@
    2.55  *)
    2.56       (* val method = axiom ||binary || factor || para || hyper*)
    2.57  
    2.58 -      val method = axiom || binary || factor || para || rewrite || mrr || obv
    2.59 +      val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
    2.60 +
    2.61        val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
    2.62              >> (fn (_, (_, a)) => Binary_s a)
    2.63        val factor_s = a (Word "factor_s")
    2.64 @@ -316,7 +349,9 @@
    2.65          || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
    2.66             >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
    2.67  
    2.68 -        || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
    2.69 +        || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
    2.70 +
    2.71 +        || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input
    2.72  
    2.73  and  nterm input =
    2.74      
    2.75 @@ -338,7 +373,9 @@
    2.76          || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
    2.77             >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
    2.78  
    2.79 -        || word >> (fn w =>  (remove_typeinfo w)) ) input 
    2.80 +        || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
    2.81 +        || word                  >> (fn w =>  (remove_typeinfo w)) 
    2.82 +         ) input 
    2.83  
    2.84  
    2.85  and peqterm input =(
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Jun 09 23:33:28 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Jun 10 16:15:36 2005 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4  
     3.5  structure Recon_Transfer =
     3.6  struct
     3.7 -
     3.8  open Recon_Parse
     3.9  infixr 8 ++; infixr 7 >>; infixr 6 ||;
    3.10  
    3.11 @@ -210,7 +209,10 @@
    3.12      end
    3.13  
    3.14  
    3.15 -(* add array and table here, so can retrieve clasimp axioms *)
    3.16 +
    3.17 +(*****************************************************)
    3.18 +(* get names of clasimp axioms used                  *)
    3.19 +(*****************************************************)
    3.20  
    3.21   fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    3.22     let 
    3.23 @@ -233,6 +235,33 @@
    3.24        clasimp_names
    3.25     end
    3.26      
    3.27 + fun get_axiom_names_vamp proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
    3.28 +   let 
    3.29 +     (* not sure why this is necessary again, but seems to be *)
    3.30 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    3.31 +      val axioms = get_init_axioms proof_steps
    3.32 +      val step_nums = get_step_nums axioms []
    3.33 +  
    3.34 +     (***********************************************)
    3.35 +     (* here need to add the clauses from clause_arr*)
    3.36 +     (***********************************************)
    3.37 +  
    3.38 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    3.39 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    3.40 +  
    3.41 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    3.42 +                         (concat clasimp_names)
    3.43 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    3.44 +   in
    3.45 +      clasimp_names
    3.46 +   end
    3.47 +    
    3.48 +
    3.49 +
    3.50 +
    3.51 +(***********************************************)
    3.52 +(* get axioms for reconstruction               *)
    3.53 +(***********************************************)
    3.54  fun numclstr (vars, []) str = str
    3.55  |   numclstr ( vars, ((num, thm)::rest)) str =
    3.56        let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    3.57 @@ -343,18 +372,53 @@
    3.58  val dummy_tac = PRIMITIVE(fn thm => thm );
    3.59  
    3.60  
    3.61 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    3.62 -           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    3.63 -                                                  val _ =  TextIO.closeOut outfile
    3.64 +(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
    3.65 +\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
    3.66 +\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
    3.67 +\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
    3.68 +\1454[0:Obv:1453.0] ||  -> .";*)
    3.69 +
    3.70 +fun remove_linebreaks str = let val strlist = explode str
    3.71 +	                        val nonewlines = filter (not_equal "\n") strlist
    3.72 +	                    in
    3.73 +				implode nonewlines
    3.74 +			    end
    3.75 +
    3.76 +
    3.77 +fun subst_for a b [] = ""
    3.78 +|   subst_for a b (x::xs) = if (x = a)
    3.79 +				   then 
    3.80 +					(b^(subst_for a b  xs))
    3.81 +				   else
    3.82 +					x^(subst_for a b xs)
    3.83 +
    3.84  
    3.85 -                                              (***********************************)
    3.86 -                                              (* parse spass proof into datatype *)
    3.87 -                                              (***********************************)
    3.88 +fun remove_linebreaks str = let val strlist = explode str
    3.89 +			    in
    3.90 +				subst_for "\n" "\t" strlist
    3.91 +			    end
    3.92 +
    3.93 +fun restore_linebreaks str = let val strlist = explode str
    3.94 +			     in
    3.95 +				subst_for "\t" "\n" strlist
    3.96 +			     end
    3.97 +
    3.98 +
    3.99 +
   3.100 +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   3.101 +           let 	val  outfile = TextIO.openAppend( File.platform_path(File.tmp_path (Path.basic"thmstringfile")));          
   3.102 +		val _ = TextIO.output (outfile, ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses)))
   3.103 +
   3.104 +              	val _ =  TextIO.closeOut outfile
   3.105 +
   3.106 +                 (***********************************)
   3.107 +                 (* parse spass proof into datatype *)
   3.108 +                 (***********************************)
   3.109           
   3.110 -                                                  val tokens = #1(lex proofstr)
   3.111 -                                                  val proof_steps1 = parse tokens
   3.112 -                                                  val proof_steps = just_change_space proof_steps1
   3.113 -                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   3.114 +                  val tokens = #1(lex proofstr)
   3.115 +                  val proof_steps1 = parse tokens
   3.116 +                  val proof_steps = just_change_space proof_steps1
   3.117 +                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));        val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   3.118                                                    val _ =  TextIO.closeOut outfile
   3.119                                                  
   3.120                                                    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   3.121 @@ -391,7 +455,7 @@
   3.122                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   3.123                                                    val _ =  TextIO.closeOut outfile
   3.124                                                in 
   3.125 -                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   3.126 +                                                 TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr) ^"\n");
   3.127                                                    TextIO.flushOut toParent;
   3.128  						   TextIO.output (toParent, thmstring^"\n");
   3.129                                           	   TextIO.flushOut toParent;
   3.130 @@ -403,6 +467,71 @@
   3.131                                                end)
   3.132  
   3.133  
   3.134 +(*fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   3.135 +           let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
   3.136 +                                                  val _ =  TextIO.closeOut outfile
   3.137 +
   3.138 +                                              (***********************************)
   3.139 +                                              (* parse spass proof into datatype *)
   3.140 +                                              (***********************************)
   3.141 +         
   3.142 +                                                  val tokens = #1(lex proofstr)
   3.143 +                                                  val proof_steps = VampParse.parse tokens
   3.144 +                                                  (*val proof_steps = just_change_space proof_steps1*)
   3.145 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   3.146 +                                                  val _ =  TextIO.closeOut outfile
   3.147 +                                                
   3.148 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   3.149 +                                                  val _ =  TextIO.closeOut outfile
   3.150 +                                              (************************************)
   3.151 +                                              (* recreate original subgoal as thm *)
   3.152 +                                              (************************************)
   3.153 +                                                
   3.154 +                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   3.155 +                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   3.156 +                                                  (* subgoal this is, and turn it into meta_clauses *)
   3.157 +                                                  (* should prob add array and table here, so that we can get axioms*)
   3.158 +                                                  (* produced from the clasimpset rather than the problem *)
   3.159 +
   3.160 +                                                  val (axiom_names) = get_axiom_names_vamp proof_steps  thms clause_arr  num_of_clauses
   3.161 +                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   3.162 +                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   3.163 +                                                  val _ =  TextIO.closeOut outfile
   3.164 +                                                   
   3.165 +                                              in 
   3.166 +                                                   TextIO.output (toParent, ax_str^"\n");
   3.167 +                                                   TextIO.flushOut toParent;
   3.168 +                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   3.169 +                                         	   TextIO.flushOut toParent;fdsa
   3.170 +                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   3.171 +                                         	   TextIO.flushOut toParent;
   3.172 +                                          
   3.173 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.174 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.175 +                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   3.176 +                                              end
   3.177 +                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   3.178 +
   3.179 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   3.180 +                                                  val _ =  TextIO.closeOut outfile
   3.181 +                                              in 
   3.182 +                                                  TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^(remove_linebreaks proofstr) ^"\n");
   3.183 +                                                  TextIO.flushOut toParent;
   3.184 +						   TextIO.output (toParent, thmstring^"\n");
   3.185 +                                         	   TextIO.flushOut toParent;
   3.186 +                                         	   TextIO.output (toParent, goalstring^"\n");
   3.187 +                                         	   TextIO.flushOut toParent;
   3.188 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.189 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.190 +                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   3.191 +                                              end)
   3.192 +*)
   3.193 +
   3.194 +
   3.195 +
   3.196 +(* val proofstr = "1582[0:Inp] || -> v_P*.\
   3.197 +                 \1583[0:Inp] || v_P* -> .\
   3.198 +		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
   3.199  
   3.200  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   3.201        let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   3.202 @@ -490,7 +619,7 @@
   3.203  	  val _ = TextIO.output (outfile, ("In exception handler"));
   3.204  	  val _ =  TextIO.closeOut outfile
   3.205        in 
   3.206 -	  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   3.207 +	   TextIO.output (toParent,"Proof found but translation failed for resolution proof: \n"^proofstr ^"\n");
   3.208  	  TextIO.flushOut toParent;
   3.209  	TextIO.output (toParent, thmstring^"\n");
   3.210  	   TextIO.flushOut toParent;
   3.211 @@ -742,12 +871,16 @@
   3.212  
   3.213  
   3.214  fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n"
   3.215 -
   3.216 +(*FIX: ask Larry to add and mrr attribute *)
   3.217  
   3.218  fun by_isar_line ((Binary ((a,b), (c,d)))) = 
   3.219      "by(rule cl"^
   3.220  		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   3.221  		(string_of_int c)^" "^(string_of_int d)^"])\n"
   3.222 +|by_isar_line ((MRR ((a,b), (c,d)))) = 
   3.223 +    "by(rule cl"^
   3.224 +		(string_of_int a)^" [binary "^(string_of_int b)^" cl"^
   3.225 +		(string_of_int c)^" "^(string_of_int d)^"])\n"
   3.226  |   by_isar_line ( (Para ((a,b), (c,d)))) =
   3.227      "by (rule cl"^
   3.228  		(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^
   3.229 @@ -826,7 +959,8 @@
   3.230  *)
   3.231  
   3.232  fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
   3.233 -
   3.234 +				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
   3.235 +			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   3.236                                     val (frees,recon_steps) = parse_step tokens 
   3.237                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   3.238                                     val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   3.239 @@ -835,6 +969,6 @@
   3.240                                 end 
   3.241  
   3.242  
   3.243 -
   3.244 -
   3.245 +(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
   3.246 +*)
   3.247  end;
     4.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Jun 09 23:33:28 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 10 16:15:36 2005 +0200
     4.3 @@ -35,8 +35,15 @@
     4.4                       | MRR of (int * int) * (int * int) 
     4.5                       | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
     4.6                       | Para of (int * int) * (int * int) 
     4.7 +		     | Super_l of (int * int) * (int * int)
     4.8 +		     | Super_r of (int * int) * (int * int)
     4.9                       | Rewrite of (int * int) * (int * int)  
    4.10 +		     | SortSimp of (int * int) * (int * int)  
    4.11 +		     | UnitConf of (int * int) * (int * int)  
    4.12                       | Obvious of (int * int)
    4.13 +  		     | AED of (int*int)
    4.14 +  		     | EqualRes of (int*int)
    4.15 +    		     | Condense of (int*int)
    4.16                       (*| Hyper of int list*)
    4.17                       | Unusedstep of unit
    4.18  
     5.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Jun 09 23:33:28 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Jun 10 16:15:36 2005 +0200
     5.3 @@ -8,6 +8,7 @@
     5.4  signature RES_CLASIMP = 
     5.5    sig
     5.6       val write_out_clasimp :string -> theory -> (ResClause.clause * thm) Array.array * int
     5.7 +val write_out_clasimp_small :string -> theory -> (ResClause.clause * thm) Array.array * int
     5.8    end;
     5.9  
    5.10  structure ResClasimp : RES_CLASIMP =
    5.11 @@ -112,6 +113,53 @@
    5.12  	(clause_arr, num_of_clauses)
    5.13    end;
    5.14  
    5.15 +
    5.16 +
    5.17 +
    5.18 +
    5.19 +(*Write out the claset and simpset rules of the supplied theory. Only include the first 50 rules*)
    5.20 +fun write_out_clasimp_small filename thy = 
    5.21 +    let val claset_rules = ResAxioms.claset_rules_of_thy thy;
    5.22 +	val named_claset = List.filter has_name_pair claset_rules;
    5.23 +	val claset_names = map remove_spaces_pair (named_claset)
    5.24 +	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    5.25 +
    5.26 +	val simpset_rules = ResAxioms.simpset_rules_of_thy thy;
    5.27 +	val named_simpset = 
    5.28 +	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    5.29 +	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    5.30 +
    5.31 +	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    5.32 +	val cls_thms_list = List.concat cls_thms;
    5.33 +        (* length 1429 *)
    5.34 +	(*************************************************)
    5.35 +	(* Write out clauses as tptp strings to filename *)
    5.36 +	(*************************************************)
    5.37 +	val clauses = map #1(cls_thms_list);
    5.38 +	val cls_tptp_strs = map ResClause.tptp_clause clauses;
    5.39 +        val alllist = pairup cls_thms_list cls_tptp_strs
    5.40 +        val whole_list = List.concat (map clause_numbering alllist);
    5.41 +        val mini_list = List.take ( whole_list,50)
    5.42 +        (*********************************************************)
    5.43 +	(* create array and put clausename, number pairs into it *)
    5.44 +	(*********************************************************)
    5.45 +	val num_of_clauses =  0;
    5.46 +	val clause_arr = Array.fromList mini_list;
    5.47 +	val num_of_clauses = List.length mini_list;
    5.48 +
    5.49 +	(* list of lists of tptp string clauses *)
    5.50 +	val stick_clasrls =   List.concat cls_tptp_strs;
    5.51 +        (* length 1581*)
    5.52 +	val out = TextIO.openOut filename;
    5.53 +	val _=   ResLib.writeln_strs out (List.take (stick_clasrls,50));
    5.54 +	val _= TextIO.flushOut out;
    5.55 +	val _= TextIO.closeOut out
    5.56 +  in
    5.57 +	(clause_arr, num_of_clauses)
    5.58 +  end;
    5.59 +
    5.60 +
    5.61 +
    5.62  end;
    5.63  
    5.64  
     6.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Jun 09 23:33:28 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Jun 10 16:15:36 2005 +0200
     6.3 @@ -150,60 +150,27 @@
     6.4                                       TextIO.flushOut toWatcherStr)
     6.5  
     6.6  (*****************************************************************************************)
     6.7 -(*  Send request to Watcher for multiple provers to be called for filenames in arg      *)
     6.8 +(*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
     6.9 +(*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
    6.10  (*****************************************************************************************)
    6.11  
    6.12 +    
    6.13  (* need to modify to send over hyps file too *)
    6.14 -fun callResProvers (toWatcherStr,  []) =
    6.15 -      (sendOutput (toWatcherStr, "End of calls\n"); 
    6.16 -       TextIO.flushOut toWatcherStr)
    6.17 +fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
    6.18 +                                     TextIO.flushOut toWatcherStr)
    6.19  |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
    6.20 -      let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    6.21 -	 (*** need to check here if the directory exists and, if not, create it***)
    6.22 -	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
    6.23 -	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
    6.24 -	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    6.25 -	 val probID = ReconOrderClauses.last(explode probfile)
    6.26 -	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    6.27 -	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    6.28 -
    6.29 -	  (*** hyps/local axioms just now (*,axfile, hypsfile,*)                                               ***)
    6.30 -	  val whole_prob_file = system ("cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ File.shell_path wholefile)
    6.31 +                                          let  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "tog_comms")));                                                                                    
    6.32 +                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^settings^clasimpfile^hypsfile^probfile) )
    6.33 +                              val _ =  TextIO.closeOut outfile
    6.34 +                                        in   (sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^
    6.35 +							             settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n"));
    6.36 +                                          goals_being_watched := (!goals_being_watched) + 1;
    6.37 +                                          TextIO.flushOut toWatcherStr;
    6.38 +					  
    6.39 +                                          callResProvers (toWatcherStr,args))
    6.40 +                                        end   
    6.41 +                                                
    6.42  
    6.43 -	  val dfg_create = if File.exists dfg_dir 
    6.44 -			   then warning("dfg dir exists")
    6.45 -			   else File.mkdir dfg_dir; 
    6.46 -	  
    6.47 -	  val dfg_path = File.platform_path dfg_dir;
    6.48 -	 (* val exec_tptp2x = 
    6.49 -	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
    6.50 -	                     ["-fdfg", "-d " ^ dfg_path, File.platform_path wholefile]) *)
    6.51 -        val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X"
    6.52 -       
    6.53 -        val systemcall = system (tptp_home ^ " -fdfg -d " ^ File.shell_path dfg_dir ^ " " ^ File.shell_path wholefile)
    6.54 -        val _ =  warning("systemcall is "^ (string_of_int systemcall))
    6.55 -	(*val _ = Posix.Process.wait ()*)
    6.56 -	(*val _ =Unix.reap exec_tptp2x*)
    6.57 -	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    6.58 - 
    6.59 -       in   
    6.60 -	  goals_being_watched := (!goals_being_watched) + 1;
    6.61 -	  Posix.Process.sleep(Time.fromSeconds 1); 
    6.62 -	  (warning ("probfile is: "^probfile));
    6.63 -	  (warning("dfg file is: "^newfile));
    6.64 -	  (warning ("wholefile is: "^(File.platform_path wholefile)));
    6.65 -	  sendOutput (toWatcherStr,
    6.66 -	       prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ 
    6.67 -	       "*" ^ settings ^ "*" ^ newfile ^ "\n");
    6.68 - (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    6.69 -	  TextIO.flushOut toWatcherStr;
    6.70 -	  (*Unix.reap exec_tptp2x;*)
    6.71 -	  if File.exists
    6.72 -	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
    6.73 -	  then callResProvers (toWatcherStr, args)
    6.74 -	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
    6.75 -	              " -fdfg " ^ File.platform_path wholefile ^ " -d " ^ dfg_path)
    6.76 -      end
    6.77  (*
    6.78  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    6.79                                       
    6.80 @@ -240,69 +207,155 @@
    6.81                                       getSettings rest (settings@[(implode set)])
    6.82                                   end
    6.83  
    6.84 -fun separateFields str =
    6.85 -  let val (prover, rest) = takeUntil "*" str []
    6.86 -      val prover = implode prover
    6.87 -      val (thmstring, rest) =  takeUntil "*" rest []
    6.88 -      val thmstring = implode thmstring
    6.89 -      val (goalstring, rest) =  takeUntil "*" rest []
    6.90 -      val goalstring = implode goalstring
    6.91 -      val (proverCmd, rest ) =  takeUntil "*" rest []
    6.92 -      val proverCmd = implode proverCmd
    6.93 -      
    6.94 -      val (settings, rest) =  takeUntil "*" rest []
    6.95 -      val settings = getSettings settings []
    6.96 -      val (file, rest) =  takeUntil "*" rest []
    6.97 -      val file = implode file
    6.98 -      val _ = File.write (File.tmp_path (Path.basic "sep_comms"))
    6.99 -                (prover^thmstring^goalstring^proverCmd^file) 
   6.100 -  in
   6.101 -     (prover,thmstring,goalstring, proverCmd, settings, file)
   6.102 -  end
   6.103 +fun separateFields str = let val  outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field")))                                                                         
   6.104 +                              val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") )
   6.105 +                              val _ =  TextIO.closeOut outfile
   6.106 +                              val (prover, rest) = takeUntil "*" str []
   6.107 +                              val prover = implode prover
   6.108 +
   6.109 +                              val (thmstring, rest) =  takeUntil "*" rest []
   6.110 +                              val thmstring = implode thmstring
   6.111 +
   6.112 +                              val (goalstring, rest) =  takeUntil "*" rest []
   6.113 +                              val goalstring = implode goalstring
   6.114 +
   6.115 +                              val (proverCmd, rest ) =  takeUntil "*" rest []
   6.116 +                              val proverCmd = implode proverCmd
   6.117 +                              
   6.118 +                              val (settings, rest) =  takeUntil "*" rest []
   6.119 +                              val settings = getSettings settings []
   6.120 +
   6.121 +			      val (clasimpfile, rest ) =  takeUntil "*" rest []
   6.122 +                              val clasimpfile = implode clasimpfile
   6.123 +                              
   6.124 +  			      val (hypsfile, rest ) =  takeUntil "*" rest []
   6.125 +                              val hypsfile = implode hypsfile
   6.126 +
   6.127 +                              val (file, rest) =  takeUntil "*" rest []
   6.128 +                              val file = implode file
   6.129 +
   6.130 +                              val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
   6.131 +                              val _ = TextIO.output (outfile,("Sep comms are: "^(implode str)^"**"^prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n") )
   6.132 +                              val _ =  TextIO.closeOut outfile
   6.133 +                              
   6.134 +                          in
   6.135 +                             (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file)
   6.136 +                          end
   6.137  
   6.138   
   6.139 +                      
   6.140 +(***********************************************************************************)
   6.141 +(* do tptp2x and cat to turn clasimpfile, hypsfile and probfile into one .dfg file *)
   6.142 +(***********************************************************************************)
   6.143 +
   6.144 +fun formatCmd (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile ,probfile) = 
   6.145 + let
   6.146 +		val dfg_dir = File.tmp_path (Path.basic "dfg"); 
   6.147 +
   6.148 +  		(*** need to check here if the directory exists and, if not, create it***)
   6.149 +  		
   6.150 +
   6.151 + 		(*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
   6.152 +		val probID = List.last(explode probfile)
   6.153 +    		val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
   6.154 +
   6.155 +    		(*** only include problem and clasimp for the moment, not sure how to refer to ***)
   6.156 +   		(*** hyps/local axioms just now                                                ***)
   6.157 +   		val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
   6.158 +    		val dfg_create =
   6.159 + 		if File.exists dfg_dir 
   6.160 +     	        then
   6.161 +     	            ((warning("dfg dir exists"));())
   6.162 + 		else
   6.163 + 		     File.mkdir dfg_dir; 
   6.164 +   		val dfg_path = File.platform_path dfg_dir;
   6.165 +   		
   6.166 +   		val bar = system ("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X -fdfg "^
   6.167 +                                 (File.platform_path wholefile)^" -d "^dfg_path)
   6.168 +    		val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
   6.169 +                val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"thmstring_in_watcher")));   
   6.170 +   		val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n"))
   6.171 + 		val _ =  TextIO.closeOut outfile
   6.172 +
   6.173 + 	     in
   6.174 + 		(prover,thmstring,goalstring, proverCmd, settings,newfile)	
   6.175 +	     end;
   6.176 +
   6.177 +
   6.178 +(* remove \n from end of command and put back into tuple format *)
   6.179 +             
   6.180 +
   6.181 +(*  val cmdStr = "spass*((ALL xa. (~ P x | P xa) & (~ P xa | P x)) & (P xa | (ALL x. P x)) & ((ALL x. ~ P x) | ~ P xb) [.])*(EX x. ALL y. P x = P y) --> (EX x. P x) = (ALL y. P y)*/homes/clq20/bin/SPASS*-DocProof*/local/scratch/clq20/27023/clasimp*/local/scratch/clq20/27023/hyps*/local/scratch/clq20/27023/prob_1\n" *)
   6.182 +
   6.183 +(*FIX:  are the two getCmd procs getting confused?  Why do I have two anyway? *)
   6.184  
   6.185   fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) 
   6.186 +                         val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic"cmdStr")));   
   6.187 +   		val _ = TextIO.output (outfile, (cmdStr))
   6.188 + 		val _ =  TextIO.closeOut outfile
   6.189                       in
   6.190  
   6.191                           if (String.isPrefix "\n"  (implode backList )) 
   6.192                           then 
   6.193 -                             separateFields ((rev ((tl backList))))
   6.194 +                            ( let 
   6.195 +              val newCmdStr = (rev(tl backList))
   6.196 +              val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic"backlist")));   
   6.197 +   		val _ = TextIO.output (outfile, ("about to call sepfields with "^(implode newCmdStr)))
   6.198 + 		val _ =  TextIO.closeOut outfile 
   6.199 +				 val cmdtuple = separateFields newCmdStr
   6.200 +                             in 
   6.201 + 				 formatCmd cmdtuple
   6.202 +			     end)
   6.203                           else
   6.204 -                           (separateFields (explode cmdStr))
   6.205 +                          ( let 
   6.206 +			      val cmdtuple =(separateFields (explode cmdStr))
   6.207 +			   in
   6.208 + 				formatCmd cmdtuple
   6.209 +			   end)
   6.210 +			   
   6.211                       end
   6.212                        
   6.213  
   6.214  fun getProofCmd (a,b,c,d,e,f) = d
   6.215  
   6.216 -
   6.217 +                        
   6.218  (**************************************************************)
   6.219  (* Get commands from Isabelle                                 *)
   6.220  (**************************************************************)
   6.221 +(* FIX: or perhaps do the tptp2x stuff here - so it's get commands and then format them, before passing them to spass *)
   6.222  
   6.223  fun getCmds (toParentStr,fromParentStr, cmdList) = 
   6.224 -       let val thisLine = TextIO.inputLine fromParentStr 
   6.225 -       in
   6.226 -	  (if (thisLine = "End of calls\n") 
   6.227 -	   then 
   6.228 -	      (cmdList)
   6.229 -	   else if (thisLine = "Kill children\n") 
   6.230 -		then 
   6.231 -		    (   TextIO.output (toParentStr,thisLine ); 
   6.232 -			TextIO.flushOut toParentStr;
   6.233 -		      (("","","","Kill children",[],"")::cmdList)
   6.234 -		     )
   6.235 -	      else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   6.236 -		    in
   6.237 -		      (*TextIO.output (toParentStr, thisCmd); 
   6.238 -			TextIO.flushOut toParentStr;*)
   6.239 -			getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   6.240 -		    end
   6.241 -		    )
   6.242 -	    )
   6.243 -	end
   6.244 +                                       let val thisLine = TextIO.inputLine fromParentStr 
   6.245 +                                           val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "parent_comms")));                                                                                    
   6.246 +                              val _ = TextIO.output (outfile,(thisLine) )
   6.247 +                              val _ =  TextIO.closeOut outfile
   6.248 +                                       in
   6.249 +                                          (if (thisLine = "End of calls\n") 
   6.250 +                                           then 
   6.251 + 					      
   6.252 +                                              (cmdList)
   6.253 + 					      
   6.254 +                                           else if (thisLine = "Kill children\n") 
   6.255 +                                                then 
   6.256 +                                                    (   TextIO.output (toParentStr,thisLine ); 
   6.257 +                                                        TextIO.flushOut toParentStr;
   6.258 +                                                      (("","","","Kill children",[],"")::cmdList)
   6.259 +                                                     )
   6.260 +                                              else (let val thisCmd = getCmd (thisLine) 
   6.261 +							(*********************************************************)
   6.262 +                                                        (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   6.263 +						        (* i.e. put back into tuple format                       *)
   6.264 +							(*********************************************************)
   6.265 +                                                    in
   6.266 +                                                      (*TextIO.output (toParentStr, thisCmd); 
   6.267 +                                                        TextIO.flushOut toParentStr;*)
   6.268 +                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   6.269 +                                                    end
   6.270 +                                                    )
   6.271 +                                            )
   6.272 +                                        end
   6.273                                      
   6.274 -                                    
   6.275 +                                                                  
   6.276  (**************************************************************)
   6.277  (*  Get Io-descriptor for polling of an input stream          *)
   6.278  (**************************************************************)
   6.279 @@ -388,6 +441,8 @@
   6.280  			 if (isSome pd ) then 
   6.281  			     let val pd' = OS.IO.pollIn (valOf pd)
   6.282  				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   6.283 +				 val _ = File.append (File.tmp_path (Path.basic "parent_poll")) 
   6.284 +			           ("In parent_poll\n")	
   6.285  			     in
   6.286  				if null pdl 
   6.287  				then
   6.288 @@ -414,13 +469,15 @@
   6.289  			 if (isSome pd ) then 
   6.290  			     let val pd' = OS.IO.pollIn (valOf pd)
   6.291  				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
   6.292 +                                 val _ = File.append (File.tmp_path (Path.basic "child_poll")) 
   6.293 +			           ("In child_poll\n")
   6.294  			     in
   6.295  				if null pdl 
   6.296  				then
   6.297  				   NONE
   6.298  				else if (OS.IO.isIn (hd pdl)) 
   6.299  				     then
   6.300 -					 SOME (getCmd (TextIO.inputLine fromStr))
   6.301 +					 SOME ((*getCmd*) (TextIO.inputLine fromStr))
   6.302  				     else
   6.303  					 NONE
   6.304  			     end
   6.305 @@ -439,13 +496,19 @@
   6.306  	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   6.307  							(*********************************)
   6.308  	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   6.309 -		    let val (childInput,childOutput) =  cmdstreamsOf childProc
   6.310 +		    let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
   6.311 +			           ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n")
   6.312 +                        val (childInput,childOutput) =  cmdstreamsOf childProc
   6.313  			val child_handle= cmdchildHandle childProc
   6.314  			(* childCmd is the .dfg file that the problem is in *)
   6.315  			val childCmd = fst(snd (cmdchildInfo childProc))
   6.316 +                        val _ = File.append (File.tmp_path (Path.basic "child_command")) 
   6.317 +			           (childCmd^"\n")
   6.318  			(* now get the number of the subgoal from the filename *)
   6.319  			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   6.320  			val childIncoming = pollChildInput childInput
   6.321 + 			val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) 
   6.322 +			           ("finished polling child \n")
   6.323  			val parentID = Posix.ProcEnv.getppid()
   6.324  			val prover = cmdProver childProc
   6.325  			val thmstring = cmdThm childProc
   6.326 @@ -454,8 +517,8 @@
   6.327  			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.328  			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   6.329  			val goalstring = cmdGoal childProc							
   6.330 -			val _ = File.write (File.tmp_path (Path.basic "child_comms")) 
   6.331 -			           (prover^thmstring^goalstring^childCmd)
   6.332 +			val _ = File.append (File.tmp_path (Path.basic "child_comms")) 
   6.333 +			           (prover^thmstring^goalstring^childCmd^"\n")
   6.334  		    in 
   6.335  		      if (isSome childIncoming) 
   6.336  		      then 
   6.337 @@ -496,8 +559,9 @@
   6.338  
   6.339  (*** add subgoal id num to this *)
   6.340  	     fun execCmds  [] procList = procList
   6.341 -	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   6.342 -		   if (prover = "spass") 
   6.343 +	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  =             let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child"))  ("About to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   6.344 +	       in 
   6.345 +		 if (prover = "spass") 
   6.346  		   then 
   6.347  		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.348  			   val (instr, outstr)=Unix.streamsOf childhandle
   6.349 @@ -509,12 +573,12 @@
   6.350  						proc_handle = childhandle,
   6.351  						instr = instr,
   6.352  						outstr = outstr })::procList))
   6.353 -			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file)
   6.354 +			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now()))))
   6.355  		       in
   6.356 -			  execCmds cmds newProcList
   6.357 +			  Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList
   6.358  		       end
   6.359  		   else 
   6.360 -		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.361 +		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (settings@[file])))
   6.362  			   val (instr, outstr)=Unix.streamsOf childhandle
   6.363  			   val newProcList =    (((CMDPROC{
   6.364  						prover = prover,
   6.365 @@ -525,9 +589,9 @@
   6.366  						instr = instr,
   6.367  						outstr = outstr })::procList))
   6.368  		       in
   6.369 -			  execCmds cmds newProcList
   6.370 +			 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList
   6.371  		       end
   6.372 -
   6.373 +		end
   6.374  
   6.375  
   6.376  	  (****************************************)                  
   6.377 @@ -587,7 +651,11 @@
   6.378  					    let 
   6.379  					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.380  					      val parentID = Posix.ProcEnv.getppid()
   6.381 +          					 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ")
   6.382  					      val newProcList' =checkChildren (newProcList, toParentStr) 
   6.383 +
   6.384 +					      val _ = warning("off to keep watching...")
   6.385 +					     val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ")
   6.386  					    in
   6.387  					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.388  					      loop (newProcList') 
   6.389 @@ -615,7 +683,8 @@
   6.390  										    (******************************)
   6.391  				  (    let val newProcList = checkChildren ((procList), toParentStr)
   6.392  				       in
   6.393 -					 Posix.Process.sleep (Time.fromSeconds 1);
   6.394 +					 (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.395 +					(File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n ");
   6.396  					 loop (newProcList)
   6.397  				       end
   6.398  				   
   6.399 @@ -797,11 +866,11 @@
   6.400                                                                     (
   6.401                                                                       goals_being_watched := (!goals_being_watched) -1;
   6.402                                                                       Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   6.403 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   6.404 +                                                                      Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr)));
   6.405                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   6.406                                                                        if (!goals_being_watched = 0)
   6.407                                                                        then 
   6.408 -                                                                          (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp")));
   6.409 +                                                                          (let val  outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp")));
   6.410                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   6.411                                                                                 val _ =  TextIO.closeOut outfile
   6.412                                                                             in
     7.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jun 09 23:33:28 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Jun 10 16:15:36 2005 +0200
     7.3 @@ -31,12 +31,13 @@
     7.4  val subgoals = [];
     7.5  
     7.6  val traceflag = ref true;
     7.7 +(* used for debug *)
     7.8 +val debug = ref false;
     7.9  
    7.10 -val debug = ref false;
    7.11  fun debug_tac tac = (warning "testing";tac);
    7.12 -
    7.13 +(* default value is false *)
    7.14 +val full_spass = ref false;
    7.15  val trace_res = ref false;
    7.16 -val full_spass = ref false;
    7.17  
    7.18  val skolem_tac = skolemize_tac;
    7.19  
    7.20 @@ -69,10 +70,13 @@
    7.21   
    7.22  (**** for Isabelle/ML interface  ****)
    7.23  
    7.24 -fun is_proof_char ch = (ch = " ") orelse
    7.25 -     ((ord"!" <= ord ch) andalso (ord ch <= ord"~") andalso (ch <> "?"))  
    7.26 +fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    7.27  
    7.28 -fun proofstring x = List.filter (is_proof_char) (explode x);
    7.29 +fun proofstring x = let val exp = explode x 
    7.30 +                    in
    7.31 +                        List.filter (is_proof_char ) exp
    7.32 +                    end
    7.33 +
    7.34  
    7.35  
    7.36  (*
    7.37 @@ -130,113 +134,90 @@
    7.38          val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    7.39  	val out = TextIO.openOut(probfile)
    7.40      in
    7.41 -	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
    7.42 -	 if !trace_res then (warning probfile) else ())
    7.43 +	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
    7.44      end;
    7.45  
    7.46  
    7.47 +
    7.48  (*********************************************************************)
    7.49  (* call SPASS with settings and problem file for the current subgoal *)
    7.50  (* should be modified to allow other provers to be called            *)
    7.51  (*********************************************************************)
    7.52 +(* now passing in list of skolemized thms and list of sgterms to go with them *)
    7.53 +fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
    7.54 +   val axfile = (File.platform_path axiom_file)
    7.55 +    val hypsfile = (File.platform_path hyps_file)
    7.56 +     val clasimpfile = (File.platform_path clasimp_file)
    7.57 +    val spass_home = getenv "SPASS_HOME"
    7.58 +     
    7.59 +fun make_atp_list [] sign n = []
    7.60 +|   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    7.61 +let 
    7.62 +	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    7.63 +	val thmproofstr = proofstring ( skothmstr)
    7.64 +	val no_returns =List.filter   not_newline ( thmproofstr)
    7.65 +	val thmstr = implode no_returns
    7.66 +	val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
    7.67  
    7.68 -fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  =
    7.69 -    let val thmstring = Meson.concat_with_and (map string_of_thm thms) 
    7.70 -	val thm_no = length thms
    7.71 -	val _ = warning ("number of thms is : "^(string_of_int thm_no))
    7.72 -	val _ = warning ("thmstring in call_res is: "^thmstring)
    7.73 -   
    7.74 -	val goalstr = Sign.string_of_term sign sg_term 
    7.75 -	val goalproofstring = proofstring goalstr
    7.76 -	val no_returns =List.filter not_newline ( goalproofstring)
    7.77 -	val goalstring = implode no_returns
    7.78 -	val _ = warning ("goalstring in call_res is: "^goalstring)
    7.79 -   
    7.80 -	(*val prob_file =File.tmp_path (Path.basic newprobfile); *)
    7.81 -	(*val _ =( warning ("calling make_clauses "))
    7.82 -	val clauses = make_clauses thms
    7.83 -	val _ =( warning ("called make_clauses "))*)
    7.84 -	(*val _ = tptp_inputs clauses prob_file*)
    7.85 -	val thmstring = Meson.concat_with_and (map string_of_thm thms) 
    7.86 -      
    7.87 -	val goalstr = Sign.string_of_term sign sg_term 
    7.88 -	val goalproofstring = proofstring goalstr
    7.89 +	val sgstr = Sign.string_of_term sign sg_term 
    7.90 +	val goalproofstring = proofstring sgstr
    7.91  	val no_returns =List.filter not_newline ( goalproofstring)
    7.92  	val goalstring = implode no_returns
    7.93 -   
    7.94 -	val thmproofstring = proofstring ( thmstring)
    7.95 -	val no_returns =List.filter   not_newline ( thmproofstring)
    7.96 -	val thmstr = implode no_returns
    7.97 -       
    7.98 +	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    7.99 +
   7.100  	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   7.101 -	val axfile = (File.platform_path axiom_file)
   7.102 -	val hypsfile = (File.platform_path hyps_file)
   7.103 -	val clasimpfile = (File.platform_path clasimp_file)
   7.104 -	val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile")))
   7.105 -	val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
   7.106 -	val _ = TextIO.flushOut outfile;
   7.107 -	val _ =  TextIO.closeOut outfile
   7.108 -     in
   7.109 -	(* without paramodulation *)
   7.110 -	(warning ("goalstring in call_res_tac is: "^goalstring));
   7.111 -	(warning ("prob file in cal_res_tac is: "^probfile));
   7.112 -     (* Watcher.callResProvers(childout,
   7.113 -     [("spass",thmstr,goalstring,*spass_home*,  
   7.114 -     "-DocProof", 
   7.115 -     clasimpfile, axfile, hypsfile, probfile)]);*)
   7.116 -  if !full_spass 
   7.117 -  then
   7.118 -   (Watcher.callResProvers(childout,
   7.119 -	    [("spass", thmstr, goalstring (*,spass_home*), 
   7.120 -	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
   7.121 -	     "-DocProof%-TimeLimit=60", 
   7.122 -	     clasimpfile, axfile, hypsfile, probfile)]))
   7.123 -  else	
   7.124 -   (Watcher.callResProvers(childout,
   7.125 -	    [("spass", thmstr, goalstring (*,spass_home*), 
   7.126 -	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
   7.127 -	     "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
   7.128 -	     clasimpfile, axfile, hypsfile, probfile)]));
   7.129 -     
   7.130 -	(* with paramodulation *)
   7.131 -	(*Watcher.callResProvers(childout,
   7.132 -	       [("spass",thmstr,goalstring,spass_home,
   7.133 -	       "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
   7.134 -		 prob_path)]); *)
   7.135 -       (* Watcher.callResProvers(childout,
   7.136 -	[("spass",thmstr,goalstring,spass_home, 
   7.137 -	"-DocProof",  prob_path)]);*)
   7.138 -	dummy_tac
   7.139 -    end
   7.140 +	val _ = (warning ("prob file in cal_res_tac is: "^probfile))                                                                           
   7.141 +in
   7.142 + 	if !full_spass 
   7.143 +  	then
   7.144 +   		([("spass", thmstr, goalstring (*,spass_home*), 
   7.145 +	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
   7.146 +	     	"-DocProof%-TimeLimit=60", 
   7.147 +	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
   7.148 +  	else	
   7.149 +   		([("spass", thmstr, goalstring (*,spass_home*), 
   7.150 +	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
   7.151 +	     	"-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
   7.152 +	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
   7.153 +end
   7.154  
   7.155 +val thms_goals = ListPair.zip( thms, sg_terms) 
   7.156 +val atp_list = make_atp_list  thms_goals sign 1
   7.157 +in
   7.158 +	Watcher.callResProvers(childout,atp_list);
   7.159 +        warning("Sent commands to watcher!");
   7.160 +  	dummy_tac
   7.161 + end
   7.162 +(*
   7.163 +  val axfile = (File.platform_path axiom_file)
   7.164 +    val hypsfile = (File.platform_path hyps_file)
   7.165 +     val clasimpfile = (File.platform_path  clasimp_file)
   7.166 +    val spass_home = getenv "SPASS_HOME"
   7.167 + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1)
   7.168 +    
   7.169 + val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ;
   7.170 + val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses);
   7.171 +Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home,  "-DocProof", clasimpfile, axfile, hypsfile,probfile)]);
   7.172 +
   7.173 +Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell",  "", clasimpfile, axfile, hypsfile,probfile)]);
   7.174 +
   7.175 +
   7.176 +*)
   7.177  (**********************************************************)
   7.178  (* write out the current subgoal as a tptp file, probN,   *)
   7.179  (* then call dummy_tac - should be call_res_tac           *)
   7.180  (**********************************************************)
   7.181  
   7.182  
   7.183 -fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
   7.184 - (
   7.185 -   warning("in call_atp_tac_tfrees");
   7.186 -   tptp_inputs_tfrees (make_clauses thms) n tfrees;
   7.187 -   call_resolve_tac sign thms sg_term (childin, childout, pid) n;
   7.188 -   dummy_tac);
   7.189 -
   7.190 -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n st = 
   7.191 -  let val sign = sign_of_thm st
   7.192 -      val _ = warning ("in atp_tac_tfrees ")
   7.193 -      val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
   7.194 -  in  
   7.195 -    SELECT_GOAL
   7.196 -      (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   7.197 -       METAHYPS(fn negs => (call_atp_tac_tfrees sign negs n tfrees sg_term
   7.198 -                            (childin, childout,pid) ))]) n st
   7.199 -  end;
   7.200 -
   7.201 -
   7.202 -fun isar_atp_g tfrees sg_term (childin, childout, pid) n =       
   7.203 -  ((warning("in isar_atp_g"));
   7.204 -   atp_tac_tfrees tfrees sg_term (childin, childout, pid) n);
   7.205 +fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
   7.206 +                       if (equal n 0) then 
   7.207 +				(call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
   7.208 +			else
   7.209 +                           
   7.210 +               		( SELECT_GOAL
   7.211 +  				(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   7.212 +  				 METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
   7.213 +                                                    get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
   7.214  
   7.215  
   7.216  
   7.217 @@ -246,24 +227,26 @@
   7.218  (* in proof reconstruction                    *)
   7.219  (**********************************************)
   7.220  
   7.221 -fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
   7.222 -      if (k > n) 
   7.223 -      then () 
   7.224 -      else 
   7.225 -	  let val prems = prems_of thm 
   7.226 -	      val sg_term = ReconOrderClauses.get_nth n prems
   7.227 -	      val thmstring = string_of_thm thm
   7.228 -	  in   
   7.229 -	      (warning("in isar_atp_goal'"));
   7.230 -	      (warning("thmstring in isar_atp_goal': "^thmstring));
   7.231 -	       isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
   7.232 -	       isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
   7.233 -	  end;
   7.234 +fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
   7.235 +                  
   7.236 +                           (let val  prems = prems_of thm 
   7.237 +                              (*val sg_term = get_nth k prems*)
   7.238 +                                val sign = sign_of_thm thm
   7.239 +                                val thmstring = string_of_thm thm
   7.240 +                            in   
   7.241 +                                 
   7.242 +                		(warning("in isar_atp_goal'"));
   7.243 +                                (warning("thmstring in isar_atp_goal': "^thmstring));
   7.244 + 				(* go and call callResProvers with this subgoal *)
   7.245 + 				(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   7.246 + 				(* recursive call to pick up the remaining subgoals *)
   7.247 +                                (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   7.248 +                                get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   7.249 +                            end);
   7.250  
   7.251 -
   7.252 -fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   7.253 +(*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   7.254                (if (!debug) then warning (string_of_thm thm) 
   7.255 -               else (isar_atp_goal' thm 1 n_subgoals tfree_lits  (childin, childout, pid) ));
   7.256 +               else (isar_atp_goal' thm n_subgoals tfree_lits  (childin, childout, pid) ));*)
   7.257  
   7.258  (**************************************************)
   7.259  (* convert clauses from "assume" to conjecture.   *)
   7.260 @@ -276,8 +259,9 @@
   7.261  
   7.262  fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   7.263      let val tfree_lits = isar_atp_h thms 
   7.264 -    in warning("in isar_atp_aux");
   7.265 -       isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid)
   7.266 +    in
   7.267 +	(warning("in isar_atp_aux"));
   7.268 +         isar_atp_goal' thm n_subgoals tfree_lits   (childin, childout, pid)
   7.269      end;
   7.270  
   7.271  (******************************************************************)
   7.272 @@ -287,8 +271,9 @@
   7.273  (* turns off xsymbol at start of function, restoring it at end    *)
   7.274  (******************************************************************)
   7.275  (*FIX changed to clasimp_file *)
   7.276 -fun isar_atp' (ctxt, thms, thm) =
   7.277 -    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   7.278 +fun isar_atp' (ctxt,thms, thm) =
   7.279 +    let 
   7.280 +	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   7.281          val _= (warning ("in isar_atp'"))
   7.282          val prems  = prems_of thm
   7.283          val sign = sign_of_thm thm
   7.284 @@ -298,12 +283,11 @@
   7.285          
   7.286  	(* set up variables for writing out the clasimps to a tptp file *)
   7.287  	val (clause_arr, num_of_clauses) =
   7.288 -	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
   7.289 +	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
   7.290  	                                 (ProofContext.theory_of ctxt)
   7.291 -        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file)
   7.292 +        val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
   7.293  
   7.294          (* cq: add write out clasimps to file *)
   7.295 -
   7.296          (* cq:create watcher and pass to isar_atp_aux *)
   7.297          (* tracing *) 
   7.298          (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   7.299 @@ -324,7 +308,7 @@
   7.300                             (warning ("subgoals: "^prems_string));
   7.301                             (warning ("pid: "^ pidstring))); 
   7.302                              isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
   7.303 -                           
   7.304 +                           (warning("turning xsymbol back on!"));
   7.305                             print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   7.306      end;
   7.307  
   7.308 @@ -343,6 +327,8 @@
   7.309  	safeEs @ safeIs @ hazEs @ hazIs
   7.310      end;
   7.311  
   7.312 +
   7.313 +
   7.314  fun append_name name [] _ = []
   7.315    | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   7.316  
   7.317 @@ -352,6 +338,7 @@
   7.318  	thms'::(append_names names thmss)
   7.319      end;
   7.320  
   7.321 +
   7.322  fun get_thms_ss [] = []
   7.323    | get_thms_ss thms =
   7.324      let val names = map Thm.name_of_thm thms 
   7.325 @@ -361,6 +348,9 @@
   7.326  	ResLib.flat_noDup thms''
   7.327      end;
   7.328  
   7.329 +
   7.330 +
   7.331 +
   7.332  in
   7.333  
   7.334  
   7.335 @@ -369,7 +359,7 @@
   7.336  (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   7.337  (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   7.338  (*claset file and prob file*)
   7.339 -(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
   7.340 +(* FIX*)
   7.341  (*fun isar_local_thms (delta_cs, delta_ss_thms) =
   7.342      let val thms_cs = get_thms_cs delta_cs
   7.343  	val thms_ss = get_thms_ss delta_ss_thms
   7.344 @@ -383,6 +373,8 @@
   7.345  *)
   7.346  
   7.347  
   7.348 +
   7.349 +
   7.350  (* called in Isar automatically *)
   7.351  
   7.352  fun isar_atp (ctxt,thm) =
   7.353 @@ -398,13 +390,15 @@
   7.354            (warning ("initial thm in isar_atp: "^thmstring));
   7.355            (warning ("subgoals in isar_atp: "^prems_string));
   7.356      	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   7.357 -          ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
   7.358 -           isar_atp' (ctxt, prems, thm))
   7.359 +          (*isar_local_thms (d_cs,d_ss_thms);*)
   7.360 +           isar_atp' (ctxt,prems, thm)
   7.361      end;
   7.362  
   7.363  end
   7.364  
   7.365  
   7.366 +
   7.367 +
   7.368  end;
   7.369  
   7.370  Proof.atp_hook := ResAtp.isar_atp;