# HG changeset patch # User blanchet # Date 1327336832 -3600 # Node ID 484dc68c8c8925d481de29ffcd48e3be9fa77ece # Parent 0b8b73b49848da0ee667f0c8c2b63111c5d4440e renamed theory exporter diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jan 23 17:40:32 2012 +0100 +++ b/src/HOL/IsaMakefile Mon Jan 23 17:40:32 2012 +0100 @@ -1169,9 +1169,9 @@ $(LOG)/HOL-TPTP.gz: \ $(OUT)/HOL \ TPTP/ROOT.ML \ - TPTP/ATP_Export.thy \ - TPTP/CASC_Setup.thy \ - TPTP/atp_export.ML + TPTP/atp_theory_export.ML \ + TPTP/ATP_Theory_Export.thy \ + TPTP/CASC_Setup.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/TPTP/ATP_Export.thy --- a/src/HOL/TPTP/ATP_Export.thy Mon Jan 23 17:40:32 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -theory ATP_Export -imports Complex_Main -uses "atp_export.ML" -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} -*} - -ML {* -if do_it then - "/tmp/axs_mono_simple.dfg" - |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) - "mono_simple" -else - () -*} - -ML {* -if do_it then - "/tmp/infs_poly_guards.tptp" - |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" -else - () -*} - -ML {* -if do_it then - "/tmp/infs_poly_tags.tptp" - |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags" -else - () -*} - -ML {* -if do_it then - "/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 - () -*} - -end diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/TPTP/ATP_Theory_Export.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Mon Jan 23 17:40:32 2012 +0100 @@ -0,0 +1,63 @@ +(* Title: HOL/TPTP/ATP_Theory_Export.thy + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* ATP Theory Exporter *} + +theory ATP_Theory_Export +imports Complex_Main +uses "atp_theory_export.ML" +begin + +ML {* +open ATP_Problem; +open ATP_Theory_Export; +*} + +ML {* +val do_it = false; (* switch to "true" to generate the files *) +val thy = @{theory Complex_Main}; +val ctxt = @{context} +*} + +ML {* +if do_it then + "/tmp/axs_mono_simple.dfg" + |> generate_tptp_inference_file_for_theory ctxt thy (DFG DFG_Sorted) + "mono_simple" +else + () +*} + +ML {* +if do_it then + "/tmp/infs_poly_guards.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_guards" +else + () +*} + +ML {* +if do_it then + "/tmp/infs_poly_tags.tptp" + |> generate_tptp_inference_file_for_theory ctxt thy FOF "poly_tags" +else + () +*} + +ML {* +if do_it then + "/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 + () +*} + +end diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/TPTP/ROOT.ML --- a/src/HOL/TPTP/ROOT.ML Mon Jan 23 17:40:32 2012 +0100 +++ b/src/HOL/TPTP/ROOT.ML Mon Jan 23 17:40:32 2012 +0100 @@ -7,7 +7,7 @@ *) use_thys [ - "ATP_Export" + "ATP_Theory_Export" ]; Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs) diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Mon Jan 23 17:40:32 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,219 +0,0 @@ -(* Title: HOL/TPTP/atp_export.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2011 - -Export Isabelle theories as first-order TPTP inferences, exploiting -Sledgehammer's translation. -*) - -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 -> atp_format -> string -> string -> unit -end; - -structure ATP_Export : ATP_EXPORT = -struct - -open ATP_Problem -open ATP_Proof -open ATP_Problem_Generate -open ATP_Systems - -val fact_name_of = prefix fact_prefix o ascii_of - -fun facts_of thy = - Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) false - Symtab.empty true [] [] - |> filter (curry (op =) @{typ bool} o fastype_of - o Object_Logic.atomize_term thy o prop_of o snd) - -(* 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 thm_name all_names f = - let - fun app n (PBody {thms, ...}) = - 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)) orelse - (* uncommon case where the proved theorem occurs twice - (e.g., "Transitive_Closure.trancl_into_trancl") *) - n = 1 andalso name = thm_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 all_names thm = - let - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - val names = - [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect - [Thm.proof_body_of thm] - |> map fact_name_of - in names end - -fun interesting_const_names ctxt = - let val thy = Proof_Context.theory_of ctxt in - Sledgehammer_Filter.const_names_in_fact thy - (Sledgehammer_Provers.is_built_in_const_for_prover ctxt 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 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 - val _ = map do_thm thms - in () end - -fun inference_term [] = NONE - | inference_term 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 - (Formula (ident, Axiom, phi, NONE, NONE)) = - Formula (ident, Lemma, phi, inference infers ident, NONE) - | add_inferences_to_problem_line _ line = line -fun add_inferences_to_problem infers = - map (apsnd (map (add_inferences_to_problem_line infers))) - -fun ident_of_problem_line (Decl (ident, _, _)) = ident - | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident - -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 (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 []) ^ " " ^ - File.shell_path prob_file - in - TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command - |> fst - |> extract_tstplike_proof_and_outcome false true proof_delims - known_failures - |> snd - end - handle TimeLimit.TimeOut => SOME TimedOut - -val likely_tautology_prefixes = - [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] - |> map (fact_name_of o Context.theory_name) - -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 format - [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) - | is_problem_line_tautology _ _ _ = false - -structure String_Graph = Graph(type key = string val ord = string_ord); - -fun order_facts ord = sort (ord o pairself ident_of_problem_line) -fun order_problem_facts _ [] = [] - | order_problem_facts ord ((heading, lines) :: problem) = - if heading = factsN then (heading, order_facts ord lines) :: problem - else (heading, lines) :: order_problem_facts ord problem - -(* 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 type_enc = type_enc |> type_enc_from_string Strict - |> 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), - th |> prop_of |> mono ? monomorphize_term ctxt)) - |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN - false true [] @{prop False} - |> #1 - val atp_problem = - atp_problem - |> 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) => - (fact_name_of (Thm.get_name_hint 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 |> filter (member (op =) all_atp_problem_names o fst) - |> map (apsnd (filter (member (op =) all_atp_problem_names))) - val ordered_names = - String_Graph.empty - |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names - |> fold (fn (to, froms) => - fold (fn from => String_Graph.add_edge (from, to)) froms) - infers - |> String_Graph.topological_order - val order_tab = - Symtab.empty - |> fold (Symtab.insert (op =)) - (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 - |> (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 - -end; diff -r 0b8b73b49848 -r 484dc68c8c89 src/HOL/TPTP/atp_theory_export.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/atp_theory_export.ML Mon Jan 23 17:40:32 2012 +0100 @@ -0,0 +1,219 @@ +(* Title: HOL/TPTP/atp_theory_export.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2011 + +Export Isabelle theories as first-order TPTP inferences, exploiting +Sledgehammer's translation. +*) + +signature ATP_THEORY_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 -> atp_format -> string -> string -> unit +end; + +structure ATP_Theory_Export : ATP_THEORY_EXPORT = +struct + +open ATP_Problem +open ATP_Proof +open ATP_Problem_Generate +open ATP_Systems + +val fact_name_of = prefix fact_prefix o ascii_of + +fun facts_of thy = + Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) false + Symtab.empty true [] [] + |> filter (curry (op =) @{typ bool} o fastype_of + o Object_Logic.atomize_term thy o prop_of o snd) + +(* 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 thm_name all_names f = + let + fun app n (PBody {thms, ...}) = + 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)) orelse + (* uncommon case where the proved theorem occurs twice + (e.g., "Transitive_Closure.trancl_into_trancl") *) + n = 1 andalso name = thm_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 all_names thm = + let + fun collect (s, _, _) = if s <> "" then insert (op =) s else I + val names = + [] |> fold_body_thms (Thm.get_name_hint thm) all_names collect + [Thm.proof_body_of thm] + |> map fact_name_of + in names end + +fun interesting_const_names ctxt = + let val thy = Proof_Context.theory_of ctxt in + Sledgehammer_Filter.const_names_in_fact thy + (Sledgehammer_Provers.is_built_in_const_for_prover ctxt 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 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 + val _ = map do_thm thms + in () end + +fun inference_term [] = NONE + | inference_term 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 + (Formula (ident, Axiom, phi, NONE, NONE)) = + Formula (ident, Lemma, phi, inference infers ident, NONE) + | add_inferences_to_problem_line _ line = line +fun add_inferences_to_problem infers = + map (apsnd (map (add_inferences_to_problem_line infers))) + +fun ident_of_problem_line (Decl (ident, _, _)) = ident + | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident + +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 (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 []) ^ " " ^ + File.shell_path prob_file + in + TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command + |> fst + |> extract_tstplike_proof_and_outcome false true proof_delims + known_failures + |> snd + end + handle TimeLimit.TimeOut => SOME TimedOut + +val likely_tautology_prefixes = + [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] + |> map (fact_name_of o Context.theory_name) + +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 format + [(factsN, [Formula (ident, Conjecture, phi, NONE, NONE)])]) + | is_problem_line_tautology _ _ _ = false + +structure String_Graph = Graph(type key = string val ord = string_ord); + +fun order_facts ord = sort (ord o pairself ident_of_problem_line) +fun order_problem_facts _ [] = [] + | order_problem_facts ord ((heading, lines) :: problem) = + if heading = factsN then (heading, order_facts ord lines) :: problem + else (heading, lines) :: order_problem_facts ord problem + +(* 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 type_enc = type_enc |> type_enc_from_string Strict + |> 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), + th |> prop_of |> mono ? monomorphize_term ctxt)) + |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combinatorsN + false true [] @{prop False} + |> #1 + val atp_problem = + atp_problem + |> 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) => + (fact_name_of (Thm.get_name_hint 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 |> filter (member (op =) all_atp_problem_names o fst) + |> map (apsnd (filter (member (op =) all_atp_problem_names))) + val ordered_names = + String_Graph.empty + |> fold (String_Graph.new_node o rpair ()) all_atp_problem_names + |> fold (fn (to, froms) => + fold (fn from => String_Graph.add_edge (from, to)) froms) + infers + |> String_Graph.topological_order + val order_tab = + Symtab.empty + |> fold (Symtab.insert (op =)) + (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 + |> (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 + +end;