# HG changeset patch # User blanchet # Date 1304330973 -7200 # Node ID a2db47fa015eec188fc014e7bc7bcc6ea4a06f88 # Parent cddab94eeb145e0717af00fcd1753a2408293845 added TPTP exporter facility -- useful to do experiments with machine learning diff -r cddab94eeb14 -r a2db47fa015e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon May 02 12:09:33 2011 +0200 +++ b/src/HOL/IsaMakefile Mon May 02 12:09:33 2011 +0200 @@ -1056,9 +1056,10 @@ ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \ ex/sledgehammer_tactics.ML ex/Sqrt.thy \ ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ - ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ - ex/While_Combinator_Example.thy ex/document/root.bib \ - ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ + ex/TPTP_Export.thy ex/Transfer_Ex.thy ex/Tree23.thy \ + ex/Unification.thy ex/While_Combinator_Example.thy \ + ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \ + ex/svc_test.thy \ ../Tools/interpretation_with_defs.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex diff -r cddab94eeb14 -r a2db47fa015e src/HOL/ex/TPTP_Export.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/TPTP_Export.thy Mon May 02 12:09:33 2011 +0200 @@ -0,0 +1,26 @@ +theory TPTP_Export +imports Complex_Main +uses "tptp_export.ML" +begin + +ML {* +val thy = @{theory Complex_Main} +val ctxt = @{context} +*} + +ML {* +TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true + "/tmp/infs_full_types.tptp" +*} + +ML {* +TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false + "/tmp/infs_partial_types.tptp" +*} + +ML {* +TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy + "/tmp/graph.out" +*} + +end diff -r cddab94eeb14 -r a2db47fa015e src/HOL/ex/tptp_export.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/tptp_export.ML Mon May 02 12:09:33 2011 +0200 @@ -0,0 +1,126 @@ +(* Title: HOL/ex/tptp_export.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2011 + +Export Isabelle theories as first-order TPTP inferences, exploiting +Sledgehammer's translation. +*) + +signature TPTP_EXPORT = +sig + val generate_tptp_graph_file_for_theory : + Proof.context -> theory -> string -> unit + val generate_tptp_inference_file_for_theory : + Proof.context -> theory -> bool -> string -> unit +end; + +structure TPTP_Export : TPTP_EXPORT = +struct + +val _ = Sledgehammer_ATP_Translate.readable_names := false + +val ascii_of = Metis_Translate.ascii_of + +val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of + +fun facts_of thy = + Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty true + true Sledgehammer_Provers.atp_relevance_fudge [] [] + +fun fold_body_thms 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 (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen); + in (x' |> n = 1 ? f (name, prop, body'), seen') end); + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; + +fun theorems_mentioned_in_proof_term thm = + let + val PBody {thms, ...} = Thm.proof_body_of thm + 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 + in names end + +fun interesting_const_names ctxt = + let val thy = ProofContext.theory_of ctxt in + Sledgehammer_Filter.const_names_in_fact thy + (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN) + end + +fun generate_tptp_graph_file_for_theory ctxt thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val axioms = Theory.all_axioms_of thy |> map fst + fun do_thm thm = + let + val name = Thm.get_name_hint thm + val s = + "[" ^ Thm.legacy_get_kind thm ^ "] " ^ + (if member (op =) axioms name then "A" else "T") ^ " " ^ + prefix Sledgehammer_ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ + commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ + commas (map (prefix Metis_Translate.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 o snd) + val _ = map do_thm thms + in () end + +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)]) + |> 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) + | add_inferences_to_problem_line _ line = line +val add_inferences_to_problem = + map o apsnd o map o add_inferences_to_problem_line + +fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts0 = facts_of thy + val facts = + facts0 + |> map_filter (try (fn ((_, loc), (_, th)) => + Sledgehammer_ATP_Translate.translate_atp_fact ctxt true + ((Thm.get_name_hint th, loc), th))) + val readable_names = false + val explicit_forall = true + val type_sys = + ATP_Systems.Preds (ATP_Systems.Polymorphic, + if full_types then ATP_Systems.All_Types + else ATP_Systems.Const_Arg_Types) + val explicit_apply = false + val (atp_problem, _, _, _, _) = + Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys + explicit_apply [] @{prop False} facts + val infers = + facts0 |> map (fn (_, (_, th)) => + (fact_name_of (Thm.get_name_hint th), + theorems_mentioned_in_proof_term th)) + val infers = + infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) + val atp_problem = atp_problem |> add_inferences_to_problem infers + val ss = + ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.Hypothesis + ATP_Problem.Fof atp_problem + val _ = app (File.append path) ss + in () end + +end;