generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
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 Metis and 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 ascii_of : string -> string
67 val unascii_of : string -> string
68 val strip_prefix_and_unascii : string -> string -> string option
69 val proxy_table : (string * (string * (thm * (string * string)))) list
70 val proxify_const : string -> (string * string) option
71 val invert_const : string -> string
72 val unproxify_const : string -> string
73 val new_skolem_var_name_from_const : string -> string
74 val num_type_args : theory -> string -> int
75 val atp_irrelevant_consts : string list
76 val atp_schematic_consts_of : term -> typ list Symtab.table
77 val is_locality_global : locality -> bool
78 val type_enc_from_string : string -> type_enc
79 val is_type_enc_higher_order : type_enc -> bool
80 val polymorphism_of_type_enc : type_enc -> polymorphism
81 val level_of_type_enc : type_enc -> type_level
82 val is_type_enc_virtually_sound : type_enc -> bool
83 val is_type_enc_fairly_sound : type_enc -> bool
84 val choose_format : format list -> type_enc -> format * type_enc
86 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
87 val unmangled_const : string -> string * (string, 'b) ho_term list
88 val unmangled_const_name : string -> string
89 val helper_table : ((string * bool) * thm list) list
91 val conceal_lambdas : Proof.context -> term -> term
92 val introduce_combinators : Proof.context -> term -> term
93 val prepare_atp_problem :
94 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
95 -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
96 -> term -> ((string * locality) * term) list
97 -> string problem * string Symtab.table * int * int
98 * (string * locality) list vector * int list * int Symtab.table
99 val atp_problem_weights : string problem -> (string * real) list
102 structure ATP_Translate : ATP_TRANSLATE =
108 type name = string * string
110 val generate_info = false (* experimental *)
112 fun isabelle_info s =
113 if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
120 val bound_var_prefix = "B_"
121 val schematic_var_prefix = "V_"
122 val fixed_var_prefix = "v_"
123 val tvar_prefix = "T_"
124 val tfree_prefix = "t_"
125 val const_prefix = "c_"
126 val type_const_prefix = "tc_"
127 val class_prefix = "cl_"
129 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
130 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
131 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
133 val type_decl_prefix = "ty_"
134 val sym_decl_prefix = "sy_"
135 val preds_sym_formula_prefix = "psy_"
136 val lightweight_tags_sym_formula_prefix = "tsy_"
137 val fact_prefix = "fact_"
138 val conjecture_prefix = "conj_"
139 val helper_prefix = "help_"
140 val class_rel_clause_prefix = "clar_"
141 val arity_clause_prefix = "arity_"
142 val tfree_clause_prefix = "tfree_"
144 val lambda_fact_prefix = "ATP.lambda_"
145 val typed_helper_suffix = "_T"
146 val untyped_helper_suffix = "_U"
147 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
149 val predicator_name = "hBOOL"
150 val app_op_name = "hAPP"
151 val type_tag_name = "ti"
152 val type_pred_name = "is"
153 val simple_type_prefix = "ty_"
155 val prefixed_predicator_name = const_prefix ^ predicator_name
156 val prefixed_app_op_name = const_prefix ^ app_op_name
157 val prefixed_type_tag_name = const_prefix ^ type_tag_name
159 (* Freshness almost guaranteed! *)
160 val atp_weak_prefix = "ATP:"
162 val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
164 (*Escaping of special characters.
165 Alphanumeric characters are left unchanged.
166 The character _ goes to __
167 Characters in the range ASCII space to / go to _A to _P, respectively.
168 Other characters go to _nnn where nnn is the decimal ASCII code.*)
169 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
171 fun stringN_of_int 0 _ = ""
172 | stringN_of_int k n =
173 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
175 fun ascii_of_char c =
176 if Char.isAlphaNum c then
178 else if c = #"_" then
180 else if #" " <= c andalso c <= #"/" then
181 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
183 (* fixed width, in case more digits follow *)
184 "_" ^ stringN_of_int 3 (Char.ord c)
186 val ascii_of = String.translate ascii_of_char
188 (** Remove ASCII armoring from names in proof files **)
190 (* We don't raise error exceptions because this code can run inside a worker
191 thread. Also, the errors are impossible. *)
194 fun un rcs [] = String.implode(rev rcs)
195 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
196 (* Three types of _ escapes: __, _A to _P, _nnn *)
197 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
198 | un rcs (#"_" :: c :: cs) =
199 if #"A" <= c andalso c<= #"P" then
200 (* translation of #" " to #"/" *)
201 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
203 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
204 case Int.fromString (String.implode digits) of
205 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
206 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
208 | un rcs (c :: cs) = un (c :: rcs) cs
209 in un [] o String.explode end
211 (* If string s has the prefix s1, return the result of deleting it,
213 fun strip_prefix_and_unascii s1 s =
214 if String.isPrefix s1 s then
215 SOME (unascii_of (String.extract (s, size s1, NONE)))
220 [("c_False", (@{const_name False}, (@{thm fFalse_def},
221 ("fFalse", @{const_name ATP.fFalse})))),
222 ("c_True", (@{const_name True}, (@{thm fTrue_def},
223 ("fTrue", @{const_name ATP.fTrue})))),
224 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
225 ("fNot", @{const_name ATP.fNot})))),
226 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
227 ("fconj", @{const_name ATP.fconj})))),
228 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
229 ("fdisj", @{const_name ATP.fdisj})))),
230 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
231 ("fimplies", @{const_name ATP.fimplies})))),
232 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
233 ("fequal", @{const_name ATP.fequal})))),
234 ("c_All", (@{const_name All}, (@{thm fAll_def},
235 ("fAll", @{const_name ATP.fAll})))),
236 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
237 ("fEx", @{const_name ATP.fEx}))))]
239 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
241 (* Readable names for the more common symbolic functions. Do not mess with the
242 table unless you know what you are doing. *)
243 val const_trans_table =
244 [(@{type_name Product_Type.prod}, "prod"),
245 (@{type_name Sum_Type.sum}, "sum"),
246 (@{const_name False}, "False"),
247 (@{const_name True}, "True"),
248 (@{const_name Not}, "Not"),
249 (@{const_name conj}, "conj"),
250 (@{const_name disj}, "disj"),
251 (@{const_name implies}, "implies"),
252 (@{const_name HOL.eq}, "equal"),
253 (@{const_name All}, "All"),
254 (@{const_name Ex}, "Ex"),
255 (@{const_name If}, "If"),
256 (@{const_name Set.member}, "member"),
257 (@{const_name Meson.COMBI}, "COMBI"),
258 (@{const_name Meson.COMBK}, "COMBK"),
259 (@{const_name Meson.COMBB}, "COMBB"),
260 (@{const_name Meson.COMBC}, "COMBC"),
261 (@{const_name Meson.COMBS}, "COMBS")]
263 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
265 (* Invert the table of translations between Isabelle and ATPs. *)
266 val const_trans_table_inv =
267 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
268 val const_trans_table_unprox =
270 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
272 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
273 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
276 case Symtab.lookup const_trans_table c of
280 fun ascii_of_indexname (v, 0) = ascii_of v
281 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
283 fun make_bound_var x = bound_var_prefix ^ ascii_of x
284 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
285 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
287 fun make_schematic_type_var (x, i) =
288 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
289 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
291 (* "HOL.eq" is mapped to the ATP's equality. *)
292 fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
293 | make_fixed_const c = const_prefix ^ lookup_const c
295 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
297 fun make_type_class clas = class_prefix ^ ascii_of clas
299 fun new_skolem_var_name_from_const s =
300 let val ss = s |> space_explode Long_Name.separator in
301 nth ss (length ss - 2)
304 (* The number of type arguments of a constant, zero if it's monomorphic. For
305 (instances of) Skolem pseudoconstants, this information is encoded in the
307 fun num_type_args thy s =
308 if String.isPrefix skolem_const_prefix s then
309 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
311 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
313 (* These are either simplified away by "Meson.presimplify" (most of the time) or
314 handled specially via "fFalse", "fTrue", ..., "fequal". *)
315 val atp_irrelevant_consts =
316 [@{const_name False}, @{const_name True}, @{const_name Not},
317 @{const_name conj}, @{const_name disj}, @{const_name implies},
318 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
320 val atp_monomorph_bad_consts =
321 atp_irrelevant_consts @
322 (* These are ignored anyway by the relevance filter (unless they appear in
323 higher-order places) but not by the monomorphizer. *)
324 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
325 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
326 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
328 fun add_schematic_const (x as (_, T)) =
329 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
330 val add_schematic_consts_of =
331 Term.fold_aterms (fn Const (x as (s, _)) =>
332 not (member (op =) atp_monomorph_bad_consts s)
333 ? add_schematic_const x
335 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
337 (** Definitions and functions for FOL clauses and formulas for TPTP **)
339 (* The first component is the type class; the second is a "TVar" or "TFree". *)
340 datatype type_literal =
341 TyLitVar of name * name |
342 TyLitFree of name * name
345 (** Isabelle arities **)
347 datatype arity_literal =
348 TConsLit of name * name * name list |
349 TVarLit of name * name
352 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
354 val type_class = the_single @{sort type}
356 fun add_packed_sort tvar =
357 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
361 prem_lits : arity_literal list,
362 concl_lits : arity_literal}
364 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
365 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
367 val tvars = gen_TVars (length args)
368 val tvars_srts = ListPair.zip (tvars, args)
371 prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
372 concl_lits = TConsLit (`make_type_class cls,
373 `make_fixed_type_const tcons,
377 fun arity_clause _ _ (_, []) = []
378 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
379 arity_clause seen n (tcons, ars)
380 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
381 if member (op =) seen class then
382 (* multiple arities for the same (tycon, class) pair *)
383 make_axiom_arity_clause (tcons,
384 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
386 arity_clause seen (n + 1) (tcons, ars)
388 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
389 ascii_of class, ar) ::
390 arity_clause (class :: seen) n (tcons, ars)
392 fun multi_arity_clause [] = []
393 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
394 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
396 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
397 theory thy provided its arguments have the corresponding sorts. *)
398 fun type_class_pairs thy tycons classes =
400 val alg = Sign.classes_of thy
401 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
402 fun add_class tycon class =
403 cons (class, domain_sorts tycon class)
404 handle Sorts.CLASS_ERROR _ => I
405 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
406 in map try_classes tycons end
408 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
409 fun iter_type_class_pairs _ _ [] = ([], [])
410 | iter_type_class_pairs thy tycons classes =
412 fun maybe_insert_class s =
413 (s <> type_class andalso not (member (op =) classes s))
415 val cpairs = type_class_pairs thy tycons classes
417 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
418 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
419 in (classes' @ classes, union (op =) cpairs' cpairs) end
421 fun make_arity_clauses thy tycons =
422 iter_type_class_pairs thy tycons ##> multi_arity_clause
425 (** Isabelle class relations **)
427 type class_rel_clause =
432 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
434 fun class_pairs _ [] _ = []
435 | class_pairs thy subs supers =
437 val class_less = Sorts.class_less (Sign.classes_of thy)
438 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
439 fun add_supers sub = fold (add_super sub) supers
440 in fold add_supers subs [] end
442 fun make_class_rel_clause (sub, super) =
443 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
444 superclass = `make_type_class super}
446 fun make_class_rel_clauses thy subs supers =
447 map make_class_rel_clause (class_pairs thy subs supers)
449 (* intermediate terms *)
451 IConst of name * typ * typ list |
453 IApp of iterm * iterm |
454 IAbs of (name * typ) * iterm
456 fun ityp_of (IConst (_, T, _)) = T
457 | ityp_of (IVar (_, T)) = T
458 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
459 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
461 (*gets the head of a combinator application, along with the list of arguments*)
462 fun strip_iterm_comb u =
464 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
466 in stripc (u, []) end
468 fun atyps_of T = fold_atyps (insert (op =)) T []
470 fun new_skolem_const_name s num_T_args =
471 [new_skolem_const_prefix, s, string_of_int num_T_args]
472 |> space_implode Long_Name.separator
474 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
475 Also accumulates sort infomation. *)
476 fun iterm_from_term thy bs (P $ Q) =
478 val (P', P_atomics_Ts) = iterm_from_term thy bs P
479 val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
480 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
481 | iterm_from_term thy _ (Const (c, T)) =
484 (if String.isPrefix old_skolem_const_prefix c then
485 [] |> Term.add_tvarsT T |> map TVar
487 (c, T) |> Sign.const_typargs thy)
488 val c' = IConst (`make_fixed_const c, T, tvar_list)
489 in (c', atyps_of T) end
490 | iterm_from_term _ _ (Free (v, T)) =
491 (IConst (`make_fixed_var v, T, []), atyps_of T)
492 | iterm_from_term _ _ (Var (v as (s, _), T)) =
493 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
495 val Ts = T |> strip_type |> swap |> op ::
496 val s' = new_skolem_const_name s (length Ts)
497 in IConst (`make_fixed_const s', T, Ts) end
499 IVar ((make_schematic_var v, s), T), atyps_of T)
500 | iterm_from_term _ bs (Bound j) =
501 nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
502 | iterm_from_term thy bs (Abs (s, T, t)) =
504 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
506 val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
508 (IAbs ((`make_bound_var s, T), tm),
509 union (op =) atomic_Ts (atyps_of T))
513 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
516 (* (quasi-)underapproximation of the truth *)
517 fun is_locality_global Local = false
518 | is_locality_global Assum = false
519 | is_locality_global Chained = false
520 | is_locality_global _ = true
522 datatype order = First_Order | Higher_Order
523 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
524 datatype type_level =
525 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
527 datatype type_heaviness = Heavyweight | Lightweight
530 Simple_Types of order * type_level |
531 Preds of polymorphism * type_level * type_heaviness |
532 Tags of polymorphism * type_level * type_heaviness
534 fun try_unsuffixes ss s =
535 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
537 fun type_enc_from_string s =
538 (case try (unprefix "poly_") s of
539 SOME s => (SOME Polymorphic, s)
541 case try (unprefix "mono_") s of
542 SOME s => (SOME Monomorphic, s)
544 case try (unprefix "mangled_") s of
545 SOME s => (SOME Mangled_Monomorphic, s)
548 (* "_query" and "_bang" are for the ASCII-challenged Metis and
550 case try_unsuffixes ["?", "_query"] s of
551 SOME s => (Noninf_Nonmono_Types, s)
553 case try_unsuffixes ["!", "_bang"] s of
554 SOME s => (Fin_Nonmono_Types, s)
555 | NONE => (All_Types, s))
557 case try (unsuffix "_heavy") s of
558 SOME s => (Heavyweight, s)
559 | NONE => (Lightweight, s))
560 |> (fn (poly, (level, (heaviness, core))) =>
561 case (core, (poly, level, heaviness)) of
562 ("simple", (NONE, _, Lightweight)) =>
563 Simple_Types (First_Order, level)
564 | ("simple_higher", (NONE, _, Lightweight)) =>
565 if level = Noninf_Nonmono_Types then raise Same.SAME
566 else Simple_Types (Higher_Order, level)
567 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
568 | ("tags", (SOME Polymorphic, _, _)) =>
569 Tags (Polymorphic, level, heaviness)
570 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
571 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
572 Preds (poly, Const_Arg_Types, Lightweight)
573 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
574 Preds (Polymorphic, No_Types, Lightweight)
575 | _ => raise Same.SAME)
576 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
578 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
579 | is_type_enc_higher_order _ = false
581 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
582 | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
583 | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
585 fun level_of_type_enc (Simple_Types (_, level)) = level
586 | level_of_type_enc (Preds (_, level, _)) = level
587 | level_of_type_enc (Tags (_, level, _)) = level
589 fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
590 | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
591 | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
593 fun is_type_level_virtually_sound level =
594 level = All_Types orelse level = Noninf_Nonmono_Types
595 val is_type_enc_virtually_sound =
596 is_type_level_virtually_sound o level_of_type_enc
598 fun is_type_level_fairly_sound level =
599 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
600 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
602 fun choose_format formats (Simple_Types (order, level)) =
603 if member (op =) formats THF then
604 (THF, Simple_Types (order, level))
605 else if member (op =) formats TFF then
606 (TFF, Simple_Types (First_Order, level))
608 choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
609 | choose_format formats type_enc =
612 (CNF_UEQ, case type_enc of
614 (if is_type_enc_fairly_sound type_enc then Tags else Preds)
617 | format => (format, type_enc))
619 type translated_formula =
623 iformula : (name, typ, iterm) formula,
624 atomic_types : typ list}
626 fun update_iformula f ({name, locality, kind, iformula, atomic_types}
627 : translated_formula) =
628 {name = name, locality = locality, kind = kind, iformula = f iformula,
629 atomic_types = atomic_types} : translated_formula
631 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
633 val type_instance = Sign.typ_instance o Proof_Context.theory_of
635 fun insert_type ctxt get_T x xs =
636 let val T = get_T x in
637 if exists (curry (type_instance ctxt) T o get_T) xs then xs
638 else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
641 (* The Booleans indicate whether all type arguments should be kept. *)
642 datatype type_arg_policy =
643 Explicit_Type_Args of bool |
644 Mangled_Type_Args of bool |
647 fun should_drop_arg_type_args (Simple_Types _) =
648 false (* since TFF doesn't support overloading *)
649 | should_drop_arg_type_args type_enc =
650 level_of_type_enc type_enc = All_Types andalso
651 heaviness_of_type_enc type_enc = Heavyweight
653 fun type_arg_policy type_enc s =
654 if s = type_tag_name then
655 (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
658 Explicit_Type_Args) false
659 else case type_enc of
660 Tags (_, All_Types, Heavyweight) => No_Type_Args
662 if level_of_type_enc type_enc = No_Types orelse
663 s = @{const_name HOL.eq} orelse
664 (s = app_op_name andalso
665 level_of_type_enc type_enc = Const_Arg_Types) then
668 should_drop_arg_type_args type_enc
669 |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
674 (* Make literals for sorted type variables. *)
675 fun generic_add_sorts_on_type (_, []) = I
676 | generic_add_sorts_on_type ((x, i), s :: ss) =
677 generic_add_sorts_on_type ((x, i), ss)
678 #> (if s = the_single @{sort HOL.type} then
681 insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
683 insert (op =) (TyLitVar (`make_type_class s,
684 (make_schematic_type_var (x, i), x))))
685 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
686 | add_sorts_on_tfree _ = I
687 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
688 | add_sorts_on_tvar _ = I
690 fun type_literals_for_types type_enc add_sorts_on_typ Ts =
691 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
693 fun mk_aconns c phis =
694 let val (phis', phi') = split_last phis in
695 fold_rev (mk_aconn c) phis' phi'
697 fun mk_ahorn [] phi = phi
698 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
699 fun mk_aquant _ [] phi = phi
700 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
701 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
702 | mk_aquant q xs phi = AQuant (q, xs, phi)
704 fun close_universally atom_vars phi =
706 fun formula_vars bounds (AQuant (_, xs, phi)) =
707 formula_vars (map fst xs @ bounds) phi
708 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
709 | formula_vars bounds (AAtom tm) =
710 union (op =) (atom_vars tm []
711 |> filter_out (member (op =) bounds o fst))
712 in mk_aquant AForall (formula_vars [] phi []) phi end
714 fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
715 | iterm_vars (IConst _) = I
716 | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
717 | iterm_vars (IAbs (_, tm)) = iterm_vars tm
718 fun close_iformula_universally phi = close_universally iterm_vars phi
720 fun term_vars bounds (ATerm (name as (s, _), tms)) =
721 (is_tptp_variable s andalso not (member (op =) bounds name))
722 ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
723 | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
724 fun close_formula_universally phi = close_universally (term_vars []) phi
726 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
727 val homo_infinite_type = Type (homo_infinite_type_name, [])
729 fun ho_term_from_typ format type_enc =
731 fun term (Type (s, Ts)) =
732 ATerm (case (is_type_enc_higher_order type_enc, s) of
733 (true, @{type_name bool}) => `I tptp_bool_type
734 | (true, @{type_name fun}) => `I tptp_fun_type
735 | _ => if s = homo_infinite_type_name andalso
736 (format = TFF orelse format = THF) then
737 `I tptp_individual_type
739 `make_fixed_type_const s,
741 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
742 | term (TVar ((x as (s, _)), _)) =
743 ATerm ((make_schematic_type_var x, s), [])
746 fun ho_term_for_type_arg format type_enc T =
747 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
749 (* This shouldn't clash with anything else. *)
750 val mangled_type_sep = "\000"
752 fun generic_mangled_type_name f (ATerm (name, [])) = f name
753 | generic_mangled_type_name f (ATerm (name, tys)) =
754 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
756 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
758 val bool_atype = AType (`I tptp_bool_type)
760 fun make_simple_type s =
761 if s = tptp_bool_type orelse s = tptp_fun_type orelse
762 s = tptp_individual_type then
765 simple_type_prefix ^ ascii_of s
767 fun ho_type_from_ho_term type_enc pred_sym ary =
770 AType ((make_simple_type (generic_mangled_type_name fst ty),
771 generic_mangled_type_name snd ty))
772 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
773 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
774 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
775 | to_fo _ _ = raise Fail "unexpected type abstraction"
776 fun to_ho (ty as ATerm ((s, _), tys)) =
777 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
778 | to_ho _ = raise Fail "unexpected type abstraction"
779 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
781 fun ho_type_from_typ format type_enc pred_sym ary =
782 ho_type_from_ho_term type_enc pred_sym ary
783 o ho_term_from_typ format type_enc
785 fun mangled_const_name format type_enc T_args (s, s') =
787 val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
788 fun type_suffix f g =
789 fold_rev (curry (op ^) o g o prefix mangled_type_sep
790 o generic_mangled_type_name f) ty_args ""
791 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
793 val parse_mangled_ident =
794 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
796 fun parse_mangled_type x =
798 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
800 and parse_mangled_types x =
801 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
803 fun unmangled_type s =
804 s |> suffix ")" |> raw_explode
805 |> Scan.finite Symbol.stopper
806 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
807 quote s)) parse_mangled_type))
810 val unmangled_const_name = space_explode mangled_type_sep #> hd
811 fun unmangled_const s =
812 let val ss = space_explode mangled_type_sep s in
813 (hd ss, map unmangled_type (tl ss))
816 fun introduce_proxies type_enc =
818 fun intro top_level (IApp (tm1, tm2)) =
819 IApp (intro top_level tm1, intro false tm2)
820 | intro top_level (IConst (name as (s, _), T, T_args)) =
821 (case proxify_const s of
823 if top_level orelse is_type_enc_higher_order type_enc then
824 case (top_level, s) of
825 (_, "c_False") => (`I tptp_false, [])
826 | (_, "c_True") => (`I tptp_true, [])
827 | (false, "c_Not") => (`I tptp_not, [])
828 | (false, "c_conj") => (`I tptp_and, [])
829 | (false, "c_disj") => (`I tptp_or, [])
830 | (false, "c_implies") => (`I tptp_implies, [])
831 | (false, "c_All") => (`I tptp_ho_forall, [])
832 | (false, "c_Ex") => (`I tptp_ho_exists, [])
834 if is_tptp_equal s then (`I tptp_equal, [])
835 else (proxy_base |>> prefix const_prefix, T_args)
838 (proxy_base |>> prefix const_prefix, T_args)
839 | NONE => (name, T_args))
840 |> (fn (name, T_args) => IConst (name, T, T_args))
841 | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm)
845 fun iformula_from_prop thy type_enc eq_as_iff =
847 fun do_term bs t atomic_types =
848 iterm_from_term thy bs (Envir.eta_contract t)
849 |>> (introduce_proxies type_enc #> AAtom)
850 ||> union (op =) atomic_types
851 fun do_quant bs q s T t' =
852 let val s = singleton (Name.variant_list (map fst bs)) s in
853 do_formula ((s, T) :: bs) t'
854 #>> mk_aquant q [(`make_bound_var s, SOME T)]
856 and do_conn bs c t1 t2 =
857 do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
858 and do_formula bs t =
860 @{const Trueprop} $ t1 => do_formula bs t1
861 | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
862 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
863 do_quant bs AForall s T t'
864 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
865 do_quant bs AExists s T t'
866 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
867 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
868 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
869 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
870 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
874 fun presimplify_term _ [] t = t
875 | presimplify_term ctxt presimp_consts t =
876 t |> exists_Const (member (op =) presimp_consts o fst) t
877 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
878 #> Meson.presimplify ctxt
881 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
882 fun conceal_bounds Ts t =
883 subst_bounds (map (Free o apfst concealed_bound_name)
884 (0 upto length Ts - 1 ~~ Ts), t)
885 fun reveal_bounds Ts =
886 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
887 (0 upto length Ts - 1 ~~ Ts))
889 fun is_fun_equality (@{const_name HOL.eq},
890 Type (_, [Type (@{type_name fun}, _), _])) = true
891 | is_fun_equality _ = false
893 fun extensionalize_term ctxt t =
894 if exists_Const is_fun_equality t then
895 let val thy = Proof_Context.theory_of ctxt in
896 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
897 |> prop_of |> Logic.dest_equals |> snd
902 fun simple_translate_lambdas do_lambdas ctxt t =
903 let val thy = Proof_Context.theory_of ctxt in
904 if Meson.is_fol_term thy t then
910 @{const Not} $ t1 => @{const Not} $ aux Ts t1
911 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
912 t0 $ Abs (s, T, aux (T :: Ts) t')
913 | (t0 as Const (@{const_name All}, _)) $ t1 =>
914 aux Ts (t0 $ eta_expand Ts t1 1)
915 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
916 t0 $ Abs (s, T, aux (T :: Ts) t')
917 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
918 aux Ts (t0 $ eta_expand Ts t1 1)
919 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
920 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
921 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
922 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
924 t0 $ aux Ts t1 $ aux Ts t2
926 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
927 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
928 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
929 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
932 fun do_conceal_lambdas Ts (t1 $ t2) =
933 do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
934 | do_conceal_lambdas Ts (Abs (_, T, t)) =
935 (* slightly unsound because of hash collisions *)
936 Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
937 T --> fastype_of1 (Ts, t))
938 | do_conceal_lambdas _ t = t
939 val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
941 fun do_introduce_combinators ctxt Ts t =
942 let val thy = Proof_Context.theory_of ctxt in
943 t |> conceal_bounds Ts
945 |> Meson_Clausify.introduce_combinators_in_cterm
946 |> prop_of |> Logic.dest_equals |> snd
949 (* A type variable of sort "{}" will make abstraction fail. *)
950 handle THM _ => t |> do_conceal_lambdas Ts
951 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
953 fun preprocess_abstractions_in_terms trans_lambdas facts =
955 val (facts, lambda_ts) =
956 facts |> map (snd o snd) |> trans_lambdas
957 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
959 map2 (fn t => fn j =>
960 ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
961 lambda_ts (1 upto length lambda_ts)
962 in (facts, lambda_facts) end
964 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
965 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
968 fun aux (t $ u) = aux t $ aux u
969 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
970 | aux (Var ((s, i), T)) =
971 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
973 in t |> exists_subterm is_Var t ? aux end
975 fun presimp_prop ctxt presimp_consts t =
977 val thy = Proof_Context.theory_of ctxt
978 val t = t |> Envir.beta_eta_contract
979 |> transform_elim_prop
980 |> Object_Logic.atomize_term thy
981 val need_trueprop = (fastype_of t = @{typ bool})
983 t |> need_trueprop ? HOLogic.mk_Trueprop
984 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
985 |> extensionalize_term ctxt
986 |> presimplify_term ctxt presimp_consts
987 |> perhaps (try (HOLogic.dest_Trueprop))
990 (* making fact and conjecture formulas *)
991 fun make_formula thy type_enc eq_as_iff name loc kind t =
993 val (iformula, atomic_types) =
994 iformula_from_prop thy type_enc eq_as_iff t []
996 {name = name, locality = loc, kind = kind, iformula = iformula,
997 atomic_types = atomic_types}
1000 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
1001 let val thy = Proof_Context.theory_of ctxt in
1002 case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1004 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1005 if s = tptp_true then NONE else SOME formula
1006 | formula => SOME formula
1009 fun make_conjecture ctxt format type_enc ps =
1011 val thy = Proof_Context.theory_of ctxt
1012 val last = length ps - 1
1014 map2 (fn j => fn ((name, loc), (kind, t)) =>
1015 t |> make_formula thy type_enc (format <> CNF) name loc kind
1016 |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
1020 (** Finite and infinite type inference **)
1022 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
1023 | deep_freeze_atyp T = T
1024 val deep_freeze_type = map_atyps deep_freeze_atyp
1026 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1027 dangerous because their "exhaust" properties can easily lead to unsound ATP
1028 proofs. On the other hand, all HOL infinite types can be given the same
1029 models in first-order logic (via Löwenheim-Skolem). *)
1031 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
1032 exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
1033 | should_encode_type _ _ All_Types _ = true
1034 | should_encode_type ctxt _ Fin_Nonmono_Types T =
1035 is_type_surely_finite ctxt false T
1036 | should_encode_type _ _ _ _ = false
1038 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
1039 should_predicate_on_var T =
1040 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
1041 should_encode_type ctxt nonmono_Ts level T
1042 | should_predicate_on_type _ _ _ _ _ = false
1044 fun is_var_or_bound_var (IConst ((s, _), _, _)) =
1045 String.isPrefix bound_var_prefix s
1046 | is_var_or_bound_var (IVar _) = true
1047 | is_var_or_bound_var _ = false
1050 Top_Level of bool option |
1051 Eq_Arg of bool option |
1054 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1055 | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
1058 Heavyweight => should_encode_type ctxt nonmono_Ts level T
1060 case (site, is_var_or_bound_var u) of
1061 (Eq_Arg pos, true) =>
1062 (* The first disjunct prevents a subtle soundness issue explained in
1063 Blanchette's Ph.D. thesis. See also
1064 "formula_lines_for_lightweight_tags_sym_decl". *)
1065 (pos <> SOME false andalso poly = Polymorphic andalso
1066 level <> All_Types andalso heaviness = Lightweight andalso
1067 exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
1068 should_encode_type ctxt nonmono_Ts level T
1070 | should_tag_with_type _ _ _ _ _ _ = false
1072 fun homogenized_type ctxt nonmono_Ts level =
1074 val should_encode = should_encode_type ctxt nonmono_Ts level
1075 fun homo 0 T = if should_encode T then T else homo_infinite_type
1076 | homo ary (Type (@{type_name fun}, [T1, T2])) =
1077 homo 0 T1 --> homo (ary - 1) T2
1078 | homo _ _ = raise Fail "expected function type"
1081 (** "hBOOL" and "hAPP" **)
1084 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1086 fun add_iterm_syms_to_table ctxt explicit_apply =
1088 fun consider_var_arity const_T var_T max_ary =
1091 if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
1092 type_instance ctxt (T, var_T) then
1095 iter (ary + 1) (range_type T)
1096 in iter 0 const_T end
1097 fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1098 if explicit_apply = NONE andalso
1099 (can dest_funT T orelse T = @{typ bool}) then
1101 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1102 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
1103 {pred_sym = pred_sym andalso not bool_vars',
1104 min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
1105 max_ary = max_ary, types = types}
1107 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1109 if bool_vars' = bool_vars andalso
1110 pointer_eq (fun_var_Ts', fun_var_Ts) then
1113 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
1117 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1118 let val (head, args) = strip_iterm_comb tm in
1120 IConst ((s, _), T, _) =>
1121 if String.isPrefix bound_var_prefix s then
1122 add_var_or_bound_var T accum
1124 let val ary = length args in
1125 ((bool_vars, fun_var_Ts),
1126 case Symtab.lookup sym_tab s of
1127 SOME {pred_sym, min_ary, max_ary, types} =>
1130 pred_sym andalso top_level andalso not bool_vars
1131 val types' = types |> insert_type ctxt I T
1133 if is_some explicit_apply orelse
1134 pointer_eq (types', types) then
1137 fold (consider_var_arity T) fun_var_Ts min_ary
1139 Symtab.update (s, {pred_sym = pred_sym,
1140 min_ary = Int.min (ary, min_ary),
1141 max_ary = Int.max (ary, max_ary),
1147 val pred_sym = top_level andalso not bool_vars
1149 case explicit_apply of
1152 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1154 Symtab.update_new (s, {pred_sym = pred_sym,
1155 min_ary = min_ary, max_ary = ary,
1160 | IVar (_, T) => add_var_or_bound_var T accum
1161 | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm
1163 |> fold (add false) args
1166 fun add_fact_syms_to_table ctxt explicit_apply =
1167 fact_lift (formula_fold NONE
1168 (K (add_iterm_syms_to_table ctxt explicit_apply)))
1170 val default_sym_tab_entries : (string * sym_info) list =
1171 (prefixed_predicator_name,
1172 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
1173 ([tptp_false, tptp_true]
1174 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1175 ([tptp_equal, tptp_old_equal]
1176 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1178 fun sym_table_for_facts ctxt explicit_apply facts =
1179 ((false, []), Symtab.empty)
1180 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1181 |> fold Symtab.update default_sym_tab_entries
1183 fun min_arity_of sym_tab s =
1184 case Symtab.lookup sym_tab s of
1185 SOME ({min_ary, ...} : sym_info) => min_ary
1187 case strip_prefix_and_unascii const_prefix s of
1189 let val s = s |> unmangled_const_name |> invert_const in
1190 if s = predicator_name then 1
1191 else if s = app_op_name then 2
1192 else if s = type_pred_name then 1
1197 (* True if the constant ever appears outside of the top-level position in
1198 literals, or if it appears with different arities (e.g., because of different
1199 type instantiations). If false, the constant always receives all of its
1200 arguments and is used as a predicate. *)
1201 fun is_pred_sym sym_tab s =
1202 case Symtab.lookup sym_tab s of
1203 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1204 pred_sym andalso min_ary = max_ary
1207 val predicator_combconst =
1208 IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1209 fun predicator tm = IApp (predicator_combconst, tm)
1211 fun introduce_predicators_in_iterm sym_tab tm =
1212 case strip_iterm_comb tm of
1213 (IConst ((s, _), _, _), _) =>
1214 if is_pred_sym sym_tab s then tm else predicator tm
1215 | _ => predicator tm
1217 fun list_app head args = fold (curry (IApp o swap)) args head
1219 val app_op = `make_fixed_const app_op_name
1221 fun explicit_app arg head =
1223 val head_T = ityp_of head
1224 val (arg_T, res_T) = dest_funT head_T
1225 val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
1226 in list_app explicit_app [head, arg] end
1227 fun list_explicit_app head args = fold explicit_app args head
1229 fun introduce_explicit_apps_in_iterm sym_tab =
1232 case strip_iterm_comb tm of
1233 (head as IConst ((s, _), _, _), args) =>
1235 |> chop (min_arity_of sym_tab s)
1237 |-> list_explicit_app
1238 | (head, args) => list_explicit_app head (map aux args)
1241 fun chop_fun 0 T = ([], T)
1242 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1243 chop_fun (n - 1) ran_T |>> cons dom_T
1244 | chop_fun _ _ = raise Fail "unexpected non-function"
1246 fun filter_type_args _ _ _ [] = []
1247 | filter_type_args thy s arity T_args =
1249 (* will throw "TYPE" for pseudo-constants *)
1250 val U = if s = app_op_name then
1251 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
1253 s |> Sign.the_const_type thy
1255 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1258 let val U_args = (s, U) |> Sign.const_typargs thy in
1260 |> map (fn (U, T) =>
1261 if member (op =) res_U_vars (dest_TVar U) then T
1265 handle TYPE _ => T_args
1267 fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
1269 val thy = Proof_Context.theory_of ctxt
1270 fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
1271 | aux arity (IConst (name as (s, _), T, T_args)) =
1272 (case strip_prefix_and_unascii const_prefix s of
1273 NONE => (name, T_args)
1276 val s'' = invert_const s''
1277 fun filtered_T_args false = T_args
1278 | filtered_T_args true = filter_type_args thy s'' arity T_args
1280 case type_arg_policy type_enc s'' of
1281 Explicit_Type_Args drop_args =>
1282 (name, filtered_T_args drop_args)
1283 | Mangled_Type_Args drop_args =>
1284 (mangled_const_name format type_enc (filtered_T_args drop_args)
1286 | No_Type_Args => (name, [])
1288 |> (fn (name, T_args) => IConst (name, T, T_args))
1289 | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
1293 fun repair_iterm ctxt format type_enc sym_tab =
1294 not (is_type_enc_higher_order type_enc)
1295 ? (introduce_explicit_apps_in_iterm sym_tab
1296 #> introduce_predicators_in_iterm sym_tab)
1297 #> enforce_type_arg_policy_in_iterm ctxt format type_enc
1298 fun repair_fact ctxt format type_enc sym_tab =
1299 update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
1301 (** Helper facts **)
1303 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1305 [(("COMBI", false), @{thms Meson.COMBI_def}),
1306 (("COMBK", false), @{thms Meson.COMBK_def}),
1307 (("COMBB", false), @{thms Meson.COMBB_def}),
1308 (("COMBC", false), @{thms Meson.COMBC_def}),
1309 (("COMBS", false), @{thms Meson.COMBS_def}),
1310 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1311 (("fFalse", true), @{thms True_or_False}),
1312 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1313 (("fTrue", true), @{thms True_or_False}),
1315 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1316 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1318 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1319 by (unfold fconj_def) fast+}),
1321 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1322 by (unfold fdisj_def) fast+}),
1323 (("fimplies", false),
1324 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1325 by (unfold fimplies_def) fast+}),
1327 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1328 However, this is done so for backward compatibility: Including the
1329 equality helpers by default in Metis breaks a few existing proofs. *)
1330 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1331 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1332 (("fAll", false), []), (*TODO: add helpers*)
1333 (("fEx", false), []), (*TODO: add helpers*)
1334 (("If", true), @{thms if_True if_False True_or_False})]
1335 |> map (apsnd (map zero_var_indexes))
1337 val type_tag = `make_fixed_const type_tag_name
1339 fun type_tag_idempotence_fact () =
1341 fun var s = ATerm (`I s, [])
1342 fun tag tm = ATerm (type_tag, [var "T", tm])
1343 val tagged_a = tag (var "A")
1345 Formula (type_tag_idempotence_helper_name, Axiom,
1346 AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
1347 |> close_formula_universally, isabelle_info simpN, NONE)
1350 fun should_specialize_helper type_enc t =
1351 polymorphism_of_type_enc type_enc = Mangled_Monomorphic andalso
1352 level_of_type_enc type_enc <> No_Types andalso
1353 not (null (Term.hidden_polymorphism t))
1355 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1356 case strip_prefix_and_unascii const_prefix s of
1359 val thy = Proof_Context.theory_of ctxt
1360 val unmangled_s = mangled_s |> unmangled_const_name
1361 fun dub needs_fairly_sound j k =
1362 (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1363 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1364 (if needs_fairly_sound then typed_helper_suffix
1365 else untyped_helper_suffix),
1367 fun dub_and_inst needs_fairly_sound (th, j) =
1368 let val t = prop_of th in
1369 if should_specialize_helper type_enc t then
1370 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1375 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1376 val make_facts = map_filter (make_fact ctxt format type_enc false)
1377 val fairly_sound = is_type_enc_fairly_sound type_enc
1380 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1381 if helper_s <> unmangled_s orelse
1382 (needs_fairly_sound andalso not fairly_sound) then
1385 ths ~~ (1 upto length ths)
1386 |> maps (dub_and_inst needs_fairly_sound)
1390 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1391 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1394 (***************************************************************)
1395 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1396 (***************************************************************)
1398 fun set_insert (x, s) = Symtab.update (x, ()) s
1400 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1402 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1403 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1405 fun classes_of_terms get_Ts =
1406 map (map snd o get_Ts)
1407 #> List.foldl add_classes Symtab.empty
1408 #> delete_type #> Symtab.keys
1410 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
1411 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
1413 fun fold_type_constrs f (Type (s, Ts)) x =
1414 fold (fold_type_constrs f) Ts (f (s, x))
1415 | fold_type_constrs _ _ x = x
1417 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1418 fun add_type_constrs_in_term thy =
1420 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1421 | add (t $ u) = add t #> add u
1422 | add (Const (x as (s, _))) =
1423 if String.isPrefix skolem_const_prefix s then I
1424 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1425 | add (Abs (_, _, u)) = add u
1429 fun type_constrs_of_terms thy ts =
1430 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1432 fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
1433 hyp_ts concl_t facts =
1435 val thy = Proof_Context.theory_of ctxt
1436 val presimp_consts = Meson.presimplified_consts ctxt
1437 val fact_ts = facts |> map snd
1438 (* Remove existing facts from the conjecture, as this can dramatically
1439 boost an ATP's performance (for some reason). *)
1442 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1443 val facts = facts |> map (apsnd (pair Axiom))
1445 map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
1446 |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
1447 val ((conjs, facts), lambdas) =
1450 |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
1451 |> preprocess_abstractions_in_terms trans_lambdas
1452 |>> chop (length conjs)
1453 |>> apfst (map (apsnd (apsnd freeze_term)))
1455 ((conjs, facts), [])
1456 val conjs = conjs |> make_conjecture ctxt format type_enc
1457 val (fact_names, facts) =
1459 |> map_filter (fn (name, (_, t)) =>
1460 make_fact ctxt format type_enc true (name, t)
1461 |> Option.map (pair name))
1464 lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1465 val all_ts = concl_t :: hyp_ts @ fact_ts
1466 val subs = tfree_classes_of_terms all_ts
1467 val supers = tvar_classes_of_terms all_ts
1468 val tycons = type_constrs_of_terms thy all_ts
1469 val (supers, arity_clauses) =
1470 if level_of_type_enc type_enc = No_Types then ([], [])
1471 else make_arity_clauses thy tycons supers
1472 val class_rel_clauses = make_class_rel_clauses thy subs supers
1474 (fact_names |> map single,
1475 (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
1478 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
1479 (true, ATerm (class, [ATerm (name, [])]))
1480 | fo_literal_from_type_literal (TyLitFree (class, name)) =
1481 (true, ATerm (class, [ATerm (name, [])]))
1483 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1485 val type_pred = `make_fixed_const type_pred_name
1487 fun type_pred_iterm ctxt format type_enc T tm =
1488 IApp (IConst (type_pred, T --> @{typ bool}, [T])
1489 |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
1491 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1492 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1493 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1494 | is_var_positively_naked_in_term _ _ _ _ = true
1495 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
1496 formula_fold pos (is_var_positively_naked_in_term name) phi false
1497 | should_predicate_on_var_in_formula _ _ _ _ = true
1499 fun mk_aterm format type_enc name T_args args =
1500 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1502 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
1503 IConst (type_tag, T --> T, [T])
1504 |> enforce_type_arg_policy_in_iterm ctxt format type_enc
1505 |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1506 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1507 | _ => raise Fail "unexpected lambda-abstraction")
1508 and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
1512 val (head, args) = strip_iterm_comb u
1515 Top_Level pos => pos
1520 IConst (name as (s, _), _, T_args) =>
1522 val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
1524 mk_aterm format type_enc name T_args (map (aux arg_site) args)
1527 mk_aterm format type_enc name [] (map (aux Elsewhere) args)
1528 | IAbs ((name, T), tm) =>
1529 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1531 | IApp _ => raise Fail "impossible \"IApp\""
1534 t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
1535 tag_with_type ctxt format nonmono_Ts type_enc pos T
1540 and formula_from_iformula ctxt format nonmono_Ts type_enc
1541 should_predicate_on_var =
1543 val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
1546 Simple_Types (_, level) =>
1547 homogenized_type ctxt nonmono_Ts level 0
1548 #> ho_type_from_typ format type_enc false 0 #> SOME
1550 fun do_out_of_bound_type pos phi universal (name, T) =
1551 if should_predicate_on_type ctxt nonmono_Ts type_enc
1552 (fn () => should_predicate_on_var pos phi universal name) T then
1554 |> type_pred_iterm ctxt format type_enc T
1555 |> do_term pos |> AAtom |> SOME
1558 fun do_formula pos (AQuant (q, xs, phi)) =
1560 val phi = phi |> do_formula pos
1561 val universal = Option.map (q = AExists ? not) pos
1563 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1564 | SOME T => do_bound_type T)),
1565 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1567 (fn (_, NONE) => NONE
1569 do_out_of_bound_type pos phi universal (s, T))
1573 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1574 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1577 fun bound_tvars type_enc Ts =
1578 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1579 (type_literals_for_types type_enc add_sorts_on_tvar Ts))
1581 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1582 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1583 the remote provers might care. *)
1584 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
1585 type_enc (j, {name, locality, kind, iformula, atomic_types}) =
1586 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
1588 |> close_iformula_universally
1589 |> formula_from_iformula ctxt format nonmono_Ts type_enc
1590 should_predicate_on_var_in_formula
1591 (if pos then SOME true else NONE)
1592 |> bound_tvars type_enc atomic_types
1593 |> close_formula_universally,
1596 Intro => isabelle_info introN
1597 | Elim => isabelle_info elimN
1598 | Simp => isabelle_info simpN
1602 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1603 : class_rel_clause) =
1604 let val ty_arg = ATerm (`I "T", []) in
1605 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1606 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
1607 AAtom (ATerm (superclass, [ty_arg]))])
1608 |> close_formula_universally, isabelle_info introN, NONE)
1611 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
1612 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
1613 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
1614 (false, ATerm (c, [ATerm (sort, [])]))
1616 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1618 Formula (arity_clause_prefix ^ name, Axiom,
1619 mk_ahorn (map (formula_from_fo_literal o apfst not
1620 o fo_literal_from_arity_literal) prem_lits)
1621 (formula_from_fo_literal
1622 (fo_literal_from_arity_literal concl_lits))
1623 |> close_formula_universally, isabelle_info introN, NONE)
1625 fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
1626 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
1627 Formula (conjecture_prefix ^ name, kind,
1628 formula_from_iformula ctxt format nonmono_Ts type_enc
1629 should_predicate_on_var_in_formula (SOME false)
1630 (close_iformula_universally iformula)
1631 |> bound_tvars type_enc atomic_types
1632 |> close_formula_universally, NONE, NONE)
1634 fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
1635 atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
1636 |> map fo_literal_from_type_literal
1638 fun formula_line_for_free_type j lit =
1639 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1640 formula_from_fo_literal lit, NONE, NONE)
1641 fun formula_lines_for_free_types type_enc facts =
1643 val litss = map (free_type_literals type_enc) facts
1644 val lits = fold (union (op =)) litss []
1645 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1647 (** Symbol declarations **)
1649 fun should_declare_sym type_enc pred_sym s =
1650 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1652 Simple_Types _ => true
1653 | Tags (_, _, Lightweight) => true
1654 | _ => not pred_sym)
1656 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
1658 fun add_iterm in_conj tm =
1659 let val (head, args) = strip_iterm_comb tm in
1661 IConst ((s, s'), T, T_args) =>
1662 let val pred_sym = is_pred_sym repaired_sym_tab s in
1663 if should_declare_sym type_enc pred_sym s then
1664 Symtab.map_default (s, [])
1665 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1670 | IAbs (_, tm) => add_iterm in_conj tm
1672 #> fold (add_iterm in_conj) args
1674 fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
1677 |> is_type_enc_fairly_sound type_enc
1678 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1681 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1682 out with monotonicity" paper presented at CADE 2011. *)
1683 fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
1684 | add_iterm_nonmonotonic_types ctxt level sound locality _
1685 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
1686 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1688 Noninf_Nonmono_Types =>
1689 not (is_locality_global locality) orelse
1690 not (is_type_surely_infinite ctxt sound T)
1691 | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
1692 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1693 | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
1694 fun add_fact_nonmonotonic_types ctxt level sound
1695 ({kind, locality, iformula, ...} : translated_formula) =
1696 formula_fold (SOME (kind <> Conjecture))
1697 (add_iterm_nonmonotonic_types ctxt level sound locality)
1699 fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
1700 let val level = level_of_type_enc type_enc in
1701 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1702 [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
1703 (* We must add "bool" in case the helper "True_or_False" is added
1704 later. In addition, several places in the code rely on the list of
1705 nonmonotonic types not being empty. *)
1706 |> insert_type ctxt I @{typ bool}
1711 fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
1712 (s', T_args, T, pred_sym, ary, _) =
1714 val (T_arg_Ts, level) =
1716 Simple_Types (_, level) => ([], level)
1717 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1719 Decl (sym_decl_prefix ^ s, (s, s'),
1720 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1721 |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
1724 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1725 poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
1727 val (kind, maybe_negate) =
1728 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1730 val (arg_Ts, res_T) = chop_fun ary T
1731 val num_args = length arg_Ts
1733 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1735 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
1736 val sym_needs_arg_types = exists (curry (op =) dummyT) T_args)
1737 fun should_keep_arg_type T =
1738 sym_needs_arg_types orelse
1739 not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
1741 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1743 Formula (preds_sym_formula_prefix ^ s ^
1744 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1745 IConst ((s, s'), T, T_args)
1746 |> fold (curry (IApp o swap)) bounds
1747 |> type_pred_iterm ctxt format type_enc res_T
1748 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1749 |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
1750 (K (K (K (K true)))) (SOME true)
1751 |> n > 1 ? bound_tvars type_enc (atyps_of T)
1752 |> close_formula_universally
1754 isabelle_info introN, NONE)
1757 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1758 poly_nonmono_Ts type_enc n s
1759 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1762 lightweight_tags_sym_formula_prefix ^ s ^
1763 (if n > 1 then "_" ^ string_of_int j else "")
1764 val (kind, maybe_negate) =
1765 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1767 val (arg_Ts, res_T) = chop_fun ary T
1769 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1770 val bounds = bound_names |> map (fn name => ATerm (name, []))
1771 val cst = mk_aterm format type_enc (s, s') T_args
1772 val atomic_Ts = atyps_of T
1774 (if pred_sym then AConn (AIff, map AAtom tms)
1775 else AAtom (ATerm (`I tptp_equal, tms)))
1776 |> bound_tvars type_enc atomic_Ts
1777 |> close_formula_universally
1779 (* See also "should_tag_with_type". *)
1780 fun should_encode T =
1781 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1783 Tags (Polymorphic, level, Lightweight) =>
1784 level <> All_Types andalso Monomorph.typ_has_tvars T
1786 val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
1787 val add_formula_for_res =
1788 if should_encode res_T then
1789 cons (Formula (ident_base ^ "_res", kind,
1790 eq [tag_with res_T (cst bounds), cst bounds],
1791 isabelle_info simpN, NONE))
1794 fun add_formula_for_arg k =
1795 let val arg_T = nth arg_Ts k in
1796 if should_encode arg_T then
1797 case chop k bounds of
1798 (bounds1, bound :: bounds2) =>
1799 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
1800 eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
1802 isabelle_info simpN, NONE))
1803 | _ => raise Fail "expected nonempty tail"
1808 [] |> not pred_sym ? add_formula_for_res
1809 |> fold add_formula_for_arg (ary - 1 downto 0)
1812 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1814 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1815 poly_nonmono_Ts type_enc (s, decls) =
1818 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
1823 decl :: (decls' as _ :: _) =>
1824 let val T = result_type_of_decl decl in
1825 if forall (curry (type_instance ctxt o swap) T
1826 o result_type_of_decl) decls' then
1832 val n = length decls
1834 decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
1836 o result_type_of_decl)
1838 (0 upto length decls - 1, decls)
1839 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1840 nonmono_Ts poly_nonmono_Ts type_enc n s)
1842 | Tags (_, _, heaviness) =>
1846 let val n = length decls in
1847 (0 upto n - 1 ~~ decls)
1848 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1849 conj_sym_kind poly_nonmono_Ts type_enc n s)
1852 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1853 poly_nonmono_Ts type_enc sym_decl_tab =
1858 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1859 nonmono_Ts poly_nonmono_Ts type_enc)
1861 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1862 poly <> Mangled_Monomorphic andalso
1863 ((level = All_Types andalso heaviness = Lightweight) orelse
1864 level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
1865 | needs_type_tag_idempotence _ = false
1867 fun offset_of_heading_in_problem _ [] j = j
1868 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1869 if heading = needle then j
1870 else offset_of_heading_in_problem needle problem (j + length lines)
1872 val implicit_declsN = "Should-be-implicit typings"
1873 val explicit_declsN = "Explicit typings"
1874 val factsN = "Relevant facts"
1875 val class_relsN = "Class relationships"
1876 val aritiesN = "Arities"
1877 val helpersN = "Helper facts"
1878 val conjsN = "Conjectures"
1879 val free_typesN = "Type variables"
1881 val explicit_apply = NONE (* for experiments *)
1883 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
1884 exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
1886 val (format, type_enc) = choose_format [format] type_enc
1887 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1888 translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
1889 hyp_ts concl_t facts
1890 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1892 conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
1893 val repair = repair_fact ctxt format type_enc sym_tab
1894 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1895 val repaired_sym_tab =
1896 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1898 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
1900 val poly_nonmono_Ts =
1901 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1902 polymorphism_of_type_enc type_enc <> Polymorphic then
1905 [TVar (("'a", 0), HOLogic.typeS)]
1906 val sym_decl_lines =
1907 (conjs, helpers @ facts)
1908 |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
1909 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1910 poly_nonmono_Ts type_enc
1912 0 upto length helpers - 1 ~~ helpers
1913 |> map (formula_line_for_fact ctxt format helper_prefix I false true
1914 poly_nonmono_Ts type_enc)
1915 |> (if needs_type_tag_idempotence type_enc then
1916 cons (type_tag_idempotence_fact ())
1919 (* Reordering these might confuse the proof reconstruction code or the SPASS
1922 [(explicit_declsN, sym_decl_lines),
1924 map (formula_line_for_fact ctxt format fact_prefix ascii_of
1925 (not exporter) (not exporter) nonmono_Ts
1927 (0 upto length facts - 1 ~~ facts)),
1928 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1929 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1930 (helpersN, helper_lines),
1932 map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
1934 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
1938 CNF => ensure_cnf_problem
1939 | CNF_UEQ => filter_cnf_ueq_problem
1941 |> (if is_format_typed format then
1942 declare_undeclared_syms_in_atp_problem type_decl_prefix
1946 val (problem, pool) = problem |> nice_atp_problem readable_names
1947 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
1949 map_filter (fn (j, {name, ...}) =>
1950 if String.isSuffix typed_helper_suffix name then SOME j
1952 ((helpers_offset + 1 upto helpers_offset + length helpers)
1954 fun add_sym_arity (s, {min_ary, ...} : sym_info) =
1956 case strip_prefix_and_unascii const_prefix s of
1957 SOME s => Symtab.insert (op =) (s, min_ary)
1963 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1964 offset_of_heading_in_problem conjsN problem 0,
1965 offset_of_heading_in_problem factsN problem 0,
1966 fact_names |> Vector.fromList,
1968 Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
1972 val conj_weight = 0.0
1973 val hyp_weight = 0.1
1974 val fact_min_weight = 0.2
1975 val fact_max_weight = 1.0
1976 val type_info_default_weight = 0.8
1978 fun add_term_weights weight (ATerm (s, tms)) =
1979 is_tptp_user_symbol s ? Symtab.default (s, weight)
1980 #> fold (add_term_weights weight) tms
1981 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
1982 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1983 formula_fold NONE (K (add_term_weights weight)) phi
1984 | add_problem_line_weights _ _ = I
1986 fun add_conjectures_weights [] = I
1987 | add_conjectures_weights conjs =
1988 let val (hyps, conj) = split_last conjs in
1989 add_problem_line_weights conj_weight conj
1990 #> fold (add_problem_line_weights hyp_weight) hyps
1993 fun add_facts_weights facts =
1995 val num_facts = length facts
1997 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
1998 / Real.fromInt num_facts
2000 map weight_of (0 upto num_facts - 1) ~~ facts
2001 |> fold (uncurry add_problem_line_weights)
2004 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2005 fun atp_problem_weights problem =
2006 let val get = these o AList.lookup (op =) problem in
2008 |> add_conjectures_weights (get free_typesN @ get conjsN)
2009 |> add_facts_weights (get factsN)
2010 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
2011 [explicit_declsN, class_relsN, aritiesN]
2013 |> sort (prod_ord Real.compare string_ord o pairself swap)