# HG changeset patch # User blanchet # Date 1307423093 -7200 # Node ID c9e87dc92d9ec7f7e000bc46a2ae023f635b6e6a # Parent d90151a666cc94b0067d8d2012c33c0fc27d39f9 renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules diff -r d90151a666cc -r c9e87dc92d9e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jun 07 06:58:52 2011 +0200 +++ b/src/HOL/IsaMakefile Tue Jun 07 07:04:53 2011 +0200 @@ -1046,8 +1046,8 @@ $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ - ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ - ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy \ + ex/ATP_Export.thy ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy \ + ex/BT.thy ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy \ ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \ ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \ ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \ @@ -1068,7 +1068,7 @@ 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/TPTP_Export.thy ex/Transfer_Ex.thy ex/Tree23.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 \ diff -r d90151a666cc -r c9e87dc92d9e src/HOL/ex/ATP_Export.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/ATP_Export.thy Tue Jun 07 07:04:53 2011 +0200 @@ -0,0 +1,36 @@ +theory ATP_Export +imports Complex_Main +uses "atp_export.ML" +begin + +ML {* +val do_it = false; (* switch to true to generate files *) +val thy = @{theory Complex_Main}; +val ctxt = @{context} +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy true + "/tmp/infs_full_types.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy false + "/tmp/infs_partial_types.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_graph_file_for_theory ctxt thy + "/tmp/graph.out" +else + () +*} + +end diff -r d90151a666cc -r c9e87dc92d9e src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Jun 07 06:58:52 2011 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Jun 07 07:04:53 2011 +0200 @@ -12,7 +12,7 @@ "Hebrew", "Chinese", "Serbian", - "TPTP_Export" + "ATP_Export" ]; use_thys [ diff -r d90151a666cc -r c9e87dc92d9e src/HOL/ex/TPTP_Export.thy --- a/src/HOL/ex/TPTP_Export.thy Tue Jun 07 06:58:52 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -theory TPTP_Export -imports Complex_Main -uses "tptp_export.ML" -begin - -ML {* -val do_it = false; (* switch to true to generate files *) -val thy = @{theory Complex_Main}; -val ctxt = @{context} -*} - -ML {* -if do_it then - TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy true - "/tmp/infs_full_types.tptp" -else - () -*} - -ML {* -if do_it then - TPTP_Export.generate_tptp_inference_file_for_theory ctxt thy false - "/tmp/infs_partial_types.tptp" -else - () -*} - -ML {* -if do_it then - TPTP_Export.generate_tptp_graph_file_for_theory ctxt thy - "/tmp/graph.out" -else - () -*} - -end diff -r d90151a666cc -r c9e87dc92d9e src/HOL/ex/atp_export.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/atp_export.ML Tue Jun 07 07:04:53 2011 +0200 @@ -0,0 +1,122 @@ +(* Title: HOL/ex/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 + 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 ATP_Export : ATP_EXPORT = +struct + +val ascii_of = ATP_Translate.ascii_of + +val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of + +fun facts_of thy = + Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty + true (K true) [] [] + +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 + 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 ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ + commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ + commas (map (prefix ATP_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 format = ATP_Problem.FOF + val type_sys = + ATP_Translate.Preds + (ATP_Translate.Polymorphic, + if full_types then ATP_Translate.All_Types + else ATP_Translate.Const_Arg_Types, + ATP_Translate.Heavyweight) + val path = file_name |> Path.explode + val _ = File.write path "" + val facts0 = facts_of thy + val facts = + facts0 |> map (fn ((_, loc), (_, th)) => + ((Thm.get_name_hint th, loc), prop_of th)) + val explicit_apply = NONE + val (atp_problem, _, _, _, _, _, _) = + ATP_Translate.prepare_atp_problem ctxt format + ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true + [] @{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.FOF atp_problem + val _ = app (File.append path) ss + in () end + +end; diff -r d90151a666cc -r c9e87dc92d9e src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Tue Jun 07 06:58:52 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,122 +0,0 @@ -(* 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 ascii_of = ATP_Translate.ascii_of - -val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of - -fun facts_of thy = - Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty - true (K true) [] [] - -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 - 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 ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ - commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ - commas (map (prefix ATP_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 format = ATP_Problem.FOF - val type_sys = - ATP_Translate.Preds - (ATP_Translate.Polymorphic, - if full_types then ATP_Translate.All_Types - else ATP_Translate.Const_Arg_Types, - ATP_Translate.Heavyweight) - val path = file_name |> Path.explode - val _ = File.write path "" - val facts0 = facts_of thy - val facts = - facts0 |> map (fn ((_, loc), (_, th)) => - ((Thm.get_name_hint th, loc), prop_of th)) - val explicit_apply = NONE - val (atp_problem, _, _, _, _, _, _) = - ATP_Translate.prepare_atp_problem ctxt format - ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true - [] @{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.FOF atp_problem - val _ = app (File.append path) ss - in () end - -end;