Updated to add watcher code.
--- a/src/HOL/IsaMakefile Mon Apr 04 18:39:45 2005 +0200
+++ b/src/HOL/IsaMakefile Mon Apr 04 18:43:18 2005 +0200
@@ -108,12 +108,17 @@
Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
- Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/res_atp.ML\
+ Tools/res_axioms.ML Tools/res_types_sorts.ML \
Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
Tools/split_rule.ML Tools/typedef_package.ML \
Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
blastdata.ML cladata.ML \
+ Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
+ Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
+ Tools/ATP/recon_transfer_proof.ML Tools/ATP/myres_axioms.ML Tools/ATP/res_clasimpset.ML \
+ Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \
+ Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\
document/root.tex hologic.ML simpdata.ML thy_syntax.ML
@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
--- a/src/HOL/Reconstruction.thy Mon Apr 04 18:39:45 2005 +0200
+++ b/src/HOL/Reconstruction.thy Mon Apr 04 18:43:18 2005 +0200
@@ -13,6 +13,7 @@
"Tools/res_skolem_function.ML"
"Tools/res_axioms.ML"
"Tools/res_types_sorts.ML"
+
"Tools/reconstruction.ML"
begin
@@ -21,4 +22,4 @@
setup Reconstruction.setup
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/meson.ML Mon Apr 04 18:39:45 2005 +0200
+++ b/src/HOL/Tools/meson.ML Mon Apr 04 18:43:18 2005 +0200
@@ -124,7 +124,8 @@
(*Conjunctive normal form, detecting tautologies early.
Strips universal quantifiers and breaks up conjunctions. *)
fun cnf_aux seen (th,ths) =
- if taut_lits (literals(prop_of th) @ seen)
+ let val _= (warning ("in cnf_aux"))
+ in if taut_lits (literals(prop_of th) @ seen)
then ths (*tautology ignored*)
else if not (has_consts ["All","op &"] (prop_of th))
then th::ths (*no work to do, terminate*)
@@ -138,8 +139,8 @@
(METAHYPS (resop (cnf_nil seen)) 1) THEN
(fn st' => st' |>
METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
- in Seq.list_of (tac (th RS disj_forward)) @ ths end
-and cnf_nil seen th = cnf_aux seen (th,[]);
+ in Seq.list_of (tac (th RS disj_forward)) @ ths end end
+and cnf_nil seen th = ((warning ("in cnf_nil "));cnf_aux seen (th,[]))
(*Top-level call to cnf -- it's safe to reset name_ref*)
fun cnf (th,ths) =
--- a/src/HOL/Tools/res_atp.ML Mon Apr 04 18:39:45 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Apr 04 18:43:18 2005 +0200
@@ -145,6 +145,8 @@
fun call_resolve_tac thms sg_term (childin, childout,pid) = let
val newprobfile = new_prob_file ()
val thmstring = 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 Mainsign sg_term
val goalproofstring = proofstring goalstr
@@ -153,7 +155,9 @@
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 = concat_with_and (map string_of_thm thms) ""
@@ -200,7 +204,7 @@
let val _ = warning ("in resolve_tac ")
in
SELECT_GOAL
- (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac, METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");call_resolve_tac negs sg_term (childin, childout,pid)))])
+ (EVERY1 [rtac ccontr,atomize_tac,skolemize_tac, METAHYPS(fn negs => (warning ("calling call_resolve_tac next ");dummy_tac (*call_resolve_tac negs sg_term (childin, childout,pid)*)))])
end;
@@ -212,18 +216,19 @@
(* write out the current subgoal as a tptp file, probN, *)
(* then call dummy_tac - should be call_res_tac *)
(**********************************************************)
-
+(* should call call_res_tac here, not resolve_tac *)
+(* if we take tptpinputs out it gets into call_res_tac then falls over as usual after printing out goalstring. but if we leave it in it falls over here *)
fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) =
- (tptp_inputs_tfrees (make_clauses thms) n tfrees;
- resolve_tac sg_term (childin, childout, pid);
+ ((*tptp_inputs_tfrees (make_clauses thms) n tfrees;*)
+ call_resolve_tac thms sg_term (childin, childout, pid);
dummy_tac);
fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n =
let val _ = (warning ("in atp_tac_tfrees "))
in
SELECT_GOAL
- (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid)))]) n
+ (EVERY1 [rtac ccontr,atomize_tac, (*skolemize_tac, *)
+ METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
end;