gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
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
18 type name = string * string
20 datatype type_literal =
21 TyLitVar of name * name |
22 TyLitFree of name * name
24 datatype arity_literal =
25 TConsLit of name * name * name list |
26 TVarLit of name * name
30 prem_lits: arity_literal list,
31 concl_lits: arity_literal}
33 type class_rel_clause =
39 CombConst of name * typ * typ list |
40 CombVar of name * typ |
41 CombApp of combterm * combterm
44 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
47 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
49 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
51 datatype type_heaviness = Heavyweight | Lightweight
54 Simple_Types of type_level |
55 Preds of polymorphism * type_level * type_heaviness |
56 Tags of polymorphism * type_level * type_heaviness
58 val bound_var_prefix : string
59 val schematic_var_prefix: string
60 val fixed_var_prefix: string
61 val tvar_prefix: string
62 val tfree_prefix: string
63 val const_prefix: string
64 val type_const_prefix: string
65 val class_prefix: string
66 val skolem_const_prefix : string
67 val old_skolem_const_prefix : string
68 val new_skolem_const_prefix : string
69 val type_decl_prefix : string
70 val sym_decl_prefix : string
71 val preds_sym_formula_prefix : string
72 val lightweight_tags_sym_formula_prefix : string
73 val fact_prefix : string
74 val conjecture_prefix : string
75 val helper_prefix : string
76 val class_rel_clause_prefix : string
77 val arity_clause_prefix : string
78 val tfree_clause_prefix : string
79 val typed_helper_suffix : string
80 val untyped_helper_suffix : string
81 val type_tag_idempotence_helper_name : string
82 val predicator_name : string
83 val app_op_name : string
84 val type_tag_name : string
85 val type_pred_name : string
86 val simple_type_prefix : string
87 val prefixed_predicator_name : string
88 val prefixed_app_op_name : string
89 val prefixed_type_tag_name : string
90 val ascii_of: string -> string
91 val unascii_of: string -> string
92 val strip_prefix_and_unascii : string -> string -> string option
93 val proxy_table : (string * (string * (thm * (string * string)))) list
94 val proxify_const : string -> (string * string) option
95 val invert_const: string -> string
96 val unproxify_const: string -> string
97 val make_bound_var : string -> string
98 val make_schematic_var : string * int -> string
99 val make_fixed_var : string -> string
100 val make_schematic_type_var : string * int -> string
101 val make_fixed_type_var : string -> string
102 val make_fixed_const : string -> string
103 val make_fixed_type_const : string -> string
104 val make_type_class : string -> string
105 val new_skolem_var_name_from_const : string -> string
106 val num_type_args : theory -> string -> int
107 val atp_irrelevant_consts : string list
108 val atp_schematic_consts_of : term -> typ list Symtab.table
109 val make_arity_clauses :
110 theory -> string list -> class list -> class list * arity_clause list
111 val make_class_rel_clauses :
112 theory -> class list -> class list -> class_rel_clause list
113 val combtyp_of : combterm -> typ
114 val strip_combterm_comb : combterm -> combterm * combterm list
115 val atyps_of : typ -> typ list
116 val combterm_from_term :
117 theory -> (string * typ) list -> term -> combterm * typ list
118 val is_locality_global : locality -> bool
119 val type_sys_from_string : string -> type_sys
120 val polymorphism_of_type_sys : type_sys -> polymorphism
121 val level_of_type_sys : type_sys -> type_level
122 val is_type_sys_virtually_sound : type_sys -> bool
123 val is_type_sys_fairly_sound : type_sys -> bool
124 val choose_format : format list -> type_sys -> format * type_sys
126 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
127 val unmangled_const_name : string -> string
128 val unmangled_const : string -> string * string fo_term list
129 val helper_table : ((string * bool) * thm list) list
130 val should_specialize_helper : type_sys -> term -> bool
131 val tfree_classes_of_terms : term list -> string list
132 val tvar_classes_of_terms : term list -> string list
133 val type_constrs_of_terms : theory -> term list -> string list
134 val prepare_atp_problem :
135 Proof.context -> format -> formula_kind -> formula_kind -> type_sys
136 -> bool -> bool -> bool -> term list -> term
137 -> ((string * locality) * term) list
138 -> string problem * string Symtab.table * int * int
139 * (string * locality) list vector * int list * int Symtab.table
140 val atp_problem_weights : string problem -> (string * real) list
143 structure ATP_Translate : ATP_TRANSLATE =
149 type name = string * string
152 val generate_useful_info = false
154 fun useful_isabelle_info s =
155 if generate_useful_info then
156 SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
160 val intro_info = useful_isabelle_info "intro"
161 val elim_info = useful_isabelle_info "elim"
162 val simp_info = useful_isabelle_info "simp"
164 val bound_var_prefix = "B_"
165 val schematic_var_prefix = "V_"
166 val fixed_var_prefix = "v_"
168 val tvar_prefix = "T_"
169 val tfree_prefix = "t_"
171 val const_prefix = "c_"
172 val type_const_prefix = "tc_"
173 val class_prefix = "cl_"
175 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
176 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
177 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
179 val type_decl_prefix = "ty_"
180 val sym_decl_prefix = "sy_"
181 val preds_sym_formula_prefix = "psy_"
182 val lightweight_tags_sym_formula_prefix = "tsy_"
183 val fact_prefix = "fact_"
184 val conjecture_prefix = "conj_"
185 val helper_prefix = "help_"
186 val class_rel_clause_prefix = "clar_"
187 val arity_clause_prefix = "arity_"
188 val tfree_clause_prefix = "tfree_"
190 val typed_helper_suffix = "_T"
191 val untyped_helper_suffix = "_U"
192 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
194 val predicator_name = "hBOOL"
195 val app_op_name = "hAPP"
196 val type_tag_name = "ti"
197 val type_pred_name = "is"
198 val simple_type_prefix = "ty_"
200 val prefixed_predicator_name = const_prefix ^ predicator_name
201 val prefixed_app_op_name = const_prefix ^ app_op_name
202 val prefixed_type_tag_name = const_prefix ^ type_tag_name
204 (* Freshness almost guaranteed! *)
205 val sledgehammer_weak_prefix = "Sledgehammer:"
207 (*Escaping of special characters.
208 Alphanumeric characters are left unchanged.
209 The character _ goes to __
210 Characters in the range ASCII space to / go to _A to _P, respectively.
211 Other characters go to _nnn where nnn is the decimal ASCII code.*)
212 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
214 fun stringN_of_int 0 _ = ""
215 | stringN_of_int k n =
216 stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
218 fun ascii_of_char c =
219 if Char.isAlphaNum c then
221 else if c = #"_" then
223 else if #" " <= c andalso c <= #"/" then
224 "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
226 (* fixed width, in case more digits follow *)
227 "_" ^ stringN_of_int 3 (Char.ord c)
229 val ascii_of = String.translate ascii_of_char
231 (** Remove ASCII armoring from names in proof files **)
233 (* We don't raise error exceptions because this code can run inside a worker
234 thread. Also, the errors are impossible. *)
237 fun un rcs [] = String.implode(rev rcs)
238 | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
239 (* Three types of _ escapes: __, _A to _P, _nnn *)
240 | un rcs (#"_" :: #"_" :: cs) = un (#"_"::rcs) cs
241 | un rcs (#"_" :: c :: cs) =
242 if #"A" <= c andalso c<= #"P" then
243 (* translation of #" " to #"/" *)
244 un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
246 let val digits = List.take (c::cs, 3) handle General.Subscript => [] in
247 case Int.fromString (String.implode digits) of
248 SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
249 | NONE => un (c:: #"_"::rcs) cs (* ERROR *)
251 | un rcs (c :: cs) = un (c :: rcs) cs
252 in un [] o String.explode end
254 (* If string s has the prefix s1, return the result of deleting it,
256 fun strip_prefix_and_unascii s1 s =
257 if String.isPrefix s1 s then
258 SOME (unascii_of (String.extract (s, size s1, NONE)))
263 [("c_False", (@{const_name False}, (@{thm fFalse_def},
264 ("fFalse", @{const_name ATP.fFalse})))),
265 ("c_True", (@{const_name True}, (@{thm fTrue_def},
266 ("fTrue", @{const_name ATP.fTrue})))),
267 ("c_Not", (@{const_name Not}, (@{thm fNot_def},
268 ("fNot", @{const_name ATP.fNot})))),
269 ("c_conj", (@{const_name conj}, (@{thm fconj_def},
270 ("fconj", @{const_name ATP.fconj})))),
271 ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
272 ("fdisj", @{const_name ATP.fdisj})))),
273 ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
274 ("fimplies", @{const_name ATP.fimplies})))),
275 ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
276 ("fequal", @{const_name ATP.fequal}))))]
278 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
280 (* Readable names for the more common symbolic functions. Do not mess with the
281 table unless you know what you are doing. *)
282 val const_trans_table =
283 [(@{type_name Product_Type.prod}, "prod"),
284 (@{type_name Sum_Type.sum}, "sum"),
285 (@{const_name False}, "False"),
286 (@{const_name True}, "True"),
287 (@{const_name Not}, "Not"),
288 (@{const_name conj}, "conj"),
289 (@{const_name disj}, "disj"),
290 (@{const_name implies}, "implies"),
291 (@{const_name HOL.eq}, "equal"),
292 (@{const_name If}, "If"),
293 (@{const_name Set.member}, "member"),
294 (@{const_name Meson.COMBI}, "COMBI"),
295 (@{const_name Meson.COMBK}, "COMBK"),
296 (@{const_name Meson.COMBB}, "COMBB"),
297 (@{const_name Meson.COMBC}, "COMBC"),
298 (@{const_name Meson.COMBS}, "COMBS")]
300 |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
302 (* Invert the table of translations between Isabelle and ATPs. *)
303 val const_trans_table_inv =
304 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
305 val const_trans_table_unprox =
307 |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
309 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
310 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
313 case Symtab.lookup const_trans_table c of
317 (*Remove the initial ' character from a type variable, if it is present*)
318 fun trim_type_var s =
319 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
320 else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
322 fun ascii_of_indexname (v,0) = ascii_of v
323 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
325 fun make_bound_var x = bound_var_prefix ^ ascii_of x
326 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
327 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
329 fun make_schematic_type_var (x,i) =
330 tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
331 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
333 (* HOL.eq MUST BE "equal" because it's built into ATPs. *)
334 fun make_fixed_const @{const_name HOL.eq} = "equal"
335 | make_fixed_const c = const_prefix ^ lookup_const c
337 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
339 fun make_type_class clas = class_prefix ^ ascii_of clas
341 fun new_skolem_var_name_from_const s =
342 let val ss = s |> space_explode Long_Name.separator in
343 nth ss (length ss - 2)
346 (* The number of type arguments of a constant, zero if it's monomorphic. For
347 (instances of) Skolem pseudoconstants, this information is encoded in the
349 fun num_type_args thy s =
350 if String.isPrefix skolem_const_prefix s then
351 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
353 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
355 (* These are either simplified away by "Meson.presimplify" (most of the time) or
356 handled specially via "fFalse", "fTrue", ..., "fequal". *)
357 val atp_irrelevant_consts =
358 [@{const_name False}, @{const_name True}, @{const_name Not},
359 @{const_name conj}, @{const_name disj}, @{const_name implies},
360 @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
362 val atp_monomorph_bad_consts =
363 atp_irrelevant_consts @
364 (* These are ignored anyway by the relevance filter (unless they appear in
365 higher-order places) but not by the monomorphizer. *)
366 [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
367 @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
368 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
370 fun add_schematic_const (x as (_, T)) =
371 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
372 val add_schematic_consts_of =
373 Term.fold_aterms (fn Const (x as (s, _)) =>
374 not (member (op =) atp_monomorph_bad_consts s)
375 ? add_schematic_const x
377 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
379 (** Definitions and functions for FOL clauses and formulas for TPTP **)
381 (* The first component is the type class; the second is a "TVar" or "TFree". *)
382 datatype type_literal =
383 TyLitVar of name * name |
384 TyLitFree of name * name
387 (** Isabelle arities **)
389 datatype arity_literal =
390 TConsLit of name * name * name list |
391 TVarLit of name * name
394 | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
396 val type_class = the_single @{sort type}
398 fun add_packed_sort tvar =
399 fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
403 prem_lits: arity_literal list,
404 concl_lits: arity_literal}
406 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
407 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
409 val tvars = gen_TVars (length args)
410 val tvars_srts = ListPair.zip (tvars, args)
413 prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
414 concl_lits = TConsLit (`make_type_class cls,
415 `make_fixed_type_const tcons,
419 fun arity_clause _ _ (_, []) = []
420 | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
421 arity_clause seen n (tcons,ars)
422 | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
423 if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
424 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ string_of_int n, ar) ::
425 arity_clause seen (n+1) (tcons,ars)
427 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
428 arity_clause (class::seen) n (tcons,ars)
430 fun multi_arity_clause [] = []
431 | multi_arity_clause ((tcons, ars) :: tc_arlists) =
432 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
434 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
435 provided its arguments have the corresponding sorts.*)
436 fun type_class_pairs thy tycons classes =
438 val alg = Sign.classes_of thy
439 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
440 fun add_class tycon class =
441 cons (class, domain_sorts tycon class)
442 handle Sorts.CLASS_ERROR _ => I
443 fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
444 in map try_classes tycons end
446 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
447 fun iter_type_class_pairs _ _ [] = ([], [])
448 | iter_type_class_pairs thy tycons classes =
450 fun maybe_insert_class s =
451 (s <> type_class andalso not (member (op =) classes s))
453 val cpairs = type_class_pairs thy tycons classes
455 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
456 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
457 in (classes' @ classes, union (op =) cpairs' cpairs) end
459 fun make_arity_clauses thy tycons =
460 iter_type_class_pairs thy tycons ##> multi_arity_clause
463 (** Isabelle class relations **)
465 type class_rel_clause =
470 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
471 fun class_pairs _ [] _ = []
472 | class_pairs thy subs supers =
474 val class_less = Sorts.class_less (Sign.classes_of thy)
475 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
476 fun add_supers sub = fold (add_super sub) supers
477 in fold add_supers subs [] end
479 fun make_class_rel_clause (sub,super) =
480 {name = sub ^ "_" ^ super,
481 subclass = `make_type_class sub,
482 superclass = `make_type_class super}
484 fun make_class_rel_clauses thy subs supers =
485 map make_class_rel_clause (class_pairs thy subs supers)
488 CombConst of name * typ * typ list |
489 CombVar of name * typ |
490 CombApp of combterm * combterm
492 fun combtyp_of (CombConst (_, T, _)) = T
493 | combtyp_of (CombVar (_, T)) = T
494 | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
496 (*gets the head of a combinator application, along with the list of arguments*)
497 fun strip_combterm_comb u =
498 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
502 fun atyps_of T = fold_atyps (insert (op =)) T []
504 fun new_skolem_const_name s num_T_args =
505 [new_skolem_const_prefix, s, string_of_int num_T_args]
506 |> space_implode Long_Name.separator
508 (* Converts a term (with combinators) into a combterm. Also accumulates sort
510 fun combterm_from_term thy bs (P $ Q) =
512 val (P', P_atomics_Ts) = combterm_from_term thy bs P
513 val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
514 in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
515 | combterm_from_term thy _ (Const (c, T)) =
518 (if String.isPrefix old_skolem_const_prefix c then
519 [] |> Term.add_tvarsT T |> map TVar
521 (c, T) |> Sign.const_typargs thy)
522 val c' = CombConst (`make_fixed_const c, T, tvar_list)
523 in (c', atyps_of T) end
524 | combterm_from_term _ _ (Free (v, T)) =
525 (CombConst (`make_fixed_var v, T, []), atyps_of T)
526 | combterm_from_term _ _ (Var (v as (s, _), T)) =
527 (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
529 val Ts = T |> strip_type |> swap |> op ::
530 val s' = new_skolem_const_name s (length Ts)
531 in CombConst (`make_fixed_const s', T, Ts) end
533 CombVar ((make_schematic_var v, s), T), atyps_of T)
534 | combterm_from_term _ bs (Bound j) =
536 |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
537 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
540 General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
543 (* (quasi-)underapproximation of the truth *)
544 fun is_locality_global Local = false
545 | is_locality_global Assum = false
546 | is_locality_global Chained = false
547 | is_locality_global _ = true
549 datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
550 datatype type_level =
551 All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
553 datatype type_heaviness = Heavyweight | Lightweight
556 Simple_Types of type_level |
557 Preds of polymorphism * type_level * type_heaviness |
558 Tags of polymorphism * type_level * type_heaviness
560 fun try_unsuffixes ss s =
561 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
563 fun type_sys_from_string s =
564 (case try (unprefix "poly_") s of
565 SOME s => (SOME Polymorphic, s)
567 case try (unprefix "mono_") s of
568 SOME s => (SOME Monomorphic, s)
570 case try (unprefix "mangled_") s of
571 SOME s => (SOME Mangled_Monomorphic, s)
574 (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
575 case try_unsuffixes ["?", "_query"] s of
576 SOME s => (Noninf_Nonmono_Types, s)
578 case try_unsuffixes ["!", "_bang"] s of
579 SOME s => (Fin_Nonmono_Types, s)
580 | NONE => (All_Types, s))
582 case try (unsuffix "_heavy") s of
583 SOME s => (Heavyweight, s)
584 | NONE => (Lightweight, s))
585 |> (fn (poly, (level, (heaviness, core))) =>
586 case (core, (poly, level, heaviness)) of
587 ("simple", (NONE, _, Lightweight)) => Simple_Types level
588 | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
589 | ("tags", (SOME Polymorphic, _, _)) =>
590 Tags (Polymorphic, level, heaviness)
591 | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
592 | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
593 Preds (poly, Const_Arg_Types, Lightweight)
594 | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
595 Preds (Polymorphic, No_Types, Lightweight)
596 | _ => raise Same.SAME)
597 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
599 fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
600 | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
601 | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
603 fun level_of_type_sys (Simple_Types level) = level
604 | level_of_type_sys (Preds (_, level, _)) = level
605 | level_of_type_sys (Tags (_, level, _)) = level
607 fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
608 | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
609 | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
611 fun is_type_level_virtually_sound level =
612 level = All_Types orelse level = Noninf_Nonmono_Types
613 val is_type_sys_virtually_sound =
614 is_type_level_virtually_sound o level_of_type_sys
616 fun is_type_level_fairly_sound level =
617 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
618 val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
620 fun is_setting_higher_order THF (Simple_Types _) = true
621 | is_setting_higher_order _ _ = false
623 fun choose_format formats (Simple_Types level) =
624 if member (op =) formats THF then (THF, Simple_Types level)
625 else if member (op =) formats TFF then (TFF, Simple_Types level)
626 else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
627 | choose_format formats type_sys =
630 (CNF_UEQ, case type_sys of
632 (if is_type_sys_fairly_sound type_sys then Tags else Preds)
635 | format => (format, type_sys))
637 type translated_formula =
641 combformula: (name, typ, combterm) formula,
642 atomic_types: typ list}
644 fun update_combformula f ({name, locality, kind, combformula, atomic_types}
645 : translated_formula) =
646 {name = name, locality = locality, kind = kind, combformula = f combformula,
647 atomic_types = atomic_types} : translated_formula
649 fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
651 val type_instance = Sign.typ_instance o Proof_Context.theory_of
653 fun insert_type ctxt get_T x xs =
654 let val T = get_T x in
655 if exists (curry (type_instance ctxt) T o get_T) xs then xs
656 else x :: filter_out (curry (type_instance ctxt o swap) T o get_T) xs
659 (* The Booleans indicate whether all type arguments should be kept. *)
660 datatype type_arg_policy =
661 Explicit_Type_Args of bool |
662 Mangled_Type_Args of bool |
665 fun should_drop_arg_type_args (Simple_Types _) =
666 false (* since TFF doesn't support overloading *)
667 | should_drop_arg_type_args type_sys =
668 level_of_type_sys type_sys = All_Types andalso
669 heaviness_of_type_sys type_sys = Heavyweight
671 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
672 | general_type_arg_policy type_sys =
673 if level_of_type_sys type_sys = No_Types then
675 else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
676 Mangled_Type_Args (should_drop_arg_type_args type_sys)
678 Explicit_Type_Args (should_drop_arg_type_args type_sys)
680 fun type_arg_policy type_sys s =
681 if s = @{const_name HOL.eq} orelse
682 (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
684 else if s = type_tag_name then
685 Explicit_Type_Args false
687 general_type_arg_policy type_sys
689 (*Make literals for sorted type variables*)
690 fun generic_add_sorts_on_type (_, []) = I
691 | generic_add_sorts_on_type ((x, i), s :: ss) =
692 generic_add_sorts_on_type ((x, i), ss)
693 #> (if s = the_single @{sort HOL.type} then
696 insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
698 insert (op =) (TyLitVar (`make_type_class s,
699 (make_schematic_type_var (x, i), x))))
700 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
701 | add_sorts_on_tfree _ = I
702 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
703 | add_sorts_on_tvar _ = I
705 fun type_literals_for_types type_sys add_sorts_on_typ Ts =
706 [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
708 fun mk_aconns c phis =
709 let val (phis', phi') = split_last phis in
710 fold_rev (mk_aconn c) phis' phi'
712 fun mk_ahorn [] phi = phi
713 | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
714 fun mk_aquant _ [] phi = phi
715 | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
716 if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
717 | mk_aquant q xs phi = AQuant (q, xs, phi)
719 fun close_universally atom_vars phi =
721 fun formula_vars bounds (AQuant (_, xs, phi)) =
722 formula_vars (map fst xs @ bounds) phi
723 | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
724 | formula_vars bounds (AAtom tm) =
725 union (op =) (atom_vars tm []
726 |> filter_out (member (op =) bounds o fst))
727 in mk_aquant AForall (formula_vars [] phi []) phi end
729 fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
730 | combterm_vars (CombConst _) = I
731 | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
732 fun close_combformula_universally phi = close_universally combterm_vars phi
734 fun term_vars (ATerm (name as (s, _), tms)) =
735 is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
736 fun close_formula_universally phi = close_universally term_vars phi
738 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
739 val homo_infinite_type = Type (homo_infinite_type_name, [])
741 fun fo_term_from_typ format type_sys =
743 fun term (Type (s, Ts)) =
744 ATerm (case (is_setting_higher_order format type_sys, s) of
745 (true, @{type_name bool}) => `I tptp_bool_type
746 | (true, @{type_name fun}) => `I tptp_fun_type
747 | _ => if s = homo_infinite_type_name andalso
748 (format = TFF orelse format = THF) then
749 `I tptp_individual_type
751 `make_fixed_type_const s,
753 | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
754 | term (TVar ((x as (s, _)), _)) =
755 ATerm ((make_schematic_type_var x, s), [])
758 fun fo_term_for_type_arg format type_sys T =
759 if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
761 (* This shouldn't clash with anything else. *)
762 val mangled_type_sep = "\000"
764 fun generic_mangled_type_name f (ATerm (name, [])) = f name
765 | generic_mangled_type_name f (ATerm (name, tys)) =
766 f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
769 val bool_atype = AType (`I tptp_bool_type)
771 fun make_simple_type s =
772 if s = tptp_bool_type orelse s = tptp_fun_type orelse
773 s = tptp_individual_type then
776 simple_type_prefix ^ ascii_of s
778 fun ho_type_from_fo_term format type_sys pred_sym ary =
781 AType ((make_simple_type (generic_mangled_type_name fst ty),
782 generic_mangled_type_name snd ty))
783 fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
784 fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
785 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
786 fun to_ho (ty as ATerm ((s, _), tys)) =
787 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
788 in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
790 fun mangled_type format type_sys pred_sym ary =
791 ho_type_from_fo_term format type_sys pred_sym ary
792 o fo_term_from_typ format type_sys
794 fun mangled_const_name format type_sys T_args (s, s') =
796 val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
797 fun type_suffix f g =
798 fold_rev (curry (op ^) o g o prefix mangled_type_sep
799 o generic_mangled_type_name f) ty_args ""
800 in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
802 val parse_mangled_ident =
803 Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
805 fun parse_mangled_type x =
807 -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
809 and parse_mangled_types x =
810 (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
812 fun unmangled_type s =
813 s |> suffix ")" |> raw_explode
814 |> Scan.finite Symbol.stopper
815 (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
816 quote s)) parse_mangled_type))
819 val unmangled_const_name = space_explode mangled_type_sep #> hd
820 fun unmangled_const s =
821 let val ss = space_explode mangled_type_sep s in
822 (hd ss, map unmangled_type (tl ss))
825 fun introduce_proxies format type_sys =
827 fun intro top_level (CombApp (tm1, tm2)) =
828 CombApp (intro top_level tm1, intro false tm2)
829 | intro top_level (CombConst (name as (s, _), T, T_args)) =
830 (case proxify_const s of
832 if top_level orelse is_setting_higher_order format type_sys then
833 case (top_level, s) of
834 (_, "c_False") => (`I tptp_false, [])
835 | (_, "c_True") => (`I tptp_true, [])
836 | (false, "c_Not") => (`I tptp_not, [])
837 | (false, "c_conj") => (`I tptp_and, [])
838 | (false, "c_disj") => (`I tptp_or, [])
839 | (false, "c_implies") => (`I tptp_implies, [])
841 if is_tptp_equal s then (`I tptp_equal, [])
842 else (proxy_base |>> prefix const_prefix, T_args)
845 (proxy_base |>> prefix const_prefix, T_args)
846 | NONE => (name, T_args))
847 |> (fn (name, T_args) => CombConst (name, T, T_args))
851 fun combformula_from_prop thy format type_sys eq_as_iff =
853 fun do_term bs t atomic_types =
854 combterm_from_term thy bs (Envir.eta_contract t)
855 |>> (introduce_proxies format type_sys #> AAtom)
856 ||> union (op =) atomic_types
857 fun do_quant bs q s T t' =
858 let val s = singleton (Name.variant_list (map fst bs)) s in
859 do_formula ((s, T) :: bs) t'
860 #>> mk_aquant q [(`make_bound_var s, SOME T)]
862 and do_conn bs c t1 t2 =
863 do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
864 and do_formula bs t =
866 @{const Trueprop} $ t1 => do_formula bs t1
867 | @{const Not} $ t1 => do_formula bs t1 #>> mk_anot
868 | Const (@{const_name All}, _) $ Abs (s, T, t') =>
869 do_quant bs AForall s T t'
870 | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
871 do_quant bs AExists s T t'
872 | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
873 | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
874 | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
875 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
876 if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t
880 fun presimplify_term _ [] t = t
881 | presimplify_term ctxt presimp_consts t =
882 t |> exists_Const (member (op =) presimp_consts o fst) t
883 ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
884 #> Meson.presimplify ctxt
887 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
888 fun conceal_bounds Ts t =
889 subst_bounds (map (Free o apfst concealed_bound_name)
890 (0 upto length Ts - 1 ~~ Ts), t)
891 fun reveal_bounds Ts =
892 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
893 (0 upto length Ts - 1 ~~ Ts))
895 fun is_fun_equality (@{const_name HOL.eq},
896 Type (_, [Type (@{type_name fun}, _), _])) = true
897 | is_fun_equality _ = false
899 fun extensionalize_term ctxt t =
900 if exists_Const is_fun_equality t then
901 let val thy = Proof_Context.theory_of ctxt in
902 t |> cterm_of thy |> Meson.extensionalize_conv ctxt
903 |> prop_of |> Logic.dest_equals |> snd
908 fun introduce_combinators_in_term ctxt kind t =
909 let val thy = Proof_Context.theory_of ctxt in
910 if Meson.is_fol_term thy t then
916 @{const Not} $ t1 => @{const Not} $ aux Ts t1
917 | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
918 t0 $ Abs (s, T, aux (T :: Ts) t')
919 | (t0 as Const (@{const_name All}, _)) $ t1 =>
920 aux Ts (t0 $ eta_expand Ts t1 1)
921 | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
922 t0 $ Abs (s, T, aux (T :: Ts) t')
923 | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
924 aux Ts (t0 $ eta_expand Ts t1 1)
925 | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
926 | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
927 | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
928 | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
930 t0 $ aux Ts t1 $ aux Ts t2
931 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
934 t |> conceal_bounds Ts
935 |> Envir.eta_contract
937 |> Meson_Clausify.introduce_combinators_in_cterm
938 |> prop_of |> Logic.dest_equals |> snd
940 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
941 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
943 (* A type variable of sort "{}" will make abstraction fail. *)
944 if kind = Conjecture then HOLogic.false_const
945 else HOLogic.true_const
948 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
949 same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
952 fun aux (t $ u) = aux t $ aux u
953 | aux (Abs (s, T, t)) = Abs (s, T, aux t)
954 | aux (Var ((s, i), T)) =
955 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
957 in t |> exists_subterm is_Var t ? aux end
959 fun preprocess_prop ctxt presimp_consts kind t =
961 val thy = Proof_Context.theory_of ctxt
962 val t = t |> Envir.beta_eta_contract
963 |> transform_elim_prop
964 |> Object_Logic.atomize_term thy
965 val need_trueprop = (fastype_of t = @{typ bool})
967 t |> need_trueprop ? HOLogic.mk_Trueprop
968 |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
969 |> extensionalize_term ctxt
970 |> presimplify_term ctxt presimp_consts
971 |> perhaps (try (HOLogic.dest_Trueprop))
972 |> introduce_combinators_in_term ctxt kind
975 (* making fact and conjecture formulas *)
976 fun make_formula thy format type_sys eq_as_iff name loc kind t =
978 val (combformula, atomic_types) =
979 combformula_from_prop thy format type_sys eq_as_iff t []
981 {name = name, locality = loc, kind = kind, combformula = combformula,
982 atomic_types = atomic_types}
985 fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
987 let val thy = Proof_Context.theory_of ctxt in
988 case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
989 |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
991 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
992 if s = tptp_true then NONE else SOME formula
993 | formula => SOME formula
996 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
998 val thy = Proof_Context.theory_of ctxt
999 val last = length ts - 1
1001 map2 (fn j => fn t =>
1003 val (kind, maybe_negate) =
1008 if prem_kind = Conjecture then update_combformula mk_anot
1012 (preprocess_prop ctxt presimp_consts kind #> freeze_term)
1013 |> make_formula thy format type_sys (format <> CNF)
1014 (string_of_int j) Local kind
1020 (** Finite and infinite type inference **)
1022 fun deep_freeze_atyp (TVar (_, S)) = TFree ("v", S)
1023 | deep_freeze_atyp T = T
1024 val deep_freeze_type = map_atyps deep_freeze_atyp
1026 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
1027 dangerous because their "exhaust" properties can easily lead to unsound ATP
1028 proofs. On the other hand, all HOL infinite types can be given the same
1029 models in first-order logic (via Löwenheim-Skolem). *)
1031 fun should_encode_type ctxt (nonmono_Ts as _ :: _) _ T =
1032 exists (curry (type_instance ctxt) (deep_freeze_type T)) nonmono_Ts
1033 | should_encode_type _ _ All_Types _ = true
1034 | should_encode_type ctxt _ Fin_Nonmono_Types T = is_type_surely_finite ctxt T
1035 | should_encode_type _ _ _ _ = false
1037 fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness))
1038 should_predicate_on_var T =
1039 (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso
1040 should_encode_type ctxt nonmono_Ts level T
1041 | should_predicate_on_type _ _ _ _ _ = false
1043 fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
1044 String.isPrefix bound_var_prefix s
1045 | is_var_or_bound_var (CombVar _) = true
1046 | is_var_or_bound_var _ = false
1049 Top_Level of bool option |
1050 Eq_Arg of bool option |
1053 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
1054 | should_tag_with_type ctxt nonmono_Ts (Tags (poly, level, heaviness)) site
1057 Heavyweight => should_encode_type ctxt nonmono_Ts level T
1059 case (site, is_var_or_bound_var u) of
1060 (Eq_Arg pos, true) =>
1061 (* The first disjunct prevents a subtle soundness issue explained in
1062 Blanchette's Ph.D. thesis. See also
1063 "formula_lines_for_lightweight_tags_sym_decl". *)
1064 (pos <> SOME false andalso poly = Polymorphic andalso
1065 level <> All_Types andalso heaviness = Lightweight andalso
1066 exists (fn T' => type_instance ctxt (T', T)) nonmono_Ts) orelse
1067 should_encode_type ctxt nonmono_Ts level T
1069 | should_tag_with_type _ _ _ _ _ _ = false
1071 fun homogenized_type ctxt nonmono_Ts level =
1073 val should_encode = should_encode_type ctxt nonmono_Ts level
1074 fun homo 0 T = if should_encode T then T else homo_infinite_type
1075 | homo ary (Type (@{type_name fun}, [T1, T2])) =
1076 homo 0 T1 --> homo (ary - 1) T2
1077 | homo _ _ = raise Fail "expected function type"
1080 (** "hBOOL" and "hAPP" **)
1083 {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
1085 fun add_combterm_syms_to_table ctxt explicit_apply =
1087 fun consider_var_arity const_T var_T max_ary =
1090 if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
1091 type_instance ctxt (T, var_T) then
1094 iter (ary + 1) (range_type T)
1095 in iter 0 const_T end
1096 fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1097 if explicit_apply = NONE andalso
1098 (can dest_funT T orelse T = @{typ bool}) then
1100 val bool_vars' = bool_vars orelse body_type T = @{typ bool}
1101 fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
1102 {pred_sym = pred_sym andalso not bool_vars',
1103 min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
1104 max_ary = max_ary, types = types}
1106 fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1108 if bool_vars' = bool_vars andalso
1109 pointer_eq (fun_var_Ts', fun_var_Ts) then
1112 ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
1116 fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
1117 let val (head, args) = strip_combterm_comb tm in
1119 CombConst ((s, _), T, _) =>
1120 if String.isPrefix bound_var_prefix s then
1121 add_var_or_bound_var T accum
1123 let val ary = length args in
1124 ((bool_vars, fun_var_Ts),
1125 case Symtab.lookup sym_tab s of
1126 SOME {pred_sym, min_ary, max_ary, types} =>
1129 pred_sym andalso top_level andalso not bool_vars
1130 val types' = types |> insert_type ctxt I T
1132 if is_some explicit_apply orelse
1133 pointer_eq (types', types) then
1136 fold (consider_var_arity T) fun_var_Ts min_ary
1138 Symtab.update (s, {pred_sym = pred_sym,
1139 min_ary = Int.min (ary, min_ary),
1140 max_ary = Int.max (ary, max_ary),
1146 val pred_sym = top_level andalso not bool_vars
1148 case explicit_apply of
1151 | NONE => fold (consider_var_arity T) fun_var_Ts ary
1153 Symtab.update_new (s, {pred_sym = pred_sym,
1154 min_ary = min_ary, max_ary = ary,
1159 | CombVar (_, T) => add_var_or_bound_var T accum
1161 |> fold (add false) args
1164 fun add_fact_syms_to_table ctxt explicit_apply =
1165 fact_lift (formula_fold NONE
1166 (K (add_combterm_syms_to_table ctxt explicit_apply)))
1168 val default_sym_tab_entries : (string * sym_info) list =
1169 (prefixed_predicator_name,
1170 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
1171 ([tptp_false, tptp_true]
1172 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
1173 ([tptp_equal, tptp_old_equal]
1174 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
1176 fun sym_table_for_facts ctxt explicit_apply facts =
1177 ((false, []), Symtab.empty)
1178 |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
1179 |> fold Symtab.update default_sym_tab_entries
1181 fun min_arity_of sym_tab s =
1182 case Symtab.lookup sym_tab s of
1183 SOME ({min_ary, ...} : sym_info) => min_ary
1185 case strip_prefix_and_unascii const_prefix s of
1187 let val s = s |> unmangled_const_name |> invert_const in
1188 if s = predicator_name then 1
1189 else if s = app_op_name then 2
1190 else if s = type_pred_name then 1
1195 (* True if the constant ever appears outside of the top-level position in
1196 literals, or if it appears with different arities (e.g., because of different
1197 type instantiations). If false, the constant always receives all of its
1198 arguments and is used as a predicate. *)
1199 fun is_pred_sym sym_tab s =
1200 case Symtab.lookup sym_tab s of
1201 SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
1202 pred_sym andalso min_ary = max_ary
1205 val predicator_combconst =
1206 CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
1207 fun predicator tm = CombApp (predicator_combconst, tm)
1209 fun introduce_predicators_in_combterm sym_tab tm =
1210 case strip_combterm_comb tm of
1211 (CombConst ((s, _), _, _), _) =>
1212 if is_pred_sym sym_tab s then tm else predicator tm
1213 | _ => predicator tm
1215 fun list_app head args = fold (curry (CombApp o swap)) args head
1217 val app_op = `make_fixed_const app_op_name
1219 fun explicit_app arg head =
1221 val head_T = combtyp_of head
1222 val (arg_T, res_T) = dest_funT head_T
1224 CombConst (app_op, head_T --> head_T, [arg_T, res_T])
1225 in list_app explicit_app [head, arg] end
1226 fun list_explicit_app head args = fold explicit_app args head
1228 fun introduce_explicit_apps_in_combterm sym_tab =
1231 case strip_combterm_comb tm of
1232 (head as CombConst ((s, _), _, _), args) =>
1234 |> chop (min_arity_of sym_tab s)
1236 |-> list_explicit_app
1237 | (head, args) => list_explicit_app head (map aux args)
1240 fun chop_fun 0 T = ([], T)
1241 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
1242 chop_fun (n - 1) ran_T |>> cons dom_T
1243 | chop_fun _ _ = raise Fail "unexpected non-function"
1245 fun filter_type_args _ _ _ [] = []
1246 | filter_type_args thy s arity T_args =
1248 (* will throw "TYPE" for pseudo-constants *)
1249 val U = if s = app_op_name then
1250 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
1252 s |> Sign.the_const_type thy
1254 case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
1257 let val U_args = (s, U) |> Sign.const_typargs thy in
1259 |> map (fn (U, T) =>
1260 if member (op =) res_U_vars (dest_TVar U) then T
1264 handle TYPE _ => T_args
1266 fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
1268 val thy = Proof_Context.theory_of ctxt
1269 fun aux arity (CombApp (tm1, tm2)) =
1270 CombApp (aux (arity + 1) tm1, aux 0 tm2)
1271 | aux arity (CombConst (name as (s, _), T, T_args)) =
1272 (case strip_prefix_and_unascii const_prefix s of
1273 NONE => (name, T_args)
1276 val s'' = invert_const s''
1277 fun filtered_T_args false = T_args
1278 | filtered_T_args true = filter_type_args thy s'' arity T_args
1280 case type_arg_policy type_sys s'' of
1281 Explicit_Type_Args drop_args =>
1282 (name, filtered_T_args drop_args)
1283 | Mangled_Type_Args drop_args =>
1284 (mangled_const_name format type_sys (filtered_T_args drop_args)
1286 | No_Type_Args => (name, [])
1288 |> (fn (name, T_args) => CombConst (name, T, T_args))
1292 fun repair_combterm ctxt format type_sys sym_tab =
1293 not (is_setting_higher_order format type_sys)
1294 ? (introduce_explicit_apps_in_combterm sym_tab
1295 #> introduce_predicators_in_combterm sym_tab)
1296 #> enforce_type_arg_policy_in_combterm ctxt format type_sys
1297 fun repair_fact ctxt format type_sys sym_tab =
1298 update_combformula (formula_map
1299 (repair_combterm ctxt format type_sys sym_tab))
1301 (** Helper facts **)
1303 (* The Boolean indicates that a fairly sound type encoding is needed. *)
1305 [(("COMBI", false), @{thms Meson.COMBI_def}),
1306 (("COMBK", false), @{thms Meson.COMBK_def}),
1307 (("COMBB", false), @{thms Meson.COMBB_def}),
1308 (("COMBC", false), @{thms Meson.COMBC_def}),
1309 (("COMBS", false), @{thms Meson.COMBS_def}),
1311 (* This is a lie: Higher-order equality doesn't need a sound type encoding.
1312 However, this is done so for backward compatibility: Including the
1313 equality helpers by default in Metis breaks a few existing proofs. *)
1314 @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1315 fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1316 (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
1317 (("fFalse", true), @{thms True_or_False}),
1318 (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
1319 (("fTrue", true), @{thms True_or_False}),
1321 @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
1322 fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
1324 @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
1325 by (unfold fconj_def) fast+}),
1327 @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
1328 by (unfold fdisj_def) fast+}),
1329 (("fimplies", false),
1330 @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
1331 by (unfold fimplies_def) fast+}),
1332 (("If", true), @{thms if_True if_False True_or_False})]
1333 |> map (apsnd (map zero_var_indexes))
1335 val type_tag = `make_fixed_const type_tag_name
1337 fun type_tag_idempotence_fact () =
1339 fun var s = ATerm (`I s, [])
1340 fun tag tm = ATerm (type_tag, [var "T", tm])
1341 val tagged_a = tag (var "A")
1343 Formula (type_tag_idempotence_helper_name, Axiom,
1344 AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
1345 |> close_formula_universally, simp_info, NONE)
1348 fun should_specialize_helper type_sys t =
1349 case general_type_arg_policy type_sys of
1350 Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1353 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
1354 case strip_prefix_and_unascii const_prefix s of
1357 val thy = Proof_Context.theory_of ctxt
1358 val unmangled_s = mangled_s |> unmangled_const_name
1359 fun dub_and_inst needs_fairly_sound (th, j) =
1360 ((unmangled_s ^ "_" ^ string_of_int j ^
1361 (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1362 (if needs_fairly_sound then typed_helper_suffix
1363 else untyped_helper_suffix),
1365 let val t = th |> prop_of in
1366 t |> should_specialize_helper type_sys t
1368 [T] => specialize_type thy (invert_const unmangled_s, T)
1372 map_filter (make_fact ctxt format type_sys false false [])
1373 val fairly_sound = is_type_sys_fairly_sound type_sys
1376 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1377 if helper_s <> unmangled_s orelse
1378 (needs_fairly_sound andalso not fairly_sound) then
1381 ths ~~ (1 upto length ths)
1382 |> map (dub_and_inst needs_fairly_sound)
1386 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
1387 Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
1390 (***************************************************************)
1391 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1392 (***************************************************************)
1394 fun set_insert (x, s) = Symtab.update (x, ()) s
1396 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
1398 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
1399 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
1401 fun classes_of_terms get_Ts =
1402 map (map snd o get_Ts)
1403 #> List.foldl add_classes Symtab.empty
1404 #> delete_type #> Symtab.keys
1406 val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
1407 val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
1409 (*fold type constructors*)
1410 fun fold_type_constrs f (Type (a, Ts)) x =
1411 fold (fold_type_constrs f) Ts (f (a,x))
1412 | fold_type_constrs _ _ x = x
1414 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
1415 fun add_type_constrs_in_term thy =
1417 fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
1418 | add (t $ u) = add t #> add u
1419 | add (Const (x as (s, _))) =
1420 if String.isPrefix skolem_const_prefix s then I
1421 else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
1422 | add (Abs (_, _, u)) = add u
1426 fun type_constrs_of_terms thy ts =
1427 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1429 fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1432 val thy = Proof_Context.theory_of ctxt
1433 val fact_ts = facts |> map snd
1434 val presimp_consts = Meson.presimplified_consts ctxt
1435 val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
1436 val (facts, fact_names) =
1437 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1438 |> map_filter (try (apfst the))
1440 (* Remove existing facts from the conjecture, as this can dramatically
1441 boost an ATP's performance (for some reason). *)
1444 |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
1445 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1446 val all_ts = goal_t :: fact_ts
1447 val subs = tfree_classes_of_terms all_ts
1448 val supers = tvar_classes_of_terms all_ts
1449 val tycons = type_constrs_of_terms thy all_ts
1452 |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
1453 val (supers', arity_clauses) =
1454 if level_of_type_sys type_sys = No_Types then ([], [])
1455 else make_arity_clauses thy tycons supers
1456 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1458 (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
1461 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
1462 (true, ATerm (class, [ATerm (name, [])]))
1463 | fo_literal_from_type_literal (TyLitFree (class, name)) =
1464 (true, ATerm (class, [ATerm (name, [])]))
1466 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
1468 val type_pred = `make_fixed_const type_pred_name
1470 fun type_pred_combterm ctxt format type_sys T tm =
1471 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1472 |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
1474 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1475 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1476 accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
1477 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
1478 | is_var_nonmonotonic_in_formula pos phi _ name =
1479 formula_fold pos (is_var_positively_naked_in_term name) phi false
1481 fun mk_const_aterm format type_sys x T_args args =
1482 ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
1484 fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
1485 CombConst (type_tag, T --> T, [T])
1486 |> enforce_type_arg_policy_in_combterm ctxt format type_sys
1487 |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1488 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1489 and term_from_combterm ctxt format nonmono_Ts type_sys =
1493 val (head, args) = strip_combterm_comb u
1494 val (x as (s, _), T_args) =
1496 CombConst (name, _, T_args) => (name, T_args)
1497 | CombVar (name, _) => (name, [])
1498 | CombApp _ => raise Fail "impossible \"CombApp\""
1499 val (pos, arg_site) =
1502 (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
1503 | Eq_Arg pos => (pos, Elsewhere)
1504 | Elsewhere => (NONE, Elsewhere)
1505 val t = mk_const_aterm format type_sys x T_args
1506 (map (aux arg_site) args)
1507 val T = combtyp_of u
1509 t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
1510 tag_with_type ctxt format nonmono_Ts type_sys pos T
1515 and formula_from_combformula ctxt format nonmono_Ts type_sys
1516 should_predicate_on_var =
1519 term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1522 Simple_Types level =>
1523 homogenized_type ctxt nonmono_Ts level 0
1524 #> mangled_type format type_sys false 0 #> SOME
1526 fun do_out_of_bound_type pos phi universal (name, T) =
1527 if should_predicate_on_type ctxt nonmono_Ts type_sys
1528 (fn () => should_predicate_on_var pos phi universal name) T then
1530 |> type_pred_combterm ctxt format type_sys T
1531 |> do_term pos |> AAtom |> SOME
1534 fun do_formula pos (AQuant (q, xs, phi)) =
1536 val phi = phi |> do_formula pos
1537 val universal = Option.map (q = AExists ? not) pos
1539 AQuant (q, xs |> map (apsnd (fn NONE => NONE
1540 | SOME T => do_bound_type T)),
1541 (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
1543 (fn (_, NONE) => NONE
1545 do_out_of_bound_type pos phi universal (s, T))
1549 | do_formula pos (AConn conn) = aconn_map pos do_formula conn
1550 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1551 in do_formula o SOME end
1553 fun bound_tvars type_sys Ts =
1554 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1555 (type_literals_for_types type_sys add_sorts_on_tvar Ts))
1557 fun formula_for_fact ctxt format nonmono_Ts type_sys
1558 ({combformula, atomic_types, ...} : translated_formula) =
1560 |> close_combformula_universally
1561 |> formula_from_combformula ctxt format nonmono_Ts type_sys
1562 is_var_nonmonotonic_in_formula true
1563 |> bound_tvars type_sys atomic_types
1564 |> close_formula_universally
1566 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1567 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1568 the remote provers might care. *)
1569 fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
1570 (j, formula as {name, locality, kind, ...}) =
1571 Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
1573 kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
1580 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
1581 : class_rel_clause) =
1582 let val ty_arg = ATerm (`I "T", []) in
1583 Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
1584 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
1585 AAtom (ATerm (superclass, [ty_arg]))])
1586 |> close_formula_universally, intro_info, NONE)
1589 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
1590 (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
1591 | fo_literal_from_arity_literal (TVarLit (c, sort)) =
1592 (false, ATerm (c, [ATerm (sort, [])]))
1594 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
1596 Formula (arity_clause_prefix ^ ascii_of name, Axiom,
1597 mk_ahorn (map (formula_from_fo_literal o apfst not
1598 o fo_literal_from_arity_literal) prem_lits)
1599 (formula_from_fo_literal
1600 (fo_literal_from_arity_literal concl_lits))
1601 |> close_formula_universally, intro_info, NONE)
1603 fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
1604 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1605 Formula (conjecture_prefix ^ name, kind,
1606 formula_from_combformula ctxt format nonmono_Ts type_sys
1607 is_var_nonmonotonic_in_formula false
1608 (close_combformula_universally combformula)
1609 |> bound_tvars type_sys atomic_types
1610 |> close_formula_universally, NONE, NONE)
1612 fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
1613 atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
1614 |> map fo_literal_from_type_literal
1616 fun formula_line_for_free_type j lit =
1617 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1618 formula_from_fo_literal lit, NONE, NONE)
1619 fun formula_lines_for_free_types type_sys facts =
1621 val litss = map (free_type_literals type_sys) facts
1622 val lits = fold (union (op =)) litss []
1623 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1625 (** Symbol declarations **)
1627 fun should_declare_sym type_sys pred_sym s =
1628 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1630 Simple_Types _ => true
1631 | Tags (_, _, Lightweight) => true
1632 | _ => not pred_sym)
1634 fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
1636 fun add_combterm in_conj tm =
1637 let val (head, args) = strip_combterm_comb tm in
1639 CombConst ((s, s'), T, T_args) =>
1640 let val pred_sym = is_pred_sym repaired_sym_tab s in
1641 if should_declare_sym type_sys pred_sym s then
1642 Symtab.map_default (s, [])
1643 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1649 #> fold (add_combterm in_conj) args
1651 fun add_fact in_conj =
1652 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1655 |> is_type_sys_fairly_sound type_sys
1656 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1659 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
1660 out with monotonicity" paper presented at CADE 2011. *)
1661 fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
1662 | add_combterm_nonmonotonic_types ctxt level locality _
1663 (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1665 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1667 Noninf_Nonmono_Types =>
1668 not (is_locality_global locality) orelse
1669 not (is_type_surely_infinite ctxt T)
1670 | Fin_Nonmono_Types => is_type_surely_finite ctxt T
1671 | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
1672 | add_combterm_nonmonotonic_types _ _ _ _ _ = I
1673 fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
1674 : translated_formula) =
1675 formula_fold (SOME (kind <> Conjecture))
1676 (add_combterm_nonmonotonic_types ctxt level locality) combformula
1677 fun nonmonotonic_types_for_facts ctxt type_sys facts =
1678 let val level = level_of_type_sys type_sys in
1679 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1680 [] |> fold (add_fact_nonmonotonic_types ctxt level) facts
1681 (* We must add "bool" in case the helper "True_or_False" is added
1682 later. In addition, several places in the code rely on the list of
1683 nonmonotonic types not being empty. *)
1684 |> insert_type ctxt I @{typ bool}
1689 fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
1690 (s', T_args, T, pred_sym, ary, _) =
1692 val (T_arg_Ts, level) =
1694 Simple_Types level => ([], level)
1695 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1697 Decl (sym_decl_prefix ^ s, (s, s'),
1698 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1699 |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
1702 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1703 poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
1705 val (kind, maybe_negate) =
1706 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1708 val (arg_Ts, res_T) = chop_fun ary T
1709 val num_args = length arg_Ts
1711 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1713 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1714 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1715 fun should_keep_arg_type T =
1716 sym_needs_arg_types orelse
1717 not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
1719 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1721 Formula (preds_sym_formula_prefix ^ s ^
1722 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1723 CombConst ((s, s'), T, T_args)
1724 |> fold (curry (CombApp o swap)) bounds
1725 |> type_pred_combterm ctxt format type_sys res_T
1726 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1727 |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
1728 (K (K (K (K true)))) true
1729 |> n > 1 ? bound_tvars type_sys (atyps_of T)
1730 |> close_formula_universally
1735 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1736 poly_nonmono_Ts type_sys n s
1737 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1740 lightweight_tags_sym_formula_prefix ^ s ^
1741 (if n > 1 then "_" ^ string_of_int j else "")
1742 val (kind, maybe_negate) =
1743 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1745 val (arg_Ts, res_T) = chop_fun ary T
1747 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1748 val bounds = bound_names |> map (fn name => ATerm (name, []))
1749 val cst = mk_const_aterm format type_sys (s, s') T_args
1750 val atomic_Ts = atyps_of T
1752 (if pred_sym then AConn (AIff, map AAtom tms)
1753 else AAtom (ATerm (`I tptp_equal, tms)))
1754 |> bound_tvars type_sys atomic_Ts
1755 |> close_formula_universally
1757 (* See also "should_tag_with_type". *)
1758 fun should_encode T =
1759 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1761 Tags (Polymorphic, level, Lightweight) =>
1762 level <> All_Types andalso Monomorph.typ_has_tvars T
1764 val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
1765 val add_formula_for_res =
1766 if should_encode res_T then
1767 cons (Formula (ident_base ^ "_res", kind,
1768 eq [tag_with res_T (cst bounds), cst bounds],
1772 fun add_formula_for_arg k =
1773 let val arg_T = nth arg_Ts k in
1774 if should_encode arg_T then
1775 case chop k bounds of
1776 (bounds1, bound :: bounds2) =>
1777 cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
1778 eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
1781 | _ => raise Fail "expected nonempty tail"
1786 [] |> not pred_sym ? add_formula_for_res
1787 |> fold add_formula_for_arg (ary - 1 downto 0)
1790 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1792 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1793 poly_nonmono_Ts type_sys (s, decls) =
1796 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
1801 decl :: (decls' as _ :: _) =>
1802 let val T = result_type_of_decl decl in
1803 if forall (curry (type_instance ctxt o swap) T
1804 o result_type_of_decl) decls' then
1810 val n = length decls
1812 decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
1814 o result_type_of_decl)
1816 (0 upto length decls - 1, decls)
1817 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1818 nonmono_Ts poly_nonmono_Ts type_sys n s)
1820 | Tags (_, _, heaviness) =>
1824 let val n = length decls in
1825 (0 upto n - 1 ~~ decls)
1826 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1827 conj_sym_kind poly_nonmono_Ts type_sys n s)
1830 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1831 poly_nonmono_Ts type_sys sym_decl_tab =
1836 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1837 nonmono_Ts poly_nonmono_Ts type_sys)
1839 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1840 poly <> Mangled_Monomorphic andalso
1841 ((level = All_Types andalso heaviness = Lightweight) orelse
1842 level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types)
1843 | needs_type_tag_idempotence _ = false
1845 fun offset_of_heading_in_problem _ [] j = j
1846 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1847 if heading = needle then j
1848 else offset_of_heading_in_problem needle problem (j + length lines)
1850 val implicit_declsN = "Should-be-implicit typings"
1851 val explicit_declsN = "Explicit typings"
1852 val factsN = "Relevant facts"
1853 val class_relsN = "Class relationships"
1854 val aritiesN = "Arities"
1855 val helpersN = "Helper facts"
1856 val conjsN = "Conjectures"
1857 val free_typesN = "Type variables"
1859 val explicit_apply = NONE (* for experimental purposes *)
1861 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
1862 freshen_facts readable_names preproc hyp_ts concl_t facts =
1864 val (format, type_sys) = choose_format [format] type_sys
1865 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1866 translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1868 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1869 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
1870 val repair = repair_fact ctxt format type_sys sym_tab
1871 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1872 val repaired_sym_tab =
1873 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1875 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
1877 val poly_nonmono_Ts =
1878 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1879 polymorphism_of_type_sys type_sys <> Polymorphic then
1882 [TVar (("'a", 0), HOLogic.typeS)]
1883 val sym_decl_lines =
1884 (conjs, helpers @ facts)
1885 |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
1886 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1887 poly_nonmono_Ts type_sys
1889 0 upto length helpers - 1 ~~ helpers
1890 |> map (formula_line_for_fact ctxt format helper_prefix I false
1891 poly_nonmono_Ts type_sys)
1892 |> (if needs_type_tag_idempotence type_sys then
1893 cons (type_tag_idempotence_fact ())
1896 (* Reordering these might confuse the proof reconstruction code or the SPASS
1899 [(explicit_declsN, sym_decl_lines),
1901 map (formula_line_for_fact ctxt format fact_prefix ascii_of
1902 freshen_facts nonmono_Ts type_sys)
1903 (0 upto length facts - 1 ~~ facts)),
1904 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1905 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1906 (helpersN, helper_lines),
1908 map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
1910 (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
1914 CNF => ensure_cnf_problem
1915 | CNF_UEQ => filter_cnf_ueq_problem
1917 |> (if is_format_typed format then
1918 declare_undeclared_syms_in_atp_problem type_decl_prefix
1922 val (problem, pool) = problem |> nice_atp_problem readable_names
1923 val helpers_offset = offset_of_heading_in_problem helpersN problem 0
1925 map_filter (fn (j, {name, ...}) =>
1926 if String.isSuffix typed_helper_suffix name then SOME j
1928 ((helpers_offset + 1 upto helpers_offset + length helpers)
1930 fun add_sym_arity (s, {min_ary, ...} : sym_info) =
1932 case strip_prefix_and_unascii const_prefix s of
1933 SOME s => Symtab.insert (op =) (s, min_ary)
1939 case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
1940 offset_of_heading_in_problem conjsN problem 0,
1941 offset_of_heading_in_problem factsN problem 0,
1942 fact_names |> Vector.fromList,
1944 Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
1948 val conj_weight = 0.0
1949 val hyp_weight = 0.1
1950 val fact_min_weight = 0.2
1951 val fact_max_weight = 1.0
1952 val type_info_default_weight = 0.8
1954 fun add_term_weights weight (ATerm (s, tms)) =
1955 is_tptp_user_symbol s ? Symtab.default (s, weight)
1956 #> fold (add_term_weights weight) tms
1957 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
1958 formula_fold NONE (K (add_term_weights weight)) phi
1959 | add_problem_line_weights _ _ = I
1961 fun add_conjectures_weights [] = I
1962 | add_conjectures_weights conjs =
1963 let val (hyps, conj) = split_last conjs in
1964 add_problem_line_weights conj_weight conj
1965 #> fold (add_problem_line_weights hyp_weight) hyps
1968 fun add_facts_weights facts =
1970 val num_facts = length facts
1972 fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
1973 / Real.fromInt num_facts
1975 map weight_of (0 upto num_facts - 1) ~~ facts
1976 |> fold (uncurry add_problem_line_weights)
1979 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
1980 fun atp_problem_weights problem =
1981 let val get = these o AList.lookup (op =) problem in
1983 |> add_conjectures_weights (get free_typesN @ get conjsN)
1984 |> add_facts_weights (get factsN)
1985 |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
1986 [explicit_declsN, class_relsN, aritiesN]
1988 |> sort (prod_ord Real.compare string_ord o pairself swap)