# HG changeset patch # User blanchet # Date 1319889095 -7200 # Node ID 3e09961326ce69f2da90da66400ea4458bd05a13 # Parent e6901aa86a9e0fdea6dc61a0f930d53164d2d835 also export DFG formats diff -r e6901aa86a9e -r 3e09961326ce src/HOL/TPTP/ATP_Export.thy --- a/src/HOL/TPTP/ATP_Export.thy Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/TPTP/ATP_Export.thy Sat Oct 29 13:51:35 2011 +0200 @@ -4,6 +4,11 @@ begin ML {* +open ATP_Problem; +open ATP_Export; +*} + +ML {* val do_it = false; (* switch to "true" to generate the files *) val thy = @{theory Complex_Main}; val ctxt = @{context} @@ -11,32 +16,40 @@ ML {* if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" - "/tmp/infs_poly_preds.tptp" + "/tmp/axs_mono_simple.dfg" + |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) + "mono_simple" else () *} ML {* if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" - "/tmp/infs_poly_tags.tptp" + "/tmp/infs_poly_guards.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" else () *} ML {* if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_uniform" - "/tmp/infs_poly_tags_uniform.tptp" + "/tmp/infs_poly_tags.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags" else () *} ML {* if do_it then - ATP_Export.generate_tptp_graph_file_for_theory ctxt thy - "/tmp/graph.out" + "/tmp/infs_poly_tags_uniform.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags_uniform" +else + () +*} + +ML {* +if do_it then + "/tmp/graph.out" |> generate_tptp_graph_file_for_theory ctxt thy else () *} diff -r e6901aa86a9e -r 3e09961326ce src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/TPTP/atp_export.ML Sat Oct 29 13:51:35 2011 +0200 @@ -8,12 +8,14 @@ signature ATP_EXPORT = sig + type atp_format = ATP_Problem.atp_format + val theorems_mentioned_in_proof_term : string list option -> thm -> string list val generate_tptp_graph_file_for_theory : Proof.context -> theory -> string -> unit val generate_tptp_inference_file_for_theory : - Proof.context -> theory -> string -> string -> unit + Proof.context -> theory -> atp_format -> string -> string -> unit end; structure ATP_Export : ATP_EXPORT = @@ -109,13 +111,13 @@ fun ident_of_problem_line (Decl (ident, _, _)) = ident | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident -fun run_some_atp ctxt problem = +fun run_some_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob.tptp") val {exec, arguments, proof_delims, known_failures, ...} = - get_atp thy spassN - val _ = problem |> lines_for_atp_problem FOF |> File.write_list prob_file + get_atp thy (case format of DFG _ => spassN | _ => eN) + val _ = problem |> lines_for_atp_problem format |> File.write_list prob_file val command = File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^ @@ -133,12 +135,12 @@ [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |> map (fact_name_of o Context.theory_name) -fun is_problem_line_tautology ctxt (Formula (ident, _, phi, _, _)) = +fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) = exists (fn prefix => String.isPrefix prefix ident) likely_tautology_prefixes andalso - is_none (run_some_atp ctxt + is_none (run_some_atp ctxt format [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) - | is_problem_line_tautology _ _ = false + | is_problem_line_tautology _ _ _ = false structure String_Graph = Graph(type key = string val ord = string_ord); @@ -148,21 +150,41 @@ if heading = factsN then (heading, order_facts ord lines) :: problem else (heading, lines) :: order_problem_facts ord problem -fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name = +(* A fairly random selection of types used for monomorphizing. *) +val ground_types = + [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, + @{typ unit}] + +fun ground_type_for_tvar _ [] tvar = + raise TYPE ("ground_type_for_sorts", [TVar tvar], []) + | ground_type_for_tvar thy (T :: Ts) tvar = + if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T + else ground_type_for_tvar thy Ts tvar + +fun monomorphize_term ctxt t = + let val thy = Proof_Context.theory_of ctxt in + t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) + handle TYPE _ => @{prop True} + end + +fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = let - val format = FOF val type_enc = type_enc |> type_enc_from_string Sound + |> adjust_type_enc format + val mono = polymorphism_of_type_enc type_enc <> Polymorphic val path = file_name |> Path.explode val _ = File.write path "" val facts = facts_of thy val (atp_problem, _, _, _, _, _, _) = facts - |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) + |> map (fn ((_, loc), th) => + ((Thm.get_name_hint th, loc), + th |> prop_of |> mono ? monomorphize_term ctxt)) |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN false true [] @{prop False} val atp_problem = atp_problem - |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) + |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) val all_names = facts |> map (Thm.get_name_hint o snd) val infers = facts |> map (fn (_, th) => @@ -186,9 +208,10 @@ (ordered_names ~~ (1 upto length ordered_names)) val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) val atp_problem = - atp_problem |> add_inferences_to_problem infers - |> order_problem_facts name_ord - val ss = lines_for_atp_problem FOF atp_problem + atp_problem + |> (case format of DFG _ => I | _ => add_inferences_to_problem infers) + |> order_problem_facts name_ord + val ss = lines_for_atp_problem format atp_problem val _ = app (File.append path) ss in () end