# HG changeset patch # User blanchet # Date 1308559262 -7200 # Node ID 5af1abc13c1fbd8622ff22f2b839bf087906d352 # Parent 1cef683b588bc2401512b327ce46b7f8cb1e88c0 only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded diff -r 1cef683b588b -r 5af1abc13c1f src/HOL/ex/atp_export.ML --- a/src/HOL/ex/atp_export.ML Mon Jun 20 10:41:02 2011 +0200 +++ b/src/HOL/ex/atp_export.ML Mon Jun 20 10:41:02 2011 +0200 @@ -8,7 +8,6 @@ signature ATP_EXPORT = sig - val theorems_mentioned_in_proof_term : thm -> string list val generate_tptp_graph_file_for_theory : Proof.context -> theory -> string -> unit val generate_tptp_inference_file_for_theory : @@ -18,9 +17,10 @@ structure ATP_Export : ATP_EXPORT = struct -val ascii_of = ATP_Translate.ascii_of +open ATP_Problem +open ATP_Translate -val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of +val fact_name_of = prefix fact_prefix o ascii_of fun facts_of thy = Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty @@ -29,25 +29,29 @@ (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to be missing over there; or maybe the two code portions are not doing the same? *) -fun fold_body_thms f = +fun fold_body_thms all_names f = let fun app n (PBody {thms, ...}) = - thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) => - if Inttab.defined seen i then - (x, seen) - else - let - val body' = Future.join body - val n' = n + (if name = "" then 0 else 1) - val (x', seen') = (x, seen) |> n' <= 1 ? app n' body' - in (x' |> n = 1 ? f (name, prop, body'), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end + thms |> fold (fn (_, (name, prop, body)) => fn x => + let + val body' = Future.join body + val n' = + n + (if name = "" orelse + (is_some all_names andalso + not (member (op =) (the all_names) name)) then + 0 + else + 1) + val x' = x |> n' <= 1 ? app n' body' + in (x' |> n = 1 ? f (name, prop, body')) end) + in fold (app 0) end -fun theorems_mentioned_in_proof_term thm = +fun theorems_mentioned_in_proof_term all_names thm = let fun collect (s, _, _) = if s <> "" then insert (op =) s else I val names = - [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of + [] |> fold_body_thms all_names collect [Thm.proof_body_of thm] + |> map fact_name_of in names end fun interesting_const_names ctxt = @@ -67,9 +71,9 @@ val s = "[" ^ Thm.legacy_get_kind thm ^ "] " ^ (if member (op =) axioms name then "A" else "T") ^ " " ^ - prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ - commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ - commas (map (prefix ATP_Translate.const_prefix o ascii_of) + prefix fact_prefix (ascii_of name) ^ ": " ^ + commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ + commas (map (prefix const_prefix o ascii_of) (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" in File.append path s end val thms = facts_of thy |> map snd @@ -78,26 +82,27 @@ fun inference_term [] = NONE | inference_term ss = - ATP_Problem.ATerm ("inference", - [ATP_Problem.ATerm ("isabelle", []), - ATP_Problem.ATerm ("[]", []), - ATP_Problem.ATerm ("[]", - map (fn s => ATP_Problem.ATerm (s, [])) ss)]) + ATerm ("inference", + [ATerm ("isabelle", []), + ATerm (tptp_empty_list, []), + ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) |> SOME fun inference infers ident = these (AList.lookup (op =) infers ident) |> inference_term fun add_inferences_to_problem_line infers - (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) = - ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident, - NONE) + (Formula (ident, Axiom, phi, NONE, NONE)) = + Formula (ident, Lemma, phi, inference infers ident, NONE) | add_inferences_to_problem_line _ line = line val add_inferences_to_problem = map o apsnd o map o add_inferences_to_problem_line +fun ident_of_problem_line (Decl (ident, _, _)) = ident + | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident + fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name = let - val format = ATP_Problem.FOF - val type_sys = type_sys |> ATP_Translate.type_sys_from_string + val format = FOF + val type_sys = type_sys |> type_sys_from_string val path = file_name |> Path.explode val _ = File.write path "" val facts0 = facts_of thy @@ -105,17 +110,19 @@ facts0 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) val (atp_problem, _, _, _, _, _, _) = - ATP_Translate.prepare_atp_problem ctxt format - ATP_Problem.Axiom ATP_Problem.Axiom type_sys false false true [] - @{prop False} facts + prepare_atp_problem ctxt format Axiom Axiom type_sys false false true [] + @{prop False} facts + val all_names = facts0 |> map (Thm.get_name_hint o snd) val infers = facts0 |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), - theorems_mentioned_in_proof_term th)) + theorems_mentioned_in_proof_term (SOME all_names) th)) + val all_atp_problem_names = + atp_problem |> maps (map ident_of_problem_line o snd) val infers = - infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) + infers |> map (apsnd (filter (member (op =) all_atp_problem_names))) val atp_problem = atp_problem |> add_inferences_to_problem infers - val ss = ATP_Problem.tptp_lines_for_atp_problem ATP_Problem.FOF atp_problem + val ss = tptp_lines_for_atp_problem FOF atp_problem val _ = app (File.append path) ss in () end