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 format = ATP_Problem.FOF |
|
93 val type_sys = |
|
94 Sledgehammer_ATP_Translate.Preds |
|
95 (Sledgehammer_ATP_Translate.Polymorphic, |
|
96 if full_types then Sledgehammer_ATP_Translate.All_Types |
|
97 else Sledgehammer_ATP_Translate.Const_Arg_Types, |
|
98 Sledgehammer_ATP_Translate.Heavy) |
93 val path = file_name |> Path.explode |
99 val path = file_name |> Path.explode |
94 val _ = File.write path "" |
100 val _ = File.write path "" |
95 val facts0 = facts_of thy |
101 val facts0 = facts_of thy |
96 val facts = |
102 val facts = |
97 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |
103 facts0 |> map_filter (try (fn ((_, loc), (_, th)) => |
98 Sledgehammer_ATP_Translate.translate_atp_fact ctxt format |
104 Sledgehammer_ATP_Translate.translate_atp_fact ctxt format |
99 true ((Thm.get_name_hint th, loc), th))) |
105 type_sys true ((Thm.get_name_hint th, loc), th))) |
100 val type_sys = |
|
101 Sledgehammer_ATP_Translate.Preds |
|
102 (Sledgehammer_ATP_Translate.Polymorphic, |
|
103 if full_types then Sledgehammer_ATP_Translate.All_Types |
|
104 else Sledgehammer_ATP_Translate.Const_Arg_Types, |
|
105 Sledgehammer_ATP_Translate.Heavy) |
|
106 val explicit_apply = false |
106 val explicit_apply = false |
107 val (atp_problem, _, _, _, _, _, _) = |
107 val (atp_problem, _, _, _, _, _, _) = |
108 Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format |
108 Sledgehammer_ATP_Translate.prepare_atp_problem ctxt format |
109 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] |
109 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply [] |
110 @{prop False} facts |
110 @{prop False} facts |