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@44365: val theorems_mentioned_in_proof_term : blanchet@44365: string list option -> thm -> string list 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@44263: Proof.context -> theory -> string -> string -> unit blanchet@43473: end; blanchet@43473: blanchet@44064: structure ATP_Export : ATP_EXPORT = blanchet@43473: struct blanchet@43473: blanchet@44350: open ATP_Problem blanchet@44350: open ATP_Translate blanchet@43473: blanchet@44350: val fact_name_of = prefix fact_prefix o ascii_of blanchet@43473: blanchet@43473: fun facts_of thy = wenzelm@44156: Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty blanchet@44217: true [] [] blanchet@43473: blanchet@44329: (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few blanchet@44329: fixes that seem to be missing over there; or maybe the two code portions are blanchet@44329: not doing the same? *) blanchet@44350: fun fold_body_thms all_names f = blanchet@43473: let blanchet@44329: fun app n (PBody {thms, ...}) = blanchet@44350: thms |> fold (fn (_, (name, prop, body)) => fn x => blanchet@44350: let blanchet@44350: val body' = Future.join body blanchet@44350: val n' = blanchet@44350: n + (if name = "" orelse blanchet@44350: (is_some all_names andalso blanchet@44350: not (member (op =) (the all_names) name)) then blanchet@44350: 0 blanchet@44350: else blanchet@44350: 1) blanchet@44350: val x' = x |> n' <= 1 ? app n' body' blanchet@44350: in (x' |> n = 1 ? f (name, prop, body')) end) blanchet@44350: in fold (app 0) end blanchet@43473: blanchet@44350: fun theorems_mentioned_in_proof_term all_names thm = blanchet@43473: let blanchet@43473: fun collect (s, _, _) = if s <> "" then insert (op =) s else I blanchet@43473: val names = blanchet@44350: [] |> fold_body_thms all_names collect [Thm.proof_body_of thm] blanchet@44350: |> map fact_name_of blanchet@43473: in names end blanchet@43473: blanchet@43473: fun interesting_const_names ctxt = wenzelm@44156: let val thy = Proof_Context.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@44350: prefix fact_prefix (ascii_of name) ^ ": " ^ blanchet@44350: commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ blanchet@44350: commas (map (prefix 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@44086: val thms = facts_of thy |> map 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@44350: ATerm ("inference", blanchet@44350: [ATerm ("isabelle", []), blanchet@44350: ATerm (tptp_empty_list, []), blanchet@44350: ATerm (tptp_empty_list, map (fn s => 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@44350: (Formula (ident, Axiom, phi, NONE, NONE)) = blanchet@44350: Formula (ident, Lemma, phi, inference infers ident, 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@44350: fun ident_of_problem_line (Decl (ident, _, _)) = ident blanchet@44350: | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident blanchet@44350: blanchet@44263: fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name = blanchet@43473: let blanchet@44350: val format = FOF blanchet@44350: val type_sys = type_sys |> type_sys_from_string 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@44086: facts0 |> map (fn ((_, loc), th) => blanchet@44063: ((Thm.get_name_hint th, loc), prop_of th)) blanchet@43750: val (atp_problem, _, _, _, _, _, _) = blanchet@44365: prepare_atp_problem ctxt format Axiom Axiom type_sys true false true [] blanchet@44350: @{prop False} facts blanchet@44350: val all_names = facts0 |> map (Thm.get_name_hint o snd) blanchet@43473: val infers = blanchet@44086: facts0 |> map (fn (_, th) => blanchet@43473: (fact_name_of (Thm.get_name_hint th), blanchet@44350: theorems_mentioned_in_proof_term (SOME all_names) th)) blanchet@44350: val all_atp_problem_names = blanchet@44350: atp_problem |> maps (map ident_of_problem_line o snd) blanchet@43473: val infers = blanchet@44350: infers |> map (apsnd (filter (member (op =) all_atp_problem_names))) blanchet@43473: val atp_problem = atp_problem |> add_inferences_to_problem infers blanchet@44350: val ss = tptp_lines_for_atp_problem FOF atp_problem blanchet@43473: val _ = app (File.append path) ss blanchet@43473: in () end blanchet@43473: blanchet@43473: end;