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, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
14 type atp_format = ATP_Problem.atp_format
15 type formula_role = ATP_Problem.formula_role
16 type 'a problem = 'a ATP_Problem.problem
18 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
20 datatype scope = Global | Local | Assum | Chained
22 General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
24 type stature = scope * status
26 datatype strictness = Strict | Non_Strict
27 datatype uniformity = Uniform | Non_Uniform
28 datatype constr_optim = With_Constr_Optim | Without_Constr_Optim
32 Nonmono_Types of strictness * uniformity |
33 Const_Types of constr_optim |
38 val hide_lamsN : string
41 val combs_and_liftingN : string
42 val combs_or_liftingN : string
43 val lam_liftingN : string
44 val keep_lamsN : string
45 val schematic_var_prefix : string
46 val fixed_var_prefix : string
47 val tvar_prefix : string
48 val tfree_prefix : string
49 val const_prefix : string
50 val type_const_prefix : string
51 val class_prefix : string
52 val lam_lifted_prefix : string
53 val lam_lifted_mono_prefix : string
54 val lam_lifted_poly_prefix : string
55 val skolem_const_prefix : string
56 val old_skolem_const_prefix : string
57 val new_skolem_const_prefix : string
58 val combinator_prefix : string
59 val class_decl_prefix : string
60 val type_decl_prefix : string
61 val sym_decl_prefix : string
62 val class_memb_prefix : string
63 val guards_sym_formula_prefix : string
64 val tags_sym_formula_prefix : string
65 val fact_prefix : string
66 val conjecture_prefix : string
67 val helper_prefix : string
68 val subclass_prefix : string
69 val tcon_clause_prefix : string
70 val tfree_clause_prefix : string
71 val lam_fact_prefix : string
72 val typed_helper_suffix : string
73 val untyped_helper_suffix : string
74 val predicator_name : string
75 val app_op_name : string
76 val type_guard_name : string
77 val type_tag_name : string
78 val native_type_prefix : string
79 val prefixed_predicator_name : string
80 val prefixed_app_op_name : string
81 val prefixed_type_tag_name : string
82 val ascii_of : string -> string
83 val unascii_of : string -> string
84 val unprefix_and_unascii : string -> string -> string option
85 val proxy_table : (string * (string * (thm * (string * string)))) list
86 val proxify_const : string -> (string * string) option
87 val invert_const : string -> string
88 val unproxify_const : string -> string
89 val new_skolem_var_name_from_const : string -> string
90 val atp_logical_consts : string list
91 val atp_irrelevant_consts : string list
92 val atp_widely_irrelevant_consts : string list
93 val atp_schematic_consts_of : term -> typ list Symtab.table
94 val is_type_enc_higher_order : type_enc -> bool
95 val is_type_enc_polymorphic : type_enc -> bool
96 val level_of_type_enc : type_enc -> type_level
97 val is_type_enc_sound : type_enc -> bool
98 val type_enc_from_string : strictness -> string -> type_enc
99 val adjust_type_enc : atp_format -> type_enc -> type_enc
100 val is_lambda_free : term -> bool
102 connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
103 val unmangled_const : string -> string * (string, 'b) ho_term list
104 val unmangled_const_name : string -> string list
105 val helper_table : ((string * bool) * (status * thm) list) list
106 val trans_lams_from_string :
107 Proof.context -> type_enc -> string -> term list -> term list * term list
108 val string_of_status : status -> string
110 val prepare_atp_problem :
111 Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
112 -> bool -> bool -> bool -> term list -> term
113 -> ((string * stature) * term) list
114 -> string problem * string Symtab.table * (string * stature) list vector
115 * (string * term) list * int Symtab.table
116 val atp_problem_selection_weights : string problem -> (string * real) list
117 val atp_problem_term_order_info : string problem -> (string * int) list
120 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
126 datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
128 datatype scope = Global | Local | Assum | Chained
130 General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
131 type stature = scope * status
135 Higher_Order of thf_choice
136 datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
137 datatype polymorphism =
138 Type_Class_Polymorphic |
139 Raw_Polymorphic of phantom_policy |
142 datatype strictness = Strict | Non_Strict
143 datatype uniformity = Uniform | Non_Uniform
144 datatype constr_optim = With_Constr_Optim | Without_Constr_Optim
145 datatype type_level =
148 Nonmono_Types of strictness * uniformity |
149 Const_Types of constr_optim |
153 Native of order * polymorphism * type_level |
154 Guards of polymorphism * type_level |
155 Tags of polymorphism * type_level
157 (* not clear whether ATPs prefer to have their negative variables tagged *)
158 val tag_neg_vars = false
160 fun is_type_enc_native (Native _) = true
161 | is_type_enc_native _ = false
162 fun is_type_enc_higher_order (Native (Higher_Order _, _, _)) = true
163 | is_type_enc_higher_order _ = false
165 fun polymorphism_of_type_enc (Native (_, poly, _)) = poly
166 | polymorphism_of_type_enc (Guards (poly, _)) = poly
167 | polymorphism_of_type_enc (Tags (poly, _)) = poly
169 fun is_type_enc_polymorphic type_enc =
170 case polymorphism_of_type_enc type_enc of
171 Raw_Polymorphic _ => true
172 | Type_Class_Polymorphic => true
175 fun is_type_enc_mangling type_enc =
176 polymorphism_of_type_enc type_enc = Mangled_Monomorphic
178 fun level_of_type_enc (Native (_, _, level)) = level
179 | level_of_type_enc (Guards (_, level)) = level
180 | level_of_type_enc (Tags (_, level)) = level
182 fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false
183 | is_type_level_uniform Undercover_Types = false
184 | is_type_level_uniform _ = true
186 fun is_type_level_sound (Const_Types _) = false
187 | is_type_level_sound No_Types = false
188 | is_type_level_sound _ = true
189 val is_type_enc_sound = is_type_level_sound o level_of_type_enc
191 fun is_type_level_monotonicity_based (Nonmono_Types _) = true
192 | is_type_level_monotonicity_based _ = false
194 val no_lamsN = "no_lams" (* used internally; undocumented *)
195 val hide_lamsN = "hide_lams"
196 val liftingN = "lifting"
198 val combs_and_liftingN = "combs_and_lifting"
199 val combs_or_liftingN = "combs_or_lifting"
200 val keep_lamsN = "keep_lams"
201 val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *)
203 val bound_var_prefix = "B_"
204 val all_bound_var_prefix = "A_"
205 val exist_bound_var_prefix = "E_"
206 val schematic_var_prefix = "V_"
207 val fixed_var_prefix = "v_"
208 val tvar_prefix = "T_"
209 val tfree_prefix = "tf_"
210 val const_prefix = "c_"
211 val type_const_prefix = "t_"
212 val native_type_prefix = "n_"
213 val class_prefix = "cl_"
215 (* Freshness almost guaranteed! *)
216 val atp_prefix = "ATP" ^ Long_Name.separator
217 val atp_weak_prefix = "ATP:"
219 val lam_lifted_prefix = atp_weak_prefix ^ "Lam"
220 val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m"
221 val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p"
223 val skolem_const_prefix = atp_prefix ^ "Sko"
224 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
225 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
227 val combinator_prefix = "COMB"
229 val class_decl_prefix = "cl_"
230 val type_decl_prefix = "ty_"
231 val sym_decl_prefix = "sy_"
232 val class_memb_prefix = "clmb_"
233 val guards_sym_formula_prefix = "gsy_"
234 val tags_sym_formula_prefix = "tsy_"
235 val uncurried_alias_eq_prefix = "unc_"
236 val fact_prefix = "fact_"
237 val conjecture_prefix = "conj_"
238 val helper_prefix = "help_"
239 val subclass_prefix = "subcl_"
240 val tcon_clause_prefix = "tcon_"
241 val tfree_clause_prefix = "tfree_"
243 val lam_fact_prefix = "ATP.lambda_"
244 val typed_helper_suffix = "_T"
245 val untyped_helper_suffix = "_U"
247 val predicator_name = "pp"
248 val app_op_name = "aa"
249 val type_guard_name = "gg"
250 val type_tag_name = "tt"
252 val prefixed_predicator_name = const_prefix ^ predicator_name
253 val prefixed_app_op_name = const_prefix ^ app_op_name
254 val prefixed_type_tag_name = const_prefix ^ type_tag_name
256 (*Escaping of special characters.
257 Alphanumeric characters are left unchanged.
258 The character _ goes to __
259 Characters in the range ASCII space to / go to _A to _P, respectively.
260 Other characters go to _nnn where nnn is the decimal ASCII code.*)
261 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
263 fun ascii_of_char c =
264 if Char.isAlphaNum c then
266 else if c = #"_" then
268 else if #" " <= c andalso c <= #"/" then
269 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
271 (* fixed width, in case more digits follow *)
272 "_" ^ stringN_of_int 3 (Char.ord c)
274 val ascii_of = String.translate ascii_of_char
276 (** Remove ASCII armoring from names in proof files **)
278 (* We don't raise error exceptions because this code can run inside a worker
279 thread. Also, the errors are impossible. *)
282 fun un rcs [] = String.implode (rev rcs)
283 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
284 (* Three types of _ escapes: __, _A to _P, _nnn *)
285 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
286 | un rcs (#"_" :: c :: cs) =
287 if #"A" <= c andalso c<= #"P" then
288 (* translation of #" " to #"/" *)
289 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
291 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
292 case Int.fromString (String.implode digits) of
293 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
294 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
296 | un rcs (c :: cs) = un (c :: rcs) cs
297 in un [] o String.explode end
299 (* If string s has the prefix s1, return the result of deleting it,
301 fun unprefix_and_unascii s1 s =
302 if String.isPrefix s1 s then
303 SOME (unascii_of (String.extract (s, size s1, NONE)))
308 [("c_False", (@{const_name False}, (@{thm fFalse_def},
309 ("fFalse", @{const_name ATP.fFalse})))),
310 ("c_True", (@{const_name True}, (@{thm fTrue_def},
311 ("fTrue", @{const_name ATP.fTrue})))),
312 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
313 ("fNot", @{const_name ATP.fNot})))),
314 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
315 ("fconj", @{const_name ATP.fconj})))),
316 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
317 ("fdisj", @{const_name ATP.fdisj})))),
318 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
319 ("fimplies", @{const_name ATP.fimplies})))),
320 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
321 ("fequal", @{const_name ATP.fequal})))),
322 ("c_All", (@{const_name All}, (@{thm fAll_def},
323 ("fAll", @{const_name ATP.fAll})))),
324 ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
325 ("fEx", @{const_name ATP.fEx}))))]
327 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
329 (* Readable names for the more common symbolic functions. Do not mess with the
330 table unless you know what you are doing. *)
331 val const_trans_table =
332 [(@{type_name Product_Type.prod}, "prod"),
333 (@{type_name Sum_Type.sum}, "sum"),
334 (@{const_name False}, "False"),
335 (@{const_name True}, "True"),
336 (@{const_name Not}, "Not"),
337 (@{const_name conj}, "conj"),
338 (@{const_name disj}, "disj"),
339 (@{const_name implies}, "implies"),
340 (@{const_name HOL.eq}, "equal"),
341 (@{const_name All}, "All"),
342 (@{const_name Ex}, "Ex"),
343 (@{const_name If}, "If"),
344 (@{const_name Set.member}, "member"),
345 (@{const_name Meson.COMBI}, combinator_prefix ^ "I"),
346 (@{const_name Meson.COMBK}, combinator_prefix ^ "K"),
347 (@{const_name Meson.COMBB}, combinator_prefix ^ "B"),
348 (@{const_name Meson.COMBC}, combinator_prefix ^ "C"),
349 (@{const_name Meson.COMBS}, combinator_prefix ^ "S")]
351 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
353 (* Invert the table of translations between Isabelle and ATPs. *)
354 val const_trans_table_inv =
355 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
356 val const_trans_table_unprox =
358 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
360 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
361 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
364 case Symtab.lookup const_trans_table c of
368 fun ascii_of_indexname (v, 0) = ascii_of v
369 | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
371 fun make_bound_var x = bound_var_prefix ^ ascii_of x
372 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
373 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
374 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
375 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
377 fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unprefix "'" s, i)
378 fun make_tfree s = tfree_prefix ^ ascii_of (unprefix "'" s)
379 fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
381 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
383 val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
384 fun default c = const_prefix ^ lookup_const c
386 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
387 | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _))) c =
388 if c = choice_const then tptp_choice else default c
389 | make_fixed_const _ c = default c
392 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
394 fun make_class clas = class_prefix ^ ascii_of clas
396 fun new_skolem_var_name_from_const s =
397 let val ss = s |> space_explode Long_Name.separator in
398 nth ss (length ss - 2)
401 (* These are ignored anyway by the relevance filter (unless they appear in
402 higher-order places) but not by the monomorphizer. *)
403 val atp_logical_consts =
404 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
405 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
406 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
408 (* These are either simplified away by "Meson.presimplify" (most of the time) or
409 handled specially via "fFalse", "fTrue", ..., "fequal". *)
410 val atp_irrelevant_consts =
411 [@{const_name False}, @{const_name True}, @{const_name Not},
412 @{const_name conj}, @{const_name disj}, @{const_name implies},
413 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
415 val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
417 fun add_schematic_const (x as (_, T)) =
418 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
419 val add_schematic_consts_of =
420 Term.fold_aterms (fn Const (x as (s, _)) =>
421 not (member (op =) atp_widely_irrelevant_consts s)
422 ? add_schematic_const x
424 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
426 val tvar_a_str = "'a"
427 val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
428 val tvar_a = TVar tvar_a_z
429 val tvar_a_name = tvar_name tvar_a_z
430 val itself_name = `make_fixed_type_const @{type_name itself}
431 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
432 val tvar_a_atype = AType (tvar_a_name, [])
433 val a_itself_atype = AType (itself_name, [tvar_a_atype])
435 (** Definitions and functions for FOL clauses and formulas for TPTP **)
437 (** Type class membership **)
439 (* In our data structures, [] exceptionally refers to the top class, not to
442 val class_of_types = the_single @{sort type}
444 fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls
446 (* Arity of type constructor "s :: (arg1, ..., argN) res" *)
447 fun make_axiom_tcon_clause (s, name, (cl, args)) =
449 val args = args |> map normalize_classes
451 1 upto length args |> map (fn j => TVar ((tvar_a_str, j), @{sort type}))
452 in (name, args ~~ tvars, (cl, Type (s, tvars))) end
454 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
455 theory thy provided its arguments have the corresponding sorts. *)
456 fun class_pairs thy tycons cls =
458 val alg = Sign.classes_of thy
459 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
460 fun add_class tycon cl =
461 cons (cl, domain_sorts tycon cl)
462 handle Sorts.CLASS_ERROR _ => I
463 fun try_classes tycon = (tycon, fold (add_class tycon) cls [])
464 in map try_classes tycons end
466 (* Proving one (tycon, class) membership may require proving others, so
468 fun all_class_pairs _ _ [] = ([], [])
469 | all_class_pairs thy tycons cls =
471 fun maybe_insert_class s =
472 (s <> class_of_types andalso not (member (op =) cls s))
474 val pairs = class_pairs thy tycons cls
476 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
477 val (cls', pairs') = all_class_pairs thy tycons new_cls
478 in (cls' @ cls, union (op =) pairs' pairs) end
480 fun tcon_clause _ _ (_, []) = []
481 | tcon_clause seen n (tcons, (ar as (cl, _)) :: ars) =
482 if cl = class_of_types then
483 tcon_clause seen n (tcons, ars)
484 else if member (op =) seen cl then
485 (* multiple clauses for the same (tycon, cl) pair *)
486 make_axiom_tcon_clause (tcons,
487 lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n,
489 tcon_clause seen (n + 1) (tcons, ars)
491 make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl,
493 tcon_clause (cl :: seen) n (tcons, ars)
495 fun make_tcon_clauses thy tycons =
496 all_class_pairs thy tycons ##> maps (tcon_clause [] 1)
499 (** Isabelle class relations **)
501 (* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all
503 fun make_subclass_pairs thy subs supers =
505 val class_less = curry (Sorts.class_less (Sign.classes_of thy))
506 fun supers_of sub = (sub, filter (class_less sub) supers)
507 in map supers_of subs |> filter_out (null o snd) end
509 (* intermediate terms *)
511 IConst of (string * string) * typ * typ list |
512 IVar of (string * string) * typ |
513 IApp of iterm * iterm |
514 IAbs of ((string * string) * typ) * iterm
516 fun ityp_of (IConst (_, T, _)) = T
517 | ityp_of (IVar (_, T)) = T
518 | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
519 | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
521 (*gets the head of a combinator application, along with the list of arguments*)
522 fun strip_iterm_comb u =
524 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
526 in stripc (u, []) end
528 fun atomic_types_of T = fold_atyps (insert (op =)) T []
530 fun new_skolem_const_name s num_T_args =
531 [new_skolem_const_prefix, s, string_of_int num_T_args]
534 val alpha_to_beta = Logic.varifyT_global @{typ "'a => 'b"}
535 val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta
537 fun robust_const_type thy s =
538 if s = app_op_name then
539 alpha_to_beta_to_alpha_to_beta
540 else if String.isPrefix lam_lifted_prefix s then
543 (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
544 s |> Sign.the_const_type thy
546 val robust_const_ary =
548 fun ary (Type (@{type_name fun}, [_, T])) = 1 + ary T
550 in ary oo robust_const_type end
552 (* This function only makes sense if "T" is as general as possible. *)
553 fun robust_const_typargs thy (s, T) =
554 if s = app_op_name then
555 let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
556 else if String.isPrefix old_skolem_const_prefix s then
557 [] |> Term.add_tvarsT T |> rev |> map TVar
558 else if String.isPrefix lam_lifted_prefix s then
559 if String.isPrefix lam_lifted_poly_prefix s then
560 let val (T1, T2) = T |> dest_funT in [T1, T2] end
564 (s, T) |> Sign.const_typargs thy
566 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
567 Also accumulates sort infomation. *)
568 fun iterm_from_term thy type_enc bs (P $ Q) =
570 val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
571 val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
572 in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
573 | iterm_from_term thy type_enc _ (Const (c, T)) =
574 (IConst (`(make_fixed_const (SOME type_enc)) c, T,
575 robust_const_typargs thy (c, T)),
577 | iterm_from_term _ _ _ (Free (s, T)) =
578 (IConst (`make_fixed_var s, T, []), atomic_types_of T)
579 | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
580 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
582 val Ts = T |> strip_type |> swap |> op ::
583 val s' = new_skolem_const_name s (length Ts)
584 in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
586 IVar ((make_schematic_var v, s), T), atomic_types_of T)
587 | iterm_from_term _ _ bs (Bound j) =
588 nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
589 | iterm_from_term thy type_enc bs (Abs (s, T, t)) =
591 fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
593 val name = `make_bound_var s
594 val (tm, atomic_Ts) =
595 iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
596 in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
598 (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
599 val queries = ["?", "_query"]
600 val ats = ["@", "_at"]
602 fun try_unsuffixes ss s =
603 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
605 fun type_enc_from_string strictness s =
606 (case try (unprefix "tc_") s of
607 SOME s => (SOME Type_Class_Polymorphic, s)
609 case try (unprefix "poly_") s of
610 (* It's still unclear whether all TFF1 implementations will support
611 type signatures such as "!>[A : $tType] : $o", with phantom type
613 SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s)
615 case try (unprefix "raw_mono_") s of
616 SOME s => (SOME Raw_Monomorphic, s)
618 case try (unprefix "mono_") s of
619 SOME s => (SOME Mangled_Monomorphic, s)
622 case try_unsuffixes queries s of
624 (case try_unsuffixes queries s of
625 SOME s => (Nonmono_Types (strictness, Non_Uniform), s)
626 | NONE => (Nonmono_Types (strictness, Uniform), s))
628 (case try_unsuffixes ats s of
629 SOME s => (Undercover_Types, s)
630 | NONE => (All_Types, s)))
631 |> (fn (poly, (level, core)) =>
632 case (core, (poly, level)) of
633 ("native", (SOME poly, _)) =>
634 (case (poly, level) of
635 (Mangled_Monomorphic, _) =>
636 if is_type_level_uniform level then
637 Native (First_Order, Mangled_Monomorphic, level)
640 | (Raw_Monomorphic, _) => raise Same.SAME
641 | (poly, All_Types) => Native (First_Order, poly, All_Types))
642 | ("native_higher", (SOME poly, _)) =>
643 (case (poly, level) of
644 (_, Nonmono_Types _) => raise Same.SAME
645 | (_, Undercover_Types) => raise Same.SAME
646 | (Mangled_Monomorphic, _) =>
647 if is_type_level_uniform level then
648 Native (Higher_Order THF_With_Choice, Mangled_Monomorphic,
652 | (poly as Raw_Polymorphic _, All_Types) =>
653 Native (Higher_Order THF_With_Choice, poly, All_Types)
654 | _ => raise Same.SAME)
655 | ("guards", (SOME poly, _)) =>
656 if (poly = Mangled_Monomorphic andalso
657 level = Undercover_Types) orelse
658 poly = Type_Class_Polymorphic then
662 | ("tags", (SOME poly, _)) =>
663 if (poly = Mangled_Monomorphic andalso
664 level = Undercover_Types) orelse
665 poly = Type_Class_Polymorphic then
669 | ("args", (SOME poly, All_Types (* naja *))) =>
670 if poly = Type_Class_Polymorphic then raise Same.SAME
671 else Guards (poly, Const_Types Without_Constr_Optim)
672 | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) =>
673 if poly = Mangled_Monomorphic orelse
674 poly = Type_Class_Polymorphic then
677 Guards (poly, Const_Types With_Constr_Optim)
678 | ("erased", (NONE, All_Types (* naja *))) =>
679 Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
680 | _ => raise Same.SAME)
681 handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
683 fun adjust_order THF_Without_Choice (Higher_Order _) =
684 Higher_Order THF_Without_Choice
685 | adjust_order _ type_enc = type_enc
687 fun no_type_classes Type_Class_Polymorphic =
688 Raw_Polymorphic With_Phantom_Type_Vars
689 | no_type_classes poly = poly
691 fun adjust_type_enc (THF (Polymorphic, _, choice, _))
692 (Native (order, poly, level)) =
693 Native (adjust_order choice order, no_type_classes poly, level)
694 | adjust_type_enc (THF (Monomorphic, _, choice, _))
695 (Native (order, _, level)) =
696 Native (adjust_order choice order, Mangled_Monomorphic, level)
697 | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) =
698 Native (First_Order, Mangled_Monomorphic, level)
699 | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) =
700 Native (First_Order, poly, level)
701 | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
702 Native (First_Order, Mangled_Monomorphic, level)
703 | adjust_type_enc (TFF _) (Native (_, poly, level)) =
704 Native (First_Order, no_type_classes poly, level)
705 | adjust_type_enc format (Native (_, poly, level)) =
706 adjust_type_enc format (Guards (no_type_classes poly, level))
707 | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
708 (if is_type_enc_sound type_enc then Tags else Guards) stuff
709 | adjust_type_enc _ type_enc = type_enc
711 fun is_lambda_free t =
713 @{const Not} $ t1 => is_lambda_free t1
714 | Const (@{const_name All}, _) $ Abs (_, _, t') => is_lambda_free t'
715 | Const (@{const_name All}, _) $ t1 => is_lambda_free t1
716 | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_lambda_free t'
717 | Const (@{const_name Ex}, _) $ t1 => is_lambda_free t1
718 | @{const HOL.conj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
719 | @{const HOL.disj} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
720 | @{const HOL.implies} $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
721 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
722 is_lambda_free t1 andalso is_lambda_free t2
723 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)
725 fun simple_translate_lambdas do_lambdas ctxt t =
726 if is_lambda_free t then
732 @{const Not} $ t1 => @{const Not} $ trans Ts t1
733 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
734 t0 $ Abs (s, T, trans (T :: Ts) t')
735 | (t0 as Const (@{const_name All}, _)) $ t1 =>
736 trans Ts (t0 $ eta_expand Ts t1 1)
737 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
738 t0 $ Abs (s, T, trans (T :: Ts) t')
739 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
740 trans Ts (t0 $ eta_expand Ts t1 1)
741 | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
742 t0 $ trans Ts t1 $ trans Ts t2
743 | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
744 t0 $ trans Ts t1 $ trans Ts t2
745 | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
746 t0 $ trans Ts t1 $ trans Ts t2
747 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
749 t0 $ trans Ts t1 $ trans Ts t2
751 if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
752 else t |> Envir.eta_contract |> do_lambdas ctxt Ts
753 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
754 in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
756 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
757 do_cheaply_conceal_lambdas Ts t1
758 $ do_cheaply_conceal_lambdas Ts t2
759 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
760 Const (lam_lifted_poly_prefix ^ serial_string (),
761 T --> fastype_of1 (T :: Ts, t))
762 | do_cheaply_conceal_lambdas _ t = t
764 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
765 fun conceal_bounds Ts t =
766 subst_bounds (map (Free o apfst concealed_bound_name)
767 (0 upto length Ts - 1 ~~ Ts), t)
768 fun reveal_bounds Ts =
769 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
770 (0 upto length Ts - 1 ~~ Ts))
772 fun do_introduce_combinators ctxt Ts t =
773 let val thy = Proof_Context.theory_of ctxt in
774 t |> conceal_bounds Ts
776 |> Meson_Clausify.introduce_combinators_in_cterm
777 |> prop_of |> Logic.dest_equals |> snd
780 (* A type variable of sort "{}" will make abstraction fail. *)
781 handle THM _ => t |> do_cheaply_conceal_lambdas Ts
782 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
784 fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
785 | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
786 | constify_lifted (Free (x as (s, _))) =
787 (if String.isPrefix lam_lifted_prefix s then Const else Free) x
788 | constify_lifted t = t
790 fun lift_lams_part_1 ctxt type_enc =
791 map hol_close_form #> rpair ctxt
792 #-> Lambda_Lifting.lift_lambdas
793 (SOME ((if is_type_enc_polymorphic type_enc then
794 lam_lifted_poly_prefix
796 lam_lifted_mono_prefix) ^ "_a"))
797 Lambda_Lifting.is_quantifier
800 fun lift_lams_part_2 ctxt (facts, lifted) =
802 (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid
804 |> pairself (map (introduce_combinators ctxt))
805 |> pairself (map constify_lifted)
806 (* Requires bound variables not to clash with any schematic variables (as
807 should be the case right after lambda-lifting). *)
808 |>> map (hol_open_form (unprefix hol_close_form_prefix))
809 ||> map (hol_open_form I)
811 fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
813 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
815 | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
817 fun lam T t = Abs (Name.uu, T, t)
818 val (head, args) = strip_comb t ||> rev
819 val head_T = fastype_of head
821 val arg_Ts = head_T |> binder_types |> take n |> rev
822 val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
823 in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
824 | intentionalize_def t = t
830 iformula : (string * string, typ, iterm, string * string) formula,
831 atomic_types : typ list}
833 fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
834 {name = name, stature = stature, role = role, iformula = f iformula,
835 atomic_types = atomic_types} : ifact
837 fun ifact_lift f ({iformula, ...} : ifact) = f iformula
839 fun insert_type thy get_T x xs =
840 let val T = get_T x in
841 if exists (type_instance thy T o get_T) xs then xs
842 else x :: filter_out (type_generalization thy T o get_T) xs
845 fun chop_fun 0 T = ([], T)
846 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
847 chop_fun (n - 1) ran_T |>> cons dom_T
848 | chop_fun _ T = ([], T)
850 fun filter_type_args thy constrs type_enc s ary T_args =
851 let val poly = polymorphism_of_type_enc type_enc in
852 if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
854 else case type_enc of
855 Native (_, Raw_Polymorphic _, _) => T_args
856 | Native (_, Type_Class_Polymorphic, _) => T_args
859 fun gen_type_args _ _ [] = []
860 | gen_type_args keep strip_ty T_args =
862 val U = robust_const_type thy s
863 val (binder_Us, body_U) = strip_ty U
864 val in_U_vars = fold Term.add_tvarsT binder_Us []
865 val out_U_vars = Term.add_tvarsT body_U []
866 fun filt (U_var, T) =
867 if keep (member (op =) in_U_vars U_var,
868 member (op =) out_U_vars U_var) then
872 val U_args = (s, U) |> robust_const_typargs thy
873 in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
874 handle TYPE _ => T_args
875 val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary)
876 val constr_infer_type_args = gen_type_args fst strip_type
877 val level = level_of_type_enc type_enc
879 if level = No_Types orelse s = @{const_name HOL.eq} orelse
880 (case level of Const_Types _ => s = app_op_name | _ => false) then
882 else if poly = Mangled_Monomorphic then
884 else if level = All_Types then
886 Guards _ => noninfer_type_args T_args
888 else if level = Undercover_Types then
889 noninfer_type_args T_args
890 else if member (op =) constrs s andalso
891 level <> Const_Types Without_Constr_Optim then
892 constr_infer_type_args T_args
898 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
899 val fused_infinite_type = Type (fused_infinite_type_name, [])
901 fun raw_ho_type_from_typ type_enc =
903 fun term (Type (s, Ts)) =
904 AType (case (is_type_enc_higher_order type_enc, s) of
905 (true, @{type_name bool}) => `I tptp_bool_type
906 | (true, @{type_name fun}) => `I tptp_fun_type
907 | _ => if s = fused_infinite_type_name andalso
908 is_type_enc_native type_enc then
909 `I tptp_individual_type
911 `make_fixed_type_const s,
913 | term (TFree (s, _)) = AType (`make_tfree s, [])
914 | term (TVar z) = AType (tvar_name z, [])
917 fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
918 | ho_term_from_ho_type _ = raise Fail "unexpected type"
920 fun ho_type_for_type_arg type_enc T =
921 if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T)
923 (* This shouldn't clash with anything else. *)
924 val uncurried_alias_sep = "\000"
925 val mangled_type_sep = "\001"
927 val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
929 fun generic_mangled_type_name f (AType (name, [])) = f name
930 | generic_mangled_type_name f (AType (name, tys)) =
931 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
933 | generic_mangled_type_name _ _ = raise Fail "unexpected type"
935 fun mangled_type type_enc =
936 generic_mangled_type_name fst o raw_ho_type_from_typ type_enc
938 fun make_native_type s =
939 if s = tptp_bool_type orelse s = tptp_fun_type orelse
940 s = tptp_individual_type then
943 native_type_prefix ^ ascii_of s
945 fun native_ho_type_from_raw_ho_type type_enc pred_sym ary =
947 fun to_mangled_atype ty =
948 AType ((make_native_type (generic_mangled_type_name fst ty),
949 generic_mangled_type_name snd ty), [])
950 fun to_poly_atype (AType (name, tys)) =
951 AType (name, map to_poly_atype tys)
952 | to_poly_atype _ = raise Fail "unexpected type"
954 if is_type_enc_polymorphic type_enc then to_poly_atype
955 else to_mangled_atype
956 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
957 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
958 | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
959 | to_fo _ _ = raise Fail "unexpected type"
960 fun to_ho (ty as AType ((s, _), tys)) =
961 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
962 | to_ho _ = raise Fail "unexpected type"
963 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
965 fun native_ho_type_from_typ type_enc pred_sym ary =
966 native_ho_type_from_raw_ho_type type_enc pred_sym ary
967 o raw_ho_type_from_typ type_enc
969 (* Make atoms for sorted type variables. *)
970 fun generic_add_sorts_on_type _ [] = I
971 | generic_add_sorts_on_type T (s :: ss) =
972 generic_add_sorts_on_type T ss
973 #> (if s = the_single @{sort type} then I else insert (op =) (s, T))
974 fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
975 | add_sorts_on_tfree _ = I
976 fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
977 | add_sorts_on_tvar _ = I
979 fun process_type_args type_enc T_args =
980 if is_type_enc_native type_enc then
981 (map (native_ho_type_from_typ type_enc false 0) T_args, [])
983 ([], map_filter (Option.map ho_term_from_ho_type
984 o ho_type_for_type_arg type_enc) T_args)
986 fun class_atom type_enc (cl, T) =
988 val cl = `make_class cl
989 val (ty_args, tm_args) = process_type_args type_enc [T]
993 Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
994 [ATerm ((TYPE_name, ty_args), [])]
996 in AAtom (ATerm ((cl, ty_args), tm_args)) end
998 fun class_atoms type_enc (cls, T) =
999 map (fn cl => class_atom type_enc (cl, T)) cls
1001 fun class_membs_for_types type_enc add_sorts_on_typ Ts =
1002 [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso
1003 level_of_type_enc type_enc <> No_Types)
1004 ? fold add_sorts_on_typ Ts
1006 fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c))
1008 fun mk_ahorn [] phi = phi
1009 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
1011 fun mk_aquant _ [] phi = phi
1012 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
1013 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
1014 | mk_aquant q xs phi = AQuant (q, xs, phi)
1016 fun mk_atyquant _ [] phi = phi
1017 | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
1018 if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
1019 | mk_atyquant q xs phi = ATyQuant (q, xs, phi)
1021 fun close_universally add_term_vars phi =
1023 fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
1024 add_formula_vars bounds phi
1025 | add_formula_vars bounds (AQuant (_, xs, phi)) =
1026 add_formula_vars (map fst xs @ bounds) phi
1027 | add_formula_vars bounds (AConn (_, phis)) =
1028 fold (add_formula_vars bounds) phis
1029 | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
1030 in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end
1032 fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
1033 (if is_tptp_variable s andalso
1034 not (String.isPrefix tvar_prefix s) andalso
1035 not (member (op =) bounds name) then
1036 insert (op =) (name, NONE)
1039 #> fold (add_term_vars bounds) tms
1040 | add_term_vars bounds (AAbs (((name, _), tm), args)) =
1041 add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
1043 fun close_formula_universally phi = close_universally add_term_vars phi
1045 fun add_iterm_vars bounds (IApp (tm1, tm2)) =
1046 fold (add_iterm_vars bounds) [tm1, tm2]
1047 | add_iterm_vars _ (IConst _) = I
1048 | add_iterm_vars bounds (IVar (name, T)) =
1049 not (member (op =) bounds name) ? insert (op =) (name, SOME T)
1050 | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
1052 fun aliased_uncurried ary (s, s') =
1053 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
1054 fun unaliased_uncurried (s, s') =
1055 case space_explode uncurried_alias_sep s of
1057 | [s1, s2] => (s1, unsuffix s2 s')
1058 | _ => raise Fail "ill-formed explicit application alias"
1060 fun raw_mangled_const_name type_name ty_args (s, s') =
1062 fun type_suffix f g =
1063 fold_rev (curry (op ^) o g o prefix mangled_type_sep o type_name f)
1065 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
1066 fun mangled_const_name type_enc =
1067 map_filter (ho_type_for_type_arg type_enc)
1068 #> raw_mangled_const_name generic_mangled_type_name
1070 val parse_mangled_ident =
1071 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
1073 fun parse_mangled_type x =
1074 (parse_mangled_ident
1075 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
1076 [] >> (ATerm o apfst (rpair []))) x
1077 and parse_mangled_types x =
1078 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
1080 fun unmangled_type s =
1081 s |> suffix ")" |> raw_explode
1082 |> Scan.finite Symbol.stopper
1083 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
1084 quote s)) parse_mangled_type))
1087 fun unmangled_const_name s =
1088 (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep
1089 fun unmangled_const s =
1090 let val ss = unmangled_const_name s in
1091 (hd ss, map unmangled_type (tl ss))
1094 fun introduce_proxies_in_iterm type_enc =
1096 fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
1097 | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
1099 (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
1100 limitation. This works in conjuction with special code in
1101 "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
1103 IAbs ((`I "P", p_T),
1104 IApp (IConst (`I ho_quant, T, []),
1105 IAbs ((`I "X", x_T),
1106 IApp (IConst (`I "P", p_T, []),
1107 IConst (`I "X", x_T, [])))))
1108 | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
1109 fun intro top_level args (IApp (tm1, tm2)) =
1110 IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
1111 | intro top_level args (IConst (name as (s, _), T, T_args)) =
1112 (case proxify_const s of
1114 if top_level orelse is_type_enc_higher_order type_enc then
1115 case (top_level, s) of
1116 (_, "c_False") => IConst (`I tptp_false, T, [])
1117 | (_, "c_True") => IConst (`I tptp_true, T, [])
1118 | (false, "c_Not") => IConst (`I tptp_not, T, [])
1119 | (false, "c_conj") => IConst (`I tptp_and, T, [])
1120 | (false, "c_disj") => IConst (`I tptp_or, T, [])
1121 | (false, "c_implies") => IConst (`I tptp_implies, T, [])
1122 | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
1123 | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
1125 if is_tptp_equal s then
1126 if length args = 2 then
1127 IConst (`I tptp_equal, T, [])
1129 (* Eta-expand partially applied THF equality, because the
1130 LEO-II and Satallax parsers complain about not being able to
1131 infer the type of "=". *)
1132 let val i_T = domain_type T in
1133 IAbs ((`I "Y", i_T),
1134 IAbs ((`I "Z", i_T),
1135 IApp (IApp (IConst (`I tptp_equal, T, []),
1136 IConst (`I "Y", i_T, [])),
1137 IConst (`I "Z", i_T, []))))
1140 IConst (name, T, [])
1141 | _ => IConst (name, T, [])
1143 IConst (proxy_base |>> prefix const_prefix, T, T_args)
1144 | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
1145 else IConst (name, T, T_args))
1146 | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
1148 in intro true [] end
1150 fun mangle_type_args_in_const type_enc (name as (s, _)) T_args =
1151 if String.isPrefix const_prefix s andalso is_type_enc_mangling type_enc then
1152 (mangled_const_name type_enc T_args name, [])
1155 fun mangle_type_args_in_iterm type_enc =
1156 if is_type_enc_mangling type_enc then
1158 fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
1159 | mangle (tm as IConst (_, _, [])) = tm
1160 | mangle (IConst (name, T, T_args)) =
1161 mangle_type_args_in_const type_enc name T_args
1162 |> (fn (name, T_args) => IConst (name, T, T_args))
1163 | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
1169 fun filter_type_args_in_const _ _ _ _ _ [] = []
1170 | filter_type_args_in_const thy constrs type_enc ary s T_args =
1171 case unprefix_and_unascii const_prefix s of
1173 if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then []
1176 filter_type_args thy constrs type_enc (invert_const s'') ary T_args
1177 fun filter_type_args_in_iterm thy constrs type_enc =
1179 fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
1180 | filt ary (IConst (name as (s, _), T, T_args)) =
1181 filter_type_args_in_const thy constrs type_enc ary s T_args
1182 |> (fn T_args => IConst (name, T, T_args))
1183 | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
1187 fun iformula_from_prop ctxt type_enc iff_for_eq =
1189 val thy = Proof_Context.theory_of ctxt
1190 fun do_term bs t atomic_Ts =
1191 iterm_from_term thy type_enc bs (Envir.eta_contract t)
1192 |>> (introduce_proxies_in_iterm type_enc
1193 #> mangle_type_args_in_iterm type_enc #> AAtom)
1194 ||> union (op =) atomic_Ts
1195 fun do_quant bs q pos s T t' =
1197 val s = singleton (Name.variant_list (map fst bs)) s
1198 val universal = Option.map (q = AExists ? not) pos
1200 s |> `(case universal of
1201 SOME true => make_all_bound_var
1202 | SOME false => make_exist_bound_var
1203 | NONE => make_bound_var)
1205 do_formula ((s, (name, T)) :: bs) pos t'
1206 #>> mk_aquant q [(name, SOME T)]
1207 ##> union (op =) (atomic_types_of T)
1209 and do_conn bs c pos1 t1 pos2 t2 =
1210 do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
1211 and do_formula bs pos t =
1213 @{const Trueprop} $ t1 => do_formula bs pos t1
1214 | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
1215 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
1216 do_quant bs AForall pos s T t'
1217 | (t0 as Const (@{const_name All}, _)) $ t1 =>
1218 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1219 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
1220 do_quant bs AExists pos s T t'
1221 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1222 do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
1223 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
1224 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
1225 | @{const HOL.implies} $ t1 $ t2 =>
1226 do_conn bs AImplies (Option.map not pos) t1 pos t2
1227 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
1228 if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
1230 in do_formula [] end
1232 fun presimplify_term thy t =
1233 if exists_Const (member (op =) Meson.presimplified_consts o fst) t then
1234 t |> Skip_Proof.make_thm thy
1235 |> Meson.presimplify
1240 fun preprocess_abstractions_in_terms trans_lams facts =
1242 val (facts, lambda_ts) =
1243 facts |> map (snd o snd) |> trans_lams
1244 |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
1246 map2 (fn t => fn j =>
1247 ((lam_fact_prefix ^ Int.toString j,
1248 (Global, Non_Rec_Def)), (Axiom, t)))
1249 lambda_ts (1 upto length lambda_ts)
1250 in (facts, lam_facts) end
1252 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
1253 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
1256 fun freeze (t $ u) = freeze t $ freeze u
1257 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
1258 | freeze (Var ((s, i), T)) =
1259 Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
1261 in t |> exists_subterm is_Var t ? freeze end
1263 fun presimp_prop ctxt type_enc t =
1265 val thy = Proof_Context.theory_of ctxt
1266 val t = t |> Envir.beta_eta_contract
1267 |> transform_elim_prop
1268 |> Object_Logic.atomize_term thy
1269 val need_trueprop = (fastype_of t = @{typ bool})
1270 val is_ho = is_type_enc_higher_order type_enc
1272 t |> need_trueprop ? HOLogic.mk_Trueprop
1273 |> (if is_ho then unextensionalize_def
1274 else cong_extensionalize_term thy #> abs_extensionalize_term ctxt)
1275 |> presimplify_term thy
1276 |> HOLogic.dest_Trueprop
1278 handle TERM _ => @{const True}
1280 (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
1281 for technical reasons. *)
1282 fun should_use_iff_for_eq CNF _ = false
1283 | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
1284 | should_use_iff_for_eq _ _ = true
1286 fun make_formula ctxt format type_enc iff_for_eq name stature role t =
1288 val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
1289 val (iformula, atomic_Ts) =
1290 iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
1292 |>> close_universally add_iterm_vars
1294 {name = name, stature = stature, role = role, iformula = iformula,
1295 atomic_types = atomic_Ts}
1298 fun is_format_with_defs (THF (_, _, _, THF_With_Defs)) = true
1299 | is_format_with_defs _ = false
1301 fun make_fact ctxt format type_enc iff_for_eq
1302 ((name, stature as (_, status)), t) =
1305 if is_format_with_defs format andalso status = Non_Rec_Def andalso
1306 is_legitimate_tptp_def t then
1311 case t |> make_formula ctxt format type_enc iff_for_eq name stature role of
1312 formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
1313 if s = tptp_true then NONE else SOME formula
1314 | formula => SOME formula
1317 fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
1318 | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
1319 | s_not_prop t = @{const "==>"} $ t $ @{prop False}
1321 fun make_conjecture ctxt format type_enc =
1322 map (fn ((name, stature), (role, t)) =>
1324 (* FIXME: The commented-out code is a hack to get decent performance
1325 out of LEO-II on the TPTP THF benchmarks. *)
1327 if (* is_format_with_defs format andalso *)
1328 role <> Conjecture andalso is_legitimate_tptp_def t then
1333 t |> role = Conjecture ? s_not
1334 |> make_formula ctxt format type_enc true name stature role
1337 (** Finite and infinite type inference **)
1339 fun tvar_footprint thy s ary =
1340 (case unprefix_and_unascii const_prefix s of
1342 let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in
1343 s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
1349 fun type_arg_cover thy pos s ary =
1350 if is_tptp_equal s then
1351 if pos = SOME false then [] else 0 upto ary - 1
1354 val footprint = tvar_footprint thy s ary
1355 val eq = (s = @{const_name HOL.eq})
1357 | cover seen ((i, tvars) :: args) =
1358 cover (union (op =) seen tvars) args
1359 |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars)
1362 if forall null footprint then
1365 0 upto length footprint - 1 ~~ footprint
1366 |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
1370 type monotonicity_info =
1371 {maybe_finite_Ts : typ list,
1372 surely_infinite_Ts : typ list,
1373 maybe_nonmono_Ts : typ list}
1375 (* These types witness that the type classes they belong to allow infinite
1376 models and hence that any types with these type classes is monotonic. *)
1377 val known_infinite_types =
1378 [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
1380 fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
1381 strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
1383 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1384 dangerous because their "exhaust" properties can easily lead to unsound ATP
1385 proofs. On the other hand, all HOL infinite types can be given the same
1386 models in first-order logic (via Loewenheim-Skolem). *)
1388 fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1390 (Nonmono_Types (strictness, _)) T =
1391 let val thy = Proof_Context.theory_of ctxt in
1392 (exists (type_intersect thy T) maybe_nonmono_Ts andalso
1393 not (exists (type_instance thy T) surely_infinite_Ts orelse
1394 (not (member (type_equiv thy) maybe_finite_Ts T) andalso
1395 is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1398 | should_encode_type _ _ level _ =
1399 (level = All_Types orelse level = Undercover_Types)
1401 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1402 should_guard_var () andalso should_encode_type ctxt mono level T
1403 | should_guard_type _ _ _ _ _ = false
1405 fun is_maybe_universal_name s =
1406 String.isPrefix bound_var_prefix s orelse
1407 String.isPrefix all_bound_var_prefix s
1409 fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s
1410 | is_maybe_universal_var (IVar _) = true
1411 | is_maybe_universal_var _ = false
1414 Top_Level of bool option |
1415 Eq_Arg of bool option |
1416 Arg of string * int * int |
1419 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1420 | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
1421 let val thy = Proof_Context.theory_of ctxt in
1423 Nonmono_Types (_, Non_Uniform) =>
1424 (case (site, is_maybe_universal_var u) of
1425 (Eq_Arg pos, true) =>
1426 (pos <> SOME false orelse tag_neg_vars) andalso
1427 should_encode_type ctxt mono level T
1429 | Undercover_Types =>
1430 (case (site, is_maybe_universal_var u) of
1431 (Eq_Arg pos, true) => pos <> SOME false
1432 | (Arg (s, j, ary), true) =>
1433 member (op =) (type_arg_cover thy NONE s ary) j
1435 | _ => should_encode_type ctxt mono level T
1437 | should_tag_with_type _ _ _ _ _ _ = false
1439 fun fused_type ctxt mono level =
1441 val should_encode = should_encode_type ctxt mono level
1442 fun fuse 0 T = if should_encode T then T else fused_infinite_type
1443 | fuse ary (Type (@{type_name fun}, [T1, T2])) =
1444 fuse 0 T1 --> fuse (ary - 1) T2
1445 | fuse _ _ = raise Fail "expected function type"
1448 (** predicators and application operators **)
1451 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
1454 fun default_sym_tab_entries type_enc =
1455 (make_fixed_const NONE @{const_name undefined},
1456 {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
1457 in_conj = false}) ::
1458 ([tptp_false, tptp_true]
1459 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
1460 in_conj = false})) @
1461 ([tptp_equal, tptp_old_equal]
1462 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
1464 |> not (is_type_enc_higher_order type_enc)
1465 ? cons (prefixed_predicator_name,
1466 {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
1469 datatype app_op_level =
1472 Sufficient_App_Op_And_Predicator |
1473 Full_App_Op_And_Predicator
1475 fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact =
1477 val thy = Proof_Context.theory_of ctxt
1478 fun consider_var_ary const_T var_T max_ary =
1481 if ary = max_ary orelse type_instance thy var_T T orelse
1482 type_instance thy T var_T then
1485 iter (ary + 1) (range_type T)
1486 in iter 0 const_T end
1487 fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1488 if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse
1489 (app_op_level = Sufficient_App_Op_And_Predicator andalso
1490 (can dest_funT T orelse T = @{typ bool})) then
1494 (app_op_level = Sufficient_App_Op_And_Predicator andalso
1495 body_type T = @{typ bool})
1496 fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
1497 {pred_sym = pred_sym andalso not bool_vars',
1498 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1499 max_ary = max_ary, types = types, in_conj = in_conj}
1501 fun_var_Ts |> can dest_funT T ? insert_type thy I T
1503 if bool_vars' = bool_vars andalso
1504 pointer_eq (fun_var_Ts', fun_var_Ts) then
1507 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
1511 fun add_iterm_syms top_level tm
1512 (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1513 let val (head, args) = strip_iterm_comb tm in
1515 IConst ((s, _), T, _) =>
1516 if is_maybe_universal_name s then
1517 add_universal_var T accum
1518 else if String.isPrefix exist_bound_var_prefix s then
1521 let val ary = length args in
1522 ((bool_vars, fun_var_Ts),
1523 case Symtab.lookup sym_tab s of
1524 SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
1527 pred_sym andalso top_level andalso not bool_vars
1528 val types' = types |> insert_type thy I T
1529 val in_conj = in_conj orelse conj_fact
1531 if (app_op_level = Sufficient_App_Op orelse
1532 app_op_level = Sufficient_App_Op_And_Predicator)
1533 andalso not (pointer_eq (types', types)) then
1534 fold (consider_var_ary T) fun_var_Ts min_ary
1538 Symtab.update (s, {pred_sym = pred_sym,
1539 min_ary = Int.min (ary, min_ary),
1540 max_ary = Int.max (ary, max_ary),
1541 types = types', in_conj = in_conj})
1546 val pred_sym = top_level andalso not bool_vars
1548 case unprefix_and_unascii const_prefix s of
1550 (if String.isSubstring uncurried_alias_sep s then
1552 else case try (robust_const_ary thy
1554 o unmangled_const_name) s of
1555 SOME ary0 => Int.min (ary0, ary)
1559 case app_op_level of
1561 | Full_App_Op_And_Predicator => 0
1562 | _ => fold (consider_var_ary T) fun_var_Ts ary
1564 Symtab.update_new (s,
1565 {pred_sym = pred_sym, min_ary = min_ary,
1566 max_ary = ary, types = [T], in_conj = conj_fact})
1570 | IVar (_, T) => add_universal_var T accum
1571 | IAbs ((_, T), tm) =>
1572 accum |> add_universal_var T |> add_iterm_syms false tm
1574 |> fold (add_iterm_syms false) args
1576 in add_iterm_syms end
1578 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
1580 fun add_iterm_syms conj_fact =
1581 add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
1582 fun add_fact_syms conj_fact =
1583 ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact)))
1585 ((false, []), Symtab.empty)
1586 |> fold (add_fact_syms true) conjs
1587 |> fold (add_fact_syms false) facts
1588 ||> fold Symtab.update (default_sym_tab_entries type_enc)
1591 fun min_ary_of sym_tab s =
1592 case Symtab.lookup sym_tab s of
1593 SOME ({min_ary, ...} : sym_info) => min_ary
1595 case unprefix_and_unascii const_prefix s of
1597 let val s = s |> unmangled_const_name |> hd |> invert_const in
1598 if s = predicator_name then 1
1599 else if s = app_op_name then 2
1600 else if s = type_guard_name then 1
1605 (* True if the constant ever appears outside of the top-level position in
1606 literals, or if it appears with different arities (e.g., because of different
1607 type instantiations). If false, the constant always receives all of its
1608 arguments and is used as a predicate. *)
1609 fun is_pred_sym sym_tab s =
1610 case Symtab.lookup sym_tab s of
1611 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1612 pred_sym andalso min_ary = max_ary
1616 IConst ((const_prefix ^ "fTrue", @{const_name ATP.fTrue}), @{typ bool}, [])
1617 val predicator_iconst =
1618 IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
1620 fun predicatify completish tm =
1622 IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm),
1625 IApp (predicator_iconst, tm)
1627 val app_op = `(make_fixed_const NONE) app_op_name
1629 fun list_app head args = fold (curry (IApp o swap)) args head
1631 fun mk_app_op type_enc head arg =
1633 val head_T = ityp_of head
1634 val (arg_T, res_T) = dest_funT head_T
1636 IConst (app_op, head_T --> head_T, [arg_T, res_T])
1637 |> mangle_type_args_in_iterm type_enc
1638 in list_app app [head, arg] end
1640 fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases
1643 fun do_app arg head = mk_app_op type_enc head arg
1644 fun list_app_ops head args = fold do_app args head
1645 fun introduce_app_ops tm =
1646 let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in
1648 IConst (name as (s, _), T, T_args) =>
1649 if uncurried_aliases andalso String.isPrefix const_prefix s then
1651 val ary = length args
1653 name |> ary > min_ary_of sym_tab s ? aliased_uncurried ary
1654 in list_app (IConst (name, T, T_args)) args end
1656 args |> chop (min_ary_of sym_tab s)
1657 |>> list_app head |-> list_app_ops
1658 | _ => list_app_ops head args
1660 fun introduce_predicators tm =
1661 case strip_iterm_comb tm of
1662 (IConst ((s, _), _, _), _) =>
1663 if is_pred_sym sym_tab s then tm else predicatify completish tm
1664 | _ => predicatify completish tm
1666 not (is_type_enc_higher_order type_enc)
1667 ? (introduce_app_ops #> introduce_predicators)
1668 #> filter_type_args_in_iterm thy constrs type_enc
1669 in update_iformula (formula_map do_iterm) end
1671 (** Helper facts **)
1673 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
1674 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
1676 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1677 val base_helper_table =
1678 [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]),
1679 (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]),
1680 (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]),
1681 (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]),
1682 (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]),
1683 ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]),
1684 (("fFalse", false), [(General, not_ffalse)]),
1685 (("fFalse", true), [(General, @{thm True_or_False})]),
1686 (("fTrue", false), [(General, ftrue)]),
1687 (("fTrue", true), [(General, @{thm True_or_False})]),
1689 [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}),
1690 (General, @{thm True_or_False})])]
1695 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1696 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
1697 |> map (pair Non_Rec_Def)),
1699 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1700 by (unfold fconj_def) fast+}
1701 |> map (pair General)),
1703 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1704 by (unfold fdisj_def) fast+}
1705 |> map (pair General)),
1706 (("fimplies", false),
1707 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1708 by (unfold fimplies_def) fast+}
1709 |> map (pair General)),
1711 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1712 However, this is done so for backward compatibility: Including the
1713 equality helpers by default in Metis breaks a few existing proofs. *)
1714 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1715 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}
1716 |> map (pair General)),
1717 (* Partial characterization of "fAll" and "fEx". A complete characterization
1718 would require the axiom of choice for replay with Metis. *)
1720 [(General, @{lemma "~ fAll P | P x" by (auto simp: fAll_def)})]),
1722 [(General, @{lemma "~ P x | fEx P" by (auto simp: fEx_def)})])]
1723 |> map (apsnd (map (apsnd zero_var_indexes)))
1725 val completish_helper_table =
1727 [((predicator_name, true),
1728 @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)),
1729 ((app_op_name, true),
1730 [(General, @{lemma "EX x. ~ f x = g x | f = g" by blast})]),
1732 @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
1734 @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)),
1735 (("fimplies", false),
1736 @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws}
1737 |> map (pair Non_Rec_Def)),
1739 (@{thms fequal_table} |> map (pair Non_Rec_Def)) @
1740 (@{thms fequal_laws} |> map (pair General))),
1742 @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)),
1744 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))]
1745 |> map (apsnd (map (apsnd zero_var_indexes)))
1747 fun bound_tvars type_enc sorts Ts =
1748 case filter is_TVar Ts of
1751 (sorts ? mk_ahorn (Ts |> class_membs_for_types type_enc add_sorts_on_tvar
1752 |> map (class_atom type_enc)))
1753 #> (case type_enc of
1754 Native (_, poly, _) =>
1756 (map (fn TVar (z as (_, S)) =>
1757 (AType (tvar_name z, []),
1758 if poly = Type_Class_Polymorphic then
1759 map (`make_class) (normalize_classes S)
1763 mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))
1765 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
1766 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
1767 else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
1768 |> mk_aquant AForall bounds
1769 |> close_formula_universally
1770 |> bound_tvars type_enc true atomic_Ts
1772 val helper_rank = default_rank
1773 val min_rank = 9 * helper_rank div 10
1774 val max_rank = 4 * min_rank
1776 fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n
1778 val type_tag = `(make_fixed_const NONE) type_tag_name
1780 fun could_specialize_helpers type_enc =
1781 not (is_type_enc_polymorphic type_enc) andalso
1782 level_of_type_enc type_enc <> No_Types
1783 fun should_specialize_helper type_enc t =
1784 could_specialize_helpers type_enc andalso
1785 not (null (Term.hidden_polymorphism t))
1787 fun add_helper_facts_for_sym ctxt format type_enc completish
1788 (s, {types, ...} : sym_info) =
1789 case unprefix_and_unascii const_prefix s of
1792 val thy = Proof_Context.theory_of ctxt
1793 val unmangled_s = mangled_s |> unmangled_const_name |> hd
1794 fun dub needs_sound j k =
1795 ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
1796 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1797 (if needs_sound then typed_helper_suffix else untyped_helper_suffix)
1798 fun specialize_helper t T =
1799 if unmangled_s = app_op_name then
1802 Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty
1803 in monomorphic_term tyenv t end
1805 specialize_type thy (invert_const unmangled_s, T) t
1806 fun dub_and_inst needs_sound ((status, t), j) =
1807 (if should_specialize_helper type_enc t then
1808 map_filter (try (specialize_helper t)) types
1812 |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t))
1813 val make_facts = map_filter (make_fact ctxt format type_enc false)
1814 val sound = is_type_enc_sound type_enc
1815 val could_specialize = could_specialize_helpers type_enc
1817 fold (fn ((helper_s, needs_sound), ths) =>
1818 if (needs_sound andalso not sound) orelse
1819 (helper_s <> unmangled_s andalso
1820 (not completish orelse could_specialize)) then
1823 ths ~~ (1 upto length ths)
1824 |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
1826 |> union (op = o pairself #iformula))
1827 (if completish then completish_helper_table else helper_table)
1830 fun helper_facts_for_sym_table ctxt format type_enc completish sym_tab =
1831 Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc completish)
1834 (***************************************************************)
1835 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1836 (***************************************************************)
1838 fun set_insert (x, s) = Symtab.update (x, ()) s
1840 fun add_classes (cls, cset) = List.foldl set_insert cset (flat cls)
1842 fun classes_of_terms get_Ts =
1843 map (map snd o get_Ts)
1844 #> List.foldl add_classes Symtab.empty #> Symtab.delete_safe class_of_types
1847 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
1848 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
1850 fun fold_type_constrs f (Type (s, Ts)) x =
1851 fold (fold_type_constrs f) Ts (f (s, x))
1852 | fold_type_constrs _ _ x = x
1854 (* Type constructors used to instantiate overloaded constants are the only ones
1856 fun add_type_constrs_in_term thy =
1858 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1859 | add (t $ u) = add t #> add u
1861 x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
1862 | add (Abs (_, _, u)) = add u
1866 fun type_constrs_of_terms thy ts =
1867 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1869 fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
1870 let val (head, args) = strip_comb t in
1871 (head |> dest_Const |> fst,
1872 fold_rev (fn t as Var ((s, _), T) =>
1873 (fn u => Abs (s, T, abstract_over (t, u)))
1874 | _ => raise Fail "expected \"Var\"") args u)
1876 | extract_lambda_def _ = raise Fail "malformed lifted lambda"
1878 fun trans_lams_from_string ctxt type_enc lam_trans =
1879 if lam_trans = no_lamsN then
1881 else if lam_trans = hide_lamsN then
1882 lift_lams ctxt type_enc ##> K []
1883 else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
1884 lift_lams ctxt type_enc
1885 else if lam_trans = combsN then
1886 map (introduce_combinators ctxt) #> rpair []
1887 else if lam_trans = combs_and_liftingN then
1888 lift_lams_part_1 ctxt type_enc
1889 ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
1890 #> lift_lams_part_2 ctxt
1891 else if lam_trans = combs_or_liftingN then
1892 lift_lams_part_1 ctxt type_enc
1893 ##> map (fn t => case head_of (strip_qnt_body @{const_name All} t) of
1894 @{term "op =::bool => bool => bool"} => t
1895 | _ => introduce_combinators ctxt (intentionalize_def t))
1896 #> lift_lams_part_2 ctxt
1897 else if lam_trans = keep_lamsN then
1898 map (Envir.eta_contract) #> rpair []
1900 error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
1902 val pull_and_reorder_definitions =
1904 fun add_consts (IApp (t, u)) = fold add_consts [t, u]
1905 | add_consts (IAbs (_, t)) = add_consts t
1906 | add_consts (IConst (name, _, _)) = insert (op =) name
1907 | add_consts (IVar _) = I
1908 fun consts_of_hs l_or_r ({iformula, ...} : ifact) =
1910 AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) []
1912 (* Quadratic, but usually OK. *)
1913 fun reorder [] [] = []
1914 | reorder (fact :: skipped) [] =
1915 fact :: reorder [] skipped (* break cycle *)
1916 | reorder skipped (fact :: facts) =
1917 let val rhs_consts = consts_of_hs snd fact in
1918 if exists (exists (exists (member (op =) rhs_consts)
1919 o consts_of_hs fst)) [skipped, facts] then
1920 reorder (fact :: skipped) facts
1922 fact :: reorder [] (facts @ skipped)
1924 in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
1926 fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts
1929 val thy = Proof_Context.theory_of ctxt
1930 val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
1931 val fact_ts = facts |> map snd
1932 (* Remove existing facts from the conjecture, as this can dramatically
1933 boost an ATP's performance (for some reason). *)
1936 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1937 val facts = facts |> map (apsnd (pair Axiom))
1939 map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
1940 |> map (apsnd freeze_term)
1941 |> map2 (pair o rpair (Local, General) o string_of_int)
1942 (0 upto length hyp_ts)
1943 val ((conjs, facts), lam_facts) =
1945 |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
1946 |> (if lam_trans = no_lamsN then
1950 #> preprocess_abstractions_in_terms trans_lams
1951 #>> chop (length conjs))
1953 conjs |> make_conjecture ctxt format type_enc
1954 |> pull_and_reorder_definitions
1956 facts |> map_filter (fn (name, (_, t)) =>
1957 make_fact ctxt format type_enc true (name, t))
1958 |> pull_and_reorder_definitions
1960 facts |> map (fn {name, stature, ...} : ifact => (name, stature))
1961 val lifted = lam_facts |> map (extract_lambda_def o snd o snd)
1963 lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
1964 val all_ts = concl_t :: hyp_ts @ fact_ts
1965 val subs = tfree_classes_of_terms all_ts
1966 val supers = tvar_classes_of_terms all_ts
1967 val tycons = type_constrs_of_terms thy all_ts
1968 val (supers, tcon_clauses) =
1969 if level_of_type_enc type_enc = No_Types then ([], [])
1970 else make_tcon_clauses thy tycons supers
1971 val subclass_pairs = make_subclass_pairs thy subs supers
1973 (fact_names |> map single, union (op =) subs supers, conjs,
1974 facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
1977 val type_guard = `(make_fixed_const NONE) type_guard_name
1979 fun type_guard_iterm type_enc T tm =
1980 IApp (IConst (type_guard, T --> @{typ bool}, [T])
1981 |> mangle_type_args_in_iterm type_enc, tm)
1983 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1984 | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum =
1986 (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
1987 | is_var_positively_naked_in_term _ _ _ _ = true
1989 fun is_var_undercover_in_term thy name pos tm accum =
1992 val var = ATerm ((name, []), [])
1993 fun is_undercover (ATerm (_, [])) = false
1994 | is_undercover (ATerm (((s, _), _), tms)) =
1996 val ary = length tms
1997 val cover = type_arg_cover thy pos s ary
1999 exists (fn (j, tm) => tm = var andalso member (op =) cover j)
2000 (0 upto ary - 1 ~~ tms) orelse
2001 exists is_undercover tms
2003 | is_undercover _ = true
2004 in is_undercover tm end
2006 fun should_guard_var_in_formula thy level pos phi (SOME true) name =
2009 | Undercover_Types =>
2010 formula_fold pos (is_var_undercover_in_term thy name) phi false
2011 | Nonmono_Types (_, Uniform) => true
2012 | Nonmono_Types (_, Non_Uniform) =>
2013 formula_fold pos (is_var_positively_naked_in_term name) phi false
2015 | should_guard_var_in_formula _ _ _ _ _ _ = true
2017 fun always_guard_var_in_formula _ _ _ _ _ _ = true
2019 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
2020 | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
2021 not (is_type_level_uniform level) andalso
2022 should_encode_type ctxt mono level T
2023 | should_generate_tag_bound_decl _ _ _ _ _ = false
2025 fun mk_aterm type_enc name T_args args =
2026 let val (ty_args, tm_args) = process_type_args type_enc T_args in
2027 ATerm ((name, ty_args), tm_args @ args)
2030 fun do_bound_type ctxt mono type_enc =
2032 Native (_, _, level) =>
2033 fused_type ctxt mono level 0 #> native_ho_type_from_typ type_enc false 0
2037 fun tag_with_type ctxt mono type_enc pos T tm =
2038 IConst (type_tag, T --> T, [T])
2039 |> mangle_type_args_in_iterm type_enc
2040 |> ho_term_from_iterm ctxt mono type_enc pos
2041 |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
2042 | _ => raise Fail "unexpected lambda-abstraction")
2043 and ho_term_from_iterm ctxt mono type_enc pos =
2047 val (head, args) = strip_iterm_comb u
2050 Top_Level pos => pos
2056 IConst (name as (s, _), _, T_args) =>
2058 val ary = length args
2060 if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
2062 map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
2063 |> mk_aterm type_enc name T_args
2066 map (term Elsewhere) args |> mk_aterm type_enc name []
2067 | IAbs ((name, T), tm) =>
2068 if is_type_enc_higher_order type_enc then
2069 AAbs (((name, native_ho_type_from_typ type_enc true 0 T), (* FIXME? why "true"? *)
2070 term Elsewhere tm), map (term Elsewhere) args)
2072 raise Fail "unexpected lambda-abstraction"
2073 | IApp _ => raise Fail "impossible \"IApp\""
2074 val tag = should_tag_with_type ctxt mono type_enc site u T
2075 in t |> tag ? tag_with_type ctxt mono type_enc pos T end
2076 in term (Top_Level pos) end
2077 and formula_from_iformula ctxt mono type_enc should_guard_var =
2079 val thy = Proof_Context.theory_of ctxt
2080 val level = level_of_type_enc type_enc
2081 val do_term = ho_term_from_iterm ctxt mono type_enc
2082 fun do_out_of_bound_type pos phi universal (name, T) =
2083 if should_guard_type ctxt mono type_enc
2084 (fn () => should_guard_var thy level pos phi universal name) T then
2086 |> type_guard_iterm type_enc T
2087 |> do_term pos |> AAtom |> SOME
2088 else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
2090 val var = ATerm ((name, []), [])
2091 val tagged_var = tag_with_type ctxt mono type_enc pos T var
2092 in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
2095 fun do_formula pos (ATyQuant (q, xs, phi)) =
2096 ATyQuant (q, map (apfst (native_ho_type_from_typ type_enc false 0)) xs,
2098 | do_formula pos (AQuant (q, xs, phi)) =
2100 val phi = phi |> do_formula pos
2101 val universal = Option.map (q = AExists ? not) pos
2102 val do_bound_type = do_bound_type ctxt mono type_enc
2104 AQuant (q, xs |> map (apsnd (fn NONE => NONE
2105 | SOME T => do_bound_type T)),
2106 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
2108 (fn (_, NONE) => NONE
2110 do_out_of_bound_type pos phi universal (s, T))
2114 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
2115 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
2118 fun string_of_status General = ""
2119 | string_of_status Induction = inductionN
2120 | string_of_status Intro = introN
2121 | string_of_status Inductive = inductiveN
2122 | string_of_status Elim = elimN
2123 | string_of_status Simp = simpN
2124 | string_of_status Non_Rec_Def = non_rec_defN
2125 | string_of_status Rec_Def = rec_defN
2127 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
2128 of monomorphization). The TPTP explicitly forbids name clashes, and some of
2129 the remote provers might care. *)
2130 fun line_for_fact ctxt prefix encode alt freshen pos mono type_enc rank
2131 (j, {name, stature = (_, status), role, iformula, atomic_types}) =
2132 Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
2133 encode name, alt name),
2136 |> formula_from_iformula ctxt mono type_enc
2137 should_guard_var_in_formula (if pos then SOME true else NONE)
2138 |> close_formula_universally
2139 |> bound_tvars type_enc true atomic_types,
2140 NONE, isabelle_info (string_of_status status) (rank j))
2142 fun lines_for_subclass type_enc sub super =
2143 Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
2145 [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
2146 |> bound_tvars type_enc false [tvar_a],
2147 NONE, isabelle_info inductiveN helper_rank)
2149 fun lines_for_subclass_pair type_enc (sub, supers) =
2150 if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
2151 [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
2152 map (`make_class) supers)]
2154 map (lines_for_subclass type_enc sub) supers
2156 fun line_for_tcon_clause type_enc (name, prems, (cl, T)) =
2157 if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
2158 Class_Memb (class_memb_prefix ^ name,
2160 (T |> dest_TVar |> tvar_name, map (`make_class) cls))
2162 native_ho_type_from_typ type_enc false 0 T, `make_class cl)
2164 Formula ((tcon_clause_prefix ^ name, ""), Axiom,
2165 mk_ahorn (maps (class_atoms type_enc) prems)
2166 (class_atom type_enc (cl, T))
2167 |> bound_tvars type_enc true (snd (dest_Type T)),
2168 NONE, isabelle_info inductiveN helper_rank)
2170 fun line_for_conjecture ctxt mono type_enc
2171 ({name, role, iformula, atomic_types, ...} : ifact) =
2172 Formula ((conjecture_prefix ^ name, ""), role,
2174 |> formula_from_iformula ctxt mono type_enc
2175 should_guard_var_in_formula (SOME false)
2176 |> close_formula_universally
2177 |> bound_tvars type_enc true atomic_types, NONE, [])
2179 fun lines_for_free_types type_enc (facts : ifact list) =
2180 if is_type_enc_polymorphic type_enc then
2183 (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
2184 fun line j (cl, T) =
2185 if type_classes then
2186 Class_Memb (class_memb_prefix ^ string_of_int j, [],
2187 native_ho_type_from_typ type_enc false 0 T,
2190 Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
2191 class_atom type_enc (cl, T), NONE, [])
2193 fold (union (op =)) (map #atomic_types facts) []
2194 |> class_membs_for_types type_enc add_sorts_on_tfree
2195 in map2 line (0 upto length membs - 1) membs end
2199 (** Symbol declarations **)
2201 fun decl_line_for_class phantoms s =
2202 let val name as (s, _) = `make_class s in
2203 Sym_Decl (sym_decl_prefix ^ s, name,
2205 if phantoms = Without_Phantom_Type_Vars then
2206 AFun (a_itself_atype, bool_atype)
2211 fun decl_lines_for_classes type_enc classes =
2213 Native (_, Raw_Polymorphic phantoms, _) =>
2214 map (decl_line_for_class phantoms) classes
2217 fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
2219 fun add_iterm_syms tm =
2220 let val (head, args) = strip_iterm_comb tm in
2222 IConst ((s, s'), T, T_args) =>
2224 val (pred_sym, in_conj) =
2225 case Symtab.lookup sym_tab s of
2226 SOME ({pred_sym, in_conj, ...} : sym_info) =>
2228 | NONE => (false, false)
2231 Guards _ => not pred_sym
2232 | _ => true) andalso
2233 is_tptp_user_symbol s
2236 Symtab.map_default (s, [])
2237 (insert_type thy #3 (s', T_args, T, pred_sym, length args,
2242 | IAbs (_, tm) => add_iterm_syms tm
2244 #> fold add_iterm_syms args
2246 val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms))
2247 fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
2248 | add_formula_var_types (AQuant (_, xs, phi)) =
2249 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
2250 #> add_formula_var_types phi
2251 | add_formula_var_types (AConn (_, phis)) =
2252 fold add_formula_var_types phis
2253 | add_formula_var_types _ = I
2255 if is_type_enc_polymorphic type_enc then [tvar_a]
2256 else fold (ifact_lift add_formula_var_types) (conjs @ facts) []
2257 fun add_undefined_const T =
2259 (* FIXME: make sure type arguments are filtered / clean up code *)
2261 `(make_fixed_const NONE) @{const_name undefined}
2262 |> (is_type_enc_mangling type_enc ? mangled_const_name type_enc [T])
2264 Symtab.map_default (s, [])
2265 (insert_type thy #3 (s', [T], T, false, 0, false))
2267 fun add_TYPE_const () =
2268 let val (s, s') = TYPE_name in
2269 Symtab.map_default (s, [])
2271 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2275 |> is_type_enc_sound type_enc
2276 ? (fold (fold add_fact_syms) [conjs, facts]
2277 #> fold add_iterm_syms extra_tms
2278 #> (case type_enc of
2279 Native (First_Order, Raw_Polymorphic phantoms, _) =>
2280 phantoms = Without_Phantom_Type_Vars ? add_TYPE_const ()
2282 | _ => fold add_undefined_const (var_types ())))
2285 (* We add "bool" in case the helper "True_or_False" is included later. *)
2286 fun default_mono level completish =
2287 {maybe_finite_Ts = [@{typ bool}],
2288 surely_infinite_Ts =
2290 Nonmono_Types (Strict, _) => []
2291 | _ => known_infinite_types,
2292 maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
2294 (* This inference is described in section 4 of Blanchette et al., "Encoding
2295 monomorphic and polymorphic types", TACAS 2013. *)
2296 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
2297 | add_iterm_mononotonicity_info ctxt level _
2298 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2299 (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) =
2300 let val thy = Proof_Context.theory_of ctxt in
2301 if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2303 Nonmono_Types (strictness, _) =>
2304 if exists (type_instance thy T) surely_infinite_Ts orelse
2305 member (type_equiv thy) maybe_finite_Ts T then
2307 else if is_type_kind_of_surely_infinite ctxt strictness
2308 surely_infinite_Ts T then
2309 {maybe_finite_Ts = maybe_finite_Ts,
2310 surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
2311 maybe_nonmono_Ts = maybe_nonmono_Ts}
2313 {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
2314 surely_infinite_Ts = surely_infinite_Ts,
2315 maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
2320 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2321 fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
2322 formula_fold (SOME (role <> Conjecture))
2323 (add_iterm_mononotonicity_info ctxt level) iformula
2324 fun mononotonicity_info_for_facts ctxt type_enc completish facts =
2325 let val level = level_of_type_enc type_enc in
2326 default_mono level completish
2327 |> is_type_level_monotonicity_based level
2328 ? fold (add_fact_mononotonicity_info ctxt level) facts
2331 fun add_iformula_monotonic_types ctxt mono type_enc =
2333 val thy = Proof_Context.theory_of ctxt
2334 val level = level_of_type_enc type_enc
2335 val should_encode = should_encode_type ctxt mono level
2336 fun add_type T = not (should_encode T) ? insert_type thy I T
2337 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2339 and add_term tm = add_type (ityp_of tm) #> add_args tm
2340 in formula_fold NONE (K add_term) end
2342 fun add_fact_monotonic_types ctxt mono type_enc =
2343 ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
2345 fun monotonic_types_for_facts ctxt mono type_enc facts =
2346 let val level = level_of_type_enc type_enc in
2347 [] |> (is_type_enc_polymorphic type_enc andalso
2348 is_type_level_monotonicity_based level)
2349 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
2352 fun line_for_guards_mono_type ctxt mono type_enc T =
2353 Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
2355 IConst (`make_bound_var "X", T, [])
2356 |> type_guard_iterm type_enc T
2358 |> formula_from_iformula ctxt mono type_enc
2359 always_guard_var_in_formula (SOME true)
2360 |> close_formula_universally
2361 |> bound_tvars type_enc true (atomic_types_of T),
2362 NONE, isabelle_info inductiveN helper_rank)
2364 fun line_for_tags_mono_type ctxt mono type_enc T =
2365 let val x_var = ATerm ((`make_bound_var "X", []), []) in
2366 Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
2368 eq_formula type_enc (atomic_types_of T) [] false
2369 (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
2370 NONE, isabelle_info non_rec_defN helper_rank)
2373 fun lines_for_mono_types ctxt mono type_enc Ts =
2376 | Guards _ => map (line_for_guards_mono_type ctxt mono type_enc) Ts
2377 | Tags _ => map (line_for_tags_mono_type ctxt mono type_enc) Ts
2379 fun decl_line_for_sym ctxt mono type_enc s
2380 (s', T_args, T, pred_sym, ary, _) =
2382 val thy = Proof_Context.theory_of ctxt
2386 else case unprefix_and_unascii const_prefix s of
2389 val s' = s' |> invert_const
2390 val T = s' |> robust_const_type thy
2391 in (T, robust_const_typargs thy (s', T)) end
2392 | NONE => raise Fail "unexpected type arguments"
2394 Sym_Decl (sym_decl_prefix ^ s, (s, s'),
2395 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
2396 |> native_ho_type_from_typ type_enc pred_sym ary
2397 |> not (null T_args)
2398 ? curry APi (map (tvar_name o dest_TVar) T_args))
2401 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
2403 fun line_for_guards_sym_decl ctxt mono type_enc n s j
2404 (s', T_args, T, _, ary, in_conj) =
2406 val thy = Proof_Context.theory_of ctxt
2407 val (role, maybe_negate) = honor_conj_sym_role in_conj
2408 val (arg_Ts, res_T) = chop_fun ary T
2409 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2411 bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
2413 case level_of_type_enc type_enc of
2414 All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
2415 | Undercover_Types =>
2416 let val cover = type_arg_cover thy NONE s ary in
2417 map2 (fn j => if member (op =) cover j then SOME else K NONE)
2418 (0 upto ary - 1) arg_Ts
2420 | _ => replicate ary NONE
2422 Formula ((guards_sym_formula_prefix ^ s ^
2423 (if n > 1 then "_" ^ string_of_int j else ""), ""),
2425 IConst ((s, s'), T, T_args)
2426 |> fold (curry (IApp o swap)) bounds
2427 |> type_guard_iterm type_enc res_T
2428 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
2429 |> formula_from_iformula ctxt mono type_enc
2430 always_guard_var_in_formula (SOME true)
2431 |> close_formula_universally
2432 |> bound_tvars type_enc (n > 1) (atomic_types_of T)
2434 NONE, isabelle_info inductiveN helper_rank)
2437 fun lines_for_tags_sym_decl ctxt mono type_enc n s
2438 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
2440 val thy = Proof_Context.theory_of ctxt
2441 val level = level_of_type_enc type_enc
2443 tags_sym_formula_prefix ^ s ^
2444 (if n > 1 then "_" ^ string_of_int j else "")
2445 val (role, maybe_negate) = honor_conj_sym_role in_conj
2446 val (arg_Ts, res_T) = chop_fun ary T
2447 val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
2448 val bounds = bound_names |> map (fn name => ATerm ((name, []), []))
2449 val cst = mk_aterm type_enc (s, s') T_args
2450 val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
2451 val tag_with = tag_with_type ctxt mono type_enc NONE
2453 [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
2454 isabelle_info non_rec_defN helper_rank)]
2456 if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
2458 else if level = Undercover_Types then
2460 val cover = type_arg_cover thy NONE s ary
2461 fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
2462 val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
2463 in formula (cst bounds) end
2465 formula (cst bounds)
2468 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2470 fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
2472 val T = result_type_of_decl decl
2473 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2475 if forall (type_generalization thy T o result_type_of_decl) decls' then
2480 | rationalize_decls _ decls = decls
2482 fun lines_for_sym_decls ctxt mono type_enc (s, decls) =
2484 Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)]
2485 | Guards (_, level) =>
2487 val thy = Proof_Context.theory_of ctxt
2488 val decls = decls |> rationalize_decls thy
2489 val n = length decls
2491 decls |> filter (should_encode_type ctxt mono level
2492 o result_type_of_decl)
2494 (0 upto length decls - 1, decls)
2495 |-> map2 (line_for_guards_sym_decl ctxt mono type_enc n s)
2497 | Tags (_, level) =>
2498 if is_type_level_uniform level then
2501 let val n = length decls in
2502 (0 upto n - 1 ~~ decls)
2503 |> maps (lines_for_tags_sym_decl ctxt mono type_enc n s)
2506 fun lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
2508 val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
2509 val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts
2510 val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms
2511 in mono_lines @ decl_lines end
2513 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
2515 fun do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab
2516 base_s0 types in_conj =
2520 val thy = Proof_Context.theory_of ctxt
2521 val (role, maybe_negate) = honor_conj_sym_role in_conj
2522 val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
2523 val T = case types of [T] => T | _ => robust_const_type thy base_s0
2524 val T_args = robust_const_typargs thy (base_s0, T)
2525 val (base_name as (base_s, _), T_args) =
2526 mangle_type_args_in_const type_enc base_name T_args
2527 val base_ary = min_ary_of sym_tab0 base_s
2528 fun do_const name = IConst (name, T, T_args)
2529 val filter_ty_args = filter_type_args_in_iterm thy constrs type_enc
2530 val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
2531 val name1 as (s1, _) =
2532 base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
2533 val name2 as (s2, _) = base_name |> aliased_uncurried ary
2534 val (arg_Ts, _) = chop_fun ary T
2536 1 upto ary |> map (`I o make_bound_var o string_of_int)
2537 val bounds = bound_names ~~ arg_Ts
2538 val (first_bounds, last_bound) =
2539 bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last
2541 mk_app_op type_enc (list_app (do_const name1) first_bounds) last_bound
2544 list_app (do_const name2) (first_bounds @ [last_bound])
2546 val do_bound_type = do_bound_type ctxt mono type_enc
2548 eq_formula type_enc (atomic_types_of T)
2549 (map (apsnd do_bound_type) bounds) false
2550 (ho_term_of tm1) (ho_term_of tm2)
2553 [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role,
2554 eq |> maybe_negate, NONE,
2555 isabelle_info non_rec_defN helper_rank)])
2556 |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
2557 else pair_append (do_alias (ary - 1)))
2560 fun uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
2561 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
2562 case unprefix_and_unascii const_prefix s of
2564 if String.isSubstring uncurried_alias_sep mangled_s then
2566 val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
2568 do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
2569 sym_tab base_s0 types in_conj min_ary
2574 fun uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
2575 uncurried_aliases sym_tab0 sym_tab =
2577 |> uncurried_aliases
2580 o uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
2583 val implicit_declsN = "Should-be-implicit typings"
2584 val explicit_declsN = "Explicit typings"
2585 val uncurried_alias_eqsN = "Uncurried aliases"
2586 val factsN = "Relevant facts"
2587 val subclassesN = "Subclasses"
2588 val tconsN = "Type constructors"
2589 val helpersN = "Helper facts"
2590 val conjsN = "Conjectures"
2591 val free_typesN = "Free types"
2593 (* TFF allows implicit declarations of types, function symbols, and predicate
2594 symbols (with "$i" as the type of individuals), but some provers (e.g.,
2595 SNARK) require explicit declarations. The situation is similar for THF. *)
2597 fun default_type pred_sym =
2599 fun typ 0 0 = if pred_sym then bool_atype else individual_atype
2600 | typ 0 tm_ary = AFun (individual_atype, typ 0 (tm_ary - 1))
2601 | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
2604 fun undeclared_in_problem problem =
2606 fun do_sym (name as (s, _)) value =
2607 if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
2608 fun do_class name = apfst (apfst (do_sym name ()))
2609 fun do_type (AType (name, tys)) =
2610 apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
2611 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
2612 | do_type (APi (_, ty)) = do_type ty
2613 fun do_term pred_sym (ATerm ((name, tys), tms)) =
2615 (fn _ => default_type pred_sym (length tys) (length tms)))
2616 #> fold do_type tys #> fold (do_term false) tms
2617 | do_term _ (AAbs (((_, ty), tm), args)) =
2618 do_type ty #> do_term false tm #> fold (do_term false) args
2619 fun do_formula (ATyQuant (_, xs, phi)) =
2620 fold (do_type o fst) xs #> fold (fold do_class o snd) xs
2622 | do_formula (AQuant (_, xs, phi)) =
2623 fold do_type (map_filter snd xs) #> do_formula phi
2624 | do_formula (AConn (_, phis)) = fold do_formula phis
2625 | do_formula (AAtom tm) = do_term true tm
2626 fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
2627 | do_line (Type_Decl _) = I
2628 | do_line (Sym_Decl (_, _, ty)) = do_type ty
2629 | do_line (Class_Memb (_, xs, ty, cl)) =
2630 fold (fold do_class o snd) xs #> do_type ty #> do_class cl
2631 | do_line (Formula (_, _, phi, _, _)) = do_formula phi
2632 val ((cls, tys), syms) = declared_in_atp_problem problem
2634 ((Symtab.empty, Symtab.empty), Symtab.empty)
2635 |>> apfst (fold (fn (s, _) => Symtab.default (s, (("", ""), ()))) cls)
2636 |>> apsnd (fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys)
2637 ||> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype))) syms
2638 |> fold (fold do_line o snd) problem
2641 fun declare_undeclared_in_problem heading problem =
2643 val ((cls, tys), syms) = undeclared_in_problem problem
2645 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
2647 cons (Class_Decl (class_decl_prefix ^ s, cls, [])))
2649 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
2651 cons (Type_Decl (type_decl_prefix ^ s, ty, ary)))
2653 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
2655 cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ())))
2657 in (heading, decls) :: problem end
2659 fun is_poly_constr (Datatype.DtTFree _) = true
2660 | is_poly_constr (Datatype.DtType (_, Us)) = exists is_poly_constr Us
2661 | is_poly_constr _ = false
2663 fun all_constrs_of_polymorphic_datatypes thy =
2664 Symtab.fold (snd #> #descr #> maps (#3 o snd)
2665 #> (fn cs => exists (exists is_poly_constr o snd) cs
2666 ? append (map fst cs)))
2667 (Datatype.get_all thy) []
2669 val app_op_and_predicator_threshold = 45
2671 fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
2672 uncurried_aliases readable_names preproc hyp_ts concl_t
2675 val thy = Proof_Context.theory_of ctxt
2676 val type_enc = type_enc |> adjust_type_enc format
2677 (* Forcing explicit applications is expensive for polymorphic encodings,
2678 because it takes only one existential variable ranging over "'a => 'b" to
2679 ruin everything. Hence we do it only if there are few facts (which is
2680 normally the case for "metis" and the minimizer). *)
2682 if mode = Sledgehammer_Completish then
2683 Full_App_Op_And_Predicator
2684 else if length facts + length hyp_ts
2685 > app_op_and_predicator_threshold then
2686 if is_type_enc_polymorphic type_enc then Min_App_Op
2687 else Sufficient_App_Op
2689 Sufficient_App_Op_And_Predicator
2690 val exporter = (mode = Exporter)
2691 val completish = (mode = Sledgehammer_Completish)
2693 if lam_trans = keep_lamsN andalso
2694 not (is_type_enc_higher_order type_enc) then
2698 val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses,
2700 translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
2703 sym_table_for_facts ctxt type_enc app_op_level conjs facts
2705 conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc completish
2706 val constrs = all_constrs_of_polymorphic_datatypes thy
2707 fun firstorderize in_helper =
2708 firstorderize_fact thy constrs type_enc sym_tab0
2709 (uncurried_aliases andalso not in_helper) completish
2710 val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
2711 val (ho_stuff, sym_tab) =
2712 sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
2713 val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
2714 uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
2715 uncurried_aliases sym_tab0 sym_tab
2718 |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
2719 uncurried_alias_eq_tms
2721 sym_tab |> helper_facts_for_sym_table ctxt format type_enc completish
2722 |> map (firstorderize true)
2724 helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
2725 val class_decl_lines = decl_lines_for_classes type_enc classes
2726 val sym_decl_lines =
2727 (conjs, helpers @ facts, uncurried_alias_eq_tms)
2728 |> sym_decl_table_for_facts thy type_enc sym_tab
2729 |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts
2730 val num_facts = length facts
2732 map (line_for_fact ctxt fact_prefix ascii_of I (not exporter)
2733 (not exporter) mono type_enc (rank_of_fact_num num_facts))
2734 (0 upto num_facts - 1 ~~ facts)
2735 val subclass_lines = maps (lines_for_subclass_pair type_enc) subclass_pairs
2736 val tcon_lines = map (line_for_tcon_clause type_enc) tcon_clauses
2738 0 upto length helpers - 1 ~~ helpers
2739 |> map (line_for_fact ctxt helper_prefix I (K "") false true mono type_enc
2741 val free_type_lines = lines_for_free_types type_enc (facts @ conjs)
2742 val conj_lines = map (line_for_conjecture ctxt mono type_enc) conjs
2743 (* Reordering these might confuse the proof reconstruction code. *)
2745 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
2746 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
2747 (factsN, fact_lines),
2748 (subclassesN, subclass_lines),
2749 (tconsN, tcon_lines),
2750 (helpersN, helper_lines),
2751 (free_typesN, free_type_lines),
2752 (conjsN, conj_lines)]
2754 problem |> (case format of
2755 CNF => ensure_cnf_problem
2756 | CNF_UEQ => filter_cnf_ueq_problem
2758 | TFF (_, TPTP_Implicit) => I
2759 | THF (_, TPTP_Implicit, _, _) => I
2760 | _ => declare_undeclared_in_problem implicit_declsN)
2761 val (problem, pool) = problem |> nice_atp_problem readable_names format
2762 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
2763 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
2765 (problem, pool |> Option.map snd |> the_default Symtab.empty,
2766 fact_names |> Vector.fromList, lifted,
2767 Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
2771 val conj_weight = 0.0
2772 val hyp_weight = 0.1
2773 val fact_min_weight = 0.2
2774 val fact_max_weight = 1.0
2775 val type_info_default_weight = 0.8
2777 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
2778 fun atp_problem_selection_weights problem =
2780 fun add_term_weights weight (ATerm ((s, _), tms)) =
2781 is_tptp_user_symbol s ? Symtab.default (s, weight)
2782 #> fold (add_term_weights weight) tms
2783 | add_term_weights weight (AAbs ((_, tm), args)) =
2784 add_term_weights weight tm #> fold (add_term_weights weight) args
2785 fun add_line_weights weight (Formula (_, _, phi, _, _)) =
2786 formula_fold NONE (K (add_term_weights weight)) phi
2787 | add_line_weights _ _ = I
2788 fun add_conjectures_weights [] = I
2789 | add_conjectures_weights conjs =
2790 let val (hyps, conj) = split_last conjs in
2791 add_line_weights conj_weight conj
2792 #> fold (add_line_weights hyp_weight) hyps
2794 fun add_facts_weights facts =
2796 val num_facts = length facts
2798 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
2799 / Real.fromInt num_facts
2801 map weight_of (0 upto num_facts - 1) ~~ facts
2802 |> fold (uncurry add_line_weights)
2804 val get = these o AList.lookup (op =) problem
2807 |> add_conjectures_weights (get free_typesN @ get conjsN)
2808 |> add_facts_weights (get factsN)
2809 |> fold (fold (add_line_weights type_info_default_weight) o get)
2810 [explicit_declsN, subclassesN, tconsN]
2812 |> sort (prod_ord Real.compare string_ord o pairself swap)
2815 (* Ugly hack: may make innocent victims (collateral damage) *)
2816 fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2
2817 fun may_be_predicator s =
2818 member (op =) [predicator_name, prefixed_predicator_name] s
2820 fun strip_predicator (tm as ATerm ((s, _), [tm'])) =
2821 if may_be_predicator s then tm' else tm
2822 | strip_predicator tm = tm
2824 fun make_head_roll (ATerm ((s, _), tms)) =
2825 if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
2827 | make_head_roll _ = ("", [])
2829 fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi
2830 | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
2831 | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
2832 | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
2834 fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi
2835 | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
2836 | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
2837 strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
2838 | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
2840 fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
2841 | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
2842 | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
2843 pairself strip_up_to_predicator (phi1, phi2)
2844 | strip_iff_etc _ = ([], [])
2846 val max_term_order_weight = 2147483647
2848 fun atp_problem_term_order_info problem =
2851 Graph.default_node (s, ())
2852 #> Graph.default_node (s', ())
2853 #> Graph.add_edge_acyclic (s, s')
2854 fun add_term_deps head (ATerm ((s, _), args)) =
2855 if is_tptp_user_symbol head then
2856 (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I)
2857 #> fold (add_term_deps head) args
2860 | add_term_deps head (AAbs ((_, tm), args)) =
2861 add_term_deps head tm #> fold (add_term_deps head) args
2862 fun add_intro_deps pred (Formula (_, role, phi, _, info)) =
2863 if pred (role, info) then
2864 let val (hyps, concl) = strip_ahorn_etc phi in
2865 case make_head_roll concl of
2866 (head, args as _ :: _) => fold (add_term_deps head) (hyps @ args)
2871 | add_intro_deps _ _ = I
2872 fun add_atom_eq_deps (SOME true) (ATerm ((s, _), [lhs as _, rhs])) =
2873 if is_tptp_equal s then
2874 case make_head_roll lhs of
2875 (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args)
2879 | add_atom_eq_deps _ _ = I
2880 fun add_eq_deps pred (Formula (_, role, phi, _, info)) =
2881 if pred (role, info) then
2882 case strip_iff_etc phi of
2884 (case make_head_roll lhs of
2885 (head, args as _ :: _) => fold (add_term_deps head) (rhs @ args)
2887 | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi
2890 | add_eq_deps _ _ = I
2891 fun has_status status (_, info) = extract_isabelle_status info = SOME status
2892 fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
2895 |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem
2896 |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN
2897 orf is_conj)) o snd) problem
2898 |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem
2899 |> fold (fold (add_intro_deps (has_status introN)) o snd) problem
2900 fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
2901 fun add_weights _ [] = I
2902 | add_weights weight syms =
2903 fold (AList.update (op =) o rpair weight) syms
2904 #> add_weights (next_weight weight)
2905 (fold (union (op =) o Graph.immediate_succs graph) syms [])
2907 (* Sorting is not just for aesthetics: It specifies the precedence order
2908 for the term ordering (KBO or LPO), from smaller to larger values. *)
2909 [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)