111 let val thy = Proof_Context.theory_of ctxt in |
111 let val thy = Proof_Context.theory_of ctxt in |
112 t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
112 t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) |
113 handle TYPE _ => @{prop True} |
113 handle TYPE _ => @{prop True} |
114 end |
114 end |
115 |
115 |
116 fun all_non_tautological_facts_of thy css_table = |
|
117 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |
|
118 |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd) |
|
119 |
|
120 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = |
116 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = |
121 let |
117 let |
122 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
118 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
123 val type_enc = |
119 val type_enc = |
124 type_enc |> type_enc_from_string Strict |
120 type_enc |> type_enc_from_string Strict |
125 |> adjust_type_enc format |
121 |> adjust_type_enc format |
126 val mono = not (is_type_enc_polymorphic type_enc) |
122 val mono = not (is_type_enc_polymorphic type_enc) |
127 val path = file_name |> Path.explode |
123 val path = file_name |> Path.explode |
128 val _ = File.write path "" |
124 val _ = File.write path "" |
129 val facts = all_non_tautological_facts_of thy css_table |
125 val facts = |
|
126 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |
130 val atp_problem = |
127 val atp_problem = |
131 facts |
128 facts |
132 |> map (fn ((_, loc), th) => |
129 |> map (fn ((_, loc), th) => |
133 ((Thm.get_name_hint th, loc), |
130 ((Thm.get_name_hint th, loc), |
134 th |> prop_of |> mono ? monomorphize_term ctxt)) |
131 th |> prop_of |> mono ? monomorphize_term ctxt)) |