Updated to add watcher code.
authorquigley
Mon Apr 04 18:43:18 2005 +0200 (2005-04-04)
changeset 156533549ff7158f3
parent 15652 a9d65894962e
child 15654 d53e5370cfbf
Updated to add watcher code.
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Apr 04 18:39:45 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Apr 04 18:43:18 2005 +0200
     1.3 @@ -108,12 +108,17 @@
     1.4    Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
     1.5    Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
     1.6    Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
     1.7 -  Tools/res_axioms.ML Tools/res_types_sorts.ML Tools/res_atp.ML\
     1.8 +  Tools/res_axioms.ML Tools/res_types_sorts.ML \
     1.9    Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.10    Tools/split_rule.ML Tools/typedef_package.ML \
    1.11    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.12    Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    1.13    blastdata.ML cladata.ML \
    1.14 +  Tools/ATP/recon_prelim.ML  Tools/ATP/recon_gandalf_base.ML  Tools/ATP/recon_order_clauses.ML\
    1.15 +  Tools/ATP/recon_translate_proof.ML   Tools/ATP/recon_parse.ML   Tools/ATP/recon_reconstruct_proof.ML \
    1.16 +  Tools/ATP/recon_transfer_proof.ML  Tools/ATP/myres_axioms.ML   Tools/ATP/res_clasimpset.ML \
    1.17 +  Tools/ATP/VampireCommunication.ML  Tools/ATP/SpassCommunication.ML     Tools/ATP/modUnix.ML  \
    1.18 +  Tools/ATP/watcher.sig  Tools/ATP/watcher.ML    Tools/res_atp.ML\
    1.19    document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    1.20  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
    1.21  
     2.1 --- a/src/HOL/Reconstruction.thy	Mon Apr 04 18:39:45 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Mon Apr 04 18:43:18 2005 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4  	  "Tools/res_skolem_function.ML"
     2.5  	  "Tools/res_axioms.ML"
     2.6  	  "Tools/res_types_sorts.ML"
     2.7 +
     2.8            "Tools/reconstruction.ML"
     2.9  
    2.10  begin
    2.11 @@ -21,4 +22,4 @@
    2.12  
    2.13  setup Reconstruction.setup
    2.14  
    2.15 -end
    2.16 \ No newline at end of file
    2.17 +end
     3.1 --- a/src/HOL/Tools/meson.ML	Mon Apr 04 18:39:45 2005 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Mon Apr 04 18:43:18 2005 +0200
     3.3 @@ -124,7 +124,8 @@
     3.4  (*Conjunctive normal form, detecting tautologies early.
     3.5    Strips universal quantifiers and breaks up conjunctions. *)
     3.6  fun cnf_aux seen (th,ths) =
     3.7 -  if taut_lits (literals(prop_of th) @ seen)  
     3.8 + let val _= (warning ("in cnf_aux"))
     3.9 + in if taut_lits (literals(prop_of th) @ seen)  
    3.10    then ths     (*tautology ignored*)
    3.11    else if not (has_consts ["All","op &"] (prop_of th))  
    3.12    then th::ths (*no work to do, terminate*)
    3.13 @@ -138,8 +139,8 @@
    3.14  	(METAHYPS (resop (cnf_nil seen)) 1) THEN
    3.15  	(fn st' => st' |>
    3.16  		METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    3.17 -    in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
    3.18 -and cnf_nil seen th = cnf_aux seen (th,[]);
    3.19 +    in  Seq.list_of (tac (th RS disj_forward)) @ ths  end end
    3.20 +and cnf_nil seen th = ((warning ("in cnf_nil "));cnf_aux seen (th,[]))
    3.21  
    3.22  (*Top-level call to cnf -- it's safe to reset name_ref*)
    3.23  fun cnf (th,ths) =
     4.1 --- a/src/HOL/Tools/res_atp.ML	Mon Apr 04 18:39:45 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Apr 04 18:43:18 2005 +0200
     4.3 @@ -145,6 +145,8 @@
     4.4  fun call_resolve_tac thms sg_term (childin, childout,pid)  = let
     4.5                              val newprobfile = new_prob_file ()
     4.6                               val thmstring = concat_with_and (map string_of_thm thms) ""
     4.7 +                            val thm_no = length thms
     4.8 +                            val _ = warning ("number of thms is : "^(string_of_int thm_no))
     4.9                             val _ = warning ("thmstring in call_res is: "^thmstring)
    4.10                              val goalstr = Sign.string_of_term Mainsign sg_term 
    4.11                              val goalproofstring = proofstring goalstr
    4.12 @@ -153,7 +155,9 @@
    4.13                              val _ = warning ("goalstring in call_res is: "^goalstring)
    4.14          
    4.15                              val prob_file =File.tmp_path (Path.basic newprobfile); 
    4.16 +                             (*val _ =( warning ("calling make_clauses "))
    4.17                               val clauses = make_clauses thms
    4.18 +                             val _ =( warning ("called make_clauses "))*)
    4.19                              (*val _ = tptp_inputs clauses prob_file*)
    4.20                              val thmstring = concat_with_and (map string_of_thm thms) ""
    4.21                             
    4.22 @@ -200,7 +204,7 @@
    4.23     let val _ = warning ("in resolve_tac ")
    4.24     in
    4.25     SELECT_GOAL
    4.26 -  (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)))])
    4.27 +  (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)*)))])
    4.28     end;
    4.29  
    4.30  
    4.31 @@ -212,18 +216,19 @@
    4.32  (* write out the current subgoal as a tptp file, probN,   *)
    4.33  (* then call dummy_tac - should be call_res_tac           *)
    4.34  (**********************************************************)
    4.35 -
    4.36 +(* should call call_res_tac here, not resolve_tac *)
    4.37 +(* 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 *)
    4.38  fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
    4.39 -                                         (tptp_inputs_tfrees (make_clauses thms) n tfrees; 
    4.40 -                                          resolve_tac sg_term (childin, childout, pid);
    4.41 +                                         ((*tptp_inputs_tfrees (make_clauses thms) n tfrees;*)
    4.42 +                                          call_resolve_tac thms sg_term (childin, childout, pid);
    4.43    					  dummy_tac);
    4.44  
    4.45  fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
    4.46  let val _ = (warning ("in atp_tac_tfrees "))
    4.47     in
    4.48  SELECT_GOAL
    4.49 -  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    4.50 -  METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid)))]) n
    4.51 +  (EVERY1 [rtac ccontr,atomize_tac, (*skolemize_tac, *)
    4.52 +  METAHYPS(fn negs => (call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
    4.53  end;
    4.54  
    4.55