# HG changeset patch # User quigley # Date 1112632998 -7200 # Node ID 3549ff7158f388696fb7b2c326115c546c03acb0 # Parent a9d65894962ee7b290b3bdbbe3492e2ea6762604 Updated to add watcher code. diff -r a9d65894962e -r 3549ff7158f3 src/HOL/IsaMakefile --- 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 diff -r a9d65894962e -r 3549ff7158f3 src/HOL/Reconstruction.thy --- 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 diff -r a9d65894962e -r 3549ff7158f3 src/HOL/Tools/meson.ML --- 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) = diff -r a9d65894962e -r 3549ff7158f3 src/HOL/Tools/res_atp.ML --- 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;