147 fun order_problem_facts _ [] = [] |
147 fun order_problem_facts _ [] = [] |
148 | order_problem_facts ord ((heading, lines) :: problem) = |
148 | order_problem_facts ord ((heading, lines) :: problem) = |
149 if heading = factsN then (heading, order_facts ord lines) :: problem |
149 if heading = factsN then (heading, order_facts ord lines) :: problem |
150 else (heading, lines) :: order_problem_facts ord problem |
150 else (heading, lines) :: order_problem_facts ord problem |
151 |
151 |
152 fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name = |
152 fun generate_tptp_inference_file_for_theory ctxt thy type_enc file_name = |
153 let |
153 let |
154 val format = FOF |
154 val format = FOF |
155 val type_sys = type_sys |> type_sys_from_string |
155 val type_enc = type_enc |> type_enc_from_string |
156 val path = file_name |> Path.explode |
156 val path = file_name |> Path.explode |
157 val _ = File.write path "" |
157 val _ = File.write path "" |
158 val facts = facts_of thy |
158 val facts = facts_of thy |
159 val (atp_problem, _, _, _, _, _, _) = |
159 val (atp_problem, _, _, _, _, _, _) = |
160 facts |
160 facts |
161 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) |
161 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) |
162 |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false |
162 |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true false |
163 true [] @{prop False} |
163 true [] @{prop False} |
164 val atp_problem = |
164 val atp_problem = |
165 atp_problem |
165 atp_problem |
166 |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) |
166 |> map (apsnd (filter_out (is_problem_line_tautology ctxt))) |
167 val all_names = facts |> map (Thm.get_name_hint o snd) |
167 val all_names = facts |> map (Thm.get_name_hint o snd) |