blanchet@44064: (* Title: HOL/ex/atp_export.ML blanchet@43473: Author: Jasmin Blanchette, TU Muenchen blanchet@43473: Copyright 2011 blanchet@43473: blanchet@43473: Export Isabelle theories as first-order TPTP inferences, exploiting blanchet@43473: Sledgehammer's translation. blanchet@43473: *) blanchet@43473: blanchet@44064: signature ATP_EXPORT = blanchet@43473: sig blanchet@43473: val generate_tptp_graph_file_for_theory : blanchet@43473: Proof.context -> theory -> string -> unit blanchet@43473: val generate_tptp_inference_file_for_theory : blanchet@43473: Proof.context -> theory -> bool -> string -> unit blanchet@43473: end; blanchet@43473: blanchet@44064: structure ATP_Export : ATP_EXPORT = blanchet@43473: struct blanchet@43473: blanchet@43929: val ascii_of = ATP_Translate.ascii_of blanchet@43473: blanchet@43929: val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of blanchet@43473: blanchet@43473: fun facts_of thy = blanchet@43509: Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty blanchet@43785: true (K true) [] [] blanchet@43473: blanchet@43473: fun fold_body_thms f = blanchet@43473: let blanchet@43473: fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) => blanchet@43473: if Inttab.defined seen i then (x, seen) blanchet@43473: else blanchet@43473: let blanchet@43473: val body' = Future.join body; blanchet@43473: val (x', seen') = app (n + (if name = "" then 0 else 1)) body' (x, Inttab.update (i, ()) seen); blanchet@43473: in (x' |> n = 1 ? f (name, prop, body'), seen') end); blanchet@43473: in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; blanchet@43473: blanchet@43473: fun theorems_mentioned_in_proof_term thm = blanchet@43473: let blanchet@43473: fun collect (s, _, _) = if s <> "" then insert (op =) s else I blanchet@43473: val names = blanchet@43473: [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of blanchet@43473: in names end blanchet@43473: blanchet@43473: fun interesting_const_names ctxt = blanchet@43473: let val thy = ProofContext.theory_of ctxt in blanchet@43473: Sledgehammer_Filter.const_names_in_fact thy blanchet@43473: (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN) blanchet@43473: end blanchet@43473: blanchet@43473: fun generate_tptp_graph_file_for_theory ctxt thy file_name = blanchet@43473: let blanchet@43473: val path = file_name |> Path.explode blanchet@43473: val _ = File.write path "" blanchet@43473: val axioms = Theory.all_axioms_of thy |> map fst blanchet@43473: fun do_thm thm = blanchet@43473: let blanchet@43473: val name = Thm.get_name_hint thm blanchet@43473: val s = blanchet@43473: "[" ^ Thm.legacy_get_kind thm ^ "] " ^ blanchet@43473: (if member (op =) axioms name then "A" else "T") ^ " " ^ blanchet@43929: prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ blanchet@43473: commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ blanchet@43929: commas (map (prefix ATP_Translate.const_prefix o ascii_of) blanchet@43473: (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" blanchet@43473: in File.append path s end blanchet@43473: val thms = facts_of thy |> map (snd o snd) blanchet@43473: val _ = map do_thm thms blanchet@43473: in () end blanchet@43473: blanchet@43473: fun inference_term [] = NONE blanchet@43473: | inference_term ss = blanchet@43473: ATP_Problem.ATerm ("inference", blanchet@43473: [ATP_Problem.ATerm ("isabelle", []), blanchet@43473: ATP_Problem.ATerm ("[]", []), blanchet@43473: ATP_Problem.ATerm ("[]", blanchet@43473: map (fn s => ATP_Problem.ATerm (s, [])) ss)]) blanchet@43473: |> SOME blanchet@43473: fun inference infers ident = blanchet@43473: these (AList.lookup (op =) infers ident) |> inference_term blanchet@43473: fun add_inferences_to_problem_line infers blanchet@43473: (ATP_Problem.Formula (ident, ATP_Problem.Axiom, phi, NONE, NONE)) = blanchet@43473: ATP_Problem.Formula (ident, ATP_Problem.Lemma, phi, inference infers ident, blanchet@43473: NONE) blanchet@43473: | add_inferences_to_problem_line _ line = line blanchet@43473: val add_inferences_to_problem = blanchet@43473: map o apsnd o map o add_inferences_to_problem_line blanchet@43473: blanchet@43473: fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name = blanchet@43473: let blanchet@43803: val format = ATP_Problem.FOF blanchet@43835: val type_sys = blanchet@43929: ATP_Translate.Preds blanchet@43929: (ATP_Translate.Polymorphic, blanchet@43929: if full_types then ATP_Translate.All_Types blanchet@43929: else ATP_Translate.Const_Arg_Types, blanchet@43969: ATP_Translate.Heavyweight) blanchet@43473: val path = file_name |> Path.explode blanchet@43473: val _ = File.write path "" blanchet@43473: val facts0 = facts_of thy blanchet@43473: val facts = blanchet@44055: facts0 |> map (fn ((_, loc), (_, th)) => blanchet@44063: ((Thm.get_name_hint th, loc), prop_of th)) blanchet@43905: val explicit_apply = NONE blanchet@43750: val (atp_problem, _, _, _, _, _, _) = blanchet@43929: ATP_Translate.prepare_atp_problem ctxt format blanchet@43951: ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true blanchet@43951: [] @{prop False} facts blanchet@43473: val infers = blanchet@43473: facts0 |> map (fn (_, (_, th)) => blanchet@43473: (fact_name_of (Thm.get_name_hint th), blanchet@43473: theorems_mentioned_in_proof_term th)) blanchet@43473: val infers = blanchet@43473: infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) blanchet@43473: val atp_problem = atp_problem |> add_inferences_to_problem infers blanchet@43473: val ss = blanchet@43778: ATP_Problem.tptp_strings_for_atp_problem ATP_Problem.FOF atp_problem blanchet@43473: val _ = app (File.append path) ss blanchet@43473: in () end blanchet@43473: blanchet@43473: end;