|
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML |
|
2 Author: Fabian Immler, TU Muenchen |
|
3 Author: Makarius |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 |
|
6 Translation of HOL to FOL. |
|
7 *) |
|
8 |
|
9 signature SLEDGEHAMMER_TRANSLATE = |
|
10 sig |
|
11 type 'a problem = 'a ATP_Problem.problem |
|
12 |
|
13 val axiom_prefix : string |
|
14 val conjecture_prefix : string |
|
15 val helper_prefix : string |
|
16 val class_rel_clause_prefix : string |
|
17 val arity_clause_prefix : string |
|
18 val tfrees_name : string |
|
19 val prepare_problem : |
|
20 Proof.context -> bool -> bool -> bool -> bool -> term list -> term |
|
21 -> (string * thm) list |
|
22 -> string problem * string Symtab.table * int * string Vector.vector |
|
23 end; |
|
24 |
|
25 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = |
|
26 struct |
|
27 |
|
28 open ATP_Problem |
|
29 open Metis_Clauses |
|
30 open Sledgehammer_Util |
|
31 |
|
32 val axiom_prefix = "ax_" |
|
33 val conjecture_prefix = "conj_" |
|
34 val helper_prefix = "help_" |
|
35 val class_rel_clause_prefix = "clrel_"; |
|
36 val arity_clause_prefix = "arity_" |
|
37 val tfrees_name = "tfrees" |
|
38 |
|
39 (* Freshness almost guaranteed! *) |
|
40 val sledgehammer_weak_prefix = "Sledgehammer:" |
|
41 |
|
42 datatype fol_formula = |
|
43 FOLFormula of {name: string, |
|
44 kind: kind, |
|
45 combformula: (name, combterm) formula, |
|
46 ctypes_sorts: typ list} |
|
47 |
|
48 fun mk_anot phi = AConn (ANot, [phi]) |
|
49 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) |
|
50 fun mk_ahorn [] phi = phi |
|
51 | mk_ahorn (phi :: phis) psi = |
|
52 AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) |
|
53 |
|
54 fun combformula_for_prop thy = |
|
55 let |
|
56 val do_term = combterm_from_term thy |
|
57 fun do_quant bs q s T t' = |
|
58 do_formula ((s, T) :: bs) t' |
|
59 #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) |
|
60 and do_conn bs c t1 t2 = |
|
61 do_formula bs t1 ##>> do_formula bs t2 |
|
62 #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) |
|
63 and do_formula bs t = |
|
64 case t of |
|
65 @{const Not} $ t1 => |
|
66 do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) |
|
67 | Const (@{const_name All}, _) $ Abs (s, T, t') => |
|
68 do_quant bs AForall s T t' |
|
69 | Const (@{const_name Ex}, _) $ Abs (s, T, t') => |
|
70 do_quant bs AExists s T t' |
|
71 | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 |
|
72 | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 |
|
73 | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 |
|
74 | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => |
|
75 do_conn bs AIff t1 t2 |
|
76 | _ => (fn ts => do_term bs (Envir.eta_contract t) |
|
77 |>> AAtom ||> union (op =) ts) |
|
78 in do_formula [] end |
|
79 |
|
80 (* Converts an elim-rule into an equivalent theorem that does not have the |
|
81 predicate variable. Leaves other theorems unchanged. We simply instantiate |
|
82 the conclusion variable to False. (Cf. "transform_elim_term" in |
|
83 "ATP_Systems".) *) |
|
84 fun transform_elim_term t = |
|
85 case Logic.strip_imp_concl t of |
|
86 @{const Trueprop} $ Var (z, @{typ bool}) => |
|
87 subst_Vars [(z, @{const False})] t |
|
88 | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t |
|
89 | _ => t |
|
90 |
|
91 fun presimplify_term thy = |
|
92 Skip_Proof.make_thm thy |
|
93 #> Meson.presimplify |
|
94 #> prop_of |
|
95 |
|
96 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j |
|
97 fun conceal_bounds Ts t = |
|
98 subst_bounds (map (Free o apfst concealed_bound_name) |
|
99 (0 upto length Ts - 1 ~~ Ts), t) |
|
100 fun reveal_bounds Ts = |
|
101 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) |
|
102 (0 upto length Ts - 1 ~~ Ts)) |
|
103 |
|
104 fun introduce_combinators_in_term ctxt kind t = |
|
105 let |
|
106 val thy = ProofContext.theory_of ctxt |
|
107 fun aux Ts t = |
|
108 case t of |
|
109 @{const Not} $ t1 => @{const Not} $ aux Ts t1 |
|
110 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => |
|
111 t0 $ Abs (s, T, aux (T :: Ts) t') |
|
112 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => |
|
113 t0 $ Abs (s, T, aux (T :: Ts) t') |
|
114 | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 |
|
115 | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 |
|
116 | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 |
|
117 | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) |
|
118 $ t1 $ t2 => |
|
119 t0 $ aux Ts t1 $ aux Ts t2 |
|
120 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then |
|
121 t |
|
122 else |
|
123 let |
|
124 val t = t |> conceal_bounds Ts |
|
125 |> Envir.eta_contract |
|
126 val ([t], ctxt') = Variable.import_terms true [t] ctxt |
|
127 in |
|
128 t |> cterm_of thy |
|
129 |> Clausifier.introduce_combinators_in_cterm |
|
130 |> singleton (Variable.export ctxt' ctxt) |
|
131 |> prop_of |> Logic.dest_equals |> snd |
|
132 |> reveal_bounds Ts |
|
133 end |
|
134 in t |> not (Meson.is_fol_term thy t) ? aux [] end |
|
135 handle THM _ => |
|
136 (* A type variable of sort "{}" will make abstraction fail. *) |
|
137 case kind of |
|
138 Axiom => HOLogic.true_const |
|
139 | Conjecture => HOLogic.false_const |
|
140 |
|
141 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the |
|
142 same in Sledgehammer to prevent the discovery of unreplable proofs. *) |
|
143 fun freeze_term t = |
|
144 let |
|
145 fun aux (t $ u) = aux t $ aux u |
|
146 | aux (Abs (s, T, t)) = Abs (s, T, aux t) |
|
147 | aux (Var ((s, i), T)) = |
|
148 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) |
|
149 | aux t = t |
|
150 in t |> exists_subterm is_Var t ? aux end |
|
151 |
|
152 (* making axiom and conjecture formulas *) |
|
153 fun make_formula ctxt presimp (name, kind, t) = |
|
154 let |
|
155 val thy = ProofContext.theory_of ctxt |
|
156 val t = t |> transform_elim_term |
|
157 |> Object_Logic.atomize_term thy |
|
158 val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop |
|
159 |> extensionalize_term |
|
160 |> presimp ? presimplify_term thy |
|
161 |> perhaps (try (HOLogic.dest_Trueprop)) |
|
162 |> introduce_combinators_in_term ctxt kind |
|
163 |> kind = Conjecture ? freeze_term |
|
164 val (combformula, ctypes_sorts) = combformula_for_prop thy t [] |
|
165 in |
|
166 FOLFormula {name = name, combformula = combformula, kind = kind, |
|
167 ctypes_sorts = ctypes_sorts} |
|
168 end |
|
169 |
|
170 fun make_axiom ctxt presimp (name, th) = |
|
171 (name, make_formula ctxt presimp (name, Axiom, prop_of th)) |
|
172 fun make_conjectures ctxt ts = |
|
173 map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t)) |
|
174 (0 upto length ts - 1) ts |
|
175 |
|
176 (** Helper facts **) |
|
177 |
|
178 fun count_combterm (CombConst ((s, _), _, _)) = |
|
179 Symtab.map_entry s (Integer.add 1) |
|
180 | count_combterm (CombVar _) = I |
|
181 | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] |
|
182 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi |
|
183 | count_combformula (AConn (_, phis)) = fold count_combformula phis |
|
184 | count_combformula (AAtom tm) = count_combterm tm |
|
185 fun count_fol_formula (FOLFormula {combformula, ...}) = |
|
186 count_combformula combformula |
|
187 |
|
188 val optional_helpers = |
|
189 [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), |
|
190 (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), |
|
191 (["c_COMBS"], @{thms COMBS_def})] |
|
192 val optional_typed_helpers = |
|
193 [(["c_True", "c_False"], @{thms True_or_False}), |
|
194 (["c_If"], @{thms if_True if_False True_or_False})] |
|
195 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} |
|
196 |
|
197 val init_counters = |
|
198 Symtab.make (maps (maps (map (rpair 0) o fst)) |
|
199 [optional_helpers, optional_typed_helpers]) |
|
200 |
|
201 fun get_helper_facts ctxt is_FO full_types conjectures axioms = |
|
202 let |
|
203 val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters |
|
204 fun is_needed c = the (Symtab.lookup ct c) > 0 |
|
205 in |
|
206 (optional_helpers |
|
207 |> full_types ? append optional_typed_helpers |
|
208 |> maps (fn (ss, ths) => |
|
209 if exists is_needed ss then map (`Thm.get_name_hint) ths |
|
210 else [])) @ |
|
211 (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) |
|
212 |> map (snd o make_axiom ctxt false) |
|
213 end |
|
214 |
|
215 fun meta_not t = @{const "==>"} $ t $ @{prop False} |
|
216 |
|
217 fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = |
|
218 let |
|
219 val thy = ProofContext.theory_of ctxt |
|
220 val axiom_ts = map (prop_of o snd) axioms |
|
221 val hyp_ts = |
|
222 if null hyp_ts then |
|
223 [] |
|
224 else |
|
225 (* Remove existing axioms from the conjecture, as this can dramatically |
|
226 boost an ATP's performance (for some reason). *) |
|
227 let |
|
228 val axiom_table = fold (Termtab.update o rpair ()) axiom_ts |
|
229 Termtab.empty |
|
230 in hyp_ts |> filter_out (Termtab.defined axiom_table) end |
|
231 val goal_t = Logic.list_implies (hyp_ts, concl_t) |
|
232 val is_FO = Meson.is_fol_term thy goal_t |
|
233 val subs = tfree_classes_of_terms [goal_t] |
|
234 val supers = tvar_classes_of_terms axiom_ts |
|
235 val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) |
|
236 (* TFrees in the conjecture; TVars in the axioms *) |
|
237 val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt |
|
238 val (axiom_names, axioms) = |
|
239 ListPair.unzip (map (make_axiom ctxt true) axioms) |
|
240 val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms |
|
241 val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
|
242 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
|
243 in |
|
244 (Vector.fromList axiom_names, |
|
245 (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) |
|
246 end |
|
247 |
|
248 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) |
|
249 |
|
250 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) |
|
251 | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) |
|
252 | fo_term_for_combtyp (CombType (name, tys)) = |
|
253 ATerm (name, map fo_term_for_combtyp tys) |
|
254 |
|
255 fun fo_literal_for_type_literal (TyLitVar (class, name)) = |
|
256 (true, ATerm (class, [ATerm (name, [])])) |
|
257 | fo_literal_for_type_literal (TyLitFree (class, name)) = |
|
258 (true, ATerm (class, [ATerm (name, [])])) |
|
259 |
|
260 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot |
|
261 |
|
262 fun fo_term_for_combterm full_types = |
|
263 let |
|
264 fun aux top_level u = |
|
265 let |
|
266 val (head, args) = strip_combterm_comb u |
|
267 val (x, ty_args) = |
|
268 case head of |
|
269 CombConst (name as (s, s'), _, ty_args) => |
|
270 if s = "equal" then |
|
271 (if top_level andalso length args = 2 then name |
|
272 else ("c_fequal", @{const_name fequal}), []) |
|
273 else if top_level then |
|
274 case s of |
|
275 "c_False" => (("$false", s'), []) |
|
276 | "c_True" => (("$true", s'), []) |
|
277 | _ => (name, if full_types then [] else ty_args) |
|
278 else |
|
279 (name, if full_types then [] else ty_args) |
|
280 | CombVar (name, _) => (name, []) |
|
281 | CombApp _ => raise Fail "impossible \"CombApp\"" |
|
282 val t = ATerm (x, map fo_term_for_combtyp ty_args @ |
|
283 map (aux false) args) |
|
284 in |
|
285 if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t |
|
286 end |
|
287 in aux true end |
|
288 |
|
289 fun formula_for_combformula full_types = |
|
290 let |
|
291 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) |
|
292 | aux (AConn (c, phis)) = AConn (c, map aux phis) |
|
293 | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) |
|
294 in aux end |
|
295 |
|
296 fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = |
|
297 mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) |
|
298 (type_literals_for_types ctypes_sorts)) |
|
299 (formula_for_combformula full_types combformula) |
|
300 |
|
301 fun problem_line_for_fact prefix full_types |
|
302 (formula as FOLFormula {name, kind, ...}) = |
|
303 Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) |
|
304 |
|
305 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, |
|
306 superclass, ...}) = |
|
307 let val ty_arg = ATerm (("T", "T"), []) in |
|
308 Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, |
|
309 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), |
|
310 AAtom (ATerm (superclass, [ty_arg]))])) |
|
311 end |
|
312 |
|
313 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = |
|
314 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) |
|
315 | fo_literal_for_arity_literal (TVarLit (c, sort)) = |
|
316 (false, ATerm (c, [ATerm (sort, [])])) |
|
317 |
|
318 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, |
|
319 ...}) = |
|
320 Fof (arity_clause_prefix ^ ascii_of name, Axiom, |
|
321 mk_ahorn (map (formula_for_fo_literal o apfst not |
|
322 o fo_literal_for_arity_literal) premLits) |
|
323 (formula_for_fo_literal |
|
324 (fo_literal_for_arity_literal conclLit))) |
|
325 |
|
326 fun problem_line_for_conjecture full_types |
|
327 (FOLFormula {name, kind, combformula, ...}) = |
|
328 Fof (conjecture_prefix ^ name, kind, |
|
329 formula_for_combformula full_types combformula) |
|
330 |
|
331 fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = |
|
332 map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) |
|
333 |
|
334 fun problem_line_for_free_type lit = |
|
335 Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) |
|
336 fun problem_lines_for_free_types conjectures = |
|
337 let |
|
338 val litss = map free_type_literals_for_conjecture conjectures |
|
339 val lits = fold (union (op =)) litss [] |
|
340 in map problem_line_for_free_type lits end |
|
341 |
|
342 (** "hBOOL" and "hAPP" **) |
|
343 |
|
344 type const_info = {min_arity: int, max_arity: int, sub_level: bool} |
|
345 |
|
346 fun consider_term top_level (ATerm ((s, _), ts)) = |
|
347 (if is_tptp_variable s then |
|
348 I |
|
349 else |
|
350 let val n = length ts in |
|
351 Symtab.map_default |
|
352 (s, {min_arity = n, max_arity = 0, sub_level = false}) |
|
353 (fn {min_arity, max_arity, sub_level} => |
|
354 {min_arity = Int.min (n, min_arity), |
|
355 max_arity = Int.max (n, max_arity), |
|
356 sub_level = sub_level orelse not top_level}) |
|
357 end) |
|
358 #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts |
|
359 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi |
|
360 | consider_formula (AConn (_, phis)) = fold consider_formula phis |
|
361 | consider_formula (AAtom tm) = consider_term true tm |
|
362 |
|
363 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi |
|
364 fun consider_problem problem = fold (fold consider_problem_line o snd) problem |
|
365 |
|
366 fun const_table_for_problem explicit_apply problem = |
|
367 if explicit_apply then NONE |
|
368 else SOME (Symtab.empty |> consider_problem problem) |
|
369 |
|
370 fun min_arity_of thy full_types NONE s = |
|
371 (if s = "equal" orelse s = type_wrapper_name orelse |
|
372 String.isPrefix type_const_prefix s orelse |
|
373 String.isPrefix class_prefix s then |
|
374 16383 (* large number *) |
|
375 else if full_types then |
|
376 0 |
|
377 else case strip_prefix_and_undo_ascii const_prefix s of |
|
378 SOME s' => num_type_args thy (invert_const s') |
|
379 | NONE => 0) |
|
380 | min_arity_of _ _ (SOME the_const_tab) s = |
|
381 case Symtab.lookup the_const_tab s of |
|
382 SOME ({min_arity, ...} : const_info) => min_arity |
|
383 | NONE => 0 |
|
384 |
|
385 fun full_type_of (ATerm ((s, _), [ty, _])) = |
|
386 if s = type_wrapper_name then ty else raise Fail "expected type wrapper" |
|
387 | full_type_of _ = raise Fail "expected type wrapper" |
|
388 |
|
389 fun list_hAPP_rev _ t1 [] = t1 |
|
390 | list_hAPP_rev NONE t1 (t2 :: ts2) = |
|
391 ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) |
|
392 | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = |
|
393 let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, |
|
394 [full_type_of t2, ty]) in |
|
395 ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) |
|
396 end |
|
397 |
|
398 fun repair_applications_in_term thy full_types const_tab = |
|
399 let |
|
400 fun aux opt_ty (ATerm (name as (s, _), ts)) = |
|
401 if s = type_wrapper_name then |
|
402 case ts of |
|
403 [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) |
|
404 | _ => raise Fail "malformed type wrapper" |
|
405 else |
|
406 let |
|
407 val ts = map (aux NONE) ts |
|
408 val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts |
|
409 in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end |
|
410 in aux NONE end |
|
411 |
|
412 fun boolify t = ATerm (`I "hBOOL", [t]) |
|
413 |
|
414 (* True if the constant ever appears outside of the top-level position in |
|
415 literals, or if it appears with different arities (e.g., because of different |
|
416 type instantiations). If false, the constant always receives all of its |
|
417 arguments and is used as a predicate. *) |
|
418 fun is_predicate NONE s = |
|
419 s = "equal" orelse String.isPrefix type_const_prefix s orelse |
|
420 String.isPrefix class_prefix s |
|
421 | is_predicate (SOME the_const_tab) s = |
|
422 case Symtab.lookup the_const_tab s of |
|
423 SOME {min_arity, max_arity, sub_level} => |
|
424 not sub_level andalso min_arity = max_arity |
|
425 | NONE => false |
|
426 |
|
427 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = |
|
428 if s = type_wrapper_name then |
|
429 case ts of |
|
430 [_, t' as ATerm ((s', _), _)] => |
|
431 if is_predicate const_tab s' then t' else boolify t |
|
432 | _ => raise Fail "malformed type wrapper" |
|
433 else |
|
434 t |> not (is_predicate const_tab s) ? boolify |
|
435 |
|
436 fun close_universally phi = |
|
437 let |
|
438 fun term_vars bounds (ATerm (name as (s, _), tms)) = |
|
439 (is_tptp_variable s andalso not (member (op =) bounds name)) |
|
440 ? insert (op =) name |
|
441 #> fold (term_vars bounds) tms |
|
442 fun formula_vars bounds (AQuant (q, xs, phi)) = |
|
443 formula_vars (xs @ bounds) phi |
|
444 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis |
|
445 | formula_vars bounds (AAtom tm) = term_vars bounds tm |
|
446 in |
|
447 case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) |
|
448 end |
|
449 |
|
450 fun repair_formula thy explicit_forall full_types const_tab = |
|
451 let |
|
452 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) |
|
453 | aux (AConn (c, phis)) = AConn (c, map aux phis) |
|
454 | aux (AAtom tm) = |
|
455 AAtom (tm |> repair_applications_in_term thy full_types const_tab |
|
456 |> repair_predicates_in_term const_tab) |
|
457 in aux #> explicit_forall ? close_universally end |
|
458 |
|
459 fun repair_problem_line thy explicit_forall full_types const_tab |
|
460 (Fof (ident, kind, phi)) = |
|
461 Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) |
|
462 fun repair_problem_with_const_table thy = |
|
463 map o apsnd o map ooo repair_problem_line thy |
|
464 |
|
465 fun repair_problem thy explicit_forall full_types explicit_apply problem = |
|
466 repair_problem_with_const_table thy explicit_forall full_types |
|
467 (const_table_for_problem explicit_apply problem) problem |
|
468 |
|
469 fun prepare_problem ctxt readable_names explicit_forall full_types |
|
470 explicit_apply hyp_ts concl_t axiom_ts = |
|
471 let |
|
472 val thy = ProofContext.theory_of ctxt |
|
473 val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, |
|
474 arity_clauses)) = |
|
475 prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts |
|
476 val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms |
|
477 val helper_lines = |
|
478 map (problem_line_for_fact helper_prefix full_types) helper_facts |
|
479 val conjecture_lines = |
|
480 map (problem_line_for_conjecture full_types) conjectures |
|
481 val tfree_lines = problem_lines_for_free_types conjectures |
|
482 val class_rel_lines = |
|
483 map problem_line_for_class_rel_clause class_rel_clauses |
|
484 val arity_lines = map problem_line_for_arity_clause arity_clauses |
|
485 (* Reordering these might or might not confuse the proof reconstruction |
|
486 code or the SPASS Flotter hack. *) |
|
487 val problem = |
|
488 [("Relevant facts", axiom_lines), |
|
489 ("Class relationships", class_rel_lines), |
|
490 ("Arity declarations", arity_lines), |
|
491 ("Helper facts", helper_lines), |
|
492 ("Conjectures", conjecture_lines), |
|
493 ("Type variables", tfree_lines)] |
|
494 |> repair_problem thy explicit_forall full_types explicit_apply |
|
495 val (problem, pool) = nice_tptp_problem readable_names problem |
|
496 val conjecture_offset = |
|
497 length axiom_lines + length class_rel_lines + length arity_lines |
|
498 + length helper_lines |
|
499 in |
|
500 (problem, |
|
501 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, |
|
502 conjecture_offset, axiom_names) |
|
503 end |
|
504 |
|
505 end; |