1 (* Title: HOL/Tools/ATP/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 ATP_TRANSLATE =
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
12 type connective = ATP_Problem.connective
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
14 type format = ATP_Problem.format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
19 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
22 datatype order = First_Order | Higher_Order
23 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
25 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
27 datatype type_heaviness = Heavyweight | Lightweight
30 Simple_Types of order * type_level |
31 Preds of polymorphism * type_level * type_heaviness |
32 Tags of polymorphism * type_level * type_heaviness
34 val bound_var_prefix : string
35 val schematic_var_prefix : string
36 val fixed_var_prefix : string
37 val tvar_prefix : string
38 val tfree_prefix : string
39 val const_prefix : string
40 val type_const_prefix : string
41 val class_prefix : string
42 val skolem_const_prefix : string
43 val old_skolem_const_prefix : string
44 val new_skolem_const_prefix : string
45 val type_decl_prefix : string
46 val sym_decl_prefix : string
47 val preds_sym_formula_prefix : string
48 val lightweight_tags_sym_formula_prefix : string
49 val fact_prefix : string
50 val conjecture_prefix : string
51 val helper_prefix : string
52 val class_rel_clause_prefix : string
53 val arity_clause_prefix : string
54 val tfree_clause_prefix : string
55 val typed_helper_suffix : string
56 val untyped_helper_suffix : string
57 val type_tag_idempotence_helper_name : string
58 val predicator_name : string
59 val app_op_name : string
60 val type_tag_name : string
61 val type_pred_name : string
62 val simple_type_prefix : string
63 val prefixed_predicator_name : string
64 val prefixed_app_op_name : string
65 val prefixed_type_tag_name : string
66 val concealed_lambdasN : string
67 val lambda_liftingN : string
68 val combinatorsN : string
71 val lambda_translation : string Config.T
72 val ascii_of : string -> string
73 val unascii_of : string -> string
74 val strip_prefix_and_unascii : string -> string -> string option
75 val proxy_table : (string * (string * (thm * (string * string)))) list
76 val proxify_const : string -> (string * string) option
77 val invert_const : string -> string
78 val unproxify_const : string -> string
79 val new_skolem_var_name_from_const : string -> string
80 val num_type_args : theory -> string -> int
81 val atp_irrelevant_consts : string list
82 val atp_schematic_consts_of : term -> typ list Symtab.table
83 val is_locality_global : locality -> bool
84 val type_enc_from_string : string -> type_enc
85 val polymorphism_of_type_enc : type_enc -> polymorphism
86 val level_of_type_enc : type_enc -> type_level
87 val is_type_enc_virtually_sound : type_enc -> bool
88 val is_type_enc_fairly_sound : type_enc -> bool
89 val choose_format : format list -> type_enc -> format * type_enc
91 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
92 val unmangled_const : string -> string * (string, 'b) ho_term list
93 val unmangled_const_name : string -> string
94 val helper_table : ((string * bool) * thm list) list
96 val prepare_atp_problem :
97 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
98 -> bool -> bool -> bool -> term list -> term
99 -> ((string * locality) * term) list
100 -> string problem * string Symtab.table * int * int
101 * (string * locality) list vector * int list * int Symtab.table
102 val atp_problem_weights : string problem -> (string * real) list
105 structure ATP_Translate : ATP_TRANSLATE =
111 type name = string * string
114 val generate_info = false
116 fun isabelle_info s =
117 if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
124 val bound_var_prefix = "B_"
125 val schematic_var_prefix = "V_"
126 val fixed_var_prefix = "v_"
128 val tvar_prefix = "T_"
129 val tfree_prefix = "t_"
131 val const_prefix = "c_"
132 val type_const_prefix = "tc_"
133 val class_prefix = "cl_"
135 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
136 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
137 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
139 val type_decl_prefix = "ty_"
140 val sym_decl_prefix = "sy_"
141 val preds_sym_formula_prefix = "psy_"
142 val lightweight_tags_sym_formula_prefix = "tsy_"
143 val fact_prefix = "fact_"
144 val conjecture_prefix = "conj_"
145 val helper_prefix = "help_"
146 val class_rel_clause_prefix = "clar_"
147 val arity_clause_prefix = "arity_"
148 val tfree_clause_prefix = "tfree_"
150 val typed_helper_suffix = "_T"
151 val untyped_helper_suffix = "_U"
152 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
154 val predicator_name = "hBOOL"
155 val app_op_name = "hAPP"
156 val type_tag_name = "ti"
157 val type_pred_name = "is"
158 val simple_type_prefix = "ty_"
160 val prefixed_predicator_name = const_prefix ^ predicator_name
161 val prefixed_app_op_name = const_prefix ^ app_op_name
162 val prefixed_type_tag_name = const_prefix ^ type_tag_name
164 (* Freshness almost guaranteed! *)
165 val sledgehammer_weak_prefix = "Sledgehammer:"
167 val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
169 val concealed_lambdasN = "concealed_lambdas"
170 val lambda_liftingN = "lambda_lifting"
171 val combinatorsN = "combinators"
172 val lambdasN = "lambdas"
175 val lambda_translation =
176 Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
178 (*Escaping of special characters.
179 Alphanumeric characters are left unchanged.
180 The character _ goes to __
181 Characters in the range ASCII space to / go to _A to _P, respectively.
182 Other characters go to _nnn where nnn is the decimal ASCII code.*)
183 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
185 fun stringN_of_int 0 _ = ""
186 | stringN_of_int k n =
187 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
189 fun ascii_of_char c =
190 if Char.isAlphaNum c then
192 else if c = #"_" then
194 else if #" " <= c andalso c <= #"/" then
195 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
197 (* fixed width, in case more digits follow *)
198 "_" ^ stringN_of_int 3 (Char.ord c)
200 val ascii_of = String.translate ascii_of_char
202 (** Remove ASCII armoring from names in proof files **)
204 (* We don't raise error exceptions because this code can run inside a worker
205 thread. Also, the errors are impossible. *)
208 fun un rcs [] = String.implode(rev rcs)
209 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
210 (* Three types of _ escapes: __, _A to _P, _nnn *)
211 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
212 | un rcs (#"_" :: c :: cs) =
213 if #"A" <= c andalso c<= #"P" then
214 (* translation of #" " to #"/" *)
215 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
217 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
218 case Int.fromString (String.implode digits) of
219 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
220 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
222 | un rcs (c :: cs) = un (c :: rcs) cs
223 in un [] o String.explode end
225 (* If string s has the prefix s1, return the result of deleting it,
227 fun strip_prefix_and_unascii s1 s =
228 if String.isPrefix s1 s then
229 SOME (unascii_of (String.extract (s, size s1, NONE)))
234 [("c_False", (@{const_name False}, (@{thm fFalse_def},
235 ("fFalse", @{const_name ATP.fFalse})))),
236 ("c_True", (@{const_name True}, (@{thm fTrue_def},
237 ("fTrue", @{const_name ATP.fTrue})))),
238 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
239 ("fNot", @{const_name ATP.fNot})))),
240 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
241 ("fconj", @{const_name ATP.fconj})))),
242 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
243 ("fdisj", @{const_name ATP.fdisj})))),
244 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
245 ("fimplies", @{const_name ATP.fimplies})))),
246 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
247 ("fequal", @{const_name ATP.fequal})))),
248 ("c_All", (@{const_name All}, (@{thm fAll_def},
249 ("fAll", @{const_name ATP.fAll})))),
250 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
251 ("fEx", @{const_name ATP.fEx}))))]
253 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
255 (* Readable names for the more common symbolic functions. Do not mess with the
256 table unless you know what you are doing. *)
257 val const_trans_table =
258 [(@{type_name Product_Type.prod}, "prod"),
259 (@{type_name Sum_Type.sum}, "sum"),
260 (@{const_name False}, "False"),
261 (@{const_name True}, "True"),
262 (@{const_name Not}, "Not"),
263 (@{const_name conj}, "conj"),
264 (@{const_name disj}, "disj"),
265 (@{const_name implies}, "implies"),
266 (@{const_name HOL.eq}, "equal"),
267 (@{const_name All}, "All"),
268 (@{const_name Ex}, "Ex"),
269 (@{const_name If}, "If"),
270 (@{const_name Set.member}, "member"),
271 (@{const_name Meson.COMBI}, "COMBI"),
272 (@{const_name Meson.COMBK}, "COMBK"),
273 (@{const_name Meson.COMBB}, "COMBB"),
274 (@{const_name Meson.COMBC}, "COMBC"),
275 (@{const_name Meson.COMBS}, "COMBS")]
277 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
279 (* Invert the table of translations between Isabelle and ATPs. *)
280 val const_trans_table_inv =
281 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
282 val const_trans_table_unprox =
284 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
286 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
287 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
290 case Symtab.lookup const_trans_table c of
294 fun ascii_of_indexname (v, 0) = ascii_of v
295 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
297 fun make_bound_var x = bound_var_prefix ^ ascii_of x
298 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
299 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
301 fun make_schematic_type_var (x, i) =
302 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
303 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
305 (* "HOL.eq" is mapped to the ATP's equality. *)
306 fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
307 | make_fixed_const c = const_prefix ^ lookup_const c
309 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
311 fun make_type_class clas = class_prefix ^ ascii_of clas
313 fun new_skolem_var_name_from_const s =
314 let val ss = s |> space_explode Long_Name.separator in
315 nth ss (length ss - 2)
318 (* The number of type arguments of a constant, zero if it's monomorphic. For
319 (instances of) Skolem pseudoconstants, this information is encoded in the
321 fun num_type_args thy s =
322 if String.isPrefix skolem_const_prefix s then
323 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
325 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
327 (* These are either simplified away by "Meson.presimplify" (most of the time) or
328 handled specially via "fFalse", "fTrue", ..., "fequal". *)
329 val atp_irrelevant_consts =
330 [@{const_name False}, @{const_name True}, @{const_name Not},
331 @{const_name conj}, @{const_name disj}, @{const_name implies},
332 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
334 val atp_monomorph_bad_consts =
335 atp_irrelevant_consts @
336 (* These are ignored anyway by the relevance filter (unless they appear in
337 higher-order places) but not by the monomorphizer. *)
338 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
339 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
340 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
342 fun add_schematic_const (x as (_, T)) =
343 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
344 val add_schematic_consts_of =
345 Term.fold_aterms (fn Const (x as (s, _)) =>
346 not (member (op =) atp_monomorph_bad_consts s)
347 ? add_schematic_const x
349 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
351 (** Definitions and functions for FOL clauses and formulas for TPTP **)
353 (* The first component is the type class; the second is a "TVar" or "TFree". *)
354 datatype type_literal =
355 TyLitVar of name * name |
356 TyLitFree of name * name
359 (** Isabelle arities **)
361 datatype arity_literal =
362 TConsLit of name * name * name list |
363 TVarLit of name * name
366 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
368 val type_class = the_single @{sort type}
370 fun add_packed_sort tvar =
371 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
375 prem_lits : arity_literal list,
376 concl_lits : arity_literal}
378 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
379 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
381 val tvars = gen_TVars (length args)
382 val tvars_srts = ListPair.zip (tvars, args)
385 prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
386 concl_lits = TConsLit (`make_type_class cls,
387 `make_fixed_type_const tcons,
391 fun arity_clause _ _ (_, []) = []
392 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
393 arity_clause seen n (tcons, ars)
394 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
395 if member (op =) seen class then
396 (* multiple arities for the same (tycon, class) pair *)
397 make_axiom_arity_clause (tcons,
398 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
400 arity_clause seen (n + 1) (tcons, ars)
402 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
403 ascii_of class, ar) ::
404 arity_clause (class :: seen) n (tcons, ars)
406 fun multi_arity_clause [] = []
407 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
408 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
410 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
411 theory thy provided its arguments have the corresponding sorts. *)
412 fun type_class_pairs thy tycons classes =
414 val alg = Sign.classes_of thy
415 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
416 fun add_class tycon class =
417 cons (class, domain_sorts tycon class)
418 handle Sorts.CLASS_ERROR _ => I
419 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
420 in map try_classes tycons end
422 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
423 fun iter_type_class_pairs _ _ [] = ([], [])
424 | iter_type_class_pairs thy tycons classes =
426 fun maybe_insert_class s =
427 (s <> type_class andalso not (member (op =) classes s))
429 val cpairs = type_class_pairs thy tycons classes
431 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
432 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
433 in (classes' @ classes, union (op =) cpairs' cpairs) end
435 fun make_arity_clauses thy tycons =
436 iter_type_class_pairs thy tycons ##> multi_arity_clause
439 (** Isabelle class relations **)
441 type class_rel_clause =
446 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
448 fun class_pairs _ [] _ = []
449 | class_pairs thy subs supers =
451 val class_less = Sorts.class_less (Sign.classes_of thy)
452 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
453 fun add_supers sub = fold (add_super sub) supers
454 in fold add_supers subs [] end
456 fun make_class_rel_clause (sub, super) =
457 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
458 superclass = `make_type_class super}
460 fun make_class_rel_clauses thy subs supers =
461 map make_class_rel_clause (class_pairs thy subs supers)
464 CombConst of name * typ * typ list |
465 CombVar of name * typ |
466 CombApp of combterm * combterm |
467 CombAbs of (name * typ) * combterm
469 fun combtyp_of (CombConst (_, T, _)) = T
470 | combtyp_of (CombVar (_, T)) = T
471 | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
472 | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
474 (*gets the head of a combinator application, along with the list of arguments*)
475 fun strip_combterm_comb u =
477 fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
479 in stripc (u, []) end
481 fun atyps_of T = fold_atyps (insert (op =)) T []
483 fun new_skolem_const_name s num_T_args =
484 [new_skolem_const_prefix, s, string_of_int num_T_args]
485 |> space_implode Long_Name.separator
487 (* Converts a term (with combinators) into a combterm. Also accumulates sort
489 fun combterm_from_term thy bs (P $ Q) =
491 val (P', P_atomics_Ts) = combterm_from_term thy bs P
492 val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
493 in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
494 | combterm_from_term thy _ (Const (c, T)) =
497 (if String.isPrefix old_skolem_const_prefix c then
498 [] |> Term.add_tvarsT T |> map TVar
500 (c, T) |> Sign.const_typargs thy)
501 val c' = CombConst (`make_fixed_const c, T, tvar_list)
502 in (c', atyps_of T) end
503 | combterm_from_term _ _ (Free (v, T)) =
504 (CombConst (`make_fixed_var v, T, []), atyps_of T)
505 | combterm_from_term _ _ (Var (v as (s, _), T)) =
506 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
508 val Ts = T |> strip_type |> swap |> op ::
509 val s' = new_skolem_const_name s (length Ts)
510 in CombConst (`make_fixed_const s', T, Ts) end
512 CombVar ((make_schematic_var v, s), T), atyps_of T)
513 | combterm_from_term _ bs (Bound j) =
515 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
516 | combterm_from_term thy bs (Abs (s, T, t)) =
518 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
520 val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
522 (CombAbs ((`make_bound_var s, T), tm),
523 union (op =) atomic_Ts (atyps_of T))
527 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
530 (* (quasi-)underapproximation of the truth *)
531 fun is_locality_global Local = false
532 | is_locality_global Assum = false
533 | is_locality_global Chained = false
534 | is_locality_global _ = true
536 datatype order = First_Order | Higher_Order
537 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
538 datatype type_level =
539 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
541 datatype type_heaviness = Heavyweight | Lightweight
544 Simple_Types of order * type_level |
545 Preds of polymorphism * type_level * type_heaviness |
546 Tags of polymorphism * type_level * type_heaviness
548 fun try_unsuffixes ss s =
549 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
551 fun type_enc_from_string s =
552 (case try (unprefix "poly_") s of
553 SOME s => (SOME Polymorphic, s)
555 case try (unprefix "mono_") s of
556 SOME s => (SOME Monomorphic, s)
558 case try (unprefix "mangled_") s of
559 SOME s => (SOME Mangled_Monomorphic, s)
562 (* "_query" and "_bang" are for the ASCII-challenged Metis and
564 case try_unsuffixes ["?", "_query"] s of
565 SOME s => (Noninf_Nonmono_Types, s)
567 case try_unsuffixes ["!", "_bang"] s of
568 SOME s => (Fin_Nonmono_Types, s)
569 | NONE => (All_Types, s))
571 case try (unsuffix "_heavy") s of
572 SOME s => (Heavyweight, s)
573 | NONE => (Lightweight, s))
574 |> (fn (poly, (level, (heaviness, core))) =>
575 case (core, (poly, level, heaviness)) of
576 ("simple", (NONE, _, Lightweight)) =>
577 Simple_Types (First_Order, level)
578 | ("simple_higher", (NONE, _, Lightweight)) =>
579 if level = Noninf_Nonmono_Types then raise Same.SAME
580 else Simple_Types (Higher_Order, level)
581 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
582 | ("tags", (SOME Polymorphic, _, _)) =>
583 Tags (Polymorphic, level, heaviness)
584 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
585 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
586 Preds (poly, Const_Arg_Types, Lightweight)
587 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
588 Preds (Polymorphic, No_Types, Lightweight)
589 | _ => raise Same.SAME)
590 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
592 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
593 | is_type_enc_higher_order _ = false
595 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
596 | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
597 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
599 fun level_of_type_enc (Simple_Types (_, level)) = level
600 | level_of_type_enc (Preds (_, level, _)) = level
601 | level_of_type_enc (Tags (_, level, _)) = level
603 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
604 | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
605 | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
607 fun is_type_level_virtually_sound level =
608 level = All_Types orelse level = Noninf_Nonmono_Types
609 val is_type_enc_virtually_sound =
610 is_type_level_virtually_sound o level_of_type_enc
612 fun is_type_level_fairly_sound level =
613 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
614 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
616 fun effective_lambda_translation ctxt type_enc =
617 Config.get ctxt lambda_translation
619 if trans = smartN then
620 if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
624 fun choose_format formats (Simple_Types (order, level)) =
625 if member (op =) formats THF then
626 (THF, Simple_Types (order, level))
627 else if member (op =) formats TFF then
628 (TFF, Simple_Types (First_Order, level))
630 choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
631 | choose_format formats type_enc =
634 (CNF_UEQ, case type_enc of
636 (if is_type_enc_fairly_sound type_enc then Tags else Preds)
639 | format => (format, type_enc))
641 type translated_formula =
645 combformula : (name, typ, combterm) formula,
646 atomic_types : typ list}
648 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
649 : translated_formula) =
650 {name = name, locality = locality, kind = kind, combformula = f combformula,
651 atomic_types = atomic_types} : translated_formula
653 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
655 val type_instance = Sign.typ_instance o Proof_Context.theory_of
657 fun insert_type ctxt get_T x xs =
658 let val T = get_T x in
659 if exists (curry (type_instance ctxt) T o get_T) xs then xs
660 else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
663 (* The Booleans indicate whether all type arguments should be kept. *)
664 datatype type_arg_policy =
665 Explicit_Type_Args of bool |
666 Mangled_Type_Args of bool |
669 fun should_drop_arg_type_args (Simple_Types _) =
670 false (* since TFF doesn't support overloading *)
671 | should_drop_arg_type_args type_enc =
672 level_of_type_enc type_enc = All_Types andalso
673 heaviness_of_type_enc type_enc = Heavyweight
675 fun type_arg_policy type_enc s =
676 if s = type_tag_name then
677 (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
680 Explicit_Type_Args) false
681 else case type_enc of
682 Tags (_, All_Types, Heavyweight) => No_Type_Args
684 if level_of_type_enc type_enc = No_Types orelse
685 s = @{const_name HOL.eq} orelse
686 (s = app_op_name andalso
687 level_of_type_enc type_enc = Const_Arg_Types) then
690 should_drop_arg_type_args type_enc
691 |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
696 (* Make literals for sorted type variables. *)
697 fun generic_add_sorts_on_type (_, []) = I
698 | generic_add_sorts_on_type ((x, i), s :: ss) =
699 generic_add_sorts_on_type ((x, i), ss)
700 #> (if s = the_single @{sort HOL.type} then
703 insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
705 insert (op =) (TyLitVar (`make_type_class s,
706 (make_schematic_type_var (x, i), x))))
707 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
708 | add_sorts_on_tfree _ = I
709 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
710 | add_sorts_on_tvar _ = I
712 fun type_literals_for_types type_enc add_sorts_on_typ Ts =
713 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
715 fun mk_aconns c phis =
716 let val (phis', phi') = split_last phis in
717 fold_rev (mk_aconn c) phis' phi'
719 fun mk_ahorn [] phi = phi
720 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
721 fun mk_aquant _ [] phi = phi
722 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
723 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
724 | mk_aquant q xs phi = AQuant (q, xs, phi)
726 fun close_universally atom_vars phi =
728 fun formula_vars bounds (AQuant (_, xs, phi)) =
729 formula_vars (map fst xs @ bounds) phi
730 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
731 | formula_vars bounds (AAtom tm) =
732 union (op =) (atom_vars tm []
733 |> filter_out (member (op =) bounds o fst))
734 in mk_aquant AForall (formula_vars [] phi []) phi end
736 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
737 | combterm_vars (CombConst _) = I
738 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
739 | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
740 fun close_combformula_universally phi = close_universally combterm_vars phi
742 fun term_vars bounds (ATerm (name as (s, _), tms)) =
743 (is_tptp_variable s andalso not (member (op =) bounds name))
744 ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
745 | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
746 fun close_formula_universally phi = close_universally (term_vars []) phi
748 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
749 val homo_infinite_type = Type (homo_infinite_type_name, [])
751 fun ho_term_from_typ format type_enc =
753 fun term (Type (s, Ts)) =
754 ATerm (case (is_type_enc_higher_order type_enc, s) of
755 (true, @{type_name bool}) => `I tptp_bool_type
756 | (true, @{type_name fun}) => `I tptp_fun_type
757 | _ => if s = homo_infinite_type_name andalso
758 (format = TFF orelse format = THF) then
759 `I tptp_individual_type
761 `make_fixed_type_const s,
763 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
764 | term (TVar ((x as (s, _)), _)) =
765 ATerm ((make_schematic_type_var x, s), [])
768 fun ho_term_for_type_arg format type_enc T =
769 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
771 (* This shouldn't clash with anything else. *)
772 val mangled_type_sep = "\000"
774 fun generic_mangled_type_name f (ATerm (name, [])) = f name
775 | generic_mangled_type_name f (ATerm (name, tys)) =
776 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
778 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
780 val bool_atype = AType (`I tptp_bool_type)
782 fun make_simple_type s =
783 if s = tptp_bool_type orelse s = tptp_fun_type orelse
784 s = tptp_individual_type then
787 simple_type_prefix ^ ascii_of s
789 fun ho_type_from_ho_term type_enc pred_sym ary =
792 AType ((make_simple_type (generic_mangled_type_name fst ty),
793 generic_mangled_type_name snd ty))
794 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
795 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
796 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
797 | to_fo _ _ = raise Fail "unexpected type abstraction"
798 fun to_ho (ty as ATerm ((s, _), tys)) =
799 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
800 | to_ho _ = raise Fail "unexpected type abstraction"
801 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
803 fun ho_type_from_typ format type_enc pred_sym ary =
804 ho_type_from_ho_term type_enc pred_sym ary
805 o ho_term_from_typ format type_enc
807 fun mangled_const_name format type_enc T_args (s, s') =
809 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
810 fun type_suffix f g =
811 fold_rev (curry (op ^) o g o prefix mangled_type_sep
812 o generic_mangled_type_name f) ty_args ""
813 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
815 val parse_mangled_ident =
816 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
818 fun parse_mangled_type x =
820 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
822 and parse_mangled_types x =
823 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
825 fun unmangled_type s =
826 s |> suffix ")" |> raw_explode
827 |> Scan.finite Symbol.stopper
828 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
829 quote s)) parse_mangled_type))
832 val unmangled_const_name = space_explode mangled_type_sep #> hd
833 fun unmangled_const s =
834 let val ss = space_explode mangled_type_sep s in
835 (hd ss, map unmangled_type (tl ss))
838 fun introduce_proxies type_enc =
840 fun intro top_level (CombApp (tm1, tm2)) =
841 CombApp (intro top_level tm1, intro false tm2)
842 | intro top_level (CombConst (name as (s, _), T, T_args)) =
843 (case proxify_const s of
845 if top_level orelse is_type_enc_higher_order type_enc then
846 case (top_level, s) of
847 (_, "c_False") => (`I tptp_false, [])
848 | (_, "c_True") => (`I tptp_true, [])
849 | (false, "c_Not") => (`I tptp_not, [])
850 | (false, "c_conj") => (`I tptp_and, [])
851 | (false, "c_disj") => (`I tptp_or, [])
852 | (false, "c_implies") => (`I tptp_implies, [])
853 | (false, "c_All") => (`I tptp_ho_forall, [])
854 | (false, "c_Ex") => (`I tptp_ho_exists, [])
856 if is_tptp_equal s then (`I tptp_equal, [])
857 else (proxy_base |>> prefix const_prefix, T_args)
860 (proxy_base |>> prefix const_prefix, T_args)
861 | NONE => (name, T_args))
862 |> (fn (name, T_args) => CombConst (name, T, T_args))
863 | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
867 fun combformula_from_prop thy type_enc eq_as_iff =
869 fun do_term bs t atomic_types =
870 combterm_from_term thy bs (Envir.eta_contract t)
871 |>> (introduce_proxies type_enc #> AAtom)
872 ||> union (op =) atomic_types
873 fun do_quant bs q s T t' =
874 let val s = singleton (Name.variant_list (map fst bs)) s in
875 do_formula ((s, T) :: bs) t'
876 #>> mk_aquant q [(`make_bound_var s, SOME T)]
878 and do_conn bs c t1 t2 =
879 do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
880 and do_formula bs t =
882 @{const Trueprop} $ t1 => do_formula bs t1
883 | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
884 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
885 do_quant bs AForall s T t'
886 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
887 do_quant bs AExists s T t'
888 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
889 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
890 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
891 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
892 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
896 fun presimplify_term _ [] t = t
897 | presimplify_term ctxt presimp_consts t =
898 t |> exists_Const (member (op =) presimp_consts o fst) t
899 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
900 #> Meson.presimplify ctxt
903 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
904 fun conceal_bounds Ts t =
905 subst_bounds (map (Free o apfst concealed_bound_name)
906 (0 upto length Ts - 1 ~~ Ts), t)
907 fun reveal_bounds Ts =
908 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
909 (0 upto length Ts - 1 ~~ Ts))
911 fun is_fun_equality (@{const_name HOL.eq},
912 Type (_, [Type (@{type_name fun}, _), _])) = true
913 | is_fun_equality _ = false
915 fun extensionalize_term ctxt t =
916 if exists_Const is_fun_equality t then
917 let val thy = Proof_Context.theory_of ctxt in
918 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
919 |> prop_of |> Logic.dest_equals |> snd
924 fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
925 | conceal_lambdas Ts (Abs (_, T, t)) =
926 Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
927 T --> fastype_of1 (Ts, t))
928 | conceal_lambdas _ t = t
930 fun process_abstractions_in_term ctxt type_enc kind t =
931 let val thy = Proof_Context.theory_of ctxt in
932 if Meson.is_fol_term thy t then
938 @{const Not} $ t1 => @{const Not} $ aux Ts t1
939 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
940 t0 $ Abs (s, T, aux (T :: Ts) t')
941 | (t0 as Const (@{const_name All}, _)) $ t1 =>
942 aux Ts (t0 $ eta_expand Ts t1 1)
943 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
944 t0 $ Abs (s, T, aux (T :: Ts) t')
945 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
946 aux Ts (t0 $ eta_expand Ts t1 1)
947 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
948 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
949 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
950 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
952 t0 $ aux Ts t1 $ aux Ts t2
954 if not (exists_subterm (fn Abs _ => true | _ => false) t) then
958 val trans = effective_lambda_translation ctxt type_enc
959 val t = t |> Envir.eta_contract
961 if trans = concealed_lambdasN then
962 t |> conceal_lambdas []
963 else if trans = lambda_liftingN then
964 t (* TODO: implement *)
965 else if trans = combinatorsN then
966 t |> conceal_bounds Ts
968 |> Meson_Clausify.introduce_combinators_in_cterm
969 |> prop_of |> Logic.dest_equals |> snd
971 else if trans = lambdasN then
974 error ("Unknown lambda translation: " ^ quote trans ^ ".")
976 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
977 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
979 (* A type variable of sort "{}" will make abstraction fail. *)
980 if kind = Conjecture then HOLogic.false_const
981 else HOLogic.true_const
984 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
985 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
988 fun aux (t $ u) = aux t $ aux u
989 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
990 | aux (Var ((s, i), T)) =
991 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
993 in t |> exists_subterm is_Var t ? aux end
995 fun preprocess_prop ctxt type_enc presimp_consts kind t =
997 val thy = Proof_Context.theory_of ctxt
998 val t = t |> Envir.beta_eta_contract
999 |> transform_elim_prop
1000 |> Object_Logic.atomize_term thy
1001 val need_trueprop = (fastype_of t = @{typ bool})
1003 t |> need_trueprop ? HOLogic.mk_Trueprop
1004 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
1005 |> extensionalize_term ctxt
1006 |> presimplify_term ctxt presimp_consts
1007 |> perhaps (try (HOLogic.dest_Trueprop))
1008 |> process_abstractions_in_term ctxt type_enc kind
1011 (* making fact and conjecture formulas *)
1012 fun make_formula thy type_enc eq_as_iff name loc kind t =
1014 val (combformula, atomic_types) =
1015 combformula_from_prop thy type_enc eq_as_iff t []
1017 {name = name, locality = loc, kind = kind, combformula = combformula,
1018 atomic_types = atomic_types}
1021 fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
1023 let val thy = Proof_Context.theory_of ctxt in
1024 case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
1025 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1027 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
1028 if s = tptp_true then NONE else SOME formula
1029 | formula => SOME formula
1032 fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
1034 val thy = Proof_Context.theory_of ctxt
1035 val last = length ts - 1
1037 map2 (fn j => fn t =>
1039 val (kind, maybe_negate) =
1044 if prem_kind = Conjecture then update_combformula mk_anot
1048 (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
1049 |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1056 (** Finite and infinite type inference **)
1058 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
1059 | deep_freeze_atyp T = T
1060 val deep_freeze_type = map_atyps deep_freeze_atyp
1062 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1063 dangerous because their "exhaust" properties can easily lead to unsound ATP
1064 proofs. On the other hand, all HOL infinite types can be given the same
1065 models in first-order logic (via Löwenheim-Skolem). *)
1067 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
1068 exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
1069 | should_encode_type _ _ All_Types _ = true
1070 | should_encode_type ctxt _ Fin_Nonmono_Types T =
1071 is_type_surely_finite ctxt false T
1072 | should_encode_type _ _ _ _ = false
1074 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
1075 should_predicate_on_var T =
1076 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
1077 should_encode_type ctxt nonmono_Ts level T
1078 | should_predicate_on_type _ _ _ _ _ = false
1080 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
1081 String.isPrefix bound_var_prefix s
1082 | is_var_or_bound_var (CombVar _) = true
1083 | is_var_or_bound_var _ = false
1086 Top_Level of bool option |
1087 Eq_Arg of bool option |
1090 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1091 | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
1094 Heavyweight => should_encode_type ctxt nonmono_Ts level T
1096 case (site, is_var_or_bound_var u) of
1097 (Eq_Arg pos, true) =>
1098 (* The first disjunct prevents a subtle soundness issue explained in
1099 Blanchette's Ph.D. thesis. See also
1100 "formula_lines_for_lightweight_tags_sym_decl". *)
1101 (pos <> SOME false andalso poly = Polymorphic andalso
1102 level <> All_Types andalso heaviness = Lightweight andalso
1103 exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
1104 should_encode_type ctxt nonmono_Ts level T
1106 | should_tag_with_type _ _ _ _ _ _ = false
1108 fun homogenized_type ctxt nonmono_Ts level =
1110 val should_encode = should_encode_type ctxt nonmono_Ts level
1111 fun homo 0 T = if should_encode T then T else homo_infinite_type
1112 | homo ary (Type (@{type_name fun}, [T1, T2])) =
1113 homo 0 T1 --> homo (ary - 1) T2
1114 | homo _ _ = raise Fail "expected function type"
1117 (** "hBOOL" and "hAPP" **)
1120 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1122 fun add_combterm_syms_to_table ctxt explicit_apply =
1124 fun consider_var_arity const_T var_T max_ary =
1127 if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
1128 type_instance ctxt (T, var_T) then
1131 iter (ary + 1) (range_type T)
1132 in iter 0 const_T end
1133 fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1134 if explicit_apply = NONE andalso
1135 (can dest_funT T orelse T = @{typ bool}) then
1137 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1138 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
1139 {pred_sym = pred_sym andalso not bool_vars',
1140 min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
1141 max_ary = max_ary, types = types}
1143 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1145 if bool_vars' = bool_vars andalso
1146 pointer_eq (fun_var_Ts', fun_var_Ts) then
1149 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
1153 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1154 let val (head, args) = strip_combterm_comb tm in
1156 CombConst ((s, _), T, _) =>
1157 if String.isPrefix bound_var_prefix s then
1158 add_var_or_bound_var T accum
1160 let val ary = length args in
1161 ((bool_vars, fun_var_Ts),
1162 case Symtab.lookup sym_tab s of
1163 SOME {pred_sym, min_ary, max_ary, types} =>
1166 pred_sym andalso top_level andalso not bool_vars
1167 val types' = types |> insert_type ctxt I T
1169 if is_some explicit_apply orelse
1170 pointer_eq (types', types) then
1173 fold (consider_var_arity T) fun_var_Ts min_ary
1175 Symtab.update (s, {pred_sym = pred_sym,
1176 min_ary = Int.min (ary, min_ary),
1177 max_ary = Int.max (ary, max_ary),
1183 val pred_sym = top_level andalso not bool_vars
1185 case explicit_apply of
1188 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1190 Symtab.update_new (s, {pred_sym = pred_sym,
1191 min_ary = min_ary, max_ary = ary,
1196 | CombVar (_, T) => add_var_or_bound_var T accum
1197 | CombAbs ((_, T), tm) =>
1198 accum |> add_var_or_bound_var T |> add false tm
1200 |> fold (add false) args
1203 fun add_fact_syms_to_table ctxt explicit_apply =
1204 fact_lift (formula_fold NONE
1205 (K (add_combterm_syms_to_table ctxt explicit_apply)))
1207 val default_sym_tab_entries : (string * sym_info) list =
1208 (prefixed_predicator_name,
1209 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
1210 ([tptp_false, tptp_true]
1211 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1212 ([tptp_equal, tptp_old_equal]
1213 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1215 fun sym_table_for_facts ctxt explicit_apply facts =
1216 ((false, []), Symtab.empty)
1217 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1218 |> fold Symtab.update default_sym_tab_entries
1220 fun min_arity_of sym_tab s =
1221 case Symtab.lookup sym_tab s of
1222 SOME ({min_ary, ...} : sym_info) => min_ary
1224 case strip_prefix_and_unascii const_prefix s of
1226 let val s = s |> unmangled_const_name |> invert_const in
1227 if s = predicator_name then 1
1228 else if s = app_op_name then 2
1229 else if s = type_pred_name then 1
1234 (* True if the constant ever appears outside of the top-level position in
1235 literals, or if it appears with different arities (e.g., because of different
1236 type instantiations). If false, the constant always receives all of its
1237 arguments and is used as a predicate. *)
1238 fun is_pred_sym sym_tab s =
1239 case Symtab.lookup sym_tab s of
1240 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1241 pred_sym andalso min_ary = max_ary
1244 val predicator_combconst =
1245 CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1246 fun predicator tm = CombApp (predicator_combconst, tm)
1248 fun introduce_predicators_in_combterm sym_tab tm =
1249 case strip_combterm_comb tm of
1250 (CombConst ((s, _), _, _), _) =>
1251 if is_pred_sym sym_tab s then tm else predicator tm
1252 | _ => predicator tm
1254 fun list_app head args = fold (curry (CombApp o swap)) args head
1256 val app_op = `make_fixed_const app_op_name
1258 fun explicit_app arg head =
1260 val head_T = combtyp_of head
1261 val (arg_T, res_T) = dest_funT head_T
1263 CombConst (app_op, head_T --> head_T, [arg_T, res_T])
1264 in list_app explicit_app [head, arg] end
1265 fun list_explicit_app head args = fold explicit_app args head
1267 fun introduce_explicit_apps_in_combterm sym_tab =
1270 case strip_combterm_comb tm of
1271 (head as CombConst ((s, _), _, _), args) =>
1273 |> chop (min_arity_of sym_tab s)
1275 |-> list_explicit_app
1276 | (head, args) => list_explicit_app head (map aux args)
1279 fun chop_fun 0 T = ([], T)
1280 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1281 chop_fun (n - 1) ran_T |>> cons dom_T
1282 | chop_fun _ _ = raise Fail "unexpected non-function"
1284 fun filter_type_args _ _ _ [] = []
1285 | filter_type_args thy s arity T_args =
1287 (* will throw "TYPE" for pseudo-constants *)
1288 val U = if s = app_op_name then
1289 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
1291 s |> Sign.the_const_type thy
1293 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1296 let val U_args = (s, U) |> Sign.const_typargs thy in
1298 |> map (fn (U, T) =>
1299 if member (op =) res_U_vars (dest_TVar U) then T
1303 handle TYPE _ => T_args
1305 fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
1307 val thy = Proof_Context.theory_of ctxt
1308 fun aux arity (CombApp (tm1, tm2)) =
1309 CombApp (aux (arity + 1) tm1, aux 0 tm2)
1310 | aux arity (CombConst (name as (s, _), T, T_args)) =
1311 (case strip_prefix_and_unascii const_prefix s of
1312 NONE => (name, T_args)
1315 val s'' = invert_const s''
1316 fun filtered_T_args false = T_args
1317 | filtered_T_args true = filter_type_args thy s'' arity T_args
1319 case type_arg_policy type_enc s'' of
1320 Explicit_Type_Args drop_args =>
1321 (name, filtered_T_args drop_args)
1322 | Mangled_Type_Args drop_args =>
1323 (mangled_const_name format type_enc (filtered_T_args drop_args)
1325 | No_Type_Args => (name, [])
1327 |> (fn (name, T_args) => CombConst (name, T, T_args))
1328 | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
1332 fun repair_combterm ctxt format type_enc sym_tab =
1333 not (is_type_enc_higher_order type_enc)
1334 ? (introduce_explicit_apps_in_combterm sym_tab
1335 #> introduce_predicators_in_combterm sym_tab)
1336 #> enforce_type_arg_policy_in_combterm ctxt format type_enc
1337 fun repair_fact ctxt format type_enc sym_tab =
1338 update_combformula (formula_map
1339 (repair_combterm ctxt format type_enc sym_tab))
1341 (** Helper facts **)
1343 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1345 [(("COMBI", false), @{thms Meson.COMBI_def}),
1346 (("COMBK", false), @{thms Meson.COMBK_def}),
1347 (("COMBB", false), @{thms Meson.COMBB_def}),
1348 (("COMBC", false), @{thms Meson.COMBC_def}),
1349 (("COMBS", false), @{thms Meson.COMBS_def}),
1350 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1351 (("fFalse", true), @{thms True_or_False}),
1352 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1353 (("fTrue", true), @{thms True_or_False}),
1355 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1356 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1358 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1359 by (unfold fconj_def) fast+}),
1361 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1362 by (unfold fdisj_def) fast+}),
1363 (("fimplies", false),
1364 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1365 by (unfold fimplies_def) fast+}),
1367 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1368 However, this is done so for backward compatibility: Including the
1369 equality helpers by default in Metis breaks a few existing proofs. *)
1370 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1371 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1372 (("fAll", false), []), (*TODO: add helpers*)
1373 (("fEx", false), []), (*TODO: add helpers*)
1374 (("If", true), @{thms if_True if_False True_or_False})]
1375 |> map (apsnd (map zero_var_indexes))
1377 val type_tag = `make_fixed_const type_tag_name
1379 fun type_tag_idempotence_fact () =
1381 fun var s = ATerm (`I s, [])
1382 fun tag tm = ATerm (type_tag, [var "T", tm])
1383 val tagged_a = tag (var "A")
1385 Formula (type_tag_idempotence_helper_name, Axiom,
1386 AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
1387 |> close_formula_universally, isabelle_info simpN, NONE)
1390 fun should_specialize_helper type_enc t =
1391 polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
1392 level_of_type_enc type_enc <> No_Types andalso
1393 not (null (Term.hidden_polymorphism t))
1395 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1396 case strip_prefix_and_unascii const_prefix s of
1399 val thy = Proof_Context.theory_of ctxt
1400 val unmangled_s = mangled_s |> unmangled_const_name
1401 fun dub needs_fairly_sound j k =
1402 (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1403 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1404 (if needs_fairly_sound then typed_helper_suffix
1405 else untyped_helper_suffix),
1407 fun dub_and_inst needs_fairly_sound (th, j) =
1408 let val t = prop_of th in
1409 if should_specialize_helper type_enc t then
1410 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1415 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1417 map_filter (make_fact ctxt format type_enc false false [])
1418 val fairly_sound = is_type_enc_fairly_sound type_enc
1421 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1422 if helper_s <> unmangled_s orelse
1423 (needs_fairly_sound andalso not fairly_sound) then
1426 ths ~~ (1 upto length ths)
1427 |> maps (dub_and_inst needs_fairly_sound)
1431 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1432 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1435 (***************************************************************)
1436 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1437 (***************************************************************)
1439 fun set_insert (x, s) = Symtab.update (x, ()) s
1441 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1443 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1444 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1446 fun classes_of_terms get_Ts =
1447 map (map snd o get_Ts)
1448 #> List.foldl add_classes Symtab.empty
1449 #> delete_type #> Symtab.keys
1451 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
1452 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
1454 fun fold_type_constrs f (Type (s, Ts)) x =
1455 fold (fold_type_constrs f) Ts (f (s, x))
1456 | fold_type_constrs _ _ x = x
1458 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1459 fun add_type_constrs_in_term thy =
1461 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1462 | add (t $ u) = add t #> add u
1463 | add (Const (x as (s, _))) =
1464 if String.isPrefix skolem_const_prefix s then I
1465 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1466 | add (Abs (_, _, u)) = add u
1470 fun type_constrs_of_terms thy ts =
1471 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1473 fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1476 val thy = Proof_Context.theory_of ctxt
1477 val fact_ts = facts |> map snd
1478 val presimp_consts = Meson.presimplified_consts ctxt
1479 val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
1480 val (facts, fact_names) =
1481 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1482 |> map_filter (try (apfst the))
1484 (* Remove existing facts from the conjecture, as this can dramatically
1485 boost an ATP's performance (for some reason). *)
1488 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1489 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1490 val all_ts = goal_t :: fact_ts
1491 val subs = tfree_classes_of_terms all_ts
1492 val supers = tvar_classes_of_terms all_ts
1493 val tycons = type_constrs_of_terms thy all_ts
1496 |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
1497 val (supers', arity_clauses) =
1498 if level_of_type_enc type_enc = No_Types then ([], [])
1499 else make_arity_clauses thy tycons supers
1500 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1502 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
1505 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
1506 (true, ATerm (class, [ATerm (name, [])]))
1507 | fo_literal_from_type_literal (TyLitFree (class, name)) =
1508 (true, ATerm (class, [ATerm (name, [])]))
1510 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1512 val type_pred = `make_fixed_const type_pred_name
1514 fun type_pred_combterm ctxt format type_enc T tm =
1515 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1516 |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
1518 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1519 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1520 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1521 | is_var_positively_naked_in_term _ _ _ _ = true
1522 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
1523 formula_fold pos (is_var_positively_naked_in_term name) phi false
1524 | should_predicate_on_var_in_formula _ _ _ _ = true
1526 fun mk_aterm format type_enc name T_args args =
1527 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1529 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
1530 CombConst (type_tag, T --> T, [T])
1531 |> enforce_type_arg_policy_in_combterm ctxt format type_enc
1532 |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1533 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1534 | _ => raise Fail "unexpected lambda-abstraction")
1535 and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
1539 val (head, args) = strip_combterm_comb u
1542 Top_Level pos => pos
1547 CombConst (name as (s, _), _, T_args) =>
1549 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1551 mk_aterm format type_enc name T_args (map (aux arg_site) args)
1553 | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1554 | CombAbs ((name, T), tm) =>
1555 AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
1556 | CombApp _ => raise Fail "impossible \"CombApp\""
1557 val T = combtyp_of u
1559 t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
1560 tag_with_type ctxt format nonmono_Ts type_enc pos T
1565 and formula_from_combformula ctxt format nonmono_Ts type_enc
1566 should_predicate_on_var =
1569 ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1572 Simple_Types (_, level) =>
1573 homogenized_type ctxt nonmono_Ts level 0
1574 #> ho_type_from_typ format type_enc false 0 #> SOME
1576 fun do_out_of_bound_type pos phi universal (name, T) =
1577 if should_predicate_on_type ctxt nonmono_Ts type_enc
1578 (fn () => should_predicate_on_var pos phi universal name) T then
1580 |> type_pred_combterm ctxt format type_enc T
1581 |> do_term pos |> AAtom |> SOME
1584 fun do_formula pos (AQuant (q, xs, phi)) =
1586 val phi = phi |> do_formula pos
1587 val universal = Option.map (q = AExists ? not) pos
1589 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1590 | SOME T => do_bound_type T)),
1591 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1593 (fn (_, NONE) => NONE
1595 do_out_of_bound_type pos phi universal (s, T))
1599 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1600 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1603 fun bound_tvars type_enc Ts =
1604 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1605 (type_literals_for_types type_enc add_sorts_on_tvar Ts))
1607 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1608 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1609 the remote provers might care. *)
1610 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
1611 type_enc (j, {name, locality, kind, combformula, atomic_types}) =
1612 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
1615 |> close_combformula_universally
1616 |> formula_from_combformula ctxt format nonmono_Ts type_enc
1617 should_predicate_on_var_in_formula
1618 (if pos then SOME true else NONE)
1619 |> bound_tvars type_enc atomic_types
1620 |> close_formula_universally,
1623 Intro => isabelle_info introN
1624 | Elim => isabelle_info elimN
1625 | Simp => isabelle_info simpN
1629 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1630 : class_rel_clause) =
1631 let val ty_arg = ATerm (`I "T", []) in
1632 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1633 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
1634 AAtom (ATerm (superclass, [ty_arg]))])
1635 |> close_formula_universally, isabelle_info introN, NONE)
1638 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
1639 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
1640 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
1641 (false, ATerm (c, [ATerm (sort, [])]))
1643 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1645 Formula (arity_clause_prefix ^ name, Axiom,
1646 mk_ahorn (map (formula_from_fo_literal o apfst not
1647 o fo_literal_from_arity_literal) prem_lits)
1648 (formula_from_fo_literal
1649 (fo_literal_from_arity_literal concl_lits))
1650 |> close_formula_universally, isabelle_info introN, NONE)
1652 fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
1653 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1654 Formula (conjecture_prefix ^ name, kind,
1655 formula_from_combformula ctxt format nonmono_Ts type_enc
1656 should_predicate_on_var_in_formula (SOME false)
1657 (close_combformula_universally combformula)
1658 |> bound_tvars type_enc atomic_types
1659 |> close_formula_universally, NONE, NONE)
1661 fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
1662 atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
1663 |> map fo_literal_from_type_literal
1665 fun formula_line_for_free_type j lit =
1666 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1667 formula_from_fo_literal lit, NONE, NONE)
1668 fun formula_lines_for_free_types type_enc facts =
1670 val litss = map (free_type_literals type_enc) facts
1671 val lits = fold (union (op =)) litss []
1672 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1674 (** Symbol declarations **)
1676 fun should_declare_sym type_enc pred_sym s =
1677 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1679 Simple_Types _ => true
1680 | Tags (_, _, Lightweight) => true
1681 | _ => not pred_sym)
1683 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
1685 fun add_combterm in_conj tm =
1686 let val (head, args) = strip_combterm_comb tm in
1688 CombConst ((s, s'), T, T_args) =>
1689 let val pred_sym = is_pred_sym repaired_sym_tab s in
1690 if should_declare_sym type_enc pred_sym s then
1691 Symtab.map_default (s, [])
1692 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1697 | CombAbs (_, tm) => add_combterm in_conj tm
1699 #> fold (add_combterm in_conj) args
1701 fun add_fact in_conj =
1702 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1705 |> is_type_enc_fairly_sound type_enc
1706 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1709 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1710 out with monotonicity" paper presented at CADE 2011. *)
1711 fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
1712 | add_combterm_nonmonotonic_types ctxt level sound locality _
1713 (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1715 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1717 Noninf_Nonmono_Types =>
1718 not (is_locality_global locality) orelse
1719 not (is_type_surely_infinite ctxt sound T)
1720 | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
1721 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1722 | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
1723 fun add_fact_nonmonotonic_types ctxt level sound
1724 ({kind, locality, combformula, ...} : translated_formula) =
1725 formula_fold (SOME (kind <> Conjecture))
1726 (add_combterm_nonmonotonic_types ctxt level sound locality)
1728 fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
1729 let val level = level_of_type_enc type_enc in
1730 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1731 [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
1732 (* We must add "bool" in case the helper "True_or_False" is added
1733 later. In addition, several places in the code rely on the list of
1734 nonmonotonic types not being empty. *)
1735 |> insert_type ctxt I @{typ bool}
1740 fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
1741 (s', T_args, T, pred_sym, ary, _) =
1743 val (T_arg_Ts, level) =
1745 Simple_Types (_, level) => ([], level)
1746 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1748 Decl (sym_decl_prefix ^ s, (s, s'),
1749 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1750 |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
1753 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1754 poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
1756 val (kind, maybe_negate) =
1757 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1759 val (arg_Ts, res_T) = chop_fun ary T
1760 val num_args = length arg_Ts
1762 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1764 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1765 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1766 fun should_keep_arg_type T =
1767 sym_needs_arg_types orelse
1768 not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
1770 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1772 Formula (preds_sym_formula_prefix ^ s ^
1773 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1774 CombConst ((s, s'), T, T_args)
1775 |> fold (curry (CombApp o swap)) bounds
1776 |> type_pred_combterm ctxt format type_enc res_T
1777 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1778 |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
1779 (K (K (K (K true)))) (SOME true)
1780 |> n > 1 ? bound_tvars type_enc (atyps_of T)
1781 |> close_formula_universally
1783 isabelle_info introN, NONE)
1786 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1787 poly_nonmono_Ts type_enc n s
1788 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1791 lightweight_tags_sym_formula_prefix ^ s ^
1792 (if n > 1 then "_" ^ string_of_int j else "")
1793 val (kind, maybe_negate) =
1794 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1796 val (arg_Ts, res_T) = chop_fun ary T
1798 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1799 val bounds = bound_names |> map (fn name => ATerm (name, []))
1800 val cst = mk_aterm format type_enc (s, s') T_args
1801 val atomic_Ts = atyps_of T
1803 (if pred_sym then AConn (AIff, map AAtom tms)
1804 else AAtom (ATerm (`I tptp_equal, tms)))
1805 |> bound_tvars type_enc atomic_Ts
1806 |> close_formula_universally
1808 (* See also "should_tag_with_type". *)
1809 fun should_encode T =
1810 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1812 Tags (Polymorphic, level, Lightweight) =>
1813 level <> All_Types andalso Monomorph.typ_has_tvars T
1815 val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
1816 val add_formula_for_res =
1817 if should_encode res_T then
1818 cons (Formula (ident_base ^ "_res", kind,
1819 eq [tag_with res_T (cst bounds), cst bounds],
1820 isabelle_info simpN, NONE))
1823 fun add_formula_for_arg k =
1824 let val arg_T = nth arg_Ts k in
1825 if should_encode arg_T then
1826 case chop k bounds of
1827 (bounds1, bound :: bounds2) =>
1828 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
1829 eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
1831 isabelle_info simpN, NONE))
1832 | _ => raise Fail "expected nonempty tail"
1837 [] |> not pred_sym ? add_formula_for_res
1838 |> fold add_formula_for_arg (ary - 1 downto 0)
1841 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1843 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1844 poly_nonmono_Ts type_enc (s, decls) =
1847 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
1852 decl :: (decls' as _ :: _) =>
1853 let val T = result_type_of_decl decl in
1854 if forall (curry (type_instance ctxt o swap) T
1855 o result_type_of_decl) decls' then
1861 val n = length decls
1863 decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
1865 o result_type_of_decl)
1867 (0 upto length decls - 1, decls)
1868 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1869 nonmono_Ts poly_nonmono_Ts type_enc n s)
1871 | Tags (_, _, heaviness) =>
1875 let val n = length decls in
1876 (0 upto n - 1 ~~ decls)
1877 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1878 conj_sym_kind poly_nonmono_Ts type_enc n s)
1881 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1882 poly_nonmono_Ts type_enc sym_decl_tab =
1887 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1888 nonmono_Ts poly_nonmono_Ts type_enc)
1890 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1891 poly <> Mangled_Monomorphic andalso
1892 ((level = All_Types andalso heaviness = Lightweight) orelse
1893 level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
1894 | needs_type_tag_idempotence _ = false
1896 fun offset_of_heading_in_problem _ [] j = j
1897 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1898 if heading = needle then j
1899 else offset_of_heading_in_problem needle problem (j + length lines)
1901 val implicit_declsN = "Should-be-implicit typings"
1902 val explicit_declsN = "Explicit typings"
1903 val factsN = "Relevant facts"
1904 val class_relsN = "Class relationships"
1905 val aritiesN = "Arities"
1906 val helpersN = "Helper facts"
1907 val conjsN = "Conjectures"
1908 val free_typesN = "Type variables"
1910 val explicit_apply = NONE (* for experimental purposes *)
1912 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
1913 exporter readable_names preproc hyp_ts concl_t facts =
1915 val (format, type_enc) = choose_format [format] type_enc
1916 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1917 translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1919 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1921 conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
1922 val repair = repair_fact ctxt format type_enc sym_tab
1923 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1924 val repaired_sym_tab =
1925 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1927 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
1929 val poly_nonmono_Ts =
1930 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1931 polymorphism_of_type_enc type_enc <> Polymorphic then
1934 [TVar (("'a", 0), HOLogic.typeS)]
1935 val sym_decl_lines =
1936 (conjs, helpers @ facts)
1937 |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
1938 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1939 poly_nonmono_Ts type_enc
1941 0 upto length helpers - 1 ~~ helpers
1942 |> map (formula_line_for_fact ctxt format helper_prefix I false true
1943 poly_nonmono_Ts type_enc)
1944 |> (if needs_type_tag_idempotence type_enc then
1945 cons (type_tag_idempotence_fact ())
1948 (* Reordering these might confuse the proof reconstruction code or the SPASS
1951 [(explicit_declsN, sym_decl_lines),
1953 map (formula_line_for_fact ctxt format fact_prefix ascii_of
1954 (not exporter) (not exporter) nonmono_Ts
1956 (0 upto length facts - 1 ~~ facts)),
1957 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1958 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1959 (helpersN, helper_lines),
1961 map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
1963 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
1967 CNF => ensure_cnf_problem
1968 | CNF_UEQ => filter_cnf_ueq_problem
1970 |> (if is_format_typed format then
1971 declare_undeclared_syms_in_atp_problem type_decl_prefix
1975 val (problem, pool) = problem |> nice_atp_problem readable_names
1976 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
1978 map_filter (fn (j, {name, ...}) =>
1979 if String.isSuffix typed_helper_suffix name then SOME j
1981 ((helpers_offset + 1 upto helpers_offset + length helpers)
1983 fun add_sym_arity (s, {min_ary, ...} : sym_info) =
1985 case strip_prefix_and_unascii const_prefix s of
1986 SOME s => Symtab.insert (op =) (s, min_ary)
1992 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1993 offset_of_heading_in_problem conjsN problem 0,
1994 offset_of_heading_in_problem factsN problem 0,
1995 fact_names |> Vector.fromList,
1997 Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
2001 val conj_weight = 0.0
2002 val hyp_weight = 0.1
2003 val fact_min_weight = 0.2
2004 val fact_max_weight = 1.0
2005 val type_info_default_weight = 0.8
2007 fun add_term_weights weight (ATerm (s, tms)) =
2008 is_tptp_user_symbol s ? Symtab.default (s, weight)
2009 #> fold (add_term_weights weight) tms
2010 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2011 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2012 formula_fold NONE (K (add_term_weights weight)) phi
2013 | add_problem_line_weights _ _ = I
2015 fun add_conjectures_weights [] = I
2016 | add_conjectures_weights conjs =
2017 let val (hyps, conj) = split_last conjs in
2018 add_problem_line_weights conj_weight conj
2019 #> fold (add_problem_line_weights hyp_weight) hyps
2022 fun add_facts_weights facts =
2024 val num_facts = length facts
2026 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2027 / Real.fromInt num_facts
2029 map weight_of (0 upto num_facts - 1) ~~ facts
2030 |> fold (uncurry add_problem_line_weights)
2033 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2034 fun atp_problem_weights problem =
2035 let val get = these o AList.lookup (op =) problem in
2037 |> add_conjectures_weights (get free_typesN @ get conjsN)
2038 |> add_facts_weights (get factsN)
2039 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2040 [explicit_declsN, class_relsN, aritiesN]
2042 |> sort (prod_ord Real.compare string_ord o pairself swap)