equal
deleted
inserted
replaced
163 | NONE => TrueI |> Isa_Raw |> some |
163 | NONE => TrueI |> Isa_Raw |> some |
164 end |
164 end |
165 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
165 | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" |
166 |
166 |
167 (* Function to generate metis clauses, including comb and type clauses *) |
167 (* Function to generate metis clauses, including comb and type clauses *) |
168 fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses = |
168 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses = |
169 let |
169 let |
170 val type_sys = type_sys_from_string type_sys |
170 val type_enc = type_enc_from_string type_enc |
171 val (conj_clauses, fact_clauses) = |
171 val (conj_clauses, fact_clauses) = |
172 if polymorphism_of_type_sys type_sys = Polymorphic then |
172 if polymorphism_of_type_enc type_enc = Polymorphic then |
173 (conj_clauses, fact_clauses) |
173 (conj_clauses, fact_clauses) |
174 else |
174 else |
175 conj_clauses @ fact_clauses |
175 conj_clauses @ fact_clauses |
176 |> map (pair 0) |
176 |> map (pair 0) |
177 |> rpair ctxt |
177 |> rpair ctxt |
194 (* |
194 (* |
195 val _ = |
195 val _ = |
196 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) |
196 tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) |
197 *) |
197 *) |
198 val (atp_problem, _, _, _, _, _, sym_tab) = |
198 val (atp_problem, _, _, _, _, _, sym_tab) = |
199 prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys true false false |
199 prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false false |
200 false [] @{prop False} props |
200 false [] @{prop False} props |
201 (* |
201 (* |
202 val _ = tracing ("ATP PROBLEM: " ^ |
202 val _ = tracing ("ATP PROBLEM: " ^ |
203 cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) |
203 cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) |
204 *) |
204 *) |