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