87 val add_inferences_to_problem = |
87 val add_inferences_to_problem = |
88 map o apsnd o map o add_inferences_to_problem_line |
88 map o apsnd o map o add_inferences_to_problem_line |
89 |
89 |
90 fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name = |
90 fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name = |
91 let |
91 let |
|
92 val format = ATP_Problem.FOF |
92 val path = file_name |> Path.explode |
93 val path = file_name |> Path.explode |
93 val _ = File.write path "" |
94 val _ = File.write path "" |
94 val facts0 = facts_of thy |
95 val facts0 = facts_of thy |
95 val facts = |
96 val facts = |
96 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |
97 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |
97 Sledgehammer_ATP_Translate.translate_atp_fact ctxt true |
98 Sledgehammer_ATP_Translate.translate_atp_fact ctxt format |
98 ((Thm.get_name_hint th, loc), th))) |
99 true ((Thm.get_name_hint th, loc), th))) |
99 val type_sys = |
100 val type_sys = |
100 Sledgehammer_ATP_Translate.Preds |
101 Sledgehammer_ATP_Translate.Preds |
101 (Sledgehammer_ATP_Translate.Polymorphic, |
102 (Sledgehammer_ATP_Translate.Polymorphic, |
102 if full_types then Sledgehammer_ATP_Translate.All_Types |
103 if full_types then Sledgehammer_ATP_Translate.All_Types |
103 else Sledgehammer_ATP_Translate.Const_Arg_Types, |
104 else Sledgehammer_ATP_Translate.Const_Arg_Types, |
104 Sledgehammer_ATP_Translate.Heavy) |
105 Sledgehammer_ATP_Translate.Heavy) |
105 val explicit_apply = false |
106 val explicit_apply = false |
106 val (atp_problem, _, _, _, _, _, _) = |
107 val (atp_problem, _, _, _, _, _, _) = |
107 Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.FOF |
108 Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format |
108 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] |
109 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] |
109 @{prop False} facts |
110 @{prop False} facts |
110 val infers = |
111 val infers = |
111 facts0 |> map (fn (_, (_, th)) => |
112 facts0 |> map (fn (_, (_, th)) => |
112 (fact_name_of (Thm.get_name_hint th), |
113 (fact_name_of (Thm.get_name_hint th), |