1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Translation of HOL to FOL for Sledgehammer.
9 signature SLEDGEHAMMER_ATP_TRANSLATE =
11 type 'a fo_term = 'a ATP_Problem.fo_term
12 type 'a problem = 'a ATP_Problem.problem
13 type locality = Sledgehammer_Filter.locality
15 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
17 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
19 datatype type_system =
20 Simple of type_level |
21 Preds of polymorphism * type_level |
22 Tags of polymorphism * type_level
24 type translated_formula
26 val readable_names : bool Config.T
27 val fact_prefix : string
28 val conjecture_prefix : string
29 val predicator_base : string
30 val explicit_app_base : string
31 val type_pred_base : string
32 val tff_type_prefix : string
33 val type_sys_from_string : string -> type_system
34 val polymorphism_of_type_sys : type_system -> polymorphism
35 val level_of_type_sys : type_system -> type_level
36 val is_type_sys_virtually_sound : type_system -> bool
37 val is_type_sys_fairly_sound : type_system -> bool
38 val num_atp_type_args : theory -> type_system -> string -> int
39 val unmangled_const : string -> string * string fo_term list
40 val translate_atp_fact :
41 Proof.context -> bool -> (string * locality) * thm
42 -> translated_formula option * ((string * locality) * thm)
43 val prepare_atp_problem :
44 Proof.context -> type_system -> bool -> term list -> term
45 -> (translated_formula option * ((string * 'a) * thm)) list
46 -> string problem * string Symtab.table * int * int
47 * (string * 'a) list vector
48 val atp_problem_weights : string problem -> (string * real) list
51 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
56 open Sledgehammer_Util
57 open Sledgehammer_Filter
60 val generate_useful_info = false
62 (* Readable names are often much shorter, especially if types are mangled in
63 names. Also, the logic for generating legal SNARK sort names is only
64 implemented for readable names. Finally, readable names are, well, more
65 readable. For these reason, they are enabled by default. *)
67 Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
69 val type_decl_prefix = "type_"
70 val sym_decl_prefix = "sym_"
71 val fact_prefix = "fact_"
72 val conjecture_prefix = "conj_"
73 val helper_prefix = "help_"
74 val class_rel_clause_prefix = "crel_";
75 val arity_clause_prefix = "arity_"
76 val tfree_prefix = "tfree_"
78 val predicator_base = "hBOOL"
79 val explicit_app_base = "hAPP"
80 val type_pred_base = "is"
81 val tff_type_prefix = "ty_"
83 fun make_tff_type s = tff_type_prefix ^ ascii_of s
85 (* official TPTP syntax *)
86 val tptp_tff_type_of_types = "$tType"
87 val tptp_tff_bool_type = "$o"
88 val tptp_false = "$false"
89 val tptp_true = "$true"
91 (* Freshness almost guaranteed! *)
92 val sledgehammer_weak_prefix = "Sledgehammer:"
94 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
96 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
98 datatype type_system =
99 Simple of type_level |
100 Preds of polymorphism * type_level |
101 Tags of polymorphism * type_level
103 fun try_unsuffixes ss s =
104 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
106 fun type_sys_from_string s =
107 (case try (unprefix "mangled_") s of
108 SOME s => (Mangled_Monomorphic, s)
110 case try (unprefix "mono_") s of
111 SOME s => (Monomorphic, s)
112 | NONE => (Polymorphic, s))
114 (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
115 case try_unsuffixes ["?", "_query"] s of
116 SOME s => (Nonmonotonic_Types, s)
118 case try_unsuffixes ["!", "_bang"] s of
119 SOME s => (Finite_Types, s)
120 | NONE => (All_Types, s))
121 |> (fn (polymorphism, (level, core)) =>
122 case (core, (polymorphism, level)) of
123 ("simple", (Polymorphic (* naja *), level)) => Simple level
124 | ("preds", extra) => Preds extra
125 | ("tags", extra) => Tags extra
126 | ("args", (_, All_Types (* naja *))) =>
127 Preds (polymorphism, Const_Arg_Types)
128 | ("erased", (Polymorphic, All_Types (* naja *))) =>
129 Preds (polymorphism, No_Types)
130 | _ => error ("Unknown type system: " ^ quote s ^ "."))
132 fun polymorphism_of_type_sys (Simple _) = Mangled_Monomorphic
133 | polymorphism_of_type_sys (Preds (poly, _)) = poly
134 | polymorphism_of_type_sys (Tags (poly, _)) = poly
136 fun level_of_type_sys (Simple level) = level
137 | level_of_type_sys (Preds (_, level)) = level
138 | level_of_type_sys (Tags (_, level)) = level
140 fun is_type_level_virtually_sound level =
141 level = All_Types orelse level = Nonmonotonic_Types
142 val is_type_sys_virtually_sound =
143 is_type_level_virtually_sound o level_of_type_sys
145 fun is_type_level_fairly_sound level =
146 is_type_level_virtually_sound level orelse level = Finite_Types
147 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
149 fun is_type_level_partial level =
150 level = Nonmonotonic_Types orelse level = Finite_Types
152 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
153 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
154 | formula_map f (AAtom tm) = AAtom (f tm)
156 fun formula_fold pos f =
158 fun aux pos (AQuant (_, _, phi)) = aux pos phi
159 | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
160 | aux pos (AConn (AImplies, [phi1, phi2])) =
161 aux (Option.map not pos) phi1 #> aux pos phi2
162 | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
163 | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
164 | aux _ (AConn (_, phis)) = fold (aux NONE) phis
165 | aux pos (AAtom tm) = f pos tm
166 in aux (SOME pos) end
168 type translated_formula =
172 combformula: (name, typ, combterm) formula,
173 atomic_types: typ list}
175 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
176 : translated_formula) =
177 {name = name, locality = locality, kind = kind, combformula = f combformula,
178 atomic_types = atomic_types} : translated_formula
180 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
182 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
184 fun should_omit_type_args type_sys s =
185 s <> type_pred_base andalso s <> type_tag_name andalso
186 (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
188 Tags (_, All_Types) => true
189 | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
190 member (op =) boring_consts s))
192 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
194 fun general_type_arg_policy type_sys =
195 if level_of_type_sys type_sys = No_Types then
197 else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
202 fun type_arg_policy type_sys s =
203 if should_omit_type_args type_sys s then No_Type_Args
204 else general_type_arg_policy type_sys
206 fun num_atp_type_args thy type_sys s =
207 if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
210 fun atp_type_literals_for_types type_sys kind Ts =
211 if level_of_type_sys type_sys = No_Types then
214 Ts |> type_literals_for_types
215 |> filter (fn TyLitVar _ => kind <> Conjecture
216 | TyLitFree _ => kind = Conjecture)
218 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
219 fun mk_aconns c phis =
220 let val (phis', phi') = split_last phis in
221 fold_rev (mk_aconn c) phis' phi'
223 fun mk_ahorn [] phi = phi
224 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
225 fun mk_aquant _ [] phi = phi
226 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
227 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
228 | mk_aquant q xs phi = AQuant (q, xs, phi)
230 fun close_universally atom_vars phi =
232 fun formula_vars bounds (AQuant (_, xs, phi)) =
233 formula_vars (map fst xs @ bounds) phi
234 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
235 | formula_vars bounds (AAtom tm) =
236 union (op =) (atom_vars tm []
237 |> filter_out (member (op =) bounds o fst))
238 in mk_aquant AForall (formula_vars [] phi []) phi end
240 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
241 | combterm_vars (CombConst _) = I
242 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
243 fun close_combformula_universally phi = close_universally combterm_vars phi
245 fun term_vars (ATerm (name as (s, _), tms)) =
246 is_atp_variable s ? insert (op =) (name, NONE)
247 #> fold term_vars tms
248 fun close_formula_universally phi = close_universally term_vars phi
250 fun fo_term_from_typ (Type (s, Ts)) =
251 ATerm (`make_fixed_type_const s, map fo_term_from_typ Ts)
252 | fo_term_from_typ (TFree (s, _)) =
253 ATerm (`make_fixed_type_var s, [])
254 | fo_term_from_typ (TVar ((x as (s, _)), _)) =
255 ATerm ((make_schematic_type_var x, s), [])
257 (* This shouldn't clash with anything else. *)
258 val mangled_type_sep = "\000"
260 fun generic_mangled_type_name f (ATerm (name, [])) = f name
261 | generic_mangled_type_name f (ATerm (name, tys)) =
262 f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
263 val mangled_type_name =
265 #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
266 generic_mangled_type_name snd ty))
268 fun generic_mangled_type_suffix f g Ts =
269 fold_rev (curry (op ^) o g o prefix mangled_type_sep
270 o generic_mangled_type_name f) Ts ""
271 fun mangled_const_name T_args (s, s') =
272 let val ty_args = map fo_term_from_typ T_args in
273 (s ^ generic_mangled_type_suffix fst ascii_of ty_args,
274 s' ^ generic_mangled_type_suffix snd I ty_args)
277 val parse_mangled_ident =
278 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
280 fun parse_mangled_type x =
282 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
284 and parse_mangled_types x =
285 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
287 fun unmangled_type s =
288 s |> suffix ")" |> raw_explode
289 |> Scan.finite Symbol.stopper
290 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
291 quote s)) parse_mangled_type))
294 val unmangled_const_name = space_explode mangled_type_sep #> hd
295 fun unmangled_const s =
296 let val ss = space_explode mangled_type_sep s in
297 (hd ss, map unmangled_type (tl ss))
300 fun introduce_proxies tm =
302 fun aux top_level (CombApp (tm1, tm2)) =
303 CombApp (aux top_level tm1, aux false tm2)
304 | aux top_level (CombConst (name as (s, s'), T, T_args)) =
305 (case proxify_const s of
309 "c_False" => (tptp_false, s')
310 | "c_True" => (tptp_true, s')
313 (proxy_base |>> prefix const_prefix, T_args)
314 | NONE => (name, T_args))
315 |> (fn (name, T_args) => CombConst (name, T, T_args))
319 fun combformula_from_prop thy eq_as_iff =
321 fun do_term bs t atomic_types =
322 combterm_from_term thy bs (Envir.eta_contract t)
323 |>> (introduce_proxies #> AAtom)
324 ||> union (op =) atomic_types
325 fun do_quant bs q s T t' =
326 let val s = Name.variant (map fst bs) s in
327 do_formula ((s, T) :: bs) t'
328 #>> mk_aquant q [(`make_bound_var s, SOME T)]
330 and do_conn bs c t1 t2 =
331 do_formula bs t1 ##>> do_formula bs t2
332 #>> uncurry (mk_aconn c)
333 and do_formula bs t =
335 @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
336 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
337 do_quant bs AForall s T t'
338 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
339 do_quant bs AExists s T t'
340 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
341 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
342 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
343 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
344 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
348 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
350 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
351 fun conceal_bounds Ts t =
352 subst_bounds (map (Free o apfst concealed_bound_name)
353 (0 upto length Ts - 1 ~~ Ts), t)
354 fun reveal_bounds Ts =
355 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
356 (0 upto length Ts - 1 ~~ Ts))
358 (* Removes the lambdas from an equation of the form "t = (%x. u)".
359 (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
360 fun extensionalize_term t =
362 fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
363 | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
364 Type (_, [_, res_T])]))
365 $ t2 $ Abs (var_s, var_T, t')) =
366 if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
367 let val var_t = Var ((var_s, j), var_T) in
368 Const (s, T' --> T' --> res_T)
369 $ betapply (t2, var_t) $ subst_bound (var_t, t')
375 in aux (maxidx_of_term t + 1) t end
377 fun introduce_combinators_in_term ctxt kind t =
378 let val thy = Proof_Context.theory_of ctxt in
379 if Meson.is_fol_term thy t then
385 @{const Not} $ t1 => @{const Not} $ aux Ts t1
386 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
387 t0 $ Abs (s, T, aux (T :: Ts) t')
388 | (t0 as Const (@{const_name All}, _)) $ t1 =>
389 aux Ts (t0 $ eta_expand Ts t1 1)
390 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
391 t0 $ Abs (s, T, aux (T :: Ts) t')
392 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
393 aux Ts (t0 $ eta_expand Ts t1 1)
394 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
395 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
396 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
397 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
399 t0 $ aux Ts t1 $ aux Ts t2
400 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
403 t |> conceal_bounds Ts
404 |> Envir.eta_contract
406 |> Meson_Clausify.introduce_combinators_in_cterm
407 |> prop_of |> Logic.dest_equals |> snd
409 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
410 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
412 (* A type variable of sort "{}" will make abstraction fail. *)
413 if kind = Conjecture then HOLogic.false_const
414 else HOLogic.true_const
417 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
418 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
421 fun aux (t $ u) = aux t $ aux u
422 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
423 | aux (Var ((s, i), T)) =
424 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
426 in t |> exists_subterm is_Var t ? aux end
428 (* making fact and conjecture formulas *)
429 fun make_formula ctxt eq_as_iff presimp name loc kind t =
431 val thy = Proof_Context.theory_of ctxt
432 val t = t |> Envir.beta_eta_contract
433 |> transform_elim_term
434 |> Object_Logic.atomize_term thy
435 val need_trueprop = (fastype_of t = @{typ bool})
436 val t = t |> need_trueprop ? HOLogic.mk_Trueprop
437 |> extensionalize_term
438 |> presimp ? presimplify_term thy
439 |> perhaps (try (HOLogic.dest_Trueprop))
440 |> introduce_combinators_in_term ctxt kind
441 |> kind <> Axiom ? freeze_term
442 val (combformula, atomic_types) =
443 combformula_from_prop thy eq_as_iff t []
445 {name = name, locality = loc, kind = kind, combformula = combformula,
446 atomic_types = atomic_types}
449 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
450 case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
451 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
453 | (_, formula) => SOME formula
455 fun make_conjecture ctxt ts =
456 let val last = length ts - 1 in
457 map2 (fn j => make_formula ctxt true true (string_of_int j) Chained
458 (if j = last then Conjecture else Hypothesis))
462 (** Finite and infinite type inference **)
464 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
465 dangerous because their "exhaust" properties can easily lead to unsound ATP
466 proofs. On the other hand, all HOL infinite types can be given the same
467 models in first-order logic (via Löwenheim-Skolem). *)
469 fun datatype_constrs thy (T as Type (s, Ts)) =
470 (case Datatype.get_info thy s of
471 SOME {index, descr, ...} =>
472 let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
473 map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
477 | datatype_constrs _ _ = []
479 (* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
480 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
481 cardinality 2 or more. The specified default cardinality is returned if the
482 cardinality of the type can't be determined. *)
483 fun tiny_card_of_type ctxt default_card T =
485 val max = 2 (* 1 would be too small for the "fun" case *)
487 (if member (op =) avoid T then
490 Type (@{type_name fun}, [T1, T2]) =>
491 (case (aux avoid T1, aux avoid T2) of
496 if k1 >= max orelse k2 >= max then max
497 else Int.min (max, Integer.pow k2 k1))
498 | @{typ bool} => 2 (* optimization *)
499 | @{typ nat} => 0 (* optimization *)
500 | @{typ int} => 0 (* optimization *)
502 let val thy = Proof_Context.theory_of ctxt in
503 case datatype_constrs thy T of
507 map (Integer.prod o map (aux (T :: avoid)) o binder_types
510 if exists (curry (op =) 0) constr_cards then 0
511 else Int.min (max, Integer.sum constr_cards)
514 case Typedef.get_info ctxt s of
515 ({abs_type, rep_type, ...}, _) :: _ =>
516 (* We cheat here by assuming that typedef types are infinite if
517 their underlying type is infinite. This is unsound in general
518 but it's hard to think of a realistic example where this would
520 (case varify_and_instantiate_type ctxt
521 (Logic.varifyT_global abs_type) T
522 (Logic.varifyT_global rep_type)
530 in Int.min (max, aux [] T) end
532 fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
533 fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
535 fun should_encode_type _ _ All_Types _ = true
536 | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
537 | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
538 exists (curry Type.raw_instance T) nonmono_Ts
539 | should_encode_type _ _ _ _ = false
541 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
542 should_encode_type ctxt nonmono_Ts level T
543 | should_predicate_on_type _ _ _ _ = false
545 fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
546 should_encode_type ctxt nonmono_Ts level T
547 | should_tag_with_type _ _ _ _ = false
549 val homo_infinite_T = @{typ ind} (* any infinite type *)
551 fun homogenized_type ctxt nonmono_Ts level T =
552 if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T
554 (** "hBOOL" and "hAPP" **)
557 {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
559 fun add_combterm_syms_to_table explicit_apply =
561 fun aux top_level tm =
562 let val (head, args) = strip_combterm_comb tm in
564 CombConst ((s, _), T, _) =>
565 if String.isPrefix bound_var_prefix s then
568 let val ary = length args in
570 (s, {pred_sym = true,
571 min_ary = if explicit_apply then 0 else ary,
572 max_ary = 0, typ = SOME T})
573 (fn {pred_sym, min_ary, max_ary, typ} =>
574 {pred_sym = pred_sym andalso top_level,
575 min_ary = Int.min (ary, min_ary),
576 max_ary = Int.max (ary, max_ary),
577 typ = if typ = SOME T then typ else NONE})
580 #> fold (aux false) args
583 fun add_fact_syms_to_table explicit_apply =
584 fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply)))
586 val default_sym_table_entries : (string * sym_info) list =
587 [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
588 (make_fixed_const predicator_base,
589 {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
590 ([tptp_false, tptp_true]
591 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
593 fun sym_table_for_facts explicit_apply facts =
594 Symtab.empty |> fold Symtab.default default_sym_table_entries
595 |> fold (add_fact_syms_to_table explicit_apply) facts
597 fun min_arity_of sym_tab s =
598 case Symtab.lookup sym_tab s of
599 SOME ({min_ary, ...} : sym_info) => min_ary
601 case strip_prefix_and_unascii const_prefix s of
603 let val s = s |> unmangled_const_name |> invert_const in
604 if s = predicator_base then 1
605 else if s = explicit_app_base then 2
606 else if s = type_pred_base then 1
611 (* True if the constant ever appears outside of the top-level position in
612 literals, or if it appears with different arities (e.g., because of different
613 type instantiations). If false, the constant always receives all of its
614 arguments and is used as a predicate. *)
615 fun is_pred_sym sym_tab s =
616 case Symtab.lookup sym_tab s of
617 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
618 pred_sym andalso min_ary = max_ary
621 val predicator_combconst =
622 CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
623 fun predicator tm = CombApp (predicator_combconst, tm)
625 fun introduce_predicators_in_combterm sym_tab tm =
626 case strip_combterm_comb tm of
627 (CombConst ((s, _), _, _), _) =>
628 if is_pred_sym sym_tab s then tm else predicator tm
631 fun list_app head args = fold (curry (CombApp o swap)) args head
633 fun explicit_app arg head =
635 val head_T = combtyp_of head
636 val (arg_T, res_T) = dest_funT head_T
638 CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
640 in list_app explicit_app [head, arg] end
641 fun list_explicit_app head args = fold explicit_app args head
643 fun introduce_explicit_apps_in_combterm sym_tab =
646 case strip_combterm_comb tm of
647 (head as CombConst ((s, _), _, _), args) =>
649 |> chop (min_arity_of sym_tab s)
651 |-> list_explicit_app
652 | (head, args) => list_explicit_app head (map aux args)
655 fun impose_type_arg_policy_in_combterm type_sys =
657 fun aux (CombApp tmp) = CombApp (pairself aux tmp)
658 | aux (CombConst (name as (s, _), T, T_args)) =
659 (case strip_prefix_and_unascii const_prefix s of
660 NONE => (name, T_args)
662 let val s'' = invert_const s'' in
663 case type_arg_policy type_sys s'' of
664 No_Type_Args => (name, [])
665 | Explicit_Type_Args => (name, T_args)
666 | Mangled_Type_Args => (mangled_const_name T_args name, [])
668 |> (fn (name, T_args) => CombConst (name, T, T_args))
672 fun repair_combterm type_sys sym_tab =
673 introduce_explicit_apps_in_combterm sym_tab
674 #> introduce_predicators_in_combterm sym_tab
675 #> impose_type_arg_policy_in_combterm type_sys
676 fun repair_fact type_sys sym_tab =
677 update_combformula (formula_map (repair_combterm type_sys sym_tab))
681 fun ti_ti_helper_fact () =
683 fun var s = ATerm (`I s, [])
684 fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
686 Formula (helper_prefix ^ "ti_ti", Axiom,
687 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
688 |> close_formula_universally, NONE, NONE)
691 fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
692 case strip_prefix_and_unascii const_prefix s of
695 val thy = Proof_Context.theory_of ctxt
696 val unmangled_s = mangled_s |> unmangled_const_name
697 fun dub_and_inst c needs_some_types (th, j) =
698 ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
700 let val t = th |> prop_of in
701 t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
702 not (null (Term.hidden_polymorphism t)))
704 SOME T => specialize_type thy (invert_const unmangled_s, T)
707 fun make_facts eq_as_iff =
708 map_filter (make_fact ctxt false eq_as_iff false)
709 val has_some_types = is_type_sys_fairly_sound type_sys
712 |> maps (fn (metis_s, (needs_some_types, ths)) =>
713 if metis_s <> unmangled_s orelse
714 (needs_some_types andalso not has_some_types) then
717 ths ~~ (1 upto length ths)
718 |> map (dub_and_inst mangled_s needs_some_types)
719 |> make_facts (not needs_some_types))
722 fun helper_facts_for_sym_table ctxt type_sys sym_tab =
723 Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
725 fun translate_atp_fact ctxt keep_trivial =
726 `(make_fact ctxt keep_trivial true true o apsnd prop_of)
728 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
730 val thy = Proof_Context.theory_of ctxt
731 val fact_ts = map (prop_of o snd o snd) rich_facts
732 val (facts, fact_names) =
734 |> map_filter (fn (NONE, _) => NONE
735 | (SOME fact, (name, _)) => SOME (fact, name))
737 (* Remove existing facts from the conjecture, as this can dramatically
738 boost an ATP's performance (for some reason). *)
739 val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
740 val goal_t = Logic.list_implies (hyp_ts, concl_t)
741 val all_ts = goal_t :: fact_ts
742 val subs = tfree_classes_of_terms all_ts
743 val supers = tvar_classes_of_terms all_ts
744 val tycons = type_consts_of_terms thy all_ts
745 val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
746 val (supers', arity_clauses) =
747 if level_of_type_sys type_sys = No_Types then ([], [])
748 else make_arity_clauses thy tycons supers
749 val class_rel_clauses = make_class_rel_clauses thy subs supers'
751 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
754 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
755 (true, ATerm (class, [ATerm (name, [])]))
756 | fo_literal_from_type_literal (TyLitFree (class, name)) =
757 (true, ATerm (class, [ATerm (name, [])]))
759 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
761 fun type_pred_combatom type_sys T tm =
762 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
764 |> impose_type_arg_policy_in_combterm type_sys
767 fun formula_from_combformula ctxt nonmono_Ts type_sys =
769 fun tag_with_type type_sys T tm =
770 CombConst (`make_fixed_const type_tag_name, T --> T, [T])
771 |> impose_type_arg_policy_in_combterm type_sys
773 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
774 and do_term top_level u =
776 val (head, args) = strip_combterm_comb u
779 CombConst (name, _, T_args) => (name, T_args)
780 | CombVar (name, _) => (name, [])
781 | CombApp _ => raise Fail "impossible \"CombApp\""
782 val t = ATerm (x, map fo_term_from_typ T_args @
783 map (do_term false) args)
786 t |> (if not top_level andalso
787 should_tag_with_type ctxt nonmono_Ts type_sys T then
788 tag_with_type type_sys T
795 SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
797 fun do_out_of_bound_type (s, T) =
798 if should_predicate_on_type ctxt nonmono_Ts type_sys T then
799 type_pred_combatom type_sys T (CombVar (s, T))
800 |> do_formula |> SOME
803 and do_formula (AQuant (q, xs, phi)) =
804 AQuant (q, xs |> map (apsnd (fn NONE => NONE
805 | SOME T => do_bound_type T)),
806 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
808 (fn (_, NONE) => NONE
809 | (s, SOME T) => do_out_of_bound_type (s, T)) xs)
811 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
812 | do_formula (AAtom tm) = AAtom (do_term true tm)
815 fun formula_for_fact ctxt nonmono_Ts type_sys
816 ({combformula, atomic_types, ...} : translated_formula) =
817 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
818 (atp_type_literals_for_types type_sys Axiom atomic_types))
819 (formula_from_combformula ctxt nonmono_Ts type_sys
820 (close_combformula_universally combformula))
821 |> close_formula_universally
823 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
825 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
826 of monomorphization). The TPTP explicitly forbids name clashes, and some of
827 the remote provers might care. *)
828 fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
829 (j, formula as {name, locality, kind, ...}) =
830 Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
831 else string_of_int j ^ "_") ^
833 kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
834 if generate_useful_info then
836 Intro => useful_isabelle_info "intro"
837 | Elim => useful_isabelle_info "elim"
838 | Simp => useful_isabelle_info "simp"
843 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
845 let val ty_arg = ATerm (`I "T", []) in
846 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
847 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
848 AAtom (ATerm (superclass, [ty_arg]))])
849 |> close_formula_universally, NONE, NONE)
852 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
853 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
854 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
855 (false, ATerm (c, [ATerm (sort, [])]))
857 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
859 Formula (arity_clause_prefix ^ ascii_of name, Axiom,
860 mk_ahorn (map (formula_from_fo_literal o apfst not
861 o fo_literal_from_arity_literal) premLits)
862 (formula_from_fo_literal
863 (fo_literal_from_arity_literal conclLit))
864 |> close_formula_universally, NONE, NONE)
866 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
867 ({name, kind, combformula, ...} : translated_formula) =
868 Formula (conjecture_prefix ^ name, kind,
869 formula_from_combformula ctxt nonmono_Ts type_sys
870 (close_combformula_universally combformula)
871 |> close_formula_universally, NONE, NONE)
873 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
874 atomic_types |> atp_type_literals_for_types type_sys Conjecture
875 |> map fo_literal_from_type_literal
877 fun formula_line_for_free_type j lit =
878 Formula (tfree_prefix ^ string_of_int j, Hypothesis,
879 formula_from_fo_literal lit, NONE, NONE)
880 fun formula_lines_for_free_types type_sys facts =
882 val litss = map (free_type_literals type_sys) facts
883 val lits = fold (union (op =)) litss []
884 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
886 (** Symbol declarations **)
888 fun insert_type get_T x xs =
889 let val T = get_T x in
890 if exists (curry Type.raw_instance T o get_T) xs then xs
891 else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
894 fun should_declare_sym type_sys pred_sym s =
895 not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
896 not (String.isPrefix "$" s) andalso
897 ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
899 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
901 fun declare_sym decl decls =
903 Preds (Polymorphic, All_Types) => insert_type #3 decl decls
904 | _ => insert (op =) decl decls
906 let val (head, args) = strip_combterm_comb tm in
908 CombConst ((s, s'), T, T_args) =>
909 let val pred_sym = is_pred_sym repaired_sym_tab s in
910 if should_declare_sym type_sys pred_sym s then
911 Symtab.map_default (s, [])
912 (declare_sym (s', T_args, T, pred_sym, length args))
920 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
921 fact_lift (formula_fold true
922 (K (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)))
923 fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
924 Symtab.empty |> is_type_sys_fairly_sound type_sys
925 ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
928 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
929 String.isPrefix bound_var_prefix s
930 | is_var_or_bound_var (CombVar _) = true
931 | is_var_or_bound_var _ = false
933 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
934 out with monotonicity" paper presented at CADE 2011. *)
935 fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
936 | add_combterm_nonmonotonic_types ctxt _
937 (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
939 (exists is_var_or_bound_var [tm1, tm2] andalso
940 not (is_type_surely_infinite ctxt T)) ? insert_type I T
941 | add_combterm_nonmonotonic_types _ _ _ = I
942 fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
943 : translated_formula) =
944 formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
946 fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
947 level_of_type_sys type_sys = Nonmonotonic_Types
948 ? (insert_type I @{typ bool} (* in case helper "True_or_False" is included *)
949 #> fold (add_fact_nonmonotonic_types ctxt) facts)
951 fun n_ary_strip_type 0 T = ([], T)
952 | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
953 n_ary_strip_type (n - 1) ran_T |>> cons dom_T
954 | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
956 fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd
958 fun decl_line_for_sym s (s', _, T, pred_sym, ary) =
959 let val (arg_Ts, res_T) = n_ary_strip_type ary T in
960 Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
961 if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
964 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
966 fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
967 (s', T_args, T, _, ary) =
969 val (arg_Ts, res_T) = n_ary_strip_type ary T
971 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
973 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
975 arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
978 Formula (sym_decl_prefix ^ s ^
979 (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
980 CombConst ((s, s'), T, T_args)
981 |> fold (curry (CombApp o swap)) bound_tms
982 |> type_pred_combatom type_sys res_T
983 |> mk_aquant AForall (bound_names ~~ bound_Ts)
984 |> formula_from_combformula ctxt nonmono_Ts type_sys
985 |> close_formula_universally,
989 fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
991 Simple _ => map (decl_line_for_sym s) decls
996 decl :: (decls' as _ :: _) =>
997 let val T = result_type_of_decl decl in
998 if forall ((fn T' => Type.raw_instance (T', T))
999 o result_type_of_decl) decls' then
1005 val n = length decls
1007 decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
1008 o result_type_of_decl)
1010 map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
1011 (0 upto length decls - 1) decls
1014 fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
1015 Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
1019 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
1020 union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
1021 | add_tff_types_in_formula (AConn (_, phis)) =
1022 fold add_tff_types_in_formula phis
1023 | add_tff_types_in_formula (AAtom _) = I
1025 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
1026 union (op =) (res_T :: arg_Ts)
1027 | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
1028 add_tff_types_in_formula phi
1030 fun tff_types_in_problem problem =
1031 fold (fold add_tff_types_in_problem_line o snd) problem []
1033 fun decl_line_for_tff_type (s, s') =
1034 Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
1036 val type_declsN = "Types"
1037 val sym_declsN = "Symbol types"
1038 val factsN = "Relevant facts"
1039 val class_relsN = "Class relationships"
1040 val aritiesN = "Arities"
1041 val helpersN = "Helper facts"
1042 val conjsN = "Conjectures"
1043 val free_typesN = "Type variables"
1045 fun offset_of_heading_in_problem _ [] j = j
1046 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1047 if heading = needle then j
1048 else offset_of_heading_in_problem needle problem (j + length lines)
1050 fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts =
1052 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1053 translate_formulas ctxt type_sys hyp_ts concl_t facts
1054 val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
1056 [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
1057 val repair = repair_fact type_sys sym_tab
1058 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1059 val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
1061 repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
1062 val sym_decl_lines =
1064 |> sym_decl_table_for_facts type_sys repaired_sym_tab
1065 |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
1066 (* Reordering these might confuse the proof reconstruction code or the SPASS
1069 [(sym_declsN, sym_decl_lines),
1070 (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
1071 (0 upto length facts - 1 ~~ facts)),
1072 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1073 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1074 (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
1076 (0 upto length helpers - 1 ~~ helpers)
1077 |> (case type_sys of
1078 Tags (Polymorphic, level) =>
1079 is_type_level_partial level
1080 ? cons (ti_ti_helper_fact ())
1082 (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
1084 (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
1087 |> (case type_sys of
1090 map decl_line_for_tff_type (tff_types_in_problem problem))
1092 val (problem, pool) =
1093 problem |> nice_atp_problem (Config.get ctxt readable_names)
1096 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1097 offset_of_heading_in_problem conjsN problem 0,
1098 offset_of_heading_in_problem factsN problem 0,
1099 fact_names |> Vector.fromList)
1103 val conj_weight = 0.0
1104 val hyp_weight = 0.1
1105 val fact_min_weight = 0.2
1106 val fact_max_weight = 1.0
1107 val type_info_default_weight = 0.8
1109 fun add_term_weights weight (ATerm (s, tms)) =
1110 (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
1111 #> fold (add_term_weights weight) tms
1112 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1113 formula_fold true (K (add_term_weights weight)) phi
1114 | add_problem_line_weights _ _ = I
1116 fun add_conjectures_weights [] = I
1117 | add_conjectures_weights conjs =
1118 let val (hyps, conj) = split_last conjs in
1119 add_problem_line_weights conj_weight conj
1120 #> fold (add_problem_line_weights hyp_weight) hyps
1123 fun add_facts_weights facts =
1125 val num_facts = length facts
1127 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
1128 / Real.fromInt num_facts
1130 map weight_of (0 upto num_facts - 1) ~~ facts
1131 |> fold (uncurry add_problem_line_weights)
1134 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
1135 fun atp_problem_weights problem =
1136 let val get = these o AList.lookup (op =) problem in
1138 |> add_conjectures_weights (get free_typesN @ get conjsN)
1139 |> add_facts_weights (get factsN)
1140 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
1141 [sym_declsN, class_relsN, aritiesN]
1143 |> sort (prod_ord Real.compare string_ord o pairself swap)