1 (* Title: HOL/Tools/ATP/atp_problem_generate.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_PROBLEM_GENERATE =
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 atp_format = ATP_Problem.atp_format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
18 datatype scope = Global | Local | Assum | Chained
19 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
20 type stature = scope * status
22 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
23 datatype strictness = Strict | Non_Strict
24 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
27 Noninf_Nonmono_Types of strictness * granularity |
28 Fin_Nonmono_Types of granularity |
33 val type_tag_idempotence : bool Config.T
34 val type_tag_arguments : bool Config.T
36 val hide_lamsN : string
39 val combs_and_liftingN : string
40 val combs_or_liftingN : string
41 val lam_liftingN : string
42 val keep_lamsN : string
43 val schematic_var_prefix : string
44 val fixed_var_prefix : string
45 val tvar_prefix : string
46 val tfree_prefix : string
47 val const_prefix : string
48 val type_const_prefix : string
49 val class_prefix : string
50 val lam_lifted_prefix : string
51 val lam_lifted_mono_prefix : string
52 val lam_lifted_poly_prefix : string
53 val skolem_const_prefix : string
54 val old_skolem_const_prefix : string
55 val new_skolem_const_prefix : string
56 val combinator_prefix : string
57 val type_decl_prefix : string
58 val sym_decl_prefix : string
59 val guards_sym_formula_prefix : string
60 val tags_sym_formula_prefix : string
61 val fact_prefix : string
62 val conjecture_prefix : string
63 val helper_prefix : string
64 val class_rel_clause_prefix : string
65 val arity_clause_prefix : string
66 val tfree_clause_prefix : string
67 val lam_fact_prefix : string
68 val typed_helper_suffix : string
69 val untyped_helper_suffix : string
70 val type_tag_idempotence_helper_name : string
71 val predicator_name : string
72 val app_op_name : string
73 val type_guard_name : string
74 val type_tag_name : string
75 val native_type_prefix : string
76 val prefixed_predicator_name : string
77 val prefixed_app_op_name : string
78 val prefixed_type_tag_name : string
79 val ascii_of : string -> string
80 val unascii_of : string -> string
81 val unprefix_and_unascii : string -> string -> string option
82 val proxy_table : (string * (string * (thm * (string * string)))) list
83 val proxify_const : string -> (string * string) option
84 val invert_const : string -> string
85 val unproxify_const : string -> string
86 val new_skolem_var_name_from_const : string -> string
87 val atp_irrelevant_consts : string list
88 val atp_schematic_consts_of : term -> typ list Symtab.table
89 val is_type_enc_higher_order : type_enc -> bool
90 val polymorphism_of_type_enc : type_enc -> polymorphism
91 val level_of_type_enc : type_enc -> type_level
92 val is_type_enc_quasi_sound : type_enc -> bool
93 val is_type_enc_fairly_sound : type_enc -> bool
94 val type_enc_from_string : strictness -> string -> type_enc
95 val adjust_type_enc : atp_format -> type_enc -> type_enc
97 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
98 val unmangled_const : string -> string * (string, 'b) ho_term list
99 val unmangled_const_name : string -> string list
100 val helper_table : ((string * bool) * thm list) list
101 val trans_lams_from_string :
102 Proof.context -> type_enc -> string -> term list -> term list * term list
104 val prepare_atp_problem :
105 Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
106 -> bool -> string -> bool -> bool -> bool -> term list -> term
107 -> ((string * stature) * term) list
108 -> string problem * string Symtab.table * (string * stature) list vector
109 * (string * term) list * int Symtab.table
110 val atp_problem_selection_weights : string problem -> (string * real) list
111 val atp_problem_term_order_weights : string problem -> (string * int) list
114 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
120 type name = string * string
122 val type_tag_idempotence =
123 Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
124 val type_tag_arguments =
125 Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
127 val no_lamsN = "no_lams" (* used internally; undocumented *)
128 val hide_lamsN = "hide_lams"
129 val liftingN = "lifting"
131 val combs_and_liftingN = "combs_and_lifting"
132 val combs_or_liftingN = "combs_or_lifting"
133 val keep_lamsN = "keep_lams"
134 val lam_liftingN = "lam_lifting" (* legacy *)
136 (* It's still unclear whether all TFF1 implementations will support type
137 signatures such as "!>[A : $tType] : $o", with ghost type variables. *)
138 val avoid_first_order_ghost_type_vars = false
140 val bound_var_prefix = "B_"
141 val all_bound_var_prefix = "BA_"
142 val exist_bound_var_prefix = "BE_"
143 val schematic_var_prefix = "V_"
144 val fixed_var_prefix = "v_"
145 val tvar_prefix = "T_"
146 val tfree_prefix = "t_"
147 val const_prefix = "c_"
148 val type_const_prefix = "tc_"
149 val native_type_prefix = "n_"
150 val class_prefix = "cl_"
152 (* Freshness almost guaranteed! *)
153 val atp_prefix = "ATP" ^ Long_Name.separator
154 val atp_weak_prefix = "ATP:"
156 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
157 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
158 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
160 val skolem_const_prefix = atp_prefix ^ "Sko"
161 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
162 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
164 val combinator_prefix = "COMB"
166 val type_decl_prefix = "ty_"
167 val sym_decl_prefix = "sy_"
168 val guards_sym_formula_prefix = "gsy_"
169 val tags_sym_formula_prefix = "tsy_"
170 val uncurried_alias_eq_prefix = "unc_"
171 val fact_prefix = "fact_"
172 val conjecture_prefix = "conj_"
173 val helper_prefix = "help_"
174 val class_rel_clause_prefix = "clar_"
175 val arity_clause_prefix = "arity_"
176 val tfree_clause_prefix = "tfree_"
178 val lam_fact_prefix = "ATP.lambda_"
179 val typed_helper_suffix = "_T"
180 val untyped_helper_suffix = "_U"
181 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
183 val predicator_name = "pp"
184 val app_op_name = "aa"
185 val type_guard_name = "gg"
186 val type_tag_name = "tt"
188 val prefixed_predicator_name = const_prefix ^ predicator_name
189 val prefixed_app_op_name = const_prefix ^ app_op_name
190 val prefixed_type_tag_name = const_prefix ^ type_tag_name
192 (*Escaping of special characters.
193 Alphanumeric characters are left unchanged.
194 The character _ goes to __
195 Characters in the range ASCII space to / go to _A to _P, respectively.
196 Other characters go to _nnn where nnn is the decimal ASCII code.*)
197 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
199 fun stringN_of_int 0 _ = ""
200 | stringN_of_int k n =
201 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
203 fun ascii_of_char c =
204 if Char.isAlphaNum c then
206 else if c = #"_" then
208 else if #" " <= c andalso c <= #"/" then
209 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
211 (* fixed width, in case more digits follow *)
212 "_" ^ stringN_of_int 3 (Char.ord c)
214 val ascii_of = String.translate ascii_of_char
216 (** Remove ASCII armoring from names in proof files **)
218 (* We don't raise error exceptions because this code can run inside a worker
219 thread. Also, the errors are impossible. *)
222 fun un rcs [] = String.implode(rev rcs)
223 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
224 (* Three types of _ escapes: __, _A to _P, _nnn *)
225 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
226 | un rcs (#"_" :: c :: cs) =
227 if #"A" <= c andalso c<= #"P" then
228 (* translation of #" " to #"/" *)
229 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
231 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
232 case Int.fromString (String.implode digits) of
233 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
234 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
236 | un rcs (c :: cs) = un (c :: rcs) cs
237 in un [] o String.explode end
239 (* If string s has the prefix s1, return the result of deleting it,
241 fun unprefix_and_unascii s1 s =
242 if String.isPrefix s1 s then
243 SOME (unascii_of (String.extract (s, size s1, NONE)))
248 [("c_False", (@{const_name False}, (@{thm fFalse_def},
249 ("fFalse", @{const_name ATP.fFalse})))),
250 ("c_True", (@{const_name True}, (@{thm fTrue_def},
251 ("fTrue", @{const_name ATP.fTrue})))),
252 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
253 ("fNot", @{const_name ATP.fNot})))),
254 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
255 ("fconj", @{const_name ATP.fconj})))),
256 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
257 ("fdisj", @{const_name ATP.fdisj})))),
258 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
259 ("fimplies", @{const_name ATP.fimplies})))),
260 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
261 ("fequal", @{const_name ATP.fequal})))),
262 ("c_All", (@{const_name All}, (@{thm fAll_def},
263 ("fAll", @{const_name ATP.fAll})))),
264 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
265 ("fEx", @{const_name ATP.fEx}))))]
267 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
269 (* Readable names for the more common symbolic functions. Do not mess with the
270 table unless you know what you are doing. *)
271 val const_trans_table =
272 [(@{type_name Product_Type.prod}, "prod"),
273 (@{type_name Sum_Type.sum}, "sum"),
274 (@{const_name False}, "False"),
275 (@{const_name True}, "True"),
276 (@{const_name Not}, "Not"),
277 (@{const_name conj}, "conj"),
278 (@{const_name disj}, "disj"),
279 (@{const_name implies}, "implies"),
280 (@{const_name HOL.eq}, "equal"),
281 (@{const_name All}, "All"),
282 (@{const_name Ex}, "Ex"),
283 (@{const_name If}, "If"),
284 (@{const_name Set.member}, "member"),
285 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
286 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
287 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
288 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
289 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
291 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
293 (* Invert the table of translations between Isabelle and ATPs. *)
294 val const_trans_table_inv =
295 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
296 val const_trans_table_unprox =
298 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
300 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
301 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
304 case Symtab.lookup const_trans_table c of
308 fun ascii_of_indexname (v, 0) = ascii_of v
309 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
311 fun make_bound_var x = bound_var_prefix ^ ascii_of x
312 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
313 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
314 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
315 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
317 fun make_schematic_type_var (x, i) =
318 tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
319 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
321 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
323 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
324 fun default c = const_prefix ^ lookup_const c
326 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
327 | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
328 if c = choice_const then tptp_choice else default c
329 | make_fixed_const _ c = default c
332 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
334 fun make_type_class clas = class_prefix ^ ascii_of clas
336 fun new_skolem_var_name_from_const s =
337 let val ss = s |> space_explode Long_Name.separator in
338 nth ss (length ss - 2)
341 (* These are either simplified away by "Meson.presimplify" (most of the time) or
342 handled specially via "fFalse", "fTrue", ..., "fequal". *)
343 val atp_irrelevant_consts =
344 [@{const_name False}, @{const_name True}, @{const_name Not},
345 @{const_name conj}, @{const_name disj}, @{const_name implies},
346 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
348 val atp_monomorph_bad_consts =
349 atp_irrelevant_consts @
350 (* These are ignored anyway by the relevance filter (unless they appear in
351 higher-order places) but not by the monomorphizer. *)
352 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
353 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
354 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
356 fun add_schematic_const (x as (_, T)) =
357 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
358 val add_schematic_consts_of =
359 Term.fold_aterms (fn Const (x as (s, _)) =>
360 not (member (op =) atp_monomorph_bad_consts s)
361 ? add_schematic_const x
363 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
365 (** Definitions and functions for FOL clauses and formulas for TPTP **)
367 (** Isabelle arities **)
369 type arity_atom = name * name * name list
371 val type_class = the_single @{sort type}
375 prem_atoms : arity_atom list,
376 concl_atom : arity_atom}
378 fun add_prem_atom tvar =
379 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
381 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
382 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
384 val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
385 val tvars_srts = ListPair.zip (tvars, args)
388 prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
389 concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
393 fun arity_clause _ _ (_, []) = []
394 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
395 arity_clause seen n (tcons, ars)
396 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
397 if member (op =) seen class then
398 (* multiple arities for the same (tycon, class) pair *)
399 make_axiom_arity_clause (tcons,
400 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
402 arity_clause seen (n + 1) (tcons, ars)
404 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
405 ascii_of class, ar) ::
406 arity_clause (class :: seen) n (tcons, ars)
408 fun multi_arity_clause [] = []
409 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
410 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
412 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
413 theory thy provided its arguments have the corresponding sorts. *)
414 fun type_class_pairs thy tycons classes =
416 val alg = Sign.classes_of thy
417 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
418 fun add_class tycon class =
419 cons (class, domain_sorts tycon class)
420 handle Sorts.CLASS_ERROR _ => I
421 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
422 in map try_classes tycons end
424 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
425 fun iter_type_class_pairs _ _ [] = ([], [])
426 | iter_type_class_pairs thy tycons classes =
428 fun maybe_insert_class s =
429 (s <> type_class andalso not (member (op =) classes s))
431 val cpairs = type_class_pairs thy tycons classes
433 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
434 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
435 in (classes' @ classes, union (op =) cpairs' cpairs) end
437 fun make_arity_clauses thy tycons =
438 iter_type_class_pairs thy tycons ##> multi_arity_clause
441 (** Isabelle class relations **)
443 type class_rel_clause =
448 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
450 fun class_pairs _ [] _ = []
451 | class_pairs thy subs supers =
453 val class_less = Sorts.class_less (Sign.classes_of thy)
454 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
455 fun add_supers sub = fold (add_super sub) supers
456 in fold add_supers subs [] end
458 fun make_class_rel_clause (sub, super) =
459 {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
460 superclass = `make_type_class super}
462 fun make_class_rel_clauses thy subs supers =
463 map make_class_rel_clause (class_pairs thy subs supers)
465 (* intermediate terms *)
467 IConst of name * typ * typ list |
469 IApp of iterm * iterm |
470 IAbs of (name * typ) * iterm
472 fun ityp_of (IConst (_, T, _)) = T
473 | ityp_of (IVar (_, T)) = T
474 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
475 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
477 (*gets the head of a combinator application, along with the list of arguments*)
478 fun strip_iterm_comb u =
480 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
482 in stripc (u, []) end
484 fun atomic_types_of T = fold_atyps (insert (op =)) T []
486 val tvar_a_str = "'a"
487 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
488 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
489 val itself_name = `make_fixed_type_const @{type_name itself}
490 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
491 val tvar_a_atype = AType (tvar_a_name, [])
492 val a_itself_atype = AType (itself_name, [tvar_a_atype])
494 fun new_skolem_const_name s num_T_args =
495 [new_skolem_const_prefix, s, string_of_int num_T_args]
498 fun robust_const_type thy s =
499 if s = app_op_name then
500 Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
501 else if String.isPrefix lam_lifted_prefix s then
502 Logic.varifyT_global @{typ "'a => 'b"}
504 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
505 s |> Sign.the_const_type thy
507 val robust_const_ary =
509 fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T
511 in ary oo robust_const_type end
513 (* This function only makes sense if "T" is as general as possible. *)
514 fun robust_const_typargs thy (s, T) =
515 if s = app_op_name then
516 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
517 else if String.isPrefix old_skolem_const_prefix s then
518 [] |> Term.add_tvarsT T |> rev |> map TVar
519 else if String.isPrefix lam_lifted_prefix s then
520 if String.isPrefix lam_lifted_poly_prefix s then
521 let val (T1, T2) = T |> dest_funT in [T1, T2] end
525 (s, T) |> Sign.const_typargs thy
527 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
528 Also accumulates sort infomation. *)
529 fun iterm_from_term thy format bs (P $ Q) =
531 val (P', P_atomics_Ts) = iterm_from_term thy format bs P
532 val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
533 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
534 | iterm_from_term thy format _ (Const (c, T)) =
535 (IConst (`(make_fixed_const (SOME format)) c, T,
536 robust_const_typargs thy (c, T)),
538 | iterm_from_term _ _ _ (Free (s, T)) =
539 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
540 | iterm_from_term _ format _ (Var (v as (s, _), T)) =
541 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
543 val Ts = T |> strip_type |> swap |> op ::
544 val s' = new_skolem_const_name s (length Ts)
545 in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
547 IVar ((make_schematic_var v, s), T), atomic_types_of T)
548 | iterm_from_term _ _ bs (Bound j) =
549 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
550 | iterm_from_term thy format bs (Abs (s, T, t)) =
552 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
554 val name = `make_bound_var s
555 val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
556 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
558 datatype scope = Global | Local | Assum | Chained
559 datatype status = General | Induct | Intro | Elim | Simp | Spec_Eq
560 type stature = scope * status
562 datatype order = First_Order | Higher_Order
563 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
564 datatype strictness = Strict | Non_Strict
565 datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
566 datatype type_level =
568 Noninf_Nonmono_Types of strictness * granularity |
569 Fin_Nonmono_Types of granularity |
574 Simple_Types of order * polymorphism * type_level |
575 Guards of polymorphism * type_level |
576 Tags of polymorphism * type_level
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 (_, poly, _)) = poly
582 | polymorphism_of_type_enc (Guards (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 (Guards (_, level)) = level
587 | level_of_type_enc (Tags (_, level)) = level
589 fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
590 | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
591 | granularity_of_type_level _ = All_Vars
593 fun is_type_level_quasi_sound All_Types = true
594 | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
595 | is_type_level_quasi_sound _ = false
596 val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc
598 fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
599 | is_type_level_fairly_sound level = is_type_level_quasi_sound level
600 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
602 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
603 | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
604 | is_type_level_monotonicity_based _ = false
606 (* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
608 val queries = ["?", "_query"]
609 val bangs = ["!", "_bang"]
610 val ats = ["@", "_at"]
612 fun try_unsuffixes ss s =
613 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
615 fun try_nonmono constr suffixes fallback s =
616 case try_unsuffixes suffixes s of
618 (case try_unsuffixes suffixes s of
619 SOME s => (constr Positively_Naked_Vars, s)
621 case try_unsuffixes ats s of
622 SOME s => (constr Ghost_Type_Arg_Vars, s)
623 | NONE => (constr All_Vars, s))
626 fun type_enc_from_string strictness s =
627 (case try (unprefix "poly_") s of
628 SOME s => (SOME Polymorphic, s)
630 case try (unprefix "raw_mono_") s of
631 SOME s => (SOME Raw_Monomorphic, s)
633 case try (unprefix "mono_") s of
634 SOME s => (SOME Mangled_Monomorphic, s)
637 |> try_nonmono Fin_Nonmono_Types bangs
638 |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
639 |> (fn (poly, (level, core)) =>
640 case (core, (poly, level)) of
641 ("native", (SOME poly, _)) =>
642 (case (poly, level) of
643 (Polymorphic, All_Types) =>
644 Simple_Types (First_Order, Polymorphic, All_Types)
645 | (Mangled_Monomorphic, _) =>
646 if granularity_of_type_level level = All_Vars then
647 Simple_Types (First_Order, Mangled_Monomorphic, level)
650 | _ => raise Same.SAME)
651 | ("native_higher", (SOME poly, _)) =>
652 (case (poly, level) of
653 (Polymorphic, All_Types) =>
654 Simple_Types (Higher_Order, Polymorphic, All_Types)
655 | (_, Noninf_Nonmono_Types _) => raise Same.SAME
656 | (Mangled_Monomorphic, _) =>
657 if granularity_of_type_level level = All_Vars then
658 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
661 | _ => raise Same.SAME)
662 | ("guards", (SOME poly, _)) =>
663 if poly = Mangled_Monomorphic andalso
664 granularity_of_type_level level = Ghost_Type_Arg_Vars then
668 | ("tags", (SOME poly, _)) =>
669 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
673 | ("args", (SOME poly, All_Types (* naja *))) =>
674 Guards (poly, Const_Arg_Types)
675 | ("erased", (NONE, All_Types (* naja *))) =>
676 Guards (Polymorphic, No_Types)
677 | _ => raise Same.SAME)
678 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
680 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
681 (Simple_Types (order, _, level)) =
682 Simple_Types (order, Mangled_Monomorphic, level)
683 | adjust_type_enc (THF _) type_enc = type_enc
684 | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
685 Simple_Types (First_Order, Mangled_Monomorphic, level)
686 | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) =
687 Simple_Types (First_Order, Mangled_Monomorphic, level)
688 | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
689 Simple_Types (First_Order, poly, level)
690 | adjust_type_enc format (Simple_Types (_, poly, level)) =
691 adjust_type_enc format (Guards (poly, level))
692 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
693 (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
694 | adjust_type_enc _ type_enc = type_enc
698 @{const Not} $ t1 => is_fol_term t1
699 | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t'
700 | Const (@{const_name All}, _) $ t1 => is_fol_term t1
701 | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t'
702 | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1
703 | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
704 | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
705 | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2
706 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
707 is_fol_term t1 andalso is_fol_term t2
708 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
710 fun simple_translate_lambdas do_lambdas ctxt t =
711 if is_fol_term t then
717 @{const Not} $ t1 => @{const Not} $ trans Ts t1
718 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
719 t0 $ Abs (s, T, trans (T :: Ts) t')
720 | (t0 as Const (@{const_name All}, _)) $ t1 =>
721 trans Ts (t0 $ eta_expand Ts t1 1)
722 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
723 t0 $ Abs (s, T, trans (T :: Ts) t')
724 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
725 trans Ts (t0 $ eta_expand Ts t1 1)
726 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
727 t0 $ trans Ts t1 $ trans Ts t2
728 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
729 t0 $ trans Ts t1 $ trans Ts t2
730 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
731 t0 $ trans Ts t1 $ trans Ts t2
732 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
734 t0 $ trans Ts t1 $ trans Ts t2
736 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
737 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
738 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
739 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
741 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
742 do_cheaply_conceal_lambdas Ts t1
743 $ do_cheaply_conceal_lambdas Ts t2
744 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
745 Const (lam_lifted_poly_prefix ^ serial_string (),
746 T --> fastype_of1 (T :: Ts, t))
747 | do_cheaply_conceal_lambdas _ t = t
749 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
750 fun conceal_bounds Ts t =
751 subst_bounds (map (Free o apfst concealed_bound_name)
752 (0 upto length Ts - 1 ~~ Ts), t)
753 fun reveal_bounds Ts =
754 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
755 (0 upto length Ts - 1 ~~ Ts))
757 fun do_introduce_combinators ctxt Ts t =
758 let val thy = Proof_Context.theory_of ctxt in
759 t |> conceal_bounds Ts
761 |> Meson_Clausify.introduce_combinators_in_cterm
762 |> prop_of |> Logic.dest_equals |> snd
765 (* A type variable of sort "{}" will make abstraction fail. *)
766 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
767 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
769 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
770 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
771 | constify_lifted (Free (x as (s, _))) =
772 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
773 | constify_lifted t = t
775 (* Requires bound variables not to clash with any schematic variables (as should
776 be the case right after lambda-lifting). *)
777 fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) =
778 (case try unprefix s of
781 val names = Name.make_context (map fst (Term.add_var_names t' []))
782 val (s, _) = Name.variant s names
783 in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end
787 fun lift_lams_part_1 ctxt type_enc =
788 map close_form #> rpair ctxt
789 #-> Lambda_Lifting.lift_lambdas
790 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
791 lam_lifted_poly_prefix
793 lam_lifted_mono_prefix) ^ "_a"))
794 Lambda_Lifting.is_quantifier
797 fun lift_lams_part_2 ctxt (facts, lifted) =
799 (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
801 |> pairself (map (introduce_combinators ctxt))
802 |> pairself (map constify_lifted)
803 |>> map (open_form (unprefix close_form_prefix))
804 ||> map (open_form I)
806 fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
808 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
810 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
812 fun lam T t = Abs (Name.uu, T, t)
813 val (head, args) = strip_comb t ||> rev
814 val head_T = fastype_of head
816 val arg_Ts = head_T |> binder_types |> take n |> rev
817 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
818 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
819 | intentionalize_def t = t
821 type translated_formula =
825 iformula : (name, typ, iterm) formula,
826 atomic_types : typ list}
828 fun update_iformula f ({name, stature, kind, iformula, atomic_types}
829 : translated_formula) =
830 {name = name, stature = stature, kind = kind, iformula = f iformula,
831 atomic_types = atomic_types} : translated_formula
833 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
835 fun insert_type ctxt get_T x xs =
836 let val T = get_T x in
837 if exists (type_instance ctxt T o get_T) xs then xs
838 else x :: filter_out (type_generalization ctxt T o get_T) xs
841 (* The Booleans indicate whether all type arguments should be kept. *)
842 datatype type_arg_policy =
843 Explicit_Type_Args of bool (* infer_from_term_args *) |
847 fun type_arg_policy monom_constrs type_enc s =
848 let val poly = polymorphism_of_type_enc type_enc in
849 if s = type_tag_name then
850 if poly = Mangled_Monomorphic then Mangled_Type_Args
851 else Explicit_Type_Args false
852 else case type_enc of
853 Simple_Types (_, Polymorphic, _) => Explicit_Type_Args false
854 | Tags (_, All_Types) => No_Type_Args
856 let val level = level_of_type_enc type_enc in
857 if level = No_Types orelse s = @{const_name HOL.eq} orelse
858 (s = app_op_name andalso level = Const_Arg_Types) then
860 else if poly = Mangled_Monomorphic then
862 else if member (op =) monom_constrs s andalso
863 granularity_of_type_level level = Positively_Naked_Vars then
867 (level = All_Types orelse
868 granularity_of_type_level level = Ghost_Type_Arg_Vars)
872 (* Make atoms for sorted type variables. *)
873 fun generic_add_sorts_on_type (_, []) = I
874 | generic_add_sorts_on_type ((x, i), s :: ss) =
875 generic_add_sorts_on_type ((x, i), ss)
876 #> (if s = the_single @{sort HOL.type} then
879 insert (op =) (`make_type_class s, `make_fixed_type_var x)
881 insert (op =) (`make_type_class s,
882 (make_schematic_type_var (x, i), x)))
883 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
884 | add_sorts_on_tfree _ = I
885 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
886 | add_sorts_on_tvar _ = I
888 fun type_class_formula type_enc class arg =
889 AAtom (ATerm (class, arg ::
891 Simple_Types (First_Order, Polymorphic, _) =>
892 if avoid_first_order_ghost_type_vars then [ATerm (TYPE_name, [arg])]
895 fun formulas_for_types type_enc add_sorts_on_typ Ts =
896 [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
897 |> map (fn (class, name) =>
898 type_class_formula type_enc class (ATerm (name, [])))
900 fun mk_aconns c phis =
901 let val (phis', phi') = split_last phis in
902 fold_rev (mk_aconn c) phis' phi'
904 fun mk_ahorn [] phi = phi
905 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
906 fun mk_aquant _ [] phi = phi
907 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
908 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
909 | mk_aquant q xs phi = AQuant (q, xs, phi)
911 fun close_universally add_term_vars phi =
913 fun add_formula_vars bounds (AQuant (_, xs, phi)) =
914 add_formula_vars (map fst xs @ bounds) phi
915 | add_formula_vars bounds (AConn (_, phis)) =
916 fold (add_formula_vars bounds) phis
917 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
918 in mk_aquant AForall (add_formula_vars [] phi []) phi end
920 fun add_term_vars bounds (ATerm (name as (s, _), tms)) =
921 (if is_tptp_variable s andalso
922 not (String.isPrefix tvar_prefix s) andalso
923 not (member (op =) bounds name) then
924 insert (op =) (name, NONE)
927 #> fold (add_term_vars bounds) tms
928 | add_term_vars bounds (AAbs ((name, _), tm)) =
929 add_term_vars (name :: bounds) tm
930 fun close_formula_universally phi = close_universally add_term_vars phi
932 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
933 fold (add_iterm_vars bounds) [tm1, tm2]
934 | add_iterm_vars _ (IConst _) = I
935 | add_iterm_vars bounds (IVar (name, T)) =
936 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
937 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
938 fun close_iformula_universally phi = close_universally add_iterm_vars phi
940 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
941 val fused_infinite_type = Type (fused_infinite_type_name, [])
943 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
945 fun ho_term_from_typ format type_enc =
947 fun term (Type (s, Ts)) =
948 ATerm (case (is_type_enc_higher_order type_enc, s) of
949 (true, @{type_name bool}) => `I tptp_bool_type
950 | (true, @{type_name fun}) => `I tptp_fun_type
951 | _ => if s = fused_infinite_type_name andalso
952 is_format_typed format then
953 `I tptp_individual_type
955 `make_fixed_type_const s,
957 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
958 | term (TVar (x, _)) = ATerm (tvar_name x, [])
961 fun ho_term_for_type_arg format type_enc T =
962 if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
964 (* This shouldn't clash with anything else. *)
965 val uncurried_alias_sep = "\000"
966 val mangled_type_sep = "\001"
968 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
970 fun generic_mangled_type_name f (ATerm (name, [])) = f name
971 | generic_mangled_type_name f (ATerm (name, tys)) =
972 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
974 | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
976 fun mangled_type format type_enc =
977 generic_mangled_type_name fst o ho_term_from_typ format type_enc
979 fun make_native_type s =
980 if s = tptp_bool_type orelse s = tptp_fun_type orelse
981 s = tptp_individual_type then
984 native_type_prefix ^ ascii_of s
986 fun ho_type_from_ho_term type_enc pred_sym ary =
988 fun to_mangled_atype ty =
989 AType ((make_native_type (generic_mangled_type_name fst ty),
990 generic_mangled_type_name snd ty), [])
991 fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
992 | to_poly_atype _ = raise Fail "unexpected type abstraction"
994 if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
995 else to_mangled_atype
996 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
997 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
998 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
999 | to_fo _ _ = raise Fail "unexpected type abstraction"
1000 fun to_ho (ty as ATerm ((s, _), tys)) =
1001 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
1002 | to_ho _ = raise Fail "unexpected type abstraction"
1003 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
1005 fun ho_type_from_typ format type_enc pred_sym ary =
1006 ho_type_from_ho_term type_enc pred_sym ary
1007 o ho_term_from_typ format type_enc
1009 fun aliased_uncurried ary (s, s') =
1010 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
1011 fun unaliased_uncurried (s, s') =
1012 case space_explode uncurried_alias_sep s of
1014 | [s1, s2] => (s1, unsuffix s2 s')
1015 | _ => raise Fail "ill-formed explicit application alias"
1017 fun raw_mangled_const_name type_name ty_args (s, s') =
1019 fun type_suffix f g =
1020 fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
1022 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
1023 fun mangled_const_name format type_enc =
1024 map_filter (ho_term_for_type_arg format type_enc)
1025 #> raw_mangled_const_name generic_mangled_type_name
1027 val parse_mangled_ident =
1028 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
1030 fun parse_mangled_type x =
1031 (parse_mangled_ident
1032 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
1034 and parse_mangled_types x =
1035 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
1037 fun unmangled_type s =
1038 s |> suffix ")" |> raw_explode
1039 |> Scan.finite Symbol.stopper
1040 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
1041 quote s)) parse_mangled_type))
1044 fun unmangled_const_name s =
1045 (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
1046 fun unmangled_const s =
1047 let val ss = unmangled_const_name s in
1048 (hd ss, map unmangled_type (tl ss))
1051 fun introduce_proxies_in_iterm type_enc =
1053 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
1054 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
1056 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
1057 limitation. This works in conjuction with special code in
1058 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
1060 IAbs ((`I "P", p_T),
1061 IApp (IConst (`I ho_quant, T, []),
1062 IAbs ((`I "X", x_T),
1063 IApp (IConst (`I "P", p_T, []),
1064 IConst (`I "X", x_T, [])))))
1065 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
1066 fun intro top_level args (IApp (tm1, tm2)) =
1067 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
1068 | intro top_level args (IConst (name as (s, _), T, T_args)) =
1069 (case proxify_const s of
1071 if top_level orelse is_type_enc_higher_order type_enc then
1072 case (top_level, s) of
1073 (_, "c_False") => IConst (`I tptp_false, T, [])
1074 | (_, "c_True") => IConst (`I tptp_true, T, [])
1075 | (false, "c_Not") => IConst (`I tptp_not, T, [])
1076 | (false, "c_conj") => IConst (`I tptp_and, T, [])
1077 | (false, "c_disj") => IConst (`I tptp_or, T, [])
1078 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
1079 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
1080 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
1082 if is_tptp_equal s andalso length args = 2 then
1083 IConst (`I tptp_equal, T, [])
1085 (* Use a proxy even for partially applied THF0 equality,
1086 because the LEO-II and Satallax parsers complain about not
1087 being able to infer the type of "=". *)
1088 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1089 | _ => IConst (name, T, [])
1091 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1092 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
1093 else IConst (name, T, T_args))
1094 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
1096 in intro true [] end
1098 fun mangle_type_args_in_const format type_enc (name as (s, _)) T_args =
1099 case unprefix_and_unascii const_prefix s of
1100 NONE => (name, T_args)
1102 case type_arg_policy [] type_enc (invert_const s'') of
1103 Mangled_Type_Args => (mangled_const_name format type_enc T_args name, [])
1104 | _ => (name, T_args)
1105 fun mangle_type_args_in_iterm format type_enc =
1106 if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1108 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
1109 | mangle (tm as IConst (_, _, [])) = tm
1110 | mangle (IConst (name, T, T_args)) =
1111 mangle_type_args_in_const format type_enc name T_args
1112 |> (fn (name, T_args) => IConst (name, T, T_args))
1113 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1119 fun chop_fun 0 T = ([], T)
1120 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1121 chop_fun (n - 1) ran_T |>> cons dom_T
1122 | chop_fun _ T = ([], T)
1124 fun filter_const_type_args _ _ _ [] = []
1125 | filter_const_type_args thy s ary T_args =
1127 val U = robust_const_type thy s
1128 val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
1129 val U_args = (s, U) |> robust_const_typargs thy
1132 |> map (fn (U, T) =>
1133 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
1135 handle TYPE _ => T_args
1137 fun filter_type_args_in_const _ _ _ _ _ [] = []
1138 | filter_type_args_in_const thy monom_constrs type_enc ary s T_args =
1139 case unprefix_and_unascii const_prefix s of
1141 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
1145 val s'' = invert_const s''
1146 fun filter_T_args false = T_args
1147 | filter_T_args true = filter_const_type_args thy s'' ary T_args
1149 case type_arg_policy monom_constrs type_enc s'' of
1150 Explicit_Type_Args infer_from_term_args =>
1151 filter_T_args infer_from_term_args
1152 | No_Type_Args => []
1153 | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
1155 fun filter_type_args_in_iterm thy monom_constrs type_enc =
1157 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1158 | filt ary (IConst (name as (s, _), T, T_args)) =
1159 filter_type_args_in_const thy monom_constrs type_enc ary s T_args
1160 |> (fn T_args => IConst (name, T, T_args))
1161 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1165 fun iformula_from_prop ctxt format type_enc eq_as_iff =
1167 val thy = Proof_Context.theory_of ctxt
1168 fun do_term bs t atomic_Ts =
1169 iterm_from_term thy format bs (Envir.eta_contract t)
1170 |>> (introduce_proxies_in_iterm type_enc
1171 #> mangle_type_args_in_iterm format type_enc #> AAtom)
1172 ||> union (op =) atomic_Ts
1173 fun do_quant bs q pos s T t' =
1175 val s = singleton (Name.variant_list (map fst bs)) s
1176 val universal = Option.map (q = AExists ? not) pos
1178 s |> `(case universal of
1179 SOME true => make_all_bound_var
1180 | SOME false => make_exist_bound_var
1181 | NONE => make_bound_var)
1183 do_formula ((s, (name, T)) :: bs) pos t'
1184 #>> mk_aquant q [(name, SOME T)]
1185 ##> union (op =) (atomic_types_of T)
1187 and do_conn bs c pos1 t1 pos2 t2 =
1188 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1189 and do_formula bs pos t =
1191 @{const Trueprop} $ t1 => do_formula bs pos t1
1192 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1193 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1194 do_quant bs AForall pos s T t'
1195 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1196 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1197 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1198 do_quant bs AExists pos s T t'
1199 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1200 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1201 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1202 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1203 | @{const HOL.implies} $ t1 $ t2 =>
1204 do_conn bs AImplies (Option.map not pos) t1 pos t2
1205 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1206 if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1208 in do_formula [] end
1210 fun presimplify_term ctxt t =
1211 t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
1212 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
1213 #> Meson.presimplify
1216 fun is_fun_equality (@{const_name HOL.eq},
1217 Type (_, [Type (@{type_name fun}, _), _])) = true
1218 | is_fun_equality _ = false
1220 fun extensionalize_term ctxt t =
1221 if exists_Const is_fun_equality t then
1222 let val thy = Proof_Context.theory_of ctxt in
1223 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
1224 |> prop_of |> Logic.dest_equals |> snd
1229 fun preprocess_abstractions_in_terms trans_lams facts =
1231 val (facts, lambda_ts) =
1232 facts |> map (snd o snd) |> trans_lams
1233 |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
1235 map2 (fn t => fn j =>
1236 ((lam_fact_prefix ^ Int.toString j, (Global, Spec_Eq)),
1238 lambda_ts (1 upto length lambda_ts)
1239 in (facts, lam_facts) end
1241 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1242 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1245 fun freeze (t $ u) = freeze t $ freeze u
1246 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1247 | freeze (Var ((s, i), T)) =
1248 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1250 in t |> exists_subterm is_Var t ? freeze end
1252 fun default_formula role = if role = Conjecture then @{term False} else @{term True}
1254 fun presimp_prop ctxt role t =
1256 val thy = Proof_Context.theory_of ctxt
1257 val t = t |> Envir.beta_eta_contract
1258 |> transform_elim_prop
1259 |> Object_Logic.atomize_term thy
1260 val need_trueprop = (fastype_of t = @{typ bool})
1262 t |> need_trueprop ? HOLogic.mk_Trueprop
1263 |> extensionalize_term ctxt
1264 |> presimplify_term ctxt
1265 |> HOLogic.dest_Trueprop
1267 handle TERM _ => default_formula role)
1270 fun make_formula ctxt format type_enc eq_as_iff name stature kind t =
1272 val (iformula, atomic_Ts) =
1273 iformula_from_prop ctxt format type_enc eq_as_iff
1274 (SOME (kind <> Conjecture)) t []
1275 |>> close_iformula_universally
1277 {name = name, stature = stature, kind = kind, iformula = iformula,
1278 atomic_types = atomic_Ts}
1281 fun make_fact ctxt format type_enc eq_as_iff ((name, stature), t) =
1282 case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
1283 name stature Axiom of
1284 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1285 if s = tptp_true then NONE else SOME formula
1286 | formula => SOME formula
1288 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1289 | s_not_trueprop t =
1290 if fastype_of t = @{typ bool} then s_not t
1291 else @{prop False} (* "t" is too meta *)
1293 fun make_conjecture ctxt format type_enc =
1294 map (fn ((name, stature), (kind, t)) =>
1295 t |> kind = Conjecture ? s_not_trueprop
1296 |> make_formula ctxt format type_enc (format <> CNF) name stature
1299 (** Finite and infinite type inference **)
1301 fun tvar_footprint thy s ary =
1302 (case unprefix_and_unascii const_prefix s of
1304 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1305 |> map (fn T => Term.add_tvarsT T [] |> map fst)
1309 fun ghost_type_args thy s ary =
1310 if is_tptp_equal s then
1314 val footprint = tvar_footprint thy s ary
1315 val eq = (s = @{const_name HOL.eq})
1316 fun ghosts _ [] = []
1317 | ghosts seen ((i, tvars) :: args) =
1318 ghosts (union (op =) seen tvars) args
1319 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1322 if forall null footprint then
1325 0 upto length footprint - 1 ~~ footprint
1326 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1330 type monotonicity_info =
1331 {maybe_finite_Ts : typ list,
1332 surely_finite_Ts : typ list,
1333 maybe_infinite_Ts : typ list,
1334 surely_infinite_Ts : typ list,
1335 maybe_nonmono_Ts : typ list}
1337 (* These types witness that the type classes they belong to allow infinite
1338 models and hence that any types with these type classes is monotonic. *)
1339 val known_infinite_types =
1340 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1342 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1343 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1345 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1346 dangerous because their "exhaust" properties can easily lead to unsound ATP
1347 proofs. On the other hand, all HOL infinite types can be given the same
1348 models in first-order logic (via Löwenheim-Skolem). *)
1350 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
1351 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1352 maybe_nonmono_Ts, ...}
1353 (Noninf_Nonmono_Types (strictness, grain)) T =
1354 grain = Ghost_Type_Arg_Vars orelse
1355 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1356 not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1357 (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1358 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1360 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1361 maybe_nonmono_Ts, ...}
1362 (Fin_Nonmono_Types grain) T =
1363 grain = Ghost_Type_Arg_Vars orelse
1364 (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1365 (exists (type_generalization ctxt T) surely_finite_Ts orelse
1366 (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1367 is_type_surely_finite ctxt T)))
1368 | should_encode_type _ _ _ _ = false
1370 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1371 should_guard_var () andalso should_encode_type ctxt mono level T
1372 | should_guard_type _ _ _ _ _ = false
1374 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
1375 String.isPrefix bound_var_prefix s orelse
1376 String.isPrefix all_bound_var_prefix s
1377 | is_maybe_universal_var (IVar _) = true
1378 | is_maybe_universal_var _ = false
1381 Top_Level of bool option |
1382 Eq_Arg of bool option |
1385 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1386 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1387 if granularity_of_type_level level = All_Vars then
1388 should_encode_type ctxt mono level T
1390 (case (site, is_maybe_universal_var u) of
1391 (Eq_Arg _, true) => should_encode_type ctxt mono level T
1393 | should_tag_with_type _ _ _ _ _ _ = false
1395 fun fused_type ctxt mono level =
1397 val should_encode = should_encode_type ctxt mono level
1398 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1399 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1400 fuse 0 T1 --> fuse (ary - 1) T2
1401 | fuse _ _ = raise Fail "expected function type"
1404 (** predicators and application operators **)
1407 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1410 fun default_sym_tab_entries type_enc =
1411 (make_fixed_const NONE @{const_name undefined},
1412 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1413 in_conj = false}) ::
1414 ([tptp_false, tptp_true]
1415 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1416 in_conj = false})) @
1417 ([tptp_equal, tptp_old_equal]
1418 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1420 |> not (is_type_enc_higher_order type_enc)
1421 ? cons (prefixed_predicator_name,
1422 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1425 datatype app_op_level = Incomplete_Apply | Sufficient_Apply | Full_Apply
1427 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
1429 val thy = Proof_Context.theory_of ctxt
1430 fun consider_var_ary const_T var_T max_ary =
1433 if ary = max_ary orelse type_instance ctxt var_T T orelse
1434 type_instance ctxt T var_T then
1437 iter (ary + 1) (range_type T)
1438 in iter 0 const_T end
1439 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1440 if app_op_level = Sufficient_Apply andalso
1441 (can dest_funT T orelse T = @{typ bool}) then
1443 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1444 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1445 {pred_sym = pred_sym andalso not bool_vars',
1446 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1447 max_ary = max_ary, types = types, in_conj = in_conj}
1449 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1451 if bool_vars' = bool_vars andalso
1452 pointer_eq (fun_var_Ts', fun_var_Ts) then
1455 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1459 fun add_iterm_syms conj_fact top_level tm
1460 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1461 let val (head, args) = strip_iterm_comb tm in
1463 IConst ((s, _), T, _) =>
1464 if String.isPrefix bound_var_prefix s orelse
1465 String.isPrefix all_bound_var_prefix s then
1466 add_universal_var T accum
1467 else if String.isPrefix exist_bound_var_prefix s then
1470 let val ary = length args in
1471 ((bool_vars, fun_var_Ts),
1472 case Symtab.lookup sym_tab s of
1473 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1476 pred_sym andalso top_level andalso not bool_vars
1477 val types' = types |> insert_type ctxt I T
1478 val in_conj = in_conj orelse conj_fact
1480 if app_op_level = Sufficient_Apply andalso
1481 not (pointer_eq (types', types)) then
1482 fold (consider_var_ary T) fun_var_Ts min_ary
1486 Symtab.update (s, {pred_sym = pred_sym,
1487 min_ary = Int.min (ary, min_ary),
1488 max_ary = Int.max (ary, max_ary),
1489 types = types', in_conj = in_conj})
1494 val pred_sym = top_level andalso not bool_vars
1496 case unprefix_and_unascii const_prefix s of
1498 (if String.isSubstring uncurried_alias_sep s then
1500 else case try (robust_const_ary thy
1502 o unmangled_const_name) s of
1503 SOME ary0 => Int.min (ary0, ary)
1507 case app_op_level of
1508 Incomplete_Apply => ary
1509 | Sufficient_Apply =>
1510 fold (consider_var_ary T) fun_var_Ts ary
1513 Symtab.update_new (s,
1514 {pred_sym = pred_sym, min_ary = min_ary,
1515 max_ary = ary, types = [T], in_conj = conj_fact})
1519 | IVar (_, T) => add_universal_var T accum
1520 | IAbs ((_, T), tm) =>
1521 accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
1523 |> fold (add_iterm_syms conj_fact false) args
1525 fun add_fact_syms conj_fact =
1526 K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
1528 ((false, []), Symtab.empty)
1529 |> fold (add_fact_syms true) conjs
1530 |> fold (add_fact_syms false) facts
1532 |> fold Symtab.update (default_sym_tab_entries type_enc)
1535 fun min_ary_of sym_tab s =
1536 case Symtab.lookup sym_tab s of
1537 SOME ({min_ary, ...} : sym_info) => min_ary
1539 case unprefix_and_unascii const_prefix s of
1541 let val s = s |> unmangled_const_name |> hd |> invert_const in
1542 if s = predicator_name then 1
1543 else if s = app_op_name then 2
1544 else if s = type_guard_name then 1
1549 (* True if the constant ever appears outside of the top-level position in
1550 literals, or if it appears with different arities (e.g., because of different
1551 type instantiations). If false, the constant always receives all of its
1552 arguments and is used as a predicate. *)
1553 fun is_pred_sym sym_tab s =
1554 case Symtab.lookup sym_tab s of
1555 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1556 pred_sym andalso min_ary = max_ary
1559 val app_op = `(make_fixed_const NONE) app_op_name
1560 val predicator_combconst =
1561 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1563 fun list_app head args = fold (curry (IApp o swap)) args head
1564 fun predicator tm = IApp (predicator_combconst, tm)
1566 fun mk_app_op format type_enc head arg =
1568 val head_T = ityp_of head
1569 val (arg_T, res_T) = dest_funT head_T
1571 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1572 |> mangle_type_args_in_iterm format type_enc
1573 in list_app app [head, arg] end
1575 fun firstorderize_fact thy monom_constrs format type_enc sym_tab
1578 fun do_app arg head = mk_app_op format type_enc head arg
1579 fun list_app_ops head args = fold do_app args head
1580 fun introduce_app_ops tm =
1581 let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
1583 IConst (name as (s, _), T, T_args) =>
1584 if uncurried_aliases andalso String.isPrefix const_prefix s then
1586 val ary = length args
1588 name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
1589 in list_app (IConst (name, T, T_args)) args end
1591 args |> chop (min_ary_of sym_tab s)
1592 |>> list_app head |-> list_app_ops
1593 | _ => list_app_ops head args
1595 fun introduce_predicators tm =
1596 case strip_iterm_comb tm of
1597 (IConst ((s, _), _, _), _) =>
1598 if is_pred_sym sym_tab s then tm else predicator tm
1599 | _ => predicator tm
1601 not (is_type_enc_higher_order type_enc)
1602 ? (introduce_app_ops #> introduce_predicators)
1603 #> filter_type_args_in_iterm thy monom_constrs type_enc
1604 in update_iformula (formula_map do_iterm) end
1606 (** Helper facts **)
1608 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1609 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1611 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1613 [(("COMBI", false), @{thms Meson.COMBI_def}),
1614 (("COMBK", false), @{thms Meson.COMBK_def}),
1615 (("COMBB", false), @{thms Meson.COMBB_def}),
1616 (("COMBC", false), @{thms Meson.COMBC_def}),
1617 (("COMBS", false), @{thms Meson.COMBS_def}),
1618 ((predicator_name, false), [not_ffalse, ftrue]),
1619 (("fFalse", false), [not_ffalse]),
1620 (("fFalse", true), @{thms True_or_False}),
1621 (("fTrue", false), [ftrue]),
1622 (("fTrue", true), @{thms True_or_False}),
1624 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1625 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1627 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1628 by (unfold fconj_def) fast+}),
1630 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1631 by (unfold fdisj_def) fast+}),
1632 (("fimplies", false),
1633 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1634 by (unfold fimplies_def) fast+}),
1636 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1637 However, this is done so for backward compatibility: Including the
1638 equality helpers by default in Metis breaks a few existing proofs. *)
1639 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1640 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1641 (* Partial characterization of "fAll" and "fEx". A complete characterization
1642 would require the axiom of choice for replay with Metis. *)
1643 (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
1644 (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
1645 (("If", true), @{thms if_True if_False True_or_False})]
1646 |> map (apsnd (map zero_var_indexes))
1648 fun atype_of_type_vars (Simple_Types (_, Polymorphic, _)) = SOME atype_of_types
1649 | atype_of_type_vars _ = NONE
1651 fun bound_tvars type_enc sorts Ts =
1652 (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
1653 #> mk_aquant AForall
1654 (map_filter (fn TVar (x as (s, _), _) =>
1655 SOME ((make_schematic_type_var x, s),
1656 atype_of_type_vars type_enc)
1659 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1660 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1661 else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
1662 |> mk_aquant AForall bounds
1663 |> close_formula_universally
1664 |> bound_tvars type_enc true atomic_Ts
1666 val helper_rank = default_rank
1667 val min_rank = 9 * helper_rank div 10
1668 val max_rank = 4 * min_rank
1670 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
1672 val type_tag = `(make_fixed_const NONE) type_tag_name
1674 fun type_tag_idempotence_fact format type_enc =
1676 fun var s = ATerm (`I s, [])
1677 fun tag tm = ATerm (type_tag, [var "A", tm])
1678 val tagged_var = tag (var "X")
1680 Formula (type_tag_idempotence_helper_name, Axiom,
1681 eq_formula type_enc [] [] false (tag tagged_var) tagged_var,
1682 NONE, isabelle_info format spec_eqN helper_rank)
1685 fun should_specialize_helper type_enc t =
1686 polymorphism_of_type_enc type_enc <> Polymorphic andalso
1687 level_of_type_enc type_enc <> No_Types andalso
1688 not (null (Term.hidden_polymorphism t))
1690 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1691 case unprefix_and_unascii const_prefix s of
1694 val thy = Proof_Context.theory_of ctxt
1695 val unmangled_s = mangled_s |> unmangled_const_name |> hd
1696 fun dub needs_fairly_sound j k =
1697 unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1698 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1699 (if needs_fairly_sound then typed_helper_suffix
1700 else untyped_helper_suffix)
1701 fun dub_and_inst needs_fairly_sound (th, j) =
1702 let val t = prop_of th in
1703 if should_specialize_helper type_enc t then
1704 map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
1710 |> map (fn (k, t) =>
1711 ((dub needs_fairly_sound j k, (Global, Spec_Eq)), t))
1712 val make_facts = map_filter (make_fact ctxt format type_enc false)
1713 val fairly_sound = is_type_enc_fairly_sound type_enc
1716 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1717 if helper_s <> unmangled_s orelse
1718 (needs_fairly_sound andalso not fairly_sound) then
1721 ths ~~ (1 upto length ths)
1722 |> maps (dub_and_inst needs_fairly_sound)
1726 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1727 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1730 (***************************************************************)
1731 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1732 (***************************************************************)
1734 fun set_insert (x, s) = Symtab.update (x, ()) s
1736 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1738 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1739 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1741 fun classes_of_terms get_Ts =
1742 map (map snd o get_Ts)
1743 #> List.foldl add_classes Symtab.empty
1744 #> delete_type #> Symtab.keys
1746 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1747 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1749 fun fold_type_constrs f (Type (s, Ts)) x =
1750 fold (fold_type_constrs f) Ts (f (s, x))
1751 | fold_type_constrs _ _ x = x
1753 (* Type constructors used to instantiate overloaded constants are the only ones
1755 fun add_type_constrs_in_term thy =
1757 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1758 | add (t $ u) = add t #> add u
1760 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1761 | add (Abs (_, _, u)) = add u
1765 fun type_constrs_of_terms thy ts =
1766 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1768 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1769 let val (head, args) = strip_comb t in
1770 (head |> dest_Const |> fst,
1771 fold_rev (fn t as Var ((s, _), T) =>
1772 (fn u => Abs (s, T, abstract_over (t, u)))
1773 | _ => raise Fail "expected Var") args u)
1775 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1777 fun trans_lams_from_string ctxt type_enc lam_trans =
1778 if lam_trans = no_lamsN then
1780 else if lam_trans = hide_lamsN then
1781 lift_lams ctxt type_enc ##> K []
1782 else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
1783 lift_lams ctxt type_enc
1784 else if lam_trans = combsN then
1785 map (introduce_combinators ctxt) #> rpair []
1786 else if lam_trans = combs_and_liftingN then
1787 lift_lams_part_1 ctxt type_enc
1788 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1789 #> lift_lams_part_2 ctxt
1790 else if lam_trans = combs_or_liftingN then
1791 lift_lams_part_1 ctxt type_enc
1792 ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1793 @{term "op =::bool => bool => bool"} => t
1794 | _ => introduce_combinators ctxt (intentionalize_def t))
1795 #> lift_lams_part_2 ctxt
1796 else if lam_trans = keep_lamsN then
1797 map (Envir.eta_contract) #> rpair []
1799 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1801 fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
1804 val thy = Proof_Context.theory_of ctxt
1805 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1806 val fact_ts = facts |> map snd
1807 (* Remove existing facts from the conjecture, as this can dramatically
1808 boost an ATP's performance (for some reason). *)
1811 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1812 val facts = facts |> map (apsnd (pair Axiom))
1814 map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
1815 |> map (apsnd freeze_term)
1816 |> map2 (pair o rpair (Local, General) o string_of_int)
1817 (0 upto length hyp_ts)
1818 val ((conjs, facts), lam_facts) =
1820 |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
1821 |> (if lam_trans = no_lamsN then
1825 #> preprocess_abstractions_in_terms trans_lams
1826 #>> chop (length conjs))
1827 val conjs = conjs |> make_conjecture ctxt format type_enc
1828 val (fact_names, facts) =
1830 |> map_filter (fn (name, (_, t)) =>
1831 make_fact ctxt format type_enc true (name, t)
1832 |> Option.map (pair name))
1834 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1836 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1837 val all_ts = concl_t :: hyp_ts @ fact_ts
1838 val subs = tfree_classes_of_terms all_ts
1839 val supers = tvar_classes_of_terms all_ts
1840 val tycons = type_constrs_of_terms thy all_ts
1841 val (supers, arity_clauses) =
1842 if level_of_type_enc type_enc = No_Types then ([], [])
1843 else make_arity_clauses thy tycons supers
1844 val class_rel_clauses = make_class_rel_clauses thy subs supers
1846 (fact_names |> map single, union (op =) subs supers, conjs,
1847 facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
1850 val type_guard = `(make_fixed_const NONE) type_guard_name
1852 fun type_guard_iterm format type_enc T tm =
1853 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1854 |> mangle_type_args_in_iterm format type_enc, tm)
1856 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1857 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1858 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1859 | is_var_positively_naked_in_term _ _ _ _ = true
1861 fun is_var_ghost_type_arg_in_term thy polym_constrs name pos tm accum =
1862 is_var_positively_naked_in_term name pos tm accum orelse
1864 val var = ATerm (name, [])
1865 fun is_nasty_in_term (ATerm (_, [])) = false
1866 | is_nasty_in_term (ATerm ((s, _), tms)) =
1868 val ary = length tms
1869 val polym_constr = member (op =) polym_constrs s
1870 val ghosts = ghost_type_args thy s ary
1872 exists (fn (j, tm) =>
1873 if polym_constr then
1874 member (op =) ghosts j andalso
1875 (tm = var orelse is_nasty_in_term tm)
1877 tm = var andalso member (op =) ghosts j)
1878 (0 upto ary - 1 ~~ tms)
1879 orelse (not polym_constr andalso exists is_nasty_in_term tms)
1881 | is_nasty_in_term _ = true
1882 in is_nasty_in_term tm end
1884 fun should_guard_var_in_formula thy polym_constrs level pos phi (SOME true)
1886 (case granularity_of_type_level level of
1888 | Positively_Naked_Vars =>
1889 formula_fold pos (is_var_positively_naked_in_term name) phi false
1890 | Ghost_Type_Arg_Vars =>
1891 formula_fold pos (is_var_ghost_type_arg_in_term thy polym_constrs name) phi
1893 | should_guard_var_in_formula _ _ _ _ _ _ _ = true
1895 fun always_guard_var_in_formula _ _ _ _ _ _ _ = true
1897 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
1898 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
1899 granularity_of_type_level level <> All_Vars andalso
1900 should_encode_type ctxt mono level T
1901 | should_generate_tag_bound_decl _ _ _ _ _ = false
1903 fun mk_aterm format type_enc name T_args args =
1904 ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
1906 fun do_bound_type ctxt format mono type_enc =
1908 Simple_Types (_, _, level) =>
1909 fused_type ctxt mono level 0
1910 #> ho_type_from_typ format type_enc false 0 #> SOME
1913 fun tag_with_type ctxt format mono type_enc pos T tm =
1914 IConst (type_tag, T --> T, [T])
1915 |> mangle_type_args_in_iterm format type_enc
1916 |> ho_term_from_iterm ctxt format mono type_enc pos
1917 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
1918 | _ => raise Fail "unexpected lambda-abstraction")
1919 and ho_term_from_iterm ctxt format mono type_enc =
1923 val (head, args) = strip_iterm_comb u
1926 Top_Level pos => pos
1931 IConst (name as (s, _), _, T_args) =>
1932 let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in
1933 map (term arg_site) args |> mk_aterm format type_enc name T_args
1936 map (term Elsewhere) args |> mk_aterm format type_enc name []
1937 | IAbs ((name, T), tm) =>
1938 if is_type_enc_higher_order type_enc then
1939 AAbs ((name, ho_type_from_typ format type_enc true 0 T),
1942 ATerm (("LAMBDA", "LAMBDA"), []) (*###*)
1944 raise Fail "unexpected lambda-abstraction"
1946 | IApp _ => raise Fail "impossible \"IApp\""
1949 if should_tag_with_type ctxt mono type_enc site u T then
1950 tag_with_type ctxt format mono type_enc pos T t
1954 in term o Top_Level end
1955 and formula_from_iformula ctxt polym_constrs format mono type_enc
1958 val thy = Proof_Context.theory_of ctxt
1959 val level = level_of_type_enc type_enc
1960 val do_term = ho_term_from_iterm ctxt format mono type_enc
1961 fun do_out_of_bound_type pos phi universal (name, T) =
1962 if should_guard_type ctxt mono type_enc
1963 (fn () => should_guard_var thy polym_constrs level pos phi
1964 universal name) T then
1966 |> type_guard_iterm format type_enc T
1967 |> do_term pos |> AAtom |> SOME
1968 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
1970 val var = ATerm (name, [])
1971 val tagged_var = tag_with_type ctxt format mono type_enc pos T var
1972 in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
1975 fun do_formula pos (AQuant (q, xs, phi)) =
1977 val phi = phi |> do_formula pos
1978 val universal = Option.map (q = AExists ? not) pos
1979 val do_bound_type = do_bound_type ctxt format mono type_enc
1981 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1982 | SOME T => do_bound_type T)),
1983 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1985 (fn (_, NONE) => NONE
1987 do_out_of_bound_type pos phi universal (s, T))
1991 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1992 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1995 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1996 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1997 the remote provers might care. *)
1998 fun formula_line_for_fact ctxt polym_constrs format prefix encode freshen pos
1999 mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) =
2000 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
2002 |> formula_from_iformula ctxt polym_constrs format mono type_enc
2003 should_guard_var_in_formula (if pos then SOME true else NONE)
2004 |> close_formula_universally
2005 |> bound_tvars type_enc true atomic_types,
2007 let val rank = rank j in
2009 Intro => isabelle_info format introN rank
2010 | Elim => isabelle_info format elimN rank
2011 | Simp => isabelle_info format simpN rank
2012 | Spec_Eq => isabelle_info format spec_eqN rank
2013 | _ => isabelle_info format "" rank
2017 fun formula_line_for_class_rel_clause format type_enc
2018 ({name, subclass, superclass, ...} : class_rel_clause) =
2019 let val ty_arg = ATerm (tvar_a_name, []) in
2020 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
2022 [type_class_formula type_enc subclass ty_arg,
2023 type_class_formula type_enc superclass ty_arg])
2024 |> mk_aquant AForall
2025 [(tvar_a_name, atype_of_type_vars type_enc)],
2026 NONE, isabelle_info format introN helper_rank)
2029 fun formula_from_arity_atom type_enc (class, t, args) =
2030 ATerm (t, map (fn arg => ATerm (arg, [])) args)
2031 |> type_class_formula type_enc class
2033 fun formula_line_for_arity_clause format type_enc
2034 ({name, prem_atoms, concl_atom} : arity_clause) =
2035 Formula (arity_clause_prefix ^ name, Axiom,
2036 mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
2037 (formula_from_arity_atom type_enc concl_atom)
2038 |> mk_aquant AForall
2039 (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
2040 NONE, isabelle_info format introN helper_rank)
2042 fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc
2043 ({name, kind, iformula, atomic_types, ...} : translated_formula) =
2044 Formula (conjecture_prefix ^ name, kind,
2046 |> formula_from_iformula ctxt polym_constrs format mono type_enc
2047 should_guard_var_in_formula (SOME false)
2048 |> close_formula_universally
2049 |> bound_tvars type_enc true atomic_types, NONE, [])
2051 fun formula_line_for_free_type j phi =
2052 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
2053 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
2056 fold (union (op =)) (map #atomic_types facts) []
2057 |> formulas_for_types type_enc add_sorts_on_tfree
2058 in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
2060 (** Symbol declarations **)
2062 fun decl_line_for_class order s =
2063 let val name as (s, _) = `make_type_class s in
2064 Decl (sym_decl_prefix ^ s, name,
2065 if order = First_Order then
2066 ATyAbs ([tvar_a_name],
2067 if avoid_first_order_ghost_type_vars then
2068 AFun (a_itself_atype, bool_atype)
2072 AFun (atype_of_types, bool_atype))
2075 fun decl_lines_for_classes type_enc classes =
2077 Simple_Types (order, Polymorphic, _) =>
2078 map (decl_line_for_class order) classes
2081 fun sym_decl_table_for_facts ctxt format type_enc sym_tab
2082 (conjs, facts, extra_tms) =
2084 fun add_iterm_syms tm =
2085 let val (head, args) = strip_iterm_comb tm in
2087 IConst ((s, s'), T, T_args) =>
2089 val (pred_sym, in_conj) =
2090 case Symtab.lookup sym_tab s of
2091 SOME ({pred_sym, in_conj, ...} : sym_info) =>
2093 | NONE => (false, false)
2096 Guards _ => not pred_sym
2097 | _ => true) andalso
2098 is_tptp_user_symbol s
2101 Symtab.map_default (s, [])
2102 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
2107 | IAbs (_, tm) => add_iterm_syms tm
2109 #> fold add_iterm_syms args
2111 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2112 fun add_formula_var_types (AQuant (_, xs, phi)) =
2113 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2114 #> add_formula_var_types phi
2115 | add_formula_var_types (AConn (_, phis)) =
2116 fold add_formula_var_types phis
2117 | add_formula_var_types _ = I
2119 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
2120 else fold (fact_lift add_formula_var_types) (conjs @ facts) []
2121 fun add_undefined_const T =
2124 `(make_fixed_const NONE) @{const_name undefined}
2125 |> (case type_arg_policy [] type_enc @{const_name undefined} of
2126 Mangled_Type_Args => mangled_const_name format type_enc [T]
2129 Symtab.map_default (s, [])
2130 (insert_type ctxt #3 (s', [T], T, false, 0, false))
2132 fun add_TYPE_const () =
2133 let val (s, s') = TYPE_name in
2134 Symtab.map_default (s, [])
2135 (insert_type ctxt #3
2136 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2140 |> is_type_enc_fairly_sound type_enc
2141 ? (fold (fold add_fact_syms) [conjs, facts]
2142 #> fold add_iterm_syms extra_tms
2143 #> (case type_enc of
2144 Simple_Types (First_Order, Polymorphic, _) =>
2145 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
2147 | Simple_Types _ => I
2148 | _ => fold add_undefined_const (var_types ())))
2151 (* We add "bool" in case the helper "True_or_False" is included later. *)
2152 fun default_mono level =
2153 {maybe_finite_Ts = [@{typ bool}],
2154 surely_finite_Ts = [@{typ bool}],
2155 maybe_infinite_Ts = known_infinite_types,
2156 surely_infinite_Ts =
2158 Noninf_Nonmono_Types (Strict, _) => []
2159 | _ => known_infinite_types,
2160 maybe_nonmono_Ts = [@{typ bool}]}
2162 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
2163 out with monotonicity" paper presented at CADE 2011. *)
2164 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2165 | add_iterm_mononotonicity_info ctxt level _
2166 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2167 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2168 surely_infinite_Ts, maybe_nonmono_Ts}) =
2169 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2171 Noninf_Nonmono_Types (strictness, _) =>
2172 if exists (type_instance ctxt T) surely_infinite_Ts orelse
2173 member (type_equiv ctxt) maybe_finite_Ts T then
2175 else if is_type_kind_of_surely_infinite ctxt strictness
2176 surely_infinite_Ts T then
2177 {maybe_finite_Ts = maybe_finite_Ts,
2178 surely_finite_Ts = surely_finite_Ts,
2179 maybe_infinite_Ts = maybe_infinite_Ts,
2180 surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2181 maybe_nonmono_Ts = maybe_nonmono_Ts}
2183 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2184 surely_finite_Ts = surely_finite_Ts,
2185 maybe_infinite_Ts = maybe_infinite_Ts,
2186 surely_infinite_Ts = surely_infinite_Ts,
2187 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2188 | Fin_Nonmono_Types _ =>
2189 if exists (type_instance ctxt T) surely_finite_Ts orelse
2190 member (type_equiv ctxt) maybe_infinite_Ts T then
2192 else if is_type_surely_finite ctxt T then
2193 {maybe_finite_Ts = maybe_finite_Ts,
2194 surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2195 maybe_infinite_Ts = maybe_infinite_Ts,
2196 surely_infinite_Ts = surely_infinite_Ts,
2197 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2199 {maybe_finite_Ts = maybe_finite_Ts,
2200 surely_finite_Ts = surely_finite_Ts,
2201 maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2202 surely_infinite_Ts = surely_infinite_Ts,
2203 maybe_nonmono_Ts = maybe_nonmono_Ts}
2207 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2208 fun add_fact_mononotonicity_info ctxt level
2209 ({kind, iformula, ...} : translated_formula) =
2210 formula_fold (SOME (kind <> Conjecture))
2211 (add_iterm_mononotonicity_info ctxt level) iformula
2212 fun mononotonicity_info_for_facts ctxt type_enc facts =
2213 let val level = level_of_type_enc type_enc in
2215 |> is_type_level_monotonicity_based level
2216 ? fold (add_fact_mononotonicity_info ctxt level) facts
2219 fun add_iformula_monotonic_types ctxt mono type_enc =
2221 val level = level_of_type_enc type_enc
2222 val should_encode = should_encode_type ctxt mono level
2223 fun add_type T = not (should_encode T) ? insert_type ctxt I T
2224 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2226 and add_term tm = add_type (ityp_of tm) #> add_args tm
2227 in formula_fold NONE (K add_term) end
2228 fun add_fact_monotonic_types ctxt mono type_enc =
2229 add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
2230 fun monotonic_types_for_facts ctxt mono type_enc facts =
2231 let val level = level_of_type_enc type_enc in
2232 [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
2233 is_type_level_monotonicity_based level andalso
2234 granularity_of_type_level level <> Ghost_Type_Arg_Vars)
2235 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2238 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
2239 Formula (guards_sym_formula_prefix ^
2240 ascii_of (mangled_type format type_enc T),
2242 IConst (`make_bound_var "X", T, [])
2243 |> type_guard_iterm format type_enc T
2245 |> formula_from_iformula ctxt [] format mono type_enc
2246 always_guard_var_in_formula (SOME true)
2247 |> close_formula_universally
2248 |> bound_tvars type_enc true (atomic_types_of T),
2249 NONE, isabelle_info format introN helper_rank)
2251 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
2252 let val x_var = ATerm (`make_bound_var "X", []) in
2253 Formula (tags_sym_formula_prefix ^
2254 ascii_of (mangled_type format type_enc T),
2256 eq_formula type_enc (atomic_types_of T) [] false
2257 (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
2258 NONE, isabelle_info format spec_eqN helper_rank)
2261 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
2263 Simple_Types _ => []
2265 map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
2266 | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
2268 fun decl_line_for_sym ctxt format mono type_enc s
2269 (s', T_args, T, pred_sym, ary, _) =
2271 val thy = Proof_Context.theory_of ctxt
2275 else case unprefix_and_unascii const_prefix s of
2278 val s' = s' |> invert_const
2279 val T = s' |> robust_const_type thy
2280 in (T, robust_const_typargs thy (s', T)) end
2281 | NONE => raise Fail "unexpected type arguments"
2283 Decl (sym_decl_prefix ^ s, (s, s'),
2284 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2285 |> ho_type_from_typ format type_enc pred_sym ary
2286 |> not (null T_args)
2287 ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
2290 fun honor_conj_sym_kind in_conj conj_sym_kind =
2291 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
2294 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
2295 j (s', T_args, T, _, ary, in_conj) =
2297 val thy = Proof_Context.theory_of ctxt
2298 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2299 val (arg_Ts, res_T) = chop_fun ary T
2300 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2302 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2304 if exists (curry (op =) dummyT) T_args then
2305 case level_of_type_enc type_enc of
2306 All_Types => map SOME arg_Ts
2308 if granularity_of_type_level level = Ghost_Type_Arg_Vars then
2309 let val ghosts = ghost_type_args thy s ary in
2310 map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
2311 (0 upto ary - 1) arg_Ts
2318 Formula (guards_sym_formula_prefix ^ s ^
2319 (if n > 1 then "_" ^ string_of_int j else ""), kind,
2320 IConst ((s, s'), T, T_args)
2321 |> fold (curry (IApp o swap)) bounds
2322 |> type_guard_iterm format type_enc res_T
2323 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2324 |> formula_from_iformula ctxt [] format mono type_enc
2325 always_guard_var_in_formula (SOME true)
2326 |> close_formula_universally
2327 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2329 NONE, isabelle_info format introN helper_rank)
2332 fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
2333 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2335 val thy = Proof_Context.theory_of ctxt
2336 val level = level_of_type_enc type_enc
2337 val grain = granularity_of_type_level level
2339 tags_sym_formula_prefix ^ s ^
2340 (if n > 1 then "_" ^ string_of_int j else "")
2341 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2342 val (arg_Ts, res_T) = chop_fun ary T
2343 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2344 val bounds = bound_names |> map (fn name => ATerm (name, []))
2345 val cst = mk_aterm format type_enc (s, s') T_args
2346 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
2347 val should_encode = should_encode_type ctxt mono level
2348 val tag_with = tag_with_type ctxt format mono type_enc NONE
2349 val add_formula_for_res =
2350 if should_encode res_T then
2353 if grain = Ghost_Type_Arg_Vars then
2354 let val ghosts = ghost_type_args thy s ary in
2355 map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
2356 (0 upto ary - 1 ~~ arg_Ts) bounds
2361 cons (Formula (ident_base ^ "_res", kind,
2362 eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
2363 NONE, isabelle_info format spec_eqN helper_rank))
2367 fun add_formula_for_arg k =
2368 let val arg_T = nth arg_Ts k in
2369 if should_encode arg_T then
2370 case chop k bounds of
2371 (bounds1, bound :: bounds2) =>
2372 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
2373 eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
2375 NONE, isabelle_info format spec_eqN helper_rank))
2376 | _ => raise Fail "expected nonempty tail"
2381 [] |> not pred_sym ? add_formula_for_res
2382 |> (Config.get ctxt type_tag_arguments andalso
2383 grain = Positively_Naked_Vars)
2384 ? fold add_formula_for_arg (ary - 1 downto 0)
2387 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2389 fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2391 val T = result_type_of_decl decl
2392 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2394 if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2399 | rationalize_decls _ decls = decls
2401 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
2404 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2405 | Guards (_, level) =>
2407 val decls = decls |> rationalize_decls ctxt
2408 val n = length decls
2410 decls |> filter (should_encode_type ctxt mono level
2411 o result_type_of_decl)
2413 (0 upto length decls - 1, decls)
2414 |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
2417 | Tags (_, level) =>
2418 if granularity_of_type_level level = All_Vars then
2421 let val n = length decls in
2422 (0 upto n - 1 ~~ decls)
2423 |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
2427 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
2428 mono_Ts sym_decl_tab =
2430 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2432 problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
2434 fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
2437 in mono_lines @ decl_lines end
2439 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
2441 fun do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2442 mono type_enc sym_tab0 sym_tab base_s0 types in_conj =
2446 val thy = Proof_Context.theory_of ctxt
2447 val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
2448 val base_name = base_s0 |> `(make_fixed_const (SOME format))
2449 val T = case types of [T] => T | _ => robust_const_type thy base_s0
2450 val T_args = robust_const_typargs thy (base_s0, T)
2451 val (base_name as (base_s, _), T_args) =
2452 mangle_type_args_in_const format type_enc base_name T_args
2453 val base_ary = min_ary_of sym_tab0 base_s
2454 fun do_const name = IConst (name, T, T_args)
2455 val filter_ty_args =
2456 filter_type_args_in_iterm thy monom_constrs type_enc
2458 ho_term_from_iterm ctxt format mono type_enc (SOME true)
2459 val name1 as (s1, _) =
2460 base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
2461 val name2 as (s2, _) = base_name |> aliased_uncurried ary
2462 val (arg_Ts, _) = chop_fun ary T
2464 1 upto ary |> map (`I o make_bound_var o string_of_int)
2465 val bounds = bound_names ~~ arg_Ts
2466 val (first_bounds, last_bound) =
2467 bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
2469 mk_app_op format type_enc (list_app (do_const name1) first_bounds)
2473 list_app (do_const name2) (first_bounds @ [last_bound])
2475 val do_bound_type = do_bound_type ctxt format mono type_enc
2477 eq_formula type_enc (atomic_types_of T)
2478 (map (apsnd do_bound_type) bounds) false
2479 (ho_term_of tm1) (ho_term_of tm2)
2482 [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate,
2483 NONE, isabelle_info format spec_eqN helper_rank)])
2484 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
2485 else pair_append (do_alias (ary - 1)))
2488 fun uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind mono
2489 type_enc sym_tab0 sym_tab
2490 (s, {min_ary, types, in_conj, ...} : sym_info) =
2491 case unprefix_and_unascii const_prefix s of
2493 if String.isSubstring uncurried_alias_sep mangled_s then
2495 val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
2497 do_uncurried_alias_lines_for_sym ctxt monom_constrs format conj_sym_kind
2498 mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
2503 fun uncurried_alias_lines_for_sym_table ctxt monom_constrs format conj_sym_kind
2504 mono type_enc uncurried_aliases sym_tab0 sym_tab =
2506 |> uncurried_aliases
2509 o uncurried_alias_lines_for_sym ctxt monom_constrs format
2510 conj_sym_kind mono type_enc sym_tab0 sym_tab) sym_tab
2512 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
2513 Config.get ctxt type_tag_idempotence andalso
2514 is_type_level_monotonicity_based level andalso
2515 poly <> Mangled_Monomorphic
2516 | needs_type_tag_idempotence _ _ = false
2518 val implicit_declsN = "Should-be-implicit typings"
2519 val explicit_declsN = "Explicit typings"
2520 val uncurried_alias_eqsN = "Uncurried aliases"
2521 val factsN = "Relevant facts"
2522 val class_relsN = "Class relationships"
2523 val aritiesN = "Arities"
2524 val helpersN = "Helper facts"
2525 val conjsN = "Conjectures"
2526 val free_typesN = "Type variables"
2528 (* TFF allows implicit declarations of types, function symbols, and predicate
2529 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2530 SNARK) require explicit declarations. The situation is similar for THF. *)
2532 fun default_type type_enc pred_sym s =
2537 if String.isPrefix type_const_prefix s then atype_of_types
2538 else individual_atype
2539 | _ => individual_atype
2540 fun typ 0 = if pred_sym then bool_atype else ind
2541 | typ ary = AFun (ind, typ (ary - 1))
2544 fun nary_type_constr_type n =
2545 funpow n (curry AFun atype_of_types) atype_of_types
2547 fun undeclared_syms_in_problem type_enc problem =
2549 val declared = declared_syms_in_problem problem
2550 fun do_sym (name as (s, _)) ty =
2551 if is_tptp_user_symbol s andalso not (member (op =) declared name) then
2552 AList.default (op =) (name, ty)
2555 fun do_type (AType (name, tys)) =
2556 do_sym name (fn () => nary_type_constr_type (length tys))
2558 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2559 | do_type (ATyAbs (_, ty)) = do_type ty
2560 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
2561 do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
2562 #> fold (do_term false) tms
2563 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
2564 fun do_formula (AQuant (_, xs, phi)) =
2565 fold do_type (map_filter snd xs) #> do_formula phi
2566 | do_formula (AConn (_, phis)) = fold do_formula phis
2567 | do_formula (AAtom tm) = do_term true tm
2568 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2569 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2571 fold (fold do_problem_line o snd) problem []
2572 |> filter_out (is_built_in_tptp_symbol o fst o fst)
2575 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2579 |> undeclared_syms_in_problem type_enc
2580 |> sort_wrt (fst o fst)
2581 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2582 in (implicit_declsN, decls) :: problem end
2584 fun exists_subdtype P =
2586 fun ex U = P U orelse
2587 (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false)
2590 fun is_poly_constr (_, Us) =
2591 exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us
2593 fun all_constrs_of_polymorphic_datatypes thy =
2597 #> (fn cs => exists is_poly_constr cs ? append cs))
2598 (Datatype.get_all thy) []
2599 |> List.partition is_poly_constr
2600 |> pairself (map fst)
2602 val app_op_threshold = 50
2604 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
2605 lam_trans uncurried_aliases readable_names preproc
2606 hyp_ts concl_t facts =
2608 val thy = Proof_Context.theory_of ctxt
2609 val type_enc = type_enc |> adjust_type_enc format
2610 (* Forcing explicit applications is expensive for polymorphic encodings,
2611 because it takes only one existential variable ranging over "'a => 'b" to
2612 ruin everything. Hence we do it only if there are few facts (which is
2613 normally the case for "metis" and the minimizer). *)
2615 if polymorphism_of_type_enc type_enc = Polymorphic andalso
2616 length facts >= app_op_threshold then
2621 if lam_trans = keep_lamsN andalso
2622 not (is_type_enc_higher_order type_enc) then
2623 error ("Lambda translation scheme incompatible with first-order \
2627 val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
2629 translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
2631 val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
2632 val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
2633 val (polym_constrs, monom_constrs) =
2634 all_constrs_of_polymorphic_datatypes thy
2635 |>> map (make_fixed_const (SOME format))
2636 fun firstorderize in_helper =
2637 firstorderize_fact thy monom_constrs format type_enc sym_tab0
2638 (uncurried_aliases andalso not in_helper)
2639 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
2640 val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
2642 sym_tab |> helper_facts_for_sym_table ctxt format type_enc
2643 |> map (firstorderize true)
2645 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2646 val class_decl_lines = decl_lines_for_classes type_enc classes
2647 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
2648 uncurried_alias_lines_for_sym_table ctxt monom_constrs format
2649 conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
2650 val sym_decl_lines =
2651 (conjs, helpers @ facts, uncurried_alias_eq_tms)
2652 |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2653 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2655 val num_facts = length facts
2657 map (formula_line_for_fact ctxt polym_constrs format fact_prefix
2658 ascii_of (not exporter) (not exporter) mono type_enc
2659 (rank_of_fact_num num_facts))
2660 (0 upto num_facts - 1 ~~ facts)
2662 0 upto length helpers - 1 ~~ helpers
2663 |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I
2664 false true mono type_enc (K default_rank))
2665 |> (if needs_type_tag_idempotence ctxt type_enc then
2666 cons (type_tag_idempotence_fact format type_enc)
2669 (* Reordering these might confuse the proof reconstruction code or the SPASS
2672 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2673 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
2674 (factsN, fact_lines),
2676 map (formula_line_for_class_rel_clause format type_enc)
2679 map (formula_line_for_arity_clause format type_enc) arity_clauses),
2680 (helpersN, helper_lines),
2681 (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
2683 map (formula_line_for_conjecture ctxt polym_constrs format mono
2688 CNF => ensure_cnf_problem
2689 | CNF_UEQ => filter_cnf_ueq_problem
2691 | TFF (_, TPTP_Implicit) => I
2692 | THF (_, TPTP_Implicit, _) => I
2693 | _ => declare_undeclared_syms_in_atp_problem type_enc)
2694 val (problem, pool) = problem |> nice_atp_problem readable_names format
2695 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2696 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2699 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
2700 fact_names |> Vector.fromList,
2702 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2706 val conj_weight = 0.0
2707 val hyp_weight = 0.1
2708 val fact_min_weight = 0.2
2709 val fact_max_weight = 1.0
2710 val type_info_default_weight = 0.8
2712 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2713 fun atp_problem_selection_weights problem =
2715 fun add_term_weights weight (ATerm (s, tms)) =
2716 is_tptp_user_symbol s ? Symtab.default (s, weight)
2717 #> fold (add_term_weights weight) tms
2718 | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
2719 fun add_line_weights weight (Formula (_, _, phi, _, _)) =
2720 formula_fold NONE (K (add_term_weights weight)) phi
2721 | add_line_weights _ _ = I
2722 fun add_conjectures_weights [] = I
2723 | add_conjectures_weights conjs =
2724 let val (hyps, conj) = split_last conjs in
2725 add_line_weights conj_weight conj
2726 #> fold (add_line_weights hyp_weight) hyps
2728 fun add_facts_weights facts =
2730 val num_facts = length facts
2732 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2733 / Real.fromInt num_facts
2735 map weight_of (0 upto num_facts - 1) ~~ facts
2736 |> fold (uncurry add_line_weights)
2738 val get = these o AList.lookup (op =) problem
2741 |> add_conjectures_weights (get free_typesN @ get conjsN)
2742 |> add_facts_weights (get factsN)
2743 |> fold (fold (add_line_weights type_info_default_weight) o get)
2744 [explicit_declsN, class_relsN, aritiesN]
2746 |> sort (prod_ord Real.compare string_ord o pairself swap)
2749 fun have_head_rolling (ATerm (s, args)) =
2750 (* ugly hack: may make innocent victims *)
2751 if String.isPrefix app_op_name s andalso length args = 2 then
2752 have_head_rolling (hd args) ||> append (tl args)
2755 | have_head_rolling _ = ("", [])
2757 val max_term_order_weight = 2147483647
2759 fun atp_problem_term_order_weights problem =
2761 fun add_term_deps head (ATerm (s, args)) =
2762 is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head)))
2763 #> fold (add_term_deps head) args
2764 | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
2765 fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
2766 if is_tptp_equal s then
2767 let val (head, rest) = have_head_rolling lhs in
2768 fold (add_term_deps head) (rhs :: rest)
2773 fun add_line_deps _ (Decl (_, s, ty)) =
2774 is_function_type ty ? Graph.default_node (s, ())
2775 | add_line_deps status (Formula (_, _, phi, _, info)) =
2776 if extract_isabelle_status info = SOME status then
2777 formula_fold NONE (K add_eq_deps) phi
2781 Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
2782 |> fold (fold (add_line_deps simpN) o snd) problem
2783 fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
2784 fun add_weights _ [] = I
2785 | add_weights weight syms =
2786 fold (AList.update (op =) o rpair weight) syms
2787 #> add_weights (next_weight weight)
2788 (fold (union (op =) o Graph.immediate_succs graph) syms [])
2790 [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)