use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
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 formula_kind = ATP_Problem.formula_kind
13 type 'a problem = 'a ATP_Problem.problem
14 type locality = Sledgehammer_Filter.locality
16 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
18 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
20 datatype type_system =
21 Simple_Types of type_level |
22 Preds of polymorphism * type_level |
23 Tags of polymorphism * type_level
25 type translated_formula
27 val readable_names : bool Config.T
28 val fact_prefix : string
29 val conjecture_prefix : string
30 val predicator_base : string
31 val explicit_app_base : string
32 val type_pred_base : string
33 val tff_type_prefix : string
34 val type_sys_from_string : string -> type_system
35 val polymorphism_of_type_sys : type_system -> polymorphism
36 val level_of_type_sys : type_system -> type_level
37 val is_type_sys_virtually_sound : type_system -> bool
38 val is_type_sys_fairly_sound : type_system -> bool
39 val num_atp_type_args : theory -> type_system -> string -> int
40 val unmangled_const : string -> string * string fo_term list
41 val translate_atp_fact :
42 Proof.context -> bool -> (string * locality) * thm
43 -> translated_formula option * ((string * locality) * thm)
44 val prepare_atp_problem :
45 Proof.context -> formula_kind -> formula_kind -> type_system -> bool
47 -> (translated_formula option * ((string * 'a) * thm)) list
48 -> string problem * string Symtab.table * int * int
49 * (string * 'a) list vector
50 val atp_problem_weights : string problem -> (string * real) list
53 structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
58 open Sledgehammer_Util
59 open Sledgehammer_Filter
62 val generate_useful_info = false
64 (* Readable names are often much shorter, especially if types are mangled in
65 names. Also, the logic for generating legal SNARK sort names is only
66 implemented for readable names. Finally, readable names are, well, more
67 readable. For these reason, they are enabled by default. *)
69 Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
71 val type_decl_prefix = "type_"
72 val sym_decl_prefix = "sym_"
73 val fact_prefix = "fact_"
74 val conjecture_prefix = "conj_"
75 val helper_prefix = "help_"
76 val class_rel_clause_prefix = "crel_";
77 val arity_clause_prefix = "arity_"
78 val tfree_prefix = "tfree_"
80 val predicator_base = "hBOOL"
81 val explicit_app_base = "hAPP"
82 val type_pred_base = "is"
83 val tff_type_prefix = "ty_"
85 fun make_tff_type s = tff_type_prefix ^ ascii_of s
87 (* Freshness almost guaranteed! *)
88 val sledgehammer_weak_prefix = "Sledgehammer:"
90 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
92 All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
94 datatype type_system =
95 Simple_Types of type_level |
96 Preds of polymorphism * type_level |
97 Tags of polymorphism * type_level
99 fun try_unsuffixes ss s =
100 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
102 fun type_sys_from_string s =
103 (case try (unprefix "poly_") s of
104 SOME s => (SOME Polymorphic, s)
106 case try (unprefix "mono_") s of
107 SOME s => (SOME Monomorphic, s)
109 case try (unprefix "mangled_") s of
110 SOME s => (SOME Mangled_Monomorphic, s)
113 (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
114 case try_unsuffixes ["?", "_query"] s of
115 SOME s => (Nonmonotonic_Types, s)
117 case try_unsuffixes ["!", "_bang"] s of
118 SOME s => (Finite_Types, s)
119 | NONE => (All_Types, s))
120 |> (fn (poly, (level, core)) =>
121 case (core, (poly, level)) of
122 ("simple_types", (NONE, level)) => Simple_Types level
123 | ("preds", (SOME poly, level)) => Preds (poly, level)
124 | ("tags", (SOME poly, level)) => Tags (poly, level)
125 | ("args", (SOME poly, All_Types (* naja *))) =>
126 Preds (poly, Const_Arg_Types)
127 | ("erased", (NONE, All_Types (* naja *))) =>
128 Preds (Polymorphic, No_Types)
129 | _ => error ("Unknown type system: " ^ quote s ^ "."))
131 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
132 | polymorphism_of_type_sys (Preds (poly, _)) = poly
133 | polymorphism_of_type_sys (Tags (poly, _)) = poly
135 fun level_of_type_sys (Simple_Types level) = level
136 | level_of_type_sys (Preds (_, level)) = level
137 | level_of_type_sys (Tags (_, level)) = level
139 fun is_type_level_virtually_sound level =
140 level = All_Types orelse level = Nonmonotonic_Types
141 val is_type_sys_virtually_sound =
142 is_type_level_virtually_sound o level_of_type_sys
144 fun is_type_level_fairly_sound level =
145 is_type_level_virtually_sound level orelse level = Finite_Types
146 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
148 fun is_type_level_partial level =
149 level = Nonmonotonic_Types orelse level = Finite_Types
151 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
152 | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
153 | formula_map f (AAtom tm) = AAtom (f tm)
155 fun formula_fold pos f =
157 fun aux pos (AQuant (_, _, phi)) = aux pos phi
158 | aux pos (AConn (ANot, [phi])) = aux (Option.map not pos) phi
159 | aux pos (AConn (AImplies, [phi1, phi2])) =
160 aux (Option.map not pos) phi1 #> aux pos phi2
161 | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
162 | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
163 | aux _ (AConn (_, phis)) = fold (aux NONE) phis
164 | aux pos (AAtom tm) = f pos tm
165 in aux (SOME pos) end
167 type translated_formula =
171 combformula: (name, typ, combterm) formula,
172 atomic_types: typ list}
174 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
175 : translated_formula) =
176 {name = name, locality = locality, kind = kind, combformula = f combformula,
177 atomic_types = atomic_types} : translated_formula
179 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
181 val boring_consts = [explicit_app_base, @{const_name Metis.fequal}]
183 fun should_omit_type_args type_sys s =
184 s <> type_pred_base andalso s <> type_tag_name andalso
185 (s = @{const_name HOL.eq} orelse level_of_type_sys type_sys = No_Types orelse
187 Tags (_, All_Types) => true
188 | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
189 member (op =) boring_consts s))
191 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
193 fun general_type_arg_policy type_sys =
194 if level_of_type_sys type_sys = No_Types then
196 else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
201 fun type_arg_policy type_sys s =
202 if should_omit_type_args type_sys s then No_Type_Args
203 else general_type_arg_policy type_sys
205 fun num_atp_type_args thy type_sys s =
206 if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
209 fun atp_type_literals_for_types type_sys kind Ts =
210 if level_of_type_sys type_sys = No_Types then
213 Ts |> type_literals_for_types
214 |> filter (fn TyLitVar _ => kind <> Conjecture
215 | TyLitFree _ => kind = Conjecture)
217 fun mk_anot phi = AConn (ANot, [phi])
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 fun extensionalize_term ctxt t =
359 let val thy = Proof_Context.theory_of ctxt in
360 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
361 |> prop_of |> Logic.dest_equals |> snd
364 fun introduce_combinators_in_term ctxt kind t =
365 let val thy = Proof_Context.theory_of ctxt in
366 if Meson.is_fol_term thy t then
372 @{const Not} $ t1 => @{const Not} $ aux Ts t1
373 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
374 t0 $ Abs (s, T, aux (T :: Ts) t')
375 | (t0 as Const (@{const_name All}, _)) $ t1 =>
376 aux Ts (t0 $ eta_expand Ts t1 1)
377 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
378 t0 $ Abs (s, T, aux (T :: Ts) t')
379 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
380 aux Ts (t0 $ eta_expand Ts t1 1)
381 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
382 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
383 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
384 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
386 t0 $ aux Ts t1 $ aux Ts t2
387 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
390 t |> conceal_bounds Ts
391 |> Envir.eta_contract
393 |> Meson_Clausify.introduce_combinators_in_cterm
394 |> prop_of |> Logic.dest_equals |> snd
396 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
397 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
399 (* A type variable of sort "{}" will make abstraction fail. *)
400 if kind = Conjecture then HOLogic.false_const
401 else HOLogic.true_const
404 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
405 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
408 fun aux (t $ u) = aux t $ aux u
409 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
410 | aux (Var ((s, i), T)) =
411 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
413 in t |> exists_subterm is_Var t ? aux end
415 (* making fact and conjecture formulas *)
416 fun make_formula ctxt eq_as_iff presimp name loc kind t =
418 val thy = Proof_Context.theory_of ctxt
419 val t = t |> Envir.beta_eta_contract
420 |> transform_elim_term
421 |> Object_Logic.atomize_term thy
422 val need_trueprop = (fastype_of t = @{typ bool})
423 val t = t |> need_trueprop ? HOLogic.mk_Trueprop
424 |> Raw_Simplifier.rewrite_term thy
425 (Meson.unfold_set_const_simps ctxt) []
426 |> extensionalize_term ctxt
427 |> presimp ? presimplify_term thy
428 |> perhaps (try (HOLogic.dest_Trueprop))
429 |> introduce_combinators_in_term ctxt kind
430 |> kind <> Axiom ? freeze_term
431 val (combformula, atomic_types) =
432 combformula_from_prop thy eq_as_iff t []
434 {name = name, locality = loc, kind = kind, combformula = combformula,
435 atomic_types = atomic_types}
438 fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, loc), t) =
439 case (keep_trivial, make_formula ctxt eq_as_iff presimp name loc Axiom t) of
440 (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
442 | (_, formula) => SOME formula
444 fun make_conjecture ctxt prem_kind ts =
445 let val last = length ts - 1 in
446 map2 (fn j => fn t =>
448 val (kind, maybe_negate) =
453 if prem_kind = Conjecture then update_combformula mk_anot
456 make_formula ctxt true true (string_of_int j) Chained kind t
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 should_encode_type _ _ All_Types _ = true
470 | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
471 | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
472 exists (curry Type.raw_instance T) nonmono_Ts
473 | should_encode_type _ _ _ _ = false
475 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
476 should_encode_type ctxt nonmono_Ts level T
477 | should_predicate_on_type _ _ _ _ = false
479 fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
480 should_encode_type ctxt nonmono_Ts level T
481 | should_tag_with_type _ _ _ _ = false
483 val homo_infinite_T = @{typ ind} (* any infinite type *)
485 fun homogenized_type ctxt nonmono_Ts level T =
486 if should_encode_type ctxt nonmono_Ts level T then T else homo_infinite_T
488 (** "hBOOL" and "hAPP" **)
491 {pred_sym : bool, min_ary : int, max_ary : int, typ : typ option}
493 fun add_combterm_syms_to_table explicit_apply =
495 fun aux top_level tm =
496 let val (head, args) = strip_combterm_comb tm in
498 CombConst ((s, _), T, _) =>
499 if String.isPrefix bound_var_prefix s then
502 let val ary = length args in
504 (s, {pred_sym = true,
505 min_ary = if explicit_apply then 0 else ary,
506 max_ary = 0, typ = SOME T})
507 (fn {pred_sym, min_ary, max_ary, typ} =>
508 {pred_sym = pred_sym andalso top_level,
509 min_ary = Int.min (ary, min_ary),
510 max_ary = Int.max (ary, max_ary),
511 typ = if typ = SOME T then typ else NONE})
514 #> fold (aux false) args
517 fun add_fact_syms_to_table explicit_apply =
518 fact_lift (formula_fold true (K (add_combterm_syms_to_table explicit_apply)))
520 val default_sym_table_entries : (string * sym_info) list =
521 [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
522 (make_fixed_const predicator_base,
523 {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
524 ([tptp_false, tptp_true]
525 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
527 fun sym_table_for_facts explicit_apply facts =
528 Symtab.empty |> fold Symtab.default default_sym_table_entries
529 |> fold (add_fact_syms_to_table explicit_apply) facts
531 fun min_arity_of sym_tab s =
532 case Symtab.lookup sym_tab s of
533 SOME ({min_ary, ...} : sym_info) => min_ary
535 case strip_prefix_and_unascii const_prefix s of
537 let val s = s |> unmangled_const_name |> invert_const in
538 if s = predicator_base then 1
539 else if s = explicit_app_base then 2
540 else if s = type_pred_base then 1
545 (* True if the constant ever appears outside of the top-level position in
546 literals, or if it appears with different arities (e.g., because of different
547 type instantiations). If false, the constant always receives all of its
548 arguments and is used as a predicate. *)
549 fun is_pred_sym sym_tab s =
550 case Symtab.lookup sym_tab s of
551 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
552 pred_sym andalso min_ary = max_ary
555 val predicator_combconst =
556 CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
557 fun predicator tm = CombApp (predicator_combconst, tm)
559 fun introduce_predicators_in_combterm sym_tab tm =
560 case strip_combterm_comb tm of
561 (CombConst ((s, _), _, _), _) =>
562 if is_pred_sym sym_tab s then tm else predicator tm
565 fun list_app head args = fold (curry (CombApp o swap)) args head
567 fun explicit_app arg head =
569 val head_T = combtyp_of head
570 val (arg_T, res_T) = dest_funT head_T
572 CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
574 in list_app explicit_app [head, arg] end
575 fun list_explicit_app head args = fold explicit_app args head
577 fun introduce_explicit_apps_in_combterm sym_tab =
580 case strip_combterm_comb tm of
581 (head as CombConst ((s, _), _, _), args) =>
583 |> chop (min_arity_of sym_tab s)
585 |-> list_explicit_app
586 | (head, args) => list_explicit_app head (map aux args)
589 fun impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys =
591 fun aux (CombApp tmp) = CombApp (pairself aux tmp)
592 | aux (CombConst (name as (s, _), T, T_args)) =
594 val level = level_of_type_sys type_sys
596 (* Aggressively merge most "hAPPs" if the type system is unsound
597 anyway, by distinguishing overloads only on the homogenized
599 if s = const_prefix ^ explicit_app_base andalso
600 length T_args = 2 andalso
601 not (is_type_sys_virtually_sound type_sys) then
602 T_args |> map (homogenized_type ctxt nonmono_Ts level)
603 |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
609 (case strip_prefix_and_unascii const_prefix s of
610 NONE => (name, T_args)
612 let val s'' = invert_const s'' in
613 case type_arg_policy type_sys s'' of
614 No_Type_Args => (name, [])
615 | Explicit_Type_Args => (name, T_args)
616 | Mangled_Type_Args => (mangled_const_name T_args name, [])
618 |> (fn (name, T_args) => CombConst (name, T, T_args))
623 fun repair_combterm ctxt nonmono_Ts type_sys sym_tab =
624 introduce_explicit_apps_in_combterm sym_tab
625 #> introduce_predicators_in_combterm sym_tab
626 #> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
627 fun repair_fact ctxt nonmono_Ts type_sys sym_tab =
628 update_combformula (formula_map
629 (repair_combterm ctxt nonmono_Ts type_sys sym_tab))
633 fun ti_ti_helper_fact () =
635 fun var s = ATerm (`I s, [])
636 fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
638 Formula (helper_prefix ^ "ti_ti", Axiom,
639 AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
640 |> close_formula_universally, NONE, NONE)
643 fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
644 case strip_prefix_and_unascii const_prefix s of
647 val thy = Proof_Context.theory_of ctxt
648 val unmangled_s = mangled_s |> unmangled_const_name
649 fun dub_and_inst c needs_some_types (th, j) =
650 ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
652 let val t = th |> prop_of in
653 t |> (general_type_arg_policy type_sys = Mangled_Type_Args andalso
654 not (null (Term.hidden_polymorphism t)))
656 SOME T => specialize_type thy (invert_const unmangled_s, T)
659 fun make_facts eq_as_iff =
660 map_filter (make_fact ctxt false eq_as_iff false)
661 val has_some_types = is_type_sys_fairly_sound type_sys
664 |> maps (fn (metis_s, (needs_some_types, ths)) =>
665 if metis_s <> unmangled_s orelse
666 (needs_some_types andalso not has_some_types) then
669 ths ~~ (1 upto length ths)
670 |> map (dub_and_inst mangled_s needs_some_types)
671 |> make_facts (not needs_some_types))
674 fun helper_facts_for_sym_table ctxt type_sys sym_tab =
675 Symtab.fold_rev (append o helper_facts_for_sym ctxt type_sys) sym_tab []
677 fun translate_atp_fact ctxt keep_trivial =
678 `(make_fact ctxt keep_trivial true true o apsnd prop_of)
680 fun translate_formulas ctxt prem_kind type_sys hyp_ts concl_t rich_facts =
682 val thy = Proof_Context.theory_of ctxt
683 val fact_ts = map (prop_of o snd o snd) rich_facts
684 val (facts, fact_names) =
686 |> map_filter (fn (NONE, _) => NONE
687 | (SOME fact, (name, _)) => SOME (fact, name))
689 (* Remove existing facts from the conjecture, as this can dramatically
690 boost an ATP's performance (for some reason). *)
691 val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
692 val goal_t = Logic.list_implies (hyp_ts, concl_t)
693 val all_ts = goal_t :: fact_ts
694 val subs = tfree_classes_of_terms all_ts
695 val supers = tvar_classes_of_terms all_ts
696 val tycons = type_consts_of_terms thy all_ts
697 val conjs = make_conjecture ctxt prem_kind (hyp_ts @ [concl_t])
698 val (supers', arity_clauses) =
699 if level_of_type_sys type_sys = No_Types then ([], [])
700 else make_arity_clauses thy tycons supers
701 val class_rel_clauses = make_class_rel_clauses thy subs supers'
703 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
706 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
707 (true, ATerm (class, [ATerm (name, [])]))
708 | fo_literal_from_type_literal (TyLitFree (class, name)) =
709 (true, ATerm (class, [ATerm (name, [])]))
711 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
713 fun type_pred_combatom ctxt nonmono_Ts type_sys T tm =
714 CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
716 |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
719 fun formula_from_combformula ctxt nonmono_Ts type_sys =
721 fun tag_with_type type_sys T tm =
722 CombConst (`make_fixed_const type_tag_name, T --> T, [T])
723 |> impose_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys
725 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
726 and do_term top_level u =
728 val (head, args) = strip_combterm_comb u
731 CombConst (name, _, T_args) => (name, T_args)
732 | CombVar (name, _) => (name, [])
733 | CombApp _ => raise Fail "impossible \"CombApp\""
734 val t = ATerm (x, map fo_term_from_typ T_args @
735 map (do_term false) args)
738 t |> (if not top_level andalso
739 should_tag_with_type ctxt nonmono_Ts type_sys T then
740 tag_with_type type_sys T
746 Simple_Types level =>
747 SOME o mangled_type_name o homogenized_type ctxt nonmono_Ts level
749 fun do_out_of_bound_type (s, T) =
750 if should_predicate_on_type ctxt nonmono_Ts type_sys T then
751 type_pred_combatom ctxt nonmono_Ts type_sys T (CombVar (s, T))
752 |> do_formula |> SOME
755 and do_formula (AQuant (q, xs, phi)) =
756 AQuant (q, xs |> map (apsnd (fn NONE => NONE
757 | SOME T => do_bound_type T)),
758 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
760 (fn (_, NONE) => NONE
761 | (s, SOME T) => do_out_of_bound_type (s, T)) xs)
763 | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
764 | do_formula (AAtom tm) = AAtom (do_term true tm)
767 fun bound_atomic_types type_sys Ts =
768 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
769 (atp_type_literals_for_types type_sys Axiom Ts))
771 fun formula_for_fact ctxt nonmono_Ts type_sys
772 ({combformula, atomic_types, ...} : translated_formula) =
774 |> close_combformula_universally
775 |> formula_from_combformula ctxt nonmono_Ts type_sys
776 |> bound_atomic_types type_sys atomic_types
777 |> close_formula_universally
779 fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
781 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
782 of monomorphization). The TPTP explicitly forbids name clashes, and some of
783 the remote provers might care. *)
784 fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
785 (j, formula as {name, locality, kind, ...}) =
786 Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
787 else string_of_int j ^ "_") ^
789 kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
790 if generate_useful_info then
792 Intro => useful_isabelle_info "intro"
793 | Elim => useful_isabelle_info "elim"
794 | Simp => useful_isabelle_info "simp"
799 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
801 let val ty_arg = ATerm (`I "T", []) in
802 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
803 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
804 AAtom (ATerm (superclass, [ty_arg]))])
805 |> close_formula_universally, NONE, NONE)
808 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
809 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
810 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
811 (false, ATerm (c, [ATerm (sort, [])]))
813 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
815 Formula (arity_clause_prefix ^ ascii_of name, Axiom,
816 mk_ahorn (map (formula_from_fo_literal o apfst not
817 o fo_literal_from_arity_literal) premLits)
818 (formula_from_fo_literal
819 (fo_literal_from_arity_literal conclLit))
820 |> close_formula_universally, NONE, NONE)
822 fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
823 ({name, kind, combformula, ...} : translated_formula) =
824 Formula (conjecture_prefix ^ name, kind,
825 formula_from_combformula ctxt nonmono_Ts type_sys
826 (close_combformula_universally combformula)
827 |> close_formula_universally, NONE, NONE)
829 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
830 atomic_types |> atp_type_literals_for_types type_sys Conjecture
831 |> map fo_literal_from_type_literal
833 fun formula_line_for_free_type j lit =
834 Formula (tfree_prefix ^ string_of_int j, Hypothesis,
835 formula_from_fo_literal lit, NONE, NONE)
836 fun formula_lines_for_free_types type_sys facts =
838 val litss = map (free_type_literals type_sys) facts
839 val lits = fold (union (op =)) litss []
840 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
842 (** Symbol declarations **)
844 fun insert_type get_T x xs =
845 let val T = get_T x in
846 if exists (curry Type.raw_instance T o get_T) xs then xs
847 else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
850 fun should_declare_sym type_sys pred_sym s =
851 not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
852 not (String.isPrefix "$" s) andalso
853 ((case type_sys of Simple_Types _ => true | _ => false) orelse not pred_sym)
855 fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
857 fun add_combterm in_conj tm =
858 let val (head, args) = strip_combterm_comb tm in
860 CombConst ((s, s'), T, T_args) =>
861 let val pred_sym = is_pred_sym repaired_sym_tab s in
862 if should_declare_sym type_sys pred_sym s then
863 Symtab.map_default (s, [])
864 (insert_type #3 (s', T_args, T, pred_sym, length args,
870 #> fold (add_combterm in_conj) args
872 fun add_fact in_conj =
873 fact_lift (formula_fold true (K (add_combterm in_conj)))
876 |> is_type_sys_fairly_sound type_sys
877 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
880 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
881 String.isPrefix bound_var_prefix s
882 | is_var_or_bound_var (CombVar _) = true
883 | is_var_or_bound_var _ = false
885 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
886 out with monotonicity" paper presented at CADE 2011. *)
887 fun add_combterm_nonmonotonic_types _ (SOME false) _ = I
888 | add_combterm_nonmonotonic_types ctxt _
889 (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
891 (exists is_var_or_bound_var [tm1, tm2] andalso
892 not (is_type_surely_infinite ctxt T)) ? insert_type I T
893 | add_combterm_nonmonotonic_types _ _ _ = I
894 fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
895 : translated_formula) =
896 formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
898 fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
899 level_of_type_sys type_sys = Nonmonotonic_Types
900 ? (fold (add_fact_nonmonotonic_types ctxt) facts
901 (* in case helper "True_or_False" is included *)
902 #> insert_type I @{typ bool})
904 fun n_ary_strip_type 0 T = ([], T)
905 | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
906 n_ary_strip_type (n - 1) ran_T |>> cons dom_T
907 | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
909 fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd
911 fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
912 let val (arg_Ts, res_T) = n_ary_strip_type ary T in
913 Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
914 if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
917 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
919 fun formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s j
920 (s', T_args, T, _, ary, in_conj) =
922 val (kind, maybe_negate) =
923 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
925 val (arg_Ts, res_T) = n_ary_strip_type ary T
927 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
929 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
931 arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
934 Formula (sym_decl_prefix ^ s ^
935 (if n > 1 then "_" ^ string_of_int j else ""), kind,
936 CombConst ((s, s'), T, T_args)
937 |> fold (curry (CombApp o swap)) bound_tms
938 |> type_pred_combatom ctxt nonmono_Ts type_sys res_T
939 |> mk_aquant AForall (bound_names ~~ bound_Ts)
940 |> formula_from_combformula ctxt nonmono_Ts type_sys
941 |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
942 |> close_formula_universally
947 fun problem_lines_for_sym_decls ctxt conj_sym_kind nonmono_Ts type_sys
950 Simple_Types _ => map (decl_line_for_sym s) decls
955 decl :: (decls' as _ :: _) =>
956 let val T = result_type_of_decl decl in
957 if forall ((fn T' => Type.raw_instance (T', T))
958 o result_type_of_decl) decls' then
966 decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
967 o result_type_of_decl)
969 (0 upto length decls - 1, decls)
970 |-> map2 (formula_line_for_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys
974 fun problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
976 Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind
980 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
981 union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
982 | add_tff_types_in_formula (AConn (_, phis)) =
983 fold add_tff_types_in_formula phis
984 | add_tff_types_in_formula (AAtom _) = I
986 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
987 union (op =) (res_T :: arg_Ts)
988 | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
989 add_tff_types_in_formula phi
991 fun tff_types_in_problem problem =
992 fold (fold add_tff_types_in_problem_line o snd) problem []
994 fun decl_line_for_tff_type (s, s') =
995 Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
997 val type_declsN = "Types"
998 val sym_declsN = "Symbol types"
999 val factsN = "Relevant facts"
1000 val class_relsN = "Class relationships"
1001 val aritiesN = "Arities"
1002 val helpersN = "Helper facts"
1003 val conjsN = "Conjectures"
1004 val free_typesN = "Type variables"
1006 fun offset_of_heading_in_problem _ [] j = j
1007 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1008 if heading = needle then j
1009 else offset_of_heading_in_problem needle problem (j + length lines)
1011 fun prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys explicit_apply
1012 hyp_ts concl_t facts =
1014 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1015 translate_formulas ctxt prem_kind type_sys hyp_ts concl_t facts
1016 val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
1018 [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys) [facts, conjs]
1019 val repair = repair_fact ctxt nonmono_Ts type_sys sym_tab
1020 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1021 val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
1023 repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
1024 val sym_decl_lines =
1025 (conjs, helpers @ facts)
1026 |> sym_decl_table_for_facts type_sys repaired_sym_tab
1027 |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
1028 (* Reordering these might confuse the proof reconstruction code or the SPASS
1031 [(sym_declsN, sym_decl_lines),
1032 (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
1033 (0 upto length facts - 1 ~~ facts)),
1034 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1035 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1036 (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
1038 (0 upto length helpers - 1 ~~ helpers)
1039 |> (case type_sys of
1040 Tags (Polymorphic, level) =>
1041 is_type_level_partial level
1042 ? cons (ti_ti_helper_fact ())
1044 (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
1046 (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
1049 |> (case type_sys of
1052 map decl_line_for_tff_type (tff_types_in_problem problem))
1054 val (problem, pool) =
1055 problem |> nice_atp_problem (Config.get ctxt readable_names)
1058 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1059 offset_of_heading_in_problem conjsN problem 0,
1060 offset_of_heading_in_problem factsN problem 0,
1061 fact_names |> Vector.fromList)
1065 val conj_weight = 0.0
1066 val hyp_weight = 0.1
1067 val fact_min_weight = 0.2
1068 val fact_max_weight = 1.0
1069 val type_info_default_weight = 0.8
1071 fun add_term_weights weight (ATerm (s, tms)) =
1072 (not (is_atp_variable s) andalso s <> "equal" andalso
1073 not (String.isPrefix "$" s)) ? Symtab.default (s, weight)
1074 #> fold (add_term_weights weight) tms
1075 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1076 formula_fold true (K (add_term_weights weight)) phi
1077 | add_problem_line_weights _ _ = I
1079 fun add_conjectures_weights [] = I
1080 | add_conjectures_weights conjs =
1081 let val (hyps, conj) = split_last conjs in
1082 add_problem_line_weights conj_weight conj
1083 #> fold (add_problem_line_weights hyp_weight) hyps
1086 fun add_facts_weights facts =
1088 val num_facts = length facts
1090 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
1091 / Real.fromInt num_facts
1093 map weight_of (0 upto num_facts - 1) ~~ facts
1094 |> fold (uncurry add_problem_line_weights)
1097 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
1098 fun atp_problem_weights problem =
1099 let val get = these o AList.lookup (op =) problem in
1101 |> add_conjectures_weights (get free_typesN @ get conjsN)
1102 |> add_facts_weights (get factsN)
1103 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
1104 [sym_declsN, class_relsN, aritiesN]
1106 |> sort (prod_ord Real.compare string_ord o pairself swap)