remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
1 (* Title: HOL/Tools/ATP/atp_translate.ML
2 Author: Fabian Immler, TU Muenchen
4 Author: Jasmin Blanchette, TU Muenchen
6 Translation of HOL to FOL for Sledgehammer.
9 signature ATP_TRANSLATE =
11 type 'a fo_term = 'a ATP_Problem.fo_term
12 type connective = ATP_Problem.connective
13 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
14 type format = ATP_Problem.format
15 type formula_kind = ATP_Problem.formula_kind
16 type 'a problem = 'a ATP_Problem.problem
19 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
22 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
24 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
26 datatype type_heaviness = Heavyweight | Lightweight
29 Simple_Types of type_level |
30 Preds of polymorphism * type_level * type_heaviness |
31 Tags of polymorphism * type_level * type_heaviness
33 val bound_var_prefix : string
34 val schematic_var_prefix : string
35 val fixed_var_prefix : string
36 val tvar_prefix : string
37 val tfree_prefix : string
38 val const_prefix : string
39 val type_const_prefix : string
40 val class_prefix : string
41 val skolem_const_prefix : string
42 val old_skolem_const_prefix : string
43 val new_skolem_const_prefix : string
44 val type_decl_prefix : string
45 val sym_decl_prefix : string
46 val preds_sym_formula_prefix : string
47 val lightweight_tags_sym_formula_prefix : string
48 val fact_prefix : string
49 val conjecture_prefix : string
50 val helper_prefix : string
51 val class_rel_clause_prefix : string
52 val arity_clause_prefix : string
53 val tfree_clause_prefix : string
54 val typed_helper_suffix : string
55 val untyped_helper_suffix : string
56 val type_tag_idempotence_helper_name : string
57 val predicator_name : string
58 val app_op_name : string
59 val type_tag_name : string
60 val type_pred_name : string
61 val simple_type_prefix : string
62 val prefixed_predicator_name : string
63 val prefixed_app_op_name : string
64 val prefixed_type_tag_name : string
65 val ascii_of : string -> string
66 val unascii_of : string -> string
67 val strip_prefix_and_unascii : string -> string -> string option
68 val proxy_table : (string * (string * (thm * (string * string)))) list
69 val proxify_const : string -> (string * string) option
70 val invert_const : string -> string
71 val unproxify_const : string -> string
72 val new_skolem_var_name_from_const : string -> string
73 val num_type_args : theory -> string -> int
74 val atp_irrelevant_consts : string list
75 val atp_schematic_consts_of : term -> typ list Symtab.table
76 val is_locality_global : locality -> bool
77 val type_sys_from_string : string -> type_sys
78 val polymorphism_of_type_sys : type_sys -> polymorphism
79 val level_of_type_sys : type_sys -> type_level
80 val is_type_sys_virtually_sound : type_sys -> bool
81 val is_type_sys_fairly_sound : type_sys -> bool
82 val choose_format : format list -> type_sys -> format * type_sys
84 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
85 val unmangled_const : string -> string * string fo_term list
86 val unmangled_const_name : string -> string
87 val helper_table : ((string * bool) * thm list) list
88 val prepare_atp_problem :
89 Proof.context -> format -> formula_kind -> formula_kind -> type_sys
90 -> bool -> bool -> bool -> term list -> term
91 -> ((string * locality) * term) list
92 -> string problem * string Symtab.table * int * int
93 * (string * locality) list vector * int list * int Symtab.table
94 val atp_problem_weights : string problem -> (string * real) list
97 structure ATP_Translate : ATP_TRANSLATE =
103 type name = string * string
106 val generate_useful_info = false
108 fun useful_isabelle_info s =
109 if generate_useful_info then
110 SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
114 val intro_info = useful_isabelle_info "intro"
115 val elim_info = useful_isabelle_info "elim"
116 val simp_info = useful_isabelle_info "simp"
118 val bound_var_prefix = "B_"
119 val schematic_var_prefix = "V_"
120 val fixed_var_prefix = "v_"
122 val tvar_prefix = "T_"
123 val tfree_prefix = "t_"
125 val const_prefix = "c_"
126 val type_const_prefix = "tc_"
127 val class_prefix = "cl_"
129 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
130 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
131 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
133 val type_decl_prefix = "ty_"
134 val sym_decl_prefix = "sy_"
135 val preds_sym_formula_prefix = "psy_"
136 val lightweight_tags_sym_formula_prefix = "tsy_"
137 val fact_prefix = "fact_"
138 val conjecture_prefix = "conj_"
139 val helper_prefix = "help_"
140 val class_rel_clause_prefix = "clar_"
141 val arity_clause_prefix = "arity_"
142 val tfree_clause_prefix = "tfree_"
144 val typed_helper_suffix = "_T"
145 val untyped_helper_suffix = "_U"
146 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
148 val predicator_name = "hBOOL"
149 val app_op_name = "hAPP"
150 val type_tag_name = "ti"
151 val type_pred_name = "is"
152 val simple_type_prefix = "ty_"
154 val prefixed_predicator_name = const_prefix ^ predicator_name
155 val prefixed_app_op_name = const_prefix ^ app_op_name
156 val prefixed_type_tag_name = const_prefix ^ type_tag_name
158 (* Freshness almost guaranteed! *)
159 val sledgehammer_weak_prefix = "Sledgehammer:"
161 (*Escaping of special characters.
162 Alphanumeric characters are left unchanged.
163 The character _ goes to __
164 Characters in the range ASCII space to / go to _A to _P, respectively.
165 Other characters go to _nnn where nnn is the decimal ASCII code.*)
166 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
168 fun stringN_of_int 0 _ = ""
169 | stringN_of_int k n =
170 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
172 fun ascii_of_char c =
173 if Char.isAlphaNum c then
175 else if c = #"_" then
177 else if #" " <= c andalso c <= #"/" then
178 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
180 (* fixed width, in case more digits follow *)
181 "_" ^ stringN_of_int 3 (Char.ord c)
183 val ascii_of = String.translate ascii_of_char
185 (** Remove ASCII armoring from names in proof files **)
187 (* We don't raise error exceptions because this code can run inside a worker
188 thread. Also, the errors are impossible. *)
191 fun un rcs [] = String.implode(rev rcs)
192 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
193 (* Three types of _ escapes: __, _A to _P, _nnn *)
194 | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
195 | un rcs (#"_" :: c :: cs) =
196 if #"A" <= c andalso c<= #"P" then
197 (* translation of #" " to #"/" *)
198 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
200 let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
201 case Int.fromString (String.implode digits) of
202 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
203 | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
205 | un rcs (c :: cs) = un (c :: rcs) cs
206 in un [] o String.explode end
208 (* If string s has the prefix s1, return the result of deleting it,
210 fun strip_prefix_and_unascii s1 s =
211 if String.isPrefix s1 s then
212 SOME (unascii_of (String.extract (s, size s1, NONE)))
217 [("c_False", (@{const_name False}, (@{thm fFalse_def},
218 ("fFalse", @{const_name ATP.fFalse})))),
219 ("c_True", (@{const_name True}, (@{thm fTrue_def},
220 ("fTrue", @{const_name ATP.fTrue})))),
221 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
222 ("fNot", @{const_name ATP.fNot})))),
223 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
224 ("fconj", @{const_name ATP.fconj})))),
225 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
226 ("fdisj", @{const_name ATP.fdisj})))),
227 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
228 ("fimplies", @{const_name ATP.fimplies})))),
229 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
230 ("fequal", @{const_name ATP.fequal}))))]
232 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
234 (* Readable names for the more common symbolic functions. Do not mess with the
235 table unless you know what you are doing. *)
236 val const_trans_table =
237 [(@{type_name Product_Type.prod}, "prod"),
238 (@{type_name Sum_Type.sum}, "sum"),
239 (@{const_name False}, "False"),
240 (@{const_name True}, "True"),
241 (@{const_name Not}, "Not"),
242 (@{const_name conj}, "conj"),
243 (@{const_name disj}, "disj"),
244 (@{const_name implies}, "implies"),
245 (@{const_name HOL.eq}, "equal"),
246 (@{const_name If}, "If"),
247 (@{const_name Set.member}, "member"),
248 (@{const_name Meson.COMBI}, "COMBI"),
249 (@{const_name Meson.COMBK}, "COMBK"),
250 (@{const_name Meson.COMBB}, "COMBB"),
251 (@{const_name Meson.COMBC}, "COMBC"),
252 (@{const_name Meson.COMBS}, "COMBS")]
254 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
256 (* Invert the table of translations between Isabelle and ATPs. *)
257 val const_trans_table_inv =
258 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
259 val const_trans_table_unprox =
261 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
263 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
264 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
267 case Symtab.lookup const_trans_table c of
271 (*Remove the initial ' character from a type variable, if it is present*)
272 fun trim_type_var s =
273 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
274 else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
276 fun ascii_of_indexname (v,0) = ascii_of v
277 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
279 fun make_bound_var x = bound_var_prefix ^ ascii_of x
280 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
281 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
283 fun make_schematic_type_var (x,i) =
284 tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
285 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
287 (* HOL.eq MUST BE "equal" because it's built into ATPs. *)
288 fun make_fixed_const @{const_name HOL.eq} = "equal"
289 | make_fixed_const c = const_prefix ^ lookup_const c
291 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
293 fun make_type_class clas = class_prefix ^ ascii_of clas
295 fun new_skolem_var_name_from_const s =
296 let val ss = s |> space_explode Long_Name.separator in
297 nth ss (length ss - 2)
300 (* The number of type arguments of a constant, zero if it's monomorphic. For
301 (instances of) Skolem pseudoconstants, this information is encoded in the
303 fun num_type_args thy s =
304 if String.isPrefix skolem_const_prefix s then
305 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
307 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
309 (* These are either simplified away by "Meson.presimplify" (most of the time) or
310 handled specially via "fFalse", "fTrue", ..., "fequal". *)
311 val atp_irrelevant_consts =
312 [@{const_name False}, @{const_name True}, @{const_name Not},
313 @{const_name conj}, @{const_name disj}, @{const_name implies},
314 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
316 val atp_monomorph_bad_consts =
317 atp_irrelevant_consts @
318 (* These are ignored anyway by the relevance filter (unless they appear in
319 higher-order places) but not by the monomorphizer. *)
320 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
321 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
322 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
324 fun add_schematic_const (x as (_, T)) =
325 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
326 val add_schematic_consts_of =
327 Term.fold_aterms (fn Const (x as (s, _)) =>
328 not (member (op =) atp_monomorph_bad_consts s)
329 ? add_schematic_const x
331 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
333 (** Definitions and functions for FOL clauses and formulas for TPTP **)
335 (* The first component is the type class; the second is a "TVar" or "TFree". *)
336 datatype type_literal =
337 TyLitVar of name * name |
338 TyLitFree of name * name
341 (** Isabelle arities **)
343 datatype arity_literal =
344 TConsLit of name * name * name list |
345 TVarLit of name * name
348 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
350 val type_class = the_single @{sort type}
352 fun add_packed_sort tvar =
353 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
357 prem_lits : arity_literal list,
358 concl_lits : arity_literal}
360 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
361 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
363 val tvars = gen_TVars (length args)
364 val tvars_srts = ListPair.zip (tvars, args)
367 prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
368 concl_lits = TConsLit (`make_type_class cls,
369 `make_fixed_type_const tcons,
373 fun arity_clause _ _ (_, []) = []
374 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) = (* ignore *)
375 arity_clause seen n (tcons, ars)
376 | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
377 if member (op =) seen class then
378 (* multiple arities for the same (tycon, class) pair *)
379 make_axiom_arity_clause (tcons,
380 lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
382 arity_clause seen (n + 1) (tcons, ars)
384 make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
385 ascii_of class, ar) ::
386 arity_clause (class :: seen) n (tcons, ars)
388 fun multi_arity_clause [] = []
389 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
390 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
392 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
393 provided its arguments have the corresponding sorts.*)
394 fun type_class_pairs thy tycons classes =
396 val alg = Sign.classes_of thy
397 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
398 fun add_class tycon class =
399 cons (class, domain_sorts tycon class)
400 handle Sorts.CLASS_ERROR _ => I
401 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
402 in map try_classes tycons end
404 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
405 fun iter_type_class_pairs _ _ [] = ([], [])
406 | iter_type_class_pairs thy tycons classes =
408 fun maybe_insert_class s =
409 (s <> type_class andalso not (member (op =) classes s))
411 val cpairs = type_class_pairs thy tycons classes
413 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
414 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
415 in (classes' @ classes, union (op =) cpairs' cpairs) end
417 fun make_arity_clauses thy tycons =
418 iter_type_class_pairs thy tycons ##> multi_arity_clause
421 (** Isabelle class relations **)
423 type class_rel_clause =
428 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
429 fun class_pairs _ [] _ = []
430 | class_pairs thy subs supers =
432 val class_less = Sorts.class_less (Sign.classes_of thy)
433 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
434 fun add_supers sub = fold (add_super sub) supers
435 in fold add_supers subs [] end
437 fun make_class_rel_clause (sub,super) =
438 {name = sub ^ "_" ^ super,
439 subclass = `make_type_class sub,
440 superclass = `make_type_class super}
442 fun make_class_rel_clauses thy subs supers =
443 map make_class_rel_clause (class_pairs thy subs supers)
446 CombConst of name * typ * typ list |
447 CombVar of name * typ |
448 CombApp of combterm * combterm
450 fun combtyp_of (CombConst (_, T, _)) = T
451 | combtyp_of (CombVar (_, T)) = T
452 | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
454 (*gets the head of a combinator application, along with the list of arguments*)
455 fun strip_combterm_comb u =
457 fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
459 in stripc (u, []) end
461 fun atyps_of T = fold_atyps (insert (op =)) T []
463 fun new_skolem_const_name s num_T_args =
464 [new_skolem_const_prefix, s, string_of_int num_T_args]
465 |> space_implode Long_Name.separator
467 (* Converts a term (with combinators) into a combterm. Also accumulates sort
469 fun combterm_from_term thy bs (P $ Q) =
471 val (P', P_atomics_Ts) = combterm_from_term thy bs P
472 val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
473 in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
474 | combterm_from_term thy _ (Const (c, T)) =
477 (if String.isPrefix old_skolem_const_prefix c then
478 [] |> Term.add_tvarsT T |> map TVar
480 (c, T) |> Sign.const_typargs thy)
481 val c' = CombConst (`make_fixed_const c, T, tvar_list)
482 in (c', atyps_of T) end
483 | combterm_from_term _ _ (Free (v, T)) =
484 (CombConst (`make_fixed_var v, T, []), atyps_of T)
485 | combterm_from_term _ _ (Var (v as (s, _), T)) =
486 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
488 val Ts = T |> strip_type |> swap |> op ::
489 val s' = new_skolem_const_name s (length Ts)
490 in CombConst (`make_fixed_const s', T, Ts) end
492 CombVar ((make_schematic_var v, s), T), atyps_of T)
493 | combterm_from_term _ bs (Bound j) =
495 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
496 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
499 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
502 (* (quasi-)underapproximation of the truth *)
503 fun is_locality_global Local = false
504 | is_locality_global Assum = false
505 | is_locality_global Chained = false
506 | is_locality_global _ = true
508 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
509 datatype type_level =
510 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
512 datatype type_heaviness = Heavyweight | Lightweight
515 Simple_Types of type_level |
516 Preds of polymorphism * type_level * type_heaviness |
517 Tags of polymorphism * type_level * type_heaviness
519 fun try_unsuffixes ss s =
520 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
522 fun type_sys_from_string s =
523 (case try (unprefix "poly_") s of
524 SOME s => (SOME Polymorphic, s)
526 case try (unprefix "mono_") s of
527 SOME s => (SOME Monomorphic, s)
529 case try (unprefix "mangled_") s of
530 SOME s => (SOME Mangled_Monomorphic, s)
533 (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
534 case try_unsuffixes ["?", "_query"] s of
535 SOME s => (Noninf_Nonmono_Types, s)
537 case try_unsuffixes ["!", "_bang"] s of
538 SOME s => (Fin_Nonmono_Types, s)
539 | NONE => (All_Types, s))
541 case try (unsuffix "_heavy") s of
542 SOME s => (Heavyweight, s)
543 | NONE => (Lightweight, s))
544 |> (fn (poly, (level, (heaviness, core))) =>
545 case (core, (poly, level, heaviness)) of
546 ("simple", (NONE, _, Lightweight)) => Simple_Types level
547 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
548 | ("tags", (SOME Polymorphic, _, _)) =>
549 Tags (Polymorphic, level, heaviness)
550 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
551 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
552 Preds (poly, Const_Arg_Types, Lightweight)
553 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
554 Preds (Polymorphic, No_Types, Lightweight)
555 | _ => raise Same.SAME)
556 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
558 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
559 | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
560 | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
562 fun level_of_type_sys (Simple_Types level) = level
563 | level_of_type_sys (Preds (_, level, _)) = level
564 | level_of_type_sys (Tags (_, level, _)) = level
566 fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
567 | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
568 | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
570 fun is_type_level_virtually_sound level =
571 level = All_Types orelse level = Noninf_Nonmono_Types
572 val is_type_sys_virtually_sound =
573 is_type_level_virtually_sound o level_of_type_sys
575 fun is_type_level_fairly_sound level =
576 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
577 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
579 fun is_setting_higher_order THF (Simple_Types _) = true
580 | is_setting_higher_order _ _ = false
582 fun choose_format formats (Simple_Types level) =
583 if member (op =) formats THF then (THF, Simple_Types level)
584 else if member (op =) formats TFF then (TFF, Simple_Types level)
585 else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
586 | choose_format formats type_sys =
589 (CNF_UEQ, case type_sys of
591 (if is_type_sys_fairly_sound type_sys then Tags else Preds)
594 | format => (format, type_sys))
596 type translated_formula =
600 combformula : (name, typ, combterm) formula,
601 atomic_types : typ list}
603 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
604 : translated_formula) =
605 {name = name, locality = locality, kind = kind, combformula = f combformula,
606 atomic_types = atomic_types} : translated_formula
608 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
610 val type_instance = Sign.typ_instance o Proof_Context.theory_of
612 fun insert_type ctxt get_T x xs =
613 let val T = get_T x in
614 if exists (curry (type_instance ctxt) T o get_T) xs then xs
615 else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
618 (* The Booleans indicate whether all type arguments should be kept. *)
619 datatype type_arg_policy =
620 Explicit_Type_Args of bool |
621 Mangled_Type_Args of bool |
624 fun should_drop_arg_type_args (Simple_Types _) =
625 false (* since TFF doesn't support overloading *)
626 | should_drop_arg_type_args type_sys =
627 level_of_type_sys type_sys = All_Types andalso
628 heaviness_of_type_sys type_sys = Heavyweight
630 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
631 | general_type_arg_policy type_sys =
632 if level_of_type_sys type_sys = No_Types then
634 else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
635 Mangled_Type_Args (should_drop_arg_type_args type_sys)
637 Explicit_Type_Args (should_drop_arg_type_args type_sys)
639 fun type_arg_policy type_sys s =
640 if s = @{const_name HOL.eq} orelse
641 (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
643 else if s = type_tag_name then
644 Explicit_Type_Args false
646 general_type_arg_policy type_sys
648 (*Make literals for sorted type variables*)
649 fun generic_add_sorts_on_type (_, []) = I
650 | generic_add_sorts_on_type ((x, i), s :: ss) =
651 generic_add_sorts_on_type ((x, i), ss)
652 #> (if s = the_single @{sort HOL.type} then
655 insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
657 insert (op =) (TyLitVar (`make_type_class s,
658 (make_schematic_type_var (x, i), x))))
659 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
660 | add_sorts_on_tfree _ = I
661 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
662 | add_sorts_on_tvar _ = I
664 fun type_literals_for_types type_sys add_sorts_on_typ Ts =
665 [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
667 fun mk_aconns c phis =
668 let val (phis', phi') = split_last phis in
669 fold_rev (mk_aconn c) phis' phi'
671 fun mk_ahorn [] phi = phi
672 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
673 fun mk_aquant _ [] phi = phi
674 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
675 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
676 | mk_aquant q xs phi = AQuant (q, xs, phi)
678 fun close_universally atom_vars phi =
680 fun formula_vars bounds (AQuant (_, xs, phi)) =
681 formula_vars (map fst xs @ bounds) phi
682 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
683 | formula_vars bounds (AAtom tm) =
684 union (op =) (atom_vars tm []
685 |> filter_out (member (op =) bounds o fst))
686 in mk_aquant AForall (formula_vars [] phi []) phi end
688 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
689 | combterm_vars (CombConst _) = I
690 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
691 fun close_combformula_universally phi = close_universally combterm_vars phi
693 fun term_vars (ATerm (name as (s, _), tms)) =
694 is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
695 fun close_formula_universally phi = close_universally term_vars phi
697 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
698 val homo_infinite_type = Type (homo_infinite_type_name, [])
700 fun fo_term_from_typ format type_sys =
702 fun term (Type (s, Ts)) =
703 ATerm (case (is_setting_higher_order format type_sys, s) of
704 (true, @{type_name bool}) => `I tptp_bool_type
705 | (true, @{type_name fun}) => `I tptp_fun_type
706 | _ => if s = homo_infinite_type_name andalso
707 (format = TFF orelse format = THF) then
708 `I tptp_individual_type
710 `make_fixed_type_const s,
712 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
713 | term (TVar ((x as (s, _)), _)) =
714 ATerm ((make_schematic_type_var x, s), [])
717 fun fo_term_for_type_arg format type_sys T =
718 if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
720 (* This shouldn't clash with anything else. *)
721 val mangled_type_sep = "\000"
723 fun generic_mangled_type_name f (ATerm (name, [])) = f name
724 | generic_mangled_type_name f (ATerm (name, tys)) =
725 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
728 val bool_atype = AType (`I tptp_bool_type)
730 fun make_simple_type s =
731 if s = tptp_bool_type orelse s = tptp_fun_type orelse
732 s = tptp_individual_type then
735 simple_type_prefix ^ ascii_of s
737 fun ho_type_from_fo_term format type_sys pred_sym ary =
740 AType ((make_simple_type (generic_mangled_type_name fst ty),
741 generic_mangled_type_name snd ty))
742 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
743 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
744 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
745 fun to_ho (ty as ATerm ((s, _), tys)) =
746 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
747 in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
749 fun mangled_type format type_sys pred_sym ary =
750 ho_type_from_fo_term format type_sys pred_sym ary
751 o fo_term_from_typ format type_sys
753 fun mangled_const_name format type_sys T_args (s, s') =
755 val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
756 fun type_suffix f g =
757 fold_rev (curry (op ^) o g o prefix mangled_type_sep
758 o generic_mangled_type_name f) ty_args ""
759 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
761 val parse_mangled_ident =
762 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
764 fun parse_mangled_type x =
766 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
768 and parse_mangled_types x =
769 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
771 fun unmangled_type s =
772 s |> suffix ")" |> raw_explode
773 |> Scan.finite Symbol.stopper
774 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
775 quote s)) parse_mangled_type))
778 val unmangled_const_name = space_explode mangled_type_sep #> hd
779 fun unmangled_const s =
780 let val ss = space_explode mangled_type_sep s in
781 (hd ss, map unmangled_type (tl ss))
784 fun introduce_proxies format type_sys =
786 fun intro top_level (CombApp (tm1, tm2)) =
787 CombApp (intro top_level tm1, intro false tm2)
788 | intro top_level (CombConst (name as (s, _), T, T_args)) =
789 (case proxify_const s of
791 if top_level orelse is_setting_higher_order format type_sys then
792 case (top_level, s) of
793 (_, "c_False") => (`I tptp_false, [])
794 | (_, "c_True") => (`I tptp_true, [])
795 | (false, "c_Not") => (`I tptp_not, [])
796 | (false, "c_conj") => (`I tptp_and, [])
797 | (false, "c_disj") => (`I tptp_or, [])
798 | (false, "c_implies") => (`I tptp_implies, [])
800 if is_tptp_equal s then (`I tptp_equal, [])
801 else (proxy_base |>> prefix const_prefix, T_args)
804 (proxy_base |>> prefix const_prefix, T_args)
805 | NONE => (name, T_args))
806 |> (fn (name, T_args) => CombConst (name, T, T_args))
810 fun combformula_from_prop thy format type_sys eq_as_iff =
812 fun do_term bs t atomic_types =
813 combterm_from_term thy bs (Envir.eta_contract t)
814 |>> (introduce_proxies format type_sys #> AAtom)
815 ||> union (op =) atomic_types
816 fun do_quant bs q s T t' =
817 let val s = singleton (Name.variant_list (map fst bs)) s in
818 do_formula ((s, T) :: bs) t'
819 #>> mk_aquant q [(`make_bound_var s, SOME T)]
821 and do_conn bs c t1 t2 =
822 do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
823 and do_formula bs t =
825 @{const Trueprop} $ t1 => do_formula bs t1
826 | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
827 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
828 do_quant bs AForall s T t'
829 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
830 do_quant bs AExists s T t'
831 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
832 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
833 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
834 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
835 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
839 fun presimplify_term _ [] t = t
840 | presimplify_term ctxt presimp_consts t =
841 t |> exists_Const (member (op =) presimp_consts o fst) t
842 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
843 #> Meson.presimplify ctxt
846 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
847 fun conceal_bounds Ts t =
848 subst_bounds (map (Free o apfst concealed_bound_name)
849 (0 upto length Ts - 1 ~~ Ts), t)
850 fun reveal_bounds Ts =
851 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
852 (0 upto length Ts - 1 ~~ Ts))
854 fun is_fun_equality (@{const_name HOL.eq},
855 Type (_, [Type (@{type_name fun}, _), _])) = true
856 | is_fun_equality _ = false
858 fun extensionalize_term ctxt t =
859 if exists_Const is_fun_equality t then
860 let val thy = Proof_Context.theory_of ctxt in
861 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
862 |> prop_of |> Logic.dest_equals |> snd
867 fun introduce_combinators_in_term ctxt kind t =
868 let val thy = Proof_Context.theory_of ctxt in
869 if Meson.is_fol_term thy t then
875 @{const Not} $ t1 => @{const Not} $ aux Ts t1
876 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
877 t0 $ Abs (s, T, aux (T :: Ts) t')
878 | (t0 as Const (@{const_name All}, _)) $ t1 =>
879 aux Ts (t0 $ eta_expand Ts t1 1)
880 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
881 t0 $ Abs (s, T, aux (T :: Ts) t')
882 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
883 aux Ts (t0 $ eta_expand Ts t1 1)
884 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
885 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
886 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
887 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
889 t0 $ aux Ts t1 $ aux Ts t2
890 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
893 t |> conceal_bounds Ts
894 |> Envir.eta_contract
896 |> Meson_Clausify.introduce_combinators_in_cterm
897 |> prop_of |> Logic.dest_equals |> snd
899 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
900 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
902 (* A type variable of sort "{}" will make abstraction fail. *)
903 if kind = Conjecture then HOLogic.false_const
904 else HOLogic.true_const
907 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
908 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
911 fun aux (t $ u) = aux t $ aux u
912 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
913 | aux (Var ((s, i), T)) =
914 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
916 in t |> exists_subterm is_Var t ? aux end
918 fun preprocess_prop ctxt presimp_consts kind t =
920 val thy = Proof_Context.theory_of ctxt
921 val t = t |> Envir.beta_eta_contract
922 |> transform_elim_prop
923 |> Object_Logic.atomize_term thy
924 val need_trueprop = (fastype_of t = @{typ bool})
926 t |> need_trueprop ? HOLogic.mk_Trueprop
927 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
928 |> extensionalize_term ctxt
929 |> presimplify_term ctxt presimp_consts
930 |> perhaps (try (HOLogic.dest_Trueprop))
931 |> introduce_combinators_in_term ctxt kind
934 (* making fact and conjecture formulas *)
935 fun make_formula thy format type_sys eq_as_iff name loc kind t =
937 val (combformula, atomic_types) =
938 combformula_from_prop thy format type_sys eq_as_iff t []
940 {name = name, locality = loc, kind = kind, combformula = combformula,
941 atomic_types = atomic_types}
944 fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
946 let val thy = Proof_Context.theory_of ctxt in
947 case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
948 |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
950 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
951 if s = tptp_true then NONE else SOME formula
952 | formula => SOME formula
955 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
957 val thy = Proof_Context.theory_of ctxt
958 val last = length ts - 1
960 map2 (fn j => fn t =>
962 val (kind, maybe_negate) =
967 if prem_kind = Conjecture then update_combformula mk_anot
971 (preprocess_prop ctxt presimp_consts kind #> freeze_term)
972 |> make_formula thy format type_sys (format <> CNF)
973 (string_of_int j) Local kind
979 (** Finite and infinite type inference **)
981 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
982 | deep_freeze_atyp T = T
983 val deep_freeze_type = map_atyps deep_freeze_atyp
985 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
986 dangerous because their "exhaust" properties can easily lead to unsound ATP
987 proofs. On the other hand, all HOL infinite types can be given the same
988 models in first-order logic (via Löwenheim-Skolem). *)
990 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
991 exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
992 | should_encode_type _ _ All_Types _ = true
993 | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
994 | should_encode_type _ _ _ _ = false
996 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
997 should_predicate_on_var T =
998 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
999 should_encode_type ctxt nonmono_Ts level T
1000 | should_predicate_on_type _ _ _ _ _ = false
1002 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
1003 String.isPrefix bound_var_prefix s
1004 | is_var_or_bound_var (CombVar _) = true
1005 | is_var_or_bound_var _ = false
1008 Top_Level of bool option |
1009 Eq_Arg of bool option |
1012 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1013 | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
1016 Heavyweight => should_encode_type ctxt nonmono_Ts level T
1018 case (site, is_var_or_bound_var u) of
1019 (Eq_Arg pos, true) =>
1020 (* The first disjunct prevents a subtle soundness issue explained in
1021 Blanchette's Ph.D. thesis. See also
1022 "formula_lines_for_lightweight_tags_sym_decl". *)
1023 (pos <> SOME false andalso poly = Polymorphic andalso
1024 level <> All_Types andalso heaviness = Lightweight andalso
1025 exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
1026 should_encode_type ctxt nonmono_Ts level T
1028 | should_tag_with_type _ _ _ _ _ _ = false
1030 fun homogenized_type ctxt nonmono_Ts level =
1032 val should_encode = should_encode_type ctxt nonmono_Ts level
1033 fun homo 0 T = if should_encode T then T else homo_infinite_type
1034 | homo ary (Type (@{type_name fun}, [T1, T2])) =
1035 homo 0 T1 --> homo (ary - 1) T2
1036 | homo _ _ = raise Fail "expected function type"
1039 (** "hBOOL" and "hAPP" **)
1042 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1044 fun add_combterm_syms_to_table ctxt explicit_apply =
1046 fun consider_var_arity const_T var_T max_ary =
1049 if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
1050 type_instance ctxt (T, var_T) then
1053 iter (ary + 1) (range_type T)
1054 in iter 0 const_T end
1055 fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1056 if explicit_apply = NONE andalso
1057 (can dest_funT T orelse T = @{typ bool}) then
1059 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1060 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
1061 {pred_sym = pred_sym andalso not bool_vars',
1062 min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
1063 max_ary = max_ary, types = types}
1065 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1067 if bool_vars' = bool_vars andalso
1068 pointer_eq (fun_var_Ts', fun_var_Ts) then
1071 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
1075 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1076 let val (head, args) = strip_combterm_comb tm in
1078 CombConst ((s, _), T, _) =>
1079 if String.isPrefix bound_var_prefix s then
1080 add_var_or_bound_var T accum
1082 let val ary = length args in
1083 ((bool_vars, fun_var_Ts),
1084 case Symtab.lookup sym_tab s of
1085 SOME {pred_sym, min_ary, max_ary, types} =>
1088 pred_sym andalso top_level andalso not bool_vars
1089 val types' = types |> insert_type ctxt I T
1091 if is_some explicit_apply orelse
1092 pointer_eq (types', types) then
1095 fold (consider_var_arity T) fun_var_Ts min_ary
1097 Symtab.update (s, {pred_sym = pred_sym,
1098 min_ary = Int.min (ary, min_ary),
1099 max_ary = Int.max (ary, max_ary),
1105 val pred_sym = top_level andalso not bool_vars
1107 case explicit_apply of
1110 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1112 Symtab.update_new (s, {pred_sym = pred_sym,
1113 min_ary = min_ary, max_ary = ary,
1118 | CombVar (_, T) => add_var_or_bound_var T accum
1120 |> fold (add false) args
1123 fun add_fact_syms_to_table ctxt explicit_apply =
1124 fact_lift (formula_fold NONE
1125 (K (add_combterm_syms_to_table ctxt explicit_apply)))
1127 val default_sym_tab_entries : (string * sym_info) list =
1128 (prefixed_predicator_name,
1129 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
1130 ([tptp_false, tptp_true]
1131 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1132 ([tptp_equal, tptp_old_equal]
1133 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1135 fun sym_table_for_facts ctxt explicit_apply facts =
1136 ((false, []), Symtab.empty)
1137 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1138 |> fold Symtab.update default_sym_tab_entries
1140 fun min_arity_of sym_tab s =
1141 case Symtab.lookup sym_tab s of
1142 SOME ({min_ary, ...} : sym_info) => min_ary
1144 case strip_prefix_and_unascii const_prefix s of
1146 let val s = s |> unmangled_const_name |> invert_const in
1147 if s = predicator_name then 1
1148 else if s = app_op_name then 2
1149 else if s = type_pred_name then 1
1154 (* True if the constant ever appears outside of the top-level position in
1155 literals, or if it appears with different arities (e.g., because of different
1156 type instantiations). If false, the constant always receives all of its
1157 arguments and is used as a predicate. *)
1158 fun is_pred_sym sym_tab s =
1159 case Symtab.lookup sym_tab s of
1160 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1161 pred_sym andalso min_ary = max_ary
1164 val predicator_combconst =
1165 CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1166 fun predicator tm = CombApp (predicator_combconst, tm)
1168 fun introduce_predicators_in_combterm sym_tab tm =
1169 case strip_combterm_comb tm of
1170 (CombConst ((s, _), _, _), _) =>
1171 if is_pred_sym sym_tab s then tm else predicator tm
1172 | _ => predicator tm
1174 fun list_app head args = fold (curry (CombApp o swap)) args head
1176 val app_op = `make_fixed_const app_op_name
1178 fun explicit_app arg head =
1180 val head_T = combtyp_of head
1181 val (arg_T, res_T) = dest_funT head_T
1183 CombConst (app_op, head_T --> head_T, [arg_T, res_T])
1184 in list_app explicit_app [head, arg] end
1185 fun list_explicit_app head args = fold explicit_app args head
1187 fun introduce_explicit_apps_in_combterm sym_tab =
1190 case strip_combterm_comb tm of
1191 (head as CombConst ((s, _), _, _), args) =>
1193 |> chop (min_arity_of sym_tab s)
1195 |-> list_explicit_app
1196 | (head, args) => list_explicit_app head (map aux args)
1199 fun chop_fun 0 T = ([], T)
1200 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1201 chop_fun (n - 1) ran_T |>> cons dom_T
1202 | chop_fun _ _ = raise Fail "unexpected non-function"
1204 fun filter_type_args _ _ _ [] = []
1205 | filter_type_args thy s arity T_args =
1207 (* will throw "TYPE" for pseudo-constants *)
1208 val U = if s = app_op_name then
1209 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
1211 s |> Sign.the_const_type thy
1213 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1216 let val U_args = (s, U) |> Sign.const_typargs thy in
1218 |> map (fn (U, T) =>
1219 if member (op =) res_U_vars (dest_TVar U) then T
1223 handle TYPE _ => T_args
1225 fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
1227 val thy = Proof_Context.theory_of ctxt
1228 fun aux arity (CombApp (tm1, tm2)) =
1229 CombApp (aux (arity + 1) tm1, aux 0 tm2)
1230 | aux arity (CombConst (name as (s, _), T, T_args)) =
1231 (case strip_prefix_and_unascii const_prefix s of
1232 NONE => (name, T_args)
1235 val s'' = invert_const s''
1236 fun filtered_T_args false = T_args
1237 | filtered_T_args true = filter_type_args thy s'' arity T_args
1239 case type_arg_policy type_sys s'' of
1240 Explicit_Type_Args drop_args =>
1241 (name, filtered_T_args drop_args)
1242 | Mangled_Type_Args drop_args =>
1243 (mangled_const_name format type_sys (filtered_T_args drop_args)
1245 | No_Type_Args => (name, [])
1247 |> (fn (name, T_args) => CombConst (name, T, T_args))
1251 fun repair_combterm ctxt format type_sys sym_tab =
1252 not (is_setting_higher_order format type_sys)
1253 ? (introduce_explicit_apps_in_combterm sym_tab
1254 #> introduce_predicators_in_combterm sym_tab)
1255 #> enforce_type_arg_policy_in_combterm ctxt format type_sys
1256 fun repair_fact ctxt format type_sys sym_tab =
1257 update_combformula (formula_map
1258 (repair_combterm ctxt format type_sys sym_tab))
1260 (** Helper facts **)
1262 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1264 [(("COMBI", false), @{thms Meson.COMBI_def}),
1265 (("COMBK", false), @{thms Meson.COMBK_def}),
1266 (("COMBB", false), @{thms Meson.COMBB_def}),
1267 (("COMBC", false), @{thms Meson.COMBC_def}),
1268 (("COMBS", false), @{thms Meson.COMBS_def}),
1270 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1271 However, this is done so for backward compatibility: Including the
1272 equality helpers by default in Metis breaks a few existing proofs. *)
1273 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1274 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1275 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1276 (("fFalse", true), @{thms True_or_False}),
1277 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1278 (("fTrue", true), @{thms True_or_False}),
1280 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1281 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1283 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1284 by (unfold fconj_def) fast+}),
1286 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1287 by (unfold fdisj_def) fast+}),
1288 (("fimplies", false),
1289 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1290 by (unfold fimplies_def) fast+}),
1291 (("If", true), @{thms if_True if_False True_or_False})]
1292 |> map (apsnd (map zero_var_indexes))
1294 val type_tag = `make_fixed_const type_tag_name
1296 fun type_tag_idempotence_fact () =
1298 fun var s = ATerm (`I s, [])
1299 fun tag tm = ATerm (type_tag, [var "T", tm])
1300 val tagged_a = tag (var "A")
1302 Formula (type_tag_idempotence_helper_name, Axiom,
1303 AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
1304 |> close_formula_universally, simp_info, NONE)
1307 fun should_specialize_helper type_sys t =
1308 case general_type_arg_policy type_sys of
1309 Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1312 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
1313 case strip_prefix_and_unascii const_prefix s of
1316 val thy = Proof_Context.theory_of ctxt
1317 val unmangled_s = mangled_s |> unmangled_const_name
1318 fun dub_and_inst needs_fairly_sound (th, j) =
1319 ((unmangled_s ^ "_" ^ string_of_int j ^
1320 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1321 (if needs_fairly_sound then typed_helper_suffix
1322 else untyped_helper_suffix),
1324 let val t = th |> prop_of in
1325 t |> should_specialize_helper type_sys t
1327 [T] => specialize_type thy (invert_const unmangled_s, T)
1331 map_filter (make_fact ctxt format type_sys false false [])
1332 val fairly_sound = is_type_sys_fairly_sound type_sys
1335 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1336 if helper_s <> unmangled_s orelse
1337 (needs_fairly_sound andalso not fairly_sound) then
1340 ths ~~ (1 upto length ths)
1341 |> map (dub_and_inst needs_fairly_sound)
1345 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
1346 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
1349 (***************************************************************)
1350 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1351 (***************************************************************)
1353 fun set_insert (x, s) = Symtab.update (x, ()) s
1355 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1357 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1358 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1360 fun classes_of_terms get_Ts =
1361 map (map snd o get_Ts)
1362 #> List.foldl add_classes Symtab.empty
1363 #> delete_type #> Symtab.keys
1365 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
1366 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
1368 (*fold type constructors*)
1369 fun fold_type_constrs f (Type (a, Ts)) x =
1370 fold (fold_type_constrs f) Ts (f (a,x))
1371 | fold_type_constrs _ _ x = x
1373 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1374 fun add_type_constrs_in_term thy =
1376 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1377 | add (t $ u) = add t #> add u
1378 | add (Const (x as (s, _))) =
1379 if String.isPrefix skolem_const_prefix s then I
1380 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1381 | add (Abs (_, _, u)) = add u
1385 fun type_constrs_of_terms thy ts =
1386 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1388 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1391 val thy = Proof_Context.theory_of ctxt
1392 val fact_ts = facts |> map snd
1393 val presimp_consts = Meson.presimplified_consts ctxt
1394 val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
1395 val (facts, fact_names) =
1396 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1397 |> map_filter (try (apfst the))
1399 (* Remove existing facts from the conjecture, as this can dramatically
1400 boost an ATP's performance (for some reason). *)
1403 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1404 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1405 val all_ts = goal_t :: fact_ts
1406 val subs = tfree_classes_of_terms all_ts
1407 val supers = tvar_classes_of_terms all_ts
1408 val tycons = type_constrs_of_terms thy all_ts
1411 |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
1412 val (supers', arity_clauses) =
1413 if level_of_type_sys type_sys = No_Types then ([], [])
1414 else make_arity_clauses thy tycons supers
1415 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1417 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
1420 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
1421 (true, ATerm (class, [ATerm (name, [])]))
1422 | fo_literal_from_type_literal (TyLitFree (class, name)) =
1423 (true, ATerm (class, [ATerm (name, [])]))
1425 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1427 val type_pred = `make_fixed_const type_pred_name
1429 fun type_pred_combterm ctxt format type_sys T tm =
1430 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1431 |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
1433 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1434 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1435 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1436 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
1437 formula_fold pos (is_var_positively_naked_in_term name) phi false
1438 | should_predicate_on_var_in_formula _ _ _ _ = true
1440 fun mk_const_aterm format type_sys x T_args args =
1441 ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
1443 fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
1444 CombConst (type_tag, T --> T, [T])
1445 |> enforce_type_arg_policy_in_combterm ctxt format type_sys
1446 |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1447 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1448 and term_from_combterm ctxt format nonmono_Ts type_sys =
1452 val (head, args) = strip_combterm_comb u
1453 val (x as (s, _), T_args) =
1455 CombConst (name, _, T_args) => (name, T_args)
1456 | CombVar (name, _) => (name, [])
1457 | CombApp _ => raise Fail "impossible \"CombApp\""
1458 val (pos, arg_site) =
1461 (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
1462 | Eq_Arg pos => (pos, Elsewhere)
1463 | Elsewhere => (NONE, Elsewhere)
1464 val t = mk_const_aterm format type_sys x T_args
1465 (map (aux arg_site) args)
1466 val T = combtyp_of u
1468 t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
1469 tag_with_type ctxt format nonmono_Ts type_sys pos T
1474 and formula_from_combformula ctxt format nonmono_Ts type_sys
1475 should_predicate_on_var =
1478 term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1481 Simple_Types level =>
1482 homogenized_type ctxt nonmono_Ts level 0
1483 #> mangled_type format type_sys false 0 #> SOME
1485 fun do_out_of_bound_type pos phi universal (name, T) =
1486 if should_predicate_on_type ctxt nonmono_Ts type_sys
1487 (fn () => should_predicate_on_var pos phi universal name) T then
1489 |> type_pred_combterm ctxt format type_sys T
1490 |> do_term pos |> AAtom |> SOME
1493 fun do_formula pos (AQuant (q, xs, phi)) =
1495 val phi = phi |> do_formula pos
1496 val universal = Option.map (q = AExists ? not) pos
1498 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1499 | SOME T => do_bound_type T)),
1500 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1502 (fn (_, NONE) => NONE
1504 do_out_of_bound_type pos phi universal (s, T))
1508 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1509 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1512 fun bound_tvars type_sys Ts =
1513 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1514 (type_literals_for_types type_sys add_sorts_on_tvar Ts))
1516 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1517 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1518 the remote provers might care. *)
1519 fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys
1520 (j, {name, locality, kind, combformula, atomic_types}) =
1521 (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name,
1524 |> close_combformula_universally
1525 |> formula_from_combformula ctxt format nonmono_Ts type_sys
1526 should_predicate_on_var_in_formula
1527 (if exporter then NONE else SOME true)
1528 |> bound_tvars type_sys atomic_types
1529 |> close_formula_universally,
1538 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1539 : class_rel_clause) =
1540 let val ty_arg = ATerm (`I "T", []) in
1541 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1542 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
1543 AAtom (ATerm (superclass, [ty_arg]))])
1544 |> close_formula_universally, intro_info, NONE)
1547 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
1548 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
1549 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
1550 (false, ATerm (c, [ATerm (sort, [])]))
1552 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1554 Formula (arity_clause_prefix ^ name, Axiom,
1555 mk_ahorn (map (formula_from_fo_literal o apfst not
1556 o fo_literal_from_arity_literal) prem_lits)
1557 (formula_from_fo_literal
1558 (fo_literal_from_arity_literal concl_lits))
1559 |> close_formula_universally, intro_info, NONE)
1561 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
1562 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1563 Formula (conjecture_prefix ^ name, kind,
1564 formula_from_combformula ctxt format nonmono_Ts type_sys
1565 should_predicate_on_var_in_formula (SOME false)
1566 (close_combformula_universally combformula)
1567 |> bound_tvars type_sys atomic_types
1568 |> close_formula_universally, NONE, NONE)
1570 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
1571 atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
1572 |> map fo_literal_from_type_literal
1574 fun formula_line_for_free_type j lit =
1575 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1576 formula_from_fo_literal lit, NONE, NONE)
1577 fun formula_lines_for_free_types type_sys facts =
1579 val litss = map (free_type_literals type_sys) facts
1580 val lits = fold (union (op =)) litss []
1581 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1583 (** Symbol declarations **)
1585 fun should_declare_sym type_sys pred_sym s =
1586 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1588 Simple_Types _ => true
1589 | Tags (_, _, Lightweight) => true
1590 | _ => not pred_sym)
1592 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
1594 fun add_combterm in_conj tm =
1595 let val (head, args) = strip_combterm_comb tm in
1597 CombConst ((s, s'), T, T_args) =>
1598 let val pred_sym = is_pred_sym repaired_sym_tab s in
1599 if should_declare_sym type_sys pred_sym s then
1600 Symtab.map_default (s, [])
1601 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1607 #> fold (add_combterm in_conj) args
1609 fun add_fact in_conj =
1610 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1613 |> is_type_sys_fairly_sound type_sys
1614 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1617 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1618 out with monotonicity" paper presented at CADE 2011. *)
1619 fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
1620 | add_combterm_nonmonotonic_types ctxt level locality _
1621 (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1623 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1625 Noninf_Nonmono_Types =>
1626 not (is_locality_global locality) orelse
1627 not (is_type_surely_infinite ctxt T)
1628 | Fin_Nonmono_Types => is_type_surely_finite ctxt T
1629 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1630 | add_combterm_nonmonotonic_types _ _ _ _ _ = I
1631 fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
1632 : translated_formula) =
1633 formula_fold (SOME (kind <> Conjecture))
1634 (add_combterm_nonmonotonic_types ctxt level locality) combformula
1635 fun nonmonotonic_types_for_facts ctxt type_sys facts =
1636 let val level = level_of_type_sys type_sys in
1637 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1638 [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
1639 (* We must add "bool" in case the helper "True_or_False" is added
1640 later. In addition, several places in the code rely on the list of
1641 nonmonotonic types not being empty. *)
1642 |> insert_type ctxt I @{typ bool}
1647 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
1648 (s', T_args, T, pred_sym, ary, _) =
1650 val (T_arg_Ts, level) =
1652 Simple_Types level => ([], level)
1653 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1655 Decl (sym_decl_prefix ^ s, (s, s'),
1656 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1657 |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
1660 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1661 poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
1663 val (kind, maybe_negate) =
1664 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1666 val (arg_Ts, res_T) = chop_fun ary T
1667 val num_args = length arg_Ts
1669 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1671 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1672 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1673 fun should_keep_arg_type T =
1674 sym_needs_arg_types orelse
1675 not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
1677 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1679 Formula (preds_sym_formula_prefix ^ s ^
1680 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1681 CombConst ((s, s'), T, T_args)
1682 |> fold (curry (CombApp o swap)) bounds
1683 |> type_pred_combterm ctxt format type_sys res_T
1684 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1685 |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
1686 (K (K (K (K true)))) (SOME true)
1687 |> n > 1 ? bound_tvars type_sys (atyps_of T)
1688 |> close_formula_universally
1693 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1694 poly_nonmono_Ts type_sys n s
1695 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1698 lightweight_tags_sym_formula_prefix ^ s ^
1699 (if n > 1 then "_" ^ string_of_int j else "")
1700 val (kind, maybe_negate) =
1701 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1703 val (arg_Ts, res_T) = chop_fun ary T
1705 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1706 val bounds = bound_names |> map (fn name => ATerm (name, []))
1707 val cst = mk_const_aterm format type_sys (s, s') T_args
1708 val atomic_Ts = atyps_of T
1710 (if pred_sym then AConn (AIff, map AAtom tms)
1711 else AAtom (ATerm (`I tptp_equal, tms)))
1712 |> bound_tvars type_sys atomic_Ts
1713 |> close_formula_universally
1715 (* See also "should_tag_with_type". *)
1716 fun should_encode T =
1717 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1719 Tags (Polymorphic, level, Lightweight) =>
1720 level <> All_Types andalso Monomorph.typ_has_tvars T
1722 val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
1723 val add_formula_for_res =
1724 if should_encode res_T then
1725 cons (Formula (ident_base ^ "_res", kind,
1726 eq [tag_with res_T (cst bounds), cst bounds],
1730 fun add_formula_for_arg k =
1731 let val arg_T = nth arg_Ts k in
1732 if should_encode arg_T then
1733 case chop k bounds of
1734 (bounds1, bound :: bounds2) =>
1735 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
1736 eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
1739 | _ => raise Fail "expected nonempty tail"
1744 [] |> not pred_sym ? add_formula_for_res
1745 |> fold add_formula_for_arg (ary - 1 downto 0)
1748 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1750 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1751 poly_nonmono_Ts type_sys (s, decls) =
1754 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
1759 decl :: (decls' as _ :: _) =>
1760 let val T = result_type_of_decl decl in
1761 if forall (curry (type_instance ctxt o swap) T
1762 o result_type_of_decl) decls' then
1768 val n = length decls
1770 decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
1772 o result_type_of_decl)
1774 (0 upto length decls - 1, decls)
1775 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1776 nonmono_Ts poly_nonmono_Ts type_sys n s)
1778 | Tags (_, _, heaviness) =>
1782 let val n = length decls in
1783 (0 upto n - 1 ~~ decls)
1784 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1785 conj_sym_kind poly_nonmono_Ts type_sys n s)
1788 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1789 poly_nonmono_Ts type_sys sym_decl_tab =
1794 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1795 nonmono_Ts poly_nonmono_Ts type_sys)
1797 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1798 poly <> Mangled_Monomorphic andalso
1799 ((level = All_Types andalso heaviness = Lightweight) orelse
1800 level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
1801 | needs_type_tag_idempotence _ = false
1803 fun offset_of_heading_in_problem _ [] j = j
1804 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1805 if heading = needle then j
1806 else offset_of_heading_in_problem needle problem (j + length lines)
1808 val implicit_declsN = "Should-be-implicit typings"
1809 val explicit_declsN = "Explicit typings"
1810 val factsN = "Relevant facts"
1811 val class_relsN = "Class relationships"
1812 val aritiesN = "Arities"
1813 val helpersN = "Helper facts"
1814 val conjsN = "Conjectures"
1815 val free_typesN = "Type variables"
1817 val explicit_apply = NONE (* for experimental purposes *)
1819 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
1820 exporter readable_names preproc hyp_ts concl_t facts =
1822 val (format, type_sys) = choose_format [format] type_sys
1823 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1824 translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1826 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1827 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
1828 val repair = repair_fact ctxt format type_sys sym_tab
1829 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1830 val repaired_sym_tab =
1831 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1833 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
1835 val poly_nonmono_Ts =
1836 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1837 polymorphism_of_type_sys type_sys <> Polymorphic then
1840 [TVar (("'a", 0), HOLogic.typeS)]
1841 val sym_decl_lines =
1842 (conjs, helpers @ facts)
1843 |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
1844 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1845 poly_nonmono_Ts type_sys
1847 0 upto length helpers - 1 ~~ helpers
1848 |> map (formula_line_for_fact ctxt format helper_prefix I exporter
1849 poly_nonmono_Ts type_sys)
1850 |> (if needs_type_tag_idempotence type_sys then
1851 cons (type_tag_idempotence_fact ())
1854 (* Reordering these might confuse the proof reconstruction code or the SPASS
1857 [(explicit_declsN, sym_decl_lines),
1859 map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter
1860 nonmono_Ts type_sys)
1861 (0 upto length facts - 1 ~~ facts)),
1862 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1863 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1864 (helpersN, helper_lines),
1866 map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
1868 (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
1872 CNF => ensure_cnf_problem
1873 | CNF_UEQ => filter_cnf_ueq_problem
1875 |> (if is_format_typed format then
1876 declare_undeclared_syms_in_atp_problem type_decl_prefix
1880 val (problem, pool) = problem |> nice_atp_problem readable_names
1881 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
1883 map_filter (fn (j, {name, ...}) =>
1884 if String.isSuffix typed_helper_suffix name then SOME j
1886 ((helpers_offset + 1 upto helpers_offset + length helpers)
1888 fun add_sym_arity (s, {min_ary, ...} : sym_info) =
1890 case strip_prefix_and_unascii const_prefix s of
1891 SOME s => Symtab.insert (op =) (s, min_ary)
1897 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1898 offset_of_heading_in_problem conjsN problem 0,
1899 offset_of_heading_in_problem factsN problem 0,
1900 fact_names |> Vector.fromList,
1902 Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
1906 val conj_weight = 0.0
1907 val hyp_weight = 0.1
1908 val fact_min_weight = 0.2
1909 val fact_max_weight = 1.0
1910 val type_info_default_weight = 0.8
1912 fun add_term_weights weight (ATerm (s, tms)) =
1913 is_tptp_user_symbol s ? Symtab.default (s, weight)
1914 #> fold (add_term_weights weight) tms
1915 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1916 formula_fold NONE (K (add_term_weights weight)) phi
1917 | add_problem_line_weights _ _ = I
1919 fun add_conjectures_weights [] = I
1920 | add_conjectures_weights conjs =
1921 let val (hyps, conj) = split_last conjs in
1922 add_problem_line_weights conj_weight conj
1923 #> fold (add_problem_line_weights hyp_weight) hyps
1926 fun add_facts_weights facts =
1928 val num_facts = length facts
1930 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
1931 / Real.fromInt num_facts
1933 map weight_of (0 upto num_facts - 1) ~~ facts
1934 |> fold (uncurry add_problem_line_weights)
1937 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
1938 fun atp_problem_weights problem =
1939 let val get = these o AList.lookup (op =) problem in
1941 |> add_conjectures_weights (get free_typesN @ get conjsN)
1942 |> add_facts_weights (get factsN)
1943 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
1944 [explicit_declsN, class_relsN, aritiesN]
1946 |> sort (prod_ord Real.compare string_ord o pairself swap)