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