# HG changeset patch # User quigley # Date 1112890804 -7200 # Node ID 28eb0fe505330929c99afb3e60ff69c66a4f8f36 # Parent 28cc2314c7ff8cdd0f60a54ab655135d94057091 Integrating the reconstruction files into the building of HOL diff -r 28cc2314c7ff -r 28eb0fe50533 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Apr 07 17:45:51 2005 +0200 +++ b/src/HOL/Tools/meson.ML Thu Apr 07 18:20:04 2005 +0200 @@ -86,6 +86,13 @@ | has _ = false in has end; +(* for tracing statements *) + +fun concat_with_and [] str = str +| concat_with_and (x::[]) str = str^" ("^x^")" +| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) + + (**** Clause handling ****) @@ -124,7 +131,7 @@ (*Conjunctive normal form, detecting tautologies early. Strips universal quantifiers and breaks up conjunctions. *) fun cnf_aux seen (th,ths) = - let val _= (warning ("in cnf_aux")) + let val _= (warning ("in cnf_aux, th : "^(string_of_thm th))) in if taut_lits (literals(prop_of th) @ seen) then ths (*tautology ignored*) else if not (has_consts ["All","op &"] (prop_of th)) @@ -310,8 +317,8 @@ (*Pull existential quantifiers (Skolemization)*) fun skolemize th = if not (has_consts ["Ex"] (prop_of th)) then th - else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, - disj_exD, disj_exD1, disj_exD2])) + else ((warning("in meson.skolemize with th: "^(string_of_thm th)));skolemize (tryres(th, [choice, conj_exD1, conj_exD2, + disj_exD, disj_exD1, disj_exD2]))) handle THM _ => skolemize (forward_res skolemize (tryres (th, [conj_forward, disj_forward, all_forward]))) @@ -321,7 +328,7 @@ (*Make clauses from a list of theorems, previously Skolemized and put into nnf. The resulting clauses are HOL disjunctions.*) fun make_clauses ths = - sort_clauses (map (generalize o nodups) (foldr cnf [] ths)); + ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths))); (*Convert a list of clauses to (contrapositive) Horn clauses*) fun make_horns ths = @@ -448,9 +455,14 @@ SUBGOAL (fn (prop,_) => let val ts = Logic.strip_assums_hyp prop + val _ = (warning("in meson.skolemize_tac ")) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "skolem"))) + val _ = TextIO.output(outfile, "in skolemize_tac "); + val _ = TextIO.flushOut outfile; + val _ = TextIO.closeOut outfile in EVERY1 [METAHYPS - (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 + (fn hyps => ((warning("in meson.skolemize_tac hyps are: "^(string_of_thm (hd hyps))));cut_facts_tac (map (skolemize o make_nnf) hyps) 1 THEN REPEAT (etac exE 1))), REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); diff -r 28cc2314c7ff -r 28eb0fe50533 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Apr 07 17:45:51 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Apr 07 18:20:04 2005 +0200 @@ -8,6 +8,8 @@ (*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*) (*Claire: changed: added actual watcher calls *) +val traceflag = ref true; + signature RES_ATP = sig val trace_res : bool ref @@ -175,7 +177,7 @@ val thmstr = implode no_returns val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) - val outfile = TextIO.openOut("/home/clq20/Jia_Code/hellofile") + val outfile = TextIO.openOut(File.sysify_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 @@ -223,25 +225,45 @@ (**********************************************************) (* 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) = + +(* dummy tac vs. Doesn't call resolve_tac *) - ( (warning("in call_atp_tac_tfrees")); +fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = + ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) ""))); + (warning("in call_atp_tac_tfrees")); + tptp_inputs_tfrees (make_clauses thms) n tfrees; - call_resolve_tac thms sg_term (childin, childout, pid) n; - dummy_tac); + call_resolve_tac thms sg_term (childin, childout, pid) n; + 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 => ((warning("calling call_atp_tac_tfrees"));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n +SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac,*) METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) "")));(*make_clauses negs;*)dummy_tac)) ])1 end; -fun isar_atp_g tfrees sg_term (childin, childout, pid) = + +METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) ""))));make_clauses negs;dummy_tac)) 1; +*) + + +fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n = +let val _ = (warning ("in atp_tac_tfrees ")) + val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term))) + + in +SELECT_GOAL + (EVERY1 [rtac ccontr,atomize_tac, tracify traceflag skolemize_tac, + METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n +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)); +((warning("in isar_atp_g"));atp_tac_tfrees tfrees sg_term (childin, childout, pid) n); @@ -257,9 +279,11 @@ else (let val prems = prems_of thm val sg_term = 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); @@ -270,7 +294,8 @@ (**************************************************) (* convert clauses from "assume" to conjecture. *) (* i.e. apply make_clauses and then get tptp for *) -(* any hypotheses in the goal *) +(* any hypotheses in the goal produced by assume *) +(* statements; *) (* write to file "hyps" *) (**************************************************) @@ -375,13 +400,15 @@ (* called in Isar automatically *) + fun isar_atp (ctxt,thm) = let val prems = ProofContext.prems_of ctxt val d_cs = Classical.get_delta_claset ctxt val d_ss_thms = Simplifier.get_delta_simpset ctxt val thmstring = string_of_thm thm - val prem_no = length prems - val prems_string = concat_with_and (map string_of_thm prems) "" + val sg_prems = prems_of thm + val prem_no = length sg_prems + val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) "" in (warning ("initial thm in isar_atp: "^thmstring));